0001100: Loop unrolling sub-optimal in presence of some labels

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001100

Frama-C

Kernel

public

2012-02-18 15:47

2014-02-12 16:59

Reporter

yakobowski

Assigned To

yakobowski

Priority

low

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Nitrogen-20111001

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0001100: Loop unrolling sub-optimal in presence of some labels

Description

Repro 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.

Tags

No 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