Thanks Christian, I did search the mail list archive before posting (I promise!). Of course, now I find plenty of references…
Thanks for not offering to google that for me :) Rick > On 10 Nov 2016, at 14:05, Cristian Cadar <[email protected]> wrote: > > Hi, this question was asked on the mailing list before, but might not be easy > to find. In a nutshell, when KLEE encounters a symbolic memory access, it > forks one path for each object which can be referenced there. > > Cristian > > On 10/11/2016 01:10, Rutledge, Richard L wrote: >> I hope someone can clarify up a little klee-fundlement on my part regarding >> how Klee performs symbolic execution. Consider the following example program: >> >> -------------------------------------------------------- >> #include <klee/klee.h> >> >> #define MAXSTR 10 >> >> int test(char *str, int offset) { >> >> if (str[offset] == '\n') { >> return 1; >> } >> return 0; >> } >> >> int main(int argc, char *argv[]) { >> >> char str[MAXSTR]; >> int offset; >> >> klee_make_symbolic(str, MAXSTR, "str"); >> offset = klee_int("offset"); >> klee_assume(offset >= 0); >> klee_assume(offset < MAXSTR); >> >> int result = test(str, offset); >> >> return result; >> } >> -------------------------------------------------------- >> >> There are two paths through this program. As expected, Klee finds exactly >> two paths and generates two test cases. >> >> However, if I delete to two klee_assume() statements, then Klee finds 186 >> paths/test cases. >> >> What leads to the path explosion? Without the assumes, the program admits >> undefined behavior, but does not introduce any new paths. It still only has >> two and execution should fork into two states at the test() if statement. >> What condition forks the other 184 states? >> >> Cheers and Thanks! >> Rick Rutledge >> >> >> >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
