diff options
author | Daniel Dunbar <daniel@zuster.org> | 2014-09-13 11:29:19 -0700 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2014-09-13 11:29:32 -0700 |
commit | 2ce22af434e383cf0c2c65e4da829de630b6cd9d (patch) | |
tree | c49e4a0461ffa7c95adfa0fefd15bbc10b654c1f /lib/Solver | |
parent | 91eab8b92526a8215ebc9ed50da5b1d405533ac7 (diff) | |
download | klee-2ce22af434e383cf0c2c65e4da829de630b6cd9d.tar.gz |
Add KLEE specific DEBUG macros.
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling the checks in that mode). - Eventually it would be nice to just move off of LLVM's DEBUG infrastructure entirely and just have our own copy, but this works for now. - Fixes #150.
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 9 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 6 |
2 files changed, 8 insertions, 7 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 57e44806..73403882 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// +#define DEBUG_TYPE "cex-solver" #include "klee/Solver.h" #include "klee/Constraints.h" @@ -16,10 +17,9 @@ #include "klee/util/ExprRangeEvaluator.h" #include "klee/util/ExprVisitor.h" // FIXME: Use APInt. +#include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/IntEvaluation.h" -#define DEBUG_TYPE "cex-solver" -#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include <sstream> #include <cassert> @@ -441,7 +441,8 @@ public: } void propogatePossibleValues(ref<Expr> e, CexValueData range) { - DEBUG(llvm::errs() << "propogate: " << range << " for\n" << e << "\n";); + KLEE_DEBUG(llvm::errs() << "propogate: " << range << " for\n" + << e << "\n"); switch (e->getKind()) { case Expr::Constant: @@ -1008,7 +1009,7 @@ static bool propogateValues(const Query& query, CexData &cd, cd.propogateExactValue(query.expr, 0); } - DEBUG(cd.dump();); + KLEE_DEBUG(cd.dump()); // Check the result. bool hasSatisfyingAssignment = true; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 46b4ee56..dcaecb05 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -7,16 +7,16 @@ // //===----------------------------------------------------------------------===// +#define DEBUG_TYPE "independent-solver" #include "klee/Solver.h" #include "klee/Expr.h" #include "klee/Constraints.h" #include "klee/SolverImpl.h" +#include "klee/Internal/Support/Debug.h" #include "klee/util/ExprUtil.h" -#define DEBUG_TYPE "independent-solver" -#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include <map> #include <vector> @@ -251,7 +251,7 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); -DEBUG( + KLEE_DEBUG( std::set< ref<Expr> > reqset(result.begin(), result.end()); errs() << "--\n"; errs() << "Q: " << query.expr << "\n"; |