Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Alt Ergo - Problem

  • Subject: [Frama-c-discuss] Alt Ergo - Problem
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Sat, 3 Oct 2015 15:30:56 -0400
  • In-reply-to: <5FB61E09-69A2-41FC-97F1-621B59B146F7@gmail.com>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C766044995@Mail1.FCMD.local> <52D1556E.7010400@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76604499E@Mail1.FCMD.local> <52D15C30.40602@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB78@Mail1.FCMD.local> <52D15D7F.3000800@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB79@Mail1.FCMD.local> <52D16266.3040201@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB7A@Mail1.FCMD.local> <52D16676.3000200@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB7B@Mail1.FCMD.local> <52D16727.8030804@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C7660449A2@Mail1.FCMD.local> <52D4D24E.8060007@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DC58@Mail1.FCMD.local> <52D55374.8020404@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682E584@Mail1.FCMD.local> <52EF36F1.7020100@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB147@Mail1.FCMD.local> <561000C3.2020700@gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB172@Mail1.FCMD.local> <5FB61E09-69A2-41FC-97F1-621B59B146F7@gmail.com>
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