Merge branch 'MartinNowack-fix_bfs2'

3 files changed, 33 insertions, 1 deletions

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 47f300d1..c787382f 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -104,6 +104,16 @@ ExecutionState &BFSSearcher::selectState() {
 void BFSSearcher::update(ExecutionState *current,
                          const std::vector<ExecutionState *> &addedStates,
                          const std::vector<ExecutionState *> &removedStates) {
+  // Assumption: If new states were added KLEE forked, therefore states evolved.
+  // constraints were added to the current state, it evolved.
+  if (!addedStates.empty() && current &&
+      std::find(removedStates.begin(), removedStates.end(), current) ==
+          removedStates.end()) {
+    assert(states.front() == current);
+    states.pop_front();
+    states.push_back(current);
+  }
+
   states.insert(states.end(),
                 addedStates.begin(),
                 addedStates.end());
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 0aa4a4b0..725836e8 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -22,7 +22,7 @@ namespace {
   cl::list<Searcher::CoreSearchType>
   CoreSearch("search", cl::desc("Specify the search heuristic (default=random-path interleaved with nurs:covnew)"),
 	     cl::values(clEnumValN(Searcher::DFS, "dfs", "use Depth First Search (DFS)"),
-			clEnumValN(Searcher::BFS, "bfs", "use Breadth First Search (BFS)"),
+			clEnumValN(Searcher::BFS, "bfs", "use Breadth First Search (BFS), where scheduling decisions are taken at the level of (2-way) forks"),
 			clEnumValN(Searcher::RandomState, "random-state", "randomly select a state to explore"),
 			clEnumValN(Searcher::RandomPath, "random-path", "use Random Path Selection (see OSDI'08 paper)"),
 			clEnumValN(Searcher::NURS_CovNew, "nurs:covnew", "use Non Uniform Random Search (NURS) with Coverage-New"),
diff --git a/test/Feature/BFSSearcher.c b/test/Feature/BFSSearcher.c
new file mode 100644
index 00000000..313791d5
--- /dev/null
+++ b/test/Feature/BFSSearcher.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --stop-after-n-instructions=500 --search=bfs %t1.bc 2>%t2.log
+// RUN: FileCheck -input-file=%t2.log %s
+#include "assert.h"
+#include "klee/klee.h"
+
+int nd() {
+  int r;
+  klee_make_symbolic(&r, sizeof(r), "r");
+  return r;
+}
+
+int main() {
+  int x = 1;
+  while (nd() != 0) {
+    x *= 2;
+  }
+  // CHECK: ASSERTION FAIL
+  klee_assert(0);
+  return x;
+}