diff options
| -rw-r--r-- | lib/Core/Searcher.cpp | 5 | ||||
| -rw-r--r-- | test/Feature/BFSSearcherAndDFSSearcherInterleaved.c | 49 |
2 files changed, 52 insertions, 2 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index fc61ab98..d5d35e8f 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -104,8 +104,9 @@ void BFSSearcher::update(ExecutionState *current, if (!addedStates.empty() && current && std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end()) { - assert(states.front() == current); - states.pop_front(); + auto pos = std::find(states.begin(), states.end(), current); + assert(pos != states.end()); + states.erase(pos); states.push_back(current); } diff --git a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c new file mode 100644 index 00000000..9cc11b70 --- /dev/null +++ b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c @@ -0,0 +1,49 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc +// RUN: rm -rf %t-bfs.klee-out +// RUN: rm -rf %t-dfs.klee-out +// RUN: rm -rf %t-bfs-dfs.klee-out +// RUN: rm -rf %t-dfs-bfs.klee-out +// RUN: %klee -output-dir=%t-bfs.klee-out -search=bfs %t.bc >%t-bfs.out +// RUN: %klee -output-dir=%t-dfs.klee-out -search=dfs %t.bc >%t-dfs.out +// RUN: %klee -output-dir=%t-bfs-dfs.klee-out -search=bfs -search=dfs %t.bc >%t-bfs-dfs.out +// RUN: %klee -output-dir=%t-dfs-bfs.klee-out -search=dfs -search=bfs %t.bc >%t-dfs-bfs.out +// RUN: FileCheck -input-file=%t-bfs.out %s +// RUN: FileCheck -input-file=%t-dfs.out %s +// RUN: FileCheck -input-file=%t-bfs-dfs.out %s +// RUN: FileCheck -input-file=%t-dfs-bfs.out %s + +#include "klee/klee.h" + +int main() { + int x, y, z; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&y, sizeof(y), "y"); + klee_make_symbolic(&z, sizeof(z), "z"); + + if (x == 1) { + if (y == 1) { + if (z == 1) { + printf("A"); + } else { + printf("B"); + } + } + } else { + if (y == 1) { + if (z == 1) { + printf("C"); + } else { + printf("D"); + } + } + } + + // exactly 4 characters + // CHECK: {{^[A-D]{4}$}} + + // for each of A, B, C and D: occurs exactly once + // CHECK-SAME: {{^[B-D]*A[B-D]*$}} + // CHECK-SAME: {{^[A,C-D]*B[A,C-D]*$}} + // CHECK-SAME: {{^[A-B,D]*C[A-B,D]*$}} + // CHECK-SAME: {{^[A-C]*D[A-C]*$}} +} |