options: fail if the debug or trace tag specified doesn't exist (-d -t)

3 files changed, 50 insertions, 0 deletions

diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 9b4d32e0b..abda24c26 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -19,6 +19,8 @@
  **/
 
 #include <string>
+#include <string.h>
+#include <stdlib.h>
 #include <sstream>
 
 #include "util/configuration.h"
@@ -147,6 +149,21 @@ char const* const* Configuration::getDebugTags() {
 #endif /* CVC4_DEBUG */
 }
 
+int strcmpptr(const char **s1, const char **s2){
+  return strcmp(*s1,*s2);
+}
+
+bool Configuration::isDebugTag(char const *){
+#if CVC4_DEBUG
+  unsigned ntags = getNumDebugTags();
+  char const* const* tags = getDebugTags();
+  return (bsearch(&optarg, tags, ntags, sizeof(char *),
+                  (int(*)(const void*,const void*))strcmpptr) != NULL);
+#else /* CVC4_DEBUG */
+  return false;
+#endif /* CVC4_DEBUG */
+}
+
 unsigned Configuration::getNumTraceTags() {
 #if CVC4_TRACING
   /* -1 because a NULL pointer is inserted as the last value */
@@ -165,6 +182,17 @@ char const* const* Configuration::getTraceTags() {
 #endif /* CVC4_TRACING */
 }
 
+bool Configuration::isTraceTag(char const *){
+#if CVC4_TRACING
+  unsigned ntags = getNumTraceTags();
+  char const* const* tags = getTraceTags();
+  return (bsearch(&optarg, tags, ntags, sizeof(char *),
+                  (int(*)(const void*,const void*))strcmpptr) != NULL);
+#else /* CVC4_TRACING */
+  return false;
+#endif /* CVC4_TRACING */
+}
+
 bool Configuration::isSubversionBuild() {
   return IS_SUBVERSION_BUILD;
 }
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 1bd48999e..b1ef7154d 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -89,11 +89,19 @@ public:
 
   static bool isBuiltWithTlsSupport();
 
+  /* Return the number of debug tags */
   static unsigned getNumDebugTags();
+  /* Return a sorted array of the debug tags name */
   static char const* const* getDebugTags();
+  /* Test if the given argument is a known debug tag name */
+  static bool isDebugTag(char const *);
 
+  /* Return the number of trace tags */
   static unsigned getNumTraceTags();
+  /* Return a sorted array of the trace tags name */
   static char const* const* getTraceTags();
+  /* Test if the given argument is a known trace tag name */
+  static bool isTraceTag(char const *);
 
   static bool isSubversionBuild();
   static const char* getSubversionBranchName();
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 4e8bc375b..e87c240a8 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -538,10 +538,24 @@ throw(OptionException) {
       break;
 
     case 't':
+      if(Configuration::isTracingBuild()) {
+        if(!Configuration::isTraceTag(optarg))
+          throw OptionException(string("trace tag ") + optarg +
+                                string(" not available"));
+      } else {
+        throw OptionException("trace tags not available in non-tracing build");
+      }
       Trace.on(optarg);
       break;
 
     case 'd':
+      if(Configuration::isDebugBuild()) {
+        if(!Configuration::isDebugTag(optarg))
+          throw OptionException(string("debug tag ") + optarg +
+                                string(" not available"));
+      } else {
+        throw OptionException("debug tags not available in non-debug build");
+      }
       Debug.on(optarg);
       Trace.on(optarg);
       break;