Hi, Many thanks for your reply. I have few follow-up questions. It would be great if you could help understand these queries:
1> I used klee-stats (eg. klee-stats --print-all klee-last) to see the statistics, but it does not report any stats about the number of feasible and infeasible paths in the program ? When I run Klee on a program, the statistics dumped looks like as follows. KLEE: done: total instructions = 272667 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 Is the number of completed paths same as number of feasible paths in the program ? 2> Does Klee invoke a SAT query at every branch point in the program by default to determine the eager infeasibility of a path ? Or is there other heuristics to selectively chose branch points ? 3> Does Klee support SAT solvers in the backend like MiniSAT etc ? I believe that the default SMT solver used is STP. The follow-up to this question is that are there options to dump the path-constraints in DIMACS format to use with a SAT solver. Many thanks in advance. Best regards, Rajdeep On Sat, Dec 19, 2015 at 11:23 AM, Carril Rodriguez, Luis Manuel (IPD) < luis.rodrig...@kit.edu> wrote: > 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 > > -- > > > > -- Thank You Rajdeep Mukherjee D.Phil Student, Dept. of Computer Science, University of Oxford Mob. :- 07405100369 Webpage :- http://www.cs.ox.ac.uk/people/rajdeep.mukherjee/ <http://cse.iitkgp.ac.in/~rajmukh/#research>
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev