Value may be incorrect in presence of several ensures
ID0000689: This issue was created automatically from Mantis Issue 689. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000689 | Frama-C | Plug-in > Eva | public | 2011-01-26 | 2014-02-12 |
| Reporter | signoles | Assigned To | monate | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20101202-beta2 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
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.