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 <lost...@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?
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
