[multiple changes]

2017-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_util.adb (Check_Part_Of_Reference):
	Continue to examine the context if the reference appears within
	an expression function.

2017-04-25  Justin Squirek  <squirek@adacore.com>

	* exp_ch7.adb, exp_ch7.ads Remove Build_Invariant_Procedure_Body
	and Build_Invariant_Procedure_Declaration.
	* exp_util.ads, exp_util.adb Add Build_Invariant_Procedure_Body
	and Build_Invariant_Procedure_Declaration from exp_ch7
	and break-out Is_Untagged_Private_Derivation from
	Build_Invariant_Procedure_Body.
	(Replace_Type_References):
	Append an extra parameter to allow for dispatching replacements
	and add the corrasponding logic.
	(Type_Invariant): Remove
	Replace_Typ_Refs and replace its references with calls to
	Replace_Type_References.
	* sem_ch3.adb, sem_prag.adb: Remove with and use of exp_ch7.

From-SVN: r247152

8 files changed, 1481 insertions, 1495 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3f938e8..917785a 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,25 @@
+2017-04-25  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_util.adb (Check_Part_Of_Reference):
+	Continue to examine the context if the reference appears within
+	an expression function.
+
+2017-04-25  Justin Squirek  <squirek@adacore.com>
+
+	* exp_ch7.adb, exp_ch7.ads Remove Build_Invariant_Procedure_Body
+	and Build_Invariant_Procedure_Declaration.
+	* exp_util.ads, exp_util.adb Add Build_Invariant_Procedure_Body
+	and Build_Invariant_Procedure_Declaration from exp_ch7
+	and break-out Is_Untagged_Private_Derivation from
+	Build_Invariant_Procedure_Body.
+	(Replace_Type_References):
+	Append an extra parameter to allow for dispatching replacements
+	and add the corrasponding logic.
+	(Type_Invariant): Remove
+	Replace_Typ_Refs and replace its references with calls to
+	Replace_Type_References.
+	* sem_ch3.adb, sem_prag.adb: Remove with and use of exp_ch7.
+
 2017-04-25  Bob Duff  <duff@adacore.com>
 
 	* sem_util.ads, sem_util.adb (Should_Ignore_Pragma): New function
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 93573a2..5d98160 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -42,7 +42,6 @@ with Exp_Prag; use Exp_Prag;
 with Exp_Tss;  use Exp_Tss;
 with Exp_Util; use Exp_Util;
 with Freeze;   use Freeze;
-with Ghost;    use Ghost;
 with Lib;      use Lib;
 with Nlists;   use Nlists;
 with Nmake;    use Nmake;
@@ -55,15 +54,12 @@ with Sinfo;    use Sinfo;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Ch3;  use Sem_Ch3;
-with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch7;  use Sem_Ch7;
 with Sem_Ch8;  use Sem_Ch8;
-with Sem_Ch13; use Sem_Ch13;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Snames;   use Snames;
 with Stand;    use Stand;
-with Stringt;  use Stringt;
 with Tbuild;   use Tbuild;
 with Ttypes;   use Ttypes;
 with Uintp;    use Uintp;
@@ -3451,1470 +3447,6 @@ package body Exp_Ch7 is
       Expand_At_End_Handler (HSS, Empty);
    end Build_Finalizer_Call;
 
