Hi, > On 11 Sep 2015, at 23:12, Jeff Wilson <[email protected]> wrote: > > Is there a way to disable the queries that KLEE makes to the SMT solver? I > would like to only get the path constraints in SMT2 format as outputs from > KLEE. > In general, if you want to generate SMT2 output use following arguments (-use-query-log): =all:smt2 to get all solver queries (i.e. every call, before any optimisations, caches, …) and/or =solver:smt2 to get queries which reach the real solver (e.g. the ones which could not be solved using caches, …)
As an example: klee -use-query-log=all:smith,solver:smt2 foobar.bc Now, even you would like to get the path constraints only, you still need to invoke the solver to progress a state (i.e. should KLEE fork a state on a conditional branch instruction, which path is valid?). Maybe a hacky work around: * add a global flag in KLEE which you can toggle on/off before and after a state fork (https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L703) * in the QueryLoggignSolver::flushBuffer (https://github.com/klee/klee/blob/master/lib/Solver/QueryLoggingSolver.cpp#L76) check for that flag and flush in that case This way, only queries for path constraints get logged. HTH. Cheers, Martin --------------------------------------------------- Martin Nowack Research Assistant Technische Universität Dresden Computer Science Institute of Systems Architecture Systems Engineering 01062 Dresden Phone: +49 351 463 39608 Email: [email protected] ----------------------------------------------------
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
