From: Yannick Moy <moy@adacore.com>
Date: Thu, 19 Sep 2019 08:13:58 +0000 (+0000)
Subject: [Ada] Allow constants of access type in Global contracts
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09709b4781192f7724e2bb2977d3610ae727260f;p=gcc.git

[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  <moy@adacore.com>

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
---

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  <moy@adacore.com>
+
+	* 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  <charlet@adacore.com>
 
 	* 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  <moy@adacore.com>
+
+	* gnat.dg/global2.adb, gnat.dg/global2.ads: New testcase.
+
 2019-09-19  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* 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;