--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2015 ---
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