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

Hello,

> In C + ACSL as for me the equal to formal program is:
> /*@ requires \true;

This is correct, but you can also write nothing.

> ?@ assigns ?\nothing;
> ?@ behavior plus:
> ?@ @ assumes x >= 0;
> ?@ @ ensures \result == ?x;
> ?@ @ ensures \result >= ?0;
> ?@ behavior minus:
> ?@ @ assumes x < 0;
> ?@ @ ensures \result == -x;
> ?@ @ ensures \result >= ?0;
> ?@ complete behaviors plus, minus;
> ?@ disjoint behaviors plus, minus;
> ?@ */
> int z_abs_x(const int x)
> {
> ?int z;
> ?if (x < 0) ? ? ? ? z = -x;
> ?else if (x >= 0) ? z = ?x;
> ?return z;
> }
> After validation I receive 14 verification conditions, 13 are valid and 1 is unknown. And this result is shown by all Automatic Theorem Provers (Alt-Ergo, CVC3, Z3, yices).
> What can be wrong in my annotations?

Wow! You have stumbled on the example that I use all the time to show
how formal specifications and verification can be useful.
There is indeed one property that is false in the contract that you
wrote, which is  \result >= 0 in the "minus" behavior. Gwhy shows you
this...

With the default analysis parameters where ints are assumed to range
from -2^31 to +2^31-1, the input value that makes the function behave
differently than imposed by the contract is -2^31. The operation z =
-x; overflows in this case. Technically the result is undefined in the
C99 standard, although most compilers will generate code that gives z
the value 2^31-1.

You can make the function correct with respect with the contract by
changing the contract :)
For instance, specify that the function only accepts values from
-2^31+1 to 2^31-1:

requires -2147483647 <= x <= 2147483647 ;

Pascal