alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Fix warnings with GCC 7 on Centos 7

Browse source 
* spot/twa/twagraph.cc: Mark two variables as unused.
* spot/twaalgos/aiger.cc: Avoid spurious nullptr dereference warning,
and mark more variable as unused.
* spot/twaalgos/forq_contains.cc (word::operator==): Mark as
maybe_unused.
* bin/ltlsynt.cc, spot/twaalgos/relabel.cc,
spot/twaalgos/mealy_machine.cc, spot/twaalgos/synthesis.cc,
spot/twaalgos/zlktree.cc: Avoid unused variables warnings.
* spot/twaalgos/toparity.cc: Remove uses of std::optional, they were
not necessary, and they trigger spurious warnings in GCC 7.  Also
work around a spurious "potential nullptr deref".
* tests/core/twacube.cc: Fix another potential nullptr warning.
* spot/twaalgos/simulation.cc: Work a around GCC 6/7 bug.
This commit is contained in:
Alexandre Duret-Lutz 2023-10-15 00:21:12 +02:00
parent 1a2746e182
commit 75f3a5f2c5
11 changed files with 115 additions and 107 deletions
Download patch file Download diff file Expand all files Collapse all files

3
bin/ltlsynt.cc
View file

@ -447,8 +447,11 @@ namespace
{
robin_hood::unordered_set<spot::formula> removed_outputs;
for (auto [from, from_is_input, to] : rs->get_mapping())
{
(void) to;
if (!from_is_input)
removed_outputs.insert(from);
}
for (const std::string& apstr: output_aps)
{
spot::formula ap = spot::formula::ap(apstr);

2
spot/twa/twagraph.cc
View file

@ -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)

20
spot/twaalgos/aiger.cc
View file

@ -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<aig>(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)
{
(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();

1
spot/twaalgos/forq_contains.cc
View file

@ -797,6 +797,7 @@ namespace spot::forq
return temp;
}
[[maybe_unused]]
bool word::operator==(word const& other) const
{
return symbols == other.symbols;

5
spot/twaalgos/mealy_machine.cc
View file

@ -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)
{

8
spot/twaalgos/relabel.cc
View file

@ -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)

12
spot/twaalgos/simulation.cc
View file

@ -33,6 +33,14 @@
#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/cleanacc.hh>
// 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_<true>(aut);
}
} // End namespace spot.
#if __GNUC__ <= 7
#pragma GCC diagnostic pop
#endif

6
spot/twaalgos/synthesis.cc
View file

@ -1393,7 +1393,7 @@ namespace spot
std::swap(left_outs, right_outs);
}
auto [_, g_outs] = form2props.aps_of(f_g);
std::set<formula> 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<formula> 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<formula> 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))

102
spot/twaalgos/toparity.cc
View file

@ -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 <algorithm>
#include <deque>
#include <optional>
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<unsigned> min_color_used_;
std::optional<unsigned> max_color_scc_;
std::optional<unsigned> max_color_used_;
unsigned min_color_used_ = -1U;
unsigned max_color_scc_ = 0;
unsigned max_color_used_ = 0;
std::vector<unsigned> state_to_res_;
std::vector<unsigned> 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,23 +1464,22 @@ 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;
@ -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_));
}
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<std::vector<unsigned>>("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<std::vector<unsigned>>("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,12 +2359,12 @@ 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<unsigned>* orig_aut =
aut_->get_named_prop<std::vector<unsigned>>("original-states");
std::optional<std::vector<unsigned>> orig_st;
std::vector<unsigned> orig_st;
if (orig_aut)
{
orig_st.emplace(std::vector<unsigned>{*orig_aut});
orig_st = std::move(*orig_aut);
std::const_pointer_cast<twa_graph>(aut_)
->set_named_prop("original-states", nullptr);
}
@ -2406,9 +2379,9 @@ namespace spot
// 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,15 +2394,16 @@ 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())
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)
{

4
spot/twaalgos/zlktree.cc
View file

@ -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<bitvect> cur(make_bitvect(nstates));
for (const auto& [sz, bv, colors, minstate]: out)
{
(void) sz;
(void) colors;
(void) minstate;
cur->clear_all();

7
tests/core/twacube.cc
View file

@ -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<std::string>& 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);