Hi Dan, Many thanks for your reply. I have another query regarding the klee-statistics.
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> How to get the statistics for the number of feasible, infeasible and total paths ? Many thanks in advance. Best, Rajdeep On Tue, Jan 5, 2016 at 4:40 PM, Dan Liew <d...@su-root.co.uk> wrote: > > 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 ? > > AFAIK KLEE issues a query at every branch point. This does not > necessarily trigger a call to the underlying solver though as KLEE has > some caching mechanisms that may fire. > > > 3> Does Klee support SAT solvers in the backend like MiniSAT etc ? > > You are looking at the wrong level. KLEE works at the level of SMT > solvers, not SAT solvers as it needs a logic over bitvectors, not > booleans. Typically an SMT solver will be implemented in terms of a > SAT solver but KLEE does not know this. STP itself supports two > backends MiniSat and CryptoMinisat4. KLEE doesn't currently set the > backend to use in STP but support could be added. I would happily > review a pull request that added this. > > KLEE supports a few other SMT solvers via the MetaSMT interface > (untested) and I am currently working on native Z3 support. > > > 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. > > KLEE supports emission of the constraints in its own custom language > (KQuery) and as SMT-LIBv2. > > HTH, > Dan. > -- 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
