diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-14 23:07:20 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-03-15 10:29:55 +0000 |
commit | f20a470e350b9a80f8e0bd7b01d47083cdb33aee (patch) | |
tree | 6cf32ee064a0cd5b6bbaf2f269d224a8d96c4b3c /lib/Module | |
parent | d13e0cbbaad29c23fc8e3bb17f3f5154990cbd6f (diff) | |
download | klee-f20a470e350b9a80f8e0bd7b01d47083cdb33aee.tar.gz |
Created a new module-related option category and moved the options in KModule.cpp in there
Diffstat (limited to 'lib/Module')
-rw-r--r-- | lib/Module/KModule.cpp | 33 |
1 files changed, 22 insertions, 11 deletions
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)); } /***/ |