--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on January 2011 ---
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