diff options
| author | Yannick Moy <moy@adacore.com> | 2019-09-19 08:13:58 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-09-19 08:13:58 +0000 |
| commit | 09709b4781192f7724e2bb2977d3610ae727260f (patch) | |
| tree | e59c2a3e5005c53d438b9fde16dce04994fe1584 /gcc/ada | |
| parent | 7005758ce72896e478245ed2de0aa146427a2ec9 (diff) | |
| download | gcc-09709b4781192f7724e2bb2977d3610ae727260f.zip gcc-09709b4781192f7724e2bb2977d3610ae727260f.tar.gz gcc-09709b4781192f7724e2bb2977d3610ae727260f.tar.bz2 | |
[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
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 9 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 35 |
2 files changed, 39 insertions, 5 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b4bfc00..070b8a1 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 5a561ea..4367383 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 |