build: fix multiple GCC warnings

These occur when Spot is compiled with --enable-optimizations and
--disable-assert.

* spot/mc/unionfind.cc, spot/twaalgos/mealy_machine.cc,
spot/twaalgos/aiger.cc: Work around warnings about variables that are
only used in assert.
* spot/misc/common.hh [NDEBUG] (SPOT_ASSUME): Do not define
as assert() when it is disabled.
* spot/twaalgos/alternation.cc: Use insert instead of emplace
to work around a spurious possible nullptr dereference.
* spot/twaalgos/ltl2taa.cc, spot/twaalgos/ndfs_result.hxx,
spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc:
Work around spurious possible nullptr dereference.
* spot/twaalgos/sbacc.cc: Work around spurious "maybe uninitialized"
warning.

spot/mc/unionfind.cc

@@ -50,6 +50,7 @@ namespace spot
   void int_unionfind::makeset(int e)
   {
     assert(e == (int) id.size());
+    (void)e;
     id.push_back(-1);
   }
 

spot/misc/common.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -71,6 +71,8 @@
 #if defined(SPOT_BUILD) or defined(SPOT_DEBUG)
   #define SPOT_ASSERT(x) spot_assert__(x)
 #else
+   // Do not replace by SPOT_ASSUME(x), as x can have some costly
+   // side-effects we do not want to pay outside of debug mode.
   #define SPOT_ASSERT(x) while (0)
 #endif
 
@@ -117,7 +119,7 @@
 #define SPOT_UNIMPLEMENTED() throw std::runtime_error("unimplemented");
 
 
-#if SPOT_DEBUG
+#if SPOT_DEBUG && !defined(NDEBUG)
 #define SPOT_ASSUME(cond) assert(cond)
 #else
 #define SPOT_ASSUME(cond)                       \

spot/twaalgos/aiger.cc

@@ -333,16 +333,19 @@ namespace spot
   void aig::unregister_lit_(unsigned v)
   {
     assert(((v&1) == 0) && "Expected positive form");
-    unsigned n_del;
+    unsigned n_del = bdd2var_.erase(var2bdd_[v].id());
-    n_del = bdd2var_.erase(var2bdd_[v].id());
     assert(n_del);
+    (void) n_del;
     n_del = var2bdd_.erase(v);
     assert(n_del);
+    (void) n_del;
     v = v ^ 1;
     n_del = bdd2var_.erase(var2bdd_[v].id());
     assert(n_del);
+    (void) n_del;
     n_del = var2bdd_.erase(v);
     assert(n_del);
+    (void) n_del;
   }
 
   // Get propositions that are commun to all
@@ -442,12 +445,12 @@ namespace spot
         std::copy(and_gates_.begin()+sf.second, and_gates_.end(),
                   gates.begin());
       }
-    // 1 Delete all literals
+    // 1. Delete all literals
     // max_var_old was used before
     // max_var_ is currently used
     for (unsigned v = sf.first + 2; v <= max_var_; v += 2)
       unregister_lit_(v);
-    // 2 Set back the gates
+    // 2. Set back the gates
     and_gates_.erase(and_gates_.begin() + sf.second, and_gates_.end());
     max_var_ = sf.first;
     return ss;
@@ -461,6 +464,7 @@ namespace spot
     assert(gates.size() == vardict.size());
     assert(sf.first == max_var_);
     assert(sf.second == and_gates_.size());
+    (void)sf;
     unsigned new_max_var_ = max_var_ + gates.size()*2;
     for (auto& p : vardict)
       {
@@ -970,6 +974,7 @@ namespace spot
               }
           }
         assert(n_occur_old == n_occur);
+        (void) n_occur_old;
       }
     // All products should now be created
     assert(std::all_of(needed_prods.cbegin(), needed_prods.cend(),
@@ -1027,6 +1032,7 @@ namespace spot
             }
           }
         assert(n_occur_old == n_occur);
+        (void) n_occur_old;
       }
   }
 
@@ -1082,9 +1088,10 @@ namespace spot
         return v - (1 + circ.num_inputs_ + circ.num_latches_);
       };
     auto& var2bdd = circ.var2bdd_;
+#ifndef NDEBUG
     auto& bdd2var = circ.bdd2var_;
-    std::function<bdd(unsigned)> get_gate_bdd;
+#endif
-    get_gate_bdd = [&](unsigned g)->bdd
+    auto get_gate_bdd = [&](unsigned g, auto self)->bdd
       {
         unsigned v = circ.gate_var(g);
         auto it = var2bdd.find(v);
@@ -1107,7 +1114,7 @@ namespace spot
           else
           {
             // Construct it
-            gsbdd[i] = get_gate_bdd(v2g(circ.aig_pos(gsv[i])));
+            gsbdd[i] = self(v2g(circ.aig_pos(gsv[i])), self);
             // Odd idx -> negate
             if (gsv[i]&1)
               gsbdd[i] = bdd_not(gsbdd[i]);
@@ -1121,7 +1128,7 @@ namespace spot
     // Also it should be consistent
     const unsigned n_gates = res_ptr->num_gates();
     for (unsigned g = 0; g < n_gates; ++g)
-      get_gate_bdd(g);
+      get_gate_bdd(g, get_gate_bdd);
     //Check that all outputs and next_latches exist
     auto check = [&var2bdd](unsigned v)
       {
@@ -1569,8 +1576,9 @@ namespace
         const auto& sn = state_numbers.at(i);
 
         auto latchoff = latch_offset[i];
+#ifndef NDEBUG
         auto latchoff_next = latch_offset.at(i+1);
-
+#endif
         auto alog2n = log2n[i];
         auto state2bdd = [&](auto s)
           {

spot/twaalgos/alternation.cc

@@ -252,10 +252,9 @@ namespace spot
 
       bdd state_as_bdd(unsigned s)
       {
-        auto p = state_as_bdd_cache_.emplace(s, bddfalse);
+        auto p = state_as_bdd_cache_.insert({s, bddfalse});
         if (!p.second)
           return p.first->second;
-
         bool marked = (int)s < 0;
         if (marked)
           s = ~s;

spot/twaalgos/ltl2taa.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2010, 2012-2016, 2018-2019 Laboratoire de
+// Copyright (C) 2009-2010, 2012-2016, 2018-2019, 2021 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -344,9 +344,11 @@ namespace spot
           pos[i] = vs[i].succ_.size();
 
         // g++ (Debian 8.3.0-3) 8.3.0 in --coverage mode,
-        // reports a "potential null pointer dereference" on the next
+        // and g++ 11.2.1-6 with -O3 -g -DNDEBUG
-        // line without this assert...
+        // both report a "potential null pointer dereference" on the
+        // while condition.
         assert(pos.size() > 0);
+        SPOT_ASSUME(pos.data());
         while (pos[0] != 0)
         {
           std::vector<formula> u; // Union

spot/twaalgos/mealy_machine.cc

@@ -3352,10 +3352,12 @@ namespace
           {
             return mmw->out(e.dst).begin()->cond;
           };
+#ifndef NDEBUG
         auto get_env_dst = [&](const auto& e)
           {
             return mmw->out(e.dst).begin()->dst;
           };
+#endif
 
         // The first two loops cover all env-edges
         for (unsigned group = 0; group < n_groups; ++group)
@@ -3617,6 +3619,7 @@ namespace spot
       throw std::runtime_error("right: Mealy machine must have an "
                                "environment controlled initial state.");
 
+#ifndef NDEBUG
     auto check_out = [](const const_twa_graph_ptr& aut,
                         const auto& sp)
       {
@@ -3635,7 +3638,7 @@ namespace spot
            "Left mealy machine has multiple or no player edges for a state");
     assert(check_out(right, spr) &&
            "Right mealy machine has multiple or no player edges for a state");
-
+#endif
     // Get for each env state of right the uncovered input letters
     std::vector<bdd> ucr(right->num_states(), bddtrue);
     const unsigned nsr = right->num_states();

spot/twaalgos/ndfs_result.hxx

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2018 Laboratoire de recherche
+// Copyright (C) 2011, 2013-2016, 2018, 2021 Laboratoire de recherche
 // et développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -462,7 +462,7 @@ namespace spot
                                     state_ptr_equal> m_source_trans;
 
     template<bool cycle>
-    class min_path: public bfs_steps
+    class min_path final: public bfs_steps
     {
     public:
       min_path(ars_statistics* ars,
@@ -486,10 +486,8 @@ namespace spot
       const state* search(const state* start, twa_run::steps& l)
       {
         const state* s = filter(start);
-        if (s)
+        SPOT_ASSERT(s);
         return this->bfs_steps::search(s, l);
-        else
-          return nullptr;
       }
 
       const state* filter(const state* s) override

spot/twaalgos/sbacc.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2018, 2021 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -55,7 +55,9 @@ namespace spot
     std::vector<acc_cond::mark_t> one_in(ns, acc_cond::mark_t({}));
     std::vector<bool> true_state(ns, false);
     acc_cond::mark_t true_state_acc = {};
-    unsigned true_state_last;
+    // Do not initialize true_state_last, but prevent GCC from warning
+    // about a possible uninitialized use later.
+    unsigned true_state_last = unsigned();
     for (auto& e: old->edges())
       for (unsigned d: old->univ_dests(e.dst))
         if (si.scc_of(e.src) == si.scc_of(d))
@@ -92,9 +94,12 @@ namespace spot
       [&](unsigned state, acc_cond::mark_t m) -> unsigned
       {
         bool ts = true_state[state];
-        if (ts)
+        if (ts) // Merge all true states.
           {
-            state = true_state_last; // Merge all true states.
+            // g++ 10.2 is afraid true_state_last might be
+            // uninitialized, however if ts==true, it means some true
+            // state were found, and the last true state is known.
+            state = true_state_last;
             m = {};
           }
         pair_t x(state, m);

spot/twaalgos/tau03.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2020  Laboratoire de Recherche et
+// Copyright (C) 2011, 2013-2021  Laboratoire de Recherche et
 // Developpement 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
@@ -305,12 +305,14 @@ namespace spot
           }
         acc_cond::mark_t get_acc() const
           {
-            SPOT_ASSUME(!is_white());
+            assert(!is_white());
+            SPOT_ASSUME(acc);
             return *acc;
           }
         void cumulate_acc(acc_cond::mark_t a)
           {
             assert(!is_white());
+            SPOT_ASSUME(acc);
             *acc |= a;
           }
         bool is_white() const

spot/twaalgos/tau03opt.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2019  Laboratoire de Recherche et
+// Copyright (C) 2011, 2013-2019, 2021  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
@@ -442,17 +442,20 @@ namespace spot
               }
             else
               {
+                SPOT_ASSUME(pc);
                 *pc=c;
               }
           }
         acc_cond::mark_t get_acc() const
           {
             assert(!is_white());
+            SPOT_ASSUME(acc);
             return *acc;
           }
         void cumulate_acc(acc_cond::mark_t a)
           {
             assert(!is_white());
+            SPOT_ASSUME(acc);
             *acc |= a;
           }
         bool is_white() const