2017-10-09 Bob Duff <duff@adacore.com>

	* exp_ch6.adb (Make_Build_In_Place_Call_In_Object_Declaration): Use
	Defining_Identifier (Obj_Decl) in two places, because it might have
	changed.
	* exp_ch6.adb (Make_Build_In_Place_Call_In_Allocator): Deal with cases
	involving 'Input on (not visibly) derived types.

2017-10-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* atree.adb: Add new soft link Rewriting_Proc.
	(Rewrite): Invoke the subprogram attached to the rewriting soft link.
	(Set_Rewriting_Proc): New routine.
	* attree.ads: Add new access-to-subprogram type Rewrite_Proc.
	(Set_Rewriting_Proc): New routine.
	* checks.adb (Install_Primitive_Elaboration_Check): Use 'E' character
	for *E*laboration flag to maintain consistency with other elaboration
	flag generating subprograms.
	* debug.adb: Document the new usage of flag -gnatdL.
	* einfo.adb: Node19 is now used as Receiving_Entry.  Node39 is now used
	as Protected_Subprogram.  Flag148 is now used as
	Is_Elaboration_Checks_OK_Id.  Flag302 is now used as
	Is_Initial_Condition_Procedure.
	(Is_Elaboration_Checks_OK_Id): New routine.
	(Is_Initial_Condition_Procedure): New routine.
	(Protected_Subprogram): New routine.
	(Receiving_Entry): New routine.
	(SPARK_Pragma): Update assertion.
	(SPARK_Pragma_Inherited): Update assertion.
	(Suppress_Elaboration_Warnings): Removed.
	(Set_Is_Elaboration_Checks_OK_Id): New routine.
	(Set_Is_Initial_Condition_Procedure): New routine.
	(Set_Protected_Subprogram): New routine.
	(Set_Receiving_Entry): New routine.
	(Set_SPARK_Pragma): Update assertion.
	(Set_SPARK_Pragma_Inherited): Update assertion.
	(Write_Entity_Flags): Update the output for Flag148 and Flag302.
	(Write_Field19_Name): Add output for Receiving_Entry.
	(Write_Field39_Name): Add output for Protected_Subprogram.
	(Write_Field40_Name): Update the output for SPARK_Pragma.
	* einfo.ads: New attributes Is_Elaboration_Checks_OK_Id,
	Is_Initial_Condition_Procedure, Protected_Subprogram, Receiving_Entry.
	Remove attribute Suppress_Elaboration_Warnings.  Update the stricture
	of various entities.
	(Is_Elaboration_Checks_OK_Id): New routine along with pragma Inline.
	(Is_Initial_Condition_Procedure): New routine along with pragma Inline.
	(Protected_Subprogram): New routine along with pragma Inline.
	(Receiving_Entry): New routine along with pragma Inline.
	(Suppress_Elaboration_Warnings): Removed.
	(Set_Is_Elaboration_Checks_OK_Id): New routine along with pragma
	Inline.
	(Set_Is_Initial_Condition_Procedure): New routine along with pragma
	Inline.
	(Set_Protected_Subprogram): New routine along with pragma Inline.
	(Set_Receiving_Entry): New routine along with pragma Inline.
	(Set_Suppress_Elaboration_Warnings): Removed.
	* exp_ch3.adb (Build_Init_Procedure): Use name _Finalizer to maintain
	consistency with other finalizer generating subprograms.
	(Default_Initialize_Object): Mark the block which wraps the call to
	finalize as being part of initialization.
	* exp_ch7.adb (Expand_N_Package_Declaration): Directly expand pragma
	Initial_Condition.
	(Expand_N_Package_Body): Directly expand pragma Initial_Condition.
	(Next_Suitable_Statement): Update the comment on usage. Skip over call
	markers generated by the ABE mechanism.
	* exp_ch9.adb (Activation_Call_Loc): New routine.
	(Add_Accept): Link the accept procedure to the original entry.
	(Build_Protected_Sub_Specification): Link the protected or unprotected
	version to the original subprogram.
	(Build_Task_Activation_Call): Code cleanup. Use a source location which
	is very close to the "begin" or "end" keywords when generating the
	activation call.
	* exp_prag.adb (Expand_Pragma_Initial_Condition): Reimplemented.
	* exp_spark.adb (Expand_SPARK): Use Expand_SPARK_N_Loop_Statement to
	process loops.
	(Expand_SPARK_N_Loop_Statement): New routine.
	(Expand_SPARK_N_Object_Declaration): Code cleanup. Partially insert the
	call to the Default_Initial_Condition procedure.
	(Expand_SPARK_Op_Ne): Renamed to Expand_SPARK_N_Op_Ne.
	* exp_util.adb (Build_DIC_Procedure_Body): Capture the SPARK_Mode in
	effect.
	(Build_DIC_Procedure_Declaration): Capture the SPARK_Mode in effect.
	(Insert_Actions): Add processing for N_Call_Marker.
	(Kill_Dead_Code): Explicitly kill an elaboration scenario.
	* exp_util.ads (Make_Invariant_Call): Update the comment on usage.
	* frontend.adb: Initialize Sem_Elab. Process all saved top level
	elaboration scenarios for ABE issues.
	* gcc-interface/trans.c (gnat_to_gnu): Add processing for N_Call_Marker
	nodes.
	* lib.adb (Earlier_In_Extended_Unit): New variant.
	* sem.adb (Analyze): Ignore N_Call_Marker nodes.
	(Preanalysis_Active): New routine.
	* sem.ads (Preanalysis_Active): New routine.
	* sem_attr.adb (Analyze_Access_Attribute): Save certain
	elaboration-related attributes. Save the scenario for ABE processing.
	* sem_ch3.adb (Analyze_Object_Declaration): Save the SPARK mode in
	effect. Save certain elaboration-related attributes.
	* sem_ch5.adb (Analyze_Assignment): Save certain elaboration-related
	attributes. Save the scenario for ABE processing.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Save the SPARK
	mode in effect. Save certain elaboration-related attributes.
	(Analyze_Subprogram_Body_Helper): Skip N_Call_Marker nodes when
	locating the first real statement.
	(Analyze_Subprogram_Declaration): Save the SPARK mode in effect. Save
	certain elaboration-related attributes.
	* sem_ch7.adb (Analyze_Package_Declaration): Do not suppress
	elaboration warnings.
	* sem_ch8.adb (Attribute_Renaming): Mark a subprogram body which was
	generated for purposes of wrapping an attribute used as a generic
	actual.
	(Find_Direct_Name): Save certain elaboration-related attributes. Save
	the scenario for ABE processing.
	(Find_Expanded_Name): Save certain elaboration-related attributes. Save
	the scenario for ABE processing.
	* sem_ch9.adb (Analyze_Entry_Declaration): Save certain
	elaboration-related attributes.
	(Analyze_Requeue): Save certain elaboration-related attributes. Save
	the scenario for ABE processing.
	(Analyze_Single_Task_Declaration): Save certain elaboration-related
	attributes.
	(Analyze_Task_Type_Declaration): Save certain elaboration-related
	attributes.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Save certain
	elaboration-related attributes.
	(Analyze_Generic_Subprogram_Declaration): Save the SPARK mode in
	effect. Save certain elaboration-related attributes.
	(Analyze_Package_Instantiation): Save certain elaboration-related
	attributes.  Save the scenario for ABE processing. Create completing
	bodies in case the instantiation results in a guaranteed ABE.
	(Analyze_Subprogram_Instantiation): Save certain elaboration-related
	attributes Save the scenario for ABE processing. Create a completing
	body in case the instantiation results in a guaranteed ABE.
	(Provide_Completing_Bodies): New routine.
	* sem_elab.ads: Brand new implementation.
	* sem_prag.adb (Analyze_Pragma, cases Elaborate, Elaborate_All,
	Elaborate_Body): Do not suppress elaboration warnings.
	* sem_res.adb (Make_Call_Into_Operator): Set the parent field of the
	operator.
	(Resolve_Call): Save certain elaboration-related attributes. Save the
	scenario for ABE processing.
	(Resolve_Entity_Name): Do not perform any ABE processing here.
	(Resolve_Entry_Call): Inherit certain attributes from the original call.
	* sem_util.adb (Begin_Keyword_Location): New routine.
	(Defining_Entity): Update the parameter profile. Add processing for
	concurrent subunits that are rewritten as null statements.
	(End_Keyword_Location): New routine.
	(Find_Enclosing_Scope): New routine.
	(In_Instance_Visible_Part): Code cleanup.
	(In_Subtree): Update the parameter profile. Add new version.
	(Is_Preelaborable_Aggregate): New routine.
	(Is_Preelaborable_Construct): New routine.
	(Mark_Elaboration_Attributes): New routine.
	(Scope_Within): Update the parameter profile.
	(Scope_Within_Or_Same): Update the parameter profile.
	* sem_util.ads (Begin_Keyword_Location): New routine.
	(Defining_Entity): Update the parameter profile and the comment on
	usage.
	(End_Keyword_Location): New routine.
	(Find_Enclosing_Scope): New routine.
	(In_Instance_Visible_Part): Update the parameter profile.
	(In_Subtree): Update the parameter profile. Add new version.
	(Is_Preelaborable_Aggregate): New routine.
	(Is_Preelaborable_Construct): New routine.
	(Mark_Elaboration_Attributes): New routine.
	(Scope_Within): Update the parameter profile and the comment on usage.
	(Scope_Within_Or_Same): Update the parameter profile and the comment on
	usage.
	* sem_warn.adb (Check_Infinite_Loop_Warning): Use Has_Condition_Actions
	to determine whether a loop has meaningful condition actions.
	(Has_Condition_Actions): New routine.
	* sinfo.adb (ABE_Is_Certain): Removed.
	(Is_Declaration_Level_Node): New routine.
	(Is_Dispatching_Call): New routine.
	(Is_Elaboration_Checks_OK_Node): New routine.
	(Is_Initialization_Block): New routine.
	(Is_Known_Guaranteed_ABE): New routine.
	(Is_Recorded_Scenario): New routine.
	(Is_Source_Call): New routine.
	(Is_SPARK_Mode_On_Node): New routine.
	(No_Elaboration_Check): Removed.
	(Target): New routine.
	(Was_Attribute_Reference): New routine.
	(Set_ABE_Is_Certain): Removed.
	(Set_Is_Declaration_Level_Node): New routine.
	(Set_Is_Dispatching_Call): New routine.
	(Set_Is_Elaboration_Checks_OK_Node): New routine.
	(Set_Is_Initialization_Block): New routine.
	(Set_Is_Known_Guaranteed_ABE): New routine.
	(Set_Is_Recorded_Scenario): New routine.
	(Set_Is_Source_Call): New routine.
	(Set_Is_SPARK_Mode_On_Node): New routine.
	(Set_No_Elaboration_Check): Removed.
	(Set_Target): New routine.
	(Set_Was_Attribute_Reference): New routine.
	* sinfo.ads: Remove attribute ABE_Is_Certain.  Attribute
	Do_Discriminant_Check now utilizes Flag3.  Attribute
	No_Side_Effect_Removal now utilizes Flag17.  Add new node
	N_Call_Marker.  Update the structure of various nodes.
	(ABE_Is_Certain): Removed along with pragma Inline.
	(Is_Declaration_Level_Node): New routine along with pragma Inline.
	(Is_Dispatching_Call): New routine along with pragma Inline.
	(Is_Elaboration_Checks_OK_Node): New routine along with pragma Inline.
	(Is_Initialization_Block): New routine along with pragma Inline.
	(Is_Known_Guaranteed_ABE): New routine along with pragma Inline.
	(Is_Recorded_Scenario): New routine along with pragma Inline.
	(Is_Source_Call): New routine along with pragma Inline.
	(Is_SPARK_Mode_On_Node): New routine along with pragma Inline.
	(No_Elaboration_Check): Removed along with pragma Inline.
	(Target): New routine along with pragma Inline.
	(Was_Attribute_Reference): New routine along with pragma Inline.
	(Set_ABE_Is_Certain): Removed along with pragma Inline.
	(Set_Is_Declaration_Level_Node): New routine along with pragma Inline.
	(Set_Is_Dispatching_Call): New routine along with pragma Inline.
	(Set_Is_Elaboration_Checks_OK_Node): New routine along with pragma
	Inline.
	(Set_Is_Initialization_Block): New routine along with pragma Inline.
	(Set_Is_Known_Guaranteed_ABE): New routine along with pragma Inline.
	(Set_Is_Recorded_Scenario): New routine along with pragma Inline.
	(Set_Is_Source_Call): New routine along with pragma Inline.
	(Set_Is_SPARK_Mode_On_Node): New routine along with pragma Inline.
	(Set_No_Elaboration_Check): Removed along with pragma Inline.
	(Set_Target): New routine along with pragma Inline.
	(Set_Was_Attribute_Reference): New routine along with pragma Inline.
	* sprint.adb (Sprint_Node_Actual): Add an entry for N_Call_Marker.




git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@253559 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 253 insertions, 47 deletions

diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 57f60cd90eb..dfed6af66a7 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -42,6 +42,7 @@ with Restrict; use Restrict;
 with Rident;   use Rident;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
+with Sem_Aux;  use Sem_Aux;
 with Sem_Ch8;  use Sem_Ch8;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
@@ -1447,82 +1448,287 @@ package body Exp_Prag is
    -- Expand_Pragma_Initial_Condition --
    -------------------------------------
 
-   procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
-      Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
+   procedure Expand_Pragma_Initial_Condition
+     (Pack_Id : Entity_Id;
+      N       : Node_Id)
+   is
+      procedure Extract_Package_Body_Lists
+        (Pack_Body : Node_Id;
+         Body_List : out List_Id;
+         Call_List : out List_Id;
+         Spec_List : out List_Id);
+      --  Obtain the various declarative and statement lists of package body
+      --  Pack_Body needed to insert the initial condition procedure and the
+      --  call to it. The lists are as follows:
+      --
+      --    * Body_List - used to insert the initial condition procedure body
+      --
+      --    * Call_List - used to insert the call to the initial condition
+      --      procedure.
+      --
+      --    * Spec_List - used to insert the initial condition procedure spec
+
+      procedure Extract_Package_Declaration_Lists
+        (Pack_Decl : Node_Id;
+         Body_List : out List_Id;
+         Call_List : out List_Id;
+         Spec_List : out List_Id);
+      --  Obtain the various declarative lists of package declaration Pack_Decl
+      --  needed to insert the initial condition procedure and the call to it.
+      --  The lists are as follows:
+      --
+      --    * Body_List - used to insert the initial condition procedure body
+      --
+      --    * Call_List - used to insert the call to the initial condition
+      --      procedure.
+      --
+      --    * Spec_List - used to insert the initial condition procedure spec
+
+      --------------------------------
+      -- Extract_Package_Body_Lists --
+      --------------------------------
+
+      procedure Extract_Package_Body_Lists
+        (Pack_Body : Node_Id;
+         Body_List : out List_Id;
+         Call_List : out List_Id;
+         Spec_List : out List_Id)
+      is
+         Pack_Spec : constant Entity_Id := Corresponding_Spec (Pack_Body);
 