-   ------------------------------------
-   -- Build_Invariant_Procedure_Body --
-   ------------------------------------
-
-   --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
-   --  Ghost mode.
-
-   procedure Build_Invariant_Procedure_Body
-     (Typ               : Entity_Id;
-      Partial_Invariant : Boolean := False)
-   is
-      Loc : constant Source_Ptr := Sloc (Typ);
-
-      Pragmas_Seen : Elist_Id := No_Elist;
-      --  This list contains all invariant pragmas processed so far. The list
-      --  is used to avoid generating redundant invariant checks.
-
-      Produced_Check : Boolean := False;
-      --  This flag tracks whether the type has produced at least one invariant
-      --  check. The flag is used as a sanity check at the end of the routine.
-
-      --  NOTE: most of the routines in Build_Invariant_Procedure_Body are
-      --  intentionally unnested to avoid deep indentation of code.
-
-      --  NOTE: all Add_xxx_Invariants routines are reactive. In other words
-      --  they emit checks, loops (for arrays) and case statements (for record
-      --  variant parts) only when there are invariants to verify. This keeps
-      --  the body of the invariant procedure free from useless code.
-
-      procedure Add_Array_Component_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id);
-      --  Generate an invariant check for each component of array type T.
-      --  Obj_Id denotes the entity of the _object formal parameter of the
-      --  invariant procedure. All created checks are added to list Checks.
-
-      procedure Add_Interface_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id);
-      --  Generate an invariant check for each inherited class-wide invariant
-      --  coming from all interfaces implemented by type T. Obj_Id denotes the
-      --  entity of the _object formal parameter of the invariant procedure.
-      --  All created checks are added to list Checks.
-
-      procedure Add_Parent_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id);
-      --  Generate an invariant check for each inherited class-wide invariant
-      --  coming from all parent types of type T. Obj_Id denotes the entity of
-      --  the _object formal parameter of the invariant procedure. All created
-      --  checks are added to list Checks.
-
-      procedure Add_Record_Component_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id);
-      --  Generate an invariant check for each component of record type T.
-      --  Obj_Id denotes the entity of the _object formal parameter of the
-      --  invariant procedure. All created checks are added to list Checks.
-
-      procedure Add_Type_Invariants
-        (Priv_Typ  : Entity_Id;
-         Full_Typ  : Entity_Id;
-         CRec_Typ  : Entity_Id;
-         Obj_Id    : Entity_Id;
-         Checks    : in out List_Id;
-         Inherit   : Boolean := False;
-         Priv_Item : Node_Id := Empty);
-      --  Generate an invariant check for each invariant found in one of the
-      --  following types (if available):
-      --
-      --    Priv_Typ - the partial view of a type
-      --    Full_Typ - the full view of a type
-      --    CRec_Typ - the corresponding record of a protected or a task type
-      --
-      --  Obj_Id denotes the entity of the _object formal parameter of the
-      --  invariant procedure. All created checks are added to list Checks.
-      --  Flag Inherit should be set when generating invariant checks for
-      --  inherited class-wide invariants. Priv_Item denotes the first rep
-      --  item of the private type.
-
-      function Is_Untagged_Private_Derivation
-        (Priv_Typ : Entity_Id;
-         Full_Typ : Entity_Id) return Boolean;
-      --  Determine whether private type Priv_Typ and its full view Full_Typ
-      --  represent an untagged derivation from a private parent.
-
-      ------------------------------------
-      -- Add_Array_Component_Invariants --
-      ------------------------------------
-
-      procedure Add_Array_Component_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id)
-      is
-         Comp_Typ : constant Entity_Id := Component_Type (T);
-         Dims     : constant Pos       := Number_Dimensions (T);
-
-         procedure Process_Array_Component
-           (Indices     : List_Id;
-            Comp_Checks : in out List_Id);
-         --  Generate an invariant check for an array component identified by
-         --  the indices in list Indices. All created checks are added to list
-         --  Comp_Checks.
-
-         procedure Process_One_Dimension
-           (Dim        : Pos;
-            Indices    : List_Id;
-            Dim_Checks : in out List_Id);
-         --  Generate a loop over the Nth dimension Dim of an array type. List
-         --  Indices contains all array indices for the dimension. All created
-         --  checks are added to list Dim_Checks.
-
-         -----------------------------
-         -- Process_Array_Component --
-         -----------------------------
-
-         procedure Process_Array_Component
-           (Indices     : List_Id;
-            Comp_Checks : in out List_Id)
-         is
-            Proc_Id : Entity_Id;
-
-         begin
-            if Has_Invariants (Comp_Typ) then
-
-               --  In GNATprove mode, the component invariants are checked by
-               --  other means. They should not be added to the array type
-               --  invariant procedure, so that the procedure can be used to
-               --  check the array type invariants if any.
-
-               if GNATprove_Mode then
-                  null;
-
-               else
-                  Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
-
-                  --  The component type should have an invariant procedure
-                  --  if it has invariants of its own or inherits class-wide
-                  --  invariants from parent or interface types.
-
-                  pragma Assert (Present (Proc_Id));
-
-                  --  Generate:
-                  --    <Comp_Typ>Invariant (_object (<Indices>));
-
-                  --  Note that the invariant procedure may have a null body if
-                  --  assertions are disabled or Assertion_Policy Ignore is in
-                  --  effect.
-
-                  if not Has_Null_Body (Proc_Id) then
-                     Append_New_To (Comp_Checks,
-                       Make_Procedure_Call_Statement (Loc,
-                         Name                   =>
-                           New_Occurrence_Of (Proc_Id, Loc),
-                         Parameter_Associations => New_List (
-                           Make_Indexed_Component (Loc,
-                             Prefix      => New_Occurrence_Of (Obj_Id, Loc),
-                             Expressions => New_Copy_List (Indices)))));
-                  end if;
-               end if;
-
-               Produced_Check := True;
-            end if;
-         end Process_Array_Component;
-
-         ---------------------------
-         -- Process_One_Dimension --
-         ---------------------------
-
-         procedure Process_One_Dimension
-           (Dim        : Pos;
-            Indices    : List_Id;
-            Dim_Checks : in out List_Id)
-         is
-            Comp_Checks : List_Id := No_List;
-            Index       : Entity_Id;
-
-         begin
-            --  Generate the invariant checks for the array component after all
-            --  dimensions have produced their respective loops.
-
-            if Dim > Dims then
-               Process_Array_Component
-                 (Indices     => Indices,
-                  Comp_Checks => Dim_Checks);
-
-            --  Otherwise create a loop for the current dimension
-
-            else
-               --  Create a new loop variable for each dimension
-
-               Index :=
-                 Make_Defining_Identifier (Loc,
-                   Chars => New_External_Name ('I', Dim));
-               Append_To (Indices, New_Occurrence_Of (Index, Loc));
-
-               Process_One_Dimension
-                 (Dim        => Dim + 1,
-                  Indices    => Indices,
-                  Dim_Checks => Comp_Checks);
-
-               --  Generate:
-               --    for I<Dim> in _object'Range (<Dim>) loop
-               --       <Comp_Checks>
-               --    end loop;
-
-               --  Note that the invariant procedure may have a null body if
-               --  assertions are disabled or Assertion_Policy Ignore is in
-               --  effect.
-
-               if Present (Comp_Checks) then
-                  Append_New_To (Dim_Checks,
-                    Make_Implicit_Loop_Statement (T,
-                      Identifier       => Empty,
-                      Iteration_Scheme =>
-                        Make_Iteration_Scheme (Loc,
-                          Loop_Parameter_Specification =>
-                            Make_Loop_Parameter_Specification (Loc,
-                              Defining_Identifier         => Index,
-                              Discrete_Subtype_Definition =>
-                                Make_Attribute_Reference (Loc,
-                                  Prefix         =>
-                                    New_Occurrence_Of (Obj_Id, Loc),
-                                  Attribute_Name => Name_Range,
-                                  Expressions    => New_List (
-                                    Make_Integer_Literal (Loc, Dim))))),
-
-                      Statements => Comp_Checks));
-               end if;
-            end if;
-         end Process_One_Dimension;
-
-      --  Start of processing for Add_Array_Component_Invariants
-
-      begin
-         Process_One_Dimension
-           (Dim        => 1,
-            Indices    => New_List,
-            Dim_Checks => Checks);
-      end Add_Array_Component_Invariants;
-
-      ------------------------------
-      -- Add_Interface_Invariants --
-      ------------------------------
-
-      procedure Add_Interface_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id)
-      is
-         Iface_Elmt : Elmt_Id;
-         Ifaces     : Elist_Id;
-
-      begin
-         if Is_Tagged_Type (T) then
-            Collect_Interfaces (T, Ifaces);
-
-            --  Process the class-wide invariants of all implemented interfaces
-
-            Iface_Elmt := First_Elmt (Ifaces);
-            while Present (Iface_Elmt) loop
-               Add_Type_Invariants
-                 (Priv_Typ => Empty,
-                  Full_Typ => Node (Iface_Elmt),
-                  CRec_Typ => Empty,
-                  Obj_Id   => Obj_Id,
-                  Checks   => Checks,
-                  Inherit  => True);
-
-               Next_Elmt (Iface_Elmt);
-            end loop;
-         end if;
-      end Add_Interface_Invariants;
-
-      ---------------------------
-      -- Add_Parent_Invariants --
-      ---------------------------
-
-      procedure Add_Parent_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id)
-      is
-         Dummy_1 : Entity_Id;
-         Dummy_2 : Entity_Id;
-
-         Curr_Typ : Entity_Id;
-         --  The entity of the current type being examined
-
-         Full_Typ : Entity_Id;
-         --  The full view of Par_Typ
-
-         Par_Typ : Entity_Id;
-         --  The entity of the parent type
-
-         Priv_Typ : Entity_Id;
-         --  The partial view of Par_Typ
-
-      begin
-         --  Do not process array types because they cannot have true parent
-         --  types. This also prevents the generation of a duplicate invariant
-         --  check when the input type is an array base type because its Etype
-         --  denotes the first subtype, both of which share the same component
-         --  type.
-
-         if Is_Array_Type (T) then
-            return;
-         end if;
-
-         --  Climb the parent type chain
-
-         Curr_Typ := T;
-         loop
-            --  Do not consider subtypes as they inherit the invariants from
-            --  their base types.
-
-            Par_Typ := Base_Type (Etype (Curr_Typ));
-
-            --  Stop the climb once the root of the parent chain is reached
-
-            exit when Curr_Typ = Par_Typ;
-
-            --  Process the class-wide invariants of the parent type
-
-            Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
-
-            Add_Type_Invariants
-              (Priv_Typ => Priv_Typ,
-               Full_Typ => Full_Typ,
-               CRec_Typ => Empty,
-               Obj_Id   => Obj_Id,
-               Checks   => Checks,
-               Inherit  => True);
-
-            Curr_Typ := Par_Typ;
-         end loop;
-      end Add_Parent_Invariants;
-
-      -------------------------------------
-      -- Add_Record_Component_Invariants --
-      -------------------------------------
-
-      procedure Add_Record_Component_Invariants
-        (T      : Entity_Id;
-         Obj_Id : Entity_Id;
-         Checks : in out List_Id)
-      is
-         procedure Process_Component_List
-           (Comp_List : Node_Id;
-            CL_Checks : in out List_Id);
-         --  Generate invariant checks for all record components found in
-         --  component list Comp_List, including variant parts. All created
-         --  checks are added to list CL_Checks.
-
-         procedure Process_Record_Component
-           (Comp_Id     : Entity_Id;
-            Comp_Checks : in out List_Id);
-         --  Generate an invariant check for a record component identified by
-         --  Comp_Id. All created checks are added to list Comp_Checks.
-
-         ----------------------------
-         -- Process_Component_List --
-         ----------------------------
-
-         procedure Process_Component_List
-           (Comp_List : Node_Id;
-            CL_Checks : in out List_Id)
-         is
-            Comp       : Node_Id;
-            Var        : Node_Id;
-            Var_Alts   : List_Id := No_List;
-            Var_Checks : List_Id := No_List;
-            Var_Stmts  : List_Id;
-
-            Produced_Variant_Check : Boolean := False;
-            --  This flag tracks whether the component has produced at least
-            --  one invariant check.
-
-         begin
-            --  Traverse the component items
-
-            Comp := First (Component_Items (Comp_List));
-            while Present (Comp) loop
-               if Nkind (Comp) = N_Component_Declaration then
-
-                  --  Generate the component invariant check
-
-                  Process_Record_Component
-                    (Comp_Id     => Defining_Entity (Comp),
-                     Comp_Checks => CL_Checks);
-               end if;
-
-               Next (Comp);
-            end loop;
-
-            --  Traverse the variant part
-
-            if Present (Variant_Part (Comp_List)) then
-               Var := First (Variants (Variant_Part (Comp_List)));
-               while Present (Var) loop
-                  Var_Checks := No_List;
-
-                  --  Generate invariant checks for all components and variant
-                  --  parts that qualify.
-
-                  Process_Component_List
-                    (Comp_List => Component_List (Var),
-                     CL_Checks => Var_Checks);
-
-                  --  The components of the current variant produced at least
-                  --  one invariant check.
-
-                  if Present (Var_Checks) then
-                     Var_Stmts := Var_Checks;
-                     Produced_Variant_Check := True;
-
-                  --  Otherwise there are either no components with invariants,
-                  --  assertions are disabled, or Assertion_Policy Ignore is in
-                  --  effect.
-
-                  else
-                     Var_Stmts := New_List (Make_Null_Statement (Loc));
-                  end if;
-
-                  Append_New_To (Var_Alts,
-                    Make_Case_Statement_Alternative (Loc,
-                      Discrete_Choices =>
-                        New_Copy_List (Discrete_Choices (Var)),
-                      Statements       => Var_Stmts));
-
-                  Next (Var);
-               end loop;
-
-               --  Create a case statement which verifies the invariant checks
-               --  of a particular component list depending on the discriminant
-               --  values only when there is at least one real invariant check.
-
-               if Produced_Variant_Check then
-                  Append_New_To (CL_Checks,
-                    Make_Case_Statement (Loc,
-                      Expression   =>
-                        Make_Selected_Component (Loc,
-                          Prefix        => New_Occurrence_Of (Obj_Id, Loc),
-                          Selector_Name =>
-                            New_Occurrence_Of
-                              (Entity (Name (Variant_Part (Comp_List))), Loc)),
-                      Alternatives => Var_Alts));
-               end if;
-            end if;
-         end Process_Component_List;
-
-         ------------------------------
-         -- Process_Record_Component --
-         ------------------------------
-
-         procedure Process_Record_Component
-           (Comp_Id     : Entity_Id;
-            Comp_Checks : in out List_Id)
-         is
-            Comp_Typ : constant Entity_Id := Etype (Comp_Id);
-            Proc_Id  : Entity_Id;
-
-            Produced_Component_Check : Boolean := False;
-            --  This flag tracks whether the component has produced at least
-            --  one invariant check.
-
-         begin
-            --  Nothing to do for internal component _parent. Note that it is
-            --  not desirable to check whether the component comes from source
-            --  because protected type components are relocated to an internal
-            --  corresponding record, but still need processing.
-
-            if Chars (Comp_Id) = Name_uParent then
-               return;
-            end if;
-
-            --  Verify the invariant of the component. Note that an access
-            --  type may have an invariant when it acts as the full view of a
-            --  private type and the invariant appears on the partial view. In
-            --  this case verify the access value itself.
-
-            if Has_Invariants (Comp_Typ) then
-
-               --  In GNATprove mode, the component invariants are checked by
-               --  other means. They should not be added to the record type
-               --  invariant procedure, so that the procedure can be used to
-               --  check the record type invariants if any.
-
-               if GNATprove_Mode then
-                  null;
-
-               else
-                  Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
-
-                  --  The component type should have an invariant procedure
-                  --  if it has invariants of its own or inherits class-wide
-                  --  invariants from parent or interface types.
-
-                  pragma Assert (Present (Proc_Id));
-
-                  --  Generate:
-                  --    <Comp_Typ>Invariant (T (_object).<Comp_Id>);
-
-                  --  Note that the invariant procedure may have a null body if
-                  --  assertions are disabled or Assertion_Policy Ignore is in
-                  --  effect.
-
-                  if not Has_Null_Body (Proc_Id) then
-                     Append_New_To (Comp_Checks,
-                       Make_Procedure_Call_Statement (Loc,
-                         Name                   =>
-                           New_Occurrence_Of (Proc_Id, Loc),
-                         Parameter_Associations => New_List (
-                           Make_Selected_Component (Loc,
-                             Prefix        =>
-                               Unchecked_Convert_To
-                                 (T, New_Occurrence_Of (Obj_Id, Loc)),
-                             Selector_Name =>
-                               New_Occurrence_Of (Comp_Id, Loc)))));
-                  end if;
-               end if;
-
-               Produced_Check           := True;
-               Produced_Component_Check := True;
-            end if;
-
-            if Produced_Component_Check and then Has_Unchecked_Union (T) then
-               Error_Msg_NE
-                 ("invariants cannot be checked on components of "
-                  & "unchecked_union type &?", Comp_Id, T);
-            end if;
-         end Process_Record_Component;
-
-         --  Local variables
-
-         Comps : Node_Id;
-         Def   : Node_Id;
-
-      --  Start of processing for Add_Record_Component_Invariants
-
-      begin
-         --  An untagged derived type inherits the components of its parent
-         --  type. In order to avoid creating redundant invariant checks, do
-         --  not process the components now. Instead wait until the ultimate
-         --  parent of the untagged derivation chain is reached.
-
-         if not Is_Untagged_Derivation (T) then
-            Def := Type_Definition (Parent (T));
-
-            if Nkind (Def) = N_Derived_Type_Definition then
-               Def := Record_Extension_Part (Def);
-            end if;
-
-            pragma Assert (Nkind (Def) = N_Record_Definition);
-            Comps := Component_List (Def);
-
-            if Present (Comps) then
-               Process_Component_List
-                 (Comp_List => Comps,
-                  CL_Checks => Checks);
-            end if;
-         end if;
-      end Add_Record_Component_Invariants;
-
-      -------------------------
-      -- Add_Type_Invariants --
-      -------------------------
-
-      procedure Add_Type_Invariants
-        (Priv_Typ  : Entity_Id;
-         Full_Typ  : Entity_Id;
-         CRec_Typ  : Entity_Id;
-         Obj_Id    : Entity_Id;
-         Checks    : in out List_Id;
-         Inherit   : Boolean := False;
-         Priv_Item : Node_Id := Empty)
-      is
-         procedure Add_Invariant (Prag : Node_Id);
-         --  Create a runtime check to verify the invariant exression of pragma
-         --  Prag. All generated code is added to list Checks.
-
-         procedure Process_Type (T : Entity_Id; Stop_Item : Node_Id := Empty);
-         --  Generate invariant checks for type T by inspecting the rep item
-         --  chain of the type. Stop_Item denotes a rep item which once seen
-         --  will stop the inspection.
-
-         -------------------
-         -- Add_Invariant --
-         -------------------
-
-         procedure Add_Invariant (Prag : Node_Id) is
-            Rep_Typ : Entity_Id;
-            --  The replacement type used in the substitution of the current
-            --  instance of a type with the _object formal parameter.
-
-            procedure Replace_Type_Ref (N : Node_Id);
-            --  Substitute the occurrence of a type name denoted by N with a
-            --  reference to the _object formal parameter.
-
-            ----------------------
-            -- Replace_Type_Ref --
-            ----------------------
-
-            procedure Replace_Type_Ref (N : Node_Id) is
-               Nloc : constant Source_Ptr := Sloc (N);
-               Ref  : Node_Id;
-
-            begin
-               --  Decorate the reference to Ref_Typ even though it may be
-               --  rewritten further down. This is done for two reasons:
-
-               --    1) ASIS has all necessary semantic information in the
-               --    original tree.
-
-               --    2) Routines which examine properties of the Original_Node
-               --    have some semantic information.
-
-               if Nkind (N) = N_Identifier then
-                  Set_Entity (N, Rep_Typ);
-                  Set_Etype  (N, Rep_Typ);
-
-               elsif Nkind (N) = N_Selected_Component then
-                  Analyze (Prefix (N));
-                  Set_Entity (Selector_Name (N), Rep_Typ);
-                  Set_Etype  (Selector_Name (N), Rep_Typ);
-               end if;
-
-               --  Perform the following substitution:
-
-               --    Ref_Typ  -->  _object
-
-               Ref := Make_Identifier (Nloc, Chars (Obj_Id));
-               Set_Entity (Ref, Obj_Id);
-               Set_Etype  (Ref, Rep_Typ);
-
-               --  When the pragma denotes a class-wide invariant, perform the
-               --  following substitution:
-
-               --    Rep_Typ  -->  Rep_Typ'Class (_object)
-
-               if Class_Present (Prag) then
-                  Ref :=
-                    Make_Type_Conversion (Nloc,
-                      Subtype_Mark =>
-                        Make_Attribute_Reference (Nloc,
-                          Prefix         =>
-                            New_Occurrence_Of (Rep_Typ, Nloc),
-                          Attribute_Name => Name_Class),
-                      Expression   => Ref);
-               end if;
-
-               Rewrite (N, Ref);
-               Set_Comes_From_Source (N, True);
-            end Replace_Type_Ref;
-
-            procedure Replace_Type_Refs is
-              new Replace_Type_References_Generic (Replace_Type_Ref);
-
-            --  Local variables
-
-            Asp  : constant Node_Id    := Corresponding_Aspect (Prag);
-            Nam  : constant Name_Id    := Original_Aspect_Pragma_Name (Prag);
-            Ploc : constant Source_Ptr := Sloc (Prag);
-
-            Arg1      : Node_Id;
-            Arg2      : Node_Id;
-            Arg3      : Node_Id;
-            ASIS_Expr : Node_Id;
-            Assoc     : List_Id;
-            Expr      : Node_Id;
-            Str       : String_Id;
-
-         --  Start of processing for Add_Invariant
-
-         begin
-            --  Nothing to do if the pragma was already processed
-
-            if Contains (Pragmas_Seen, Prag) then
-               return;
-            end if;
-
-            --  Extract the arguments of the invariant pragma
-
-            Arg1 := First (Pragma_Argument_Associations (Prag));
-            Arg2 := Next (Arg1);
-            Arg3 := Next (Arg2);
-
-            Arg1 := Get_Pragma_Arg (Arg1);
-            Arg2 := Get_Pragma_Arg (Arg2);
-
-            --  The pragma applies to the partial view
-
-            if Present (Priv_Typ) and then Entity (Arg1) = Priv_Typ then
-               Rep_Typ := Priv_Typ;
-
-            --  The pragma applies to the full view
-
-            elsif Present (Full_Typ) and then Entity (Arg1) = Full_Typ then
-               Rep_Typ := Full_Typ;
-
-            --  Otherwise the pragma applies to a parent type in which case it
-            --  will be processed at a later stage by Add_Parent_Invariants or
-            --  Add_Interface_Invariants.
-
-            else
-               return;
-            end if;
-
-            --  Nothing to do when the caller requests the processing of all
-            --  inherited class-wide invariants, but the pragma does not fall
-            --  in this category.
-
-            if Inherit and then not Class_Present (Prag) then
-               return;
-            end if;
-
-            Expr := New_Copy_Tree (Arg2);
-
-            --  Substitute all references to type Rep_Typ with references to
-            --  the _object formal parameter.
-
-            Replace_Type_Refs (Expr, Rep_Typ);
-
-            --  Additional processing for non-class-wide invariants
-
-            if not Inherit then
-
-               --  Preanalyze the invariant expression to detect errors and at
-               --  the same time capture the visibility of the proper package
-               --  part.
-
-               --  Historical note: the old implementation of invariants used
-               --  node N as the parent, but a package specification as parent
-               --  of an expression is bizarre.
-
-               Set_Parent (Expr, Parent (Arg2));
-               Preanalyze_Assert_Expression (Expr, Any_Boolean);
-
-               --  If the pragma comes from an aspect specification, replace
-               --  the saved expression because all type references must be
-               --  substituted for the call to Preanalyze_Spec_Expression in
-               --  Check_Aspect_At_xxx routines.
-
-               if Present (Asp) then
-                  Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
-               end if;
-
-               --  Analyze the original invariant expression for ASIS
-
-               if ASIS_Mode then
-                  ASIS_Expr := Empty;
-
-                  if Comes_From_Source (Prag) then
-                     ASIS_Expr := Arg2;
-                  elsif Present (Asp) then
-                     ASIS_Expr := Expression (Asp);
-                  end if;
-
-                  if Present (ASIS_Expr) then
-                     Replace_Type_Refs (ASIS_Expr, Rep_Typ);
-                     Preanalyze_Assert_Expression (ASIS_Expr, Any_Boolean);
-                  end if;
-               end if;
-
-               --  A class-wide invariant may be inherited in a separate unit,
-               --  where the corresponding expression cannot be resolved by
-               --  visibility, because it refers to a local function. Propagate
-               --  semantic information to the original representation item, to
-               --  be used when an invariant procedure for a derived type is
-               --  constructed.
-
-               --  ??? Unclear how to handle class-wide invariants that are not
-               --  function calls.
-
-               if Class_Present (Prag)
-                 and then Nkind (Expr) = N_Function_Call
-                 and then Nkind (Arg2) = N_Indexed_Component
-               then
-                  Rewrite (Arg2,
-                    Make_Function_Call (Ploc,
-                      Name                   =>
-                        New_Occurrence_Of (Entity (Name (Expr)), Ploc),
-                      Parameter_Associations => Expressions (Arg2)));
-               end if;
-            end if;
-
-            --  The invariant is ignored, nothing left to do
-
-            if Is_Ignored (Prag) then
-               null;
-
-            --  Otherwise the invariant is checked. Build a Check pragma to
-            --  verify the expression at runtime.
-
-            else
-               Assoc := New_List (
-                 Make_Pragma_Argument_Association (Ploc,
-                   Expression => Make_Identifier (Ploc, Nam)),
-                 Make_Pragma_Argument_Association (Ploc,
-                   Expression => Expr));
-
-               --  Handle the String argument (if any)
-
-               if Present (Arg3) then
-                  Str := Strval (Get_Pragma_Arg (Arg3));
-
-                  --  When inheriting an invariant, modify the message from
-                  --  "failed invariant" to "failed inherited invariant".
-
-                  if Inherit then
-                     String_To_Name_Buffer (Str);
-
-                     if Name_Buffer (1 .. 16) = "failed invariant" then
-                        Insert_Str_In_Name_Buffer ("inherited ", 8);
-                        Str := String_From_Name_Buffer;
-                     end if;
-                  end if;
-
-                  Append_To (Assoc,
-                    Make_Pragma_Argument_Association (Ploc,
-                      Expression => Make_String_Literal (Ploc, Str)));
-               end if;
-
-               --  Generate:
-               --    pragma Check (<Nam>, <Expr>, <Str>);
-
-               Append_New_To (Checks,
-                 Make_Pragma (Ploc,
-                   Chars                        => Name_Check,
-                   Pragma_Argument_Associations => Assoc));
-            end if;
-
-            --  Output an info message when inheriting an invariant and the
-            --  listing option is enabled.
-
-            if Inherit and Opt.List_Inherited_Aspects then
-               Error_Msg_Sloc := Sloc (Prag);
-               Error_Msg_N
-                 ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
-            end if;
-
-            --  Add the pragma to the list of processed pragmas
-
-            Append_New_Elmt (Prag, Pragmas_Seen);
-            Produced_Check := True;
-         end Add_Invariant;
-
-         ------------------
-         -- Process_Type --
-         ------------------
-
-         procedure Process_Type
-           (T         : Entity_Id;
-            Stop_Item : Node_Id := Empty)
-         is
-            Rep_Item : Node_Id;
-
-         begin
-            Rep_Item := First_Rep_Item (T);
-            while Present (Rep_Item) loop
-               if Nkind (Rep_Item) = N_Pragma
-                 and then Pragma_Name (Rep_Item) = Name_Invariant
-               then
-                  --  Stop the traversal of the rep item chain once a specific
-                  --  item is encountered.
-
-                  if Present (Stop_Item) and then Rep_Item = Stop_Item then
-                     exit;
-
-                  --  Otherwise generate an invariant check
-
-                  else
-                     Add_Invariant (Rep_Item);
-                  end if;
-               end if;
-
-               Next_Rep_Item (Rep_Item);
-            end loop;
-         end Process_Type;
-
-      --  Start of processing for Add_Type_Invariants
-
-      begin
-         --  Process the invariants of the partial view
-
-         if Present (Priv_Typ) then
-            Process_Type (Priv_Typ);
-         end if;
-
-         --  Process the invariants of the full view
-
-         if Present (Full_Typ) then
-            Process_Type (Full_Typ, Stop_Item => Priv_Item);
-
-            --  Process the elements of an array type
-
-            if Is_Array_Type (Full_Typ) then
-               Add_Array_Component_Invariants (Full_Typ, Obj_Id, Checks);
-
-            --  Process the components of a record type
-
-            elsif Ekind (Full_Typ) = E_Record_Type then
-               Add_Record_Component_Invariants (Full_Typ, Obj_Id, Checks);
-            end if;
-         end if;
-
-         --  Process the components of a corresponding record type
-
-         if Present (CRec_Typ) then
-            Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Checks);
-         end if;
-      end Add_Type_Invariants;
-
-      ------------------------------------
-      -- Is_Untagged_Private_Derivation --
-      ------------------------------------
-
-      function Is_Untagged_Private_Derivation
-        (Priv_Typ : Entity_Id;
-         Full_Typ : Entity_Id) return Boolean
-      is
-      begin
-         return
-           Present (Priv_Typ)
-             and then Is_Untagged_Derivation (Priv_Typ)
-             and then Is_Private_Type (Etype (Priv_Typ))
-             and then Present (Full_Typ)
-             and then Is_Itype (Full_Typ);
-      end Is_Untagged_Private_Derivation;
-
-      --  Local variables
-
-      Dummy        : Entity_Id;
-      Mode         : Ghost_Mode_Type;
-      Priv_Item    : Node_Id;
-      Proc_Body    : Node_Id;
-      Proc_Body_Id : Entity_Id;
-      Proc_Decl    : Node_Id;
-      Proc_Id      : Entity_Id;
-      Stmts        : List_Id := No_List;
-
-      CRec_Typ : Entity_Id;
-      --  The corresponding record type of Full_Typ
-
-      Full_Proc : Entity_Id;
-      --  The entity of the "full" invariant procedure
-
-      Full_Typ : Entity_Id;
-      --  The full view of the working type
-
-      Obj_Id : Entity_Id;
-      --  The _object formal parameter of the invariant procedure
-
-      Part_Proc : Entity_Id;
-      --  The entity of the "partial" invariant procedure
-
-      Priv_Typ : Entity_Id;
-      --  The partial view of the working type
-
-      Work_Typ : Entity_Id;
-      --  The working type
-
-   --  Start of processing for Build_Invariant_Procedure_Body
-
-   begin
-      Work_Typ := Typ;
-
-      --  The input type denotes the implementation base type of a constrained
-      --  array type. Work with the first subtype as all invariant pragmas are
-      --  on its rep item chain.
-
-      if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
-         Work_Typ := First_Subtype (Work_Typ);
-
-      --  The input type denotes the corresponding record type of a protected
-      --  or task type. Work with the concurrent type because the corresponding
-      --  record type may not be visible to clients of the type.
-
-      elsif Ekind (Work_Typ) = E_Record_Type
-        and then Is_Concurrent_Record_Type (Work_Typ)
-      then
-         Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
-      end if;
-
-      --  The working type may be subject to pragma Ghost. Set the mode now to
-      --  ensure that the invariant procedure is properly marked as Ghost.
-
-      Set_Ghost_Mode (Work_Typ, Mode);
-
-      --  The type must either have invariants of its own, inherit class-wide
-      --  invariants from parent types or interfaces, or be an array or record
-      --  type whose components have invariants.
-
-      pragma Assert (Has_Invariants (Work_Typ));
-
-      --  Nothing to do for interface types as their class-wide invariants are
-      --  inherited by implementing types.
-
-      if Is_Interface (Work_Typ) then
-         goto Leave;
-      end if;
-
-      --  Obtain both views of the type
-
-      Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ);
-
-      --  The caller requests a body for the partial invariant procedure
-
-      if Partial_Invariant then
-         Full_Proc := Invariant_Procedure (Work_Typ);
-         Proc_Id   := Partial_Invariant_Procedure (Work_Typ);
-
-         --  The "full" invariant procedure body was already created
-
-         if Present (Full_Proc)
-           and then Present
-                      (Corresponding_Body (Unit_Declaration_Node (Full_Proc)))
-         then
-            --  This scenario happens only when the type is an untagged
-            --  derivation from a private parent and the underlying full
-            --  view was processed before the partial view.
-
-            pragma Assert
-              (Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ));
-
-            --  Nothing to do because the processing of the underlying full
-            --  view already checked the invariants of the partial view.
-
-            goto Leave;
-         end if;
-
-         --  Create a declaration for the "partial" invariant procedure if it
-         --  is not available.
-
-         if No (Proc_Id) then
-            Build_Invariant_Procedure_Declaration
-              (Typ               => Work_Typ,
-               Partial_Invariant => True);
-
-            Proc_Id := Partial_Invariant_Procedure (Work_Typ);
-         end if;
-
-      --  The caller requests a body for the "full" invariant procedure
-
-      else
-         Proc_Id   := Invariant_Procedure (Work_Typ);
-         Part_Proc := Partial_Invariant_Procedure (Work_Typ);
-
-         --  Create a declaration for the "full" invariant procedure if it is
-         --  not available.
-
-         if No (Proc_Id) then
-            Build_Invariant_Procedure_Declaration (Work_Typ);
-            Proc_Id := Invariant_Procedure (Work_Typ);
-         end if;
-      end if;
-
-      --  At this point there should be an invariant procedure declaration
-
-      pragma Assert (Present (Proc_Id));
-      Proc_Decl := Unit_Declaration_Node (Proc_Id);
-
-      --  Nothing to do if the invariant procedure already has a body
-
-      if Present (Corresponding_Body (Proc_Decl)) then
-         goto Leave;
-      end if;
-
-      --  Emulate the environment of the invariant procedure by installing
-      --  its scope and formal parameters. Note that this is not needed, but
-      --  having the scope of the invariant procedure installed helps with
-      --  the detection of invariant-related errors.
-
-      Push_Scope (Proc_Id);
-      Install_Formals (Proc_Id);
-
-      Obj_Id := First_Formal (Proc_Id);
-      pragma Assert (Present (Obj_Id));
-
-      --  The "partial" invariant procedure verifies the invariants of the
-      --  partial view only.
-
-      if Partial_Invariant then
-         pragma Assert (Present (Priv_Typ));
-
-         Add_Type_Invariants
-           (Priv_Typ => Priv_Typ,
-            Full_Typ => Empty,
-            CRec_Typ => Empty,
-            Obj_Id   => Obj_Id,
-            Checks   => Stmts);
-
-      --  Otherwise the "full" invariant procedure verifies the invariants of
-      --  the full view, all array or record components, as well as class-wide
-      --  invariants inherited from parent types or interfaces. In addition, it
-      --  indirectly verifies the invariants of the partial view by calling the
-      --  "partial" invariant procedure.
-
-      else
-         pragma Assert (Present (Full_Typ));
-
-         --  Check the invariants of the partial view by calling the "partial"
-         --  invariant procedure. Generate:
-
-         --    <Work_Typ>Partial_Invariant (_object);
-
-         if Present (Part_Proc) then
-            Append_New_To (Stmts,
-              Make_Procedure_Call_Statement (Loc,
-                Name                   => New_Occurrence_Of (Part_Proc, Loc),
-                Parameter_Associations => New_List (
-                  New_Occurrence_Of (Obj_Id, Loc))));
-
-            Produced_Check := True;
-         end if;
-
-         Priv_Item := Empty;
-
-         --  Derived subtypes do not have a partial view
-
-         if Present (Priv_Typ) then
-
-            --  The processing of the "full" invariant procedure intentionally
-            --  skips the partial view because a) this may result in changes of
-            --  visibility and b) lead to duplicate checks. However, when the
-            --  full view is the underlying full view of an untagged derived
-            --  type whose parent type is private, partial invariants appear on
-            --  the rep item chain of the partial view only.
-
-            --    package Pack_1 is
-            --       type Root ... is private;
-            --    private
-            --       <full view of Root>
-            --    end Pack_1;
-
-            --    with Pack_1;
-            --    package Pack_2 is
-            --       type Child is new Pack_1.Root with Type_Invariant => ...;
-            --       <underlying full view of Child>
-            --    end Pack_2;
-
-            --  As a result, the processing of the full view must also consider
-            --  all invariants of the partial view.
-
-            if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then
-               null;
-
-            --  Otherwise the invariants of the partial view are ignored
-
-            else
-               --  Note that the rep item chain is shared between the partial
-               --  and full views of a type. To avoid processing the invariants
-               --  of the partial view, signal the logic to stop when the first
-               --  rep item of the partial view has been reached.
-
-               Priv_Item := First_Rep_Item (Priv_Typ);
-
-               --  Ignore the invariants of the partial view by eliminating the
-               --  view.
-
-               Priv_Typ := Empty;
-            end if;
-         end if;
-
-         --  Process the invariants of the full view and in certain cases those
-         --  of the partial view. This also handles any invariants on array or
-         --  record components.
-
-         Add_Type_Invariants
-           (Priv_Typ  => Priv_Typ,
-            Full_Typ  => Full_Typ,
-            CRec_Typ  => CRec_Typ,
-            Obj_Id    => Obj_Id,
-            Checks    => Stmts,
-            Priv_Item => Priv_Item);
-
-         --  Process the inherited class-wide invariants of all parent types.
-         --  This also handles any invariants on record components.
-
-         Add_Parent_Invariants (Full_Typ, Obj_Id, Stmts);
-
-         --  Process the inherited class-wide invariants of all implemented
-         --  interface types.
-
-         Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts);
-      end if;
-
-      End_Scope;
-
-      --  At this point there should be at least one invariant check. If this
-      --  is not the case, then the invariant-related flags were not properly
-      --  set, or there is a missing invariant procedure on one of the array
-      --  or record components.
-
-      pragma Assert (Produced_Check);
-
-      --  Account for the case where assertions are disabled or all invariant
-      --  checks are subject to Assertion_Policy Ignore. Produce a completing
-      --  empty body.
-
-      if No (Stmts) then
-         Stmts := New_List (Make_Null_Statement (Loc));
-      end if;
-
-      --  Generate:
-      --    procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>) is
-      --    begin
-      --       <Stmts>
-      --    end <Work_Typ>[Partial_]Invariant;
-
-      Proc_Body :=
-        Make_Subprogram_Body (Loc,
-          Specification                =>
-            Copy_Subprogram_Spec (Parent (Proc_Id)),
-          Declarations                 => Empty_List,
-            Handled_Statement_Sequence =>
-              Make_Handled_Sequence_Of_Statements (Loc,
-                Statements => Stmts));
-      Proc_Body_Id := Defining_Entity (Proc_Body);
-
-      --  Perform minor decoration in case the body is not analyzed
-
-      Set_Ekind (Proc_Body_Id, E_Subprogram_Body);
-      Set_Etype (Proc_Body_Id, Standard_Void_Type);
-      Set_Scope (Proc_Body_Id, Current_Scope);
-
-      --  Link both spec and body to avoid generating duplicates
-
-      Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
-      Set_Corresponding_Spec (Proc_Body, Proc_Id);
-
-      --  The body should not be inserted into the tree when the context is
-      --  ASIS or a generic unit because it is not part of the template. Note
-      --  that the body must still be generated in order to resolve the
-      --  invariants.
-
-      if ASIS_Mode or Inside_A_Generic then
-         null;
-
-      --  Semi-insert the body into the tree for GNATprove by setting its
-      --  Parent field. This allows for proper upstream tree traversals.
-
-      elsif GNATprove_Mode then
-         Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
-
-      --  Otherwise the body is part of the freezing actions of the type
-
-      else
-         Append_Freeze_Action (Work_Typ, Proc_Body);
-      end if;
-
-   <<Leave>>
-      Restore_Ghost_Mode (Mode);
-   end Build_Invariant_Procedure_Body;
-
-   -------------------------------------------
-   -- Build_Invariant_Procedure_Declaration --
-   -------------------------------------------
-
-   --  WARNING: This routine manages Ghost regions. Return statements must be
-   --  replaced by gotos which jump to the end of the routine and restore the
-   --  Ghost mode.
-
-   procedure Build_Invariant_Procedure_Declaration
-     (Typ               : Entity_Id;
-      Partial_Invariant : Boolean := False)
-   is
-      Loc : constant Source_Ptr := Sloc (Typ);
-
-      Mode      : Ghost_Mode_Type;
-      Proc_Decl : Node_Id;
-      Proc_Id   : Entity_Id;
-      Proc_Nam  : Name_Id;
-      Typ_Decl  : Node_Id;
-
-      CRec_Typ : Entity_Id;
-      --  The corresponding record type of Full_Typ
-
-      Full_Base : Entity_Id;
-      --  The base type of Full_Typ
-
-      Full_Typ : Entity_Id;
-      --  The full view of working type
-
-      Obj_Id : Entity_Id;
-      --  The _object formal parameter of the invariant procedure
-
-      Priv_Typ : Entity_Id;
-      --  The partial view of working type
-
-      Work_Typ : Entity_Id;
-      --  The working type
-
-   begin
-      Work_Typ := Typ;
-
-      --  The input type denotes the implementation base type of a constrained
-      --  array type. Work with the first subtype as all invariant pragmas are
-      --  on its rep item chain.
-
-      if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
-         Work_Typ := First_Subtype (Work_Typ);
-
-      --  The input denotes the corresponding record type of a protected or a
-      --  task type. Work with the concurrent type because the corresponding
-      --  record type may not be visible to clients of the type.
-
-      elsif Ekind (Work_Typ) = E_Record_Type
-        and then Is_Concurrent_Record_Type (Work_Typ)
-      then
-         Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
-      end if;
-
-      --  The working type may be subject to pragma Ghost. Set the mode now to
-      --  ensure that the invariant procedure is properly marked as Ghost.
-
-      Set_Ghost_Mode (Work_Typ, Mode);
-
-      --  The type must either have invariants of its own, inherit class-wide
-      --  invariants from parent or interface types, or be an array or record
-      --  type whose components have invariants.
-
-      pragma Assert (Has_Invariants (Work_Typ));
-
-      --  Nothing to do for interface types as their class-wide invariants are
-      --  inherited by implementing types.
-
-      if Is_Interface (Work_Typ) then
-         goto Leave;
-
-      --  Nothing to do if the type already has a "partial" invariant procedure
-
-      elsif Partial_Invariant then
-         if Present (Partial_Invariant_Procedure (Work_Typ)) then
-            goto Leave;
-         end if;
-
-      --  Nothing to do if the type already has a "full" invariant procedure
-
-      elsif Present (Invariant_Procedure (Work_Typ)) then
-         goto Leave;
-      end if;
-
-      --  The caller requests the declaration of the "partial" invariant
-      --  procedure.
-
-      if Partial_Invariant then
-         Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_Invariant");
-
-      --  Otherwise the caller requests the declaration of the "full" invariant
-      --  procedure.
-
-      else
-         Proc_Nam := New_External_Name (Chars (Work_Typ), "Invariant");
-      end if;
-
-      Proc_Id := Make_Defining_Identifier (Loc, Chars => Proc_Nam);
-
-      --  Perform minor decoration in case the declaration is not analyzed
-
-      Set_Ekind (Proc_Id, E_Procedure);
-      Set_Etype (Proc_Id, Standard_Void_Type);
-      Set_Scope (Proc_Id, Current_Scope);
-
-      if Partial_Invariant then
-         Set_Is_Partial_Invariant_Procedure (Proc_Id);
-         Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
-      else
-         Set_Is_Invariant_Procedure (Proc_Id);
-         Set_Invariant_Procedure (Work_Typ, Proc_Id);
-      end if;
-
-      --  The invariant procedure requires debug info when the invariants are
-      --  subject to Source Coverage Obligations.
-
-      if Opt.Generate_SCO then
-         Set_Needs_Debug_Info (Proc_Id);
-      end if;
-
-      --  Obtain all views of the input type
-
-      Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
-
-      --  Associate the invariant procedure with all views
-
-      Propagate_Invariant_Attributes (Priv_Typ,  From_Typ => Work_Typ);
-      Propagate_Invariant_Attributes (Full_Typ,  From_Typ => Work_Typ);
-      Propagate_Invariant_Attributes (Full_Base, From_Typ => Work_Typ);
-      Propagate_Invariant_Attributes (CRec_Typ,  From_Typ => Work_Typ);
-
-      --  The declaration of the invariant procedure is inserted after the
-      --  declaration of the partial view as this allows for proper external
-      --  visibility.
-
-      if Present (Priv_Typ) then
-         Typ_Decl := Declaration_Node (Priv_Typ);
-
-      --  Derived types with the full view as parent do not have a partial
-      --  view. Insert the invariant procedure after the derived type.
-
-      else
-         Typ_Decl := Declaration_Node (Full_Typ);
-      end if;
-
-      --  The type should have a declarative node
-
-      pragma Assert (Present (Typ_Decl));
-
-      --  Create the formal parameter which emulates the variable-like behavior
-      --  of the current type instance.
-
-      Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
-
-      --  Perform minor decoration in case the declaration is not analyzed
-
-      Set_Ekind (Obj_Id, E_In_Parameter);
-      Set_Etype (Obj_Id, Work_Typ);
-      Set_Scope (Obj_Id, Proc_Id);
-
-      Set_First_Entity (Proc_Id, Obj_Id);
-
-      --  Generate:
-      --    procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>);
-
-      Proc_Decl :=
-        Make_Subprogram_Declaration (Loc,
-          Specification =>
-            Make_Procedure_Specification (Loc,
-              Defining_Unit_Name       => Proc_Id,
-              Parameter_Specifications => New_List (
-                Make_Parameter_Specification (Loc,
-                  Defining_Identifier => Obj_Id,
-                  Parameter_Type      =>
-                    New_Occurrence_Of (Work_Typ, Loc)))));
-
-      --  The declaration should not be inserted into the tree when the context
-      --  is ASIS or a generic unit because it is not part of the template.
-
-      if ASIS_Mode or Inside_A_Generic then
-         null;
-
-      --  Semi-insert the declaration into the tree for GNATprove by setting
-      --  its Parent field. This allows for proper upstream tree traversals.
-
-      elsif GNATprove_Mode then
-         Set_Parent (Proc_Decl, Parent (Typ_Decl));
-
-      --  Otherwise insert the declaration
-
-      else
-         pragma Assert (Present (Typ_Decl));
-         Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
-      end if;
-
-   <<Leave>>
-      Restore_Ghost_Mode (Mode);
-   end Build_Invariant_Procedure_Declaration;
-
    ---------------------
    -- Build_Late_Proc --
    ---------------------
