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 !
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

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

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:49svn
2013-07-29 14:49virgileRelationship addedrelated to 0001462
2013-07-29 14:59virgileRelationship deletedrelated to 0001462
2013-07-30 17:46svn
2013-07-30 17:46svnStatusassigned => resolved
2013-07-30 17:46svnResolutionopen => fixed
2013-12-19 01:11corrensonSource_changeset_attached => framac master 65231d4d
2013-12-19 01:11Source_changeset_attached => framac master a0206924
2014-02-12 16:53corrensonSource_changeset_attached => framac stable/neon 65231d4d
2014-02-12 16:53Source_changeset_attached => framac stable/neon a0206924
2014-02-12 16:57corrensonNote Added: 0004562
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed