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: Mon, 10 Jan 2011 20:42:31 +0100
  • In-reply-to: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com> (David MENTRE's message of "Mon, 10 Jan 2011 15:18:31 +0100")
  • References: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com>
Hello,

David MENTRE <dmentre at linux-france.org> writes:

> I read the value analysis manual of Frama-C Boron and I have therefore
> several questions and remarks:

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?

Best regards,
david

[1] BTW, in section 5.2, "Absence of arithmetic overflows" paragraph,
    the example does no work without this -val-signed-overflow-alarms
    option: no alarm is raised with only -val option.
"""
int abs ( int x ) {
if (x <0) x = -x ;
return x;
}
"""
-- 
GPG/PGP key: A3AD7A2A David MENTRE <dmentre at linux-france.org>
 5996 CC46 4612 9CA4 3562  D7AC 6C67 9E96 A3AD 7A2A