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