--- layout: fc_discuss_archives title: Message 8 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 10:03:26PM +0200, Pascal Cuoq wrote:
> 
> The usual logic rules do not apply in a C program in presence of undefined
> behavior.

Just to clarify this, the compiler will assume you did not do
something that creates undefined behaviour, so it assumes that in
case of a (signed) int x that x * x does not overflow, and so that
if x >= 0 then x * x must be >= 0.


Kurt