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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Sat, 3 Oct 2015 20:50:25 +0200
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB172@Mail1.FCMD.local>
  • 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>
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.