Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Alt Ergo - Problem

  • Subject: [Frama-c-discuss] Alt Ergo - Problem
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Sat, 3 Oct 2015 22:03:26 +0200
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB178@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C766044995@Mail1.FCMD.local> <52D1556E.7010400@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76604499E@Mail1.FCMD.local> <52D15C30.40602@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB78@Mail1.FCMD.local> <52D15D7F.3000800@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB79@Mail1.FCMD.local> <52D16266.3040201@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB7A@Mail1.FCMD.local> <52D16676.3000200@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DB7B@Mail1.FCMD.local> <52D16727.8030804@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C7660449A2@Mail1.FCMD.local> <52D4D24E.8060007@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DC58@Mail1.FCMD.local> <52D55374.8020404@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682E584@Mail1.FCMD.local> <52EF36F1.7020100@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB147@Mail1.FCMD.local> <561000C3.2020700@gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB172@Mail1.FCMD.local> <5FB61E09-69A2-41FC-97F1-621B59B146F7@gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB178@Mail1.FCMD.local>
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>