1 files changed, 24 insertions, 0 deletions
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 6e1c86a..a75a507 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 --
    ------------------------------