diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/expr/Lexer.h | 9 | ||||
| -rw-r--r-- | include/expr/Parser.h | 4 | ||||
| -rw-r--r-- | include/klee/util/ExprPPrinter.h | 3 |
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); }; } |