diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Config/config.h.in | 3 | ||||
| -rw-r--r-- | include/klee/Internal/Support/Debug.h | 27 |
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 |