[klee-dev] Klee path statistics and merging options

[Dan Liew]

Hi,

On 17 December 2015 at 02:08, RAJDEEP MUKHERJEE
<rajdeep.mukherjee87 at 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.