From 306eca8ce13cf44e8313c522447d737d9d994fe9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 14 Apr 2020 23:24:13 +0200
Subject: [PATCH] fix invalid iterator handling, reported by -D_GLIBCXX_DEBUG

* spot/tl/unabbrev.cc, spot/twa/twagraph.cc,
spot/twaalgos/complement.cc: Here.  All of these caused
test suite failure with -D_GLIBCXX_DEBUG.
---
 spot/tl/unabbrev.cc         |  6 ++++--
 spot/twa/twagraph.cc        |  8 ++++----
 spot/twaalgos/complement.cc | 27 +++++++++++++++------------
 3 files changed, 23 insertions(+), 18 deletions(-)

diff --git a/spot/tl/unabbrev.cc b/spot/tl/unabbrev.cc
index fba2aec8f..1df1334a3 100644
--- a/spot/tl/unabbrev.cc
+++ b/spot/tl/unabbrev.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2018-2019 Laboratoire de Recherche et
+// Copyright (C) 2015, 2018-2020 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -276,7 +276,9 @@ namespace spot
           break;
         }
       }
-    return entry.first->second = out;
+    // The recursion may have invalidated the "entry" iterator, so do
+    // not reuse it.
+    return cache_[in] = out;
   }
 
   formula unabbreviate(formula in, const char* opt)
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index 37d6f7c5b..3102ea23d 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -964,7 +964,7 @@ namespace spot
       // States already seen.
       state_map<unsigned> seen;
       // States to process
-      std::deque<state_map<unsigned>::const_iterator> todo;
+      std::deque<state_map<unsigned>::value_type> todo;
 
       auto new_state = [&](const state* s) -> unsigned
         {
@@ -972,7 +972,7 @@ namespace spot
           if (p.second)
             {
               p.first->second = out->new_state();
-              todo.emplace_back(p.first);
+              todo.emplace_back(*p.first);
               if (names)
                 names->emplace_back(aut->format_state(s));
               if (ohstates)
@@ -994,7 +994,7 @@ namespace spot
         {
           const state* src1;
           unsigned src2;
-          std::tie(src1, src2) = *todo.front();
+          std::tie(src1, src2) = todo.front();
           todo.pop_front();
           for (auto* t: aut->succ(src1))
             {
diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc
index d2664ff31..9cbe7d138 100644
--- a/spot/twaalgos/complement.cc
+++ b/spot/twaalgos/complement.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2015, 2017-2019 Laboratoire de Recherche et
+// Copyright (C) 2013-2015, 2017-2020 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -260,19 +260,22 @@ namespace spot
                   }
                 else       // state stays in check
                   {
+                    // remove states that should stay in s (ncsb_s),
+                    // and mark the other as ncsb_c.
+                    // The first two loops form a kind of remove_if()
+                    // that set the non-removed states to ncsb_c.
                     auto it = succs.begin();
-                    while (it != succs.end())
-                      {
-                        // remove state if it should stay in s
-                        if ((*it)[t.dst] == ncsb_s)
-                          {
-                            std::iter_swap(it, succs.end() - 1);
-                            succs.pop_back();
-                            continue;
-                          }
+                    auto end = succs.end();
+                    for (; it != end; ++it)
+                      if ((*it)[t.dst] != ncsb_s)
                         (*it)[t.dst] = ncsb_c;
-                        ++it;
-                      }
+                      else
+                        break;
+                    if (it != end)
+                      for (auto it2 = it; ++it2 != end;)
+                        if ((*it2)[t.dst] != ncsb_s)
+                          *it++ = std::move(*it2);
+                    succs.erase(it, end);
                   }
                 // No need to look for other compatible transitions
                 // for this state; it's in the deterministic part of