about summary refs log tree commit diff homepage
path: root/tools
diff options
context:
space:
mode:
authorDaniel Schemmel <daniel@schemmel.net>2023-03-24 15:05:43 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2023-04-21 13:07:31 +0100
commitac0fa15ab0679fe1b5067b07647b0701ae3bc347 (patch)
treef2294eb5f0795ee9ce0f92d527242b7b7a507e79 /tools
parente9d77be6c688836d68a2be5f3f0a02e63f392bb8 (diff)
downloadklee-ac0fa15ab0679fe1b5067b07647b0701ae3bc347.tar.gz
use unique_ptr all throughout the solver chain
Diffstat (limited to 'tools')
-rw-r--r--tools/kleaver/main.cpp19
1 files changed, 8 insertions, 11 deletions
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index eed4e4c9..51298dfb 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -29,12 +29,11 @@
 #include "llvm/Support/ManagedStatic.h"
 #include "llvm/Support/MemoryBuffer.h"
 #include "llvm/Support/raw_ostream.h"
+#include "llvm/Support/Signals.h"
 
 #include <sys/stat.h>
 #include <unistd.h>
-
-
-#include "llvm/Support/Signals.h"
+#include <utility>
 
 using namespace llvm;
 using namespace klee;
@@ -200,7 +199,7 @@ static bool EvaluateInputAST(const char *Filename,
   if (!success)
     return false;
 
-  Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
+  std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse);
 
   if (CoreSolverToUse != DUMMY_SOLVER) {
     const time::Span maxCoreSolverTime(MaxCoreSolverTime);
@@ -209,11 +208,11 @@ static bool EvaluateInputAST(const char *Filename,
     }
   }
 
-  Solver *S = constructSolverChain(coreSolver,
-                                   getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
-                                   getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
-                                   getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME),
-                                   getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME));
+  std::unique_ptr<Solver> S = constructSolverChain(
+      std::move(coreSolver), getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
+      getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
+      getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME),
+      getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME));
 
   unsigned Index = 0;
   for (std::vector<Decl*>::iterator it = Decls.begin(),
@@ -294,8 +293,6 @@ static bool EvaluateInputAST(const char *Filename,
     delete *it;
   delete P;
 
-  delete S;
-
   if (uint64_t queries = *theStatisticManager->getStatisticByName("SolverQueries")) {
     llvm::outs()
       << "--\n"