diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-06-23 22:34:12 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2023-07-21 10:00:02 +0100 |
commit | 7082eafd05b4f268132ab94772c0243dbebf5087 (patch) | |
tree | 549f66608f0cb4e50cee2e51c53206e798ab82cd | |
parent | 974f140d79a621785b1fe4a0fc7fe321ba1089e2 (diff) | |
download | klee-7082eafd05b4f268132ab94772c0243dbebf5087.tar.gz |
Add code to only keep in the --help menu the KLEE/Kleaver option categories
-rw-r--r-- | include/klee/Solver/SolverCmdLine.h | 12 | ||||
-rw-r--r-- | lib/Solver/SolverCmdLine.cpp | 16 | ||||
-rw-r--r-- | tools/kleaver/main.cpp | 6 | ||||
-rw-r--r-- | tools/klee/main.cpp | 23 |
4 files changed, 31 insertions, 26 deletions
diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h index 90c162ee..4414dc7a 100644 --- a/include/klee/Solver/SolverCmdLine.h +++ b/include/klee/Solver/SolverCmdLine.h @@ -24,6 +24,8 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/CommandLine.h" DISABLE_WARNING_POP +#include <set> + namespace klee { extern llvm::cl::opt<bool> UseFastCexSolver; @@ -86,12 +88,12 @@ extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend; class KCommandLine { public: - /// Hide all options in the specified category - static void HideOptions(llvm::cl::OptionCategory &Category); - - /// Hide all options except the ones in the specified category - static void HideUnrelatedOptions(llvm::cl::OptionCategory &Category); + /// Keep only the options in the provided categories, + /// together with --help, --help-list, --version and --color + static void + KeepOnlyCategories(std::set<llvm::cl::OptionCategory *> const &categories); }; + } // namespace klee #endif /* KLEE_SOLVERCMDLINE_H */ diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index b0bff6e6..a371d5e4 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -112,16 +112,24 @@ cl::opt<bool> UseAssignmentValidatingSolver( cl::desc("Debug the correctness of generated assignments (default=false)"), cl::cat(SolvingCat)); - -void KCommandLine::HideOptions(llvm::cl::OptionCategory &Category) { +void KCommandLine::KeepOnlyCategories( + std::set<llvm::cl::OptionCategory *> const &categories) { StringMap<cl::Option *> &map = cl::getRegisteredOptions(); for (auto &elem : map) { + if (elem.first() == "version" || elem.first() == "color" || + elem.first() == "help" || elem.first() == "help-list") + continue; + + bool keep = false; for (auto &cat : elem.second->Categories) { - if (cat == &Category) { - elem.second->setHiddenFlag(cl::Hidden); + if (categories.find(cat) != categories.end()) { + keep = true; + break; } } + if (!keep) + elem.second->setHiddenFlag(cl::Hidden); } } diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 51298dfb..42ca0c55 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -382,11 +382,7 @@ static bool printInputAsSMTLIBv2(const char *Filename, } int main(int argc, char **argv) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(13, 0) - KCommandLine::HideOptions(llvm::cl::getGeneralCategory()); -#else - KCommandLine::HideOptions(llvm::cl::GeneralCategory); -#endif + KCommandLine::KeepOnlyCategories({&ExprCat, &SolvingCat}); bool success = true; diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 483397c1..a3062d24 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -9,18 +9,18 @@ // //===----------------------------------------------------------------------===// +#include "klee/ADT/KTest.h" #include "klee/ADT/TreeStream.h" #include "klee/Config/Version.h" #include "klee/Core/Interpreter.h" #include "klee/Expr/Expr.h" -#include "klee/ADT/KTest.h" -#include "klee/Support/OptionCategories.h" -#include "klee/Statistics/Statistics.h" #include "klee/Solver/SolverCmdLine.h" +#include "klee/Statistics/Statistics.h" #include "klee/Support/Debug.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/FileHandling.h" #include "klee/Support/ModuleUtil.h" +#include "klee/Support/OptionCategories.h" #include "klee/Support/PrintVersion.h" #include "klee/System/Time.h" @@ -44,15 +44,15 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/Path.h" #include "llvm/Support/raw_ostream.h" -#include "llvm/Support/TargetSelect.h" #include "llvm/Support/Signals.h" +#include "llvm/Support/TargetSelect.h" DISABLE_WARNING_POP #include <dirent.h> #include <signal.h> -#include <unistd.h> #include <sys/stat.h> #include <sys/wait.h> +#include <unistd.h> #include <cerrno> #include <ctime> @@ -61,7 +61,6 @@ DISABLE_WARNING_POP #include <iterator> #include <sstream> - using namespace llvm; using namespace klee; @@ -1118,13 +1117,13 @@ linkWithUclibc(StringRef libDir, std::string opt_suffix, } int main(int argc, char **argv, char **envp) { - atexit(llvm_shutdown); // Call llvm_shutdown() on exit. + atexit(llvm_shutdown); // Call llvm_shutdown() on exit -#if LLVM_VERSION_CODE >= LLVM_VERSION(13, 0) - KCommandLine::HideOptions(llvm::cl::getGeneralCategory()); -#else - KCommandLine::HideOptions(llvm::cl::GeneralCategory); -#endif + KCommandLine::KeepOnlyCategories( + {&ChecksCat, &DebugCat, &ExtCallsCat, &ExprCat, &LinkCat, + &MemoryCat, &MergeCat, &MiscCat, &ModuleCat, &ReplayCat, + &SearchCat, &SeedingCat, &SolvingCat, &StartCat, &StatsCat, + &TerminationCat, &TestCaseCat, &TestGenCat}); llvm::InitializeNativeTarget(); |