diff options
| -rw-r--r-- | include/klee/OptionCategories.h | 3 | ||||
| -rw-r--r-- | lib/Module/KModule.cpp | 33 |
2 files changed, 24 insertions, 12 deletions
diff --git a/include/klee/OptionCategories.h b/include/klee/OptionCategories.h index d0e359fa..e107f853 100644 --- a/include/klee/OptionCategories.h +++ b/include/klee/OptionCategories.h @@ -17,8 +17,9 @@ #include "llvm/Support/CommandLine.h" namespace klee { - extern llvm::cl::OptionCategory SolvingCat; extern llvm::cl::OptionCategory MergeCat; + extern llvm::cl::OptionCategory ModuleCat; + extern llvm::cl::OptionCategory SolvingCat; } #endif diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 4a2e6e79..4817b6cc 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -8,18 +8,20 @@ //===----------------------------------------------------------------------===// #define DEBUG_TYPE "KModule" -#include "klee/Internal/Module/KModule.h" -#include "klee/Internal/Support/ErrorHandling.h" #include "Passes.h" #include "klee/Config/Version.h" -#include "klee/Interpreter.h" #include "klee/Internal/Module/Cell.h" -#include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Module/InstructionInfoTable.h" +#include "klee/Internal/Module/KInstruction.h" +#include "klee/Internal/Module/KModule.h" +#include "klee/Internal/Module/LLVMPassManager.h" #include "klee/Internal/Support/Debug.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/Support/ModuleUtil.h" +#include "klee/Interpreter.h" +#include "klee/OptionCategories.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) #include "llvm/Bitcode/BitcodeWriter.h" @@ -42,7 +44,6 @@ #include "llvm/Linker/Linker.h" #endif -#include "klee/Internal/Module/LLVMPassManager.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Support/raw_os_ostream.h" @@ -63,6 +64,12 @@ using namespace llvm; using namespace klee; +namespace klee { +cl::OptionCategory + ModuleCat("Module-related options", + "These options affect the compile-time processing of the code."); +} + namespace { enum SwitchImplType { eSwitchTypeSimple, @@ -72,16 +79,18 @@ namespace { cl::opt<bool> OutputSource("output-source", - cl::desc("Write the assembly for the final transformed source"), - cl::init(true)); + cl::desc("Write the assembly for the final transformed source (default=true)"), + cl::init(true), + cl::cat(ModuleCat)); cl::opt<bool> OutputModule("output-module", cl::desc("Write the bitcode for the final transformed module"), - cl::init(false)); + cl::init(false), + cl::cat(ModuleCat)); cl::opt<SwitchImplType> - SwitchType("switch-type", cl::desc("Select the implementation of switch"), + SwitchType("switch-type", cl::desc("Select the implementation of switch (default=internal)"), cl::values(clEnumValN(eSwitchTypeSimple, "simple", "lower to ordered branches"), clEnumValN(eSwitchTypeLLVM, "llvm", @@ -89,11 +98,13 @@ namespace { clEnumValN(eSwitchTypeInternal, "internal", "execute switch internally") KLEE_LLVM_CL_VAL_END), - cl::init(eSwitchTypeInternal)); + cl::init(eSwitchTypeInternal), + cl::cat(ModuleCat)); cl::opt<bool> DebugPrintEscapingFunctions("debug-print-escaping-functions", - cl::desc("Print functions whose address is taken.")); + cl::desc("Print functions whose address is taken (default=false)"), + cl::cat(ModuleCat)); } /***/ |