2021-03-02 01:45 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001353Frama-CPlug-in > wppublic2014-03-13 15:57
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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.
Attached Files

-Relationships
+Relationships

-Notes

~0004562

correnson (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2013-01-30 16:58 Anne New Issue
2013-01-30 16:58 Anne Status new => assigned
2013-01-30 16:58 Anne Assigned To => correnson
2013-07-26 14:49 svn
2013-07-29 14:49 virgile Relationship added related to 0001462
2013-07-29 14:59 virgile Relationship deleted related to 0001462
2013-07-30 17:46 svn
2013-07-30 17:46 svn Status assigned => resolved
2013-07-30 17:46 svn Resolution open => fixed
2013-12-19 01:11 correnson Source_changeset_attached => framac master 65231d4d
2013-12-19 01:11 Source_changeset_attached => framac master a0206924
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon 65231d4d
2014-02-12 16:53 Source_changeset_attached => framac stable/neon a0206924
2014-02-12 16:57 correnson Note Added: 0004562
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History