diff --git a/gcc/ada/exp_ch7.ads b/gcc/ada/exp_ch7.ads
index 0db3df5..b0a8b0b 100644
--- a/gcc/ada/exp_ch7.ads
+++ b/gcc/ada/exp_ch7.ads
@@ -118,21 +118,6 @@ package Exp_Ch7 is
    --  finalization master must be analyzed. Insertion_Node is the insertion
    --  point before which the master is to be inserted.
 
-   procedure Build_Invariant_Procedure_Body
-     (Typ               : Entity_Id;
-      Partial_Invariant : Boolean := False);
-   --  Create the body of the procedure which verifies the invariants of type
-   --  Typ at runtime. Flag Partial_Invariant should be set when Typ denotes a
-   --  private type, otherwise it is assumed that Typ denotes the full view of
-   --  a private type.
-
-   procedure Build_Invariant_Procedure_Declaration
-     (Typ               : Entity_Id;
-      Partial_Invariant : Boolean := False);
-   --  Create the declaration of the procedure which verifies the invariants of
-   --  type Typ at runtime. Flag Partial_Invariant should be set when building
-   --  the invariant procedure for a private type.
-
    procedure Build_Late_Proc (Typ : Entity_Id; Nam : Name_Id);
    --  Build one controlling procedure when a late body overrides one of the
    --  controlling operations.
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 638f574..bb36ce99 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1949,6 +1949,1383 @@ package body Exp_Util is
       Restore_Ghost_Mode (Mode);
    end Build_DIC_Procedure_Declaration;
 
+   ------------------------------------
+   -- Build_Invariant_Procedure_Body --
+   ------------------------------------
+
+   --  WARNING: This routine manages Ghost regions. Return statements must be
+   --  replaced by gotos which jump to the end of the routine and restore the
+   --  Ghost mode.
+
+   procedure Build_Invariant_Procedure_Body
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False)
+   is
+      Loc : constant Source_Ptr := Sloc (Typ);
+
+      Pragmas_Seen : Elist_Id := No_Elist;
+      --  This list contains all invariant pragmas processed so far. The list
+      --  is used to avoid generating redundant invariant checks.
+
+      Produced_Check : Boolean := False;
+      --  This flag tracks whether the type has produced at least one invariant
+      --  check. The flag is used as a sanity check at the end of the routine.
+
+      --  NOTE: most of the routines in Build_Invariant_Procedure_Body are
+      --  intentionally unnested to avoid deep indentation of code.
+
+      --  NOTE: all Add_xxx_Invariants routines are reactive. In other words
+      --  they emit checks, loops (for arrays) and case statements (for record
+      --  variant parts) only when there are invariants to verify. This keeps
+      --  the body of the invariant procedure free from useless code.
+
+      procedure Add_Array_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each component of array type T.
+      --  Obj_Id denotes the entity of the _object formal parameter of the
+      --  invariant procedure. All created checks are added to list Checks.
+
+      procedure Add_Interface_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each inherited class-wide invariant
+      --  coming from all interfaces implemented by type T. Obj_Id denotes the
+      --  entity of the _object formal parameter of the invariant procedure.
+      --  All created checks are added to list Checks.
+
+      procedure Add_Parent_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each inherited class-wide invariant
+      --  coming from all parent types of type T. Obj_Id denotes the entity of
+      --  the _object formal parameter of the invariant procedure. All created
+      --  checks are added to list Checks.
+
+      procedure Add_Record_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each component of record type T.
+      --  Obj_Id denotes the entity of the _object formal parameter of the
+      --  invariant procedure. All created checks are added to list Checks.
+
+      procedure Add_Type_Invariants
+        (Priv_Typ  : Entity_Id;
+         Full_Typ  : Entity_Id;
+         CRec_Typ  : Entity_Id;
+         Obj_Id    : Entity_Id;
+         Checks    : in out List_Id;
+         Inherit   : Boolean := False;
+         Priv_Item : Node_Id := Empty);
+      --  Generate an invariant check for each invariant found in one of the
+      --  following types (if available):
+      --
+      --    Priv_Typ - the partial view of a type
+      --    Full_Typ - the full view of a type
+      --    CRec_Typ - the corresponding record of a protected or a task type
+      --
+      --  Obj_Id denotes the entity of the _object formal parameter of the
+      --  invariant procedure. All created checks are added to list Checks.
+      --  Flag Inherit should be set when generating invariant checks for
+      --  inherited class-wide invariants. Priv_Item denotes the first rep
+      --  item of the private type.
+
+      ------------------------------------
+      -- Add_Array_Component_Invariants --
+      ------------------------------------
+
+      procedure Add_Array_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         Comp_Typ : constant Entity_Id := Component_Type (T);
+         Dims     : constant Pos       := Number_Dimensions (T);
+
+         procedure Process_Array_Component
+           (Indices     : List_Id;
+            Comp_Checks : in out List_Id);
+         --  Generate an invariant check for an array component identified by
+         --  the indices in list Indices. All created checks are added to list
+         --  Comp_Checks.
+
+         procedure Process_One_Dimension
+           (Dim        : Pos;
+            Indices    : List_Id;
+            Dim_Checks : in out List_Id);
+         --  Generate a loop over the Nth dimension Dim of an array type. List
+         --  Indices contains all array indices for the dimension. All created
+         --  checks are added to list Dim_Checks.
+
+         -----------------------------
+         -- Process_Array_Component --
+         -----------------------------
+
+         procedure Process_Array_Component
+           (Indices     : List_Id;
+            Comp_Checks : in out List_Id)
+         is
+            Proc_Id : Entity_Id;
+
+         begin
+            if Has_Invariants (Comp_Typ) then
+
+               --  In GNATprove mode, the component invariants are checked by
+               --  other means. They should not be added to the array type
+               --  invariant procedure, so that the procedure can be used to
+               --  check the array type invariants if any.
+
+               if GNATprove_Mode then
+                  null;
+
+               else
+                  Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
+
+                  --  The component type should have an invariant procedure
+                  --  if it has invariants of its own or inherits class-wide
+                  --  invariants from parent or interface types.
+
+                  pragma Assert (Present (Proc_Id));
+
+                  --  Generate:
+                  --    <Comp_Typ>Invariant (_object (<Indices>));
+
+                  --  Note that the invariant procedure may have a null body if
+                  --  assertions are disabled or Assertion_Policy Ignore is in
+                  --  effect.
+
+                  if not Has_Null_Body (Proc_Id) then
+                     Append_New_To (Comp_Checks,
+                       Make_Procedure_Call_Statement (Loc,
+                         Name                   =>
+                           New_Occurrence_Of (Proc_Id, Loc),
+                         Parameter_Associations => New_List (
+                           Make_Indexed_Component (Loc,
+                             Prefix      => New_Occurrence_Of (Obj_Id, Loc),
+                             Expressions => New_Copy_List (Indices)))));
+                  end if;
+               end if;
+
+               Produced_Check := True;
+            end if;
+         end Process_Array_Component;
+
+         ---------------------------
+         -- Process_One_Dimension --
+         ---------------------------
+
+         procedure Process_One_Dimension
+           (Dim        : Pos;
+            Indices    : List_Id;
+            Dim_Checks : in out List_Id)
+         is
+            Comp_Checks : List_Id := No_List;
+            Index       : Entity_Id;
+
+         begin
+            --  Generate the invariant checks for the array component after all
+            --  dimensions have produced their respective loops.
+
+            if Dim > Dims then
+               Process_Array_Component
+                 (Indices     => Indices,
+                  Comp_Checks => Dim_Checks);
+
+            --  Otherwise create a loop for the current dimension
+
+            else
+               --  Create a new loop variable for each dimension
+
+               Index :=
+                 Make_Defining_Identifier (Loc,
+                   Chars => New_External_Name ('I', Dim));
+               Append_To (Indices, New_Occurrence_Of (Index, Loc));
+
+               Process_One_Dimension
+                 (Dim        => Dim + 1,
+                  Indices    => Indices,
+                  Dim_Checks => Comp_Checks);
+
+               --  Generate:
+               --    for I<Dim> in _object'Range (<Dim>) loop
+               --       <Comp_Checks>
+               --    end loop;
+
+               --  Note that the invariant procedure may have a null body if
+               --  assertions are disabled or Assertion_Policy Ignore is in
+               --  effect.
+
+               if Present (Comp_Checks) then
+                  Append_New_To (Dim_Checks,
+                    Make_Implicit_Loop_Statement (T,
+                      Identifier       => Empty,
+                      Iteration_Scheme =>
+                        Make_Iteration_Scheme (Loc,
+                          Loop_Parameter_Specification =>
+                            Make_Loop_Parameter_Specification (Loc,
+                              Defining_Identifier         => Index,
+                              Discrete_Subtype_Definition =>
+                                Make_Attribute_Reference (Loc,
+                                  Prefix         =>
+                                    New_Occurrence_Of (Obj_Id, Loc),
+                                  Attribute_Name => Name_Range,
+                                  Expressions    => New_List (
+                                    Make_Integer_Literal (Loc, Dim))))),
+
+                      Statements => Comp_Checks));
+               end if;
+            end if;
+         end Process_One_Dimension;
+
+      --  Start of processing for Add_Array_Component_Invariants
+
+      begin
+         Process_One_Dimension
+           (Dim        => 1,
+            Indices    => New_List,
+            Dim_Checks => Checks);
+      end Add_Array_Component_Invariants;
+
+      ------------------------------
+      -- Add_Interface_Invariants --
+      ------------------------------
+
+      procedure Add_Interface_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         Iface_Elmt : Elmt_Id;
+         Ifaces     : Elist_Id;
+
+      begin
+         if Is_Tagged_Type (T) then
+            Collect_Interfaces (T, Ifaces);
+
+            --  Process the class-wide invariants of all implemented interfaces
+
+            Iface_Elmt := First_Elmt (Ifaces);
+            while Present (Iface_Elmt) loop
+               Add_Type_Invariants
+                 (Priv_Typ => Empty,
+                  Full_Typ => Node (Iface_Elmt),
+                  CRec_Typ => Empty,
+                  Obj_Id   => Obj_Id,
+                  Checks   => Checks,
+                  Inherit  => True);
+
+               Next_Elmt (Iface_Elmt);
+            end loop;
+         end if;
+      end Add_Interface_Invariants;
+
+      ---------------------------
+      -- Add_Parent_Invariants --
+      ---------------------------
+
+      procedure Add_Parent_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         Dummy_1 : Entity_Id;
+         Dummy_2 : Entity_Id;
+
+         Curr_Typ : Entity_Id;
+         --  The entity of the current type being examined
+
+         Full_Typ : Entity_Id;
+         --  The full view of Par_Typ
+
+         Par_Typ : Entity_Id;
+         --  The entity of the parent type
+
+         Priv_Typ : Entity_Id;
+         --  The partial view of Par_Typ
+
+      begin
+         --  Do not process array types because they cannot have true parent
+         --  types. This also prevents the generation of a duplicate invariant
+         --  check when the input type is an array base type because its Etype
+         --  denotes the first subtype, both of which share the same component
+         --  type.
+
+         if Is_Array_Type (T) then
+            return;
+         end if;
+
+         --  Climb the parent type chain
+
+         Curr_Typ := T;
+         loop
+            --  Do not consider subtypes as they inherit the invariants from
+            --  their base types.
+
+            Par_Typ := Base_Type (Etype (Curr_Typ));
+
+            --  Stop the climb once the root of the parent chain is reached
+
+            exit when Curr_Typ = Par_Typ;
+
+            --  Process the class-wide invariants of the parent type
+
+            Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
+
+            Add_Type_Invariants
+              (Priv_Typ => Priv_Typ,
+               Full_Typ => Full_Typ,
+               CRec_Typ => Empty,
+               Obj_Id   => Obj_Id,
+               Checks   => Checks,
+               Inherit  => True);
+
+            Curr_Typ := Par_Typ;
+         end loop;
+      end Add_Parent_Invariants;
+
+      -------------------------------------
+      -- Add_Record_Component_Invariants --
+      -------------------------------------
+
+      procedure Add_Record_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         procedure Process_Component_List
+           (Comp_List : Node_Id;
+            CL_Checks : in out List_Id);
+         --  Generate invariant checks for all record components found in
+         --  component list Comp_List, including variant parts. All created
+         --  checks are added to list CL_Checks.
+
+         procedure Process_Record_Component
+           (Comp_Id     : Entity_Id;
+            Comp_Checks : in out List_Id);
+         --  Generate an invariant check for a record component identified by
+         --  Comp_Id. All created checks are added to list Comp_Checks.
+
+         ----------------------------
+         -- Process_Component_List --
+         ----------------------------
+
+         procedure Process_Component_List
+           (Comp_List : Node_Id;
+            CL_Checks : in out List_Id)
+         is
+            Comp       : Node_Id;
+            Var        : Node_Id;
+            Var_Alts   : List_Id := No_List;
+            Var_Checks : List_Id := No_List;
+            Var_Stmts  : List_Id;
+
+            Produced_Variant_Check : Boolean := False;
+            --  This flag tracks whether the component has produced at least
+            --  one invariant check.
+
+         begin
+            --  Traverse the component items
+
+            Comp := First (Component_Items (Comp_List));
+            while Present (Comp) loop
+               if Nkind (Comp) = N_Component_Declaration then
+
+                  --  Generate the component invariant check
+
+                  Process_Record_Component
+                    (Comp_Id     => Defining_Entity (Comp),
+                     Comp_Checks => CL_Checks);
+               end if;
+
+               Next (Comp);
+            end loop;
+
+            --  Traverse the variant part
+
+            if Present (Variant_Part (Comp_List)) then
+               Var := First (Variants (Variant_Part (Comp_List)));
+               while Present (Var) loop
+                  Var_Checks := No_List;
+
+                  --  Generate invariant checks for all components and variant
+                  --  parts that qualify.
+
+                  Process_Component_List
+                    (Comp_List => Component_List (Var),
+                     CL_Checks => Var_Checks);
+
+                  --  The components of the current variant produced at least
+                  --  one invariant check.
+
+                  if Present (Var_Checks) then
+                     Var_Stmts := Var_Checks;
+                     Produced_Variant_Check := True;
+
+                  --  Otherwise there are either no components with invariants,
+                  --  assertions are disabled, or Assertion_Policy Ignore is in
+                  --  effect.
+
+                  else
+                     Var_Stmts := New_List (Make_Null_Statement (Loc));
+                  end if;
+
+                  Append_New_To (Var_Alts,
+                    Make_Case_Statement_Alternative (Loc,
+                      Discrete_Choices =>
+                        New_Copy_List (Discrete_Choices (Var)),
+                      Statements       => Var_Stmts));
+
+                  Next (Var);
+               end loop;
+
+               --  Create a case statement which verifies the invariant checks
+               --  of a particular component list depending on the discriminant
+               --  values only when there is at least one real invariant check.
+
+               if Produced_Variant_Check then
+                  Append_New_To (CL_Checks,
+                    Make_Case_Statement (Loc,
+                      Expression   =>
+                        Make_Selected_Component (Loc,
+                          Prefix        => New_Occurrence_Of (Obj_Id, Loc),
+                          Selector_Name =>
+                            New_Occurrence_Of
+                              (Entity (Name (Variant_Part (Comp_List))), Loc)),
+                      Alternatives => Var_Alts));
+               end if;
+            end if;
+         end Process_Component_List;
+
+         ------------------------------
+         -- Process_Record_Component --
+         ------------------------------
+
+         procedure Process_Record_Component
+           (Comp_Id     : Entity_Id;
+            Comp_Checks : in out List_Id)
+         is
+            Comp_Typ : constant Entity_Id := Etype (Comp_Id);
+            Proc_Id  : Entity_Id;
+
+            Produced_Component_Check : Boolean := False;
+            --  This flag tracks whether the component has produced at least
+            --  one invariant check.
+
+         begin
+            --  Nothing to do for internal component _parent. Note that it is
+            --  not desirable to check whether the component comes from source
+            --  because protected type components are relocated to an internal
+            --  corresponding record, but still need processing.
+
+            if Chars (Comp_Id) = Name_uParent then
+               return;
+            end if;
+
+            --  Verify the invariant of the component. Note that an access
+            --  type may have an invariant when it acts as the full view of a
+            --  private type and the invariant appears on the partial view. In
+            --  this case verify the access value itself.
+
+            if Has_Invariants (Comp_Typ) then
+
+               --  In GNATprove mode, the component invariants are checked by
+               --  other means. They should not be added to the record type
+               --  invariant procedure, so that the procedure can be used to
+               --  check the record type invariants if any.
+
+               if GNATprove_Mode then
+                  null;
+
+               else
+                  Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
+
+                  --  The component type should have an invariant procedure
+                  --  if it has invariants of its own or inherits class-wide
+                  --  invariants from parent or interface types.
+
+                  pragma Assert (Present (Proc_Id));
+
+                  --  Generate:
+                  --    <Comp_Typ>Invariant (T (_object).<Comp_Id>);
+
+                  --  Note that the invariant procedure may have a null body if
+                  --  assertions are disabled or Assertion_Policy Ignore is in
+                  --  effect.
+
+                  if not Has_Null_Body (Proc_Id) then
+                     Append_New_To (Comp_Checks,
+                       Make_Procedure_Call_Statement (Loc,
+                         Name                   =>
+                           New_Occurrence_Of (Proc_Id, Loc),
+                         Parameter_Associations => New_List (
+                           Make_Selected_Component (Loc,
+                             Prefix        =>
+                               Unchecked_Convert_To
+                                 (T, New_Occurrence_Of (Obj_Id, Loc)),
+                             Selector_Name =>
+                               New_Occurrence_Of (Comp_Id, Loc)))));
+                  end if;
+               end if;
+
+               Produced_Check           := True;
+               Produced_Component_Check := True;
+            end if;
+
+            if Produced_Component_Check and then Has_Unchecked_Union (T) then
+               Error_Msg_NE
+                 ("invariants cannot be checked on components of "
+                  & "unchecked_union type &?", Comp_Id, T);
+            end if;
+         end Process_Record_Component;
+
+         --  Local variables
+
+         Comps : Node_Id;
+         Def   : Node_Id;
+
+      --  Start of processing for Add_Record_Component_Invariants
+
+      begin
+         --  An untagged derived type inherits the components of its parent
+         --  type. In order to avoid creating redundant invariant checks, do
+         --  not process the components now. Instead wait until the ultimate
+         --  parent of the untagged derivation chain is reached.
+
+         if not Is_Untagged_Derivation (T) then
+            Def := Type_Definition (Parent (T));
+
+            if Nkind (Def) = N_Derived_Type_Definition then
+               Def := Record_Extension_Part (Def);
+            end if;
+
+            pragma Assert (Nkind (Def) = N_Record_Definition);
+            Comps := Component_List (Def);
+
+            if Present (Comps) then
+               Process_Component_List
+                 (Comp_List => Comps,
+                  CL_Checks => Checks);
+            end if;
+         end if;
+      end Add_Record_Component_Invariants;
+
+      -------------------------
+      -- Add_Type_Invariants --
+      -------------------------
+
+      procedure Add_Type_Invariants
+        (Priv_Typ  : Entity_Id;
+         Full_Typ  : Entity_Id;
+         CRec_Typ  : Entity_Id;
+         Obj_Id    : Entity_Id;
+         Checks    : in out List_Id;
+         Inherit   : Boolean := False;
+         Priv_Item : Node_Id := Empty)
+      is
+         procedure Add_Invariant (Prag : Node_Id);
+         --  Create a runtime check to verify the invariant exression of pragma
+         --  Prag. All generated code is added to list Checks.
+
+         procedure Process_Type (T : Entity_Id; Stop_Item : Node_Id := Empty);
+         --  Generate invariant checks for type T by inspecting the rep item
+         --  chain of the type. Stop_Item denotes a rep item which once seen
+         --  will stop the inspection.
+
+         -------------------
+         -- Add_Invariant --
+         -------------------
+
+         procedure Add_Invariant (Prag : Node_Id) is
+            Asp  : constant Node_Id    := Corresponding_Aspect (Prag);
+            Nam  : constant Name_Id    := Original_Aspect_Pragma_Name (Prag);
+            Ploc : constant Source_Ptr := Sloc (Prag);
+
+            Arg1      : Node_Id;
+            Arg2      : Node_Id;
+            Arg3      : Node_Id;
+            ASIS_Expr : Node_Id;
+            Assoc     : List_Id;
+            Expr      : Node_Id;
+            Str       : String_Id;
+
+            Rep_Typ : Entity_Id;
+            --  The replacement type used in the substitution of the current
+            --  instance of a type with the _object formal parameter.
+
+         begin
+            --  Nothing to do if the pragma was already processed
+
+            if Contains (Pragmas_Seen, Prag) then
+               return;
+            end if;
+
+            --  Extract the arguments of the invariant pragma
+
+            Arg1 := First (Pragma_Argument_Associations (Prag));
+            Arg2 := Next (Arg1);
+            Arg3 := Next (Arg2);
+
+            Arg1 := Get_Pragma_Arg (Arg1);
+            Arg2 := Get_Pragma_Arg (Arg2);
+
+            --  The pragma applies to the partial view
+
+            if Present (Priv_Typ) and then Entity (Arg1) = Priv_Typ then
+               Rep_Typ := Priv_Typ;
+
+            --  The pragma applies to the full view
+
+            elsif Present (Full_Typ) and then Entity (Arg1) = Full_Typ then
+               Rep_Typ := Full_Typ;
+
+            --  Otherwise the pragma applies to a parent type in which case it
+            --  will be processed at a later stage by Add_Parent_Invariants or
+            --  Add_Interface_Invariants.
+
+            else
+               return;
+            end if;
+
+            --  Nothing to do when the caller requests the processing of all
+            --  inherited class-wide invariants, but the pragma does not fall
+            --  in this category.
+
+            if Inherit and then not Class_Present (Prag) then
+               return;
+            end if;
+
+            Expr := New_Copy_Tree (Arg2);
+
+            --  Substitute all references to type Rep_Typ with references to
+            --  the _object formal parameter. Dispatching here must be removed
+            --  due to AI12-0150-1 !!!
+
+            Replace_Type_References
+              (Expr, Rep_Typ, Obj_Id, Dispatch => Class_Present (Prag));
+
+            --  Additional processing for non-class-wide invariants
+
+            if not Inherit then
+
+               --  Preanalyze the invariant expression to detect errors and at
+               --  the same time capture the visibility of the proper package
+               --  part.
+
+               --  Historical note: the old implementation of invariants used
+               --  node N as the parent, but a package specification as parent
+               --  of an expression is bizarre.
+
+               Set_Parent (Expr, Parent (Arg2));
+               Preanalyze_Assert_Expression (Expr, Any_Boolean);
+
+               --  If the pragma comes from an aspect specification, replace
+               --  the saved expression because all type references must be
+               --  substituted for the call to Preanalyze_Spec_Expression in
+               --  Check_Aspect_At_xxx routines.
+
+               if Present (Asp) then
+                  Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
+               end if;
+
+               --  Analyze the original invariant expression for ASIS
+
+               if ASIS_Mode then
+                  ASIS_Expr := Empty;
+
+                  if Comes_From_Source (Prag) then
+                     ASIS_Expr := Arg2;
+                  elsif Present (Asp) then
+                     ASIS_Expr := Expression (Asp);
+                  end if;
+
+                  if Present (ASIS_Expr) then
+                     Replace_Type_References
+                       (ASIS_Expr, Rep_Typ, Obj_Id, Class_Present (Prag));
+                     Preanalyze_Assert_Expression (ASIS_Expr, Any_Boolean);
+                  end if;
+               end if;
+
+               --  A class-wide invariant may be inherited in a separate unit,
+               --  where the corresponding expression cannot be resolved by
+               --  visibility, because it refers to a local function. Propagate
+               --  semantic information to the original representation item, to
+               --  be used when an invariant procedure for a derived type is
+               --  constructed.
+
+               --  ??? Unclear how to handle class-wide invariants that are not
+               --  function calls.
+
+               if Class_Present (Prag)
+                 and then Nkind (Expr) = N_Function_Call
+                 and then Nkind (Arg2) = N_Indexed_Component
+               then
+                  Rewrite (Arg2,
+                    Make_Function_Call (Ploc,
+                      Name                   =>
+                        New_Occurrence_Of (Entity (Name (Expr)), Ploc),
+                      Parameter_Associations => Expressions (Arg2)));
+               end if;
+            end if;
+
+            --  The invariant is ignored, nothing left to do
+
+            if Is_Ignored (Prag) then
+               null;
+
+            --  Otherwise the invariant is checked. Build a Check pragma to
+            --  verify the expression at runtime.
+
+            else
+               Assoc := New_List (
+                 Make_Pragma_Argument_Association (Ploc,
+                   Expression => Make_Identifier (Ploc, Nam)),
+                 Make_Pragma_Argument_Association (Ploc,
+                   Expression => Expr));
+
+               --  Handle the String argument (if any)
+
+               if Present (Arg3) then
+                  Str := Strval (Get_Pragma_Arg (Arg3));
+
+                  --  When inheriting an invariant, modify the message from
+                  --  "failed invariant" to "failed inherited invariant".
+
+                  if Inherit then
+                     String_To_Name_Buffer (Str);
+
+                     if Name_Buffer (1 .. 16) = "failed invariant" then
+                        Insert_Str_In_Name_Buffer ("inherited ", 8);
+                        Str := String_From_Name_Buffer;
+                     end if;
+                  end if;
+
+                  Append_To (Assoc,
+                    Make_Pragma_Argument_Association (Ploc,
+                      Expression => Make_String_Literal (Ploc, Str)));
+               end if;
+
+               --  Generate:
+               --    pragma Check (<Nam>, <Expr>, <Str>);
+
+               Append_New_To (Checks,
+                 Make_Pragma (Ploc,
+                   Chars                        => Name_Check,
+                   Pragma_Argument_Associations => Assoc));
+            end if;
+
+            --  Output an info message when inheriting an invariant and the
+            --  listing option is enabled.
+
+            if Inherit and Opt.List_Inherited_Aspects then
+               Error_Msg_Sloc := Sloc (Prag);
+               Error_Msg_N
+                 ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
+            end if;
+
+            --  Add the pragma to the list of processed pragmas
+
+            Append_New_Elmt (Prag, Pragmas_Seen);
+            Produced_Check := True;
+         end Add_Invariant;
+
+         ------------------
+         -- Process_Type --
+         ------------------
+
+         procedure Process_Type
+           (T         : Entity_Id;
+            Stop_Item : Node_Id := Empty)
+         is
+            Rep_Item : Node_Id;
+
+         begin
+            Rep_Item := First_Rep_Item (T);
+            while Present (Rep_Item) loop
+               if Nkind (Rep_Item) = N_Pragma
+                 and then Pragma_Name (Rep_Item) = Name_Invariant
+               then
+                  --  Stop the traversal of the rep item chain once a specific
+                  --  item is encountered.
+
+                  if Present (Stop_Item) and then Rep_Item = Stop_Item then
+                     exit;
+
+                  --  Otherwise generate an invariant check
+
+                  else
+                     Add_Invariant (Rep_Item);
+                  end if;
+               end if;
+
+               Next_Rep_Item (Rep_Item);
+            end loop;
+         end Process_Type;
+
+      --  Start of processing for Add_Type_Invariants
+
+      begin
+         --  Process the invariants of the partial view
+
+         if Present (Priv_Typ) then
+            Process_Type (Priv_Typ);
+         end if;
+
+         --  Process the invariants of the full view
+
+         if Present (Full_Typ) then
+            Process_Type (Full_Typ, Stop_Item => Priv_Item);
+
+            --  Process the elements of an array type
+
+            if Is_Array_Type (Full_Typ) then
+               Add_Array_Component_Invariants (Full_Typ, Obj_Id, Checks);
+
+            --  Process the components of a record type
+
+            elsif Ekind (Full_Typ) = E_Record_Type then
+               Add_Record_Component_Invariants (Full_Typ, Obj_Id, Checks);
+            end if;
+         end if;
+
+         --  Process the components of a corresponding record type
+
+         if Present (CRec_Typ) then
+            Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Checks);
+         end if;
+      end Add_Type_Invariants;
+
+      --  Local variables
+
+      Dummy        : Entity_Id;
+      Mode         : Ghost_Mode_Type;
+      Priv_Item    : Node_Id;
+      Proc_Body    : Node_Id;
+      Proc_Body_Id : Entity_Id;
+      Proc_Decl    : Node_Id;
+      Proc_Id      : Entity_Id;
+      Stmts        : List_Id := No_List;
+
+      CRec_Typ : Entity_Id;
+      --  The corresponding record type of Full_Typ
+
+      Full_Proc : Entity_Id;
+      --  The entity of the "full" invariant procedure
+
+      Full_Typ : Entity_Id;
+      --  The full view of the working type
+
+      Obj_Id : Entity_Id;
+      --  The _object formal parameter of the invariant procedure
+
+      Part_Proc : Entity_Id;
+      --  The entity of the "partial" invariant procedure
+
+      Priv_Typ : Entity_Id;
+      --  The partial view of the working type
+
+      Work_Typ : Entity_Id;
+      --  The working type
+
+   --  Start of processing for Build_Invariant_Procedure_Body
+
+   begin
+      Work_Typ := Typ;
+
+      --  The input type denotes the implementation base type of a constrained
+      --  array type. Work with the first subtype as all invariant pragmas are
+      --  on its rep item chain.
+
+      if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
+         Work_Typ := First_Subtype (Work_Typ);
+
+      --  The input type denotes the corresponding record type of a protected
+      --  or task type. Work with the concurrent type because the corresponding
+      --  record type may not be visible to clients of the type.
+
+      elsif Ekind (Work_Typ) = E_Record_Type
+        and then Is_Concurrent_Record_Type (Work_Typ)
+      then
+         Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
+      end if;
+
+      --  The working type may be subject to pragma Ghost. Set the mode now to
+      --  ensure that the invariant procedure is properly marked as Ghost.
+
+      Set_Ghost_Mode (Work_Typ, Mode);
+
+      --  The type must either have invariants of its own, inherit class-wide
+      --  invariants from parent types or interfaces, or be an array or record
+      --  type whose components have invariants.
+
+      pragma Assert (Has_Invariants (Work_Typ));
+
+      --  Nothing to do for interface types as their class-wide invariants are
+      --  inherited by implementing types.
+
+      if Is_Interface (Work_Typ) then
+         goto Leave;
+      end if;
+
+      --  Obtain both views of the type
+
+      Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ);
+
+      --  The caller requests a body for the partial invariant procedure
+
+      if Partial_Invariant then
+         Full_Proc := Invariant_Procedure (Work_Typ);
+         Proc_Id   := Partial_Invariant_Procedure (Work_Typ);
+
+         --  The "full" invariant procedure body was already created
+
+         if Present (Full_Proc)
+           and then Present
+                      (Corresponding_Body (Unit_Declaration_Node (Full_Proc)))
+         then
+            --  This scenario happens only when the type is an untagged
+            --  derivation from a private parent and the underlying full
+            --  view was processed before the partial view.
+
+            pragma Assert
+              (Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ));
+
+            --  Nothing to do because the processing of the underlying full
+            --  view already checked the invariants of the partial view.
+
+            goto Leave;
+         end if;
+
+         --  Create a declaration for the "partial" invariant procedure if it
+         --  is not available.
+
+         if No (Proc_Id) then
+            Build_Invariant_Procedure_Declaration
+              (Typ               => Work_Typ,
+               Partial_Invariant => True);
+
+            Proc_Id := Partial_Invariant_Procedure (Work_Typ);
+         end if;
+
+      --  The caller requests a body for the "full" invariant procedure
+
+      else
+         Proc_Id   := Invariant_Procedure (Work_Typ);
+         Part_Proc := Partial_Invariant_Procedure (Work_Typ);
+
+         --  Create a declaration for the "full" invariant procedure if it is
+         --  not available.
+
+         if No (Proc_Id) then
+            Build_Invariant_Procedure_Declaration (Work_Typ);
+            Proc_Id := Invariant_Procedure (Work_Typ);
+         end if;
+      end if;
+
+      --  At this point there should be an invariant procedure declaration
+
+      pragma Assert (Present (Proc_Id));
+      Proc_Decl := Unit_Declaration_Node (Proc_Id);
+
+      --  Nothing to do if the invariant procedure already has a body
+
+      if Present (Corresponding_Body (Proc_Decl)) then
+         goto Leave;
+      end if;
+
+      --  Emulate the environment of the invariant procedure by installing
+      --  its scope and formal parameters. Note that this is not needed, but
+      --  having the scope of the invariant procedure installed helps with
+      --  the detection of invariant-related errors.
+
+      Push_Scope (Proc_Id);
+      Install_Formals (Proc_Id);
+
+      Obj_Id := First_Formal (Proc_Id);
+      pragma Assert (Present (Obj_Id));
+
+      --  The "partial" invariant procedure verifies the invariants of the
+      --  partial view only.
+
+      if Partial_Invariant then
+         pragma Assert (Present (Priv_Typ));
+
+         Add_Type_Invariants
+           (Priv_Typ => Priv_Typ,
+            Full_Typ => Empty,
+            CRec_Typ => Empty,
+            Obj_Id   => Obj_Id,
+            Checks   => Stmts);
+
+      --  Otherwise the "full" invariant procedure verifies the invariants of
+      --  the full view, all array or record components, as well as class-wide
+      --  invariants inherited from parent types or interfaces. In addition, it
+      --  indirectly verifies the invariants of the partial view by calling the
+      --  "partial" invariant procedure.
+
+      else
+         pragma Assert (Present (Full_Typ));
+
+         --  Check the invariants of the partial view by calling the "partial"
+         --  invariant procedure. Generate:
+
+         --    <Work_Typ>Partial_Invariant (_object);
+
+         if Present (Part_Proc) then
+            Append_New_To (Stmts,
+              Make_Procedure_Call_Statement (Loc,
+                Name                   => New_Occurrence_Of (Part_Proc, Loc),
+                Parameter_Associations => New_List (
+                  New_Occurrence_Of (Obj_Id, Loc))));
+
+            Produced_Check := True;
+         end if;
+
+         Priv_Item := Empty;
+
+         --  Derived subtypes do not have a partial view
+
+         if Present (Priv_Typ) then
+
+            --  The processing of the "full" invariant procedure intentionally
+            --  skips the partial view because a) this may result in changes of
+            --  visibility and b) lead to duplicate checks. However, when the
+            --  full view is the underlying full view of an untagged derived
+            --  type whose parent type is private, partial invariants appear on
+            --  the rep item chain of the partial view only.
+
+            --    package Pack_1 is
+            --       type Root ... is private;
+            --    private
+            --       <full view of Root>
+            --    end Pack_1;
+
+            --    with Pack_1;
+            --    package Pack_2 is
+            --       type Child is new Pack_1.Root with Type_Invariant => ...;
+            --       <underlying full view of Child>
+            --    end Pack_2;
+
+            --  As a result, the processing of the full view must also consider
+            --  all invariants of the partial view.
+
+            if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then
+               null;
+
+            --  Otherwise the invariants of the partial view are ignored
+
+            else
+               --  Note that the rep item chain is shared between the partial
+               --  and full views of a type. To avoid processing the invariants
+               --  of the partial view, signal the logic to stop when the first
+               --  rep item of the partial view has been reached.
+
+               Priv_Item := First_Rep_Item (Priv_Typ);
+
+               --  Ignore the invariants of the partial view by eliminating the
+               --  view.
+
+               Priv_Typ := Empty;
+            end if;
+         end if;
+
+         --  Process the invariants of the full view and in certain cases those
+         --  of the partial view. This also handles any invariants on array or
+         --  record components.
+
+         Add_Type_Invariants
+           (Priv_Typ  => Priv_Typ,
+            Full_Typ  => Full_Typ,
+            CRec_Typ  => CRec_Typ,
+            Obj_Id    => Obj_Id,
+            Checks    => Stmts,
+            Priv_Item => Priv_Item);
+
+         --  Process the inherited class-wide invariants of all parent types.
+         --  This also handles any invariants on record components.
+
+         Add_Parent_Invariants (Full_Typ, Obj_Id, Stmts);
+
+         --  Process the inherited class-wide invariants of all implemented
+         --  interface types.
+
+         Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts);
+      end if;
+
+      End_Scope;
+
+      --  At this point there should be at least one invariant check. If this
+      --  is not the case, then the invariant-related flags were not properly
+      --  set, or there is a missing invariant procedure on one of the array
+      --  or record components.
+
+      pragma Assert (Produced_Check);
+
+      --  Account for the case where assertions are disabled or all invariant
+      --  checks are subject to Assertion_Policy Ignore. Produce a completing
+      --  empty body.
+
+      if No (Stmts) then
+         Stmts := New_List (Make_Null_Statement (Loc));
+      end if;
+
+      --  Generate:
+      --    procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>) is
+      --    begin
+      --       <Stmts>
+      --    end <Work_Typ>[Partial_]Invariant;
+
+      Proc_Body :=
+        Make_Subprogram_Body (Loc,
+          Specification                =>
+            Copy_Subprogram_Spec (Parent (Proc_Id)),
+          Declarations                 => Empty_List,
+            Handled_Statement_Sequence =>
+              Make_Handled_Sequence_Of_Statements (Loc,
+                Statements => Stmts));
+      Proc_Body_Id := Defining_Entity (Proc_Body);
+
+      --  Perform minor decoration in case the body is not analyzed
+
+      Set_Ekind (Proc_Body_Id, E_Subprogram_Body);
+      Set_Etype (Proc_Body_Id, Standard_Void_Type);
+      Set_Scope (Proc_Body_Id, Current_Scope);
+
+      --  Link both spec and body to avoid generating duplicates
+
+      Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
+      Set_Corresponding_Spec (Proc_Body, Proc_Id);
+
+      --  The body should not be inserted into the tree when the context is
+      --  ASIS or a generic unit because it is not part of the template. Note
+      --  that the body must still be generated in order to resolve the
+      --  invariants.
+
+      if ASIS_Mode or Inside_A_Generic then
+         null;
+
+      --  Semi-insert the body into the tree for GNATprove by setting its
+      --  Parent field. This allows for proper upstream tree traversals.
+
+      elsif GNATprove_Mode then
+         Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+
+      --  Otherwise the body is part of the freezing actions of the type
+
+      else
+         Append_Freeze_Action (Work_Typ, Proc_Body);
+      end if;
+
+   <<Leave>>
+      Restore_Ghost_Mode (Mode);
+   end Build_Invariant_Procedure_Body;
+
+   -------------------------------------------
+   -- Build_Invariant_Procedure_Declaration --
+   -------------------------------------------
+
+   --  WARNING: This routine manages Ghost regions. Return statements must be
+   --  replaced by gotos which jump to the end of the routine and restore the
+   --  Ghost mode.
+
+   procedure Build_Invariant_Procedure_Declaration
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False)
+   is
+      Loc : constant Source_Ptr := Sloc (Typ);
+
+      Mode      : Ghost_Mode_Type;
+      Proc_Decl : Node_Id;
+      Proc_Id   : Entity_Id;
+      Proc_Nam  : Name_Id;
+      Typ_Decl  : Node_Id;
+
+      CRec_Typ : Entity_Id;
+      --  The corresponding record type of Full_Typ
+
+      Full_Base : Entity_Id;
+      --  The base type of Full_Typ
+
+      Full_Typ : Entity_Id;
+      --  The full view of working type
+
+      Obj_Id : Entity_Id;
+      --  The _object formal parameter of the invariant procedure
+
+      Priv_Typ : Entity_Id;
+      --  The partial view of working type
+
+      Work_Typ : Entity_Id;
+      --  The working type
+
+   begin
+      Work_Typ := Typ;
+
+      --  The input type denotes the implementation base type of a constrained
+      --  array type. Work with the first subtype as all invariant pragmas are
+      --  on its rep item chain.
+
+      if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
+         Work_Typ := First_Subtype (Work_Typ);
+
+      --  The input denotes the corresponding record type of a protected or a
+      --  task type. Work with the concurrent type because the corresponding
+      --  record type may not be visible to clients of the type.
+
+      elsif Ekind (Work_Typ) = E_Record_Type
+        and then Is_Concurrent_Record_Type (Work_Typ)
+      then
+         Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
+      end if;
+
+      --  The working type may be subject to pragma Ghost. Set the mode now to
+      --  ensure that the invariant procedure is properly marked as Ghost.
+
+      Set_Ghost_Mode (Work_Typ, Mode);
+
+      --  The type must either have invariants of its own, inherit class-wide
+      --  invariants from parent or interface types, or be an array or record
+      --  type whose components have invariants.
+
+      pragma Assert (Has_Invariants (Work_Typ));
+
+      --  Nothing to do for interface types as their class-wide invariants are
+      --  inherited by implementing types.
+
+      if Is_Interface (Work_Typ) then
+         goto Leave;
+
+      --  Nothing to do if the type already has a "partial" invariant procedure
+
+      elsif Partial_Invariant then
+         if Present (Partial_Invariant_Procedure (Work_Typ)) then
+            goto Leave;
+         end if;
+
+      --  Nothing to do if the type already has a "full" invariant procedure
+
+      elsif Present (Invariant_Procedure (Work_Typ)) then
+         goto Leave;
+      end if;
+
+      --  The caller requests the declaration of the "partial" invariant
+      --  procedure.
+
+      if Partial_Invariant then
+         Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_Invariant");
+
+      --  Otherwise the caller requests the declaration of the "full" invariant
+      --  procedure.
+
+      else
+         Proc_Nam := New_External_Name (Chars (Work_Typ), "Invariant");
+      end if;
+
+      Proc_Id := Make_Defining_Identifier (Loc, Chars => Proc_Nam);
+
+      --  Perform minor decoration in case the declaration is not analyzed
+
+      Set_Ekind (Proc_Id, E_Procedure);
+      Set_Etype (Proc_Id, Standard_Void_Type);
+      Set_Scope (Proc_Id, Current_Scope);
+
+      if Partial_Invariant then
+         Set_Is_Partial_Invariant_Procedure (Proc_Id);
+         Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
+      else
+         Set_Is_Invariant_Procedure (Proc_Id);
+         Set_Invariant_Procedure (Work_Typ, Proc_Id);
+      end if;
+
+      --  The invariant procedure requires debug info when the invariants are
+      --  subject to Source Coverage Obligations.
+
+      if Opt.Generate_SCO then
+         Set_Needs_Debug_Info (Proc_Id);
+      end if;
+
+      --  Obtain all views of the input type
+
+      Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
+
+      --  Associate the invariant procedure with all views
+
+      Propagate_Invariant_Attributes (Priv_Typ,  From_Typ => Work_Typ);
+      Propagate_Invariant_Attributes (Full_Typ,  From_Typ => Work_Typ);
+      Propagate_Invariant_Attributes (Full_Base, From_Typ => Work_Typ);
+      Propagate_Invariant_Attributes (CRec_Typ,  From_Typ => Work_Typ);
+
+      --  The declaration of the invariant procedure is inserted after the
+      --  declaration of the partial view as this allows for proper external
+      --  visibility.
+
+      if Present (Priv_Typ) then
+         Typ_Decl := Declaration_Node (Priv_Typ);
+
+      --  Derived types with the full view as parent do not have a partial
+      --  view. Insert the invariant procedure after the derived type.
+
+      else
+         Typ_Decl := Declaration_Node (Full_Typ);
+      end if;
+
+      --  The type should have a declarative node
+
+      pragma Assert (Present (Typ_Decl));
+
+      --  Create the formal parameter which emulates the variable-like behavior
+      --  of the current type instance.
+
+      Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
+
+      --  Perform minor decoration in case the declaration is not analyzed
+
+      Set_Ekind (Obj_Id, E_In_Parameter);
+      Set_Etype (Obj_Id, Work_Typ);
+      Set_Scope (Obj_Id, Proc_Id);
+
+      Set_First_Entity (Proc_Id, Obj_Id);
+
+      --  Generate:
+      --    procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>);
+
+      Proc_Decl :=
+        Make_Subprogram_Declaration (Loc,
+          Specification =>
+            Make_Procedure_Specification (Loc,
+              Defining_Unit_Name       => Proc_Id,
+              Parameter_Specifications => New_List (
+                Make_Parameter_Specification (Loc,
+                  Defining_Identifier => Obj_Id,
+                  Parameter_Type      =>
+                    New_Occurrence_Of (Work_Typ, Loc)))));
+
+      --  The declaration should not be inserted into the tree when the context
+      --  is ASIS or a generic unit because it is not part of the template.
+
+      if ASIS_Mode or Inside_A_Generic then
+         null;
+
+      --  Semi-insert the declaration into the tree for GNATprove by setting
+      --  its Parent field. This allows for proper upstream tree traversals.
+
+      elsif GNATprove_Mode then
+         Set_Parent (Proc_Decl, Parent (Typ_Decl));
+
+      --  Otherwise insert the declaration
+
+      else
+         pragma Assert (Present (Typ_Decl));
+         Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
+      end if;
+
+   <<Leave>>
+      Restore_Ghost_Mode (Mode);
+   end Build_Invariant_Procedure_Declaration;
+
    --------------------------
    -- Build_Procedure_Form --
    --------------------------
