diff options
author | Dan Liew <delcypher@gmail.com> | 2016-04-08 14:36:06 +0100 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2016-04-08 14:36:06 +0100 |
commit | 386d972fbbb6064eff394c687d427d4385f95716 (patch) | |
tree | 44fc2a65d5ab8fcc706f8eeecf5f86837a839ec3 /lib/Core/Executor.cpp | |
parent | 6609a03e68bf551f433ddd0fd8cf64a8683ee2ee (diff) | |
parent | 5fbbd8a6ea51c81419b29ccfd133b4a9789fd638 (diff) | |
download | klee-386d972fbbb6064eff394c687d427d4385f95716.tar.gz |
Merge pull request #368 from delcypher/refactor_klee_out_file_to_ktest
Refactor use of the name "outFile" to "KTest"
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r-- | lib/Core/Executor.cpp | 16 |
1 files changed, 8 insertions, 8 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 { |