introduce SPOT_FALLTHROUGH to cope with -Wimplicit-fallthrough

* NEWS: Mention the fix.
* HACKING: Mention the new macro.
* spot/misc/common.hh (SPOT_FALLTHROUGH): Add the macro.
* bin/randltl.cc, spot/misc/escape.cc, spot/tl/mutation.cc,
spot/tl/print.cc, spot/tl/simplify.hh, spot/tl/snf.cc, spot/twa/acc.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/sepsets.cc, spot/twaalgos/translate.cc: Use it.

HACKING

@@ -554,6 +554,37 @@ Naming
   * Use *.hxx for the implementation of templates that are private to
     Spot (i.e., not installed) and need to be included multiple times.
 
+SPOT macros
+-----------
+
+  A few macros are defined in misc/common.hh notably:
+
+  * SPOT_FALLTHROUGH should be used to mark fall-throughs in switches:
+
+     switch (foo)
+     {
+       case 1:
+         f();
+         SPOT_FALLTHROUGH;
+       case 2:
+         g();
+         break;
+     }
+
+  * Use SPOT_UNREACHABLE() to mark places that are not reachable but
+    that a compiler might not see as unreachable.
+
+  * Use SPOT_API in front of functions and class that should be
+    exported by the shared library.  See "Exporting symbolss" above.
+
+  * Use SPOT_ASSERT(...) if you ever have to put an assertion in
+    some header file.  See "Assertions" above.
+
+  * Use SPOT_LIKELY / SPOT_UNLIKELY in case you need to help the
+    compiler figure out the commont output of a test.  Do not abuse
+    this without checking the assembly output to make sure the effect
+    is what you desired.
+
 Other style recommandations
 ---------------------------
 

NEWS

@@ -27,6 +27,8 @@ New in spot 2.1.1.dev (not yet released)
     should flush std::cout; however it was well visible when reading
     from files.  Flushing is now done more regularly.
 
+  - Fix compilation warnings when -Wimplicit-fallthrough it enabled.
+
 New in spot 2.1.1 (2016-09-20)
 
   Command-line tools:

bin/randltl.cc

@@ -289,7 +289,7 @@ main(int argc, char** argv)
               std::cout <<
                 "Use --ltl-priorities to set the following LTL priorities:\n";
               rg.dump_psl_priorities(std::cout);
-              // Fall through.
+              SPOT_FALLTHROUGH;
             case OUTPUTSERE:
               std::cout <<
                 "Use --sere-priorities to set the following SERE priorities:\n";

spot/misc/common.hh

@@ -117,6 +117,20 @@
 //   auto func(int param) SPOT_RETURN(implem_.func(param));
 #define SPOT_RETURN(code) -> decltype(code) { return code; }
 
+// We hope compilers that implement -Wimplicit-fallthrough
+// also support __has_cpp_attribute and some form of [[fallthrough]].
+#ifdef __has_cpp_attribute
+#  if __has_cpp_attribute(fallthrough)
+#    define SPOT_FALLTHROUGH [[fallthrough]]
+#  elif __has_cpp_attribute(clang::fallthrough)
+#    define SPOT_FALLTHROUGH [[clang::fallthrough]]
+#  elif __has_cpp_attribute(gcc::fallthrough)
+#    define SPOT_FALLTHROUGH [[gcc::fallthrough]]
+#  endif
+#endif
+#ifndef SPOT_FALLTHROUGH
+#  define SPOT_FALLTHROUGH while (0)
+#endif
 
 namespace spot
 {

spot/misc/escape.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2012, 2013, 2015, 2016 Laboratoire de Recherche et
-// l'Epita (LRDE)
+// Developpement 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.
@@ -67,6 +67,7 @@ namespace spot
         case '{':
         case '}':
           os << '\\';
+          SPOT_FALLTHROUGH;
         default:
           os << i;
           break;
@@ -149,7 +150,7 @@ namespace spot
             case '"':
             case '\\':
               os << '\\';
-              // fall through
+              SPOT_FALLTHROUGH;
             default:
               os << *str++;
               break;

spot/tl/mutation.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
-// l'Epita (LRDE).
+// Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -85,7 +85,7 @@ namespace spot
             if ((opts_ & Mut_Remove_Ops)
                 && mutation_counter_-- == 0)
               return f[0];
-            // fall through
+            SPOT_FALLTHROUGH;
           case op::Closure:
           case op::NegClosure:
           case op::NegClosureMarked:

spot/tl/print.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2010, 2012, 2013, 2014, 2015 Laboratoire de
+// Copyright (C) 2008, 2010, 2012, 2013, 2014, 2015, 2016 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
@@ -527,7 +527,7 @@ namespace spot
             emit(KNot);
             if (o == op::NegClosureMarked)
               os_ << (kw_ == utf8_kw ? "̃": "+");
-            // Fall through
+            SPOT_FALLTHROUGH;
           case op::Closure:
             os_ << '{';
             in_ratexp_ = true;

spot/tl/simplify.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
+// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
-// et Developpement de l'Epita (LRDE).
+// Recherche et Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -58,14 +58,14 @@ namespace spot
         case 3:
           containment_checks = true;
           containment_checks_stronger = true;
-          // fall through
+          SPOT_FALLTHROUGH;
         case 2:
           synt_impl = true;
-          // fall through
+          SPOT_FALLTHROUGH;
         case 1:
           reduce_basics = true;
           event_univ = true;
-          // fall through
+          SPOT_FALLTHROUGH;
         default:
           break;
         }

