diff options
Diffstat (limited to 'lib/Solver/Z3Builder.cpp')
| -rw-r--r-- | lib/Solver/Z3Builder.cpp | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index ae78c21c..fc826c07 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -15,6 +15,8 @@ #include "klee/util/Bits.h" #include "ConstantDivision.h" #include "klee/SolverStats.h" + +#include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" using namespace klee; @@ -356,17 +358,16 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { if (!hashed) { // Unique arrays by name, so we make sure the name is unique by - // including the address. - char buf[32]; - unsigned const addrlen = - sprintf(buf, "_%p", (const void *)root) + 1; // +1 for null-termination - unsigned const space = (root->name.length() > 32 - addrlen) - ? (32 - addrlen) + // using the size of the array hash as a counter. + std::string unique_id = llvm::itostr(_arr_hash._array_hash.size()); + unsigned const uid_length = unique_id.length(); + unsigned const space = (root->name.length() > 32 - uid_length) + ? (32 - uid_length) : root->name.length(); - memmove(buf + space, buf, addrlen); // moving the address part to the end - memcpy(buf, root->name.c_str(), space); // filling out the name part + std::string unique_name = root->name.substr(0, space) + unique_id; - array_expr = buildArray(buf, root->getDomain(), root->getRange()); + array_expr = buildArray(unique_name.c_str(), root->getDomain(), + root->getRange()); if (root->isConstantArray()) { // FIXME: Flush the concrete values into Z3. Ideally we would do this |