Alive2 doesn't support verification of optimizations that use inter-procedural analyses.
Right now, clang uses GlobalsAA by default and there's no way to disable it. This leads to Alive2 producing false positives.
Example:
file.c:
static int x; int f() { x = 0; *p = 1; x = 2; return *p; }
This file.c right now compiles to:
define i32 @f(ptr nocapture noundef %p) { store i32 1, ptr %p, align 4 store i1 true, ptr @x, align 4 ret i32 1 }
without globalsaa:
$ clang -S -emit-llvm -o - -O3 file.c -mllvm -enable-global-analyses=0
define i32 @f(ptr nocapture noundef %p) { store i32 1, ptr %p, align 4 store i1 true, ptr @x, align 4 %0 = load i32, ptr %p, align 4 ret i32 %0 }
Make the var name EnableGlobalAnalyses to match the option name?