ada: Allow IN OUT parameters for first parameter of traversal functions

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.

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index d4e6d1693263591c4daaafcc169a7930c4131d95..dcbcc608f8399bf447417deb19226e952749bf2b 100644 (file)
--- 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)