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?

Thanks, but replacing the ensures by \false still proves correct.

The code is incorrect (comparing an unsigned int to < 0) but  WP is not pointing me this error.  

-----Original Message-----
From: frama-c-discuss-bounces at [mailto:frama-c-discuss-bounces at] On Behalf Of Virgile Prevosto
Sent: Saturday, January 25, 2014 1:00 PM
To: frama-c-discuss at
Subject: Re: [Frama-c-discuss] Frama-C: Detecting unreachable code?


Le ven. 24 janv. 2014 14:05:14 CET,
Dharmalingam Ganesan <dganesan at> 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.

Frama-c-discuss mailing list
Frama-c-discuss at