[klee-dev] Solver goals

[Andy Owen]

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