Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001100Frama-CKernelpublic2012-02-18 15:472014-02-12 16:59
Reporteryakobowski 
Assigned Toyakobowski 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001100: Loop unrolling sub-optimal in presence of some labels
DescriptionRepro case :
-------------------p.c---------------
void main () {
  int x = 0;
 L:
    while(x < 4) { x++; }
}
-------------------------------------

frama-c -ulevel 2 -print p.c results in

void main(void)
{
  int x;
  x = 0;
  if (! (x < 4)) { goto unrolling_2_loop; }
  x ++;
  unrolling_4_loop: /* internal */ ;
  if (! (x < 4)) { goto unrolling_2_loop; }
  x ++;
  unrolling_3_loop: /* internal */ ;
  L:
  while (x < 4) { x ++; }
  unrolling_2_loop: /* internal */ ;
  return;
}

The loop is unrolled before the label L. This is not incorrect per se, and even seems to be ok inside 'switch'. However, this will rarely be what the user expects and needs.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004724)
yakobowski (manager)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-02-18 15:47 yakobowski New Issue
2012-02-18 15:48 yakobowski Status new => assigned
2012-02-18 15:48 yakobowski Assigned To => yakobowski
2012-02-20 10:53 svn Checkin
2012-02-20 10:53 svn Status assigned => resolved
2012-02-20 10:53 svn Resolution open => fixed
2012-02-20 13:27 svn Checkin
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:59 yakobowski Note Added: 0004724
2014-02-12 16:59 yakobowski Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker