--- layout: fc_discuss_archives title: Message 79 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?



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 lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Virgile Prevosto
Sent: Saturday, January 25, 2014 1:00 PM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [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


_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/2DRPoOd38srhpd7dT1OrOq9KVJeXObP33WapJeXObP33Xz9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSrp847mvjvW_8T76zB4seWZOW9EVpsV5MQszAn4-mKzp5dl557BgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdLEL9CMnWhEwdboL7ltbSbEiFpKB3iWq81ueGWn4Azh07vfXjB0yq86Uh_r4Z87-q8blgYArKrk4k4