[multiple changes]
[gcc.git] / gcc / ada / sem_ch12.adb
index 78881a9033477426499d51fd5527395c613eb575..cac9db9cbf3735553ff9c8aa5f5d098e7b1674c2 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -25,7 +25,6 @@
 
 with Aspects;  use Aspects;
 with Atree;    use Atree;
-with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Elists;   use Elists;
 with Errout;   use Errout;
@@ -34,6 +33,7 @@ with Exp_Disp; use Exp_Disp;
 with Fname;    use Fname;
 with Fname.UF; use Fname.UF;
 with Freeze;   use Freeze;
+with Ghost;    use Ghost;
 with Itypes;   use Itypes;
 with Lib;      use Lib;
 with Lib.Load; use Lib.Load;
@@ -240,13 +240,125 @@ package body Sem_Ch12 is
    --  circularity is detected, and used to abandon compilation after the
    --  messages have been posted.
 
+   -----------------------------------------
+   -- Implementation of Generic Contracts --
+   -----------------------------------------
+
+   --  A "contract" is a collection of aspects and pragmas that either verify a
+   --  property of a construct at runtime or classify the data flow to and from
+   --  the construct in some fashion.
+
+   --  Generic packages, subprograms and their respective bodies may be subject
+   --  to the following contract-related aspects or pragmas collectively known
+   --  as annotations:
+
+   --     package                  subprogram [body]
+   --       Abstract_State           Contract_Cases
+   --       Initial_Condition        Depends
+   --       Initializes              Extensions_Visible
+   --                                Global
+   --     package body               Post
+   --       Refined_State            Post_Class
+   --                                Postcondition
+   --                                Pre
+   --                                Pre_Class
+   --                                Precondition
+   --                                Refined_Depends
+   --                                Refined_Global
+   --                                Refined_Post
+   --                                Test_Case
+
+   --  Most package contract annotations utilize forward references to classify
+   --  data declared within the package [body]. Subprogram annotations then use
+   --  the classifications to further refine them. These inter dependencies are
+   --  problematic with respect to the implementation of generics because their
+   --  analysis, capture of global references and instantiation does not mesh
+   --  well with the existing mechanism.
+
+   --  1) Analysis of generic contracts is carried out the same way non-generic
+   --  contracts are analyzed:
+
+   --    1.1) General rule - a contract is analyzed after all related aspects
+   --    and pragmas are analyzed. This is done by routines
+
+   --       Analyze_Package_Body_Contract
+   --       Analyze_Package_Contract
+   --       Analyze_Subprogram_Body_Contract
+   --       Analyze_Subprogram_Contract
+
+   --    1.2) Compilation unit - the contract is analyzed after Pragmas_After
+   --    are processed.
+
+   --    1.3) Compilation unit body - the contract is analyzed at the end of
+   --    the body declaration list.
+
+   --    1.4) Package - the contract is analyzed at the end of the private or
+   --    visible declarations, prior to analyzing the contracts of any nested
+   --    packages or subprograms.
+
+   --    1.5) Package body - the contract is analyzed at the end of the body
+   --    declaration list, prior to analyzing the contracts of any nested
+   --    packages or subprograms.
+
+   --    1.6) Subprogram - if the subprogram is declared inside a block, a
+   --    package or a subprogram, then its contract is analyzed at the end of
+   --    the enclosing declarations, otherwise the subprogram is a compilation
+   --    unit 1.2).
+
+   --    1.7) Subprogram body - if the subprogram body is declared inside a
+   --    block, a package body or a subprogram body, then its contract is
+   --    analyzed at the end of the enclosing declarations, otherwise the
+   --    subprogram is a compilation unit 1.3).
+
+   --  2) Capture of global references within contracts is done after capturing
+   --  global references within the generic template. There are two reasons for
+   --  this delay - pragma annotations are not part of the generic template in
+   --  the case of a generic subprogram declaration, and analysis of contracts
+   --  is delayed.
+
+   --  Contract-related source pragmas within generic templates are prepared
+   --  for delayed capture of global references by routine
+
+   --    Create_Generic_Contract
+
+   --  The routine associates these pragmas with the contract of the template.
+   --  In the case of a generic subprogram declaration, the routine creates
+   --  generic templates for the pragmas declared after the subprogram because
+   --  they are not part of the template.
+
+   --    generic                                --  template starts
+   --    procedure Gen_Proc (Input : Integer);  --  template ends
+   --    pragma Precondition (Input > 0);       --  requires own template
+
+   --    2.1) The capture of global references with aspect specifications and
+   --    source pragmas that apply to a generic unit must be suppressed when
+   --    the generic template is being processed because the contracts have not
+   --    been analyzed yet. Any attempts to capture global references at that
+   --    point will destroy the Associated_Node linkages and leave the template
+   --    undecorated. This delay is controlled by routine
+
+   --       Requires_Delayed_Save
+
+   --    2.2) The real capture of global references within a contract is done
+   --    after the contract has been analyzed, by routine
+
+   --       Save_Global_References_In_Contract
+
+   --  3) The instantiation of a generic contract occurs as part of the
+   --  instantiation of the contract owner. Generic subprogram declarations
+   --  require additional processing when the contract is specified by pragmas
+   --  because the pragmas are not part of the generic template. This is done
+   --  by routine
+
+   --    Instantiate_Subprogram_Contract
+
    Circularity_Detected : Boolean := False;
    --  This should really be reset on encountering a new main unit, but in
    --  practice we are not using multiple main units so it is not critical.
 
-   -------------------------------------------------
-   -- Formal packages and partial parametrization --
-   -------------------------------------------------
+   --------------------------------------------------
+   -- Formal packages and partial parameterization --
+   --------------------------------------------------
 
    --  When compiling a generic, a formal package is a local instantiation. If
    --  declared with a box, its generic formals are visible in the enclosing
@@ -263,7 +375,7 @@ package body Sem_Ch12 is
 
    --  In a generic, a formal package is treated like a special instantiation.
    --  Our Ada 95 compiler handled formals with and without box in different
-   --  ways. With partial parametrization, we use a single model for both.
+   --  ways. With partial parameterization, we use a single model for both.
    --  We create a package declaration that consists of the specification of
    --  the generic package, and a set of declarations that map the actuals
    --  into local renamings, just as we do for bona fide instantiations. For
@@ -477,6 +589,74 @@ package body Sem_Ch12 is
    --  packages, and the prefix of the formal type may be needed to resolve
    --  the ambiguity in the instance ???
 
+   procedure Freeze_Subprogram_Body
+     (Inst_Node : Node_Id;
+      Gen_Body  : Node_Id;
+      Pack_Id   : Entity_Id);
+   --  The generic body may appear textually after the instance, including
+   --  in the proper body of a stub, or within a different package instance.
+   --  Given that the instance can only be elaborated after the generic, we
+   --  place freeze_nodes for the instance and/or for packages that may enclose
+   --  the instance and the generic, so that the back-end can establish the
+   --  proper order of elaboration.
+
+   function Get_Associated_Node (N : Node_Id) return Node_Id;
+   --  In order to propagate semantic information back from the analyzed copy
+   --  to the original generic, we maintain links between selected nodes in the
+   --  generic and their corresponding copies. At the end of generic analysis,
+   --  the routine Save_Global_References traverses the generic tree, examines
+   --  the semantic information, and preserves the links to those nodes that
+   --  contain global information. At instantiation, the information from the
+   --  associated node is placed on the new copy, so that name resolution is
+   --  not repeated.
+   --
+   --  Three kinds of source nodes have associated nodes:
+   --
+   --    a) those that can reference (denote) entities, that is identifiers,
+   --       character literals, expanded_names, operator symbols, operators,
+   --       and attribute reference nodes. These nodes have an Entity field
+   --       and are the set of nodes that are in N_Has_Entity.
+   --
+   --    b) aggregates (N_Aggregate and N_Extension_Aggregate)
+   --
+   --    c) selected components (N_Selected_Component)
+   --
+   --  For the first class, the associated node preserves the entity if it is
+   --  global. If the generic contains nested instantiations, the associated
+   --  node itself has been recopied, and a chain of them must be followed.
+   --
+   --  For aggregates, the associated node allows retrieval of the type, which
+   --  may otherwise not appear in the generic. The view of this type may be
+   --  different between generic and instantiation, and the full view can be
+   --  installed before the instantiation is analyzed. For aggregates of type
+   --  extensions, the same view exchange may have to be performed for some of
+   --  the ancestor types, if their view is private at the point of
+   --  instantiation.
+   --
+   --  Nodes that are selected components in the parse tree may be rewritten
+   --  as expanded names after resolution, and must be treated as potential
+   --  entity holders, which is why they also have an Associated_Node.
+   --
+   --  Nodes that do not come from source, such as freeze nodes, do not appear
+   --  in the generic tree, and need not have an associated node.
+   --
+   --  The associated node is stored in the Associated_Node field. Note that
+   --  this field overlaps Entity, which is fine, because the whole point is
+   --  that we don't need or want the normal Entity field in this situation.
+
+   function Has_Been_Exchanged (E : Entity_Id) return Boolean;
+   --  Traverse the Exchanged_Views list to see if a type was private
+   --  and has already been flipped during this phase of instantiation.
+
+   procedure Hide_Current_Scope;
+   --  When instantiating a generic child unit, the parent context must be
+   --  present, but the instance and all entities that may be generated
+   --  must be inserted in the current scope. We leave the current scope
+   --  on the stack, but make its entities invisible to avoid visibility
+   --  problems. This is reversed at the end of the instantiation. This is
+   --  not done for the instantiation of the bodies, which only require the
+   --  instances of the generic parents to be in scope.
+
    function In_Same_Declarative_Part
      (F_Node : Node_Id;
       Inst   : Node_Id) return Boolean;
@@ -493,32 +673,31 @@ package body Sem_Ch12 is
    --  Used to determine whether its body should be elaborated to allow
    --  front-end inlining.
 
-   procedure Set_Instance_Env
-     (Gen_Unit : Entity_Id;
-      Act_Unit : Entity_Id);
-   --  Save current instance on saved environment, to be used to determine
-   --  the global status of entities in nested instances. Part of Save_Env.
-   --  called after verifying that the generic unit is legal for the instance,
-   --  The procedure also examines whether the generic unit is a predefined
-   --  unit, in order to set configuration switches accordingly. As a result
-   --  the procedure must be called after analyzing and freezing the actuals.
+   procedure Inherit_Context (Gen_Decl : Node_Id; Inst : Node_Id);
+   --  Add the context clause of the unit containing a generic unit to a
+   --  compilation unit that is, or contains, an instantiation.
 
-   procedure Set_Instance_Of (A : Entity_Id; B : Entity_Id);
-   --  Associate analyzed generic parameter with corresponding
-   --  instance. Used for semantic checks at instantiation time.
+   procedure Init_Env;
+   --  Establish environment for subsequent instantiation. Separated from
+   --  Save_Env because data-structures for visibility handling must be
+   --  initialized before call to Check_Generic_Child_Unit.
 
-   function Has_Been_Exchanged (E : Entity_Id) return Boolean;
-   --  Traverse the Exchanged_Views list to see if a type was private
-   --  and has already been flipped during this phase of instantiation.
+   procedure Inline_Instance_Body
+     (N        : Node_Id;
+      Gen_Unit : Entity_Id;
+      Act_Decl : Node_Id);
+   --  If front-end inlining is requested, instantiate the package body,
+   --  and preserve the visibility of its compilation unit, to insure
+   --  that successive instantiations succeed.
 
-   procedure Hide_Current_Scope;
-   --  When instantiating a generic child unit, the parent context must be
-   --  present, but the instance and all entities that may be generated
-   --  must be inserted in the current scope. We leave the current scope
-   --  on the stack, but make its entities invisible to avoid visibility
-   --  problems. This is reversed at the end of the instantiation. This is
-   --  not done for the instantiation of the bodies, which only require the
-   --  instances of the generic parents to be in scope.
+   procedure Insert_Freeze_Node_For_Instance
+     (N      : Node_Id;
+      F_Node : Node_Id);
+   --  N denotes a package or a subprogram instantiation and F_Node is the
+   --  associated freeze node. Insert the freeze node before the first source
+   --  body which follows immediately after N. If no such body is found, the
+   --  freeze node is inserted at the end of the declarative region which
+   --  contains N.
 
    procedure Install_Body
      (Act_Body : Node_Id;
@@ -535,46 +714,11 @@ package body Sem_Ch12 is
    --  of packages that are early instantiations are delayed, and their freeze
    --  node appears after the generic body.
 
-   procedure Insert_Freeze_Node_For_Instance
-     (N      : Node_Id;
-      F_Node : Node_Id);
-   --  N denotes a package or a subprogram instantiation and F_Node is the
-   --  associated freeze node. Insert the freeze node before the first source
-   --  body which follows immediately after N. If no such body is found, the
-   --  freeze node is inserted at the end of the declarative region which
-   --  contains N.
-
-   procedure Freeze_Subprogram_Body
-     (Inst_Node : Node_Id;
-      Gen_Body  : Node_Id;
-      Pack_Id   : Entity_Id);
-   --  The generic body may appear textually after the instance, including
-   --  in the proper body of a stub, or within a different package instance.
-   --  Given that the instance can only be elaborated after the generic, we
-   --  place freeze_nodes for the instance and/or for packages that may enclose
-   --  the instance and the generic, so that the back-end can establish the
-   --  proper order of elaboration.
-
-   procedure Init_Env;
-   --  Establish environment for subsequent instantiation. Separated from
-   --  Save_Env because data-structures for visibility handling must be
-   --  initialized before call to Check_Generic_Child_Unit.
-
    procedure Install_Formal_Packages (Par : Entity_Id);
    --  Install the visible part of any formal of the parent that is a formal
    --  package. Note that for the case of a formal package with a box, this
    --  includes the formal part of the formal package (12.7(10/2)).
 
-   procedure Install_Parent (P : Entity_Id; In_Body : Boolean := False);
-   --  When compiling an instance of a child unit the parent (which is
-   --  itself an instance) is an enclosing scope that must be made
-   --  immediately visible. This procedure is also used to install the non-
-   --  generic parent of a generic child unit when compiling its body, so
-   --  that full views of types in the parent are made visible.
-
-   procedure Remove_Parent (In_Body : Boolean := False);
-   --  Reverse effect after instantiation of child is complete
-
    procedure Install_Hidden_Primitives
      (Prims_List : in out Elist_Id;
       Gen_T      : Entity_Id;
@@ -583,17 +727,12 @@ package body Sem_Ch12 is
    --  visibility of primitives of Gen_T. The list of primitives to which
    --  the suffix is removed is added to Prims_List to restore them later.
 
-   procedure Restore_Hidden_Primitives (Prims_List : in out Elist_Id);
-   --  Restore suffix 'P' to primitives of Prims_List and leave Prims_List
-   --  set to No_Elist.
-
-   procedure Inline_Instance_Body
-     (N        : Node_Id;
-      Gen_Unit : Entity_Id;
-      Act_Decl : Node_Id);
-   --  If front-end inlining is requested, instantiate the package body,
-   --  and preserve the visibility of its compilation unit, to insure
-   --  that successive instantiations succeed.
+   procedure Install_Parent (P : Entity_Id; In_Body : Boolean := False);
+   --  When compiling an instance of a child unit the parent (which is
+   --  itself an instance) is an enclosing scope that must be made
+   --  immediately visible. This procedure is also used to install the non-
+   --  generic parent of a generic child unit when compiling its body, so
+   --  that full views of types in the parent are made visible.
 
    --  The functions Instantiate_XXX perform various legality checks and build
    --  the declarations for instantiated generic parameters. In all of these
@@ -663,54 +802,6 @@ package body Sem_Ch12 is
    --  instances in the current declarative part that precede the one being
    --  loaded. In that case a missing body is acceptable.
 
-   procedure Inherit_Context (Gen_Decl : Node_Id; Inst : Node_Id);
-   --  Add the context clause of the unit containing a generic unit to a
-   --  compilation unit that is, or contains, an instantiation.
-
-   function Get_Associated_Node (N : Node_Id) return Node_Id;
-   --  In order to propagate semantic information back from the analyzed copy
-   --  to the original generic, we maintain links between selected nodes in the
-   --  generic and their corresponding copies. At the end of generic analysis,
-   --  the routine Save_Global_References traverses the generic tree, examines
-   --  the semantic information, and preserves the links to those nodes that
-   --  contain global information. At instantiation, the information from the
-   --  associated node is placed on the new copy, so that name resolution is
-   --  not repeated.
-   --
-   --  Three kinds of source nodes have associated nodes:
-   --
-   --    a) those that can reference (denote) entities, that is identifiers,
-   --       character literals, expanded_names, operator symbols, operators,
-   --       and attribute reference nodes. These nodes have an Entity field
-   --       and are the set of nodes that are in N_Has_Entity.
-   --
-   --    b) aggregates (N_Aggregate and N_Extension_Aggregate)
-   --
-   --    c) selected components (N_Selected_Component)
-   --
-   --  For the first class, the associated node preserves the entity if it is
-   --  global. If the generic contains nested instantiations, the associated
-   --  node itself has been recopied, and a chain of them must be followed.
-   --
-   --  For aggregates, the associated node allows retrieval of the type, which
-   --  may otherwise not appear in the generic. The view of this type may be
-   --  different between generic and instantiation, and the full view can be
-   --  installed before the instantiation is analyzed. For aggregates of type
-   --  extensions, the same view exchange may have to be performed for some of
-   --  the ancestor types, if their view is private at the point of
-   --  instantiation.
-   --
-   --  Nodes that are selected components in the parse tree may be rewritten
-   --  as expanded names after resolution, and must be treated as potential
-   --  entity holders, which is why they also have an Associated_Node.
-   --
-   --  Nodes that do not come from source, such as freeze nodes, do not appear
-   --  in the generic tree, and need not have an associated node.
-   --
-   --  The associated node is stored in the Associated_Node field. Note that
-   --  this field overlaps Entity, which is fine, because the whole point is
-   --  that we don't need or want the normal Entity field in this situation.
-
    procedure Map_Formal_Package_Entities (Form : Entity_Id; Act : Entity_Id);
    --  Within the generic part, entities in the formal package are
    --  visible. To validate subsequent type declarations, indicate
@@ -740,6 +831,31 @@ package body Sem_Ch12 is
    --  before installing parents of generics, that are not visible for the
    --  actuals themselves.
 
+   procedure Remove_Parent (In_Body : Boolean := False);
+   --  Reverse effect after instantiation of child is complete
+
+   procedure Restore_Hidden_Primitives (Prims_List : in out Elist_Id);
+   --  Restore suffix 'P' to primitives of Prims_List and leave Prims_List
+   --  set to No_Elist.
+
+   procedure Save_Global_References_In_Aspects (N : Node_Id);
+   --  Save all global references found within the expressions of all aspects
+   --  that appear on node N.
+
+   procedure Set_Instance_Env
+     (Gen_Unit : Entity_Id;
+      Act_Unit : Entity_Id);
+   --  Save current instance on saved environment, to be used to determine
+   --  the global status of entities in nested instances. Part of Save_Env.
+   --  called after verifying that the generic unit is legal for the instance,
+   --  The procedure also examines whether the generic unit is a predefined
+   --  unit, in order to set configuration switches accordingly. As a result
+   --  the procedure must be called after analyzing and freezing the actuals.
+
+   procedure Set_Instance_Of (A : Entity_Id; B : Entity_Id);
+   --  Associate analyzed generic parameter with corresponding instance. Used
+   --  for semantic checks at instantiation time.
+
    function True_Parent (N : Node_Id) return Node_Id;
    --  For a subunit, return parent of corresponding stub, else return
    --  parent of node.
@@ -921,7 +1037,7 @@ package body Sem_Ch12 is
    is
       Actuals_To_Freeze : constant Elist_Id  := New_Elmt_List;
       Assoc             : constant List_Id   := New_List;
-      Default_Actuals   : constant Elist_Id  := New_Elmt_List;
+      Default_Actuals   : constant List_Id   := New_List;
       Gen_Unit          : constant Entity_Id :=
                             Defining_Entity (Parent (F_Copy));
 
@@ -951,7 +1067,7 @@ package body Sem_Ch12 is
 
       Others_Present : Boolean := False;
       Others_Choice  : Node_Id := Empty;
-      --  In Ada 2005, indicates partial parametrization of a formal
+      --  In Ada 2005, indicates partial parameterization of a formal
       --  package. As usual an other association must be last in the list.
 
       procedure Check_Overloaded_Formal_Subprogram (Formal : Entity_Id);
@@ -978,7 +1094,7 @@ package body Sem_Ch12 is
       --  but return Empty for the actual itself. In this case the code below
       --  creates a corresponding declaration for the formal.
 
-      function Partial_Parametrization return Boolean;
+      function Partial_Parameterization return Boolean;
       --  Ada 2005: if no match is found for a given formal, check if the
       --  association for it includes a box, or whether the associations
       --  include an Others clause.
@@ -1168,15 +1284,15 @@ package body Sem_Ch12 is
          return Act;
       end Matching_Actual;
 
-      -----------------------------
-      -- Partial_Parametrization --
-      -----------------------------
+      ------------------------------
+      -- Partial_Parameterization --
+      ------------------------------
 
-      function Partial_Parametrization return Boolean is
+      function Partial_Parameterization return Boolean is
       begin
          return Others_Present
           or else (Present (Found_Assoc) and then Box_Present (Found_Assoc));
-      end Partial_Parametrization;
+      end Partial_Parameterization;
 
       ---------------------
       -- Process_Default --
@@ -1208,7 +1324,8 @@ package body Sem_Ch12 is
          if No (Found_Assoc) then
             Default :=
                Make_Generic_Association (Loc,
-                 Selector_Name => New_Occurrence_Of (Id, Loc),
+                 Selector_Name                     =>
+                   New_Occurrence_Of (Id, Loc),
                  Explicit_Generic_Actual_Parameter => Empty);
             Set_Box_Present (Default);
             Append (Default, Default_Formals);
@@ -1289,7 +1406,7 @@ package body Sem_Ch12 is
 
       if Present (Actuals) then
 
-         --  Check for an Others choice, indicating a partial parametrization
+         --  Check for an Others choice, indicating a partial parameterization
          --  for a formal package.
 
          Actual := First (Actuals);
@@ -1384,36 +1501,66 @@ package body Sem_Ch12 is
             case Nkind (Formal) is
                when N_Formal_Object_Declaration =>
                   Match :=
-                    Matching_Actual (
-                      Defining_Identifier (Formal),
-                      Defining_Identifier (Analyzed_Formal));
+                    Matching_Actual
+                      (Defining_Identifier (Formal),
+                       Defining_Identifier (Analyzed_Formal));
 
-                  if No (Match) and then Partial_Parametrization then
+                  if No (Match) and then Partial_Parameterization then
                      Process_Default (Formal);
+
                   else
                      Append_List
                        (Instantiate_Object (Formal, Match, Analyzed_Formal),
                         Assoc);
+
+                     --  For a defaulted in_parameter, create an entry in the
+                     --  the list of defaulted actuals, for GNATProve use. Do
+                     --  not included these defaults for an instance nested
+                     --  within a generic, because the defaults are also used
+                     --  in the analysis of the enclosing generic, and only
+                     --  defaulted subprograms are relevant there.
+
+                     if No (Match) and then not Inside_A_Generic then
+                        Append_To (Default_Actuals,
+                          Make_Generic_Association (Sloc (I_Node),
+                            Selector_Name                     =>
+                              New_Occurrence_Of
+                                (Defining_Identifier (Formal), Sloc (I_Node)),
+                            Explicit_Generic_Actual_Parameter =>
+                              New_Copy_Tree (Default_Expression (Formal))));
+                     end if;
+                  end if;
+
+                  --  If the object is a call to an expression function, this
+                  --  is a freezing point for it.
+
+                  if Is_Entity_Name (Match)
+                    and then Present (Entity (Match))
+                    and then Nkind
+                      (Original_Node (Unit_Declaration_Node (Entity (Match))))
+                                                     = N_Expression_Function
+                  then
+                     Append_Elmt (Entity (Match), Actuals_To_Freeze);
                   end if;
 
                when N_Formal_Type_Declaration =>
                   Match :=
