Work around spurious g++-12 warnings
* spot/twaalgos/ltl2tgba_fm.cc, spot/tl/formula.hh, spot/twaalgos/translate.cc: Add SPOT_ASSUME in various places to help g++.
This commit is contained in:
parent
720c380412
commit
1248d326aa
3 changed files with 19 additions and 9 deletions
|
|
@ -294,7 +294,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
if (SPOT_UNLIKELY(i >= size()))
|
if (SPOT_UNLIKELY(i >= size()))
|
||||||
report_non_existing_child();
|
report_non_existing_child();
|
||||||
return children[i];
|
const fnode* c = children[i];
|
||||||
|
SPOT_ASSUME(c != nullptr);
|
||||||
|
return c;
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \see formula::ff
|
/// \see formula::ff
|
||||||
|
|
|
||||||
|
|
@ -1026,11 +1026,16 @@ namespace spot
|
||||||
bool coacc = false;
|
bool coacc = false;
|
||||||
auto& st = sm->states_of(n);
|
auto& st = sm->states_of(n);
|
||||||
for (auto l: st)
|
for (auto l: st)
|
||||||
if (namer->get_name(l).accepts_eword())
|
{
|
||||||
|
formula lf = namer->get_name(l);
|
||||||
|
// Somehow gcc 12.2.0 thinks lf can be nullptr.
|
||||||
|
SPOT_ASSUME(lf != nullptr);
|
||||||
|
if (lf.accepts_eword())
|
||||||
{
|
{
|
||||||
coacc = true;
|
coacc = true;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
}
|
||||||
if (!coacc)
|
if (!coacc)
|
||||||
{
|
{
|
||||||
// ... or if any of its successors is coaccessible.
|
// ... or if any of its successors is coaccessible.
|
||||||
|
|
|
||||||
|
|
@ -210,6 +210,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
auto safety = [](formula f)
|
auto safety = [](formula f)
|
||||||
{
|
{
|
||||||
|
// Prevent gcc 12.2.0 from warning us that f could be a
|
||||||
|
// nullptr formula.
|
||||||
|
SPOT_ASSUME(f != nullptr);
|
||||||
return f.is_syntactic_safety();
|
return f.is_syntactic_safety();
|
||||||
};
|
};
|
||||||
auto i = std::remove_if(oblg.begin(), oblg.end(), safety);
|
auto i = std::remove_if(oblg.begin(), oblg.end(), safety);
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue