--- layout: fc_discuss_archives title: Message 4 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



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