2017-10-14 Ed Schonberg <schonberg@adacore.com>

	* doc/gnat_rm/implementation_defined_aspects.rst: Add documentation
	for reverse iteration over formal containers.
	* gnat_rm.texi: Regenerate.

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

	* sem_elab.adb (Ensure_Dynamic_Prior_Elaboration): Renamed to
	Ensure_Prior_Elaboration_Dynamic for consistency reasons.
	(Ensure_Static_Prior_Elaboration): Renamed to
	Ensure_Prior_Elaboration_Static for consistency reasons.
	(Info_Variable_Reference): Renamed to Info_Variable_Read in order to
	reflect its new purpose.
	(Is_Initialized): New routine.
	(Is_Suitable_Variable_Reference): Renamed to Is_Suitable_Variable_Read
	in order to reflect its new purpose.
	(Is_Variable_Read): New routine.
	(Output_Variable_Reference): Renamed to Output_Variable_Read in order
	to reflect its new purpose.
	(Process_Variable_Assignment): This routine now acts as a top level
	dispatcher for variable assignments.
	(Process_Variable_Assignment_Ada): New routine.
	(Process_Variable_Assignment_SPARK): New routine.
	(Process_Variable_Reference): Renamed to Process_Variable_Read in order
	to reflects its new purpose. A reference to a variable is now suitable
	for ABE processing only when it is a read. The logic in the routine now
	reflects the latest SPARK elaboration rules.

2017-10-14  Justin Squirek  <squirek@adacore.com>

	* sem_ch8.adb (Analyze_Subprogram_Renaming): Modify condition that
	triggers marking on formal subprograms.

2017-10-14  Javier Miranda  <miranda@adacore.com>

	* checks.adb (Ensure_Valid): Do not skip adding the validity check on
	renamings of objects that come from the sources.

2017-10-14  Eric Botcazou  <ebotcazou@adacore.com>

	* cstand.adb (Build_Float_Type): Move down Siz parameter, add Align
	parameter and set the alignment of the type to Align.
	(Copy_Float_Type): Adjust call to Build_Float_Type.
	(Register_Float_Type): Add pragma Unreferenced for Precision.  Adjust
	call to Build_Float_Type and do not set RM_Size and Alignment.



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

7 files changed, 516 insertions, 241 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 020e8779589..5ffb2e428cd 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,50 @@
+2017-10-14  Ed Schonberg  <schonberg@adacore.com>
+
+	* doc/gnat_rm/implementation_defined_aspects.rst: Add documentation
+	for reverse iteration over formal containers.
+	* gnat_rm.texi: Regenerate.
+
+2017-10-14  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_elab.adb (Ensure_Dynamic_Prior_Elaboration): Renamed to
+	Ensure_Prior_Elaboration_Dynamic for consistency reasons.
+	(Ensure_Static_Prior_Elaboration): Renamed to
+	Ensure_Prior_Elaboration_Static for consistency reasons.
+	(Info_Variable_Reference): Renamed to Info_Variable_Read in order to
+	reflect its new purpose.
+	(Is_Initialized): New routine.
+	(Is_Suitable_Variable_Reference): Renamed to Is_Suitable_Variable_Read
+	in order to reflect its new purpose.
+	(Is_Variable_Read): New routine.
+	(Output_Variable_Reference): Renamed to Output_Variable_Read in order
+	to reflect its new purpose.
+	(Process_Variable_Assignment): This routine now acts as a top level
+	dispatcher for variable assignments.
+	(Process_Variable_Assignment_Ada): New routine.
+	(Process_Variable_Assignment_SPARK): New routine.
+	(Process_Variable_Reference): Renamed to Process_Variable_Read in order
+	to reflects its new purpose. A reference to a variable is now suitable
+	for ABE processing only when it is a read. The logic in the routine now
+	reflects the latest SPARK elaboration rules.
+
+2017-10-14  Justin Squirek  <squirek@adacore.com>
+
+	* sem_ch8.adb (Analyze_Subprogram_Renaming): Modify condition that
+	triggers marking on formal subprograms.
+
+2017-10-14  Javier Miranda  <miranda@adacore.com>
+
+	* checks.adb (Ensure_Valid): Do not skip adding the validity check on
+	renamings of objects that come from the sources.
+
+2017-10-14  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* cstand.adb (Build_Float_Type): Move down Siz parameter, add Align
+	parameter and set the alignment of the type to Align.
+	(Copy_Float_Type): Adjust call to Build_Float_Type.
+	(Register_Float_Type): Add pragma Unreferenced for Precision.  Adjust
+	call to Build_Float_Type and do not set RM_Size and Alignment.
+
 2017-10-14  Patrick Bernardi  <bernardi@adacore.com>
 
 	* Makefile.rtl (GNATRTL_NONTASKING_OBJ): Add s-soliin to
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index a99da08c733..b2c26ca4981 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -5940,6 +5940,10 @@ package body Checks is
       --  In addition, we force a check if Force_Validity_Checks is set
 
       elsif not Comes_From_Source (Expr)
+        and then not
+          (Nkind (Expr) = N_Identifier
+            and then Present (Renamed_Object (Entity (Expr)))
+            and then Comes_From_Source (Renamed_Object (Entity (Expr))))
         and then not Force_Validity_Checks
         and then (Nkind (Expr) /= N_Unchecked_Type_Conversion
                     or else Kill_Range_Check (Expr))
diff --git a/gcc/ada/cstand.adb b/gcc/ada/cstand.adb
index fe480beb426..34617bbe3cc 100644
--- a/gcc/ada/cstand.adb
+++ b/gcc/ada/cstand.adb
@@ -62,15 +62,22 @@ package body CStand is
    -----------------------
 
    procedure Build_Float_Type
-     (E    : Entity_Id;
-      Siz  : Int;
-      Rep  : Float_Rep_Kind;
-      Digs : Int);
+     (E     : Entity_Id;
+      Digs  : Int;
+      Rep   : Float_Rep_Kind;
+      Siz   : Int;
+      Align : Int);
    --  Procedure to build standard predefined float base type. The first
