diff options
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 16 | ||||
-rw-r--r-- | lib/Core/Executor.h | 12 |
2 files changed, 14 insertions, 14 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dc9edf5f..47c1be02 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -282,7 +282,7 @@ Executor::Executor(const InterpreterOptions &opts, symPathWriter(0), specialFunctionHandler(0), processTree(0), - replayOut(0), + replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), @@ -736,7 +736,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { } } } else if (res==Solver::Unknown) { - assert(!replayOut && "in replay mode, only one branch can be true."); + assert(!replayKTest && "in replay mode, only one branch can be true."); if ((MaxMemoryInhibit && atMemoryLimit) || current.forkDisabled || @@ -2652,8 +2652,8 @@ std::string Executor::getAddressInfo(ExecutionState &state, } void Executor::terminateState(ExecutionState &state) { - if (replayOut && replayPosition!=replayOut->numObjects) { - klee_warning_once(replayOut, + if (replayKTest && replayPosition!=replayKTest->numObjects) { + klee_warning_once(replayKTest, "replay did not consume all objects in test input."); } @@ -2875,7 +2875,7 @@ void Executor::callExternalFunction(ExecutionState &state, ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, ref<Expr> e) { unsigned n = interpreterOpts.MakeConcreteSymbolic; - if (!n || replayOut || replayPath) + if (!n || replayKTest || replayPath) return e; // right now, we don't replace symbolics (is there any reason to?) @@ -3221,7 +3221,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, const std::string &name) { // Create a new object state for the memory object (instead of a copy). - if (!replayOut) { + if (!replayKTest) { // Find a unique name for this array. First try the original name, // or if that fails try adding a unique identifier. unsigned id = 0; @@ -3281,10 +3281,10 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } } else { ObjectState *os = bindObjectInState(state, mo, false); - if (replayPosition >= replayOut->numObjects) { + if (replayPosition >= replayKTest->numObjects) { terminateStateOnError(state, "replay count mismatch", "user.err"); } else { - KTestObject *obj = &replayOut->objects[replayPosition++]; + KTestObject *obj = &replayKTest->objects[replayPosition++]; if (obj->numBytes != mo->size) { terminateStateOnError(state, "replay size mismatch", "user.err"); } else { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 8bfa278a..1997bad2 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -150,10 +150,10 @@ private: /// When non-null the bindings that will be used for calls to /// klee_make_symbolic in order replay. - const struct KTest *replayOut; + const struct KTest *replayKTest; /// When non-null a list of branch decisions to be used for replay. const std::vector<bool> *replayPath; - /// The index into the current \ref replayOut or \ref replayPath + /// The index into the current \ref replayKTest or \ref replayPath /// object. unsigned replayPosition; @@ -417,16 +417,16 @@ public: } virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) { symPathWriter = tsw; - } + } - virtual void setReplayOut(const struct KTest *out) { + virtual void setReplayKTest(const struct KTest *out) { assert(!replayPath && "cannot replay both buffer and path"); - replayOut = out; + replayKTest = out; replayPosition = 0; } virtual void setReplayPath(const std::vector<bool> *path) { - assert(!replayOut && "cannot replay both buffer and path"); + assert(!replayKTest && "cannot replay both buffer and path"); replayPath = path; replayPosition = 0; } |