---
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
- Subject: [Frama-c-discuss] Alt Ergo - Problem
- From: kurt at roeckx.be (Kurt Roeckx)
- Date: Sat, 3 Oct 2015 22:29:04 +0200
- In-reply-to: <CAOH62JjU36dhVFbYEN63nA-Kn=oz0pi5oo=_7XVXjieKdchOZw@mail.gmail.com>
- References: <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>
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