--- 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



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>