[klee-dev] Option for generating MC/DC test cases

[Damir]

>
> 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?
-------------- next part --------------
HTML attachment scrubbed and removed