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.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information