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



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>