-                    Matching_Actual (
-                      Defining_Identifier (Formal),
-                      Defining_Identifier (Analyzed_Formal));
+                    Matching_Actual
+                      (Defining_Identifier (Formal),
+                       Defining_Identifier (Analyzed_Formal));
 
                   if No (Match) then
-                     if Partial_Parametrization then
+                     if Partial_Parameterization then
                         Process_Default (Formal);
 
                      else
                         Error_Msg_Sloc := Sloc (Gen_Unit);
                         Error_Msg_NE
                           ("missing actual&",
-                            Instantiation_Node,
-                              Defining_Identifier (Formal));
-                        Error_Msg_NE ("\in instantiation of & declared#",
-                            Instantiation_Node, Gen_Unit);
+                           Instantiation_Node, Defining_Identifier (Formal));
+                        Error_Msg_NE
+                          ("\in instantiation of & declared#",
+                           Instantiation_Node, Gen_Unit);
                         Abandon_Instantiation (Instantiation_Node);
                      end if;
 
@@ -1461,10 +1608,10 @@ package body Sem_Ch12 is
                   then
                      declare
                         Formal_Ent : constant Entity_Id :=
-                                        Defining_Identifier (Analyzed_Formal);
+                                       Defining_Identifier (Analyzed_Formal);
                      begin
                         if Is_Remote_Access_To_Class_Wide_Type (Entity (Match))
-                             = Is_Remote_Types (Formal_Ent)
+                                                = Is_Remote_Types (Formal_Ent)
                         then
                            --  Remoteness of formal and actual match
 
@@ -1505,11 +1652,11 @@ package body Sem_Ch12 is
                      Check_Overloaded_Formal_Subprogram (Formal);
                   end if;
 
-                  --  If there is no corresponding actual, this may be case of
-                  --  partial parametrization, or else the formal has a default
-                  --  or a box.
+                  --  If there is no corresponding actual, this may be case
+                  --  of partial parameterization, or else the formal has a
+                  --  default or a box.
 
-                  if No (Match) and then Partial_Parametrization then
+                  if No (Match) and then Partial_Parameterization then
                      Process_Default (Formal);
 
                      if Nkind (I_Node) = N_Formal_Package_Declaration then
@@ -1554,33 +1701,42 @@ package body Sem_Ch12 is
                   end if;
 
                   --  If this is a nested generic, preserve default for later
-                  --  instantiations.
+                  --  instantiations. We do this as well for GNATProve use,
+                  --  so that the list of generic associations is complete.
 
-                  if No (Match)
-                    and then Box_Present (Formal)
-                  then
-                     Append_Elmt
-                       (Defining_Unit_Name (Specification (Last (Assoc))),
-                        Default_Actuals);
+                  if No (Match) and then Box_Present (Formal) then
+                     declare
+                        Subp : constant Entity_Id :=
+                          Defining_Unit_Name (Specification (Last (Assoc)));
+
+                     begin
+                        Append_To (Default_Actuals,
+                          Make_Generic_Association (Sloc (I_Node),
+                            Selector_Name                     =>
+                              New_Occurrence_Of (Subp, Sloc (I_Node)),
+                            Explicit_Generic_Actual_Parameter =>
+                              New_Occurrence_Of (Subp, Sloc (I_Node))));
+                     end;
                   end if;
 
                when N_Formal_Package_Declaration =>
                   Match :=
-                    Matching_Actual (
-                      Defining_Identifier (Formal),
-                      Defining_Identifier (Original_Node (Analyzed_Formal)));
+                    Matching_Actual
+                      (Defining_Identifier (Formal),
+                       Defining_Identifier (Original_Node (Analyzed_Formal)));
 
                   if No (Match) then
-                     if Partial_Parametrization then
+                     if Partial_Parameterization then
                         Process_Default (Formal);
 
                      else
                         Error_Msg_Sloc := Sloc (Gen_Unit);
                         Error_Msg_NE
                           ("missing actual&",
-                            Instantiation_Node, Defining_Identifier (Formal));
-                        Error_Msg_NE ("\in instantiation of & declared#",
-                            Instantiation_Node, Gen_Unit);
+                           Instantiation_Node, Defining_Identifier (Formal));
+                        Error_Msg_NE
+                          ("\in instantiation of & declared#",
+                           Instantiation_Node, Gen_Unit);
 
                         Abandon_Instantiation (Instantiation_Node);
                      end if;
@@ -1623,14 +1779,13 @@ package body Sem_Ch12 is
 
             if Present (Selector_Name (Actual)) then
                Error_Msg_NE
-                 ("unmatched actual&",
-                    Actual, Selector_Name (Actual));
-               Error_Msg_NE ("\in instantiation of& declared#",
-                    Actual, Gen_Unit);
+                 ("unmatched actual &", Actual, Selector_Name (Actual));
+               Error_Msg_NE
+                 ("\in instantiation of & declared#", Actual, Gen_Unit);
             else
                Error_Msg_NE
-                 ("unmatched actual in instantiation of& declared#",
-                   Actual, Gen_Unit);
+                 ("unmatched actual in instantiation of & declared#",
+                  Actual, Gen_Unit);
             end if;
          end if;
 
@@ -1656,30 +1811,24 @@ package body Sem_Ch12 is
       --  explicit associations for them. This is required if the instance
       --  appears within a generic.
 
-      declare
-         Elmt  : Elmt_Id;
-         Subp  : Entity_Id;
-         New_D : Node_Id;
+      if not Is_Empty_List (Default_Actuals) then
+         declare
+            Default : Node_Id;
+
+         begin
+            Default := First (Default_Actuals);
+            while Present (Default) loop
+               Mark_Rewrite_Insertion (Default);
+               Next (Default);
+            end loop;
 
-      begin
-         Elmt := First_Elmt (Default_Actuals);
-         while Present (Elmt) loop
             if No (Actuals) then
-               Actuals := New_List;
-               Set_Generic_Associations (I_Node, Actuals);
-            end if;
-
-            Subp := Node (Elmt);
-            New_D :=
-              Make_Generic_Association (Sloc (Subp),
-                Selector_Name => New_Occurrence_Of (Subp, Sloc (Subp)),
-                  Explicit_Generic_Actual_Parameter =>
-                    New_Occurrence_Of (Subp, Sloc (Subp)));
-            Mark_Rewrite_Insertion (New_D);
-            Append_To (Actuals, New_D);
-            Next_Elmt (Elmt);
-         end loop;
-      end;
+               Set_Generic_Associations (I_Node, Default_Actuals);
+            else
+               Append_List_To (Actuals, Default_Actuals);
+            end if;
+         end;
+      end if;
 
       --  If this is a formal package, normalize the parameter list by adding
       --  explicit box associations for the formals that are covered by an
@@ -1741,8 +1890,8 @@ package body Sem_Ch12 is
       then
          Error_Msg_N
            ("in a formal, a subtype indication can only be "
-             & "a subtype mark (RM 12.5.3(3))",
-             Subtype_Indication (Component_Definition (Def)));
+            & "a subtype mark (RM 12.5.3(3))",
+            Subtype_Indication (Component_Definition (Def)));
       end if;
 
    end Analyze_Formal_Array_Type;
@@ -1776,6 +1925,22 @@ package body Sem_Ch12 is
       Delta_Val : constant Ureal := Ureal_1;
       Digs_Val  : constant Uint  := Uint_6;
 
+      function Make_Dummy_Bound return Node_Id;
+      --  Return a properly typed universal real literal to use as a bound
+
+      ----------------------
+      -- Make_Dummy_Bound --
+      ----------------------
+
+      function Make_Dummy_Bound return Node_Id is
+         Bound : constant Node_Id := Make_Real_Literal (Loc, Ureal_1);
+      begin
+         Set_Etype (Bound, Universal_Real);
+         return Bound;
+      end Make_Dummy_Bound;
+
+   --  Start of processing for Analyze_Formal_Decimal_Fixed_Point_Type
+
    begin
       Enter_Name (T);
 
@@ -1788,8 +1953,8 @@ package body Sem_Ch12 is
       Set_Small_Value    (Base, Delta_Val);
       Set_Scalar_Range   (Base,
         Make_Range (Loc,
-          Low_Bound  => Make_Real_Literal (Loc, Ureal_1),
-          High_Bound => Make_Real_Literal (Loc, Ureal_1)));
+          Low_Bound  => Make_Dummy_Bound,
+          High_Bound => Make_Dummy_Bound));
 
       Set_Is_Generic_Type (Base);
       Set_Parent          (Base, Parent (Def));
@@ -1863,10 +2028,10 @@ package body Sem_Ch12 is
       else
          New_N :=
            Make_Full_Type_Declaration (Loc,
-             Defining_Identifier => T,
+             Defining_Identifier         => T,
              Discriminant_Specifications =>
                Discriminant_Specifications (Parent (T)),
-             Type_Definition =>
+             Type_Definition             =>
                Make_Derived_Type_Definition (Loc,
                  Subtype_Indication => Subtype_Mark (Def)));
 
@@ -1931,13 +2096,13 @@ package body Sem_Ch12 is
       Lo :=
         Make_Attribute_Reference (Loc,
           Attribute_Name => Name_First,
-          Prefix         => New_Reference_To (T, Loc));
+          Prefix         => New_Occurrence_Of (T, Loc));
       Set_Etype (Lo, T);
 
       Hi :=
         Make_Attribute_Reference (Loc,
           Attribute_Name => Name_Last,
-          Prefix         => New_Reference_To (T, Loc));
+          Prefix         => New_Occurrence_Of (T, Loc));
       Set_Etype (Hi, T);
 
       Set_Scalar_Range (T,
@@ -2006,7 +2171,7 @@ package body Sem_Ch12 is
       New_N :=
         Make_Full_Type_Declaration (Loc,
           Defining_Identifier => T,
-          Type_Definition => Def);
+          Type_Definition     => Def);
 
       Rewrite (N, New_N);
       Analyze (N);
@@ -2067,8 +2232,7 @@ package body Sem_Ch12 is
 
             elsif Can_Never_Be_Null (T) then
                Error_Msg_NE
-                 ("`NOT NULL` not allowed (& already excludes null)",
-                    N, T);
+                 ("`NOT NULL` not allowed (& already excludes null)", N, T);
             end if;
          end if;
 
@@ -2135,15 +2299,12 @@ package body Sem_Ch12 is
          Set_Ekind (Id, K);
          Set_Etype (Id, T);
 
-         if (Is_Array_Type (T)
-              and then not Is_Constrained (T))
-           or else
-            (Ekind (T) = E_Record_Type
-              and then Has_Discriminants (T))
+         if (Is_Array_Type (T) and then not Is_Constrained (T))
+           or else (Ekind (T) = E_Record_Type and then Has_Discriminants (T))
          then
             declare
                Non_Freezing_Ref : constant Node_Id :=
-                                    New_Reference_To (Id, Sloc (Id));
+                                    New_Occurrence_Of (Id, Sloc (Id));
                Decl : Node_Id;
 
             begin
@@ -2261,10 +2422,11 @@ package body Sem_Ch12 is
                  (Specification (Original_Node (Gen_Decl)),
                     Empty, Instantiating => True));
 
-         Renaming := Make_Package_Renaming_Declaration (Loc,
+         Renaming :=
+           Make_Package_Renaming_Declaration (Loc,
              Defining_Unit_Name =>
                Make_Defining_Identifier (Loc, Chars (Gen_Unit)),
-             Name => New_Occurrence_Of (Formal, Loc));
+             Name               => New_Occurrence_Of (Formal, Loc));
 
          if Nkind (Gen_Id) = N_Identifier
            and then Chars (Gen_Id) = Chars (Pack_Id)
@@ -2346,7 +2508,7 @@ package body Sem_Ch12 is
    --  Start of processing for Analyze_Formal_Package_Declaration
 
    begin
-      Text_IO_Kludge (Gen_Id);
+      Check_Text_IO_Special_Unit (Gen_Id);
 
       Init_Env;
       Check_Generic_Child_Unit (Gen_Id, Parent_Installed);
@@ -2372,10 +2534,10 @@ package body Sem_Ch12 is
          Restore_Env;
          goto Leave;
 
-      elsif  Gen_Unit = Current_Scope then
+      elsif Gen_Unit = Current_Scope then
          Error_Msg_N
            ("generic package cannot be used as a formal package of itself",
-             Gen_Id);
+            Gen_Id);
          Restore_Env;
          goto Leave;
 
@@ -2388,14 +2550,12 @@ package body Sem_Ch12 is
 
             Error_Msg_N
               ("generic parent cannot be used as formal package "
-                & "of a child unit",
-                Gen_Id);
+               & "of a child unit", Gen_Id);
 
          else
             Error_Msg_N
               ("generic package cannot be used as a formal package "
-                & "within itself",
-                Gen_Id);
+               & "within itself", Gen_Id);
             Restore_Env;
             goto Leave;
          end if;
@@ -2417,7 +2577,7 @@ package body Sem_Ch12 is
          if Chars (Gen_Name) = Chars (Pack_Id) then
             Error_Msg_NE
              ("& is hidden within declaration of formal package",
-               Gen_Id, Gen_Name);
+              Gen_Id, Gen_Name);
          end if;
       end;
 
@@ -2481,9 +2641,8 @@ package body Sem_Ch12 is
       Set_Inner_Instances (Formal, New_Elmt_List);
       Push_Scope  (Formal);
 
-      if Is_Child_Unit (Gen_Unit)
-        and then Parent_Installed
-      then
+      if Is_Child_Unit (Gen_Unit) and then Parent_Installed then
+
          --  Similarly, we have to make the name of the formal visible in the
          --  parent instance, to resolve properly fully qualified names that
          --  may appear in the generic unit. The parent instance has been
@@ -2516,15 +2675,11 @@ package body Sem_Ch12 is
       begin
          E := First_Entity (Formal);
          while Present (E) loop
-            if Associations
-              and then not Is_Generic_Formal (E)
-            then
+            if Associations and then not Is_Generic_Formal (E) then
                Set_Is_Hidden (E);
             end if;
 
-            if Ekind (E) = E_Package
-              and then Renamed_Entity (E) = Formal
-            then
+            if Ekind (E) = E_Package and then Renamed_Entity (E) = Formal then
                Set_Is_Hidden (E);
                exit;
             end if;
@@ -2675,8 +2830,8 @@ package body Sem_Ch12 is
               and then Is_Incomplete_Type (Ctrl_Type)
             then
                Error_Msg_NE
-                 ("controlling type of abstract formal subprogram cannot " &
-                     "be incomplete type", N, Ctrl_Type);
+                 ("controlling type of abstract formal subprogram cannot "
+                  & "be incomplete type", N, Ctrl_Type);
 
             else
                Check_Controlling_Formals (Ctrl_Type, Nam);
@@ -2952,7 +3107,6 @@ package body Sem_Ch12 is
       --  caller.
 
       Gen_Parm_Decl := First (Generic_Formal_Declarations (N));
-
       while Present (Gen_Parm_Decl) loop
          Analyze (Gen_Parm_Decl);
          Next (Gen_Parm_Decl);
@@ -2976,7 +3130,12 @@ package body Sem_Ch12 is
       Decl        : Node_Id;
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      --  The generic package declaration may be subject to pragma Ghost with
+      --  policy Ignore. Set the mode now to ensure that any nodes generated
+      --  during analysis and expansion are properly flagged as ignored Ghost.
+
+      Set_Ghost_Mode (N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
       --  We introduce a renaming of the enclosing package, to have a usable
       --  entity as the prefix of an expanded name for a local entity of the
@@ -2989,13 +3148,12 @@ package body Sem_Ch12 is
           Defining_Unit_Name =>
             Make_Defining_Identifier (Loc,
              Chars => New_External_Name (Chars (Defining_Entity (N)), "GH")),
-          Name => Make_Identifier (Loc, Chars (Defining_Entity (N))));
+          Name               =>
+            Make_Identifier (Loc, Chars (Defining_Entity (N))));
 
       if Present (Decls) then
          Decl := First (Decls);
-         while Present (Decl)
-           and then Nkind (Decl) = N_Pragma
-         loop
+         while Present (Decl) and then Nkind (Decl) = N_Pragma loop
             Next (Decl);
          end loop;
 
@@ -3019,6 +3177,18 @@ package body Sem_Ch12 is
       New_N := Copy_Generic_Node (N, Empty, Instantiating => False);
       Set_Parent_Spec (New_N, Save_Parent);
       Rewrite (N, New_N);
+
+      --  Once the contents of the generic copy and the template are swapped,
+      --  do the same for their respective aspect specifications.
+
+      Exchange_Aspects (N, New_N);
+
+      --  Collect all contract-related source pragmas found within the template
+      --  and attach them to the contract of the package spec. This contract is
+      --  used in the capture of global references within annotations.
+
+      Create_Generic_Contract (N);
+
       Id := Defining_Entity (N);
       Generate_Definition (Id);
 
@@ -3027,9 +3197,15 @@ package body Sem_Ch12 is
       Start_Generic;
 
       Enter_Name (Id);
-      Set_Ekind    (Id, E_Generic_Package);
-      Set_Etype    (Id, Standard_Void_Type);
-      Set_Contract (Id, Make_Contract (Sloc (Id)));
+      Set_Ekind  (Id, E_Generic_Package);
+      Set_Etype  (Id, Standard_Void_Type);
+
+      --  A generic package declared within a Ghost region is rendered Ghost
+      --  (SPARK RM 6.9(2)).
+
+      if Ghost_Mode > None then
+         Set_Is_Ghost_Entity (Id);
+      end if;
 
       --  Analyze aspects now, so that generated pragmas appear in the
       --  declarations before building and analyzing the generic copy.
@@ -3089,6 +3265,27 @@ package body Sem_Ch12 is
          end if;
       end if;
 
+      --  If there is a specified storage pool in the context, create an
+      --  aspect on the package declaration, so that it is used in any
+      --  instance that does not override it.
+
+      if Present (Default_Pool) then
+         declare
+            ASN : Node_Id;
+
+         begin
+            ASN :=
+              Make_Aspect_Specification (Loc,
+                Identifier => Make_Identifier (Loc, Name_Default_Storage_Pool),
+                Expression => New_Copy (Default_Pool));
+
+            if No (Aspect_Specifications (Specification (N))) then
+               Set_Aspect_Specifications (Specification (N), New_List (ASN));
+            else
+               Append (ASN, Aspect_Specifications (Specification (N)));
+            end if;
+         end;
+      end if;
    end Analyze_Generic_Package_Declaration;
 
    --------------------------------------------
@@ -3096,16 +3293,22 @@ package body Sem_Ch12 is
    --------------------------------------------
 
    procedure Analyze_Generic_Subprogram_Declaration (N : Node_Id) is
-      Spec        : Node_Id;
-      Id          : Entity_Id;
       Formals     : List_Id;
+      Id          : Entity_Id;
       New_N       : Node_Id;
       Result_Type : Entity_Id;
       Save_Parent : Node_Id;
