---
layout: fc_discuss_archives
title: Message 9 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
- Subject: [Frama-c-discuss] Alt Ergo - Problem
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Sat, 3 Oct 2015 22:32:10 +0200
- In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB17D@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> <CAOH62JjU36dhVFbYEN63nA-Kn=oz0pi5oo=_7XVXjieKdchOZw@mail.gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB17D@Mail1.FCMD.local>
On Sat, Oct 3, 2015 at 10:26 PM, Dharmalingam Ganesan <
dganesan at fc-md.umd.edu> wrote:
> Interesting to see that x * x > 0 on your machine when x = 0xFFFF. Thanks
> a lot for trying.
>
You should try to reproduce it on your machine. I assume that Clang has
been compiling this program in this way for a long time, and you might not
need the exact same version in order to produce the same behavior on your
computer. Also I wouldn't be surprised if GCC on that computer was able to
conclude that x * x >= 0.
>
>
> 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â¦
>
It is much simpler than that: my program (and yours) invoke undefined
behavior. Everything is allowed to happen, and the opposite too.
https://en.wikipedia.org/wiki/Undefined_behavior
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151003/90cf658a/attachment-0001.html>