aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-03-11 13:13:58 +0000
committerMartinNowack <martin.nowack@gmail.com>2019-03-13 10:25:33 +0000
commit92fd446f72136594e6519065fbd5bca3e0aee8e3 (patch)
treec324641a9054253cd22da88094680f6d1d305621
parent8cfce20c9c53b6ec4ff2d54c9fa2b494ee699ebc (diff)
downloadklee-92fd446f72136594e6519065fbd5bca3e0aee8e3.tar.gz
Consistently use "default=true" and "default=false" instead of "default=on" and "default=off" in --help
-rw-r--r--lib/Basic/CmdLineOptions.cpp16
-rw-r--r--lib/Core/Executor.cpp28
-rw-r--r--lib/Core/MemoryManager.cpp4
-rw-r--r--lib/Core/StatsTracker.cpp8
-rw-r--r--lib/Core/UserSearcher.cpp4
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp2
-rw-r--r--lib/Expr/Constraints.cpp2
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp2
-rw-r--r--lib/Solver/CexCachingSolver.cpp6
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp4
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