[Ada] Reject violation of SPARK 6.1.4(12) with enclosing task unit

SPARK 6.1.4(12) applies both to enclosing subprograms and enclosing task
units, but the latter was not correctly rejected.

2018-06-11  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_prag.adb (Check_Mode_Restriction_In_Enclosing_Context): Adapt for
	possible task unit as the enclosing context.

gcc/testsuite/

	* gnat.dg/spark1.adb, gnat.dg/spark1.ads: New testcase.

From-SVN: r261421

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f6902cf..175d15d 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-06-11  Yannick Moy  <moy@adacore.com>
+
+       * sem_prag.adb (Check_Mode_Restriction_In_Enclosing_Context): Adapt for
+       possible task unit as the enclosing context.
+
 2018-06-11  Eric Botcazou  <ebotcazou@adacore.com>
 
        * gnat1drv.adb: Remove use clause for Repinfo.

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 3065dab..c5b710e 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2128,10 +2128,10 @@ package body Sem_Prag is
          procedure Check_Mode_Restriction_In_Enclosing_Context
            (Item    : Node_Id;
             Item_Id : Entity_Id);
-         --  Verify that an item of mode In_Out or Output does not appear as an
-         --  input in the Global aspect of an enclosing subprogram. If this is
-         --  the case, emit an error. Item and Item_Id are respectively the
-         --  item and its entity.
+         --  Verify that an item of mode In_Out or Output does not appear as
+         --  an input in the Global aspect of an enclosing subprogram or task
+         --  unit. If this is the case, emit an error. Item and Item_Id are
+         --  respectively the item and its entity.
 
          procedure Check_Mode_Restriction_In_Function (Mode : Node_Id);
          --  Mode denotes either In_Out or Output. Depending on the kind of the
@@ -2483,12 +2483,24 @@ package body Sem_Prag is
             Outputs : Elist_Id := No_Elist;
 
          begin
-            --  Traverse the scope stack looking for enclosing subprograms
-            --  subject to pragma [Refined_]Global.
+            --  Traverse the scope stack looking for enclosing subprograms or
+            --  tasks subject to pragma [Refined_]Global.
 
             Context := Scope (Subp_Id);
             while Present (Context) and then Context /= Standard_Standard loop
-               if Is_Subprogram (Context)
+
+               --  For a single task type, retrieve the corresponding object to
+               --  which pragma [Refined_]Global is attached.
+
+               if Ekind (Context) = E_Task_Type
+                 and then Is_Single_Concurrent_Type (Context)
+               then
+                  Context := Anonymous_Object (Context);
+               end if;
+
+               if (Is_Subprogram (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
@@ -2501,7 +2513,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 (SPARK RM 6.1.4(12)).
+                  --  an Input in an enclosing subprogram or task unit (SPARK
+                  --  RM 6.1.4(12)).
 
                   if Appears_In (Inputs, Item_Id)
                     and then not Appears_In (Outputs, Item_Id)
@@ -2510,9 +2523,15 @@ package body Sem_Prag is
                        ("global item & cannot have mode In_Out or Output",
                         Item, Item_Id);
 
-                     SPARK_Msg_NE
-                       (Fix_Msg (Subp_Id, "\item already appears as input of "
-                        & "subprogram &"), Item, Context);
+                     if Is_Subprogram (Context) then
+                        SPARK_Msg_NE
+                          (Fix_Msg (Subp_Id, "\item already appears as input "
+                           & "of subprogram &"), Item, Context);
+                     else
+                        SPARK_Msg_NE
+                          (Fix_Msg (Subp_Id, "\item already appears as input "
+                           & "of task &"), Item, Context);
+                     end if;
 
                      --  Stop the traversal once an error has been detected
 

diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index 9b5ecca..111fdd0 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2018-06-11  Yannick Moy  <moy@adacore.com>
+
+       * gnat.dg/spark1.adb, gnat.dg/spark1.ads: New testcase.
+
 2018-06-11  Hristian Kirtchev  <kirtchev@adacore.com>
 
        * gnat.dg/gnat_array_split1.adb, gnat.dg/gnat_array_split1.ads: New

diff --git a/gcc/testsuite/gnat.dg/spark1.adb b/gcc/testsuite/gnat.dg/spark1.adb
new file mode 100644 (file)
index 0000000..2776023
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/spark1.adb
@@ -0,0 +1,22 @@
+--  { dg-do compile }
+
+package body Spark1 is
+
+   task body Worker is
+
+      procedure Update with
+        Global => (In_Out => Mailbox) --  { dg-error "global item \"Mailbox\" cannot have mode In_Out or Output|item already appears as input of task \"Worker\"" }
+      is
+         Tmp : Integer := Mailbox;
+      begin
+         Mailbox := Tmp + 1;
+      end Update;
+
+      X : Integer := Mailbox;
+   begin
+      loop
+         Update;
+      end loop;
+   end;
+
+end;

diff --git a/gcc/testsuite/gnat.dg/spark1.ads b/gcc/testsuite/gnat.dg/spark1.ads
new file mode 100644 (file)
index 0000000..d903cc7
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/spark1.ads
@@ -0,0 +1,8 @@
+package Spark1 is
+
+   Mailbox : Integer with Atomic, Async_Writers, Async_Readers;
+
+   task Worker
+     with Global => (Input => Mailbox);
+
+end;