Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001353Frama-CPlug-in > wppublic2013-01-30 16:582014-03-13 15:57
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001353: ACSL label LoopEntry not handled by WP
DescriptionAs said in the title, the ACSL label LoopEntry seems to be not handled by WP but it is accepted by the kernel. Using the -wp-warnings option I got warnings like : - Warning: Generalization of un-labeled values Reason: Some labels may escape the control flow but it took me some time to understand the problem. In the example below, changing LoopEntry by L in the loop invariant makes it work. BTW, in the example below, it doesn't work either when removing the first (c++;) statement !
Steps To Reproduce
Additional Informationint G; //@ requires G == 0; ensures G == 0; void f (int c) { c++; L: //@ loop invariant G == \at (G, LoopEntry); while (c) c++; }
TagsNo tags attached.
Relationships
Attached Files
Issue History
Date ModifiedUsernameFieldChange
2013-01-30 16:58AnneNew Issue
2013-01-30 16:58AnneStatusnew => assigned
2013-01-30 16:58AnneAssigned To => correnson
2013-07-26 14:49svnCheckin
2013-07-29 14:49virgileRelationship addedrelated to 0001462
2013-07-29 14:59virgileRelationship deletedrelated to 0001462
2013-07-30 17:46svnCheckin
2013-07-30 17:46svnStatusassigned => resolved
2013-07-30 17:46svnResolutionopen => fixed
2014-02-12 16:57corrensonNote Added: 0004562
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004562)
correnson   
2014-02-12 16:57   
Fix committed to stable/neon branch.