[Ada] Reject formals of mode IN appearing as global outputs

[Ada] Reject formals of mode IN appearing as global outputs

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 889 bytes --]

Fix implementation of SPARK RM 6.1.4(13), which says:

  "... if the global_specification of the outer subprogram has an entity
   denoted by a global_item with a mode_specification of Input or the
   entity is a formal parameter with a mode of in"

but the rule was only enforced for outer subprograms with explicit
Global contracts. Now it is enforced for subprograms with implicit
Global contracts as well, i.e. both implicit Global => null, implicit
Global implied by Depends, and with Global generated by the flow
analysis of GNATprove.

In particular, this is useful for detecting formals of mode IN appearing
in as global outputs of nested subprograms.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* sem_prag.adb (Check_Mode_Restriction_In_Enclosing_Context):
	Apply the rule even with no explicit Global contract (and remove
	a dead condition for Refined_Global).

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1466 bytes --]

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2634,13 +2634,9 @@ package body Sem_Prag is
                   Context := Anonymous_Object (Context);
                end if;
 
-               if (Is_Subprogram_Or_Entry (Context)
-                     or else Ekind (Context) = E_Task_Type
-                     or else Is_Single_Task_Object (Context))
-                 and then
-                  (Present (Get_Pragma (Context, Pragma_Global))
-                     or else
-                   Present (Get_Pragma (Context, Pragma_Refined_Global)))
+               if Is_Subprogram_Or_Entry (Context)
+                 or else Ekind (Context) = E_Task_Type
+                 or else Is_Single_Task_Object (Context)
                then
                   Collect_Subprogram_Inputs_Outputs
                     (Subp_Id      => Context,
@@ -2649,8 +2645,8 @@ package body Sem_Prag is
                      Global_Seen  => Dummy);
 
                   --  The item is classified as In_Out or Output but appears as
-                  --  an Input in an enclosing subprogram or task unit (SPARK
-                  --  RM 6.1.4(13)).
+                  --  an Input or a formal parameter of mode IN in an enclosing
+                  --  subprogram or task unit (SPARK RM 6.1.4(13)).
 
                   if Appears_In (Inputs, Item_Id)
                     and then not Appears_In (Outputs, Item_Id)