aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2021-07-22 15:33:16 +0200
committerPierre-Marie de Rodat <derodat@adacore.com>2021-09-22 15:01:47 +0000
commit920e43ee2143c2dbe71d0117243ef53363396ee1 (patch)
tree121191ea7281051ca8e3c336af9167a456e3ca51 /gcc
parentf4f6c18d9f739df6f1cf8aedbc2a0c4b3c0248fa (diff)
downloadgcc-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.adb25
-rw-r--r--gcc/ada/sem_aux.ads4
-rw-r--r--gcc/ada/sem_elab.adb4
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