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

[Frama-c-discuss] Evaluation of an expression?



Hello,

In a course, I would like to illustrate how one can control precision
of Frama-C value analysis. I'm using following example:
"""
int x, y, z;

void main(int c)
{
  x = c ? 0 : 1;
  y = x ? 0 : 1;
  z = 10 / (x - y);
}
"""

I'm using Frama-C Nitrogen or Carbon (depending of the machine). In
both cases, I'm calling Frama-C with:
  frama-c-gui -val possible-zero.c
and
  frama-c-gui -val -slevel 2 possible-zero.c

In the second case, the assertion "(x - y) != 0" is not inserted,
which is I wanted.

However, if I do "Evalute expression" at "z = ..." for "x - y", I get
{-1; 0; 1; }. I would have expected {-1; 1;} as the assertion is not
inserted.

Any explanation?

Best regards,
david