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

1 files changed, 2 insertions, 11 deletions

diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index 65105f12..f67e27ab 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -71,16 +71,12 @@ namespace expr {
   ///
   /// For example:
   ///   array obj[] : w32 -> w8 = symbolic
-  ///   array obj[32] : w32 -> w8 = { ... }
+  ///   array obj[32] : w32 -> w8 = [ ... ]
   class ArrayDecl : public Decl {
   public:
     /// Name - The name of this array.
     const Identifier *Name;
 
-    /// Size - The maximum array size (or 0 if unspecified). Concrete
-    /// arrays always are specified with a size.
-    const uint64_t Size;
-
     /// Domain - The width of indices.
     const unsigned Domain;
 
@@ -90,17 +86,12 @@ namespace expr {
     /// Root - The root array object defined by this decl.
     const Array *Root;
 
-    /// Contents - The initial contents of the array. The array is
-    /// symbolic if no contents are specified. The contained
-    /// expressions are guaranteed to be constants.
-    const std::vector<ExprHandle> Contents;
-
   public:
     ArrayDecl(const Identifier *_Name, uint64_t _Size, 
               unsigned _Domain, unsigned _Range,
               const Array *_Root)
       : Decl(ArrayDeclKind), Name(_Name), 
-        Size(_Size), Domain(_Domain), Range(_Range), 
+        Domain(_Domain), Range(_Range), 
         Root(_Root) {
     }