--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Alt Ergo - Problem



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