+      Spec        : Node_Id;
       Typ         : Entity_Id;
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      --  The generic subprogram declaration may be subject to pragma Ghost
+      --  with policy Ignore. Set the mode now to ensure that any nodes
+      --  generated during analysis and expansion are properly flagged as
+      --  ignored Ghost.
+
+      Set_Ghost_Mode (N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
       --  Create copy of generic unit, and save for instantiation. If the unit
       --  is a child unit, do not copy the specifications for the parent, which
@@ -3118,24 +3321,20 @@ package body Sem_Ch12 is
       Set_Parent_Spec (New_N, Save_Parent);
       Rewrite (N, New_N);
 
-      --  The aspect specifications are not attached to the tree, and must
-      --  be copied and attached to the generic copy explicitly.
+      --  Once the contents of the generic copy and the template are swapped,
+      --  do the same for their respective aspect specifications.
 
-      if Present (Aspect_Specifications (New_N)) then
-         declare
-            Aspects : constant List_Id := Aspect_Specifications (N);
-         begin
-            Set_Has_Aspects (N, False);
-            Move_Aspects (New_N, To => N);
-            Set_Has_Aspects (Original_Node (N), False);
-            Set_Aspect_Specifications (Original_Node (N), Aspects);
-         end;
-      end if;
+      Exchange_Aspects (N, New_N);
+
+      --  Collect all contract-related source pragmas found within the template
+      --  and attach them to the contract of the subprogram spec. This contract
+      --  is used in the capture of global references within annotations.
+
+      Create_Generic_Contract (N);
 
       Spec := Specification (N);
       Id := Defining_Entity (Spec);
       Generate_Definition (Id);
-      Set_Contract (Id, Make_Contract (Sloc (Id)));
 
       if Nkind (Id) = N_Defining_Operator_Symbol then
          Error_Msg_N
@@ -3145,8 +3344,15 @@ package body Sem_Ch12 is
       Start_Generic;
 
       Enter_Name (Id);
-
       Set_Scope_Depth_Value (Id, Scope_Depth (Current_Scope) + 1);
+
+      --  Analyze the aspects of the generic copy to ensure that all generated
+      --  pragmas (if any) perform their semantic effects.
+
+      if Has_Aspects (N) then
+         Analyze_Aspect_Specifications (N, Id);
+      end if;
+
       Push_Scope (Id);
       Enter_Generic_Scope (Id);
       Set_Inner_Instances (Id, New_Elmt_List);
@@ -3176,8 +3382,9 @@ package body Sem_Ch12 is
             if Is_Abstract_Type (Designated_Type (Result_Type))
               and then Ada_Version >= Ada_2012
             then
-               Error_Msg_N ("generic function cannot have an access result"
-                 & " that designates an abstract type", Spec);
+               Error_Msg_N
+                 ("generic function cannot have an access result "
+                  & "that designates an abstract type", Spec);
             end if;
 
          else
@@ -3213,6 +3420,13 @@ package body Sem_Ch12 is
          Set_Etype (Id, Standard_Void_Type);
       end if;
 
+      --  A generic subprogram declared within a Ghost region is rendered Ghost
+      --  (SPARK RM 6.9(2)).
+
+      if Ghost_Mode > None then
+         Set_Is_Ghost_Entity (Id);
+      end if;
+
       --  For a library unit, we have reconstructed the entity for the unit,
       --  and must reset it in the library tables. We also make sure that
       --  Body_Required is set properly in the original compilation unit node.
@@ -3225,51 +3439,13 @@ package body Sem_Ch12 is
       Set_Categorization_From_Pragmas (N);
       Validate_Categorization_Dependency (N, Id);
 
-      Save_Global_References (Original_Node (N));
-
-      --  For ASIS purposes, convert any postcondition, precondition pragmas
-      --  into aspects, if N is not a compilation unit by itself, in order to
-      --  enable the analysis of expressions inside the corresponding PPC
-      --  pragmas.
-
-      if ASIS_Mode and then Is_List_Member (N) then
-         Make_Aspect_For_PPC_In_Gen_Sub_Decl (N);
-      end if;
-
-      --  To capture global references, analyze the expressions of aspects,
-      --  and propagate information to original tree. Note that in this case
-      --  analysis of attributes is not delayed until the freeze point.
-
-      --  It seems very hard to recreate the proper visibility of the generic
-      --  subprogram at a later point because the analysis of an aspect may
-      --  create pragmas after the generic copies have been made ???
-
-      if Has_Aspects (N) then
-         declare
-            Aspect : Node_Id;
-
-         begin
-            Aspect := First (Aspect_Specifications (N));
-            while Present (Aspect) loop
-               if Get_Aspect_Id (Aspect) /= Aspect_Warnings
-                 and then Present (Expression (Aspect))
-               then
-                  Analyze (Expression (Aspect));
-               end if;
-
-               Next (Aspect);
-            end loop;
-
-            Aspect := First (Aspect_Specifications (Original_Node (N)));
-            while Present (Aspect) loop
-               if Present (Expression (Aspect)) then
-                  Save_Global_References (Expression (Aspect));
-               end if;
+      --  Capture all global references that occur within the profile of the
+      --  generic subprogram. Aspects are not part of this processing because
+      --  they must be delayed. If processed now, Save_Global_References will
+      --  destroy the Associated_Node links and prevent the capture of global
+      --  references when the contract of the generic subprogram is analyzed.
 
-               Next (Aspect);
-            end loop;
-         end;
-      end if;
+      Save_Global_References (Original_Node (N));
 
       End_Generic;
       End_Scope;
@@ -3294,17 +3470,26 @@ package body Sem_Ch12 is
       Act_Tree      : Node_Id;
 
       Gen_Decl : Node_Id;
+      Gen_Spec : Node_Id;
       Gen_Unit : Entity_Id;
 
       Is_Actual_Pack : constant Boolean :=
                          Is_Internal (Defining_Entity (N));
 
-      Env_Installed    : Boolean := False;
-      Parent_Installed : Boolean := False;
-      Renaming_List    : List_Id;
-      Unit_Renaming    : Node_Id;
-      Needs_Body       : Boolean;
-      Inline_Now       : Boolean := False;
+      Env_Installed     : Boolean := False;
+      Parent_Installed  : Boolean := False;
+      Renaming_List     : List_Id;
+      Unit_Renaming     : Node_Id;
+      Needs_Body        : Boolean;
+      Inline_Now        : Boolean := False;
+      Has_Inline_Always : Boolean := False;
+
+      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
+      Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the SPARK_Mode-related data for restore on exit
 
       Save_Style_Check : constant Boolean := Style_Check;
       --  Save style check mode for restore on exit
@@ -3318,11 +3503,6 @@ package body Sem_Ch12 is
       --  but it is simpler than detecting the need for the body at the point
       --  of inlining, when the context of the instance is not available.
 
-      function Must_Inline_Subp return Boolean;
-      --  If inlining is active and the generic contains inlined subprograms,
-      --  return True if some of the inlined subprograms must be inlined by
-      --  the frontend.
-
       -----------------------
       -- Delay_Descriptors --
       -----------------------
@@ -3349,37 +3529,13 @@ package body Sem_Ch12 is
          else
             E := First_Entity (Gen_Unit);
             while Present (E) loop
-               if Is_Subprogram (E)
-                 and then Is_Inlined (E)
-               then
-                  return True;
-               end if;
-
-               Next_Entity (E);
-            end loop;
-         end if;
-
-         return False;
-      end Might_Inline_Subp;
-
-      ----------------------
-      -- Must_Inline_Subp --
-      ----------------------
-
-      function Must_Inline_Subp return Boolean is
-         E : Entity_Id;
+               if Is_Subprogram (E) and then Is_Inlined (E) then
+                  --  Remember if there are any subprograms with Inline_Always
 
-      begin
-         if not Inline_Processing_Required then
-            return False;
+                  if Has_Pragma_Inline_Always (E) then
+                     Has_Inline_Always := True;
+                  end if;
 
-         else
-            E := First_Entity (Gen_Unit);
-            while Present (E) loop
-               if Is_Subprogram (E)
-                 and then Is_Inlined (E)
-                 and then Must_Inline (E)
-               then
                   return True;
                end if;
 
@@ -3388,7 +3544,7 @@ package body Sem_Ch12 is
          end if;
 
          return False;
-      end Must_Inline_Subp;
+      end Might_Inline_Subp;
 
       --  Local declarations
 
@@ -3399,12 +3555,12 @@ package body Sem_Ch12 is
    --  Start of processing for Analyze_Package_Instantiation
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
-      --  Very first thing: apply the special kludge for Text_IO processing
-      --  in case we are instantiating one of the children of [Wide_]Text_IO.
+      --  Very first thing: check for Text_IO sp[ecial unit in case we are
+      --  instantiating one of the children of [[Wide_]Wide_]Text_IO.
 
-      Text_IO_Kludge (Name (N));
+      Check_Text_IO_Special_Unit (Name (N));
 
       --  Make node global for error reporting
 
@@ -3425,7 +3581,8 @@ package body Sem_Ch12 is
          if Nkind (Defining_Unit_Name (N)) = N_Defining_Program_Unit_Name then
             Act_Decl_Name :=
               Make_Defining_Program_Unit_Name (Loc,
-                Name => New_Copy_Tree (Name (Defining_Unit_Name (N))),
+                Name                =>
+                  New_Copy_Tree (Name (Defining_Unit_Name (N))),
                 Defining_Identifier => Act_Decl_Id);
          else
             Act_Decl_Name :=  Act_Decl_Id;
@@ -3545,7 +3702,16 @@ package body Sem_Ch12 is
          goto Leave;
 
       else
+         --  If the context of the instance is subject to SPARK_Mode "off",
+         --  set the global flag which signals Analyze_Pragma to ignore all
+         --  SPARK_Mode pragmas within the instance.
+
+         if SPARK_Mode = Off then
+            Ignore_Pragma_SPARK_Mode := True;
+         end if;
+
          Gen_Decl := Unit_Declaration_Node (Gen_Unit);
+         Gen_Spec := Specification (Gen_Decl);
 
          --  Initialize renamings map, for error checking, and the list that
          --  holds private entities whose views have changed between generic
@@ -3582,7 +3748,6 @@ package body Sem_Ch12 is
          Set_Instance_Env (Gen_Unit, Act_Decl_Id);
          Set_Defining_Unit_Name (Act_Spec, Act_Decl_Name);
          Set_Is_Generic_Instance (Act_Decl_Id);
-
          Set_Generic_Parent (Act_Spec, Gen_Unit);
 
          --  References to the generic in its own declaration or its body are
@@ -3596,7 +3761,7 @@ package body Sem_Ch12 is
            Make_Package_Renaming_Declaration (Loc,
              Defining_Unit_Name =>
                Make_Defining_Identifier (Loc, Chars (Gen_Unit)),
-             Name => New_Reference_To (Act_Decl_Id, Loc));
+             Name               => New_Occurrence_Of (Act_Decl_Id, Loc));
 
          Append (Unit_Renaming, Renaming_List);
 
@@ -3610,9 +3775,60 @@ package body Sem_Ch12 is
             Set_Visible_Declarations (Act_Spec, Renaming_List);
          end if;
 
-         Act_Decl :=
-           Make_Package_Declaration (Loc,
-             Specification => Act_Spec);
+         Act_Decl := Make_Package_Declaration (Loc, Specification => Act_Spec);
+
+         --  Propagate the aspect specifications from the package declaration
+         --  template to the instantiated version of the package declaration.
+
+         if Has_Aspects (Act_Tree) then
+            Set_Aspect_Specifications (Act_Decl,
+              New_Copy_List_Tree (Aspect_Specifications (Act_Tree)));
+         end if;
+
+         --  The generic may have a generated Default_Storage_Pool aspect,
+         --  set at the point of generic declaration. If the instance has
+         --  that aspect, it overrides the one inherited from the generic.
+
+         if Has_Aspects (Gen_Spec) then
+            if No (Aspect_Specifications (N)) then
+               Set_Aspect_Specifications (N,
+                 (New_Copy_List_Tree
+                   (Aspect_Specifications (Gen_Spec))));
+
+            else
+               declare
+                  ASN1, ASN2 : Node_Id;
+
+               begin
+                  ASN1 := First (Aspect_Specifications (N));
+                  while Present (ASN1) loop
+                     if Chars (Identifier (ASN1)) = Name_Default_Storage_Pool
+                     then
+                        --  If generic carries a default storage pool, remove
+                        --  it in favor of the instance one.
+
+                        ASN2 := First (Aspect_Specifications (Gen_Spec));
+                        while Present (ASN2) loop
+                           if Chars (Identifier (ASN2)) =
+                                                    Name_Default_Storage_Pool
+                           then
+                              Remove (ASN2);
+                              exit;
+                           end if;
+
+                           Next (ASN2);
+                        end loop;
+                     end if;
+
+                     Next (ASN1);
+                  end loop;
+
+                  Prepend_List_To (Aspect_Specifications (N),
+                    (New_Copy_List_Tree
+                      (Aspect_Specifications (Gen_Spec))));
+               end;
+            end if;
+         end if;
 
          --  Save the instantiation node, for subsequent instantiation of the
          --  body, if there is one and we are generating code for the current
@@ -3636,10 +3852,7 @@ package body Sem_Ch12 is
               and then not Is_Child_Unit (Gen_Unit)
             then
                Scop := Scope (Gen_Unit);
-
-               while Present (Scop)
-                 and then Scop /= Standard_Standard
-               loop
+               while Present (Scop) and then Scop /= Standard_Standard loop
                   if Unit_Requires_Body (Scop) then
                      Enclosing_Body_Present := True;
                      exit;
@@ -3656,8 +3869,9 @@ package body Sem_Ch12 is
                end loop;
             end if;
 
-            --  If front-end inlining is enabled, and this is a unit for which
-            --  code will be generated, we instantiate the body at once.
+            --  If front-end inlining is enabled or there are any subprograms
+            --  marked with Inline_Always, and this is a unit for which code
+            --  will be generated, we instantiate the body at once.
 
             --  This is done if the instance is not the main unit, and if the
             --  generic is not a child unit of another generic, to avoid scope
@@ -3669,16 +3883,8 @@ package body Sem_Ch12 is
               and then Might_Inline_Subp
               and then not Is_Actual_Pack
             then
-               if not Debug_Flag_Dot_K
-                 and then Front_End_Inlining
-                 and then (Is_In_Main_Unit (N)
-                            or else In_Main_Context (Current_Scope))
-                 and then Nkind (Parent (N)) /= N_Compilation_Unit
-               then
-                  Inline_Now := True;
-
-               elsif Debug_Flag_Dot_K
-                 and then Must_Inline_Subp
+               if not Back_End_Inlining
+                 and then (Front_End_Inlining or else Has_Inline_Always)
                  and then (Is_In_Main_Unit (N)
                             or else In_Main_Context (Current_Scope))
                  and then Nkind (Parent (N)) /= N_Compilation_Unit
@@ -3721,22 +3927,24 @@ package body Sem_Ch12 is
 
             Needs_Body :=
               (Unit_Requires_Body (Gen_Unit)
-                  or else Enclosing_Body_Present
-                  or else Present (Corresponding_Body (Gen_Decl)))
-                and then (Is_In_Main_Unit (N) or else Might_Inline_Subp)
-                and then not Is_Actual_Pack
-                and then not Inline_Now
-                and then (Operating_Mode = Generate_Code
+                or else Enclosing_Body_Present
+                or else Present (Corresponding_Body (Gen_Decl)))
+               and then (Is_In_Main_Unit (N) or else Might_Inline_Subp)
+               and then not Is_Actual_Pack
+               and then not Inline_Now
+               and then (Operating_Mode = Generate_Code
 
-                           --  Need comment for this check ???
+                          --  Need comment for this check ???
 
-                           or else (Operating_Mode = Check_Semantics
-                                     and then (ASIS_Mode or GNATprove_Mode)));
+                          or else (Operating_Mode = Check_Semantics
+                                    and then (ASIS_Mode or GNATprove_Mode)));
 
-            --  If front_end_inlining is enabled, do not instantiate body if
-            --  within a generic context.
+            --  If front-end inlining is enabled or there are any subprograms
+            --  marked with Inline_Always, do not instantiate body when within
+            --  a generic context.
 
-            if (Front_End_Inlining and then not Expander_Active)
+            if ((Front_End_Inlining or else Has_Inline_Always)
+                  and then not Expander_Active)
               or else Is_Generic_Unit (Cunit_Entity (Main_Unit))
             then
                Needs_Body := False;
@@ -3924,6 +4132,40 @@ package body Sem_Ch12 is
          if Nkind (Parent (N)) /= N_Compilation_Unit then
             Mark_Rewrite_Insertion (Act_Decl);
             Insert_Before (N, Act_Decl);
+
+            if Has_Aspects (N) then
+               Analyze_Aspect_Specifications (N, Act_Decl_Id);
+
+               --  The pragma created for a Default_Storage_Pool aspect must
+               --  appear ahead of the declarations in the instance spec.
+               --  Analysis has placed it after the instance node, so remove
+               --  it and reinsert it properly now.
+
+               declare
+                  ASN : constant Node_Id := First (Aspect_Specifications (N));
+                  A_Name : constant Name_Id := Chars (Identifier (ASN));
+                  Decl : Node_Id;
+
+               begin
+                  if A_Name = Name_Default_Storage_Pool then
+                     if No (Visible_Declarations (Act_Spec)) then
+                        Set_Visible_Declarations (Act_Spec, New_List);
+                     end if;
+
+                     Decl := Next (N);
+                     while Present (Decl) loop
+                        if Nkind (Decl) = N_Pragma then
+                           Remove (Decl);
+                           Prepend (Decl, Visible_Declarations (Act_Spec));
+                           exit;
+                        end if;
+
+                        Next (Decl);
+                     end loop;
+                  end if;
+               end;
+            end if;
+
             Analyze (Act_Decl);
 
          --  For an instantiation that is a compilation unit, place
@@ -4044,7 +4286,14 @@ package body Sem_Ch12 is
          Set_Defining_Identifier (N, Act_Decl_Id);
       end if;
 
-      Style_Check := Save_Style_Check;
+      Ignore_Pragma_SPARK_Mode := Save_IPSM;
+      SPARK_Mode               := Save_SM;
+      SPARK_Mode_Pragma        := Save_SMP;
+      Style_Check              := Save_Style_Check;
+
+      if SPARK_Mode = On then
+         Dynamic_Elaboration_Checks := False;
+      end if;
 
       --  Check that if N is an instantiation of System.Dim_Float_IO or
       --  System.Dim_Integer_IO, the formal type has a dimension system.
@@ -4078,7 +4327,14 @@ package body Sem_Ch12 is
             Restore_Env;
          end if;
 
-         Style_Check := Save_Style_Check;
+         Ignore_Pragma_SPARK_Mode := Save_IPSM;
+         SPARK_Mode               := Save_SM;
+         SPARK_Mode_Pragma        := Save_SMP;
+         Style_Check              := Save_Style_Check;
+
+         if SPARK_Mode = On then
+            Dynamic_Elaboration_Checks := False;
+         end if;
    end Analyze_Package_Instantiation;
 
    --------------------------
@@ -4090,14 +4346,16 @@ package body Sem_Ch12 is
       Gen_Unit : Entity_Id;
       Act_Decl : Node_Id)
    is
-      Vis          : Boolean;
-      Gen_Comp     : constant Entity_Id :=
-                      Cunit_Entity (Get_Source_Unit (Gen_Unit));
-      Curr_Comp    : constant Node_Id := Cunit (Current_Sem_Unit);
-      Curr_Scope   : Entity_Id := Empty;
-      Curr_Unit    : constant Entity_Id := Cunit_Entity (Current_Sem_Unit);
-      Removed      : Boolean := False;
-      Num_Scopes   : Int := 0;
+      Curr_Comp : constant Node_Id   := Cunit (Current_Sem_Unit);
+      Curr_Unit : constant Entity_Id := Cunit_Entity (Current_Sem_Unit);
+      Gen_Comp  : constant Entity_Id :=
+                    Cunit_Entity (Get_Source_Unit (Gen_Unit));
+
+      Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save all SPARK_Mode-related attributes as removing enclosing scopes
+      --  to provide a clean environment for analysis of the inlined body will
+      --  eliminate any previously set SPARK_Mode.
 
       Scope_Stack_Depth : constant Int :=
                             Scope_Stack.Last - Scope_Stack.First + 1;
@@ -4105,10 +4363,14 @@ package body Sem_Ch12 is
       Use_Clauses  : array (1 .. Scope_Stack_Depth) of Node_Id;
       Instances    : array (1 .. Scope_Stack_Depth) of Entity_Id;
       Inner_Scopes : array (1 .. Scope_Stack_Depth) of Entity_Id;
+      Curr_Scope   : Entity_Id := Empty;
       List         : Elist_Id;
       Num_Inner    : Int := 0;
+      Num_Scopes   : Int := 0;
       N_Instances  : Int := 0;
+      Removed      : Boolean := False;
       S            : Entity_Id;
+      Vis          : Boolean;
 
    begin
       --  Case of generic unit defined in another unit. We must remove the
@@ -4131,14 +4393,13 @@ package body Sem_Ch12 is
 
                exit when Scope_Stack.Last - Num_Scopes + 1 = Scope_Stack.First
                  or else Scope_Stack.Table
-                           (Scope_Stack.Last - Num_Scopes).Entity
-                             = Scope (S);
+                           (Scope_Stack.Last - Num_Scopes).Entity = Scope (S);
             end loop;
 
             exit when Is_Generic_Instance (S)
               and then (In_Package_Body (S)
-                          or else Ekind (S) = E_Procedure
-                          or else Ekind (S) = E_Function);
+                         or else Ekind (S) = E_Procedure
+                         or else Ekind (S) = E_Function);
             S := Scope (S);
          end loop;
 
@@ -4171,14 +4432,10 @@ package body Sem_Ch12 is
          --  must be made invisible as well.
 
          S := Current_Scope;
-
-         while Present (S)
-           and then S /= Standard_Standard
-         loop
+         while Present (S) and then S /= Standard_Standard loop
             if Is_Generic_Instance (S)
               and then (In_Package_Body (S)
-                          or else Ekind (S) = E_Procedure
-                            or else Ekind (S) = E_Function)
+                         or else Ekind_In (S, E_Procedure, E_Function))
             then
                --  We still have to remove the entities of the enclosing
                --  instance from direct visibility.
@@ -4200,9 +4457,8 @@ package body Sem_Ch12 is
               or else (Ekind (Curr_Unit) = E_Package_Body
                         and then S = Spec_Entity (Curr_Unit))
               or else (Ekind (Curr_Unit) = E_Subprogram_Body
-                        and then S =
-                          Corresponding_Spec
-                            (Unit_Declaration_Node (Curr_Unit)))
+                        and then S = Corresponding_Spec
+                                       (Unit_Declaration_Node (Curr_Unit)))
             then
                Removed := True;
 
@@ -4238,8 +4494,13 @@ package body Sem_Ch12 is
 
             S := Scope (S);
          end loop;
+
          pragma Assert (Num_Inner < Num_Scopes);
 
+         --  The inlined package body must be analyzed with the SPARK_Mode of
+         --  the enclosing context, otherwise the body may cause bogus errors
+         --  if a configuration SPARK_Mode pragma in in effect.
+
          Push_Scope (Standard_Standard);
          Scope_Stack.Table (Scope_Stack.Last).Is_Active_Stack_Base := True;
          Instantiate_Package_Body
@@ -4253,8 +4514,8 @@ package body Sem_Ch12 is
                Version                  => Ada_Version,
                Version_Pragma           => Ada_Version_Pragma,
                Warnings                 => Save_Warnings,
-               SPARK_Mode               => SPARK_Mode,
-               SPARK_Mode_Pragma        => SPARK_Mode_Pragma)),
+               SPARK_Mode               => Save_SM,
+               SPARK_Mode_Pragma        => Save_SMP)),
             Inlined_Body => True);
 
          Pop_Scope;
@@ -4302,9 +4563,7 @@ package body Sem_Ch12 is
                   Par : Entity_Id;
                begin
                   Par := Scope (Curr_Scope);
-                  while (Present (Par))
-                    and then Par /= Standard_Standard
-                  loop
+                  while (Present (Par)) and then Par /= Standard_Standard loop
                      Install_Private_Declarations (Par);
                      Par := Scope (Par);
                   end loop;
@@ -4317,9 +4576,7 @@ package body Sem_Ch12 is
          --  scopes (and those local to the child unit itself) need to be
          --  installed explicitly.
 
-         if Is_Child_Unit (Curr_Unit)
-           and then Removed
-         then
+         if Is_Child_Unit (Curr_Unit) and then Removed then
             for J in reverse 1 .. Num_Inner + 1 loop
                Scope_Stack.Table (Scope_Stack.Last - J + 1).First_Use_Clause :=
                  Use_Clauses (J);
@@ -4347,8 +4604,7 @@ package body Sem_Ch12 is
                Set_Is_Generic_Instance (Inst, True);
 
                if In_Package_Body (Inst)
-                 or else Ekind (S) = E_Procedure
-                 or else Ekind (S) = E_Function
+                 or else Ekind_In (S, E_Procedure, E_Function)
                then
                   E := First_Entity (Instances (J));
                   while Present (E) loop
@@ -4359,7 +4615,9 @@ package body Sem_Ch12 is
             end loop;
          end;
 
-      --  If generic unit is in current unit, current context is correct
+      --  If generic unit is in current unit, current context is correct. Note
+      --  that the context is guaranteed to carry the correct SPARK_Mode as no
+      --  enclosing scopes were removed.
 
       else
          Instantiate_Package_Body
@@ -4470,7 +4728,13 @@ package body Sem_Ch12 is
       Gen_Decl         : Node_Id;
       Pack_Id          : Entity_Id;
       Parent_Installed : Boolean := False;
-      Renaming_List    : List_Id;
+
+      Renaming_List : List_Id;
+      --  The list of declarations that link formals and actuals of the
+      --  instance. These are subtype declarations for formal types, and
+      --  renaming declarations for other formals. The subprogram declaration
+      --  for the instance is then appended to the list, and the last item on
+      --  the list is the renaming declaration for the instance.
 
       procedure Analyze_Instance_And_Renamings;
       --  The instance must be analyzed in a context that includes the mappings
@@ -4479,6 +4743,19 @@ package body Sem_Ch12 is
       --  package. The subprogram instance is simply an alias for the internal
       --  subprogram, declared in the current scope.
 
+      procedure Build_Subprogram_Renaming;
+      --  If the subprogram is recursive, there are occurrences of the name of
+      --  the generic within the body, which must resolve to the current
+      --  instance. We add a renaming declaration after the declaration, which
+      --  is available in the instance body, as well as in the analysis of
+      --  aspects that appear in the generic. This renaming declaration is
+      --  inserted after the instance declaration which it renames.
+
+      procedure Instantiate_Subprogram_Contract (Templ : Node_Id);
+      --  Instantiate all source pragmas found in the contract of the generic
+      --  subprogram declaration template denoted by Templ. The instantiated
+      --  pragmas are added to list Renaming_List.
+
       ------------------------------------
       -- Analyze_Instance_And_Renamings --
       ------------------------------------
@@ -4511,11 +4788,12 @@ package body Sem_Ch12 is
                             Suffix_Index => Source_Offset (Sloc (Def_Ent))));
          end if;
 
-         Pack_Decl := Make_Package_Declaration (Loc,
-           Specification => Make_Package_Specification (Loc,
-             Defining_Unit_Name   => Pack_Id,
-             Visible_Declarations => Renaming_List,
-             End_Label            => Empty));
+         Pack_Decl :=
+           Make_Package_Declaration (Loc,
+             Specification => Make_Package_Specification (Loc,
+               Defining_Unit_Name   => Pack_Id,
+               Visible_Declarations => Renaming_List,
+               End_Label            => Empty));
 
          Set_Instance_Spec (N, Pack_Decl);
          Set_Is_Generic_Instance (Pack_Id);
@@ -4578,7 +4856,10 @@ package body Sem_Ch12 is
          Set_Parent            (Act_Decl_Id, Parent (Anon_Id));
          Set_Chars             (Act_Decl_Id, Chars (Defining_Entity (N)));
          Set_Sloc              (Act_Decl_Id, Sloc (Defining_Entity (N)));
