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

On Sat, 3 Oct 2015 22:29:04 +0200, Kurt Roeckx <kurt at roeckx.be> wrote:
> 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.

Yes.  Sadly, it's really easy to do something that is undefined in C
(a lot of things you THINK would be defined are not).

Some C compilers have flags that can detect many of these cases.
In particular, both gcc and LLVM have a lot of "-fsanitize=...." options
that turn on runtime checks, and some of them can help you detect problems like this.
LLVM has "-fsanitize=unsigned-integer-overflow" for detecting unsigned integer overflows,
and both gcc and LLVM have "-fsanitize=undefined" that detect MANY such cases.

Some places for more info:
  http://developerblog.redhat.com/2014/10/16/gcc-undefined-behavior-sanitizer-ubsan/
  http://clang.llvm.org/docs/UsersManual.html

--- David A. Wheeler