Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000518Frama-CPlug-in > jessiepublic2010-06-22 15:522010-06-22 15:52
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000518: Loop assigns are not taken into account when proving a safety PO
DescriptionIn 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 InformationNote 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.
TagsNo tags attached.
Attached Files? file icon loop_assigns.i [^] (439 bytes) 2010-06-22 15:52 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-06-22 15:52 virgile New Issue
2010-06-22 15:52 virgile Status new => assigned
2010-06-22 15:52 virgile Assigned To => cmarche
2010-06-22 15:52 virgile File Added: loop_assigns.i

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker