diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-04-08 09:50:44 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-04-08 13:09:45 +0100 |
commit | 5fbbd8a6ea51c81419b29ccfd133b4a9789fd638 (patch) | |
tree | 44fc2a65d5ab8fcc706f8eeecf5f86837a839ec3 /lib/Core/Executor.cpp | |
parent | 93dd487b972743a3081b311a07a66bc499a9b723 (diff) | |
download | klee-5fbbd8a6ea51c81419b29ccfd133b4a9789fd638.tar.gz |
Rename KLEE command line options from
* ``-replay-out`` to ``-replay-ktest-file`` * ``-replay-out-dir`` to ``-replay-ktest-dir`` and also rename * help descriptions * global variables corresponding to these options. * Names used in ``KleeHandler``, ``Interpreter``, ``Executor`` and in KLEE's ``main()`` function. The old name for the options/code was very unhelpful as it wasn't obvious that "out" files are ``.ktest`` files unless you examine KLEE's source code.
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 { |