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

work around a null pointer dereference error

Browse source 
This fixes #462.

* spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Replace the
redirect_src vector by a unique_ptr<unsigned[]>.  Not only does this
remove the false positive diagnostic, but it also removes the unneeded
default initialization of the elements of that vector.
This commit is contained in:
Alexandre Duret-Lutz 2021-06-21 11:42:36 +02:00
parent ba0c8e8a29
commit 7c5f81e3bb
1 changed files with 21 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

36
spot/twaalgos/gfguarantee.cc
View file

@ -188,13 +188,18 @@ namespace spot
unsigned new_init = -1U; unsigned new_init = -1U;
// We do two the rewrite in two passes. The first one // We do two the rewrite in two passes. The first one
// replays histories to detect the new source the edges // replays histories to detect the new source the edges
// should synchronize with. We used to have single // should synchronize with. The second pass do the actual
// loop, but replaying history on edges that have been modified // rewrite. We used to have single loop, but replaying
// result in different automaton depending on the edge order. // history on edges that have been modified results in
std::vector<unsigned> redirect_src; // different automata depending on the edge order.
std::unique_ptr<unsigned[]> redirect_src;
if (is_det) if (is_det)
{ {
redirect_src.resize(aut->edge_vector().size()); // We use a unique_ptr instead of a resized vector to
// avoid default initializing all values. Doing so
// also removes an incorrect "null pointer dereference"
// diagnostic from g++ 11.0 (see issue #462).
redirect_src.reset(new unsigned[aut->edge_vector().size()]);
for (auto& e: aut->edges()) for (auto& e: aut->edges())
{ {
unsigned edge = aut->edge_number(e); unsigned edge = aut->edge_number(e);
@ -268,7 +273,7 @@ namespace spot
} }
} }
// No we do the redirections. // Now we do the redirections.
// We will modify most of the edges in place, but some cases // We will modify most of the edges in place, but some cases
// require the addition of new edges. However we cannot add // require the addition of new edges. However we cannot add
@ -311,10 +316,10 @@ namespace spot
new_init = init; new_init = init;
continue; continue;
} }
// If initial state cannot be reached from another // If the initial state cannot be reached from
// state of the automaton, we can get rid of it by // another state of the automaton, we can get rid of
// combining the edge reaching the terminal state // it by combining the edge reaching the terminal
// with the edges leaving the initial state. // state with the edges leaving the initial state.
// //
// However if we have some histories for e.src // However if we have some histories for e.src
// (which implies that the automaton is // (which implies that the automaton is
@ -323,11 +328,12 @@ namespace spot
// //
// One problem with those histories, is that we do // One problem with those histories, is that we do
// not know how much of it to replay. It's possible // not know how much of it to replay. It's possible
// that we cannot find a matching transition (e.g. if // that we cannot find a matching transition
// the history if "b" but the choices are "!a" or "a"), // (e.g. if the history if "b" but the choices are
// and its also possible to that playing too much of // "!a" or "a"), and it's also possible that playing
// history will get us back the terminal state. In both // too much of history will get us back the terminal
// cases, we should try again with a smaller history. // state. In both cases, we should try again with a
// smaller history.
unsigned moved_init = init; unsigned moved_init = init;
bdd econd = e.cond; bdd econd = e.cond;
bool first; bool first;