Documented default values for various options and improved the description of some.

4 files changed, 61 insertions, 36 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index dcc1b238..1724ea06 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -86,7 +86,7 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
 
 llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
     "metasmt-backend",
-    llvm::cl::desc("Specify the MetaSMT solver backend type."),
+    llvm::cl::desc("Specify the MetaSMT solver backend type (default=STP)."),
     llvm::cl::values(
         clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
         clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 33cee9f9..dc9edf5f 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -136,27 +136,33 @@ namespace {
 
   cl::opt<bool>
   SimplifySymIndices("simplify-sym-indices",
-                     cl::init(false));
+                     cl::init(false),
+		     cl::desc("Simplify symbolic accesses using equalities from other constraints (default=off)"));
 
   cl::opt<bool>
   EqualitySubstitution("equality-substitution",
-                     cl::init(true),
-                     cl::desc("Simplify equality expressions before querying the solver (default=on)."));
+		       cl::init(true),
+		       cl::desc("Simplify equality expressions before querying the solver (default=on)."));
 
   cl::opt<unsigned>
   MaxSymArraySize("max-sym-array-size",
                   cl::init(0));
 
   cl::opt<bool>
-  SuppressExternalWarnings("suppress-external-warnings");
+  SuppressExternalWarnings("suppress-external-warnings",
+			   cl::init(false),
+			   cl::desc("Supress warnings about calling external functions."));
 
   cl::opt<bool>
-  AllExternalWarnings("all-external-warnings");
+  AllExternalWarnings("all-external-warnings",
+		      cl::init(false),
+		      cl::desc("Issue an warning everytime an external call is made," 
+			       "as opposed to once per function (default=off)"));
 
   cl::opt<bool>
   OnlyOutputStatesCoveringNew("only-output-states-covering-new",
                               cl::init(false),
-			      cl::desc("Only output test cases covering new code."));
+			      cl::desc("Only output test cases covering new code (default=off)."));
 
   cl::opt<bool>
   EmitAllErrors("emit-all-errors",
@@ -173,36 +179,54 @@ namespace {
 		    cl::init(true));
 
   cl::opt<bool>
-  OnlyReplaySeeds("only-replay-seeds", 
-                  cl::desc("Discard states that do not have a seed."));
+  OnlyReplaySeeds("only-replay-seeds",
+		  cl::init(false),
+                  cl::desc("Discard states that do not have a seed (default=off)."));
  
   cl::opt<bool>
-  OnlySeed("only-seed", 
-           cl::desc("Stop execution after seeding is done without doing regular search."));
+  OnlySeed("only-seed",
+	   cl::init(false),
+           cl::desc("Stop execution after seeding is done without doing regular search (default=off)."));
  
   cl::opt<bool>
-  AllowSeedExtension("allow-seed-extension", 
-                     cl::desc("Allow extra (unbound) values to become symbolic during seeding."));
+  AllowSeedExtension("allow-seed-extension",
+		     cl::init(false),
+                     cl::desc("Allow extra (unbound) values to become symbolic during seeding (default=false)."));
  
   cl::opt<bool>
-  ZeroSeedExtension("zero-seed-extension");
+  ZeroSeedExtension("zero-seed-extension",
+		    cl::init(false),
+		    cl::desc("(default=off)"));
  
   cl::opt<bool>
-  AllowSeedTruncation("allow-seed-truncation", 
-                      cl::desc("Allow smaller buffers than in seeds."));
+  AllowSeedTruncation("allow-seed-truncation",
+		      cl::init(false),
+                      cl::desc("Allow smaller buffers than in seeds (default=off)."));
  
   cl::opt<bool>
   NamedSeedMatching("named-seed-matching",
-                    cl::desc("Use names to match symbolic objects to inputs."));
+		    cl::init(false),
+                    cl::desc("Use names to match symbolic objects to inputs (default=off)."));
 
   cl::opt<double>
-  MaxStaticForkPct("max-static-fork-pct", cl::init(1.));
+  MaxStaticForkPct("max-static-fork-pct", 
+		   cl::init(1.),
+		   cl::desc("(default=1.0)"));
+
   cl::opt<double>
-  MaxStaticSolvePct("max-static-solve-pct", cl::init(1.));
+  MaxStaticSolvePct("max-static-solve-pct",
+		    cl::init(1.),
+		    cl::desc("(default=1.0)"));
+
   cl::opt<double>
-  MaxStaticCPForkPct("max-static-cpfork-pct", cl::init(1.));
+  MaxStaticCPForkPct("max-static-cpfork-pct", 
+		     cl::init(1.),
+		     cl::desc("(default=1.0)"));
+
   cl::opt<double>
-  MaxStaticCPSolvePct("max-static-cpsolve-pct", cl::init(1.));
+  MaxStaticCPSolvePct("max-static-cpsolve-pct",
+		      cl::init(1.),
+		      cl::desc("(default=1.0)"));
 
   cl::opt<double>
   MaxInstructionTime("max-instruction-time",
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 38411c4f..b8ea97c2 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -39,7 +39,7 @@ using namespace klee;
 
 cl::opt<double>
 MaxTime("max-time",
-        cl::desc("Halt execution after the specified number of seconds (0=off)"),
+        cl::desc("Halt execution after the specified number of seconds (default=0 (off))"),
         cl::init(0));
 
 ///
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 9995b7e2..5e77172e 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -68,45 +68,46 @@ using namespace llvm;
 namespace {  
   cl::opt<bool>
   TrackInstructionTime("track-instruction-time",
-                       cl::desc("Enable tracking of time for individual instructions"),
-                       cl::init(false));
+                       cl::init(false),
+		       cl::desc("Enable tracking of time for individual instructions (default=off)"));
 
   cl::opt<bool>
   OutputStats("output-stats",
-              cl::desc("Write running stats trace file"),
-              cl::init(true));
+              cl::init(true),
+	      cl::desc("Write running stats trace file (default=on)"));
 
   cl::opt<bool>
   OutputIStats("output-istats",
-               cl::desc("Write instruction level statistics (in callgrind format)"),
-               cl::init(true));
+	       cl::init(true),
+               cl::desc("Write instruction level statistics in callgrind format (default=on)"));
 
   cl::opt<double>
   StatsWriteInterval("stats-write-interval",
-                     cl::desc("Approximate number of seconds between stats writes (default: 1.0)"),
-                     cl::init(1.));
+                     cl::init(1.),
+		     cl::desc("Approximate number of seconds between stats writes (default=1.0s)"));
 
   cl::opt<double>
   IStatsWriteInterval("istats-write-interval",
-                      cl::desc("Approximate number of seconds between istats writes (default: 10.0)"),
-                      cl::init(10.));
+		      cl::init(10.),
+                      cl::desc("Approximate number of seconds between istats writes (default: 10.0s)"));
 
   /*
   cl::opt<double>
   BranchCovCountsWriteInterval("branch-cov-counts-write-interval",
-                     cl::desc("Approximate number of seconds between run.branches writes (default: 5.0)"),
+                     cl::desc("Approximate number of seconds between run.branches writes (default: 5.0s)"),
                      cl::init(5.));
   */
 
   // XXX I really would like to have dynamic rate control for something like this.
   cl::opt<double>
   UncoveredUpdateInterval("uncovered-update-interval",
-                          cl::init(30.));
+                          cl::init(30.),
+			  cl::desc("(default=30.0s)"));
   
   cl::opt<bool>
   UseCallPaths("use-call-paths",
-               cl::desc("Enable calltree tracking for instruction level statistics"),
-               cl::init(true));
+	       cl::init(true),
+               cl::desc("Enable calltree tracking for instruction level statistics (default=on)"));
   
 }