2021-03-01 04:52 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001100Frama-CKernelpublic2012-02-18 15:472014-02-12 16:59
Reporteryakobowski 
Assigned Toyakobowski 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0004724

yakobowski (manager)

2014-02-12 16:59

 Fix committed to stable/neon branch.
+Notes

-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
2012-02-20 10:53 svn Status assigned => resolved
2012-02-20 10:53 svn Resolution open => fixed
2012-02-20 13:27 svn
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master 22bff434
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master 4851e66a
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon 22bff434
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon 4851e66a
2014-02-12 16:59 yakobowski Note Added: 0004724
2014-02-12 16:59 yakobowski Status closed => resolved
+Issue History