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 17:17:37 +0100
  • In-reply-to: <AANLkTi=J6M2zmDG9AeijKibNrTQRG=94o13umdj98Rjf@mail.gmail.com>
  • References: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com> <87aaj8r1eg.fsf@linux-france.org> <AANLkTi=MoQkxxWKW8AHT7TeiF-+vUxjg8st5T+nLSsJP@mail.gmail.com> <AANLkTinft2xqd3Zr2atVuY2bF84KPidpeuiAE_XaOWJV@mail.gmail.com> <AANLkTi=J6M2zmDG9AeijKibNrTQRG=94o13umdj98Rjf@mail.gmail.com>
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.