From 574a2285830a45917de2390da4b21a2b61c8229b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 25 Jan 2011 18:56:42 +0100 Subject: [PATCH] Introduce a destroy() method on states, and use it instead of delete. Right now, destroy() just executes "delete this". But in a later version, we will rewrite tgba_explicit so that it does not allocate new states (and the destroy() method for explicit state will do nothing). * src/tgba/state.hh (state::destroy): New method, to replace state::~state() in the future. (shared_state_deleter): New function. * src/evtgba/product.cc, src/evtgbaalgos/reachiter.cc, src/evtgbaalgos/save.cc, src/evtgbaalgos/tgba2evtgba.cc, src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, src/tgbaalgos/cutscc.cc, src/tgbaalgos/emptiness.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.hh, src/tgbaalgos/reachiter.cc, src/tgbaalgos/reducerun.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/replayrun.cc, src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust to call "s->destroy()" instead of "delete s". * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc: Pass shared_state_deleter to the shared_ptr constructor, so that it calls destroy() instead of delete. --- ChangeLog | 38 ++++++++++++++++++++++++++++-- src/evtgba/product.cc | 4 ++-- src/evtgbaalgos/reachiter.cc | 6 +++-- src/evtgbaalgos/save.cc | 6 +++-- src/evtgbaalgos/tgba2evtgba.cc | 4 ++-- src/saba/sabacomplementtgba.cc | 11 +++++---- src/tgba/state.hh | 25 +++++++++++++++++++- src/tgba/tgba.cc | 14 +++++++---- src/tgba/tgbakvcomplement.cc | 9 +++---- src/tgba/tgbaproduct.cc | 4 ++-- src/tgba/tgbareduc.cc | 10 ++++---- src/tgba/tgbasafracomplement.cc | 10 ++++---- src/tgba/tgbasgba.cc | 4 ++-- src/tgba/tgbatba.cc | 18 +++++++------- src/tgba/tgbaunion.cc | 10 ++++---- src/tgba/wdbacomp.cc | 3 ++- src/tgbaalgos/cutscc.cc | 14 +++++------ src/tgbaalgos/emptiness.cc | 12 +++++----- src/tgbaalgos/gtec/ce.cc | 10 ++++---- src/tgbaalgos/gtec/explscc.cc | 4 +++- src/tgbaalgos/gtec/gtec.cc | 4 ++-- src/tgbaalgos/gtec/nsheap.cc | 8 ++++--- src/tgbaalgos/gv04.cc | 12 +++++----- src/tgbaalgos/magic.cc | 10 ++++---- src/tgbaalgos/minimize.cc | 20 ++++++++-------- src/tgbaalgos/ndfs_result.hxx | 34 +++++++++++++------------- src/tgbaalgos/neverclaim.cc | 10 ++++---- src/tgbaalgos/powerset.hh | 4 ++-- src/tgbaalgos/reachiter.cc | 6 ++--- src/tgbaalgos/reducerun.cc | 8 ++++--- src/tgbaalgos/reductgba_sim.cc | 10 ++++---- src/tgbaalgos/reductgba_sim_del.cc | 12 +++++----- src/tgbaalgos/replayrun.cc | 18 +++++++------- src/tgbaalgos/safety.cc | 4 ++-- src/tgbaalgos/save.cc | 10 ++++---- src/tgbaalgos/scc.cc | 6 ++--- src/tgbaalgos/se05.cc | 14 ++++++----- src/tgbaalgos/tau03.cc | 8 ++++--- src/tgbaalgos/tau03opt.cc | 12 ++++++---- 39 files changed, 259 insertions(+), 167 deletions(-) diff --git a/ChangeLog b/ChangeLog index f1fe395c7..0de9e43ac 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,40 @@ +2011-01-25 Alexandre Duret-Lutz + + Introduce a destroy() method on states, and use it instead of delete. + + Right now, destroy() just executes "delete this". But in a later + version, we will rewrite tgba_explicit so that it does not + allocate new states (and the destroy() method for explicit state + will do nothing). + + * src/tgba/state.hh (state::destroy): New method, to replace + state::~state() in the future. + (shared_state_deleter): New function. + * src/evtgba/product.cc, src/evtgbaalgos/reachiter.cc, + src/evtgbaalgos/save.cc, src/evtgbaalgos/tgba2evtgba.cc, + src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc, + src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc, + src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc, + src/tgbaalgos/cutscc.cc, src/tgbaalgos/emptiness.cc, + src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.cc, + src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/nsheap.cc, + src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, + src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx, + src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.hh, + src/tgbaalgos/reachiter.cc, src/tgbaalgos/reducerun.cc, + src/tgbaalgos/reductgba_sim.cc, + src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/replayrun.cc, + src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, + src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc, + src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust to call + "s->destroy()" instead of "delete s". + * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc: + Pass shared_state_deleter to the shared_ptr constructor, so that + it calls destroy() instead of delete. + 2011-01-26 Alexandre Duret-Lutz - * wrap/python/ajax/ltl2tgba.html: Display the Spot version in + * wrap/python/ajax/ltl2tgba.html: Display the Spot version in the tooltip over the Spot logo. 2011-01-26 Alexandre Duret-Lutz @@ -17,7 +51,7 @@ * wrap/python/ajax/ltl2tgba.html: Remove the auto-update button, and enable auto-update automatically after the first submission. Add - tools tips for the "Desired Output" tabs, and the Spot logo. + tools tips for the "Desired Output" tabs, and the Spot logo. Add a email icon to encourage feedback. * wrap/python/ajax/ltl2tgba.css: fix sizes of formula field and send button. Set position of mail icon. diff --git a/src/evtgba/product.cc b/src/evtgba/product.cc index 067987e82..63ef1575f 100644 --- a/src/evtgba/product.cc +++ b/src/evtgba/product.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -43,7 +43,7 @@ namespace spot ~evtgba_product_state() { for (int j = 0; j < n_; ++j) - delete s_[j]; + s_[j]->destroy(); delete[] s_; } diff --git a/src/evtgbaalgos/reachiter.cc b/src/evtgbaalgos/reachiter.cc index 60432c06e..a7065be97 100644 --- a/src/evtgbaalgos/reachiter.cc +++ b/src/evtgbaalgos/reachiter.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -40,7 +42,7 @@ namespace spot // Advance the iterator before deleting the "key" pointer. const state* ptr = s->first; ++s; - delete ptr; + ptr->destroy(); } } @@ -79,7 +81,7 @@ namespace spot else { process_link(tn, s->second, si); - delete current; + current->destroy(); } } delete si; diff --git a/src/evtgbaalgos/save.cc b/src/evtgbaalgos/save.cc index ce46af751..3bb82db8a 100644 --- a/src/evtgbaalgos/save.cc +++ b/src/evtgbaalgos/save.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -48,7 +50,7 @@ namespace spot { const state* s = i->current_state(); os_ << " " << quote_unless_bare_word(automata_->format_state(s)); - delete s; + s->destroy(); } os_ << ";" << std::endl; delete i; @@ -69,7 +71,7 @@ namespace spot << ","; output_acc_set(si->current_acceptance_conditions()); os_ << ";" << std::endl; - delete dest; + dest->destroy(); } } diff --git a/src/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc index b50b4a9ea..d103c5ef1 100644 --- a/src/evtgbaalgos/tgba2evtgba.cc +++ b/src/evtgbaalgos/tgba2evtgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -72,7 +72,7 @@ namespace spot { const state* s = si->current_state(); process_state(s, out, 0); - delete s; + s->destroy(); } rsymbol_set ss = acc_to_symbol_set(si->current_acceptance_conditions()); diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc index 201facc66..a0f28526e 100644 --- a/src/saba/sabacomplementtgba.cc +++ b/src/saba/sabacomplementtgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -220,7 +220,8 @@ namespace spot { bdd c = iterator->current_condition(); if ((c & condition) != bddfalse) - state_list.push_back(shared_state(iterator->current_state())); + state_list.push_back(shared_state(iterator->current_state(), + shared_state_deleter)); } delete iterator; @@ -399,12 +400,14 @@ namespace spot saba_state_complement_tgba* new_init; if (automaton_->state_is_accepting(original_init_state)) new_init = - new saba_state_complement_tgba(shared_state(original_init_state), + new saba_state_complement_tgba(shared_state(original_init_state, + shared_state_deleter), 2 * nb_states_, the_acceptance_cond_); else new_init = - new saba_state_complement_tgba(shared_state(original_init_state), + new saba_state_complement_tgba(shared_state(original_init_state, + shared_state_deleter), 2 * nb_states_, bddfalse); diff --git a/src/tgba/state.hh b/src/tgba/state.hh index 1b5911b6c..8947bd89e 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -74,6 +74,27 @@ namespace spot /// Duplicate a state. virtual state* clone() const = 0; + /// \brief Release a state. + /// + /// Methods from the tgba or tgba_succ_iterator always return a + /// new state that you should deallocate with this function. + /// Before Spot 0.7, you had to "delete" your state directly. + /// Starting with Spot 0.7, you update your code to this function + /// instead (which simply calls "delete"). In a future version, + /// some subclasses will redefine destroy() to allow better memory + /// management (e.g. no memory allocation for explicit automata). + virtual void destroy() const + { + delete this; + } + + // FIXME: Make the destructor protected after Spot 0.7. + //protected: + + /// \brief Destructor. + /// + /// \deprecated Client code should now call + /// s->destroy(); instead of delete s;. virtual ~state() { } @@ -156,6 +177,8 @@ namespace spot typedef boost::shared_ptr shared_state; + inline void shared_state_deleter(state* s) { s->destroy(); } + /// \brief Strict Weak Ordering for \c shared_state /// (shared_ptr). /// \ingroup tgba_essentials diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index 19a7383c1..dd6a46fad 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -32,8 +34,10 @@ namespace spot tgba::~tgba() { - delete last_support_conditions_input_; - delete last_support_variables_input_; + if (last_support_conditions_input_) + last_support_conditions_input_->destroy(); + if (last_support_variables_input_) + last_support_variables_input_->destroy(); } bdd @@ -43,7 +47,8 @@ namespace spot || last_support_conditions_input_->compare(state) != 0) { last_support_conditions_output_ = compute_support_conditions(state); - delete last_support_conditions_input_; + if (last_support_conditions_input_) + last_support_conditions_input_->destroy(); last_support_conditions_input_ = state->clone(); } return last_support_conditions_output_; @@ -56,7 +61,8 @@ namespace spot || last_support_variables_input_->compare(state) != 0) { last_support_variables_output_ = compute_support_variables(state); - delete last_support_variables_input_; + if (last_support_variables_input_) + last_support_variables_input_->destroy(); last_support_variables_input_ = state->clone(); } return last_support_variables_output_; diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index 0f0ef4bd1..7c5a5b228 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -443,7 +443,7 @@ namespace spot bdd c = iterator->current_condition(); if ((c & condition) != bddfalse) { - shared_state s(iterator->current_state()); + shared_state s(iterator->current_state(), shared_state_deleter); if (highest_current_ranks_.find(s) != highest_current_ranks_.end()) { if (i->second < highest_current_ranks_[s]) @@ -470,7 +470,7 @@ namespace spot bdd c = iterator->current_condition(); if ((c & condition) != bddfalse) { - shared_state s(iterator->current_state()); + shared_state s(iterator->current_state(), shared_state_deleter); highest_state_set_.insert(s); } } @@ -621,7 +621,8 @@ namespace spot { state_kv_complement* init = new state_kv_complement(); rank_t r = {2 * nb_states_, bdd_ordered()}; - init->add(shared_state(automaton_->get_init_state()), r); + init->add(shared_state(automaton_->get_init_state(), shared_state_deleter), + r); return init; } diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index dd502796a..f925ba06e 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -41,8 +41,8 @@ namespace spot state_product::~state_product() { - delete left_; - delete right_; + left_->destroy(); + right_->destroy(); } int diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index bc9818efc..6fab4ee32 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -156,7 +156,7 @@ namespace spot spot::state* init = automata_->get_init_state(); if (init->compare(s) == 0) this->set_init_state(automata_->format_state(s)); - delete init; + init->destroy(); transition* t; for (si->first(); !si->done(); si->next()) @@ -165,7 +165,7 @@ namespace spot t = this->create_transition(s, init); this->add_conditions(t, si->current_condition()); this->add_acceptance_conditions(t, si->current_acceptance_conditions()); - delete init; + init->destroy(); } } @@ -361,7 +361,7 @@ namespace spot sim1 = sim2; sim2 = simtmp; } - delete init; + init->destroy(); sp_map::iterator i = state_predecessor_map_.find(s1); if (i == state_predecessor_map_.end()) // 0 predecessor diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 4464ae38e..0e4fd053e 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -170,7 +170,7 @@ namespace spot delete *i; for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i) - delete *i; + (*i)->destroy(); } const safra_tree& @@ -403,7 +403,7 @@ namespace spot const state* s = *node_it; (*child_it)->remove_node_from_children(*node_it); (*child_it)->nodes.erase(node_it++); - delete s; + s->destroy(); } else { @@ -431,7 +431,7 @@ namespace spot { const spot::state* s = *it; (*child_it)->nodes.erase(it); - delete s; + s->destroy(); } (*child_it)->remove_node_from_children(state); } @@ -679,7 +679,7 @@ namespace spot for (safra_tree::tr_cache_t::iterator j = i->second.begin(); j != i->second.end(); ++j) - delete j->second; + j->second->destroy(); // delete node; } diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc index 67078b67a..051cea4f8 100644 --- a/src/tgba/tgbasgba.cc +++ b/src/tgba/tgbasgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -48,7 +48,7 @@ namespace spot virtual ~state_sgba_proxy() { - delete s_; + s_->destroy(); } state* diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 878fbeb8a..2c728f9e1 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de // l'Epita. // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -56,7 +56,7 @@ namespace spot virtual ~state_tba_proxy() { - delete s_; + s_->destroy(); } state* @@ -204,7 +204,7 @@ namespace spot else // Yes, combine labels. { id->second |= it->current_condition(); - delete dest; + dest->destroy(); } } delete it; @@ -219,7 +219,7 @@ namespace spot const state* d = i->first.first; // Advance i before deleting d. ++i; - delete d; + d->destroy(); } } @@ -318,7 +318,7 @@ namespace spot // Advance the iterator before deleting the key. const state* s = i->first; ++i; - delete s; + s->destroy(); } } @@ -452,15 +452,15 @@ namespace spot // duplication of the initial state. // The cycle_start_ points to the right starting // point already, so just return. - delete dest; + dest->destroy(); delete it; - delete init; + init->destroy(); return; } - delete dest; + dest->destroy(); } delete it; - delete init; + init->destroy(); } // If we arrive here either because the number of acceptance diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc index 0f3865f23..1f5c8301c 100644 --- a/src/tgba/tgbaunion.cc +++ b/src/tgba/tgbaunion.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -38,8 +38,8 @@ namespace spot state_union::~state_union() { - delete left_; - delete right_; + left_->destroy(); + right_->destroy(); } int @@ -293,8 +293,8 @@ namespace spot right_acc_missing_, left_var_missing_, right_var_missing_); - delete left_init; - delete right_init; + left_init->destroy(); + right_init->destroy(); } else { diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc index 36bd41a0e..345ed775a 100644 --- a/src/tgba/wdbacomp.cc +++ b/src/tgba/wdbacomp.cc @@ -44,7 +44,8 @@ namespace spot virtual ~state_wdba_comp_proxy() { - delete s_; + if (s_) + s_->destroy(); } state* diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc index b029f858d..5001e1b67 100644 --- a/src/tgbaalgos/cutscc.cc +++ b/src/tgbaalgos/cutscc.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -72,7 +72,7 @@ namespace spot } else { - delete dst; + dst->destroy(); } tgba_explicit::transition* t = sub_a->create_transition(cur_format, dst_format); @@ -83,7 +83,7 @@ namespace spot } else { - delete dst; + dst->destroy(); } } delete sit; @@ -93,7 +93,7 @@ namespace spot // Free visited states. for (it2 = seen.begin(); it2 != seen.end(); it2++) { - delete *it2; + (*it2)->destroy(); } return sub_a; } @@ -255,7 +255,7 @@ namespace spot scc_sizes[i] = m.states_of(i).size(); state* initial_state = a->get_init_state(); unsigned init = m.scc_of_state(initial_state); - delete initial_state; + initial_state->destroy(); // Find all interesting pathes in our automaton. find_paths_sub(init, m, d, scc_sizes); @@ -272,7 +272,7 @@ namespace spot std::vector >* rec_paths = find_paths(a, m); state* initial_state = a->get_init_state(); unsigned init = m.scc_of_state(initial_state); - delete initial_state; + initial_state->destroy(); std::vector* final_sets =&(*rec_paths)[init]; if (rec_paths->empty()) { diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index bda1bcc06..b302e91ad 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -42,9 +42,9 @@ namespace spot tgba_run::~tgba_run() { for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i) - delete i->s; + i->s->destroy(); for (steps::const_iterator i = cycle.begin(); i != cycle.end(); ++i) - delete i->s; + i->s->destroy(); } tgba_run::tgba_run(const tgba_run& run) @@ -345,7 +345,7 @@ namespace spot // browse the actual outgoing transitions tgba_succ_iterator* j = a->succ_iter(s); - delete s; + s->destroy(); // FIXME: is it always legitimate to destroy s before j? for (j->first(); !j->done(); j->next()) { if (j->current_condition() != label @@ -355,7 +355,7 @@ namespace spot const state* s2 = j->current_state(); if (s2->compare(next) != 0) { - delete s2; + s2->destroy(); continue; } else @@ -386,7 +386,7 @@ namespace spot if (l == &run->cycle && i != l->begin()) seen_acc |= acc; } - delete s; + s->destroy(); assert(seen_acc == a->all_acceptance_conditions()); diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 1e7638f6b..c7a06c51b 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -1,8 +1,8 @@ +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. -// Copyright (C) 2010 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -55,7 +55,7 @@ namespace spot // Ignore unknown states ... if (!sip.first) { - delete s; + s->destroy(); return 0; } // ... as well as dead states. @@ -129,7 +129,7 @@ namespace spot if (ps != ss.end()) { // The initial state is on the cycle. - delete prefix_start; + prefix_start->destroy(); cycle_entry_point = *ps; } else @@ -198,7 +198,7 @@ namespace spot // Ignore unknown states. if (!sip.first) { - delete s; + s->destroy(); return 0; } // Stay in the final SCC. diff --git a/src/tgbaalgos/gtec/explscc.cc b/src/tgbaalgos/gtec/explscc.cc index 5e2826dfe..09a6114cd 100644 --- a/src/tgbaalgos/gtec/explscc.cc +++ b/src/tgbaalgos/gtec/explscc.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -30,7 +32,7 @@ namespace spot if (it != states.end()) { if (s != *it) - delete s; + s->destroy(); return *it; } else diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 0406f80f8..b9f4e69c0 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -376,7 +376,7 @@ namespace spot numbered_state_heap::state_index_p spi = ecs_->h->index(q->s); // ... or if it is an unknown state. if (spi.first == 0) - delete q->s; + q->s->destroy(); } dec_depth(todo.back().q.size() + 1); todo.pop_back(); diff --git a/src/tgbaalgos/gtec/nsheap.cc b/src/tgbaalgos/gtec/nsheap.cc index 4089a8c0e..0fbef7b5a 100644 --- a/src/tgbaalgos/gtec/nsheap.cc +++ b/src/tgbaalgos/gtec/nsheap.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -84,7 +86,7 @@ namespace spot // Advance the iterator before deleting the key. const state* s = i->first; ++i; - delete s; + s->destroy(); } } @@ -105,7 +107,7 @@ namespace spot res.second = i->second; if (s != i->first) - delete s; + s->destroy(); } return res; } @@ -127,7 +129,7 @@ namespace spot res.second = &i->second; if (s != i->first) - delete s; + s->destroy(); } return res; } diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 9a5e338c8..f9d216ca4 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -1,8 +1,8 @@ +// Copyright (C) 2008, 2010, 2011 Laboratoire de recherche et +// développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. -// Copyright (C) 2008, 2010 Laboratoire de recherche et développement -// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -88,7 +88,7 @@ namespace spot // Advance the iterator before deleting the "key" pointer. const state* ptr = s->first; ++s; - delete ptr; + ptr->destroy(); } } @@ -156,7 +156,7 @@ namespace spot << std::endl; } - delete s_prime; + s_prime->destroy(); } } set_states(h.size()); @@ -355,11 +355,11 @@ namespace spot // Or it is still on the stack but not in the SCC || data.stack[j->second].lowlink < scc_root) { - delete s; + s->destroy(); return 0; } r->inc_ars_cycle_states(); - delete s; + s->destroy(); return j->first; } diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index ee75b7512..0a055aad6 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de recherche et développement de +// l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -292,7 +294,7 @@ namespace spot // to visit white states either if a cycle can be missed // with bit-state hashing search. trace << " It is white, pop it" << std::endl; - delete s_prime; + s_prime->destroy(); } else if (c.get_color() == BLUE) { @@ -463,7 +465,7 @@ namespace spot // Advance the iterator before deleting the "key" pointer. const state* ptr = s->first; ++s; - delete ptr; + ptr->destroy(); } } @@ -474,7 +476,7 @@ namespace spot return color_ref(0); if (s!=it->first) { - delete s; + s->destroy(); s = it->first; } return color_ref(&(it->second)); @@ -564,7 +566,7 @@ namespace spot void pop_notify(const state* s) const { - delete s; + s->destroy(); } bool has_been_visited(const state* s) const diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 16dcfb9a2..1cad49077 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -105,7 +105,7 @@ namespace spot seen->insert(dst); } else - delete dst; + dst->destroy(); } delete sit; } @@ -151,7 +151,7 @@ namespace spot { const state* dst = succit->current_state(); unsigned dst_num = state_num[dst]; - delete dst; + dst->destroy(); trs* t = res->create_transition(src_num, dst_num); res->add_conditions(t, succit->current_condition()); if (accepting) @@ -163,7 +163,7 @@ namespace spot res->merge_transitions(); const state* init_state = a->get_init_state(); unsigned init_num = state_num[init_state]; - delete init_state; + init_state->destroy(); res->set_init_state(init_num); return res; } @@ -190,7 +190,7 @@ namespace spot { hash_set::const_iterator old = i; ++i; - delete *old; + (*old)->destroy(); } } @@ -205,7 +205,7 @@ namespace spot } else { - delete s; + s->destroy(); s = *i; } // Ignore states outside SCC #n. @@ -250,11 +250,11 @@ namespace spot for (n = 1, i = loop.begin(); n < loop_size; ++n, ++i) { loop_a.create_transition(n - 1, n)->condition = i->label; - delete i->s; + i->s->destroy(); } assert(i != loop.end()); loop_a.create_transition(n - 1, 0)->condition = i->label; - delete i->s; + i->s->destroy(); assert(++i == loop.end()); const state* loop_a_init = loop_a.get_init_state(); @@ -284,7 +284,7 @@ namespace spot delete p; } - delete loop_a_init; + loop_a_init->destroy(); return accepting; } @@ -383,7 +383,7 @@ namespace spot { const state* dst = si->current_state(); unsigned dst_set = state_set_map[dst]; - delete dst; + dst->destroy(); f |= (bdd_ithvar(dst_set) & si->current_condition()); } delete si; @@ -480,7 +480,7 @@ namespace spot for (hit = state_set_map.begin(); hit != state_set_map.end();) { hash_map::iterator old = hit++; - delete old->first; + old->first->destroy(); } std::list::iterator it; for (it = done.begin(); it != done.end(); ++it) diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index f2b12fa46..07b6cb87b 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de recherche et développement de +// l'Epita (LRDE). // Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -190,7 +192,7 @@ namespace spot (void) b; } - delete start; + start->destroy(); assert(!acc_trans.empty()); @@ -205,8 +207,8 @@ namespace spot for (typename accepting_transitions_list::const_iterator i = acc_trans.begin(); i != acc_trans.end(); ++i) { - delete i->source; - delete i->dest; + i->source->destroy(); + i->dest->destroy(); } return run; @@ -240,13 +242,13 @@ namespace spot { const state* s = *i; ++i; - delete s; + s->destroy(); } for (state_set::iterator i = dead.begin(); i != dead.end();) { const state* s = *i; ++i; - delete s; + s->destroy(); } } @@ -282,7 +284,7 @@ namespace spot if (dead.find(s_prime) != dead.end()) { ndfsr_trace << " it is dead, pop it" << std::endl; - delete s_prime; + s_prime->destroy(); } else if (seen.find(s_prime) == seen.end()) { @@ -309,23 +311,23 @@ namespace spot if (covered_acc == a_->all_acceptance_conditions()) { clean(st1, seen, dead); - delete s_prime; + s_prime->destroy(); return true; } } - delete s_prime; + s_prime->destroy(); } else { ndfsr_trace << " already seen, pop it" << std::endl; - delete s_prime; + s_prime->destroy(); } } else { ndfsr_trace << " not seen during the search, pop it" << std::endl; - delete s_prime; + s_prime->destroy(); } } else @@ -384,7 +386,7 @@ namespace spot { const state* ptr = *i; ++i; - delete ptr; + ptr->destroy(); } } @@ -403,7 +405,7 @@ namespace spot || seen.find(s) != seen.end() || dead.find(s) != dead.end()) { - delete s; + s->destroy(); return 0; } ars->inc_ars_cycle_states(); @@ -477,7 +479,7 @@ namespace spot { const state* ptr = *i; ++i; - delete ptr; + ptr->destroy(); } } @@ -499,7 +501,7 @@ namespace spot ndfsr_trace << " not visited" << std::endl; else ndfsr_trace << " already seen" << std::endl; - delete s; + s->destroy(); return 0; } ndfsr_trace << " OK" << std::endl; @@ -634,7 +636,7 @@ namespace spot if (ps != target.end()) { // The initial state is on the cycle. - delete prefix_start; + prefix_start->destroy(); cycle_entry_point = ps->first->clone(); } else @@ -653,7 +655,7 @@ namespace spot && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) continue; assert(cycle_ep_it != run->cycle.end()); - delete cycle_entry_point; + cycle_entry_point->destroy(); // Now shift the cycle so it starts on cycle_entry_point. run->cycle.splice(run->cycle.end(), run->cycle, diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index beb7a069b..9ea937827 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -71,7 +71,7 @@ namespace spot os_ << " skip" << std::endl; } os_ << "}" << std::endl; - delete init_; + init_->destroy(); } bool @@ -110,7 +110,7 @@ namespace spot label = "accept_S" + ns; else label = "accept_all"; - delete current; + current->destroy(); } delete it; } @@ -156,7 +156,7 @@ namespace spot os_ << " if" << std::endl; fi_needed_ = true; } - delete current; + current->destroy(); } delete it; } @@ -174,7 +174,7 @@ namespace spot f->destroy(); state* current = si->current_state(); os_ << ") -> goto " << get_state_label(current, out) << std::endl; - delete current; + current->destroy(); } } diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 96add97d3..b1142351a 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -47,7 +47,7 @@ namespace spot // Advance the iterator before deleting the key. const state* s = *i; ++i; - delete s; + s->destroy(); } } @@ -63,7 +63,7 @@ namespace spot state_set::const_iterator i = states.find(s); if (i != states.end()) { - delete s; + s->destroy(); s = *i; } else diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc index 8d64d980f..03880dcc6 100644 --- a/src/tgbaalgos/reachiter.cc +++ b/src/tgbaalgos/reachiter.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -42,7 +42,7 @@ namespace spot // Advance the iterator before deleting the "key" pointer. const state* ptr = s->first; ++s; - delete ptr; + ptr->destroy(); } } @@ -80,7 +80,7 @@ namespace spot { if (ws) process_link(t, tn, s->first, s->second, si); - delete current; + current->destroy(); } } delete si; diff --git a/src/tgbaalgos/reducerun.cc b/src/tgbaalgos/reducerun.cc index 9ab94c267..9e652281d 100644 --- a/src/tgbaalgos/reducerun.cc +++ b/src/tgbaalgos/reducerun.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -46,7 +48,7 @@ namespace spot { const state* ptr = *i; ++i; - delete ptr; + ptr->destroy(); } } @@ -70,7 +72,7 @@ namespace spot seen.insert(s); else { - delete s; + s->destroy(); s = *i; } return s; @@ -162,7 +164,7 @@ namespace spot if (ps != ss.end()) { // The initial state is on the cycle. - delete prefix_start; + prefix_start->destroy(); cycle_entry_point = *ps; } else diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index f818954c4..e9c5ece0b 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -469,7 +469,7 @@ namespace spot else delete p; } - delete s; + s->destroy(); } delete si; } @@ -513,7 +513,7 @@ namespace spot (*j)->add_succ(*i); ++nb_ds; } - delete s; + s->destroy(); } delete si; } @@ -534,7 +534,7 @@ namespace spot (*i)->add_succ(*j); ++nb_sd; } - delete s; + s->destroy(); } delete si; } @@ -656,7 +656,7 @@ namespace spot { const state* ptr = j->first; ++j; - delete ptr; + ptr->destroy(); } } diff --git a/src/tgbaalgos/reductgba_sim_del.cc b/src/tgbaalgos/reductgba_sim_del.cc index ec9b1ceda..38c837f7e 100644 --- a/src/tgbaalgos/reductgba_sim_del.cc +++ b/src/tgbaalgos/reductgba_sim_del.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -410,7 +410,7 @@ namespace spot s = si->current_state(); if (s->compare(*i1) == 0) { - delete s; + s->destroy(); duplicator_node_delayed* dn = add_duplicator_node_delayed(*i1, sn->get_duplicator_node(), @@ -426,7 +426,7 @@ namespace spot build_recurse_successor_duplicator(dn, sn, os2); } else - delete s; + s->destroy(); } } @@ -463,7 +463,7 @@ namespace spot if (s->compare(*i1) == 0) { - delete s; + s->destroy(); spoiler_node_delayed* sn_n = add_spoiler_node_delayed(dn->get_spoiler_node(), *i1, @@ -478,7 +478,7 @@ namespace spot build_recurse_successor_spoiler(sn_n, os2); } else - delete s; + s->destroy(); } } @@ -668,7 +668,7 @@ namespace spot { const state* ptr = j->first; ++j; - delete ptr; + ptr->destroy(); } } diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index 819c28224..4d9b297da 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/src/tgbaalgos/replayrun.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -80,7 +82,7 @@ namespace spot << a->format_state(i->s) << std::endl << "does not match initial state of automata: " << a->format_state(s) << std::endl; - delete s; + s->destroy(); return false; } @@ -98,7 +100,7 @@ namespace spot for (d = o->second.begin(); d != o->second.end(); ++d) msg << " == " << *d; o->second.insert(serial); - delete s; + s->destroy(); s = o->first; } else @@ -142,7 +144,7 @@ namespace spot // When not debugging, S is not used as key in SEEN, so we can // delete it right now. if (!debug) - delete s; + s->destroy(); for (j->first(); !j->done(); j->next()) { if (j->current_condition() != label @@ -152,7 +154,7 @@ namespace spot const state* s2 = j->current_state(); if (s2->compare(next)) { - delete s2; + s2->destroy(); continue; } else @@ -185,11 +187,11 @@ namespace spot << bdd_format_accset(a->get_dict(), j->current_acceptance_conditions()) << " going to " << a->format_state(s2) << std::endl; - delete s2; + s2->destroy(); } } delete j; - delete s; + s->destroy(); return false; } if (debug) @@ -232,7 +234,7 @@ namespace spot } } } - delete s; + s->destroy(); if (all_acc != expected_all_acc) { if (debug) @@ -251,7 +253,7 @@ namespace spot // Advance the iterator before deleting the "key" pointer. const state* ptr = o->first; ++o; - delete ptr; + ptr->destroy(); } return true; diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 42d86d15e..ca4786f81 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -58,7 +58,7 @@ namespace spot bdd cond = it->current_condition(); it->next(); result = (!dest->compare(s)) && it->done() && (cond == bddtrue); - delete dest; + dest->destroy(); delete it; } diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index b87a36eff..9812b5b42 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -1,6 +1,8 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2011 Laboratoire de Recherche et Développement de +// l'Epita (LRDE) +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -59,7 +61,7 @@ namespace spot escape_str(os_, bdd_format_formula(d, si->current_condition())); os_ << "\","; print_acc(si->current_acceptance_conditions()) << ";" << std::endl; - delete dest; + dest->destroy(); } } diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 7279bb7a2..bbfe5419f 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -54,7 +54,7 @@ namespace spot // Advance the iterator before deleting the key. const state* s = i->first; ++i; - delete s; + s->destroy(); } } @@ -63,7 +63,7 @@ namespace spot { state* in = aut_->get_init_state(); int val = scc_of_state(in); - delete in; + in->destroy(); return val; } @@ -231,7 +231,7 @@ namespace spot } // If we know the state, reuse the previous object. - delete dest; + dest->destroy(); dest = spi->first; // Have we reached a maximal SCC? diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index 5e144ee35..63048f0ab 100644 --- a/src/tgbaalgos/se05.cc +++ b/src/tgbaalgos/se05.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -292,7 +294,7 @@ namespace spot // collision, this property does not hold. trace << " It is white (due to collision), pop it" << std::endl; - delete s_prime; + s_prime->destroy(); } else if (c.get_color() == RED) { @@ -499,14 +501,14 @@ namespace spot { const state* ptr = *sc; ++sc; - delete ptr; + ptr->destroy(); } hash_type::const_iterator s = h.begin(); while (s != h.end()) { const state* ptr = s->first; ++s; - delete ptr; + ptr->destroy(); } } @@ -520,14 +522,14 @@ namespace spot return color_ref(0); // white state if (s!=it->first) { - delete s; + s->destroy(); s = it->first; } return color_ref(&(it->second)); // blue or red state } if (s!=*ic) { - delete s; + s->destroy(); s = *ic; } return color_ref(&h, &hc, *ic); // cyan state @@ -651,7 +653,7 @@ namespace spot void pop_notify(const state* s) const { - delete s; + s->destroy(); } bool has_been_visited(const state* s) const diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 503a2fe20..fd633bc54 100644 --- a/src/tgbaalgos/tau03.cc +++ b/src/tgbaalgos/tau03.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -251,7 +253,7 @@ namespace spot if (c_prime.is_white()) { trace << " It is white, pop it" << std::endl; - delete s_prime; + s_prime->destroy(); } else if ((c_prime.get_acc() & acu) != acu) { @@ -328,7 +330,7 @@ namespace spot // Advance the iterator before deleting the "key" pointer. const state* ptr = s->first; ++s; - delete ptr; + ptr->destroy(); } } @@ -339,7 +341,7 @@ namespace spot return color_ref(0, 0); if (s!=it->first) { - delete s; + s->destroy(); s = it->first; } return color_ref(&(it->second.first), &(it->second.second)); diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 76c1a7d4d..d5be226c8 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -1,3 +1,5 @@ +// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -340,7 +342,7 @@ namespace spot if (c_prime.is_white()) { trace << " It is white, pop it" << std::endl; - delete s_prime; + s_prime->destroy(); continue; } else if (c_prime.get_color() == CYAN && @@ -492,14 +494,14 @@ namespace spot { const state* ptr = sc->first; ++sc; - delete ptr; + ptr->destroy(); } hash_type::const_iterator s = h.begin(); while (s != h.end()) { const state* ptr = s->first; ++s; - delete ptr; + ptr->destroy(); } } @@ -514,7 +516,7 @@ namespace spot return color_ref(0, 0); if (s!=it->first) { - delete s; + s->destroy(); s = it->first; } // blue or red state @@ -522,7 +524,7 @@ namespace spot } if (s!=ic->first) { - delete s; + s->destroy(); s = ic->first; } // cyan state