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