diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-15 20:47:47 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-03-16 21:23:24 +0000 |
commit | c1d3977f07ddbf840ca3cdbd580239921a9c5f91 (patch) | |
tree | 92774b4a261228f4ae5523850a2efce122b00e6c /lib/Core | |
parent | d44d507631c345edf33ee7f6ecf7fd942af7760b (diff) | |
download | klee-c1d3977f07ddbf840ca3cdbd580239921a9c5f91.tar.gz |
Added support for disabling --batch-instructions and --batch-time by setting them to 0
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Searcher.cpp | 8 | ||||
-rw-r--r-- | lib/Core/UserSearcher.cpp | 31 |
2 files changed, 23 insertions, 16 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index db295468..47457a91 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -351,9 +351,11 @@ BatchingSearcher::~BatchingSearcher() { } ExecutionState &BatchingSearcher::selectState() { - if (!lastState || - (time::getWallTime() - lastStartTime) > timeBudget || - (stats::instructions - lastStartInstructions) > instructionBudget) { + if (!lastState || + (((timeBudget.toSeconds() > 0) && + (time::getWallTime() - lastStartTime) > timeBudget)) || + ((instructionBudget > 0) && + (stats::instructions - lastStartInstructions) > instructionBudget)) { if (lastState) { time::Span delta = time::getWallTime() - lastStartTime; auto t = timeBudget; diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 754b3796..7efdb30d 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -56,25 +56,30 @@ cl::opt<bool> UseIterativeDeepeningTimeSearch( "use-iterative-deepening-time-search", cl::desc( "Use iterative deepening time search (experimental) (default=false)"), - cl::init(false), cl::cat(SearchCat)); + 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=false)"), - cl::init(false), cl::cat(SearchCat)); - -cl::opt<unsigned> - BatchInstructions("batch-instructions", - cl::desc("Number of instructions to batch when using " - "--use-batching-search (default=10000)"), - cl::init(10000), cl::cat(SearchCat)); - -cl::opt<std::string> BatchTime("batch-time", - cl::desc("Amount of time to batch when using " - "--use-batching-search (default=5s)"), - cl::init("5s"), cl::cat(SearchCat)); + cl::init(false), + cl::cat(SearchCat)); + +cl::opt<unsigned> BatchInstructions( + "batch-instructions", + cl::desc("Number of instructions to batch when using " + "--use-batching-search. Set to 0 to disable (default=10000)"), + cl::init(10000), + cl::cat(SearchCat)); + +cl::opt<std::string> BatchTime( + "batch-time", + cl::desc("Amount of time to batch when using " + "--use-batching-search. Set to 0s to disable (default=5s)"), + cl::init("5s"), + cl::cat(SearchCat)); } // namespace |