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 [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