-         Set_Comes_From_Source (Act_Decl_Id, True);
+
+         --  Subprogram instance comes from source only if generic does
+
+         Set_Comes_From_Source (Act_Decl_Id, Comes_From_Source (Gen_Unit));
 
          --  The signature may involve types that are not frozen yet, but the
          --  subprogram will be frozen at the point the wrapper package is
@@ -4630,8 +4911,108 @@ package body Sem_Ch12 is
          end if;
       end Analyze_Instance_And_Renamings;
 
+      -------------------------------
+      -- Build_Subprogram_Renaming --
+      -------------------------------
+
+      procedure Build_Subprogram_Renaming is
+         Renaming_Decl : Node_Id;
+         Unit_Renaming : Node_Id;
+
+      begin
+         Unit_Renaming :=
+           Make_Subprogram_Renaming_Declaration (Loc,
+             Specification =>
+               Copy_Generic_Node
+                 (Specification (Original_Node (Gen_Decl)),
+                  Empty,
+                  Instantiating => True),
+             Name          => New_Occurrence_Of (Anon_Id, Loc));
+
+         --  The generic may be a a child unit. The renaming needs an
+         --  identifier with the proper name.
+
+         Set_Defining_Unit_Name (Specification (Unit_Renaming),
+            Make_Defining_Identifier (Loc, Chars (Gen_Unit)));
+
+         --  If there is a formal subprogram with the same name as the unit
+         --  itself, do not add this renaming declaration, to prevent
+         --  ambiguities when there is a call with that name in the body.
+         --  This is a partial and ugly fix for one ACATS test. ???
+
+         Renaming_Decl := First (Renaming_List);
+         while Present (Renaming_Decl) loop
+            if Nkind (Renaming_Decl) = N_Subprogram_Renaming_Declaration
+              and then
+                Chars (Defining_Entity (Renaming_Decl)) = Chars (Gen_Unit)
+            then
+               exit;
+            end if;
+
+            Next (Renaming_Decl);
+         end loop;
+
+         if No (Renaming_Decl) then
+            Append  (Unit_Renaming, Renaming_List);
+         end if;
+      end Build_Subprogram_Renaming;
+
+      -------------------------------------
+      -- Instantiate_Subprogram_Contract --
+      -------------------------------------
+
+      procedure Instantiate_Subprogram_Contract (Templ : Node_Id) is
+         procedure Instantiate_Pragmas (First_Prag : Node_Id);
+         --  Instantiate all contract-related source pragmas found in the list
+         --  starting with pragma First_Prag. Each instantiated pragma is added
+         --  to list Renaming_List.
+
+         -------------------------
+         -- Instantiate_Pragmas --
+         -------------------------
+
+         procedure Instantiate_Pragmas (First_Prag : Node_Id) is
+            Inst_Prag : Node_Id;
+            Prag      : Node_Id;
+
+         begin
+            Prag := First_Prag;
+            while Present (Prag) loop
+               if Is_Generic_Contract_Pragma (Prag) then
+                  Inst_Prag :=
+                    Copy_Generic_Node (Prag, Empty, Instantiating => True);
+
+                  Set_Analyzed (Inst_Prag, False);
+                  Append_To (Renaming_List, Inst_Prag);
+               end if;
+
+               Prag := Next_Pragma (Prag);
+            end loop;
+         end Instantiate_Pragmas;
+
+         --  Local variables
+
+         Items : constant Node_Id := Contract (Defining_Entity (Templ));
+
+      --  Start of processing for Instantiate_Subprogram_Contract
+
+      begin
+         if Present (Items) then
+            Instantiate_Pragmas (Pre_Post_Conditions (Items));
+            Instantiate_Pragmas (Contract_Test_Cases (Items));
+            Instantiate_Pragmas (Classifications     (Items));
+         end if;
+      end Instantiate_Subprogram_Contract;
+
       --  Local variables
 
+      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
+      Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the SPARK_Mode-related data for restore on exit
+
       Vis_Prims_List : Elist_Id := No_Elist;
       --  List of primitives made temporarily visible in the instantiation
       --  to match the visibility of the formal type
@@ -4639,14 +5020,14 @@ package body Sem_Ch12 is
    --  Start of processing for Analyze_Subprogram_Instantiation
 
    begin
-      Check_SPARK_Restriction ("generic is not allowed", N);
+      Check_SPARK_05_Restriction ("generic is not allowed", N);
 
-      --  Very first thing: apply the special kludge for Text_IO processing
-      --  in case we are instantiating one of the children of [Wide_]Text_IO.
-      --  Of course such an instantiation is bogus (these are packages, not
-      --  subprograms), but we get a better error message if we do this.
+      --  Very first thing: check for special Text_IO unit in case we are
+      --  instantiating one of the children of [[Wide_]Wide_]Text_IO. Of course
+      --  such an instantiation is bogus (these are packages, not subprograms),
+      --  but we get a better error message if we do this.
 
-      Text_IO_Kludge (Gen_Id);
+      Check_Text_IO_Special_Unit (Gen_Id);
 
       --  Make node global for error reporting
 
@@ -4696,6 +5077,14 @@ package body Sem_Ch12 is
          Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
 
       else
+         --  If the context of the instance is subject to SPARK_Mode "off",
+         --  set the global flag which signals Analyze_Pragma to ignore all
+         --  SPARK_Mode pragmas within the instance.
+
+         if SPARK_Mode = Off then
+            Ignore_Pragma_SPARK_Mode := True;
+         end if;
+
          Set_Entity (Gen_Id, Gen_Unit);
          Set_Is_Instantiated (Gen_Unit);
 
@@ -4706,9 +5095,8 @@ package body Sem_Ch12 is
          --  If renaming, get original unit
 
          if Present (Renamed_Object (Gen_Unit))
-           and then (Ekind (Renamed_Object (Gen_Unit)) = E_Generic_Procedure
-                       or else
-                     Ekind (Renamed_Object (Gen_Unit)) = E_Generic_Function)
+           and then Ekind_In (Renamed_Object (Gen_Unit), E_Generic_Procedure,
+                                                         E_Generic_Function)
          then
             Gen_Unit := Renamed_Object (Gen_Unit);
             Set_Is_Instantiated (Gen_Unit);
@@ -4781,7 +5169,15 @@ package body Sem_Ch12 is
          end if;
 
          Append (Act_Decl, Renaming_List);
-         Analyze_Instance_And_Renamings;
+
+         --  Contract-related source pragmas that follow a generic subprogram
+         --  must be instantiated explicitly because they are not part of the
+         --  subprogram template.
+
+         Instantiate_Subprogram_Contract (Original_Node (Gen_Decl));
+         Build_Subprogram_Renaming;
+
+         Analyze_Instance_And_Renamings;
 
          --  If the generic is marked Import (Intrinsic), then so is the
          --  instance. This indicates that there is no body to instantiate. If
@@ -4811,9 +5207,6 @@ package body Sem_Ch12 is
          end if;
 
          Generate_Definition (Act_Decl_Id);
-         --  Set_Contract (Anon_Id, Make_Contract (Sloc (Anon_Id)));
-         --  ??? needed?
-         Set_Contract (Act_Decl_Id, Make_Contract (Sloc (Act_Decl_Id)));
 
          --  Inherit all inlining-related flags which apply to the generic in
          --  the subprogram and its declaration.
@@ -4846,11 +5239,11 @@ package body Sem_Ch12 is
                     and then Is_Controlling_Formal (Formal)
                     and then not Can_Never_Be_Null (Formal)
                   then
-                     Error_Msg_NE ("access parameter& is controlling,",
-                       N, Formal);
                      Error_Msg_NE
-                       ("\corresponding parameter of & must be"
-                       & " explicitly null-excluding", N, Gen_Id);
+                       ("access parameter& is controlling,", N, Formal);
+                     Error_Msg_NE
+                       ("\corresponding parameter of & must be "
+                       & "explicitly null-excluding", N, Gen_Id);
                   end if;
 
                   Next_Formal (Formal);
@@ -4906,6 +5299,15 @@ package body Sem_Ch12 is
          Env_Installed := False;
          Generic_Renamings.Set_Last (0);
          Generic_Renamings_HTable.Reset;
+
+         Ignore_Pragma_SPARK_Mode := Save_IPSM;
+         SPARK_Mode               := Save_SM;
+         SPARK_Mode_Pragma        := Save_SMP;
+
+         if SPARK_Mode = On then
+            Dynamic_Elaboration_Checks := False;
+         end if;
+
       end if;
 
    <<Leave>>
@@ -4922,6 +5324,14 @@ package body Sem_Ch12 is
          if Env_Installed then
             Restore_Env;
          end if;
+
+         Ignore_Pragma_SPARK_Mode := Save_IPSM;
+         SPARK_Mode               := Save_SM;
+         SPARK_Mode_Pragma        := Save_SMP;
+
+         if SPARK_Mode = On then
+            Dynamic_Elaboration_Checks := False;
+         end if;
    end Analyze_Subprogram_Instantiation;
 
    -------------------------
@@ -4981,6 +5391,211 @@ package body Sem_Ch12 is
       end if;
    end Get_Associated_Node;
 
