diff --git a/NEWS b/NEWS index a1e2361f5..3b94d43ab 100644 --- a/NEWS +++ b/NEWS @@ -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, 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) Bugs fixed: diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 6419fc27a..06ddf0997 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -804,8 +804,23 @@ namespace spot return *dst_begin; SPOT_ASSERT(sz > 1); unsigned d = dests_.size(); - dests_.emplace_back(sz); - dests_.insert(dests_.end(), dst_begin, dst_end); + if (!dests_.empty() + && &*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 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; }