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

fix invalid iterator handling, reported by -D_GLIBCXX_DEBUG

Browse source 
* spot/tl/unabbrev.cc, spot/twa/twagraph.cc,
spot/twaalgos/complement.cc: Here.  All of these caused
test suite failure with -D_GLIBCXX_DEBUG.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-14 23:24:13 +02:00
parent 4d2922eafa
commit 306eca8ce1
3 changed files with 23 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/tl/unabbrev.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2018-2019 Laboratoire de Recherche et // Copyright (C) 2015, 2018-2020 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -276,7 +276,9 @@ namespace spot
break; break;
} }
} }
return entry.first->second = out; // The recursion may have invalidated the "entry" iterator, so do
// not reuse it.
return cache_[in] = out;
} }
formula unabbreviate(formula in, const char* opt) formula unabbreviate(formula in, const char* opt)

8
spot/twa/twagraph.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement // Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
// de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -964,7 +964,7 @@ namespace spot
// States already seen. // States already seen.
state_map<unsigned> seen; state_map<unsigned> seen;
// States to process // States to process
std::deque<state_map<unsigned>::const_iterator> todo; std::deque<state_map<unsigned>::value_type> todo;
auto new_state = [&](const state* s) -> unsigned auto new_state = [&](const state* s) -> unsigned
{ {
@ -972,7 +972,7 @@ namespace spot
if (p.second) if (p.second)
{ {
p.first->second = out->new_state(); p.first->second = out->new_state();
todo.emplace_back(p.first); todo.emplace_back(*p.first);
if (names) if (names)
names->emplace_back(aut->format_state(s)); names->emplace_back(aut->format_state(s));
if (ohstates) if (ohstates)
@ -994,7 +994,7 @@ namespace spot
{ {
const state* src1; const state* src1;
unsigned src2; unsigned src2;
std::tie(src1, src2) = *todo.front(); std::tie(src1, src2) = todo.front();
todo.pop_front(); todo.pop_front();
for (auto* t: aut->succ(src1)) for (auto* t: aut->succ(src1))
{ {

27
spot/twaalgos/complement.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013-2015, 2017-2019 Laboratoire de Recherche et // Copyright (C) 2013-2015, 2017-2020 Laboratoire de Recherche et
// Développement de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -260,19 +260,22 @@ namespace spot
} }
else // state stays in check else // state stays in check
{ {
// remove states that should stay in s (ncsb_s),
// and mark the other as ncsb_c.
// The first two loops form a kind of remove_if()
// that set the non-removed states to ncsb_c.
auto it = succs.begin(); auto it = succs.begin();
while (it != succs.end()) auto end = succs.end();
{ for (; it != end; ++it)
// remove state if it should stay in s if ((*it)[t.dst] != ncsb_s)
if ((*it)[t.dst] == ncsb_s)
{
std::iter_swap(it, succs.end() - 1);
succs.pop_back();
continue;
}
(*it)[t.dst] = ncsb_c; (*it)[t.dst] = ncsb_c;
++it; else
} break;
if (it != end)
for (auto it2 = it; ++it2 != end;)
if ((*it2)[t.dst] != ncsb_s)
*it++ = std::move(*it2);
succs.erase(it, end);
} }
// No need to look for other compatible transitions // No need to look for other compatible transitions
// for this state; it's in the deterministic part of // for this state; it's in the deterministic part of