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.