Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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: dwheeler at dwheeler.com (David A. Wheeler)
  • Date: Sat, 03 Oct 2015 16:45:25 -0400 (EDT)
  • In-reply-to: <20151003202904.GA552@roeckx.be>
> 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