Fix documentation errors reported by clang++ 3.2.

* m4/gccwarn.m4: Use -Wdocumentation if supported.
* src/ltlast/binop.hh, src/ltlparse/public.hh, src/ta/taproduct.hh,
src/taalgos/emptinessta.hh, src/taalgos/reachiter.hh,
src/tgba/state.hh, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/ltl2tgba_fm.hh: Fix Doxygen documentations errors signaled
by clang++ 3.2.

m4/gccwarn.m4

@@ -29,6 +29,7 @@ EOF
    Wpointer-arith \
    Wwrite-strings \
    Wcast-qual \
+   Wdocumentation \
    Werror
   do
     CXXFLAGS="$cf_save_CXXFLAGS $ac_cv_prog_gxx_warn_flags -$cf_opt"

src/ltlast/binop.hh

@@ -1,8 +1,9 @@
-// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+// -*- coding: utf-8 -*-
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012, 2013 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),
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -48,13 +49,13 @@ namespace spot
       enum type { Xor,
 		  Implies,
 		  Equiv,
-		  U, //< until
+		  U, ///< until
-		  R, //< release (dual of until)
+		  R, ///< release (dual of until)
-		  W, //< weak until
+		  W, ///< weak until
-		  M,  //< strong release (dual of weak until)
+		  M, ///< strong release (dual of weak until)
-		  EConcat, // Existential Concatenation
+		  EConcat, ///< Existential Concatenation
-		  EConcatMarked, // Existential Concatenation, Marked
+		  EConcatMarked, ///< Existential Concatenation, Marked
-		  UConcat // Universal Concatenation
+		  UConcat ///< Universal Concatenation
       };
 
       /// \brief Build a unary operator with operation \a op and

src/ltlparse/public.hh

@@ -1,8 +1,9 @@
-// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+// -*- coding: utf-8 -*-
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013 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),
+// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -189,7 +190,7 @@ namespace spot
     /// \param error_list The error list filled by spot::ltl::parse
     ///        or spot::ltl::parse_sere while parsing \a input_string.
     void
-    fix_utf8_locations(const std::string& ltl_string,
+    fix_utf8_locations(const std::string& input_string,
 		       parse_error_list& error_list);
 
     /// @}

src/ta/taproduct.hh

@@ -1,5 +1,6 @@
-// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// -*- coding: utf-8 -*-
-// 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.
 //
@@ -35,7 +36,7 @@ namespace spot
   public:
     /// \brief Constructor
     /// \param ta_state The state from the ta automaton.
-    /// \param kripke_state_ The state from Kripke structure.
+    /// \param kripke_state The state from Kripke structure.
     state_ta_product(state* ta_state, state* kripke_state) :
       ta_state_(ta_state), kripke_state_(kripke_state)
     {

src/taalgos/emptinessta.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2012 Laboratoire de Recherche et Dévelopment de
+// Copyright (C) 2008, 2012, 2013 Laboratoire de Recherche et
-// l'Epita (LRDE).
+// Dévelopment 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),
 // Université Pierre et Marie Curie.
@@ -99,19 +99,19 @@ namespace spot
     ///
     /// Return false if the product automaton accepts no run, otherwise true
     ///
-    /// \param disable_second_pass: is used to disable the second pass when
+    /// \param disable_second_pass is used to disable the second pass when
     /// when it is not necessary, for example when all the livelock-accepting
     /// states of the TA automaton have no successors, we call this kind of
     /// TA as STA (Single-pass Testing Automata)
     /// (see spot::tgba2ta::add_artificial_livelock_accepting_state() for an
     /// automatic transformation of any TA automaton into STA automaton
     ///
-    /// \param disable_heuristic_for_livelock_detection: disable the heuristic
+    /// \param disable_heuristic_for_livelock_detection disable the heuristic
     /// used in the first pass to detect livelock-accepting runs,
     /// this heuristic is described in the paper cited above
     virtual bool
     check(bool disable_second_pass = false,
-        bool disable_heuristic_for_livelock_detection = false);
+	  bool disable_heuristic_for_livelock_detection = false);
 
     /// \brief Check whether the product automaton contains
     /// a livelock-accepting run

src/taalgos/reachiter.hh

@@ -1,6 +1,6 @@
-// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// -*- coding: utf-8 -*-
-// de l Epita (LRDE).
+// 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.
 //
@@ -74,21 +74,14 @@ namespace spot
     ///
     /// \param s The current state.
     /// \param n A unique number assigned to \a s.
-    /// \param si The spot::ta_succ_iterator for \a s.
     virtual void
     process_state(const state* s, int n);
     /// Called by run() to process a transition.
     ///
-    /// \param in_s The source state
     /// \param in The source state number.
-    /// \param out_s The destination state
     /// \param out The destination state number.
     /// \param si The spot::tgba_succ_iterator positionned on the current
     ///             transition.
-    ///
-    /// The in_s and out_s states are owned by the
-    /// spot::ta_reachable_iterator instance and destroyed when the
-    /// instance is destroyed.
     virtual void
     process_link(int in, int out, const ta_succ_iterator* si);
 

src/tgba/state.hh

@@ -1,7 +1,8 @@
-// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2011, 2013 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é
+// (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.
@@ -78,10 +79,10 @@ namespace spot
     /// 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
+    /// Starting with Spot 0.7, you should update your code to use
-    /// instead (which simply calls "delete").  In a future version,
+    /// this function instead. destroy() usually call delete, except
-    /// some subclasses will redefine destroy() to allow better memory
+    /// in subclasses that destroy() to allow better memory management
-    /// management (e.g. no memory allocation for explicit automata).
+    /// (e.g., no memory allocation for explicit automata).
     virtual void destroy() const
     {
       delete this;
@@ -90,7 +91,7 @@ namespace spot
   protected:
     /// \brief Destructor.
     ///
-    /// \deprecated Client code should now call
+    /// Note that client code should call
     /// <code>s->destroy();</code> instead of <code>delete s;</code>.
     virtual ~state()
     {

src/tgba/tgbasafracomplement.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
-// Développement de l'Epita (LRDE).
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -191,7 +191,7 @@ namespace spot
 
     /// \brief Compare two safra trees.
     ///
-    /// \param other
+    /// \param other the tree to compare too.
     ///
     /// \return 0 if the trees are the same. Otherwise
     /// a signed value.
@@ -520,7 +520,7 @@ namespace spot
     ///
     /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
     /// filled with FALSE bits.
-    /// \return bitset[i] will be true if this state-tree is included in L_i
+    /// On return bitset[i] will be set if this state-tree is included in L_i.
     void
     safra_tree::getL(bitset_t& bitset) const
     {
@@ -538,7 +538,7 @@ namespace spot
     ///
     /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
     /// filled with TRUE bits.
-    /// \return bitset[i] will be true if this state-tree is included in U_i
+    /// On return bitset[i] will be set if this state-tree is included in U_i.
     void
     safra_tree::getU(bitset_t& bitset) const
     {
@@ -1202,7 +1202,7 @@ namespace spot
   ///   publisher     = {Springer-Verlag}
   /// }
   ///
-  /// @param local_state
+  /// @param local_state the state from which we want to compute the successors.
   ///
   tgba_succ_iterator*
   tgba_safra_complement::succ_iter(const state* local_state,

src/tgbaalgos/ltl2tgba_fm.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+// Copyright (C) 2010, 2011, 2012, 2013 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),
@@ -97,11 +97,12 @@ namespace spot
   /// formula are observable events, and \c unobs can be filled with
   /// additional unobservable events.
   ///
-  /// \param simpl If this parameter is set, the LTL formulae representing
+  /// \param simplifier If this parameter is set, the LTL formulae
-  /// each state of the automaton will be simplified
+  /// representing each state of the automaton will be simplified
   /// before computing the successor.  \a simpl should be configured
-  /// for the type of reduction you want, see spot::ltl::ltl_simplifier.
+  /// for the type of reduction you want, see
-  /// This idea is taken from the following paper.
+  /// spot::ltl::ltl_simplifier.  This idea is taken from the
+  /// following paper.
   /// \verbatim
   /// @InProceedings{	  thirioux.02.fmics,
   ///   author	  = {Xavier Thirioux},