View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000384 | Frama-C | Kernel | public | 2010-01-29 17:13 | 2012-09-19 17:16 | ||||
Reporter | gmelquio | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
Summary | 0000384: Labels in loops are not unrolled | ||||||||
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; } } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
virgile (developer) 2010-01-29 18:07 |
Distinct copies of the label are made in the code, but this is not reflected in the ACSL comment... |
yakobowski (manager) 2012-04-05 01:00 |
This has been corrected recently by either Virgile or Patrick. Loop unrolling should be much more robust. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2010-01-29 17:13 | gmelquio | New Issue | |
2010-01-29 18:06 | virgile | Status | new => assigned |
2010-01-29 18:06 | virgile | Assigned To | => virgile |
2010-01-29 18:07 | virgile | Note Added: 0000655 | |
2010-01-29 18:07 | virgile | Status | assigned => acknowledged |
2012-04-05 01:00 | yakobowski | Note Added: 0002831 | |
2012-04-05 01:00 | yakobowski | Status | acknowledged => resolved |
2012-04-05 01:00 | yakobowski | Resolution | open => fixed |
2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
2012-09-19 17:16 | signoles | Status | resolved => closed |