From 1248d326aaa03debb539db2ae34693f01553233b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 8 Dec 2022 17:27:32 +0100
Subject: [PATCH] Work around spurious g++-12 warnings

* spot/twaalgos/ltl2tgba_fm.cc, spot/tl/formula.hh,
spot/twaalgos/translate.cc: Add SPOT_ASSUME in various places to help
g++.
---
 spot/tl/formula.hh           |  4 +++-
 spot/twaalgos/ltl2tgba_fm.cc | 15 ++++++++++-----
 spot/twaalgos/translate.cc   |  9 ++++++---
 3 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh
index 9239e1a68..074ec8b02 100644
--- a/spot/tl/formula.hh
+++ b/spot/tl/formula.hh
@@ -294,7 +294,9 @@ namespace spot
       {
         if (SPOT_UNLIKELY(i >= size()))
           report_non_existing_child();
-        return children[i];
+        const fnode* c = children[i];
+        SPOT_ASSUME(c != nullptr);
+        return c;
       }
 
       /// \see formula::ff
diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc
index 42571f00f..9768dfbfd 100644
--- a/spot/twaalgos/ltl2tgba_fm.cc
+++ b/spot/twaalgos/ltl2tgba_fm.cc
@@ -1026,11 +1026,16 @@ namespace spot
           bool coacc = false;
           auto& st = sm->states_of(n);
           for (auto l: st)
-            if (namer->get_name(l).accepts_eword())
-              {
-                coacc = true;
-                break;
-              }
+            {
+              formula lf = namer->get_name(l);
+              // Somehow gcc 12.2.0 thinks lf can be nullptr.
+              SPOT_ASSUME(lf != nullptr);
+              if (lf.accepts_eword())
+                {
+                  coacc = true;
+                  break;
+                }
+            }
           if (!coacc)
             {
               // ... or if any of its successors is coaccessible.
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index d5b1aacd0..339463426 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -209,9 +209,12 @@ namespace spot
         if (!rest.empty() && !oblg.empty())
           {
             auto safety = [](formula f)
-              {
-                return f.is_syntactic_safety();
-              };
+            {
+              // Prevent gcc 12.2.0 from warning us that f could be a
+              // nullptr formula.
+              SPOT_ASSUME(f != nullptr);
+              return f.is_syntactic_safety();
+            };
             auto i = std::remove_if(oblg.begin(), oblg.end(), safety);
             rest.insert(rest.end(), i, oblg.end());
             oblg.erase(i, oblg.end());