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