about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2018-12-18 14:19:08 +0000
committerMartinNowack <martin.nowack@gmail.com>2018-12-19 13:25:31 +0000
commitc44b6aa52812d712860677af18d586bea18d3c94 (patch)
tree9eea8045ffc7341dae8d3fd57b6186c0347e45b4
parent19d36f8ce251f9cfa3405b9d8e3d2c30828ce632 (diff)
downloadklee-c44b6aa52812d712860677af18d586bea18d3c94.tar.gz
Added some descriptions suggested by @MartinNowack and placed --max-static-... options under the termination category of options
-rw-r--r--lib/Core/Executor.cpp51
1 files changed, 27 insertions, 24 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 3ef6a116..6ac24447 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -182,7 +182,7 @@ namespace {
   cl::opt<bool>
   AlwaysOutputSeeds("always-output-seeds",
 		    cl::init(true),
-                    cl::desc("(default=true)"),
+                    cl::desc("Dump test cases even if they are driven by seeds only (default=true)"),
                     cl::cat(SeedingCat));
 
   cl::opt<bool>
@@ -206,7 +206,7 @@ namespace {
   cl::opt<bool>
   ZeroSeedExtension("zero-seed-extension",
 		    cl::init(false),
-		    cl::desc("(default=off)"),
+		    cl::desc("Use zero-filled objects if matching seed not found (default=off)"),
                     cl::cat(SeedingCat));
  
   cl::opt<bool>
@@ -293,7 +293,31 @@ namespace {
                      cl::desc("Allow a single instruction to take only this much time (default=0s (off)). Enables --use-forked-solver"),
                      cl::cat(TerminationCat));
 
-  
+  cl::opt<double>
+  MaxStaticForkPct("max-static-fork-pct",
+		   cl::init(1.),
+		   cl::desc("Maximum percentage spent by an instruction forking out of the forking of all instructions (default=1.0 (always))"),
+                   cl::cat(TerminationCat));
+
+  cl::opt<double>
+  MaxStaticSolvePct("max-static-solve-pct",
+		    cl::init(1.),
+		    cl::desc("Maximum percentage of solving time that can be spent by a single instruction over total solving time for all instructions (default=1.0 (always))"),
+                    cl::cat(TerminationCat));
+
+  cl::opt<double>
+  MaxStaticCPForkPct("max-static-cpfork-pct", 
+		     cl::init(1.),
+		     cl::desc("Maximum percentage spent by an instruction of a call path forking out of the forking of all instructions in the call path (default=1.0 (always))"),
+                     cl::cat(TerminationCat));
+
+  cl::opt<double>
+  MaxStaticCPSolvePct("max-static-cpsolve-pct",
+		      cl::init(1.),
+		      cl::desc("Maximum percentage of solving time that can be spent by a single instruction of a call path over total solving time for all instructions (default=1.0 (always))"),
+                      cl::cat(TerminationCat));
+
+
 
   /*** Debugging options ***/
 
@@ -337,27 +361,6 @@ namespace {
 
   cl::opt<bool>
   DebugCheckForImpliedValues("debug-check-for-implied-values");
-
-
-  cl::opt<double>
-  MaxStaticForkPct("max-static-fork-pct", 
-		   cl::init(1.),
-		   cl::desc("(default=1.0)"));
-
-  cl::opt<double>
-  MaxStaticSolvePct("max-static-solve-pct",
-		    cl::init(1.),
-		    cl::desc("(default=1.0)"));
-
-  cl::opt<double>
-  MaxStaticCPForkPct("max-static-cpfork-pct", 
-		     cl::init(1.),
-		     cl::desc("(default=1.0)"));
-
-  cl::opt<double>
-  MaxStaticCPSolvePct("max-static-cpsolve-pct",
-		      cl::init(1.),
-		      cl::desc("(default=1.0)"));
   
 }