-   --  parameter is the entity for the type, and the second parameter is the
-   --  size in bits. The third parameter indicates the kind of representation
-   --  to be used. The fourth parameter is the digits value. Each type
+   --  parameter is the entity for the type. The second parameter is the
+   --  digits value. The third parameter indicates the representation to
+   --  be used for the type. The fourth parameter is the size in bits.
+   --  The fifth parameter is the alignment in storage units. Each type
    --  is added to the list of predefined floating point types.
+   --
+   --  Note that both RM_Size and Esize are set to the specified size, i.e.
+   --  we do not set the RM_Size to the precision passed by the back end.
+   --  This is consistent with the semantics of 'Size specified in the RM
+   --  because we cannot pack components of the type tighter than this size.
 
    procedure Build_Signed_Integer_Type (E : Entity_Id; Siz : Nat);
    --  Procedure to build standard predefined signed integer subtype. The
@@ -189,10 +196,11 @@ package body CStand is
    ----------------------
 
    procedure Build_Float_Type
-     (E    : Entity_Id;
-      Siz  : Int;
-      Rep  : Float_Rep_Kind;
-      Digs : Int)
+     (E     : Entity_Id;
+      Digs  : Int;
+      Rep   : Float_Rep_Kind;
+      Siz   : Int;
+      Align : Int)
    is
    begin
       Set_Type_Definition (Parent (E),
@@ -201,10 +209,10 @@ package body CStand is
 
       Set_Ekind                      (E, E_Floating_Point_Type);
       Set_Etype                      (E, E);
-      Set_Float_Rep (E, Rep);
-      Init_Size                      (E, Siz);
-      Set_Elem_Alignment             (E);
       Init_Digits_Value              (E, Digs);
+      Set_Float_Rep                  (E, Rep);
+      Init_Size                      (E, Siz);
+      Set_Alignment                  (E, UI_From_Int (Align));
       Set_Float_Bounds               (E);
       Set_Is_Frozen                  (E);
       Set_Is_Public                  (E);
@@ -295,8 +303,9 @@ package body CStand is
 
    procedure Copy_Float_Type (To : Entity_Id; From : Entity_Id) is
    begin
-      Build_Float_Type (To, UI_To_Int (Esize (From)), Float_Rep (From),
-                        UI_To_Int (Digits_Value (From)));
+      Build_Float_Type
+        (To, UI_To_Int (Digits_Value (From)), Float_Rep (From),
+         UI_To_Int (Esize (From)), UI_To_Int (Alignment (From)));
    end Copy_Float_Type;
 
    ----------------------
@@ -2065,15 +2074,17 @@ package body CStand is
       Size      : Positive;
       Alignment : Natural)
    is
+      pragma Unreferenced (Precision);
+      --  See Build_Float_Type for the rationale
+
       Ent : constant Entity_Id := New_Standard_Entity;
 
    begin
       Set_Defining_Identifier (New_Node (N_Full_Type_Declaration, Stloc), Ent);
       Make_Name (Ent, Name);
       Set_Scope (Ent, Standard_Standard);
-      Build_Float_Type (Ent, Int (Size), Float_Rep, Pos (Digs));
-      Set_RM_Size (Ent, UI_From_Int (Int (Precision)));
-      Set_Alignment (Ent, UI_From_Int (Int (Alignment / 8)));
+      Build_Float_Type
+        (Ent, Pos (Digs), Float_Rep, Int (Size), Int (Alignment / 8));
 
       if No (Back_End_Float_Types) then
          Back_End_Float_Types := New_Elmt_List;
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
index be7338f7436..c6018227b06 100644
--- a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
@@ -302,11 +302,15 @@ Aspect Iterable
 This aspect provides a light-weight mechanism for loops and quantified
 expressions over container types, without the overhead imposed by the tampering
 checks of standard Ada 2012 iterators. The value of the aspect is an aggregate
-with four named components: ``First``, ``Next``, ``Has_Element``, and ``Element`` (the
-last one being optional). When only 3 components are specified, only the
-``for .. in`` form of iteration over cursors is available. When all 4 components
-are specified, both this form and the ``for .. of`` form of iteration over
-elements are available. The following is a typical example of use:
+with six named components, or which the last three are optional: ``First``,
+ ``Next``, ``Has_Element``,``Element``, ``Last``, and ``Previous``.
+When only the first three components are specified, only the
+``for .. in`` form of iteration over cursors is available. When ``Element``
+is specified, both this form and the ``for .. of`` form of iteration over
+elements are available. If the last two components are specified, reverse
+iterations over the container can be specified (analogous to what can be done
+over predefined containers that support the Reverse_Iterator interface).
+The following is a typical example of use:
 
 .. code-block:: ada
 
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 8ed58c4fc7f..b042e2be3e1 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -21,7 +21,7 @@
 
 @copying
 @quotation
-GNAT Reference Manual , Sep 29, 2017
+GNAT Reference Manual , Oct 14, 2017
 
 AdaCore
 
@@ -9413,11 +9413,20 @@ that it is separately controllable using pragma @code{Assertion_Policy}.
 This aspect provides a light-weight mechanism for loops and quantified
 expressions over container types, without the overhead imposed by the tampering
 checks of standard Ada 2012 iterators. The value of the aspect is an aggregate
-with four named components: @code{First}, @code{Next}, @code{Has_Element}, and @code{Element} (the
-last one being optional). When only 3 components are specified, only the
-@code{for .. in} form of iteration over cursors is available. When all 4 components
-are specified, both this form and the @code{for .. of} form of iteration over
-elements are available. The following is a typical example of use:
+with six named components, or which the last three are optional: @code{First},
+
+@quotation
+
+@code{Next}, @code{Has_Element},`@w{`}Element`@w{`}, @code{Last}, and @code{Previous}.
+@end quotation
+
+When only the first three components are specified, only the
+@code{for .. in} form of iteration over cursors is available. When @code{Element}
+is specified, both this form and the @code{for .. of} form of iteration over
+elements are available. If the last two components are specified, reverse
+iterations over the container can be specified (analogous to what can be done
+over predefined containers that support the Reverse_Iterator interface).
+The following is a typical example of use:
 
 @example
 type List is private with
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index aa53045498b..982b2221632 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -3644,19 +3644,16 @@ package body Sem_Ch8 is
       --  and mark any use_package_clauses that affect the visibility of the
       --  implicit generic actual.
 
