[klee-dev] memcmp generate too many paths

[Chaoqiang Zhang]

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 <sylvain.gault at inria.fr>
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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed