--- layout: fc_discuss_archives title: Message 36 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



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