-      Check     : Node_Id;
-      Expr      : Node_Id;
-      Init_Cond : Node_Id;
-      List      : List_Id;
-      Pack_Id   : Entity_Id;
+         Dummy_1 : List_Id;
+         Dummy_2 : List_Id;
+         HSS     : Node_Id;
 
-   begin
-      if Nkind (Spec_Or_Body) = N_Package_Body then
-         Pack_Id := Corresponding_Spec (Spec_Or_Body);
+      begin
+         pragma Assert (Present (Pack_Spec));
 
-         if Present (Handled_Statement_Sequence (Spec_Or_Body)) then
-            List := Statements (Handled_Statement_Sequence (Spec_Or_Body));
+         --  The different parts of the invariant procedure are inserted as
+         --  follows:
 
-         --  The package body lacks statements, create an empty list
+         --    package Pack is       package body Pack is
+         --       <IC spec>             <IC body>
+         --    private               begin
+         --       ...                   <IC call>
+         --    end Pack;             end Pack;
 
-         else
-            List := New_List;
+         --  The initial condition procedure spec is inserted in the visible
+         --  declaration of the corresponding package spec.
+
+         Extract_Package_Declaration_Lists
+           (Pack_Decl => Unit_Declaration_Node (Pack_Spec),
+            Body_List => Dummy_1,
+            Call_List => Dummy_2,
+            Spec_List => Spec_List);
+
+         --  The initial condition procedure body is added to the declarations
+         --  of the package body.
+
+         Body_List := Declarations (Pack_Body);
 
-            Set_Handled_Statement_Sequence (Spec_Or_Body,
-              Make_Handled_Sequence_Of_Statements (Loc, Statements => List));
+         if No (Body_List) then
+            Body_List := New_List;
+            Set_Declarations (Pack_Body, Body_List);
          end if;
 
-      elsif Nkind (Spec_Or_Body) = N_Package_Declaration then
-         Pack_Id := Defining_Entity (Spec_Or_Body);
+         --  The call to the initial condition procedure is inserted in the
+         --  statements of the package body.
 
-         if Present (Visible_Declarations (Specification (Spec_Or_Body))) then
-            List := Visible_Declarations (Specification (Spec_Or_Body));
+         HSS := Handled_Statement_Sequence (Pack_Body);
 
-         --  The package lacks visible declarations, create an empty list
+         if No (HSS) then
+            HSS :=
+              Make_Handled_Sequence_Of_Statements (Sloc (Pack_Body),
+                Statements => New_List);
+            Set_Handled_Statement_Sequence (Pack_Body, HSS);
+         end if;
 
-         else
-            List := New_List;
+         Call_List := Statements (HSS);
+      end Extract_Package_Body_Lists;
+
+      ---------------------------------------
+      -- Extract_Package_Declaration_Lists --
+      ---------------------------------------
+
+      procedure Extract_Package_Declaration_Lists
+        (Pack_Decl : Node_Id;
+         Body_List : out List_Id;
+         Call_List : out List_Id;
+         Spec_List : out List_Id)
+      is
+         Pack_Spec : constant Node_Id := Specification (Pack_Decl);
+
+      begin
+         --  The different parts of the invariant procedure are inserted as
+         --  follows:
 
-            Set_Visible_Declarations (Specification (Spec_Or_Body), List);
+         --    package Pack is
+         --       <IC spec>
+         --       <IC body>
+         --    private
+         --       <IC call>
+         --    end Pack;
+
+         --  The initial condition procedure spec and body are inserted in the
+         --  visible declarations of the package spec.
+
+         Body_List := Visible_Declarations (Pack_Spec);
+
+         if No (Body_List) then
+            Body_List := New_List;
+            Set_Visible_Declarations (Pack_Spec, Body_List);
+         end if;
+
+         Spec_List := Body_List;
+
+         --  The call to the initial procedure is inserted in the private
+         --  declarations of the package spec.
+
+         Call_List := Private_Declarations (Pack_Spec);
+
+         if No (Call_List) then
+            Call_List := New_List;
+            Set_Private_Declarations (Pack_Spec, Call_List);
          end if;
+      end Extract_Package_Declaration_Lists;
+
+      --  Local variables
+
+      IC_Prag : constant Node_Id :=
+                  Get_Pragma (Pack_Id, Pragma_Initial_Condition);
+
+      Body_List    : List_Id;
+      Call         : Node_Id;
+      Call_List    : List_Id;
+      Call_Loc     : Source_Ptr;
+      Expr         : Node_Id;
+      Loc          : Source_Ptr;
+      Proc_Body    : Node_Id;
+      Proc_Body_Id : Entity_Id;
+      Proc_Decl    : Node_Id;
+      Proc_Id      : Entity_Id;
+      Spec_List    : List_Id;
+
+   --  Start of processing for Expand_Pragma_Initial_Condition
+
+   begin
+      --  Nothing to do when the package is not subject to an Initial_Condition
+      --  pragma.
+
+      if No (IC_Prag) then
+         return;
+      end if;
+
+      Expr := Get_Pragma_Arg (First (Pragma_Argument_Associations (IC_Prag)));
+      Loc  := Sloc (IC_Prag);
+
+      --  Nothing to do when the pragma or its argument are illegal because
+      --  there is no valid expression to check.
+
+      if Error_Posted (IC_Prag) or else Error_Posted (Expr) then
+         return;
+      end if;
+
+      --  Obtain the various lists of the context where the individual pieces
+      --  of the initial condition procedure are to be inserted.
+
+      if Nkind (N) = N_Package_Body then
+         Extract_Package_Body_Lists
+           (Pack_Body => N,
+            Body_List => Body_List,
+            Call_List => Call_List,
+            Spec_List => Spec_List);
+
+      elsif Nkind (N) = N_Package_Declaration then
+         Extract_Package_Declaration_Lists
+           (Pack_Decl => N,
+            Body_List => Body_List,
+            Call_List => Call_List,
+            Spec_List => Spec_List);
 
       --  This routine should not be used on anything other than packages
 
       else
-         raise Program_Error;
+         pragma Assert (False);
+         return;
       end if;
 
-      Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
+      Proc_Id :=
+        Make_Defining_Identifier (Loc,
+          Chars => New_External_Name (Chars (Pack_Id), "Initial_Condition"));
 
-      --  The caller should check whether the package is subject to pragma
-      --  Initial_Condition.
+      Set_Ekind                          (Proc_Id, E_Procedure);
+      Set_Is_Initial_Condition_Procedure (Proc_Id);
 
-      pragma Assert (Present (Init_Cond));
+      --  Generate:
+      --    procedure <Pack_Id>Initial_Condition;
 
-      Expr :=
-        Get_Pragma_Arg (First (Pragma_Argument_Associations (Init_Cond)));
+      Proc_Decl :=
+        Make_Subprogram_Declaration (Loc,
+          Make_Procedure_Specification (Loc,
+            Defining_Unit_Name => Proc_Id));
 
-      --  The assertion expression was found to be illegal, do not generate the
-      --  runtime check as it will repeat the illegality.
+      Append_To (Spec_List, Proc_Decl);
 
-      if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
-         return;
+      --  The initial condition procedure requires debug info when initial
+      --  condition is subject to Source Coverage Obligations.
+
+      if Generate_SCO then
+         Set_Needs_Debug_Info (Proc_Id);
       end if;
 
       --  Generate:
-      --    pragma Check (Initial_Condition, <Expr>);
+      --    procedure <Pack_Id>Initial_Condition is
+      --    begin
+      --       pragma Check (Initial_Condition, <Expr>);
+      --    end <Pack_Id>Initial_Condition;
+
+      Proc_Body :=
+        Make_Subprogram_Body (Loc,
+          Specification              =>
+            Copy_Subprogram_Spec (Specification (Proc_Decl)),
+          Declarations               => Empty_List,
+          Handled_Statement_Sequence =>
+            Make_Handled_Sequence_Of_Statements (Loc,
+              Statements => New_List (
+                Make_Pragma (Loc,
+                  Chars                        => Name_Check,
+                  Pragma_Argument_Associations => New_List (
+                    Make_Pragma_Argument_Association (Loc,
+                      Expression =>
+                        Make_Identifier (Loc, Name_Initial_Condition)),
+                    Make_Pragma_Argument_Association (Loc,
+                      Expression => New_Copy_Tree (Expr)))))));
 
-      Check :=
-        Make_Pragma (Loc,
-          Chars                        => Name_Check,
-          Pragma_Argument_Associations => New_List (
-            Make_Pragma_Argument_Association (Loc,
-              Expression => Make_Identifier (Loc, Name_Initial_Condition)),
-            Make_Pragma_Argument_Association (Loc,
-              Expression => New_Copy_Tree (Expr))));
+      Append_To (Body_List, Proc_Body);
+
+      --  The initial condition procedure requires debug info when initial
+      --  condition is subject to Source Coverage Obligations.
+
+      Proc_Body_Id := Defining_Entity (Proc_Body);
+
+      if Generate_SCO then
+         Set_Needs_Debug_Info (Proc_Body_Id);
+      end if;
+
+      --  The location of the initial condition procedure call must be as close
+      --  as possible to the intended semantic location of the check because
+      --  the ABE mechanism relies heavily on accurate locations.
+
+      Call_Loc := End_Keyword_Location (N);
+
+      --  Generate:
+      --    <Pack_Id>Initial_Condition;
+
+      Call :=
+        Make_Procedure_Call_Statement (Call_Loc,
+          Name => New_Occurrence_Of (Proc_Id, Call_Loc));
+
+      Append_To (Call_List, Call);
 
-      Append_To (List, Check);
-      Analyze (Check);
+      Analyze (Proc_Decl);
+      Analyze (Proc_Body);
+      Analyze (Call);
    end Expand_Pragma_Initial_Condition;
 
    ------------------------------------