diff options
author | Andrea Mattavelli <andreamattavelli@gmail.com> | 2016-05-24 18:21:35 +0100 |
---|---|---|
committer | Andrea Mattavelli <andreamattavelli@gmail.com> | 2016-05-24 18:21:35 +0100 |
commit | ae57319086f0b99b459fa6a8a0bfde5bcf115e19 (patch) | |
tree | 9c7b67f1b020fb5b61736218915f6c47f56a00e3 /lib/Expr | |
parent | 4278fdcb819bb9a68ed43f88c86df21c6b04a0ab (diff) | |
download | klee-ae57319086f0b99b459fa6a8a0bfde5bcf115e19.tar.gz |
Fixed bug #375 in Kleaver's parser
Diffstat (limited to 'lib/Expr')
-rw-r--r-- | lib/Expr/Parser.cpp | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index e914cb80..572b9572 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -111,6 +111,7 @@ namespace { const MemoryBuffer *TheMemoryBuffer; ExprBuilder *Builder; ArrayCache TheArrayCache; + bool ClearArrayAfterQuery; Lexer TheLexer; unsigned MaxErrors; @@ -322,14 +323,11 @@ namespace { void Error(const char *Message) { Error(Message, Tok); } public: - ParserImpl(const std::string _Filename, - const MemoryBuffer *MB, - ExprBuilder *_Builder) : Filename(_Filename), - TheMemoryBuffer(MB), - Builder(_Builder), - TheLexer(MB), - MaxErrors(~0u), - NumErrors(0) {} + ParserImpl(const std::string _Filename, const MemoryBuffer *MB, + ExprBuilder *_Builder, bool _ClearArrayAfterQuery) + : Filename(_Filename), TheMemoryBuffer(MB), Builder(_Builder), + ClearArrayAfterQuery(_ClearArrayAfterQuery), TheLexer(MB), + MaxErrors(~0u), NumErrors(0) {} virtual ~ParserImpl(); @@ -492,9 +490,9 @@ DeclResult ParserImpl::ParseArrayDecl() { Values.clear(); } - for (unsigned i = 0; i != Size.get(); ++i) { - // FIXME: Must be constant expression. - } + // for (unsigned i = 0; i != Size.get(); ++i) { + // TODO: Check: Must be constant expression. + //} } // FIXME: Validate that size makes sense for domain type. @@ -532,7 +530,7 @@ DeclResult ParserImpl::ParseArrayDecl() { ArrayDecl *AD = new ArrayDecl(Label, Size.get(), DomainType.get(), RangeType.get(), Root); - ArraySymTab.insert(std::make_pair(Label, AD)); + ArraySymTab[Label] = AD; // Create the initial version reference. VersionSymTab.insert(std::make_pair(Label, @@ -681,7 +679,13 @@ DeclResult ParserImpl::ParseQueryCommand() { exit: if (Tok.kind != Token::EndOfFile) - ExpectRParen("unexpected argument to 'query'."); + ExpectRParen("unexpected argument to 'query'."); + + // If we assume that the queries are independent, we clear the array + // table from the previous declarations + if (ClearArrayAfterQuery) + ArraySymTab.clear(); + return new QueryCommand(Constraints, Res.get(), Values, Objects); } @@ -1641,10 +1645,9 @@ Parser::Parser() { Parser::~Parser() { } -Parser *Parser::Create(const std::string Filename, - const MemoryBuffer *MB, - ExprBuilder *Builder) { - ParserImpl *P = new ParserImpl(Filename, MB, Builder); +Parser *Parser::Create(const std::string Filename, const MemoryBuffer *MB, + ExprBuilder *Builder, bool ClearArrayAfterQuery) { + ParserImpl *P = new ParserImpl(Filename, MB, Builder, ClearArrayAfterQuery); P->Initialize(); return P; } |