Frama-C Bug Tracking System - Frama-C
View Issue Details
0000384Frama-CKernelpublic2010-01-29 17:132012-09-19 17:16
gmelquio 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Oxygen-20120901 
0000384: Labels in loops are not unrolled
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; } }
No tags attached.
Issue History
2010-01-29 17:13gmelquioNew Issue
2010-01-29 18:06virgileStatusnew => assigned
2010-01-29 18:06virgileAssigned To => virgile
2010-01-29 18:07virgileNote Added: 0000655
2010-01-29 18:07virgileStatusassigned => acknowledged
2012-04-05 01:00yakobowskiNote Added: 0002831
2012-04-05 01:00yakobowskiStatusacknowledged => resolved
2012-04-05 01:00yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

Notes
(0000655)
virgile   
2010-01-29 18:07   
Distinct copies of the label are made in the code, but this is not reflected in the ACSL comment...
(0002831)
yakobowski   
2012-04-05 01:00   
This has been corrected recently by either Virgile or Patrick. Loop unrolling should be much more robust.