aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Module
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-03-14 23:07:20 +0000
committerMartinNowack <martin.nowack@gmail.com>2019-03-15 10:29:55 +0000
commitf20a470e350b9a80f8e0bd7b01d47083cdb33aee (patch)
tree6cf32ee064a0cd5b6bbaf2f269d224a8d96c4b3c /lib/Module
parentd13e0cbbaad29c23fc8e3bb17f3f5154990cbd6f (diff)
downloadklee-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.cpp33
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));
}
/***/