> > have reconstructed my test platform enough to run an experiment > > The platform is based on LLVM 2.9 >
I'm using KLEE built with LLVM 3.8 (experimental build), and right now I've reproduced the same results with official LLVM 3.4 docker image. I use clang for compiling into bytecode. This is a program I wrote: #include <klee/klee.h> int main(void) { int a, b, c; klee_make_symbolic(&a, sizeof(a), "a"); klee_make_symbolic(&b, sizeof(b), "b"); klee_make_symbolic(&c, sizeof(c), "c"); if ((a && b) || c) return 42; else return 0; } I compile it with clang, and then use with klee. With SimplifyCFG pass, klee produces 2 test cases. WIthout SimplifyCFG pass, klee produces 5 test cases. I use klee -debug-print-instructions to see what klee executes. WIth SimplifyCFG pass, it basically does %or.cond = and %a, %b %or.cond3 = or %or.cond, %c br %or.cond3, label_then, label_else Without SimplifyCFG pass, it does br %a, check_b, check_c check_b: br %b, do_then, check_c check_c: br %c, label_then, label_else and this makes klee generates full 5 testcases without using CIL. > > The difference relates to the LLVM compilation probably compiler options > > > Probably, can you try my example then on LLVM 2.9 to confirm?
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev