diff --git a/src/kripke/Makefile.am b/src/kripke/Makefile.am
index 05a9bd1f6..3a10ef203 100644
--- a/src/kripke/Makefile.am
+++ b/src/kripke/Makefile.am
@@ -1,5 +1,6 @@
-## Copyright (C) 2009, 2011 Laboratoire de Recherche et Developpement
-## de l'Epita (LRDE).
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
+## Developpement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -17,7 +18,7 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
-AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
 
 kripkedir = $(pkgincludedir)/kripke
 
diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh
index 22e3656e4..59b8d9de6 100644
--- a/src/kripke/fairkripke.hh
+++ b/src/kripke/fairkripke.hh
@@ -1,4 +1,6 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et
+// Developpement de l'Epita
 //
 // This file is part of Spot, a model checking library.
 //
@@ -44,7 +46,7 @@ namespace spot
   ///
   /// This class implements fair_kripke_succ_iterator::current_condition(),
   /// and fair_kripke_succ_iterator::current_acceptance_conditions().
-  class fair_kripke_succ_iterator : public tgba_succ_iterator
+  class SPOT_API fair_kripke_succ_iterator : public tgba_succ_iterator
   {
   public:
     /// \brief Constructor
@@ -86,7 +88,7 @@ namespace spot
   /// class and need not be defined.
   ///
   /// See also spot::fair_kripke_succ_iterator.
-  class fair_kripke : public tgba
+  class SPOT_API fair_kripke : public tgba
   {
   public:
     /// \brief The condition that label the state \a s.
diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh
index b9c08f752..608b50891 100644
--- a/src/kripke/kripke.hh
+++ b/src/kripke/kripke.hh
@@ -1,4 +1,6 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et
+// Developpement de l'Epita
 //
 // This file is part of Spot, a model checking library.
 //
@@ -39,7 +41,7 @@ namespace spot
   ///
   /// This class implements kripke_succ_iterator::current_condition(),
   /// and kripke_succ_iterator::current_acceptance_conditions().
-  class kripke_succ_iterator : public tgba_succ_iterator
+  class SPOT_API kripke_succ_iterator : public tgba_succ_iterator
   {
   public:
     /// \brief Constructor
@@ -78,7 +80,7 @@ namespace spot
   /// need not be defined.
   ///
   /// See also spot::kripke_succ_iterator.
-  class kripke: public fair_kripke
+  class SPOT_API kripke: public fair_kripke
   {
   public:
     virtual ~kripke();
diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh
index 7d4e26810..c76f92a33 100644
--- a/src/kripke/kripkeexplicit.hh
+++ b/src/kripke/kripkeexplicit.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE)
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -29,7 +29,7 @@
 namespace spot
 {
   /// \brief Concrete class for kripke states.
-  class state_kripke : public state
+  class SPOT_API state_kripke : public state
   {
     friend class kripke_explicit;
     friend class kripke_explicit_succ_iterator;
@@ -90,7 +90,7 @@ namespace spot
 
   /// \class kripke_explicit_succ_iterator
   /// \brief Implement iterator pattern on successor of a state_kripke.
-  class kripke_explicit_succ_iterator : public kripke_succ_iterator
+  class SPOT_API kripke_explicit_succ_iterator : public kripke_succ_iterator
   {
   public:
     kripke_explicit_succ_iterator(const state_kripke*, bdd);
@@ -111,7 +111,7 @@ namespace spot
 
   /// \class kripke_explicit
   /// \brief Kripke Structure.
-  class kripke_explicit : public kripke
+  class SPOT_API kripke_explicit : public kripke
   {
   public:
     kripke_explicit(bdd_dict*);
@@ -183,4 +183,4 @@ namespace spot
     std::map<const state_kripke*, std::string> sn_nodes_;
   };
 }
-#endif /* !SPOT_KRIPKEEXPLICIT_HH_ */
+#endif // SPOT_KRIPKE_KRIPKEEXPLICIT_HH
diff --git a/src/kripke/kripkeprint.hh b/src/kripke/kripkeprint.hh
index d232a4a77..4f96bb422 100644
--- a/src/kripke/kripkeprint.hh
+++ b/src/kripke/kripkeprint.hh
@@ -1,4 +1,5 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Developpement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -20,7 +21,9 @@
 #ifndef SPOT_KRIPKE_KRIPKEPRINT_HH
 # define SPOT_KRIPKE_KRIPKEPRINT_HH
 
+# include "misc/common.hh"
 # include <iosfwd>
+
 namespace spot
 {
 
@@ -35,7 +38,8 @@ namespace spot
   /// function only for debugging.  Use
   /// kripke_save_reachable_renumbered() for large output.
   ///
-  std::ostream& kripke_save_reachable(std::ostream& os, const kripke* k);
+  SPOT_API std::ostream&
+  kripke_save_reachable(std::ostream& os, const kripke* k);
 
   /// \ingroup tgba_io
   /// \brief Save the reachable part of Kripke structure in text format.
@@ -45,9 +49,9 @@ namespace spot
   /// state names.  The drawback is that any information carried by
   /// the state name is lost.
   ///
-  std::ostream& kripke_save_reachable_renumbered(std::ostream& os,
-						 const kripke* k);
+  SPOT_API std::ostream&
+  kripke_save_reachable_renumbered(std::ostream& os, const kripke* k);
 
 } // End namespace spot
 
-#endif /* !KRIPKEPRINT_HH_ */
+#endif // SPOT_KRIPKE_KRIPKEPRINT_HH
diff --git a/src/saba/Makefile.am b/src/saba/Makefile.am
index b06731a4d..5247c7b23 100644
--- a/src/saba/Makefile.am
+++ b/src/saba/Makefile.am
@@ -1,4 +1,5 @@
-## Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et Développement
 ## de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -17,7 +18,7 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
-AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
 
 sabadir = $(pkgincludedir)/saba
 
diff --git a/src/saba/explicitstateconjunction.hh b/src/saba/explicitstateconjunction.hh
index 9c22b975c..a9c1735b3 100644
--- a/src/saba/explicitstateconjunction.hh
+++ b/src/saba/explicitstateconjunction.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,7 +20,8 @@
 #ifndef SPOT_SABA_EXPLICITSTATECONJUNCTION_HH
 # define SPOT_SABA_EXPLICITSTATECONJUNCTION_HH
 
-#include <misc/hash.hh>
+#include "misc/common.hh"
+#include "misc/hash.hh"
 #include "sabasucciter.hh"
 
 namespace spot
@@ -30,7 +31,7 @@ namespace spot
   ///
   /// This class provides a basic implementation to
   /// iterate over a conjunction of states of a saba.
-  class explicit_state_conjunction : public saba_state_conjunction
+  class SPOT_API explicit_state_conjunction : public saba_state_conjunction
   {
   public:
 
diff --git a/src/saba/saba.hh b/src/saba/saba.hh
index 87ded4016..5759112f3 100644
--- a/src/saba/saba.hh
+++ b/src/saba/saba.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 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
 {
-  /// \defgroup saba SABA (State-based Alternating Büchi Automata)
+  /// \defgroup saba SABA (State-based Alternating Büchi Automata)
   ///
   /// Spot was centered around non-deterministic \ref tgba.
   /// Alternating automata are an extension to non-deterministic
@@ -37,7 +38,7 @@ namespace spot
   /// \ingroup saba
 
   /// \ingroup saba_essentials
-  /// \brief A State-based Alternating (Generalized) Büchi Automaton.
+  /// \brief A State-based Alternating (Generalized) Büchi Automaton.
   ///
   /// Browsing such automaton can be achieved using two functions:
   /// \c get_init_state, and \c succ_iter.  The former returns
@@ -48,7 +49,7 @@ namespace spot
   /// we never represent transitions!  Transition informations are
   /// obtained by querying the iterator over the successors of
   /// a state.
-  class saba
+  class SPOT_API saba
   {
   protected:
     saba();
diff --git a/src/saba/sabacomplementtgba.hh b/src/saba/sabacomplementtgba.hh
index d78c80fbe..23f35319a 100644
--- a/src/saba/sabacomplementtgba.hh
+++ b/src/saba/sabacomplementtgba.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -51,7 +51,7 @@ namespace spot
   /// The construction is done on-the-fly, by the
   /// \c saba_complement_succ_iterator class.
   /// \see saba_complement_succ_iterator
-  class saba_complement_tgba : public saba
+  class SPOT_API saba_complement_tgba : public saba
   {
   public:
     saba_complement_tgba(const tgba* a);
diff --git a/src/saba/sabastate.hh b/src/saba/sabastate.hh
index f169677f6..0d317952c 100644
--- a/src/saba/sabastate.hh
+++ b/src/saba/sabastate.hh
@@ -1,4 +1,5 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -19,6 +20,7 @@
 #ifndef SPOT_SABA_SABASTATE_HH
 # define SPOT_SABA_SABASTATE_HH
 
+#include "misc/common.hh"
 #include <bdd.h>
 #include <functional>
 #include <boost/shared_ptr.hpp>
@@ -28,7 +30,7 @@ namespace spot
 
   /// \ingroup saba_essentials
   /// \brief Abstract class for saba states.
-  class saba_state
+  class SPOT_API saba_state
   {
   public:
     /// \brief Compares two states (that come from the same automaton).
diff --git a/src/saba/sabasucciter.hh b/src/saba/sabasucciter.hh
index 46e4a8d30..9d18d2798 100644
--- a/src/saba/sabasucciter.hh
+++ b/src/saba/sabasucciter.hh
@@ -1,4 +1,5 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -28,7 +29,7 @@ namespace spot
   ///
   /// This class provides the basic functionalities required to
   /// iterate over a conjunction of states of a saba.
-  class saba_state_conjunction
+  class SPOT_API saba_state_conjunction
   {
   public:
     virtual
@@ -95,7 +96,7 @@ namespace spot
   /// transitions of an alternating automaton are defined as a
   /// boolean function with conjunctions (universal) and
   /// disjunctions (non-deterministic),
-  class saba_succ_iterator
+  class SPOT_API saba_succ_iterator
   {
   public:
     virtual
diff --git a/src/sabaalgos/Makefile.am b/src/sabaalgos/Makefile.am
index ab0dac6f3..0e08129c1 100644
--- a/src/sabaalgos/Makefile.am
+++ b/src/sabaalgos/Makefile.am
@@ -1,5 +1,6 @@
-## Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
-## de l'Epita (LRDE).
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -17,7 +18,7 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
-AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
 
 sabaalgosdir = $(pkgincludedir)/sabaalgos
 
diff --git a/src/sabaalgos/sabadotty.hh b/src/sabaalgos/sabadotty.hh
index 402fcf687..559d41f15 100644
--- a/src/sabaalgos/sabadotty.hh
+++ b/src/sabaalgos/sabadotty.hh
@@ -1,4 +1,5 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -19,6 +20,7 @@
 #ifndef SPOT_SABAALGOS_SABADOTTY_HH
 # define SPOT_SABAALGOS_SABADOTTY_HH
 
+#include "misc/common.hh"
 #include <iosfwd>
 
 namespace spot
@@ -27,7 +29,7 @@ namespace spot
 
   /// \ingroup saba_io
   /// \brief Print reachable states in dot format.
-  std::ostream&
+  SPOT_API std::ostream&
   saba_dotty_reachable(std::ostream& os,
                        const saba* g);
 }
diff --git a/src/sabaalgos/sabareachiter.hh b/src/sabaalgos/sabareachiter.hh
index d183f1446..b52c4b103 100644
--- a/src/sabaalgos/sabareachiter.hh
+++ b/src/sabaalgos/sabareachiter.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -28,7 +29,7 @@ namespace spot
 {
   /// \ingroup saba_generic
   /// \brief Iterate over all reachable states of a spot::saba.
-  class saba_reachable_iterator
+  class SPOT_API saba_reachable_iterator
   {
   public:
     saba_reachable_iterator(const saba* a);
@@ -115,7 +116,8 @@ namespace spot
   /// \ingroup saba_generic
   /// \brief An implementation of spot::saba_reachable_iterator that browses
   /// states depth first.
-  class saba_reachable_iterator_depth_first : public saba_reachable_iterator
+  class SPOT_API saba_reachable_iterator_depth_first:
+    public saba_reachable_iterator
   {
   public:
     saba_reachable_iterator_depth_first(const saba* a);
@@ -130,7 +132,8 @@ namespace spot
   /// \ingroup saba_generic
   /// \brief An implementation of spot::saba_reachable_iterator that browses
   /// states breadth first.
-  class saba_reachable_iterator_breadth_first : public saba_reachable_iterator
+  class SPOT_API saba_reachable_iterator_breadth_first:
+    public saba_reachable_iterator
   {
   public:
     saba_reachable_iterator_breadth_first(const saba* a);