--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on June 2010 ---
> 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