-      if From_Default (N)
-        and then Is_Generic_Actual_Subprogram (New_S)
-        and then Present (Alias (New_S))
+      if Is_Generic_Actual_Subprogram (New_S)
+        and then (Is_Intrinsic_Subprogram (New_S) or else From_Default (N))
       then
-         Mark_Use_Clauses (Alias (New_S));
+         Mark_Use_Clauses (New_S);
 
-      --  Check intrinsic operators used as generic actuals since they may
-      --  make a use_type_clause effective.
+         --  Handle overloaded subprograms
 
-      elsif Is_Generic_Actual_Subprogram (New_S)
-        and then Is_Intrinsic_Subprogram (New_S)
-      then
-         Mark_Use_Clauses (New_S);
+         if Present (Alias (New_S)) then
+            Mark_Use_Clauses (Alias (New_S));
+         end if;
       end if;
    end Analyze_Subprogram_Renaming;
 
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index dafc563d56b..289e853143e 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -292,7 +292,7 @@ package body Sem_Elab is
    --  |       |                                                            |
    --  |       +--> Process_Variable_Assignment                             |
    --  |       |                                                            |
-   --  |       +--> Process_Variable_Reference                              |
+   --  |       +--> Process_Variable_Read                                   |
    --  |                                                                    |
    --  +------------------------- Processing phase -------------------------+
 
@@ -776,14 +776,6 @@ 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.
 
-   procedure Ensure_Dynamic_Prior_Elaboration
-     (N        : Node_Id;
-      Unit_Id  : Entity_Id;
-      Prag_Nam : Name_Id);
-   --  Guarantee the elaboration of unit Unit_Id with respect to the main unit
-   --  by suggesting the use of Elaborate[_All] with name Prag_Nam. N denotes
-   --  the related scenario.
-
    procedure Ensure_Prior_Elaboration
      (N            : Node_Id;
       Unit_Id      : Entity_Id;
@@ -792,7 +784,15 @@ package body Sem_Elab is
    --  N denotes the related scenario. Flag In_Task_Body should be set when the
    --  need for elaboration is initiated from a task body.
 
-   procedure Ensure_Static_Prior_Elaboration
+   procedure Ensure_Prior_Elaboration_Dynamic
+     (N        : Node_Id;
+      Unit_Id  : Entity_Id;
+      Prag_Nam : Name_Id);
+   --  Guarantee the elaboration of unit Unit_Id with respect to the main unit
+   --  by suggesting the use of Elaborate[_All] with name Prag_Nam. N denotes
+   --  the related scenario.
+
+   procedure Ensure_Prior_Elaboration_Static
      (N        : Node_Id;
       Unit_Id  : Entity_Id;
       Prag_Nam : Name_Id);
@@ -808,6 +808,7 @@ package body Sem_Elab is
      (Call      : Node_Id;
       Target_Id : out Entity_Id;
       Attrs     : out Call_Attributes);
+   pragma Inline (Extract_Call_Attributes);
    --  Obtain attributes Attrs associated with call Call. Target_Id is the
    --  entity of the call target.
 
@@ -828,6 +829,7 @@ package body Sem_Elab is
       Inst_Id  : out Entity_Id;
       Gen_Id   : out Entity_Id;
       Attrs    : out Instantiation_Attributes);
+   pragma Inline (Extract_Instantiation_Attributes);
    --  Obtain attributes Attrs associated with expanded instantiation Exp_Inst.
    --  Inst is the instantiation. Inst_Id is the entity of the instance. Gen_Id
    --  is the entity of the generic unit being instantiated.
@@ -841,13 +843,15 @@ package body Sem_Elab is
    procedure Extract_Task_Attributes
      (Typ   : Entity_Id;
       Attrs : out Task_Attributes);
+   pragma Inline (Extract_Task_Attributes);
    --  Obtain attributes Attrs associated with task type Typ
 
    procedure Extract_Variable_Reference_Attributes
      (Ref    : Node_Id;
       Var_Id : out Entity_Id;
       Attrs  : out Variable_Attributes);
-   --  Obtain attributes Attrs associated with reference Ref which mentions
+   pragma Inline (Extract_Variable_Reference_Attributes);
+   --  Obtain attributes Attrs associated with reference Ref that mentions
    --  variable Var_Id.
 
    function Find_Code_Unit (N : Node_Or_Entity_Id) return Entity_Id;
@@ -908,6 +912,7 @@ package body Sem_Elab is
    function In_External_Instance
      (N           : Node_Id;
       Target_Decl : Node_Id) return Boolean;
+   pragma Inline (In_External_Instance);
    --  Determine whether a target desctibed by its declaration Target_Decl
    --  resides in a package instance which is external to scenario N.
 
@@ -931,28 +936,30 @@ package body Sem_Elab is
       In_SPARK  : Boolean);
    --  Output information concerning call Call which invokes target Target_Id.
    --  If flag Info_Msg is set, the routine emits an information message,
-   --  otherwise it emits an error. If flag In_SPARK is set, then string " in
-   --  SPARK" is added to the end of the message.
+   --  otherwise it emits an error. If flag In_SPARK is set, then the string
+   --  " in SPARK" is added to the end of the message.
 
    procedure Info_Instantiation
      (Inst     : Node_Id;
       Gen_Id   : Entity_Id;
       Info_Msg : Boolean;
       In_SPARK : Boolean);
+   pragma Inline (Info_Instantiation);
    --  Output information concerning instantiation Inst which instantiates
    --  generic unit Gen_Id. If flag Info_Msg is set, the routine emits an
    --  information message, otherwise it emits an error. If flag In_SPARK
    --  is set, then string " in SPARK" is added to the end of the message.
 
-   procedure Info_Variable_Reference
+   procedure Info_Variable_Read
      (Ref      : Node_Id;
       Var_Id   : Entity_Id;
       Info_Msg : Boolean;
       In_SPARK : Boolean);
-   --  Output information concerning reference Ref which mentions variable
-   --  Var_Id. If flag Info_Msg is set, the routine emits an information
-   --  message, otherwise it emits an error. If flag In_SPARK is set, then
-   --  string " in SPARK" is added to the end of the message.
+   pragma Inline (Info_Variable_Read);
+   --  Output information concerning reference Ref which reads variable Var_Id.
+   --  If flag Info_Msg is set, the routine emits an information 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 Insertion_Node (N : Node_Id; Ins_Nod : Node_Id) return Node_Id;
    pragma Inline (Insertion_Node);
@@ -1026,6 +1033,7 @@ package body Sem_Elab is
      (N           : Node_Id;
       Target_Decl : Node_Id;
       Target_Body : Node_Id) return Boolean;
+   pragma Inline (Is_Guaranteed_ABE);
    --  Determine whether scenario N with a target described by its initial
    --  declaration Target_Decl and body Target_Decl results in a guaranteed
    --  ABE.
@@ -1035,6 +1043,10 @@ package body Sem_Elab is
    --  Determine whether arbitrary entity Id denotes internally generated
    --  routine Initial_Condition.
 
+   function Is_Initialized (Obj_Decl : Node_Id) return Boolean;
+   pragma Inline (Is_Initialized);
+   --  Determine whether object declaration Obj_Decl is initialized
+
    function Is_Invariant_Proc (Id : Entity_Id) return Boolean;
    pragma Inline (Is_Invariant_Proc);
    --  Determine whether arbitrary entity Id denotes an invariant procedure
@@ -1139,10 +1151,10 @@ package body Sem_Elab is
    --  Determine whether arbitrary node N denotes a suitable assignment for ABE
    --  processing.
 
-   function Is_Suitable_Variable_Reference (N : Node_Id) return Boolean;
-   pragma Inline (Is_Suitable_Variable_Reference);
-   --  Determine whether arbitrary node N is a suitable reference to a variable
-   --  for ABE processing.
+   function Is_Suitable_Variable_Read (N : Node_Id) return Boolean;
+   pragma Inline (Is_Suitable_Variable_Read);
+   --  Determine whether arbitrary node N is a suitable variable read for ABE
+   --  processing.
 
    function Is_Task_Entry (Id : Entity_Id) return Boolean;
    pragma Inline (Is_Task_Entry);
@@ -1234,7 +1246,7 @@ package body Sem_Elab is
       Call_Attrs   : Call_Attributes;
       Target_Id    : Entity_Id;
       In_Task_Body : Boolean);
-   --  Top level dispatcher for processing of calls. Perform ABE checks and
+   --  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_Task_Body should be set when
    --  the processing is initiated from a task body.
@@ -1334,10 +1346,24 @@ package body Sem_Elab is
    --  should be set when the processing is initiated from a task body.
 
    procedure Process_Variable_Assignment (Asmt : Node_Id);
-   --  Perform ABE checks and diagnostics for assignment statement Asmt
-
-   procedure Process_Variable_Reference (Ref : Node_Id);
-   --  Perform ABE checks and diagnostics for variable reference Ref
+   --  Top level dispatcher for processing of variable assignments. Perform ABE
+   --  checks and diagnostics for assignment statement Asmt.
+
+   procedure Process_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
+     (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_Read (Ref : Node_Id);
+   --  Perform ABE checks and diagnostics for reference Ref that reads a
+   --  variable.
 
    procedure Push_Active_Scenario (N : Node_Id);
    pragma Inline (Push_Active_Scenario);
@@ -1359,6 +1385,7 @@ package body Sem_Elab is
    --  should be set when the traversal is initiated from a task body.
 
    procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id);
+   pragma Inline (Update_Elaboration_Scenario);
    --  Update all relevant internal data structures when scenario Old_N is
    --  transformed into scenario New_N by Atree.Rewrite.
 
@@ -1939,97 +1966,6 @@ package body Sem_Elab is
       return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
    end Elaboration_Context_Hash;
 
-   --------------------------------------
-   -- Ensure_Dynamic_Prior_Elaboration --
-   --------------------------------------
-
-   procedure Ensure_Dynamic_Prior_Elaboration
-     (N        : Node_Id;
-      Unit_Id  : Entity_Id;
-      Prag_Nam : Name_Id)
-   is
-      procedure Info_Missing_Pragma;
-      pragma Inline (Info_Missing_Pragma);
-      --  Output information concerning missing Elaborate or Elaborate_All
-      --  pragma with name Prag_Nam for scenario N which ensures the prior
-      --  elaboration of Unit_Id.
-
-      -------------------------
-      -- Info_Missing_Pragma --
-      -------------------------
-
-      procedure Info_Missing_Pragma is
-      begin
-         --  Internal units are ignored as they cause unnecessary noise
-
-         if not In_Internal_Unit (Unit_Id) then
-
-            --  The name of the unit subjected to the elaboration pragma is
-            --  fully qualified to improve the clarity of the info message.
-
-            Error_Msg_Name_1     := Prag_Nam;
-            Error_Msg_Qual_Level := Nat'Last;
-
-            Error_Msg_NE ("info: missing pragma % for unit &", N, Unit_Id);
-            Error_Msg_Qual_Level := 0;
-         end if;
-      end Info_Missing_Pragma;
-
-      --  Local variables
-
-      Elab_Attrs : Elaboration_Attributes;
-      Level      : Enclosing_Level_Kind;
-
-   --  Start of processing for Ensure_Dynamic_Prior_Elaboration
-
-   begin
-      Elab_Attrs := Elaboration_Context.Get (Unit_Id);
-
-      --  Nothing to do when the unit is guaranteed prior elaboration by means
-      --  of a source Elaborate[_All] pragma.
-
-      if Present (Elab_Attrs.Source_Pragma) then
-         return;
-      end if;
-
-      --  Output extra information on a missing Elaborate[_All] pragma when
-      --  switch -gnatel (info messages on implicit Elaborate[_All] pragmas
-      --  is in effect.
-
-      if Elab_Info_Messages then
-
-         --  Performance note: parent traversal
-
-         Level := Find_Enclosing_Level (N);
-
-         --  Declaration level scenario
-
-         if (Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N))
-           and then Level = Declaration_Level
-         then
-            null;
-
-         --  Library level scenario
-
-         elsif Level in Library_Level then
-            null;
-
-         --  Instantiation library level scenario
-
-         elsif Level = Instantiation then
-            null;
-
-         --  Otherwise the scenario does not appear at the proper level and
-         --  cannot possibly act as a top level scenario.
-
-         else
-            return;
-         end if;
-
-         Info_Missing_Pragma;
-      end if;
-   end Ensure_Dynamic_Prior_Elaboration;
-
    ------------------------------
    -- Ensure_Prior_Elaboration --
    ------------------------------
