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] Frama-C: Detecting unreachable code?

Hello,

Le ven. 24 janv. 2014 14:05:14 CET,
Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

> I'm not sure how unsigned types are handled by Frama-c. Bit confused
> why the following code worked for the "neg" behavior,
> 
> I was hoping that the tool will report an invalid comparison between
> unsigned int with < 0, or something like that, but the "neg" contract
> worked.

> typedef unsigned short int uint16;
> 
> /*@
>  behavior neg:
>    assumes i < 0;
>    ensures \result == -1;
...
> */
> int sign(uint16 i)

WP indeed will happily prove the behavior valid. In fact, it is meant
to prove that if the function is called in a state that satisfies the
assumes then the state at the end of execution will be satisfy the
ensures. Thus, if the assumes clause is always false, the proof is
trivial: ex falso, quod libet...
In order to detect such erroneous assumes, you might replace the
ensures clause by ensures \false: if WP is still able to prove it,
something fishy is going on, either in the spec or in the code.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile