--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on October 2015 ---
Interesting to see that x * x > 0 on your machine when x = 0xFFFF. Thanks a lot for trying. I do not know whether this matters: One of the assumptions of this problem is that right shifts are performed arithmetically for signed values and logically for unsigned values. Iâm wondering whether this assumption may be not true on your machine. Just speculating⦠From: Frama-c-discuss [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal Cuoq Sent: Saturday, October 03, 2015 4:03 PM To: Frama-C public discussion Cc: Randy Bryant; david.ohallaron at gmail.com Subject: Re: [Frama-c-discuss] Alt Ergo - Problem On Sat, Oct 3, 2015 at 9:16 PM, Dharmalingam Ganesan <dganesan at fc-md.umd.edu<mailto:dganesan at fc-md.umd.edu>> wrote: (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? This is the wrong way to look at it. The truth value, when int is a 32-bit signed type, of x = 0xffff; x * x < 0 is âDEMONS FLY OUT OF YOUR NOSEâ. This may be counter-intuitive, but the truth value of x = 0xffff; x * x >= 0 is also âDEMONS FLY OUT OF YOUR NOSEâ. The usual logic rules do not apply in a C program in presence of undefined behavior. Anyway, you asked for an architecture for which x * x >= 0 when x is 0xffff, and I am happy to oblige: the architecture is the computer on which I am typing this message, a 2012 Mac Pro with a Xeon W3680 processor on which I am using clang 4.1: Hexa:~ $ clang -v Apple clang version 4.1 (tags/Apple/clang-421.11.66) (based on LLVM 3.1svn) Target: x86_64-apple-darwin12.6.0 Thread model: posix Hexa:~ $ cat t.c #include <stdio.h> #include <limits.h> int x; void f(int x) { if (x < 0) return; if (x * x >= 0) printf("x * x >= 0\n"); } int main(void){ int x = 0xffff; printf("%zu %d %d\n", sizeof(int), (int)CHAR_BIT, INT_MAX); f(x); } Hexa:~ $ clang -O3 t.c && ./a.out 4 8 2147483647 x * x >= 0 Hexa:~ $ -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151003/4bdb24ac/attachment.html>