0000440: Pb with annot.c in - Frama-C Bug Tracking System

(0000821)
monate (reporter)
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 (developer)
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 (reporter)
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 (developer)
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

Issue History
Date Modified	Username	Field	Change
2010-04-04 01:06	gava	New Issue
2010-04-04 01:06	gava	Status	new => assigned
2010-04-04 01:06	gava	Assigned To	=> cmarche
2010-04-06 10:27	cmarche	Additional Information Updated
2010-05-10 16:45	monate	Assigned To	cmarche => virgile
2010-05-10 16:47	monate	Note Added: 0000821
2010-05-11 16:12	virgile	Note Added: 0000829
2010-05-12 00:45	monate	Note Added: 0000831
2010-06-02 11:18	virgile	Note Added: 0000893
2010-06-02 11:45	svn	Checkin
2010-06-02 11:45	svn	Status	assigned => resolved
2010-06-02 11:45	svn	Resolution	open => fixed
2010-12-10 15:47	signoles	Fixed in Version	=> Frama-C Carbon-20101201-beta1
2010-12-10 15:47	signoles	Additional Information Updated
2010-12-17 19:35	signoles	Status	resolved => closed

Notes
(0000821) monate (reporter) 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(rn,before)); / ; } /sid:14*/ return (r); }

(0000829) virgile (developer) 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 (reporter) 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 (developer) 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

Relationships