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] Value analysis manual: questions and remarks

  • Subject: [Frama-c-discuss] Value analysis manual: questions and remarks
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 11 Jan 2011 04:13:13 +0100
  • In-reply-to: <87aaj8r1eg.fsf@linux-france.org>
  • References: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com> <87aaj8r1eg.fsf@linux-france.org>
There is also a new section in the Skein tutorial that was until today not
posted as an episode in the blog:

http://blog.frama-c.com/index.php?post/2011/01/10/Value-analysis-assisted-verification-of-output-variables-and-information-flow

> Another question: why the -val-signed-overflow-alarms is not activated
> by default and is not activated together with -val option (at least in
> Boron)? It is needed for the absolute value on int example (if (x < 0)
> z=-x; else z=x;)[1]. Because it is experimental? If so, what are the
> expected issues?

Historically, the detection of signed overflows was a high-impact change
that I was not sure wouldn't subtly affect existing behaviors of the analysis.
In addition, when initially implementing this option as "on by default", there
were regression tests, made of actual industrial code, that had their
analysis results changed because they were doing signed overflows on
purpose (expecting 2's complement behavior).

Lastly, there is the issue with derived analyses, of which
the options -deps and -out described in the new section of the tutorial
alluded to above are examples.

In these use cases, emitted alarms for conditions that
the programmer intended and did not feel were dangerous
mean that the results of the derived analyses are partial.
Since one way to use derived analyses is never to look at the
alarms, the verifier may never notice that some intended behaviors
of the target program are being omitted. I tried to discuss
the issue of "benign alarms" in these two posts, but I am not very
happy with the way it came out:
http://blog.frama-c.com/index.php?tag/unspecified%20behavior

Pascal