From 2ce22af434e383cf0c2c65e4da829de630b6cd9d Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sat, 13 Sep 2014 11:29:19 -0700 Subject: 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. --- include/klee/Config/config.h.in | 3 +++ include/klee/Internal/Support/Debug.h | 27 +++++++++++++++++++++++++++ 2 files changed, 30 insertions(+) create mode 100644 include/klee/Internal/Support/Debug.h (limited to 'include') 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 +#include + +// 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 -- cgit 1.4.1