@@ -2147,7 +2083,7 @@ package body Sem_Elab is
       --  effect.
 
       elsif Dynamic_Elaboration_Checks then
-         Ensure_Dynamic_Prior_Elaboration
+         Ensure_Prior_Elaboration_Dynamic
            (N        => N,
             Unit_Id  => Unit_Id,
             Prag_Nam => Prag_Nam);
@@ -2158,18 +2094,109 @@ package body Sem_Elab is
       else
          pragma Assert (Static_Elaboration_Checks);
 
-         Ensure_Static_Prior_Elaboration
+         Ensure_Prior_Elaboration_Static
            (N        => N,
             Unit_Id  => Unit_Id,
             Prag_Nam => Prag_Nam);
       end if;
    end Ensure_Prior_Elaboration;
 
+   --------------------------------------
+   -- Ensure_Prior_Elaboration_Dynamic --
+   --------------------------------------
+
+   procedure Ensure_Prior_Elaboration_Dynamic
+     (N        : Node_Id;
+      Unit_Id  : Entity_Id;
+      Prag_Nam : Name_Id)
+   is
+      procedure Info_Missing_Pragma;
+      pragma Inline (Info_Missing_Pragma);
+      --  Output information concerning missing Elaborate or Elaborate_All
+      --  pragma with name Prag_Nam for scenario N, which would ensure the
+      --  prior elaboration of Unit_Id.
+
+      -------------------------
+      -- Info_Missing_Pragma --
+      -------------------------
+
+      procedure Info_Missing_Pragma is
+      begin
+         --  Internal units are ignored as they cause unnecessary noise
+
+         if not In_Internal_Unit (Unit_Id) then
+
+            --  The name of the unit subjected to the elaboration pragma is
+            --  fully qualified to improve the clarity of the info message.
+
+            Error_Msg_Name_1     := Prag_Nam;
+            Error_Msg_Qual_Level := Nat'Last;
+
+            Error_Msg_NE ("info: missing pragma % for unit &", N, Unit_Id);
+            Error_Msg_Qual_Level := 0;
+         end if;
+      end Info_Missing_Pragma;
+
+      --  Local variables
+
+      Elab_Attrs : Elaboration_Attributes;
+      Level      : Enclosing_Level_Kind;
+
+   --  Start of processing for Ensure_Prior_Elaboration_Dynamic
+
+   begin
+      Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+
+      --  Nothing to do when the unit is guaranteed prior elaboration by means
+      --  of a source Elaborate[_All] pragma.
+
+      if Present (Elab_Attrs.Source_Pragma) then
+         return;
+      end if;
+
+      --  Output extra information on a missing Elaborate[_All] pragma when
+      --  switch -gnatel (info messages on implicit Elaborate[_All] pragmas
+      --  is in effect.
+
+      if Elab_Info_Messages then
+
+         --  Performance note: parent traversal
+
+         Level := Find_Enclosing_Level (N);
+
+         --  Declaration-level scenario
+
+         if (Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N))
+           and then Level = Declaration_Level
+         then
+            null;
+
+         --  Library-level scenario
+
+         elsif Level in Library_Level then
+            null;
+
+         --  Instantiation library-level scenario
+
+         elsif Level = Instantiation then
+            null;
+
+         --  Otherwise the scenario does not appear at the proper level and
+         --  cannot possibly act as a top-level scenario.
+
+         else
+            return;
+         end if;
+
+         Info_Missing_Pragma;
+      end if;
+   end Ensure_Prior_Elaboration_Dynamic;
+
    -------------------------------------
-   -- Ensure_Static_Prior_Elaboration --
+   -- Ensure_Prior_Elaboration_Static --
    -------------------------------------
 
-   procedure Ensure_Static_Prior_Elaboration
+   procedure Ensure_Prior_Elaboration_Static
      (N        : Node_Id;
       Unit_Id  : Entity_Id;
       Prag_Nam : Name_Id)
@@ -2177,8 +2204,9 @@ package body Sem_Elab is
       function Find_With_Clause
         (Items     : List_Id;
          Withed_Id : Entity_Id) return Node_Id;
-      --  Find a non-limited with clause in the list of context items Items
-      --  which withs unit Withed_Id. Return Empty if no such clause is found.
+      pragma Inline (Find_With_Clause);
+      --  Find a nonlimited with clause in the list of context items Items
+      --  that withs unit Withed_Id. Return Empty if no such clause is found.
 
       procedure Info_Implicit_Pragma;
       pragma Inline (Info_Implicit_Pragma);
@@ -2253,7 +2281,7 @@ package body Sem_Elab is
       Elab_Attrs : Elaboration_Attributes;
       Items      : List_Id;
 
-   --  Start of processing for Ensure_Static_Prior_Elaboration
+   --  Start of processing for Ensure_Prior_Elaboration_Static
 
    begin
       Elab_Attrs := Elaboration_Context.Get (Unit_Id);
@@ -2347,7 +2375,7 @@ package body Sem_Elab is
       if Elab_Info_Messages then
          Info_Implicit_Pragma;
       end if;
-   end Ensure_Static_Prior_Elaboration;
+   end Ensure_Prior_Elaboration_Static;
 
    -----------------------------
    -- Extract_Assignment_Name --
@@ -2921,7 +2949,7 @@ package body Sem_Elab is
          Full_Context : Boolean);
       --  Add unit Unit_Id to the elaboration context. Prag denotes the pragma
       --  which prompted the inclusion of the unit to the elaboration context.
