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



On Sat, Oct 3, 2015 at 9:16 PM, Dharmalingam Ganesan <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/931b14a2/attachment-0001.html>