about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/Internal/Support/CompressionStream.h8
-rw-r--r--include/klee/Internal/Support/FileHandling.h18
-rw-r--r--include/klee/Interpreter.h10
-rw-r--r--lib/Core/Executor.cpp13
-rw-r--r--lib/Core/Executor.h3
-rw-r--r--lib/Core/ExecutorTimers.cpp21
-rw-r--r--lib/Core/StatsTracker.cpp33
-rw-r--r--lib/Core/StatsTracker.h17
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp25
-rw-r--r--lib/Solver/QueryLoggingSolver.h2
-rw-r--r--lib/Solver/Z3Solver.cpp12
-rw-r--r--lib/Support/CompressionStream.cpp3
-rw-r--r--lib/Support/FileHandling.cpp33
-rw-r--r--tools/klee/main.cpp92
14 files changed, 145 insertions, 145 deletions
diff --git a/include/klee/Internal/Support/CompressionStream.h b/include/klee/Internal/Support/CompressionStream.h
index fda68d89..bc9119dd 100644
--- a/include/klee/Internal/Support/CompressionStream.h
+++ b/include/klee/Internal/Support/CompressionStream.h
@@ -7,8 +7,8 @@
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_
-#define INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_
+#ifndef KLEE_COMPRESSIONSTREAM_H
+#define KLEE_COMPRESSIONSTREAM_H
 
 #include "llvm/Support/raw_ostream.h"
 #include "zlib.h"
@@ -37,10 +37,10 @@ public:
   /// should be immediately destroyed; the string will be empty if no error
   /// occurred. This allows optional flags to control how the file will be
   /// opened.
-  compressed_fd_ostream(const char *Filename, std::string &ErrorInfo);
+  compressed_fd_ostream(const std::string &Filename, std::string &ErrorInfo);
 
   ~compressed_fd_ostream();
 };
 }
 
-#endif /* INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_ */
+#endif /* KLEE_COMPRESSIONSTREAM_H */
diff --git a/include/klee/Internal/Support/FileHandling.h b/include/klee/Internal/Support/FileHandling.h
index bee06b9b..90ce20b3 100644
--- a/include/klee/Internal/Support/FileHandling.h
+++ b/include/klee/Internal/Support/FileHandling.h
@@ -6,14 +6,22 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-#ifndef __KLEE_FILE_HANDLING_H__
-#define __KLEE_FILE_HANDLING_H__
+
+#ifndef KLEE_FILEHANDLING_H
+#define KLEE_FILEHANDLING_H
+
 #include "llvm/Support/raw_ostream.h"
+#include <memory>
 #include <string>
 
 namespace klee {
-llvm::raw_fd_ostream *klee_open_output_file(std::string &path,
-                                            std::string &error);
-}
+std::unique_ptr<llvm::raw_fd_ostream>
+klee_open_output_file(const std::string &path, std::string &error);
 
+#ifdef HAVE_ZLIB_H
+std::unique_ptr<llvm::raw_ostream>
+klee_open_compressed_output_file(const std::string &path, std::string &error);
 #endif
+} // namespace klee
+
+#endif /* KLEE_FILEHANDLING_H */
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index 4d8a580c..a88814c9 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -38,12 +38,12 @@ public:
   virtual llvm::raw_ostream &getInfoStream() const = 0;
 
   virtual std::string getOutputFilename(const std::string &filename) = 0;
-  virtual llvm::raw_fd_ostream *openOutputFile(const std::string &filename) = 0;
+  virtual std::unique_ptr<llvm::raw_fd_ostream> openOutputFile(const std::string &filename) = 0;
 
   virtual void incPathsExplored() = 0;
 
   virtual void processTestCase(const ExecutionState &state,
-                               const char *err, 
+                               const char *err,
                                const char *suffix) = 0;
 };
 
@@ -147,13 +147,13 @@ public:
   virtual unsigned getPathStreamID(const ExecutionState &state) = 0;
 
   virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0;
-  
+
   virtual void getConstraintLog(const ExecutionState &state,
                                 std::string &res,
                                 LogType logFormat = STP) = 0;
 
-  virtual bool getSymbolicSolution(const ExecutionState &state, 
-                                   std::vector< 
+  virtual bool getSymbolicSolution(const ExecutionState &state,
+                                   std::vector<
                                    std::pair<std::string,
                                    std::vector<unsigned char> > >
                                    &res) = 0;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 475beacb..0506b685 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -76,10 +76,6 @@
 #include "llvm/IR/CallSite.h"
 #endif
 
-#ifdef HAVE_ZLIB_H
-#include "klee/Internal/Support/CompressionStream.h"
-#endif
-
 #include <cassert>
 #include <algorithm>
 #include <iomanip>
@@ -336,7 +332,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
                             ? std::min(MaxCoreSolverTime, MaxInstructionTime)
                             : std::max(MaxCoreSolverTime, MaxInstructionTime)),
-      debugInstFile(0), debugLogBuffer(debugBufferString) {
+      debugLogBuffer(debugBufferString) {
 
   if (coreSolverTimeout) UseForkedCoreSolver = true;
   Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
@@ -371,11 +367,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       debugInstFile = klee_open_output_file(debug_file_name, error);
 #ifdef HAVE_ZLIB_H
     } else {
-      debugInstFile = new compressed_fd_ostream(
-          (debug_file_name + ".gz").c_str(), error);
+      debug_file_name.append(".gz");
+      debugInstFile = klee_open_compressed_output_file(debug_file_name, error);
     }
 #endif
-    if (!error.empty()) {
+    if (!debugInstFile) {
       klee_error("Could not open file %s : %s", debug_file_name.c_str(),
                  error.c_str());
     }
@@ -455,7 +451,6 @@ Executor::~Executor() {
     delete timers.back();
     timers.pop_back();
   }
-  delete debugInstFile;
 }
 
 /***/
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index d9e20f1e..3643c3f4 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -27,6 +27,7 @@
 
 #include "../Expr/ArrayExprOptimizer.h"
 #include <map>
+#include <memory>
 #include <set>
 #include <string>
 #include <vector>
@@ -221,7 +222,7 @@ private:
   ArrayCache arrayCache;
 
   /// File to print executed instructions to
-  llvm::raw_ostream *debugInstFile;
+  std::unique_ptr<llvm::raw_ostream> debugInstFile;
 
   // @brief Buffer used by logBuffer
   std::string debugBufferString;
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index dd0d824e..a3c13530 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -116,28 +116,25 @@ void Executor::processTimers(ExecutionState *current,
     if (dumpPTree) {
       char name[32];
       sprintf(name, "ptree%08d.dot", (int) stats::instructions);
-      llvm::raw_ostream *os = interpreterHandler->openOutputFile(name);
+      auto os = interpreterHandler->openOutputFile(name);
       if (os) {
         processTree->dump(*os);
-        delete os;
       }
-      
+
       dumpPTree = 0;
     }
 
     if (dumpStates) {
-      llvm::raw_ostream *os = interpreterHandler->openOutputFile("states.txt");
-      
+      auto os = interpreterHandler->openOutputFile("states.txt");
+
       if (os) {
-        for (std::set<ExecutionState*>::const_iterator it = states.begin(), 
-               ie = states.end(); it != ie; ++it) {
-          ExecutionState *es = *it;
+        for (ExecutionState *es : states) {
           *os << "(" << es << ",";
           *os << "[";
-          ExecutionState::stack_ty::iterator next = es->stack.begin();
+          auto next = es->stack.begin();
           ++next;
-          for (ExecutionState::stack_ty::iterator sfIt = es->stack.begin(),
-                 sf_ie = es->stack.end(); sfIt != sf_ie; ++sfIt) {
+          for (auto sfIt = es->stack.begin(), sf_ie = es->stack.end();
+               sfIt != sf_ie; ++sfIt) {
             *os << "('" << sfIt->kf->function->getName().str() << "',";
             if (next == es->stack.end()) {
               *os << es->prevPC->info->line << "), ";
@@ -167,8 +164,6 @@ void Executor::processTimers(ExecutionState *current,
           *os << "}";
           *os << ")\n";
         }
-        
-        delete os;
       }
 
       dumpStates = 0;
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 6ad5b89f..dee14e61 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -176,8 +176,6 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
                            bool _updateMinDistToUncovered)
   : executor(_executor),
     objectFilename(_objectFilename),
-    statsFile(0),
-    istatsFile(0),
     startWallTime(util::getWallTime()),
     numBranches(0),
     fullBranches(0),
@@ -243,12 +241,15 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
 
   if (OutputStats) {
     statsFile = executor.interpreterHandler->openOutputFile("run.stats");
-    assert(statsFile && "unable to open statistics trace file");
-    writeStatsHeader();
-    writeStatsLine();
+    if (statsFile) {
+      writeStatsHeader();
+      writeStatsLine();
 
-    if (StatsWriteInterval > 0)
-      executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+      if (StatsWriteInterval > 0)
+        executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+    } else {
+      klee_error("Unable to open statistics trace file (run.stats).");
+    }
   }
 
   // Add timer to calculate uncovered instructions if needed by the solver
@@ -259,18 +260,15 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
 
   if (OutputIStats) {
     istatsFile = executor.interpreterHandler->openOutputFile("run.istats");
-    assert(istatsFile && "unable to open istats file");
-
-    if (IStatsWriteInterval > 0)
-      executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
+    if (istatsFile) {
+      if (IStatsWriteInterval > 0)
+        executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
+    } else {
+      klee_error("Unable to open instruction level stats file (run.istats).");
+    }
   }
 }
 
-StatsTracker::~StatsTracker() {  
-  delete statsFile;
-  delete istatsFile;
-}
-
 void StatsTracker::done() {
   if (statsFile)
     writeStatsLine();
@@ -278,7 +276,8 @@ void StatsTracker::done() {
   if (OutputIStats) {
     if (updateMinDistToUncovered)
       computeReachableUncovered();
-    writeIStats();
+    if (istatsFile)
+      writeIStats();
   }
 }
 
diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h
index 23abac06..e352bb91 100644
--- a/lib/Core/StatsTracker.h
+++ b/lib/Core/StatsTracker.h
@@ -12,6 +12,7 @@
 
 #include "CallPathManager.h"
 
+#include <memory>
 #include <set>
 
 namespace llvm {
@@ -23,7 +24,7 @@ namespace llvm {
 
 namespace klee {
   class ExecutionState;
-  class Executor;  
+  class Executor;
   class InstructionInfoTable;
   class InterpreterHandler;
   struct KInstruction;
@@ -36,13 +37,13 @@ namespace klee {
     Executor &executor;
     std::string objectFilename;
 
-    llvm::raw_fd_ostream *statsFile, *istatsFile;
+    std::unique_ptr<llvm::raw_fd_ostream> statsFile, istatsFile;
     double startWallTime;
-    
+
     unsigned numBranches;
     unsigned fullBranches, partialBranches;
 
-    CallPathManager callPathManager;    
+    CallPathManager callPathManager;
 
     bool updateMinDistToUncovered;
 
@@ -59,20 +60,20 @@ namespace klee {
   public:
     StatsTracker(Executor &_executor, std::string _objectFilename,
                  bool _updateMinDistToUncovered);
-    ~StatsTracker();
+    ~StatsTracker() = default;
 
     // called after a new StackFrame has been pushed (for callpath tracing)
     void framePushed(ExecutionState &es, StackFrame *parentFrame);
 
-    // called after a StackFrame has been popped 
+    // called after a StackFrame has been popped
     void framePopped(ExecutionState &es);
 
     // called when some side of a branch has been visited. it is
     // imperative that this be called when the statistics index is at
     // the index for the branch itself.
-    void markBranchVisited(ExecutionState *visitedTrue, 
+    void markBranchVisited(ExecutionState *visitedTrue,
                            ExecutionState *visitedFalse);
-    
+
     // called when execution is done and stats files should be flushed
     void done();
 
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 7e4d8fe0..0fb145d7 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -7,18 +7,11 @@
 //
 //===----------------------------------------------------------------------===//
 #include "QueryLoggingSolver.h"
-#include "klee/Config/config.h"
-#include "klee/Internal/System/Time.h"
 #include "klee/Statistics.h"
-#ifdef HAVE_ZLIB_H
-#include "klee/Internal/Support/CompressionStream.h"
+#include "klee/Config/config.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Internal/Support/FileHandling.h"
-#endif
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-#include "llvm/Support/FileSystem.h"
-#endif
+#include "klee/Internal/System/Time.h"
 
 using namespace klee::util;
 
@@ -37,9 +30,9 @@ llvm::cl::opt<bool> CreateCompressedQueryLog(
 QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
                                        const std::string &commentSign,
                                        int queryTimeToLog)
-    : solver(_solver), os(0), BufferString(""), logBuffer(BufferString),
-      queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f),
-      lastQueryTime(0.0f), queryCommentSign(commentSign) {
+    : solver(_solver), BufferString(""), logBuffer(BufferString), queryCount(0),
+      minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f),
+      queryCommentSign(commentSign) {
   std::string error;
 #ifdef HAVE_ZLIB_H
   if (!CreateCompressedQueryLog) {
@@ -47,18 +40,18 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
     os = klee_open_output_file(path, error);
 #ifdef HAVE_ZLIB_H
   } else {
-    os = new compressed_fd_ostream((path + ".gz").c_str(), error);
+    path.append(".gz");
+    os = klee_open_compressed_output_file(path, error);
   }
-  if (!error.empty()) {
+#endif
+  if (!os) {
     klee_error("Could not open file %s : %s", path.c_str(), error.c_str());
   }
-#endif
   assert(0 != solver);
 }
 
 QueryLoggingSolver::~QueryLoggingSolver() {
   delete solver;
-  delete os;
 }
 
 void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) {
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 68edfe55..4da3c129 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -25,7 +25,7 @@ class QueryLoggingSolver : public SolverImpl {
 
 protected:
   Solver *solver;
-  llvm::raw_ostream *os;
+  std::unique_ptr<llvm::raw_ostream> os;
   // @brief Buffer used by logBuffer
   std::string BufferString;
   // @brief buffer to store logs before flushing to file
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 72a15c50..f127de9b 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -49,7 +49,7 @@ private:
   Z3Builder *builder;
   double timeout;
   SolverRunStatus runStatusCode;
-  llvm::raw_fd_ostream* dumpedQueriesFile;
+  std::unique_ptr<llvm::raw_fd_ostream> dumpedQueriesFile;
   ::Z3_params solverParameters;
   // Parameter symbols
   ::Z3_symbol timeoutParamStrSymbol;
@@ -96,8 +96,7 @@ Z3SolverImpl::Z3SolverImpl()
           /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0
               ? Z3LogInteractionFile.c_str()
               : NULL)),
-      timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE),
-      dumpedQueriesFile(0) {
+      timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
   assert(builder && "unable to create Z3Builder");
   solverParameters = Z3_mk_params(builder->ctx);
   Z3_params_inc_ref(builder->ctx, solverParameters);
@@ -107,7 +106,7 @@ Z3SolverImpl::Z3SolverImpl()
   if (!Z3QueryDumpFile.empty()) {
     std::string error;
     dumpedQueriesFile = klee_open_output_file(Z3QueryDumpFile, error);
-    if (!error.empty()) {
+    if (!dumpedQueriesFile) {
       klee_error("Error creating file for dumping Z3 queries: %s",
                  error.c_str());
     }
@@ -127,11 +126,6 @@ Z3SolverImpl::Z3SolverImpl()
 Z3SolverImpl::~Z3SolverImpl() {
   Z3_params_dec_ref(builder->ctx, solverParameters);
   delete builder;
-
-  if (dumpedQueriesFile) {
-    dumpedQueriesFile->close();
-    delete dumpedQueriesFile;
-  }
 }
 
 Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {}
diff --git a/lib/Support/CompressionStream.cpp b/lib/Support/CompressionStream.cpp
index 01fe1352..d17e1df1 100644
--- a/lib/Support/CompressionStream.cpp
+++ b/lib/Support/CompressionStream.cpp
@@ -23,7 +23,7 @@
 
 namespace klee {
 
-compressed_fd_ostream::compressed_fd_ostream(const char *Filename,
+compressed_fd_ostream::compressed_fd_ostream(const std::string &Filename,
                                              std::string &ErrorInfo)
     : llvm::raw_ostream(), pos(0) {
   ErrorInfo = "";
@@ -38,6 +38,7 @@ compressed_fd_ostream::compressed_fd_ostream(const char *Filename,
   if (EC) {
     ErrorInfo = EC.message();
     FD = -1;
+    return;
   }
   // Initialize the compression library
   strm.zalloc = Z_NULL;
diff --git a/lib/Support/FileHandling.cpp b/lib/Support/FileHandling.cpp
index 3e156f3c..068ce44b 100644
--- a/lib/Support/FileHandling.cpp
+++ b/lib/Support/FileHandling.cpp
@@ -7,6 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 #include "klee/Internal/Support/FileHandling.h"
+
 #include "klee/Config/Version.h"
 #include "klee/Config/config.h"
 #include "klee/Internal/Support/ErrorHandling.h"
@@ -15,25 +16,41 @@
 #include "llvm/Support/FileSystem.h"
 #endif
 
+#ifdef HAVE_ZLIB_H
+#include "klee/Internal/Support/CompressionStream.h"
+#endif
+
 namespace klee {
 
-llvm::raw_fd_ostream *klee_open_output_file(std::string &path,
-                                            std::string &error) {
-  llvm::raw_fd_ostream *f;
+std::unique_ptr<llvm::raw_fd_ostream>
+klee_open_output_file(const std::string &path, std::string &error) {
+  error = "";
+  std::unique_ptr<llvm::raw_fd_ostream> f;
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6)
   std::error_code ec;
-  f = new llvm::raw_fd_ostream(path.c_str(), ec, llvm::sys::fs::F_None);
+  f = std::unique_ptr<llvm::raw_fd_ostream>(new llvm::raw_fd_ostream(path.c_str(), ec, llvm::sys::fs::F_None)); // FIXME C++14
   if (ec)
     error = ec.message();
 #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-  f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_None);
+  f = std::unique_ptr<llvm::raw_fd_ostream>(new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_None)); // FIXME C++14
 #else
-  f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_Binary);
+  f = std::unique_ptr<llvm::raw_fd_ostream>(new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_Binary)); // FIXME C++14
 #endif
   if (!error.empty()) {
-    delete f;
-    f = NULL;
+    f.reset(nullptr);
   }
   return f;
 }
+
+#ifdef HAVE_ZLIB_H
+std::unique_ptr<llvm::raw_ostream>
+klee_open_compressed_output_file(const std::string &path, std::string &error) {
+  error = "";
+  std::unique_ptr<llvm::raw_ostream> f(new compressed_fd_ostream(path, error));
+  if (!error.empty()) {
+    f.reset(nullptr);
+  }
+  return f;
+}
+#endif
 }
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 1de5fbeb..4b32c00b 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -221,7 +221,7 @@ class KleeHandler : public InterpreterHandler {
 private:
   Interpreter *m_interpreter;
   TreeStreamWriter *m_pathWriter, *m_symPathWriter;
-  llvm::raw_ostream *m_infoFile;
+  std::unique_ptr<llvm::raw_ostream> m_infoFile;
 
   SmallString<128> m_outputDirectory;
 
@@ -250,9 +250,9 @@ public:
                        const char *errorSuffix);
 
   std::string getOutputFilename(const std::string &filename);
-  llvm::raw_fd_ostream *openOutputFile(const std::string &filename);
+  std::unique_ptr<llvm::raw_fd_ostream> openOutputFile(const std::string &filename);
   std::string getTestFilename(const std::string &suffix, unsigned id);
-  llvm::raw_fd_ostream *openTestFile(const std::string &suffix, unsigned id);
+  std::unique_ptr<llvm::raw_fd_ostream> openTestFile(const std::string &suffix, unsigned id);
 
   // load a .path file
   static void loadPathFile(std::string name,
@@ -265,7 +265,7 @@ public:
 };
 
 KleeHandler::KleeHandler(int argc, char **argv)
-    : m_interpreter(0), m_pathWriter(0), m_symPathWriter(0), m_infoFile(0),
+    : m_interpreter(0), m_pathWriter(0), m_symPathWriter(0),
       m_outputDirectory(), m_numTotalTests(0), m_numGeneratedTests(0),
       m_pathsExplored(0), m_argc(argc), m_argv(argv) {
 
@@ -347,7 +347,6 @@ KleeHandler::~KleeHandler() {
   delete m_symPathWriter;
   fclose(klee_warning_file);
   fclose(klee_message_file);
-  delete m_infoFile;
 }
 
 void KleeHandler::setInterpreter(Interpreter *i) {
@@ -372,17 +371,17 @@ std::string KleeHandler::getOutputFilename(const std::string &filename) {
   return path.str();
 }
 
-llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string &filename) {
-  llvm::raw_fd_ostream *f;
+std::unique_ptr<llvm::raw_fd_ostream>
+KleeHandler::openOutputFile(const std::string &filename) {
   std::string Error;
   std::string path = getOutputFilename(filename);
-  f = klee_open_output_file(path, Error);
-  if (!Error.empty()) {
+  auto f = klee_open_output_file(path, Error);
+  if (!f) {
     klee_warning("error opening file \"%s\".  KLEE may have run out of file "
                  "descriptors: try to increase the maximum number of open file "
                  "descriptors by using ulimit (%s).",
                  path.c_str(), Error.c_str());
-    return NULL;
+    return nullptr;
   }
   return f;
 }
@@ -393,8 +392,8 @@ std::string KleeHandler::getTestFilename(const std::string &suffix, unsigned id)
   return filename.str();
 }
 
-llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix,
-                                                unsigned id) {
+std::unique_ptr<llvm::raw_fd_ostream>
+KleeHandler::openTestFile(const std::string &suffix, unsigned id) {
   return openOutputFile(getTestFilename(suffix, id));
 }
 
@@ -444,30 +443,29 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     }
 
     if (errorMessage) {
-      llvm::raw_ostream *f = openTestFile(errorSuffix, id);
-      *f << errorMessage;
-      delete f;
+      auto f = openTestFile(errorSuffix, id);
+      if (f)
+        *f << errorMessage;
     }
 
     if (m_pathWriter) {
       std::vector<unsigned char> concreteBranches;
       m_pathWriter->readStream(m_interpreter->getPathStreamID(state),
                                concreteBranches);
-      llvm::raw_fd_ostream *f = openTestFile("path", id);
-      for (std::vector<unsigned char>::iterator I = concreteBranches.begin(),
-                                                E = concreteBranches.end();
-           I != E; ++I) {
-        *f << *I << "\n";
+      auto f = openTestFile("path", id);
+      if (f) {
+        for (const auto &branch : concreteBranches) {
+          *f << branch << '\n';
+        }
       }
-      delete f;
     }
 
     if (errorMessage || WriteKQueries) {
       std::string constraints;
       m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY);
-      llvm::raw_ostream *f = openTestFile("kquery", id);
-      *f << constraints;
-      delete f;
+      auto f = openTestFile("kquery", id);
+      if (f)
+        *f << constraints;
     }
 
     if (WriteCVCs) {
@@ -475,43 +473,42 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       // SMT-LIBv2 not CVC which is a bit confusing
       std::string constraints;
       m_interpreter->getConstraintLog(state, constraints, Interpreter::STP);
-      llvm::raw_ostream *f = openTestFile("cvc", id);
-      *f << constraints;
-      delete f;
+      auto f = openTestFile("cvc", id);
+      if (f)
+        *f << constraints;
     }
 
     if(WriteSMT2s) {
       std::string constraints;
         m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2);
-        llvm::raw_ostream *f = openTestFile("smt2", id);
-        *f << constraints;
-        delete f;
+        auto f = openTestFile("smt2", id);
+        if (f)
+          *f << constraints;
     }
 
     if (m_symPathWriter) {
       std::vector<unsigned char> symbolicBranches;
       m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state),
                                   symbolicBranches);
-      llvm::raw_fd_ostream *f = openTestFile("sym.path", id);
-      for (std::vector<unsigned char>::iterator I = symbolicBranches.begin(), E = symbolicBranches.end(); I!=E; ++I) {
-        *f << *I << "\n";
+      auto f = openTestFile("sym.path", id);
+      if (f) {
+        for (const auto &branch : symbolicBranches) {
+          *f << branch << '\n';
+        }
       }
-      delete f;
     }
 
     if (WriteCov) {
       std::map<const std::string*, std::set<unsigned> > cov;
       m_interpreter->getCoveredLines(state, cov);
-      llvm::raw_ostream *f = openTestFile("cov", id);
-      for (std::map<const std::string*, std::set<unsigned> >::iterator
-             it = cov.begin(), ie = cov.end();
-           it != ie; ++it) {
-        for (std::set<unsigned>::iterator
-               it2 = it->second.begin(), ie = it->second.end();
-             it2 != ie; ++it2)
-          *f << *it->first << ":" << *it2 << "\n";
+      auto f = openTestFile("cov", id);
+      if (f) {
+        for (const auto &entry : cov) {
+          for (const auto &line : entry.second) {
+            *f << *entry.first << ':' << line << '\n';
+          }
+        }
       }
-      delete f;
     }
 
     if (m_numGeneratedTests == StopAfterNTests)
@@ -519,13 +516,12 @@ void KleeHandler::processTestCase(const ExecutionState &state,
 
     if (WriteTestInfo) {
       double elapsed_time = util::getWallTime() - start_time;
-      llvm::raw_ostream *f = openTestFile("info", id);
-      *f << "Time to generate test case: "
-         << elapsed_time << "s\n";
-      delete f;
+      auto f = openTestFile("info", id);
+      if (f)
+        *f << "Time to generate test case: " << elapsed_time << "s\n";
     }
   }
-  
+
   if (errorMessage && OptExitOnError) {
     m_interpreter->prepareForEarlyExit();
     klee_error("EXITING ON ERROR:\n%s\n", errorMessage);