@@ -7124,6 +8501,23 @@ package body Exp_Util is
                    and then Etype (Full_View (T)) /= T);
    end Is_Untagged_Derivation;
 
+   ------------------------------------
+   -- Is_Untagged_Private_Derivation --
+   ------------------------------------
+
+   function Is_Untagged_Private_Derivation
+     (Priv_Typ : Entity_Id;
+      Full_Typ : Entity_Id) return Boolean
+   is
+   begin
+      return
+        Present (Priv_Typ)
+          and then Is_Untagged_Derivation (Priv_Typ)
+          and then Is_Private_Type (Etype (Priv_Typ))
+          and then Present (Full_Typ)
+          and then Is_Itype (Full_Typ);
+   end Is_Untagged_Private_Derivation;
+
    ---------------------------
    -- Is_Volatile_Reference --
    ---------------------------
@@ -10181,9 +11575,10 @@ package body Exp_Util is
    -----------------------------
 
    procedure Replace_Type_References
-     (Expr   : Node_Id;
-      Typ    : Entity_Id;
-      Obj_Id : Entity_Id)
+     (Expr     : Node_Id;
+      Typ      : Entity_Id;
+      Obj_Id   : Entity_Id;
+      Dispatch : Boolean := False)
    is
       procedure Replace_Type_Ref (N : Node_Id);
       --  Substitute a single reference of the current instance of type Typ
