From 9298b60d25da080b0c81682afe58d4a8d9e1971b Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 10 Aug 2015 09:36:10 +0200 Subject: [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. --- lib/Solver/Solver.cpp | 9 +++++++-- 1 file 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 +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; -- cgit 1.4.1