diff options
| author | François Bobot <francois@bobot.eu> | 2012-05-04 14:28:00 +0000 |
|---|---|---|
| committer | François Bobot <francois@bobot.eu> | 2012-05-04 14:28:00 +0000 |
| commit | 66c8c03e12d42d4b6095a05229567b83e6f175e1 (patch) | |
| tree | 8da53d2cc7a36c5e361f1bf98a375038ae26a748 /src/util/configuration.cpp | |
| parent | 3d1c57e0506b2454aa815c3c1cb634d96ade1d7c (diff) | |
fix: getNumTraceTags, getNumDebugTags
Diffstat (limited to 'src/util/configuration.cpp')
| -rw-r--r-- | src/util/configuration.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 8942c049b..9b4d32e0b 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -131,7 +131,8 @@ bool Configuration::isBuiltWithTlsSupport() { unsigned Configuration::getNumDebugTags() { #if CVC4_DEBUG - return sizeof(Debug_tags) / sizeof(Debug_tags[0]); + /* -1 because a NULL pointer is inserted as the last value */ + return sizeof(Debug_tags) / sizeof(Debug_tags[0]) - 1; #else /* CVC4_DEBUG */ return 0; #endif /* CVC4_DEBUG */ @@ -148,7 +149,8 @@ char const* const* Configuration::getDebugTags() { unsigned Configuration::getNumTraceTags() { #if CVC4_TRACING - return sizeof(Trace_tags) / sizeof(Trace_tags[0]); + /* -1 because a NULL pointer is inserted as the last value */ + return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1; #else /* CVC4_TRACING */ return 0; #endif /* CVC4_TRACING */ |