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

[Frama-c-discuss] Value analysis manual: questions and remarks



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