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>
- References:
- [Frama-c-discuss] Alt Ergo - Problem
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Alt Ergo - Problem
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Alt Ergo - Problem
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Alt Ergo - Problem
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Alt Ergo - Problem
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Alt Ergo - Problem
- Prev by Date: [Frama-c-discuss] Alt Ergo - Problem
- Next by Date: [Frama-c-discuss] Alt Ergo - Problem
- Previous by thread: [Frama-c-discuss] Alt Ergo - Problem
- Next by thread: [Frama-c-discuss] Alt Ergo - Problem
- Index(es):