--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on January 2014 ---
[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