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] 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