--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on October 2015 ---
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