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

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

Verifying the safety of the code is done by making sure there aren't any
alarms. You can compute and take advantage of functional dependencies
(or other analyses that exploit values) without verifying the safety of the
code.

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

Yes.

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

The difference is that (unless perhaps for very special compilation
platforms) the programmer probably did not divide by zero on purpose,
since that halts the program. Divisions by zero, if they
really happen, are the border cases that were not encountered during
testing (they would have been fixed if they had). The dependency flow
is probably correct despite the borderline cases. More importantly,
tool and human agree on what an incorrect execution is (an execution
that is abruptly terminated by a hardware exception is an
incorrect execution).

A "benign alarm", on the other hand, may be an inconsequential
idiom in the code. Tests did not reveal anything was wrong (indeed,
the code was working as the programmer intended). It can happen
in a large proportion of executions, and therefore hide most of the
behavior of the program from the analysis. The tool calls "incorrect"
some executions that look perfectly normal to the human, and
that the human would have liked to see included in the synthetic
results.

> Maybe a table in the documentation explaining for each alarm the
> assumption made and the conditions under which the analysis continues
> would help.

You are right, the only solution is to document these things more
precisely. I will try to improve this part of the documentation.

Pascal