diff options
Diffstat (limited to 'tools')
-rw-r--r-- | tools/kleaver/main.cpp | 13 | ||||
-rw-r--r-- | tools/klee/main.cpp | 8 |
2 files changed, 15 insertions, 6 deletions
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<std::string> 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<bool> 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<Decl*> 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<Decl*> 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<Decl*> 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); diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 391c8fa2..de04d92e 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -606,11 +606,15 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { SmallString<128> libDir; - if ( strcmp(toolRoot.c_str(), KLEE_INSTALL_BIN_DIR ) == 0) + if (strlen( KLEE_INSTALL_BIN_DIR ) != 0 && + strlen( KLEE_INSTALL_RUNTIME_DIR ) != 0 && + toolRoot.str().endswith( KLEE_INSTALL_BIN_DIR )) { KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << "Using installed KLEE library runtime: "); - libDir = KLEE_INSTALL_RUNTIME_DIR ; + libDir = toolRoot.str().substr(0, + toolRoot.str().size() - strlen( KLEE_INSTALL_BIN_DIR )); + llvm::sys::path::append(libDir, KLEE_INSTALL_RUNTIME_DIR); } else { |