diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 14 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 2 |
3 files changed, 13 insertions, 6 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0dbaab80..1826a4d6 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3066,12 +3066,18 @@ void Executor::executeMemoryOperation(ExecutionState &state, } void Executor::executeMakeSymbolic(ExecutionState &state, - const MemoryObject *mo) { + const MemoryObject *mo, + const std::string &name) { // Create a new object state for the memory object (instead of a copy). if (!replayOut) { - static unsigned id = 0; - const Array *array = new Array("arr" + llvm::utostr(++id), - mo->size); + // Find a unique name for this array. First try the original name, + // or if that fails try adding a unique identifier. + unsigned id = 0; + std::string uniqueName = name; + while (!state.arrayNames.insert(uniqueName).second) { + uniqueName = name + "_" + llvm::utostr(++id); + } + const Array *array = new Array(uniqueName, mo->size); bindObjectInState(state, mo, false, array); state.addSymbolic(mo, array); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c37a2869..3a0fa139 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -261,7 +261,8 @@ private: ref<Expr> value /* undef if read */, KInstruction *target /* undef if write */); - void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo); + void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, + const std::string &name); /// Create a new state where each input condition has been added as /// a constraint and return the results. The input state is included diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 1a0ca406..d01a9ef4 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -680,7 +680,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, assert(success && "FIXME: Unhandled solver failure"); if (res) { - executor.executeMakeSymbolic(*s, mo); + executor.executeMakeSymbolic(*s, mo, name); } else { executor.terminateStateOnError(*s, "wrong size given to klee_make_symbolic[_name]", |