Hi, about the slicing this work could interest you:
http://www.fi.muni.cz/~xstrejc/publications/tacas2013preprint.pdf Basically they have a llvm pass that perform the program slicing before running it under KLEE, reducing effectively the search space. Cheers Luis M. ________________________________ From: klee-dev-boun...@imperial.ac.uk <klee-dev-boun...@imperial.ac.uk> on behalf of RAJDEEP MUKHERJEE <rajdeep.mukherje...@gmail.com> Sent: 17 December 2015 03:08 To: klee-dev@imperial.ac.uk Subject: [klee-dev] Klee path statistics and merging options Hi, I have the following queries regarding Klee. I would really appreciate any help. 1> How to obtain the following statistics from Klee: A> Total number of feasible paths, B> Total number of infeasible paths, C> Total number of paths in the program. D> Total number of solver queries and E> Total time spent in solver 2> Does Klee perform any state merging or path-merging ? What option to use for this ? 3> Does Klee perform property driven slicing before it begins symbolic execution ? Many thanks in advance. Best, Rajdeep --
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev