aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/FastCexSolver.cpp14
-rw-r--r--lib/Solver/IndependentSolver.cpp9
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;
}