+   ----------------------------
+   -- Build_Function_Wrapper --
+   ----------------------------
+
+   function Build_Function_Wrapper
+     (Formal_Subp : Entity_Id;
+      Actual_Subp : Entity_Id) return Node_Id
+   is
+      Loc       : constant Source_Ptr := Sloc (Current_Scope);
+      Ret_Type  : constant Entity_Id  := Get_Instance_Of (Etype (Formal_Subp));
+      Actuals   : List_Id;
+      Decl      : Node_Id;
+      Func_Name : Node_Id;
+      Func      : Entity_Id;
+      Parm_Type : Node_Id;
+      Profile   : List_Id := New_List;
+      Spec      : Node_Id;
+      Act_F     : Entity_Id;
+      Form_F    : Entity_Id;
+      New_F     : Entity_Id;
+
+   begin
+      Func_Name := New_Occurrence_Of (Actual_Subp, Loc);
+
+      Func := Make_Defining_Identifier (Loc, Chars (Formal_Subp));
+      Set_Ekind (Func, E_Function);
+      Set_Is_Generic_Actual_Subprogram (Func);
+
+      Actuals := New_List;
+      Profile := New_List;
+
+      Act_F  := First_Formal (Actual_Subp);
+      Form_F := First_Formal (Formal_Subp);
+      while Present (Form_F) loop
+
+         --  Create new formal for profile of wrapper, and add a reference
+         --  to it in the list of actuals for the enclosing call. The name
+         --  must be that of the formal in the formal subprogram, because
+         --  calls to it in the generic body may use named associations.
+
+         New_F := Make_Defining_Identifier (Loc, Chars (Form_F));
+
+         Parm_Type :=
+           New_Occurrence_Of (Get_Instance_Of (Etype (Form_F)), Loc);
+
+         Append_To (Profile,
+           Make_Parameter_Specification (Loc,
+             Defining_Identifier => New_F,
+             Parameter_Type      => Parm_Type));
+
+         Append_To (Actuals, New_Occurrence_Of (New_F, Loc));
+         Next_Formal (Form_F);
+
+         if Present (Act_F) then
+            Next_Formal (Act_F);
+         end if;
+      end loop;
+
+      Spec :=
+        Make_Function_Specification (Loc,
+          Defining_Unit_Name       => Func,
+          Parameter_Specifications => Profile,
+          Result_Definition        => New_Occurrence_Of (Ret_Type, Loc));
+
+      Decl :=
+        Make_Expression_Function (Loc,
+          Specification => Spec,
+          Expression    =>
+            Make_Function_Call (Loc,
+              Name                   => Func_Name,
+              Parameter_Associations => Actuals));
+
+      return Decl;
+   end Build_Function_Wrapper;
+
+   ----------------------------
+   -- Build_Operator_Wrapper --
+   ----------------------------
+
+   function Build_Operator_Wrapper
+     (Formal_Subp : Entity_Id;
+      Actual_Subp : Entity_Id) return Node_Id
+   is
+      Loc       : constant Source_Ptr := Sloc (Current_Scope);
+      Ret_Type  : constant Entity_Id  :=
+                    Get_Instance_Of (Etype (Formal_Subp));
+      Op_Type   : constant Entity_Id  :=
+                    Get_Instance_Of (Etype (First_Formal (Formal_Subp)));
+      Is_Binary : constant Boolean    :=
+                    Present (Next_Formal (First_Formal (Formal_Subp)));
+
+      Decl    : Node_Id;
+      Expr    : Node_Id;
+      F1, F2  : Entity_Id;
+      Func    : Entity_Id;
+      Op_Name : Name_Id;
+      Spec    : Node_Id;
+      L, R    : Node_Id;
+
+   begin
+      Op_Name := Chars (Actual_Subp);
+
+      --  Create entities for wrapper function and its formals
+
+      F1 := Make_Temporary (Loc, 'A');
+      F2 := Make_Temporary (Loc, 'B');
+      L  := New_Occurrence_Of (F1, Loc);
+      R  := New_Occurrence_Of (F2, Loc);
+
+      Func := Make_Defining_Identifier (Loc, Chars (Formal_Subp));
+      Set_Ekind (Func, E_Function);
+      Set_Is_Generic_Actual_Subprogram (Func);
+
+      Spec :=
+        Make_Function_Specification (Loc,
+          Defining_Unit_Name       => Func,
+          Parameter_Specifications => New_List (
+            Make_Parameter_Specification (Loc,
+               Defining_Identifier => F1,
+               Parameter_Type      => New_Occurrence_Of (Op_Type, Loc))),
+          Result_Definition        =>  New_Occurrence_Of (Ret_Type, Loc));
+
+      if Is_Binary then
+         Append_To (Parameter_Specifications (Spec),
+            Make_Parameter_Specification (Loc,
+              Defining_Identifier => F2,
+              Parameter_Type      => New_Occurrence_Of (Op_Type, Loc)));
+      end if;
+
+      --  Build expression as a function call, or as an operator node
+      --  that corresponds to the name of the actual, starting with
+      --  binary operators.
+
+      if Op_Name not in Any_Operator_Name then
+         Expr :=
+           Make_Function_Call (Loc,
+             Name                   =>
+               New_Occurrence_Of (Actual_Subp, Loc),
+             Parameter_Associations => New_List (L));
+
+         if Is_Binary then
+            Append_To (Parameter_Associations (Expr), R);
+         end if;
+
+      --  Binary operators
+
+      elsif Is_Binary then
+         if Op_Name = Name_Op_And then
+            Expr := Make_Op_And      (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Or then
+            Expr := Make_Op_Or       (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Xor then
+            Expr := Make_Op_Xor      (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Eq then
+            Expr := Make_Op_Eq       (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Ne then
+            Expr := Make_Op_Ne       (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Le then
+            Expr := Make_Op_Le       (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Gt then
+            Expr := Make_Op_Gt       (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Ge then
+            Expr := Make_Op_Ge       (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Lt then
+            Expr := Make_Op_Lt       (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Add then
+            Expr := Make_Op_Add      (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Subtract then
+            Expr := Make_Op_Subtract (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Concat then
+            Expr := Make_Op_Concat   (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Multiply then
+            Expr := Make_Op_Multiply (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Divide then
+            Expr := Make_Op_Divide   (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Mod then
+            Expr := Make_Op_Mod      (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Rem then
+            Expr := Make_Op_Rem      (Loc, Left_Opnd => L, Right_Opnd => R);
+         elsif Op_Name = Name_Op_Expon then
+            Expr := Make_Op_Expon    (Loc, Left_Opnd => L, Right_Opnd => R);
+         end if;
+
+      --  Unary operators
+
+      else
+         if Op_Name = Name_Op_Add then
+            Expr := Make_Op_Plus  (Loc, Right_Opnd => L);
+         elsif Op_Name = Name_Op_Subtract then
+            Expr := Make_Op_Minus (Loc, Right_Opnd => L);
+         elsif Op_Name = Name_Op_Abs then
+            Expr := Make_Op_Abs   (Loc, Right_Opnd => L);
+         elsif Op_Name = Name_Op_Not then
+            Expr := Make_Op_Not   (Loc, Right_Opnd => L);
+         end if;
+      end if;
+
+      Decl :=
+        Make_Expression_Function (Loc,
+          Specification => Spec,
+          Expression    => Expr);
+
+      return Decl;
+   end Build_Operator_Wrapper;
+
    -------------------------------------------
    -- Build_Instance_Compilation_Unit_Nodes --
    -------------------------------------------
@@ -5005,7 +5620,7 @@ package body Sem_Ch12 is
           Unit           => Act_Decl,
           Aux_Decls_Node => Make_Compilation_Unit_Aux (Sloc (N)));
 
-      Set_Parent_Spec   (Act_Decl, Parent_Spec (N));
+      Set_Parent_Spec (Act_Decl, Parent_Spec (N));
 
       --  The new compilation unit is linked to its body, but both share the
       --  same file, so we do not set Body_Required on the new unit so as not
@@ -5016,6 +5631,15 @@ package body Sem_Ch12 is
       --  compilation unit of the instance, since this is the main unit.
 
       Rewrite (N, Act_Body);
+
+      --  Propagate the aspect specifications from the package body template to
+      --  the instantiated version of the package body.
+
+      if Has_Aspects (Act_Body) then
+         Set_Aspect_Specifications
+           (N, New_Copy_List_Tree (Aspect_Specifications (Act_Body)));
+      end if;
+
       Body_Cunit := Parent (N);
 
       --  The two compilation unit nodes are linked by the Library_Unit field
@@ -5134,6 +5758,12 @@ package body Sem_Ch12 is
          then
             null;
 
+         --  Ada 2012: If both formal and actual are incomplete types they
+         --  are conformant.
+
+         elsif Is_Incomplete_Type (E1) and then Is_Incomplete_Type (E2) then
+            null;
+
          elsif B then
             Error_Msg_NE
               ("actual for & in actual instance does not match formal",
@@ -5170,7 +5800,8 @@ package body Sem_Ch12 is
             --  original name.
 
             elsif Is_Entity_Name (Original_Node (Constant_Value (Ent))) then
-                  Ent := Entity (Original_Node (Constant_Value (Ent)));
+               Ent := Entity (Original_Node (Constant_Value (Ent)));
+
             else
                return False;
             end if;
@@ -5218,9 +5849,7 @@ package body Sem_Ch12 is
    --  Start of processing for Check_Formal_Package_Instance
 
    begin
-      while Present (E1)
-        and then Present (E2)
-      loop
+      while Present (E1) and then Present (E2) loop
          exit when Ekind (E1) = E_Package
            and then Renamed_Entity (E1) = Renamed_Entity (Actual_Pack);
 
@@ -5241,9 +5870,7 @@ package body Sem_Ch12 is
            and then not Comes_From_Source (E1)
            and then Chars (E1) /= Chars (E2)
          then
-            while Present (E1)
-              and then  Chars (E1) /= Chars (E2)
-            loop
+            while Present (E1) and then  Chars (E1) /= Chars (E2) loop
                Next_Entity (E1);
             end loop;
          end if;
@@ -5275,9 +5902,7 @@ package body Sem_Ch12 is
             --  If E2 is a formal type declaration, it is a defaulted parameter
             --  and needs no checking.
 
-            if not Is_Itype (E1)
-              and then not Is_Itype (E2)
-            then
+            if not Is_Itype (E1) and then not Is_Itype (E2) then
                Check_Mismatch
                  (not Is_Type (E2)
                    or else Etype (E1) /= Etype (E2)
@@ -5298,9 +5923,8 @@ package body Sem_Ch12 is
                Expr2 := Expression (Parent (E2));
             end if;
 
-            if Is_Static_Expression (Expr1) then
-
-               if not Is_Static_Expression (Expr2) then
+            if Is_OK_Static_Expression (Expr1) then
+               if not Is_OK_Static_Expression (Expr2) then
                   Check_Mismatch (True);
 
                elsif Is_Discrete_Type (Etype (E1)) then
@@ -5339,15 +5963,15 @@ package body Sem_Ch12 is
                        (not Same_Instantiated_Constant
                          (Entity (Expr1), Entity (Expr2)));
                   end if;
+
                else
                   Check_Mismatch (True);
                end if;
 
             elsif Is_Entity_Name (Original_Node (Expr1))
               and then Is_Entity_Name (Expr2)
-            and then
-              Same_Instantiated_Constant
-                (Entity (Original_Node (Expr1)), Entity (Expr2))
+              and then Same_Instantiated_Constant
+                         (Entity (Original_Node (Expr1)), Entity (Expr2))
             then
                null;
 
@@ -5646,9 +6270,7 @@ package body Sem_Ch12 is
          --  If the formal package is declared with a box, or if the formal
          --  parameter is defaulted, it is visible in the body.
 
-         elsif Is_Formal_Box
-           or else Is_Visible_Formal (E)
-         then
+         elsif Is_Formal_Box or else Is_Visible_Formal (E) then
             Set_Is_Hidden (E, False);
          end if;
 
@@ -5673,10 +6295,10 @@ package body Sem_Ch12 is
             begin
                if Is_Wrapper_Package (Instance) then
                   Gen_Id :=
-                     Generic_Parent
-                       (Specification
-                         (Unit_Declaration_Node
-                           (Related_Instance (Instance))));
+                    Generic_Parent
+                      (Specification
+                        (Unit_Declaration_Node
+                          (Related_Instance (Instance))));
                else
                   Gen_Id :=
                     Generic_Parent (Package_Specification (Instance));
@@ -5932,7 +6554,7 @@ package body Sem_Ch12 is
                if Is_Child_Unit (E)
                  and then not Comes_From_Source (Entity (Prefix (Gen_Id)))
                  and then (not In_Instance
-                             or else Nkind (Parent (Parent (Gen_Id))) =
+                            or else Nkind (Parent (Parent (Gen_Id))) =
                                                          N_Compilation_Unit)
                then
                   Error_Msg_N
@@ -6056,8 +6678,7 @@ package body Sem_Ch12 is
               and then Is_Generic_Unit (Scope (Renamed_Object (E)))
               and then Nkind (Name (Parent (E))) = N_Expanded_Name
             then
-               Rewrite (Gen_Id,
-                 New_Copy_Tree (Name (Parent (E))));
+               Rewrite (Gen_Id, New_Copy_Tree (Name (Parent (E))));
                Inst_Par := Entity (Prefix (Gen_Id));
 
                if not In_Open_Scopes (Inst_Par) then
@@ -6105,7 +6726,7 @@ package body Sem_Ch12 is
          Error_Msg_Node_2 := Scope (Act_Decl_Id);
          Error_Msg_NE
            ("generic unit & is implicitly declared in &",
-             Defining_Unit_Name (N), Gen_Unit);
+            Defining_Unit_Name (N), Gen_Unit);
          Error_Msg_N ("\instance must have different name",
            Defining_Unit_Name (N));
       end if;
@@ -6263,9 +6884,8 @@ package body Sem_Ch12 is
          if Nkind (Actual) = N_Subtype_Declaration then
             Gen_T := Generic_Parent_Type (Actual);
 
-            if Present (Gen_T)
-              and then Is_Tagged_Type (Gen_T)
-            then
+            if Present (Gen_T) and then Is_Tagged_Type (Gen_T) then
+
                --  Traverse the list of primitives of the actual types
                --  searching for hidden primitives that are visible in the
                --  corresponding generic formal; leave them visible and
@@ -6314,7 +6934,7 @@ package body Sem_Ch12 is
 
          if Ekind (Scop) = E_Generic_Package
            or else (Is_Subprogram (Scop)
-                      and then Nkind (Unit_Declaration_Node (Scop)) =
+                     and then Nkind (Unit_Declaration_Node (Scop)) =
                                         N_Generic_Subprogram_Declaration)
          then
             Elmt := First_Elmt (Inner_Instances (Inner));
@@ -6324,7 +6944,7 @@ package body Sem_Ch12 is
                   Error_Msg_Node_2 := Inner;
                   Error_Msg_NE
                     ("circular Instantiation: & instantiated within &!",
-                       N, Scop);
+                     N, Scop);
                   return True;
 
                elsif Node (Elmt) = Inner then
@@ -6334,7 +6954,7 @@ package body Sem_Ch12 is
                   Error_Msg_Node_2 := Inner;
                   Error_Msg_NE
                     ("circular Instantiation: & instantiated within &!",
-                      N, Node (Elmt));
+                     N, Node (Elmt));
                   return True;
                end if;
 
@@ -6396,7 +7016,6 @@ package body Sem_Ch12 is
       ----------------------
 
       procedure Copy_Descendants is
-
          use Atree.Unchecked_Access;
          --  This code section is part of the implementation of an untyped
          --  tree traversal, so it needs direct access to node fields.
@@ -6495,11 +7114,12 @@ package body Sem_Ch12 is
 
       function In_Defining_Unit_Name (Nam : Node_Id) return Boolean is
       begin
-         return Present (Parent (Nam))
-           and then (Nkind (Parent (Nam)) = N_Defining_Program_Unit_Name
-                      or else
-                        (Nkind (Parent (Nam)) = N_Expanded_Name
-                          and then In_Defining_Unit_Name (Parent (Nam))));
+         return
+           Present (Parent (Nam))
+             and then (Nkind (Parent (Nam)) = N_Defining_Program_Unit_Name
+                        or else
+                          (Nkind (Parent (Nam)) = N_Expanded_Name
+                            and then In_Defining_Unit_Name (Parent (Nam))));
       end In_Defining_Unit_Name;
 
    --  Start of processing for Copy_Generic_Node
@@ -6527,17 +7147,12 @@ package body Sem_Ch12 is
          Set_Parent (New_N, Parent_Id);
       end if;
 
-      --  If defining identifier, then all fields have been copied already
-
-      if Nkind (New_N) in N_Entity then
-         null;
-
       --  Special casing for identifiers and other entity names and operators
 
-      elsif Nkind_In (New_N, N_Identifier,
-                             N_Character_Literal,
-                             N_Expanded_Name,
-                             N_Operator_Symbol)
+      if Nkind_In (New_N, N_Character_Literal,
+                          N_Expanded_Name,
+                          N_Identifier,
+                          N_Operator_Symbol)
         or else Nkind (New_N) in N_Op
       then
          if not Instantiating then
@@ -6668,6 +7283,19 @@ package body Sem_Ch12 is
             end if;
          end if;
 
+      --  Establish a link between an entity from the generic template and the
+      --  corresponding entity in the generic copy to be analyzed.
+
+      elsif Nkind (N) in N_Entity then
+         if not Instantiating then
+            Set_Associated_Entity (N, New_N);
+         end if;
+
+         --  Clear any existing link the copy may inherit from the replicated
+         --  generic template entity.
+
+         Set_Associated_Entity (New_N, Empty);
+
       --  Special casing for stubs
 
       elsif Nkind (N) in N_Body_Stub then
@@ -6842,9 +7470,7 @@ package body Sem_Ch12 is
                   Rt  : Entity_Id;
 
                begin
-                  if Present (T)
-                    and then Is_Private_Type (T)
-                  then
+                  if Present (T) and then Is_Private_Type (T) then
                      Switch_View (T);
                   end if;
 
@@ -6903,9 +7529,8 @@ package body Sem_Ch12 is
                --  Retrieve the allocator node in the generic copy
 
                Acc_T := Etype (Parent (Parent (T)));
-               if Present (Acc_T)
-                 and then Is_Private_Type (Acc_T)
-               then
+
+               if Present (Acc_T) and then Is_Private_Type (Acc_T) then
                   Switch_View (Acc_T);
                end if;
             end if;
@@ -6943,19 +7568,24 @@ package body Sem_Ch12 is
             S_Adjustment := Save_Adjustment;
          end;
 
-      --  Don't copy Ident or Comment pragmas, since the comment belongs to the
-      --  generic unit, not to the instantiating unit.
-
       elsif Nkind (N) = N_Pragma and then Instantiating then
-         declare
-            Prag_Id : constant Pragma_Id := Get_Pragma_Id (N);
-         begin
-            if Prag_Id = Pragma_Ident or else Prag_Id = Pragma_Comment then
-               New_N := Make_Null_Statement (Sloc (N));
-            else
-               Copy_Descendants;
-            end if;
-         end;
+
+         --  Do not copy Comment or Ident pragmas their content is relevant to
+         --  the generic unit, not to the instantiating unit.
+
+         if Nam_In (Pragma_Name (N), Name_Comment, Name_Ident) then
+            New_N := Make_Null_Statement (Sloc (N));
+
+         --  Do not copy pragmas generated from aspects because the pragmas do
+         --  not carry any semantic information, plus they will be regenerated
+         --  in the instance.
+
+         elsif From_Aspect_Specification (N) then
+            New_N := Make_Null_Statement (Sloc (N));
+
+         else
+            Copy_Descendants;
+         end if;
 
       elsif Nkind_In (N, N_Integer_Literal, N_Real_Literal) then
 
@@ -6968,9 +7598,8 @@ package body Sem_Ch12 is
         and then Instantiating
       then
          --  If the string is declared in an outer scope, the string_literal
-         --  subtype created for it may have the wrong scope. We force the
-         --  reanalysis of the constant to generate a new itype in the proper
-         --  context.
+         --  subtype created for it may have the wrong scope. Force reanalysis
+         --  of the constant to generate a new itype in the proper context.
 
          Set_Etype (New_N, Empty);
          Set_Analyzed (New_N, False);
@@ -7333,7 +7962,6 @@ package body Sem_Ch12 is
          while Present (T) loop
             if In_Open_Scopes (Scope (T)) then
                return T;
-
             elsif Is_Generic_Actual_Type (T) then
                return T;
             end if;
@@ -7504,7 +8132,8 @@ package body Sem_Ch12 is
         and then Earlier (Inst_Node, Gen_Body)
       then
          if Nkind (Enc_G) = N_Package_Body then
-            E_G_Id := Corresponding_Spec (Enc_G);
+            E_G_Id :=
+              Corresponding_Spec (Enc_G);
          else pragma Assert (Nkind (Enc_G) = N_Package_Body_Stub);
             E_G_Id :=
               Corresponding_Spec (Proper_Body (Unit (Library_Unit (Enc_G))));
@@ -7572,6 +8201,7 @@ package body Sem_Ch12 is
    begin
       if Res /= Assoc_Null then
          return Generic_Renamings.Table (Res).Act_Id;
+
       else
          --  On exit, entity is not instantiated: not a generic parameter, or
          --  else parameter of an inner generic unit.
@@ -7757,9 +8387,10 @@ package body Sem_Ch12 is
       Inst   : Node_Id) return Boolean
    is
       Decls : constant Node_Id := Parent (F_Node);
-      Nod   : Node_Id := Parent (Inst);
+      Nod   : Node_Id;
 
    begin
+      Nod := Parent (Inst);
       while Present (Nod) loop
          if Nod = Decls then
             return True;
@@ -7973,9 +8604,7 @@ package body Sem_Ch12 is
 
       begin
          S := Scope (Gen);
-         while Present (S)
-           and then S /= Standard_Standard
-         loop
+         while Present (S) and then S /= Standard_Standard loop
             if Is_Generic_Instance (S)
               and then In_Same_Source_Unit (S, N)
             then
@@ -8033,9 +8662,7 @@ package body Sem_Ch12 is
                   --  In these three cases the freeze node of the previous
                   --  instance is not relevant.
 
-                  while Present (Scop)
-                    and then Scop /= Standard_Standard
-                  loop
+                  while Present (Scop) and then Scop /= Standard_Standard loop
                      exit when Scop = Par_I
                        or else
                          (Is_Generic_Instance (Scop)
@@ -8052,8 +8679,8 @@ package body Sem_Ch12 is
                   --  the current scope as well.
 
                   elsif Present (Next (N))
-                    and then Nkind_In (Next (N),
-                      N_Subprogram_Body, N_Package_Body)
+                    and then Nkind_In (Next (N), N_Subprogram_Body,
+                                                 N_Package_Body)
                     and then Comes_From_Source (Next (N))
                   then
                      null;
@@ -8066,7 +8693,7 @@ package body Sem_Ch12 is
                   --  Current instance is within an unrelated body
 
                   elsif Present (Enclosing_N)
-                     and then Enclosing_N /= Enclosing_Body (Par_I)
+                    and then Enclosing_N /= Enclosing_Body (Par_I)
                   then
                      null;
 
@@ -8148,8 +8775,8 @@ package body Sem_Ch12 is
 
       Must_Delay : Boolean;
 
-      function Enclosing_Subp (Id : Entity_Id) return Entity_Id;
-      --  Find subprogram (if any) that encloses instance and/or generic body
+      function In_Same_Enclosing_Subp return Boolean;
+      --  Check whether instance and generic body are within same subprogram.
 
       function True_Sloc (N : Node_Id) return Source_Ptr;
       --  If the instance is nested inside a generic unit, the Sloc of the
@@ -8159,23 +8786,39 @@ package body Sem_Ch12 is
       --  origin of a node by finding the maximum sloc of any ancestor node.
       --  Why is this not equivalent to Top_Level_Location ???
 
-      --------------------
-      -- Enclosing_Subp --
-      --------------------
+      ----------------------------
+      -- In_Same_Enclosing_Subp --
+      ----------------------------
 
-      function Enclosing_Subp (Id : Entity_Id) return Entity_Id is
+      function In_Same_Enclosing_Subp return Boolean is
          Scop : Entity_Id;
+         Subp : Entity_Id;
 
       begin
-         Scop := Scope (Id);
+         Scop := Scope (Act_Id);
          while Scop /= Standard_Standard
            and then not Is_Overloadable (Scop)
          loop
             Scop := Scope (Scop);
          end loop;
 
-         return Scop;
-      end Enclosing_Subp;
+         if Scop = Standard_Standard then
+            return False;
+         else
+            Subp := Scop;
+         end if;
+
+         Scop := Scope (Gen_Id);
+         while Scop /= Standard_Standard loop
+            if Scop = Subp then
+               return True;
+            else
+               Scop := Scope (Scop);
+            end if;
+         end loop;
+
+         return False;
+      end In_Same_Enclosing_Subp;
 
       ---------------
       -- True_Sloc --
@@ -8219,21 +8862,20 @@ package body Sem_Ch12 is
       --  the generic body appears textually later, and the generic body is
       --  also in the main unit.
 
-      --  If instance is nested within a subprogram, and the generic body is
-      --  not, the instance is delayed because the enclosing body is. If
-      --  instance and body are within the same scope, or the same sub-
-      --  program body, indicate explicitly that the instance is delayed.
+      --  If instance is nested within a subprogram, and the generic body
+      --  is not, the instance is delayed because the enclosing body is. If
+      --  instance and body are within the same scope, or the same subprogram
+      --  body, indicate explicitly that the instance is delayed.
 
       Must_Delay :=
         (Gen_Unit = Act_Unit
           and then (Nkind_In (Gen_Unit, N_Package_Declaration,
                                         N_Generic_Package_Declaration)
-                      or else (Gen_Unit = Body_Unit
-                                and then True_Sloc (N) < Sloc (Orig_Body)))
+                     or else (Gen_Unit = Body_Unit
+                               and then True_Sloc (N) < Sloc (Orig_Body)))
           and then Is_In_Main_Unit (Gen_Unit)
           and then (Scope (Act_Id) = Scope (Gen_Id)
-                      or else
-                    Enclosing_Subp (Act_Id) = Enclosing_Subp (Gen_Id)));
+                     or else In_Same_Enclosing_Subp));
 
       --  If this is an early instantiation, the freeze node is placed after
       --  the generic body. Otherwise, if the generic appears in an instance,
@@ -8271,14 +8913,14 @@ package body Sem_Ch12 is
                --    package Inst is new ...
 
                --  In this particular scenario, the freeze node for Inst must
-               --  be inserted in the same manner as that of Parent_Inst -
+               --  be inserted in the same manner as that of Parent_Inst,
                --  before the next source body or at the end of the declarative
                --  list (body not available). If body P did not exist and
                --  Parent_Inst was frozen after Inst, either by a body
-               --  following Inst or at the end of the declarative region, the
-               --  freeze node for Inst must be inserted after that of
-               --  Parent_Inst. This relation is established by comparing the
-               --  Slocs of Parent_Inst freeze node and Inst.
+               --  following Inst or at the end of the declarative region,
+               --  the freeze node for Inst must be inserted after that of
+               --  Parent_Inst. This relation is established by comparing
+               --  the Slocs of Parent_Inst freeze node and Inst.
 
                if List_Containing (Get_Package_Instantiation_Node (Par)) =
                   List_Containing (N)
@@ -8416,6 +9058,7 @@ package body Sem_Ch12 is
          end if;
 
          Next_Entity (E);
+
          if Present (Gen_E) then
             Next_Entity (Gen_E);
          end if;
@@ -8536,9 +9179,8 @@ package body Sem_Ch12 is
 
       First_Gen := Gen_Par;
 
-      while Present (Gen_Par)
-        and then Is_Child_Unit (Gen_Par)
-      loop
+      while Present (Gen_Par) and then Is_Child_Unit (Gen_Par) loop
+
          --  Load grandparent instance as well
 
          Inst_Node := Get_Package_Instantiation_Node (Inst_Par);
@@ -8672,12 +9314,7 @@ package body Sem_Ch12 is
            and then Remove_Suffix (Prim_A, 'P') = Chars (Prim_G)
          then
             Set_Chars (Prim_A, Chars (Prim_G));
-
-            if List = No_Elist then
-               List := New_Elmt_List;
-            end if;
-
-            Append_Elmt (Prim_A, List);
+            Append_New_Elmt (Prim_A, To => List);
          end if;
 
          Next_Elmt (Prim_A_Elmt);
@@ -9046,10 +9683,10 @@ package body Sem_Ch12 is
          Nod :=
            Make_Package_Renaming_Declaration (Loc,
              Defining_Unit_Name => New_Copy (Defining_Identifier (Formal)),
-             Name               => New_Reference_To (Actual_Pack, Loc));
+             Name               => New_Occurrence_Of (Actual_Pack, Loc));
 
-         Set_Associated_Formal_Package (Defining_Unit_Name (Nod),
-           Defining_Identifier (Formal));
+         Set_Associated_Formal_Package
+           (Defining_Unit_Name (Nod), Defining_Identifier (Formal));
          Decls := New_List (Nod);
 
          --  If the formal F has a box, then the generic declarations are
@@ -9066,11 +9703,11 @@ package body Sem_Ch12 is
          --  actual parameter associations for later formals that depend on
          --  actuals declared in the formal package.
 
-         --  In Ada 2005, partial parametrization requires that we make visible
-         --  the actuals corresponding to formals that were defaulted in the
-         --  formal package. There formals are identified because they remain
-         --  formal generics within the formal package, rather than being
-         --  renamings of the actuals supplied.
+         --  In Ada 2005, partial parameterization requires that we make
+         --  visible the actuals corresponding to formals that were defaulted
+         --  in the formal package. There formals are identified because they
+         --  remain formal generics within the formal package, rather than
+         --  being renamings of the actuals supplied.
 
          declare
             Gen_Decl : constant Node_Id :=
@@ -9101,8 +9738,7 @@ package body Sem_Ch12 is
 
                   if Present (Formal_Ent) then
                      Find_Matching_Actual (Formal_Node, Actual_Ent);
-                     Match_Formal_Entity
-                       (Formal_Node, Formal_Ent, Actual_Ent);
+                     Match_Formal_Entity (Formal_Node, Formal_Ent, Actual_Ent);
 
                      --  We iterate at the same time over the actuals of the
                      --  local package created for the formal, to determine
@@ -9188,12 +9824,11 @@ package body Sem_Ch12 is
 
                Append_To (Decls,
                  Make_Package_Instantiation (Sloc (Actual),
-                   Defining_Unit_Name => I_Pack,
-                   Name =>
+                   Defining_Unit_Name   => I_Pack,
+                   Name                 =>
                      New_Occurrence_Of
                        (Get_Instance_Of (Gen_Parent), Sloc (Actual)),
-                   Generic_Associations =>
-                     Generic_Associations (Formal)));
+                   Generic_Associations => Generic_Associations (Formal)));
             end;
          end if;
 
@@ -9210,14 +9845,10 @@ package body Sem_Ch12 is
       Actual          : Node_Id;
       Analyzed_Formal : Node_Id) return Node_Id
    is
-      Loc        : Source_Ptr;
-      Formal_Sub : constant Entity_Id :=
-                     Defining_Unit_Name (Specification (Formal));
       Analyzed_S : constant Entity_Id :=
                      Defining_Unit_Name (Specification (Analyzed_Formal));
-      Decl_Node  : Node_Id;
-      Nam        : Node_Id;
-      New_Spec   : Node_Id;
+      Formal_Sub : constant Entity_Id :=
+                     Defining_Unit_Name (Specification (Formal));
 
       function From_Parent_Scope (Subp : Entity_Id) return Boolean;
       --  If the generic is a child unit, the parent has been installed on the
@@ -9281,12 +9912,19 @@ package body Sem_Ch12 is
          end if;
 
          Error_Msg_NE
-           ("expect subprogram or entry name in instantiation of&",
+           ("expect subprogram or entry name in instantiation of &",
             Instantiation_Node, Formal_Sub);
          Abandon_Instantiation (Instantiation_Node);
-
       end Valid_Actual_Subprogram;
 
+      --  Local variables
+
+      Decl_Node  : Node_Id;
+      Loc        : Source_Ptr;
+      Nam        : Node_Id;
+      New_Spec   : Node_Id;
+      New_Subp   : Entity_Id;
+
    --  Start of processing for Instantiate_Formal_Subprogram
 
    begin
@@ -9298,23 +9936,29 @@ package body Sem_Ch12 is
 
       Loc := Sloc (Defining_Unit_Name (New_Spec));
 
-      --  Create new entity for the actual (New_Copy_Tree does not)
+      --  Create new entity for the actual (New_Copy_Tree does not), and
+      --  indicate that it is an actual.
 
-      Set_Defining_Unit_Name
-        (New_Spec, Make_Defining_Identifier (Loc, Chars (Formal_Sub)));
+      New_Subp := Make_Defining_Identifier (Loc, Chars (Formal_Sub));
+      Set_Ekind (New_Subp, Ekind (Analyzed_S));
+      Set_Is_Generic_Actual_Subprogram (New_Subp);
+      Set_Defining_Unit_Name (New_Spec, New_Subp);
 
-      --  Create new entities for the each of the formals in the
-      --  specification of the renaming declaration built for the actual.
+      --  Create new entities for the each of the formals in the specification
+      --  of the renaming declaration built for the actual.
 
       if Present (Parameter_Specifications (New_Spec)) then
          declare
-            F : Node_Id;
+            F    : Node_Id;
+            F_Id : Entity_Id;
+
          begin
             F := First (Parameter_Specifications (New_Spec));
             while Present (F) loop
+               F_Id := Defining_Identifier (F);
+
                Set_Defining_Identifier (F,
-                  Make_Defining_Identifier (Sloc (F),
-                    Chars => Chars (Defining_Identifier (F))));
+                  Make_Defining_Identifier (Sloc (F_Id), Chars (F_Id)));
                Next (F);
             end loop;
          end;
@@ -9363,9 +10007,10 @@ package body Sem_Ch12 is
          --  identifier or operator with the same name as the formal.
 
          if Nkind (Formal_Sub) = N_Defining_Operator_Symbol then
-            Nam := Make_Operator_Symbol (Loc,
-              Chars =>  Chars (Formal_Sub),
-              Strval => No_String);
+            Nam :=
+              Make_Operator_Symbol (Loc,
+                Chars  => Chars (Formal_Sub),
+                Strval => No_String);
          else
             Nam := Make_Identifier (Loc, Chars (Formal_Sub));
          end if;
@@ -9412,9 +10057,7 @@ package body Sem_Ch12 is
       --  instance. If overloaded, it will be resolved when analyzing the
       --  renaming declaration.
 
-      if Box_Present (Formal)
-        and then No (Actual)
-      then
+      if Box_Present (Formal) and then No (Actual) then
          Analyze (Nam);
 
          if Is_Child_Unit (Scope (Analyzed_S))
@@ -9521,7 +10164,46 @@ package body Sem_Ch12 is
       Subt_Decl   : Node_Id             := Empty;
       Subt_Mark   : Node_Id             := Empty;
 
+      function Copy_Access_Def return Node_Id;
+      --  If formal is an anonymous access, copy access definition of formal
+      --  for generated object declaration.
+
+      ---------------------
+      -- Copy_Access_Def --
+      ---------------------
+
+      function Copy_Access_Def return Node_Id is
+      begin
+         Def := New_Copy_Tree (Acc_Def);
+
+         --  In addition, if formal is an access to subprogram we need to
+         --  generate new formals for the signature of the default, so that
+         --  the tree is properly formatted for ASIS use.
+
+         if Present (Access_To_Subprogram_Definition (Acc_Def)) then
+            declare
+               Par_Spec : Node_Id;
+            begin
+               Par_Spec :=
+                 First (Parameter_Specifications
+                          (Access_To_Subprogram_Definition (Def)));
+               while Present (Par_Spec) loop
+                  Set_Defining_Identifier (Par_Spec,
+                    Make_Defining_Identifier (Sloc (Acc_Def),
+                      Chars => Chars (Defining_Identifier (Par_Spec))));
+                  Next (Par_Spec);
+               end loop;
+            end;
+         end if;
+
+         return Def;
+      end Copy_Access_Def;
+
+   --  Start of processing for Instantiate_Object
+
    begin
+      --  Formal may be an anonymous access
+
       if Present (Subtype_Mark (Formal)) then
          Subt_Mark := Subtype_Mark (Formal);
       else
@@ -9553,11 +10235,11 @@ package body Sem_Ch12 is
 
          if No (Actual) then
             Error_Msg_NE
-              ("missing actual&",
+              ("missing actual &",
                Instantiation_Node, Gen_Obj);
             Error_Msg_NE
               ("\in instantiation of & declared#",
-                 Instantiation_Node, Scope (A_Gen_Obj));
+               Instantiation_Node, Scope (A_Gen_Obj));
             Abandon_Instantiation (Instantiation_Node);
          end if;
 
@@ -9652,8 +10334,7 @@ package body Sem_Ch12 is
          Resolve (Actual, Ftyp);
 
          if not Denotes_Variable (Actual) then
-            Error_Msg_NE
-              ("actual for& must be a variable", Actual, Gen_Obj);
+            Error_Msg_NE ("actual for& must be a variable", Actual, Gen_Obj);
 
          elsif Base_Type (Ftyp) /= Base_Type (Etype (Actual)) then
 
@@ -9662,15 +10343,13 @@ package body Sem_Ch12 is
             --  access type.
 
             if Ada_Version < Ada_2005
-              or else
-                Ekind (Base_Type (Ftyp)) /=
-                  E_Anonymous_Access_Type
-              or else
-                Ekind (Base_Type (Etype (Actual))) /=
-                  E_Anonymous_Access_Type
+              or else Ekind (Base_Type (Ftyp))           /=
+                                                  E_Anonymous_Access_Type
+              or else Ekind (Base_Type (Etype (Actual))) /=
+                                                  E_Anonymous_Access_Type
             then
-               Error_Msg_NE ("type of actual does not match type of&",
-                             Actual, Gen_Obj);
+               Error_Msg_NE
+                 ("type of actual does not match type of&", Actual, Gen_Obj);
             end if;
          end if;
 
@@ -9679,19 +10358,16 @@ package body Sem_Ch12 is
          --  Check for instantiation of atomic/volatile actual for
          --  non-atomic/volatile formal (RM C.6 (12)).
 
-         if Is_Atomic_Object (Actual)
-           and then not Is_Atomic (Orig_Ftyp)
-         then
+         if Is_Atomic_Object (Actual) and then not Is_Atomic (Orig_Ftyp) then
             Error_Msg_N
-              ("cannot instantiate non-atomic formal object " &
-               "with atomic actual", Actual);
+              ("cannot instantiate non-atomic formal object "
+               "with atomic actual", Actual);
 
-         elsif Is_Volatile_Object (Actual)
-           and then not Is_Volatile (Orig_Ftyp)
+         elsif Is_Volatile_Object (Actual) and then not Is_Volatile (Orig_Ftyp)
          then
             Error_Msg_N
-              ("cannot instantiate non-volatile formal object " &
-               "with volatile actual", Actual);
+              ("cannot instantiate non-volatile formal object "
+               "with volatile actual", Actual);
          end if;
 
       --  Formal in-parameter
@@ -9699,12 +10375,15 @@ package body Sem_Ch12 is
       else
          --  The instantiation of a generic formal in-parameter is constant
          --  declaration. The actual is the expression for that declaration.
+         --  Its type is a full copy of the type of the formal. This may be
+         --  an access to subprogram, for which we need to generate entities
+         --  for the formals in the new signature.
 
          if Present (Actual) then
             if Present (Subt_Mark) then
-               Def := Subt_Mark;
+               Def := New_Copy_Tree (Subt_Mark);
             else pragma Assert (Present (Acc_Def));
-               Def := Acc_Def;
+               Def := Copy_Access_Def;
             end if;
 
             Decl_Node :=
@@ -9712,7 +10391,7 @@ package body Sem_Ch12 is
                 Defining_Identifier    => New_Copy (Gen_Obj),
                 Constant_Present       => True,
                 Null_Exclusion_Present => Null_Exclusion_Present (Formal),
-                Object_Definition      => New_Copy_Tree (Def),
+                Object_Definition      => Def,
                 Expression             => Actual);
 
             Set_Corresponding_Generic_Association (Decl_Node, Act_Assoc);
@@ -9746,7 +10425,20 @@ package body Sem_Ch12 is
             begin
                Typ := Get_Instance_Of (Formal_Type);
 
-               Freeze_Before (Instantiation_Node, Typ);
+               --  If the actual appears in the current or an enclosing scope,
+               --  use its type directly. This is relevant if it has an actual
+               --  subtype that is distinct from its nominal one. This cannot
+               --  be done in general because the type of the actual may
+               --  depend on other actuals, and only be fully determined when
+               --  the enclosing instance is analyzed.
+
+               if Present (Etype (Actual))
+                 and then Is_Constr_Subt_For_U_Nominal (Etype (Actual))
+               then
+                  Freeze_Before (Instantiation_Node, Etype (Actual));
+               else
+                  Freeze_Before (Instantiation_Node, Typ);
+               end if;
 
                --  If the actual is an aggregate, perform name resolution on
                --  its components (the analysis of an aggregate does not do it)
@@ -9771,9 +10463,9 @@ package body Sem_Ch12 is
             --  Use default to construct declaration
 
             if Present (Subt_Mark) then
-               Def := Subt_Mark;
+               Def := New_Copy (Subt_Mark);
             else pragma Assert (Present (Acc_Def));
-               Def := Acc_Def;
+               Def := Copy_Access_Def;
             end if;
 
             Decl_Node :=
@@ -9781,7 +10473,7 @@ package body Sem_Ch12 is
                 Defining_Identifier    => New_Copy (Gen_Obj),
                 Constant_Present       => True,
                 Null_Exclusion_Present => Null_Exclusion_Present (Formal),
-                Object_Definition      => New_Copy (Def),
+                Object_Definition      => Def,
                 Expression             => New_Copy_Tree
                                             (Default_Expression (Formal)));
 
@@ -9789,11 +10481,9 @@ package body Sem_Ch12 is
             Set_Analyzed (Expression (Decl_Node), False);
 
          else
-            Error_Msg_NE
-              ("missing actual&",
-                Instantiation_Node, Gen_Obj);
+            Error_Msg_NE ("missing actual&", Instantiation_Node, Gen_Obj);
             Error_Msg_NE ("\in instantiation of & declared#",
-              Instantiation_Node, Scope (A_Gen_Obj));
+                          Instantiation_Node, Scope (A_Gen_Obj));
 
             if Is_Scalar_Type (Etype (A_Gen_Obj)) then
 
@@ -9841,9 +10531,8 @@ package body Sem_Ch12 is
 
       if Ada_Version >= Ada_2005
         and then Present (Actual_Decl)
-        and then
-          Nkind_In (Actual_Decl, N_Formal_Object_Declaration,
-                                 N_Object_Declaration)
+        and then Nkind_In (Actual_Decl, N_Formal_Object_Declaration,
+                                        N_Object_Declaration)
         and then Nkind (Analyzed_Formal) = N_Formal_Object_Declaration
         and then not Has_Null_Exclusion (Actual_Decl)
         and then Has_Null_Exclusion (Analyzed_Formal)
@@ -9853,13 +10542,13 @@ package body Sem_Ch12 is
            ("actual must exclude null to match generic formal#", Actual);
       end if;
 
-      --  A volatile object cannot be used as an actual in a generic instance.
-      --  The following check is only relevant when SPARK_Mode is on as it is
-      --  not a standard Ada legality rule.
+      --  An effectively volatile object cannot be used as an actual in
+      --  a generic instance. The following check is only relevant when
+      --  SPARK_Mode is on as it is not a standard Ada legality rule.
 
       if SPARK_Mode = On
         and then Present (Actual)
-        and then Is_SPARK_Volatile_Object (Actual)
+        and then Is_Effectively_Volatile_Object (Actual)
       then
          Error_Msg_N
            ("volatile object cannot act as actual in generic instantiation "
@@ -9904,6 +10593,76 @@ package body Sem_Ch12 is
       --  List of primitives made temporarily visible in the instantiation
       --  to match the visibility of the formal type
 
+      procedure Check_Initialized_Types;
+      --  In a generic package body, an entity of a generic private type may
+      --  appear uninitialized. This is suspicious, unless the actual is a
+      --  fully initialized type.
+
+      -----------------------------
+      -- Check_Initialized_Types --
+      -----------------------------
+
+      procedure Check_Initialized_Types is
+         Decl       : Node_Id;
+         Formal     : Entity_Id;
+         Actual     : Entity_Id;
+         Uninit_Var : Entity_Id;
+
+      begin
+         Decl := First (Generic_Formal_Declarations (Gen_Decl));
+         while Present (Decl) loop
+            Uninit_Var := Empty;
+
+            if Nkind (Decl) = N_Private_Extension_Declaration then
+               Uninit_Var := Uninitialized_Variable (Decl);
+
+            elsif Nkind (Decl) = N_Formal_Type_Declaration
+                    and then Nkind (Formal_Type_Definition (Decl)) =
+                                          N_Formal_Private_Type_Definition
+            then
+               Uninit_Var :=
+                 Uninitialized_Variable (Formal_Type_Definition (Decl));
+            end if;
+
+            if Present (Uninit_Var) then
+               Formal := Defining_Identifier (Decl);
+               Actual := First_Entity (Act_Decl_Id);
+
+               --  For each formal there is a subtype declaration that renames
+               --  the actual and has the same name as the formal. Locate the
+               --  formal for warning message about uninitialized variables
+               --  in the generic, for which the actual type should be a fully
+               --  initialized type.
+
+               while Present (Actual) loop
+                  exit when Ekind (Actual) = E_Package
+                    and then Present (Renamed_Object (Actual));
+
+                  if Chars (Actual) = Chars (Formal)
+                    and then not Is_Scalar_Type (Actual)
+                    and then not Is_Fully_Initialized_Type (Actual)
+                    and then Warn_On_No_Value_Assigned
+                  then
+                     Error_Msg_Node_2 := Formal;
+                     Error_Msg_NE
+                       ("generic unit has uninitialized variable& of "
+                        & "formal private type &?v?", Actual, Uninit_Var);
+                     Error_Msg_NE
+                       ("actual type for& should be fully initialized type?v?",
+                        Actual, Formal);
+                     exit;
+                  end if;
+
+                  Next_Entity (Actual);
+               end loop;
+            end if;
+
+            Next (Decl);
+         end loop;
+      end Check_Initialized_Types;
+
+   --  Start of processing for Instantiate_Package_Body
+
    begin
       Gen_Body_Id := Corresponding_Body (Gen_Decl);
 
@@ -9930,9 +10689,21 @@ package body Sem_Ch12 is
       Opt.SPARK_Mode_Pragma    := Body_Info.SPARK_Mode_Pragma;
 
       if No (Gen_Body_Id) then
-         Load_Parent_Of_Generic
-           (Inst_Node, Specification (Gen_Decl), Body_Optional);
-         Gen_Body_Id := Corresponding_Body (Gen_Decl);
+
+         --  Do not look for parent of generic body if none is required.
+         --  This may happen when the routine is called as part of the
+         --  Pending_Instantiations processing, when nested instances
+         --  may precede the one generated from the main unit.
+
+         if not Unit_Requires_Body (Defining_Entity (Gen_Decl))
+           and then Body_Optional
+         then
+            return;
+         else
+            Load_Parent_Of_Generic
+              (Inst_Node, Specification (Gen_Decl), Body_Optional);
+            Gen_Body_Id := Corresponding_Body (Gen_Decl);
+         end if;
       end if;
 
       --  Establish global variable for sloc adjustment and for error recovery
@@ -9976,6 +10747,7 @@ package body Sem_Ch12 is
 
          Set_Corresponding_Spec (Act_Body, Act_Decl_Id);
          Check_Generic_Actuals (Act_Decl_Id, False);
+         Check_Initialized_Types;
 
          --  Install primitives hidden at the point of the instantiation but
          --  visible when processing the generic formals
@@ -10047,8 +10819,7 @@ package body Sem_Ch12 is
                if Nkind (Defining_Unit_Name (Act_Spec)) =
                                               N_Defining_Program_Unit_Name
                then
-                  Set_Scope
-                    (Defining_Entity (Inst_Node), Scope (Act_Decl_Id));
+                  Set_Scope (Defining_Entity (Inst_Node), Scope (Act_Decl_Id));
                end if;
             end if;
 
@@ -10067,8 +10838,7 @@ package body Sem_Ch12 is
             --  to be compiled with checks off.
 
             --  Note that we do NOT apply this criterion to children of GNAT
-            --  (or on VMS, children of DEC). The latter units must suppress
-            --  checks explicitly if this is needed.
+            --  The latter units must suppress checks explicitly if needed.
 
             if Is_Predefined_File_Name
                  (Unit_File_Name (Get_Source_Unit (Gen_Decl)))
@@ -10168,32 +10938,29 @@ package body Sem_Ch12 is
      (Body_Info     : Pending_Body_Info;
       Body_Optional : Boolean := False)
    is
-      Act_Decl      : constant Node_Id    := Body_Info.Act_Decl;
-      Inst_Node     : constant Node_Id    := Body_Info.Inst_Node;
-      Loc           : constant Source_Ptr := Sloc (Inst_Node);
-      Gen_Id        : constant Node_Id    := Name (Inst_Node);
-      Gen_Unit      : constant Entity_Id  := Get_Generic_Entity (Inst_Node);
-      Gen_Decl      : constant Node_Id    := Unit_Declaration_Node (Gen_Unit);
-      Anon_Id       : constant Entity_Id  :=
-                        Defining_Unit_Name (Specification (Act_Decl));
-      Pack_Id       : constant Entity_Id  :=
-                        Defining_Unit_Name (Parent (Act_Decl));
-      Decls         : List_Id;
-      Gen_Body      : Node_Id;
-      Gen_Body_Id   : Node_Id;
-      Act_Body      : Node_Id;
-      Pack_Body     : Node_Id;
-      Prev_Formal   : Entity_Id;
-      Ret_Expr      : Node_Id;
-      Unit_Renaming : Node_Id;
-
-      Parent_Installed : Boolean := False;
+      Act_Decl    : constant Node_Id    := Body_Info.Act_Decl;
+      Inst_Node   : constant Node_Id    := Body_Info.Inst_Node;
+      Loc         : constant Source_Ptr := Sloc (Inst_Node);
+      Gen_Id      : constant Node_Id    := Name (Inst_Node);
+      Gen_Unit    : constant Entity_Id  := Get_Generic_Entity (Inst_Node);
+      Gen_Decl    : constant Node_Id    := Unit_Declaration_Node (Gen_Unit);
+      Anon_Id     : constant Entity_Id  :=
+                      Defining_Unit_Name (Specification (Act_Decl));
+      Pack_Id     : constant Entity_Id  :=
+                      Defining_Unit_Name (Parent (Act_Decl));
 
       Saved_Style_Check : constant Boolean        := Style_Check;
       Saved_Warnings    : constant Warning_Record := Save_Warnings;
 
-      Par_Ent : Entity_Id := Empty;
-      Par_Vis : Boolean   := False;
+      Act_Body    : Node_Id;
+      Gen_Body    : Node_Id;
+      Gen_Body_Id : Node_Id;
+      Pack_Body   : Node_Id;
+      Par_Ent     : Entity_Id := Empty;
+      Par_Vis     : Boolean   := False;
+      Ret_Expr    : Node_Id;
+
+      Parent_Installed : Boolean := False;
 
    begin
       Gen_Body_Id := Corresponding_Body (Gen_Decl);
@@ -10315,47 +11082,14 @@ package body Sem_Ch12 is
             Parent_Installed := True;
          end if;
 
-         --  Inside its body, a reference to the generic unit is a reference
-         --  to the instance. The corresponding renaming is the first
-         --  declaration in the body.
-
-         Unit_Renaming :=
-           Make_Subprogram_Renaming_Declaration (Loc,
-             Specification =>
-               Copy_Generic_Node (
-                 Specification (Original_Node (Gen_Body)),
-                 Empty,
-                 Instantiating => True),
-             Name => New_Occurrence_Of (Anon_Id, Loc));
-
-         --  If there is a formal subprogram with the same name as the unit
-         --  itself, do not add this renaming declaration. This is a temporary
-         --  fix for one ACVC test. ???
-
-         Prev_Formal := First_Entity (Pack_Id);
-         while Present (Prev_Formal) loop
-            if Chars (Prev_Formal) = Chars (Gen_Unit)
-              and then Is_Overloadable (Prev_Formal)
-            then
-               exit;
-            end if;
-
-            Next_Entity (Prev_Formal);
-         end loop;
-
-         if Present (Prev_Formal) then
-            Decls :=  New_List (Act_Body);
-         else
-            Decls :=  New_List (Unit_Renaming, Act_Body);
-         end if;
-
-         --  The subprogram body is placed in the body of a dummy package body,
-         --  whose spec contains the subprogram declaration as well as the
-         --  renaming declarations for the generic parameters.
+         --  Subprogram body is placed in the body of wrapper package,
+         --  whose spec contains the subprogram declaration as well as
+         --  the renaming declarations for the generic parameters.
 
-         Pack_Body := Make_Package_Body (Loc,
-           Defining_Unit_Name => New_Copy (Pack_Id),
-           Declarations       => Decls);
+         Pack_Body :=
+           Make_Package_Body (Loc,
+             Defining_Unit_Name => New_Copy (Pack_Id),
+             Declarations       => New_List (Act_Body));
 
          Set_Corresponding_Spec (Pack_Body, Pack_Id);
 
@@ -10497,6 +11231,13 @@ package body Sem_Ch12 is
       Loc        : Source_Ptr;
       Subt       : Entity_Id;
 
+      procedure Diagnose_Predicated_Actual;
+      --  There are a number of constructs in which a discrete type with
+      --  predicates is illegal, e.g. as an index in an array type declaration.
+      --  If a generic type is used is such a construct in a generic package
+      --  declaration, it carries the flag No_Predicate_On_Actual. it is part
+      --  of the generic contract that the actual cannot have predicates.
+
       procedure Validate_Array_Type_Instance;
       procedure Validate_Access_Subprogram_Instance;
       procedure Validate_Access_Type_Instance;
@@ -10514,6 +11255,29 @@ package body Sem_Ch12 is
       --  Check that base types are the same and that the subtypes match
       --  statically. Used in several of the above.
 
+      ---------------------------------
+      --  Diagnose_Predicated_Actual --
+      ---------------------------------
+
+      procedure Diagnose_Predicated_Actual is
+      begin
+         if No_Predicate_On_Actual (A_Gen_T)
+           and then Has_Predicates (Act_T)
+         then
+            Error_Msg_NE
+              ("actual for& cannot be a type with predicate",
+               Instantiation_Node, A_Gen_T);
+
+         elsif No_Dynamic_Predicate_On_Actual (A_Gen_T)
+           and then Has_Predicates (Act_T)
+           and then not Has_Static_Predicate_Aspect (Act_T)
+         then
+            Error_Msg_NE
+              ("actual for& cannot be a type with a dynamic predicate",
+               Instantiation_Node, A_Gen_T);
+         end if;
+      end Diagnose_Predicated_Actual;
+
       --------------------
       -- Subtypes_Match --
       --------------------
@@ -10581,6 +11345,17 @@ package body Sem_Ch12 is
               ("expect protected access type for formal &",
                Actual, Gen_T);
          end if;
+
+         --  If the formal has a specified convention (which in most cases
+         --  will be StdCall) verify that the actual has the same convention.
+
+         if Has_Convention_Pragma (A_Gen_T)
+           and then Convention (A_Gen_T) /= Convention (Act_T)
+         then
+            Error_Msg_Name_1 := Get_Convention_Name (Convention (A_Gen_T));
+            Error_Msg_NE
+              ("actual for formal & must have convention %", Actual, Gen_T);
+         end if;
       end Validate_Access_Subprogram_Instance;
 
       -----------------------------------
@@ -10636,21 +11411,30 @@ package body Sem_Ch12 is
             Desig_Act := Available_View (Desig_Act);
          end if;
 
-         if not Subtypes_Match
-           (Desig_Type, Desig_Act) then
+         if not Subtypes_Match (Desig_Type, Desig_Act) then
             Error_Msg_NE
               ("designated type of actual does not match that of formal &",
-                 Actual, Gen_T);
+               Actual, Gen_T);
+
+            if not Predicates_Match (Desig_Type, Desig_Act) then
+               Error_Msg_N ("\predicates do not match", Actual);
+            end if;
+
             Abandon_Instantiation (Actual);
 
          elsif Is_Access_Type (Designated_Type (Act_T))
            and then Is_Constrained (Designated_Type (Designated_Type (Act_T)))
                       /=
-                  Is_Constrained (Designated_Type (Desig_Type))
+                    Is_Constrained (Designated_Type (Desig_Type))
          then
             Error_Msg_NE
               ("designated type of actual does not match that of formal &",
-                 Actual, Gen_T);
+               Actual, Gen_T);
+
+            if not Predicates_Match (Desig_Type, Desig_Act) then
+               Error_Msg_N ("\predicates do not match", Actual);
+            end if;
+
             Abandon_Instantiation (Actual);
          end if;
 
@@ -10767,9 +11551,10 @@ package body Sem_Ch12 is
 
          if Subtypes_Match
            (Component_Type (A_Gen_T), Component_Type (Act_T))
-             or else Subtypes_Match
-               (Find_Actual_Type (Component_Type (A_Gen_T), A_Gen_T),
-               Component_Type (Act_T))
+             or else
+               Subtypes_Match
+                 (Find_Actual_Type (Component_Type (A_Gen_T), A_Gen_T),
+                  Component_Type (Act_T))
          then
             null;
          else
@@ -10972,9 +11757,9 @@ package body Sem_Ch12 is
 
             elsif Nkind (Parent (Act_T)) = N_Full_Type_Declaration
               and then Nkind (Type_Definition (Parent (Act_T))) =
-                         N_Derived_Type_Definition
-              and then not Synchronized_Present (Type_Definition
-                             (Parent (Act_T)))
+                                                 N_Derived_Type_Definition
+              and then not Synchronized_Present
+                             (Type_Definition (Parent (Act_T)))
             then
                Error_Msg_N
                  ("actual of synchronized type must be synchronized", Actual);
@@ -11005,16 +11790,14 @@ package body Sem_Ch12 is
            and then not Unknown_Discriminants_Present (Formal)
            and then Is_Indefinite_Subtype (Act_T)
          then
-            Error_Msg_N
-              ("actual subtype must be constrained", Actual);
+            Error_Msg_N ("actual subtype must be constrained", Actual);
             Abandon_Instantiation (Actual);
          end if;
 
          if not Unknown_Discriminants_Present (Formal) then
             if Is_Constrained (Ancestor) then
                if not Is_Constrained (Act_T) then
-                  Error_Msg_N
-                    ("actual subtype must be constrained", Actual);
+                  Error_Msg_N ("actual subtype must be constrained", Actual);
                   Abandon_Instantiation (Actual);
                end if;
 
@@ -11024,12 +11807,10 @@ package body Sem_Ch12 is
 
             elsif Is_Constrained (Act_T) then
                if Ekind (Ancestor) = E_Access_Type
-                 or else
-                   (not Is_Constrained (A_Gen_T)
-                     and then Is_Composite_Type (A_Gen_T))
+                 or else (not Is_Constrained (A_Gen_T)
+                           and then Is_Composite_Type (A_Gen_T))
                then
-                  Error_Msg_N
-                    ("actual subtype must be unconstrained", Actual);
+                  Error_Msg_N ("actual subtype must be unconstrained", Actual);
                   Abandon_Instantiation (Actual);
                end if;
 
@@ -11043,7 +11824,7 @@ package body Sem_Ch12 is
                  ("actual for & cannot be a class-wide type", Actual, Gen_T);
                Abandon_Instantiation (Actual);
 
-            --  Otherwise, the formal and actual shall have the same number
+            --  Otherwise, the formal and actual must have the same number
             --  of discriminants and each discriminant of the actual must
             --  correspond to a discriminant of the formal.
 
@@ -11060,8 +11841,8 @@ package body Sem_Ch12 is
                     No (Corresponding_Discriminant (Actual_Discr))
                   then
                      Error_Msg_NE
-                       ("discriminant & does not correspond " &
-                        "to ancestor discriminant", Actual, Actual_Discr);
+                       ("discriminant & does not correspond "
+                        "to ancestor discriminant", Actual, Actual_Discr);
                      Abandon_Instantiation (Actual);
                   end if;
 
@@ -11092,7 +11873,9 @@ package body Sem_Ch12 is
                Abandon_Instantiation (Actual);
             end if;
 
-            if not Subtypes_Statically_Compatible (Act_T, Ancestor) then
+            if not Subtypes_Statically_Compatible
+                     (Act_T, Ancestor, Formal_Derived_Matching => True)
+            then
                Error_Msg_N
                  ("constraint on actual is incompatible with formal", Actual);
                Abandon_Instantiation (Actual);
@@ -11210,13 +11993,13 @@ package body Sem_Ch12 is
                                  Anc_F_Type := Etype (Anc_Formal);
                                  Act_F_Type := Etype (Act_Formal);
 
-                                 if Ekind (Anc_F_Type)
-                                      = E_Anonymous_Access_Type
+                                 if Ekind (Anc_F_Type) =
+                                                        E_Anonymous_Access_Type
                                  then
                                     Anc_F_Type := Designated_Type (Anc_F_Type);
 
-                                    if Ekind (Act_F_Type)
-                                         = E_Anonymous_Access_Type
+                                    if Ekind (Act_F_Type) =
+                                                        E_Anonymous_Access_Type
                                     then
                                        Act_F_Type :=
                                          Designated_Type (Act_F_Type);
@@ -11268,14 +12051,14 @@ package body Sem_Ch12 is
                                     Anc_F_Type := Etype (Anc_Subp);
                                     Act_F_Type := Etype (Act_Subp);
 
-                                    if Ekind (Anc_F_Type)
-                                         = E_Anonymous_Access_Type
+                                    if Ekind (Anc_F_Type) =
+                                                        E_Anonymous_Access_Type
                                     then
                                        Anc_F_Type :=
                                          Designated_Type (Anc_F_Type);
 
-                                       if Ekind (Act_F_Type)
-                                            = E_Anonymous_Access_Type
+                                       if Ekind (Act_F_Type) =
+                                                        E_Anonymous_Access_Type
                                        then
                                           Act_F_Type :=
                                             Designated_Type (Act_F_Type);
@@ -11303,9 +12086,8 @@ package body Sem_Ch12 is
                                       and then Anc_F_Type /= Act_F_Type
                                       and then
                                         Has_Controlling_Result (Anc_Subp)
-                                      and then
-                                        not Is_Tagged_Ancestor
-                                              (Anc_F_Type, Act_F_Type)
+                                      and then not Is_Tagged_Ancestor
+                                                     (Anc_F_Type, Act_F_Type)
                                     then
                                        Subprograms_Correspond := False;
                                     end if;
@@ -11317,10 +12099,9 @@ package body Sem_Ch12 is
 
                                  if Subprograms_Correspond then
                                     Error_Msg_NE
-                                      ("abstract subprogram & overrides " &
-                                       "nonabstract subprogram of ancestor",
-                                       Actual,
-                                       Act_Subp);
+                                      ("abstract subprogram & overrides "
+                                       & "nonabstract subprogram of ancestor",
+                                       Actual, Act_Subp);
                                  end if;
                               end if;
                            end if;
@@ -11352,8 +12133,8 @@ package body Sem_Ch12 is
                null;
             else
                Error_Msg_NE
-                 ("actual for non-limited & cannot be a limited type", Actual,
-                  Gen_T);
+                 ("actual for non-limited & cannot be a limited type",
+                  Actual, Gen_T);
                Explain_Limited_Type (Act_T, Actual);
                Abandon_Instantiation (Actual);
             end if;
@@ -11463,17 +12244,14 @@ package body Sem_Ch12 is
          if not Is_Interface (Act_T) then
             Error_Msg_NE
               ("actual for formal interface type must be an interface",
-                Actual, Gen_T);
+               Actual, Gen_T);
 
          elsif Is_Limited_Type (Act_T) /= Is_Limited_Type (A_Gen_T)
-           or else
-             Is_Task_Interface (A_Gen_T) /= Is_Task_Interface (Act_T)
-           or else
-             Is_Protected_Interface (A_Gen_T) /=
-               Is_Protected_Interface (Act_T)
-           or else
-             Is_Synchronized_Interface (A_Gen_T) /=
-               Is_Synchronized_Interface (Act_T)
+           or else Is_Task_Interface (A_Gen_T) /= Is_Task_Interface (Act_T)
+           or else Is_Protected_Interface (A_Gen_T) /=
+                   Is_Protected_Interface (Act_T)
+           or else Is_Synchronized_Interface (A_Gen_T) /=
+                   Is_Synchronized_Interface (Act_T)
          then
             Error_Msg_NE
               ("actual for interface& does not match (RM 12.5.5(4))",
@@ -11549,15 +12327,13 @@ package body Sem_Ch12 is
 
          if Is_Unchecked_Union (Base_Type (Act_T)) then
             if not Has_Discriminants (A_Gen_T)
-                     or else
-                   (Is_Derived_Type (A_Gen_T)
-                     and then
-                    Is_Unchecked_Union (A_Gen_T))
+              or else (Is_Derived_Type (A_Gen_T)
+                        and then Is_Unchecked_Union (A_Gen_T))
             then
                null;
             else
-               Error_Msg_N ("unchecked union cannot be the actual for a" &
-                 discriminated formal type", Act_T);
+               Error_Msg_N ("unchecked union cannot be the actual for a "
+                            & "discriminated formal type", Act_T);
 
             end if;
          end if;
@@ -11576,8 +12352,7 @@ package body Sem_Ch12 is
 
          if Ekind (Act_T) = E_Incomplete_Type
            or else (Is_Class_Wide_Type (Act_T)
-                      and then
-                         Ekind (Root_Type (Act_T)) = E_Incomplete_Type)
+                     and then Ekind (Root_Type (Act_T)) = E_Incomplete_Type)
          then
             --  If the formal is an incomplete type, the actual can be
             --  incomplete as well.
@@ -11667,10 +12442,12 @@ package body Sem_Ch12 is
                if not Is_Discrete_Type (Act_T) then
                   Error_Msg_NE
                     ("expect discrete type in instantiation of&",
-                       Actual, Gen_T);
+                     Actual, Gen_T);
                   Abandon_Instantiation (Actual);
                end if;
 
+               Diagnose_Predicated_Actual;
+
             when N_Formal_Signed_Integer_Type_Definition =>
                if not Is_Signed_Integer_Type (Act_T) then
                   Error_Msg_NE
@@ -11679,6 +12456,8 @@ package body Sem_Ch12 is
                   Abandon_Instantiation (Actual);
                end if;
 
+               Diagnose_Predicated_Actual;
+
             when N_Formal_Modular_Type_Definition =>
                if not Is_Modular_Integer_Type (Act_T) then
                   Error_Msg_NE
@@ -11687,6 +12466,8 @@ package body Sem_Ch12 is
                   Abandon_Instantiation (Actual);
                end if;
 
+               Diagnose_Predicated_Actual;
+
             when N_Formal_Floating_Point_Definition =>
                if not Is_Floating_Point_Type (Act_T) then
                   Error_Msg_NE
@@ -11742,7 +12523,7 @@ package body Sem_Ch12 is
       Decl_Node :=
         Make_Subtype_Declaration (Loc,
           Defining_Identifier => Subt,
-          Subtype_Indication  => New_Reference_To (Act_T, Loc));
+          Subtype_Indication  => New_Occurrence_Of (Act_T, Loc));
 
       if Is_Private_Type (Act_T) then
          Set_Has_Private_View (Subtype_Indication (Decl_Node));
