Loop unrolling sub-optimal in presence of some labels
ID0001100: This issue was created automatically from Mantis Issue 1100. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001100 | Frama-C | Kernel | public | 2012-02-18 | 2014-02-12 |
| Reporter | yakobowski | Assigned To | yakobowski | Resolution | fixed |
| Priority | low | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
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.