diff options
| author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2014-05-22 21:56:22 +0200 |
|---|---|---|
| committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2014-05-29 23:57:46 +0200 |
| commit | 48492cbfa729fe035b7b69b71b541cb67f8545df (patch) | |
| tree | 8134b6396e68f2d2e6fd1658907aeac528008443 /lib/Solver | |
| parent | d124e44cf09da646f88b61b1937efb39b98efc6d (diff) | |
| download | klee-48492cbfa729fe035b7b69b71b541cb67f8545df.tar.gz | |
Use LLVM DEBUG macro instead of #if 0 or #if DEBUG
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/FastCexSolver.cpp | 14 | ||||
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 9 |
2 files changed, 9 insertions, 14 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 5c0cf8d0..57e44806 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -18,6 +18,8 @@ // FIXME: Use APInt. #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> @@ -406,10 +408,6 @@ public: : objects(_objects) {} }; -#if 0 -#define DEBUG -#endif - class CexData { public: std::map<const Array*, CexObjectData*> objects; @@ -443,9 +441,7 @@ public: } void propogatePossibleValues(ref<Expr> e, CexValueData range) { - #ifdef DEBUG - llvm::errs() << "propogate: " << range << " for\n" << e << "\n"; - #endif + DEBUG(llvm::errs() << "propogate: " << range << " for\n" << e << "\n";); switch (e->getKind()) { case Expr::Constant: @@ -1012,9 +1008,7 @@ static bool propogateValues(const Query& query, CexData &cd, cd.propogateExactValue(query.expr, 0); } -#ifdef DEBUG - cd.dump(); -#endif + DEBUG(cd.dump();); // Check the result. bool hasSatisfyingAssignment = true; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 2cb4b2c6..46b4ee56 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -15,6 +15,8 @@ #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> @@ -249,8 +251,7 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); -#if 0 - if (0) { +DEBUG( std::set< ref<Expr> > reqset(result.begin(), result.end()); errs() << "--\n"; errs() << "Q: " << query.expr << "\n"; @@ -263,8 +264,8 @@ IndependentElementSet getIndependentConstraints(const Query& query, errs() << "\telts: " << IndependentElementSet(*it) << "\n"; } errs() << "elts closure: " << eltsClosure << "\n"; - } -#endif + ); + return eltsClosure; } |