@@ -10194,7 +11589,8 @@ package body Exp_Util is
       ----------------------
 
       procedure Replace_Type_Ref (N : Node_Id) is
-         Ref : Node_Id;
+         Nloc : constant Source_Ptr := Sloc (N);
+         Ref  : Node_Id;
 
       begin
          --  Decorate the reference to Typ even though it may be rewritten
@@ -10224,8 +11620,27 @@ package body Exp_Util is
          Set_Entity (Ref, Obj_Id);
          Set_Etype  (Ref, Typ);
 
-         Rewrite (N, Ref);
+         --  When the pragma denotes a class-wide and the Dispatch flag is set
+         --  perform the following substitution. Note: dispatching in this
+         --  fashion is illegal Ada according to AI12-0150-1 because class-wide
+         --  aspects like type invariants and default initial conditions be
+         --  evaluated statically. Currently it is used only for class-wide
+         --  type invariants, but this will be fixed.
+
+         --    Rep_Typ  -->  Rep_Typ'Class (_object)
 
+         if Dispatch then
+            Ref :=
+              Make_Type_Conversion (Nloc,
+                Subtype_Mark =>
+                  Make_Attribute_Reference (Nloc,
+                    Prefix         =>
+                      New_Occurrence_Of (Typ, Nloc),
+                    Attribute_Name => Name_Class),
+                Expression   => Ref);
+         end if;
+
+         Rewrite (N, Ref);
          Set_Comes_From_Source (N, True);
       end Replace_Type_Ref;
 
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 8e00217..0a409f3 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -290,6 +290,21 @@ package Exp_Util is
    --  Create the declaration of the procedure which verifies the assertion
    --  expression of pragma Default_Initial_Condition at run time.
 