spot/tl/snf.cc

@@ -19,6 +19,11 @@
 
 #include <spot/tl/snf.hh>
 
+#if defined __clang__
+// See https://llvm.org/bugs/show_bug.cgi?id=30636
+#pragma clang diagnostic ignored "-Wimplicit-fallthrough"
+#endif
+
 namespace spot
 {
   namespace
@@ -65,7 +70,7 @@ namespace spot
                 out = f;
                 break;
               }
-            // Fall through
+            SPOT_FALLTHROUGH;
           case op::OrRat:
           case op::AndNLM:
             // Let F designate expressions that accept [*0],

spot/twa/acc.cc

@@ -77,6 +77,7 @@ namespace spot
         {
         case acc_cond::acc_op::And:
           op = html ? " & " : " & ";
+          SPOT_FALLTHROUGH;
         case acc_cond::acc_op::Or:
           {
             unsigned sub = pos - w.size;
@@ -99,6 +100,7 @@ namespace spot
           break;
         case acc_cond::acc_op::InfNeg:
           negated = "!";
+          SPOT_FALLTHROUGH;
         case acc_cond::acc_op::Inf:
           {
             auto a = code[pos - 1].mark.id;
@@ -134,6 +136,7 @@ namespace spot
           break;
         case acc_cond::acc_op::FinNeg:
           negated = "!";
+          SPOT_FALLTHROUGH;
         case acc_cond::acc_op::Fin:
           {
             auto a = code[pos - 1].mark.id;
@@ -347,6 +350,7 @@ namespace spot
                 pos -= 2;
                 break;
               }
+            SPOT_FALLTHROUGH;
           case acc_cond::acc_op::FinNeg:
             return true;
           }
@@ -1017,7 +1021,7 @@ namespace spot
           case acc_cond::acc_op::FinNeg:
             if (pos[-1].mark.count() > 1 && pos > and_scope)
               return false;
-            /* fall through */
+            SPOT_FALLTHROUGH;
           case acc_cond::acc_op::Inf:
           case acc_cond::acc_op::InfNeg:
             pos -= 2;
@@ -1050,7 +1054,7 @@ namespace spot
           case acc_cond::acc_op::InfNeg:
             if (pos[-1].mark.count() > 1 && pos > or_scope)
               return false;
-            /* fall through */
+            SPOT_FALLTHROUGH;
           case acc_cond::acc_op::Fin:
           case acc_cond::acc_op::FinNeg:
             pos -= 2;

spot/twaalgos/ltl2taa.cc

@@ -154,7 +154,7 @@ namespace spot
         {
         case op::U:
           strong = true;
-          // fall thru
+          SPOT_FALLTHROUGH;
         case op::W:
           if (refined_)
             contained = lcc_->contained(f[0], f[1]);
@@ -186,6 +186,7 @@ namespace spot
           return;
         case op::M: // Strong Release
           strong = true;
+          SPOT_FALLTHROUGH;
         case op::R: // Weak Release
           if (refined_)
             contained = lcc_->contained(f[0], f[1]);

spot/twaalgos/ltl2tgba_fm.cc

@@ -1264,6 +1264,7 @@ namespace spot
             }
           case op::NegClosureMarked:
             has_marked_ = true;
+            SPOT_FALLTHROUGH;
           case op::NegClosure:
             rat_seen_ = true;
             {
@@ -1394,7 +1395,7 @@ namespace spot
             }
           case op::EConcatMarked:
             has_marked_ = true;
-            /* fall through */
+            SPOT_FALLTHROUGH;
           case op::EConcat:
             rat_seen_ = true;
             {

spot/twaalgos/sepsets.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
-// Développement de l'Epita.
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -76,7 +76,7 @@ namespace spot
                   pos[-1].mark -= p.first;
                   pos[-1].mark |= p.second;
                 }
-            /* fall through */
+            SPOT_FALLTHROUGH;
           case acc_cond::acc_op::Inf:
           case acc_cond::acc_op::InfNeg:
             pos -= 2;

spot/twaalgos/translate.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -49,14 +49,13 @@ namespace spot
       case High:
         options.containment_checks = true;
         options.containment_checks_stronger = true;
-        // fall through
+        SPOT_FALLTHROUGH;
       case Medium:
         options.synt_impl = true;
-        // fall through
+        SPOT_FALLTHROUGH;
       case Low:
         options.reduce_basics = true;
         options.event_univ = true;
-        // fall through
       }
     simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
   }