View Issue Details [ Jump to Notes ] | [ 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 | ||||||
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 |
|
![]() |
|
yakobowski (manager) 2014-02-12 16:59 |
Fix committed to stable/neon branch. |
![]() |
|||
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 | ||
2012-02-20 10:53 | svn | Status | assigned => resolved |
2012-02-20 10:53 | svn | Resolution | open => fixed |
2012-02-20 13:27 | svn | ||
2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
2012-09-19 17:16 | signoles | Status | resolved => closed |
2013-12-19 01:12 | yakobowski | Source_changeset_attached | => framac master 22bff434 |
2013-12-19 01:12 | yakobowski | Source_changeset_attached | => framac master 4851e66a |
2014-02-12 16:54 | yakobowski | Source_changeset_attached | => framac stable/neon 22bff434 |
2014-02-12 16:54 | yakobowski | Source_changeset_attached | => framac stable/neon 4851e66a |
2014-02-12 16:59 | yakobowski | Note Added: 0004724 | |
2014-02-12 16:59 | yakobowski | Status | closed => resolved |