--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Example for jessie



> There is indeed one property that is false in the contract that you
> wrote, which is ?\result >= 0 in the "minus" behavior.

I wrote this before testing it, and sure enough, this is not how things
work in Jessie (but they work this way in the value analysis,
unless using -val-signed-overflow-alarms). The problem is
divided by Jessie into "Safety" and "Functional properties" and
it's one of the properties for safety (the one that says that z = -x;
does not overflow) that remains unproved. And yes, GWhy shows
which property fails to be proved. It's the
-integer_of_int32(x) <= 2147483647 which is a prerequisite for
safely computing -x.

Pascal