about summary refs log tree commit diff homepage
path: root/tools
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2018-12-18 15:17:28 +0000
committerMartinNowack <martin.nowack@gmail.com>2018-12-19 21:26:48 +0000
commitb7b53fa5a7dbeb906fff9b117b76944fd6de27a2 (patch)
tree08f723a12c493e3aac50e52e9c98ecb681e133b9 /tools
parent6a8ec2bd4d9b1c2c70408d529a50c8c1c3d041ef (diff)
downloadklee-b7b53fa5a7dbeb906fff9b117b76944fd6de27a2.tar.gz
Added checks option category, moved --optimize to starting category, renamed original --run-in option to --running-dir
Diffstat (limited to 'tools')
-rw-r--r--tools/klee/main.cpp53
1 files changed, 32 insertions, 21 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index af97b759..a5130429 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -133,14 +133,26 @@ namespace {
 
   cl::opt<std::string>
   RunInDir("run-in-dir",
-           cl::desc("Change to the given directory prior to executing"),
+           cl::desc("Change to the given directory before starting execution"),
            cl::cat(StartCat));
+  
+  cl::opt<std::string>
+  OutputDir("output-dir",
+            cl::desc("Directory in which to write results (default=klee-out-<N>)"),
+            cl::init(""),
+            cl::cat(StartCat));
 
   cl::opt<std::string>
   Environ("environ",
           cl::desc("Parse environment from given file (in \"env\" format)"),
           cl::cat(StartCat));
 
+  cl::opt<bool>
+  OptimizeModule("optimize",
+                 cl::desc("Optimize the code before execution"),
+		 cl::init(false),
+                 cl::cat(StartCat));
+  
 
   /*** Linking options ***/
 
@@ -178,6 +190,25 @@ namespace {
                    cl::cat(LinkCat));
 
 
+  /*** Checks options ***/
+
+  cl::OptionCategory ChecksCat("Checks options",
+                               "These options control some of the checks being done by KLEE.");
+
+  cl::opt<bool>
+  CheckDivZero("check-div-zero",
+               cl::desc("Inject checks for division-by-zero (default=true)"),
+               cl::init(true),
+               cl::cat(ChecksCat));
+
+  cl::opt<bool>
+  CheckOvershift("check-overshift",
+                 cl::desc("Inject checks for overshift (default=true)"),
+                 cl::init(true),
+                 cl::cat(ChecksCat));
+
+ 
+
   cl::opt<bool>
   NoOutput("no-output",
            cl::desc("Don't generate test files"));
@@ -191,26 +222,6 @@ namespace {
               cl::desc("Exit if errors occur"));
 
   cl::opt<bool>
-  OptimizeModule("optimize",
-                 cl::desc("Optimize before execution"),
-		 cl::init(false));
-
-  cl::opt<bool>
-  CheckDivZero("check-div-zero",
-               cl::desc("Inject checks for division-by-zero"),
-               cl::init(true));
-
-  cl::opt<bool>
-  CheckOvershift("check-overshift",
-               cl::desc("Inject checks for overshift"),
-               cl::init(true));
-
-  cl::opt<std::string>
-  OutputDir("output-dir",
-            cl::desc("Directory to write results in (defaults to klee-out-N)"),
-            cl::init(""));
-
-  cl::opt<bool>
   ReplayKeepSymbolic("replay-keep-symbolic",
                      cl::desc("Replay the test cases only by asserting "
                               "the bytes, not necessarily making them concrete."));