@@ -11753,6 +12534,14 @@ package body Sem_Ch12 is
          Set_Has_Private_View (Subtype_Indication (Decl_Node));
       end if;
 
+      --  In Ada 2012 the actual may be a limited view. Indicate that
+      --  the local subtype must be treated as such.
+
+      if From_Limited_With (Act_T) then
+         Set_Ekind (Subt, E_Incomplete_Subtype);
+         Set_From_Limited_With (Subt);
+      end if;
+
       Decl_Nodes := New_List (Decl_Node);
 
       --  Flag actual derived types so their elaboration produces the
@@ -11774,9 +12563,8 @@ package body Sem_Ch12 is
             Set_Generic_Parent_Type (Decl_Node, Ancestor);
          end if;
 
-      elsif Nkind_In (Def,
-        N_Formal_Private_Type_Definition,
-        N_Formal_Incomplete_Type_Definition)
+      elsif Nkind_In (Def, N_Formal_Private_Type_Definition,
+                           N_Formal_Incomplete_Type_Definition)
       then
          Set_Generic_Parent_Type (Decl_Node, A_Gen_T);
       end if;
@@ -11805,7 +12593,7 @@ package body Sem_Ch12 is
               Make_Subtype_Declaration (Loc,
                 Defining_Identifier => New_Corr,
                 Subtype_Indication  =>
-                  New_Reference_To (Corr_Rec, Loc));
+                  New_Occurrence_Of (Corr_Rec, Loc));
             Append_To (Decl_Nodes, Corr_Decl);
 
             if Ekind (Act_T) = E_Task_Type then
