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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Thu, 20 Jan 2011 16:18:06 +0100
  • In-reply-to: <AANLkTi=d6Jmq-b9cKMwsrkqjdXp22=0UhAvj=0SRifHo@mail.gmail.com>
  • References: <AANLkTi=d6Jmq-b9cKMwsrkqjdXp22=0UhAvj=0SRifHo@mail.gmail.com>
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