From 958e9f99e3837ea018f18799c0055d8dc8075c4d Mon Sep 17 00:00:00 2001 From: Peter Collingbourne Date: Wed, 25 May 2011 15:37:03 +0000 Subject: Name symbolic arrays using the 3rd argument to klee_make_symbolic, and make sure the name is unique. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132054 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Core/Executor.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'lib/Core/Executor.cpp') 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); -- cgit 1.4.1