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:16: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>
Thanks, Pascal. 

I'm looking into the practice problem 2.44 (c) from the wonderful book "Computer Systems - A Programmer's Perspective" - 2nd edition.

They gave this problem - argue that it is true for all values of x, or give values of x for which it is false. I'm also CCing the authors of this book Prof. O'Hallaron.

int x;

(x*x) > = 0.

In the answer they mentioned that when x  is 65535 (0xFFFF), x*x < 0.

I'm a bit puzzled now. Is it possible to know more details of "undefined behavior"  - do you know any architecture under which x*x >= 0 when x  is 0xFFFF?

Best regards,
Dharma

@Profs: I'm using Frama-c to verify some of the practice and homework problems.

-----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