diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 0ab6b05fa..8497c152d 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -145,7 +145,7 @@ namespace spot // one without. template - struct SPOT_API distate_storage: public State_Data + struct SPOT_API distate_storage final: public State_Data { Transition succ = 0; // First outgoing transition (used when iterating) Transition succ_tail = 0; // Last outgoing transition (used for @@ -168,7 +168,7 @@ namespace spot template - struct SPOT_API trans_storage: public Trans_Data + struct SPOT_API trans_storage final: public Trans_Data { typedef Transition transition; diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 213408517..d94353703 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 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 et Marie Curie. @@ -36,7 +36,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Multi-operand operators. - class SPOT_API multop : public formula + class SPOT_API multop final: public formula { public: enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion }; diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh index f6e00c481..71d1dab66 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -1,5 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013, 2014, 2015 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 @@ -37,7 +38,7 @@ namespace spot /// /// This is a singleton. Use default_environment::instance() /// to obtain the instance. - class SPOT_API default_environment : public environment + class SPOT_API default_environment final: public environment { public: virtual ~default_environment(); diff --git a/src/misc/tmpfile.hh b/src/misc/tmpfile.hh index 0fc3121b1..d824e21da 100644 --- a/src/misc/tmpfile.hh +++ b/src/misc/tmpfile.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -52,7 +52,7 @@ namespace spot typedef std::list::iterator cleanpos_t; SPOT_LOCAL temporary_file(char* name, cleanpos_t cp); - ~temporary_file(); + virtual ~temporary_file() override; const char* name() const { @@ -66,7 +66,7 @@ namespace spot } virtual void - print(std::ostream& os, const char*) const + print(std::ostream& os, const char*) const final override { os << this; } @@ -83,11 +83,11 @@ namespace spot /// /// Use the open_temporary_file::close() method if you want to close /// that descriptor; do no call the POSIX close() function directly. - class SPOT_API open_temporary_file: public temporary_file + class SPOT_API open_temporary_file final: public temporary_file { public: SPOT_LOCAL open_temporary_file(char* name, cleanpos_t cp, int fd); - ~open_temporary_file(); + virtual ~open_temporary_file() override; void close(); diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 1c93698b0..e3e8ab051 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -33,7 +33,7 @@ namespace spot { /// \brief A self-loop Transition-based Alternating Automaton (TAA) /// which is seen as a TGBA (abstract class, see below). - class SPOT_API taa_tgba : public tgba + class SPOT_API taa_tgba: public tgba { public: taa_tgba(const bdd_dict_ptr& dict); @@ -54,12 +54,13 @@ namespace spot /// TGBA interface. virtual ~taa_tgba(); - virtual spot::state* get_init_state() const; - virtual tgba_succ_iterator* succ_iter(const spot::state* state) const; + virtual spot::state* get_init_state() const final; + virtual tgba_succ_iterator* succ_iter(const spot::state* state) const final; virtual std::string format_state(const spot::state* state) const = 0; protected: - virtual bdd compute_support_conditions(const spot::state* state) const; + virtual bdd compute_support_conditions(const spot::state* state) + const final; typedef std::vector ss_vec; @@ -76,7 +77,7 @@ namespace spot }; /// Set of states deriving from spot::state. - class SPOT_API set_state : public spot::state + class SPOT_API set_state final: public spot::state { public: set_state(const taa_tgba::state_set* s, bool delete_me = false) @@ -100,7 +101,7 @@ namespace spot bool delete_me_; }; - class SPOT_API taa_succ_iterator : public tgba_succ_iterator + class SPOT_API taa_succ_iterator final: public tgba_succ_iterator { public: taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc); @@ -145,7 +146,7 @@ namespace spot /// A taa_tgba instance with states labeled by a given type. /// Still an abstract class, see below. template - class SPOT_API taa_tgba_labelled : public taa_tgba + class SPOT_API taa_tgba_labelled: public taa_tgba { public: taa_tgba_labelled(const bdd_dict_ptr& dict) : taa_tgba(dict) {}; @@ -305,7 +306,7 @@ namespace spot } }; - class SPOT_API taa_tgba_string : + class SPOT_API taa_tgba_string final: #ifndef SWIG public taa_tgba_labelled #else @@ -329,7 +330,7 @@ namespace spot return std::make_shared(dict); } - class SPOT_API taa_tgba_formula : + class SPOT_API taa_tgba_formula final: #ifndef SWIG public taa_tgba_labelled #else diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index dd99099ce..eef3cc51a 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -105,7 +105,8 @@ namespace spot template - class SPOT_API tgba_digraph_succ_iterator: public tgba_succ_iterator + class SPOT_API tgba_digraph_succ_iterator final: + public tgba_succ_iterator { private: typedef typename Graph::transition transition; @@ -168,7 +169,7 @@ namespace spot }; - class SPOT_API tgba_digraph: public tgba + class SPOT_API tgba_digraph final: public tgba { public: typedef digraph graph_t; diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index d90579bf2..b0d42fc33 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -33,7 +33,7 @@ namespace spot /// /// This state is in fact a pair of state: the state from the left /// automaton and that of the right. - class SPOT_API state_product : public state + class SPOT_API state_product final: public state { public: /// \brief Constructor @@ -119,7 +119,7 @@ namespace spot }; /// \brief A lazy product with different initial states. - class SPOT_API tgba_product_init: public tgba_product + class SPOT_API tgba_product_init final: public tgba_product { public: tgba_product_init(const const_tgba_ptr& left, const const_tgba_ptr& right, diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 37d0e727b..155e579c1 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2008, 2013, 2014, 2015 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), @@ -184,7 +184,7 @@ namespace spot /// known states first. /// /// See the documentation for spot::couvreur99. - class SPOT_API couvreur99_check_shy : public couvreur99_check + class SPOT_API couvreur99_check_shy final: public couvreur99_check { public: couvreur99_check_shy(const const_tgba_ptr& a, option_map o = option_map());