about summary refs log tree commit diff homepage
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
parentd13e0cbbaad29c23fc8e3bb17f3f5154990cbd6f (diff)
downloadklee-f20a470e350b9a80f8e0bd7b01d47083cdb33aee.tar.gz
Created a new module-related option category and moved the options in KModule.cpp in there
-rw-r--r--include/klee/OptionCategories.h3
-rw-r--r--lib/Module/KModule.cpp33
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));
 }
 
 /***/