diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2012-10-24 14:43:50 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2012-10-24 14:43:50 +0000 |
| commit | 30db83cfba2070f0693eef39c16b3c52432a22bb (patch) | |
| tree | 53d7fdca73b35a55260cf3e898b7de4f18b6c0f2 /lib/Core/Executor.h | |
| parent | 2eec409061b6f3f107ba3679e9d4745e64451952 (diff) | |
| download | klee-30db83cfba2070f0693eef39c16b3c52432a22bb.tar.gz | |
Patch by Dan Liew which improves the logging options: "Removed
-use-query-pc-log and -use-stp-query-pc-log and replaced with better command line option -use-query-log=option. Multiple comma seperated options can be specified after -use-query-log=. In addition queries can now be logged in SMT-LIBv2 format as well as KQuery format. The names of logging files has changed and also KLEE now informs users which files are being written to. Because of the changes the test/Feature/ExprLogging.c test broke so it was necessary to fix it." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166565 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Core/Executor.h')
| -rw-r--r-- | lib/Core/Executor.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 7e6b79cd..f0c9f576 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -70,6 +70,16 @@ namespace klee { class TreeStreamWriter; template<class T> class ref; + ///The different query logging solvers that can switched on/off + enum QueryLoggingSolver + { + ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format + ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format + SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format + SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format + }; + + /// \todo Add a context object to keep track of data only live /// during an instruction step. Should contain addedStates, /// removedStates, and haltExecution, among others. |