[gcc r16-2407] ada: Expand continue procedure calls for GNATprove

[Marc Poulhies via Gcc-cvs]

https://gcc.gnu.org/g:c543be28e2e9c1047b81e7abe6377ea6a6ccc1a6

commit r16-2407-gc543be28e2e9c1047b81e7abe6377ea6a6ccc1a6
Author: Martin Clochard <cloch...@adacore.com>
Date:   Thu Jul 3 15:52:02 2025 +0200

    ada: Expand continue procedure calls for GNATprove
    
    Continue being a non-reserved keyword, occurrences of continue may
    be resolved as procedure calls. Get that special case out of the
    way for GNATprove, in anticipation of support for continue keyword.
    
    gcc/ada/ChangeLog:
    
            * exp_spark.adb (Expand_SPARK): Add expansion of continue 
statements.
            (Expand_SPARK_N_Continue_Statement): Expand continue statements 
resolved
            as procedure calls into said procedure calls.

Diff:
---
 gcc/ada/exp_spark.adb | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 6e1c86acc39e..a75a507388bc 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -73,6 +73,10 @@ package body Exp_SPARK is
    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
    --  Perform attribute-reference-specific expansion
 
+   procedure Expand_SPARK_N_Continue_Statement (N : Node_Id);
+   --  Expand continue statements which are resolved as procedure calls, into
+   --  said procedure calls. Real continue statements are left as-is.
+
    procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id);
    --  Perform delta-aggregate-specific expansion
 
@@ -191,6 +195,9 @@ package body Exp_SPARK is
 
          --  In SPARK mode, no other constructs require expansion
 
+         when N_Continue_Statement =>
+            Expand_SPARK_N_Continue_Statement (N);
+
          when others =>
             null;
       end case;
@@ -435,6 +442,23 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_Delta_Or_Update;
 
+   ---------------------------------------
+   -- Expand_SPARK_N_Continue_Statement --
+   ---------------------------------------
+
+   procedure Expand_SPARK_N_Continue_Statement (N : Node_Id) is
+      X : constant Node_Id := Call_Or_Target_Loop (N);
+   begin
+      if No (X) then
+         return;
+      end if;
+
+      if Nkind (X) = N_Procedure_Call_Statement then
+         Replace (N, X);
+         Analyze (N);
+      end if;
+   end Expand_SPARK_N_Continue_Statement;
+
    ------------------------------
    -- Expand_SPARK_N_Aggregate --
    ------------------------------