--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on January 2011 ---
Yes. I'm glad that someone understood what this post was about. I was afraid it was a bit obscure because it refers to a problem you mostly only notice when preparing demos of the value analysis. Not that the "afternoon" alluded to in the post took place after the release of Carbon 20101202. You'll have to wait until the next release. Pascal On 20 janv. 2011, at 15:57, David MENTRE <dmentre at linux-france.org> wrote: > Hello, > > I'm using Frama-C Boron. > > I have following program: > ------------- > void main(void) > { > int i; > > for (i=0; i<10; i++) { > i = i + 1; > } > } > ------------- > > I apply on it value analysis: > frama-c-gui -val one-loop.c > > In the resulting analysed program (with a while construct), if I > select the "i" in "i=0;" statement (line 4), Frama-C tells: > """ > Before statement: > i ? UNINITIALIZED > At next statement: > i ? {0; 2; 4; 6; 8; 10; } > """ > > I would expect to have "At next statement: i ? {0; }". It seems that > the "next statement" for the "i=0;" statement is at the join point > after the "while ..." statement. > > Is my reasoning correct? > > Is this this issue which is fixed in Carbon release (according to > http://blog.frama-c.com/index.php?post/2011/01/11/Seven-errors-game )? > > Yours, > david > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss