diff options
| author | Daniel Dunbar <daniel@zuster.org> | 2009-06-07 09:57:01 +0000 |
|---|---|---|
| committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-07 09:57:01 +0000 |
| commit | 20aebfdb32657e9427c6a2567516dc8fd8843bdb (patch) | |
| tree | ffa9457d29bd96f3d568fc7c77d8ea948cee2355 /include/expr | |
| parent | 1287ce6562613d656bb3d74af21326bf91183ffa (diff) | |
| download | klee-20aebfdb32657e9427c6a2567516dc8fd8843bdb.tar.gz | |
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
Diffstat (limited to 'include/expr')
| -rw-r--r-- | include/expr/Lexer.h | 9 | ||||
| -rw-r--r-- | include/expr/Parser.h | 4 |
2 files changed, 9 insertions, 4 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), |