-{d,t} help => --show-{debug,trace}-tags

diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 15813a7745ea9d93f397a227e30af5697f98cb68..e701ee13d7fefd02c618ef4109d7c31f9fde248f 100644 (file)
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -121,6 +121,18 @@ inline std::string suggestTags(char const* const* validTags, std::string inputTa
 inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) {
   if(Configuration::isTracingBuild()) {
     if(!Configuration::isTraceTag(optarg.c_str()))
+
+      if(optarg == "help") {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumTraceTags();
+        char const* const* tags = Configuration::getTraceTags();
+        for(unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
+        }
+        printf("\n");
+        exit(0);
+      }
+
       throw OptionException(std::string("trace tag ") + optarg +
                             std::string(" not available.") +
                             suggestTags(Configuration::getTraceTags(), optarg) );
@@ -134,6 +146,18 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt)
   if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
     if(!Configuration::isDebugTag(optarg.c_str()) &&
        !Configuration::isTraceTag(optarg.c_str())) {
+
+      if(optarg == "help") {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumDebugTags();
+        char const* const* tags = Configuration::getDebugTags();
+        for(unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
+        }
+        printf("\n");
+        exit(0);
+      }
+
       throw OptionException(std::string("debug tag ") + optarg +
                             std::string(" not available.") +
                             suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) );