--- layout: fc_discuss_archives title: Message 10 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 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