@@ -11820,6 +12608,14 @@ package body Sem_Ch12 is
          end;
       end if;
 
+      --  For a floating-point type, capture dimension info if any, because
+      --  the generated subtype declaration does not come from source and
+      --  will not process dimensions.
+
+      if Is_Floating_Point_Type (Act_T) then
+         Copy_Dimensions (Act_T, Subt);
+      end if;
+
       return Decl_Nodes;
    end Instantiate_Type;
 
@@ -11954,7 +12750,7 @@ package body Sem_Ch12 is
       if not In_Same_Source_Unit (N, Spec)
         or else Nkind (Unit (Comp_Unit)) = N_Package_Declaration
         or else (Nkind (Unit (Comp_Unit)) = N_Package_Body
-                   and then not Is_In_Main_Unit (Spec))
+                  and then not Is_In_Main_Unit (Spec))
       then
          --  Find body of parent of spec, and analyze it. A special case arises
          --  when the parent is an instantiation, that is to say when we are
@@ -11973,8 +12769,8 @@ package body Sem_Ch12 is
            and then Nkind (True_Parent) /= N_Compilation_Unit
          loop
             if Nkind (True_Parent) = N_Package_Declaration
-                 and then
-               Nkind (Original_Node (True_Parent)) = N_Package_Instantiation
+              and then
+                Nkind (Original_Node (True_Parent)) = N_Package_Instantiation
             then
                --  Parent is a compilation unit that is an instantiation.
                --  Instantiation node has been replaced with package decl.
@@ -12123,14 +12919,24 @@ package body Sem_Ch12 is
                            --  Subprogram instance
 
                            else
-                              --  The instance_spec is the wrapper package,
-                              --  and the subprogram declaration is the last
-                              --  declaration in the wrapper.
+                              --  The instance_spec is in the wrapper package,
+                              --  usually followed by its local renaming
+                              --  declaration. See Build_Subprogram_Renaming
+                              --  for details.
+
+                              declare
+                                 Decl : Node_Id :=
+                                          (Last (Visible_Declarations
+                                            (Specification (Info.Act_Decl))));
+                              begin
+                                 if Nkind (Decl) =
+                                      N_Subprogram_Renaming_Declaration
+                                 then
+                                    Decl := Prev (Decl);
+                                 end if;
 
-                              Info.Act_Decl :=
-                                Last
-                                  (Visible_Declarations
-                                    (Specification (Info.Act_Decl)));
+                                 Info.Act_Decl := Decl;
+                              end;
 
                               Instantiate_Subprogram_Body
                                 (Info, Body_Optional => True);
@@ -12471,16 +13277,7 @@ package body Sem_Ch12 is
                Analyze (Act);
             end if;
 
-            --  Ensure that a ghost subprogram does not act as generic actual
-
-            if Is_Entity_Name (Act)
-              and then Is_Ghost_Subprogram (Entity (Act))
-            then
-               Error_Msg_N
-                 ("ghost subprogram & cannot act as generic actual", Act);
-               Abandon_Instantiation (Act);
-
-            elsif Errs /= Serious_Errors_Detected then
+            if Errs /= Serious_Errors_Detected then
 
                --  Do a minimal analysis of the generic, to prevent spurious
                --  warnings complaining about the generic being unreferenced,
@@ -12501,8 +13298,9 @@ package body Sem_Ch12 is
                   --  provide additional warning which might explain the error.
 
                   Set_Is_Immediately_Visible (Cur, Vis);
-                  Error_Msg_NE ("& hides outer unit with the same name??",
-                    N, Defining_Unit_Name (N));
+                  Error_Msg_NE
+                    ("& hides outer unit with the same name??",
+                     N, Defining_Unit_Name (N));
                end if;
 
                Abandon_Instantiation (Act);
@@ -12859,10 +13657,18 @@ package body Sem_Ch12 is
    -- Save_Global_References --
    ----------------------------
 
-   procedure Save_Global_References (N : Node_Id) is
+   procedure Save_Global_References (Templ : Node_Id) is
+
+      --  ??? it is horrible to use global variables in highly recursive code
+
+      E : Entity_Id;
+      --  The entity of the current associated node
+
       Gen_Scope : Entity_Id;
-      E         : Entity_Id;
-      N2        : Node_Id;
+      --  The scope of the generic for which references are being saved
+
+      N2 : Node_Id;
+      --  The current associated node
 
       function Is_Global (E : Entity_Id) return Boolean;
       --  Check whether entity is defined outside of generic unit. Examine the
@@ -12891,7 +13697,7 @@ package body Sem_Ch12 is
       --  nodes. N can also be a character literal, identifier, or operator
       --  symbol node, but the call has no effect in these cases.
 
-      procedure Save_Global_Defaults (N1, N2 : Node_Id);
+      procedure Save_Global_Defaults (N1 : Node_Id; N2 : Node_Id);
       --  Default actuals in nested instances must be handled specially
       --  because there is no link to them from the original tree. When an
       --  actual subprogram is given by a default, we add an explicit generic
@@ -12904,8 +13710,7 @@ package body Sem_Ch12 is
       --  so that it can be properly resolved in a subsequent instantiation.
 
       procedure Save_Global_Descendant (D : Union_Id);
-      --  Apply Save_Global_References recursively to the descendents of the
-      --  current node.
+      --  Apply Save_References recursively to the descendents of node D
 
       procedure Save_References (N : Node_Id);
       --  This is the recursive procedure that does the work, once the
@@ -12973,7 +13778,6 @@ package body Sem_Ch12 is
       ------------------
 
       procedure Reset_Entity (N : Node_Id) is
-
          procedure Set_Global_Type (N : Node_Id; N2 : Node_Id);
          --  If the type of N2 is global to the generic unit, save the type in
          --  the generic node. Just as we perform name capture for explicit
@@ -12997,14 +13801,12 @@ package body Sem_Ch12 is
          begin
             Set_Etype (N, Typ);
 
-            if Entity (N) /= N2
-              and then Has_Private_View (Entity (N))
-            then
-               --  If the entity of N is not the associated node, this is a
-               --  nested generic and it has an associated node as well, whose
-               --  type is already the full view (see below). Indicate that the
-               --  original node has a private view.
+            --  If the entity of N is not the associated node, this is a
+            --  nested generic and it has an associated node as well, whose
+            --  type is already the full view (see below). Indicate that the
+            --  original node has a private view.
 
+            if Entity (N) /= N2 and then Has_Private_View (Entity (N)) then
                Set_Has_Private_View (N);
             end if;
 
@@ -13055,7 +13857,7 @@ package body Sem_Ch12 is
 
       begin
          N2 := Get_Associated_Node (N);
-         E := Entity (N2);
+         E  := Entity (N2);
 
          if Present (E) then
 
@@ -13064,12 +13866,12 @@ package body Sem_Ch12 is
             --  preserve in this case, since the expansion will be redone in
             --  the instance.
 
-            if not Nkind_In (E, N_Defining_Identifier,
-                                N_Defining_Character_Literal,
+            if not Nkind_In (E, N_Defining_Character_Literal,
+                                N_Defining_Identifier,
                                 N_Defining_Operator_Symbol)
             then
                Set_Associated_Node (N, Empty);
-               Set_Etype  (N, Empty);
+               Set_Etype (N, Empty);
                return;
             end if;
 
@@ -13110,11 +13912,11 @@ package body Sem_Ch12 is
                      Set_Associated_Node (N, N2);
                      Set_Global_Type (N, N2);
 
-                  else
-                     --  Renaming is local, and will be resolved in instance
+                  --  Renaming is local, and will be resolved in instance
 
+                  else
                      Set_Associated_Node (N, Empty);
-                     Set_Etype  (N, Empty);
+                     Set_Etype (N, Empty);
                   end if;
 
                else
@@ -13124,18 +13926,18 @@ package body Sem_Ch12 is
             elsif Nkind (N) = N_Op_Concat
               and then Is_Generic_Type (Etype (N2))
               and then (Base_Type (Etype (Right_Opnd (N2))) = Etype (N2)
-                         or else
-                        Base_Type (Etype (Left_Opnd (N2)))  = Etype (N2))
+                          or else
+                        Base_Type (Etype (Left_Opnd  (N2))) = Etype (N2))
               and then Is_Intrinsic_Subprogram (E)
             then
                null;
 
-            else
-               --  Entity is local. Mark generic node as unresolved.
-               --  Note that now it does not have an entity.
+            --  Entity is local. Mark generic node as unresolved. Note that now
+            --  it does not have an entity.
 
+            else
                Set_Associated_Node (N, Empty);
-               Set_Etype  (N, Empty);
+               Set_Etype (N, Empty);
             end if;
 
             if Nkind (Parent (N)) in N_Generic_Instantiation
@@ -13180,7 +13982,7 @@ package body Sem_Ch12 is
               and then Parent (N) = Name (Parent (Parent (N)))
             then
                Save_Global_Defaults
-                 (Parent (Parent (N)), Parent (Parent ((N2))));
+                 (Parent (Parent (N)), Parent (Parent (N2)));
             end if;
 
          --  A selected component may denote a static constant that has been
@@ -13195,9 +13997,6 @@ package body Sem_Ch12 is
             then
                Rewrite (Parent (N), New_Copy (Parent (N2)));
                Set_Analyzed (Parent (N), False);
-
-            else
-               null;
             end if;
 
          --  A selected component may be transformed into a parameterless
@@ -13250,17 +14049,20 @@ package body Sem_Ch12 is
       begin
          case Nkind (N) is
             when N_Binary_Op =>
-               Save_Global_Descendant (Union_Id (Left_Opnd (N)));
+               Save_Global_Descendant (Union_Id (Left_Opnd  (N)));
                Save_Global_Descendant (Union_Id (Right_Opnd (N)));
 
             when N_Unary_Op =>
                Save_Global_Descendant (Union_Id (Right_Opnd (N)));
 
-            when N_Expanded_Name | N_Selected_Component =>
+            when N_Expanded_Name      |
+                 N_Selected_Component =>
                Save_Global_Descendant (Union_Id (Prefix (N)));
                Save_Global_Descendant (Union_Id (Selector_Name (N)));
 
-            when N_Identifier | N_Character_Literal | N_Operator_Symbol =>
+            when N_Identifier         |
+                 N_Character_Literal  |
+                 N_Operator_Symbol    =>
                null;
 
             when others =>
@@ -13272,7 +14074,7 @@ package body Sem_Ch12 is
       -- Save_Global_Defaults --
       --------------------------
 
-      procedure Save_Global_Defaults (N1, N2 : Node_Id) is
+      procedure Save_Global_Defaults (N1 : Node_Id; N2 : Node_Id) is
          Loc    : constant Source_Ptr := Sloc (N1);
          Assoc2 : constant List_Id    := Generic_Associations (N2);
          Gen_Id : constant Entity_Id  := Get_Generic_Entity (N2);
@@ -13341,9 +14143,10 @@ package body Sem_Ch12 is
                if Is_Global (Actual) then
                   Ndec :=
                     Make_Generic_Association (Loc,
-                      Selector_Name => New_Occurrence_Of (Subp, Loc),
-                        Explicit_Generic_Actual_Parameter =>
-                          New_Occurrence_Of (Actual, Loc));
+                      Selector_Name                     =>
+                        New_Occurrence_Of (Subp, Loc),
+                      Explicit_Generic_Actual_Parameter =>
+                        New_Occurrence_Of (Actual, Loc));
 
                   Set_Associated_Node
                     (Explicit_Generic_Actual_Parameter (Ndec), Def);
@@ -13356,8 +14159,9 @@ package body Sem_Ch12 is
                elsif Present (Next (Act2)) then
                   Ndec :=
                     Make_Generic_Association (Loc,
-                      Selector_Name => New_Occurrence_Of (Subp, Loc),
-                        Explicit_Generic_Actual_Parameter => Empty);
+                      Selector_Name                     =>
+                        New_Occurrence_Of (Subp, Loc),
+                      Explicit_Generic_Actual_Parameter => Empty);
 
                   Append (Ndec, Assoc1);
                end if;
@@ -13397,7 +14201,6 @@ package body Sem_Ch12 is
               (Selector_Name (Name (N1)), Selector_Name (Name (N2)));
             Set_Etype (Name (N1), Etype (Gen_Id));
          end if;
-
       end Save_Global_Defaults;
 
       ----------------------------
@@ -13417,9 +14220,7 @@ package body Sem_Ch12 is
             end if;
 
          elsif D in List_Range then
-            if D = Union_Id (No_List)
-              or else Is_Empty_List (List_Id (D))
-            then
+            if D = Union_Id (No_List) or else Is_Empty_List (List_Id (D)) then
                null;
 
             else
@@ -13452,99 +14253,197 @@ package body Sem_Ch12 is
       procedure Save_References (N : Node_Id) is
          Loc : constant Source_Ptr := Sloc (N);
 
-      begin
-         if N = Empty then
-            null;
+         function Requires_Delayed_Save (Nod : Node_Id) return Boolean;
+         --  Determine whether arbitrary node Nod requires delayed capture of
+         --  global references within its aspect specifications.
 
-         elsif Nkind_In (N, N_Character_Literal, N_Operator_Symbol) then
-            if Nkind (N) = Nkind (Get_Associated_Node (N)) then
-               Reset_Entity (N);
+         procedure Save_References_In_Aggregate (N : Node_Id);
+         --  Save all global references in [extension] aggregate node N
 
-            elsif Nkind (N) = N_Operator_Symbol
-              and then Nkind (Get_Associated_Node (N)) = N_String_Literal
-            then
-               Change_Operator_Symbol_To_String_Literal (N);
-            end if;
+         procedure Save_References_In_Char_Lit_Or_Op_Symbol (N : Node_Id);
+         --  Save all global references in a character literal or operator
+         --  symbol denoted by N.
 
-         elsif Nkind (N) in N_Op then
-            if Nkind (N) = Nkind (Get_Associated_Node (N)) then
-               if Nkind (N) = N_Op_Concat then
-                  Set_Is_Component_Left_Opnd (N,
-                    Is_Component_Left_Opnd (Get_Associated_Node (N)));
+         procedure Save_References_In_Descendants (N : Node_Id);
+         --  Save all global references in all descendants of node N
 
-                  Set_Is_Component_Right_Opnd (N,
-                    Is_Component_Right_Opnd (Get_Associated_Node (N)));
-               end if;
+         procedure Save_References_In_Identifier (N : Node_Id);
+         --  Save all global references in identifier node N
 
-               Reset_Entity (N);
+         procedure Save_References_In_Operator (N : Node_Id);
+         --  Save all global references in operator node N
 
-            else
-               --  Node may be transformed into call to a user-defined operator
+         procedure Save_References_In_Pragma (Prag : Node_Id);
+         --  Save all global references found within the expression of pragma
+         --  Prag.
 
-               N2 := Get_Associated_Node (N);
+         ---------------------------
+         -- Requires_Delayed_Save --
+         ---------------------------
 
-               if Nkind (N2) = N_Function_Call then
-                  E := Entity (Name (N2));
+         function Requires_Delayed_Save (Nod : Node_Id) return Boolean is
+         begin
+            --  Generic packages and subprograms require delayed capture of
+            --  global references within their aspects due to the timing of
+            --  annotation analysis.
 
-                  if Present (E)
-                    and then Is_Global (E)
-                  then
-                     Set_Etype (N, Etype (N2));
-                  else
-                     Set_Associated_Node (N, Empty);
-                     Set_Etype (N, Empty);
-                  end if;
+            if Nkind_In (Nod, N_Generic_Package_Declaration,
+                              N_Generic_Subprogram_Declaration,
+                              N_Package_Body,
+                              N_Package_Body_Stub,
+                              N_Subprogram_Body,
+                              N_Subprogram_Body_Stub)
+            then
+               --  Since the capture of global references is done on the
+               --  unanalyzed generic template, there is no information around
+               --  to infer the context. Use the Associated_Entity linkages to
+               --  peek into the analyzed generic copy and determine what the
+               --  template corresponds to.
+
+               if Nod = Templ then
+                  return
+                    Is_Generic_Declaration_Or_Body
+                      (Unit_Declaration_Node
+                        (Associated_Entity (Defining_Entity (Nod))));
+
+               --  Otherwise the generic unit being processed is not the top
+               --  level template. It is safe to capture of global references
+               --  within the generic unit because at this point the top level
+               --  copy is fully analyzed.
 
