| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000689 | Frama-C | Plug-in > Eva | public | 2011-01-26 17:50 | 2014-02-12 16:59 | ||||
| Reporter | signoles | ||||||||
| Assigned To | monate | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Carbon-20101202-beta2 | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000689: Value may be incorrect in presence of several ensures | ||||||||
| Description | If a function has 1 valid ensure and 1 invalid ensure, the GUI says that both ensures are invalid. | ||||||||
| Steps To Reproduce | ==== a.c ==== /*@ ensures \result == 0; @ ensures \false; @ */ int f(void) { return 0; } void main(void) { f(); } ============== $ frama-c-gui a.c Then check the property status of both ensures. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
pascal (reporter) 2011-01-26 21:38 |
Thinking more about it, I am not sure this is incorrectness per se. Because if one "ensures" is invalid, then everytime the execution reaches the end of the function, you have false in as an hypothesis. That is, the other "ensures" may be valid, but it is not wrong to say that it is also invalid. It's still worth fixing. |
|
monate (reporter) 2014-02-12 16:59 |
Fix committed to stable/neon branch. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-01-26 17:50 | signoles | New Issue | |
| 2011-01-26 17:50 | signoles | Status | new => assigned |
| 2011-01-26 17:50 | signoles | Assigned To | => monate |
| 2011-01-26 18:09 | signoles | Product Version | => Frama-C Carbon-20101202-beta2 |
| 2011-01-26 21:38 | pascal | Note Added: 0001424 | |
| 2011-03-30 14:48 | svn | ||
| 2011-03-30 14:48 | svn | Status | assigned => resolved |
| 2011-03-30 14:48 | svn | Resolution | open => fixed |
| 2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
| 2011-10-10 14:14 | signoles | Status | resolved => closed |
| 2013-12-19 01:12 | svn | Source_changeset_attached | => framac master b1ecd87f |
| 2014-02-12 16:54 | monate | Source_changeset_attached | => framac stable/neon b1ecd87f |
| 2014-02-12 16:59 | monate | Note Added: 0004817 | |
| 2014-02-12 16:59 | monate | Status | closed => resolved |
| 2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |
| Issue History |