Remove Array::id.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73128 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 14 insertions, 10 deletions

diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 8c18fe73..856541ee 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -517,11 +517,9 @@ DeclResult ParserImpl::ParseArrayDecl() {
   if (!RangeType.isValid())
     RangeType = 8;
 
-  // FIXME: Array should take name, not id.
   // FIXME: Array should take domain and range.
   const Identifier *Label = GetOrCreateIdentifier(Name);
-  static int counter = 0;
-  Array *Root = new Array(Label->Name, 0, ++counter, Size.get());
+  Array *Root = new Array(Label->Name, 0, Size.get());
   ArrayDecl *AD = new ArrayDecl(Label, Size.get(), 
                                 DomainType.get(), RangeType.get(), Root);
 
@@ -1300,7 +1298,7 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
   VersionResult Res = ParseVersion();
   // Define update list to avoid use-of-undef errors.
   if (!Res.isValid()) {
-    Res = VersionResult(true, UpdateList(new Array("", 0, -1, 0), NULL));
+    Res = VersionResult(true, UpdateList(new Array("", 0, 0), NULL));
   }
   
   if (Label)
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 22544820..379f1c8d 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -94,10 +94,14 @@ void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
 }
 
 int UpdateList::compare(const UpdateList &b) const {
-  // use object id to increase determinism
-  if (root->id != b.root->id) 
-    return root->id < b.root->id ? -1 : 1;
-  
+  if (root->name != b.root->name)
+    return root->name < b.root->name ? -1 : 1;
+
+  // Check the root itself in case we have separate objects with the
+  // same name.
+  if (root != b.root)
+    return root < b.root ? -1 : 1;
+
   if (getSize() < b.getSize()) return -1;
   else if (getSize() > b.getSize()) return 1;    
 
@@ -111,12 +115,14 @@ int UpdateList::compare(const UpdateList &b) const {
         return res;
     }
   }
-  assert(!an && !bn);
+  assert(!an && !bn);  
   return 0;
 }
 
 unsigned UpdateList::hash() const {
-  unsigned res = root->id * Expr::MAGIC_HASH_CONSTANT;
+  unsigned res = 0;
+  for (unsigned i = 0, e = root->name.size(); i != e; ++i)
+    res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i];
   if (head)
     res ^= head->hash();
   return res;