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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 9 Jan 2012 09:32:31 +0100
  • In-reply-to: <CAC3Lx=ZDCuZ2aqUCMkiyAF7tSaRTtC4d9ancT4hkbTmQDZzufA@mail.gmail.com>
  • References: <CAC3Lx=ZDCuZ2aqUCMkiyAF7tSaRTtC4d9ancT4hkbTmQDZzufA@mail.gmail.com>
Hello David,

On Mon, Jan 9, 2012 at 9:21 AM, David MENTRE <dmentre at linux-france.org>wrote:

> int x, y, z;
>
> void main(int c)
> {
>  x = c ? 0 : 1;
>  y = x ? 0 : 1;
>  z = 10 / (x - y);
> }
>   frama-c-gui -val -slevel 2 possible-zero.c
>
>   ... 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.
>

This falls under paragraph "Propagation of the displayed states",
in section "What the value analysis does not provide",
page 46 of the manual, although that paragraph is written backwards
with respect to your question.

If the value analysis provided propagation of the displayed states,
then what you observe in the GUI would be guaranteed to have
been propagated, and you would have an assertion for the division.
As it is, in your example, the GUI shows an over-approximation of
what has really been propagated (that is, once x==1 and y==0
and once x==0 and y==1). No alarm was emitted because the propagated
states were not dangerous for the division.

Your example seems to come from there and I do not really see
how I should make it clearer than:

"The values available through the graphical and programmatic interfaces do
not come from
a single propagated state but from the union of several states that the
analyzer may have
propagated separately. As a consequence, it should not be assumed that the
?state? displayed
at a particular program point has been propagated."

But your suggestions are welcome.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120109/c2245d3c/attachment.htm>