Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000384Frama-CKernelpublic2010-01-29 17:132012-09-19 17:16
Reportergmelquio 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000384: Labels in loops are not unrolled
DescriptionFor the following testcase with revision 7516, the Jessie output doesn't contain copies of label L in the unrolled parts of the loop, causing the unrolled assertions to be dangling.

int main() {
  int i, j;
  j = 0;
  /*@ loop pragma UNROLL 4; */
  for (i = 0; i <= 2; ++i) {
    L:
    j = j + 1;
    //@assert j == \at(j,L) + 1;
  }
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000655)
virgile (developer)
2010-01-29 18:07

Distinct copies of the label are made in the code, but this is not reflected in the ACSL comment...
(0002831)
yakobowski (manager)
2012-04-05 01:00

This has been corrected recently by either Virgile or Patrick. Loop unrolling should be much more robust.

- Issue History
Date Modified Username Field Change
2010-01-29 17:13 gmelquio New Issue
2010-01-29 18:06 virgile Status new => assigned
2010-01-29 18:06 virgile Assigned To => virgile
2010-01-29 18:07 virgile Note Added: 0000655
2010-01-29 18:07 virgile Status assigned => acknowledged
2012-04-05 01:00 yakobowski Note Added: 0002831
2012-04-05 01:00 yakobowski Status acknowledged => resolved
2012-04-05 01:00 yakobowski Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker