Documented several KLEE options.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160779 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 36 insertions, 30 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 278f8941..d61cb5dd 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -86,7 +86,8 @@ using namespace klee;
 namespace {
   cl::opt<bool>
   DumpStatesOnHalt("dump-states-on-halt",
-                   cl::init(true));
+                   cl::init(true),
+		   "Dump test cases for all active states on exit (default=on)");
  
   cl::opt<bool>
   NoPreferCex("no-prefer-cex",
@@ -102,7 +103,8 @@ namespace {
  
   cl::opt<bool>
   AllowExternalSymCalls("allow-external-sym-calls",
-                        cl::init(false));
+                        cl::init(false),
+			cl::desc("Allow calls with symbolic arguments to external functions.  This concretizes the symbolic arguments.  (default=off)"));
 
   cl::opt<bool>
   DebugPrintInstructions("debug-print-instructions", 
@@ -132,48 +134,52 @@ namespace {
 
   cl::opt<bool>
   OnlyOutputStatesCoveringNew("only-output-states-covering-new",
-                              cl::init(false));
-
-  cl::opt<bool>
-  AlwaysOutputSeeds("always-output-seeds",
-                              cl::init(true));
+                              cl::init(false),
+			      cl::desc("Only output test cases covering new code."));
 
   cl::opt<bool>
   UseFastCexSolver("use-fast-cex-solver",
-		   cl::init(false));
+		   cl::init(false),
+		   cl::desc("(default=off"));
 
   cl::opt<bool>
   UseIndependentSolver("use-independent-solver",
                        cl::init(true),
-		       cl::desc("Use constraint independence"));
+		       cl::desc("Use constraint independence (default=on)"));
 
   cl::opt<bool>
   EmitAllErrors("emit-all-errors",
                 cl::init(false),
                 cl::desc("Generate tests cases for all errors "
-                         "(default=one per (error,instruction) pair)"));
+                         "(default=off, i.e. one per (error,instruction) pair)"));
 
   cl::opt<bool>
   UseCexCache("use-cex-cache",
               cl::init(true),
-	      cl::desc("Use counterexample caching"));
+	      cl::desc("Use counterexample caching (default=on)"));
 
   cl::opt<bool>
   UseQueryPCLog("use-query-pc-log",
-                cl::init(false));
+                cl::init(false),
+		cl::desc("Log all queries into queries.pc (default=off)"));
   
   cl::opt<bool>
   UseSTPQueryPCLog("use-stp-query-pc-log",
-                   cl::init(false));
+                   cl::init(false),
+		   cl::desc("Log all queries sent to STP into queries.pc (default=off)"));
 
   cl::opt<bool>
   NoExternals("no-externals", 
-           cl::desc("Do not allow external functin calls"));
+           cl::desc("Do not allow external function calls (default=off)"));
 
   cl::opt<bool>
   UseCache("use-cache",
 	   cl::init(true),
-	   cl::desc("Use validity caching"));
+	   cl::desc("Use validity caching (default=on)"));
+
+  cl::opt<bool>
+  AlwaysOutputSeeds("always-output-seeds",
+		    cl::init(true));
 
   cl::opt<bool>
   OnlyReplaySeeds("only-replay-seeds", 
@@ -224,36 +230,36 @@ namespace {
   
   cl::opt<unsigned int>
   StopAfterNInstructions("stop-after-n-instructions",
-                         cl::desc("Stop execution after specified number of instructions (0=off)"),
+                         cl::desc("Stop execution after specified number of instructions (default=0 (off))"),
                          cl::init(0));
   
   cl::opt<unsigned>
   MaxForks("max-forks",
-           cl::desc("Only fork this many times (-1=off)"),
+           cl::desc("Only fork this many times (default=-1 (off))"),
            cl::init(~0u));
   
   cl::opt<unsigned>
   MaxDepth("max-depth",
-           cl::desc("Only allow this many symbolic branches (0=off)"),
+           cl::desc("Only allow this many symbolic branches (default=0 (off))"),
            cl::init(0));
   
   cl::opt<unsigned>
   MaxMemory("max-memory",
-            cl::desc("Refuse to fork when more above this about of memory (in MB, 0=off)"),
+            cl::desc("Refuse to fork when above this amount of memory (in MB, default=0 (off))"),
             cl::init(0));
 
   cl::opt<bool>
   MaxMemoryInhibit("max-memory-inhibit",
-            cl::desc("Inhibit forking at memory cap (vs. random terminate)"),
+            cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=on)"),
             cl::init(true));
 
   cl::opt<bool>
-  UseForkedSTP("use-forked-stp", 
-                 cl::desc("Run STP in a forked process (default=off)"));
+  UseForkedSTP("use-forked-stp",
+	       cl::desc("Run STP in a forked process (default=off)"));
 
   cl::opt<bool>
   STPOptimizeDivides("stp-optimize-divides", 
-                 cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP"),
+                 cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"),
                  cl::init(true));
 }
 
@@ -722,7 +728,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
   solver->setTimeout(0);
   if (!success) {
     current.pc = current.prevPC;
-    terminateStateEarly(current, "query timed out");
+    terminateStateEarly(current, "Query timed out (fork).");
     return StatePair(0, 0);
   }
 
@@ -899,8 +905,8 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 
     // Kinda gross, do we even really still want this option?
     if (MaxDepth && MaxDepth<=trueState->depth) {
-      terminateStateEarly(*trueState, "max-depth exceeded");
-      terminateStateEarly(*falseState, "max-depth exceeded");
+      terminateStateEarly(*trueState, "max-depth exceeded.");
+      terminateStateEarly(*falseState, "max-depth exceeded.");
       return StatePair(0, 0);
     }
 
@@ -2530,7 +2536,7 @@ void Executor::run(ExecutionState &initialState) {
                 idx = rand() % N;
 
               std::swap(arr[idx], arr[N-1]);
-              terminateStateEarly(*arr[N-1], "memory limit");
+              terminateStateEarly(*arr[N-1], "Memory limit exceeded.");
             }
           }
           atMemoryLimit = true;
@@ -2554,7 +2560,7 @@ void Executor::run(ExecutionState &initialState) {
          it != ie; ++it) {
       ExecutionState &state = **it;
       stepInstruction(state); // keep stats rolling
-      terminateStateEarly(state, "execution halting");
+      terminateStateEarly(state, "Execution halting.");
     }
     updateStates(0);
   }
@@ -3041,7 +3047,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     solver->setTimeout(0);
     if (!success) {
       state.pc = state.prevPC;
-      terminateStateEarly(state, "query timed out");
+      terminateStateEarly(state, "Query timed out (bounds check).");
       return;
     }
 
@@ -3114,7 +3120,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   // XXX should we distinguish out of bounds and overlapped cases?
   if (unbound) {
     if (incomplete) {
-      terminateStateEarly(*unbound, "query timed out (resolve)");
+      terminateStateEarly(*unbound, "Query timed out (resolve).");
     } else {
       terminateStateOnError(*unbound,
                             "memory error: out of bound pointer",