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

graph: fix creation of universal edge

Browse source 
* spot/graph/graph.hh: Use a temporary array to store the destination
vector if the passed range belong to the dests_ vector.  Otherwise the
passed begin/end risk being invalidated when dests_ is reallocated.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2022-06-23 15:52:24 +02:00
parent 288b1c7958
commit 166a26417c
2 changed files with 24 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -113,6 +113,13 @@ New in spot 2.10.6.dev (not yet released)
to obtain a simple model checker (that returns true or false, to obtain a simple model checker (that returns true or false,
without counterexample). without counterexample).
Bugs fixed:
- calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could
produce unexpected result if begin and end where already pointing
into the universal edge vector, since the later can be
reallocated during that process.
New in spot 2.10.6 (2022-05-18) New in spot 2.10.6 (2022-05-18)
Bugs fixed: Bugs fixed:

19
spot/graph/graph.hh
View file

@ -804,8 +804,23 @@ namespace spot
return *dst_begin; return *dst_begin;
SPOT_ASSERT(sz > 1); SPOT_ASSERT(sz > 1);
unsigned d = dests_.size(); unsigned d = dests_.size();
dests_.emplace_back(sz); if (!dests_.empty()
dests_.insert(dests_.end(), dst_begin, dst_end); && &*dst_begin >= &dests_.front()
&& &*dst_begin <= &dests_.back()
&& (dests_.capacity() - dests_.size()) < (sz + 1))
{
// If dst_begin...dst_end points into dests_ and dests_ risk
// being reallocated, we have to savea the destination
// states before we lose them.
std::vector<unsigned> tmp(dst_begin, dst_end);
dests_.emplace_back(sz);
dests_.insert(dests_.end(), tmp.begin(), tmp.end());
}
else
{
dests_.emplace_back(sz);
dests_.insert(dests_.end(), dst_begin, dst_end);
}
return ~d; return ~d;
} }