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: [email protected] <[email protected]> on behalf of RAJDEEP MUKHERJEE <[email protected]> Sent: 17 December 2015 03:08 To: [email protected] 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 [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
