Switch Array* print-outs to use name instead of ID, and update a few

constructors I missed.


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

4 files changed, 10 insertions, 8 deletions

diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 831a4d91..e3a83f9a 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -167,7 +167,9 @@ private:
 
     // Special case empty list.
     if (!head) {
-      PC << "arr" << updates.root->id;
+      // FIXME: We need to do something (assert, mangle, etc.) so that printing
+      // distinct arrays with the same name doesn't fail.
+      PC << updates.root->name;
       return;
     }
 
@@ -217,7 +219,7 @@ private:
     if (openedList)
       PC << ']';
 
-    PC << " @ arr" << updates.root->id;
+    PC << " @ " << updates.root->name;
   }
 
   void printWidth(PrintContext &PC, ref<Expr> e) {
@@ -528,7 +530,7 @@ void ExprPPrinter::printQuery(std::ostream &os,
            ie = p.usedArrays.end(); it != ie; ++it) {
       const Array *A = *it;
       // FIXME: Print correct name, domain, and range.
-      PC << "array " << "arr" << A->id 
+      PC << "array " << A->name
          << "[" << A->size << "]"
          << " : " << "w32" << " -> " << "w8"
          << " = symbolic";
@@ -572,7 +574,7 @@ void ExprPPrinter::printQuery(std::ostream &os,
     PC.breakLine(indent - 1);
     PC << '[';
     for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it) {
-      PC << "arr" << (*it)->id;
+      PC << (*it)->name;
       if (it + 1 != evalArraysEnd)
         PC.breakLine(indent);
     }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 77596727..8c18fe73 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -1557,7 +1557,7 @@ Decl::Decl(DeclKind _Kind) : Kind(_Kind) {}
 
 void ArrayDecl::dump() {
   // FIXME: For now, print using the Array* "name".
-  std::cout << "array " << "arr" << Root->id
+  std::cout << "array " << Root->name
             << "[" << Size << "]"
             << " : " << 'w' << Domain << " -> " << 'w' << Range << " = ";
 
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 7ebee1c7..69f9567c 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -131,7 +131,7 @@ public:
         os << ", ";
       }
 
-      os << "MO" << array->id;
+      os << "MO" << array->name;
     }
     for (elements_ty::const_iterator it = elements.begin(), ie = elements.end();
          it != ie; ++it) {
@@ -144,7 +144,7 @@ public:
         os << ", ";
       }
 
-      os << "MO" << array->id << " : " << dis;
+      os << "MO" << array->name << " : " << dis;
     }
     os << "}";
   }
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
index 3c605256..03146251 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -128,7 +128,7 @@ public:
                e = objects.end(); i != e; ++i, ++values_it) {
           const Array *array = *i;
           std::vector<unsigned char> &data = *values_it;
-          os << "#     arr" << array->id << " = [";
+          os << "#     " << array->name << " = [";
           for (unsigned j = 0; j < array->size; j++) {
             os << (int) data[j];
             if (j+1 < array->size)