View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001135 | Frama-C | Kernel | public | 2012-03-27 10:52 | 2014-02-12 16:59 | ||||
Reporter | patrick | ||||||||
Assigned To | patrick | ||||||||
Priority | normal | Severity | major | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
Summary | 0001135: unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel) | ||||||||
Description | Fresh labels and correct gotos are introduced when unrolling loop statements, but labels into code annotations are not handled correctly. Into the given example, the assertion is not unrolled correctly. | ||||||||
Additional Information | > cat file.c int X ; void main (int c) { for (int i = 0 ; i < 10 ;) { if (c) goto there ; X++; there: i++; //@ assert c==0 ==> \at(X,there)==i+1; } } > frama-c file.c -ulevel 1 -print int X; void main(int c) { int i; i = 0; if (! (i < 10)) { goto unrolling_2_loop; } if (c) { goto there_unrolling_4_loop; } X ++; there_unrolling_4_loop: /* internal */ i ++; /*@ assert c ? 0 ? \at(X,there) ? i+1; */ ; unrolling_3_loop: /* internal */ ; while (i < 10) { if (c) { goto there; } X ++; there: i ++; /*@ assert c ? 0 ? \at(X,there) ? i+1; */ ; } unrolling_2_loop: /* internal */ ; return; } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2012-03-27 10:52 | patrick | New Issue | |
2012-03-27 10:55 | patrick | Status | new => assigned |
2012-03-27 10:55 | patrick | Assigned To | => patrick |
2012-03-27 11:02 | signoles | Assigned To | patrick => virgile |
2012-03-28 08:12 | svn | ||
2012-03-28 08:12 | svn | Status | assigned => resolved |
2012-03-28 08:12 | svn | Resolution | open => fixed |
2012-04-02 13:59 | 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 | patrick | Source_changeset_attached | => framac master 70965aad |
2013-12-19 01:12 | patrick | Source_changeset_attached | => framac master 07b38ef2 |
2014-02-12 16:54 | patrick | Source_changeset_attached | => framac stable/neon 70965aad |
2014-02-12 16:54 | patrick | Source_changeset_attached | => framac stable/neon 07b38ef2 |
2014-02-12 16:59 | patrick | Note Added: 0004710 | |
2014-02-12 16:59 | patrick | Assigned To | virgile => patrick |
2014-02-12 16:59 | patrick | Status | closed => resolved |