diff options
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 2 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 64 | ||||
| -rw-r--r-- | lib/Core/ExecutorTimers.cpp | 2 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 29 |
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)")); } |