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: kurt at roeckx.be (Kurt Roeckx)
  • Date: Sat, 3 Oct 2015 22:40:16 +0200
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7CAEBB17D@Mail1.FCMD.local>
  • References: <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 03, 2015 at 04:26:39PM -0400, Dharmalingam Ganesan wrote:
> 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...

You're completly missing the point.  For a signed number overflow
is undefined.  So far a 32 bit signed number 0xFFFF * 0xFFFF is
*UNDEFINED*.  The compiler is allowed to turn that into anything
it wants.  The compiler assumes you write code that has defined
meaning.  So clearly it should be a positive number, else it would
be undefined.

Anyway, you also failed to see my other reply.  For frama-c there
is no such thing as overflow in things like the asserts.  So that
assert will never work.


Kurt