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

graph: fix invalid read

Browse source 
Reported by Florian Renkin.

* spot/graph/graph.hh (sort_edges_of): Fix invalid read when sorting a
state without successor.  Seen on core/tgbagraph.test.
This commit is contained in:
Alexandre Duret-Lutz 2022-03-22 12:18:25 +01:00
parent bb7072402a
commit 3ed337ec46
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
spot/graph/graph.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et // Copyright (C) 2014-2018, 2020-2022 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.
@ -1243,14 +1243,19 @@ namespace spot
//dump_storage(std::cerr); //dump_storage(std::cerr);
auto pi = [&](unsigned t1, unsigned t2) auto pi = [&](unsigned t1, unsigned t2)
{return p(edges_[t1], edges_[t2]); }; {return p(edges_[t1], edges_[t2]); };
// Sort the outgoing edges of each selected state according
// to predicate p. Do that in place.
std::vector<unsigned> sort_idx_; std::vector<unsigned> sort_idx_;
for (unsigned i = 0; i < num_states(); ++i) unsigned ns = num_states();
for (unsigned i = 0; i < ns; ++i)
{ {
if (to_sort_ptr && !(*to_sort_ptr)[i]) if (to_sort_ptr && !(*to_sort_ptr)[i])
continue; continue;
sort_idx_.clear();
unsigned t = states_[i].succ; unsigned t = states_[i].succ;
if (t == 0)
continue;
sort_idx_.clear();
do do
{ {
sort_idx_.push_back(t); sort_idx_.push_back(t);