--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue on value analysis with loops



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