Wrong postconditions are "valid according to value analysis"
ID0000372: This issue was created automatically from Mantis Issue 372. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000372 | Frama-C | Plug-in > Eva | public | 2010-01-13 | 2010-04-13 |
| Reporter | gmelquio | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
/*@ ensures \result == 1; */ int main() { return 0; }
When clicking on the "ensures" clause, Frama-C GUI (r7298) reports:
This is an ensures clause. Status: Valid according to value analysis
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information