From f01d30eb9186f061d10790ef9a06b55376f7464c Mon Sep 17 00:00:00 2001
From: Thomas Badie <badie@lrde.epita.fr>
Date: Tue, 4 Sep 2012 16:19:59 +0200
Subject: [PATCH] Create unique_ptr for Spot.

* src/misc/unique_ptr.hh: Create unique_ptr for Spot.
* src/misc/Makefile.am: Register this new file.
* src/tgbatest/ltl2tgba.cc: Replace two calls to delete by the
utilisation of unique_ptr.
* src/tgbaalgos/simulation.cc: Replace two calls to delete by the
utilisation of unique_ptr.
---
 src/misc/Makefile.am        |  1 +
 src/misc/unique_ptr.hh      | 83 +++++++++++++++++++++++++++++++++++++
 src/tgbaalgos/simulation.cc |  9 ++--
 src/tgbatest/ltl2tgba.cc    |  9 ++--
 4 files changed, 91 insertions(+), 11 deletions(-)
 create mode 100644 src/misc/unique_ptr.hh

diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am
index 22bd419c6..6228db472 100644
--- a/src/misc/Makefile.am
+++ b/src/misc/Makefile.am
@@ -52,6 +52,7 @@ misc_HEADERS = \
   optionmap.hh \
   random.hh \
   timer.hh \
+  unique_ptr.hh \
   version.hh
 
 noinst_LTLIBRARIES = libmisc.la
diff --git a/src/misc/unique_ptr.hh b/src/misc/unique_ptr.hh
new file mode 100644
index 000000000..e96eaed58
--- /dev/null
+++ b/src/misc/unique_ptr.hh
@@ -0,0 +1,83 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2012 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_MISC_UNIQUE_PTR_HH
+# define SPOT_MISC_UNIQUE_PTR_HH
+
+namespace spot
+{
+  /// \brief Take ownership of a pointer at its construction, and
+  /// destroy it at the end of the scope.
+  template <typename T>
+  class unique_ptr
+  {
+    typedef T* pointer;
+  public:
+    unique_ptr(pointer ptr)
+      : ptr_(ptr)
+    {
+    }
+
+    ~unique_ptr()
+    {
+      delete ptr_;
+    }
+
+    operator pointer()
+    {
+      return ptr_;
+    }
+
+    pointer
+    operator->()
+    {
+      return ptr_;
+    }
+
+  private:
+    pointer ptr_;
+
+    // This copy gives the ownership of the pointer to the new copy.
+    // Can only be used by make_unique.
+    unique_ptr(const unique_ptr& up)
+    {
+      unique_ptr& non_const_up = const_cast<unique_ptr&>(up);
+      ptr_ = non_const_up.ptr_;
+      non_const_up.ptr_ = 0;
+    }
+
+    // Allow `make_unique' to have an access to the private copy.
+    template <typename V> friend unique_ptr<V> make_unique(V* ptr);
+
+    unique_ptr& operator=(const unique_ptr&);
+  };
+
+
+  /// \brief Change a pointer into a unique_ptr.
+  template <typename T>
+  inline unique_ptr<T> make_unique(T* ptr)
+  {
+    return unique_ptr<T>(ptr);
+  }
+}
+
+
+#endif // !SPOT_MISC_UNIQUE_PTR_HH
diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index 1e772063b..0a58565f0 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -26,6 +26,7 @@
 #include "simulation.hh"
 #include "misc/acccompl.hh"
 #include "misc/minato.hh"
+#include "misc/unique_ptr.hh"
 #include "tgba/bddprint.hh"
 #include "tgbaalgos/reachiter.hh"
 #include "tgbaalgos/sccfilter.hh"
@@ -702,7 +703,6 @@ namespace spot
       state* initial_state;
 
       automaton_size stat;
-
     };
 
   } // End namespace anonymous.
@@ -735,21 +735,18 @@ namespace spot
         prev = next;
         direct_simulation<false> simul(res);
 
-        tgba* after_simulation = simul.run();
+        unique_ptr<tgba> after_simulation(simul.run());
 
         if (res != t)
           delete res;
 
         direct_simulation<true> cosimul(after_simulation);
 
-        tgba* after_cosimulation = cosimul.run();
+        unique_ptr<tgba> after_cosimulation(cosimul.run());
 
         next = cosimul.get_stat();
 
         res = scc_filter(after_cosimulation, false);
-
-        delete after_cosimulation;
-        delete after_simulation;
       }
     while (prev != next);
 
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 6c690ecb1..fb45f6334 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -59,6 +59,7 @@
 #include "tgbaalgos/gtec/gtec.hh"
 #include "eltlparse/public.hh"
 #include "misc/timer.hh"
+#include "misc/unique_ptr.hh"
 #include "tgbaalgos/stats.hh"
 #include "tgbaalgos/scc.hh"
 #include "tgbaalgos/emptiness_stats.hh"
@@ -1364,9 +1365,8 @@ main(int argc, char** argv)
 		    // It is possible that we have applied other
 		    // operations to the automaton since its initial
 		    // degeneralization.  Let's degeneralize again!
-		    spot::tgba* s = spot::degeneralize(a);
+                    spot::unique_ptr<spot::tgba> s(spot::degeneralize(a));
 		    spot::never_claim_reachable(std::cout, s, f, spin_comments);
-		    delete s;
 		  }
 		break;
 	      }
@@ -1562,10 +1562,9 @@ main(int argc, char** argv)
 				}
 			      else if (graph_run_tgba_opt)
 				{
-				  spot::tgba* ar =
-				    spot::tgba_run_to_tgba(a, run);
+                                  spot::unique_ptr<spot::tgba>
+                                    ar(spot::tgba_run_to_tgba(a, run));
 				  spot::dotty_reachable(std::cout, ar, false);
-				  delete ar;
 				}
 			      else
 				{