From 4710577dfe17f4a0cd09b3c340aaeb46e05b68ae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 16 Sep 2021 22:52:43 +0200 Subject: [PATCH] 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 | 1 + spot/misc/common.hh | 6 ++++-- spot/twaalgos/aiger.cc | 30 +++++++++++++++++++----------- spot/twaalgos/alternation.cc | 3 +-- spot/twaalgos/ltl2taa.cc | 8 +++++--- spot/twaalgos/mealy_machine.cc | 5 ++++- spot/twaalgos/ndfs_result.hxx | 10 ++++------ spot/twaalgos/sbacc.cc | 13 +++++++++---- spot/twaalgos/tau03.cc | 6 ++++-- spot/twaalgos/tau03opt.cc | 5 ++++- 10 files changed, 55 insertions(+), 32 deletions(-) diff --git a/spot/mc/unionfind.cc b/spot/mc/unionfind.cc index de4921055..2193d2080 100644 --- a/spot/mc/unionfind.cc +++ b/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); } diff --git a/spot/misc/common.hh b/spot/misc/common.hh index 9d8b58ef9..e38f9f15a 100644 --- a/spot/misc/common.hh +++ b/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) \ diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 6b52ee542..bb90c54a0 100644 --- a/spot/twaalgos/aiger.cc +++ b/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; - n_del = bdd2var_.erase(var2bdd_[v].id()); + unsigned 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,13 +445,13 @@ 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) + for (unsigned v = sf.first + 2; v <= max_var_; v += 2) unregister_lit_(v); - // 2 Set back the gates - and_gates_.erase(and_gates_.begin()+sf.second, and_gates_.end()); + // 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 get_gate_bdd; - get_gate_bdd = [&](unsigned g)->bdd +#endif + 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) { diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 5a4ef668a..a3762f9b0 100644 --- a/spot/twaalgos/alternation.cc +++ b/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; diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc index 5cf779c2e..9c10777a9 100644 --- a/spot/twaalgos/ltl2taa.cc +++ b/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 - // line without this assert... + // and g++ 11.2.1-6 with -O3 -g -DNDEBUG + // 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 u; // Union diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index a056dfe6d..b837a436f 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/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 ucr(right->num_states(), bddtrue); const unsigned nsr = right->num_states(); diff --git a/spot/twaalgos/ndfs_result.hxx b/spot/twaalgos/ndfs_result.hxx index bc0c7f3f1..2e17fc3fa 100644 --- a/spot/twaalgos/ndfs_result.hxx +++ b/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 - 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) - return this->bfs_steps::search(s, l); - else - return nullptr; + SPOT_ASSERT(s); + return this->bfs_steps::search(s, l); } const state* filter(const state* s) override diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 52f9e7b63..c2db036ca 100644 --- a/spot/twaalgos/sbacc.cc +++ b/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 one_in(ns, acc_cond::mark_t({})); std::vector 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); diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index 1fef18fe9..a67001874 100644 --- a/spot/twaalgos/tau03.cc +++ b/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 diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index e1c4e5885..831211764 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/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