-      --  If flag Full_Context is set, examine the non-limited clauses of unit
+      --  If flag Full_Context is set, examine the nonlimited clauses of unit
       --  Unit_Id and add each withed unit to the context.
 
       procedure Find_Elaboration_Context (Comp_Unit : Node_Id);
@@ -3018,7 +3046,7 @@ package body Sem_Elab is
 
          if Full_Context then
 
-            --  Process all non-limited with clauses found in the context of
+            --  Process all nonlimited with clauses found in the context of
             --  the current unit. Note that limited clauses do not impose an
             --  elaboration order.
 
@@ -4140,11 +4168,11 @@ package body Sem_Elab is
          In_SPARK => In_SPARK);
    end Info_Instantiation;
 
-   -----------------------------
-   -- Info_Variable_Reference --
-   -----------------------------
+   ------------------------
+   -- Info_Variable_Read --
+   ------------------------
 
-   procedure Info_Variable_Reference
+   procedure Info_Variable_Read
      (Ref      : Node_Id;
       Var_Id   : Entity_Id;
       Info_Msg : Boolean;
@@ -4152,12 +4180,12 @@ package body Sem_Elab is
    is
    begin
       Elab_Msg_NE
-        (Msg      => "reference to variable & during elaboration",
+        (Msg      => "read of variable & during elaboration",
          N        => Ref,
          Id       => Var_Id,
          Info_Msg => Info_Msg,
          In_SPARK => In_SPARK);
-   end Info_Variable_Reference;
+   end Info_Variable_Read;
 
    --------------------
    -- Insertion_Node --
@@ -4642,6 +4670,18 @@ package body Sem_Elab is
         Ekind (Id) = E_Procedure and then Is_Initial_Condition_Procedure (Id);
    end Is_Initial_Condition_Proc;
 
+   --------------------
+   -- Is_Initialized --
+   --------------------
+
+   function Is_Initialized (Obj_Decl : Node_Id) return Boolean is
+   begin
+      --  To qualify, the object declaration must have an expression
+
+      return
+        Present (Expression (Obj_Decl)) or else Has_Init_Expression (Obj_Decl);
+   end Is_Initialized;
+
    -----------------------
    -- Is_Invariant_Proc --
    -----------------------
@@ -5102,7 +5142,7 @@ package body Sem_Elab is
           or else Is_Suitable_Call (N)
           or else Is_Suitable_Instantiation (N)
           or else Is_Suitable_Variable_Assignment (N)
-          or else Is_Suitable_Variable_Reference (N);
+          or else Is_Suitable_Variable_Read (N);
    end Is_Suitable_Scenario;
 
    -------------------------------------
@@ -5182,11 +5222,7 @@ package body Sem_Elab is
       --  To qualify, the assignment must meet the following prerequisites:
 
       return
-
-        --  The variable must be a source entity and susceptible to warnings
-
         Comes_From_Source (Var_Id)
-          and then not Warnings_Off (Var_Id)
 
           --  The variable must be declared in the spec of compilation unit U
 
@@ -5196,29 +5232,23 @@ package body Sem_Elab is
 
           and then Find_Enclosing_Level (Var_Decl) = Package_Spec
 
-          --  The variable must lack initialization
-
-          and then not Has_Init_Expression (Var_Decl)
-          and then No (Expression (Var_Decl))
-
           --  The assignment must occur in the body of compilation unit U
 
           and then Nkind (N_Unit) = N_Package_Body
           and then Present (Corresponding_Body (Var_Unit))
-          and then Corresponding_Body (Var_Unit) = N_Unit_Id
-
-          --  The package spec must lack pragma Elaborate_Body
-
-          and then not Has_Pragma_Elaborate_Body (Var_Unit_Id);
+          and then Corresponding_Body (Var_Unit) = N_Unit_Id;
    end Is_Suitable_Variable_Assignment;
 
-   ------------------------------------
-   -- Is_Suitable_Variable_Reference --
-   ------------------------------------
+   -------------------------------
+   -- Is_Suitable_Variable_Read --
+   -------------------------------
 
-   function Is_Suitable_Variable_Reference (N : Node_Id) return Boolean is
+   function Is_Suitable_Variable_Read (N : Node_Id) return Boolean is
       function In_Pragma (Nod : Node_Id) return Boolean;
-      --  Determine whether arbitrary node N appears within a pragma
+      --  Determine whether arbitrary node Nod appears within a pragma
+
+      function Is_Variable_Read (Ref : Node_Id) return Boolean;
+      --  Determine whether variable reference Ref constitutes a read
 
       ---------------
       -- In_Pragma --
@@ -5245,12 +5275,88 @@ package body Sem_Elab is
          return False;
       end In_Pragma;
 
+      ----------------------
+      -- Is_Variable_Read --
+      ----------------------
+
+      function Is_Variable_Read (Ref : Node_Id) return Boolean is
+         function Is_Out_Actual (Call : Node_Id) return Boolean;
+         --  Determine whether the corresponding formal of actual Ref which
+         --  appears in call Call has mode OUT.
+
+         -------------------
+         -- Is_Out_Actual --
+         -------------------
+
+         function Is_Out_Actual (Call : Node_Id) return Boolean is
+            Actual     : Node_Id;
+            Call_Attrs : Call_Attributes;
+            Formal     : Entity_Id;
+            Target_Id  : Entity_Id;
+
+         begin
+            Extract_Call_Attributes
+              (Call      => Call,
+               Target_Id => Target_Id,
+               Attrs     => Call_Attrs);
+
+            --  Inspect the actual and formal parameters, trying to find the
+            --  corresponding formal for Ref.
+
+            Actual := First_Actual (Call);
+            Formal := First_Formal (Target_Id);
+            while Present (Actual) and then Present (Formal) loop
+               if Actual = Ref then
+                  return Ekind (Formal) = E_Out_Parameter;
+               end if;
+
+               Next_Actual (Actual);
+               Next_Formal (Formal);
+            end loop;
+
+            return False;
+         end Is_Out_Actual;
+
+         --  Local variables
+
+         Context : constant Node_Id := Parent (Ref);
+
+      --  Start of processing for Is_Variable_Read
+
+      begin
+         --  The majority of variable references are reads, and they can appear
+         --  in a great number of contexts. To determine whether a reference is
+         --  a read, it is more practical to find out whether it is a write.
+
+         --  A reference is a write when appearing immediately on the left-hand
+         --  side of an assignment.
+
+         if Nkind (Context) = N_Assignment_Statement
+           and then Name (Context) = Ref
+         then
+            return False;
+
+         --  A reference is a write when it acts as an actual in a subprogram
+         --  call and the corresponding formal has mode OUT.
+
+         elsif Nkind_In (Context, N_Function_Call,
+                                  N_Procedure_Call_Statement)
+           and then Is_Out_Actual (Context)
+         then
+            return False;
+         end if;
+
+         --  Any other reference is a read
+
+         return True;
+      end Is_Variable_Read;
+
       --  Local variables
 
       Prag   : Node_Id;
       Var_Id : Entity_Id;
 
-   --  Start of processing for Is_Suitable_Variable_Reference
+   --  Start of processing for Is_Suitable_Variable_Read
 
    begin
       --  This scenario is relevant only when the static model is in effect
@@ -5262,8 +5368,7 @@ package body Sem_Elab is
          return False;
 
       --  Attributes and operator sumbols are not considered to be suitable
-      --  references to variables even though they are part of predicate
-      --  Is_Entity_Name.
+      --  references even though they are part of predicate Is_Entity_Name.
 
       elsif not Nkind_In (N, N_Expanded_Name, N_Identifier) then
          return False;
@@ -5303,6 +5408,10 @@ package body Sem_Elab is
           and then Get_SPARK_Mode_From_Annotation (Prag) = On
           and then Is_SPARK_Mode_On_Node (N)
 
+          --  The reference must denote a variable read
+
+          and then Is_Variable_Read (N)
+
           --  The reference must not be considered when it appears in a pragma.
           --  If the pragma has run-time semantics, then the reference will be
           --  reconsidered once the pragma is expanded.
@@ -5310,7 +5419,7 @@ package body Sem_Elab is
           --  Performance note: parent traversal
 
           and then not In_Pragma (N);
-   end Is_Suitable_Variable_Reference;
+   end Is_Suitable_Variable_Read;
 
    -------------------
    -- Is_Task_Entry --
@@ -5485,8 +5594,8 @@ package body Sem_Elab is
                Info_Msg => False,
                In_SPARK => True);
 
-         elsif Is_Suitable_Variable_Reference (N) then
-            Info_Variable_Reference
+         elsif Is_Suitable_Variable_Read (N) then
+            Info_Variable_Read
               (Ref      => N,
                Var_Id   => Target_Id,
                Info_Msg => False,
@@ -5650,8 +5759,9 @@ package body Sem_Elab is
       procedure Output_Variable_Assignment (N : Node_Id);
       --  Emit a specific diagnostic message for assignment statement N
 
-      procedure Output_Variable_Reference (N : Node_Id);
-      --  Emit a specific diagnostic message for variable reference N
+      procedure Output_Variable_Read (N : Node_Id);
+      --  Emit a specific diagnostic message for reference N which reads a
+      --  variable.
 
       -------------------
       -- Output_Access --
@@ -5980,11 +6090,11 @@ package body Sem_Elab is
          Error_Msg_NE ("\\  variable & assigned #", Error_Nod, Var_Id);
       end Output_Variable_Assignment;
 
-      -------------------------------
-      -- Output_Variable_Reference --
-      -------------------------------
+      --------------------------
+      -- Output_Variable_Read --
+      --------------------------
 
-      procedure Output_Variable_Reference (N : Node_Id) is
+      procedure Output_Variable_Read (N : Node_Id) is
          Dummy  : Variable_Attributes;
          Var_Id : Entity_Id;
 
@@ -5995,8 +6105,8 @@ package body Sem_Elab is
             Attrs  => Dummy);
 
          Error_Msg_Sloc := Sloc (N);
-         Error_Msg_NE ("\\  variable & referenced #", Error_Nod, Var_Id);
-      end Output_Variable_Reference;
+         Error_Msg_NE ("\\  variable & read #", Error_Nod, Var_Id);
+      end Output_Variable_Read;
 
       --  Local variables
 
@@ -6057,10 +6167,10 @@ package body Sem_Elab is
          elsif Nkind (N) = N_Assignment_Statement then
             Output_Variable_Assignment (N);
 
-         --  Variable references
+         --  Variable read
 
-         elsif Is_Suitable_Variable_Reference (N) then
-            Output_Variable_Reference (N);
+         elsif Is_Suitable_Variable_Read (N) then
+            Output_Variable_Read (N);
 
          else
             pragma Assert (False);
@@ -7732,31 +7842,73 @@ package body Sem_Elab is
    ---------------------------------
 
    procedure Process_Variable_Assignment (Asmt : Node_Id) is
-      Var_Id  : constant Entity_Id := Entity (Extract_Assignment_Name (Asmt));
-      Spec_Id : Entity_Id;
+      Var_Id : constant Entity_Id := Entity (Extract_Assignment_Name (Asmt));
+      Prag   : constant Node_Id   := SPARK_Pragma (Var_Id);
+
+      SPARK_Rules_On : Boolean;
+      --  This flag is set when the SPARK rules are in effect
 
    begin
+      --  The SPARK rules are in effect when both the assignment and the
+      --  variable are subject to SPARK_Mode On.
+
+      SPARK_Rules_On :=
+        Present (Prag)
+          and then Get_SPARK_Mode_From_Annotation (Prag) = On
+          and then Is_SPARK_Mode_On_Node (Asmt);
+
       --  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: assignment to & during elaboration", Asmt, Var_Id);
+         Elab_Msg_NE
+           (Msg      => "assignment to & during elaboration",
+            N        => Asmt,
+            Id       => Var_Id,
+            Info_Msg => True,
+            In_SPARK => SPARK_Rules_On);
       end if;
 
-      Spec_Id := Find_Top_Unit (Var_Id);
+      --  The SPARK rules are in effect
+
+      if SPARK_Rules_On then
+         Process_Variable_Assignment_SPARK
+           (Asmt   => Asmt,
+            Var_Id => Var_Id);
 
-      --  Generate an implicit Elaborate_Body in the spec
+      --  Otherwise the Ada rules are in effect
 
-      Set_Elaborate_Body_Desirable (Spec_Id);
+      else
+         Process_Variable_Assignment_Ada
+           (Asmt   => Asmt,
+            Var_Id => Var_Id);
+      end if;
+   end Process_Variable_Assignment;
 
-      --  No warning is emitted for internal uses. This behaviour parallels
-      --  that of the old ABE mechanism.
+   -------------------------------------
+   -- Process_Variable_Assignment_Ada --
+   -------------------------------------
 
-      if GNAT_Mode then
-         null;
+   procedure Process_Variable_Assignment_Ada
+     (Asmt   : Node_Id;
+      Var_Id : Entity_Id)
+   is
+      Var_Decl : constant Node_Id   := Declaration_Node (Var_Id);
+      Spec_Id  : constant Entity_Id := Find_Top_Unit (Var_Decl);
+
+   begin
+      --  Emit a warning when an uninitialized variable declared in a package
+      --  spec without a pragma Elaborate_Body is initialized by elaboration
+      --  code within the corresponding body.
+
+      if not Warnings_Off (Var_Id)
+        and then not Is_Initialized (Var_Decl)
+        and then not Has_Pragma_Elaborate_Body (Spec_Id)
+      then
+         --  Generate an implicit Elaborate_Body in the spec
+
+         Set_Elaborate_Body_Desirable (Spec_Id);
 
-      else
          Error_Msg_NE
            ("??variable & can be accessed by clients before this "
             & "initialization", Asmt, Var_Id);
@@ -7767,13 +7919,44 @@ package body Sem_Elab is
 
          Output_Active_Scenarios (Asmt);
       end if;
-   end Process_Variable_Assignment;
+   end Process_Variable_Assignment_Ada;
 
-   --------------------------------
-   -- Process_Variable_Reference --
-   --------------------------------
+   ---------------------------------------
+   -- Process_Variable_Assignment_SPARK --
+   ---------------------------------------
+
+   procedure Process_Variable_Assignment_SPARK
+     (Asmt   : Node_Id;
+      Var_Id : Entity_Id)
+   is
+      Var_Decl : constant Node_Id   := Declaration_Node (Var_Id);
+      Spec_Id  : constant Entity_Id := Find_Top_Unit (Var_Decl);
+
+   begin
+      --  Emit an error when an initialized variable declared in a package spec
+      --  without pragma Elaborate_Body is further modified by elaboration code
+      --  within the corresponding body.
+
+      if Is_Initialized (Var_Decl)
+        and then not Has_Pragma_Elaborate_Body (Spec_Id)
+      then
+         Error_Msg_NE
+           ("variable & modified by elaboration code in package body",
+            Asmt, Var_Id);
 
-   procedure Process_Variable_Reference (Ref : Node_Id) is
+         Error_Msg_NE
+           ("\add pragma ""Elaborate_Body"" to spec & to ensure full "
+            & "initialization", Asmt, Spec_Id);
+
+         Output_Active_Scenarios (Asmt);
+      end if;
+   end Process_Variable_Assignment_SPARK;
+
+   ---------------------------
+   -- Process_Variable_Read --
+   ---------------------------
+
+   procedure Process_Variable_Read (Ref : Node_Id) is
       Var_Attrs : Variable_Attributes;
       Var_Id    : Entity_Id;
 
@@ -7788,22 +7971,42 @@ package body Sem_Elab is
 
       if Elab_Info_Messages then
          Elab_Msg_NE
-           (Msg      => "reference to variable & during elaboration",
+           (Msg      => "read of variable & during elaboration",
             N        => Ref,
             Id       => Var_Id,
             Info_Msg => True,
             In_SPARK => True);
       end if;
 
-      --  A source variable reference imposes an Elaborate_All requirement on
-      --  the context of the main unit. Determine whethe the context has a
-      --  pragma strong enough to meet the requirement.
+      --  Nothing to do when the variable appears within the main unit because
+      --  diagnostics on reads are relevant only for external variables.
 
-      Meet_Elaboration_Requirement
-        (N         => Ref,
-         Target_Id => Var_Id,
-         Req_Nam   => Name_Elaborate_All);
-   end Process_Variable_Reference;
+      if Is_Same_Unit (Var_Attrs.Unit_Id, Cunit_Entity (Main_Unit)) then
+         null;
+
+      --  Nothing to do when the variable is already initialized. Note that the
+      --  variable may be further modified by the external unit.
+
+      elsif Is_Initialized (Declaration_Node (Var_Id)) then
+         null;
+
+      --  Nothing to do when the external unit guarantees the initialization of
+      --  the variable by means of pragma Elaborate_Body.
+
+      elsif Has_Pragma_Elaborate_Body (Var_Attrs.Unit_Id) then
+         null;
+
+      --  A variable read imposes an Elaborate requirement on the context of
+      --  the main unit. Determine whether the context has a pragma strong
+      --  enough to meet the requirement.
+
+      else
+         Meet_Elaboration_Requirement
+           (N         => Ref,
+            Target_Id => Var_Id,
+            Req_Nam   => Name_Elaborate);
+      end if;
+   end Process_Variable_Read;
 
    --------------------------
    -- Push_Active_Scenario --
@@ -7874,10 +8077,10 @@ package body Sem_Elab is
       elsif Is_Suitable_Variable_Assignment (N) then
          Process_Variable_Assignment (N);
 
-      --  Variable references
+      --  Variable read
 
-      elsif Is_Suitable_Variable_Reference (N) then
-         Process_Variable_Reference (N);
+      elsif Is_Suitable_Variable_Read (N) then
+         Process_Variable_Read (N);
       end if;
 
       --  Remove the current scenario from the stack of active scenarios once
@@ -7945,7 +8148,7 @@ package body Sem_Elab is
 
       elsif Is_Suitable_Access (N)
         or else Is_Suitable_Variable_Assignment (N)
-        or else Is_Suitable_Variable_Reference (N)
+        or else Is_Suitable_Variable_Read (N)
       then
          null;