diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-22 16:39:28 +0100 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-08 21:56:28 +0200 |
commit | f3ff3b06318cae93db4d682e6451ddbca4760328 (patch) | |
tree | b984df4d0ab09629ef423831f542ff746ff8e34c /lib/Core/Executor.cpp | |
parent | 07632e75e21e3c61f1ab46f76618cb1b807bd6c3 (diff) | |
download | klee-f3ff3b06318cae93db4d682e6451ddbca4760328.tar.gz |
Use vector instead of set to add/remove states
Deterministic adding/removing of states.
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r-- | lib/Core/Executor.cpp | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2c4e5202..49cba67f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -665,7 +665,7 @@ void Executor::branch(ExecutionState &state, for (unsigned i=1; i<N; ++i) { ExecutionState *es = result[theRNG.getInt32() % i]; ExecutionState *ns = es->branch(); - addedStates.insert(ns); + addedStates.push_back(ns); result.push_back(ns); es->ptreeNode->data = 0; std::pair<PTree::Node*,PTree::Node*> res = @@ -883,7 +883,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { ++stats::forks; falseState = trueState->branch(); - addedStates.insert(falseState); + addedStates.push_back(falseState); if (RandomizeFork && theRNG.getBool()) std::swap(trueState, falseState); @@ -2467,9 +2467,9 @@ void Executor::updateStates(ExecutionState *current) { states.insert(addedStates.begin(), addedStates.end()); addedStates.clear(); - - for (std::set<ExecutionState*>::iterator - it = removedStates.begin(), ie = removedStates.end(); + + for (std::vector<ExecutionState *>::iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::iterator it2 = states.find(es); @@ -2674,7 +2674,8 @@ void Executor::run(ExecutionState &initialState) { searcher = constructUserSearcher(*this); - searcher->update(0, states, std::set<ExecutionState*>()); + std::vector<ExecutionState *> newStates(states.begin(), states.end()); + searcher->update(0, newStates, std::vector<ExecutionState *>()); while (!states.empty() && !haltExecution) { ExecutionState &state = searcher->selectState(); @@ -2753,11 +2754,12 @@ void Executor::terminateState(ExecutionState &state) { interpreterHandler->incPathsExplored(); - std::set<ExecutionState*>::iterator it = addedStates.find(&state); + std::vector<ExecutionState *>::iterator it = + std::find(addedStates.begin(), addedStates.end(), &state); if (it==addedStates.end()) { state.pc = state.prevPC; - removedStates.insert(&state); + removedStates.push_back(&state); } else { // never reached searcher, just delete immediately std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 = |