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: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Sat, 3 Oct 2015 16:26:39 -0400
  • In-reply-to: <CAOH62JjU36dhVFbYEN63nA-Kn=oz0pi5oo=_7XVXjieKdchOZw@mail.gmail.com>
  • 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> <CAOH62JjU36dhVFbYEN63nA-Kn=oz0pi5oo=_7XVXjieKdchOZw@mail.gmail.com>
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>