aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp16
-rw-r--r--lib/Core/Executor.h12
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 &current, 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;
}