From 577b1ab4b158ba501df6c6b721b83043fc26cbff Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 11 Jun 2018 09:18:56 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 5 ++++ gcc/ada/sem_prag.adb | 41 +++++++++++++++++++++++--------- gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/spark1.adb | 22 +++++++++++++++++ gcc/testsuite/gnat.dg/spark1.ads | 8 +++++++ 5 files changed, 69 insertions(+), 11 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/spark1.adb create mode 100644 gcc/testsuite/gnat.dg/spark1.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f6902cfca71..175d15d7069 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-06-11 Yannick Moy + + * sem_prag.adb (Check_Mode_Restriction_In_Enclosing_Context): Adapt for + possible task unit as the enclosing context. + 2018-06-11 Eric Botcazou * gnat1drv.adb: Remove use clause for Repinfo. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 3065dabc09d..c5b710e840d 100644 --- 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 9b5eccaa7c5..111fdd0544f 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2018-06-11 Yannick Moy + + * gnat.dg/spark1.adb, gnat.dg/spark1.ads: New testcase. + 2018-06-11 Hristian Kirtchev * 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 index 00000000000..27760237c9b --- /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 index 00000000000..d903cc74945 --- /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; -- 2.30.2