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