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: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 11 Jan 2011 15:37:43 +0100
  • In-reply-to: <AANLkTi=MoQkxxWKW8AHT7TeiF-+vUxjg8st5T+nLSsJP@mail.gmail.com>
  • References: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com> <87aaj8r1eg.fsf@linux-france.org> <AANLkTi=MoQkxxWKW8AHT7TeiF-+vUxjg8st5T+nLSsJP@mail.gmail.com>
Hello Pascal,

2011/1/11 Pascal Cuoq <pascal.cuoq at gmail.com>:
> 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

This post is not clear. On one side you say: "Although the outputs and
dependencies computations rely on the results of the value analysis,
they do not require you to check each of the alarms generated by the
value analysis."

On the other side, you say: "(which is done by making sure that the
value analysis emits no alarm or by checking the emitted alarms with
alternative techniques)".

So when using -deps option, is it mandatory or not to look at raised
alarms? I would say one should look at alarms. If so, what did you
meant with the first sentence?

>> 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).

I would have leant on the safe side (like recent Jessie module
regarding termination) and made this option active by default. But I
haven't used Frama-C on real code so I'll trust you on this.

> 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.

If I understand correctly, you are saying that the -deps like analyses
can be trusted if one is using the modulo integer model, i.e. without
-val-signed-overflow-alarms option. On the other side, if one is using
the -val-signed-overflow-alarms option, the -deps analysis might
produce erroneous result if some alarms are raised during the
analysis. Am I correct?

> 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

Well, at least I think I understand the issue regarding int overflow.
But I have the feeling that the issue is the same for other alarms.
For example, for division by zero, the analysis might continue or not
on a branch depending on whether the value analysis can determine if
the divisor is not only or only zero.

Maybe a table in the documentation explaining for each alarm the
assumption made and the conditions under which the analysis continues
would help. Or a general explanation of value analysis behaviour
regarding several branches, based on a simple example with an alarm on
one branch.

Best regards,
david