--- layout: fc_discuss_archives title: Message 13 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



Hello Pascal,

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

That's clearer, thanks.

Regards,
d.