[multiple changes]

2017-11-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* atree.ads (Nkind_In): Add 10 and 11 parameter versions.
	* checks.adb (Install_Primitive_Elaboration_Check): Mark the setting of
	the elaboration flag as elaboration code.
	* einfo.adb (Contract): Update the comments.
	(Ignore_SPARK_Mode_Pragmas): Update the comments.
	(SPARK_Aux_Pragma): Update the comments.
	(SPARK_Aux_Pragma_Inherited): Update the comments.
	(SPARK_Pragma): Update the comments. The attribute now applies
	to all types and abstract states.
	(SPARK_Pragma_Inherited): Update the comments. The attribute now
	applies to all types and abstract states.
	(Set_Contract): Update the comments.
	(Set_Ignore_SPARK_Mode_Pragmas): Update the comments.
	(Set_SPARK_Aux_Pragma): Update the comments.
	(Set_SPARK_Aux_Pragma_Inherited): Update the comments.
	(Set_SPARK_Pragma): Update the comments. The attribute now applies to
	all types and abstract states.
	(Set_SPARK_Pragma_Inherited): Update the comments. The attribute now
	applies to all types and abstract states.
	(Write_Field40_Name): Add output for SPARK_Pragma when it appears on a
	type and abstract states.
	* einfo.ads: Update the documentation of attributes SPARK_Pragma and
	SPARK_Pragma_Inherited.  Both of them now apply to all types and
	abstract states.
	* exp_util.adb (Set_Elaboration_Flag): Mark the setting of the
	elaboration flag as elaboration code.
	* sem_ch3.adb: Add with and use clauses for Sem_Elab.
	(Analyze_Full_Type_Declaration): Set the SPARK_Mode of the type. Record
	a derived type for later processing by the ABE mechanism.
	(Analyze_Incomplete_Type_Decl): Set the SPARK_Mode of the type.
	(Analyze_Private_Extension_Declaration): Set the SPARK_Mode of the
	type.
	* sem_ch7.adb (Analyze_Private_Type_Declaration): Set the SPARK_Mode of
	the type.
	* sem_elab.adb: Define the term "early call region".  Update the
	terminology for "scenario" and "target".  Update the architecture of
	the ABE mechanism.  Update the steps which must be taken when adding a
	new scenario.  Update the section on debugging ABE issues.  Add new
	hash tables Early_Call_Regions and Recorded_SPARK_Scenarios.  Add new
	table SPARK_Scenarios.  Hash table Elaboration_Context is now
	Elaboration_Statuses.  The majority of Process_xxx routines have been
	updated to better reflect their role.
	(Add_Unit): Reimplemented.
	(Check_Elaboration_Constituent): New routine.
	(Check_Elaboration_Scenarios): Verify previously recorded scenarios for
	conditional ABE issues. Verify previously recorded SPARK scenarios.
	(Check_SPARK_Derived_Type): New routine.
	(Check_SPARK_Instantiation): New routine.
	(Check_SPARK_Scenario): New routine.
	(Check_SPARK_Refined_State_Pragma): New routine.
	(Early_Call_Region): New routine.
	(Elaboration_Status): New routine.
	(Ensure_Prior_Elaboration): Add new formal parameter Prag_Nam. The
	implicit Elabotate[_All] pragma is now specified via Prag_Nam.
	(Find_Early_Call_Region): New routine.
	(Info_Scenario): Add output for refinement constituents.
	(Is_Recorded_SPARK_Scenario): New routine.
	(Is_Suitable_SPARK_Derived_Type): New routine.
	(Is_Suitable_SPARK_Instantiation): New routine.
	(Is_Suitable_SPARK_Refined_State_Pragma): New routine.
	(Is_Visited_Body): New routine.
	(Kill_Elaboration_Scenario): Reimplemented.
	(Output_Active_Scenarios): Add output for pragma Refined_State.
	(Output_SPARK_Refined_State_Pragma): New routine.
	(Process_Conditional_ABE_Call): Remove the use of -gnatd.v. The effect
	is now achieved by different means.
	(Process_Conditional_ABE_Call_SPARK): Verify that a call which precedes
	the subprogram body appears within the early call region of the body.
	Either ensure the prior elaboration of external subprograms or verify
	that the context meets the suitable elaboration requirement.
	(Process_Conditional_ABE_Instantiation_SPARK): New routine.
	(Record_Elaboration_Scenario): Reimplement the portion which enforces
	the level restrictions of the static model. Add support for SPARK
	scenarios.
	(Record_SPARK_Elaboration_Scenario): New routine.
	(Reset_Visited_Bodies): New routine.
	(Set_Early_Call_Region): New routine.
	(Set_Elaboration_Status): New routine.
	(Set_Is_Recorded_SPARK_Scenario): New routine.
	(Update_Elaboration_Scenario): Reimplemented.
	* sem_elab.ads: Add new subtype Library_Or_Instantiation_Level.
	* sem_prag.adb (Analyze_Refined_State_In_Decl_Part): Save the pragma
	for examination by the ABE Processing phase.
	(Create_Abstract_State): Save the SPARK_Mode from the context.
	* sem_util.adb (Is_Non_Preelaborable_Construct): New routine.
	* sem_util.ads (Is_Non_Preelaborable_Construct): New routine.
	* sinfo.adb (Is_Elaboration_Code): New routine.
	(Set_Is_Elaboration_Code): New routine.
	(Nkind_In): Add 10 and 11 parameter versions.
	* sinfo.ads: Add new attribute Is_Elaboration_Code along with
	occurrences in nodes.
	(Is_Elaboration_Code): New routine along with pragma Inline.
	(Set_Is_Elaboration_Code): New routine along with pragma Inline.
	(Nkind_In): Add 10 and 11 parameter versions.

2017-11-16  Justin Squirek  <squirek@adacore.com>

	* sem.adb (Analyze): Remove requirement that the original node of N be
	an operator in the case that analysis on the node yields the relevant
	operator - so prefer it instead.

From-SVN: r254802

17 files changed, 4339 insertions, 1348 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 50b3084..b18c46f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,106 @@
+2017-11-16  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* atree.ads (Nkind_In): Add 10 and 11 parameter versions.
+	* checks.adb (Install_Primitive_Elaboration_Check): Mark the setting of
+	the elaboration flag as elaboration code.
+	* einfo.adb (Contract): Update the comments.
+	(Ignore_SPARK_Mode_Pragmas): Update the comments.
+	(SPARK_Aux_Pragma): Update the comments.
+	(SPARK_Aux_Pragma_Inherited): Update the comments.
+	(SPARK_Pragma): Update the comments. The attribute now applies
+	to all types and abstract states.
+	(SPARK_Pragma_Inherited): Update the comments. The attribute now
+	applies to all types and abstract states.
+	(Set_Contract): Update the comments.
+	(Set_Ignore_SPARK_Mode_Pragmas): Update the comments.
+	(Set_SPARK_Aux_Pragma): Update the comments.
+	(Set_SPARK_Aux_Pragma_Inherited): Update the comments.
+	(Set_SPARK_Pragma): Update the comments. The attribute now applies to
+	all types and abstract states.
+	(Set_SPARK_Pragma_Inherited): Update the comments. The attribute now
+	applies to all types and abstract states.
+	(Write_Field40_Name): Add output for SPARK_Pragma when it appears on a
+	type and abstract states.
+	* einfo.ads: Update the documentation of attributes SPARK_Pragma and
+	SPARK_Pragma_Inherited.  Both of them now apply to all types and
+	abstract states.
+	* exp_util.adb (Set_Elaboration_Flag): Mark the setting of the
+	elaboration flag as elaboration code.
+	* sem_ch3.adb: Add with and use clauses for Sem_Elab.
+	(Analyze_Full_Type_Declaration): Set the SPARK_Mode of the type. Record
+	a derived type for later processing by the ABE mechanism.
+	(Analyze_Incomplete_Type_Decl): Set the SPARK_Mode of the type.
+	(Analyze_Private_Extension_Declaration): Set the SPARK_Mode of the
+	type.
+	* sem_ch7.adb (Analyze_Private_Type_Declaration): Set the SPARK_Mode of
+	the type.
+	* sem_elab.adb: Define the term "early call region".  Update the
+	terminology for "scenario" and "target".  Update the architecture of
+	the ABE mechanism.  Update the steps which must be taken when adding a
+	new scenario.  Update the section on debugging ABE issues.  Add new
+	hash tables Early_Call_Regions and Recorded_SPARK_Scenarios.  Add new
+	table SPARK_Scenarios.  Hash table Elaboration_Context is now
+	Elaboration_Statuses.  The majority of Process_xxx routines have been
+	updated to better reflect their role.
+	(Add_Unit): Reimplemented.
+	(Check_Elaboration_Constituent): New routine.
+	(Check_Elaboration_Scenarios): Verify previously recorded scenarios for
+	conditional ABE issues. Verify previously recorded SPARK scenarios.
+	(Check_SPARK_Derived_Type): New routine.
+	(Check_SPARK_Instantiation): New routine.
+	(Check_SPARK_Scenario): New routine.
+	(Check_SPARK_Refined_State_Pragma): New routine.
+	(Early_Call_Region): New routine.
+	(Elaboration_Status): New routine.
+	(Ensure_Prior_Elaboration): Add new formal parameter Prag_Nam. The
+	implicit Elabotate[_All] pragma is now specified via Prag_Nam.
+	(Find_Early_Call_Region): New routine.
+	(Info_Scenario): Add output for refinement constituents.
+	(Is_Recorded_SPARK_Scenario): New routine.
+	(Is_Suitable_SPARK_Derived_Type): New routine.
+	(Is_Suitable_SPARK_Instantiation): New routine.
+	(Is_Suitable_SPARK_Refined_State_Pragma): New routine.
+	(Is_Visited_Body): New routine.
+	(Kill_Elaboration_Scenario): Reimplemented.
+	(Output_Active_Scenarios): Add output for pragma Refined_State.
+	(Output_SPARK_Refined_State_Pragma): New routine.
+	(Process_Conditional_ABE_Call): Remove the use of -gnatd.v. The effect
+	is now achieved by different means.
+	(Process_Conditional_ABE_Call_SPARK): Verify that a call which precedes
+	the subprogram body appears within the early call region of the body.
+	Either ensure the prior elaboration of external subprograms or verify
+	that the context meets the suitable elaboration requirement.
+	(Process_Conditional_ABE_Instantiation_SPARK): New routine.
+	(Record_Elaboration_Scenario): Reimplement the portion which enforces
+	the level restrictions of the static model. Add support for SPARK
+	scenarios.
+	(Record_SPARK_Elaboration_Scenario): New routine.
+	(Reset_Visited_Bodies): New routine.
+	(Set_Early_Call_Region): New routine.
+	(Set_Elaboration_Status): New routine.
+	(Set_Is_Recorded_SPARK_Scenario): New routine.
+	(Update_Elaboration_Scenario): Reimplemented.
+	* sem_elab.ads: Add new subtype Library_Or_Instantiation_Level.
+	* sem_prag.adb (Analyze_Refined_State_In_Decl_Part): Save the pragma
+	for examination by the ABE Processing phase.
+	(Create_Abstract_State): Save the SPARK_Mode from the context.
+	* sem_util.adb (Is_Non_Preelaborable_Construct): New routine.
+	* sem_util.ads (Is_Non_Preelaborable_Construct): New routine.
+	* sinfo.adb (Is_Elaboration_Code): New routine.
+	(Set_Is_Elaboration_Code): New routine.
+	(Nkind_In): Add 10 and 11 parameter versions.
+	* sinfo.ads: Add new attribute Is_Elaboration_Code along with
+	occurrences in nodes.
+	(Is_Elaboration_Code): New routine along with pragma Inline.
+	(Set_Is_Elaboration_Code): New routine along with pragma Inline.
+	(Nkind_In): Add 10 and 11 parameter versions.
+
+2017-11-16  Justin Squirek  <squirek@adacore.com>
+
+	* sem.adb (Analyze): Remove requirement that the original node of N be
+	an operator in the case that analysis on the node yields the relevant
+	operator - so prefer it instead.
+
 2017-11-16  Bob Duff  <duff@adacore.com>
 
 	* sem_ch6.adb (Create_Extra_Formals): The type of the BIP_Object_Access
diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
index 1a7e36c..0a44164 100644
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -1866,6 +1866,42 @@ package body Atree is
       return Nkind_In (Nkind (N), V1, V2, V3, V4, V5, V6, V7, V8, V9);
    end Nkind_In;
 
+   function Nkind_In
+     (N   : Node_Id;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind) return Boolean
+   is
+   begin
+      return Nkind_In (Nkind (N), V1, V2, V3, V4, V5, V6, V7, V8, V9, V10);
+   end Nkind_In;
+
+   function Nkind_In
+     (N   : Node_Id;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind;
+      V11 : Node_Kind) return Boolean
+   is
+   begin
+      return Nkind_In (Nkind (N), V1, V2, V3, V4, V5, V6, V7, V8, V9, V10,
+                                  V11);
+   end Nkind_In;
+
    --------
    -- No --
    --------
diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads
index bf0da16..b01f873 100644
--- a/gcc/ada/atree.ads
+++ b/gcc/ada/atree.ads
@@ -746,6 +746,33 @@ package Atree is
       V8 : Node_Kind;
       V9 : Node_Kind) return Boolean;
 
+   function Nkind_In
+     (N   : Node_Id;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind) return Boolean;
+
+   function Nkind_In
+     (N   : Node_Id;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind;
+      V11 : Node_Kind) return Boolean;
+
    pragma Inline (Nkind_In);
    --  Inline all above functions
 
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index c4b37e7..f47e635 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -7841,10 +7841,11 @@ package body Checks is
       Subp_Id   : constant Entity_Id  := Unique_Defining_Entity (Subp_Body);
       Subp_Decl : constant Node_Id    := Unit_Declaration_Node (Subp_Id);
 
-      Decls   : List_Id;
-      Flag_Id : Entity_Id;
-      Set_Ins : Node_Id;
-      Tag_Typ : Entity_Id;
+      Decls    : List_Id;
+      Flag_Id  : Entity_Id;
+      Set_Ins  : Node_Id;
+      Set_Stmt : Node_Id;
+      Tag_Typ  : Entity_Id;
 
    --  Start of processing for Install_Primitive_Elaboration_Check
 
@@ -7878,8 +7879,8 @@ package body Checks is
       elsif Nkind (Context) = N_Compilation_Unit then
          return;
 
-      --  Only nonabstract library-level source primitives are considered for
-      --  this check.
+      --  Do not consider anything other than nonabstract library-level source
+      --  primitives.
 
       elsif not
         (Comes_From_Source (Subp_Id)
@@ -7996,10 +7997,18 @@ package body Checks is
       --  Generate:
       --    E := True;
 
-      Insert_After_And_Analyze (Set_Ins,
+      Set_Stmt :=
         Make_Assignment_Statement (Loc,
           Name       => New_Occurrence_Of (Flag_Id, Loc),
-          Expression => New_Occurrence_Of (Standard_True, Loc)));
+          Expression => New_Occurrence_Of (Standard_True, Loc));
+
+      --  Mark the assignment statement as elaboration code. This allows the
+      --  early call region mechanism (see Sem_Elab) to properly ignore such
+      --  assignments even though they are non-preelaborable code.
+
+      Set_Is_Elaboration_Code (Set_Stmt);
+
+      Insert_After_And_Analyze (Set_Ins, Set_Stmt);
    end Install_Primitive_Elaboration_Check;
 
    --------------------------
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 94e3261..1312965 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -1265,14 +1265,14 @@ package body Einfo is
    function Contract (Id : E) return N is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Type,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Type,      --  concurrent types
                        E_Task_Body,
                        E_Task_Type)
            or else
-         Ekind_In (Id, E_Constant,         --  object variants
+         Ekind_In (Id, E_Constant,            --  objects
                        E_Variable)
            or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Entry,               --  overloadable
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -1281,11 +1281,11 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body)
            or else
-         Ekind (Id) = E_Void);             --  special purpose
+         Ekind (Id) = E_Void);                --  special purpose
       return Node34 (Id);
    end Contract;
 
@@ -1996,12 +1996,12 @@ package body Einfo is
    function Ignore_SPARK_Mode_Pragmas (Id : E) return B is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Body,      --  concurrent types
                        E_Protected_Type,
                        E_Task_Body,
                        E_Task_Type)
           or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Entry,               --  overloadable
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -2010,7 +2010,7 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body));
       return Flag301 (Id);
@@ -3322,10 +3322,10 @@ package body Einfo is
    function SPARK_Aux_Pragma (Id : E) return N is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Type,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Type,      --  concurrent types
                        E_Task_Type)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body));
       return Node41 (Id);
@@ -3334,10 +3334,10 @@ package body Einfo is
    function SPARK_Aux_Pragma_Inherited (Id : E) return B is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Type,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Type,      --  concurrent types
                        E_Task_Type)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body));
       return Flag266 (Id);
@@ -3346,15 +3346,11 @@ package body Einfo is
    function SPARK_Pragma (Id : E) return N is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
-                       E_Protected_Type,
-                       E_Task_Body,
-                       E_Task_Type)
-          or else
-         Ekind_In (Id, E_Constant,         --  object variants
+        (Ekind_In (Id, E_Constant,            --  objects
                        E_Variable)
           or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Abstract_State,      --  overloadable
+                       E_Entry,
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -3363,26 +3359,27 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body)
            or else
-         Ekind (Id) = E_Void);             --  special purpose
+         Ekind (Id) = E_Void                  --  special purpose
+           or else
+         Ekind_In (Id, E_Protected_Body,      --  types
+                       E_Task_Body)
+           or else
+         Is_Type (Id));
       return Node40 (Id);
    end SPARK_Pragma;
 
    function SPARK_Pragma_Inherited (Id : E) return B is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
-                       E_Protected_Type,
-                       E_Task_Body,
-                       E_Task_Type)
-          or else
-         Ekind_In (Id, E_Constant,         --  object variants
+        (Ekind_In (Id, E_Constant,            --  objects
                        E_Variable)
           or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Abstract_State,      --  overloadable
+                       E_Entry,
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -3391,11 +3388,16 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body)
            or else
-         Ekind (Id) = E_Void);             --  special purpose
+         Ekind (Id) = E_Void                  --  special purpose
+           or else
+         Ekind_In (Id, E_Protected_Body,      --  types
+                       E_Task_Body)
+           or else
+         Is_Type (Id));
       return Flag265 (Id);
    end SPARK_Pragma_Inherited;
 
@@ -4092,14 +4094,14 @@ package body Einfo is
    procedure Set_Contract (Id : E; V : N) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Type,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Type,      --  concurrent types
                        E_Task_Body,
                        E_Task_Type)
            or else
-         Ekind_In (Id, E_Constant,         --  object variants
+         Ekind_In (Id, E_Constant,            --  objects
                        E_Variable)
            or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Entry,               --  overloadable
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -4108,11 +4110,11 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body)
            or else
-         Ekind (Id) = E_Void);             --  special purpose
+         Ekind (Id) = E_Void);                --  special purpose
       Set_Node34 (Id, V);
    end Set_Contract;
 
@@ -5173,12 +5175,12 @@ package body Einfo is
    procedure Set_Ignore_SPARK_Mode_Pragmas (Id : E; V : B := True) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Body,      --  concurrent types
                        E_Protected_Type,
                        E_Task_Body,
                        E_Task_Type)
           or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Entry,               --  overloadable
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -5187,7 +5189,7 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body));
       Set_Flag301 (Id, V);
@@ -6546,10 +6548,10 @@ package body Einfo is
    procedure Set_SPARK_Aux_Pragma (Id : E; V : N) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Type,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Type,      --  concurrent types
                        E_Task_Type)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body));
       Set_Node41 (Id, V);
@@ -6558,10 +6560,10 @@ package body Einfo is
    procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Type,   --  concurrent variants
+        (Ekind_In (Id, E_Protected_Type,      --  concurrent types
                        E_Task_Type)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body));
       Set_Flag266 (Id, V);
@@ -6570,15 +6572,11 @@ package body Einfo is
    procedure Set_SPARK_Pragma (Id : E; V : N) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
-                       E_Protected_Type,
-                       E_Task_Body,
-                       E_Task_Type)
-          or else
-         Ekind_In (Id, E_Constant,         --  object variants
+        (Ekind_In (Id, E_Constant,            --  objects
                        E_Variable)
           or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Abstract_State,      --  overloadable
+                       E_Entry,
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -6587,26 +6585,27 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body)
            or else
-         Ekind (Id) = E_Void);             --  special purpose
+         Ekind (Id) = E_Void                  --  special purpose
+           or else
+         Ekind_In (Id, E_Protected_Body,      --  types
+                       E_Task_Body)
+           or else
+         Is_Type (Id));
       Set_Node40 (Id, V);
    end Set_SPARK_Pragma;
 
    procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Protected_Body,   --  concurrent variants
-                       E_Protected_Type,
-                       E_Task_Body,
-                       E_Task_Type)
-          or else
-         Ekind_In (Id, E_Constant,         --  object variants
+        (Ekind_In (Id, E_Constant,            --  objects
                        E_Variable)
           or else
-         Ekind_In (Id, E_Entry,            --  overloadable variants
+         Ekind_In (Id, E_Abstract_State,      --  overloadable
+                       E_Entry,
                        E_Entry_Family,
                        E_Function,
                        E_Generic_Function,
@@ -6615,11 +6614,16 @@ package body Einfo is
                        E_Procedure,
                        E_Subprogram_Body)
            or else
-         Ekind_In (Id, E_Generic_Package,  --  package variants
+         Ekind_In (Id, E_Generic_Package,     --  packages
                        E_Package,
                        E_Package_Body)
            or else
-         Ekind (Id) = E_Void);             --  special purpose
+         Ekind (Id) = E_Void                  --  special purpose
+           or else
+         Ekind_In (Id, E_Protected_Body,      --  types
+                       E_Task_Body)
+           or else
+         Is_Type (Id));
       Set_Flag265 (Id, V);
    end Set_SPARK_Pragma_Inherited;
 
@@ -11200,7 +11204,8 @@ package body Einfo is
    procedure Write_Field40_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
-         when E_Constant
+         when E_Abstract_State
+            | E_Constant
             | E_Entry
             | E_Entry_Family
             | E_Function
@@ -11212,12 +11217,11 @@ package body Einfo is
             | E_Package_Body
             | E_Procedure
             | E_Protected_Body
-            | E_Protected_Type
             | E_Subprogram_Body
             | E_Task_Body
-            | E_Task_Type
             | E_Variable
             | E_Void
+            | Type_Kind
          =>
             Write_Str ("SPARK_Pragma");
 
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 7bcf3f9..ab05611 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -4284,20 +4284,42 @@ package Einfo is
 --       inherited, rather than a local one.
 
 --    SPARK_Pragma (Node40)
---       Present in concurrent type, constant, entry, operator, [generic]
---       package, package body, [generic] subprogram, subprogram body and
---       variable entities. Points to the N_Pragma node that applies to the
---       initial declaration or body. This is either set by a local SPARK_Mode
---       pragma or is inherited from the context (from an outer scope for the
---       spec case or from the spec for the body case). In the case where it
---       is inherited the flag SPARK_Pragma_Inherited is set. Empty if no
---       SPARK_Mode pragma is applicable.
+--       Present in the following entities:
+--
+--         abstract states
+--         constants
+--         entries
+--         operators
+--         [generic] packages
+--         package bodies
+--         [generic] subprograms
+--         subprogram bodies
+--         variables
+--         types
+--
+--       Points to the N_Pragma node that applies to the initial declaration or
+--       body. This is either set by a local SPARK_Mode pragma or is inherited
+--       from the context (from an outer scope for the spec case or from the
+--       spec for the body case). In the case where the attribute is inherited,
+--       flag SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma is
+--       applicable.
 
 --    SPARK_Pragma_Inherited (Flag265)
---       Present in concurrent type, constant, entry, operator, [generic]
---       package, package body, [generic] subprogram, subprogram body and
---       variable entities. Set if the SPARK_Pragma attribute points to a
---       pragma that is inherited, rather than a local one.
+--       Present in the following entities:
+--
+--         abstract states
+--         constants
+--         entries
+--         operators
+--         [generic] packages
+--         package bodies
+--         [generic] subprograms
+--         subprogram bodies
+--         variables
+--         types
+--
+--       Set if the SPARK_Pragma attribute points to an inherited pragma rather
+--       than a local one.
 
 --    Spec_Entity (Node19)
 --       Defined in package body entities. Points to corresponding package
@@ -5617,6 +5639,7 @@ package Einfo is
    --    Derived_Type_Link                   (Node31)
    --    No_Tagged_Streams_Pragma            (Node32)
    --    Linker_Section_Pragma               (Node33)
+   --    SPARK_Pragma                        (Node40)
 
    --    Depends_On_Private                  (Flag14)
    --    Disable_Controlled                  (Flag253)
@@ -5687,6 +5710,7 @@ package Einfo is
    --    Partial_View_Has_Unknown_Discr      (Flag280)
    --    Size_Depends_On_Discriminant        (Flag177)
    --    Size_Known_At_Compile_Time          (Flag92)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Strict_Alignment                    (Flag145)  (base type only)
    --    Suppress_Initialization             (Flag105)
    --    Treat_As_Volatile                   (Flag41)
@@ -5718,9 +5742,11 @@ package Einfo is
    --    Body_References                     (Elist16)
    --    Non_Limited_View                    (Node19)
    --    Encapsulating_State                 (Node32)
+   --    SPARK_Pragma                        (Node40)
    --    From_Limited_With                   (Flag159)
    --    Has_Partial_Visible_Refinement      (Flag296)
    --    Has_Visible_Refinement              (Flag263)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Has_Non_Limited_View                (synth)
    --    Has_Non_Null_Visible_Refinement     (synth)
    --    Has_Null_Visible_Refinement         (synth)
@@ -6488,11 +6514,9 @@ package Einfo is
    --    Anonymous_Object                    (Node30)
    --    Contract                            (Node34)
    --    Entry_Max_Queue_Lengths_Array       (Node35)
-   --    SPARK_Pragma                        (Node40)
    --    SPARK_Aux_Pragma                    (Node41)
    --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    SPARK_Aux_Pragma_Inherited          (Flag266)
-   --    SPARK_Pragma_Inherited              (Flag265)
    --    Uses_Lock_Free                      (Flag188)
    --    First_Component                     (synth)
    --    First_Component_Or_Discriminant     (synth)
@@ -6506,7 +6530,6 @@ package Einfo is
    --  E_Record_Subtype
    --    Direct_Primitive_Operations         (Elist10)
    --    Access_Disp_Table                   (Elist16)  (base type only)
-   --    Access_Disp_Table_Elab_Flag         (Node30)   (base type only)
    --    Cloned_Subtype                      (Node16)   (subtype case only)
    --    First_Entity                        (Node17)
    --    Corresponding_Concurrent_Type       (Node18)
@@ -6518,6 +6541,7 @@ package Einfo is
    --    Interfaces                          (Elist25)
    --    Dispatch_Table_Wrappers             (Elist26)  (base type only)
    --    Underlying_Record_View              (Node28)   (base type only)
+   --    Access_Disp_Table_Elab_Flag         (Node30)   (base type only)
    --    Component_Alignment                 (special)  (base type only)
    --    C_Pass_By_Copy                      (Flag125)  (base type only)
    --    Has_Dispatch_Table                  (Flag220)  (base tagged type only)
@@ -6640,7 +6664,6 @@ package Einfo is
    --    Relative_Deadline_Variable          (Node28)   (base type only)
    --    Anonymous_Object                    (Node30)
    --    Contract                            (Node34)
-   --    SPARK_Pragma                        (Node40)
    --    SPARK_Aux_Pragma                    (Node41)
    --    Delay_Cleanups                      (Flag114)
    --    Has_Master_Entity                   (Flag21)
@@ -6648,7 +6671,6 @@ package Einfo is
    --    Ignore_SPARK_Mode_Pragmas           (Flag301)
    --    Is_Elaboration_Checks_OK_Id         (Flag148)
    --    SPARK_Aux_Pragma_Inherited          (Flag266)
-   --    SPARK_Pragma_Inherited              (Flag265)
    --    First_Component                     (synth)
    --    First_Component_Or_Discriminant     (synth)
    --    Has_Entries                         (synth)
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 6ebcc4c..c5e565b 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -12459,11 +12459,19 @@ package body Exp_Util is
 
          else
             Check_Restriction (No_Elaboration_Code, N);
+
             Asn :=
               Make_Assignment_Statement (Loc,
                 Name       => New_Occurrence_Of (Ent, Loc),
                 Expression => Make_Integer_Literal (Loc, Uint_1));
 
+            --  Mark the assignment statement as elaboration code. This allows
+            --  the early call region mechanism (see Sem_Elab) to properly
+            --  ignore such assignments even though they are non-preelaborable
+            --  code.
+
+            Set_Is_Elaboration_Code (Asn);
+
             if Nkind (Parent (N)) = N_Subunit then
                Insert_After (Corresponding_Stub (Parent (N)), Asn);
             else
diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb
index 02c8fa2..c0c8962 100644
--- a/gcc/ada/sem.adb
+++ b/gcc/ada/sem.adb
@@ -740,17 +740,32 @@ package body Sem is
 
       Debug_A_Exit ("analyzing  ", N, "  (done)");
 
-      --  Mark relevant use-type and use-package clauses as effective using the
-      --  original node, because constant folding may have occurred and removed
-      --  references that need to be examined. If the node in question is
-      --  overloaded then this is deferred until resolution.
-
-      if Nkind (Original_Node (N)) in N_Op
-        and then Present (Entity (Original_Node (N)))
-        and then not Is_Overloaded (Original_Node (N))
-      then
-         Mark_Use_Clauses (Original_Node (N));
-      end if;
+      --  Mark relevant use-type and use-package clauses as effective
+      --  preferring the original node over the analyzed one in the case that
+      --  constant folding has occurred and removed references that need to be
+      --  examined. Also, if the node in question is overloaded then this is
+      --  deferred until resolution.
+
+      declare
+         Operat : Node_Id := Empty;
+      begin
+         --  Attempt to obtain a checkable operator node
+
+         if Nkind (Original_Node (N)) in N_Op then
+            Operat := Original_Node (N);
+         elsif Nkind (N) in N_Op then
+            Operat := N;
+         end if;
+
+         --  Mark the operator
+
+         if Present (Operat)
+           and then Present (Entity (Operat))
+           and then not Is_Overloaded (Operat)
+         then
+            Mark_Use_Clauses (Operat);
+         end if;
+      end;
 
       --  Now that we have analyzed the node, we call the expander to perform
       --  possible expansion. We skip this for subexpressions, because we don't
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 9dc3902..2c75337 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -61,6 +61,7 @@ with Sem_Ch13;  use Sem_Ch13;
 with Sem_Dim;   use Sem_Dim;
 with Sem_Disp;  use Sem_Disp;
 with Sem_Dist;  use Sem_Dist;
+with Sem_Elab;  use Sem_Elab;
 with Sem_Elim;  use Sem_Elim;
 with Sem_Eval;  use Sem_Eval;
 with Sem_Mech;  use Sem_Mech;
@@ -3120,6 +3121,11 @@ package body Sem_Ch3 is
       if not Analyzed (T) then
          Set_Analyzed (T);
 
+         --  Set the SPARK mode from the current context
+
+         Set_SPARK_Pragma           (T, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (T);
+
          case Nkind (Def) is
             when N_Access_To_Subprogram_Definition =>
                Access_Subprogram_Declaration (T, Def);
@@ -3167,6 +3173,11 @@ package body Sem_Ch3 is
                   Set_Has_Predicates (Def_Id);
                end if;
 
+               --  Save the scenario for examination by the ABE Processing
+               --  phase.
+
+               Record_Elaboration_Scenario (N);
+
             when N_Enumeration_Type_Definition =>
                Enumeration_Type_Declaration (T, Def);
 
@@ -3362,10 +3373,15 @@ package body Sem_Ch3 is
 
       T := Find_Type_Name (N);
 
-      Set_Ekind (T, E_Incomplete_Type);
-      Init_Size_Align (T);
-      Set_Is_First_Subtype (T, True);
-      Set_Etype (T, T);
+      Set_Ekind            (T, E_Incomplete_Type);
+      Set_Etype            (T, T);
+      Set_Is_First_Subtype (T);
+      Init_Size_Align      (T);
+
+      --  Set the SPARK mode from the current context
+
+      Set_SPARK_Pragma           (T, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited (T);
 
       --  Ada 2005 (AI-326): Minimum decoration to give support to tagged
       --  incomplete types.
@@ -5065,6 +5081,11 @@ package body Sem_Ch3 is
       Set_Is_First_Subtype (T);
       Make_Class_Wide_Type (T);
 
+      --  Set the SPARK mode from the current context
+
+      Set_SPARK_Pragma           (T, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited (T);
+
       if Unknown_Discriminants_Present (N) then
          Set_Discriminant_Constraint (T, No_Elist);
       end if;
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index f50b866..2e035c7 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -1850,6 +1850,11 @@ package body Sem_Ch7 is
       New_Private_Type (N, Id, N);
       Set_Depends_On_Private (Id);
 
+      --  Set the SPARK mode from the current context
+
+      Set_SPARK_Pragma           (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited (Id);
+
       if Has_Aspects (N) then
          Analyze_Aspect_Specifications (N, Id);
       end if;
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index b3077ad..8c5611c 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -130,6 +130,11 @@ package body Sem_Elab is
    --    block statement, entry body, subprogram body, or task body, ignoring
    --    enclosing packages.
    --
+   --  * Early call region - A section of code which ends at a subprogram body
+   --    and starts from the nearest non-preelaborable construct which precedes
+   --    the subprogram body. The early call region extends from a package body
+   --    to a package spec when the spec carries pragma Elaborate_Body.
+   --
    --  * Generic library level - A type of enclosing level. A scenario or
    --    target is at the generic library level if it appears in a generic
    --    package library unit, ignoring enclosing packages.
@@ -155,15 +160,19 @@ package body Sem_Elab is
    --
    --      - '[Unrestricted_]Access of entries, operators, and subprograms
    --
-   --      -  Assignments to variables
+   --      - Assignments to variables
+   --
+   --      - Calls to entries, operators, and subprograms
+   --
+   --      - Derived type declarations
    --
-   --      -  Calls to entries, operators, and subprograms
+   --      - Instantiations
    --
-   --      -  Instantiations
+   --      - Pragma Refined_State
    --
-   --      -  Reads of variables
+   --      - Reads of variables
    --
-   --      -  Task activation
+   --      - Task activation
    --
    --  * Target - A construct referenced by a scenario. The targets recognized
    --    by the ABE mechanism are as follows:
@@ -175,8 +184,12 @@ package body Sem_Elab is
    --
    --      - For calls, the target is the entry, operator, or subprogram
    --
+   --      - For derived type declarations, the target is the derived type
+   --
    --      - For instantiations, the target is the generic template
    --
+   --      - For pragma Refined_State, the targets are the constituents
+   --
    --      - For reads of variables, the target is the variable
    --
    --      - For task activation, the target is the task body
@@ -205,6 +218,13 @@ package body Sem_Elab is
    --      the ABE mechanism. This eliminates the need to examine the whole
    --      tree in a separate pass.
    --
+   --    * Record certain SPARK scenarios which are not necessarily executable
+   --      during elaboration, but still require elaboration-related checks.
+   --
+   --      Saving only a certain number of nodes improves the performance of
+   --      the ABE mechanism. This eliminates the need to examine the whole
+   --      tree in a separate pass.
+   --
    --    * Detect and diagnose calls in preelaborable or pure units, including
    --      generic bodies.
    --
@@ -237,6 +257,8 @@ package body Sem_Elab is
    --      the call/instantiation/task activation graph. The traversal stops
    --      when an outgoing edge leaves the main unit.
    --
+   --    * Examine all SPARK scenarios saved during the Recording phase
+   --
    --    * Depending on the elaboration model in effect, perform the following
    --      actions:
    --
@@ -259,44 +281,72 @@ package body Sem_Elab is
    -- Architecture --
    ------------------
 
-   --  +------------------------ Recording phase ---------------------------+
-   --  |                                                                    |
-   --  |              Record_Elaboration_Scenario                           |
-   --  |                           |                                        |
-   --  |                           +--> Check_Preelaborated_Call            |
-   --  |                           |                                        |
-   --  |                           +--> Process_Guaranteed_ABE              |
-   --  |                           |                                        |
-   --  +-------------------------  |  --------------------------------------+
-   --                              |
-   --                              |
-   --                              v
-   --                    Top_Level_Scenarios
-   --          +-----------+-----------+ .. +-----------+
-   --          | Scenario1 | Scenario2 | .. | ScenarioN |
-   --          +-----------+-----------+ .. +-----------+
-   --                              |
-   --                              |
-   --  +-------------------------  |  --------------------------------------+
-   --  |                           |                                        |
-   --  |              Check_Elaboration_Scenarios                           |
-   --  |                           |                                        |
-   --  |                           v                                        |
-   --  |       +----------- Process_Scenario <-----------+                  |
-   --  |       |                                         |                  |
-   --  |       +--> Process_Access               Is_Suitable_Scenario       |
-   --  |       |                                         ^                  |
-   --  |       +--> Process_Activation_Call --+          |                  |
-   --  |       |                              +---> Traverse_Body           |
-   --  |       +--> Process_Call -------------+                             |
+   --     Analysis/Resolution
+   --     |
+   --     +- Build_Call_Marker
+   --     |
+   --     +- Build_Variable_Reference_Marker
+   --     |
+   --  +- | -------------------- Recording phase ---------------------------+
+   --  |  v                                                                 |
+   --  |  Record_Elaboration_Scenario                                       |
+   --  |  |                                                                 |
+   --  |  +--> Check_Preelaborated_Call                                     |
+   --  |  |                                                                 |
+   --  |  +--> Process_Guaranteed_ABE                                       |
+   --  |  |    |                                                            |
+   --  |  |    +--> Process_Guaranteed_ABE_Activation                       |
+   --  |  |    |                                                            |
+   --  |  |    +--> Process_Guaranteed_ABE_Call                             |
+   --  |  |    |                                                            |
+   --  |  |    +--> Process_Guaranteed_ABE_Instantiation                    |
+   --  |  |                                                                 |
+   --  +- | ----------------------------------------------------------------+
+   --     |
+   --     |
+   --     +--> SPARK_Scenarios
+   --     |    +-----------+-----------+ .. +-----------+
+   --     |    | Scenario1 | Scenario2 | .. | ScenarioN |
+   --     |    +-----------+-----------+ .. +-----------+
+   --     |
+   --     +--> Top_Level_Scenarios
+   --     |    +-----------+-----------+ .. +-----------+
+   --     |    | Scenario1 | Scenario2 | .. | ScenarioN |
+   --     |    +-----------+-----------+ .. +-----------+
+   --     |
+   --     End of Compilation
+   --     |
+   --  +- | --------------------- Processing phase -------------------------+
+   --  |  v                                                                 |
+   --  |  Check_Elaboration_Scenarios                                       |
+   --  |  |                                                                 |
+   --  |  +--> Check_SPARK_Scenario                                         |
+   --  |  |    |                                                            |
+   --  |  |    +--> Check_SPARK_Derived_Type                                |
+   --  |  |    |                                                            |
+   --  |  |    +--> Check_SPARK_Instantiation                               |
+   --  |  |    |                                                            |
+   --  |  |    +--> Check_SPARK_Refined_State_Pragma                        |
+   --  |  |                                                                 |
+   --  |  +--> Process_Conditional_ABE <---------------------------+        |
+   --  |       |                                                   |        |
+   --  |       +--> Process_Conditional_ABE_Access    Is_Suitable_Scenario  |
+   --  |       |                                                   ^        |
+   --  |       +--> Process_Conditional_ABE_Activation             |        |
+   --  |       |    |                                              |        |
+   --  |       |    +-----------------------------+                |        |
+   --  |       |                                  |                |        |
+   --  |       +--> Process_Conditional_ABE_Call  +--------> Traverse_Body  |
+   --  |       |    |                             |                         |
+   --  |       |    +-----------------------------+                         |
    --  |       |                                                            |
-   --  |       +--> Process_Instantiation                                   |
+   --  |       +--> Process_Conditional_ABE_Instantiation                   |
    --  |       |                                                            |
-   --  |       +--> Process_Variable_Assignment                             |
+   --  |       +--> Process_Conditional_ABE_Variable_Assignment             |
    --  |       |                                                            |
-   --  |       +--> Process_Variable_Reference                              |
+   --  |       +--> Process_Conditional_ABE_Variable_Reference              |
    --  |                                                                    |
-   --  +------------------------- Processing phase -------------------------+
+   --  +--------------------------------------------------------------------+
 
    ----------------------
    -- Important points --
@@ -418,32 +468,42 @@ package body Sem_Elab is
    ---------------------------
 
    --  The following steps describe how to add a new elaboration scenario and
-   --  preserve the existing architecture.
+   --  preserve the existing architecture. Note that not all of the steps may
+   --  need to be carried out.
    --
-   --    1) If necessary, update predicate Is_Scenario
+   --    1) Update predicate Is_Scenario
    --
    --    2) Add predicate Is_Suitable_xxx. Include a call to it in predicate
    --       Is_Suitable_Scenario.
    --
    --    3) Update routine Record_Elaboration_Scenario
    --
-   --    4) Add routine Process_xxx. Include a call to it in Process_Scenario.
+   --    4) Add routine Process_Conditional_ABE_xxx. Include a call to it in
+   --       routine Process_Conditional_ABE.
+   --
+   --    5) Add routine Process_Guaranteed_ABE_xxx. Include a call to it in
+   --       routine Process_Guaranteed_ABE.
    --
