diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-15 12:45:13 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-03-15 22:53:39 +0000 |
commit | 380622261e76f89b482d227a2c54413e0bb7f1f3 (patch) | |
tree | ada060c53c73803a9855f0b957d59d703f3bd4c9 | |
parent | 7885041375ae3b878dbd7bafaf80ad21e38ab2bc (diff) | |
download | klee-380622261e76f89b482d227a2c54413e0bb7f1f3.tar.gz |
Placed --exit-on-error, --max-tests and --watchdog in the termination category
-rw-r--r-- | include/klee/OptionCategories.h | 2 | ||||
-rw-r--r-- | tools/klee/main.cpp | 17 |
2 files changed, 13 insertions, 6 deletions
diff --git a/include/klee/OptionCategories.h b/include/klee/OptionCategories.h index bcf224bd..26cfc694 100644 --- a/include/klee/OptionCategories.h +++ b/include/klee/OptionCategories.h @@ -17,10 +17,12 @@ #include "llvm/Support/CommandLine.h" namespace klee { + extern llvm::cl::OptionCategory DebugCat; extern llvm::cl::OptionCategory MergeCat; extern llvm::cl::OptionCategory ModuleCat; extern llvm::cl::OptionCategory SeedingCat; extern llvm::cl::OptionCategory SolvingCat; + extern llvm::cl::OptionCategory TerminationCat; } #endif diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 24b96867..36015c5e 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -221,7 +221,9 @@ namespace { cl::opt<bool> OptExitOnError("exit-on-error", - cl::desc("Exit KLEE if an error in the tested application has been found (default=false).")); + cl::desc("Exit KLEE if an error in the tested application has been found (default=false)"), + cl::init(false), + cl::cat(TerminationCat)); /*** Replaying options ***/ @@ -269,18 +271,21 @@ namespace { MakeConcreteSymbolic("make-concrete-symbolic", cl::desc("Probabilistic rate at which to make concrete reads symbolic, " "i.e. approximately 1 in n concrete reads will be made symbolic (0=off, 1=all). " - "Used for testing."), - cl::init(0)); + "Used for testing (default=0)"), + cl::init(0), + cl::cat(DebugCat)); cl::opt<unsigned> MaxTests("max-tests", - cl::desc("Stop execution after generating the given number of tests. Extra tests corresponding to partially explored paths will also be dumped (default=0 (off))."), - cl::init(0)); + cl::desc("Stop execution after generating the given number of tests. Extra tests corresponding to partially explored paths will also be dumped. Set to 0 to disable (default=0)"), + cl::init(0), + cl::cat(TerminationCat)); cl::opt<bool> Watchdog("watchdog", cl::desc("Use a watchdog process to enforce --max-time."), - cl::init(0)); + cl::init(0), + cl::cat(TerminationCat)); } extern cl::opt<std::string> MaxTime; |