From: Claire Dross <dr...@adacore.com>
In general, functions in SPARK cannot have parameters of mode IN OUT
unless they are annotated with the Side_Effects aspect. Borrowing
traversal functions are special functions which can return a part
of their first parameter as an access-to-variable type. This might not
be allowed in Ada if the parameter is a constant. Allow the first
parameter of borrowing traversal functions to have mode IN OUT.
gcc/ada/ChangeLog:
* sem_ch6.adb (Analyze_SPARK_Subprogram_Specification):
Allow the first parameter of functions whose return type is
an anonymous access-to-variable type to have mode IN OUT.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_ch6.adb | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index d4e6d169326..dcbcc608f83 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2275,6 +2275,23 @@ package body Sem_Ch6 is
end if;
Formal := First_Formal (Spec_Id);
+
+ -- The first parameter of a borrowing traversal function might be an IN
+ -- or an IN OUT parameter.
+
+ if Present (Formal)
+ and then Ekind (Etype (Spec_Id)) = E_Anonymous_Access_Type
+ and then not Is_Access_Constant (Etype (Spec_Id))
+ then
+ if Ekind (Formal) = E_Out_Parameter then
+ Error_Msg_Code := GEC_Out_Parameter_In_Function;
+ Error_Msg_N
+ ("first parameter of traversal function cannot have mode `OUT` "
+ & "in SPARK '[[]']", Formal);
+ end if;
+ Next_Formal (Formal);
+ end if;
+
while Present (Formal) loop
if Ekind (Spec_Id) in E_Function | E_Generic_Function
and then not Is_Function_With_Side_Effects (Spec_Id)
--
2.43.0
