about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-04-01 12:20:32 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-07-01 15:52:40 +0100
commitda5d238b5a78b54f89728132d71cfa6f8be16d21 (patch)
tree888f532812d45d6fbc4d9d25a9c29fa37633b493
parenta1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 (diff)
downloadklee-da5d238b5a78b54f89728132d71cfa6f8be16d21.tar.gz
Use `unique_ptr` for solver in timing solver
-rw-r--r--lib/Core/Executor.cpp2
-rw-r--r--lib/Core/TimingSolver.h6
2 files changed, 3 insertions, 5 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 39de6e8d..ceefc710 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -4058,7 +4058,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state,
   abort(); // FIXME: Broken until we sort out how to do the write back.
 
   if (DebugCheckForImpliedValues)
-    ImpliedValue::checkForImpliedValues(solver->solver, e, value);
+    ImpliedValue::checkForImpliedValues(solver->solver.get(), e, value);
 
   ImpliedValueList results;
   ImpliedValue::getImpliedValues(e, value, results);
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 8e25b21c..9470bd31 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -15,6 +15,7 @@
 #include "klee/Solver/Solver.h"
 #include "klee/System/Time.h"
 
+#include <memory>
 #include <vector>
 
 namespace klee {
@@ -25,7 +26,7 @@ namespace klee {
   /// tracking the statistics that we care about.
   class TimingSolver {
   public:
-    Solver *solver;
+    std::unique_ptr<Solver> solver;
     bool simplifyExprs;
 
   public:
@@ -36,9 +37,6 @@ namespace klee {
     /// querying.
     TimingSolver(Solver *_solver, bool _simplifyExprs = true) 
       : solver(_solver), simplifyExprs(_simplifyExprs) {}
-    ~TimingSolver() {
-      delete solver;
-    }
 
     void setTimeout(time::Span t) {
       solver->setCoreSolverTimeout(t);