+   procedure Build_Invariant_Procedure_Body
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False);
+   --  Create the body of the procedure which verifies the invariants of type
+   --  Typ at runtime. Flag Partial_Invariant should be set when Typ denotes a
+   --  private type, otherwise it is assumed that Typ denotes the full view of
+   --  a private type.
+
+   procedure Build_Invariant_Procedure_Declaration
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False);
+   --  Create the declaration of the procedure which verifies the invariants of
+   --  type Typ at runtime. Flag Partial_Invariant should be set when building
+   --  the invariant procedure for a private type.
+
    procedure Build_Procedure_Form (N : Node_Id);
    --  Create a procedure declaration which emulates the behavior of a function
    --  that returns an array type, for C-compatible generation.
@@ -805,6 +820,12 @@ package Exp_Util is
    --  Returns true if type T is not tagged and is a derived type,
    --  or is a private type whose completion is such a type.
 
+   function Is_Untagged_Private_Derivation
+     (Priv_Typ : Entity_Id;
+      Full_Typ : Entity_Id) return Boolean;
+   --  Determine whether private type Priv_Typ and its full view Full_Typ
+   --  represent an untagged derivation from a private parent.
+
    function Is_Volatile_Reference (N : Node_Id) return Boolean;
    --  Checks if the node N represents a volatile reference, which can be
    --  either a direct reference to a variable treated as volatile, or an
@@ -1037,9 +1058,10 @@ package Exp_Util is
    --      the internally-generated inherited primitive of Deriv_Typ.
 
    procedure Replace_Type_References
-     (Expr   : Node_Id;
-      Typ    : Entity_Id;
-      Obj_Id : Entity_Id);
+     (Expr     : Node_Id;
+      Typ      : Entity_Id;
+      Obj_Id   : Entity_Id;
+      Dispatch : Boolean := False);
    --  Substitute all references of the current instance of type Typ with
    --  references to formal parameter Obj_Id within expression Expr.
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 0c4d230..cbae00f 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -33,7 +33,6 @@ with Einfo;     use Einfo;
 with Errout;    use Errout;
 with Eval_Fat;  use Eval_Fat;
 with Exp_Ch3;   use Exp_Ch3;
-with Exp_Ch7;   use Exp_Ch7;
 with Exp_Ch9;   use Exp_Ch9;
 with Exp_Disp;  use Exp_Disp;
 with Exp_Dist;  use Exp_Dist;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index c169737..2638b37 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -39,7 +39,6 @@ with Debug;     use Debug;
 with Einfo;     use Einfo;
 with Elists;    use Elists;
 with Errout;    use Errout;
-with Exp_Ch7;   use Exp_Ch7;
 with Exp_Dist;  use Exp_Dist;
 with Exp_Util;  use Exp_Util;
 with Freeze;    use Freeze;
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 7002035..ed88373 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -1823,8 +1823,20 @@ package body Sem_Util is
                               N_Subprogram_Declaration)
            and then not Comes_From_Source (Par)
          then
-            OK_Use := True;
-            exit;
+            --  Continue to examine the context if the reference appears in a
+            --  subprogram body which was previously an expression function.
+
+            if Nkind (Par) = N_Subprogram_Body
+              and then Was_Expression_Function (Par)
+            then
+               null;
+
+            --  Otherwise the reference is legal
+
+            else
+               OK_Use := True;
+               exit;
+            end if;
 
          --  The reference has been relocated to an inlined body for GNATprove.
          --  Assume that the reference is legal as the real check was already