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] Evaluation of an expression?

  • Subject: [Frama-c-discuss] Evaluation of an expression?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 9 Jan 2012 09:21:17 +0100
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