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 --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 6e1c86acc39eace40bf2dcf1c4cfdf7029da78e6..a75a507388bc9b4b45a12c9f30b643b533eb72bb 100644 (file)
--- 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 --
    ------------------------------