about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2015-08-10 09:36:10 +0200
committerDan Liew <daniel.liew@imperial.ac.uk>2015-12-17 19:30:14 +0000
commit9298b60d25da080b0c81682afe58d4a8d9e1971b (patch)
tree8b6c0b65fd65cd50cc5d14b10ff049aaa6272a40 /lib/Solver
parent8331998f8232db61e960863936ac27b36a147507 (diff)
downloadklee-9298b60d25da080b0c81682afe58d4a8d9e1971b.tar.gz
[Solver]Add support to dump STP qeries using
Use "-debug-dump-stp-queries" argument for KLEE/Kleaver
to print out each STP query sent to the STP Solver.

Queries have the format which `stp` frontend can understand.
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/Solver.cpp9
1 files changed, 7 insertions, 2 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 07331fa4..341ca17c 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -21,6 +21,7 @@
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprUtil.h"
 #include "klee/Internal/Support/Timer.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/CommandLine.h"
 
 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
@@ -45,6 +46,10 @@ IgnoreSolverFailures("ignore-solver-failures",
                      llvm::cl::init(false),
                      llvm::cl::desc("Ignore any solver failures (default=off)"));
 
+llvm::cl::opt<bool>
+DebugDumpSTPQueries("debug-dump-stp-queries",
+                     llvm::cl::init(false),
+                     llvm::cl::desc("Dump every STP query to stderr (default=off)"));
 
 using namespace klee;
 
@@ -812,11 +817,11 @@ STPSolverImpl::computeInitialValues(const Query &query,
 
   ExprHandle stp_e = builder->construct(query.expr);
      
-  if (0) {
+  if (DebugDumpSTPQueries) {
     char *buf;
     unsigned long len;
     vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
-    fprintf(stderr, "note: STP query: %.*s\n", (unsigned) len, buf);
+    klee_warning("STP query:\n%.*s\n", (unsigned) len, buf);
   }
 
   bool success;