| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | 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 | | 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 
Relationships