| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ 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 | |
| Platform | | OS | | OS Version | |
| 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 | |
|
Relationships 
Relationships