Frama-C Bug Tracking System - Frama-C
View Issue Details
0001353Frama-CPlug-in > wppublic2013-01-30 16:582014-03-13 15:57
normalminorhave not tried
Frama-C Oxygen-20120901 
Frama-C Neon-20140301 
0001353: ACSL label LoopEntry not handled by WP
As 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 !
int G; //@ requires G == 0; ensures G == 0; void f (int c) { c++; L: //@ loop invariant G == \at (G, LoopEntry); while (c) c++; }
No tags attached.
Issue History
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

2014-02-12 16:57   
Fix committed to stable/neon branch.