From: Martin Clochard <cloch...@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
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 6e1c86acc39..a75a507388b 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 --
------------------------------
--
2.43.0
