Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
Attached Files

- Relationships

-  Notes
(0004562)
correnson (manager)
2014-02-12 16:57

Fix committed to stable/neon branch.

- 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 Checkin
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 Checkin
2013-07-30 17:46 svn Status assigned => resolved
2013-07-30 17:46 svn Resolution open => fixed
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker