]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
[Ada] Add Package_Body helper routine to be used in GNATprove
authorPiotr Trojanek <trojanek@adacore.com>
Thu, 22 Jul 2021 13:33:16 +0000 (15:33 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 22 Sep 2021 15:01:47 +0000 (15:01 +0000)
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.

gcc/ada/sem_aux.adb
gcc/ada/sem_aux.ads
gcc/ada/sem_elab.adb

index bce7c387ae3f188413f2b81f25a2814726fef666..dcced7e40e657d4ade9232ccbdee0ca5876bb804 100644 (file)
@@ -1401,6 +1401,31 @@ package body Sem_Aux is
                   and then Has_Discriminants (Typ));
    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 --
    ------------------
index 810e2d8854bea3b269910435d16c2b047bab52aa..3adaee416b26fb0d30309a80a91fa84991bb4c9c 100644 (file)
@@ -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.
index f6edcac2c021f39c376068ab0d6fadc7dfa04675..7635ae180d28973bdd3ad751877d10e73d7a506b 100644 (file)
@@ -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