about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2016-11-09 22:51:48 +0100
committerMartin Nowack <martin.nowack@gmail.com>2016-11-09 22:51:48 +0100
commit2b2b2b0e46ae260e7974f0d2738f2d23ca255874 (patch)
treee02b6c490d84e47fa3f8458660105e0f2507bc13 /lib
parente853f0bceeb7099acc3df16e52a3cfd1dabad422 (diff)
downloadklee-2b2b2b0e46ae260e7974f0d2738f2d23ca255874.tar.gz
Fix BFS searcher
For performance reasons, if KLEE branches, one state is reused
and it is progressed by adding new constraints.
Make sure both new states end up at the end of the BFS searcher queue.
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Searcher.cpp10
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 3bfcd6b3..f61ae6ec 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());