From 1fa1621a6bd573ee8e1b061e5d17b237af1ccb4e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 7 Oct 2010 15:17:18 +0200 Subject: [PATCH] Hide the safra_tree_automaton type from the public interface. We do that because the declaration of this type, which is local to src/tgba/tgbasafracomplement.cc has a member in an anonymous namespace, and some versions of g++-4.2 issue a very annoying warning about this legitimate code. See Bug 29365 on GCC's Bugzilla. Report by Silien Hong . * src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not forward declare. (tgba_safra_complement): Use void* instead of safra_tree_automaton*. * src/tgba/tgbasafracomplement.cc: static_cast void* to safra_tree_automaton* anywhere needed. --- ChangeLog | 17 +++++++ THANKS | 1 + src/tgba/tgbasafracomplement.cc | 78 ++++++++++++++++----------------- src/tgba/tgbasafracomplement.hh | 15 +++---- 4 files changed, 63 insertions(+), 48 deletions(-) diff --git a/ChangeLog b/ChangeLog index 7173a79c7..eafcd7ac7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2010-10-07 Alexandre Duret-Lutz + + Hide the safra_tree_automaton type from the public interface. + + We do that because the declaration of this type, which is local to + src/tgba/tgbasafracomplement.cc has a member in an anonymous + namespace, and some versions of g++-4.2 issue a very annoying + warning about this legitimate code. See Bug 29365 on GCC's + Bugzilla. Report by Silien Hong . + + * src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not + forward declare. + (tgba_safra_complement): Use void* instead of + safra_tree_automaton*. + * src/tgba/tgbasafracomplement.cc: static_cast void* to + safra_tree_automaton* anywhere needed. + 2010-05-20 Alexandre Duret-Lutz Fix the --enable-optimizations check. diff --git a/THANKS b/THANKS index a5e245bb2..ddcbe09f8 100644 --- a/THANKS +++ b/THANKS @@ -6,4 +6,5 @@ Jean-Michel Couvreur Jean-Michel Ilié Kristin Y. Rozier Rüdiger Ehlers +Silien Hong Yann Thierry-Mieg diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index c465dc810..4464ae38e 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -50,32 +50,29 @@ namespace spot operator()(const safra_tree* left, const safra_tree* right) const; }; - } // anonymous. - /// \brief Automaton with Safra's tree as states. - struct safra_tree_automaton - { - safra_tree_automaton(const tgba* sba); - ~safra_tree_automaton(); - typedef std::map transition_list; - typedef - std::map - automaton_t; - automaton_t automaton; + /// \brief Automaton with Safra's tree as states. + struct safra_tree_automaton + { + safra_tree_automaton(const tgba* sba); + ~safra_tree_automaton(); + typedef std::map transition_list; + typedef + std::map + automaton_t; + automaton_t automaton; - /// \brief The number of acceptance pairs of this Rabin (Streett) - /// automaton. - int get_nb_acceptance_pairs() const; - safra_tree* get_initial_state() const; - void set_initial_state(safra_tree* s); - private: - mutable int max_nb_pairs_; - safra_tree* initial_state; - const tgba* a_; - }; + /// \brief The number of acceptance pairs of this Rabin (Streett) + /// automaton. + int get_nb_acceptance_pairs() const; + safra_tree* get_initial_state() const; + void set_initial_state(safra_tree* s); + private: + mutable int max_nb_pairs_; + safra_tree* initial_state; + const tgba* a_; + }; - namespace - { /// \brief A Safra tree, used as state during the determinization /// of a Büchi automaton /// @@ -1120,7 +1117,8 @@ namespace spot #endif #if TRANSFORM_TO_TGBA - unsigned nb_acc = safra_->get_nb_acceptance_pairs(); + unsigned nb_acc = + static_cast(safra_)->get_nb_acceptance_pairs(); all_acceptance_cond_ = bddfalse; neg_acceptance_cond_ = bddtrue; acceptance_cond_vec_.reserve(nb_acc); @@ -1138,15 +1136,15 @@ namespace spot tgba_safra_complement::~tgba_safra_complement() { get_dict()->unregister_all_my_variables(safra_); - delete safra_; + delete static_cast(safra_); } state* tgba_safra_complement::get_init_state() const { - bitset_t empty(safra_->get_nb_acceptance_pairs()); - return new state_complement(empty, empty, safra_->get_initial_state(), - false); + safra_tree_automaton* a = static_cast(safra_); + bitset_t empty(a->get_nb_acceptance_pairs()); + return new state_complement(empty, empty, a->get_initial_state(), false); } @@ -1189,19 +1187,20 @@ namespace spot const state* /* = 0 */, const tgba* /* = 0 */) const { + const safra_tree_automaton* a = static_cast(safra_); const state_complement* s = dynamic_cast(local_state); assert(s); safra_tree_automaton::automaton_t::const_iterator tr = - safra_->automaton.find(const_cast(s->get_safra())); + a->automaton.find(const_cast(s->get_safra())); typedef safra_tree_automaton::transition_list::const_iterator trans_iter; - if (tr != safra_->automaton.end()) + if (tr != a->automaton.end()) { bdd condition = bddfalse; tgba_safra_complement_succ_iterator::succ_list_t succ_list; - int nb_acceptance_pairs = safra_->get_nb_acceptance_pairs(); + int nb_acceptance_pairs = a->get_nb_acceptance_pairs(); bitset_t e(nb_acceptance_pairs); if (!s->get_use_bitset()) // if \delta'(q, a) @@ -1311,14 +1310,14 @@ namespace spot bdd tgba_safra_complement::compute_support_conditions(const state* state) const { + const safra_tree_automaton* a = static_cast(safra_); const state_complement* s = dynamic_cast(state); assert(s); typedef safra_tree_automaton::automaton_t::const_iterator auto_it; typedef safra_tree_automaton::transition_list::const_iterator trans_it; - auto_it node(safra_-> - automaton.find(const_cast(s->get_safra()))); + auto_it node(a->automaton.find(const_cast(s->get_safra()))); - if (node == safra_->automaton.end()) + if (node == a->automaton.end()) return bddtrue; bdd res = bddtrue; @@ -1331,14 +1330,14 @@ namespace spot bdd tgba_safra_complement::compute_support_variables(const state* state) const { + const safra_tree_automaton* a = static_cast(safra_); const state_complement* s = dynamic_cast(state); assert(s); typedef safra_tree_automaton::automaton_t::const_iterator auto_it; typedef safra_tree_automaton::transition_list::const_iterator trans_it; - auto_it node(safra_-> - automaton.find(const_cast(s->get_safra()))); + auto_it node(a->automaton.find(const_cast(s->get_safra()))); - if (node == safra_->automaton.end()) + if (node == a->automaton.end()) return bddtrue; bdd res = bddtrue; @@ -1352,6 +1351,7 @@ namespace spot ////////////////////////////// void display_safra(const tgba_safra_complement* a) { - test::print_safra_automaton(a->get_safra()); + test::print_safra_automaton(static_cast + (a->get_safra())); } } diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index 8ed60ab26..5f6b41374 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -31,8 +31,6 @@ namespace spot { - struct safra_tree_automaton; - /// \brief Build a complemented automaton. /// \ingroup tgba_on_the_fly_algorithms /// @@ -56,11 +54,6 @@ namespace spot tgba_safra_complement(const tgba* a); virtual ~tgba_safra_complement(); - safra_tree_automaton* get_safra() const - { - return safra_; - } - // tgba interface. virtual state* get_init_state() const; virtual tgba_succ_iterator* @@ -73,12 +66,17 @@ namespace spot virtual bdd all_acceptance_conditions() const; virtual bdd neg_acceptance_conditions() const; + void* get_safra() const + { + return safra_; + } + protected: virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_variables(const state* state) const; private: const tgba* automaton_; - safra_tree_automaton* safra_; + void* safra_; #if TRANSFORM_TO_TBA bdd the_acceptance_cond_; #endif @@ -88,7 +86,6 @@ namespace spot // Map to i the i-th acceptance condition of the final automaton. std::vector acceptance_cond_vec_; #endif - }; /// \brief Produce a dot output of the Safra automaton associated