-   --    5) Add routine Info_xxx. Include a call to it in Process_xxx.
+   --    6) Add routine Check_SPARK_xxx. Include a call to it in routine
+   --       Check_SPARK_Scenario.
    --
-   --    6) Add routine Output_xxx. Include a call to it in routine
+   --    7) Add routine Info_xxx. Include a call to it in routine
+   --       Process_Conditional_ABE_xxx.
+   --
+   --    8) Add routine Output_xxx. Include a call to it in routine
    --       Output_Active_Scenarios.
    --
-   --    7) If necessary, add a new Extract_xxx_Attributes routine
+   --    9) Add routine Extract_xxx_Attributes
    --
-   --    8) If necessary, update routine Is_Potential_Scenario
+   --   10) Update routine Is_Potential_Scenario
 
    -------------------------
    -- Adding a new target --
    -------------------------
 
    --  The following steps describe how to add a new elaboration target and
-   --  preserve the existing architecture.
+   --  preserve the existing architecture. Note that not all of the steps may
+   --  need to be carried out.
    --
    --    1) Add predicate Is_xxx.
    --
@@ -473,7 +533,8 @@ package body Sem_Elab is
    --    body. The routines of interest are
    --
    --      Record_Elaboration_Scenario
-   --      Process_Scenario
+   --      Process_Conditional_ABE
+   --      Process_Guaranteed_ABE
    --      Traverse_Body
 
    --  * If the issue involves a circularity in the elaboration order, examine
@@ -496,6 +557,10 @@ package body Sem_Elab is
    -- Attributes --
    ----------------
 
+   --  To minimize the amount of code within routines, the ABE mechanism relies
+   --  on "attribute" records to capture relevant information for a scenario or
+   --  a target.
+
    --  The following type captures relevant attributes which pertain to a call
 
    type Call_Attributes is record
@@ -692,23 +757,87 @@ package body Sem_Elab is
    -- Data structures --
    ---------------------
 
+   --  The ABE mechanism employs lists and hash tables to store information
+   --  pertaining to scenarios and targets, as well as the Processing phase.
+   --  The need for data structures comes partly from the size limitation of
+   --  nodes. Note that the use of hash tables is conservative and operations
+   --  are carried out only when a particular hash table has at least one key
+   --  value pair (see xxx_In_Use flags).
+
+   --  The following table stores the early call regions of subprogram bodies
+
+   Early_Call_Regions_Max : constant := 101;
+
+   type Early_Call_Regions_Index is range 0 .. Early_Call_Regions_Max - 1;
+
+   function Early_Call_Regions_Hash
+     (Key : Entity_Id) return Early_Call_Regions_Index;
+   --  Obtain the hash value of entity Key
+
+   Early_Call_Regions_In_Use : Boolean := False;
+   --  This flag flag determines whether table Early_Call_Regions contains at
+   --  least one key/value pair.
+
+   Early_Call_Regions_No_Element : constant Node_Id := Empty;
+
+   package Early_Call_Regions is new Simple_HTable
+     (Header_Num => Early_Call_Regions_Index,
+      Element    => Node_Id,
+      No_Element => Early_Call_Regions_No_Element,
+      Key        => Entity_Id,
+      Hash       => Early_Call_Regions_Hash,
+      Equal      => "=");
+
    --  The following table stores the elaboration status of all units withed by
    --  the main unit.
 
-   Elaboration_Context_Max : constant := 1009;
+   Elaboration_Statuses_Max : constant := 1009;
 
-   type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
+   type Elaboration_Statuses_Index is range 0 .. Elaboration_Statuses_Max - 1;
 
-   function Elaboration_Context_Hash
-     (Key : Entity_Id) return Elaboration_Context_Index;
+   function Elaboration_Statuses_Hash
+     (Key : Entity_Id) return Elaboration_Statuses_Index;
    --  Obtain the hash value of entity Key
 
-   package Elaboration_Context is new Simple_HTable
-     (Header_Num => Elaboration_Context_Index,
+   Elaboration_Statuses_In_Use : Boolean := False;
+   --  This flag flag determines whether table Elaboration_Statuses contains at
+   --  least one key/value pair.
+
+   Elaboration_Statuses_No_Element : constant Elaboration_Attributes :=
+                                       No_Elaboration_Attributes;
+
+   package Elaboration_Statuses is new Simple_HTable
+     (Header_Num => Elaboration_Statuses_Index,
       Element    => Elaboration_Attributes,
-      No_Element => No_Elaboration_Attributes,
+      No_Element => Elaboration_Statuses_No_Element,
       Key        => Entity_Id,
-      Hash       => Elaboration_Context_Hash,
+      Hash       => Elaboration_Statuses_Hash,
+      Equal      => "=");
+
+   --  The following table stores a status flag for each SPARK scenario saved
+   --  in table SPARK_Scenarios.
+
+   Recorded_SPARK_Scenarios_Max : constant := 127;
+
+   type Recorded_SPARK_Scenarios_Index is
+     range 0 .. Recorded_SPARK_Scenarios_Max - 1;
+
+   function Recorded_SPARK_Scenarios_Hash
+     (Key : Node_Id) return Recorded_SPARK_Scenarios_Index;
+   --  Obtain the hash value of Key
+
+   Recorded_SPARK_Scenarios_In_Use : Boolean := False;
+   --  This flag flag determines whether table Recorded_SPARK_Scenarios
+   --  contains at least one key/value pair.
+
+   Recorded_SPARK_Scenarios_No_Element : constant Boolean := False;
+
+   package Recorded_SPARK_Scenarios is new Simple_HTable
+     (Header_Num => Recorded_SPARK_Scenarios_Index,
+      Element    => Boolean,
+      No_Element => Recorded_SPARK_Scenarios_No_Element,
+      Key        => Node_Id,
+      Hash       => Recorded_SPARK_Scenarios_Hash,
       Equal      => "=");
 
    --  The following table stores a status flag for each top-level scenario
@@ -723,10 +852,16 @@ package body Sem_Elab is
      (Key : Node_Id) return Recorded_Top_Level_Scenarios_Index;
    --  Obtain the hash value of entity Key
 
+   Recorded_Top_Level_Scenarios_In_Use : Boolean := False;
+   --  This flag flag determines whether table Recorded_Top_Level_Scenarios
+   --  contains at least one key/value pair.
+
+   Recorded_Top_Level_Scenarios_No_Element : constant Boolean := False;
+
    package Recorded_Top_Level_Scenarios is new Simple_HTable
      (Header_Num => Recorded_Top_Level_Scenarios_Index,
       Element    => Boolean,
-      No_Element => False,
+      No_Element => Recorded_Top_Level_Scenarios_No_Element,
       Key        => Node_Id,
       Hash       => Recorded_Top_Level_Scenarios_Hash,
       Equal      => "=");
@@ -743,6 +878,18 @@ package body Sem_Elab is
       Table_Increment      => 100,
       Table_Name           => "Scenario_Stack");
 
+   --  The following table stores SPARK scenarios which are not necessarily
+   --  executable during elaboration, but still require elaboration-related
+   --  checks.
+
+   package SPARK_Scenarios is new Table.Table
+     (Table_Component_Type => Node_Id,
+      Table_Index_Type     => Int,
+      Table_Low_Bound      => 1,
+      Table_Initial        => 50,
+      Table_Increment      => 100,
+      Table_Name           => "SPARK_Scenarios");
+
    --  The following table stores all top-level scenario saved during the
    --  Recording phase. The contents of this table act as traversal roots
    --  later in the Processing phase. This table must be maintained in a
@@ -767,10 +914,16 @@ package body Sem_Elab is
    function Visited_Bodies_Hash (Key : Node_Id) return Visited_Bodies_Index;
    --  Obtain the hash value of node Key
 
+   Visited_Bodies_In_Use : Boolean := False;
+   --  This flag determines whether table Visited_Bodies contains at least one
+   --  key/value pair.
+
+   Visited_Bodies_No_Element : constant Boolean := False;
+
    package Visited_Bodies is new Simple_HTable
      (Header_Num => Visited_Bodies_Index,
       Element    => Boolean,
-      No_Element => False,
+      No_Element => Visited_Bodies_No_Element,
       Key        => Node_Id,
       Hash       => Visited_Bodies_Hash,
       Equal      => "=");
@@ -779,15 +932,46 @@ package body Sem_Elab is
    -- Local subprograms --
    -----------------------
 
+   --  Multiple local subprograms are utilized to lower the semantic complexity
+   --  of the Recording and Processing phase.
+
    procedure Check_Preelaborated_Call (Call : Node_Id);
-   --  Determine whether entry, operator, or subprogram call Call appears at
-   --  the library level of a preelaborated unit. Emit an error if this is the
-   --  case.
+   pragma Inline (Check_Preelaborated_Call);
+   --  Verify that entry, operator, or subprogram call Call does not appear at
+   --  the library level of a preelaborated unit.
+
+   procedure Check_SPARK_Derived_Type (Typ_Decl : Node_Id);
+   pragma Inline (Check_SPARK_Derived_Type);
+   --  Verify that the freeze node of a derived type denoted by declaration
+   --  Typ_Decl is within the early call region of each overriding primitive
+   --  body that belongs to the derived type (SPARK RM 7.7(8)).
+
+   procedure Check_SPARK_Instantiation (Exp_Inst : Node_Id);
+   pragma Inline (Check_SPARK_Instantiation);
+   --  Verify that expanded instance Exp_Inst does not precede the generic body
+   --  it instantiates (SPARK RM 7.7(6)).
+
+   procedure Check_SPARK_Scenario (N : Node_Id);
+   pragma Inline (Check_SPARK_Scenario);
+   --  Top level dispatcher for verifying SPARK scenarios which are not always
+   --  executable during elaboration but still need elaboration-related checks.
+
+   procedure Check_SPARK_Refined_State_Pragma (N : Node_Id);
+   pragma Inline (Check_SPARK_Refined_State_Pragma);
+   --  Verify that each constituent of Refined_State pragma N which belongs to
+   --  an abstract state mentioned in pragma Initializes has prior elaboration
+   --  with respect to the main unit (SPARK RM 7.7.1(7)).
 
    function Compilation_Unit (Unit_Id : Entity_Id) return Node_Id;
    pragma Inline (Compilation_Unit);
    --  Return the N_Compilation_Unit node of unit Unit_Id
 
+   function Early_Call_Region (Body_Id : Entity_Id) return Node_Id;
+   pragma Inline (Early_Call_Region);
+   --  Return the early call region associated with entry or subprogram body
+   --  Body_Id. IMPORTANT: This routine does not find the early call region.
+   --  To compute it, use routine Find_Early_Call_Region.
+
    procedure Elab_Msg_NE
      (Msg      : String;
       N        : Node_Id;
@@ -800,16 +984,24 @@ package body Sem_Elab is
    --  message, otherwise it emits an error. If flag In_SPARK is set, then
    --  string " in SPARK" is added to the end of the message.
 
+   function Elaboration_Status
+     (Unit_Id : Entity_Id) return Elaboration_Attributes;
+   pragma Inline (Elaboration_Status);
+   --  Return the set of elaboration attributes associated with unit Unit_Id
+
    procedure Ensure_Prior_Elaboration
      (N              : Node_Id;
       Unit_Id        : Entity_Id;
+      Prag_Nam       : Name_Id;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean);
-   --  Guarantee the elaboration of unit Unit_Id with respect to the main unit.
-   --  N denotes the related scenario. Flag In_Partial_Fin should be set when
-   --  the need for elaboration is initiated by a partial finalization routine.
-   --  Flag In_Task_Body should be set when the need for prior elaboration is
-   --  initiated from a task body.
+   --  Guarantee the elaboration of unit Unit_Id with respect to the main unit
+   --  by installing pragma Elaborate or Elaborate_All denoted by Prag_Nam. N
+   --  denotes the related scenario. The flags should be set when the need for
+   --  elaboration was initiated as follows:
+   --
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
    procedure Ensure_Prior_Elaboration_Dynamic
      (N        : Node_Id;
@@ -888,8 +1080,20 @@ package body Sem_Elab is
    --  denoted by N except when N is within an instantiation. In that case the
    --  unit is that of the top-level instantiation.
 
+   function Find_Early_Call_Region
+     (Body_Decl        : Node_Id;
+      Assume_Elab_Body : Boolean := False;
+      Skip_Memoization : Boolean := False) return Node_Id;
+   --  Find the start of the early call region which belongs to subprogram body
+   --  Body_Decl as defined in SPARK RM 7.7. The behavior of the routine is to
+   --  find the early call region, memoize it, and return it, but this behavior
+   --  can be altered. Flag Assume_Elab_Body should be set when a package spec
+   --  may lack pragma Elaborate_Body, but the routine must still examine that
+   --  spec. Flag Skip_Memoization should be set when the routine must avoid
+   --  memoizing the region.
+
    procedure Find_Elaborated_Units;
-   --  Populate table Elaboration_Context with all units which have prior
+   --  Populate table Elaboration_Statuses with all units which have prior
    --  elaboration with respect to the main unit.
 
    function Find_Enclosing_Instance (N : Node_Id) return Node_Id;
@@ -1115,10 +1319,15 @@ package body Sem_Elab is
    --  Determine whether entity Id denotes the protected or unprotected version
    --  of a protected subprogram.
 
+   function Is_Recorded_SPARK_Scenario (N : Node_Id) return Boolean;
+   pragma Inline (Is_Recorded_SPARK_Scenario);
+   --  Determine whether arbitrary node N is a recorded SPARK scenario which
+   --  appears in table SPARK_Scenarios.
+
    function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean;
    pragma Inline (Is_Recorded_Top_Level_Scenario);
-   --  Determine whether arbitrary node is a recorded top-level scenario which
-   --  appears in table Top_Level_Scenarios.
+   --  Determine whether arbitrary node N is a recorded top-level scenario
+   --  which appears in table Top_Level_Scenarios.
 
    function Is_Safe_Activation
      (Call      : Node_Id;
@@ -1177,6 +1386,22 @@ package body Sem_Elab is
    --  Determine whether arbitrary node N is a suitable scenario for ABE
    --  processing.
 
+   function Is_Suitable_SPARK_Derived_Type (N : Node_Id) return Boolean;
+   pragma Inline (Is_Suitable_SPARK_Derived_Type);
+   --  Determine whether arbitrary node N denotes a suitable derived type
+   --  declaration for ABE processing using the SPARK rules.
+
+   function Is_Suitable_SPARK_Instantiation (N : Node_Id) return Boolean;
+   pragma Inline (Is_Suitable_SPARK_Instantiation);
+   --  Determine whether arbitrary node N denotes a suitable instantiation for
+   --  ABE processing using the SPARK rules.
+
+   function Is_Suitable_SPARK_Refined_State_Pragma
+     (N : Node_Id) return Boolean;
+   pragma Inline (Is_Suitable_SPARK_Refined_State_Pragma);
+   --  Determine whether arbitrary node N denotes a suitable Refined_State
+   --  pragma for ABE processing using the SPARK rules.
+
    function Is_Suitable_Variable_Assignment (N : Node_Id) return Boolean;
    pragma Inline (Is_Suitable_Variable_Assignment);
    --  Determine whether arbitrary node N denotes a suitable assignment for ABE
@@ -1198,6 +1423,11 @@ package body Sem_Elab is
    --  Target_Decl is within a context which encloses the current root or is in
    --  a different unit.
 
+   function Is_Visited_Body (Body_Decl : Node_Id) return Boolean;
+   pragma Inline (Is_Visited_Body);
+   --  Determine whether subprogram body Body_Decl is already visited during a
+   --  recursive traversal started from a top-level scenario.
+
    procedure Meet_Elaboration_Requirement
      (N         : Node_Id;
       Target_Id : Entity_Id;
@@ -1221,87 +1451,100 @@ package body Sem_Elab is
    --  Pop the top of the scenario stack. A check is made to ensure that the
    --  scenario being removed is the same as N.
 
-   procedure Process_Access
-     (Attr           : Node_Id;
-      In_Partial_Fin : Boolean;
-      In_Task_Body   : Boolean);
-   --  Perform ABE checks and diagnostics for 'Access to entry, operator, or
-   --  subprogram denoted by Attr. Flag In_Partial_Fin shoud be set when the
-   --  processing is initiated by a partial finalization routine. Flag
-   --  In_Task_Body should be set when the processing is initiated from a task
-   --  body.
-
    generic
       with procedure Process_Single_Activation
         (Call           : Node_Id;
          Call_Attrs     : Call_Attributes;
          Obj_Id         : Entity_Id;
          Task_Attrs     : Task_Attributes;
+         In_Init_Cond   : Boolean;
          In_Partial_Fin : Boolean;
          In_Task_Body   : Boolean);
       --  Perform ABE checks and diagnostics for task activation call Call
       --  which activates task Obj_Id. Call_Attrs are the attributes of the
       --  activation call. Task_Attrs are the attributes of the task type.
-      --  Flag In_Partial_Fin shoud be set when the processing is initiated
-      --  by a partial finalization routine. Flag In_Task_Body should be set
-      --  when the processing is initiated from a task body.
+      --  The flags should be set when the processing was initated as follows:
+      --
+      --    In_Init_Cond   - initial condition procedure
+      --    In_Partial_Fin - partial finalization procedure
+      --    In_Task_Body   - task body
 
-   procedure Process_Activation_Call
+   procedure Process_Activation_Generic
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean);
    --  Perform ABE checks and diagnostics for activation call Call by invoking
    --  routine Process_Single_Activation on each task object being activated.
-   --  Call_Attrs are the attributes of the activation call. In_Partial_Fin
-   --  shoud be set when the processing is initiated by a partial finalization
-   --  routine. Flag In_Task_Body should be set when the processing is started
-   --  from a task body.
+   --  Call_Attrs are the attributes of the activation call. The flags should
+   --  be set when the processing was initiated as follows:
+   --
+   --    In_Init_Cond   - initial condition procedure
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Activation_Conditional_ABE_Impl
-     (Call           : Node_Id;
-      Call_Attrs     : Call_Attributes;
-      Obj_Id         : Entity_Id;
-      Task_Attrs     : Task_Attributes;
+   procedure Process_Conditional_ABE
+     (N              : Node_Id;
+      In_Init_Cond   : Boolean := False;
+      In_Partial_Fin : Boolean := False;
+      In_Task_Body   : Boolean := False);
+   --  Top-level dispatcher for processing of various elaboration scenarios.
+   --  Perform conditional ABE checks and diagnostics for scenario N. The flags
+   --  should be set when the processing was initiated as follows:
+   --
+   --    In_Init_Cond   - initial condition procedure
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
+
+   procedure Process_Conditional_ABE_Access
+     (Attr           : Node_Id;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean);
-   --  Perform common conditional ABE checks and diagnostics for call Call
-   --  which activates task Obj_Id ignoring the Ada or SPARK rules. CAll_Attrs
-   --  are the attributes of the activation call. Task_Attrs are the attributes
-   --  of the task type. Flag In_Partial_Fin shoud be set when the processing
-   --  is initiated by a partial finalization routine. Flag In_Task_Body should
-   --  be set when the processing is initiated from a task body.
+   --  Perform ABE checks and diagnostics for 'Access to entry, operator, or
+   --  subprogram denoted by Attr. The flags should be set when the processing
+   --  was initiated as follows:
+   --
+   --    In_Init_Cond   - initial condition procedure
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Activation_Guaranteed_ABE_Impl
+   procedure Process_Conditional_ABE_Activation_Impl
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
       Obj_Id         : Entity_Id;
       Task_Attrs     : Task_Attributes;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean);
-   --  Perform common guaranteed ABE checks and diagnostics for call Call which
-   --  activates task Obj_Id ignoring the Ada or SPARK rules. Task_Attrs are
-   --  the attributes of the task type. The following parameters are provided
-   --  for compatibility and are unused.
+   --  Perform common conditional ABE checks and diagnostics for call Call
+   --  which activates task Obj_Id ignoring the Ada or SPARK rules. CAll_Attrs
+   --  are the attributes of the activation call. Task_Attrs are the attributes
+   --  of the task type. The flags should be set when the processing was
+   --  initiated as follows:
    --
-   --    Call_Attrs
-   --    In_Partial_Fin
-   --    In_Task_Body
+   --    In_Init_Cond   - initial condition procedure
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Call
+   procedure Process_Conditional_ABE_Call
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
       Target_Id      : Entity_Id;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean);
    --  Top-level dispatcher for processing of calls. Perform ABE checks and
    --  diagnostics for call Call which invokes target Target_Id. Call_Attrs
-   --  are the attributes of the call. Flag In_Partial_Fin shoud be set when
-   --  the processing is initiated by a partial finalization routine. Flag
-   --  In_Task_Body should be set when the processing is started from a task
-   --  body.
+   --  are the attributes of the call. The flags should be set when the
+   --  processing was initiated as follows:
+   --
+   --    In_Init_Cond   - initial condition procedure
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Call_Ada
+   procedure Process_Conditional_ABE_Call_Ada
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
       Target_Id      : Entity_Id;
@@ -1310,58 +1553,40 @@ package body Sem_Elab is
       In_Task_Body   : Boolean);
    --  Perform ABE checks and diagnostics for call Call which invokes target
    --  Target_Id using the Ada rules. Call_Attrs are the attributes of the
-   --  call. Target_Attrs are attributes of the target. Flag In_Partial_Fin
-   --  shoud be set when the processing is initiated by a partial finalization
-   --  routine. Flag In_Task_Body should be set when the processing is started
-   --  from a task body.
-
-   procedure Process_Call_Conditional_ABE
-     (Call           : Node_Id;
-      Call_Attrs     : Call_Attributes;
-      Target_Id      : Entity_Id;
-      Target_Attrs   : Target_Attributes;
-      In_Partial_Fin : Boolean);
-   --  Perform common conditional ABE checks and diagnostics for call Call that
-   --  invokes target Target_Id ignoring the Ada or SPARK rules. Call_Attrs are
-   --  the attributes of the call. Target_Attrs are attributes of the target.
-   --  Flag In_Partial_Fin shoud be set when the processing is initiated by a
-   --  partial finalization routine.
-
-   procedure Process_Call_Guaranteed_ABE
-     (Call       : Node_Id;
-      Call_Attrs : Call_Attributes;
-      Target_Id  : Entity_Id);
-   --  Perform common guaranteed ABE checks and diagnostics for call Call which
-   --  invokes target Target_Id ignoring the Ada or SPARK rules. Call_Attrs are
-   --  the attributes of the call.
+   --  call. Target_Attrs are attributes of the target. The flags should be
+   --  set when the processing was initiated as follows:
+   --
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Call_SPARK
+   procedure Process_Conditional_ABE_Call_SPARK
      (Call           : Node_Id;
-      Call_Attrs     : Call_Attributes;
       Target_Id      : Entity_Id;
       Target_Attrs   : Target_Attributes;
-      In_Partial_Fin : Boolean);
+      In_Init_Cond   : Boolean;
+      In_Partial_Fin : Boolean;
+      In_Task_Body   : Boolean);
    --  Perform ABE checks and diagnostics for call Call which invokes target
-   --  Target_Id using the SPARK rules. Call_Attrs are the attributes of the
-   --  call. Target_Attrs are attributes of the target. Flag In_Partial_Fin
-   --  shoud be set when the processing is initiated by a partial finalization
-   --  routine.
-
-   procedure Process_Guaranteed_ABE (N : Node_Id);
-   --  Top-level dispatcher for processing of scenarios which result in a
-   --  guaranteed ABE.
+   --  Target_Id using the SPARK rules. Target_Attrs denotes the attributes of
+   --  the target. The flags should be set when the processing was initiated as
+   --  follows:
+   --
+   --    In_Init_Cond   - initial condition procedure
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Instantiation
+   procedure Process_Conditional_ABE_Instantiation
      (Exp_Inst       : Node_Id;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean);
    --  Top-level dispatcher for processing of instantiations. Perform ABE
-   --  checks and diagnostics for expanded instantiation Exp_Inst. Flag
-   --  In_Partial_Fin shoud be set when the processing is initiated by a
-   --  partial finalization routine. Flag In_Task_Body should be set when
-   --  the processing is initiated from a task body.
+   --  checks and diagnostics for expanded instantiation Exp_Inst. The flags
+   --  should be set when the processing was initiated as follows:
+   --
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Instantiation_Ada
+   procedure Process_Conditional_ABE_Instantiation_Ada
      (Exp_Inst       : Node_Id;
       Inst           : Node_Id;
       Inst_Attrs     : Instantiation_Attributes;
@@ -1372,108 +1597,150 @@ package body Sem_Elab is
    --  Perform ABE checks and diagnostics for expanded instantiation Exp_Inst
    --  of generic Gen_Id using the Ada rules. Inst is the instantiation node.
    --  Inst_Attrs are the attributes of the instance. Gen_Attrs denotes the
-   --  attributes of the generic. Flag In_Partial_Fin shoud be set when the
-   --  processing is initiated by a partial finalization routine. In_Task_Body
-   --  should be set when the processing is initiated from a task body.
-
-   procedure Process_Instantiation_Conditional_ABE
-     (Exp_Inst       : Node_Id;
-      Inst           : Node_Id;
-      Inst_Attrs     : Instantiation_Attributes;
-      Gen_Id         : Entity_Id;
-      Gen_Attrs      : Target_Attributes;
-      In_Partial_Fin : Boolean);
-   --  Perform common conditional ABE checks and diagnostics for expanded
-   --  instantiation Exp_Inst of generic Gen_Id ignoring the Ada or SPARK
-   --  rules. Inst is the instantiation node. Inst_Attrs are the attributes
-   --  of the instance. Gen_Attrs are the attributes of the generic. Flag
-   --  In_Partial_Fin shoud be set when the processing is initiated by a
-   --  partial finalization routine.
-
-   procedure Process_Instantiation_Guaranteed_ABE (Exp_Inst : Node_Id);
-   --  Perform common guaranteed ABE checks and diagnostics for expanded
-   --  instantiation Exp_Inst of generic Gen_Id ignoring the Ada or SPARK
-   --  rules.
+   --  attributes of the generic. The flags should be set when the processing
+   --  was initiated as follows:
+   --
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Instantiation_SPARK
-     (Exp_Inst       : Node_Id;
-      Inst           : Node_Id;
-      Inst_Attrs     : Instantiation_Attributes;
+   procedure Process_Conditional_ABE_Instantiation_SPARK
+     (Inst           : Node_Id;
       Gen_Id         : Entity_Id;
       Gen_Attrs      : Target_Attributes;
-      In_Partial_Fin : Boolean);
-   --  Perform ABE checks and diagnostics for expanded instantiation Exp_Inst
-   --  of generic Gen_Id using the SPARK rules. Inst is the instantiation node.
-   --  Inst_Attrs are the attributes of the instance. Gen_Attrs denotes the
-   --  attributes of the generic. Flag In_Partial_Fin shoud be set when the
-   --  processing is initiated by a partial finalization routine.
-
-   procedure Process_Scenario
-     (N              : Node_Id;
-      In_Partial_Fin : Boolean := False;
-      In_Task_Body   : Boolean := False);
-   --  Top-level dispatcher for processing of various elaboration scenarios.
-   --  Perform ABE checks and diagnostics for scenario N. Flag In_Partial_Fin
-   --  shoud be set when the processing is initiated by a partial finalization
-   --  routine. Flag In_Task_Body should be set when the processing is started
-   --  from a task body.
+      In_Partial_Fin : Boolean;
+      In_Task_Body   : Boolean);
+   --  Perform ABE checks and diagnostics for instantiation Inst of generic
+   --  Gen_Id using the SPARK rules. Gen_Attrs denotes the attributes of the
+   --  generic. The flags should be set when the processing was initiated as
+   --  follows:
+   --
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
-   procedure Process_Variable_Assignment (Asmt : Node_Id);
+   procedure Process_Conditional_ABE_Variable_Assignment (Asmt : Node_Id);
    --  Top-level dispatcher for processing of variable assignments. Perform ABE
    --  checks and diagnostics for assignment statement Asmt.
 
-   procedure Process_Variable_Assignment_Ada
+   procedure Process_Conditional_ABE_Variable_Assignment_Ada
      (Asmt   : Node_Id;
       Var_Id : Entity_Id);
    --  Perform ABE checks and diagnostics for assignment statement Asmt that
    --  updates the value of variable Var_Id using the Ada rules.
 
-   procedure Process_Variable_Assignment_SPARK
+   procedure Process_Conditional_ABE_Variable_Assignment_SPARK
      (Asmt   : Node_Id;
       Var_Id : Entity_Id);
    --  Perform ABE checks and diagnostics for assignment statement Asmt that
    --  updates the value of variable Var_Id using the SPARK rules.
 
-   procedure Process_Variable_Reference (Ref : Node_Id);
+   procedure Process_Conditional_ABE_Variable_Reference (Ref : Node_Id);
    --  Top-level dispatcher for processing of variable references. Perform ABE
    --  checks and diagnostics for variable reference Ref.
 
-   procedure Process_Variable_Reference_Read
+   procedure Process_Conditional_ABE_Variable_Reference_Read
      (Ref    : Node_Id;
       Var_Id : Entity_Id;
       Attrs  : Variable_Attributes);
    --  Perform ABE checks and diagnostics for reference Ref described by its
    --  attributes Attrs, that reads variable Var_Id.
 
+   procedure Process_Guaranteed_ABE (N : Node_Id);
+   --  Top-level dispatcher for processing of scenarios which result in a
+   --  guaranteed ABE.
+
+   procedure Process_Guaranteed_ABE_Activation_Impl
+     (Call           : Node_Id;
+      Call_Attrs     : Call_Attributes;
+      Obj_Id         : Entity_Id;
+      Task_Attrs     : Task_Attributes;
+      In_Init_Cond   : Boolean;
+      In_Partial_Fin : Boolean;
+      In_Task_Body   : Boolean);
+   --  Perform common guaranteed ABE checks and diagnostics for call Call which
+   --  activates task Obj_Id ignoring the Ada or SPARK rules. Task_Attrs are
+   --  the attributes of the task type. The following parameters are provided
+   --  for compatibility and are unused.
+   --
+   --    Call_Attrs
+   --    In_Init_Cond
+   --    In_Partial_Fin
+   --    In_Task_Body
+
+   procedure Process_Guaranteed_ABE_Call
+     (Call       : Node_Id;
+      Call_Attrs : Call_Attributes;
+      Target_Id  : Entity_Id);
+   --  Perform common guaranteed ABE checks and diagnostics for call Call which
+   --  invokes target Target_Id ignoring the Ada or SPARK rules. Call_Attrs are
+   --  the attributes of the call.
+
+   procedure Process_Guaranteed_ABE_Instantiation (Exp_Inst : Node_Id);
+   --  Perform common guaranteed ABE checks and diagnostics for expanded
+   --  instantiation Exp_Inst of generic Gen_Id ignoring the Ada or SPARK
+   --  rules.
+
    procedure Push_Active_Scenario (N : Node_Id);
    pragma Inline (Push_Active_Scenario);
    --  Push scenario N on top of the scenario stack
 
+   procedure Record_SPARK_Elaboration_Scenario (N : Node_Id);
+   pragma Inline (Record_SPARK_Elaboration_Scenario);
+   --  Save SPARK scenario N in table SPARK_Scenarios for later processing
+
+   procedure Reset_Visited_Bodies;
+   pragma Inline (Reset_Visited_Bodies);
+   --  Clear the contents of table Visited_Bodies
+
    function Root_Scenario return Node_Id;
    pragma Inline (Root_Scenario);
    --  Return the top-level scenario which started a recursive search for other
    --  scenarios. It is assumed that there is a valid top-level scenario on the
    --  active scenario stack.
 
+   procedure Set_Early_Call_Region (Body_Id : Entity_Id; Start : Node_Id);
+   pragma Inline (Set_Early_Call_Region);
+   --  Associate an early call region with begins at construct Start with entry
+   --  or subprogram body Body_Id.
+
+   procedure Set_Elaboration_Status
+     (Unit_Id : Entity_Id;
+      Val     : Elaboration_Attributes);
+   pragma Inline (Set_Elaboration_Status);
+   --  Associate an set of elaboration attributes with unit Unit_Id
+
+   procedure Set_Is_Recorded_SPARK_Scenario
+     (N   : Node_Id;
+      Val : Boolean := True);
+   pragma Inline (Set_Is_Recorded_SPARK_Scenario);
+   --  Mark scenario N as being recorded in table SPARK_Scenarios
+
    procedure Set_Is_Recorded_Top_Level_Scenario
      (N   : Node_Id;
       Val : Boolean := True);
    pragma Inline (Set_Is_Recorded_Top_Level_Scenario);
    --  Mark scenario N as being recorded in table Top_Level_Scenarios
 
+   procedure Set_Is_Visited_Body (Subp_Body : Node_Id);
+   pragma Inline (Set_Is_Visited_Body);
+   --  Mark subprogram body Subp_Body as being visited during a recursive
+   --  traversal started from a top-level scenario.
+
    function Static_Elaboration_Checks return Boolean;
    pragma Inline (Static_Elaboration_Checks);
    --  Determine whether the static model is in effect
 
    procedure Traverse_Body
      (N              : Node_Id;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean);
    --  Inspect the declarations and statements of subprogram body N for
-   --  suitable elaboration scenarios and process them. Flag In_Partial_Fin
-   --  shoud be set when the processing is initiated by a partial finalization
-   --  routine. Flag In_Task_Body should be set when the traversal is initiated
-   --  from a task body.
+   --  suitable elaboration scenarios and process them. The flags should
+   --  be set when the processing was initiated as follows:
+   --
+   --    In_Init_Cond   - initial condition procedure
+   --    In_Partial_Fin - partial finalization procedure
+   --    In_Task_Body   - task body
 
    procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id);
    pragma Inline (Update_Elaboration_Scenario);
@@ -1995,17 +2262,23 @@ package body Sem_Elab is
 
       Find_Elaborated_Units;
 
-      --  Examine each top-level scenario saved during the Recording phase and
-      --  perform various actions depending on the elaboration model in effect.
+      --  Examine each top-level scenario saved during the Recording phase for
+      --  conditional ABEs and perform various actions depending on the model
+      --  in effect. The table of visited bodies is created for each new top-
+      --  level scenario.
 
       for Index in Top_Level_Scenarios.First .. Top_Level_Scenarios.Last loop
+         Reset_Visited_Bodies;
 
-         --  Clear the table of visited scenario bodies for each new top-level
-         --  scenario.
+         Process_Conditional_ABE (Top_Level_Scenarios.Table (Index));
+      end loop;
 
-         Visited_Bodies.Reset;
+      --  Examine each SPARK scenario saved during the Recording phase which
+      --  isnot necessarily executable during elaboration, but still requires
+      --  elaboration-related checks.
 
-         Process_Scenario (Top_Level_Scenarios.Table (Index));
+      for Index in SPARK_Scenarios.First .. SPARK_Scenarios.Last loop
+         Check_SPARK_Scenario (SPARK_Scenarios.Table (Index));
       end loop;
    end Check_Elaboration_Scenarios;
 
@@ -2102,6 +2375,576 @@ package body Sem_Elab is
       end if;
    end Check_Preelaborated_Call;
 
+   ------------------------------
+   -- Check_SPARK_Derived_Type --
+   ------------------------------
+
+   procedure Check_SPARK_Derived_Type (Typ_Decl : Node_Id) is
+      Typ : constant Entity_Id := Defining_Entity (Typ_Decl);
+
+      --  NOTE: The routines within Check_SPARK_Derived_Type are intentionally
+      --  unnested to avoid deep indentation of code.
+
+      Stop_Check : exception;
+      --  This exception is raised when the freeze node violates the placement
+      --  rules.
+
+      procedure Check_Overriding_Primitive
+        (Prim  : Entity_Id;
+         FNode : Node_Id);
+      pragma Inline (Check_Overriding_Primitive);
+      --  Verify that freeze node FNode is within the early call region of
+      --  overriding primitive Prim's body.
+
+      function Freeze_Node_Location (FNode : Node_Id) return Source_Ptr;
+      pragma Inline (Freeze_Node_Location);
+      --  Return a more accurate source location associated with freeze node
+      --  FNode.
+
+      function Precedes_Source_Construct (N : Node_Id) return Boolean;
+      pragma Inline (Precedes_Source_Construct);
+      --  Determine whether arbitrary node N appears prior to some source
+      --  construct.
+
+      procedure Suggest_Elaborate_Body
+        (N         : Node_Id;
+         Body_Decl : Node_Id;
+         Error_Nod : Node_Id);
+      pragma Inline (Suggest_Elaborate_Body);
+      --  Suggest the use of pragma Elaborate_Body when the pragma will allow
+      --  for node N to appear within the early call region of subprogram body
+      --  Body_Decl. The suggestion is attached to Error_Nod as a continuation
+      --  error.
+
+      --------------------------------
+      -- Check_Overriding_Primitive --
+      --------------------------------
+
+      procedure Check_Overriding_Primitive
+        (Prim  : Entity_Id;
+         FNode : Node_Id)
+      is
+         Prim_Decl : constant Node_Id := Unit_Declaration_Node (Prim);
+         Body_Decl : Node_Id;
+         Body_Id   : Entity_Id;
+         Region    : Node_Id;
+
+      begin
+         Body_Id := Corresponding_Body (Prim_Decl);
+
+         --  Nothing to do when the primitive does not have a corresponding
+         --  body. This can happen when the unit with the bodies is not the
+         --  main unit subjected to ABE checks.
+
+         if No (Body_Id) then
+            return;
+
+         --  The primitive overrides a parent or progenitor primitive
+
+         elsif Present (Overridden_Operation (Prim)) then
+
+            --  Nothing to do when overriding an interface primitive happens by
+            --  inheriting a non-interface primitive as the check would be done
+            --  on the parent primitive.
+
+            if Present (Alias (Prim)) then
+               return;
+            end if;
+
+         --  Nothing to do when the primitive is not overriding. The body of
+         --  such a primitive cannot be targeted by a dispatching call which
+         --  is executable during elaboration, and cannot cause an ABE.
+
+         else
+            return;
+         end if;
+
+         Body_Decl := Unit_Declaration_Node (Body_Id);
+         Region    := Find_Early_Call_Region (Body_Decl);
+
+         --  The freeze node appears prior to the early call region of the
+         --  primitive body.
+
+         --  IMPORTANT: This check must always be performed even when -gnatd.v
+         --  (enforce SPARK elaboration rules in SPARK code) is not specified
+         --  because the static model cannot guarantee the absence of ABEs in
+         --  in the presence of dispatching calls.
+
+         if Earlier_In_Extended_Unit (FNode, Region) then
+            Error_Msg_Node_2 := Prim;
+            Error_Msg_NE
+              ("first freezing point of type & must appear within early call "
+               & "region of primitive body & (SPARK RM 7.7(8))",
+               Typ_Decl, Typ);
+
+            Error_Msg_Sloc := Sloc (Region);
+            Error_Msg_N ("\region starts #", Typ_Decl);
+
+            Error_Msg_Sloc := Sloc (Body_Decl);
+            Error_Msg_N ("\region ends #", Typ_Decl);
+
+            Error_Msg_Sloc := Freeze_Node_Location (FNode);
+            Error_Msg_N ("\first freezing point #", Typ_Decl);
+
+            --  If applicable, suggest the use of pragma Elaborate_Body in the
+            --  associated package spec.
+
+            Suggest_Elaborate_Body
+              (N         => FNode,
+               Body_Decl => Body_Decl,
+               Error_Nod => Typ_Decl);
+
+            raise Stop_Check;
+         end if;
+      end Check_Overriding_Primitive;
+
+      --------------------------
+      -- Freeze_Node_Location --
+      --------------------------
+
+      function Freeze_Node_Location (FNode : Node_Id) return Source_Ptr is
+         Context : constant Node_Id    := Parent (FNode);
+         Loc     : constant Source_Ptr := Sloc (FNode);
+
+         Prv_Decls : List_Id;
+         Vis_Decls : List_Id;
+
+      begin
+         --  In general, the source location of the freeze node is as close as
+         --  possible to the real freeze point, except when the freeze node is
+         --  at the "bottom" of a package spec.
+
+         if Nkind (Context) = N_Package_Specification then
+            Prv_Decls := Private_Declarations (Context);
+            Vis_Decls := Visible_Declarations (Context);
+
+            --  The freeze node appears in the private declarations of the
+            --  package.
+
+            if Present (Prv_Decls)
+              and then List_Containing (FNode) = Prv_Decls
+            then
+               null;
+
+            --  The freeze node appears in the visible declarations of the
+            --  package and there are no private declarations.
+
+            elsif Present (Vis_Decls)
+              and then List_Containing (FNode) = Vis_Decls
+              and then (No (Prv_Decls) or else Is_Empty_List (Prv_Decls))
+            then
+               null;
+
+            --  Otherwise the freeze node is not in the "last" declarative list
+            --  of the package. Use the existing source location of the freeze
+            --  node.
+
+            else
+               return Loc;
+            end if;
+
+            --  The freeze node appears at the "bottom" of the package when it
+            --  is in the "last" declarative list and is either the last in the
+            --  list or is followed by internal constructs only. In that case
+            --  the more appropriate source location is that of the package end
+            --  label.
+
+            if not Precedes_Source_Construct (FNode) then
+               return Sloc (End_Label (Context));
+            end if;
+         end if;
+
+         return Loc;
+      end Freeze_Node_Location;
+
+      -------------------------------
+      -- Precedes_Source_Construct --
+      -------------------------------
+
+      function Precedes_Source_Construct (N : Node_Id) return Boolean is
+         Decl : Node_Id;
+
+      begin
+         Decl := Next (N);
+         while Present (Decl) loop
+            if Comes_From_Source (Decl) then
+               return True;
+
+            --  A generated body for a source expression function is treated as
+            --  a source construct.
+
+            elsif Nkind (Decl) = N_Subprogram_Body
+              and then Was_Expression_Function (Decl)
+              and then Comes_From_Source (Original_Node (Decl))
+            then
+               return True;
+            end if;
+
+            Next (Decl);
+         end loop;
+
+         return False;
+      end Precedes_Source_Construct;
+
+      ----------------------------
+      -- Suggest_Elaborate_Body --
+      ----------------------------
+
+      procedure Suggest_Elaborate_Body
+        (N         : Node_Id;
+         Body_Decl : Node_Id;
+         Error_Nod : Node_Id)
+      is
+         Unt    : constant Node_Id := Unit (Cunit (Main_Unit));
+         Region : Node_Id;
+
+      begin
+         --  The suggestion applies only when the subprogram body resides in a
+         --  compilation package body, and a pragma Elaborate_Body would allow
+         --  for the node to appear in the early call region of the subprogram
+         --  body. This implies that all code from the subprogram body upto the
+         --  node is preelaborable.
+
+         if Nkind (Unt) = N_Package_Body then
+
+            --  Find the start of the early call region again assuming that the
+            --  package spec has pragma Elaborate_Body. Note that the internal
+            --  data structures are intentionally not updated because this is a
+            --  speculative search.
+
+            Region :=
+              Find_Early_Call_Region
+                (Body_Decl        => Body_Decl,
+                 Assume_Elab_Body => True,
+                 Skip_Memoization => True);
+
+            --  If the node appears within the early call region assuming that
+            --  the package spec carries pragma Elaborate_Body, then it is safe
+            --  to suggest the pragma.
+
+            if Earlier_In_Extended_Unit (Region, N) then
+               Error_Msg_Name_1 := Name_Elaborate_Body;
+               Error_Msg_NE
+                 ("\consider adding pragma % in spec of unit &",
+                  Error_Nod, Defining_Entity (Unt));
+            end if;
+         end if;
+      end Suggest_Elaborate_Body;
+
+      --  Local variables
+
+      FNode : constant Node_Id  := Freeze_Node (Typ);
+      Prims : constant Elist_Id := Direct_Primitive_Operations (Typ);
+
+      Prim_Elmt : Elmt_Id;
+
+   --  Start of processing for Check_SPARK_Derived_Type
+
+   begin
+      --  A type should have its freeze node set by the time SPARK scenarios
+      --  are being verified.
+
+      pragma Assert (Present (FNode));
+
+      --  Verify that the freeze node of the derived type is within the early
+      --  call region of each overriding primitive body (SPARK RM 7.7(8)).
+
+      if Present (Prims) then
+         Prim_Elmt := First_Elmt (Prims);
+         while Present (Prim_Elmt) loop
+            Check_Overriding_Primitive
+              (Prim  => Node (Prim_Elmt),
+               FNode => FNode);
+
+            Next_Elmt (Prim_Elmt);
+         end loop;
+      end if;
+
+   exception
+      when Stop_Check =>
+         null;
+   end Check_SPARK_Derived_Type;
+
+   -------------------------------
+   -- Check_SPARK_Instantiation --
+   -------------------------------
+
+   procedure Check_SPARK_Instantiation (Exp_Inst : Node_Id) is
+      Gen_Attrs  : Target_Attributes;
+      Gen_Id     : Entity_Id;
+      Inst       : Node_Id;
+      Inst_Attrs : Instantiation_Attributes;
+      Inst_Id    : Entity_Id;
+
+   begin
+      Extract_Instantiation_Attributes
+        (Exp_Inst => Exp_Inst,
+         Inst     => Inst,
+         Inst_Id  => Inst_Id,
+         Gen_Id   => Gen_Id,
+         Attrs    => Inst_Attrs);
+
+      Extract_Target_Attributes (Gen_Id, Gen_Attrs);
+
+      --  The instantiation and the generic body are both in the main unit
+
+      if Present (Gen_Attrs.Body_Decl)
+        and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl)
+
+        --  If the instantiation appears prior to the generic body, then the
+        --  instantiation is illegal (SPARK RM 7.7(6)).
+
+        --  IMPORTANT: This check must always be performed even when -gnatd.v
+        --  (enforce SPARK elaboration rules in SPARK code) is not specified
+        --  because the rule prevents use-before-declaration of objects that
+        --  may precede the generic body.
+
+        and then Earlier_In_Extended_Unit (Inst, Gen_Attrs.Body_Decl)
+      then
+         Error_Msg_NE ("cannot instantiate & before body seen", Inst, Gen_Id);
+      end if;
+   end Check_SPARK_Instantiation;
+
+   --------------------------
+   -- Check_SPARK_Scenario --
+   --------------------------
+
+   procedure Check_SPARK_Scenario (N : Node_Id) is
+   begin
+      --  Add the current scenario to the stack of active scenarios
+
+      Push_Active_Scenario (N);
+
+      if Is_Suitable_SPARK_Derived_Type (N) then
+         Check_SPARK_Derived_Type (N);
+
+      elsif Is_Suitable_SPARK_Instantiation (N) then
+         Check_SPARK_Instantiation (N);
+
+      elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+         Check_SPARK_Refined_State_Pragma (N);
+      end if;
+
+      --  Remove the current scenario from the stack of active scenarios once
+      --  all ABE diagnostics and checks have been performed.
+
+      Pop_Active_Scenario (N);
+   end Check_SPARK_Scenario;
+
+   --------------------------------------
+   -- Check_SPARK_Refined_State_Pragma --
+   --------------------------------------
+
+   procedure Check_SPARK_Refined_State_Pragma (N : Node_Id) is
+
+      --  NOTE: The routines within Check_SPARK_Refined_State_Pragma are
+      --  intentionally unnested to avoid deep indentation of code.
+
+      procedure Check_SPARK_Constituent (Constit_Id : Entity_Id);
+      pragma Inline (Check_SPARK_Constituent);
+      --  Ensure that a single constituent Constit_Id is elaborated prior to
+      --  the main unit.
+
+      procedure Check_SPARK_Constituents (Constits : Elist_Id);
+      pragma Inline (Check_SPARK_Constituents);
+      --  Ensure that all constituents found in list Constits are elaborated
+      --  prior to the main unit.
+
+      procedure Check_SPARK_Initialized_State (State : Node_Id);
+      pragma Inline (Check_SPARK_Initialized_State);
+      --  Ensure that the constituents of single abstract state State are
+      --  elaborated prior to the main unit.
+
+      procedure Check_SPARK_Initialized_States (Pack_Id : Entity_Id);
+      pragma Inline (Check_SPARK_Initialized_States);
+      --  Ensure that the constituents of all abstract states which appear in
+      --  the Initializes pragma of package Pack_Id are elaborated prior to the
+      --  main unit.
+
+      -----------------------------
+      -- Check_SPARK_Constituent --
+      -----------------------------
+
+      procedure Check_SPARK_Constituent (Constit_Id : Entity_Id) is
+         Prag : Node_Id;
+
+      begin
+         --  Nothing to do for "null" constituents
+
+         if Nkind (Constit_Id) = N_Null then
+            return;
+
+         --  Nothing to do for illegal constituents
+
+         elsif Error_Posted (Constit_Id) then
+            return;
+         end if;
+
+         Prag := SPARK_Pragma (Constit_Id);
+
+         --  The check applies only when the constituent is subject to pragma
+         --  SPARK_Mode On.
+
+         if Present (Prag)
+           and then Get_SPARK_Mode_From_Annotation (Prag) = On
+         then
+            --  An external constituent of an abstract state which appears in
+            --  the Initializes pragma of a package spec imposes an Elaborate
+            --  requirement on the context of the main unit. Determine whether
+            --  the context has a pragma strong enough to meet the requirement.
+
+            --  IMPORTANT: This check is performed only when -gnatd.v (enforce
+            --  SPARK elaboration rules in SPARK code) is in effect because the
+            --  static model can ensure the prior elaboration of the unit which
+            --  contains a constituent by installing implicit Elaborate pragma.
+
+            if Debug_Flag_Dot_V then
+               Meet_Elaboration_Requirement
+                 (N         => N,
+                  Target_Id => Constit_Id,
+                  Req_Nam   => Name_Elaborate);
+
+            --  Otherwise ensure that the unit with the external constituent is
+            --  elaborated prior to the main unit.
+
+            else
+               Ensure_Prior_Elaboration
+                 (N              => N,
+                  Unit_Id        => Find_Top_Unit (Constit_Id),
+                  Prag_Nam       => Name_Elaborate,
+                  In_Partial_Fin => False,
+                  In_Task_Body   => False);
+            end if;
+         end if;
+      end Check_SPARK_Constituent;
+
+      ------------------------------
+      -- Check_SPARK_Constituents --
+      ------------------------------
+
+      procedure Check_SPARK_Constituents (Constits : Elist_Id) is
+         Constit_Elmt : Elmt_Id;
+
+      begin
+         if Present (Constits) then
+            Constit_Elmt := First_Elmt (Constits);
+            while Present (Constit_Elmt) loop
+               Check_SPARK_Constituent (Node (Constit_Elmt));
+               Next_Elmt (Constit_Elmt);
+            end loop;
+         end if;
+      end Check_SPARK_Constituents;
+
+      -----------------------------------
+      -- Check_SPARK_Initialized_State --
+      -----------------------------------
+
+      procedure Check_SPARK_Initialized_State (State : Node_Id) is
+         Prag     : Node_Id;
+         State_Id : Entity_Id;
+
+      begin
+         --  Nothing to do for "null" initialization items
+
+         if Nkind (State) = N_Null then
+            return;
+
+         --  Nothing to do for illegal states
+
+         elsif Error_Posted (State) then
+            return;
+         end if;
+
+         State_Id := Entity_Of (State);
+
+         --  Sanitize the state
+
+         if No (State_Id) then
+            return;
+
+         elsif Error_Posted (State_Id) then
+            return;
+
+         elsif Ekind (State_Id) /= E_Abstract_State then
+            return;
+         end if;
+
+         --  The check is performed only when the abstract state is subject to
+         --  SPARK_Mode On.
+
+         Prag := SPARK_Pragma (State_Id);
+
+         if Present (Prag)
+           and then Get_SPARK_Mode_From_Annotation (Prag) = On
+         then
+            Check_SPARK_Constituents (Refinement_Constituents (State_Id));
+         end if;
+      end Check_SPARK_Initialized_State;
+
+      ------------------------------------
+      -- Check_SPARK_Initialized_States --
+      ------------------------------------
+
+      procedure Check_SPARK_Initialized_States (Pack_Id : Entity_Id) is
+         Prag  : constant Node_Id := Get_Pragma (Pack_Id, Pragma_Initializes);
+         Init  : Node_Id;
+         Inits : Node_Id;
+
+      begin
+         if Present (Prag) then
+            Inits := Expression (Get_Argument (Prag, Pack_Id));
+
+            --  Avoid processing a "null" initialization list. The only other
+            --  alternative is an aggregate.
+
+            if Nkind (Inits) = N_Aggregate then
+
+               --  The initialization items appear in list form:
+               --
+               --    (state1, state2)
+
+               if Present (Expressions (Inits)) then
+                  Init := First (Expressions (Inits));
+                  while Present (Init) loop
+                     Check_SPARK_Initialized_State (Init);
+                     Next (Init);
+                  end loop;
+               end if;
+
+               --  The initialization items appear in associated form:
+               --
+               --    (state1 => item1,
+               --     state2 => (item2, item3))
+
+               if Present (Component_Associations (Inits)) then
+                  Init := First (Component_Associations (Inits));
+                  while Present (Init) loop
+                     Check_SPARK_Initialized_State (Init);
+                     Next (Init);
+                  end loop;
+               end if;
+            end if;
+         end if;
+      end Check_SPARK_Initialized_States;
+
+      --  Local variables
+
+      Pack_Body : constant Node_Id := Find_Related_Package_Or_Body (N);
+
+   --  Start of processing for Check_SPARK_Refined_State_Pragma
+
+   begin
+      --  Pragma Refined_State must be associated with a package body
+
+      pragma Assert
+        (Present (Pack_Body) and then Nkind (Pack_Body) = N_Package_Body);
+
+      --  Verify that each external contitunent of an abstract state mentioned
+      --  in pragma Initializes is properly elaborated.
+
+      Check_SPARK_Initialized_States (Unique_Defining_Entity (Pack_Body));
+   end Check_SPARK_Refined_State_Pragma;
+
    ----------------------
    -- Compilation_Unit --
    ----------------------
@@ -2150,6 +2993,36 @@ package body Sem_Elab is
       return Comp_Unit;
    end Compilation_Unit;
 
+   -----------------------
+   -- Early_Call_Region --
+   -----------------------
+
+   function Early_Call_Region (Body_Id : Entity_Id) return Node_Id is
+   begin
+      pragma Assert (Ekind_In (Body_Id, E_Entry,
+                                        E_Entry_Family,
+                                        E_Function,
+                                        E_Procedure,
+                                        E_Subprogram_Body));
+
+      if Early_Call_Regions_In_Use then
+         return Early_Call_Regions.Get (Body_Id);
+      end if;
+
+      return Early_Call_Regions_No_Element;
+   end Early_Call_Region;
+
+   -----------------------------
+   -- Early_Call_Regions_Hash --
+   -----------------------------
+
+   function Early_Call_Regions_Hash
+     (Key : Entity_Id) return Early_Call_Regions_Index
+   is
+   begin
+      return Early_Call_Regions_Index (Key mod Early_Call_Regions_Max);
+   end Early_Call_Regions_Hash;
+
    -----------------
    -- Elab_Msg_NE --
    -----------------
@@ -2199,16 +3072,31 @@ package body Sem_Elab is
       Error_Msg_NE (Prefix & Msg & Suffix, N, Id);
    end Elab_Msg_NE;
 
-   ------------------------------
-   -- Elaboration_Context_Hash --
-   ------------------------------
+   ------------------------
+   -- Elaboration_Status --
+   ------------------------
 
-   function Elaboration_Context_Hash
-     (Key : Entity_Id) return Elaboration_Context_Index
+   function Elaboration_Status
+     (Unit_Id : Entity_Id) return Elaboration_Attributes
    is
    begin
-      return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
-   end Elaboration_Context_Hash;
+      if Elaboration_Statuses_In_Use then
+         return Elaboration_Statuses.Get (Unit_Id);
+      end if;
+
+      return Elaboration_Statuses_No_Element;
+   end Elaboration_Status;
+
+   -------------------------------
+   -- Elaboration_Statuses_Hash --
+   -------------------------------
+
+   function Elaboration_Statuses_Hash
+     (Key : Entity_Id) return Elaboration_Statuses_Index
+   is
+   begin
+      return Elaboration_Statuses_Index (Key mod Elaboration_Statuses_Max);
+   end Elaboration_Statuses_Hash;
 
    ------------------------------
    -- Ensure_Prior_Elaboration --
@@ -2217,43 +3105,12 @@ package body Sem_Elab is
    procedure Ensure_Prior_Elaboration
      (N              : Node_Id;
       Unit_Id        : Entity_Id;
+      Prag_Nam       : Name_Id;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean)
    is
-      Prag_Nam : Name_Id;
-
    begin
-      --  Instantiating an external generic unit requires an implicit Elaborate
-      --  because Elaborate_All is too strong and could introduce non-existent
-      --  elaboration cycles.
-
-      --    package External is
-      --       function Func ...;
-      --    end External;
-
-      --    with External;
-      --    generic
-      --    package Gen is
-      --       X : ... := External.Func;
-      --    end Gen;
-
-      --   [with External;]                      --  implicit with for External
-      --   [pragma Elaborate_All (External);]    --  Elaborate_All for External
-      --    with Gen;
-      --   [pragma Elaborate (Gen);]             --  Elaborate for generic
-      --    procedure Main is
-      --       package Inst is new Gen;          --  calls External.Func
-      --       ...
-      --    end Main;
-
-      if Nkind (N) in N_Generic_Instantiation then
-         Prag_Nam := Name_Elaborate;
-
-      --  Otherwise generate an implicit Elaborate_All
-
-      else
-         Prag_Nam := Name_Elaborate_All;
-      end if;
+      pragma Assert (Nam_In (Prag_Nam, Name_Elaborate, Name_Elaborate_All));
 
       --  Nothing to do when the need for prior elaboration came from a partial
       --  finalization routine which occurs in an initialization context. This
@@ -2397,7 +3254,7 @@ package body Sem_Elab is
    --  Start of processing for Ensure_Prior_Elaboration_Dynamic
 
    begin
-      Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+      Elab_Attrs := Elaboration_Status (Unit_Id);
 
       --  Nothing to do when the unit is guaranteed prior elaboration by means
       --  of a source Elaborate[_All] pragma.
@@ -2536,7 +3393,7 @@ package body Sem_Elab is
    --  Start of processing for Ensure_Prior_Elaboration_Static
 
    begin
-      Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+      Elab_Attrs := Elaboration_Status (Unit_Id);
 
       --  Nothing to do when the unit is guaranteed prior elaboration by means
       --  of a source Elaborate[_All] pragma.
@@ -2616,9 +3473,10 @@ package body Sem_Elab is
       --  The implicit Elaborate[_All] ensures the prior elaboration of the
       --  unit. Include the unit in the elaboration context of the main unit.
 
-      Elaboration_Context.Set (Unit_Id,
-        Elaboration_Attributes'(Source_Pragma => Empty,
-                                With_Clause   => Clause));
+      Set_Elaboration_Status
+        (Unit_Id => Unit_Id,
+         Val     => Elaboration_Attributes'(Source_Pragma => Empty,
+                                            With_Clause   => Clause));
 
       --  Output extra information on an implicit Elaborate[_All] pragma when
       --  switch -gnatel (info messages on implicit Elaborate[_All] pragmas is
@@ -3213,6 +4071,831 @@ package body Sem_Elab is
       return Find_Unit_Entity (Unit (Cunit (Get_Code_Unit (N))));
    end Find_Code_Unit;
 
+   ----------------------------
+   -- Find_Early_Call_Region --
+   ----------------------------
+
+   function Find_Early_Call_Region
+     (Body_Decl        : Node_Id;
+      Assume_Elab_Body : Boolean := False;
+      Skip_Memoization : Boolean := False) return Node_Id
+   is
+      --  NOTE: The routines within Find_Early_Call_Region are intentionally
+      --  unnested to avoid deep indentation of code.
+
+      ECR_Found : exception;
+      --  This exception is raised when the early call region has been found
+
+      Start : Node_Id := Empty;
+      --  The start of the early call region. This variable is updated by the
+      --  various nested routines. Due to the use of exceptions, the variable
+      --  must be global to the nested routines.
+
+      --  The algorithm implemented in this routine attempts to find the early
+      --  call region of a subprogram body by inspecting constructs in reverse
+      --  declarative order, while navigating the tree. The algorithm consists
+      --  of an Inspection phase and an Advancement phase. The pseudocode is as
+      --  follows:
+      --
+      --    loop
+      --       inspection phase
+      --       advancement phase
+      --    end loop
+      --
+      --  The infinite loop is terminated by raising exception ECR_Found. The
+      --  algorithm utilizes two pointers, Curr and Start, to represent the
+      --  current construct to inspect and the start of the early call region.
+      --
+      --  IMPORTANT: The algorithm must maintain the following invariant at all
+      --  time for it to function properly - a nested construct is entered only
+      --  when it contains suitable constructs. This guarantees that leaving a
+      --  nested or encapsulating construct functions properly.
+      --
+      --  The Inspection phase determines whether the current construct is non-
+      --  preelaborable, and if it is, the algorithm terminates.
+      --
+      --  The Advancement phase walks the tree in reverse declarative order,
+      --  while entering and leaving nested and encapsulating constructs. It
+      --  may also terminate the elaborithm. There are several special cases
+      --  of advancement.
+      --
+      --  1) General case:
+      --
+      --    <construct 1>
+      --     ...
+      --    <construct N-1>                      <- Curr
+      --    <construct N>                        <- Start
+      --    <subprogram body>
+      --
+      --  In the general case, a declarative or statement list is traversed in
+      --  reverse order where Curr is the lead pointer, and Start indicates the
+      --  last preelaborable construct.
+      --
+      --  2) Entering handled bodies
+      --
+      --    package body Nested is               <- Curr (2.3)
+      --       <declarations>                    <- Curr (2.2)
+      --    begin
+      --       <statements>                      <- Curr (2.1)
+      --    end Nested;
+      --    <construct>                          <- Start
+      --
+      --  In this case, the algorithm enters a handled body by starting from
+      --  the last statement (2.1), or the last declaration (2.2), or the body
+      --  is consumed (2.3) because it is empty and thus preelaborable.
+      --
+      --  3) Entering package declarations
+      --
+      --    package Nested is                    <- Curr (2.3)
+      --       <visible declarations>            <- Curr (2.2)
+      --    private
+      --       <private declarations>            <- Curr (2.1)
+      --    end Nested;
+      --    <construct>                          <- Start
+      --
+      --  In this case, the algorithm enters a package declaration by starting
+      --  from the last private declaration (2.1), the last visible declaration
+      --  (2.2), or the package is consumed (2.3) because it is empty and thus
+      --  preelaborable.
+      --
+      --  4) Transitioning from list to list of the same construct
+      --
+      --  Certain constructs have two eligible lists. The algorithm must thus
+      --  transition from the second to the first list when the second list is
+      --  exhausted.
+      --
+      --    declare                              <- Curr (4.2)
+      --       <declarations>                    <- Curr (4.1)
+      --    begin
+      --       <statements>                      <- Start
+      --    end;
+      --
+      --  In this case, the algorithm has exhausted the second list (statements
+      --  in the example), and continues with the last declaration (4.1) or the
+      --  construct is consumed (4.2) because it contains only preelaborable
+      --  code.
+      --
+      --  5) Transitioning from list to construct
+      --
+      --    tack body Task is                    <- Curr (5.1)
+      --                                         <- Curr (Empty)
+      --       <construct 1>                     <- Start
+      --
+      --  In this case, the algorithm has exhausted a list, Curr is Empty, and
+      --  the owner of the list is consumed (5.1).
+      --
+      --  6) Transitioning from unit to unit
+      --
+      --  A package body with a spec subject to pragma Elaborate_Body extends
+      --  the possible range of the early call region to the package spec.
+      --
+      --    package Pack is                      <- Curr (6.3)
+      --       pragma Elaborate_Body;            <- Curr (6.2)
+      --       <visible declarations>            <- Curr (6.2)
+      --    private
+      --       <private declarations>            <- Curr (6.1)
+      --    end Pack;
+      --
+      --    package body Pack is                 <- Curr, Start
+      --
+      --  In this case, the algorithm has reached a package body compilation
+      --  unit whose spec is subject to pragma Elaborate_Body, or the caller
+      --  of the algorithm has specified this behavior. This transition is
+      --  equivalent to 3).
+      --
+      --  7) Transitioning from unit to termination
+      --
+      --  Reaching a compilation unit always terminates the algorithm as there
+      --  are no more lists to examine. This must take 6) into account.
+      --
+      --  8) Transitioning from subunit to stub
+      --
+      --    package body Pack is separate;       <- Curr (8.1)
+      --
+      --    separate (...)
+      --    package body Pack is                 <- Curr, Start
+      --
+      --  Reaching a subunit continues the search from the corresponding stub
+      --  (8.1).
+
+      procedure Advance (Curr : in out Node_Id);
+      pragma Inline (Advance);
+      --  Update the Curr and Start pointers depending on their location in the
+      --  tree to the next eligible construct. This routine raises ECR_Found.
+
+      procedure Enter_Handled_Body (Curr : in out Node_Id);
+      pragma Inline (Enter_Handled_Body);
+      --  Update the Curr and Start pointers to enter a nested handled body if
+      --  applicable. This routine raises ECR_Found.
+
+      procedure Enter_Package_Declaration (Curr : in out Node_Id);
+      pragma Inline (Enter_Package_Declaration);
+      --  Update the Curr and Start pointers to enter a nested package spec if
+      --  applicable. This routine raises ECR_Found.
+
+      function Find_ECR (N : Node_Id) return Node_Id;
+      pragma Inline (Find_ECR);
+      --  Find an early call region starting from arbitrary node N
+
+      function Has_Suitable_Construct (List : List_Id) return Boolean;
+      pragma Inline (Has_Suitable_Construct);
+      --  Determine whether list List contains at least one suitable construct
+      --  for inclusion into an early call region.
+
+      procedure Include (N : Node_Id; Curr : in out Node_Id);
+      pragma Inline (Include);
+      --  Update the Curr and Start pointers to include arbitrary construct N
+      --  in the early call region.
+
+      function Is_OK_Preelaborable_Construct (N : Node_Id) return Boolean;
+      pragma Inline (Is_OK_Preelaborable_Construct);
+      --  Determine whether arbitrary node N denotes a preelaboration-safe
+      --  construct.
+
+      function Is_Suitable_Construct (N : Node_Id) return Boolean;
+      pragma Inline (Is_Suitable_Construct);
+      --  Determine whether arbitrary node N denotes a suitable construct for
+      --  inclusion into the early call region.
+
+      procedure Transition_Body_Declarations
+        (Bod  : Node_Id;
+         Curr : in out Node_Id);
+      pragma Inline (Transition_Body_Declarations);
+      --  Update the Curr and Start pointers when construct Bod denotes a block
+      --  statement or a suitable body. This routine raises ECR_Found.
+
+      procedure Transition_Handled_Statements
+        (HSS  : Node_Id;
+         Curr : in out Node_Id);
+      pragma Inline (Transition_Handled_Statements);
+      --  Update the Curr and Start pointers when node HSS denotes a handled
+      --  sequence of statements. This routine raises ECR_Found.
+
+      procedure Transition_Spec_Declarations
+        (Spec : Node_Id;
+         Curr : in out Node_Id);
+      pragma Inline (Transition_Spec_Declarations);
+      --  Update the Curr and Start pointers when construct Spec denotes
+      --  a concurrent definition or a package spec. This routine raises
+      --  ECR_Found.
+
+      procedure Transition_Unit (Unit : Node_Id; Curr : in out Node_Id);
+      pragma Inline (Transition_Unit);
+      --  Update the Curr and Start pointers when node Unit denotes a potential
+      --  compilation unit. This routine raises ECR_Found.
+
+      -------------
+      -- Advance --
+      -------------
+
+      procedure Advance (Curr : in out Node_Id) is
+         Context : Node_Id;
+
+      begin
+         --  Curr denotes one of the following cases upon entry into this
+         --  routine:
+         --
+         --    * Empty - There is no current construct when a declarative or a
+         --      statement list has been exhausted. This does not necessarily
+         --      indicate that the early call region has been computed as it
+         --      may still be possible to transition to another list.
+         --
+         --    * Encapsulator - The current construct encapsulates declarations
+         --      and/or statements. This indicates that the early call region
+         --      may extend within the nested construct.
+         --
+         --    * Preelaborable - The current construct is always preelaborable
+         --      because Find_ECR would not invoke Advance if this was not the
+         --      case.
+
+         --  The current construct is an encapsulator or is preelaborable
+
+         if Present (Curr) then
+
+            --  Enter encapsulators by inspecting their declarations and/or
+            --  statements.
+
+            if Nkind_In (Curr, N_Block_Statement, N_Package_Body) then
+               Enter_Handled_Body (Curr);
+
+            elsif Nkind (Curr) = N_Package_Declaration then
+               Enter_Package_Declaration (Curr);
+
+            --  Early call regions have a property which can be exploited to
+            --  optimize the algorithm.
+            --
+            --    <preceding subprogram body>
+            --    <preelaborable construct 1>
+            --     ...
+            --    <preelaborable construct N>
+            --    <initiating subprogram body>
+            --
+            --  If a traversal initiated from a subprogram body reaches a
+            --  preceding subprogram body, then both bodies share the same
+            --  early call region.
+            --
+            --  The property results in the following desirable effects:
+            --
+            --  * If the preceding body already has an early call region, then
+            --    the initiating body can reuse it. This minimizes the amount
+            --    of processing performed by the algorithm.
+            --
+            --  * If the preceding body lack an early call region, then the
+            --    algorithm can compute the early call region, and reuse it
+            --    for the initiating body. This processing performs the same
+            --    amount of work, but has the beneficial effect of computing
+            --    the early call regions of all preceding bodies.
+
+            elsif Nkind_In (Curr, N_Entry_Body, N_Subprogram_Body) then
+               Start :=
+                 Find_Early_Call_Region
+                   (Body_Decl        => Curr,
+                    Assume_Elab_Body => Assume_Elab_Body,
+                    Skip_Memoization => Skip_Memoization);
+
+               raise ECR_Found;
+
+            --  Otherwise current construct is preelaborable. Unpdate the early
+            --  call region to include it.
+
+            else
+               Include (Curr, Curr);
+            end if;
+
+         --  Otherwise the current construct is missing, indicating that the
+         --  current list has been exhausted. Depending on the context of the
+         --  list, several transitions are possible.
+
+         else
+            --  The invariant of the algorithm ensures that Curr and Start are
+            --  at the same level of nesting at the point of a transition. The
+            --  algorithm can determine which list the traversal came from by
+            --  examining Start.
+
+            Context := Parent (Start);
+
+            --  Attempt the following transitions:
+            --
+            --    private declarations -> visible declarations
+            --    private declarations -> upper level
+            --    private declarations -> terminate
+            --    visible declarations -> upper level
+            --    visible declarations -> terminate
+
+            if Nkind_In (Context, N_Package_Specification,
+                                  N_Protected_Definition,
+                                  N_Task_Definition)
+            then
+               Transition_Spec_Declarations (Context, Curr);
+
+            --  Attempt the following transitions:
+            --
+            --    statements -> declarations
+            --    statements -> upper level
+            --    statements -> corresponding package spec (Elab_Body)
+            --    statements -> terminate
+
+            elsif Nkind (Context) = N_Handled_Sequence_Of_Statements then
+               Transition_Handled_Statements (Context, Curr);
+
+            --  Attempt the following transitions:
+            --
+            --    declarations -> upper level
+            --    declarations -> corresponding package spec (Elab_Body)
+            --    declarations -> terminate
+
+            elsif Nkind_In (Context, N_Block_Statement,
+                                     N_Entry_Body,
+                                     N_Package_Body,
+                                     N_Protected_Body,
+                                     N_Subprogram_Body,
+                                     N_Task_Body)
+            then
+               Transition_Body_Declarations (Context, Curr);
+
+            --  Otherwise it is not possible to transition. Stop the search
+            --  because there are no more declarations or statements to check.
+
+            else
+               raise ECR_Found;
+            end if;
+         end if;
+      end Advance;
+
+      --------------------------
+      -- Enter_Handled_Body --
+      --------------------------
+
+      procedure Enter_Handled_Body (Curr : in out Node_Id) is
+         Decls : constant List_Id := Declarations (Curr);
+         HSS   : constant Node_Id := Handled_Statement_Sequence (Curr);
+         Stmts : List_Id := No_List;
+
+      begin
+         if Present (HSS) then
+            Stmts := Statements (HSS);
+         end if;
+
+         --  The handled body has a non-empty statement sequence. The construct
+         --  to inspect is the last statement.
+
+         if Has_Suitable_Construct (Stmts) then
+            Curr := Last (Stmts);
+
+         --  The handled body lacks statements, but has non-empty declarations.
+         --  The construct to inspect is the last declaration.
+
+         elsif Has_Suitable_Construct (Decls) then
+            Curr := Last (Decls);
+
+         --  Otherwise the handled body lacks both declarations and statements.
+         --  The construct to inspect is the node which precedes the handled
+         --  body. Update the early call region to include the handled body.
+
+         else
+            Include (Curr, Curr);
+         end if;
+      end Enter_Handled_Body;
+
+      -------------------------------
+      -- Enter_Package_Declaration --
+      -------------------------------
+
+      procedure Enter_Package_Declaration (Curr : in out Node_Id) is
+         Pack_Spec : constant Node_Id := Specification (Curr);
+         Prv_Decls : constant List_Id := Private_Declarations (Pack_Spec);
+         Vis_Decls : constant List_Id := Visible_Declarations (Pack_Spec);
+
+      begin
+         --  The package has a non-empty private declarations. The construct to
+         --  inspect is the last private declaration.
+
+         if Has_Suitable_Construct (Prv_Decls) then
+            Curr := Last (Prv_Decls);
+
+         --  The package lacks private declarations, but has non-empty visible
+         --  declarations. In this case the construct to inspect is the last
+         --  visible declaration.
+
+         elsif Has_Suitable_Construct (Vis_Decls) then
+            Curr := Last (Vis_Decls);
+
+         --  Otherwise the package lacks any declarations. The construct to
+         --  inspect is the node which precedes the package. Update the early
+         --  call region to include the package declaration.
+
+         else
+            Include (Curr, Curr);
+         end if;
+      end Enter_Package_Declaration;
+
+      --------------
+      -- Find_ECR --
+      --------------
+
+      function Find_ECR (N : Node_Id) return Node_Id is
+         Curr : Node_Id;
+
+      begin
+         --  The early call region starts at N
+
+         Curr  := Prev (N);
+         Start := N;
+
+         --  Inspect each node in reverse declarative order while going in and
+         --  out of nested and enclosing constructs. Note that the only way to
+         --  terminate this infinite loop is to raise exception ECR_Found.
+
+         loop
+            --  The current construct is not preelaboration-safe. Terminate the
+            --  traversal.
+
+            if Present (Curr)
+              and then not Is_OK_Preelaborable_Construct (Curr)
+            then
+               raise ECR_Found;
+            end if;
+
+            --  Advance to the next suitable construct. This may terminate the
+            --  traversal by raising ECR_Found.
+
+            Advance (Curr);
+         end loop;
+
+      exception
+         when ECR_Found =>
+            return Start;
+      end Find_ECR;
+
+      ----------------------------
+      -- Has_Suitable_Construct --
+      ----------------------------
+
+      function Has_Suitable_Construct (List : List_Id) return Boolean is
+         Item : Node_Id;
+
+      begin
+         --  Examine the list in reverse declarative order, looking for a
+         --  suitable construct.
+
+         if Present (List) then
+            Item := Last (List);
+            while Present (Item) loop
+               if Is_Suitable_Construct (Item) then
+                  return True;
+               end if;
+
+               Prev (Item);
+            end loop;
+         end if;
+
+         return False;
+      end Has_Suitable_Construct;
+
+      -------------
+      -- Include --
+      -------------
+
+      procedure Include (N : Node_Id; Curr : in out Node_Id) is
+      begin
+         Start := N;
+         Curr  := Prev (Start);
+      end Include;
+
+      -----------------------------------
+      -- Is_OK_Preelaborable_Construct --
+      -----------------------------------
+
+      function Is_OK_Preelaborable_Construct (N : Node_Id) return Boolean is
+      begin
+         --  Assignment statements are acceptable as long as they were produced
+         --  by the ABE mechanism to update elaboration flags.
+
+         if Nkind (N) = N_Assignment_Statement then
+            return Is_Elaboration_Code (N);
+
+         --  Block statements are acceptable even though they directly violate
+         --  preelaborability. The intention is not to penalize the early call
+         --  region when a block contains only preelaborable constructs.
+         --
+         --    declare
+         --       Val : constant Integer := 1;
+         --    begin
+         --       pragma Assert (Val = 1);
+         --       null;
+         --    end;
+         --
+         --  Note that the Advancement phase does enter blocks, and will detect
+         --  any non-preelaborable declarations or statements within.
+
+         elsif Nkind (N) = N_Block_Statement then
+            return True;
+         end if;
+
+         --  Otherwise the construct must be preelaborable. The check must take
+         --  the syntactic and semantic structure of the construct. DO NOT use
+         --  Is_Preelaborable_Construct here.
+
+         return not Is_Non_Preelaborable_Construct (N);
+      end Is_OK_Preelaborable_Construct;
+
+      ---------------------------
+      -- Is_Suitable_Construct --
+      ---------------------------
+
+      function Is_Suitable_Construct (N : Node_Id) return Boolean is
+         Context : constant Node_Id := Parent (N);
+
+      begin
+         --  An internally-generated statement sequence which contains only a
+         --  single null statement is not a suitable construct because it is a
+         --  byproduct of the parser. Such a null statement should be excluded
+         --  from the early call region because it carries the source location
+         --  of the "end" keyword, and may lead to confusing diagnistics.
+
+         if Nkind (N) = N_Null_Statement
+           and then not Comes_From_Source (N)
+           and then Present (Context)
+           and then Nkind (Context) = N_Handled_Sequence_Of_Statements
+           and then not Comes_From_Source (N)
+         then
+            return False;
+         end if;
+
+         --  Otherwise only constructs which correspond to pure Ada constructs
+         --  are considered suitable.
+
+         case Nkind (N) is
+            when N_Call_Marker
+               | N_Freeze_Entity
+               | N_Freeze_Generic_Entity
+               | N_Implicit_Label_Declaration
+               | N_Itype_Reference
+               | N_Pop_Constraint_Error_Label
+               | N_Pop_Program_Error_Label
+               | N_Pop_Storage_Error_Label
+               | N_Push_Constraint_Error_Label
+               | N_Push_Program_Error_Label
+               | N_Push_Storage_Error_Label
+               | N_SCIL_Dispatch_Table_Tag_Init
+               | N_SCIL_Dispatching_Call
+               | N_SCIL_Membership_Test
+               | N_Variable_Reference_Marker
+            =>
+               return False;
+
+            when others =>
+               return True;
+         end case;
+      end Is_Suitable_Construct;
+
+      ----------------------------------
+      -- Transition_Body_Declarations --
+      ----------------------------------
+
+      procedure Transition_Body_Declarations
+        (Bod  : Node_Id;
+         Curr : in out Node_Id)
+      is
+         Decls : constant List_Id := Declarations (Bod);
+
+      begin
+         --  The search must come from the declarations of the body
+
+         pragma Assert
+           (Is_Non_Empty_List (Decls)
+             and then List_Containing (Start) = Decls);
+
+         --  The search finished inspecting the declarations. The construct
+         --  to inspect is the node which precedes the handled body, unless
+         --  the body is a compilation unit. The transitions are:
+         --
+         --    declarations -> upper level
+         --    declarations -> corresponding package spec (Elab_Body)
+         --    declarations -> terminate
+
+         Transition_Unit (Bod, Curr);
+      end Transition_Body_Declarations;
+
+      -----------------------------------
+      -- Transition_Handled_Statements --
+      -----------------------------------
+
+      procedure Transition_Handled_Statements
+        (HSS  : Node_Id;
+         Curr : in out Node_Id)
+      is
+         Bod   : constant Node_Id := Parent (HSS);
+         Decls : constant List_Id := Declarations (Bod);
+         Stmts : constant List_Id := Statements (HSS);
+
+      begin
+         --  The search must come from the statements of certain bodies or
+         --  statements.
+
+         pragma Assert (Nkind_In (Bod, N_Block_Statement,
+                                       N_Entry_Body,
+                                       N_Package_Body,
+                                       N_Protected_Body,
+                                       N_Subprogram_Body,
+                                       N_Task_Body));
+
+         --  The search must come from the statements of the handled sequence
+
+         pragma Assert
+           (Is_Non_Empty_List (Stmts)
+             and then List_Containing (Start) = Stmts);
+
+         --  The search finished inspecting the statements. The handled body
+         --  has non-empty declarations. The construct to inspect is the last
+         --  declaration. The transitions are:
+         --
+         --    statements -> declarations
+
+         if Has_Suitable_Construct (Decls) then
+            Curr := Last (Decls);
+
+         --  Otherwise the handled body lacks declarations. The construct to
+         --  inspect is the node which precedes the handled body, unless the
+         --  body is a compilation unit. The transitions are:
+         --
+         --    statements -> upper level
+         --    statements -> corresponding package spec (Elab_Body)
+         --    statements -> terminate
+
+         else
+            Transition_Unit (Bod, Curr);
+         end if;
+      end Transition_Handled_Statements;
+
+      ----------------------------------
+      -- Transition_Spec_Declarations --
+      ----------------------------------
+
+      procedure Transition_Spec_Declarations
+        (Spec : Node_Id;
+         Curr : in out Node_Id)
+      is
+         Prv_Decls : constant List_Id := Private_Declarations (Spec);
+         Vis_Decls : constant List_Id := Visible_Declarations (Spec);
+
+      begin
+         pragma Assert (Present (Start) and then Is_List_Member (Start));
+
+         --  The search came from the private declarations and finished their
+         --  inspection.
+
+         if Has_Suitable_Construct (Prv_Decls)
+           and then List_Containing (Start) = Prv_Decls
+         then
+            --  The context has non-empty visible declarations. The node to
+            --  inspect is the last visible declaration. The transitions are:
+            --
+            --    private declarations -> visible declarations
+
+            if Has_Suitable_Construct (Vis_Decls) then
+               Curr := Last (Vis_Decls);
+
+            --  Otherwise the context lacks visible declarations. The construct
+            --  to inspect is the node which precedes the context unless the
+            --  context is a compilation unit. The transitions are:
+            --
+            --    private declarations -> upper level
+            --    private declarations -> terminate
+
+            else
+               Transition_Unit (Parent (Spec), Curr);
+            end if;
+
+         --  The search came from the visible declarations and finished their
+         --  inspections. The construct to inspect is the node which precedes
+         --  the context, unless the context is a compilaton unit. The
+         --  transitions are:
+         --
+         --    visible declarations -> upper level
+         --    visible declarations -> terminate
+
+         elsif Has_Suitable_Construct (Vis_Decls)
+           and then List_Containing (Start) = Vis_Decls
+         then
+            Transition_Unit (Parent (Spec), Curr);
+
+         --  At this point both declarative lists are empty, but the traversal
+         --  still came from within the spec. This indicates that the invariant
+         --  of the algorithm has been violated.
+
+         else
+            pragma Assert (False);
+            raise ECR_Found;
+         end if;
+      end Transition_Spec_Declarations;
+
+      ---------------------
+      -- Transition_Unit --
+      ---------------------
+
+      procedure Transition_Unit
+        (Unit : Node_Id;
+         Curr : in out Node_Id)
+      is
+         Context : constant Node_Id := Parent (Unit);
+
+      begin
+         --  The unit is a compilation unit. This terminates the search because
+         --  there are no more lists to inspect and there are no more enclosing
+         --  constructs to climb up to.
+
+         if Nkind (Context) = N_Compilation_Unit then
+
+            --  A package body with a corresponding spec subject to pragma
+            --  Elaborate_Body is an exception to the above. The annotation
+            --  allows the search to continue into the package declaration.
+            --  The transitions are:
+            --
+            --    statements   -> corresponding package spec (Elab_Body)
+            --    declarations -> corresponding package spec (Elab_Body)
+
+            if Nkind (Unit) = N_Package_Body
+              and then (Assume_Elab_Body
+                         or else Has_Pragma_Elaborate_Body
+                                   (Corresponding_Spec (Unit)))
+            then
+               Curr := Unit_Declaration_Node (Corresponding_Spec (Unit));
+               Enter_Package_Declaration (Curr);
+
+            --  Otherwise terminate the search. The transitions are:
+            --
+            --    private declarations -> terminate
+            --    visible declarations -> terminate
+            --    statements           -> terminate
+            --    declarations         -> terminate
+
+            else
+               raise ECR_Found;
+            end if;
+
+         --  The unit is a subunit. The construct to inspect is the node which
+         --  precedes the corresponding stub. Update the early call region to
+         --  include the unit.
+
+         elsif Nkind (Context) = N_Subunit then
+            Start := Unit;
+            Curr  := Corresponding_Stub (Context);
+
+         --  Otherwise the unit is nested. The construct to inspect is the node
+         --  which precedes the unit. Update the early call region to include
+         --  the unit.
+
+         else
+            Include (Unit, Curr);
+         end if;
+      end Transition_Unit;
+
+      --  Local variables
+
+      Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
+      Region  : Node_Id;
+
+   --  Start of processing for Find_Early_Call_Region
+
+   begin
+      --  The caller demands the start of the early call region without saving
+      --  or retrieving it to/from internal data structures.
+
+      if Skip_Memoization then
+         Region := Find_ECR (Body_Decl);
+
+      --  Default behavior
+
+      else
+         --  Check whether the early call region of the subprogram body is
+         --  available.
+
+         Region := Early_Call_Region (Body_Id);
+
+         if No (Region) then
+
+            --  Traverse the declarations in reverse order, starting from the
+            --  subprogram body, searching for the nearest non-preelaborable
+            --  construct. The early call region starts after this construct
+            --  and ends at the subprogram body.
+
+            Region := Find_ECR (Body_Decl);
+
+            --  Associate the early call region with the subprogram body in
+            --  case other scenarios need it.
+
+            Set_Early_Call_Region (Body_Id, Region);
+         end if;
+      end if;
+
+      --  A subprogram body must always have an early call region
+
+      pragma Assert (Present (Region));
+
+      return Region;
+   end Find_Early_Call_Region;
+
    ---------------------------
    -- Find_Elaborated_Units --
    ---------------------------
@@ -3292,35 +4975,41 @@ package body Sem_Elab is
             return;
          end if;
 
-         Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+         Elab_Attrs := Elaboration_Status (Unit_Id);
 
-         --  The current unit is not part of the context. Prepare a new set of
-         --  attributes.
+         --  The unit is already included in the context by means of pragma
+         --  Elaborate[_All].
 
-         if Elab_Attrs = No_Elaboration_Attributes then
-            Elab_Attrs :=
-              Elaboration_Attributes'(Source_Pragma => Prag,
-                                      With_Clause   => Empty);
+         if Present (Elab_Attrs.Source_Pragma) then
 
-         --  The unit is already included in the context by means of pragma
-         --  Elaborate. "Upgrage" the existing attributes when the unit is
-         --  subject to Elaborate_All because the new pragma covers a larger
-         --  set of units. All other properties remain the same.
+            --  Upgrade an existing pragma Elaborate when the unit is subject
+            --  to Elaborate_All because the new pragma covers a larger set of
+            --  units.
 
-         elsif Pragma_Name (Elab_Attrs.Source_Pragma) = Name_Elaborate
-           and then Pragma_Name (Prag) = Name_Elaborate_All
-         then
-            Elab_Attrs.Source_Pragma := Prag;
+            if Pragma_Name (Elab_Attrs.Source_Pragma) = Name_Elaborate
+              and then Pragma_Name (Prag) = Name_Elaborate_All
+            then
+               Elab_Attrs.Source_Pragma := Prag;
+
+            --  Otherwise the unit retains its existing pragma and does not
+            --  need to be included in the context again.
 
-         --  Otherwise the unit is already included in the context
+            else
+               return;
+            end if;
+
+         --  The current unit is not part of the context. Prepare a new set of
+         --  attributes.
 
          else
-            return;
+            Elab_Attrs :=
+              Elaboration_Attributes'(Source_Pragma => Prag,
+                                      With_Clause   => Empty);
          end if;
 
          --  Add or update the attributes of the unit
 
-         Elaboration_Context.Set (Unit_Id, Elab_Attrs);
+         Set_Elaboration_Status (Unit_Id, Elab_Attrs);
 
          --  Includes all units withed by the current one when computing the
          --  full context.
@@ -4019,7 +5708,7 @@ package body Sem_Elab is
       --  main unit. Consider this case only when requested by the caller.
 
       elsif Context_OK
-        and then Elaboration_Context.Get (Unit_Id) /= No_Elaboration_Attributes
+        and then Elaboration_Status (Unit_Id) /= No_Elaboration_Attributes
       then
          return True;
 
@@ -4155,7 +5844,7 @@ package body Sem_Elab is
             if Nkind (Par) = N_Subunit then
                Par := Corresponding_Stub (Par);
 
-            --  Stop the traversal when the nearest enclosing non-library level
+            --  Stop the traversal when the nearest enclosing non-library-level
             --  encapsulator has been reached.
 
             elsif Is_Non_Library_Level_Encapsulator (Par) then
@@ -5117,13 +6806,30 @@ package body Sem_Elab is
           and then Present (Protected_Subprogram (Id));
    end Is_Protected_Body_Subp;
 
+   --------------------------------
+   -- Is_Recorded_SPARK_Scenario --
+   --------------------------------
+
+   function Is_Recorded_SPARK_Scenario (N : Node_Id) return Boolean is
+   begin
+      if Recorded_SPARK_Scenarios_In_Use then
+         return Recorded_SPARK_Scenarios.Get (N);
+      end if;
+
+      return Recorded_SPARK_Scenarios_No_Element;
+   end Is_Recorded_SPARK_Scenario;
+
    ------------------------------------
    -- Is_Recorded_Top_Level_Scenario --
    ------------------------------------
 
    function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean is
    begin
-      return Recorded_Top_Level_Scenarios.Get (N);
+      if Recorded_Top_Level_Scenarios_In_Use then
+         return Recorded_Top_Level_Scenarios.Get (N);
+      end if;
+
+      return Recorded_Top_Level_Scenarios_No_Element;
    end Is_Recorded_Top_Level_Scenario;
 
    ------------------------
@@ -5451,6 +7157,9 @@ package body Sem_Elab is
 
    function Is_Suitable_Scenario (N : Node_Id) return Boolean is
    begin
+      --  NOTE: Derived types and pragma Refined_State are intentionally left
+      --  out because they are not executable during elaboration.
+
       return
         Is_Suitable_Access (N)
           or else Is_Suitable_Call (N)
@@ -5459,6 +7168,80 @@ package body Sem_Elab is
           or else Is_Suitable_Variable_Reference (N);
    end Is_Suitable_Scenario;
 
+   ------------------------------------
+   -- Is_Suitable_SPARK_Derived_Type --
+   ------------------------------------
+
+   function Is_Suitable_SPARK_Derived_Type (N : Node_Id) return Boolean is
+      Prag : Node_Id;
+      Typ  : Entity_Id;
+
+   begin
+      --  To qualify, the type declaration must denote a derived tagged type
+      --  with primitive operations, subject to pragma SPARK_Mode On.
+
+      if Nkind (N) = N_Full_Type_Declaration
+        and then Nkind (Type_Definition (N)) = N_Derived_Type_Definition
+      then
+         Typ  := Defining_Entity (N);
+         Prag := SPARK_Pragma (Typ);
+
+         return
+           Is_Tagged_Type (Typ)
+             and then Has_Primitive_Operations (Typ)
+             and then Present (Prag)
+             and then Get_SPARK_Mode_From_Annotation (Prag) = On;
+      end if;
+
+      return False;
+   end Is_Suitable_SPARK_Derived_Type;
+
+   -------------------------------------
+   -- Is_Suitable_SPARK_Instantiation --
+   -------------------------------------
+
+   function Is_Suitable_SPARK_Instantiation (N : Node_Id) return Boolean is
+      Gen_Attrs  : Target_Attributes;
+      Gen_Id     : Entity_Id;
+      Inst       : Node_Id;
+      Inst_Attrs : Instantiation_Attributes;
+      Inst_Id    : Entity_Id;
+
+   begin
+      --  To qualify, both the instantiation and the generic must be subject to
+      --  SPARK_Mode On.
+
+      if Is_Suitable_Instantiation (N) then
+         Extract_Instantiation_Attributes
+           (Exp_Inst => N,
+            Inst     => Inst,
+            Inst_Id  => Inst_Id,
+            Gen_Id   => Gen_Id,
+            Attrs    => Inst_Attrs);
+
+         Extract_Target_Attributes (Gen_Id, Gen_Attrs);
+
+         return Inst_Attrs.SPARK_Mode_On and Gen_Attrs.SPARK_Mode_On;
+      end if;
+
+      return False;
+   end Is_Suitable_SPARK_Instantiation;
+
+   --------------------------------------------
+   -- Is_Suitable_SPARK_Refined_State_Pragma --
+   --------------------------------------------
+
+   function Is_Suitable_SPARK_Refined_State_Pragma
+     (N : Node_Id) return Boolean
+   is
+   begin
+      --  To qualfy, the pragma must denote Refined_State
+
+      return
+        Nkind (N) = N_Pragma
+          and then Pragma_Name (N) = Name_Refined_State;
+   end Is_Suitable_SPARK_Refined_State_Pragma;
+
    -------------------------------------
    -- Is_Suitable_Variable_Assignment --
    -------------------------------------
@@ -5625,37 +7408,103 @@ package body Sem_Elab is
       return False;
    end Is_Up_Level_Target;
 
+   ---------------------
+   -- Is_Visited_Body --
+   ---------------------
+
+   function Is_Visited_Body (Body_Decl : Node_Id) return Boolean is
+   begin
+      if Visited_Bodies_In_Use then
+         return Visited_Bodies.Get (Body_Decl);
+      end if;
+
+      return Visited_Bodies_No_Element;
+   end Is_Visited_Body;
+
    -------------------------------
    -- Kill_Elaboration_Scenario --
    -------------------------------
 
    procedure Kill_Elaboration_Scenario (N : Node_Id) is
-      package Scenarios renames Top_Level_Scenarios;
+      procedure Kill_SPARK_Scenario;
+      pragma Inline (Kill_SPARK_Scenario);
+      --  Eliminate scenario N from table SPARK_Scenarios if it is recorded
+      --  there.
 
-   begin
-      --  Eliminate a recorded top-level scenario when it appears within dead
-      --  code because it will not be executed at elaboration time.
+      procedure Kill_Top_Level_Scenario;
+      pragma Inline (Kill_Top_Level_Scenario);
+      --  Eliminate scenario N from table Top_Level_Scenarios if it is recorded
+      --  there.
 
-      if Is_Scenario (N)
-        and then Is_Recorded_Top_Level_Scenario (N)
-      then
-         --  Performance node: list traversal
+      -------------------------
+      -- Kill_SPARK_Scenario --
+      -------------------------
 
-         for Index in Scenarios.First .. Scenarios.Last loop
-            if Scenarios.Table (Index) = N then
-               Scenarios.Table (Index) := Empty;
+      procedure Kill_SPARK_Scenario is
+         package Scenarios renames SPARK_Scenarios;
 
-               --  The top-level scenario is no longer recorded
+      begin
+         if Is_Recorded_SPARK_Scenario (N) then
 
-               Set_Is_Recorded_Top_Level_Scenario (N, False);
-               return;
-            end if;
-         end loop;
+            --  Performance note: list traversal
+
+            for Index in Scenarios.First .. Scenarios.Last loop
+               if Scenarios.Table (Index) = N then
+                  Scenarios.Table (Index) := Empty;
 
-         --  A recorded top-level scenario must be in the table of recorded
-         --  top-level scenarios.
+                  --  The SPARK scenario is no longer recorded
 
-         pragma Assert (False);
+                  Set_Is_Recorded_SPARK_Scenario (N, False);
+                  return;
+               end if;
+            end loop;
+
+            --  A recorded SPARK scenario must be in the table of recorded
+            --  SPARK scenarios.
+
+            pragma Assert (False);
+         end if;
+      end Kill_SPARK_Scenario;
+
+      -----------------------------
+      -- Kill_Top_Level_Scenario --
+      -----------------------------
+
+      procedure Kill_Top_Level_Scenario is
+         package Scenarios renames Top_Level_Scenarios;
+
+      begin
+         if Is_Recorded_Top_Level_Scenario (N) then
+
+            --  Performance node: list traversal
+
+            for Index in Scenarios.First .. Scenarios.Last loop
+               if Scenarios.Table (Index) = N then
+                  Scenarios.Table (Index) := Empty;
+
+                  --  The top-level scenario is no longer recorded
+
+                  Set_Is_Recorded_Top_Level_Scenario (N, False);
+                  return;
+               end if;
+            end loop;
+
+            --  A recorded top-level scenario must be in the table of recorded
+            --  top-level scenarios.
+
+            pragma Assert (False);
+         end if;
+      end Kill_Top_Level_Scenario;
+
+   --  Start of processing for Kill_Elaboration_Scenario
+
+   begin
+      --  Eliminate a recorded scenario when it appears within dead code
+      --  because it will not be executed at elaboration time.
+
+      if Is_Scenario (N) then
+         Kill_SPARK_Scenario;
+         Kill_Top_Level_Scenario;
       end if;
    end Kill_Elaboration_Scenario;
 
@@ -5758,6 +7607,11 @@ package body Sem_Elab is
                Info_Msg => False,
                In_SPARK => True);
 
+         elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+            Error_Msg_N
+              ("read of refinement constituents during elaboration in SPARK",
+               N);
+
          elsif Is_Suitable_Variable_Reference (N) then
             Info_Variable_Reference
               (Ref      => N,
@@ -5847,7 +7701,7 @@ package body Sem_Elab is
       --  enough to meet the requirement.
 
       else
-         Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+         Elab_Attrs := Elaboration_Status (Unit_Id);
 
          --  The pragma must be either Elaborate_All or be as strong as the
          --  requirement.
@@ -5920,6 +7774,9 @@ package body Sem_Elab is
       procedure Output_Instantiation (N : Node_Id);
       --  Emit a specific diagnostic message for instantiation N
 
+      procedure Output_SPARK_Refined_State_Pragma (N : Node_Id);
+      --  Emit a specific diagnostic message for Refined_State pragma N
+
       procedure Output_Variable_Assignment (N : Node_Id);
       --  Emit a specific diagnostic message for assignment statement N
 
@@ -6242,6 +8099,16 @@ package body Sem_Elab is
          end if;
       end Output_Instantiation;
 
+      ---------------------------------------
+      -- Output_SPARK_Refined_State_Pragma --
+      ---------------------------------------
+
+      procedure Output_SPARK_Refined_State_Pragma (N : Node_Id) is
+      begin
+         Error_Msg_Sloc := Sloc (N);
+         Error_Msg_N ("\\  refinement constituents read #", Error_Nod);
+      end Output_SPARK_Refined_State_Pragma;
+
       --------------------------------
       -- Output_Variable_Assignment --
       --------------------------------
@@ -6272,6 +8139,10 @@ package body Sem_Elab is
 
          if Is_Read (N) then
             Error_Msg_NE ("\\  variable & read #", Error_Nod, Var_Id);
+
+         else
+            pragma Assert (False);
+            null;
          end if;
       end Output_Variable_Reference;
 
@@ -6329,6 +8200,11 @@ package body Sem_Elab is
          elsif Is_Suitable_Instantiation (N) then
             Output_Instantiation (N);
 
+         --  Pragma Refined_State
+
+         elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+            Output_SPARK_Refined_State_Pragma (N);
+
          --  Variable assignments
 
          elsif Nkind (N) = N_Assignment_Statement then
@@ -6358,124 +8234,14 @@ package body Sem_Elab is
       Scenario_Stack.Decrement_Last;
    end Pop_Active_Scenario;
 
-   --------------------
-   -- Process_Access --
-   --------------------
-
-   procedure Process_Access
-     (Attr           : Node_Id;
-      In_Partial_Fin : Boolean;
-      In_Task_Body   : Boolean)
-   is
-      function Build_Access_Marker (Target_Id : Entity_Id) return Node_Id;
-      pragma Inline (Build_Access_Marker);
-      --  Create a suitable call marker which invokes target Target_Id
-
-      -------------------------
-      -- Build_Access_Marker --
-      -------------------------
-
-      function Build_Access_Marker (Target_Id : Entity_Id) return Node_Id is
-         Marker : Node_Id;
-
-      begin
-         Marker := Make_Call_Marker (Sloc (Attr));
-
-         --  Inherit relevant attributes from the attribute
-
-         --  Performance note: parent traversal
-
-         Set_Target (Marker, Target_Id);
-         Set_Is_Declaration_Level_Node
-                    (Marker, Find_Enclosing_Level (Attr) = Declaration_Level);
-         Set_Is_Dispatching_Call
-                    (Marker, False);
-         Set_Is_Elaboration_Checks_OK_Node
-                    (Marker, Is_Elaboration_Checks_OK_Node (Attr));
-         Set_Is_Source_Call
-                    (Marker, Comes_From_Source (Attr));
-         Set_Is_SPARK_Mode_On_Node
-                    (Marker, Is_SPARK_Mode_On_Node (Attr));
-
-         --  Partially insert the call marker into the tree by setting its
-         --  parent pointer.
-
-         Set_Parent (Marker, Attr);
-
-         return Marker;
-      end Build_Access_Marker;
-
-      --  Local variables
-
-      Root      : constant Node_Id   := Root_Scenario;
-      Target_Id : constant Entity_Id := Entity (Prefix (Attr));
-
-      Target_Attrs : Target_Attributes;
-
-   --  Start of processing for Process_Access
-
-   begin
-      --  Output relevant information when switch -gnatel (info messages on
-      --  implicit Elaborate[_All] pragmas) is in effect.
-
-      if Elab_Info_Messages then
-         Error_Msg_NE
-           ("info: access to & during elaboration", Attr, Target_Id);
-      end if;
-
-      Extract_Target_Attributes
-        (Target_Id => Target_Id,
-         Attrs     => Target_Attrs);
-
-      --  Both the attribute and the corresponding body are in the same unit.
-      --  The corresponding body must appear prior to the root scenario which
-      --  started the recursive search. If this is not the case, then there is
-      --  a potential ABE if the access value is used to call the subprogram.
-      --  Emit a warning only when switch -gnatw.f (warnings on suspucious
-      --  'Access) is in effect.
-
-      if Warn_On_Elab_Access
-        and then Present (Target_Attrs.Body_Decl)
-        and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl)
-        and then Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl)
-      then
-         Error_Msg_Name_1 := Attribute_Name (Attr);
-         Error_Msg_NE ("??% attribute of & before body seen", Attr, Target_Id);
-         Error_Msg_N ("\possible Program_Error on later references", Attr);
-
-         Output_Active_Scenarios (Attr);
-      end if;
-
-      --  Treat the attribute as an immediate invocation of the target when
-      --  switch -gnatd.o (conservative elaboration order for indirect calls)
-      --  is in effect. Note that the prior elaboration of the unit containing
-      --  the target is ensured processing the corresponding call marker.
-
-      if Debug_Flag_Dot_O then
-         Process_Scenario
-           (N              => Build_Access_Marker (Target_Id),
-            In_Partial_Fin => In_Partial_Fin,
-            In_Task_Body   => In_Task_Body);
-
-      --  Otherwise ensure that the unit with the corresponding body is
-      --  elaborated prior to the main unit.
-
-      else
-         Ensure_Prior_Elaboration
-           (N              => Attr,
-            Unit_Id        => Target_Attrs.Unit_Id,
-            In_Partial_Fin => In_Partial_Fin,
-            In_Task_Body   => In_Task_Body);
-      end if;
-   end Process_Access;
-
-   -----------------------------
-   -- Process_Activation_Call --
-   -----------------------------
+   --------------------------------
+   -- Process_Activation_Generic --
+   --------------------------------
 
-   procedure Process_Activation_Call
+   procedure Process_Activation_Generic
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean)
    is
@@ -6509,6 +8275,7 @@ package body Sem_Elab is
                Call_Attrs     => Call_Attrs,
                Obj_Id         => Obj_Id,
                Task_Attrs     => Task_Attrs,
+               In_Init_Cond   => In_Init_Cond,
                In_Partial_Fin => In_Partial_Fin,
                In_Task_Body   => In_Task_Body);
 
@@ -6561,7 +8328,7 @@ package body Sem_Elab is
       Context : Node_Id;
       Spec    : Node_Id;
 
-   --  Start of processing for Process_Activation_Call
+   --  Start of processing for Process_Activation_Generic
 
    begin
       --  Nothing to do when the activation is a guaranteed ABE
@@ -6617,17 +8384,132 @@ package body Sem_Elab is
 
          Process_Task_Objects (Statements (Context));
       end if;
-   end Process_Activation_Call;
+   end Process_Activation_Generic;
+
+   ------------------------------------
+   -- Process_Conditional_ABE_Access --
+   ------------------------------------
+
+   procedure Process_Conditional_ABE_Access
+     (Attr           : Node_Id;
+      In_Init_Cond   : Boolean;
+      In_Partial_Fin : Boolean;
+      In_Task_Body   : Boolean)
+   is
+      function Build_Access_Marker (Target_Id : Entity_Id) return Node_Id;
+      pragma Inline (Build_Access_Marker);
+      --  Create a suitable call marker which invokes target Target_Id
+
+      -------------------------
+      -- Build_Access_Marker --
+      -------------------------
+
+      function Build_Access_Marker (Target_Id : Entity_Id) return Node_Id is
+         Marker : Node_Id;
+
+      begin
+         Marker := Make_Call_Marker (Sloc (Attr));
+
+         --  Inherit relevant attributes from the attribute
+
+         --  Performance note: parent traversal
+
+         Set_Target (Marker, Target_Id);
+         Set_Is_Declaration_Level_Node
+                    (Marker, Find_Enclosing_Level (Attr) = Declaration_Level);
+         Set_Is_Dispatching_Call
+                    (Marker, False);
+         Set_Is_Elaboration_Checks_OK_Node
+                    (Marker, Is_Elaboration_Checks_OK_Node (Attr));
+         Set_Is_Source_Call
+                    (Marker, Comes_From_Source (Attr));
+         Set_Is_SPARK_Mode_On_Node
+                    (Marker, Is_SPARK_Mode_On_Node (Attr));
+
+         --  Partially insert the call marker into the tree by setting its
+         --  parent pointer.
+
+         Set_Parent (Marker, Attr);
+
+         return Marker;
+      end Build_Access_Marker;
+
+      --  Local variables
+
+      Root      : constant Node_Id   := Root_Scenario;
+      Target_Id : constant Entity_Id := Entity (Prefix (Attr));
+
+      Target_Attrs : Target_Attributes;
+
+   --  Start of processing for Process_Conditional_ABE_Access
+
+   begin
+      --  Output relevant information when switch -gnatel (info messages on
+      --  implicit Elaborate[_All] pragmas) is in effect.
+
+      if Elab_Info_Messages then
+         Error_Msg_NE
+           ("info: access to & during elaboration", Attr, Target_Id);
+      end if;
+
+      Extract_Target_Attributes
+        (Target_Id => Target_Id,
+         Attrs     => Target_Attrs);
+
+      --  Both the attribute and the corresponding body are in the same unit.
+      --  The corresponding body must appear prior to the root scenario which
+      --  started the recursive search. If this is not the case, then there is
+      --  a potential ABE if the access value is used to call the subprogram.
+      --  Emit a warning only when switch -gnatw.f (warnings on suspucious
+      --  'Access) is in effect.
+
+      if Warn_On_Elab_Access
+        and then Present (Target_Attrs.Body_Decl)
+        and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl)
+        and then Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl)
+      then
+         Error_Msg_Name_1 := Attribute_Name (Attr);
+         Error_Msg_NE ("??% attribute of & before body seen", Attr, Target_Id);
+         Error_Msg_N ("\possible Program_Error on later references", Attr);
+
+         Output_Active_Scenarios (Attr);
+      end if;
+
+      --  Treat the attribute as an immediate invocation of the target when
+      --  switch -gnatd.o (conservative elaboration order for indirect calls)
+      --  is in effect. Note that the prior elaboration of the unit containing
+      --  the target is ensured processing the corresponding call marker.
+
+      if Debug_Flag_Dot_O then
+         Process_Conditional_ABE
+           (N              => Build_Access_Marker (Target_Id),
+            In_Init_Cond   => In_Init_Cond,
+            In_Partial_Fin => In_Partial_Fin,
+            In_Task_Body   => In_Task_Body);
+
+      --  Otherwise ensure that the unit with the corresponding body is
+      --  elaborated prior to the main unit.
+
+      else
+         Ensure_Prior_Elaboration
+           (N              => Attr,
+            Unit_Id        => Target_Attrs.Unit_Id,
+            Prag_Nam       => Name_Elaborate_All,
+            In_Partial_Fin => In_Partial_Fin,
+            In_Task_Body   => In_Task_Body);
+      end if;
+   end Process_Conditional_ABE_Access;
 
    ---------------------------------------------
-   -- Process_Activation_Conditional_ABE_Impl --
+   -- Process_Conditional_ABE_Activation_Impl --
    ---------------------------------------------
 
-   procedure Process_Activation_Conditional_ABE_Impl
+   procedure Process_Conditional_ABE_Activation_Impl
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
       Obj_Id         : Entity_Id;
       Task_Attrs     : Task_Attributes;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean)
    is
@@ -6834,174 +8716,30 @@ package body Sem_Elab is
          Ensure_Prior_Elaboration
            (N              => Call,
             Unit_Id        => Task_Attrs.Unit_Id,
+            Prag_Nam       => Name_Elaborate_All,
             In_Partial_Fin => In_Partial_Fin,
             In_Task_Body   => In_Task_Body);
       end if;
 
       Traverse_Body
         (N              => Task_Attrs.Body_Decl,
+         In_Init_Cond   => In_Init_Cond,
          In_Partial_Fin => In_Partial_Fin,
          In_Task_Body   => True);
-   end Process_Activation_Conditional_ABE_Impl;
-
-   procedure Process_Activation_Conditional_ABE is
-     new Process_Activation_Call (Process_Activation_Conditional_ABE_Impl);
-
-   --------------------------------------------
-   -- Process_Activation_Guaranteed_ABE_Impl --
-   --------------------------------------------
-
-   procedure Process_Activation_Guaranteed_ABE_Impl
-     (Call           : Node_Id;
-      Call_Attrs     : Call_Attributes;
-      Obj_Id         : Entity_Id;
-      Task_Attrs     : Task_Attributes;
-      In_Partial_Fin : Boolean;
-      In_Task_Body   : Boolean)
-   is
-      pragma Unreferenced (Call_Attrs);
-      pragma Unreferenced (In_Partial_Fin);
-      pragma Unreferenced (In_Task_Body);
-
-      Check_OK : constant Boolean :=
-                   not Is_Ignored_Ghost_Entity (Obj_Id)
-                     and then not Task_Attrs.Ghost_Mode_Ignore
-                     and then Is_Elaboration_Checks_OK_Id (Obj_Id)
-                     and then Task_Attrs.Elab_Checks_OK;
-      --  A run-time ABE check may be installed only when the object and the
-      --  task type have active elaboration checks, and both are not ignored
-      --  Ghost constructs.
-
-   begin
-      --  Nothing to do when the root scenario appears at the declaration
-      --  level and the task is in the same unit, but outside this context.
-
-      --    task type Task_Typ;                  --  task declaration
-
-      --    procedure Proc is
-      --       function A ... is
-      --       begin
-      --          if Some_Condition then
-      --             declare
-      --                T : Task_Typ;
-      --             begin
-      --                <activation call>        --  activation site
-      --             end;
-      --          ...
-      --       end A;
-
-      --       X : ... := A;                     --  root scenario
-      --    ...
-
-      --    task body Task_Typ is
-      --       ...
-      --    end Task_Typ;
-
-      --  In the example above, the context of X is the declarative list of
-      --  Proc. The "elaboration" of X may reach the activation of T whose body
-      --  is defined outside of X's context. The task body is relevant only
-      --  when Proc is invoked, but this happens only in "normal" elaboration,
-      --  therefore the task body must not be considered if this is not the
-      --  case.
-
-      --  Performance note: parent traversal
-
-      if Is_Up_Level_Target (Task_Attrs.Task_Decl) then
-         return;
-
-      --  Nothing to do when the activation is ABE-safe
-
-      --    generic
-      --    package Gen is
-      --       task type Task_Typ;
-      --    end Gen;
-
-      --    package body Gen is
-      --       task body Task_Typ is
-      --       begin
-      --          ...
-      --       end Task_Typ;
-      --    end Gen;
-
-      --    with Gen;
-      --    procedure Main is
-      --       package Nested is
-      --          ...
-      --       end Nested;
-
-      --       package body Nested is
-      --          package Inst is new Gen;
-      --          T : Inst.Task_Typ;
-      --      [begin]
-      --          <activation call>              --  safe activation
-      --       end Nested;
-      --    ...
-
-      elsif Is_Safe_Activation (Call, Task_Attrs.Task_Decl) then
-         return;
-
-      --  An activation call leads to a guaranteed ABE when the activation
-      --  call and the task appear within the same context ignoring library
-      --  levels, and the body of the task has not been seen yet or appears
-      --  after the activation call.
-
-      --    procedure Guaranteed_ABE is
-      --       task type Task_Typ;
-
-      --       package Nested is
-      --          ...
-      --       end Nested;
-
-      --       package body Nested is
-      --          T : Task_Typ;
-      --      [begin]
-      --          <activation call>              --  guaranteed ABE
-      --       end Nested;
-
-      --       task body Task_Typ is
-      --          ...
-      --       end Task_Typ;
-      --    ...
-
-      --  Performance note: parent traversal
-
-      elsif Is_Guaranteed_ABE
-              (N           => Call,
-               Target_Decl => Task_Attrs.Task_Decl,
-               Target_Body => Task_Attrs.Body_Decl)
-      then
-         Error_Msg_Sloc := Sloc (Call);
-         Error_Msg_N
-           ("??task & will be activated # before elaboration of its body",
-            Obj_Id);
-         Error_Msg_N ("\Program_Error will be raised at run time", Obj_Id);
+   end Process_Conditional_ABE_Activation_Impl;
 
-         --  Mark the activation call as a guaranteed ABE
-
-         Set_Is_Known_Guaranteed_ABE (Call);
-
-         --  Install a run-time ABE failue because this activation call will
-         --  always result in an ABE.
+   procedure Process_Conditional_ABE_Activation is
+     new Process_Activation_Generic (Process_Conditional_ABE_Activation_Impl);
 
-         if Check_OK then
-            Install_ABE_Failure
-              (N       => Call,
-               Ins_Nod => Call);
-         end if;
-      end if;
-   end Process_Activation_Guaranteed_ABE_Impl;
-
-   procedure Process_Activation_Guaranteed_ABE is
-     new Process_Activation_Call (Process_Activation_Guaranteed_ABE_Impl);
-
-   ------------------
-   -- Process_Call --
-   ------------------
+   ----------------------------------
+   -- Process_Conditional_ABE_Call --
+   ----------------------------------
 
-   procedure Process_Call
+   procedure Process_Conditional_ABE_Call
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
       Target_Id      : Entity_Id;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean)
    is
@@ -7083,17 +8821,25 @@ package body Sem_Elab is
 
       --  Local variables
 
+      Init_Cond_On   : Boolean;
       Partial_Fin_On : Boolean;
       SPARK_Rules_On : Boolean;
       Target_Attrs   : Target_Attributes;
 
-   --  Start of processing for Process_Call
+   --  Start of processing for Process_Conditional_ABE_Call
 
    begin
       Extract_Target_Attributes
         (Target_Id => Target_Id,
          Attrs     => Target_Attrs);
 
+      --  The call occurs in an initial condition context when a prior
+      --  scenario is already in that mode, or when the target denotes
+      --  an Initial_Condition procedure.
+
+      Init_Cond_On :=
+        In_Init_Cond or else Is_Initial_Condition_Proc (Target_Id);
+
       --  The call occurs in a partial finalization context when a prior
       --  scenario is already in that mode, or when the target denotes a
       --  [Deep_]Finalize primitive or a finalizer within an initialization
@@ -7169,22 +8915,24 @@ package body Sem_Elab is
       elsif Is_Up_Level_Target (Target_Attrs.Spec_Decl) then
          return;
 
-      --  The SPARK rules are verified only when -gnatd.v (enforce SPARK
-      --  elaboration rules in SPARK code) is in effect.
+      --  The SPARK rules are in effect. Note that -gnatd.v (enforce SPARK
+      --  elaboration rules in SPARK code) is intentionally not taken into
+      --  account here because Process_Conditional_ABE_Call_SPARK has two
+      --  separate modes of operation.
 
-      elsif SPARK_Rules_On and Debug_Flag_Dot_V then
-         Process_Call_SPARK
+      elsif SPARK_Rules_On then
+         Process_Conditional_ABE_Call_SPARK
            (Call           => Call,
-            Call_Attrs     => Call_Attrs,
             Target_Id      => Target_Id,
             Target_Attrs   => Target_Attrs,
-            In_Partial_Fin => In_Partial_Fin);
+            In_Init_Cond   => Init_Cond_On,
+            In_Partial_Fin => Partial_Fin_On,
+            In_Task_Body   => In_Task_Body);
 
-      --  Otherwise the Ada rules are in effect, or SPARK code is allowed to
-      --  violate the SPARK rules.
+      --  Otherwise the Ada rules are in effect
 
       else
-         Process_Call_Ada
+         Process_Conditional_ABE_Call_Ada
            (Call           => Call,
             Call_Attrs     => Call_Attrs,
             Target_Id      => Target_Id,
@@ -7196,15 +8944,24 @@ package body Sem_Elab is
       --  Inspect the target body (and barried function) for other suitable
       --  elaboration scenarios.
 
-      Traverse_Body (Target_Attrs.Body_Barf, Partial_Fin_On, In_Task_Body);
-      Traverse_Body (Target_Attrs.Body_Decl, Partial_Fin_On, In_Task_Body);
-   end Process_Call;
+      Traverse_Body
+        (N              => Target_Attrs.Body_Barf,
+         In_Init_Cond   => Init_Cond_On,
+         In_Partial_Fin => Partial_Fin_On,
+         In_Task_Body   => In_Task_Body);
 
-   ----------------------
-   -- Process_Call_Ada --
-   ----------------------
+      Traverse_Body
+        (N              => Target_Attrs.Body_Decl,
+         In_Init_Cond   => Init_Cond_On,
+         In_Partial_Fin => Partial_Fin_On,
+         In_Task_Body   => In_Task_Body);
+   end Process_Conditional_ABE_Call;
+
+   --------------------------------------
+   -- Process_Conditional_ABE_Call_Ada --
+   --------------------------------------
 
-   procedure Process_Call_Ada
+   procedure Process_Conditional_ABE_Call_Ada
      (Call           : Node_Id;
       Call_Attrs     : Call_Attributes;
       Target_Id      : Entity_Id;
@@ -7221,6 +8978,8 @@ package body Sem_Elab is
       --  target have active elaboration checks, and both are not ignored Ghost
       --  constructs.
 
+      Root : constant Node_Id := Root_Scenario;
+
    begin
       --  Nothing to do for an Ada dispatching call because there are no ABE
       --  diagnostics for either models. ABE checks for the dynamic model are
@@ -7253,12 +9012,65 @@ package body Sem_Elab is
       elsif Present (Target_Attrs.Body_Decl)
         and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl)
       then
-         Process_Call_Conditional_ABE
-           (Call           => Call,
-            Call_Attrs     => Call_Attrs,
-            Target_Id      => Target_Id,
-            Target_Attrs   => Target_Attrs,
-            In_Partial_Fin => In_Partial_Fin);
+         --  If the root scenario appears prior to the target body, then this
+         --  is a possible ABE with respect to the root scenario.
+
+         --    function B ...;
+
+         --    function A ... is
+         --    begin
+         --       if Some_Condition then
+         --          return B;                      --  call site
+         --       ...
+         --    end A;
+
+         --    X : ... := A;                        --  root scenario
+
+         --    function B ... is                    --  target body
+         --       ...
+         --    end B;
+
+         --    Y : ... := A;                        --  root scenario
+
+         --  IMPORTANT: The call to B from A is a possible ABE for X, but not
+         --  for Y. Installing an unconditional ABE raise prior to the call to
+         --  B would be wrong as it will fail for Y as well, but in Y's case
+         --  the call to B is never an ABE.
+
+         if Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl) then
+
+            --  Do not emit any ABE diagnostics when the call occurs in a
+            --  partial finalization context because this leads to confusing
+            --  noise.
+
+            if In_Partial_Fin then
+               null;
+
+            --  ABE diagnostics are emitted only in the static model because
+            --  there is a well-defined order to visiting scenarios. Without
+            --  this order diagnostics appear jumbled and result in unwanted
+            --  noise.
+
+            elsif Static_Elaboration_Checks then
+               Error_Msg_NE
+                 ("??cannot call & before body seen", Call, Target_Id);
+               Error_Msg_N ("\Program_Error may be raised at run time", Call);
+
+               Output_Active_Scenarios (Call);
+            end if;
+
+            --  Install a conditional run-time ABE check to verify that the
+            --  target body has been elaborated prior to the call.
+
+            if Check_OK then
+               Install_ABE_Check
+                 (N           => Call,
+                  Ins_Nod     => Call,
+                  Target_Id   => Target_Attrs.Spec_Id,
+                  Target_Decl => Target_Attrs.Spec_Decl,
+                  Target_Body => Target_Attrs.Body_Decl);
+            end if;
+         end if;
 
       --  Otherwise the target body is not available in this compilation or it
       --  resides in an external unit. Install a run-time ABE check to verify
@@ -7281,326 +9093,201 @@ package body Sem_Elab is
          Ensure_Prior_Elaboration
            (N              => Call,
             Unit_Id        => Target_Attrs.Unit_Id,
+            Prag_Nam       => Name_Elaborate_All,
             In_Partial_Fin => In_Partial_Fin,
             In_Task_Body   => In_Task_Body);
       end if;
-   end Process_Call_Ada;
+   end Process_Conditional_ABE_Call_Ada;
 
-   ----------------------------------
-   -- Process_Call_Conditional_ABE --
-   ----------------------------------
+   ----------------------------------------
+   -- Process_Conditional_ABE_Call_SPARK --
+   ----------------------------------------
 
-   procedure Process_Call_Conditional_ABE
+   procedure Process_Conditional_ABE_Call_SPARK
      (Call           : Node_Id;
-      Call_Attrs     : Call_Attributes;
       Target_Id      : Entity_Id;
       Target_Attrs   : Target_Attributes;
-      In_Partial_Fin : Boolean)
+      In_Init_Cond   : Boolean;
+      In_Partial_Fin : Boolean;
+      In_Task_Body   : Boolean)
    is
-      Check_OK : constant Boolean :=
-                   not Call_Attrs.Ghost_Mode_Ignore
-                     and then not Target_Attrs.Ghost_Mode_Ignore
-                     and then Call_Attrs.Elab_Checks_OK
-                     and then Target_Attrs.Elab_Checks_OK;
-      --  A run-time ABE check may be installed only when both the call and the
-      --  target have active elaboration checks, and both are not ignored Ghost
-      --  constructs.
-
-      Root : constant Node_Id := Root_Scenario;
+      Region : Node_Id;
 
    begin
-      --  If the root scenario appears prior to the target body, then this is a
-      --  possible ABE with respect to the root scenario.
-
-      --    function B ...;
-
-      --    function A ... is
-      --    begin
-      --       if Some_Condition then
-      --          return B;                      --  call site
-      --       ...
-      --    end A;
-
-      --    X : ... := A;                        --  root scenario
-
-      --    function B ... is                    --  target body
-      --       ...
-      --    end B;
-
-      --    Y : ... := A;                        --  root scenario
-
-      --  IMPORTANT: The call to B from A is a possible ABE for X, but not for
-      --  Y. Installing an unconditional ABE raise prior to the call to B would
-      --  be wrong as it will fail for Y as well, but in Y's case the call to B
-      --  is never an ABE.
-
-      if Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl) then
-
-         --  Do not emit any ABE diagnostics when the call occurs in a partial
-         --  finalization context because this leads to confusing noise.
-
-         if In_Partial_Fin then
-            null;
+      --  The call and the target body are both in the main unit
 
-         --  ABE diagnostics are emitted only in the static model because there
-         --  is a well-defined order to visiting scenarios. Without this order
-         --  diagnostics appear jumbled and result in unwanted noise.
+      if Present (Target_Attrs.Body_Decl)
+        and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl)
+      then
+         --  If the call appears prior to the target body, then the call must
+         --  appear within the early call region of the target body.
 
-         elsif Static_Elaboration_Checks then
-            Error_Msg_NE ("??cannot call & before body seen", Call, Target_Id);
-            Error_Msg_N ("\Program_Error may be raised at run time", Call);
+         --    function B ...;
 
-            Output_Active_Scenarios (Call);
-         end if;
+         --    X : ... := B;                     --  call site
 
-         --  Install a conditional run-time ABE check to verify that the target
-         --  body has been elaborated prior to the call.
+         --    <preelaborable construct 1>       --+
+         --               ...                      | early call region
+         --    <preelaborable construct N>       --+
 
-         if Check_OK then
-            Install_ABE_Check
-              (N           => Call,
-               Ins_Nod     => Call,
-               Target_Id   => Target_Attrs.Spec_Id,
-               Target_Decl => Target_Attrs.Spec_Decl,
-               Target_Body => Target_Attrs.Body_Decl);
-         end if;
-      end if;
-   end Process_Call_Conditional_ABE;
-
-   ---------------------------------
-   -- Process_Call_Guaranteed_ABE --
-   ---------------------------------
+         --    function B ... is                 --  target body
+         --       ...
+         --    end B;
+
+         --  When the call to B is not nested within some other scenario, the
+         --  call is automatically illegal because it can never appear in the
+         --  early call region of B's body. This is equivalent to a guaranteed
+         --  ABE.
+
+         --    <preelaborable construct 1>       --+
+         --                                        |
+         --    function B ...;                     |
+         --                                        |
+         --    function A ... is                   |
+         --    begin                               | early call region
+         --       if Some_Condition then
+         --          return B;                   --  call site
+         --       ...
+         --    end A;                              |
+         --                                        |
+         --    <preelaborable construct N>       --+
 
-   procedure Process_Call_Guaranteed_ABE
-     (Call       : Node_Id;
-      Call_Attrs : Call_Attributes;
-      Target_Id  : Entity_Id)
-   is
-      Target_Attrs : Target_Attributes;
+         --    function B ... is                 --  target body
+         --       ...
+         --    end B;
 
-   begin
-      Extract_Target_Attributes
-        (Target_Id => Target_Id,
-         Attrs     => Target_Attrs);
+         --  When the call to B is nested within some other scenario, the call
+         --  is always ABE-safe. It is not immediately obvious why this is the
+         --  case. The elaboration safety follows from the early call region
+         --  rule being applied to ALL calls preceding their associated bodies.
 
-      --  Nothing to do when the root scenario appears at the declaration level
-      --  and the target is in the same unit, but outside this context.
+         --  In the example above, the call to B is safe as long as the call to
+         --  A is safe. There are several cases to consider:
 
-      --    function B ...;                      --  target declaration
+         --    <call 1 to A>
+         --    function B ...;
 
-      --    procedure Proc is
-      --       function A ... is
-      --       begin
-      --          if Some_Condition then
-      --             return B;                   --  call site
-      --          ...
-      --       end A;
+         --    <call 2 to A>
+         --    function A ... is
+         --    begin
+         --       if Some_Condition then
+         --          return B;
+         --       ...
+         --    end A;
 
-      --       X : ... := A;                     --  root scenario
-      --    ...
+         --    <call 3 to A>
+         --    function B ... is
+         --       ...
+         --    end B;
 
-      --    function B ... is
-      --       ...
-      --    end B;
+         --  * Call 1 - This call is either nested within some scenario or not,
+         --    which falls under the two general cases outlined above.
 
-      --  In the example above, the context of X is the declarative region of
-      --  Proc. The "elaboration" of X may eventually reach B which is defined
-      --  outside of X's context. B is relevant only when Proc is invoked, but
-      --  this happens only by means of "normal" elaboration, therefore B must
-      --  not be considered if this is not the case.
+         --  * Call 2 - This is the same case as Call 1.
 
-      --  Performance note: parent traversal
+         --  * Call 3 - The placement of this call limits the range of B's
+         --    early call region unto call 3, therefore the call to B is no
+         --    longer within the early call region of B's body, making it ABE-
+         --    unsafe and therefore illegal.
 
-      if Is_Up_Level_Target (Target_Attrs.Spec_Decl) then
-         return;
+         if Earlier_In_Extended_Unit (Call, Target_Attrs.Body_Decl) then
 
-      --  Nothing to do when the call is ABE-safe
+            --  Do not emit any ABE diagnostics when the call occurs in an
+            --  initial condition context because this leads to incorrect
+            --  diagnostics.
 
-      --    generic
-      --    function Gen ...;
+            if In_Init_Cond then
+               null;
 
-      --    function Gen ... is
-      --    begin
-      --       ...
-      --    end Gen;
+            --  Do not emit any ABE diagnostics when the call occurs in a
+            --  partial finalization context because this leads to confusing
+            --  noise.
 
-      --    with Gen;
-      --    procedure Main is
-      --       function Inst is new Gen;
-      --       X : ... := Inst;                  --  safe call
-      --    ...
+            elsif In_Partial_Fin then
+               null;
 
-      elsif Is_Safe_Call (Call, Target_Attrs) then
-         return;
+            --  ABE diagnostics are emitted only in the static model because
+            --  there is a well-defined order to visiting scenarios. Without
+            --  this order diagnostics appear jumbled and result in unwanted
+            --  noise.
 
-      --  A call leads to a guaranteed ABE when the call and the target appear
-      --  within the same context ignoring library levels, and the body of the
-      --  target has not been seen yet or appears after the call.
+            elsif Static_Elaboration_Checks then
 
-      --    procedure Guaranteed_ABE is
-      --       function Func ...;
+               --  Ensure that a call which textually precedes the subprogram
+               --  body it invokes appears within the early call region of the
+               --  subprogram body.
 
-      --       package Nested is
-      --          Obj : ... := Func;             --  guaranteed ABE
-      --       end Nested;
+               --  IMPORTANT: This check must always be performed even when
+               --  -gnatd.v (enforce SPARK elaboration rules in SPARK code) is
+               --  not specified because the static model cannot guarantee the
+               --  absence of elaboration issues in the presence of dispatching
+               --  calls.
 
-      --       function Func ... is
-      --          ...
-      --       end Func;
-      --    ...
+               Region := Find_Early_Call_Region (Target_Attrs.Body_Decl);
 
-      --  Performance note: parent traversal
+               if Earlier_In_Extended_Unit (Call, Region) then
+                  Error_Msg_NE
+                    ("call must appear within early call region of subprogram "
+                     & "body & (SPARK RM 7.7(3))", Call, Target_Id);
 
-      elsif Is_Guaranteed_ABE
-              (N           => Call,
-               Target_Decl => Target_Attrs.Spec_Decl,
-               Target_Body => Target_Attrs.Body_Decl)
-      then
-         Error_Msg_NE ("??cannot call & before body seen", Call, Target_Id);
-         Error_Msg_N ("\Program_Error will be raised at run time", Call);
+                  Error_Msg_Sloc := Sloc (Region);
+                  Error_Msg_N ("\region starts #", Call);
 
-         --  Mark the call as a guarnateed ABE
+                  Error_Msg_Sloc := Sloc (Target_Attrs.Body_Decl);
+                  Error_Msg_N ("\region ends #", Call);
 
-         Set_Is_Known_Guaranteed_ABE (Call);
+                  Output_Active_Scenarios (Call);
+               end if;
+            end if;
 
-         --  Install a run-time ABE failure because the call will always result
-         --  in an ABE. The failure is installed when both the call and target
-         --  have enabled elaboration checks, and both are not ignored Ghost
-         --  constructs.
+         --  Otherwise the call appears after the target body. The call is
+         --  ABE-safe as a consequence of applying the early call region rule
+         --  to ALL calls preceding their associated bodies.
 
-         if Call_Attrs.Elab_Checks_OK
-           and then Target_Attrs.Elab_Checks_OK
-           and then not Call_Attrs.Ghost_Mode_Ignore
-           and then not Target_Attrs.Ghost_Mode_Ignore
-         then
-            Install_ABE_Failure
-              (N       => Call,
-               Ins_Nod => Call);
+         else
+            null;
          end if;
       end if;
-   end Process_Call_Guaranteed_ABE;
 
-   ------------------------
-   -- Process_Call_SPARK --
-   ------------------------
-
-   procedure Process_Call_SPARK
-     (Call           : Node_Id;
-      Call_Attrs     : Call_Attributes;
-      Target_Id      : Entity_Id;
-      Target_Attrs   : Target_Attributes;
-      In_Partial_Fin : Boolean)
-   is
-   begin
       --  A call to a source target or to a target which emulates Ada or SPARK
       --  semantics imposes an Elaborate_All requirement on the context of the
       --  main unit. Determine whether the context has a pragma strong enough
-      --  to meet the requirement. The check is orthogonal to the ABE effects
-      --  of the call.
+      --  to meet the requirement.
 
-      if Target_Attrs.From_Source
-        or else Is_Ada_Semantic_Target (Target_Id)
-        or else Is_SPARK_Semantic_Target (Target_Id)
-      then
-         Meet_Elaboration_Requirement
-           (N         => Call,
-            Target_Id => Target_Id,
-            Req_Nam   => Name_Elaborate_All);
-      end if;
+      --  IMPORTANT: This check must be performed only when -gnatd.v (enforce
+      --  SPARK elaboration rules in SPARK code) is active because the static
+      --  model can ensure the prior elaboration of the unit which contains a
+      --  body by installing an implicit Elaborate[_All] pragma.
 
-      --  Nothing to do when the call is ABE-safe
-
-      --    generic
-      --    function Gen ...;
-
-      --    function Gen ... is
-      --    begin
-      --       ...
-      --    end Gen;
-
-      --    with Gen;
-      --    procedure Main is
-      --       function Inst is new Gen;
-      --       X : ... := Inst;                  --  safe call
-      --    ...
-
-      if Is_Safe_Call (Call, Target_Attrs) then
-         return;
-
-      --  The call and the target body are both in the main unit
-
-      elsif Present (Target_Attrs.Body_Decl)
-        and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl)
-      then
-         Process_Call_Conditional_ABE
-           (Call           => Call,
-            Call_Attrs     => Call_Attrs,
-            Target_Id      => Target_Id,
-            Target_Attrs   => Target_Attrs,
-            In_Partial_Fin => In_Partial_Fin);
+      if Debug_Flag_Dot_V then
+         if Target_Attrs.From_Source
+           or else Is_Ada_Semantic_Target (Target_Id)
+           or else Is_SPARK_Semantic_Target (Target_Id)
+         then
+            Meet_Elaboration_Requirement
+              (N         => Call,
+               Target_Id => Target_Id,
+               Req_Nam   => Name_Elaborate_All);
+         end if;
 
-      --  Otherwise the target body is not available in this compilation or it
-      --  resides in an external unit. There is no need to guarantee the prior
-      --  elaboration of the unit with the target body because either the main
-      --  unit meets the Elaborate_All requirement imposed by the call, or the
-      --  program is illegal.
+      --  Otherwise ensure that the unit with the target body is elaborated
+      --  prior to the main unit.
 
       else
-         null;
-      end if;
-   end Process_Call_SPARK;
-
-   ----------------------------
-   -- Process_Guaranteed_ABE --
-   ----------------------------
-
-   procedure Process_Guaranteed_ABE (N : Node_Id) is
-      Call_Attrs : Call_Attributes;
-      Target_Id  : Entity_Id;
-
-   begin
-      --  Add the current scenario to the stack of active scenarios
-
-      Push_Active_Scenario (N);
-
-      --  Only calls, instantiations, and task activations may result in a
-      --  guaranteed ABE.
-
-      if Is_Suitable_Call (N) then
-         Extract_Call_Attributes
-           (Call      => N,
-            Target_Id => Target_Id,
-            Attrs     => Call_Attrs);
-
-         if Is_Activation_Proc (Target_Id) then
-            Process_Activation_Guaranteed_ABE
-              (Call           => N,
-               Call_Attrs     => Call_Attrs,
-               In_Partial_Fin => False,
-               In_Task_Body   => False);
-
-         else
-            Process_Call_Guaranteed_ABE
-              (Call       => N,
-               Call_Attrs => Call_Attrs,
-               Target_Id  => Target_Id);
-         end if;
-
-      elsif Is_Suitable_Instantiation (N) then
-         Process_Instantiation_Guaranteed_ABE (N);
+         Ensure_Prior_Elaboration
+           (N              => Call,
+            Unit_Id        => Target_Attrs.Unit_Id,
+            Prag_Nam       => Name_Elaborate_All,
+            In_Partial_Fin => In_Partial_Fin,
+            In_Task_Body   => In_Task_Body);
       end if;
+   end Process_Conditional_ABE_Call_SPARK;
 
-      --  Remove the current scenario from the stack of active scenarios once
-      --  all ABE diagnostics and checks have been performed.
-
-      Pop_Active_Scenario (N);
-   end Process_Guaranteed_ABE;
-
-   ---------------------------
-   -- Process_Instantiation --
-   ---------------------------
+   -------------------------------------------
+   -- Process_Conditional_ABE_Instantiation --
+   -------------------------------------------
 
-   procedure Process_Instantiation
+   procedure Process_Conditional_ABE_Instantiation
      (Exp_Inst       : Node_Id;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean)
@@ -7679,23 +9366,21 @@ package body Sem_Elab is
       elsif Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then
          return;
 
-      --  The SPARK rules are verified only when -gnatd.v (enforce SPARK
-      --  elaboration rules in SPARK code) is in effect.
+      --  The SPARK rules are in effect
 
-      elsif SPARK_Rules_On and Debug_Flag_Dot_V then
-         Process_Instantiation_SPARK
-           (Exp_Inst       => Exp_Inst,
-            Inst           => Inst,
-            Inst_Attrs     => Inst_Attrs,
+      elsif SPARK_Rules_On then
+         Process_Conditional_ABE_Instantiation_SPARK
+           (Inst           => Inst,
             Gen_Id         => Gen_Id,
             Gen_Attrs      => Gen_Attrs,
-            In_Partial_Fin => In_Partial_Fin);
+            In_Partial_Fin => In_Partial_Fin,
+            In_Task_Body   => In_Task_Body);
 
       --  Otherwise the Ada rules are in effect, or SPARK code is allowed to
       --  violate the SPARK rules.
 
       else
-         Process_Instantiation_Ada
+         Process_Conditional_ABE_Instantiation_Ada
            (Exp_Inst       => Exp_Inst,
             Inst           => Inst,
             Inst_Attrs     => Inst_Attrs,
@@ -7704,13 +9389,13 @@ package body Sem_Elab is
             In_Partial_Fin => In_Partial_Fin,
             In_Task_Body   => In_Task_Body);
       end if;
-   end Process_Instantiation;
+   end Process_Conditional_ABE_Instantiation;
 
-   -------------------------------
-   -- Process_Instantiation_Ada --
-   -------------------------------
+   -----------------------------------------------
+   -- Process_Conditional_ABE_Instantiation_Ada --
+   -----------------------------------------------
 
-   procedure Process_Instantiation_Ada
+   procedure Process_Conditional_ABE_Instantiation_Ada
      (Exp_Inst       : Node_Id;
       Inst           : Node_Id;
       Inst_Attrs     : Instantiation_Attributes;
@@ -7728,6 +9413,8 @@ package body Sem_Elab is
       --  the generic have active elaboration checks and both are not ignored
       --  Ghost constructs.
 
+      Root : constant Node_Id := Root_Scenario;
+
    begin
       --  Nothing to do when the instantiation is ABE-safe
 
@@ -7753,13 +9440,69 @@ package body Sem_Elab is
       elsif Present (Gen_Attrs.Body_Decl)
         and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl)
       then
-         Process_Instantiation_Conditional_ABE
-           (Exp_Inst       => Exp_Inst,
-            Inst           => Inst,
-            Inst_Attrs     => Inst_Attrs,
-            Gen_Id         => Gen_Id,
-            Gen_Attrs      => Gen_Attrs,
-            In_Partial_Fin => In_Partial_Fin);
+         --  If the root scenario appears prior to the generic body, then this
+         --  is a possible ABE with respect to the root scenario.
+
+         --    generic
+         --    package Gen is
+         --       ...
+         --    end Gen;
+
+         --    function A ... is
+         --    begin
+         --       if Some_Condition then
+         --          declare
+         --             package Inst is new Gen;    --  instantiation site
+         --       ...
+         --    end A;
+
+         --    X : ... := A;                        --  root scenario
+
+         --    package body Gen is                  --  generic body
+         --       ...
+         --    end Gen;
+
+         --    Y : ... := A;                        --  root scenario
+
+         --  IMPORTANT: The instantiation of Gen is a possible ABE for X, but
+         --  not for Y. Installing an unconditional ABE raise prior to the
+         --  instance site would be wrong as it will fail for Y as well, but in
+         --  Y's case the instantiation of Gen is never an ABE.
+
+         if Earlier_In_Extended_Unit (Root, Gen_Attrs.Body_Decl) then
+
+            --  Do not emit any ABE diagnostics when the instantiation occurs
+            --  in partial finalization context because this leads to unwanted
+            --  noise.
+
+            if In_Partial_Fin then
+               null;
+
+            --  ABE diagnostics are emitted only in the static model because
+            --  there is a well-defined order to visiting scenarios. Without
+            --  this order diagnostics appear jumbled and result in unwanted
+            --  noise.
+
+            elsif Static_Elaboration_Checks then
+               Error_Msg_NE
+                 ("??cannot instantiate & before body seen", Inst, Gen_Id);
+               Error_Msg_N ("\Program_Error may be raised at run time", Inst);
+
+               Output_Active_Scenarios (Inst);
+            end if;
+
+            --  Install a conditional run-time ABE check to verify that the
+            --  generic body has been elaborated prior to the instantiation.
+
+            if Check_OK then
+               Install_ABE_Check
+                 (N           => Inst,
+                  Ins_Nod     => Exp_Inst,
+                  Target_Id   => Gen_Attrs.Spec_Id,
+                  Target_Decl => Gen_Attrs.Spec_Decl,
+                  Target_Body => Gen_Attrs.Body_Decl);
+            end if;
+         end if;
 
       --  Otherwise the generic body is not available in this compilation or it
       --  resides in an external unit. Install a run-time ABE check to verify
@@ -7774,242 +9517,30 @@ package body Sem_Elab is
       end if;
 
       --  Ensure that the unit with the generic body is elaborated prior to
-      --  the main unit. No implicit pragma Elaborate[_All] is generated if
-      --  the instantiation has elaboration checks suppressed. This behaviour
+      --  the main unit. No implicit pragma Elaborate is generated if the
+      --  instantiation has elaboration checks suppressed. This behaviour
       --  parallels that of the old ABE mechanism.
 
       if Inst_Attrs.Elab_Checks_OK then
          Ensure_Prior_Elaboration
            (N              => Inst,
             Unit_Id        => Gen_Attrs.Unit_Id,
+            Prag_Nam       => Name_Elaborate,
             In_Partial_Fin => In_Partial_Fin,
             In_Task_Body   => In_Task_Body);
       end if;
-   end Process_Instantiation_Ada;
+   end Process_Conditional_ABE_Instantiation_Ada;
 
-   -------------------------------------------
-   -- Process_Instantiation_Conditional_ABE --
-   -------------------------------------------
+   -------------------------------------------------
+   -- Process_Conditional_ABE_Instantiation_SPARK --
+   -------------------------------------------------
 
-   procedure Process_Instantiation_Conditional_ABE
-     (Exp_Inst       : Node_Id;
-      Inst           : Node_Id;
-      Inst_Attrs     : Instantiation_Attributes;
+   procedure Process_Conditional_ABE_Instantiation_SPARK
+     (Inst           : Node_Id;
       Gen_Id         : Entity_Id;
       Gen_Attrs      : Target_Attributes;
-      In_Partial_Fin : Boolean)
-   is
-      Check_OK : constant Boolean :=
-                   not Inst_Attrs.Ghost_Mode_Ignore
-                     and then not Gen_Attrs.Ghost_Mode_Ignore
-                     and then Inst_Attrs.Elab_Checks_OK
-                     and then Gen_Attrs.Elab_Checks_OK;
-      --  A run-time ABE check may be installed only when both the instance and
-      --  the generic have active elaboration checks and both are not ignored
-      --  Ghost constructs.
-
-      Root : constant Node_Id := Root_Scenario;
-
-   begin
-      --  If the root scenario appears prior to the generic body, then this is
-      --  a possible ABE with respect to the root scenario.
-
-      --    generic
-      --    package Gen is
-      --       ...
-      --    end Gen;
-
-      --    function A ... is
-      --    begin
-      --       if Some_Condition then
-      --          declare
-      --             package Inst is new Gen;    --  instantiation site
-      --       ...
-      --    end A;
-
-      --    X : ... := A;                        --  root scenario
-
-      --    package body Gen is                  --  generic body
-      --       ...
-      --    end Gen;
-
-      --    Y : ... := A;                        --  root scenario
-
-      --  IMPORTANT: The instantiation of Gen is a possible ABE for X, but not
-      --  for Y. Installing an unconditional ABE raise prior to the instance
-      --  site would be wrong as it will fail for Y as well, but in Y's case
-      --  the instantiation of Gen is never an ABE.
-
-      if Earlier_In_Extended_Unit (Root, Gen_Attrs.Body_Decl) then
-
-         --  Do not emit any ABE diagnostics when the instantiation occurs in a
-         --  partial finalization context because this leads to unwanted noise.
-
-         if In_Partial_Fin then
-            null;
-
-         --  ABE diagnostics are emitted only in the static model because there
-         --  is a well-defined order to visiting scenarios. Without this order
-         --  diagnostics appear jumbled and result in unwanted noise.
-
-         elsif Static_Elaboration_Checks then
-            Error_Msg_NE
-              ("??cannot instantiate & before body seen", Inst, Gen_Id);
-            Error_Msg_N ("\Program_Error may be raised at run time", Inst);
-
-            Output_Active_Scenarios (Inst);
-         end if;
-
-         --  Install a conditional run-time ABE check to verify that the
-         --  generic body has been elaborated prior to the instantiation.
-
-         if Check_OK then
-            Install_ABE_Check
-              (N           => Inst,
-               Ins_Nod     => Exp_Inst,
-               Target_Id   => Gen_Attrs.Spec_Id,
-               Target_Decl => Gen_Attrs.Spec_Decl,
-               Target_Body => Gen_Attrs.Body_Decl);
-         end if;
-      end if;
-   end Process_Instantiation_Conditional_ABE;
-
-   ------------------------------------------
-   -- Process_Instantiation_Guaranteed_ABE --
-   ------------------------------------------
-
-   procedure Process_Instantiation_Guaranteed_ABE (Exp_Inst : Node_Id) is
-      Gen_Attrs  : Target_Attributes;
-      Gen_Id     : Entity_Id;
-      Inst       : Node_Id;
-      Inst_Attrs : Instantiation_Attributes;
-      Inst_Id    : Entity_Id;
-
-   begin
-      Extract_Instantiation_Attributes
-        (Exp_Inst => Exp_Inst,
-         Inst     => Inst,
-         Inst_Id  => Inst_Id,
-         Gen_Id   => Gen_Id,
-         Attrs    => Inst_Attrs);
-
-      Extract_Target_Attributes (Gen_Id, Gen_Attrs);
-
-      --  Nothing to do when the root scenario appears at the declaration level
-      --  and the generic is in the same unit, but outside this context.
-
-      --    generic
-      --    procedure Gen is ...;                --  generic declaration
-
-      --    procedure Proc is
-      --       function A ... is
-      --       begin
-      --          if Some_Condition then
-      --             declare
-      --                procedure I is new Gen;  --  instantiation site
-      --             ...
-      --          ...
-      --       end A;
-
-      --       X : ... := A;                     --  root scenario
-      --    ...
-
-      --    procedure Gen is
-      --       ...
-      --    end Gen;
-
-      --  In the example above, the context of X is the declarative region of
-      --  Proc. The "elaboration" of X may eventually reach Gen which appears
-      --  outside of X's context. Gen is relevant only when Proc is invoked,
-      --  but this happens only by means of "normal" elaboration, therefore
-      --  Gen must not be considered if this is not the case.
-
-      --  Performance note: parent traversal
-
-      if Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then
-         return;
-
-      --  Nothing to do when the instantiation is ABE-safe
-
-      --    generic
-      --    package Gen is
-      --       ...
-      --    end Gen;
-
-      --    package body Gen is
-      --       ...
-      --    end Gen;
-
-      --    with Gen;
-      --    procedure Main is
-      --       package Inst is new Gen (ABE);    --  safe instantiation
-      --    ...
-
-      elsif Is_Safe_Instantiation (Inst, Gen_Attrs) then
-         return;
-
-      --  An instantiation leads to a guaranteed ABE when the instantiation and
-      --  the generic appear within the same context ignoring library levels,
-      --  and the body of the generic has not been seen yet or appears after
-      --  the instantiation.
-
-      --    procedure Guaranteed_ABE is
-      --       generic
-      --       procedure Gen;
-
-      --       package Nested is
-      --          procedure Inst is new Gen;     --  guaranteed ABE
-      --       end Nested;
-
-      --       procedure Gen is
-      --          ...
-      --       end Gen;
-      --    ...
-
-      --  Performance note: parent traversal
-
-      elsif Is_Guaranteed_ABE
-              (N           => Inst,
-               Target_Decl => Gen_Attrs.Spec_Decl,
-               Target_Body => Gen_Attrs.Body_Decl)
-      then
-         Error_Msg_NE
-           ("??cannot instantiate & before body seen", Inst, Gen_Id);
-         Error_Msg_N ("\Program_Error will be raised at run time", Inst);
-
-         --  Mark the instantiation as a guarantee ABE. This automatically
-         --  suppresses the instantiation of the generic body.
-
-         Set_Is_Known_Guaranteed_ABE (Inst);
-
-         --  Install a run-time ABE failure because the instantiation will
-         --  always result in an ABE. The failure is installed when both the
-         --  instance and the generic have enabled elaboration checks, and both
-         --  are not ignored Ghost constructs.
-
-         if Inst_Attrs.Elab_Checks_OK
-           and then Gen_Attrs.Elab_Checks_OK
-           and then not Inst_Attrs.Ghost_Mode_Ignore
-           and then not Gen_Attrs.Ghost_Mode_Ignore
-         then
-            Install_ABE_Failure
-              (N       => Inst,
-               Ins_Nod => Exp_Inst);
-         end if;
-      end if;
-   end Process_Instantiation_Guaranteed_ABE;
-
-   ---------------------------------
-   -- Process_Instantiation_SPARK --
-   ---------------------------------
-
-   procedure Process_Instantiation_SPARK
-     (Exp_Inst       : Node_Id;
-      Inst           : Node_Id;
-      Inst_Attrs     : Instantiation_Attributes;
-      Gen_Id         : Entity_Id;
-      Gen_Attrs      : Target_Attributes;
-      In_Partial_Fin : Boolean)
+      In_Partial_Fin : Boolean;
+      In_Task_Body   : Boolean)
    is
       Req_Nam : Name_Id;
 
@@ -8019,65 +9550,41 @@ package body Sem_Elab is
       --  strong enough to meet the requirement. The check is orthogonal to the
       --  ABE ramifications of the instantiation.
 
-      if Nkind (Inst) = N_Package_Instantiation then
-         Req_Nam := Name_Elaborate_All;
-      else
-         Req_Nam := Name_Elaborate;
-      end if;
-
-      Meet_Elaboration_Requirement
-        (N         => Inst,
-         Target_Id => Gen_Id,
-         Req_Nam   => Req_Nam);
+      --  IMPORTANT: This check must be performed only when -gnatd.v (enforce
+      --  SPARK elaboration rules in SPARK code) is active because the static
+      --  model can ensure the prior elaboration of the unit which contains a
+      --  body by installing an implicit Elaborate[_All] pragma.
 
-      --  Nothing to do when the instantiation is ABE-safe
-
-      --    generic
-      --    package Gen is
-      --       ...
-      --    end Gen;
-
-      --    package body Gen is
-      --       ...
-      --    end Gen;
-
-      --    with Gen;
-      --    procedure Main is
-      --       package Inst is new Gen (ABE);    --  safe instantiation
-      --    ...
-
-      if Is_Safe_Instantiation (Inst, Gen_Attrs) then
-         return;
-
-      --  The instantiation and the generic body are both in the main unit
+      if Debug_Flag_Dot_V then
+         if Nkind (Inst) = N_Package_Instantiation then
+            Req_Nam := Name_Elaborate_All;
+         else
+            Req_Nam := Name_Elaborate;
+         end if;
 
-      elsif Present (Gen_Attrs.Body_Decl)
-        and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl)
-      then
-         Process_Instantiation_Conditional_ABE
-           (Exp_Inst       => Exp_Inst,
-            Inst           => Inst,
-            Inst_Attrs     => Inst_Attrs,
-            Gen_Id         => Gen_Id,
-            Gen_Attrs      => Gen_Attrs,
-            In_Partial_Fin => In_Partial_Fin);
+         Meet_Elaboration_Requirement
+           (N         => Inst,
+            Target_Id => Gen_Id,
+            Req_Nam   => Req_Nam);
 
-      --  Otherwise the generic body is not available in this compilation or
-      --  it resides in an external unit. There is no need to guarantee the
-      --  prior elaboration of the unit with the generic body because either
-      --  the main unit meets the Elaborate[_All] requirement imposed by the
-      --  instantiation, or the program is illegal.
+      --  Otherwise ensure that the unit with the target body is elaborated
+      --  prior to the main unit.
 
       else
-         null;
+         Ensure_Prior_Elaboration
+           (N              => Inst,
+            Unit_Id        => Gen_Attrs.Unit_Id,
+            Prag_Nam       => Name_Elaborate,
+            In_Partial_Fin => In_Partial_Fin,
+            In_Task_Body   => In_Task_Body);
       end if;
-   end Process_Instantiation_SPARK;
+   end Process_Conditional_ABE_Instantiation_SPARK;
 
-   ---------------------------------
-   -- Process_Variable_Assignment --
-   ---------------------------------
+   -------------------------------------------------
+   -- Process_Conditional_ABE_Variable_Assignment --
+   -------------------------------------------------
 
-   procedure Process_Variable_Assignment (Asmt : Node_Id) is
+   procedure Process_Conditional_ABE_Variable_Assignment (Asmt : Node_Id) is
       Var_Id : constant Entity_Id := Entity (Extract_Assignment_Name (Asmt));
       Prag   : constant Node_Id   := SPARK_Pragma (Var_Id);
 
@@ -8111,24 +9618,24 @@ package body Sem_Elab is
       --  variables.
 
       if SPARK_Rules_On then
-         Process_Variable_Assignment_SPARK
+         Process_Conditional_ABE_Variable_Assignment_SPARK
            (Asmt   => Asmt,
             Var_Id => Var_Id);
 
       --  Otherwise the Ada rules are in effect
 
       else
-         Process_Variable_Assignment_Ada
+         Process_Conditional_ABE_Variable_Assignment_Ada
            (Asmt   => Asmt,
             Var_Id => Var_Id);
       end if;
-   end Process_Variable_Assignment;
+   end Process_Conditional_ABE_Variable_Assignment;
 
-   -------------------------------------
-   -- Process_Variable_Assignment_Ada --
-   -------------------------------------
+   -----------------------------------------------------
+   -- Process_Conditional_ABE_Variable_Assignment_Ada --
+   -----------------------------------------------------
 
-   procedure Process_Variable_Assignment_Ada
+   procedure Process_Conditional_ABE_Variable_Assignment_Ada
      (Asmt   : Node_Id;
       Var_Id : Entity_Id)
    is
@@ -8158,13 +9665,13 @@ package body Sem_Elab is
 
          Output_Active_Scenarios (Asmt);
       end if;
-   end Process_Variable_Assignment_Ada;
+   end Process_Conditional_ABE_Variable_Assignment_Ada;
 
-   ---------------------------------------
-   -- Process_Variable_Assignment_SPARK --
-   ---------------------------------------
+   -------------------------------------------------------
+   -- Process_Conditional_ABE_Variable_Assignment_SPARK --
+   -------------------------------------------------------
 
-   procedure Process_Variable_Assignment_SPARK
+   procedure Process_Conditional_ABE_Variable_Assignment_SPARK
      (Asmt   : Node_Id;
       Var_Id : Entity_Id)
    is
@@ -8189,13 +9696,13 @@ package body Sem_Elab is
 
          Output_Active_Scenarios (Asmt);
       end if;
-   end Process_Variable_Assignment_SPARK;
+   end Process_Conditional_ABE_Variable_Assignment_SPARK;
 
-   --------------------------------
-   -- Process_Variable_Reference --
-   --------------------------------
+   ------------------------------------------------
+   -- Process_Conditional_ABE_Variable_Reference --
+   ------------------------------------------------
 
-   procedure Process_Variable_Reference (Ref : Node_Id) is
+   procedure Process_Conditional_ABE_Variable_Reference (Ref : Node_Id) is
       Var_Attrs : Variable_Attributes;
       Var_Id    : Entity_Id;
 
@@ -8206,18 +9713,18 @@ package body Sem_Elab is
          Attrs  => Var_Attrs);
 
       if Is_Read (Ref) then
-         Process_Variable_Reference_Read
+         Process_Conditional_ABE_Variable_Reference_Read
            (Ref    => Ref,
             Var_Id => Var_Id,
             Attrs  => Var_Attrs);
       end if;
-   end Process_Variable_Reference;
+   end Process_Conditional_ABE_Variable_Reference;
 
-   -------------------------------------
-   -- Process_Variable_Reference_Read --
-   -------------------------------------
+   -----------------------------------------------------
+   -- Process_Conditional_ABE_Variable_Reference_Read --
+   -----------------------------------------------------
 
-   procedure Process_Variable_Reference_Read
+   procedure Process_Conditional_ABE_Variable_Reference_Read
      (Ref    : Node_Id;
       Var_Id : Entity_Id;
       Attrs  : Variable_Attributes)
@@ -8263,23 +9770,19 @@ package body Sem_Elab is
             Target_Id => Var_Id,
             Req_Nam   => Name_Elaborate);
       end if;
-   end Process_Variable_Reference_Read;
-
-   --------------------------
-   -- Push_Active_Scenario --
-   --------------------------
+   end Process_Conditional_ABE_Variable_Reference_Read;
 
-   procedure Push_Active_Scenario (N : Node_Id) is
-   begin
-      Scenario_Stack.Append (N);
-   end Push_Active_Scenario;
+   -----------------------------
+   -- Process_Conditional_ABE --
+   -----------------------------
 
-   ----------------------
-   -- Process_Scenario --
-   ----------------------
+   --  NOTE: The body of this routine is intentionally out of order because it
+   --  invokes an instantiated subprogram (Process_Conditional_ABE_Activation).
+   --  Placing the body in alphabetical order will result in a guaranteed ABE.
 
-   procedure Process_Scenario
+   procedure Process_Conditional_ABE
      (N              : Node_Id;
+      In_Init_Cond   : Boolean := False;
       In_Partial_Fin : Boolean := False;
       In_Task_Body   : Boolean := False)
    is
@@ -8294,7 +9797,11 @@ package body Sem_Elab is
       --  'Access
 
       if Is_Suitable_Access (N) then
-         Process_Access (N, In_Partial_Fin, In_Task_Body);
+         Process_Conditional_ABE_Access
+           (Attr           => N,
+            In_Init_Cond   => In_Init_Cond,
+            In_Partial_Fin => In_Partial_Fin,
+            In_Task_Body   => In_Task_Body);
 
       --  Calls
 
@@ -8314,17 +9821,19 @@ package body Sem_Elab is
                Attrs     => Call_Attrs);
 
             if Is_Activation_Proc (Target_Id) then
-               Process_Activation_Conditional_ABE
+               Process_Conditional_ABE_Activation
                  (Call           => N,
                   Call_Attrs     => Call_Attrs,
+                  In_Init_Cond   => In_Init_Cond,
                   In_Partial_Fin => In_Partial_Fin,
                   In_Task_Body   => In_Task_Body);
 
             else
-               Process_Call
+               Process_Conditional_ABE_Call
                  (Call           => N,
                   Call_Attrs     => Call_Attrs,
                   Target_Id      => Target_Id,
+                  In_Init_Cond   => In_Init_Cond,
                   In_Partial_Fin => In_Partial_Fin,
                   In_Task_Body   => In_Task_Body);
             end if;
@@ -8333,12 +9842,15 @@ package body Sem_Elab is
       --  Instantiations
 
       elsif Is_Suitable_Instantiation (N) then
-         Process_Instantiation (N, In_Partial_Fin, In_Task_Body);
+         Process_Conditional_ABE_Instantiation
+           (Exp_Inst       => N,
+            In_Partial_Fin => In_Partial_Fin,
+            In_Task_Body   => In_Task_Body);
 
       --  Variable assignments
 
       elsif Is_Suitable_Variable_Assignment (N) then
-         Process_Variable_Assignment (N);
+         Process_Conditional_ABE_Variable_Assignment (N);
 
       --  Variable references
 
@@ -8353,7 +9865,7 @@ package body Sem_Elab is
          --  reason, external variable references must not be processed.
 
          if In_Main_Context (N) then
-            Process_Variable_Reference (N);
+            Process_Conditional_ABE_Variable_Reference (N);
          end if;
       end if;
 
@@ -8361,7 +9873,454 @@ package body Sem_Elab is
       --  all ABE diagnostics and checks have been performed.
 
       Pop_Active_Scenario (N);
-   end Process_Scenario;
+   end Process_Conditional_ABE;
+
+   --------------------------------------------
+   -- Process_Guaranteed_ABE_Activation_Impl --
+   --------------------------------------------
+
+   procedure Process_Guaranteed_ABE_Activation_Impl
+     (Call           : Node_Id;
+      Call_Attrs     : Call_Attributes;
+      Obj_Id         : Entity_Id;
+      Task_Attrs     : Task_Attributes;
+      In_Init_Cond   : Boolean;
+      In_Partial_Fin : Boolean;
+      In_Task_Body   : Boolean)
+   is
+      pragma Unreferenced (Call_Attrs);
+      pragma Unreferenced (In_Init_Cond);
+      pragma Unreferenced (In_Partial_Fin);
+      pragma Unreferenced (In_Task_Body);
+
+      Check_OK : constant Boolean :=
+                   not Is_Ignored_Ghost_Entity (Obj_Id)
+                     and then not Task_Attrs.Ghost_Mode_Ignore
+                     and then Is_Elaboration_Checks_OK_Id (Obj_Id)
+                     and then Task_Attrs.Elab_Checks_OK;
+      --  A run-time ABE check may be installed only when the object and the
+      --  task type have active elaboration checks, and both are not ignored
+      --  Ghost constructs.
+
+   begin
+      --  Nothing to do when the root scenario appears at the declaration
+      --  level and the task is in the same unit, but outside this context.
+
+      --    task type Task_Typ;                  --  task declaration
+
+      --    procedure Proc is
+      --       function A ... is
+      --       begin
+      --          if Some_Condition then
+      --             declare
+      --                T : Task_Typ;
+      --             begin
+      --                <activation call>        --  activation site
+      --             end;
+      --          ...
+      --       end A;
+
+      --       X : ... := A;                     --  root scenario
+      --    ...
+
+      --    task body Task_Typ is
+      --       ...
+      --    end Task_Typ;
+
+      --  In the example above, the context of X is the declarative list of
+      --  Proc. The "elaboration" of X may reach the activation of T whose body
+      --  is defined outside of X's context. The task body is relevant only
+      --  when Proc is invoked, but this happens only in "normal" elaboration,
+      --  therefore the task body must not be considered if this is not the
+      --  case.
+
+      --  Performance note: parent traversal
+
+      if Is_Up_Level_Target (Task_Attrs.Task_Decl) then
+         return;
+
+      --  Nothing to do when the activation is ABE-safe
+
+      --    generic
+      --    package Gen is
+      --       task type Task_Typ;
+      --    end Gen;
+
+      --    package body Gen is
+      --       task body Task_Typ is
+      --       begin
+      --          ...
+      --       end Task_Typ;
+      --    end Gen;
+
+      --    with Gen;
+      --    procedure Main is
+      --       package Nested is
+      --          ...
+      --       end Nested;
+
+      --       package body Nested is
+      --          package Inst is new Gen;
+      --          T : Inst.Task_Typ;
+      --      [begin]
+      --          <activation call>              --  safe activation
+      --       end Nested;
+      --    ...
+
+      elsif Is_Safe_Activation (Call, Task_Attrs.Task_Decl) then
+         return;
+
+      --  An activation call leads to a guaranteed ABE when the activation
+      --  call and the task appear within the same context ignoring library
+      --  levels, and the body of the task has not been seen yet or appears
+      --  after the activation call.
+
+      --    procedure Guaranteed_ABE is
+      --       task type Task_Typ;
+
+      --       package Nested is
+      --          ...
+      --       end Nested;
+
+      --       package body Nested is
+      --          T : Task_Typ;
+      --      [begin]
+      --          <activation call>              --  guaranteed ABE
+      --       end Nested;
+
+      --       task body Task_Typ is
+      --          ...
+      --       end Task_Typ;
+      --    ...
+
+      --  Performance note: parent traversal
+
+      elsif Is_Guaranteed_ABE
+              (N           => Call,
+               Target_Decl => Task_Attrs.Task_Decl,
+               Target_Body => Task_Attrs.Body_Decl)
+      then
+         Error_Msg_Sloc := Sloc (Call);
+         Error_Msg_N
+           ("??task & will be activated # before elaboration of its body",
+            Obj_Id);
+         Error_Msg_N ("\Program_Error will be raised at run time", Obj_Id);
+
+         --  Mark the activation call as a guaranteed ABE
+
+         Set_Is_Known_Guaranteed_ABE (Call);
+
+         --  Install a run-time ABE failue because this activation call will
+         --  always result in an ABE.
+
+         if Check_OK then
+            Install_ABE_Failure
+              (N       => Call,
+               Ins_Nod => Call);
+         end if;
+      end if;
+   end Process_Guaranteed_ABE_Activation_Impl;
+
+   procedure Process_Guaranteed_ABE_Activation is
+     new Process_Activation_Generic (Process_Guaranteed_ABE_Activation_Impl);
+
+   ---------------------------------
+   -- Process_Guaranteed_ABE_Call --
+   ---------------------------------
+
+   procedure Process_Guaranteed_ABE_Call
+     (Call       : Node_Id;
+      Call_Attrs : Call_Attributes;
+      Target_Id  : Entity_Id)
+   is
+      Target_Attrs : Target_Attributes;
+
+   begin
+      Extract_Target_Attributes
+        (Target_Id => Target_Id,
+         Attrs     => Target_Attrs);
+
+      --  Nothing to do when the root scenario appears at the declaration level
+      --  and the target is in the same unit, but outside this context.
+
+      --    function B ...;                      --  target declaration
+
+      --    procedure Proc is
+      --       function A ... is
+      --       begin
+      --          if Some_Condition then
+      --             return B;                   --  call site
+      --          ...
+      --       end A;
+
+      --       X : ... := A;                     --  root scenario
+      --    ...
+
+      --    function B ... is
+      --       ...
+      --    end B;
+
+      --  In the example above, the context of X is the declarative region of
+      --  Proc. The "elaboration" of X may eventually reach B which is defined
+      --  outside of X's context. B is relevant only when Proc is invoked, but
+      --  this happens only by means of "normal" elaboration, therefore B must
+      --  not be considered if this is not the case.
+
+      --  Performance note: parent traversal
+
+      if Is_Up_Level_Target (Target_Attrs.Spec_Decl) then
+         return;
+
+      --  Nothing to do when the call is ABE-safe
+
+      --    generic
+      --    function Gen ...;
+
+      --    function Gen ... is
+      --    begin
+      --       ...
+      --    end Gen;
+
+      --    with Gen;
+      --    procedure Main is
+      --       function Inst is new Gen;
+      --       X : ... := Inst;                  --  safe call
+      --    ...
+
+      elsif Is_Safe_Call (Call, Target_Attrs) then
+         return;
+
+      --  A call leads to a guaranteed ABE when the call and the target appear
+      --  within the same context ignoring library levels, and the body of the
+      --  target has not been seen yet or appears after the call.
+
+      --    procedure Guaranteed_ABE is
+      --       function Func ...;
+
+      --       package Nested is
+      --          Obj : ... := Func;             --  guaranteed ABE
+      --       end Nested;
+
+      --       function Func ... is
+      --          ...
+      --       end Func;
+      --    ...
+
+      --  Performance note: parent traversal
+
+      elsif Is_Guaranteed_ABE
+              (N           => Call,
+               Target_Decl => Target_Attrs.Spec_Decl,
+               Target_Body => Target_Attrs.Body_Decl)
+      then
+         Error_Msg_NE ("??cannot call & before body seen", Call, Target_Id);
+         Error_Msg_N ("\Program_Error will be raised at run time", Call);
+
+         --  Mark the call as a guarnateed ABE
+
+         Set_Is_Known_Guaranteed_ABE (Call);
+
+         --  Install a run-time ABE failure because the call will always result
+         --  in an ABE. The failure is installed when both the call and target
+         --  have enabled elaboration checks, and both are not ignored Ghost
+         --  constructs.
+
+         if Call_Attrs.Elab_Checks_OK
+           and then Target_Attrs.Elab_Checks_OK
+           and then not Call_Attrs.Ghost_Mode_Ignore
+           and then not Target_Attrs.Ghost_Mode_Ignore
+         then
+            Install_ABE_Failure
+              (N       => Call,
+               Ins_Nod => Call);
+         end if;
+      end if;
+   end Process_Guaranteed_ABE_Call;
+
+   ------------------------------------------
+   -- Process_Guaranteed_ABE_Instantiation --
+   ------------------------------------------
+
+   procedure Process_Guaranteed_ABE_Instantiation (Exp_Inst : Node_Id) is
+      Gen_Attrs  : Target_Attributes;
+      Gen_Id     : Entity_Id;
+      Inst       : Node_Id;
+      Inst_Attrs : Instantiation_Attributes;
+      Inst_Id    : Entity_Id;
+
+   begin
+      Extract_Instantiation_Attributes
+        (Exp_Inst => Exp_Inst,
+         Inst     => Inst,
+         Inst_Id  => Inst_Id,
+         Gen_Id   => Gen_Id,
+         Attrs    => Inst_Attrs);
+
+      Extract_Target_Attributes (Gen_Id, Gen_Attrs);
+
+      --  Nothing to do when the root scenario appears at the declaration level
+      --  and the generic is in the same unit, but outside this context.
+
+      --    generic
+      --    procedure Gen is ...;                --  generic declaration
+
+      --    procedure Proc is
+      --       function A ... is
+      --       begin
+      --          if Some_Condition then
+      --             declare
+      --                procedure I is new Gen;  --  instantiation site
+      --             ...
+      --          ...
+      --       end A;
+
+      --       X : ... := A;                     --  root scenario
+      --    ...
+
+      --    procedure Gen is
+      --       ...
+      --    end Gen;
+
+      --  In the example above, the context of X is the declarative region of
+      --  Proc. The "elaboration" of X may eventually reach Gen which appears
+      --  outside of X's context. Gen is relevant only when Proc is invoked,
+      --  but this happens only by means of "normal" elaboration, therefore
+      --  Gen must not be considered if this is not the case.
+
+      --  Performance note: parent traversal
+
+      if Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then
+         return;
+
+      --  Nothing to do when the instantiation is ABE-safe
+
+      --    generic
+      --    package Gen is
+      --       ...
+      --    end Gen;
+
+      --    package body Gen is
+      --       ...
+      --    end Gen;
+
+      --    with Gen;
+      --    procedure Main is
+      --       package Inst is new Gen (ABE);    --  safe instantiation
+      --    ...
+
+      elsif Is_Safe_Instantiation (Inst, Gen_Attrs) then
+         return;
+
+      --  An instantiation leads to a guaranteed ABE when the instantiation and
+      --  the generic appear within the same context ignoring library levels,
+      --  and the body of the generic has not been seen yet or appears after
+      --  the instantiation.
+
+      --    procedure Guaranteed_ABE is
+      --       generic
+      --       procedure Gen;
+
+      --       package Nested is
+      --          procedure Inst is new Gen;     --  guaranteed ABE
+      --       end Nested;
+
+      --       procedure Gen is
+      --          ...
+      --       end Gen;
+      --    ...
+
+      --  Performance note: parent traversal
+
+      elsif Is_Guaranteed_ABE
+              (N           => Inst,
+               Target_Decl => Gen_Attrs.Spec_Decl,
+               Target_Body => Gen_Attrs.Body_Decl)
+      then
+         Error_Msg_NE
+           ("??cannot instantiate & before body seen", Inst, Gen_Id);
+         Error_Msg_N ("\Program_Error will be raised at run time", Inst);
+
+         --  Mark the instantiation as a guarantee ABE. This automatically
+         --  suppresses the instantiation of the generic body.
+
+         Set_Is_Known_Guaranteed_ABE (Inst);
+
+         --  Install a run-time ABE failure because the instantiation will
+         --  always result in an ABE. The failure is installed when both the
+         --  instance and the generic have enabled elaboration checks, and both
+         --  are not ignored Ghost constructs.
+
+         if Inst_Attrs.Elab_Checks_OK
+           and then Gen_Attrs.Elab_Checks_OK
+           and then not Inst_Attrs.Ghost_Mode_Ignore
+           and then not Gen_Attrs.Ghost_Mode_Ignore
+         then
+            Install_ABE_Failure
+              (N       => Inst,
+               Ins_Nod => Exp_Inst);
+         end if;
+      end if;
+   end Process_Guaranteed_ABE_Instantiation;
+
+   ----------------------------
+   -- Process_Guaranteed_ABE --
+   ----------------------------
+
+   --  NOTE: The body of this routine is intentionally out of order because it
+   --  invokes an instantiated subprogram (Process_Guaranteed_ABE_Activation).
+   --  Placing the body in alphabetical order will result in a guaranteed ABE.
+
+   procedure Process_Guaranteed_ABE (N : Node_Id) is
+      Call_Attrs : Call_Attributes;
+      Target_Id  : Entity_Id;
+
+   begin
+      --  Add the current scenario to the stack of active scenarios
+
+      Push_Active_Scenario (N);
+
+      --  Only calls, instantiations, and task activations may result in a
+      --  guaranteed ABE.
+
+      if Is_Suitable_Call (N) then
+         Extract_Call_Attributes
+           (Call      => N,
+            Target_Id => Target_Id,
+            Attrs     => Call_Attrs);
+
+         if Is_Activation_Proc (Target_Id) then
+            Process_Guaranteed_ABE_Activation
+              (Call           => N,
+               Call_Attrs     => Call_Attrs,
+               In_Init_Cond   => False,
+               In_Partial_Fin => False,
+               In_Task_Body   => False);
+
+         else
+            Process_Guaranteed_ABE_Call
+              (Call       => N,
+               Call_Attrs => Call_Attrs,
+               Target_Id  => Target_Id);
+         end if;
+
+      elsif Is_Suitable_Instantiation (N) then
+         Process_Guaranteed_ABE_Instantiation (N);
+      end if;
+
+      --  Remove the current scenario from the stack of active scenarios once
+      --  all ABE diagnostics and checks have been performed.
+
+      Pop_Active_Scenario (N);
+   end Process_Guaranteed_ABE;
+
+   --------------------------
+   -- Push_Active_Scenario --
+   --------------------------
+
+   procedure Push_Active_Scenario (N : Node_Id) is
+   begin
+      Scenario_Stack.Append (N);
+   end Push_Active_Scenario;
 
    ---------------------------------
    -- Record_Elaboration_Scenario --
@@ -8370,14 +10329,24 @@ package body Sem_Elab is
    procedure Record_Elaboration_Scenario (N : Node_Id) is
       Level : Enclosing_Level_Kind;
 
+      Any_Level_OK : Boolean;
+      --  This flag is set when a particular scenario is allowed to appear at
+      --  any level.
+
       Declaration_Level_OK : Boolean;
       --  This flag is set when a particular scenario is allowed to appear at
       --  the declaration level.
 
+      Library_Level_OK : Boolean;
+      --  This flag is set when a particular scenario is allowed to appear at
+      --  the library level.
+
    begin
-      --  Assume that the scenario must not appear at the declaration level
+      --  Assume that the scenario cannot appear on any level
 
+      Any_Level_OK         := False;
       Declaration_Level_OK := False;
+      Library_Level_OK     := False;
 
       --  Nothing to do for ASIS. As a result, no ABE checks and diagnostics
       --  are performed in this mode.
@@ -8417,10 +10386,13 @@ package body Sem_Elab is
       --   'Access for entries, operators, and subprograms
       --    Assignments to variables
       --    Calls (includes task activation)
+      --    Derived types
       --    Instantiations
+      --    Pragma Refined_State
       --    Reads of variables
 
       elsif Is_Suitable_Access (N) then
+         Library_Level_OK := True;
 
          --  Signal any enclosing local exception handlers that the 'Access may
          --  raise Program_Error due to a failed ABE check when switch -gnatd.o
@@ -8435,6 +10407,7 @@ package body Sem_Elab is
 
       elsif Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N) then
          Declaration_Level_OK := True;
+         Library_Level_OK     := True;
 
          --  Signal any enclosing local exception handlers that the call or
          --  instantiation may raise Program_Error due to a failed ABE check.
@@ -8444,10 +10417,16 @@ package body Sem_Elab is
 
          Possible_Local_Raise (N, Standard_Program_Error);
 
+      elsif Is_Suitable_SPARK_Derived_Type (N) then
+         Any_Level_OK := True;
+
+      elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+         Library_Level_OK := True;
+
       elsif Is_Suitable_Variable_Assignment (N)
         or else Is_Suitable_Variable_Reference (N)
       then
-         null;
+         Library_Level_OK := True;
 
       --  Otherwise the input does not denote a suitable scenario
 
@@ -8461,33 +10440,78 @@ package body Sem_Elab is
 
       if Static_Elaboration_Checks then
 
-         --  Performance note: parent traversal
+         --  Certain scenarios are allowed to appear at any level. This check
+         --  is performed here in order to save on a parent traversal.
 
-         Level := Find_Enclosing_Level (N);
+         if Any_Level_OK then
+            null;
 
-         --  Declaration-level scenario
+         --  Otherwise the scenario must appear at a specific level
 
-         if Declaration_Level_OK and then Level = Declaration_Level then
-            null;
+         else
+            --  Performance note: parent traversal
 
-         --  Library-level scenario
+            Level := Find_Enclosing_Level (N);
 
-         elsif Level in Library_Level then
-            null;
+            --  Declaration-level scenario
 
-         --  Instantiation library-level scenario
+            if Declaration_Level_OK and then Level = Declaration_Level then
+               null;
 
-         elsif Level = Instantiation then
-            null;
+            --  Library-level scenario
 
-         --  Otherwise the scenario does not appear at the proper level and
-         --  cannot possibly act as a top-level scenario.
+            elsif Library_Level_OK
+              and then Level in Library_Or_Instantiation_Level
+            then
+               null;
 
-         else
-            return;
+            --  Otherwise the scenario does not appear at the proper level and
+            --  cannot possibly act as a top-level scenario.
+
+            else
+               return;
+            end if;
          end if;
       end if;
 
+      --  Derived types subject to SPARK_Mode On require elaboration-related
+      --  checks even though the type may not be declared within elaboration
+      --  code. The types are recorded in a separate table which is examined
+      --  during the Processing phase. Note that the checks must be delayed
+      --  because the bodies of overriding primitives are not available yet.
+
+      if Is_Suitable_SPARK_Derived_Type (N) then
+         Record_SPARK_Elaboration_Scenario (N);
+
+         --  Nothing left to do for derived types
+
+         return;
+
+      --  Instantiations of generics both subject to SPARK_Mode On require
+      --  elaboration-related checks even though the instantiations may not
+      --  appear within elaboration code. The instantiations are recored in
+      --  a separate table which is examined during the Procesing phase. Note
+      --  that the checks must be delayed because it is not known yet whether
+      --  the generic unit has a body or not.
+
+      --  IMPORTANT: A SPARK instantiation is also a normal instantiation which
+      --  is subject to common conditional and guaranteed ABE checks.
+
+      elsif Is_Suitable_SPARK_Instantiation (N) then
+         Record_SPARK_Elaboration_Scenario (N);
+
+      --  External constituents that refine abstract states which appear in
+      --  pragma Initializes require elaboration-related checks even though
+      --  a Refined_State pragma lacks any elaboration semantic.
+
+      elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+         Record_SPARK_Elaboration_Scenario (N);
+
+         --  Nothing left to do for pragma Refined_State
+
+         return;
+      end if;
+
       --  Perform early detection of guaranteed ABEs in order to suppress the
       --  instantiation of generic bodies as gigi cannot handle certain types
       --  of premature instantiations.
@@ -8502,6 +10526,28 @@ package body Sem_Elab is
    end Record_Elaboration_Scenario;
 
    ---------------------------------------
+   -- Record_SPARK_Elaboration_Scenario --
+   ---------------------------------------
+
+   procedure Record_SPARK_Elaboration_Scenario (N : Node_Id) is
+   begin
+      SPARK_Scenarios.Append (N);
+      Set_Is_Recorded_SPARK_Scenario (N);
+   end Record_SPARK_Elaboration_Scenario;
+
+   -----------------------------------
+   -- Recorded_SPARK_Scenarios_Hash --
+   -----------------------------------
+
+   function Recorded_SPARK_Scenarios_Hash
+     (Key : Node_Id) return Recorded_SPARK_Scenarios_Index
+   is
+   begin
+      return
+        Recorded_SPARK_Scenarios_Index (Key mod Recorded_SPARK_Scenarios_Max);
+   end Recorded_SPARK_Scenarios_Hash;
+
+   ---------------------------------------
    -- Recorded_Top_Level_Scenarios_Hash --
    ---------------------------------------
 
@@ -8514,6 +10560,18 @@ package body Sem_Elab is
           (Key mod Recorded_Top_Level_Scenarios_Max);
    end Recorded_Top_Level_Scenarios_Hash;
 
+   --------------------------
+   -- Reset_Visited_Bodies --
+   --------------------------
+
+   procedure Reset_Visited_Bodies is
+   begin
+      if Visited_Bodies_In_Use then
+         Visited_Bodies_In_Use := False;
+         Visited_Bodies.Reset;
+      end if;
+   end Reset_Visited_Bodies;
+
    -------------------
    -- Root_Scenario --
    -------------------
@@ -8529,6 +10587,48 @@ package body Sem_Elab is
       return Stack.Table (Stack.First);
    end Root_Scenario;
 
+   ---------------------------
+   -- Set_Early_Call_Region --
+   ---------------------------
+
+   procedure Set_Early_Call_Region (Body_Id : Entity_Id; Start : Node_Id) is
+   begin
+      pragma Assert (Ekind_In (Body_Id, E_Entry,
+                                        E_Entry_Family,
+                                        E_Function,
+                                        E_Procedure,
+                                        E_Subprogram_Body));
+
+      Early_Call_Regions_In_Use := True;
+      Early_Call_Regions.Set (Body_Id, Start);
+   end Set_Early_Call_Region;
+
+   ----------------------------
+   -- Set_Elaboration_Status --
+   ----------------------------
+
+   procedure Set_Elaboration_Status
+     (Unit_Id : Entity_Id;
+      Val     : Elaboration_Attributes)
+   is
+   begin
+      Elaboration_Statuses_In_Use := True;
+      Elaboration_Statuses.Set (Unit_Id, Val);
+   end Set_Elaboration_Status;
+
+   ------------------------------------
+   -- Set_Is_Recorded_SPARK_Scenario --
+   ------------------------------------
+
+   procedure Set_Is_Recorded_SPARK_Scenario
+     (N   : Node_Id;
+      Val : Boolean := True)
+   is
+   begin
+      Recorded_SPARK_Scenarios_In_Use := True;
+      Recorded_SPARK_Scenarios.Set (N, Val);
+   end Set_Is_Recorded_SPARK_Scenario;
+
    ----------------------------------------
    -- Set_Is_Recorded_Top_Level_Scenario --
    ----------------------------------------
@@ -8538,9 +10638,20 @@ package body Sem_Elab is
       Val : Boolean := True)
    is
    begin
+      Recorded_Top_Level_Scenarios_In_Use := True;
       Recorded_Top_Level_Scenarios.Set (N, Val);
    end Set_Is_Recorded_Top_Level_Scenario;
 
+   -------------------------
+   -- Set_Is_Visited_Body --
+   -------------------------
+
+   procedure Set_Is_Visited_Body (Subp_Body : Node_Id) is
+   begin
+      Visited_Bodies_In_Use := True;
+      Visited_Bodies.Set (Subp_Body, True);
+   end Set_Is_Visited_Body;
+
    -------------------------------
    -- Static_Elaboration_Checks --
    -------------------------------
@@ -8556,6 +10667,7 @@ package body Sem_Elab is
 
    procedure Traverse_Body
      (N              : Node_Id;
+      In_Init_Cond   : Boolean;
       In_Partial_Fin : Boolean;
       In_Task_Body   : Boolean)
    is
@@ -8567,7 +10679,7 @@ package body Sem_Elab is
 
       procedure Process_Nested_Scenarios (Nested : Elist_Id);
       pragma Inline (Process_Nested_Scenarios);
-      --  Invoke Process_Scenario on each individual scenario whith appears in
+      --  Invoke Process_Conditional_ABE on each individual scenario found in
       --  list Nested.
 
       ---------------------------------------
@@ -8651,7 +10763,12 @@ package body Sem_Elab is
 
             elsif Is_Suitable_Scenario (Nod) then
                Save_Scenario (Nod);
-               Process_Scenario (Nod, In_Partial_Fin, In_Task_Body);
+
+               Process_Conditional_ABE
+                 (N              => Nod,
+                  In_Init_Cond   => In_Init_Cond,
+                  In_Partial_Fin => In_Partial_Fin,
+                  In_Task_Body   => In_Task_Body);
             end if;
 
             return OK;
@@ -8713,8 +10830,9 @@ package body Sem_Elab is
       begin
          Nested_Elmt := First_Elmt (Nested);
          while Present (Nested_Elmt) loop
-            Process_Scenario
+            Process_Conditional_ABE
               (N              => Node (Nested_Elmt),
+               In_Init_Cond   => In_Init_Cond,
                In_Partial_Fin => In_Partial_Fin,
                In_Task_Body   => In_Task_Body);
 
@@ -8741,13 +10859,13 @@ package body Sem_Elab is
       --  Nothing to do if the body was already traversed during the processing
       --  of the same top-level scenario.
 
-      if Visited_Bodies.Get (N) then
+      if Is_Visited_Body (N) then
          return;
 
       --  Otherwise mark the body as traversed
 
       else
-         Visited_Bodies.Set (N, True);
+         Set_Is_Visited_Body (N);
       end if;
 
       Nested := Nested_Scenarios (Defining_Entity (N));
@@ -8774,7 +10892,81 @@ package body Sem_Elab is
    ---------------------------------
 
    procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id) is
-      package Scenarios renames Top_Level_Scenarios;
+      procedure Update_SPARK_Scenario;
+      pragma Inline (Update_SPARK_Scenario);
+      --  Update the contents of table SPARK_Scenarios if Old_N is recorded
+      --  there.
+
+      procedure Update_Top_Level_Scenario;
+      pragma Inline (Update_Top_Level_Scenario);
+      --  Update the contexts of table Top_Level_Scenarios if Old_N is recorded
+      --  there.
+
+      ---------------------------
+      -- Update_SPARK_Scenario --
+      ---------------------------
+
+      procedure Update_SPARK_Scenario is
+         package Scenarios renames SPARK_Scenarios;
+
+      begin
+         if Is_Recorded_SPARK_Scenario (Old_N) then
+
+            --  Performance note: list traversal
+
+            for Index in Scenarios.First .. Scenarios.Last loop
+               if Scenarios.Table (Index) = Old_N then
+                  Scenarios.Table (Index) := New_N;
+
+                  --  The old SPARK scenario is no longer recorded, but the new
+                  --  one is.
+
+                  Set_Is_Recorded_Top_Level_Scenario (Old_N, False);
+                  Set_Is_Recorded_Top_Level_Scenario (New_N);
+                  return;
+               end if;
+            end loop;
+
+            --  A recorded SPARK scenario must be in the table of recorded
+            --  SPARK scenarios.
+
+            pragma Assert (False);
+         end if;
+      end Update_SPARK_Scenario;
+
+      -------------------------------
+      -- Update_Top_Level_Scenario --
+      -------------------------------
+
+      procedure Update_Top_Level_Scenario is
+         package Scenarios renames Top_Level_Scenarios;
+
+      begin
+         if Is_Recorded_Top_Level_Scenario (Old_N) then
+
+            --  Performance note: list traversal
+
+            for Index in Scenarios.First .. Scenarios.Last loop
+               if Scenarios.Table (Index) = Old_N then
+                  Scenarios.Table (Index) := New_N;
+
+                  --  The old top-level scenario is no longer recorded, but the
+                  --  new one is.
+
+                  Set_Is_Recorded_Top_Level_Scenario (Old_N, False);
+                  Set_Is_Recorded_Top_Level_Scenario (New_N);
+                  return;
+               end if;
+            end loop;
+
+            --  A recorded top-level scenario must be in the table of recorded
+            --  top-level scenarios.
+
+            pragma Assert (False);
+         end if;
+      end Update_Top_Level_Scenario;
+
+   --  Start of processing for Update_Elaboration_Requirement
 
    begin
       --  Nothing to do when the old and new scenarios are one and the same
@@ -8787,28 +10979,9 @@ package body Sem_Elab is
       --  potential run-time conditional ABE check or a guaranteed ABE failure
       --  is inserted at the proper place in the tree.
 
-      elsif Is_Scenario (Old_N)
-        and then Is_Recorded_Top_Level_Scenario (Old_N)
-      then
-         --  Performance note: list traversal
-
-         for Index in Scenarios.First .. Scenarios.Last loop
-            if Scenarios.Table (Index) = Old_N then
-               Scenarios.Table (Index) := New_N;
-
-               --  The old top-level scenario is no longer recorded, but the
-               --  new one is.
-
-               Set_Is_Recorded_Top_Level_Scenario (Old_N, False);
-               Set_Is_Recorded_Top_Level_Scenario (New_N);
-               return;
-            end if;
-         end loop;
-
-         --  A recorded top-level scenario must be in the table of recorded
-         --  top-level scenarios.
-
-         pragma Assert (False);
+      elsif Is_Scenario (Old_N) then
+         Update_SPARK_Scenario;
+         Update_Top_Level_Scenario;
       end if;
    end Update_Elaboration_Scenario;
 
diff --git a/gcc/ada/sem_elab.ads b/gcc/ada/sem_elab.ads
index 69d65d8..bfb174d 100644
--- a/gcc/ada/sem_elab.ads
+++ b/gcc/ada/sem_elab.ads
@@ -93,6 +93,10 @@ package Sem_Elab is
       --  This value is used to indicate that none of the levels above are in
       --  effect.
 
+   subtype Any_Library_Level is Enclosing_Level_Kind range
+     Generic_Package_Spec ..
+     Package_Body;
+
    subtype Generic_Library_Level is Enclosing_Level_Kind range
      Generic_Package_Spec ..
      Generic_Package_Body;
@@ -101,8 +105,8 @@ package Sem_Elab is
      Package_Spec ..
      Package_Body;
 
-   subtype Any_Library_Level is Enclosing_Level_Kind range
-     Generic_Package_Spec ..
+   subtype Library_Or_Instantiation_Level is Enclosing_Level_Kind range
+     Instantiation ..
      Package_Body;
 
    function Find_Enclosing_Level (N : Node_Id) return Enclosing_Level_Kind;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index b071aa8..219ccf5 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -64,6 +64,7 @@ with Sem_Ch12;  use Sem_Ch12;
 with Sem_Ch13;  use Sem_Ch13;
 with Sem_Disp;  use Sem_Disp;
 with Sem_Dist;  use Sem_Dist;
+with Sem_Elab;  use Sem_Elab;
 with Sem_Elim;  use Sem_Elim;
 with Sem_Eval;  use Sem_Eval;
 with Sem_Intr;  use Sem_Intr;
@@ -11563,6 +11564,11 @@ package body Sem_Prag is
                   Set_Etype               (State_Id, Standard_Void_Type);
                   Set_Encapsulating_State (State_Id, Empty);
 
+                  --  Set the SPARK mode from the current context
+
+                  Set_SPARK_Pragma           (State_Id, SPARK_Mode_Pragma);
+                  Set_SPARK_Pragma_Inherited (State_Id);
+
                   --  An abstract state declared within a Ghost region becomes
                   --  Ghost (SPARK RM 6.9(2)).
 
@@ -27756,6 +27762,10 @@ package body Sem_Prag is
          return;
       end if;
 
+      --  Save the scenario for examination by the ABE Processing phase
+
+      Record_Elaboration_Scenario (N);
+
       --  Replicate the abstract states declared by the package because the
       --  matching algorithm will consume states.
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 2050286..056703c 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -14634,6 +14634,442 @@ package body Sem_Util is
       end case;
    end Is_Name_Reference;
 
+   ------------------------------------
+   -- Is_Non_Preelaborable_Construct --
+   ------------------------------------
+
+   function Is_Non_Preelaborable_Construct (N : Node_Id) return Boolean is
+
+      --  NOTE: the routines within Is_Non_Preelaborable_Construct are
+      --  intentionally unnested to avoid deep indentation of code.
+
+      Non_Preelaborable : exception;
+      --  This exception is raised when the construct violates preelaborability
+      --  to terminate the recursion.
+
+      procedure Visit (Nod : Node_Id);
+      --  Semantically inspect construct Nod to determine whether it violates
+      --  preelaborability. This routine raises Non_Preelaborable.
+
+      procedure Visit_List (List : List_Id);
+      pragma Inline (Visit_List);
+      --  Invoke Visit on each element of list List. This routine raises
+      --  Non_Preelaborable.
+
+      procedure Visit_Pragma (Prag : Node_Id);
+      pragma Inline (Visit_Pragma);
+      --  Semantically inspect pragma Prag to determine whether it violates
+      --  preelaborability. This routine raises Non_Preelaborable.
+
+      procedure Visit_Subexpression (Expr : Node_Id);
+      pragma Inline (Visit_Subexpression);
+      --  Semantically inspect expression Expr to determine whether it violates
+      --  preelaborability. This routine raises Non_Preelaborable.
+
+      -----------
+      -- Visit --
+      -----------
+
+      procedure Visit (Nod : Node_Id) is
+      begin
+         case Nkind (Nod) is
+
+            --  Declarations
+
+            when N_Component_Declaration =>
+
+               --  Defining_Identifier is left out because it is not relevant
+               --  for preelaborability.
+
+               Visit (Component_Definition (Nod));
+               Visit (Expression (Nod));
+
+            when N_Derived_Type_Definition =>
+
+               --  Interface_List is left out because it is not relevant for
+               --  preelaborability.
+
+               Visit (Record_Extension_Part (Nod));
+               Visit (Subtype_Indication (Nod));
+
+            when N_Entry_Declaration =>
+
+               --  A protected type with at leat one entry is not preelaborable
+               --  while task types are never preelaborable. This renders entry
+               --  declarations non-preelaborable.
+
+               raise Non_Preelaborable;
+
+            when N_Full_Type_Declaration =>
+
+               --  Defining_Identifier and Discriminant_Specifications are left
+               --  out because they are not relevant for preelaborability.
+
+               Visit (Type_Definition (Nod));
+
+            when N_Function_Instantiation
+               | N_Package_Instantiation
+               | N_Procedure_Instantiation
+            =>
+               --  Defining_Unit_Name and Name are left out because they are
+               --  not relevant for preelaborability.
+
+               Visit_List (Generic_Associations (Nod));
+
+            when N_Object_Declaration =>
+
+               --  Defining_Identifier is left out because it is not relevant
+               --  for preelaborability.
+
+               Visit (Object_Definition (Nod));
+
+               if Has_Init_Expression (Nod) then
+                  Visit (Expression (Nod));
+
+               elsif not Has_Preelaborable_Initialization
+                           (Etype (Defining_Entity (Nod)))
+               then
+                  raise Non_Preelaborable;
+               end if;
+
+            when N_Private_Extension_Declaration
+               | N_Subtype_Declaration
+            =>
+               --  Defining_Identifier, Discriminant_Specifications, and
+               --  Interface_List are left out because they are not relevant
+               --  for preelaborability.
+
+               Visit (Subtype_Indication (Nod));
+
+            when N_Protected_Type_Declaration
+               | N_Single_Protected_Declaration
+            =>
+               --  Defining_Identifier, Discriminant_Specifications, and
+               --  Interface_List are left out because they are not relevant
+               --  for preelaborability.
+
+               Visit (Protected_Definition (Nod));
+
+            --  A [single] task type is never preelaborable
+
+            when N_Single_Task_Declaration
+               | N_Task_Type_Declaration
+            =>
+               raise Non_Preelaborable;
+
+            --  Pragmas
+
+            when N_Pragma =>
+               Visit_Pragma (Nod);
+
+            --  Statements
+
+            when N_Statement_Other_Than_Procedure_Call =>
+               if Nkind (Nod) /= N_Null_Statement then
+                  raise Non_Preelaborable;
+               end if;
+
+            --  Subexpressions
+
+            when N_Subexpr =>
+               Visit_Subexpression (Nod);
+
+            --  Special
+
+            when N_Access_To_Object_Definition =>
+               Visit (Subtype_Indication (Nod));
+
+            when N_Case_Expression_Alternative =>
+               Visit (Expression (Nod));
+               Visit_List (Discrete_Choices (Nod));
+
+            when N_Component_Definition =>
+               Visit (Access_Definition (Nod));
+               Visit (Subtype_Indication (Nod));
+
+            when N_Component_List =>
+               Visit_List (Component_Items (Nod));
+               Visit (Variant_Part (Nod));
+
+            when N_Constrained_Array_Definition =>
+               Visit_List (Discrete_Subtype_Definitions (Nod));
+               Visit (Component_Definition (Nod));
+
+            when N_Delta_Constraint
+               | N_Digits_Constraint
+            =>
+               --  Delta_Expression and Digits_Expression are left out because
+               --  they are not relevant for preelaborability.
+
+               Visit (Range_Constraint (Nod));
+
+            when N_Discriminant_Specification =>
+
+               --  Defining_Identifier and Expression are left out because they
+               --  are not relevant for preelaborability.
+
+               Visit (Discriminant_Type (Nod));
+
+            when N_Generic_Association =>
+
+               --  Selector_Name is left out because it is not relevant for
+               --  preelaborability.
+
+               Visit (Explicit_Generic_Actual_Parameter (Nod));
+
+            when N_Index_Or_Discriminant_Constraint =>
+               Visit_List (Constraints (Nod));
+
+            when N_Iterator_Specification =>
+
+               --  Defining_Identifier is left out because it is not relevant
+               --  for preelaborability.
+
+               Visit (Name (Nod));
+               Visit (Subtype_Indication (Nod));
+
+            when N_Loop_Parameter_Specification =>
+
+               --  Defining_Identifier is left out because it is not relevant
+               --  for preelaborability.
+
+               Visit (Discrete_Subtype_Definition (Nod));
+
+            when N_Protected_Definition =>
+
+               --  End_Label is left out because it is not relevant for
+               --  preelaborability.
+
+               Visit_List (Private_Declarations (Nod));
+               Visit_List (Visible_Declarations (Nod));
+
+            when N_Range_Constraint =>
+               Visit (Range_Expression (Nod));
+
+            when N_Record_Definition
+               | N_Variant
+            =>
+               --  End_Label, Discrete_Choices, and Interface_List are left out
+               --  because they are not relevant for preelaborability.
+
+               Visit (Component_List (Nod));
+
+            when N_Subtype_Indication =>
+
+               --  Subtype_Mark is left out because it is not relevant for
+               --  preelaborability.
+
+               Visit (Constraint (Nod));
+
+            when N_Unconstrained_Array_Definition =>
+
+               --  Subtype_Marks is left out because it is not relevant for
+               --  preelaborability.
+
+               Visit (Component_Definition (Nod));
+
+            when N_Variant_Part =>
+
+               --  Name is left out because it is not relevant for
+               --  preelaborability.
+
+               Visit_List (Variants (Nod));
+
+            --  Default
+
+            when others =>
+               null;
+         end case;
+      end Visit;
+
+      ----------------
+      -- Visit_List --
+      ----------------
+
+      procedure Visit_List (List : List_Id) is
+         Nod : Node_Id;
+
+      begin
+         if Present (List) then
+            Nod := First (List);
+            while Present (Nod) loop
+               Visit (Nod);
+               Next (Nod);
+            end loop;
+         end if;
+      end Visit_List;
+
+      ------------------
+      -- Visit_Pragma --
+      ------------------
+
+      procedure Visit_Pragma (Prag : Node_Id) is
+      begin
+         case Get_Pragma_Id (Prag) is
+            when Pragma_Assert
+               | Pragma_Assert_And_Cut
+               | Pragma_Assume
+               | Pragma_Async_Readers
+               | Pragma_Async_Writers
+               | Pragma_Attribute_Definition
+               | Pragma_Check
+               | Pragma_Constant_After_Elaboration
+               | Pragma_CPU
+               | Pragma_Deadline_Floor
+               | Pragma_Dispatching_Domain
+               | Pragma_Effective_Reads
+               | Pragma_Effective_Writes
+               | Pragma_Extensions_Visible
+               | Pragma_Ghost
+               | Pragma_Secondary_Stack_Size
+               | Pragma_Task_Name
+               | Pragma_Volatile_Function
+            =>
+               Visit_List (Pragma_Argument_Associations (Prag));
+
+            --  Default
+
+            when others =>
+               null;
+         end case;
+      end Visit_Pragma;
+
+      -------------------------
+      -- Visit_Subexpression --
+      -------------------------
+
+      procedure Visit_Subexpression (Expr : Node_Id) is
+         procedure Visit_Aggregate (Aggr : Node_Id);
+         pragma Inline (Visit_Aggregate);
+         --  Semantically inspect aggregate Aggr to determine whether it
+         --  violates preelaborability.
+
+         ---------------------
+         -- Visit_Aggregate --
+         ---------------------
+
+         procedure Visit_Aggregate (Aggr : Node_Id) is
+         begin
+            if not Is_Preelaborable_Aggregate (Aggr) then
+               raise Non_Preelaborable;
+            end if;
+         end Visit_Aggregate;
+
+      --  Start of processing for Visit_Subexpression
+
+      begin
+         case Nkind (Expr) is
+            when N_Allocator
+               | N_Qualified_Expression
+               | N_Type_Conversion
+               | N_Unchecked_Expression
+               | N_Unchecked_Type_Conversion
+            =>
+               --  Subpool_Handle_Name and Subtype_Mark are left out because
+               --  they are not relevant for preelaborability.
+
+               Visit (Expression (Expr));
+
+            when N_Aggregate
+               | N_Extension_Aggregate
+            =>
+               Visit_Aggregate (Expr);
+
+            when N_Attribute_Reference
+               | N_Explicit_Dereference
+               | N_Reference
+            =>
+               --  Attribute_Name and Expressions are left out because they are
+               --  not relevant for preelaborability.
+
+               Visit (Prefix (Expr));
+
+            when N_Case_Expression =>
+
+               --  End_Span is left out because it is not relevant for
+               --  preelaborability.
+
+               Visit_List (Alternatives (Expr));
+               Visit (Expression (Expr));
+
+            when N_Delta_Aggregate =>
+               Visit_Aggregate (Expr);
+               Visit (Expression (Expr));
+
+            when N_Expression_With_Actions =>
+               Visit_List (Actions (Expr));
+               Visit (Expression (Expr));
+
+            when N_If_Expression =>
+               Visit_List (Expressions (Expr));
+
+            when N_Quantified_Expression =>
+               Visit (Condition (Expr));
+               Visit (Iterator_Specification (Expr));
+               Visit (Loop_Parameter_Specification (Expr));
+
+            when N_Range =>
+               Visit (High_Bound (Expr));
+               Visit (Low_Bound (Expr));
+
+            when N_Slice =>
+               Visit (Discrete_Range (Expr));
+               Visit (Prefix (Expr));
+
+            --  Default
+
+            when others =>
+
+               --  The evaluation of an object name is not preelaborable,
+               --  unless the name is a static expression (checked further
+               --  below), or statically denotes a discriminant.
+
+               if Is_Entity_Name (Expr) then
+                  Object_Name : declare
+                     Id : constant Entity_Id := Entity (Expr);
+
+                  begin
+                     if Is_Object (Id) then
+                        if Ekind (Id) = E_Discriminant then
+                           null;
+
+                        elsif Ekind_In (Id, E_Constant, E_In_Parameter)
+                          and then Present (Discriminal_Link (Id))
+                        then
+                           null;
+
+                        else
+                           raise Non_Preelaborable;
+                        end if;
+                     end if;
+                  end Object_Name;
+
+               --  A non-static expression is not preelaborable
+
+               elsif not Is_OK_Static_Expression (Expr) then
+                  raise Non_Preelaborable;
+               end if;
+         end case;
+      end Visit_Subexpression;
+
+   --  Start of processing for Is_Non_Preelaborable_Construct
+
+   begin
+      Visit (N);
+
+      --  At this point it is known that the construct is preelaborable
+
+      return False;
+
+   exception
+
+      --  The elaboration of the construct performs an action which violates
+      --  preelaborability.
+
+      when Non_Preelaborable =>
+         return True;
+   end Is_Non_Preelaborable_Construct;
+
    ---------------------------------
    -- Is_Nontrivial_DIC_Procedure --
    ---------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 4c2cec5..76fc6af 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1730,6 +1730,11 @@ package Sem_Util is
    --  without the need for a temporary, the typical example of an object not
    --  in this category being a function call.
 
+   function Is_Non_Preelaborable_Construct (N : Node_Id) return Boolean;
+   --  Determine whether arbitrary construct N violates preelaborability as
+   --  defined in ARM 10.2.1 5-9/3. This routine takes into account both the
+   --  syntactic and semantic properties of the construct.
+
    function Is_Nontrivial_DIC_Procedure (Id : Entity_Id) return Boolean;
    --  Determine whether entity Id denotes the procedure that verifies the
    --  assertion expression of pragma Default_Initial_Condition and if it does,
@@ -1807,7 +1812,9 @@ package Sem_Util is
 
    function Is_Preelaborable_Construct (N : Node_Id) return Boolean;
    --  Determine whether arbitrary node N violates the restrictions of
-   --  preelaborable constructs as defined in ARM 10.2.1(5-9).
+   --  preelaborable constructs as defined in ARM 10.2.1(5-9). Routine
+   --  Is_Non_Preelaborable_Construct takes into account the syntactic
+   --  and semantic properties of N for a more accurate diagnostic.
 
    function Is_Protected_Self_Reference (N : Node_Id) return Boolean;
    --  Return True if node N denotes a protected type name which represents
diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb
index 20ff3b2..06f62c5 100644
--- a/gcc/ada/sinfo.adb
+++ b/gcc/ada/sinfo.adb
@@ -1925,6 +1925,14 @@ package body Sinfo is
       return Flag1 (N);
    end Is_Elaboration_Checks_OK_Node;
 
+   function Is_Elaboration_Code
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Assignment_Statement);
+      return Flag9 (N);
+   end Is_Elaboration_Code;
+
    function Is_Elsif
       (N : Node_Id) return Boolean is
    begin
@@ -5353,6 +5361,14 @@ package body Sinfo is
       Set_Flag1 (N, Val);
    end Set_Is_Elaboration_Checks_OK_Node;
 
+   procedure Set_Is_Elaboration_Code
+      (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Assignment_Statement);
+      Set_Flag9 (N, Val);
+   end Set_Is_Elaboration_Code;
+
    procedure Set_Is_Elsif
       (N : Node_Id; Val : Boolean := True) is
    begin
@@ -7123,6 +7139,60 @@ package body Sinfo is
              T = V9;
    end Nkind_In;
 
+   function Nkind_In
+     (T   : Node_Kind;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind) return Boolean
+   is
+   begin
+      return T = V1 or else
+             T = V2 or else
+             T = V3 or else
+             T = V4 or else
+             T = V5 or else
+             T = V6 or else
+             T = V7 or else
+             T = V8 or else
+             T = V9 or else
+             T = V10;
+   end Nkind_In;
+
+   function Nkind_In
+     (T   : Node_Kind;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind;
+      V11 : Node_Kind) return Boolean
+   is
+   begin
+      return T = V1  or else
+             T = V2  or else
+             T = V3  or else
+             T = V4  or else
+             T = V5  or else
+             T = V6  or else
+             T = V7  or else
+             T = V8  or else
+             T = V9  or else
+             T = V10 or else
+             T = V11;
+   end Nkind_In;
+
    -----------------
    -- Pragma_Name --
    -----------------
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index f9f84ac..f14d2d1 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -1732,6 +1732,11 @@ package Sinfo is
    --    run-time ABE checks. This flag detemines whether the ABE Processing
    --    phase generates conditional ABE checks and guaranteed ABE failures.
 
+   --  Is_Elaboration_Code (Flag9-Sem)
+   --    Present in assignment statements. Set for an assignment which updates
+   --    the elaboration flag of a package or subprogram when the corresponding
+   --    body is successfully elaborated.
+
    --  Is_Entry_Barrier_Function (Flag8-Sem)
    --    This flag is set on N_Subprogram_Declaration and N_Subprogram_Body
    --    nodes which emulate the barrier function of a protected entry body.
@@ -4900,6 +4905,7 @@ package Sinfo is
       --  Backwards_OK (Flag6-Sem)
       --  No_Ctrl_Actions (Flag7-Sem)
       --  Has_Target_Names (Flag8-Sem)
+      --  Is_Elaboration_Code (Flag9-Sem)
       --  Do_Tag_Check (Flag13-Sem)
       --  Componentwise_Assignment (Flag14-Sem)
       --  Suppress_Assignment_Checks (Flag18-Sem)
@@ -9704,6 +9710,9 @@ package Sinfo is
    function Is_Elaboration_Checks_OK_Node
      (N : Node_Id) return Boolean;    -- Flag1
 
+   function Is_Elaboration_Code
+     (N : Node_Id) return Boolean;    -- Flag9
+
    function Is_Elsif
      (N : Node_Id) return Boolean;    -- Flag13
 
@@ -10796,6 +10805,9 @@ package Sinfo is
    procedure Set_Is_Elaboration_Checks_OK_Node
      (N : Node_Id; Val : Boolean := True);    -- Flag1
 
+   procedure Set_Is_Elaboration_Code
+     (N : Node_Id; Val : Boolean := True);    -- Flag9
+
    procedure Set_Is_Elsif
      (N : Node_Id; Val : Boolean := True);    -- Flag13
 
@@ -11400,6 +11412,33 @@ package Sinfo is
       V8 : Node_Kind;
       V9 : Node_Kind) return Boolean;
 
+   function Nkind_In
+     (T   : Node_Kind;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind) return Boolean;
+
+   function Nkind_In
+     (T   : Node_Kind;
+      V1  : Node_Kind;
+      V2  : Node_Kind;
+      V3  : Node_Kind;
+      V4  : Node_Kind;
+      V5  : Node_Kind;
+      V6  : Node_Kind;
+      V7  : Node_Kind;
+      V8  : Node_Kind;
+      V9  : Node_Kind;
+      V10 : Node_Kind;
+      V11 : Node_Kind) return Boolean;
+
    pragma Inline (Nkind_In);
    --  Inline all above functions
 
@@ -11792,7 +11831,7 @@ package Sinfo is
         5 => False),  --  unused
 
      N_Delta_Aggregate =>
-       (1 => False,   --  Expressions (List1)
+       (1 => False,   --  Expressions (List1-Sem)
         2 => True,    --  Component_Associations (List2)
         3 => True,    --  Expression (Node3)
         4 => False,   --  Unused
@@ -12003,7 +12042,7 @@ package Sinfo is
 
      N_Quantified_Expression =>
        (1 => True,    --  Condition (Node1)
-        2 => True,    --  Iterator_Specification
+        2 => True,    --  Iterator_Specification (Node2)
         3 => False,   --  unused
         4 => True,    --  Loop_Parameter_Specification (Node4)
         5 => False),  --  Etype (Node5-Sem)
@@ -13300,6 +13339,7 @@ package Sinfo is
    pragma Inline (Is_Dynamic_Coextension);
    pragma Inline (Is_Effective_Use_Clause);
    pragma Inline (Is_Elaboration_Checks_OK_Node);
+   pragma Inline (Is_Elaboration_Code);
    pragma Inline (Is_Elsif);
    pragma Inline (Is_Entry_Barrier_Function);
    pragma Inline (Is_Expanded_Build_In_Place_Call);
@@ -13659,6 +13699,7 @@ package Sinfo is
    pragma Inline (Set_Is_Dynamic_Coextension);
    pragma Inline (Set_Is_Effective_Use_Clause);
    pragma Inline (Set_Is_Elaboration_Checks_OK_Node);
+   pragma Inline (Set_Is_Elaboration_Code);
    pragma Inline (Set_Is_Elsif);
    pragma Inline (Set_Is_Entry_Barrier_Function);
    pragma Inline (Set_Is_Expanded_Build_In_Place_Call);