diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-12-18 14:19:08 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2018-12-19 13:25:31 +0000 |
commit | c44b6aa52812d712860677af18d586bea18d3c94 (patch) | |
tree | 9eea8045ffc7341dae8d3fd57b6186c0347e45b4 | |
parent | 19d36f8ce251f9cfa3405b9d8e3d2c30828ce632 (diff) | |
download | klee-c44b6aa52812d712860677af18d586bea18d3c94.tar.gz |
Added some descriptions suggested by @MartinNowack and placed --max-static-... options under the termination category of options
-rw-r--r-- | lib/Core/Executor.cpp | 51 |
1 files changed, 27 insertions, 24 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3ef6a116..6ac24447 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -182,7 +182,7 @@ namespace { cl::opt<bool> AlwaysOutputSeeds("always-output-seeds", cl::init(true), - cl::desc("(default=true)"), + cl::desc("Dump test cases even if they are driven by seeds only (default=true)"), cl::cat(SeedingCat)); cl::opt<bool> @@ -206,7 +206,7 @@ namespace { cl::opt<bool> ZeroSeedExtension("zero-seed-extension", cl::init(false), - cl::desc("(default=off)"), + cl::desc("Use zero-filled objects if matching seed not found (default=off)"), cl::cat(SeedingCat)); cl::opt<bool> @@ -293,7 +293,31 @@ namespace { cl::desc("Allow a single instruction to take only this much time (default=0s (off)). Enables --use-forked-solver"), cl::cat(TerminationCat)); - + cl::opt<double> + MaxStaticForkPct("max-static-fork-pct", + cl::init(1.), + cl::desc("Maximum percentage spent by an instruction forking out of the forking of all instructions (default=1.0 (always))"), + cl::cat(TerminationCat)); + + cl::opt<double> + MaxStaticSolvePct("max-static-solve-pct", + cl::init(1.), + cl::desc("Maximum percentage of solving time that can be spent by a single instruction over total solving time for all instructions (default=1.0 (always))"), + cl::cat(TerminationCat)); + + cl::opt<double> + MaxStaticCPForkPct("max-static-cpfork-pct", + cl::init(1.), + cl::desc("Maximum percentage spent by an instruction of a call path forking out of the forking of all instructions in the call path (default=1.0 (always))"), + cl::cat(TerminationCat)); + + cl::opt<double> + MaxStaticCPSolvePct("max-static-cpsolve-pct", + cl::init(1.), + cl::desc("Maximum percentage of solving time that can be spent by a single instruction of a call path over total solving time for all instructions (default=1.0 (always))"), + cl::cat(TerminationCat)); + + /*** Debugging options ***/ @@ -337,27 +361,6 @@ namespace { cl::opt<bool> DebugCheckForImpliedValues("debug-check-for-implied-values"); - - - cl::opt<double> - MaxStaticForkPct("max-static-fork-pct", - cl::init(1.), - cl::desc("(default=1.0)")); - - cl::opt<double> - MaxStaticSolvePct("max-static-solve-pct", - cl::init(1.), - cl::desc("(default=1.0)")); - - cl::opt<double> - MaxStaticCPForkPct("max-static-cpfork-pct", - cl::init(1.), - cl::desc("(default=1.0)")); - - cl::opt<double> - MaxStaticCPSolvePct("max-static-cpsolve-pct", - cl::init(1.), - cl::desc("(default=1.0)")); } |