[klee-dev] Solver goals

[Cristian Cadar]

Hi Andy, the answer to the first two questions is a qualified yes -- you 
can make these guarantees assuming no interaction with external code, no 
constraint solving timeouts, no bugs in KLEE, etc.  As to your final 
question, there are several research projects that aim to do this (e.g., 
https://srg.doc.ic.ac.uk/projects/katch/), but they are not part of the 
KLEE mainline.

Cristian

On 12/09/18 13:18, Andy Owen wrote:
> Hi, I have two questions which seem vaguely related:
> 
> 1) If I run "klee foo.bc" and wait for it to finish, and it generates a 
> bunch of test vectors, then what guarantees can I make about that set of 
> test vectors?
> - Can I guarantee that all possible lines of code (or basic blocks) 
> which can be reached (within the constraints of what memory I made 
> symbolic) will be reached?
> - Can I guarantee that it is impossible for my code to dereference NULL 
> or fail an assert (again with the same constraints) or there will be a 
> test that demonstrates this?
> - Will all the tests generated be distinct according to some property 
> (e.g. the set of basic blocks they hit will be different)?
> 
> 2) Is there a way to give KLEE a specific goal, so instead of generating 
> lots of test cases, it instead tries to generate a single test case that 
> does a specific thing (e.g. hits a klee_assert())?
> 
> Thanks for any assistance. I've searched lots over the KLEE 
> documentation, but I haven't been able to find anything so far.
> 
> Andy
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev