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

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