about summary refs log tree commit diff homepage
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/kleaver/main.cpp13
-rw-r--r--tools/klee/main.cpp8
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
   {