about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2014-09-13 11:29:19 -0700
committerDaniel Dunbar <daniel@zuster.org>2014-09-13 11:29:32 -0700
commit2ce22af434e383cf0c2c65e4da829de630b6cd9d (patch)
treec49e4a0461ffa7c95adfa0fefd15bbc10b654c1f /lib/Solver
parent91eab8b92526a8215ebc9ed50da5b1d405533ac7 (diff)
downloadklee-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.cpp9
-rw-r--r--lib/Solver/IndependentSolver.cpp6
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";