From 166a26417c10e1a97f834b384c2e700b6efc5505 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 23 Jun 2022 15:52:24 +0200 Subject: [PATCH] graph: fix creation of universal edge * 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. --- NEWS | 7 +++++++ spot/graph/graph.hh | 19 +++++++++++++++++-- 2 files changed, 24 insertions(+), 2 deletions(-) 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; }