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.

2 files changed, 30 insertions, 0 deletions

diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index b97f0b05..6f24cde3 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -3,6 +3,9 @@
 #ifndef KLEE_CONFIG_CONFIG_H
 #define KLEE_CONFIG_CONFIG_H
 
+/* Enable KLEE DEBUG checks */
+#undef ENABLE_KLEE_DEBUG
+
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
diff --git a/include/klee/Internal/Support/Debug.h b/include/klee/Internal/Support/Debug.h
new file mode 100644
index 00000000..8f46b93b
--- /dev/null
+++ b/include/klee/Internal/Support/Debug.h
@@ -0,0 +1,27 @@
+//===-- Debug.h -------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_INTERNAL_SUPPORT_DEBUG_H
+#define KLEE_INTERNAL_SUPPORT_DEBUG_H
+
+#include <klee/Config/config.h>
+#include <llvm/Support/Debug.h>
+
+// We define wrappers around the LLVM DEBUG macros that are conditionalized on
+// whether the LLVM we are building against has the symbols needed by these
+// checks.
+
+#ifdef ENABLE_KLEE_DEBUG
+#define KLEE_DEBUG_WITH_TYPE(TYPE, X) DEBUG_WITH_TYPE(TYPE, X)
+#else
+#define KLEE_DEBUG_WITH_TYPE(TYPE, X) do { } while (0)
+#endif
+#define KLEE_DEBUG(X) KLEE_DEBUG_WITH_TYPE(DEBUG_TYPE, X)
+
+#endif