From 352984293abef4c643723003a3aca0d0830818c7 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 28 May 2009 18:18:00 +0200
Subject: [PATCH] Test "ltl2tgba -FC" and plug the memory leaks of scc_map.

* src/tgbaalgos/scc.hh (scc_map::~scc_map): Declare it.
* src/tgbaalgos/scc.cc (scc_map::~scc_map): Implement it.
(scc_map::build_map): Delete duplicate states.
* src/tbbatest/ltl2tgba.test: Run ltl2tgba -FV to catch
memory leaks with valgrind.
---
 ChangeLog                  | 10 ++++++++++
 src/tgbaalgos/scc.cc       | 17 +++++++++++++++++
 src/tgbaalgos/scc.hh       |  1 +
 src/tgbatest/ltl2tgba.test |  3 ++-
 4 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/ChangeLog b/ChangeLog
index 6fa5a9e2e..f76af1a55 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,13 @@
+2009-05-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Test "ltl2tgba -FC" and plug the memory leaks of scc_map.
+
+	* src/tgbaalgos/scc.hh (scc_map::~scc_map): Declare it.
+	* src/tgbaalgos/scc.cc (scc_map::~scc_map): Implement it.
+	(scc_map::build_map): Delete duplicate states.
+	* src/tbbatest/ltl2tgba.test: Run ltl2tgba -FV to catch
+	memory leaks with valgrind.
+
 2009-05-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Implement spot::future_conditions_collector.
diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc
index e527310f9..23ef562f5 100644
--- a/src/tgbaalgos/scc.cc
+++ b/src/tgbaalgos/scc.cc
@@ -44,6 +44,19 @@ namespace spot
   {
   }
 
+  scc_map::~scc_map()
+  {
+    hash_type::iterator i = h_.begin();
+
+    while (i != h_.end())
+      {
+	// Advance the iterator before deleting the key.
+	const state* s = i->first;
+	++i;
+	delete s;
+      }
+  }
+
   unsigned
   scc_map::initial() const
   {
@@ -182,6 +195,10 @@ namespace spot
 	    continue;
 	  }
 
+	// If we now the state, reuse the previous object.
+	delete dest;
+	dest = spi->first;
+
 	// Have we reached a maximal SCC?
 	if (spi->second >= 0)
 	  {
diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh
index 1f806590c..b4ed08e02 100644
--- a/src/tgbaalgos/scc.hh
+++ b/src/tgbaalgos/scc.hh
@@ -64,6 +64,7 @@ namespace spot
     typedef std::set<bdd, bdd_less_than> cond_set;
 
     scc_map(const tgba* aut);
+    ~scc_map();
 
     void build_map();
 
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index 1dbceb51e..c1321d2e4 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -29,6 +29,7 @@ check ()
 {
   run 0 ./ltl2tgba "$1"
   run 0 ./ltl2tgba -f "$1"
+  run 0 ./ltl2tgba -f -FC "$1"
 }
 
 # We don't check the output, but just running these might be enough to