Labels in loops are not unrolled
ID0000384: This issue was created automatically from Mantis Issue 384. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000384 | Frama-C | Kernel | public | 2010-01-29 | 2012-09-19 |
| Reporter | gmelquio | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
For the following testcase with revision 7516, the Jessie output doesn't contain copies of label L in the unrolled parts of the loop, causing the unrolled assertions to be dangling.
int main() { int i, j; j = 0; /*@ loop pragma UNROLL 4; */ for (i = 0; i <= 2; ++i) { L: j = j + 1; //@assert j == \at(j,L) + 1; } }