diff options
author | Julian Büning <julian.buening@comsys.rwth-aachen.de> | 2020-04-11 16:43:01 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-06-05 17:13:21 +0100 |
commit | d3aee9c0e619fa097e296de81de93a09aaab82f2 (patch) | |
tree | 01bd41526ea0cbcb05f5092870fac47be9b409f4 /test | |
parent | 3c42e214fb2ec4a101dd1e91e2d8c1ce4983a569 (diff) | |
download | klee-d3aee9c0e619fa097e296de81de93a09aaab82f2.tar.gz |
fix BatchingSearcher's disabled time budget
The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own.
Diffstat (limited to 'test')
-rw-r--r-- | test/regression/2020-04-11-batching-search-zero-time-budget.c | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regression/2020-04-11-batching-search-zero-time-budget.c b/test/regression/2020-04-11-batching-search-zero-time-budget.c new file mode 100644 index 00000000..46043f31 --- /dev/null +++ b/test/regression/2020-04-11-batching-search-zero-time-budget.c @@ -0,0 +1,16 @@ +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-batching-search --batch-time=0 --batch-instructions=1 %t.bc 2>&1 | FileCheck %s + +#include <time.h> + +#include "klee/klee.h" + +int main(void) { + for (int i = 0; i < 10; ++i) { + struct timespec ts = {.tv_sec = 0, .tv_nsec = 10000000}; // 10 ms + nanosleep(&ts, NULL); + } + // CHECK-NOT: increased time budget + return 0; +} |