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