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.
|ID0000518||Frama-C||Plug-in > jessie||public||2010-06-22||2010-06-22|
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||-|
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.