Loop assigns are not taken into account when proving a safety PO
ID0000518: This issue was created automatically from Mantis Issue 518. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000518 | Frama-C | Plug-in > jessie | public | 2010-06-22 | 2010-06-22 |
| Reporter | virgile | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
In the program given below, the access to t[i] leads to a safety verification condition. However, the generated goal does not contain as hypothesis the fact that only the cell 0 to i-1 have been modified, and can not conclude that t[i] is still 1, so that no overflow can occur.
Might be a Why bug, though.
Additional Information :
Note that this is specific to safety VC. If you add an assert /*@ assert t[i]==0; */ before the assignment, the loop assigns is present in the hypotheses of the VC corresponding to the assert and all the proofs succeed.