| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000877 | Frama-C | Plug-in > RTE | public | 2011-07-06 10:10 | 2012-05-16 18:22 | ||||
| Reporter | yakobowski | ||||||||
| Assigned To | pherrmann | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000877: RTE does not generate assertions for non initialized arguments | ||||||||
| Description | Calling the WP (or Jessie for that matter) on the following code results in all goals being proven. Yet, there is a RTE on the call to max, because a is not initialized. I tend to think that -rte-precond should add \initialized(a) and \initialized(b) to the local contract for the call to max, but there is perhaps another better way. Anyway, either RTE or the WP are faulty here. /*@ ensures \result == (a < b ? a : b); */ int max(int a, int b) { return (a < b ? a : b); } int main () { int a; int b = 2; return max (a, b); } | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
yakobowski (manager) 2011-07-06 10:10 |
(Wp called with -wp-rte.) |
|
pherrmann (reporter) 2011-08-22 10:15 |
See svn 14739 for documentation update: RTE does not report usage of non initialized automatic variables. Would require a dataflow analysis to avoid an excessive number of generated annotations. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-07-06 10:10 | yakobowski | New Issue | |
| 2011-07-06 10:10 | yakobowski | Status | new => assigned |
| 2011-07-06 10:10 | yakobowski | Assigned To | => pherrmann |
| 2011-07-06 10:10 | yakobowski | Note Added: 0002010 | |
| 2011-08-22 10:15 | pherrmann | Note Added: 0002152 | |
| 2011-08-22 10:15 | pherrmann | Status | assigned => resolved |
| 2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
| 2011-10-10 14:14 | signoles | Status | resolved => closed |
| 2012-05-16 18:22 | signoles | Resolution | open => fixed |
| Issue History |