-               elsif Nkind_In (N2, N_Integer_Literal,
-                                   N_Real_Literal,
-                                   N_String_Literal)
-               then
-                  if Present (Original_Node (N2))
-                    and then Nkind (Original_Node (N2)) = Nkind (N)
-                  then
+               else
+                  return False;
+               end if;
 
-                     --  Operation was constant-folded. Whenever possible,
-                     --  recover semantic information from unfolded node,
-                     --  for ASIS use.
+            --  Otherwise capture the global references without interference
 
-                     Set_Associated_Node (N, Original_Node (N2));
+            else
+               return False;
+            end if;
+         end Requires_Delayed_Save;
 
-                     if Nkind (N) = N_Op_Concat then
-                        Set_Is_Component_Left_Opnd (N,
-                          Is_Component_Left_Opnd  (Get_Associated_Node (N)));
-                        Set_Is_Component_Right_Opnd (N,
-                          Is_Component_Right_Opnd (Get_Associated_Node (N)));
-                     end if;
+         ----------------------------------
+         -- Save_References_In_Aggregate --
+         ----------------------------------
 
-                     Reset_Entity (N);
+         procedure Save_References_In_Aggregate (N : Node_Id) is
+            Nam   : Node_Id;
+            Qual  : Node_Id   := Empty;
+            Typ   : Entity_Id := Empty;
 
-                  else
-                     --  If original node is already modified, propagate
-                     --  constant-folding to template.
+            use Atree.Unchecked_Access;
+            --  This code section is part of implementing an untyped tree
+            --  traversal, so it needs direct access to node fields.
 
-                     Rewrite (N, New_Copy (N2));
-                     Set_Analyzed (N, False);
-                  end if;
+         begin
+            N2 := Get_Associated_Node (N);
 
-               elsif Nkind (N2) = N_Identifier
-                 and then Ekind (Entity (N2)) = E_Enumeration_Literal
+            if Present (N2) then
+               Typ := Etype (N2);
+
+               --  In an instance within a generic, use the name of the actual
+               --  and not the original generic parameter. If the actual is
+               --  global in the current generic it must be preserved for its
+               --  instantiation.
+
+               if Nkind (Parent (Typ)) = N_Subtype_Declaration
+                 and then Present (Generic_Parent_Type (Parent (Typ)))
                then
-                  --  Same if call was folded into a literal, but in this case
-                  --  retain the entity to avoid spurious ambiguities if it is
-                  --  overloaded at the point of instantiation or inlining.
+                  Typ := Base_Type (Typ);
+                  Set_Etype (N2, Typ);
+               end if;
+            end if;
 
-                  Rewrite (N, New_Copy (N2));
-                  Set_Analyzed (N, False);
+            if No (N2) or else No (Typ) or else not Is_Global (Typ) then
+               Set_Associated_Node (N, Empty);
+
+               --  If the aggregate is an actual in a call, it has been
+               --  resolved in the current context, to some local type. The
+               --  enclosing call may have been disambiguated by the aggregate,
+               --  and this disambiguation might fail at instantiation time
+               --  because the type to which the aggregate did resolve is not
+               --  preserved. In order to preserve some of this information,
+               --  wrap the aggregate in a qualified expression, using the id
+               --  of its type. For further disambiguation we qualify the type
+               --  name with its scope (if visible) because both id's will have
+               --  corresponding entities in an instance. This resolves most of
+               --  the problems with missing type information on aggregates in
+               --  instances.
+
+               if Present (N2)
+                 and then Nkind (N2) = Nkind (N)
+                 and then Nkind (Parent (N2)) in N_Subprogram_Call
+                 and then Present (Typ)
+                 and then Comes_From_Source (Typ)
+               then
+                  Nam := Make_Identifier (Loc, Chars (Typ));
+
+                  if Is_Immediately_Visible (Scope (Typ)) then
+                     Nam :=
+                       Make_Selected_Component (Loc,
+                         Prefix        =>
+                           Make_Identifier (Loc, Chars (Scope (Typ))),
+                         Selector_Name => Nam);
+                  end if;
+
+                  Qual :=
+                    Make_Qualified_Expression (Loc,
+                      Subtype_Mark => Nam,
+                      Expression   => Relocate_Node (N));
                end if;
             end if;
 
-            --  Complete operands check if node has not been constant-folded
+            Save_Global_Descendant (Field1 (N));
+            Save_Global_Descendant (Field2 (N));
+            Save_Global_Descendant (Field3 (N));
+            Save_Global_Descendant (Field5 (N));
 
-            if Nkind (N) in N_Op then
-               Save_Entity_Descendants (N);
+            if Present (Qual) then
+               Rewrite (N, Qual);
             end if;
+         end Save_References_In_Aggregate;
+
+         ----------------------------------------------
+         -- Save_References_In_Char_Lit_Or_Op_Symbol --
+         ----------------------------------------------
+
+         procedure Save_References_In_Char_Lit_Or_Op_Symbol (N : Node_Id) is
+         begin
+            if Nkind (N) = Nkind (Get_Associated_Node (N)) then
+               Reset_Entity (N);
+
+            elsif Nkind (N) = N_Operator_Symbol
+              and then Nkind (Get_Associated_Node (N)) = N_String_Literal
+            then
+               Change_Operator_Symbol_To_String_Literal (N);
+            end if;
+         end Save_References_In_Char_Lit_Or_Op_Symbol;
+
+         ------------------------------------
+         -- Save_References_In_Descendants --
+         ------------------------------------
+
+         procedure Save_References_In_Descendants (N : Node_Id) is
+            use Atree.Unchecked_Access;
+            --  This code section is part of implementing an untyped tree
+            --  traversal, so it needs direct access to node fields.
+
+         begin
+            Save_Global_Descendant (Field1 (N));
+            Save_Global_Descendant (Field2 (N));
+            Save_Global_Descendant (Field3 (N));
+            Save_Global_Descendant (Field4 (N));
+            Save_Global_Descendant (Field5 (N));
+         end Save_References_In_Descendants;
+
+         -----------------------------------
+         -- Save_References_In_Identifier --
+         -----------------------------------
+
+         procedure Save_References_In_Identifier (N : Node_Id) is
+         begin
+            --  The node did not undergo a transformation
 
-         elsif Nkind (N) = N_Identifier then
             if Nkind (N) = Nkind (Get_Associated_Node (N)) then
 
                --  If this is a discriminant reference, always save it. It is
@@ -13555,50 +14454,47 @@ package body Sem_Ch12 is
                  (N, Original_Discriminant (Get_Associated_Node (N)));
                Reset_Entity (N);
 
+            --  The analysis of the generic copy transformed the identifier
+            --  into another construct. Propagate the changes to the template.
+
             else
                N2 := Get_Associated_Node (N);
 
+               --  The identifier denotes a call to a parameterless function.
+               --  Mark the node as resolved when the function is external.
+
                if Nkind (N2) = N_Function_Call then
                   E := Entity (Name (N2));
 
-                  --  Name resolves to a call to parameterless function. If
-                  --  original entity is global, mark node as resolved.
-
-                  if Present (E)
-                    and then Is_Global (E)
-                  then
+                  if Present (E) and then Is_Global (E) then
                      Set_Etype (N, Etype (N2));
                   else
                      Set_Associated_Node (N, Empty);
                      Set_Etype (N, Empty);
                   end if;
 
+               --  The identifier denotes a named number that was constant
+               --  folded. Preserve the original name for ASIS and undo the
+               --  constant folding which will be repeated in the instance.
+
                elsif Nkind_In (N2, N_Integer_Literal, N_Real_Literal)
                  and then Is_Entity_Name (Original_Node (N2))
                then
-                  --  Name resolves to named number that is constant-folded,
-                  --  We must preserve the original name for ASIS use, and
-                  --  undo the constant-folding, which will be repeated in
-                  --  each instance.
-
                   Set_Associated_Node (N, Original_Node (N2));
                   Reset_Entity (N);
 
-               elsif Nkind (N2) = N_String_Literal then
-
-                  --  Name resolves to string literal. Perform the same
-                  --  replacement in generic.
+               --  The identifier resolved to a string literal. Propagate this
+               --  information to the generic template.
 
+               elsif Nkind (N2) = N_String_Literal then
                   Rewrite (N, New_Copy (N2));
 
-               elsif Nkind (N2) = N_Explicit_Dereference then
-
-                  --  An identifier is rewritten as a dereference if it is the
-                  --  prefix in an implicit dereference (call or attribute).
-                  --  The analysis of an instantiation will expand the node
-                  --  again, so we preserve the original tree but link it to
-                  --  the resolved entity in case it is global.
+               --  The identifier is rewritten as a dereference if it is the
+               --  prefix of an implicit dereference. Preserve the original
+               --  tree as the analysis of the instance will expand the node
+               --  again, but preserve the resolved entity if it is global.
 
+               elsif Nkind (N2) = N_Explicit_Dereference then
                   if Is_Entity_Name (Prefix (N2))
                     and then Present (Entity (Prefix (N2)))
                     and then Is_Global (Entity (Prefix (N2)))
@@ -13606,14 +14502,16 @@ package body Sem_Ch12 is
                      Set_Associated_Node (N, Prefix (N2));
 
                   elsif Nkind (Prefix (N2)) = N_Function_Call
+                    and then Present (Entity (Name (Prefix (N2))))
                     and then Is_Global (Entity (Name (Prefix (N2))))
                   then
                      Rewrite (N,
                        Make_Explicit_Dereference (Loc,
-                          Prefix => Make_Function_Call (Loc,
-                            Name =>
-                              New_Occurrence_Of (Entity (Name (Prefix (N2))),
-                                                 Loc))));
+                         Prefix =>
+                           Make_Function_Call (Loc,
+                             Name =>
+                               New_Occurrence_Of
+                                 (Entity (Name (Prefix (N2))), Loc))));
 
                   else
                      Set_Associated_Node (N, Empty);
@@ -13629,127 +14527,211 @@ package body Sem_Ch12 is
                then
                   Set_Associated_Node (N, Original_Node (N2));
                   Reset_Entity (N);
-
-               else
-                  null;
                end if;
             end if;
+         end Save_References_In_Identifier;
 
-         elsif Nkind (N) in N_Entity then
-            null;
+         ---------------------------------
+         -- Save_References_In_Operator --
+         ---------------------------------
 
-         else
-            declare
-               Qual : Node_Id := Empty;
-               Typ  : Entity_Id := Empty;
-               Nam  : Node_Id;
+         procedure Save_References_In_Operator (N : Node_Id) is
+         begin
+            --  The node did not undergo a transformation
 
-               use Atree.Unchecked_Access;
-               --  This code section is part of implementing an untyped tree
-               --  traversal, so it needs direct access to node fields.
+            if Nkind (N) = Nkind (Get_Associated_Node (N)) then
+               if Nkind (N) = N_Op_Concat then
+                  Set_Is_Component_Left_Opnd (N,
+                    Is_Component_Left_Opnd (Get_Associated_Node (N)));
 
-            begin
-               if Nkind_In (N, N_Aggregate, N_Extension_Aggregate) then
-                  N2 := Get_Associated_Node (N);
+                  Set_Is_Component_Right_Opnd (N,
+                    Is_Component_Right_Opnd (Get_Associated_Node (N)));
+               end if;
 
-                  if No (N2) then
-                     Typ := Empty;
-                  else
-                     Typ := Etype (N2);
+               Reset_Entity (N);
 
-                     --  In an instance within a generic, use the name of the
-                     --  actual and not the original generic parameter. If the
-                     --  actual is global in the current generic it must be
-                     --  preserved for its instantiation.
+            --  The analysis of the generic copy transformed the operator into
+            --  some other construct. Propagate the changes to the template.
 
-                     if Nkind (Parent (Typ)) = N_Subtype_Declaration
-                       and then
-                         Present (Generic_Parent_Type (Parent (Typ)))
-                     then
-                        Typ := Base_Type (Typ);
-                        Set_Etype (N2, Typ);
-                     end if;
+            else
+               N2 := Get_Associated_Node (N);
+
+               --  The operator resoved to a function call
+
+               if Nkind (N2) = N_Function_Call then
+                  E := Entity (Name (N2));
+
+                  if Present (E) and then Is_Global (E) then
+                     Set_Etype (N, Etype (N2));
+                  else
+                     Set_Associated_Node (N, Empty);
+                     Set_Etype (N, Empty);
                   end if;
 
-                  if No (N2)
-                    or else No (Typ)
-                    or else not Is_Global (Typ)
+               --  The operator was folded into a literal
+
+               elsif Nkind_In (N2, N_Integer_Literal,
+                                   N_Real_Literal,
+                                   N_String_Literal)
+               then
+                  if Present (Original_Node (N2))
+                    and then Nkind (Original_Node (N2)) = Nkind (N)
                   then
-                     Set_Associated_Node (N, Empty);
+                     --  Operation was constant-folded. Whenever possible,
+                     --  recover semantic information from unfolded node,
+                     --  for ASIS use.
 
-                     --  If the aggregate is an actual in a call, it has been
-                     --  resolved in the current context, to some local type.
-                     --  The enclosing call may have been disambiguated by the
-                     --  aggregate, and this disambiguation might fail at
-                     --  instantiation time because the type to which the
-                     --  aggregate did resolve is not preserved. In order to
-                     --  preserve some of this information, we wrap the
-                     --  aggregate in a qualified expression, using the id of
-                     --  its type. For further disambiguation we qualify the
-                     --  type name with its scope (if visible) because both
-                     --  id's will have corresponding entities in an instance.
-                     --  This resolves most of the problems with missing type
-                     --  information on aggregates in instances.
-
-                     if Nkind (N2) = Nkind (N)
-                       and then Nkind (Parent (N2)) in N_Subprogram_Call
-                       and then Comes_From_Source (Typ)
-                     then
-                        if Is_Immediately_Visible (Scope (Typ)) then
-                           Nam := Make_Selected_Component (Loc,
-                             Prefix =>
-                               Make_Identifier (Loc, Chars (Scope (Typ))),
-                             Selector_Name =>
-                               Make_Identifier (Loc, Chars (Typ)));
-                        else
-                           Nam := Make_Identifier (Loc, Chars (Typ));
-                        end if;
+                     Set_Associated_Node (N, Original_Node (N2));
 
-                        Qual :=
-                          Make_Qualified_Expression (Loc,
-                            Subtype_Mark => Nam,
-                            Expression => Relocate_Node (N));
+                     if Nkind (N) = N_Op_Concat then
+                        Set_Is_Component_Left_Opnd (N,
+                          Is_Component_Left_Opnd  (Get_Associated_Node (N)));
+                        Set_Is_Component_Right_Opnd (N,
+                          Is_Component_Right_Opnd (Get_Associated_Node (N)));
                      end if;
-                  end if;
 
-                  Save_Global_Descendant (Field1 (N));
-                  Save_Global_Descendant (Field2 (N));
-                  Save_Global_Descendant (Field3 (N));
-                  Save_Global_Descendant (Field5 (N));
+                     Reset_Entity (N);
 
-                  if Present (Qual) then
-                     Rewrite (N, Qual);
+                  --  Propagate the constant folding back to the template
+
+                  else
+                     Rewrite (N, New_Copy (N2));
+                     Set_Analyzed (N, False);
                   end if;
 
-               --  All other cases than aggregates
+               --  The operator was folded into an enumeration literal. Retain
+               --  the entity to avoid spurious ambiguities if it is overloaded
+               --  at the point of instantiation or inlining.
+
+               elsif Nkind (N2) = N_Identifier
+                 and then Ekind (Entity (N2)) = E_Enumeration_Literal
+               then
+                  Rewrite (N, New_Copy (N2));
+                  Set_Analyzed (N, False);
+               end if;
+            end if;
+
+            --  Complete the operands check if node has not been constant
+            --  folded.
+
+            if Nkind (N) in N_Op then
+               Save_Entity_Descendants (N);
+            end if;
+         end Save_References_In_Operator;
+
+         -------------------------------
+         -- Save_References_In_Pragma --
+         -------------------------------
+
+         procedure Save_References_In_Pragma (Prag : Node_Id) is
+            Context : Node_Id;
+            Do_Save : Boolean := True;
+
+            use Atree.Unchecked_Access;
+            --  This code section is part of implementing an untyped tree
+            --  traversal, so it needs direct access to node fields.
+
+         begin
+            --  Do not save global references in pragmas generated from aspects
+            --  because the pragmas will be regenerated at instantiation time.
+
+            if From_Aspect_Specification (Prag) then
+               Do_Save := False;
+
+            --  The capture of global references within contract-related source
+            --  pragmas associated with generic packages, subprograms or their
+            --  respective bodies must be delayed due to timing of annotation
+            --  analysis. Global references are still captured in routine
+            --  Save_Global_References_In_Contract.
+
+            elsif Is_Generic_Contract_Pragma (Prag) and then Prag /= Templ then
+               if Is_Package_Contract_Annotation (Prag) then
+                  Context := Find_Related_Package_Or_Body (Prag);
 
                else
-                  Save_Global_Descendant (Field1 (N));
-                  Save_Global_Descendant (Field2 (N));
-                  Save_Global_Descendant (Field3 (N));
-                  Save_Global_Descendant (Field4 (N));
-                  Save_Global_Descendant (Field5 (N));
+                  pragma Assert (Is_Subprogram_Contract_Annotation (Prag));
+                  Context := Find_Related_Subprogram_Or_Body (Prag);
                end if;
-            end;
+
+               --  The use of Original_Node accounts for the case when the
+               --  related context is generic template.
+
+               if Requires_Delayed_Save (Original_Node (Context)) then
+                  Do_Save := False;
+               end if;
+            end if;
+
+            --  For all other cases, save all global references within the
+            --  descendants, but skip the following semantic fields:
+
+            --    Field1 - Next_Pragma
+            --    Field3 - Corresponding_Aspect
+            --    Field5 - Next_Rep_Item
+
+            if Do_Save then
+               Save_Global_Descendant (Field2 (Prag));
+               Save_Global_Descendant (Field4 (Prag));
+            end if;
+         end Save_References_In_Pragma;
+
+      --  Start of processing for Save_References
+
+      begin
+         if N = Empty then
+            null;
+
+         --  Aggregates
+
+         elsif Nkind_In (N, N_Aggregate, N_Extension_Aggregate) then
+            Save_References_In_Aggregate (N);
+
+         --  Character literals, operator symbols
+
+         elsif Nkind_In (N, N_Character_Literal, N_Operator_Symbol) then
+            Save_References_In_Char_Lit_Or_Op_Symbol (N);
+
+         --  Defining identifiers
+
+         elsif Nkind (N) in N_Entity then
+            null;
+
+         --  Identifiers
+
+         elsif Nkind (N) = N_Identifier then
+            Save_References_In_Identifier (N);
+
+         --  Operators
+
+         elsif Nkind (N) in N_Op then
+            Save_References_In_Operator (N);
+
+         --  Pragmas
+
+         elsif Nkind (N) = N_Pragma then
+            Save_References_In_Pragma (N);
+
+         else
+            Save_References_In_Descendants (N);
          end if;
 
-         --  If a node has aspects, references within their expressions must
-         --  be saved separately, given they are not directly in the tree.
+         --  Save all global references found within the aspect specifications
+         --  of the related node.
 
-         if Has_Aspects (N) then
-            declare
-               Aspect : Node_Id;
+         if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
 
-            begin
-               Aspect := First (Aspect_Specifications (N));
-               while Present (Aspect) loop
-                  if Present (Expression (Aspect)) then
-                     Save_Global_References (Expression (Aspect));
-                  end if;
+            --  The capture of global references within aspects associated with
+            --  generic packages, subprograms or their bodies must be delayed
+            --  due to timing of annotation analysis. Global references are
+            --  still captured in routine Save_Global_References_In_Contract.
 
-                  Next (Aspect);
-               end loop;
-            end;
+            if Requires_Delayed_Save (N) then
+               null;
+
+            --  Otherwise save all global references within the aspects
+
+            else
+               Save_Global_References_In_Aspects (N);
+            end if;
          end if;
       end Save_References;
 
@@ -13768,9 +14750,87 @@ package body Sem_Ch12 is
          Gen_Scope := Scope (Gen_Scope);
       end loop;
 
-      Save_References (N);
+      Save_References (Templ);
    end Save_Global_References;
 
+   ---------------------------------------
+   -- Save_Global_References_In_Aspects --
+   ---------------------------------------
+
+   procedure Save_Global_References_In_Aspects (N : Node_Id) is
+      Asp  : Node_Id;
+      Expr : Node_Id;
+
+   begin
+      Asp := First (Aspect_Specifications (N));
+      while Present (Asp) loop
+         Expr := Expression (Asp);
+
+         if Present (Expr) then
+            Save_Global_References (Expr);
+         end if;
+
+         Next (Asp);
+      end loop;
+   end Save_Global_References_In_Aspects;
+
+   ----------------------------------------
+   -- Save_Global_References_In_Contract --
+   ----------------------------------------
+
+   procedure Save_Global_References_In_Contract
+     (Templ  : Node_Id;
+      Gen_Id : Entity_Id)
+   is
+      procedure Save_Global_References_In_List (First_Prag : Node_Id);
+      --  Save all global references in contract-related source pragmas found
+      --  in the list starting with pragma First_Prag.
+
+      ------------------------------------
+      -- Save_Global_References_In_List --
+      ------------------------------------
+
+      procedure Save_Global_References_In_List (First_Prag : Node_Id) is
+         Prag : Node_Id;
+
+      begin
+         Prag := First_Prag;
+         while Present (Prag) loop
+            if Is_Generic_Contract_Pragma (Prag) then
+               Save_Global_References (Prag);
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+      end Save_Global_References_In_List;
+
+      --  Local variables
+
+      Items : constant Node_Id := Contract (Defining_Entity (Templ));
+
+   --  Start of processing for Save_Global_References_In_Contract
+
+   begin
+      --  The entity of the analyzed generic copy must be on the scope stack
+      --  to ensure proper detection of global references.
+
+      Push_Scope (Gen_Id);
+
+      if Permits_Aspect_Specifications (Templ)
+        and then Has_Aspects (Templ)
+      then
+         Save_Global_References_In_Aspects (Templ);
+      end if;
+
+      if Present (Items) then
+         Save_Global_References_In_List (Pre_Post_Conditions (Items));
+         Save_Global_References_In_List (Contract_Test_Cases (Items));
+         Save_Global_References_In_List (Classifications     (Items));
+      end if;
+
+      Pop_Scope;
+   end Save_Global_References_In_Contract;
+
    --------------------------------------
    -- Set_Copied_Sloc_For_Inlined_Body --
    --------------------------------------
@@ -13854,6 +14914,12 @@ package body Sem_Ch12 is
 
          SPARK_Mode := Save_SPARK_Mode;
          SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma;
+
+         --  Make sure dynamic elaboration checks are off in SPARK Mode
+
+         if SPARK_Mode = On then
+            Dynamic_Elaboration_Checks := False;
+         end if;
       end if;
 
       Current_Instantiated_Parent :=
@@ -13940,9 +15006,7 @@ package body Sem_Ch12 is
       OK      : Boolean;
 
    begin
-      if No (T)
-        or else T = Any_Id
-      then
+      if No (T) or else T = Any_Id then
          return;
       end if;
 
@@ -13981,8 +15045,8 @@ package body Sem_Ch12 is
       end case;
 
       if not OK then
-         Error_Msg_N ("attribute reference has wrong profile for subprogram",
-           Def);
+         Error_Msg_N
+           ("attribute reference has wrong profile for subprogram", Def);
       end if;
    end Valid_Default_Attribute;