From cfbd31384f28e112ba15eec2d215724d04ef019c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 28 Jun 2013 18:39:17 +0200 Subject: [PATCH] Use -fvisibility=hidden in src/ta/ and src/taalgos/. * src/ta/Makefile.am, src/taalgos/Makefile.am: Use $(VISIBILITY_CXXFLAGS). * src/ta/ta.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/dotty.hh, src/taalgos/emptinessta.hh, src/taalgos/minimize.hh, src/taalgos/reachiter.hh, src/taalgos/statessetbuilder.hh, src/taalgos/stats.hh, src/taalgos/tgba2ta.hh: Add SPOT_API in front of all public symbols. --- src/ta/Makefile.am | 6 +++--- src/ta/ta.hh | 9 +++++---- src/ta/taexplicit.hh | 6 +++--- src/ta/taproduct.hh | 24 ++++++++++-------------- src/ta/tgta.hh | 3 ++- src/ta/tgtaexplicit.hh | 5 +++-- src/ta/tgtaproduct.hh | 9 +++------ src/taalgos/Makefile.am | 6 +++--- src/taalgos/dotty.hh | 7 ++++--- src/taalgos/emptinessta.hh | 2 +- src/taalgos/minimize.hh | 8 ++++---- src/taalgos/reachiter.hh | 8 +++++--- src/taalgos/statessetbuilder.hh | 5 +++-- src/taalgos/stats.hh | 10 ++++------ src/taalgos/tgba2ta.hh | 8 ++++---- 15 files changed, 57 insertions(+), 59 deletions(-) diff --git a/src/ta/Makefile.am b/src/ta/Makefile.am index b22efcb86..ab2a121a3 100644 --- a/src/ta/Makefile.am +++ b/src/ta/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -18,7 +18,7 @@ ## along with this program. If not, see . AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS) tadir = $(pkgincludedir)/ta diff --git a/src/ta/ta.hh b/src/ta/ta.hh index 3a1066baa..eebf71e84 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et +// Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -50,7 +51,7 @@ namespace spot /// The Testing Automata (TA) were introduced by /// Henri Hansen, Wojciech Penczek and Antti Valmari /// in "Stuttering-insensitive automata for on-the-fly detection of livelock - /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in + /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in /// Theoretical Computer Science.Elsevier. /// /// While a TGBA automaton observes the value of the atomic propositions, the @@ -74,7 +75,7 @@ namespace spot /// obtained by querying the iterator over the successors of /// a state. - class ta + class SPOT_API ta { public: diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index a6516b987..6b45a778f 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -38,7 +38,7 @@ namespace spot /// Explicit representation of a spot::ta. /// \ingroup ta_representation - class ta_explicit : public ta + class SPOT_API ta_explicit : public ta { public: ta_explicit(const tgba* tgba, bdd all_acceptance_conditions, @@ -146,7 +146,7 @@ namespace spot /// states used by spot::ta_explicit. /// \ingroup ta_representation - class state_ta_explicit : public spot::state + class SPOT_API state_ta_explicit : public spot::state { #ifndef SWIG public: @@ -241,7 +241,7 @@ namespace spot }; /// Successor iterators used by spot::ta_explicit. - class ta_explicit_succ_iterator : public ta_succ_iterator + class SPOT_API ta_explicit_succ_iterator : public ta_succ_iterator { public: ta_explicit_succ_iterator(const state_ta_explicit* s); diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh index b1352a84b..311e804e4 100644 --- a/src/ta/taproduct.hh +++ b/src/ta/taproduct.hh @@ -31,7 +31,7 @@ namespace spot /// /// This state is in fact a pair of state: the state from the TA /// automaton and that of Kripke structure. - class state_ta_product : public state + class SPOT_API state_ta_product : public state { public: /// \brief Constructor @@ -73,7 +73,7 @@ namespace spot }; /// \brief Iterate over the successors of a product computed on the fly. - class ta_succ_iterator_product : public ta_succ_iterator + class SPOT_API ta_succ_iterator_product : public ta_succ_iterator { public: ta_succ_iterator_product(const state_ta_product* s, const ta* t, @@ -135,7 +135,7 @@ namespace spot /// \ingroup ta_emptiness_check /// \brief A lazy product between a Testing automaton and a Kripke structure. /// (States are computed on the fly.) - class ta_product : public ta + class SPOT_API ta_product: public ta { public: /// \brief Constructor. @@ -208,21 +208,17 @@ namespace spot }; - class ta_succ_iterator_product_by_changeset : public ta_succ_iterator_product + class SPOT_API ta_succ_iterator_product_by_changeset : + public ta_succ_iterator_product { public: ta_succ_iterator_product_by_changeset(const state_ta_product* s, - const ta* t, const kripke* k, bdd changeset); - - - - /// \brief Move to the next successor in the kripke structure - void - next_kripke_dest(); - - - }; + const ta* t, const kripke* k, + bdd changeset); + /// \brief Move to the next successor in the Kripke structure + void next_kripke_dest(); + }; } diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh index 5114f62b6..20446a28d 100644 --- a/src/ta/tgta.hh +++ b/src/ta/tgta.hh @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // @@ -57,7 +58,7 @@ namespace spot /// a state. - class tgta : public tgba + class SPOT_API tgta : public tgba { protected: diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index a9374e5f6..34a66b7b3 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -1,4 +1,5 @@ -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -34,7 +35,7 @@ namespace spot /// Explicit representation of a spot::tgta. /// \ingroup ta_representation - class tgta_explicit : public tgta + class SPOT_API tgta_explicit : public tgta { public: tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions, diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index 33860213c..58aa364af 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -1,9 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2006 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. // @@ -33,7 +30,7 @@ namespace spot { /// \brief A lazy product. (States are computed on the fly.) - class tgta_product : public tgba_product + class SPOT_API tgta_product : public tgba_product { public: tgta_product(const kripke* left, const tgta* right); @@ -47,7 +44,7 @@ namespace spot }; /// \brief Iterate over the successors of a product computed on the fly. - class tgta_succ_iterator_product : public tgba_succ_iterator + class SPOT_API tgta_succ_iterator_product : public tgba_succ_iterator { public: tgta_succ_iterator_product(const state_product* s, const kripke* k, diff --git a/src/taalgos/Makefile.am b/src/taalgos/Makefile.am index 465ecff90..750bcbc25 100644 --- a/src/taalgos/Makefile.am +++ b/src/taalgos/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library.et Marie Curie. ## @@ -19,7 +19,7 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS) taalgosdir = $(pkgincludedir)/taalgos diff --git a/src/taalgos/dotty.hh b/src/taalgos/dotty.hh index 33726bc36..8629239e8 100644 --- a/src/taalgos/dotty.hh +++ b/src/taalgos/dotty.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -26,7 +27,7 @@ namespace spot { class ta; - std::ostream& + SPOT_API std::ostream& dotty_reachable(std::ostream& os, const ta* a); } diff --git a/src/taalgos/emptinessta.hh b/src/taalgos/emptinessta.hh index 6c754b5bb..733b93da8 100644 --- a/src/taalgos/emptinessta.hh +++ b/src/taalgos/emptinessta.hh @@ -85,7 +85,7 @@ namespace spot /// between a TA and a Kripke structure /// /// See the paper cited above. - class ta_check : public ec_statistics + class SPOT_API ta_check : public ec_statistics { public: ta_check(const ta_product* a, option_map o = option_map()); diff --git a/src/taalgos/minimize.hh b/src/taalgos/minimize.hh index 14e59fe03..2d9a81814 100644 --- a/src/taalgos/minimize.hh +++ b/src/taalgos/minimize.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -56,7 +56,7 @@ namespace spot \endverbatim */ /// /// \param ta_ the TA automaton to convert into a simplified TA - ta* + SPOT_API ta* minimize_ta(const ta* ta_); @@ -70,7 +70,7 @@ namespace spot /// the acceptance conditions of the outgoing transitions. /// /// \param tgta_ the TGTA automaton to convert into a simplified TGTA - tgta_explicit* + SPOT_API tgta_explicit* minimize_tgta(const tgta_explicit* tgta_); /// @} diff --git a/src/taalgos/reachiter.hh b/src/taalgos/reachiter.hh index e8d77b486..f1a428056 100644 --- a/src/taalgos/reachiter.hh +++ b/src/taalgos/reachiter.hh @@ -29,7 +29,7 @@ namespace spot { /// \ingroup ta_generic /// \brief Iterate over all reachable states of a spot::ta. - class ta_reachable_iterator + class SPOT_API ta_reachable_iterator { public: ta_reachable_iterator(const ta* a); @@ -97,7 +97,8 @@ namespace spot /// \ingroup ta_generic /// \brief An implementation of spot::ta_reachable_iterator that browses /// states depth first. - class ta_reachable_iterator_depth_first : public ta_reachable_iterator + class SPOT_API ta_reachable_iterator_depth_first + : public ta_reachable_iterator { public: ta_reachable_iterator_depth_first(const ta* a); @@ -114,7 +115,8 @@ namespace spot /// \ingroup ta_generic /// \brief An implementation of spot::ta_reachable_iterator that browses /// states breadth first. - class ta_reachable_iterator_breadth_first : public ta_reachable_iterator + class SPOT_API ta_reachable_iterator_breadth_first + : public ta_reachable_iterator { public: ta_reachable_iterator_breadth_first(const ta* a); diff --git a/src/taalgos/statessetbuilder.hh b/src/taalgos/statessetbuilder.hh index aebd7e2d4..2bdd215e6 100644 --- a/src/taalgos/statessetbuilder.hh +++ b/src/taalgos/statessetbuilder.hh @@ -1,4 +1,5 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,7 +26,7 @@ namespace spot { /// \brief Compute states set for an automaton. - std::set get_states_set(const ta* t); + SPOT_API std::set get_states_set(const ta* t); /// @} } diff --git a/src/taalgos/stats.hh b/src/taalgos/stats.hh index d3fd305d6..3c19ca3f5 100644 --- a/src/taalgos/stats.hh +++ b/src/taalgos/stats.hh @@ -1,8 +1,6 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013 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. // // This file is part of Spot, a model checking library. // @@ -31,7 +29,7 @@ namespace spot /// \addtogroup ta_misc /// @{ - struct ta_statistics + struct SPOT_API ta_statistics { unsigned transitions; unsigned states; @@ -41,7 +39,7 @@ namespace spot }; /// \brief Compute statistics for an automaton. - ta_statistics stats_reachable(const ta* t); + SPOT_API ta_statistics stats_reachable(const ta* t); /// @} } diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh index 8ad468034..babc69e2b 100644 --- a/src/taalgos/tgba2ta.hh +++ b/src/taalgos/tgba2ta.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -79,7 +79,7 @@ namespace spot /// /// \return A spot::ta_explicit that recognizes the same language as the /// TGBA \a tgba_to_convert. - ta_explicit* + SPOT_API ta_explicit* tgba_to_ta(const tgba* tgba_to_convert, bdd atomic_propositions_set, bool degeneralized = true, bool artificial_initial_state_mode = true, bool single_pass_emptiness_check = false, @@ -94,7 +94,7 @@ namespace spot /// /// \return A spot::tgta_explicit (spot::tgta) that recognizes the same /// language as the TGBA \a tgba_to_convert. - tgta_explicit* + SPOT_API tgta_explicit* tgba_to_tgta(const tgba* tgba_to_convert, bdd atomic_propositions_set); }