Frama-C Bug Tracking System - Frama-C
View Issue Details
0001100Frama-CKernelpublic2012-02-18 15:472014-02-12 16:59
yakobowski 
yakobowski 
lowminoralways
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001100: Loop unrolling sub-optimal in presence of some labels
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.
No tags attached.
Issue History
2012-02-18 15:47yakobowskiNew Issue
2012-02-18 15:48yakobowskiStatusnew => assigned
2012-02-18 15:48yakobowskiAssigned To => yakobowski
2012-02-20 10:53svnCheckin
2012-02-20 10:53svnStatusassigned => resolved
2012-02-20 10:53svnResolutionopen => fixed
2012-02-20 13:27svnCheckin
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:59yakobowskiNote Added: 0004724
2014-02-12 16:59yakobowskiStatusclosed => resolved

Notes
(0004724)
yakobowski   
2014-02-12 16:59   
Fix committed to stable/neon branch.