[Ada] Allow constants of access type in Global contracts
diff mbox series

Message ID 20190919132819.GA41817@adacore.com
State New
Headers show
Series
  • [Ada] Allow constants of access type in Global contracts
Related show

Commit Message

Pierre-Marie de Rodat Sept. 19, 2019, 1:28 p.m. UTC
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).

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

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.

Patch
diff mbox series

--- gcc/ada/sem_prag.adb
+++ 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

--- /dev/null
new file mode 100644
+++ 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

--- /dev/null
new file mode 100644
+++ 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;