Implement array declarations.

 - Printing current prints all declarations, and we allow redefinition, since
   the printer doesn't know what has already been printed.

 - Names don't print right yet, since the Array* object doesn't have the name.

 - Various things are unsupported.
   o Array domain/range must be w32/w8.
   o Concrete initializers for arrays are unsupported.


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

3 files changed, 11 insertions, 5 deletions

diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h
index 4ae760a0..a8719b4d 100644
--- a/include/expr/Lexer.h
+++ b/include/expr/Lexer.h
@@ -28,9 +28,11 @@ namespace expr {
       EndOfFile,                /// <end of file>
       Equals,                   /// ' = '
       Identifier,               /// [a-zA-Z_][a-zA-Z0-9._]*
+      KWArray,                  /// 'array'
       KWFalse,                  /// 'false'
       KWQuery,                  /// 'query'
       KWReserved,               /// fp[0-9]+([.].*)?, i[0-9]+
+      KWSymbolic,               /// 'symbolic'
       KWTrue,                   /// 'true'
       KWWidth,                  /// w[0-9]+
       LBrace,                   /// '{'
@@ -41,7 +43,10 @@ namespace expr {
       RParen,                   /// ')'
       RSquare,                  /// ']'
       Semicolon,                /// ';'
-      Unknown                   /// <other>
+      Unknown,                   /// <other>
+      
+      KWKindFirst=KWArray,
+      KWKindLast=KWWidth
     };
 
     Kind        kind;           /// The token kind.
@@ -60,7 +65,7 @@ namespace expr {
 
     /// isKeyword - True if this token is a keyword.
     bool isKeyword() const { 
-      return kind >= KWFalse && kind <= KWTrue; 
+      return kind >= KWKindFirst && kind <= KWKindLast; 
     }
 
     // dump - Dump the token to stderr.
diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index 5caf0027..65105f12 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -79,7 +79,7 @@ namespace expr {
 
     /// Size - The maximum array size (or 0 if unspecified). Concrete
     /// arrays always are specified with a size.
-    const unsigned Size;
+    const uint64_t Size;
 
     /// Domain - The width of indices.
     const unsigned Domain;
@@ -96,7 +96,7 @@ namespace expr {
     const std::vector<ExprHandle> Contents;
 
   public:
-    ArrayDecl(const Identifier *_Name, unsigned _Size, 
+    ArrayDecl(const Identifier *_Name, uint64_t _Size, 
               unsigned _Domain, unsigned _Range,
               const Array *_Root)
       : Decl(ArrayDeclKind), Name(_Name), 
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
index 50ccd203..4d1930d8 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/util/ExprPPrinter.h
@@ -65,7 +65,8 @@ namespace klee {
                            const ref<Expr> *evalExprsBegin = 0,
                            const ref<Expr> *evalExprsEnd = 0,
                            const Array * const* evalArraysBegin = 0,
-                           const Array * const* evalArraysEnd = 0);
+                           const Array * const* evalArraysEnd = 0,
+                           bool printArrayDecls = true);
   };
 
 }