Hi, On 17 December 2015 at 02:08, RAJDEEP MUKHERJEE <rajdeep.mukherje...@gmail.com> wrote: > > 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
Use the ``klee-stats`` tool tool on an output directory (e.g. ``klee-last``) produced by KLEE after it has finished executing. > 2> Does Klee perform any state merging or path-merging ? What option to use > for this ? Not by default. There is experimental support for merging paths with the ``klee_merge()`` special function but I've never used it. > 3> Does Klee perform property driven slicing before it begins symbolic > execution ? Technically I think running an optimisation that the LLVM optimiser considers remove dead code could be considered a form of program slicing but that's probably not what you mean by "property driven slicing" in which case the answer is probably no. Dan. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev