From 7d5f1158a4c97a5165cabe0817db94e98c0917bc Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Mon, 10 Apr 2017 21:57:46 +0100
Subject: [PATCH] Replace owning raw pointers with unique_ptr

Implement @tautschnig's fixes

Fix residual memory leak from narrow_argv
---
 src/analyses/ai.h                             |  10 +-
 src/analyses/goto_rw.cpp                      |  41 ++++---
 src/analyses/goto_rw.h                        |  16 +--
 src/analyses/local_may_alias.h                |   6 +-
 src/analyses/reaching_definitions.cpp         |  30 ++---
 src/analyses/reaching_definitions.h           |  15 +--
 src/analyses/static_analysis.h                |  11 +-
 src/ansi-c/ansi_c_language.cpp                |   4 +-
 src/ansi-c/ansi_c_language.h                  |  11 +-
 src/cbmc/bmc.cpp                              |   6 +-
 src/cbmc/cbmc_main.cpp                        |   4 +-
 src/cbmc/cbmc_parse_options.cpp               |  12 +-
 src/cbmc/cbmc_solvers.cpp                     | 109 +++++++++---------
 src/cbmc/cbmc_solvers.h                       |  61 +++++-----
 src/clobber/clobber_main.cpp                  |   9 +-
 src/clobber/clobber_parse_options.cpp         |   2 +-
 src/cpp/cpp_language.cpp                      |   4 +-
 src/cpp/cpp_language.h                        |  11 +-
 src/goto-analyzer/goto_analyzer_main.cpp      |   4 +-
 src/goto-cc/compile.cpp                       |  11 +-
 src/goto-cc/goto_cc_main.cpp                  |   4 +-
 src/goto-diff/goto_diff_main.cpp              |   4 +-
 src/goto-diff/goto_diff_parse_options.cpp     |   9 +-
 .../enumerating_loop_acceleration.h           |  19 ++-
 .../accelerate/scratch_program.h              |  11 +-
 src/goto-instrument/dump_c_class.h            |   8 +-
 src/goto-instrument/goto_instrument_main.cpp  |   4 +-
 .../wmm/instrumenter_strategies.cpp           |   9 +-
 src/goto-programs/show_symbol_table.cpp       |  14 ++-
 src/goto-symex/goto_symex_state.cpp           |   2 +
 src/goto-symex/goto_symex_state.h             |   7 +-
 src/goto-symex/symex_main.cpp                 |   5 +-
 src/java_bytecode/jar_file.cpp                |  10 +-
 src/java_bytecode/java_bytecode_language.cpp  |   4 +-
 src/java_bytecode/java_bytecode_language.h    |   7 +-
 src/jsil/jsil_language.cpp                    |   4 +-
 src/jsil/jsil_language.h                      |  12 +-
 src/langapi/language_ui.cpp                   |  14 ++-
 src/langapi/language_util.cpp                 |   4 +-
 src/langapi/mode.cpp                          |   7 +-
 src/langapi/mode.h                            |  11 +-
 src/memory-models/mmcc_main.cpp               |   4 +-
 src/symex/symex_main.cpp                      |   9 +-
 src/util/freer.h                              |  33 ++++++
 src/util/invariant.cpp                        |  22 ++--
 src/util/language.h                           |   3 +-
 src/util/language_file.cpp                    |  16 +--
 src/util/language_file.h                      |  12 +-
 src/util/make_unique.h                        |  24 ++++
 src/util/mp_arith.cpp                         |  21 ++--
 src/util/pipe_stream.cpp                      |  24 ++--
 src/util/pipe_stream.h                        |   3 +-
 src/util/run.cpp                              |  10 +-
 src/util/sharing_node.h                       |  10 +-
 src/util/unicode.cpp                          |  12 +-
 src/util/unicode.h                            |  16 ++-
 56 files changed, 428 insertions(+), 337 deletions(-)
 create mode 100644 src/util/freer.h
 create mode 100644 src/util/make_unique.h

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 5e0d1db3b2e..a04c60547d0 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -12,12 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANALYSES_AI_H
 #define CPROVER_ANALYSES_AI_H
 
-#include <map>
 #include <iosfwd>
+#include <map>
+#include <memory>
 
 #include <util/json.h>
 #include <util/xml.h>
 #include <util/expr.h>
+#include <util/make_unique.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -334,7 +336,7 @@ class ai_baset
     const namespacet &ns)=0;
   virtual statet &get_state(locationt l)=0;
   virtual const statet &find_state(locationt l) const=0;
-  virtual statet* make_temporary_state(const statet &s)=0;
+  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
 };
 
 // domainT is expected to be derived from ai_domain_baseT
@@ -400,9 +402,9 @@ class ait:public ai_baset
       static_cast<const domainT &>(src), from, to);
   }
 
-  statet *make_temporary_state(const statet &s) override
+  std::unique_ptr<statet> make_temporary_state(const statet &s) override
   {
-    return new domainT(static_cast<const domainT &>(s));
+    return util_make_unique<domainT>(static_cast<const domainT &>(s));
   }
 
   void fixedpoint(
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 49827bd2bd3..c7de024f6f9 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -10,8 +10,9 @@ Date: April 2010
 
 #include "goto_rw.h"
 
-#include <limits>
 #include <algorithm>
+#include <limits>
+#include <memory>
 
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -20,6 +21,7 @@ Date: April 2010
 #include <util/endianness_map.h>
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
+#include <util/make_unique.h>
 
 #include <goto-programs/goto_functions.h>
 
@@ -49,12 +51,12 @@ rw_range_sett::~rw_range_sett()
   for(rw_range_sett::objectst::iterator it=r_range_set.begin();
       it!=r_range_set.end();
       ++it)
-    delete it->second;
+    it->second=nullptr;
 
   for(rw_range_sett::objectst::iterator it=w_range_set.begin();
       it!=w_range_set.end();
       ++it)
-    delete it->second;
+    it->second=nullptr;
 }
 
 void rw_range_sett::output(std::ostream &out) const
@@ -461,16 +463,18 @@ void rw_range_sett::add(
   const range_spect &range_start,
   const range_spect &range_end)
 {
-  objectst::iterator entry=(mode==get_modet::LHS_W ? w_range_set : r_range_set).
-    insert(
-      std::pair<const irep_idt&, range_domain_baset*>(
-        identifier, nullptr)).first;
+  objectst::iterator entry=
+    (mode==get_modet::LHS_W?w_range_set:r_range_set)
+       .insert(
+         std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
+           identifier, nullptr))
+       .first;
 
   if(entry->second==nullptr)
-    entry->second=new range_domaint();
+    entry->second=util_make_unique<range_domaint>();
 
-  static_cast<range_domaint*>(entry->second)->push_back(
-    std::make_pair(range_start, range_end));
+  static_cast<range_domaint&>(*entry->second).push_back(
+    {range_start, range_end});
 }
 
 void rw_range_sett::get_objects_rec(
@@ -662,17 +666,18 @@ void rw_guarded_range_set_value_sett::add(
   const range_spect &range_start,
   const range_spect &range_end)
 {
-  objectst::iterator entry=(mode==get_modet::LHS_W ? w_range_set : r_range_set).
-    insert(
-      std::pair<const irep_idt&, range_domain_baset*>(
-        identifier, nullptr)).first;
+  objectst::iterator entry=
+    (mode==get_modet::LHS_W?w_range_set:r_range_set)
+      .insert(
+        std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
+          identifier, nullptr))
+      .first;
 
   if(entry->second==nullptr)
-    entry->second=new guarded_range_domaint();
+    entry->second=util_make_unique<guarded_range_domaint>();
 
-  static_cast<guarded_range_domaint*>(entry->second)->insert(
-    std::make_pair(range_start,
-                   std::make_pair(range_end, guard.as_expr())));
+  static_cast<guarded_range_domaint&>(*entry->second).insert(
+    {range_start, {range_end, guard.as_expr()}});
 }
 
 void goto_rw(goto_programt::const_targett target,
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index 1f92c3e0e14..8dd43880f93 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -15,6 +15,7 @@ Date: April 2010
 #include <map>
 #include <ostream>
 #include <limits>
+#include <memory> // unique_ptr
 
 #include <util/guard.h>
 
@@ -83,10 +84,10 @@ class rw_range_sett
 {
 public:
   #ifdef USE_DSTRING
-  typedef std::map<irep_idt, range_domain_baset*> objectst;
+  typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
   #else
-  typedef std::unordered_map<irep_idt, range_domain_baset*, string_hash>
-    objectst;
+  typedef std::unordered_map<
+    irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
   #endif
 
   virtual ~rw_range_sett();
@@ -108,8 +109,8 @@ class rw_range_sett
 
   const range_domaint &get_ranges(objectst::const_iterator it) const
   {
-    PRECONDITION(dynamic_cast<range_domaint*>(it->second)!=nullptr);
-    return *static_cast<range_domaint*>(it->second);
+    PRECONDITION(dynamic_cast<range_domaint*>(it->second.get())!=nullptr);
+    return static_cast<const range_domaint &>(*it->second);
   }
 
   enum class get_modet { LHS_W, READ };
@@ -277,8 +278,9 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
 
   const guarded_range_domaint &get_ranges(objectst::const_iterator it) const
   {
-    PRECONDITION(dynamic_cast<guarded_range_domaint*>(it->second)!=nullptr);
-    return *static_cast<guarded_range_domaint*>(it->second);
+    PRECONDITION(
+      dynamic_cast<guarded_range_domaint*>(it->second.get())!=nullptr);
+    return static_cast<const guarded_range_domaint &>(*it->second);
   }
 
   virtual void get_objects_rec(
diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h
index 5e04ff01a75..307513a64eb 100644
--- a/src/analyses/local_may_alias.h
+++ b/src/analyses/local_may_alias.h
@@ -12,10 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
 #define CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
 
-#include <stack>
 #include <memory>
+#include <stack>
 
 #include <util/union_find.h>
+#include <util/make_unique.h>
 
 #include "locals.h"
 #include "dirty.h"
@@ -117,8 +118,7 @@ class local_may_alias_factoryt
     goto_functionst::function_mapt::const_iterator f_it2=
       goto_functions->function_map.find(fkt);
     assert(f_it2!=goto_functions->function_map.end());
-    return *(fkt_map[fkt]=std::unique_ptr<local_may_aliast>(
-              new local_may_aliast(f_it2->second)));
+    return *(fkt_map[fkt]=util_make_unique<local_may_aliast>(f_it2->second));
   }
 
   local_may_aliast &operator()(goto_programt::const_targett t)
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 89b31da543b..c3242849511 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -15,14 +15,26 @@ Date: February 2013
 
 #include "reaching_definitions.h"
 
+#include <memory>
+
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
+#include <util/make_unique.h>
 
 #include <pointer-analysis/value_set_analysis_fi.h>
 
 #include "is_threaded.h"
 #include "dirty.h"
 
+reaching_definitions_analysist::reaching_definitions_analysist(
+  const namespacet &_ns):
+    concurrency_aware_ait<rd_range_domaint>(),
+    ns(_ns)
+{
+}
+
+reaching_definitions_analysist::~reaching_definitions_analysist()=default;
+
 void rd_range_domaint::populate_cache(const irep_idt &identifier) const
 {
   assert(bv_container);
@@ -717,26 +729,16 @@ const rd_range_domaint::ranges_at_loct &rd_range_domaint::get(
     return entry->second;
 }
 
-reaching_definitions_analysist::~reaching_definitions_analysist()
-{
-  if(is_dirty)
-    delete is_dirty;
-  if(is_threaded)
-    delete is_threaded;
-  if(value_sets)
-    delete value_sets;
-}
-
 void reaching_definitions_analysist::initialize(
   const goto_functionst &goto_functions)
 {
-  value_set_analysis_fit *value_sets_=new value_set_analysis_fit(ns);
+  auto value_sets_=util_make_unique<value_set_analysis_fit>(ns);
   (*value_sets_)(goto_functions);
-  value_sets=value_sets_;
+  value_sets=std::move(value_sets_);
 
-  is_threaded=new is_threadedt(goto_functions);
+  is_threaded=util_make_unique<is_threadedt>(goto_functions);
 
-  is_dirty=new dirtyt(goto_functions);
+  is_dirty=util_make_unique<dirtyt>(goto_functions);
 
   concurrency_aware_ait<rd_range_domaint>::initialize(goto_functions);
 }
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 21cbd1ed377..c62bd5e4b51 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -241,14 +241,7 @@ class reaching_definitions_analysist:
 {
 public:
   // constructor
-  explicit reaching_definitions_analysist(const namespacet &_ns):
-    concurrency_aware_ait<rd_range_domaint>(),
-    ns(_ns),
-    value_sets(nullptr),
-    is_threaded(nullptr),
-    is_dirty(nullptr)
-  {
-  }
+  explicit reaching_definitions_analysist(const namespacet &_ns);
 
   virtual ~reaching_definitions_analysist();
 
@@ -290,9 +283,9 @@ class reaching_definitions_analysist:
 
 protected:
   const namespacet &ns;
-  value_setst * value_sets;
-  is_threadedt * is_threaded;
-  dirtyt * is_dirty;
+  std::unique_ptr<value_setst> value_sets;
+  std::unique_ptr<is_threadedt> is_threaded;
+  std::unique_ptr<dirtyt> is_dirty;
 };
 
 #endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H
diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h
index 1f384ec979d..405c6509bdc 100644
--- a/src/analyses/static_analysis.h
+++ b/src/analyses/static_analysis.h
@@ -16,10 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #error Deprecated, use ai.h instead
 #endif
 
-#include <map>
 #include <iosfwd>
+#include <map>
+#include <memory>
 #include <unordered_set>
 
+#include <util/make_unique.h>
+
 #include <goto-programs/goto_functions.h>
 
 // don't use me -- I am just a base class
@@ -252,7 +255,7 @@ class static_analysis_baset
   virtual void generate_state(locationt l)=0;
   virtual statet &get_state(locationt l)=0;
   virtual const statet &get_state(locationt l) const=0;
-  virtual statet* make_temporary_state(statet &s)=0;
+  virtual std::unique_ptr<statet> make_temporary_state(statet &s)=0;
 
   typedef domain_baset::expr_sett expr_sett;
 
@@ -331,9 +334,9 @@ class static_analysist:public static_analysis_baset
     return static_cast<T &>(a).merge(static_cast<const T &>(b), to);
   }
 
-  virtual statet *make_temporary_state(statet &s)
+  virtual std::unique_ptr<statet> make_temporary_state(statet &s)
   {
-    return new T(static_cast<T &>(s));
+    return util_make_unique<T>(static_cast<T &>(s));
   }
 
   virtual void generate_state(locationt l)
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index 4a9faddf1a7..46024683f96 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -139,9 +139,9 @@ void ansi_c_languaget::show_parse(std::ostream &out)
   parse_tree.output(out);
 }
 
-languaget *new_ansi_c_language()
+std::unique_ptr<languaget> new_ansi_c_language()
 {
-  return new ansi_c_languaget;
+  return util_make_unique<ansi_c_languaget>();
 }
 
 bool ansi_c_languaget::from_expr(
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index 89f8399b117..e20593c1f03 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -10,7 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
 #define CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
 
+/*! \defgroup gr_ansi_c ANSI-C front-end */
+
+#include <memory>
+
 #include <util/language.h>
+#include <util/make_unique.h>
 
 #include "ansi_c_parse_tree.h"
 
@@ -59,8 +64,8 @@ class ansi_c_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
-  languaget *new_language() override
-  { return new ansi_c_languaget; }
+  std::unique_ptr<languaget> new_language() override
+  { return util_make_unique<ansi_c_languaget>(); }
 
   std::string id() const override { return "C"; }
   std::string description() const override { return "ANSI-C 99"; }
@@ -73,6 +78,6 @@ class ansi_c_languaget:public languaget
   std::string parse_path;
 };
 
-languaget *new_ansi_c_language();
+std::unique_ptr<languaget> new_ansi_c_language();
 
 #endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 4f2230c9783..ab5d6883ab0 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -314,11 +314,11 @@ safety_checkert::resultt bmct::run(
   std::unique_ptr<memory_model_baset> memory_model;
 
   if(mm.empty() || mm=="sc")
-    memory_model=std::unique_ptr<memory_model_baset>(new memory_model_sct(ns));
+    memory_model=util_make_unique<memory_model_sct>(ns);
   else if(mm=="tso")
-    memory_model=std::unique_ptr<memory_model_baset>(new memory_model_tsot(ns));
+    memory_model=util_make_unique<memory_model_tsot>(ns);
   else if(mm=="pso")
-    memory_model=std::unique_ptr<memory_model_baset>(new memory_model_psot(ns));
+    memory_model=util_make_unique<memory_model_psot>(ns);
   else
   {
     error() << "Invalid memory model " << mm
diff --git a/src/cbmc/cbmc_main.cpp b/src/cbmc/cbmc_main.cpp
index 3a35c6bb197..bcf6c764c68 100644
--- a/src/cbmc/cbmc_main.cpp
+++ b/src/cbmc/cbmc_main.cpp
@@ -34,7 +34,9 @@ extern unsigned long long irep_cmp_ne_cnt;
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 239b34d9b8c..ed6f3f081a2 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -601,7 +601,7 @@ int cbmc_parse_optionst::get_goto_program(
         return 6;
       }
 
-      languaget *language=get_language_from_filename(filename);
+      std::unique_ptr<languaget> language=get_language_from_filename(filename);
       language->get_language_options(cmdline);
 
       if(language==nullptr)
@@ -750,18 +750,16 @@ void cbmc_parse_optionst::preprocessing()
       return;
     }
 
-    languaget *ptr=get_language_from_filename(filename);
-    ptr->get_language_options(cmdline);
+    std::unique_ptr<languaget> language=get_language_from_filename(filename);
+    language->get_language_options(cmdline);
 
-    if(ptr==nullptr)
+    if(language==nullptr)
     {
       error() << "failed to figure out type of file" << eom;
       return;
     }
 
-    ptr->set_message_handler(get_message_handler());
-
-    std::unique_ptr<languaget> language(ptr);
+    language->set_message_handler(get_message_handler());
 
     if(language->preprocess(infile, filename, std::cout))
       error() << "PREPROCESSING ERROR" << eom;
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index 2c5287fc199..c53c34375e3 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -11,11 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cbmc_solvers.h"
 
-#include <memory>
-#include <iostream>
 #include <fstream>
+#include <iostream>
+#include <memory>
 
 #include <util/unicode.h>
+#include <util/make_unique.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
@@ -87,65 +88,65 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
   return s;
 }
 
-/// Get the default decision procedure
-cbmc_solverst::solvert* cbmc_solverst::get_default()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
 {
-  solvert *solver=new solvert;
+  auto solver=util_make_unique<solvert>();
 
   if(options.get_bool_option("beautify") ||
      !options.get_bool_option("sat-preprocessor")) // no simplifier
   {
     // simplifier won't work with beautification
-    solver->set_prop(new satcheck_no_simplifiert());
+    solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
   }
   else // with simplifier
   {
-    solver->set_prop(new satcheckt());
+    solver->set_prop(util_make_unique<satcheckt>());
   }
 
   solver->prop().set_message_handler(get_message_handler());
 
-  bv_cbmct *bv_cbmc=new bv_cbmct(ns, solver->prop());
+  auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());
 
   if(options.get_option("arrays-uf")=="never")
     bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_NONE;
   else if(options.get_option("arrays-uf")=="always")
     bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_ALL;
 
-  solver->set_prop_conv(bv_cbmc);
+  solver->set_prop_conv(std::move(bv_cbmc));
 
   return solver;
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_dimacs()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
 {
   no_beautification();
   no_incremental_check();
 
-  dimacs_cnft *prop=new dimacs_cnft();
+  auto prop=util_make_unique<dimacs_cnft>();
   prop->set_message_handler(get_message_handler());
 
   std::string filename=options.get_option("outfile");
 
-  return new solvert(new cbmc_dimacst(ns, *prop, filename), prop);
+  auto cbmc_dimacs=util_make_unique<cbmc_dimacst>(ns, *prop, filename);
+  return util_make_unique<solvert>(std::move(cbmc_dimacs), std::move(prop));
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
 {
-  propt *prop;
-
-  // We offer the option to disable the SAT preprocessor
-  if(options.get_bool_option("sat-preprocessor"))
+  std::unique_ptr<propt> prop=[this]() -> std::unique_ptr<propt>
   {
-    no_beautification();
-    prop=new satcheckt();
-  }
-  else
-    prop=new satcheck_no_simplifiert();
+    // We offer the option to disable the SAT preprocessor
+    if(options.get_bool_option("sat-preprocessor"))
+    {
+      no_beautification();
+      return util_make_unique<satcheckt>();
+    }
+    return util_make_unique<satcheck_no_simplifiert>();
+  }();
 
   prop->set_message_handler(get_message_handler());
 
-  bv_refinementt *bv_refinement=new bv_refinementt(ns, *prop);
+  auto bv_refinement=util_make_unique<bv_refinementt>(ns, *prop);
   bv_refinement->set_ui(ui);
 
   // we allow setting some parameters
@@ -158,19 +159,18 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
   bv_refinement->do_arithmetic_refinement =
     options.get_bool_option("refine-arithmetic");
 
-  return new solvert(bv_refinement, prop);
+  return util_make_unique<solvert>(std::move(bv_refinement), std::move(prop));
 }
 
 /// the string refinement adds to the bit vector refinement specifications for
 /// functions from the Java string library
 /// \return a solver for cbmc
-cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
 {
-  propt *prop;
-  prop=new satcheck_no_simplifiert();
+  auto prop=util_make_unique<satcheck_no_simplifiert>();
   prop->set_message_handler(get_message_handler());
 
-  string_refinementt *string_refinement=new string_refinementt(
+  auto string_refinement=util_make_unique<string_refinementt>(
     ns, *prop, MAX_NB_REFINEMENT);
   string_refinement->set_ui(ui);
 
@@ -192,10 +192,12 @@ cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
   string_refinement->do_arithmetic_refinement=
     options.get_bool_option("refine-arithmetic");
 
-  return new solvert(string_refinement, prop);
+  return util_make_unique<solvert>(
+    std::move(string_refinement), std::move(prop));
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt1(
+  smt1_dect::solvert solver)
 {
   no_beautification();
   no_incremental_check();
@@ -210,20 +212,20 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
       throw 0;
     }
 
-    smt1_dect *smt1_dec=
-      new smt1_dect(
+    auto smt1_dec=
+      util_make_unique<smt1_dect>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
         "QF_AUFBV",
         solver);
 
-    return new solvert(smt1_dec);
+    return util_make_unique<solvert>(std::move(smt1_dec));
   }
   else if(filename=="-")
   {
-    smt1_convt *smt1_conv=
-      new smt1_convt(
+    auto smt1_conv=
+      util_make_unique<smt1_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -233,14 +235,14 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
 
     smt1_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt1_conv);
+    return util_make_unique<solvert>(std::move(smt1_conv));
   }
   else
   {
     #ifdef _MSC_VER
-    std::ofstream *out=new std::ofstream(widen(filename));
+    auto out=util_make_unique<std::ofstream>(widen(filename));
     #else
-    std::ofstream *out=new std::ofstream(filename);
+    auto out=util_make_unique<std::ofstream>(filename);
     #endif
 
     if(!out)
@@ -249,8 +251,8 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
       throw 0;
     }
 
-    smt1_convt *smt1_conv=
-      new smt1_convt(
+    auto smt1_conv=
+      util_make_unique<smt1_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -260,11 +262,12 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
 
     smt1_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt1_conv, out);
+    return util_make_unique<solvert>(std::move(smt1_conv), std::move(out));
   }
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
+  smt2_dect::solvert solver)
 {
   no_beautification();
 
@@ -278,8 +281,8 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
       throw 0;
     }
 
-    smt2_dect *smt2_dec=
-      new smt2_dect(
+    auto smt2_dec=
+      util_make_unique<smt2_dect>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -289,12 +292,12 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_dec->use_FPA_theory=true;
 
-    return new solvert(smt2_dec);
+    return util_make_unique<solvert>(std::move(smt2_dec));
   }
   else if(filename=="-")
   {
-    smt2_convt *smt2_conv=
-      new smt2_convt(
+    auto smt2_conv=
+      util_make_unique<smt2_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -307,14 +310,14 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
 
     smt2_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt2_conv);
+    return util_make_unique<solvert>(std::move(smt2_conv));
   }
   else
   {
     #ifdef _MSC_VER
-    std::ofstream *out=new std::ofstream(widen(filename));
+    auto out=util_make_unique<std::ofstream>(widen(filename));
     #else
-    std::ofstream *out=new std::ofstream(filename);
+    auto out=util_make_unique<std::ofstream>(filename);
     #endif
 
     if(!*out)
@@ -323,8 +326,8 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
       throw 0;
     }
 
-    smt2_convt *smt2_conv=
-      new smt2_convt(
+    auto smt2_conv=
+      util_make_unique<smt2_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -337,7 +340,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
 
     smt2_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt2_conv, out);
+    return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
   }
 }
 
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
index 8b0644b2d79..02bbb8b5db9 100644
--- a/src/cbmc/cbmc_solvers.h
+++ b/src/cbmc/cbmc_solvers.h
@@ -54,19 +54,19 @@ class cbmc_solverst:public messaget
     {
     }
 
-    explicit solvert(prop_convt *p):prop_conv_ptr(p)
+    explicit solvert(std::unique_ptr<prop_convt> p):prop_conv_ptr(std::move(p))
     {
     }
 
-    solvert(prop_convt *p1, propt *p2):
-      prop_ptr(p2),
-      prop_conv_ptr(p1)
+    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2):
+      prop_ptr(std::move(p2)),
+      prop_conv_ptr(std::move(p1))
     {
     }
 
-    solvert(prop_convt *p1, std::ofstream *p2):
-      ofstream_ptr(p2),
-      prop_conv_ptr(p1)
+    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2):
+      ofstream_ptr(std::move(p2)),
+      prop_conv_ptr(std::move(p1))
     {
     }
 
@@ -82,19 +82,19 @@ class cbmc_solverst:public messaget
       return *prop_ptr;
     }
 
-    void set_prop_conv(prop_convt *p)
+    void set_prop_conv(std::unique_ptr<prop_convt> p)
     {
-      prop_conv_ptr=std::unique_ptr<prop_convt>(p);
+      prop_conv_ptr=std::move(p);
     }
 
-    void set_prop(propt *p)
+    void set_prop(std::unique_ptr<propt> p)
     {
-      prop_ptr=std::unique_ptr<propt>(p);
+      prop_ptr=std::move(p);
     }
 
-    void set_ofstream(std::ofstream *p)
+    void set_ofstream(std::unique_ptr<std::ofstream> p)
     {
-      ofstream_ptr=std::unique_ptr<std::ofstream>(p);
+      ofstream_ptr=std::move(p);
     }
 
     // the objects are deleted in the opposite order they appear below
@@ -106,22 +106,17 @@ class cbmc_solverst:public messaget
   // returns a solvert object
   virtual std::unique_ptr<solvert> get_solver()
   {
-    solvert *solver;
-
     if(options.get_bool_option("dimacs"))
-      solver=get_dimacs();
-    else if(options.get_bool_option("refine"))
-      solver=get_bv_refinement();
+      return get_dimacs();
+    if(options.get_bool_option("refine"))
+      return get_bv_refinement();
     else if(options.get_bool_option("refine-strings"))
-      solver=get_string_refinement();
-    else if(options.get_bool_option("smt1"))
-      solver=get_smt1(get_smt1_solver_type());
-    else if(options.get_bool_option("smt2"))
-      solver=get_smt2(get_smt2_solver_type());
-    else
-      solver=get_default();
-
-    return std::unique_ptr<solvert>(solver);
+      return get_string_refinement();
+    if(options.get_bool_option("smt1"))
+      return get_smt1(get_smt1_solver_type());
+    if(options.get_bool_option("smt2"))
+      return get_smt2(get_smt2_solver_type());
+    return get_default();
   }
 
   virtual ~cbmc_solverst()
@@ -138,12 +133,12 @@ class cbmc_solverst:public messaget
   // use gui format
   language_uit::uit ui;
 
-  solvert *get_default();
-  solvert *get_dimacs();
-  solvert *get_bv_refinement();
-  solvert *get_string_refinement();
-  solvert *get_smt1(smt1_dect::solvert solver);
-  solvert *get_smt2(smt2_dect::solvert solver);
+  std::unique_ptr<solvert> get_default();
+  std::unique_ptr<solvert> get_dimacs();
+  std::unique_ptr<solvert> get_bv_refinement();
+  std::unique_ptr<solvert> get_string_refinement();
+  std::unique_ptr<solvert> get_smt1(smt1_dect::solvert solver);
+  std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
 
   smt1_dect::solvert get_smt1_solver_type() const;
   smt2_dect::solvert get_smt2_solver_type() const;
diff --git a/src/clobber/clobber_main.cpp b/src/clobber/clobber_main.cpp
index e63a9d63e49..c52099efb6d 100644
--- a/src/clobber/clobber_main.cpp
+++ b/src/clobber/clobber_main.cpp
@@ -16,14 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
-  clobber_parse_optionst parse_options(argc, argv);
-  return parse_options.main();
-}
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
+#endif
   clobber_parse_optionst parse_options(argc, argv);
   return parse_options.main();
 }
-#endif
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 71a7b41c7f8..7df4d5fa56f 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -246,7 +246,7 @@ bool clobber_parse_optionst::get_goto_program(
         return true;
       }
 
-      languaget *language=get_language_from_filename(filename);
+      std::unique_ptr<languaget> language=get_language_from_filename(filename);
       language->get_language_options(cmdline);
 
       if(language==nullptr)
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index c8b7f999653..baa06dbcd48 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -205,9 +205,9 @@ void cpp_languaget::show_parse(
     out << "UNKNOWN: " << item.pretty() << '\n';
 }
 
-languaget *new_cpp_language()
+std::unique_ptr<languaget> new_cpp_language()
 {
-  return new cpp_languaget;
+  return util_make_unique<cpp_languaget>();
 }
 
 bool cpp_languaget::from_expr(
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index 5be4330da2f..c43f9304a98 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -12,7 +12,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_LANGUAGE_H
 #define CPROVER_CPP_CPP_LANGUAGE_H
 
+/*! \defgroup gr_cpp C++ front-end */
+
+#include <memory>
+
 #include <util/language.h>
+#include <util/make_unique.h> // unique_ptr
 
 #include "cpp_parse_tree.h"
 
@@ -71,8 +76,8 @@ class cpp_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
-  languaget *new_language() override
-  { return new cpp_languaget; }
+  std::unique_ptr<languaget> new_language() override
+  { return util_make_unique<cpp_languaget>(); }
 
   std::string id() const override { return "cpp"; }
   std::string description() const override { return "C++"; }
@@ -92,6 +97,6 @@ class cpp_languaget:public languaget
   }
 };
 
-languaget *new_cpp_language();
+std::unique_ptr<languaget> new_cpp_language();
 
 #endif // CPROVER_CPP_CPP_LANGUAGE_H
diff --git a/src/goto-analyzer/goto_analyzer_main.cpp b/src/goto-analyzer/goto_analyzer_main.cpp
index 8e367dd7ebc..f2192925ab4 100644
--- a/src/goto-analyzer/goto_analyzer_main.cpp
+++ b/src/goto-analyzer/goto_analyzer_main.cpp
@@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 0a6e3c4dd58..c54b6b60f6b 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -457,7 +457,7 @@ bool compilet::parse(const std::string &file_name)
     return true;
   }
 
-  languaget *languagep;
+  std::unique_ptr<languaget> languagep;
 
   // Using '-x', the type of a file can be overridden;
   // otherwise, it's guessed from the extension.
@@ -478,8 +478,7 @@ bool compilet::parse(const std::string &file_name)
     return true;
   }
 
-  languaget &language=*languagep;
-  language.set_message_handler(get_message_handler());
+  languagep->set_message_handler(get_message_handler());
 
   language_filet language_file;
 
@@ -489,7 +488,7 @@ bool compilet::parse(const std::string &file_name)
 
   language_filet &lf=res.first->second;
   lf.filename=file_name;
-  lf.language=languagep;
+  lf.language=std::move(languagep);
 
   if(mode==PREPROCESS_ONLY)
   {
@@ -511,13 +510,13 @@ bool compilet::parse(const std::string &file_name)
       }
     }
 
-    language.preprocess(infile, file_name, *os);
+    lf.language->preprocess(infile, file_name, *os);
   }
   else
   {
     statistics() << "Parsing: " << file_name << eom;
 
-    if(language.parse(infile, file_name))
+    if(lf.language->parse(infile, file_name))
     {
       if(get_ui()==ui_message_handlert::uit::PLAIN)
         error() << "PARSING ERROR" << eom;
diff --git a/src/goto-cc/goto_cc_main.cpp b/src/goto-cc/goto_cc_main.cpp
index 8d3e4222194..8d76e897c77 100644
--- a/src/goto-cc/goto_cc_main.cpp
+++ b/src/goto-cc/goto_cc_main.cpp
@@ -45,7 +45,9 @@ int main(int argc, const char **argv)
 #endif
 {
   #ifdef _MSC_VER
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
   #endif
 
   if(argv==nullptr || argc<1)
diff --git a/src/goto-diff/goto_diff_main.cpp b/src/goto-diff/goto_diff_main.cpp
index 8affa718746..b2ba7e211d6 100644
--- a/src/goto-diff/goto_diff_main.cpp
+++ b/src/goto-diff/goto_diff_main.cpp
@@ -26,7 +26,9 @@ extern unsigned long long irep_cmp_ne_cnt;
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 1bfb9152c50..8fd0f19ca06 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -11,8 +11,8 @@ Author: Peter Schrammel
 
 #include "goto_diff_parse_options.h"
 
-#include <fstream>
 #include <cstdlib> // exit()
+#include <fstream>
 #include <iostream>
 #include <memory>
 
@@ -20,6 +20,7 @@ Author: Peter Schrammel
 #include <util/config.h>
 #include <util/language.h>
 #include <util/options.h>
+#include <util/make_unique.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>
@@ -318,9 +319,9 @@ int goto_diff_parse_optionst::doit()
     return 0;
   }
 
-  std::unique_ptr<goto_difft> goto_diff;
-  goto_diff = std::unique_ptr<goto_difft>(
-    new syntactic_difft(goto_model1, goto_model2, get_message_handler()));
+  std::unique_ptr<goto_difft> goto_diff=
+    util_make_unique<syntactic_difft>(
+      goto_model1, goto_model2, get_message_handler());
   goto_diff->set_ui(get_ui());
 
   (*goto_diff)();
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
index f84d3fbd23b..a9d03b7ad69 100644
--- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
+++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
@@ -12,6 +12,10 @@ Author: Matt Lewis
 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
 
+#include <memory>
+
+#include <util/make_unique.h>
+
 #include <goto-programs/goto_program.h>
 
 #include <analyses/natural_loops.h>
@@ -39,17 +43,10 @@ class enumerating_loop_accelerationt:public loop_accelerationt
     loop(_loop),
     loop_header(_loop_header),
     polynomial_accelerator(symbol_table, goto_functions),
-    path_limit(_path_limit)
-  {
-    // path_enumerator = new all_paths_enumeratort(goto_program, loop,
-    // loop_header);
-    path_enumerator = new sat_path_enumeratort(symbol_table, goto_functions,
-        goto_program, loop, loop_header);
-  }
-
-  ~enumerating_loop_accelerationt()
+    path_limit(_path_limit),
+    path_enumerator(util_make_unique<sat_path_enumeratort>(
+      symbol_table, goto_functions, goto_program, loop, loop_header))
   {
-    delete path_enumerator;
   }
 
   virtual bool accelerate(path_acceleratort &accelerator);
@@ -63,7 +60,7 @@ class enumerating_loop_accelerationt:public loop_accelerationt
   polynomial_acceleratort polynomial_accelerator;
   int path_limit;
 
-  path_enumeratort *path_enumerator;
+  std::unique_ptr<path_enumeratort> path_enumerator;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
index da860f39e1a..a132f597c3a 100644
--- a/src/goto-instrument/accelerate/scratch_program.h
+++ b/src/goto-instrument/accelerate/scratch_program.h
@@ -12,8 +12,10 @@ Author: Matt Lewis
 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
 
+#include <memory>
 #include <string>
 
+#include <util/make_unique.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/goto_program.h>
@@ -38,18 +40,13 @@ class scratch_programt:public goto_programt
     ns(symbol_table),
     equation(ns),
     symex(ns, symbol_table, equation),
-    satcheck(new satcheckt),
+    satcheck(util_make_unique<satcheckt>()),
     satchecker(ns, *satcheck),
     z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
     checker(&z3) // checker(&satchecker)
   {
   }
 
-  ~scratch_programt()
-  {
-    delete satcheck;
-  }
-
   void append(goto_programt::instructionst &instructions);
   void append(goto_programt &program);
   void append_path(patht &path);
@@ -79,7 +76,7 @@ class scratch_programt:public goto_programt
   symex_target_equationt equation;
   goto_symext symex;
 
-  propt *satcheck;
+  std::unique_ptr<propt> satcheck;
   bv_pointerst satchecker;
   smt2_dect z3;
   prop_convt *checker;
diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
index 1b45186b9c9..26a89242aa5 100644
--- a/src/goto-instrument/dump_c_class.h
+++ b/src/goto-instrument/dump_c_class.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <set>
 #include <string>
+#include <memory> // unique_ptr
 
 #include <util/language.h>
 
@@ -39,10 +40,7 @@ class dump_ct
     system_symbols.set_use_all_headers(use_all_headers);
   }
 
-  virtual ~dump_ct()
-  {
-    delete language;
-  }
+  virtual ~dump_ct()=default;
 
   void operator()(std::ostream &out);
 
@@ -50,7 +48,7 @@ class dump_ct
   const goto_functionst &goto_functions;
   symbol_tablet copied_symbol_table;
   const namespacet ns;
-  languaget *language;
+  std::unique_ptr<languaget> language;
 
   typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
   convertedt converted_compound, converted_global, converted_enum;
diff --git a/src/goto-instrument/goto_instrument_main.cpp b/src/goto-instrument/goto_instrument_main.cpp
index 0782ab6352b..a317f471cec 100644
--- a/src/goto-instrument/goto_instrument_main.cpp
+++ b/src/goto-instrument/goto_instrument_main.cpp
@@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-instrument/wmm/instrumenter_strategies.cpp
index b4b04bc1b43..97ad9888f80 100644
--- a/src/goto-instrument/wmm/instrumenter_strategies.cpp
+++ b/src/goto-instrument/wmm/instrumenter_strategies.cpp
@@ -272,9 +272,9 @@ void inline instrumentert::instrument_minimum_interference_inserter(
   const std::size_t mat_size=set_of_cycles.size()*edges.size();
   message.debug() << "size of the system: " << mat_size
     << messaget::eom;
-  int *imat=new int[mat_size+1];
-  int *jmat=new int[mat_size+1];
-  double *vmat=new double[mat_size+1];
+  std::vector<int> imat(mat_size+1);
+  std::vector<int> jmat(mat_size+1);
+  std::vector<double> vmat(mat_size+1);
 
   /* fills the constraints coeff */
   /* tables read from 1 in glpk -- first row/column ignored */
@@ -343,9 +343,6 @@ void inline instrumentert::instrument_minimum_interference_inserter(
   }
 
   glp_delete_prob(lp);
-  delete[] imat;
-  delete[] jmat;
-  delete[] vmat;
 #else
   throw "sorry, minimum interference option requires glpk; "
         "please recompile goto-instrument with glpk";
diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp
index 6a15759f11e..eebb63dcfcd 100644
--- a/src/goto-programs/show_symbol_table.cpp
+++ b/src/goto-programs/show_symbol_table.cpp
@@ -41,25 +41,27 @@ void show_symbol_table_plain(
   {
     const symbolt &symbol=ns.lookup(id);
 
-    languaget *ptr;
+    std::unique_ptr<languaget> ptr;
 
     if(symbol.mode=="")
+    {
       ptr=get_default_language();
+    }
     else
     {
       ptr=get_language_from_mode(symbol.mode);
-      if(ptr==nullptr)
-        throw "symbol "+id2string(symbol.name)+" has unknown mode";
     }
 
-    std::unique_ptr<languaget> p(ptr);
+    if(!ptr)
+      throw "symbol "+id2string(symbol.name)+" has unknown mode";
+
     std::string type_str, value_str;
 
     if(symbol.type.is_not_nil())
-      p->from_type(symbol.type, type_str, ns);
+      ptr->from_type(symbol.type, type_str, ns);
 
     if(symbol.value.is_not_nil())
-      p->from_expr(symbol.value, value_str, ns);
+      ptr->from_expr(symbol.value, value_str, ns);
 
     out << "Symbol......: " << symbol.name << '\n' << std::flush;
     out << "Pretty name.: " << symbol.pretty_name << '\n';
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 6402923c4cf..bd13a853605 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -32,6 +32,8 @@ goto_symex_statet::goto_symex_statet():
   new_frame();
 }
 
+goto_symex_statet::~goto_symex_statet()=default;
+
 void goto_symex_statet::initialize(const goto_functionst &goto_functions)
 {
   goto_functionst::function_mapt::const_iterator it=
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index d62d4a66af9..3c2deecf994 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -13,11 +13,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
 #include <cassert>
+#include <memory>
 #include <unordered_set>
 
 #include <util/guard.h>
 #include <util/std_expr.h>
 #include <util/ssa_expr.h>
+#include <util/make_unique.h>
 
 #include <pointer-analysis/value_set.h>
 #include <goto-programs/goto_functions.h>
@@ -27,10 +29,11 @@ Author: Daniel Kroening, kroening@kroening.com
 class dirtyt;
 
 // central data structure: state
-class goto_symex_statet
+class goto_symex_statet final
 {
 public:
   goto_symex_statet();
+  ~goto_symex_statet();
 
   // distance from entry
   unsigned depth;
@@ -341,7 +344,7 @@ class goto_symex_statet
 
   void switch_to_thread(unsigned t);
   bool record_events;
-  const dirtyt * dirty;
+  std::unique_ptr<const dirtyt> dirty;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 4fce789ad3a..d7a897e7f85 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -12,11 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_symex.h"
 
 #include <cassert>
+#include <memory>
 
 #include <util/std_expr.h>
 #include <util/rename.h>
 #include <util/symbol_table.h>
 #include <util/replace_symbol.h>
+#include <util/make_unique.h>
 
 #include <analyses/dirty.h>
 
@@ -136,7 +138,7 @@ void goto_symext::operator()(
   state.top().end_of_function=--goto_program.instructions.end();
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=&target;
-  state.dirty=new dirtyt(goto_functions);
+  state.dirty=util_make_unique<dirtyt>(goto_functions);
 
   symex_transition(state, state.source.pc);
 
@@ -157,7 +159,6 @@ void goto_symext::operator()(
     }
   }
 
-  delete state.dirty;
   state.dirty=nullptr;
 }
 
diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp
index bc065d7a0e9..0d6c183ec69 100644
--- a/src/java_bytecode/jar_file.cpp
+++ b/src/java_bytecode/jar_file.cpp
@@ -35,21 +35,22 @@ void jar_filet::open(
     {
       // get the length of the filename, including the trailing \0
       mz_uint filename_length=mz_zip_reader_get_filename(&zip, i, nullptr, 0);
-      char *filename_char=new char[filename_length+1];
+      std::vector<char> filename_char(filename_length+1);
       INVARIANT(filename_length>=1, "buffer size must include trailing \\0");
 
       // read and convert to std::string
       mz_uint filename_len=
-        mz_zip_reader_get_filename(&zip, i, filename_char, filename_length);
+        mz_zip_reader_get_filename(
+          &zip, i, filename_char.data(), filename_length);
       INVARIANT(
         filename_length==filename_len,
         "buffer size was incorrectly pre-computed");
-      std::string file_name(filename_char);
+      std::string file_name(filename_char.data());
 #if DEBUG
       debug()
         << "jar_filet.open: idx " << i
         << " len " << filename_len
-        << " filename '" << filename_char << "'" << eom;
+        << " filename '" << std::string(filename_char.data()) << "'" << eom;
 #endif
       INVARIANT(file_name.size()==filename_len-1, "no \\0 found in file name");
 
@@ -64,7 +65,6 @@ void jar_filet::open(
                    << " from " << filename << eom;
         filtered_jar[file_name]=i;
       }
-      delete[] filename_char;
     }
   }
 }
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index bac7157df5c..f966600b38b 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -389,9 +389,9 @@ void java_bytecode_languaget::show_parse(std::ostream &out)
   java_class_loader(main_class).output(out);
 }
 
-languaget *new_java_bytecode_language()
+std::unique_ptr<languaget> new_java_bytecode_language()
 {
-  return new java_bytecode_languaget;
+  return util_make_unique<java_bytecode_languaget>();
 }
 
 bool java_bytecode_languaget::from_expr(
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index a688440e64d..c70e7ce082a 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/language.h>
 #include <util/cmdline.h>
+#include <util/make_unique.h>
 
 #include "java_class_loader.h"
 #include "java_string_library_preprocess.h"
@@ -124,8 +125,8 @@ class java_bytecode_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
-  languaget *new_language() override
-  { return new java_bytecode_languaget; }
+  std::unique_ptr<languaget> new_language() override
+  { return util_make_unique<java_bytecode_languaget>(); }
 
   std::string id() const override { return "java"; }
   std::string description() const override { return "Java Bytecode"; }
@@ -159,6 +160,6 @@ class java_bytecode_languaget:public languaget
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
 };
 
-languaget *new_java_bytecode_language();
+std::unique_ptr<languaget> new_java_bytecode_language();
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index 48b5c8dcbe2..f0c5ad38c13 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -101,9 +101,9 @@ void jsil_languaget::show_parse(std::ostream &out)
   parse_tree.output(out);
 }
 
-languaget *new_jsil_language()
+std::unique_ptr<languaget> new_jsil_language()
 {
-  return new jsil_languaget;
+  return util_make_unique<jsil_languaget>();
 }
 
 bool jsil_languaget::from_expr(
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index 2f6f376525b..da889e111a1 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -12,7 +12,10 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #ifndef CPROVER_JSIL_JSIL_LANGUAGE_H
 #define CPROVER_JSIL_JSIL_LANGUAGE_H
 
+#include <memory>
+
 #include <util/language.h>
+#include <util/make_unique.h>
 
 #include "jsil_parse_tree.h"
 
@@ -32,8 +35,7 @@ class jsil_languaget:public languaget
     symbol_tablet &context,
     const std::string &module);
 
-  virtual bool final(
-    symbol_tablet &context);
+  virtual bool final(symbol_tablet &context);
 
   virtual void show_parse(std::ostream &out);
 
@@ -56,8 +58,8 @@ class jsil_languaget:public languaget
     exprt &expr,
     const namespacet &ns);
 
-  virtual languaget *new_language()
-  { return new jsil_languaget; }
+  virtual std::unique_ptr<languaget> new_language()
+  { return util_make_unique<jsil_languaget>(); }
 
   virtual std::string id() const { return "jsil"; }
   virtual std::string description() const
@@ -72,6 +74,6 @@ class jsil_languaget:public languaget
   std::string parse_path;
 };
 
-languaget *new_jsil_language();
+std::unique_ptr<languaget> new_jsil_language();
 
 #endif // CPROVER_JSIL_JSIL_LANGUAGE_H
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 521354c7aa8..625cc819f42 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -172,25 +172,27 @@ void language_uit::show_symbol_table_plain(
   {
     const symbolt &symbol=ns.lookup(id);
 
-    languaget *ptr;
+    std::unique_ptr<languaget> ptr;
 
     if(symbol.mode=="")
+    {
       ptr=get_default_language();
+    }
     else
     {
       ptr=get_language_from_mode(symbol.mode);
-      if(ptr==nullptr)
-        throw "symbol "+id2string(symbol.name)+" has unknown mode";
     }
 
-    std::unique_ptr<languaget> p(ptr);
+    if(!ptr)
+      throw "symbol "+id2string(symbol.name)+" has unknown mode";
+
     std::string type_str, value_str;
 
     if(symbol.type.is_not_nil())
-      p->from_type(symbol.type, type_str, ns);
+      ptr->from_type(symbol.type, type_str, ns);
 
     if(symbol.value.is_not_nil())
-      p->from_expr(symbol.value, value_str, ns);
+      ptr->from_expr(symbol.value, value_str, ns);
 
     if(brief)
     {
diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp
index a919f6c816f..06398eea3da 100644
--- a/src/langapi/language_util.cpp
+++ b/src/langapi/language_util.cpp
@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "mode.h"
 
-static languaget* get_language(
+static std::unique_ptr<languaget> get_language(
   const namespacet &ns,
   const irep_idt &identifier)
 {
@@ -28,7 +28,7 @@ static languaget* get_language(
      symbol->mode=="")
     return get_default_language();
 
-  languaget *ptr=get_language_from_mode(symbol->mode);
+  std::unique_ptr<languaget> ptr=get_language_from_mode(symbol->mode);
 
   if(ptr==nullptr)
     throw "symbol `"+id2string(symbol->name)+
diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp
index 2c3a852b73a..8d1d9128010 100644
--- a/src/langapi/mode.cpp
+++ b/src/langapi/mode.cpp
@@ -37,7 +37,7 @@ void register_language(language_factoryt factory)
   languages.back().mode=l->id();
 }
 
-languaget *get_language_from_mode(const irep_idt &mode)
+std::unique_ptr<languaget> get_language_from_mode(const irep_idt &mode)
 {
   for(languagest::const_iterator it=languages.begin();
       it!=languages.end();
@@ -48,7 +48,8 @@ languaget *get_language_from_mode(const irep_idt &mode)
   return nullptr;
 }
 
-languaget *get_language_from_filename(const std::string &filename)
+std::unique_ptr<languaget> get_language_from_filename(
+  const std::string &filename)
 {
   std::size_t ext_pos=filename.rfind('.');
 
@@ -82,7 +83,7 @@ languaget *get_language_from_filename(const std::string &filename)
   return nullptr;
 }
 
-languaget *get_default_language()
+std::unique_ptr<languaget> get_default_language()
 {
   assert(!languages.empty());
   return languages.front().factory();
diff --git a/src/langapi/mode.h b/src/langapi/mode.h
index e8cf679d0e2..3edb7a30be8 100644
--- a/src/langapi/mode.h
+++ b/src/langapi/mode.h
@@ -12,13 +12,16 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/irep.h>
 
+#include <memory> // unique_ptr
+
 class languaget;
 
-languaget *get_language_from_mode(const irep_idt &mode);
-languaget *get_language_from_filename(const std::string &filename);
-languaget *get_default_language();
+std::unique_ptr<languaget> get_language_from_mode(const irep_idt &mode);
+std::unique_ptr<languaget> get_language_from_filename(
+  const std::string &filename);
+std::unique_ptr<languaget> get_default_language();
 
-typedef languaget *(*language_factoryt)();
+typedef std::unique_ptr<languaget> (*language_factoryt)();
 void register_language(language_factoryt factory);
 
 #endif // CPROVER_LANGAPI_MODE_H
diff --git a/src/memory-models/mmcc_main.cpp b/src/memory-models/mmcc_main.cpp
index 962c5bbf527..4430059e556 100644
--- a/src/memory-models/mmcc_main.cpp
+++ b/src/memory-models/mmcc_main.cpp
@@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/symex/symex_main.cpp b/src/symex/symex_main.cpp
index 36080f4a69a..8d6f4a2089c 100644
--- a/src/symex/symex_main.cpp
+++ b/src/symex/symex_main.cpp
@@ -16,14 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
-  symex_parse_optionst parse_options(argc, argv);
-  return parse_options.main();
-}
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
+#endif
   symex_parse_optionst parse_options(argc, argv);
   return parse_options.main();
 }
-#endif
diff --git a/src/util/freer.h b/src/util/freer.h
new file mode 100644
index 00000000000..72b6faeab70
--- /dev/null
+++ b/src/util/freer.h
@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module:
+
+Author: Reuben Thomas, reuben.thomas@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_FREER_H
+#define CPROVER_UTIL_FREER_H
+
+#include <cstdlib>
+#include <utility>
+
+/// A functor wrapping `std::free`. Can be used as the deleter of a unique_ptr
+/// to free memory originally allocated by `std::malloc`. This is primarily
+/// useful for interfacing with C APIs in a memory-safe way.
+/// Note that the approach of using an empty functor as a unique_ptr deleter
+/// does not impose any space overhead on the unique_ptr instance, whereas
+/// using a function-pointer as the deleter requires the unique_ptr to store
+/// this function pointer internally, effectively doubling the size of the
+/// object. Therefore, `std::unique_ptr<T, freert>` should be preferred to
+/// `std::unique_ptr<T, decltype(&std::free)>`.
+struct freert
+{
+  template <typename T>
+  void operator()(T &&t) const
+  {
+    free(std::forward<T>(t));
+  }
+};
+
+#endif
diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp
index 835a00b4409..ff31d044829 100644
--- a/src/util/invariant.cpp
+++ b/src/util/invariant.cpp
@@ -6,9 +6,11 @@ Author: Martin Brain, martin.brain@diffblue.com
 
 \*******************************************************************/
 
-
 #include "invariant.h"
 
+#include "util/freer.h"
+
+#include <memory>
 #include <string>
 #include <sstream>
 
@@ -53,18 +55,17 @@ static bool output_demangled_name(
     std::string mangled(working.substr(start+1, length));
 
     int demangle_success=1;
-    char *demangled=
-      abi::__cxa_demangle(mangled.c_str(), nullptr, nullptr, &demangle_success);
+    std::unique_ptr<char, freert> demangled(
+      abi::__cxa_demangle(
+        mangled.c_str(), nullptr, nullptr, &demangle_success));
 
     if(demangle_success==0)
     {
       out << working.substr(0, start+1)
-          << demangled
+          << demangled.get()
           << working.substr(end);
       return_value=true;
     }
-
-    free(demangled);
   }
 
   return return_value;
@@ -83,17 +84,16 @@ void print_backtrace(
     void * stack[50] = {};
 
     std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
-    char **description=backtrace_symbols(stack, entries);
+    std::unique_ptr<char*, freert> description(
+      backtrace_symbols(stack, entries));
 
     for(std::size_t i=0; i<entries; i++)
     {
-      if(!output_demangled_name(out, description[i]))
-        out << description[i];
+      if(!output_demangled_name(out, description.get()[i]))
+        out << description.get()[i];
       out << '\n' << std::flush;
     }
 
-    free(description);
-
 #else
     out << "Backtraces not supported\n" << std::flush;
 #endif
diff --git a/src/util/language.h b/src/util/language.h
index b1e51dbbfec..1b020e03685 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <iosfwd>
 #include <string>
+#include <memory> // unique_ptr
 #include <util/symbol.h>
 #include <util/std_types.h>
 #include <goto-programs/system_library_symbols.h>
@@ -114,7 +115,7 @@ class languaget:public messaget
     exprt &expr,
     const namespacet &ns)=0;
 
-  virtual languaget *new_language()=0;
+  virtual std::unique_ptr<languaget> new_language()=0;
 
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
 
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index 6f4f07716af..300dccd93be 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -19,11 +19,13 @@ language_filet::language_filet(const language_filet &rhs):
 {
 }
 
-language_filet::~language_filet()
-{
-  if(language!=nullptr)
-    delete language;
-}
+/// To avoid compiler errors, the complete definition of a pointed-to type must
+/// be visible at the point at which the unique_ptr destructor is created.  In
+/// this case, the pointed-to type is forward-declared, so we have to place the
+/// destructor in the source file, where the full definition is availible.
+language_filet::~language_filet()=default;
+
+language_filet::language_filet()=default;
 
 void language_filet::get_modules()
 {
@@ -51,8 +53,8 @@ void language_filest::set_should_generate_opaque_method_stubs(
 {
   for(file_mapt::value_type &language_file_entry : file_map)
   {
-    languaget *language=language_file_entry.second.language;
-    language->set_should_generate_opaque_method_stubs(stubs_enabled);
+    auto &language=*language_file_entry.second.language;
+    language.set_should_generate_opaque_method_stubs(stubs_enabled);
   }
 }
 
diff --git a/src/util/language_file.h b/src/util/language_file.h
index 4404d1868e4..e414182e3c5 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <map>
 #include <string>
+#include <memory> // unique_ptr
 
 #include "message.h"
 
@@ -21,7 +22,7 @@ class symbol_tablet;
 class language_filet;
 class languaget;
 
-class language_modulet
+class language_modulet final
 {
 public:
   std::string name;
@@ -35,13 +36,13 @@ class language_modulet
   {}
 };
 
-class language_filet
+class language_filet final
 {
 public:
   typedef std::set<std::string> modulest;
   modulest modules;
 
-  languaget *language;
+  std::unique_ptr<languaget> language;
   std::string filename;
 
   void get_modules();
@@ -50,12 +51,9 @@ class language_filet
     const irep_idt &id,
     symbol_tablet &symbol_table);
 
+  language_filet();
   language_filet(const language_filet &rhs);
 
-  language_filet():language(nullptr)
-  {
-  }
-
   ~language_filet();
 };
 
diff --git a/src/util/make_unique.h b/src/util/make_unique.h
new file mode 100644
index 00000000000..0f4ba41ac3e
--- /dev/null
+++ b/src/util/make_unique.h
@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Really simple unique_ptr utilities
+
+Author: Reuben Thomas, reuben.thomas@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_MAKE_UNIQUE_H
+#define CPROVER_UTIL_MAKE_UNIQUE_H
+
+#include <memory> // unique_ptr
+
+// This is a stand-in for std::make_unique, which isn't part of the standard
+// library until C++14.  When we move to C++14, we should do a find-and-replace
+// on this to use std::make_unique instead.
+
+template<typename T, typename... Ts>
+std::unique_ptr<T> util_make_unique(Ts &&... ts)
+{
+  return std::unique_ptr<T>(new T(std::forward<Ts>(ts)...));
+}
+
+#endif
diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp
index 77ffa9ed614..6de218f24ed 100644
--- a/src/util/mp_arith.cpp
+++ b/src/util/mp_arith.cpp
@@ -8,12 +8,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "mp_arith.h"
 
-#include <cstdlib>
+#include <cassert>
 #include <cctype>
-
-#include <sstream>
-#include <ostream>
+#include <cstdlib>
 #include <limits>
+#include <ostream>
+#include <sstream>
+#include <vector>
 
 #include "arith_tools.h"
 #include "invariant.h"
@@ -79,13 +80,11 @@ const std::string integer2binary(const mp_integer &n, std::size_t width)
   }
 
   std::size_t len = a.digits(2) + 2;
-  char *buffer=new char[len];
-  char *s = a.as_string(buffer, len, 2);
+  std::vector<char> buffer(len);
+  char *s = a.as_string(buffer.data(), len, 2);
 
   std::string result(s);
 
-  delete[] buffer;
-
   if(result.size()<width)
   {
     std::string fill;
@@ -107,13 +106,11 @@ const std::string integer2binary(const mp_integer &n, std::size_t width)
 const std::string integer2string(const mp_integer &n, unsigned base)
 {
   unsigned len = n.digits(base) + 2;
-  char *buffer=new char[len];
-  char *s = n.as_string(buffer, len, base);
+  std::vector<char> buffer(len);
+  char *s = n.as_string(buffer.data(), len, base);
 
   std::string result(s);
 
-  delete[] buffer;
-
   return result;
 }
 
diff --git a/src/util/pipe_stream.cpp b/src/util/pipe_stream.cpp
index e9fc1887fb5..c2875a11d12 100644
--- a/src/util/pipe_stream.cpp
+++ b/src/util/pipe_stream.cpp
@@ -106,19 +106,17 @@ int pipe_streamt::run()
   for(const auto &s : args)
         command += L" " + ::widen(s);
 
-  LPWSTR lpCommandLine = new wchar_t[command.length()+1];
+  std::vector<wchar_t> lpCommandLine(command.length()+1);
 
   #ifdef _MSC_VER
-  wcscpy_s(lpCommandLine, command.length()+1, command.c_str());
+  wcscpy_s(lpCommandLine.data(), command.length()+1, command.c_str());
   #else
-  wcsncpy(lpCommandLine, command.c_str(), command.length()+1);
+  wcsncpy(lpCommandLine.data(), command.c_str(), command.length()+1);
   #endif
 
-  BOOL ret=CreateProcessW(NULL, lpCommandLine, NULL, NULL, TRUE,
+  BOOL ret=CreateProcessW(NULL, lpCommandLine.data(), NULL, NULL, TRUE,
                           CREATE_NO_WINDOW, NULL, NULL, &si, &pi);
 
-  delete lpCommandLine; // clean up
-
   if(!ret)
     return -1;
 
@@ -147,7 +145,7 @@ int pipe_streamt::run()
     dup2(in[0], STDIN_FILENO);
     dup2(out[1], STDOUT_FILENO);
 
-    char **_argv=new char * [args.size()+2];
+    std::vector<char *> _argv(args.size()+2);
 
     _argv[0]=strdup(executable.c_str());
 
@@ -161,7 +159,7 @@ int pipe_streamt::run()
 
     _argv[args.size()+1]=nullptr;
 
-    int result=execvp(executable.c_str(), _argv);
+    int result=execvp(executable.c_str(), _argv.data());
 
     if(result==-1)
       perror(nullptr);
@@ -218,14 +216,14 @@ int pipe_streamt::wait()
 filedescriptor_streambuft::filedescriptor_streambuft():
   #ifdef _WIN32
   proc_in(INVALID_HANDLE_VALUE),
-  proc_out(INVALID_HANDLE_VALUE)
+  proc_out(INVALID_HANDLE_VALUE),
   #else
   proc_in(STDOUT_FILENO),
-  proc_out(STDIN_FILENO)
+  proc_out(STDIN_FILENO),
   #endif
+  in_buffer(READ_BUFFER_SIZE)
 {
-  in_buffer=new char[READ_BUFFER_SIZE];
-  setg(in_buffer, in_buffer, in_buffer);
+  setg(in_buffer.data(), in_buffer.data(), in_buffer.data());
 }
 
 /// Destructor
@@ -248,8 +246,6 @@ filedescriptor_streambuft::~filedescriptor_streambuft()
     close(proc_out);
 
   #endif
-
-  delete in_buffer;
 }
 
 /// write one character to the piped process
diff --git a/src/util/pipe_stream.h b/src/util/pipe_stream.h
index 385cb65f790..748038ff2b6 100644
--- a/src/util/pipe_stream.h
+++ b/src/util/pipe_stream.h
@@ -15,6 +15,7 @@ Module: A stdin/stdout pipe as STL stream
 #include <iostream>
 #include <string>
 #include <list>
+#include <vector>
 
 #ifdef _WIN32
 #include <windows.h>
@@ -43,7 +44,7 @@ class filedescriptor_streambuft:public std::streambuf
 
 protected:
   HANDLE proc_in, proc_out;
-  char *in_buffer;
+  std::vector<char> in_buffer;
 
   int_type overflow(int_type);
   std::streamsize xsputn(const char *, std::streamsize);
diff --git a/src/util/run.cpp b/src/util/run.cpp
index c01aff35bd6..f106309002e 100644
--- a/src/util/run.cpp
+++ b/src/util/run.cpp
@@ -61,7 +61,7 @@ int run(
   for(std::size_t i=0; i<argv.size(); i++)
     wargv[i]=widen(argv[i]);
 
-  const wchar_t **_argv=new const wchar_t * [argv.size()+1];
+  std::vector<const wchar_t *> _argv(argv.size()+1);
 
   for(std::size_t i=0; i<wargv.size(); i++)
     _argv[i]=wargv[i].c_str();
@@ -72,9 +72,7 @@ int run(
 
   std::wstring wide_what=widen(what);
 
-  int status=_wspawnvp(_P_WAIT, wide_what.c_str(), _argv);
-
-  delete[] _argv;
+  int status=_wspawnvp(_P_WAIT, wide_what.c_str(), _argv.data());
 
   return status;
 
@@ -119,7 +117,7 @@ int run(
       remove_signal_catcher();
       sigprocmask(SIG_SETMASK, &old_mask, nullptr);
 
-      char **_argv=new char * [argv.size()+1];
+      std::vector<char *> _argv(argv.size()+1);
       for(std::size_t i=0; i<argv.size(); i++)
         _argv[i]=strdup(argv[i].c_str());
 
@@ -129,7 +127,7 @@ int run(
         dup2(stdin_fd, STDIN_FILENO);
       if(stdout_fd!=STDOUT_FILENO)
         dup2(stdout_fd, STDOUT_FILENO);
-      execvp(what.c_str(), _argv);
+      execvp(what.c_str(), _argv.data());
 
       /* usually no return */
       return 1;
diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h
index 9f8cc0a4416..c2501f7f345 100644
--- a/src/util/sharing_node.h
+++ b/src/util/sharing_node.h
@@ -64,7 +64,7 @@ class sharing_nodet
     d.k=std::make_shared<key_type>(k);
 
     _sn_assert(d.m==nullptr);
-    d.m.reset(new mapped_type(m));
+    d.m=std::make_shared<mapped_type>(m);
   }
 
   sharing_nodet(const self_type &other)
@@ -266,7 +266,7 @@ class sharing_nodet
       if(d.is_leaf())
       {
         _sn_assert(m==nullptr);
-        m.reset(new mapped_type(*d.m));
+        m=std::make_shared<mapped_type>(*d.m);
       }
     }
 
@@ -277,7 +277,7 @@ class sharing_nodet
     }
 
     std::shared_ptr<key_type> k;
-    std::unique_ptr<mapped_type> m;
+    std::shared_ptr<mapped_type> m;
 
     subt sub;
     containert con;
@@ -339,8 +339,8 @@ class sharing_nodet
 
 template <class keyT, class valueT, class predT, bool no_sharing>
 std::shared_ptr<typename sharing_nodet<keyT, valueT, predT, no_sharing>::dt>
-  sharing_nodet<keyT, valueT, predT, no_sharing>::empty_data(
-    new sharing_nodet<keyT, valueT, predT, no_sharing>::dt());
+  sharing_nodet<keyT, valueT, predT, no_sharing>::empty_data=
+    std::make_shared<sharing_nodet<keyT, valueT, predT, no_sharing>::dt>();
 
 template <class keyT, class valueT, class predT, bool no_sharing>
 sharing_nodet<keyT, valueT, predT, no_sharing>
diff --git a/src/util/unicode.cpp b/src/util/unicode.cpp
index 6e0c483ec08..4603d6d8023 100644
--- a/src/util/unicode.cpp
+++ b/src/util/unicode.cpp
@@ -152,17 +152,15 @@ std::string utf32_to_utf8(const std::basic_string<unsigned int> &s)
   return result;
 }
 
-const char **narrow_argv(int argc, const wchar_t **argv_wide)
+std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide)
 {
   if(argv_wide==nullptr)
-    return nullptr;
+    return std::vector<std::string>();
 
-  // the following never gets deleted
-  const char **argv_narrow=new const char *[argc+1];
-  argv_narrow[argc]=nullptr;
+  std::vector<std::string> argv_narrow(argc);
 
-  for(int i=0; i<argc; i++)
-    argv_narrow[i]=strdup(narrow(argv_wide[i]).c_str());
+  for(int i=0; i!=argc; ++i)
+    argv_narrow[i]=narrow(argv_wide[i]);
 
   return argv_narrow;
 }
diff --git a/src/util/unicode.h b/src/util/unicode.h
index 22b7fadb464..2133123f50c 100644
--- a/src/util/unicode.h
+++ b/src/util/unicode.h
@@ -10,7 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_UNICODE_H
 #define CPROVER_UTIL_UNICODE_H
 
+#include <algorithm>
 #include <string>
+#include <vector>
 
 // we follow the ideas suggested at
 // http://www.utf8everywhere.org/
@@ -26,6 +28,18 @@ std::wstring utf8_to_utf16_big_endian(const std::string &);
 std::wstring utf8_to_utf16_little_endian(const std::string &);
 std::string utf16_little_endian_to_java(const std::wstring &in);
 
-const char **narrow_argv(int argc, const wchar_t **argv_wide);
+std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide);
+
+template <typename It>
+std::vector<const char *> to_c_str_array(It b, It e)
+{
+  // Assumes that walking the range will be faster than repeated allocation
+  std::vector<const char *> ret(std::distance(b, e) + 1, nullptr);
+  std::transform(b, e, std::begin(ret), [] (const std::string & s)
+    {
+      return s.c_str();
+    });
+  return ret;
+}
 
 #endif // CPROVER_UTIL_UNICODE_H