|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000518||Frama-C||Plug-in > jessie||public||2010-06-22 15:52||2010-06-22 15:52|
|Assigned To||cmarche|| |
|Product Version||Frama-C Boron-20100401|| |
|Target Version||Fixed in Version|| |
|Summary||0000518: Loop assigns are not taken into account when proving a safety PO|
|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.
|Tags||No tags attached.|
|Attached Files|| loop_assigns.i [^] (439 bytes) 2010-06-22 15:52 [Show Content]