Statement contract and "hiding" of statement
ID0000399: This issue was created automatically from Mantis Issue 399. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000399 | Frama-C | Plug-in > jessie | public | 2010-02-06 | 2010-04-19 |
| Reporter | dpariente | Assigned To | cmarche | 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 :
Hello,
On the following annotated code:
int main(int x) { int y=0; //@ assigns y; ensures y==3; y=x; //@ assert y>0; }
analyzed by: frama-c -jessie foo.c assert y>0 is not discharged (no matter the preceding statement contract is valid or not).
Indeed, statement contract (assigns y; ensures y==3;) doesn't seem to be taken into account as it does not appear in .jc file.