From 2ce22af434e383cf0c2c65e4da829de630b6cd9d Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sat, 13 Sep 2014 11:29:19 -0700 Subject: 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. --- lib/Solver/FastCexSolver.cpp | 9 +++++---- lib/Solver/IndependentSolver.cpp | 6 +++--- 2 files changed, 8 insertions(+), 7 deletions(-) (limited to 'lib/Solver') 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 #include @@ -441,7 +441,8 @@ public: } void propogatePossibleValues(ref 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 #include @@ -251,7 +251,7 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); -DEBUG( + KLEE_DEBUG( std::set< ref > reqset(result.begin(), result.end()); errs() << "--\n"; errs() << "Q: " << query.expr << "\n"; -- cgit 1.4.1