From 58d1592fa3fd84aded956801183949b9c710490e Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Tue, 9 Jun 2009 08:42:08 +0000
Subject: More constant Array support.  - The are parsed, printed, and solved
 now.

 - Remove some members of ArrayDecl which are only duplicates of Array members.

 - KLEE still doesn't create these, but you can write them by hand.

The EXE style constant array optimization for STP (turning the initial writes
into asserts) is now only a stones throw away, but I need to leave something fun
to do tomorrow. :)


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73133 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/Expr/ExprPPrinter.cpp | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'lib/Expr/ExprPPrinter.cpp')

diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index e3a83f9a..6ad5fffd 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -532,8 +532,18 @@ void ExprPPrinter::printQuery(std::ostream &os,
       // FIXME: Print correct name, domain, and range.
       PC << "array " << A->name
          << "[" << A->size << "]"
-         << " : " << "w32" << " -> " << "w8"
-         << " = symbolic";
+         << " : " << "w32" << " -> " << "w8" << " = ";
+      if (A->isSymbolicArray()) {
+        PC << "symbolic";
+      } else {
+        PC << "[";
+        for (unsigned i = 0, e = A->size; i != e; ++i) {
+          if (i)
+            PC << " ";
+          PC << A->constantValues[i];
+        }
+        PC << "]";
+      }
       PC.breakLine();
     }
   }
-- 
cgit 1.4.1