Frama-C Bug Tracking System - Frama-C
View Issue Details
0000440Frama-CPlug-in > jessiepublic2010-04-04 01:062014-02-12 16:55
gava 
virgile 
normalminoralways
closedfixed 
Frama-C Beryllium-20090902 
Frama-C Carbon-20101201-beta1 
0000440: Pb with annot.c in
If you use frama-c -jessie annot.c where annot.c (from /test/cil.) == int fact(int n) { int r = 1 ; while ( n > 0 ) { //@ assert n > 0 ; before: r *= n-- ; //@ assert r == \at(r*n,before) ; } return r ; } Computation of VCs... File "why/annot.why", line 410, characters 74-82: Unbound label 'before' (which is true when looking the file)
The bug does not show up if the first assert is removed. So it seems the first assert "enclosed" the statement "before: r *= n-- ;" Which means that the problem might come from the Frama-C parser itself, which might have built a wrong AST. Virgile, any thoughts ?
No tags attached.
Issue History
2010-04-04 01:06gavaNew Issue
2010-04-04 01:06gavaStatusnew => assigned
2010-04-04 01:06gavaAssigned To => cmarche
2010-04-06 10:27cmarcheAdditional Information Updated
2010-05-10 16:45monateAssigned Tocmarche => virgile
2010-05-10 16:47monateNote Added: 0000821
2010-05-11 16:12virgileNote Added: 0000829
2010-05-12 00:45monateNote Added: 0000831
2010-06-02 11:18virgileNote Added: 0000893
2010-06-02 11:45svnCheckin
2010-06-02 11:45svnStatusassigned => resolved
2010-06-02 11:45svnResolutionopen => fixed
2010-12-10 15:47signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-10 15:47signolesAdditional Information Updated
2010-12-17 19:35signolesStatusresolved => closed

Notes
(0000821)
monate   
2010-05-10 16:47   
This is a bug of the AST elaboration. "frama-c -print -debug 1" outputs incorrectly imbricated blocks. int fact(int n ) { int r ; int tmp ; /*sid:1*/ r = 1; /*sid:2*/ while (1) { /*sid:4*/ if (n > 0) { } else { /*sid:5*/ break; } /*sid:6*/ /*@ assert (n > 0); */ ; /*sid:7*/ { /* */ before: /*sid:8*/ { /*undefined sequence*/ /*sid:9*/ /*block:begin*/ { /* */ /*sid:10*/ tmp = n; /*sid:11*/ n -= 1; } /*block:end*/ /*effects: n <- */ /*sid:12*/ r *= tmp; /*effects: r <- tmp*/ } } /*sid:13*/ /*@ assert (r ? \at(r*n,before)); */ ; } /*sid:14*/ return (r); }
(0000829)
virgile   
2010-05-11 16:12   
It's not incorrect. The annotation is tied to the next statement, which happens to be split by CIL, and is thus enclosed in a block to preserve its semantics (not a problem for assert, but with an ensures you definitely do not want it to be tied to tmp = n;)
(0000831)
monate   
2010-05-12 00:45   
I think you may have lissed the point. Annotation in sid 13 refers to a label "before" in sid 8. But the scoping rule of logic label prevents sid 13 from mentioning a label _inside_ sid 7. By the way the output is not parsable: this really seems to be a bug.
(0000893)
virgile   
2010-06-02 11:18   
A fix is about to be commited, but this slightly changes how annotations are handled wrt labels. See http://bts.frama-c.com/wiki.php?id=440 for more information/discussion