diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2021-07-22 15:33:16 +0200 |
---|---|---|
committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-09-22 15:01:47 +0000 |
commit | 920e43ee2143c2dbe71d0117243ef53363396ee1 (patch) | |
tree | 121191ea7281051ca8e3c336af9167a456e3ca51 /gcc | |
parent | f4f6c18d9f739df6f1cf8aedbc2a0c4b3c0248fa (diff) | |
download | gcc-920e43ee2143c2dbe71d0117243ef53363396ee1.zip gcc-920e43ee2143c2dbe71d0117243ef53363396ee1.tar.gz gcc-920e43ee2143c2dbe71d0117243ef53363396ee1.tar.bz2 |
[Ada] Add Package_Body helper routine to be used in GNATprove
gcc/ada/
* sem_aux.adb, sem_aux.ads (Package_Body): Moved from GNATprove.
* sem_elab.adb (Spec_And_Body_From_Entity): Refine type of parameter.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/sem_aux.adb | 25 | ||||
-rw-r--r-- | gcc/ada/sem_aux.ads | 4 | ||||
-rw-r--r-- | gcc/ada/sem_elab.adb | 4 |
3 files changed, 31 insertions, 2 deletions
diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb index bce7c38..dcced7e 100644 --- a/gcc/ada/sem_aux.adb +++ b/gcc/ada/sem_aux.adb @@ -1402,6 +1402,31 @@ package body Sem_Aux is end Object_Type_Has_Constrained_Partial_View; ------------------ + -- Package_Body -- + ------------------ + + function Package_Body (E : Entity_Id) return Node_Id is + Body_Decl : Node_Id; + Body_Id : constant Opt_E_Package_Body_Id := + Corresponding_Body (Package_Spec (E)); + + begin + if Present (Body_Id) then + Body_Decl := Parent (Body_Id); + + if Nkind (Body_Decl) = N_Defining_Program_Unit_Name then + Body_Decl := Parent (Body_Decl); + end if; + + pragma Assert (Nkind (Body_Decl) = N_Package_Body); + + return Body_Decl; + else + return Empty; + end if; + end Package_Body; + + ------------------ -- Package_Spec -- ------------------ diff --git a/gcc/ada/sem_aux.ads b/gcc/ada/sem_aux.ads index 810e2d8..3adaee4 100644 --- a/gcc/ada/sem_aux.ads +++ b/gcc/ada/sem_aux.ads @@ -377,6 +377,10 @@ package Sem_Aux is -- derived type, and the subtype is not an unconstrained array subtype -- (RM 3.3(23.10/3)). + function Package_Body (E : Entity_Id) return Node_Id; + -- Given an entity for a package, return the corresponding package body, if + -- any, or else Empty. + function Package_Spec (E : Entity_Id) return Node_Id; -- Given an entity for a package spec, return the corresponding package -- spec if any, or else Empty. diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index f6edcac..7635ae1 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -2070,7 +2070,7 @@ package body Sem_Elab is -- Change the status of the elaboration phase of the compiler to Status procedure Spec_And_Body_From_Entity - (Id : Node_Id; + (Id : Entity_Id; Spec_Decl : out Node_Id; Body_Decl : out Node_Id); pragma Inline (Spec_And_Body_From_Entity); @@ -15835,7 +15835,7 @@ package body Sem_Elab is ------------------------------- procedure Spec_And_Body_From_Entity - (Id : Node_Id; + (Id : Entity_Id; Spec_Decl : out Node_Id; Body_Decl : out Node_Id) is |