state merging is one of the techniques for addressing this problem, there are several papers on it, one of them is:
http://dslab.epfl.ch/pubs/stateMerging.pdf On Wed, Jul 23, 2014 at 5:43 PM, Sylvain Gault <[email protected]> wrote: > > Hello, > > It seems that when a program use memcmp, klee generate as many path as > the array size since its loop can exit anytime. While all I'm interested > in is whether the arrays are equal or not. > > For instance this code would generate 5 paths. > > char a1[] = {0, 1, 2, 3}; > char a2[sizeof(a1)]; > > klee_make_symbolic(a2, sizeof(a2), "a2"); > > if (memcmp(a1, a2, sizeof(a1))) > printf("Winner!\n"); > else > printf("Loser!\n"); > > > I understand that during the execution of memcmp, there are different > path depending on the loop iteration that exists. But once the > function exists, most of these path end in the exact same state. > > But I'm only interested in the paths in my code. So is there a way to > make klee merge the test cases that differ only in the path through the > libc? > > My real case has an array of 168 bytes. So a memcmp generate 168 paths > by itself. Which means that the code after it will be run 168 times for > the exact same result. This is a bit insane. > > > Sylvain Gault > > _______________________________________________ > 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
