diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 0ff44625d..fb24a4e6b 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -447,8 +447,11 @@ namespace { robin_hood::unordered_set removed_outputs; for (auto [from, from_is_input, to] : rs->get_mapping()) - if (!from_is_input) - removed_outputs.insert(from); + { + (void) to; + if (!from_is_input) + removed_outputs.insert(from); + } for (const std::string& apstr: output_aps) { spot::formula ap = spot::formula::ap(apstr); diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 50145803d..e7a875680 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -531,7 +531,9 @@ namespace spot }; auto [i1, nsl1, sl1, e1] = e_idx[s1]; + (void) nsl1; auto [i2, nsl2, sl2, e2] = e_idx[s2]; + (void) nsl2; unsigned n_trans = e1 - i1; if ((e2 - i2) != n_trans) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 49ac54997..df3d05bdb 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -509,6 +509,7 @@ namespace spot { // Do some check_ups auto& [gates, vardict, _] = ss; + (void)_; trace << "Reapplying sf: " << sf.first << "; " << sf.second << "\nwith " << gates.size() << " additional gates.\n\n"; assert(gates.size() == vardict.size()); @@ -993,6 +994,7 @@ namespace spot { auto [it, ins] = occur_map.try_emplace({term[i], term[j]} , 0); + (void)ins; it->second += 1; } }; @@ -1169,12 +1171,14 @@ namespace spot aig_ptr res_ptr = std::make_shared(in_names__, out_names__, next_latches__.size(), dict); + // For some reason g++-7 thinks res_ptr could be null. + SPOT_ASSUME(res_ptr); aig& circ = *res_ptr; - res_ptr->max_var_ = + circ.max_var_ = (in_names__.size() + next_latches__.size() + gates__.size())*2; - std::swap(res_ptr->next_latches_, next_latches__); - std::swap(res_ptr->outputs_, outputs__); - std::swap(res_ptr->and_gates_, gates__); + std::swap(circ.next_latches_, next_latches__); + std::swap(circ.outputs_, outputs__); + std::swap(circ.and_gates_, gates__); // Create all the bdds/vars // true/false/latches/inputs already exist @@ -1520,7 +1524,10 @@ namespace { // We do not care about an output if it does not appear in the bdd for (auto& [_, dc_v] : out_dc_vec) - dc_v = true; + { + (void) _; + dc_v = true; + } v.clear(); while (b != bddtrue) { @@ -1591,8 +1598,8 @@ namespace if (bdd_implies(all_outputs, b)) // ap is an output AP { output_names.push_back(ap.ap_name()); - auto [it, inserted] = bddvar_to_num.try_emplace(bddvar, - i_out++); + bool inserted = bddvar_to_num.try_emplace(bddvar, + i_out++).second; if (SPOT_UNLIKELY(!inserted)) throw std::runtime_error("Intersecting outputs"); } @@ -1629,6 +1636,7 @@ namespace // there. for (auto [k, k_is_input, v]: rs->get_mapping()) { + (void) v; if (k_is_input) continue; const std::string s = k.ap_name(); diff --git a/spot/twaalgos/forq_contains.cc b/spot/twaalgos/forq_contains.cc index 6292dbe76..1e397106f 100644 --- a/spot/twaalgos/forq_contains.cc +++ b/spot/twaalgos/forq_contains.cc @@ -797,6 +797,7 @@ namespace spot::forq return temp; } + [[maybe_unused]] bool word::operator==(word const& other) const { return symbols == other.symbols; diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 25bab05a9..fc36a42f1 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -1326,6 +1326,8 @@ namespace if (inserted) trace << "Register oc " << it->first << ", " << it->second << " for state " << s1 << '\n'; +#else + (void)inserted; #endif } // Are two player condition ids states incompatible @@ -1952,6 +1954,7 @@ namespace // construction of the sat-problem latter on depends on it for (auto&& [id, pv] : sim_map) { + (void)id; // We want front (the representative) to be the smallest std::sort(pv.second.begin(), pv.second.end()); bs.emplace_back(std::move(pv.second)); @@ -2562,6 +2565,7 @@ namespace picosat_push(lm.psat_); for (auto& [_, clause] : state_cover_clauses) { + (void)_; // Clause is not nullterminated! clause.push_back(0); picosat_add_lits(lm.psat_, clause.data()); @@ -3278,6 +3282,7 @@ namespace bdd repr = red.minimal_letters_vec[group][idx]; const auto& [_, repr_letters] = red.minimal_letters[group].at(repr); + (void)_; // The class of letters is the first set for (int id : repr_letters) { diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index ba5e4ed14..2ba9e7d52 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2015-2018, 2020, 2022, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -184,9 +184,7 @@ namespace spot continue; } - auto [_, ins] = - all_cond_id2idx.try_emplace(e.cond.id(), all_cond.size()); - if (ins) + if (all_cond_id2idx.try_emplace(e.cond.id(), all_cond.size()).second) { all_cond.push_back(e.cond); if (all_cond.size() > max_letter) diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index ed53929b3..404a8eebc 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -33,6 +33,14 @@ #include #include +// Work around GCC bug 80947 (dominates_edge is causing spurious +// visibility warnings) +#if __GNUC__ <= 7 +#pragma GCC diagnostic push +#pragma GCC diagnostic ignored "-Wattributes" +#endif + + // Simulation-based reduction, implemented using bdd-based signatures. // // The signature of a state is a Boolean function (implemented as a @@ -1554,3 +1562,7 @@ namespace spot return reduce_iterated_(aut); } } // End namespace spot. + +#if __GNUC__ <= 7 +#pragma GCC diagnostic pop +#endif diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index aef11d27b..0aff98880 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1393,7 +1393,7 @@ namespace spot std::swap(left_outs, right_outs); } - auto [_, g_outs] = form2props.aps_of(f_g); + std::set g_outs = form2props.aps_of(f_g).second; if (are_intersecting(g_outs, right_outs)) return ret_sol_maybe(); @@ -1480,7 +1480,7 @@ namespace spot auto res = make_twa_graph(dict); bdd output_bdd = bddtrue; - auto [ins_f, _] = form2props.aps_of(f_g); + std::set ins_f = form2props.aps_of(f_g).first; for (auto &out : output_aps) output_bdd &= bdd_ithvar(res->register_ap(out)); @@ -1697,7 +1697,7 @@ namespace // anonymous for subsformula continue; done_ass[i] = true; auto &ass = assumptions_split[i]; - auto [left_aps, right_aps] = form2props.aps_of(ass); + std::set left_aps = form2props.aps_of(ass).first; // If an assumption hasn't any decRelProp, it is considered as // a free assumption. if (!are_intersecting(left_aps, decRelProps_ins)) diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index a82c7d57a..7abec3e15 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2018-2020, 2022 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2018-2020, 2022-2023 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -31,7 +31,6 @@ #include #include -#include namespace std { @@ -288,6 +287,8 @@ namespace spot was_able_to_color, max_color)) { auto res = make_twa_graph(aut, twa::prop_set::all()); + // GCC 7 warns about potential null pointer dereference. + SPOT_ASSUME(res); auto &res_vector = res->edge_vector(); unsigned rv_size = res_vector.size(); for (unsigned i = 1; i < rv_size; ++i) @@ -796,9 +797,9 @@ namespace spot // Tells if we are constructing a parity max odd bool is_odd_ = false; // min_color used in the automaton + 1 (result of max_set). - std::optional min_color_used_; - std::optional max_color_scc_; - std::optional max_color_used_; + unsigned min_color_used_ = -1U; + unsigned max_color_scc_ = 0; + unsigned max_color_used_ = 0; std::vector state_to_res_; std::vector res_to_aut_; // Map a state of aut_ to every copy of this state. Used by a recursive call @@ -976,7 +977,7 @@ namespace spot edge_cache = nullptr) { // In a parity automaton we just need the maximal value - auto simax = mark.max_set(); + unsigned simax = mark.max_set(); const bool need_cache = edge_cache != nullptr && can_merge_edge; long long key = 0; @@ -999,24 +1000,9 @@ namespace spot assert(res_src != -1U); assert(res_dst != -1U); - // No edge already done in the current scc. - if (!max_color_scc_.has_value()) - max_color_scc_.emplace(simax); - else - max_color_scc_.emplace(std::max(*max_color_scc_, simax)); - - // If it is the first edge of the result - if (!min_color_used_.has_value()) - { - assert(!max_color_used_.has_value()); - max_color_used_.emplace(simax); - min_color_used_.emplace(simax); - } - else - { - min_color_used_.emplace(std::min(*min_color_used_, simax)); - max_color_used_.emplace(std::max(*max_color_used_, simax)); - } + max_color_scc_ = std::max(max_color_scc_, simax); + min_color_used_ = std::min(min_color_used_, simax); + max_color_used_ = std::max(max_color_used_, simax); auto new_edge_num = res_->new_edge(res_src, res_dst, cond, simplified); if (need_cache) @@ -1478,31 +1464,30 @@ namespace spot return; is_odd_ = true; // We can reduce if we don't have an edge without color. - bool can_reduce = (min_color_used_.has_value() && *min_color_used_ != 0); + bool can_reduce = (min_color_used_ != -1U) && (min_color_used_ != 0); int shift; if (can_reduce) - shift = -1 * (*min_color_used_ - (*min_color_used_ % 2) + 1); + shift = - (min_color_used_ | 1); else shift = 1; // If we cannot decrease and we already the the maximum color, we don't // have to try. Constructs a mark_t to avoid to make report_too_many_sets // public. - if (!can_reduce && max_color_used_.value_or(-1) + shift == MAX_ACCSETS) + if (!can_reduce && max_color_used_ + shift >= MAX_ACCSETS) acc_cond::mark_t {SPOT_MAX_ACCSETS}; - if (max_color_used_.has_value()) - *max_color_used_ += shift; - if (min_color_used_.has_value()) - *min_color_used_ += shift; + max_color_used_ += shift; + if (min_color_used_ < -1U) + min_color_used_ += shift; for (auto &e : res_->edges()) - { - auto new_val = e.acc.max_set() - 1 + shift; - if (new_val != -1U) - e.acc = { new_val }; - else - e.acc = {}; - } + { + auto new_val = e.acc.max_set() - 1 + shift; + if (new_val != -1U) + e.acc = { new_val }; + else + e.acc = {}; + } } template @@ -1877,29 +1862,22 @@ namespace spot bool old_pp_gen = opt_.parity_prefix_general; opt_.parity_prefix_general = false; - auto max_scc_color_rec = max_color_scc_; + unsigned max_scc_color_rec = max_color_scc_; for (auto x : sub.split_aut({removed_cols})) - { - x->set_acceptance(new_cond); - process_scc(x, algorithm::PARITY_PREFIX); - if (max_color_scc_.has_value()) { - if (!max_scc_color_rec.has_value()) - max_scc_color_rec.emplace(*max_color_scc_); - else - max_scc_color_rec.emplace( - std::max(*max_scc_color_rec, *max_color_scc_)); + x->set_acceptance(new_cond); + process_scc(x, algorithm::PARITY_PREFIX); + max_scc_color_rec = std::max(max_scc_color_rec, max_color_scc_); } - } opt_.parity_prefix = true; opt_.parity_prefix_general = old_pp_gen; - assert(max_scc_color_rec.has_value()); - auto max_used_is_accepting = ((*max_scc_color_rec - 1) % 2) == is_odd_; + assert(max_scc_color_rec > 0); + bool max_used_is_accepting = ((max_scc_color_rec - 1) % 2) == is_odd_; bool last_prefix_acc = (prefixes.size() % 2) != first_is_accepting; unsigned m = prefixes.size() + (max_used_is_accepting != last_prefix_acc) - + *max_scc_color_rec - 1; + + max_scc_color_rec - 1; auto sub_aut_orig = sub_aut->get_named_prop>("original-states"); assert(sub_aut_orig); @@ -1914,8 +1892,7 @@ namespace spot const unsigned col = m - pos; // As it is a parity prefix we should never get a lower value than // the color recursively produced. - assert(!max_scc_color_rec.has_value() || *max_scc_color_rec == 0 - || col + 1 > *max_scc_color_rec); + assert(col >= max_scc_color_rec); unsigned dst = state_to_res_[(*sub_aut_orig)[e.dst]]; for (auto src : (*state_to_nums_)[(*sub_aut_orig)[e.src]]) if (col != -1U) @@ -2003,7 +1980,7 @@ namespace spot bool old_pp = opt_.parity_prefix; opt_.parity_prefix = false; - auto max_scc_color_rec = max_color_scc_; + unsigned max_scc_color_rec = max_color_scc_; scc_info lower_scc(sub_aut, scc_info_options::TRACK_STATES); scc_info_to_parity sub(lower_scc, keep); state_to_nums_ = @@ -2011,11 +1988,7 @@ namespace spot for (auto x : sub.split_aut(keep)) { process_scc(x, algorithm::PARITY_PREFIX_GENERAL); - if (!max_scc_color_rec.has_value()) - max_scc_color_rec = max_color_scc_; - else if (max_color_scc_.has_value()) - max_scc_color_rec.emplace( - std::max(*max_scc_color_rec, *max_color_scc_)); + max_scc_color_rec = std::max(max_scc_color_rec, max_color_scc_); } // restore options @@ -2043,11 +2016,11 @@ namespace spot const bool min_prefix_accepting = (min_set_prefix % 2) == start_inf; // max_scc_color_rec has a value as the automaton is not parity-type, // so there was a recursive paritisation - assert(max_scc_color_rec.has_value()); - const bool max_rec_accepting = ((*max_scc_color_rec - 1) % 2) == is_odd_; + assert(max_scc_color_rec > 0); + const bool max_rec_accepting = ((max_scc_color_rec - 1) % 2) == is_odd_; const bool same_prio = min_prefix_accepting == max_rec_accepting; const unsigned delta = - min_set_prefix - (*max_scc_color_rec + 1) - !same_prio; + min_set_prefix - (max_scc_color_rec + 1) - !same_prio; auto sub_aut_orig = sub_aut->get_named_prop>("original-states"); @@ -2248,7 +2221,7 @@ namespace spot const algorithm none_algo = algorithm::NONE) { // Init the maximal color produced when processing this SCC. - max_color_scc_.reset(); + max_color_scc_ = 0; // If the sub_automaton is "empty", we don't need to apply an algorithm. if (sub_aut->num_edges() == 0) { @@ -2386,29 +2359,29 @@ namespace spot res_ = make_twa_graph(aut_->get_dict()); res_->copy_ap_of(aut_); const unsigned num_scc = si_.scc_count(); - auto orig_aut = + std::vector* orig_aut = aut_->get_named_prop>("original-states"); - std::optional> orig_st; + std::vector orig_st; if (orig_aut) - { - orig_st.emplace(std::vector{*orig_aut}); - std::const_pointer_cast(aut_) - ->set_named_prop("original-states", nullptr); - } + { + orig_st = std::move(*orig_aut); + std::const_pointer_cast(aut_) + ->set_named_prop("original-states", nullptr); + } auto sccs = si_.split_aut(); for (unsigned scc = 0; scc < num_scc; ++scc) - { - auto sub_automaton = sccs[scc]; - process_scc(sub_automaton); - } + { + auto sub_automaton = sccs[scc]; + process_scc(sub_automaton); + } link_sccs(); // During the execution, to_parity works on its own // original-states and we must combine it with the property original // states of aut_ to propagate the information. - if (orig_st) + if (orig_aut) for (unsigned i = 0; i < orig_->size(); ++i) - (*orig_)[i] = (*orig_aut)[(*orig_)[i]]; + (*orig_)[i] = orig_st[(*orig_)[i]]; res_->set_named_prop("original-states", orig_); if (opt_.pretty_print) res_->set_named_prop("state-names", names_); @@ -2421,16 +2394,17 @@ namespace spot res_->purge_unreachable_states(); // A special case is an automaton without edge. It implies // max_color_used_ has not value so we need to test it. - if (!max_color_used_.has_value()) - { - assert(aut_->num_edges() == 0); - res_->set_acceptance(acc_cond(acc_cond::acc_code::f())); - } + if (max_color_used_ == 0) + { + assert(aut_->num_edges() == 0); + res_->set_acceptance(acc_cond(acc_cond::acc_code::f())); + } else - { - res_->set_acceptance(acc_cond( - acc_cond::acc_code::parity(true, is_odd_, *max_color_used_))); - } + { + res_->set_acceptance(acc_cond(acc_cond::acc_code:: + parity(true, is_odd_, + max_color_used_))); + } if (opt_.datas) { constexpr std::array diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index f31c46896..da6a5e208 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2021, 2022 Laboratoire de Recherche et Developpement de +// Copyright (C) 2021, 2022, 2023 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -669,6 +669,7 @@ namespace spot // seen_dup. for (auto& [sz, bv, colors, minstate]: out) { + (void) sz; (void) colors; (void) minstate; seen_src->clear_all(); // local source of the node @@ -735,6 +736,7 @@ namespace spot std::unique_ptr cur(make_bitvect(nstates)); for (const auto& [sz, bv, colors, minstate]: out) { + (void) sz; (void) colors; (void) minstate; cur->clear_all(); diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc index 31eeaed69..1a2cd73a8 100644 --- a/tests/core/twacube.cc +++ b/tests/core/twacube.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2018, 2020 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2018, 2020, 2023 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -78,7 +78,10 @@ int main() const std::vector& aps = aut->ap(); unsigned int seed = 17; - for (auto it = aut->succ(2); !it->done(); it->next()) + auto it = aut->succ(2); + SPOT_ASSUME(it); // GCC 7 warns about potential nullptr. + for (; !it->done(); it->next()) + for (; !it->done(); it->next()) { auto& t = aut->trans_storage(it, seed); auto& d = aut->trans_data(it, seed);