strange warning "postcondition got status invalid"
ID0001369: This issue was created automatically from Mantis Issue 1369. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001369 | Frama-C | Plug-in > Eva | public | 2013-02-15 | 2014-03-13 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | Frama-C Neon-20140301 | Fixed in Version | Frama-C Neon-20140301 |
Description :
Running "frama-c -val ftest.c" on the attached program produces a "[value] Function foo: postcondition got status invalid" in line 6, although the ensures clause looks quite reasonable. (I don't understand the notion of a "postcondition status": shouldn't the postconditions of a function be satisfied automatically if all its preconditions are?) The warning disappears if the ensures clause in line 5 is removed or an appropriate function body (e.g. the one commented out at the end of line 6) is added.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information