From ae57319086f0b99b459fa6a8a0bfde5bcf115e19 Mon Sep 17 00:00:00 2001 From: Andrea Mattavelli Date: Tue, 24 May 2016 18:21:35 +0100 Subject: Fixed bug #375 in Kleaver's parser --- tools/kleaver/main.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'tools') diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 9c374eb8..a937d761 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -95,6 +95,11 @@ namespace { llvm::cl::opt directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."), llvm::cl::init(".")); + llvm::cl::opt ClearArrayAfterQuery( + "clear-array-decls-after-query", + llvm::cl::desc("We discard the previous array declarations after a query " + "is performed. Default: false"), + llvm::cl::init(false)); } static std::string getQueryLogPath(const char filename[]) @@ -160,7 +165,7 @@ static bool PrintInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder) { std::vector Decls; - Parser *P = Parser::Create(Filename, MB, Builder); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); P->SetMaxErrors(20); unsigned NumQueries = 0; @@ -193,7 +198,7 @@ static bool EvaluateInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder) { std::vector Decls; - Parser *P = Parser::Create(Filename, MB, Builder); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { Decls.push_back(D); @@ -327,8 +332,8 @@ static bool printInputAsSMTLIBv2(const char *Filename, { //Parse the input file std::vector Decls; - Parser *P = Parser::Create(Filename, MB, Builder); - P->SetMaxErrors(20); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); + P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { Decls.push_back(D); -- cgit 1.4.1