From 09709b4781192f7724e2bb2977d3610ae727260f Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 19 Sep 2019 08:13:58 +0000 Subject: [PATCH] [Ada] Allow constants of access type in Global contracts Now that SPARK supports access types, global constants of access type may appear as outputs of a subprogram, with the meaning that the underlying memory can be modified (see SPARK RM 3.10). 2019-09-19 Yannick Moy gcc/ada/ * sem_prag.adb (Analyze_Global_In_Decl_Part): Do not issue an error when a constant of an access type is used as output in a Global contract. (Analyze_Depends_In_Decl_Part): Do not issue an error when a constant of an access type is used as output in a Depends contract. gcc/testsuite/ * gnat.dg/global2.adb, gnat.dg/global2.ads: New testcase. From-SVN: r275947 --- gcc/ada/ChangeLog | 9 ++++++++ gcc/ada/sem_prag.adb | 35 ++++++++++++++++++++++++++----- gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/global2.adb | 12 +++++++++++ gcc/testsuite/gnat.dg/global2.ads | 6 ++++++ 5 files changed, 61 insertions(+), 5 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/global2.adb create mode 100644 gcc/testsuite/gnat.dg/global2.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b4bfc009b3e..070b8a125bd 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,12 @@ +2019-09-19 Yannick Moy + + * sem_prag.adb (Analyze_Global_In_Decl_Part): Do not issue an + error when a constant of an access type is used as output in a + Global contract. + (Analyze_Depends_In_Decl_Part): Do not issue an error when a + constant of an access type is used as output in a Depends + contract. + 2019-09-19 Arnaud Charlet * exp_attr.adb: Remove obsolete comment. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 5a561ea64b2..43673830c83 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -1262,8 +1262,28 @@ package body Sem_Prag is (Item_Is_Input : out Boolean; Item_Is_Output : out Boolean) is + -- A constant or IN parameter of access type should be handled + -- like a variable, as the underlying memory pointed-to can be + -- modified. Use Adjusted_Kind to do this adjustment. + + Adjusted_Kind : Entity_Kind := Ekind (Item_Id); + begin - case Ekind (Item_Id) is + if Ekind_In (Item_Id, E_Constant, + E_Generic_In_Parameter, + E_In_Parameter) + + -- If Item_Id is of a private type whose completion has not been + -- analyzed yet, its Underlying_Type is empty and we handle it + -- as a constant. + + and then Present (Underlying_Type (Etype (Item_Id))) + and then Is_Access_Type (Underlying_Type (Etype (Item_Id))) + then + Adjusted_Kind := E_Variable; + end if; + + case Adjusted_Kind is -- Abstract states @@ -1303,7 +1323,9 @@ package body Sem_Prag is Item_Is_Output := False; - -- Variables and IN OUT parameters + -- Variables and IN OUT parameters, as well as constants and + -- IN parameters of access type which are handled like + -- variables. when E_Generic_In_Out_Parameter | E_In_Out_Parameter @@ -2412,10 +2434,13 @@ package body Sem_Prag is -- Constant related checks - elsif Ekind (Item_Id) = E_Constant then + elsif Ekind (Item_Id) = E_Constant + and then + not Is_Access_Type (Underlying_Type (Etype (Item_Id))) + then - -- A constant is a read-only item, therefore it cannot act - -- as an output. + -- Unless it is of an access type, a constant is a read-only + -- item, therefore it cannot act as an output. if Nam_In (Global_Mode, Name_In_Out, Name_Output) then SPARK_Msg_NE diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index a927297a82b..da23e2cd5af 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2019-09-19 Yannick Moy + + * gnat.dg/global2.adb, gnat.dg/global2.ads: New testcase. + 2019-09-19 Eric Botcazou * gnat.dg/access9.adb: New testcase. diff --git a/gcc/testsuite/gnat.dg/global2.adb b/gcc/testsuite/gnat.dg/global2.adb new file mode 100644 index 00000000000..b18d9ac1fda --- /dev/null +++ b/gcc/testsuite/gnat.dg/global2.adb @@ -0,0 +1,12 @@ +-- { dg-do compile } + +package body Global2 is + procedure Change_X is + begin + X.all := 1; + end Change_X; + procedure Change2_X is + begin + X.all := 1; + end Change2_X; +end Global2; \ No newline at end of file diff --git a/gcc/testsuite/gnat.dg/global2.ads b/gcc/testsuite/gnat.dg/global2.ads new file mode 100644 index 00000000000..4de3158a4a2 --- /dev/null +++ b/gcc/testsuite/gnat.dg/global2.ads @@ -0,0 +1,6 @@ +package Global2 is + type Int_Acc is access Integer; + X : constant Int_Acc := new Integer'(34); + procedure Change_X with Global => (In_Out => X); + procedure Change2_X with Depends => (X => X); +end Global2; -- 2.30.2