--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on January 2011 ---
On Thu, Jan 20, 2011 at 3:57 PM, David MENTRE <dmentre at linux-france.org> wrote: > 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? Yes, almost: it is actually the "while" itself, not the join point after it. What is called "Next statement" in the context of "i=0" is actually a "while(1)" statement, which is transparently printed as "while(i<10)" by Frama-C. On this while statement, i takes the values 0,2,4,6,8,10, as the value 10 is pruned out only later, in an "if" inside the while. You can see that yourself by invoking frama-c with the option -kernel-debug 1 > 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 )? Yes. We implemented this new functionality both for the needs of a plugin, and to avoid having to explain this puzzling behavior :-) The new improved message will be present in the final release of Carbon, which is due in the next few weeks. -- Boris