--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 2015 ---
I think something is fishy. I changed my assert to x*x >= 0. The output is true. int x = (1 << 16)-1; /* two power 16 - 1 */ /*@ assert x*x >= 0 ;*/ Goal Assertion (file square_neg.c, line 10): Assume { (* Domain *) Type: (is_sint32 x_0). (* Block In *) Have: ta_retres_0 /\ ta_x_0 /\ (not ta_retres_2) /\ (not ta_x_2). (* square_neg.c:6: Assignment *) Have: x_0=(to_sint32 ((to_sint32 (lsl 1 16))-1)). } Prove: 0<=(x_0*x_0). Prover Alt-Ergo returns Valid (20ms) (13) frama-c -wp square_neg.c -wp-no-check -wp-no-simpl -wp-print -wp-model "Typed,var,cint,real" -wp-no-let -wp-no-pruning -wp-no-clean -wp-no-bits -wp-split -wp-out t16 -wp-prover alt-ergo -----Original Message----- From: Frama-c-discuss [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal Cuoq Sent: Saturday, October 03, 2015 2:50 PM To: Frama-C public discussion Cc: Mohamed Iguernlala Subject: Re: [Frama-c-discuss] Alt Ergo - Problem Hello, I'm going to leave the WP aspects of your question to others but > int main() > { > int x = (1 << 16)-1; /* two power 16 - 1 */ > > // why is this not ok? > > /*@ assert x*x < 0 ;*/ > > assert(x*x < 0); /* This is true when I run using gcc and then a.out */ } It is undefined behavior. The fact that it produces this result for one compilation doesn't mean anything. Even, and I can hardly emphasize this enough, if you know that you are targeting a 2's complement architecture. _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://cp.mcafee.com/d/k-Kr6xASyMMOYqenDTDPtPqtTAnC67QkPqtTAnC67T6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISYwMDt5N_HY-qehPPXB-LsLtd7AkS7TbK9Zh5dqWqJTCul3PWApmU6CQjq9K_8KcKnhhshsdTdw0PVkDjybE07-B2cJVSe2qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JMQszDzobZ8Qg6BInzGKBX5Q9kITixFtd40wvcQg3kidjh0nd40mzkwvWFJyVKMFFoJYxIE_1