diff options
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 16 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 28 | ||||
| -rw-r--r-- | lib/Core/MemoryManager.cpp | 4 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 8 | ||||
| -rw-r--r-- | lib/Core/UserSearcher.cpp | 4 | ||||
| -rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 2 | ||||
| -rw-r--r-- | lib/Expr/Constraints.cpp | 2 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 2 | ||||
| -rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 6 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 4 |
10 files changed, 38 insertions, 38 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 9976a7ad..05ee2821 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -39,26 +39,26 @@ cl::OptionCategory SolvingCat("Constraint solving options", cl::opt<bool> UseFastCexSolver( "use-fast-cex-solver", cl::init(false), - cl::desc("Enable an experimental range-based solver (default=off)"), + cl::desc("Enable an experimental range-based solver (default=false)"), cl::cat(SolvingCat)); cl::opt<bool> UseCexCache("use-cex-cache", cl::init(true), - cl::desc("Use counterexample caching (default=on)"), + cl::desc("Use counterexample caching (default=true)"), cl::cat(SolvingCat)); cl::opt<bool> UseCache("use-cache", cl::init(true), - cl::desc("Use validity caching (default=on)"), + cl::desc("Use validity caching (default=true)"), cl::cat(SolvingCat)); cl::opt<bool> UseIndependentSolver("use-independent-solver", cl::init(true), - cl::desc("Use constraint independence (default=on)"), + cl::desc("Use constraint independence (default=true)"), cl::cat(SolvingCat)); cl::opt<bool> DebugValidateSolver( "debug-validate-solver", cl::init(false), cl::desc("Crosscheck the results of the solver chain above the core solver " - "with the results of the core solver (default=off)"), + "with the results of the core solver (default=false)"), cl::cat(SolvingCat)); cl::opt<std::string> MinQueryTimeToLog( @@ -80,13 +80,13 @@ cl::opt<std::string> MaxCoreSolverTime( cl::opt<bool> UseForkedCoreSolver( "use-forked-solver", - cl::desc("Run the core SMT solver in a forked process (default=on)"), + cl::desc("Run the core SMT solver in a forked process (default=true)"), cl::init(true), cl::cat(SolvingCat)); cl::opt<bool> CoreSolverOptimizeDivides( "solver-optimize-divides", cl::desc("Optimize constant divides into add/shift/multiplies before " - "passing them to the core SMT solver (default=off)"), + "passing them to the core SMT solver (default=false)"), cl::init(false), cl::cat(SolvingCat)); cl::bits<QueryLoggingSolverType> QueryLoggingOptions( @@ -109,7 +109,7 @@ cl::bits<QueryLoggingSolverType> QueryLoggingOptions( cl::opt<bool> UseAssignmentValidatingSolver( "debug-assignment-validating-solver", cl::init(false), - cl::desc("Debug the correctness of generated assignments (default=off)"), + cl::desc("Debug the correctness of generated assignments (default=false)"), cl::cat(SolvingCat)); void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 488ffa34..abb5be7d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -103,20 +103,20 @@ namespace { cl::opt<bool> DumpStatesOnHalt("dump-states-on-halt", cl::init(true), - cl::desc("Dump test cases for all active states on exit (default=on)"), + cl::desc("Dump test cases for all active states on exit (default=true)"), cl::cat(TestGenCat)); cl::opt<bool> OnlyOutputStatesCoveringNew("only-output-states-covering-new", cl::init(false), - cl::desc("Only output test cases covering new code (default=off)."), + cl::desc("Only output test cases covering new code (default=false)."), cl::cat(TestGenCat)); cl::opt<bool> EmitAllErrors("emit-all-errors", cl::init(false), cl::desc("Generate tests cases for all errors " - "(default=off, i.e. one per (error,instruction) pair)"), + "(default=false, i.e. one per (error,instruction) pair)"), cl::cat(TestGenCat)); @@ -125,12 +125,12 @@ namespace { cl::opt<bool> SimplifySymIndices("simplify-sym-indices", cl::init(false), - cl::desc("Simplify symbolic accesses using equalities from other constraints (default=off)")); + cl::desc("Simplify symbolic accesses using equalities from other constraints (default=false)")); cl::opt<bool> EqualitySubstitution("equality-substitution", cl::init(true), - cl::desc("Simplify equality expressions before querying the solver (default=on).")); + cl::desc("Simplify equality expressions before querying the solver (default=true).")); cl::opt<unsigned> MaxSymArraySize("max-sym-array-size", @@ -169,7 +169,7 @@ namespace { AllExternalWarnings("all-external-warnings", cl::init(false), cl::desc("Issue a warning everytime an external call is made, " - "as opposed to once per function (default=off)"), + "as opposed to once per function (default=false)"), cl::cat(ExtCallsCat)); @@ -187,13 +187,13 @@ namespace { cl::opt<bool> OnlyReplaySeeds("only-replay-seeds", cl::init(false), - cl::desc("Discard states that do not have a seed (default=off)."), + cl::desc("Discard states that do not have a seed (default=false)."), cl::cat(SeedingCat)); cl::opt<bool> OnlySeed("only-seed", cl::init(false), - cl::desc("Stop execution after seeding is done without doing regular search (default=off)."), + cl::desc("Stop execution after seeding is done without doing regular search (default=false)."), cl::cat(SeedingCat)); cl::opt<bool> @@ -205,19 +205,19 @@ namespace { cl::opt<bool> ZeroSeedExtension("zero-seed-extension", cl::init(false), - cl::desc("Use zero-filled objects if matching seed not found (default=off)"), + cl::desc("Use zero-filled objects if matching seed not found (default=false)"), cl::cat(SeedingCat)); cl::opt<bool> AllowSeedTruncation("allow-seed-truncation", cl::init(false), - cl::desc("Allow smaller buffers than in seeds (default=off)."), + cl::desc("Allow smaller buffers than in seeds (default=false)."), cl::cat(SeedingCat)); cl::opt<bool> NamedSeedMatching("named-seed-matching", cl::init(false), - cl::desc("Use names to match symbolic objects to inputs (default=off)."), + cl::desc("Use names to match symbolic objects to inputs (default=false)."), cl::cat(SeedingCat)); cl::opt<std::string> @@ -233,7 +233,7 @@ namespace { cl::list<Executor::TerminateReason> ExitOnErrorType("exit-on-error-type", - cl::desc("Stop execution after reaching a specified condition (default=off)"), + cl::desc("Stop execution after reaching a specified condition (default=false)"), cl::values( clEnumValN(Executor::Abort, "Abort", "The program crashed"), clEnumValN(Executor::Assert, "Assert", "An assertion was hit"), @@ -278,7 +278,7 @@ namespace { cl::opt<bool> MaxMemoryInhibit("max-memory-inhibit", - cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=on)"), + cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=true)"), cl::init(true), cl::cat(TerminationCat)); @@ -361,7 +361,7 @@ namespace { cl::opt<bool> DebugCompressInstructions("debug-compress-instructions", cl::init(false), - cl::desc("Compress the logged instructions in gzip format (default=off)."), + cl::desc("Compress the logged instructions in gzip format (default=false)."), cl::cat(DebugCat)); #endif diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp index b8762c65..f98a8a34 100644 --- a/lib/Core/MemoryManager.cpp +++ b/lib/Core/MemoryManager.cpp @@ -29,7 +29,7 @@ llvm::cl::OptionCategory MemoryCat("Memory management options", llvm::cl::opt<bool> DeterministicAllocation( "allocate-determ", - llvm::cl::desc("Allocate memory deterministically (default=off)"), + llvm::cl::desc("Allocate memory deterministically (default=false)"), llvm::cl::init(false), llvm::cl::cat(MemoryCat)); llvm::cl::opt<unsigned> DeterministicAllocationSize( @@ -40,7 +40,7 @@ llvm::cl::opt<unsigned> DeterministicAllocationSize( llvm::cl::opt<bool> NullOnZeroMalloc( "return-null-on-zero-malloc", - llvm::cl::desc("Returns NULL if malloc(0) is called (default=off)"), + llvm::cl::desc("Returns NULL if malloc(0) is called (default=false)"), llvm::cl::init(false), llvm::cl::cat(MemoryCat)); llvm::cl::opt<unsigned> RedZoneSpace( diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 5ad0f174..0300d1ba 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -58,17 +58,17 @@ namespace { cl::opt<bool> TrackInstructionTime("track-instruction-time", cl::init(false), - cl::desc("Enable tracking of time for individual instructions (default=off)")); + cl::desc("Enable tracking of time for individual instructions (default=false)")); cl::opt<bool> OutputStats("output-stats", cl::init(true), - cl::desc("Write running stats trace file (default=on)")); + cl::desc("Write running stats trace file (default=true)")); cl::opt<bool> OutputIStats("output-istats", cl::init(true), - cl::desc("Write instruction level statistics in callgrind format (default=on)")); + cl::desc("Write instruction level statistics in callgrind format (default=true)")); cl::opt<std::string> StatsWriteInterval("stats-write-interval", @@ -99,7 +99,7 @@ namespace { cl::opt<bool> UseCallPaths("use-call-paths", cl::init(true), - cl::desc("Enable calltree tracking for instruction level statistics (default=on)")); + cl::desc("Enable calltree tracking for instruction level statistics (default=true)")); } diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 4af732e5..754b3796 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -55,14 +55,14 @@ cl::list<Searcher::CoreSearchType> CoreSearch( cl::opt<bool> UseIterativeDeepeningTimeSearch( "use-iterative-deepening-time-search", cl::desc( - "Use iterative deepening time search (experimental) (default=off)"), + "Use iterative deepening time search (experimental) (default=false)"), cl::init(false), cl::cat(SearchCat)); cl::opt<bool> UseBatchingSearch( "use-batching-search", cl::desc("Use batching searcher (keep running selected state for N " "instructions/time, see --batch-instructions and --batch-time) " - "(default=off)"), + "(default=false)"), cl::init(false), cl::cat(SearchCat)); cl::opt<unsigned> diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index d043783a..43b289e2 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -42,7 +42,7 @@ llvm::cl::opt<ArrayOptimizationType> OptimizeArray( KLEE_LLVM_CL_VAL_END), llvm::cl::init(NONE), llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " - "arrays. (default=off)"), + "arrays. (default=false)"), llvm::cl::cat(klee::SolvingCat)); llvm::cl::opt<double> ArrayValueRatio( diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 1b3ad983..8bf6bc58 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -24,7 +24,7 @@ namespace { llvm::cl::opt<bool> RewriteEqualities("rewrite-equalities", llvm::cl::init(true), - llvm::cl::desc("Rewrite existing constraints when an equality with a constant is added (default=on)")); + llvm::cl::desc("Rewrite existing constraints when an equality with a constant is added (default=true)")); } diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index fd515509..8e0810ad 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -32,7 +32,7 @@ argConstantDisplayMode( llvm::cl::opt<bool> humanReadableSMTLIB( "smtlib-human-readable", llvm::cl::desc( - "Enables generated SMT-LIBv2 files to be human readable (default=off)"), + "Enables generated SMT-LIBv2 files to be human readable (default=false)"), llvm::cl::init(false)); llvm::cl::opt<klee::ExprSMTLIBPrinter::AbbreviationMode> abbreviationMode( diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 8bf41ee6..d2e080d9 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -30,13 +30,13 @@ namespace { cl::opt<bool> DebugCexCacheCheckBinding( "debug-cex-cache-check-binding", cl::init(false), cl::desc("Debug the correctness of the counterexample " - "cache assignments (default=off)"), + "cache assignments (default=false)"), cl::cat(SolvingCat)); cl::opt<bool> CexCacheTryAll("cex-cache-try-all", cl::init(false), cl::desc("Try substituting all counterexamples before " - "asking the SMT solver (default=off)"), + "asking the SMT solver (default=false)"), cl::cat(SolvingCat)); cl::opt<bool> @@ -47,7 +47,7 @@ cl::opt<bool> cl::opt<bool> CexCacheExperimental( "cex-cache-exp", cl::init(false), - cl::desc("Optimization for validity queries (default=off)"), + cl::desc("Optimization for validity queries (default=false)"), cl::cat(SolvingCat)); } // namespace diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 4e06d1b2..19716e84 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -18,13 +18,13 @@ namespace { llvm::cl::opt<bool> DumpPartialQueryiesEarly( "log-partial-queries-early", llvm::cl::init(false), - llvm::cl::desc("Log queries before calling the solver (default=off)"), + llvm::cl::desc("Log queries before calling the solver (default=false)"), llvm::cl::cat(klee::SolvingCat)); #ifdef HAVE_ZLIB_H llvm::cl::opt<bool> CreateCompressedQueryLog( "compress-query-log", llvm::cl::init(false), - llvm::cl::desc("Compress query log files (default=off)"), + llvm::cl::desc("Compress query log files (default=false)"), llvm::cl::cat(klee::SolvingCat)); #endif } // namespace |