diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
commit | 6a4af721d1dc55f1dc6454014c08f87465398a54 (patch) | |
tree | 178f006869c0c4af6b6c71f46b55c28de643c7bd /src/util/configuration.cpp | |
parent | 1ce0650dcf8ce30424b546deb540974cc510c215 (diff) |
--disable-tracing at configure time now disables Trace() and Debug() gestures both.
Diffstat (limited to 'src/util/configuration.cpp')
-rw-r--r-- | src/util/configuration.cpp | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 6f01d6cf4..d0fc3cd1d 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -27,9 +27,9 @@ #include "util/configuration_private.h" #include "cvc4autoconfig.h" -#ifdef CVC4_DEBUG +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) # include "util/Debug_tags.h" -#endif /* CVC4_DEBUG */ +#endif /* CVC4_DEBUG && CVC4_TRACING */ #ifdef CVC4_TRACING # include "util/Trace_tags.h" @@ -132,21 +132,21 @@ bool Configuration::isBuiltWithTlsSupport() { } unsigned Configuration::getNumDebugTags() { -#if CVC4_DEBUG +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) /* -1 because a NULL pointer is inserted as the last value */ - return sizeof(Debug_tags) / sizeof(Debug_tags[0]) - 1; -#else /* CVC4_DEBUG */ + return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1; +#else /* CVC4_DEBUG && CVC4_TRACING */ return 0; -#endif /* CVC4_DEBUG */ +#endif /* CVC4_DEBUG && CVC4_TRACING */ } char const* const* Configuration::getDebugTags() { -#if CVC4_DEBUG +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) return Debug_tags; -#else /* CVC4_DEBUG */ +#else /* CVC4_DEBUG && CVC4_TRACING */ static char const* no_tags[] = { NULL }; return no_tags; -#endif /* CVC4_DEBUG */ +#endif /* CVC4_DEBUG && CVC4_TRACING */ } int strcmpptr(const char **s1, const char **s2){ @@ -154,7 +154,7 @@ int strcmpptr(const char **s1, const char **s2){ } bool Configuration::isDebugTag(char const *tag){ -#if CVC4_DEBUG +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) unsigned ntags = getNumDebugTags(); char const* const* tags = getDebugTags(); for (unsigned i = 0; i < ntags; ++ i) { @@ -162,7 +162,7 @@ bool Configuration::isDebugTag(char const *tag){ return true; } } -#endif /* CVC4_DEBUG */ +#endif /* CVC4_DEBUG && CVC4_TRACING */ return false; } |