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.
This commit is contained in:
Alexandre Duret-Lutz 2009-05-28 18:18:00 +02:00
parent d74578ef6e
commit 352984293a
4 changed files with 30 additions and 1 deletions

View file

@ -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> 2009-05-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Implement spot::future_conditions_collector. Implement spot::future_conditions_collector.

View file

@ -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 unsigned
scc_map::initial() const scc_map::initial() const
{ {
@ -182,6 +195,10 @@ namespace spot
continue; continue;
} }
// If we now the state, reuse the previous object.
delete dest;
dest = spi->first;
// Have we reached a maximal SCC? // Have we reached a maximal SCC?
if (spi->second >= 0) if (spi->second >= 0)
{ {

View file

@ -64,6 +64,7 @@ namespace spot
typedef std::set<bdd, bdd_less_than> cond_set; typedef std::set<bdd, bdd_less_than> cond_set;
scc_map(const tgba* aut); scc_map(const tgba* aut);
~scc_map();
void build_map(); void build_map();

View file

@ -1,5 +1,5 @@
#!/bin/sh #!/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 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
@ -29,6 +29,7 @@ check ()
{ {
run 0 ./ltl2tgba "$1" run 0 ./ltl2tgba "$1"
run 0 ./ltl2tgba -f "$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 # We don't check the output, but just running these might be enough to