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: dmentre at linux-france.org (David MENTRE)
  • Date: Thu, 20 Jan 2011 15:57:11 +0100
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