From 3f5470898db2ac6ed1c84c42f00ee58026e186ed Mon Sep 17 00:00:00 2001
From: Maximilien Colange <colange@lrde.epita.fr>
Date: Wed, 1 Feb 2017 17:50:01 +0100
Subject: [PATCH] Rework the 'down_cast' macro, closing #196.

* spot/misc/casts.hh: New inline functions and compile-time checks.
* spot/kripke/kripkegraph.hh, spot/ta/taexplicit.cc,
  spot/ta/taproduct.cc, spot/ta/tgtaproduct.cc, spot/taalgos/tgba2ta.cc,
  spot/twa/taatgba.hh, spot/twa/taatgba.cc, spot/twa/twagraph.hh,
  spot/twa/twaproduct.cc, spot/twaalgos/emptiness.cc,
  spot/twaalgos/stutter.cc, spot/ltsmin/ltsmin.cc, tests/core/ikwiad.cc,
  tests/core/ngraph.cc: Remove downcast checks from code.
---
 spot/kripke/kripkegraph.hh |   8 +--
 spot/ltsmin/ltsmin.cc      |   4 --
 spot/misc/casts.hh         | 132 +++++++++++++++++++++++++++++++++----
 spot/ta/taexplicit.cc      |  15 +----
 spot/ta/taproduct.cc       |  16 +----
 spot/ta/tgtaproduct.cc     |   5 +-
 spot/taalgos/tgba2ta.cc    |   5 +-
 spot/twa/taatgba.cc        |   6 +-
 spot/twa/taatgba.hh        |   5 +-
 spot/twa/twagraph.hh       |   6 +-
 spot/twa/twaproduct.cc     |   4 --
 spot/twaalgos/emptiness.cc |  11 ++--
 spot/twaalgos/stutter.cc   |   7 +-
 tests/core/ikwiad.cc       |   3 +-
 tests/core/ngraph.cc       |   5 +-
 15 files changed, 143 insertions(+), 89 deletions(-)

diff --git a/spot/kripke/kripkegraph.hh b/spot/kripke/kripkegraph.hh
index 59c5b9ae5..57297b024 100644
--- a/spot/kripke/kripkegraph.hh
+++ b/spot/kripke/kripkegraph.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE)
+// Copyright (C) 2011-2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -42,7 +42,6 @@ namespace spot
     virtual int compare(const spot::state* other) const override
     {
       auto o = down_cast<const kripke_graph_state*>(other);
-      SPOT_ASSERT(o);
 
       // Do not simply return "other - this", it might not fit in an int.
       if (o < this)
@@ -194,7 +193,6 @@ namespace spot
     succ_iter(const spot::state* st) const override
     {
       auto s = down_cast<const typename graph_t::state_storage_t*>(st);
-      SPOT_ASSERT(s);
       SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
 
       if (this->iter_cache_)
@@ -213,7 +211,6 @@ namespace spot
     state_number(const state* st) const
     {
       auto s = down_cast<const typename graph_t::state_storage_t*>(st);
-      SPOT_ASSERT(s);
       return s - &g_.state_storage(0);
     }
 
@@ -245,7 +242,6 @@ namespace spot
     virtual bdd state_condition(const state* s) const override
     {
       auto gs = down_cast<const kripke_graph_state*>(s);
-      SPOT_ASSERT(gs);
       return gs->cond();
     }
 
diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc
index 2a8373de5..b8e53610d 100644
--- a/spot/ltsmin/ltsmin.cc
+++ b/spot/ltsmin/ltsmin.cc
@@ -121,7 +121,6 @@ namespace spot
         if (this == other)
           return 0;
         const spins_state* o = down_cast<const spins_state*>(other);
-        assert(o);
         if (hash_value < o->hash_value)
           return -1;
         if (hash_value > o->hash_value)
@@ -182,7 +181,6 @@ namespace spot
           return 0;
         const spins_compressed_state* o =
           down_cast<const spins_compressed_state*>(other);
-        assert(o);
         if (hash_value < o->hash_value)
           return -1;
         if (hash_value > o->hash_value)
@@ -833,7 +831,6 @@ namespace spot
           {
             const spins_compressed_state* s =
               down_cast<const spins_compressed_state*>(st);
-            assert(s);
 
             decompress_(s->vars, s->size, uncompressed_, state_size_);
             vars = uncompressed_;
@@ -841,7 +838,6 @@ namespace spot
         else
           {
             const spins_state* s = down_cast<const spins_state*>(st);
-            assert(s);
             vars = s->vars;
           }
         return vars;
diff --git a/spot/misc/casts.hh b/spot/misc/casts.hh
index a4050893a..56c315ae3 100644
--- a/spot/misc/casts.hh
+++ b/spot/misc/casts.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2015-2016 Laboratoire de Recherche et Développement
+// Copyright (C) 2011, 2015-2017 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -19,23 +19,127 @@
 
 #pragma once
 
+#include <memory>
+#include <type_traits>
+
 // We usually write code like
-//   subclass* i = down_cast<subclass*>(m);
-//   assert(i);
+//   subtypename* i = down_cast<subtypename*>(m);
 //   ... use i ...
-// When NDEBUG is set, the down_cast is a fast static_cast
-// and the assert has no effect.
+// When NDEBUG is set, the down_cast is a fast static_cast.
 // Otherwise, the down_cast is a dynamic_cast and may return 0
-// on error, which the assert catches.
+// on error, which is caught by an assert in the down_cast function.
+//
+// NB: It is valid to use down_cast with non-pointer template argument:
+//    subtypename& i = down_cast<subtypename&>(m);
+// If an error occurs during the cast, an exception is thrown.
+//
+// NB: down_cast can also be used on shared_ptr.
 
-#if NDEBUG
-#  define down_cast static_cast
-#else
-#  define down_cast dynamic_cast
-#endif
+namespace
+{
+  // A helper struct to check that downcasts are performed down an inheritance
+  // hierarchy, not between unrelated types.
+  template<typename Base, typename Derived>
+  struct is_base_of : std::is_base_of<Base, Derived>
+  {};
+  template<typename Base, typename Derived>
+  struct is_base_of<Base*, Derived*> : is_base_of<Base, Derived>
+  {};
+  // Also handle smart pointers.
+  template<typename Base, typename Derived>
+  struct is_base_of<std::shared_ptr<Base>, std::shared_ptr<Derived>>
+    : is_base_of<Base, Derived>
+  {};
 
-#if NDEBUG
-#  define down_pointer_cast std::static_pointer_cast
+  // std::is_pointer does not detect smart pointers.
+  // Make our own version that detects pointer, plain or smart.
+  template<typename T>
+  struct is_pointer : std::is_pointer<T>
+  {};
+  template<typename T>
+  struct is_pointer<std::shared_ptr<T>> : std::true_type
+  {};
+
+  template<typename T, typename U, bool check>
+  struct _downcast;
+
+  // A down-cast on non-pointer type is legitimate, e.g. down_cast<Derived&>(m);
+  // An error in the dynamic_cast will throw an exception.
+  template<typename T, typename U>
+  struct _downcast<T, U, false>
+  {
+    static_assert(is_base_of<U, T>::value, "invalid downcast");
+
+    static
+    inline
+    T
+    cast(U u)
+#ifdef NDEBUG
+    noexcept
 #else
-#  define down_pointer_cast std::dynamic_pointer_cast
+    noexcept(is_pointer<T>::value)
 #endif
+    {
+#ifdef NDEBUG
+      return static_cast<T>(u);
+#else
+      return dynamic_cast<T>(u);
+#endif
+    }
+  };
+
+  // A specialization for smart pointer, so that down_cast can be used
+  // uniformly.
+  // NB: Use
+  //    auto d = down_cast<std::shared_ptr<T>>(b);
+  // instead of
+  //    auto d = std::dynamic_pointer_cast<T>(b);
+  template<typename T, typename U>
+  struct _downcast<std::shared_ptr<T>, U, false>
+  {
+    static_assert(is_base_of<U, std::shared_ptr<T>>::value, "invalid downcast");
+
+    static
+    inline
+    std::shared_ptr<T>
+    cast(U u) noexcept
+    {
+#ifdef NDEBUG
+      return std::static_pointer_cast<T>(u);
+#else
+      return std::dynamic_pointer_cast<T>(u);
+#endif
+    }
+  };
+
+  // Pointer type specialization.
+  // Cast errors are caught by an assertion, no exception is thrown.
+  template<typename T, typename U>
+  struct _downcast<T, U, true>
+  {
+    static
+    inline
+    T
+    cast(U u) noexcept
+    {
+      T t = _downcast<T, U, false>::cast(u);
+      SPOT_ASSERT(t);
+      return t;
+    }
+  };
+} // anonymous namespace
+
+// The actual function to call.
+template<typename T, typename U>
+inline
+T
+down_cast(U u)
+#ifdef NDEBUG
+    noexcept
+#else
+    noexcept(is_pointer<T>::value)
+#endif
+{
+  return _downcast<T, U, is_pointer<T>::value>::cast(u);
+}
+
diff --git a/spot/ta/taexplicit.cc b/spot/ta/taexplicit.cc
index 400f8f140..075f725ed 100644
--- a/spot/ta/taexplicit.cc
+++ b/spot/ta/taexplicit.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
-// de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -230,7 +230,6 @@ namespace spot
   state_ta_explicit::compare(const spot::state* other) const
   {
     const state_ta_explicit* o = down_cast<const state_ta_explicit*>(other);
-    assert(o);
 
     int compare_value = tgba_state_->compare(o->tgba_state_);
 
@@ -362,7 +361,6 @@ namespace spot
       {
         auto* s = const_cast<state_ta_explicit*>
           (down_cast<const state_ta_explicit*>(*it));
-        assert(s);
         s->free_transitions();
         s->get_tgba_state()->destroy();
         delete s;
@@ -383,7 +381,6 @@ namespace spot
   ta_explicit::add_to_initial_states_set(state* state, bdd condition)
   {
     state_ta_explicit* s = down_cast<state_ta_explicit*>(state);
-    assert(s);
     s->set_initial_state(true);
     if (condition == bddfalse)
       condition = get_state_condition(s);
@@ -402,7 +399,6 @@ namespace spot
   {
     auto state =
       const_cast<state_ta_explicit*>(down_cast<const state_ta_explicit*>(s));
-    assert(state);
     state->delete_stuttering_and_hole_successors();
     if (state->is_initial_state())
       add_to_initial_states_set(state);
@@ -435,7 +431,6 @@ namespace spot
   {
     const state_ta_explicit* sta =
         down_cast<const state_ta_explicit*>(initial_state);
-    assert(sta);
     return sta->get_tgba_condition();
   }
 
@@ -443,7 +438,6 @@ namespace spot
   ta_explicit::is_accepting_state(const spot::state* s) const
   {
     const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
-    assert(sta);
     return sta->is_accepting_state();
   }
 
@@ -451,7 +445,6 @@ namespace spot
   ta_explicit::is_initial_state(const spot::state* s) const
   {
     const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
-    assert(sta);
     return sta->is_initial_state();
   }
 
@@ -459,7 +452,6 @@ namespace spot
   ta_explicit::is_livelock_accepting_state(const spot::state* s) const
   {
     const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
-    assert(sta);
     return sta->is_livelock_accepting_state();
   }
 
@@ -467,7 +459,6 @@ namespace spot
   ta_explicit::succ_iter(const spot::state* state) const
   {
     const state_ta_explicit* s = down_cast<const state_ta_explicit*>(state);
-    assert(s);
     return new ta_explicit_succ_iterator(s);
   }
 
@@ -475,7 +466,6 @@ namespace spot
   ta_explicit::succ_iter(const spot::state* state, bdd condition) const
   {
     const state_ta_explicit* s = down_cast<const state_ta_explicit*>(state);
-    assert(s);
     return new ta_explicit_succ_iterator(s, condition);
   }
 
@@ -495,7 +485,6 @@ namespace spot
   ta_explicit::format_state(const spot::state* s) const
   {
     const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
-    assert(sta);
 
     if (sta->get_tgba_condition() == bddtrue)
       return tgba_->format_state(sta->get_tgba_state());
diff --git a/spot/ta/taproduct.cc b/spot/ta/taproduct.cc
index 859521d16..d6975d293 100644
--- a/spot/ta/taproduct.cc
+++ b/spot/ta/taproduct.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2011, 2012, 2014-2017 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 //
 // This file is part of Spot, a model checking library.
@@ -38,7 +38,6 @@ namespace spot
   state_ta_product::compare(const state* other) const
   {
     const state_ta_product* o = down_cast<const state_ta_product*> (other);
-    assert(o);
     int res = ta_state_->compare(o->get_ta_state());
     if (res != 0)
       return res;
@@ -298,7 +297,6 @@ namespace spot
   ta_product::succ_iter(const state* s) const
   {
     const state_ta_product* stp = down_cast<const state_ta_product*>(s);
-    assert(stp);
     return new ta_succ_iterator_product(stp, ta_.get(), kripke_.get());
   }
 
@@ -307,7 +305,6 @@ namespace spot
   ta_product::succ_iter(const spot::state* s, bdd changeset) const
   {
     const state_ta_product* stp = down_cast<const state_ta_product*>(s);
-    assert(stp);
     return new ta_succ_iterator_product_by_changeset(stp,
                                                      ta_.get(), kripke_.get(),
                                                      changeset);
@@ -324,7 +321,6 @@ namespace spot
   ta_product::format_state(const state* state) const
   {
     const state_ta_product* s = down_cast<const state_ta_product*> (state);
-    assert(s);
     return kripke_->format_state(s->get_kripke_state()) + " * \n"
         + ta_->format_state(s->get_ta_state());
   }
@@ -333,8 +329,6 @@ namespace spot
   ta_product::is_accepting_state(const spot::state* s) const
   {
     const state_ta_product* stp = down_cast<const state_ta_product*> (s);
-    assert(stp);
-
     return ta_->is_accepting_state(stp->get_ta_state());
   }
 
@@ -342,8 +336,6 @@ namespace spot
   ta_product::is_livelock_accepting_state(const spot::state* s) const
   {
     const state_ta_product* stp = down_cast<const state_ta_product*> (s);
-    assert(stp);
-
     return ta_->is_livelock_accepting_state(stp->get_ta_state());
   }
 
@@ -351,7 +343,6 @@ namespace spot
   ta_product::is_initial_state(const spot::state* s) const
   {
     const state_ta_product* stp = down_cast<const state_ta_product*> (s);
-    assert(stp);
 
     const state* ta_s = stp->get_ta_state();
     const state* kr_s = stp->get_kripke_state();
@@ -366,7 +357,6 @@ namespace spot
   ta_product::is_hole_state_in_ta_component(const spot::state* s) const
   {
     const state_ta_product* stp = down_cast<const state_ta_product*> (s);
-    assert(stp);
     ta_succ_iterator* ta_succ_iter = get_ta()->succ_iter(stp->get_ta_state());
     bool is_hole_state = ta_succ_iter->done();
     delete ta_succ_iter;
@@ -377,7 +367,6 @@ namespace spot
   ta_product::get_state_condition(const spot::state* s) const
   {
     const state_ta_product* stp = down_cast<const state_ta_product*> (s);
-    assert(stp);
     const state* ta_s = stp->get_ta_state();
     return ta_->get_state_condition(ta_s);
   }
@@ -387,7 +376,6 @@ namespace spot
   {
 
     const state_ta_product* stp = down_cast<const state_ta_product*> (s);
-    assert(stp);
     ta_->free_state(stp->get_ta_state());
     delete stp;
 
diff --git a/spot/ta/tgtaproduct.cc b/spot/ta/tgtaproduct.cc
index 7f16b6c72..e49c6d629 100644
--- a/spot/ta/tgtaproduct.cc
+++ b/spot/ta/tgtaproduct.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
-// Développement de l Epita (LRDE).
+// Copyright (C) 2012, 2014-2017 Laboratoire de Recherche et Développement de
+// l Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -61,7 +61,6 @@ namespace spot
   tgta_product::succ_iter(const state* state) const
   {
     const state_product* s = down_cast<const state_product*> (state);
-    assert(s);
 
     fixed_size_pool* p = const_cast<fixed_size_pool*> (&pool_);
 
diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc
index 5c4d006c1..b3dda288d 100644
--- a/spot/taalgos/tgba2ta.cc
+++ b/spot/taalgos/tgba2ta.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -313,7 +313,6 @@ namespace spot
                 {
                   auto self_loop_state = const_cast<state_ta_explicit*>
                     (down_cast<const state_ta_explicit*>(curr));
-                  assert(self_loop_state);
 
                   if (testing_aut->is_accepting_state(self_loop_state)
                       || (testing_aut->acc().accepting(acc_cond)))
diff --git a/spot/twa/taatgba.cc b/spot/twa/taatgba.cc
index e831407fe..5cdab01d3 100644
--- a/spot/twa/taatgba.cc
+++ b/spot/twa/taatgba.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
-// Laboratoire de Recherche et Développement de l'Epita (LRDE)
+// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -62,7 +62,6 @@ namespace spot
   taa_tgba::succ_iter(const spot::state* state) const
   {
     const spot::set_state* s = down_cast<const spot::set_state*>(state);
-    assert(s);
     return new taa_succ_iterator(s->get_state(), acc());
   }
 
@@ -80,7 +79,6 @@ namespace spot
   set_state::compare(const spot::state* other) const
   {
     const set_state* o = down_cast<const set_state*>(other);
-    assert(o);
 
     const taa_tgba::state_set* s1 = get_state();
     const taa_tgba::state_set* s2 = o->get_state();
diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh
index 9a3c8b647..80c753bbe 100644
--- a/spot/twa/taatgba.hh
+++ b/spot/twa/taatgba.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -209,7 +209,6 @@ namespace spot
     virtual std::string format_state(const spot::state* s) const override
     {
       const spot::set_state* se = down_cast<const spot::set_state*>(s);
-      SPOT_ASSERT(se);
       const state_set* ss = se->get_state();
       return format_state_set(ss);
     }
diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh
index ccab488ab..9c3f77014 100644
--- a/spot/twa/twagraph.hh
+++ b/spot/twa/twagraph.hh
@@ -1,6 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
-// de l'Epita.
+// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -45,7 +44,6 @@ namespace spot
     virtual int compare(const spot::state* other) const override
     {
       auto o = down_cast<const twa_graph_state*>(other);
-      SPOT_ASSERT(o);
 
       // Do not simply return "other - this", it might not fit in an int.
       if (o < this)
@@ -306,7 +304,6 @@ namespace spot
     succ_iter(const state* st) const override
     {
       auto s = down_cast<const typename graph_t::state_storage_t*>(st);
-      SPOT_ASSERT(s);
       SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
 
       if (this->iter_cache_)
@@ -336,7 +333,6 @@ namespace spot
     state_number(const state* st) const
     {
       auto s = down_cast<const typename graph_t::state_storage_t*>(st);
-      SPOT_ASSERT(s);
       return s - &g_.state_storage(0);
     }
 
diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc
index 2a7756135..3476341ef 100644
--- a/spot/twa/twaproduct.cc
+++ b/spot/twa/twaproduct.cc
@@ -52,7 +52,6 @@ namespace spot
   state_product::compare(const state* other) const
   {
     const state_product* o = down_cast<const state_product*>(other);
-    assert(o);
     int res = left_->compare(o->left());
     if (res != 0)
       return res;
@@ -336,7 +335,6 @@ namespace spot
   twa_product::succ_iter(const state* state) const
   {
     const state_product* s = down_cast<const state_product*>(state);
-    assert(s);
     twa_succ_iterator* li = left_->succ_iter(s->left());
     twa_succ_iterator* ri = right_->succ_iter(s->right());
 
@@ -370,7 +368,6 @@ namespace spot
   twa_product::format_state(const state* state) const
   {
     const state_product* s = down_cast<const state_product*>(state);
-    assert(s);
     return (left_->format_state(s->left())
             + " * "
             + right_->format_state(s->right()));
@@ -380,7 +377,6 @@ namespace spot
   twa_product::project_state(const state* s, const const_twa_ptr& t) const
   {
     const state_product* s2 = down_cast<const state_product*>(s);
-    assert(s2);
     if (t.get() == this)
       return s2->clone();
     state* res = left_->project_state(s2->left(), t);
diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc
index a9934946d..23fa84692 100644
--- a/spot/twaalgos/emptiness.cc
+++ b/spot/twaalgos/emptiness.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -446,11 +446,11 @@ namespace spot
     auto res = std::make_shared<twa_run>(other);
     if (auto ps = aut->get_named_prop<const product_states>("product-states"))
       {
-        auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
+        auto a = down_cast<const_twa_graph_ptr>(aut);
         if (!a)
           throw std::runtime_error("twa_run::project() confused: "
                                    "product-states found in a non-twa_graph");
-        auto oth = std::dynamic_pointer_cast<const twa_graph>(other);
+        auto oth = down_cast<const_twa_graph_ptr>(other);
         if (!oth)
           throw std::runtime_error("twa_run::project() confused: "
                                    "other ought to be a twa_graph");
@@ -709,8 +709,7 @@ namespace spot
   /// Note that this works only if the automaton is a twa_graph_ptr.
   void twa_run::highlight(unsigned color)
   {
-    auto a = std::dynamic_pointer_cast<twa_graph>
-      (std::const_pointer_cast<twa>(aut));
+    auto a = down_cast<twa_graph_ptr>(std::const_pointer_cast<twa>(aut));
     if (!a)
       throw std::runtime_error("highlight() only work for twa_graph");
 
diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc
index 1dad5a144..1d1e7e1f1 100644
--- a/spot/twaalgos/stutter.cc
+++ b/spot/twaalgos/stutter.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -59,7 +59,6 @@ namespace spot
       {
         const state_tgbasl* o =
           down_cast<const state_tgbasl*>(other);
-        assert(o);
         int res = s_->compare(o->real_state());
         if (res != 0)
           return res;
@@ -223,7 +222,6 @@ namespace spot
       virtual twa_succ_iterator* succ_iter(const state* state) const override
       {
         const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
-        assert(s);
         return new twasl_succ_iterator(a_->succ_iter(s->real_state()), s,
                                         a_->get_dict(), aps_);
       }
@@ -231,7 +229,6 @@ namespace spot
       virtual std::string format_state(const state* state) const override
       {
         const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
-        assert(s);
         return (a_->format_state(s->real_state())
                 + ", "
                 + bdd_format_formula(a_->get_dict(), s->cond()));
diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc
index 04083a65d..73a0e9ac8 100644
--- a/tests/core/ikwiad.cc
+++ b/tests/core/ikwiad.cc
@@ -1156,8 +1156,7 @@ checked_main(int argc, char** argv)
           if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
             {
               tm.start("SCC-filter post-sim");
-              auto aa = std::dynamic_pointer_cast<const spot::twa_graph>(a);
-              assert(aa);
+              auto aa = down_cast<spot::const_twa_graph_ptr>(a);
               // Do not filter_all for SBA
               a = spot::scc_filter(aa, assume_sba ?
                                    false : scc_filter_all);
diff --git a/tests/core/ngraph.cc b/tests/core/ngraph.cc
index 69726398f..793329981 100644
--- a/tests/core/ngraph.cc
+++ b/tests/core/ngraph.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
-// Développement de l'Epita.
+// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de
+// l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -348,7 +348,6 @@ public:
   int compare(const spot::state* other) const override
   {
     auto o = down_cast<const my_state*>(other);
-    assert(o);
 
     // Do not simply return "other - this", it might not fit in an int.
     if (o < this)