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

[David Lightstone]

The results are meaningful. There is no question. 
There is at least one potentially loose end to consider

Some languages are capable of allowing the developer to select whether boolean expressions will be evaluated as non-short circuiting operations or evaluated as short circuiting operations. Ada is one such language. I do not know of others.

One ideally should be able to address the 3 situations 
Always short circuiting 
Never short circuiting
Developer selected short circuiting via language construct

If the LLVM byte code distinguishes between the two everything will eventually sort out
If it does not  there is a potential proboem solving effort to consider

Concievably a run option could be created which serves to determine if SimplifyCGF will be invoked.


Sent from my iPad

On May 12, 2016, at 2:51 PM, Damir <lost404 at gmail.com> wrote:

>> 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