From 307f6201cedeeab244fa7a219a9495cbb0c9529c Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Tue, 9 Jun 2009 06:39:17 +0000 Subject: Remove Array::id. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73128 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/Expr.h | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'include') diff --git a/include/klee/Expr.h b/include/klee/Expr.h index d9cdf5e0..f13ab6d5 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -476,7 +476,6 @@ public: const std::string name; // FIXME: This does not belong here. const MemoryObject *object; - unsigned id; // FIXME: Not 64-bit clean. unsigned size; @@ -484,14 +483,15 @@ public: mutable void *stpInitialArray; public: - // NOTE: id's ***MUST*** be unique to ensure sanity w.r.t. STP, - // which hashes different arrays with the same id to the same - // object! We should probably use the pointer for talking to STP, as - // long as we can guarantee that it won't be a "stale" reference - // once we have freed it. - Array(const std::string &_name, const MemoryObject *_object, - unsigned _id, uint64_t _size) - : name(_name), object(_object), id(_id), size(_size), stpInitialArray(0) {} + /// Array - Construct a new array object. + /// + /// \param _name - The name for this arrays. Names should generally be unique + /// across an application, but this is not necessary for correctness, except + /// when printing expressions. When expressions are printed the output will + /// not parse correctly since two arrays with the same name cannot be + /// distinguished once printed. + Array(const std::string &_name, const MemoryObject *_object, uint64_t _size) + : name(_name), object(_object), size(_size), stpInitialArray(0) {} ~Array() { // FIXME: This relies on caller to delete the STP array. assert(!stpInitialArray && "Array must be deleted by caller!"); -- cgit 1.4.1