I have started to play with Klee to see what it does, to see its limits
The test problem which I choose to apply third was
int test(int a)
{
if (( a < 1) && (a > 1))
return 1;
else
return 0;
}
There is no value of a for which the condition is true, so path coverage is
impossible.
A good optimizing compiler probably would have reduced the code to
return (0);
I did not compile with optimization enabled
I used --emit-llvm -c -g for the compile options
I used --only-output-states-covering-new -optimize for the klee options
The generated test cases were
a = 0;
a = 2;
(1) It is not clear what the Klee -optimize option achieves. Certainly it is
not code optimization. Were that the case the impossibility if achieving the
TRUE path would have been discovered symbolically. I suspect that somewhere
there is a declaration of intent for each of the options. I have yet to
actually look for it. If such a declaration does not yet exist, best to
write one.
dbl
_______________________________________________
klee-dev mailing list
klee-dev at keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
