Frama-C Bug Tracking System - Frama-C
View Issue Details
0000518Frama-CPlug-in > jessiepublic2010-06-22 15:522010-06-22 15:52
virgile 
cmarche 
normalminoralways
assignedopen 
Frama-C Boron-20100401 
 
0000518: Loop assigns are not taken into account when proving a safety PO
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.
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.
No tags attached.
? loop_assigns.i (439) 2010-06-22 15:52
https://bts.frama-c.com/file_download.php?file_id=98&type=bug
Issue History
2010-06-22 15:52virgileNew Issue
2010-06-22 15:52virgileStatusnew => assigned
2010-06-22 15:52virgileAssigned To => cmarche
2010-06-22 15:52virgileFile Added: loop_assigns.i

There are no notes attached to this issue.