From 6b2752ae9c9c9af67a86c27c0d688f16f8fd0c41 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 9 Jan 2018 12:44:27 -0800 Subject: [PATCH] Fix output of --trace=help. (#1500) --- src/options/base_options | 4 +- src/options/options_handler.cpp | 197 ++++++++++++++++---------------- src/options/options_handler.h | 8 +- 3 files changed, 102 insertions(+), 107 deletions(-) diff --git a/src/options/base_options b/src/options/base_options index 7346641c7..7098e1f5d 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -199,9 +199,9 @@ option parseOnly parse-only --parse-only bool :read-write option preprocessOnly preprocess-only --preprocess-only bool exit after preprocessing input -option - trace -t --trace=TAG argument :handler addTraceTag +option - trace -t --trace=TAG argument :handler enableTraceTag trace something (e.g. -t pushpop), can repeat -option - debug -d --debug=TAG argument :handler addDebugTag +option - debug -d --debug=TAG argument :handler enableDebugTag debug something (e.g. -d arith), can repeat option printSuccess print-success --print-success bool :notify notifyPrintSuccess diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 583f79d2d..e8a243448 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1546,38 +1546,115 @@ void OptionsHandler::showConfiguration(std::string option) { exit(0); } -void OptionsHandler::showDebugTags(std::string option) { - if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { - std::cout << "available tags:"; - unsigned ntags = Configuration::getNumDebugTags(); - char const* const* tags = Configuration::getDebugTags(); - for(unsigned i = 0; i < ntags; ++ i) { - std::cout << tags[i]; - } - std::cout << std::endl; - } else if(! Configuration::isDebugBuild()) { +static void printTags(unsigned ntags, char const* const* tags) +{ + std::cout << "available tags:"; + for (unsigned i = 0; i < ntags; ++ i) + { + std::cout << " " << tags[i] << std::endl; + } + std::cout << std::endl; +} + +void OptionsHandler::showDebugTags(std::string option) +{ + if (!Configuration::isDebugBuild()) + { throw OptionException("debug tags not available in non-debug builds"); - } else { + } + else if (!Configuration::isTracingBuild()) + { throw OptionException("debug tags not available in non-tracing builds"); } + printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags()); exit(0); } -void OptionsHandler::showTraceTags(std::string option) { - if(Configuration::isTracingBuild()) { - std::cout << "available tags:" << std::endl; - unsigned ntags = Configuration::getNumTraceTags(); - char const* const* tags = Configuration::getTraceTags(); - for (unsigned i = 0; i < ntags; ++ i) { - std::cout << " " << tags[i] << std::endl; - } - std::cout << std::endl; - } else { +void OptionsHandler::showTraceTags(std::string option) +{ + if (!Configuration::isTracingBuild()) + { throw OptionException("trace tags not available in non-tracing build"); } + printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags()); exit(0); } +static std::string suggestTags(char const* const* validTags, + std::string inputTag, + char const* const* additionalTags) +{ + DidYouMean didYouMean; + + const char* opt; + for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i) + { + didYouMean.addWord(validTags[i]); + } + if (additionalTags != nullptr) + { + for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i) + { + didYouMean.addWord(additionalTags[i]); + } + } + + return didYouMean.getMatchAsString(inputTag); +} + +void OptionsHandler::enableTraceTag(std::string option, std::string optarg) +{ + if(!Configuration::isTracingBuild()) + { + throw OptionException("trace tags not available in non-tracing builds"); + } + else if(!Configuration::isTraceTag(optarg.c_str())) + { + if (optarg == "help") + { + printTags( + Configuration::getNumTraceTags(), Configuration::getTraceTags()); + exit(0); + } + + throw OptionException( + std::string("trace tag ") + optarg + std::string(" not available.") + + suggestTags(Configuration::getTraceTags(), optarg, nullptr)); + } + Trace.on(optarg); +} + +void OptionsHandler::enableDebugTag(std::string option, std::string optarg) +{ + if (!Configuration::isDebugBuild()) + { + throw OptionException("debug tags not available in non-debug builds"); + } + else if (!Configuration::isTracingBuild()) + { + throw OptionException("debug tags not available in non-tracing builds"); + } + + if (!Configuration::isDebugTag(optarg.c_str()) + && !Configuration::isTraceTag(optarg.c_str())) + { + if (optarg == "help") + { + printTags( + Configuration::getNumDebugTags(), Configuration::getDebugTags()); + exit(0); + } + + throw OptionException(std::string("debug tag ") + optarg + + std::string(" not available.") + + suggestTags(Configuration::getDebugTags(), + optarg, + Configuration::getTraceTags())); + } + Debug.on(optarg); + Trace.on(optarg); +} + OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) { if(optarg == "help") { @@ -1651,83 +1728,5 @@ void OptionsHandler::decreaseVerbosity(std::string option) { } -void OptionsHandler::addTraceTag(std::string option, std::string optarg) { - if(Configuration::isTracingBuild()) { - if(!Configuration::isTraceTag(optarg.c_str())) { - - if(optarg == "help") { - std::cout << "available tags:"; - unsigned ntags = Configuration::getNumTraceTags(); - char const* const* tags = Configuration::getTraceTags(); - for(unsigned i = 0; i < ntags; ++ i) { - std::cout << tags[i]; - } - std::cout << std::endl; - exit(0); - } - - throw OptionException(std::string("trace tag ") + optarg + - std::string(" not available.") + - suggestTags(Configuration::getTraceTags(), optarg) ); - } - } else { - throw OptionException("trace tags not available in non-tracing builds"); - } - Trace.on(optarg); -} - -void OptionsHandler::addDebugTag(std::string option, std::string optarg) { - if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { - if(!Configuration::isDebugTag(optarg.c_str()) && - !Configuration::isTraceTag(optarg.c_str())) { - - if(optarg == "help") { - std::cout << "available tags:"; - unsigned ntags = Configuration::getNumDebugTags(); - char const* const* tags = Configuration::getDebugTags(); - for(unsigned i = 0; i < ntags; ++ i) { - std::cout << tags[i]; - } - std::cout << std::endl; - exit(0); - } - - throw OptionException(std::string("debug tag ") + optarg + - std::string(" not available.") + - suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) ); - } - } else if(! Configuration::isDebugBuild()) { - throw OptionException("debug tags not available in non-debug builds"); - } else { - throw OptionException("debug tags not available in non-tracing builds"); - } - Debug.on(optarg); - Trace.on(optarg); -} - - - - -std::string OptionsHandler::suggestTags(char const* const* validTags, std::string inputTag, - char const* const* additionalTags) -{ - DidYouMean didYouMean; - - const char* opt; - for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) { - didYouMean.addWord(validTags[i]); - } - if(additionalTags != NULL) { - for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) { - didYouMean.addWord(additionalTags[i]); - } - } - - return didYouMean.getMatchAsString(inputTag); -} - - - - }/* CVC4::options namespace */ }/* CVC4 namespace */ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index eef4c9b61..23a6be501 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -188,16 +188,12 @@ public: void decreaseVerbosity(std::string option); OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException); InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException); - void addTraceTag(std::string option, std::string optarg); - void addDebugTag(std::string option, std::string optarg); + void enableTraceTag(std::string option, std::string optarg); + void enableDebugTag(std::string option, std::string optarg); void notifyPrintSuccess(std::string option); private: - /* Helper utilities */ - static std::string suggestTags(char const* const* validTags, std::string inputTag, - char const* const* additionalTags = NULL); - /** Pointer to the containing Options object.*/ Options* d_options; -- 2.30.2