Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Issue on value analysis with loops
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Thu, 20 Jan 2011 16:14:54 +0100
  • In-reply-to: <AANLkTi=d6Jmq-b9cKMwsrkqjdXp22=0UhAvj=0SRifHo@mail.gmail.com>
  • References: <AANLkTi=d6Jmq-b9cKMwsrkqjdXp22=0UhAvj=0SRifHo@mail.gmail.com>
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