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

1 files changed, 7 insertions, 2 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.