[multiple changes]
[gcc.git] / gcc / ada / sem_ch3.adb
index df0293c8525b4ba2229b413fd5e9f57afc633ac3..1f774c00a62ece2d3284ff60460d45e25acad08d 100644 (file)
@@ -33,6 +33,7 @@ with Einfo;     use Einfo;
 with Errout;    use Errout;
 with Eval_Fat;  use Eval_Fat;
 with Exp_Ch3;   use Exp_Ch3;
+with Exp_Ch7;   use Exp_Ch7;
 with Exp_Ch9;   use Exp_Ch9;
 with Exp_Disp;  use Exp_Disp;
 with Exp_Dist;  use Exp_Dist;
@@ -646,17 +647,6 @@ package body Sem_Ch3 is
    --  present. If errors are found, error messages are posted, and the
    --  Real_Range_Specification of Def is reset to Empty.
 
-   procedure Propagate_Default_Init_Cond_Attributes
-     (From_Typ             : Entity_Id;
-      To_Typ               : Entity_Id;
-      Parent_To_Derivation : Boolean := False;
-      Private_To_Full_View : Boolean := False);
-   --  Subsidiary to routines Build_Derived_Type and Process_Full_View. Inherit
-   --  all attributes related to pragma Default_Initial_Condition from From_Typ
-   --  to To_Typ. Flag Parent_To_Derivation should be set when the context is
-   --  the creation of a derived type. Flag Private_To_Full_View should be set
-   --  when processing both views of a private type.
-
    procedure Record_Type_Declaration
      (T    : Entity_Id;
       N    : Node_Id;
@@ -1343,7 +1333,9 @@ package body Sem_Ch3 is
       if Nkind (S) /= N_Subtype_Indication then
          Analyze (S);
 
-         if Ekind (Root_Type (Entity (S))) = E_Incomplete_Type then
+         if Present (Entity (S))
+           and then Ekind (Root_Type (Entity (S))) = E_Incomplete_Type
+         then
             Set_Directly_Designated_Type (T, Entity (S));
 
             --  If the designated type is a limited view, we cannot tell if
@@ -1415,7 +1407,7 @@ package body Sem_Ch3 is
       elsif Is_Class_Wide_Type (Full_Desig) and then Etype (Full_Desig) = T
       then
          Error_Msg_N
-           ("access type cannot designate its own classwide type", S);
+           ("access type cannot designate its own class-wide type", S);
 
          --  Clean up indication of tagged status to prevent cascaded errors
 
@@ -1437,8 +1429,9 @@ package body Sem_Ch3 is
       --  and to Has_Protected.
 
       Set_Has_Task                 (T, False);
-      Set_Has_Controlled_Component (T, False);
       Set_Has_Protected            (T, False);
+      Set_Has_Timing_Event         (T, False);
+      Set_Has_Controlled_Component (T, False);
 
       --  Initialize field Finalization_Master explicitly to Empty, to avoid
       --  problems where an incomplete view of this entity has been previously
@@ -1857,7 +1850,6 @@ package body Sem_Ch3 is
 
             when others =>
                return False;
-
          end case;
       end Contains_POC;
 
@@ -2164,16 +2156,45 @@ package body Sem_Ch3 is
       --  (They have the sloc of the label as found in the source, and that
       --  is ahead of the current declarative part).
 
+      procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id);
+      --  Create the subprogram bodies which verify the run-time semantics of
+      --  the pragmas listed below for each elibigle type found in declarative
+      --  list Decls. The pragmas are:
+      --
+      --    Default_Initial_Condition
+      --    Invariant
+      --    Type_Invariant
+      --
+      --  Context denotes the owner of the declarative list.
+
+      procedure Check_Entry_Contracts;
+      --  Perform a pre-analysis of the pre- and postconditions of an entry
+      --  declaration. This must be done before full resolution and creation
+      --  of the parameter block, etc. to catch illegal uses within the
+      --  contract expression. Full analysis of the expression is done when
+      --  the contract is processed.
+
       procedure Handle_Late_Controlled_Primitive (Body_Decl : Node_Id);
       --  Determine whether Body_Decl denotes the body of a late controlled
       --  primitive (either Initialize, Adjust or Finalize). If this is the
       --  case, add a proper spec if the body lacks one. The spec is inserted
-      --  before Body_Decl and immedately analyzed.
+      --  before Body_Decl and immediately analyzed.
+
+      procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id);
+      --  Spec_Id is the entity of a package that may define abstract states,
+      --  and in the case of a child unit, whose ancestors may define abstract
+      --  states. If the states have partial visible refinement, remove the
+      --  partial visibility of each constituent at the end of the package
+      --  spec and body declarations.
 
       procedure Remove_Visible_Refinements (Spec_Id : Entity_Id);
       --  Spec_Id is the entity of a package that may define abstract states.
       --  If the states have visible refinement, remove the visibility of each
-      --  constituent at the end of the package body declarations.
+      --  constituent at the end of the package body declaration.
+
+      procedure Resolve_Aspects;
+      --  Utility to resolve the expressions of aspects at the end of a list of
+      --  declarations.
 
       -----------------
       -- Adjust_Decl --
@@ -2188,6 +2209,135 @@ package body Sem_Ch3 is
          end loop;
       end Adjust_Decl;
 
+      ----------------------------
+      -- Build_Assertion_Bodies --
+      ----------------------------
+
+      procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id) is
+         procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id);
+         --  Create the subprogram bodies which verify the run-time semantics
+         --  of the pragmas listed below for type Typ. The pragmas are:
+         --
+         --    Default_Initial_Condition
+         --    Invariant
+         --    Type_Invariant
+
+         -------------------------------------
+         -- Build_Assertion_Bodies_For_Type --
+         -------------------------------------
+
+         procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id) is
+         begin
+            --  Preanalyze and resolve the Default_Initial_Condition assertion
+            --  expression at the end of the declarations to catch any errors.
+
+            if Has_DIC (Typ) then
+               Build_DIC_Procedure_Body (Typ);
+            end if;
+
+            if Nkind (Context) = N_Package_Specification then
+
+               --  Preanalyze and resolve the invariants of a private type
+               --  at the end of the visible declarations to catch potential
+               --  errors. Inherited class-wide invariants are not included
+               --  because they have already been resolved.
+
+               if Decls = Visible_Declarations (Context)
+                 and then Ekind_In (Typ, E_Limited_Private_Type,
+                                         E_Private_Type,
+                                         E_Record_Type_With_Private)
+                 and then Has_Own_Invariants (Typ)
+               then
+                  Build_Invariant_Procedure_Body
+                    (Typ               => Typ,
+                     Partial_Invariant => True);
+
+               --  Preanalyze and resolve the invariants of a private type's
+               --  full view at the end of the private declarations to catch
+               --  potential errors.
+
+               elsif Decls = Private_Declarations (Context)
+                 and then not Is_Private_Type (Typ)
+                 and then Has_Private_Declaration (Typ)
+                 and then Has_Invariants (Typ)
+               then
+                  Build_Invariant_Procedure_Body (Typ);
+               end if;
+            end if;
+         end Build_Assertion_Bodies_For_Type;
+
+         --  Local variables
+
+         Decl    : Node_Id;
+         Decl_Id : Entity_Id;
+
+      --  Start of processing for Build_Assertion_Bodies
+
+      begin
+         Decl := First (Decls);
+         while Present (Decl) loop
+            if Is_Declaration (Decl) then
+               Decl_Id := Defining_Entity (Decl);
+
+               if Is_Type (Decl_Id) then
+                  Build_Assertion_Bodies_For_Type (Decl_Id);
+               end if;
+            end if;
+
+            Next (Decl);
+         end loop;
+      end Build_Assertion_Bodies;
+
+      ---------------------------
+      -- Check_Entry_Contracts --
+      ---------------------------
+
+      procedure Check_Entry_Contracts is
+         ASN : Node_Id;
+         Ent : Entity_Id;
+         Exp : Node_Id;
+
+      begin
+         Ent := First_Entity (Current_Scope);
+         while Present (Ent) loop
+
+            --  This only concerns entries with pre/postconditions
+
+            if Ekind (Ent) = E_Entry
+              and then Present (Contract (Ent))
+              and then Present (Pre_Post_Conditions (Contract (Ent)))
+            then
+               ASN := Pre_Post_Conditions (Contract (Ent));
+               Push_Scope (Ent);
+               Install_Formals (Ent);
+
+               --  Pre/postconditions are rewritten as Check pragmas. Analysis
+               --  is performed on a copy of the pragma expression, to prevent
+               --  modifying the original expression.
+
+               while Present (ASN) loop
+                  if Nkind (ASN) = N_Pragma then
+                     Exp :=
+                       New_Copy_Tree
+                         (Expression
+                           (First (Pragma_Argument_Associations (ASN))));
+                     Set_Parent (Exp, ASN);
+
+                     --  ??? why not Preanalyze_Assert_Expression
+
+                     Preanalyze (Exp);
+                  end if;
+
+                  ASN := Next_Pragma (ASN);
+               end loop;
+
+               End_Scope;
+            end if;
+
+            Next_Entity (Ent);
+         end loop;
+      end Check_Entry_Contracts;
+
       --------------------------------------
       -- Handle_Late_Controlled_Primitive --
       --------------------------------------
@@ -2269,10 +2419,37 @@ package body Sem_Ch3 is
 
          Set_Null_Present (Spec, False);
 
-         Insert_Before_And_Analyze (Body_Decl,
-           Make_Subprogram_Declaration (Loc, Specification => Spec));
+         --  Ensure that the freeze node is inserted after the declaration of
+         --  the primitive since its expansion will freeze the primitive.
+
+         Decl := Make_Subprogram_Declaration (Loc, Specification => Spec);
+
+         Insert_Before_And_Analyze (Body_Decl, Decl);
       end Handle_Late_Controlled_Primitive;
 
+      ----------------------------------------
+      -- Remove_Partial_Visible_Refinements --
+      ----------------------------------------
+
+      procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id) is
+         State_Elmt : Elmt_Id;
+      begin
+         if Present (Abstract_States (Spec_Id)) then
+            State_Elmt := First_Elmt (Abstract_States (Spec_Id));
+            while Present (State_Elmt) loop
+               Set_Has_Partial_Visible_Refinement (Node (State_Elmt), False);
+               Next_Elmt (State_Elmt);
+            end loop;
+         end if;
+
+         --  For a child unit, also hide the partial state refinement from
+         --  ancestor packages.
+
+         if Is_Child_Unit (Spec_Id) then
+            Remove_Partial_Visible_Refinements (Scope (Spec_Id));
+         end if;
+      end Remove_Partial_Visible_Refinements;
+
       --------------------------------
       -- Remove_Visible_Refinements --
       --------------------------------
@@ -2289,6 +2466,21 @@ package body Sem_Ch3 is
          end if;
       end Remove_Visible_Refinements;
 
+      ---------------------
+      -- Resolve_Aspects --
+      ---------------------
+
+      procedure Resolve_Aspects is
+         E : Entity_Id;
+
+      begin
+         E := First_Entity (Current_Scope);
+         while Present (E) loop
+            Resolve_Aspect_Expressions (E);
+            Next_Entity (E);
+         end loop;
+      end Resolve_Aspects;
+
       --  Local variables
 
       Context     : Node_Id   := Empty;
@@ -2298,6 +2490,10 @@ package body Sem_Ch3 is
       Body_Seen : Boolean := False;
       --  Flag set when the first body [stub] is encountered
 
+      Ignore_Freezing : Boolean;
+      --  Flag set when deciding to freeze an expression function in the
+      --  current scope.
+
    --  Start of processing for Analyze_Declarations
 
    begin
@@ -2344,12 +2540,14 @@ package body Sem_Ch3 is
          --  (This is needed in any case for early instantiations ???).
 
          if No (Next_Decl) then
-            if Nkind_In (Parent (L), N_Component_List,
-                                     N_Task_Definition,
-                                     N_Protected_Definition)
-            then
+            if Nkind (Parent (L)) = N_Component_List then
                null;
 
+            elsif Nkind_In (Parent (L), N_Protected_Definition,
+                                        N_Task_Definition)
+            then
+               Check_Entry_Contracts;
+
             elsif Nkind (Parent (L)) /= N_Package_Specification then
                if Nkind (Parent (L)) = N_Package_Body then
                   Freeze_From := First_Entity (Current_Scope);
@@ -2365,17 +2563,42 @@ package body Sem_Ch3 is
                Freeze_All (First_Entity (Current_Scope), Decl);
                Freeze_From := Last_Entity (Current_Scope);
 
+            --  Current scope is a package specification
+
             elsif Scope (Current_Scope) /= Standard_Standard
               and then not Is_Child_Unit (Current_Scope)
               and then No (Generic_Parent (Parent (L)))
             then
-               null;
+               --  This is needed in all cases to catch visibility errors in
+               --  aspect expressions, but several large user tests are now
+               --  rejected. Pending notification we restrict this call to
+               --  ASIS mode.
+
+               if False and then ASIS_Mode then -- ????
+                  Resolve_Aspects;
+               end if;
 
             elsif L /= Visible_Declarations (Parent (L))
-               or else No (Private_Declarations (Parent (L)))
-               or else Is_Empty_List (Private_Declarations (Parent (L)))
+              or else No (Private_Declarations (Parent (L)))
+              or else Is_Empty_List (Private_Declarations (Parent (L)))
             then
                Adjust_Decl;
+
+               --  End of a package declaration
+
+               --  In compilation mode the expansion of freeze node takes care
+               --  of resolving expressions of all aspects in the list. In ASIS
+               --  mode this must be done explicitly.
+
+               if ASIS_Mode
+                 and then Scope (Current_Scope) = Standard_Standard
+               then
+                  Resolve_Aspects;
+               end if;
+
+               --  This is a freeze point because it is the end of a
+               --  compilation unit.
+
                Freeze_All (First_Entity (Current_Scope), Decl);
                Freeze_From := Last_Entity (Current_Scope);
 
@@ -2391,16 +2614,7 @@ package body Sem_Ch3 is
             --  pragmas do not appear in the original generic tree.
 
             elsif Serious_Errors_Detected = 0 then
-               declare
-                  E : Entity_Id;
-
-               begin
-                  E := First_Entity (Current_Scope);
-                  while Present (E) loop
-                     Resolve_Aspect_Expressions (E);
-                     Next_Entity (E);
-                  end loop;
-               end;
+               Resolve_Aspects;
             end if;
 
          --  If next node is a body then freeze all types before the body.
@@ -2420,49 +2634,97 @@ package body Sem_Ch3 is
 
          elsif not Analyzed (Next_Decl) and then Is_Body (Next_Decl) then
 
-            --  When a controlled type is frozen, the expander generates stream
-            --  and controlled type support routines. If the freeze is caused
-            --  by the stand alone body of Initialize, Adjust and Finalize, the
-            --  expander will end up using the wrong version of these routines
-            --  as the body has not been processed yet. To remedy this, detect
-            --  a late controlled primitive and create a proper spec for it.
-            --  This ensures that the primitive will override its inherited
-            --  counterpart before the freeze takes place.
+            --  Check for an edge case that may cause premature freezing of
+            --  a private type. If there is a type which depends on another
+            --  private type from an enclosing package that is in the same
+            --  scope as a non-completing expression function then we cannot
+            --  freeze here.
 
-            --  If the declaration we just processed is a body, do not attempt
-            --  to examine Next_Decl as the late primitive idiom can only apply
-            --  to the first encountered body.
+            Ignore_Freezing := False;
 
-            --  The spec of the late primitive is not generated in ASIS mode to
-            --  ensure a consistent list of primitives that indicates the true
-            --  semantic structure of the program (which is not relevant when
-            --  generating executable code.
+            if Nkind (Next_Decl) = N_Subprogram_Body
+              and then Was_Expression_Function (Next_Decl)
+              and then not Is_Compilation_Unit (Current_Scope)
+              and then not Is_Generic_Instance (Current_Scope)
+            then
+               --  Loop through all entities in the current scope to identify
+               --  an instance of the edge case outlined above and ignore
+               --  freezing if it is detected.
 
-            --  ??? a cleaner approach may be possible and/or this solution
-            --  could be extended to general-purpose late primitives, TBD.
+               declare
+                  Curr : Entity_Id := First_Entity (Current_Scope);
+               begin
+                  loop
+                     if Nkind (Curr) in N_Entity
+                       and then Depends_On_Private (Curr)
+                     then
+                        Ignore_Freezing := True;
+                        exit;
+                     end if;
 
-            if not ASIS_Mode and then not Body_Seen and then not Is_Body (Decl)
-            then
-               Body_Seen := True;
+                     exit when Last_Entity (Current_Scope) = Curr;
+                     Curr := Next_Entity (Curr);
+                  end loop;
+               end;
+            end if;
 
-               if Nkind (Next_Decl) = N_Subprogram_Body then
-                  Handle_Late_Controlled_Primitive (Next_Decl);
+            if not Ignore_Freezing then
+
+               --  When a controlled type is frozen, the expander generates
+               --  stream and controlled-type support routines. If the freeze
+               --  is caused by the stand-alone body of Initialize, Adjust, or
+               --  Finalize, the expander will end up using the wrong version
+               --  of these routines, as the body has not been processed yet.
+               --  To remedy this, detect a late controlled primitive and
+               --  create a proper spec for it. This ensures that the primitive
+               --  will override its inherited counterpart before the freeze
+               --  takes place.
+
+               --  If the declaration we just processed is a body, do not
+               --  attempt to examine Next_Decl as the late primitive idiom can
+               --  only apply to the first encountered body.
+
+               --  The spec of the late primitive is not generated in ASIS mode
+               --  to ensure a consistent list of primitives that indicates the
+               --  true semantic structure of the program (which is not
+               --  relevant when generating executable code).
+
+               --  ??? A cleaner approach may be possible and/or this solution
+               --  could be extended to general-purpose late primitives, TBD.
+
+               if not ASIS_Mode
+                 and then not Body_Seen
+                 and then not Is_Body (Decl)
+               then
+                  Body_Seen := True;
+
+                  if Nkind (Next_Decl) = N_Subprogram_Body then
+                     Handle_Late_Controlled_Primitive (Next_Decl);
+                  end if;
                end if;
-            end if;
 
-            Adjust_Decl;
-            Freeze_All (Freeze_From, Decl);
-            Freeze_From := Last_Entity (Current_Scope);
+               Adjust_Decl;
+
+               --  The generated body of an expression function does not
+               --  freeze, unless it is a completion, in which case only the
+               --  expression itself freezes. This is handled when the body
+               --  itself is analyzed (see Freeze_Expr_Types, sem_ch6.adb).
+
+               Freeze_All (Freeze_From, Decl);
+               Freeze_From := Last_Entity (Current_Scope);
+            end if;
          end if;
 
          Decl := Next_Decl;
       end loop;
 
-      --  Analyze the contracts of packages and their bodies
+      --  Post-freezing actions
 
       if Present (L) then
          Context := Parent (L);
 
+         --  Analyze the contracts of packages and their bodies
+
          if Nkind (Context) = N_Package_Specification then
 
             --  When a package has private declarations, its contract must be
@@ -2473,15 +2735,6 @@ package body Sem_Ch3 is
             if L = Private_Declarations (Context) then
                Analyze_Package_Contract (Defining_Entity (Context));
 
-               --  Build the bodies of the default initial condition procedures
-               --  for all types subject to pragma Default_Initial_Condition.
-               --  From a purely Ada stand point, this is a freezing activity,
-               --  however freezing is not available under GNATprove_Mode. To
-               --  accomodate both scenarios, the bodies are build at the end
-               --  of private declaration analysis.
-
-               Build_Default_Init_Cond_Procedure_Bodies (L);
-
             --  Otherwise the contract is analyzed at the end of the visible
             --  declarations.
 
@@ -2512,6 +2765,15 @@ package body Sem_Ch3 is
             --  restore the original state conditions.
 
             Remove_Visible_Refinements (Corresponding_Spec (Context));
+            Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
+
+         elsif Nkind (Context) = N_Package_Declaration then
+
+            --  Partial state refinements are visible up to the end of the
+            --  package spec declarations. Hide the partial state refinements
+            --  from visibility to restore the original state conditions.
+
+            Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
          end if;
 
          --  Verify that all abstract states found in any package declared in
@@ -2520,6 +2782,15 @@ package body Sem_Ch3 is
          --  protected, subprogram, or task body (SPARK RM 7.2.2(3)).
 
          Check_State_Refinements (Context);
+
+         --  Create the subprogram bodies which verify the run-time semantics
+         --  of pragmas Default_Initial_Condition and [Type_]Invariant for all
+         --  types within the current declarative list. This ensures that all
+         --  assertion expressions are preanalyzed and resolved at the end of
+         --  the declarative part. Note that the resolution happens even when
+         --  freezing does not take place.
+
+         Build_Assertion_Bodies (L, Context);
       end if;
    end Analyze_Declarations;
 
@@ -2556,44 +2827,48 @@ package body Sem_Ch3 is
       ----------------------------------
 
       procedure Check_Nonoverridable_Aspects is
-         Prev_Aspects   : constant List_Id :=
-                            Aspect_Specifications (Parent (Def_Id));
-         Par_Type       : Entity_Id;
-
-         function Has_Aspect_Spec
-           (Specs : List_Id;
-            Aspect_Name : Name_Id) return Boolean;
+         function Get_Aspect_Spec
+           (Specs       : List_Id;
+            Aspect_Name : Name_Id) return Node_Id;
          --  Check whether a list of aspect specifications includes an entry
          --  for a specific aspect. The list is either that of a partial or
          --  a full view.
 
          ---------------------
-         -- Has_Aspect_Spec --
+         -- Get_Aspect_Spec --
          ---------------------
 
-         function Has_Aspect_Spec
-           (Specs : List_Id;
-            Aspect_Name : Name_Id) return Boolean
+         function Get_Aspect_Spec
+           (Specs       : List_Id;
+            Aspect_Name : Name_Id) return Node_Id
          is
             Spec : Node_Id;
+
          begin
             Spec := First (Specs);
             while Present (Spec) loop
                if Chars (Identifier (Spec)) = Aspect_Name then
-                  return True;
+                  return Spec;
                end if;
                Next (Spec);
             end loop;
-            return False;
-         end Has_Aspect_Spec;
+
+            return Empty;
+         end Get_Aspect_Spec;
+
+         --  Local variables
+
+         Prev_Aspects   : constant List_Id :=
+                            Aspect_Specifications (Parent (Def_Id));
+         Par_Type       : Entity_Id;
+         Prev_Aspect    : Node_Id;
 
       --  Start of processing for Check_Nonoverridable_Aspects
 
       begin
-
-         --  Get parent type of derived type. Note that Prev is the entity
-         --  in the partial declaration, but its contents are now those of
-         --  full view, while Def_Id reflects the partial view.
+         --  Get parent type of derived type. Note that Prev is the entity in
+         --  the partial declaration, but its contents are now those of full
+         --  view, while Def_Id reflects the partial view.
 
          if Is_Private_Type (Def_Id) then
             Par_Type := Etype (Full_View (Def_Id));
@@ -2609,8 +2884,13 @@ package body Sem_Ch3 is
            and then Present (Discriminant_Specifications (Parent (Prev)))
            and then Present (Get_Reference_Discriminant (Par_Type))
          then
-            if
-              not Has_Aspect_Spec (Prev_Aspects, Name_Implicit_Dereference)
+            Prev_Aspect :=
+              Get_Aspect_Spec (Prev_Aspects, Name_Implicit_Dereference);
+
+            if No (Prev_Aspect)
+              and then Present
+                         (Discriminant_Specifications
+                           (Original_Node (Parent (Prev))))
             then
                Error_Msg_N
                  ("type does not inherit implicit dereference", Prev);
@@ -2620,14 +2900,28 @@ package body Sem_Ch3 is
                --  is consistent with that of the parent.
 
                declare
-                  Par_Discr : constant Entity_Id :=
+                  Par_Discr  : constant Entity_Id :=
                                 Get_Reference_Discriminant (Par_Type);
-                  Cur_Discr : constant Entity_Id :=
+                  Cur_Discr  : constant Entity_Id :=
                                 Get_Reference_Discriminant (Prev);
+
                begin
                   if Corresponding_Discriminant (Cur_Discr) /= Par_Discr then
                      Error_Msg_N ("aspect incosistent with that of parent", N);
                   end if;
+
+                  --  Check that specification in partial view matches the
+                  --  inherited aspect. Compare names directly because aspect
+                  --  expression may not be analyzed.
+
+                  if Present (Prev_Aspect)
+                    and then Nkind (Expression (Prev_Aspect)) = N_Identifier
+                    and then Chars (Expression (Prev_Aspect)) /=
+                               Chars (Cur_Discr)
+                  then
+                     Error_Msg_N
+                       ("aspect incosistent with that of parent", N);
+                  end if;
                end;
             end if;
          end if;
@@ -2809,7 +3103,6 @@ package body Sem_Ch3 is
 
             when others =>
                raise Program_Error;
-
          end case;
       end if;
 
@@ -2823,13 +3116,6 @@ package body Sem_Ch3 is
          Check_SPARK_05_Restriction ("controlled type is not allowed", N);
       end if;
 
-      --  A type declared within a Ghost region is automatically Ghost
-      --  (SPARK RM 6.9(2)).
-
-      if Ghost_Mode > None then
-         Set_Is_Ghost_Entity (T);
-      end if;
-
       --  Some common processing for all types
 
       Set_Depends_On_Private (T, Has_Private_Component (T));
@@ -2989,13 +3275,6 @@ package body Sem_Ch3 is
       Set_Is_First_Subtype (T, True);
       Set_Etype (T, T);
 
-      --  An incomplete type declared within a Ghost region is automatically
-      --  Ghost (SPARK RM 6.9(2)).
-
-      if Ghost_Mode > None then
-         Set_Is_Ghost_Entity (T);
-      end if;
-
       --  Ada 2005 (AI-326): Minimum decoration to give support to tagged
       --  incomplete types.
 
@@ -3103,13 +3382,6 @@ package body Sem_Ch3 is
       Generate_Definition (Id);
       Enter_Name (Id);
 
-      --  A number declared within a Ghost region is automatically Ghost
-      --  (SPARK RM 6.9(2)).
-
-      if Ghost_Mode > None then
-         Set_Is_Ghost_Entity (Id);
-      end if;
-
       --  This is an optimization of a common case of an integer literal
 
       if Nkind (E) = N_Integer_Literal then
@@ -3241,6 +3513,10 @@ package body Sem_Ch3 is
    -- Analyze_Object_Declaration --
    --------------------------------
 
+   --  WARNING: This routine manages Ghost regions. Return statements must be
+   --  replaced by gotos which jump to the end of the routine and restore the
+   --  Ghost mode.
+
    procedure Analyze_Object_Declaration (N : Node_Id) is
       Loc   : constant Source_Ptr := Sloc (N);
       Id    : constant Entity_Id  := Defining_Identifier (N);
@@ -3352,8 +3628,9 @@ package body Sem_Ch3 is
 
       --  Local variables
 
-      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-      Related_Id      : Entity_Id;
+      Mode       : Ghost_Mode_Type;
+      Mode_Set   : Boolean := False;
+      Related_Id : Entity_Id;
 
    --  Start of processing for Analyze_Object_Declaration
 
@@ -3402,20 +3679,30 @@ package body Sem_Ch3 is
                                                N_Package_Renaming_Declaration
                    and then not Comes_From_Source (Prev_Entity)
                    and then
-                     Is_Generic_Instance (Renamed_Entity (Prev_Entity))))
+                     Is_Generic_Instance (Renamed_Entity (Prev_Entity)))
+
+               --  The entity may be a homonym of a private component of the
+               --  enclosing protected object, for which we create a local
+               --  renaming declaration. The declaration is legal, even if
+               --  useless when it just captures that component.
+
+               or else
+                 (Ekind (Scope (Current_Scope)) = E_Protected_Type
+                   and then Nkind (Parent (Prev_Entity)) =
+                              N_Object_Renaming_Declaration))
          then
             Prev_Entity := Empty;
          end if;
       end if;
 
-      --  The object declaration is Ghost when it is subject to pragma Ghost or
-      --  completes a deferred Ghost constant. Set the mode now to ensure that
-      --  any nodes generated during analysis and expansion are properly marked
-      --  as Ghost.
+      if Present (Prev_Entity) then
 
-      Set_Ghost_Mode (N, Prev_Entity);
+         --  The object declaration is Ghost when it completes a deferred Ghost
+         --  constant.
+
+         Mark_And_Set_Ghost_Completion (N, Prev_Entity, Mode);
+         Mode_Set := True;
 
-      if Present (Prev_Entity) then
          Constant_Redeclaration (Id, N, T);
 
          Generate_Reference (Prev_Entity, Id, 'c');
@@ -3466,7 +3753,7 @@ package body Sem_Ch3 is
 
          --  In case of aggregates we must also take care of the correct
          --  initialization of nested aggregates bug this is done at the
-         --  point of the analysis of the aggregate (see sem_aggr.adb).
+         --  point of the analysis of the aggregate (see sem_aggr.adb) ???
 
          if Present (Expression (N))
            and then Nkind (Expression (N)) = N_Aggregate
@@ -3581,6 +3868,12 @@ package body Sem_Ch3 is
          end if;
       end if;
 
+      --  Check for violation of No_Local_Timing_Events
+
+      if Has_Timing_Event (T) and then not Is_Library_Level_Entity (Id) then
+         Check_Restriction (No_Local_Timing_Events, Id);
+      end if;
+
       --  The actual subtype of the object is the nominal subtype, unless
       --  the nominal one is unconstrained and obtained from the expression.
 
@@ -3703,8 +3996,7 @@ package body Sem_Ch3 is
            and then Analyzed (N)
            and then No (Expression (N))
          then
-            Ghost_Mode := Save_Ghost_Mode;
-            return;
+            goto Leave;
          end if;
 
          --  If E is null and has been replaced by an N_Raise_Constraint_Error
@@ -3792,8 +4084,8 @@ package body Sem_Ch3 is
            and then Is_EVF_Expression (E)
          then
             Error_Msg_N
-              ("formal parameter with Extensions_Visible False cannot be "
-               & "implicitly converted to class-wide type", E);
+              ("formal parameter cannot be implicitly converted to "
+               & "class-wide type when Extensions_Visible is False", E);
          end if;
       end if;
 
@@ -3962,23 +4254,6 @@ package body Sem_Ch3 is
                   Set_Ekind (Id, E_Variable);
                end if;
 
-               --  An object declared within a Ghost region is automatically
-               --  Ghost (SPARK RM 6.9(2)).
-
-               if Ghost_Mode > None then
-                  Set_Is_Ghost_Entity (Id);
-
-                  --  The Ghost policy in effect at the point of declaration
-                  --  and at the point of completion must match
-                  --  (SPARK RM 6.9(14)).
-
-                  if Present (Prev_Entity)
-                    and then Is_Ghost_Entity (Prev_Entity)
-                  then
-                     Check_Ghost_Completion (Prev_Entity, Id);
-                  end if;
-               end if;
-
                Rewrite (N,
                  Make_Object_Renaming_Declaration (Loc,
                    Defining_Identifier => Id,
@@ -3988,9 +4263,7 @@ package body Sem_Ch3 is
                Set_Renamed_Object (Id, E);
                Freeze_Before (N, T);
                Set_Is_Frozen (Id);
-
-               Ghost_Mode := Save_Ghost_Mode;
-               return;
+               goto Leave;
 
             else
                --  Ensure that the generated subtype has a unique external name
@@ -4027,7 +4300,10 @@ package body Sem_Ch3 is
 
       elsif Is_Array_Type (T)
         and then No_Initialization (N)
-        and then Nkind (Original_Node (E)) = N_Aggregate
+        and then (Nkind (Original_Node (E)) = N_Aggregate
+                   or else (Nkind (Original_Node (E)) = N_Qualified_Expression
+                             and then Nkind (Original_Node (Expression
+                                        (Original_Node (E)))) = N_Aggregate))
       then
          if not Is_Entity_Name (Object_Definition (N)) then
             Act_T := Etype (E);
@@ -4057,9 +4333,10 @@ package body Sem_Ch3 is
 
          elsif Nkind (E) = N_Aggregate
            and then Present (Component_Associations (E))
-           and then Present (Choices (First (Component_Associations (E))))
-           and then Nkind (First
-            (Choices (First (Component_Associations (E))))) = N_Others_Choice
+           and then Present (Choice_List (First (Component_Associations (E))))
+           and then
+             Nkind (First (Choice_List (First (Component_Associations (E))))) =
+               N_Others_Choice
          then
             null;
 
@@ -4161,22 +4438,6 @@ package body Sem_Ch3 is
       Init_Esize                   (Id);
       Set_Optimize_Alignment_Flags (Id);
 
-      --  An object declared within a Ghost region is automatically Ghost
-      --  (SPARK RM 6.9(2)).
-
-      if Ghost_Mode > None
-        or else (Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity))
-      then
-         Set_Is_Ghost_Entity (Id);
-
-         --  The Ghost policy in effect at the point of declaration and at the
-         --  point of completion must match (SPARK RM 6.9(14)).
-
-         if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then
-            Check_Ghost_Completion (Prev_Entity, Id);
-         end if;
-      end if;
-
       --  Deal with aliased case
 
       if Aliased_Present (N) then
@@ -4311,7 +4572,7 @@ package body Sem_Ch3 is
       --  type, rewrite the declaration as a renaming of the result of the
       --  call. The exceptions below are cases where the copy is expected,
       --  either by the back end (Aliased case) or by the semantics, as for
-      --  initializing controlled types or copying tags for classwide types.
+      --  initializing controlled types or copying tags for class-wide types.
 
       if Present (E)
         and then Nkind (E) = N_Explicit_Dereference
@@ -4358,15 +4619,6 @@ package body Sem_Ch3 is
          Set_In_Private_Part (Id);
       end if;
 
-      --  Check for violation of No_Local_Timing_Events
-
-      if Restriction_Check_Required (No_Local_Timing_Events)
-        and then not Is_Library_Level_Entity (Id)
-        and then Is_RTE (Etype (Id), RE_Timing_Event)
-      then
-         Check_Restriction (No_Local_Timing_Events, N);
-      end if;
-
    <<Leave>>
       --  Initialize the refined state of a variable here because this is a
       --  common destination for legal and illegal object declarations.
@@ -4388,7 +4640,9 @@ package body Sem_Ch3 is
          Check_No_Hidden_State (Id);
       end if;
 
-      Ghost_Mode := Save_Ghost_Mode;
+      if Mode_Set then
+         Restore_Ghost_Mode (Mode);
+      end if;
    end Analyze_Object_Declaration;
 
    ---------------------------
@@ -4411,6 +4665,8 @@ package body Sem_Ch3 is
    procedure Analyze_Private_Extension_Declaration (N : Node_Id) is
       Indic       : constant Node_Id   := Subtype_Indication (N);
       T           : constant Entity_Id := Defining_Identifier (N);
+      Iface       : Entity_Id;
+      Iface_Elmt  : Elmt_Id;
       Parent_Base : Entity_Id;
       Parent_Type : Entity_Id;
 
@@ -4476,8 +4732,8 @@ package body Sem_Ch3 is
 
       elsif Is_Concurrent_Type (Parent_Type) then
          Error_Msg_N
-           ("parent type of a private extension cannot be "
-            & "a synchronized tagged type (RM 3.9.1 (3/1))", N);
+           ("parent type of a private extension cannot be a synchronized "
+            & "tagged type (RM 3.9.1 (3/1))", N);
 
          Set_Etype              (T, Any_Type);
          Set_Ekind              (T, E_Limited_Private_Type);
@@ -4498,7 +4754,6 @@ package body Sem_Ch3 is
       if (not Is_Package_Or_Generic_Package (Current_Scope)
            and then Nkind (Parent (N)) /= N_Generic_Subprogram_Declaration)
         or else In_Private_Part (Current_Scope)
-
       then
          Error_Msg_N ("invalid context for private extension", N);
       end if;
@@ -4511,9 +4766,8 @@ package body Sem_Ch3 is
       Init_Size_Align      (T);
       Set_Default_SSO      (T);
 
-      Set_Etype            (T,            Parent_Base);
-      Set_Has_Task         (T, Has_Task  (Parent_Base));
-      Set_Has_Protected    (T, Has_Task  (Parent_Base));
+      Set_Etype            (T,                Parent_Base);
+      Propagate_Concurrent_Flags (T, Parent_Base);
 
       Set_Convention       (T, Convention     (Parent_Type));
       Set_First_Rep_Item   (T, First_Rep_Item (Parent_Type));
@@ -4526,13 +4780,35 @@ package body Sem_Ch3 is
 
       Build_Derived_Record_Type (N, Parent_Type, T);
 
-      --  Propagate inherited invariant information. The new type has
-      --  invariants, if the parent type has inheritable invariants,
-      --  and these invariants can in turn be inherited.
+      --  A private extension inherits the Default_Initial_Condition pragma
+      --  coming from any parent type within the derivation chain.
 
-      if Has_Inheritable_Invariants (Parent_Type) then
-         Set_Has_Inheritable_Invariants (T);
-         Set_Has_Invariants (T);
+      if Has_DIC (Parent_Type) then
+         Set_Has_Inherited_DIC (T);
+      end if;
+
+      --  A private extension inherits any class-wide invariants coming from a
+      --  parent type or an interface. Note that the invariant procedure of the
+      --  parent type should not be inherited because the private extension may
+      --  define invariants of its own.
+
+      if Has_Inherited_Invariants (Parent_Type)
+        or else Has_Inheritable_Invariants (Parent_Type)
+      then
+         Set_Has_Inherited_Invariants (T);
+
+      elsif Present (Interfaces (T)) then
+         Iface_Elmt := First_Elmt (Interfaces (T));
+         while Present (Iface_Elmt) loop
+            Iface := Node (Iface_Elmt);
+
+            if Has_Inheritable_Invariants (Iface) then
+               Set_Has_Inherited_Invariants (T);
+               exit;
+            end if;
+
+            Next_Elmt (Iface_Elmt);
+         end loop;
       end if;
 
       --  Ada 2005 (AI-443): Synchronized private extension or a rewritten
@@ -4554,33 +4830,29 @@ package body Sem_Ch3 is
                 (not Is_Interface (Parent_Type)
                   or else not Is_Synchronized_Interface (Parent_Type))
             then
-               Error_Msg_NE ("parent type of & must be tagged limited " &
-                             "or synchronized", N, T);
+               Error_Msg_NE
+                 ("parent type of & must be tagged limited or synchronized",
+                  N, T);
             end if;
 
             --  The progenitors (if any) must be limited or synchronized
             --  interfaces.
 
             if Present (Interfaces (T)) then
-               declare
-                  Iface      : Entity_Id;
-                  Iface_Elmt : Elmt_Id;
-
-               begin
-                  Iface_Elmt := First_Elmt (Interfaces (T));
-                  while Present (Iface_Elmt) loop
-                     Iface := Node (Iface_Elmt);
+               Iface_Elmt := First_Elmt (Interfaces (T));
+               while Present (Iface_Elmt) loop
+                  Iface := Node (Iface_Elmt);
 
-                     if not Is_Limited_Interface (Iface)
-                       and then not Is_Synchronized_Interface (Iface)
-                     then
-                        Error_Msg_NE ("progenitor & must be limited " &
-                                      "or synchronized", N, Iface);
-                     end if;
+                  if not Is_Limited_Interface (Iface)
+                    and then not Is_Synchronized_Interface (Iface)
+                  then
+                     Error_Msg_NE
+                       ("progenitor & must be limited or synchronized",
+                        N, Iface);
+                  end if;
 
-                     Next_Elmt (Iface_Elmt);
-                  end loop;
-               end;
+                  Next_Elmt (Iface_Elmt);
+               end loop;
             end if;
 
          --  Regular derived extension, the parent must be a limited or
@@ -4719,6 +4991,24 @@ package body Sem_Ch3 is
       then
          Set_Has_Predicates (Id);
          Set_Has_Delayed_Freeze (Id);
+
+         --  Generated subtypes inherit the predicate function from the parent
+         --  (no aspects to examine on the generated declaration).
+
+         if not Comes_From_Source (N) then
+            Set_Ekind (Id, Ekind (T));
+
+            if Present (Predicate_Function (T)) then
+               Set_Predicate_Function (Id, Predicate_Function (T));
+
+            elsif Present (Ancestor_Subtype (T))
+              and then Has_Predicates (Ancestor_Subtype (T))
+              and then Present (Predicate_Function (Ancestor_Subtype (T)))
+            then
+               Set_Predicate_Function (Id,
+                 Predicate_Function (Ancestor_Subtype (T)));
+            end if;
+         end if;
       end if;
 
       --  Subtype of Boolean cannot have a constraint in SPARK
@@ -4790,8 +5080,8 @@ package body Sem_Ch3 is
 
          case Ekind (T) is
             when Array_Kind =>
-               Set_Ekind                       (Id, E_Array_Subtype);
-               Copy_Array_Subtype_Attributes   (Id, T);
+               Set_Ekind                     (Id, E_Array_Subtype);
+               Copy_Array_Subtype_Attributes (Id, T);
 
             when Decimal_Fixed_Point_Kind =>
                Set_Ekind                (Id, E_Decimal_Fixed_Point_Subtype);
@@ -4863,7 +5153,9 @@ package body Sem_Ch3 is
                   Set_Equivalent_Type   (Id, Equivalent_Type    (T));
                end if;
 
-            when E_Record_Type | E_Record_Subtype =>
+            when E_Record_Subtype
+               | E_Record_Type
+            =>
                Set_Ekind                (Id, E_Record_Subtype);
 
                if Ekind (T) = E_Record_Subtype
@@ -5018,7 +5310,7 @@ package body Sem_Ch3 is
                   Set_Stored_Constraint_From_Discriminant_Constraint (Id);
                end if;
 
-            when Incomplete_Kind  =>
+            when Incomplete_Kind =>
                if Ada_Version >= Ada_2005 then
 
                   --  In Ada 2005 an incomplete type can be explicitly tagged:
@@ -5091,10 +5383,9 @@ package body Sem_Ch3 is
 
       if Has_Predicates (T)
         and then Present (Predicate_Function (T))
-
-         and then
-           ((In_Instance and then not Comes_From_Source (N))
-              or else No (Aspect_Specifications (N)))
+        and then
+          ((In_Instance and then not Comes_From_Source (N))
+             or else No (Aspect_Specifications (N)))
       then
          Set_Subprograms_For_Type (Id, Subprograms_For_Type (T));
 
@@ -5165,9 +5456,9 @@ package body Sem_Ch3 is
 
       if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
          if Is_Scalar_Type (Etype (Id))
-            and then Scalar_Range (Id) /=
-                     Scalar_Range (Etype (Subtype_Mark
-                                           (Subtype_Indication (N))))
+           and then Scalar_Range (Id) /=
+                    Scalar_Range
+                      (Etype (Subtype_Mark (Subtype_Indication (N))))
          then
             Apply_Range_Check
               (Scalar_Range (Id),
@@ -5238,28 +5529,6 @@ package body Sem_Ch3 is
          end if;
       end if;
 
-      --  A type invariant applies to any subtype in its scope, in particular
-      --  to a generic actual.
-
-      if Has_Invariants (T) and then In_Open_Scopes (Scope (T)) then
-         Set_Has_Invariants (Id);
-         Set_Invariant_Procedure (Id, Invariant_Procedure (T));
-      end if;
-
-      --  Make sure that generic actual types are properly frozen. The subtype
-      --  is marked as a generic actual type when the enclosing instance is
-      --  analyzed, so here we identify the subtype from the tree structure.
-
-      if Expander_Active
-        and then Is_Generic_Actual_Type (Id)
-        and then In_Instance
-        and then not Comes_From_Source (N)
-        and then Nkind (Subtype_Indication (N)) /= N_Subtype_Indication
-        and then Is_Frozen (T)
-      then
-         Freeze_Before (N, Id);
-      end if;
-
       Set_Optimize_Alignment_Flags (Id);
       Check_Eliminated (Id);
 
@@ -5395,13 +5664,13 @@ package body Sem_Ch3 is
    procedure Array_Type_Declaration (T : in out Entity_Id; Def : Node_Id) is
       Component_Def : constant Node_Id := Component_Definition (Def);
       Component_Typ : constant Node_Id := Subtype_Indication (Component_Def);
+      P             : constant Node_Id := Parent (Def);
       Element_Type  : Entity_Id;
       Implicit_Base : Entity_Id;
       Index         : Node_Id;
-      Related_Id    : Entity_Id := Empty;
       Nb_Index      : Nat;
-      P             : constant Node_Id := Parent (Def);
       Priv          : Entity_Id;
+      Related_Id    : Entity_Id := Empty;
 
    begin
       if Nkind (Def) = N_Constrained_Array_Definition then
@@ -5457,8 +5726,8 @@ package body Sem_Ch3 is
          then
             declare
                Loc   : constant Source_Ptr := Sloc (Def);
-               New_E : Entity_Id;
                Decl  : Entity_Id;
+               New_E : Entity_Id;
 
             begin
                New_E := Make_Temporary (Loc, 'T');
@@ -5584,23 +5853,20 @@ package body Sem_Ch3 is
 
          --  Complete setup of implicit base type
 
-         Set_First_Index       (Implicit_Base, First_Index (T));
-         Set_Component_Type    (Implicit_Base, Element_Type);
-         Set_Has_Task          (Implicit_Base, Has_Task (Element_Type));
-         Set_Has_Protected     (Implicit_Base, Has_Protected (Element_Type));
-         Set_Component_Size    (Implicit_Base, Uint_0);
-         Set_Packed_Array_Impl_Type (Implicit_Base, Empty);
-         Set_Has_Controlled_Component (Implicit_Base,
-           Has_Controlled_Component (Element_Type)
-             or else Is_Controlled_Active  (Element_Type));
-         Set_Finalize_Storage_Only (Implicit_Base,
-           Finalize_Storage_Only (Element_Type));
-
-         --  Inherit the "ghostness" from the constrained array type
+         Set_Component_Size (Implicit_Base, Uint_0);
+         Set_Component_Type (Implicit_Base, Element_Type);
+         Set_Finalize_Storage_Only
+                            (Implicit_Base,
+                              Finalize_Storage_Only (Element_Type));
+         Set_First_Index    (Implicit_Base, First_Index (T));
+         Set_Has_Controlled_Component
+                            (Implicit_Base,
+                              Has_Controlled_Component (Element_Type)
+                                or else Is_Controlled_Active  (Element_Type));
+         Set_Packed_Array_Impl_Type
+                            (Implicit_Base, Empty);
 
-         if Ghost_Mode > None or else Is_Ghost_Entity (T) then
-            Set_Is_Ghost_Entity (Implicit_Base);
-         end if;
+         Propagate_Concurrent_Flags (Implicit_Base, Element_Type);
 
       --  Unconstrained array case
 
@@ -5613,8 +5879,7 @@ package body Sem_Ch3 is
          Set_Is_Constrained           (T, False);
          Set_First_Index              (T, First (Subtype_Marks (Def)));
          Set_Has_Delayed_Freeze       (T, True);
-         Set_Has_Task                 (T, Has_Task      (Element_Type));
-         Set_Has_Protected            (T, Has_Protected (Element_Type));
+         Propagate_Concurrent_Flags   (T, Element_Type);
          Set_Has_Controlled_Component (T, Has_Controlled_Component
                                                         (Element_Type)
                                             or else
@@ -5756,9 +6021,10 @@ package body Sem_Ch3 is
       Set_Is_Internal (Anon);
 
       case Nkind (N) is
-         when N_Component_Declaration       |
-           N_Unconstrained_Array_Definition |
-           N_Constrained_Array_Definition   =>
+         when N_Constrained_Array_Definition
+            | N_Component_Declaration
+            | N_Unconstrained_Array_Definition
+         =>
             Comp := Component_Definition (N);
             Acc  := Access_Definition (Comp);
 
@@ -5851,15 +6117,20 @@ package body Sem_Ch3 is
       end if;
 
       --  Insert the new declaration in the nearest enclosing scope. If the
-      --  node is a body and N is its return type, the declaration belongs in
-      --  the enclosing scope.
+      --  parent is a body and N is its return type, the declaration belongs
+      --  in the enclosing scope. Likewise if N is the type of a parameter.
 
       P := Parent (N);
 
-      if Nkind (P) = N_Subprogram_Body
-        and then Nkind (N) = N_Function_Specification
+      if Nkind (N) = N_Function_Specification
+        and then Nkind (P) = N_Subprogram_Body
       then
          P := Parent (P);
+      elsif Nkind (N) = N_Parameter_Specification
+        and then Nkind (P) in N_Subprogram_Specification
+        and then Nkind (Parent (P)) = N_Subprogram_Body
+      then
+         P := Parent (Parent (P));
       end if;
 
       while Present (P) and then not Has_Declarations (P) loop
@@ -5974,6 +6245,11 @@ package body Sem_Ch3 is
          begin
             Copy_Node (Pbase, Ibase);
 
+            --  Restore Itype status after Copy_Node
+
+            Set_Is_Itype (Ibase);
+            Set_Associated_Node_For_Itype (Ibase, N);
+
             Set_Chars             (Ibase, Svg_Chars);
             Set_Next_Entity       (Ibase, Svg_Next_E);
             Set_Sloc              (Ibase, Sloc (Derived_Type));
@@ -6070,12 +6346,6 @@ package body Sem_Ch3 is
          Copy_Array_Base_Type_Attributes (Implicit_Base, Parent_Base);
 
          Set_Has_Delayed_Freeze (Implicit_Base, True);
-
-         --  Inherit the "ghostness" from the parent base type
-
-         if Ghost_Mode > None or else Is_Ghost_Entity (Parent_Base) then
-            Set_Is_Ghost_Entity (Implicit_Base);
-         end if;
       end Make_Implicit_Base;
 
    --  Start of processing for Build_Derived_Array_Type
@@ -6654,8 +6924,12 @@ package body Sem_Ch3 is
          --  If we constructed a default range for the case where no range
          --  was given, then the expressions in the range must not freeze
          --  since they do not correspond to expressions in the source.
+         --  However, if the type inherits predicates the expressions will
+         --  be elaborated earlier and must freeze.
 
-         if Nkind (Indic) /= N_Subtype_Indication then
+         if Nkind (Indic) /= N_Subtype_Indication
+           and then not Has_Predicates (Derived_Type)
+         then
             Set_Must_Not_Freeze (Lo);
             Set_Must_Not_Freeze (Hi);
             Set_Must_Not_Freeze (Rang_Expr);
@@ -7239,6 +7513,7 @@ package body Sem_Ch3 is
                   Set_Full_View (Derived_Type, Full_Der);
                else
                   Set_Underlying_Full_View (Derived_Type, Full_Der);
+                  Set_Is_Underlying_Full_View (Full_Der);
                end if;
 
                if not Is_Base_Type (Derived_Type) then
@@ -7296,6 +7571,7 @@ package body Sem_Ch3 is
             Set_Full_View (Derived_Type, Full_Der);
          else
             Set_Underlying_Full_View (Derived_Type, Full_Der);
+            Set_Is_Underlying_Full_View (Full_Der);
          end if;
 
          --  In any case, the primitive operations are inherited from the
@@ -7402,6 +7678,7 @@ package body Sem_Ch3 is
             else
                Build_Full_Derivation;
                Set_Underlying_Full_View (Derived_Type, Full_Der);
+               Set_Is_Underlying_Full_View (Full_Der);
             end if;
 
             --  The full view will be used to swap entities on entry/exit to
@@ -8729,36 +9006,6 @@ package body Sem_Ch3 is
                   end;
                end if;
 
-               --  Propagate inherited invariant information of parents
-               --  and progenitors
-
-               if Ada_Version >= Ada_2012
-                 and then not Is_Interface (Derived_Type)
-               then
-                  if Has_Inheritable_Invariants (Parent_Type) then
-                     Set_Has_Invariants (Derived_Type);
-                     Set_Has_Inheritable_Invariants (Derived_Type);
-
-                  elsif not Is_Empty_Elmt_List (Ifaces_List) then
-                     declare
-                        AI : Elmt_Id;
-
-                     begin
-                        AI := First_Elmt (Ifaces_List);
-                        while Present (AI) loop
-                           if Has_Inheritable_Invariants (Node (AI)) then
-                              Set_Has_Invariants (Derived_Type);
-                              Set_Has_Inheritable_Invariants (Derived_Type);
-
-                              exit;
-                           end if;
-
-                           Next_Elmt (AI);
-                        end loop;
-                     end;
-                  end if;
-               end if;
-
                --  A type extension is automatically Ghost when one of its
                --  progenitors is Ghost (SPARK RM 6.9(9)). This property is
                --  also inherited when the parent type is Ghost, but this is
@@ -8795,6 +9042,9 @@ package body Sem_Ch3 is
 
       --  STEP 5a: Copy the parent record declaration for untagged types
 
+      Set_Has_Implicit_Dereference
+        (Derived_Type, Has_Implicit_Dereference (Parent_Type));
+
       if not Is_Tagged then
 
          --  Discriminant_Constraint (Derived_Type) has been properly
@@ -8837,8 +9087,6 @@ package body Sem_Ch3 is
             Set_Stored_Constraint
               (Derived_Type, Expand_To_Stored_Constraint (Parent_Type, Discs));
             Replace_Components (Derived_Type, New_Decl);
-            Set_Has_Implicit_Dereference
-              (Derived_Type, Has_Implicit_Dereference (Parent_Type));
          end if;
 
          --  Insert the new derived type declaration
@@ -8951,12 +9199,11 @@ package body Sem_Ch3 is
    begin
       --  Set common attributes
 
-      Set_Scope              (Derived_Type, Current_Scope);
+      Set_Scope                (Derived_Type, Current_Scope);
 
-      Set_Etype              (Derived_Type,                Parent_Base);
-      Set_Ekind              (Derived_Type, Ekind         (Parent_Base));
-      Set_Has_Task           (Derived_Type, Has_Task      (Parent_Base));
-      Set_Has_Protected      (Derived_Type, Has_Protected (Parent_Base));
+      Set_Etype                  (Derived_Type,        Parent_Base);
+      Set_Ekind                  (Derived_Type, Ekind (Parent_Base));
+      Propagate_Concurrent_Flags (Derived_Type,        Parent_Base);
 
       Set_Size_Info          (Derived_Type,                     Parent_Type);
       Set_RM_Size            (Derived_Type, RM_Size            (Parent_Type));
@@ -8991,13 +9238,62 @@ package body Sem_Ch3 is
          Set_Default_SSO (Derived_Type);
       end if;
 
-      --  Propagate invariant information. The new type has invariants if
-      --  they are inherited from the parent type, and these invariants can
-      --  be further inherited, so both flags are set.
+      --  A derived type inherits the Default_Initial_Condition pragma coming
+      --  from any parent type within the derivation chain.
+
+      if Has_DIC (Parent_Type) then
+         Set_Has_Inherited_DIC (Derived_Type);
+      end if;
+
+      --  A derived type inherits any class-wide invariants coming from a
+      --  parent type or an interface. Note that the invariant procedure of
+      --  the parent type should not be inherited because the derived type may
+      --  define invariants of its own.
+
+      if not Is_Interface (Derived_Type) then
+         if Has_Inherited_Invariants (Parent_Type)
+           or else Has_Inheritable_Invariants (Parent_Type)
+         then
+            Set_Has_Inherited_Invariants (Derived_Type);
+
+         elsif Is_Concurrent_Type (Derived_Type)
+           or else Is_Tagged_Type (Derived_Type)
+         then
+            declare
+               Iface      : Entity_Id;
+               Ifaces     : Elist_Id;
+               Iface_Elmt : Elmt_Id;
+
+            begin
+               Collect_Interfaces
+                 (T               => Derived_Type,
+                  Ifaces_List     => Ifaces,
+                  Exclude_Parents => True);
+
+               if Present (Ifaces) then
+                  Iface_Elmt := First_Elmt (Ifaces);
+                  while Present (Iface_Elmt) loop
+                     Iface := Node (Iface_Elmt);
 
-      --  We similarly inherit predicates
+                     if Has_Inheritable_Invariants (Iface) then
+                        Set_Has_Inherited_Invariants (Derived_Type);
+                        exit;
+                     end if;
 
-      if Has_Predicates (Parent_Type) then
+                     Next_Elmt (Iface_Elmt);
+                  end loop;
+               end if;
+            end;
+         end if;
+      end if;
+
+      --  We similarly inherit predicates. Note that for scalar derived types
+      --  the predicate is inherited from the first subtype, and not from its
+      --  (anonymous) base type.
+
+      if Has_Predicates (Parent_Type)
+        or else Has_Predicates (First_Subtype (Parent_Type))
+      then
          Set_Has_Predicates (Derived_Type);
       end if;
 
@@ -9005,18 +9301,6 @@ package body Sem_Ch3 is
 
       Inherit_Rep_Item_Chain (Derived_Type, Parent_Type);
 
-      --  Propagate the attributes related to pragma Default_Initial_Condition
-      --  from the parent type to the private extension. A derived type always
-      --  inherits the default initial condition flag from the parent type. If
-      --  the derived type carries its own Default_Initial_Condition pragma,
-      --  the flag is later reset in Analyze_Pragma. Note that both flags are
-      --  mutually exclusive.
-
-      Propagate_Default_Init_Cond_Attributes
-        (From_Typ             => Parent_Type,
-         To_Typ               => Derived_Type,
-         Parent_To_Derivation => True);
-
       --  If the parent type has delayed rep aspects, then mark the derived
       --  type as possibly inheriting a delayed rep aspect.
 
@@ -9024,8 +9308,9 @@ package body Sem_Ch3 is
          Set_May_Inherit_Delayed_Rep_Aspects (Derived_Type);
       end if;
 
-      --  Propagate the attributes related to pragma Ghost from the parent type
-      --  to the derived type or type extension (SPARK RM 6.9(9)).
+      --  A derived type becomes Ghost when its parent type is also Ghost
+      --  (SPARK RM 6.9(9)). Note that the Ghost-related attributes are not
+      --  directly inherited because the Ghost policy in effect may differ.
 
       if Is_Ghost_Entity (Parent_Type) then
          Set_Is_Ghost_Entity (Derived_Type);
@@ -9040,9 +9325,10 @@ package body Sem_Ch3 is
          when Array_Kind =>
             Build_Derived_Array_Type (N, Parent_Type,  Derived_Type);
 
-         when E_Record_Type
+         when Class_Wide_Kind
             | E_Record_Subtype
-            | Class_Wide_Kind  =>
+            | E_Record_Type
+         =>
             Build_Derived_Record_Type
               (N, Parent_Type, Derived_Type, Derive_Subps);
             return;
@@ -9112,6 +9398,7 @@ package body Sem_Ch3 is
       Set_Mechanism (D_Minal, Default_Mechanism);
       Set_Etype     (D_Minal, Etype (Discrim));
       Set_Scope     (D_Minal, Current_Scope);
+      Set_Parent    (D_Minal, Parent (Discrim));
 
       Set_Discriminal (Discrim, D_Minal);
       Set_Discriminal_Link (D_Minal, Discrim);
@@ -9418,12 +9705,19 @@ package body Sem_Ch3 is
             --  If any of the discriminant constraints is given by a
             --  discriminant and we are in a derived type declaration we
             --  have a discriminant renaming. Establish link between new
-            --  and old discriminant.
+            --  and old discriminant. The new discriminant has an implicit
+            --  dereference if the old one does.
 
             if Denotes_Discriminant (Discr_Expr (J)) then
                if Derived_Def then
-                  Set_Corresponding_Discriminant
-                    (Entity (Discr_Expr (J)), Discr);
+                  declare
+                     New_Discr : constant Entity_Id := Entity (Discr_Expr (J));
+
+                  begin
+                     Set_Corresponding_Discriminant (New_Discr, Discr);
+                     Set_Has_Implicit_Dereference (New_Discr,
+                       Has_Implicit_Dereference (Discr));
+                  end;
                end if;
 
             --  Force the evaluation of non-discriminant expressions.
@@ -9439,9 +9733,8 @@ package body Sem_Ch3 is
                   null;
 
                elsif Nkind (Parent (Parent (Def))) = N_Component_Declaration
-                 and then
-                   Has_Per_Object_Constraint
-                     (Defining_Identifier (Parent (Parent (Def))))
+                 and then Has_Per_Object_Constraint
+                            (Defining_Identifier (Parent (Parent (Def))))
                then
                   null;
 
@@ -9461,7 +9754,7 @@ package body Sem_Ch3 is
 
             if Ekind (Etype (Discr)) = E_Anonymous_Access_Type
               and then not Is_Class_Wide_Type
-                         (Designated_Type (Etype (Discr)))
+                             (Designated_Type (Etype (Discr)))
               and then Etype (Discr_Expr (J)) /= Any_Type
               and then Is_Class_Wide_Type
                          (Designated_Type (Etype (Discr_Expr (J))))
@@ -9475,7 +9768,7 @@ package body Sem_Ch3 is
             then
                Error_Msg_NE
                  ("constraint for discriminant& must be access to variable",
-                    Def, Discr);
+                  Def, Discr);
             end if;
          end if;
 
@@ -9804,6 +10097,7 @@ package body Sem_Ch3 is
 
       Analyze (Indic);
       Set_Underlying_Full_View (Typ, Full_View (Subt));
+      Set_Is_Underlying_Full_View (Full_View (Subt));
    end Build_Underlying_Full_View;
 
    -------------------------------
@@ -11596,12 +11890,13 @@ package body Sem_Ch3 is
       Save_Homonym     := Homonym (Priv);
 
       case Ekind (Full_Base) is
-         when E_Record_Type    |
-              E_Record_Subtype |
-              Class_Wide_Kind  |
-              Private_Kind     |
-              Task_Kind        |
-              Protected_Kind   =>
+         when Class_Wide_Kind
+            | Private_Kind
+            | Protected_Kind
+            | Task_Kind
+            | E_Record_Subtype
+            | E_Record_Type
+         =>
             Copy_Node (Priv, Full);
 
             Set_Has_Discriminants
@@ -11678,12 +11973,22 @@ package body Sem_Ch3 is
       --  already frozen. We skip this processing if the type is an anonymous
       --  subtype of a record component, or is the corresponding record of a
       --  protected type, since these are processed when the enclosing type
-      --  is frozen.
+      --  is frozen. If the parent type is declared in a nested package then
+      --  the freezing of the private and full views also happens later.
 
       if not Is_Type (Scope (Full)) then
-         Set_Has_Delayed_Freeze (Full,
-           Has_Delayed_Freeze (Full_Base)
-             and then (not Is_Frozen (Full_Base)));
+         if Is_Itype (Priv)
+           and then In_Same_Source_Unit (Full, Full_Base)
+           and then Scope (Full_Base) /= Scope (Full)
+         then
+            Set_Has_Delayed_Freeze (Full);
+            Set_Has_Delayed_Freeze (Priv);
+
+         else
+            Set_Has_Delayed_Freeze (Full,
+              Has_Delayed_Freeze (Full_Base)
+                and then not Is_Frozen (Full_Base));
+         end if;
       end if;
 
       Set_Freeze_Node (Full, Empty);
@@ -11809,9 +12114,11 @@ package body Sem_Ch3 is
          Append    : Boolean;
          Item      : Node_Id;
          Next_Item : Node_Id;
+         Priv_Item : Node_Id;
 
       begin
          Item := First_Rep_Item (Full);
+         Priv_Item := First_Rep_Item (Priv);
 
          --  If no existing rep items on full type, we can just link directly
          --  to the list of items on the private type, if any exist.. Same if
@@ -11820,16 +12127,26 @@ package body Sem_Ch3 is
          if (No (Item)
               or else Nkind (Item) /= N_Aspect_Specification
               or else Entity (Item) = Full_Base)
-             and then Present (First_Rep_Item (Priv))
+           and then Present (First_Rep_Item (Priv))
          then
-            Set_First_Rep_Item (Full, First_Rep_Item (Priv));
+            Set_First_Rep_Item (Full, Priv_Item);
 
          --  Otherwise, search to the end of items currently linked to the full
          --  subtype and append the private items to the end. However, if Priv
          --  and Full already have the same list of rep items, then the append
          --  is not done, as that would create a circularity.
+         --
+         --  The partial view may have a predicate and the rep item lists of
+         --  both views agree when inherited from the same ancestor. In that
+         --  case, simply propagate the list from one view to the other.
+         --  A more complex analysis needed here ???
+
+         elsif Present (Priv_Item)
+           and then Item = Next_Rep_Item (Priv_Item)
+         then
+            Set_First_Rep_Item (Full, Priv_Item);
 
-         elsif Item /= First_Rep_Item (Priv) then
+         elsif Item /= Priv_Item then
             Append := True;
             loop
                Next_Item := Next_Rep_Item (Item);
@@ -13713,8 +14030,7 @@ package body Sem_Ch3 is
       Set_Component_Size           (T1, Component_Size           (T2));
       Set_Has_Controlled_Component (T1, Has_Controlled_Component (T2));
       Set_Has_Non_Standard_Rep     (T1, Has_Non_Standard_Rep     (T2));
-      Set_Has_Protected            (T1, Has_Protected            (T2));
-      Set_Has_Task                 (T1, Has_Task                 (T2));
+      Propagate_Concurrent_Flags   (T1, T2);
       Set_Is_Packed                (T1, Is_Packed                (T2));
       Set_Has_Aliased_Components   (T1, Has_Aliased_Components   (T2));
       Set_Has_Atomic_Components    (T1, Has_Atomic_Components    (T2));
@@ -14033,7 +14349,8 @@ package body Sem_Ch3 is
            Governed_By   => Assoc_List,
            Into          => Comp_List,
            Report_Errors => Errors);
-         pragma Assert (not Errors);
+         pragma Assert (not Errors
+           or else Serious_Errors_Detected > 0);
 
          Create_All_Components;
 
@@ -14421,7 +14738,7 @@ package body Sem_Ch3 is
    -----------------------
 
    procedure Derive_Subprogram
-     (New_Subp     : in out Entity_Id;
+     (New_Subp     : out Entity_Id;
       Parent_Subp  : Entity_Id;
       Derived_Type : Entity_Id;
       Parent_Type  : Entity_Id;
@@ -14660,9 +14977,10 @@ package body Sem_Ch3 is
         or else Is_Internal (Parent_Subp)
         or else Is_Private_Overriding
         or else Is_Internal_Name (Chars (Parent_Subp))
-        or else Nam_In (Chars (Parent_Subp), Name_Initialize,
-                                             Name_Adjust,
-                                             Name_Finalize)
+        or else (Is_Controlled (Parent_Type)
+                  and then Nam_In (Chars (Parent_Subp), Name_Adjust,
+                                                        Name_Finalize,
+                                                        Name_Initialize))
       then
          Set_Derived_Name;
 
@@ -14798,12 +15116,6 @@ package body Sem_Ch3 is
          Set_Alias (New_Subp, Actual_Subp);
       end if;
 
-      --  Inherit the "ghostness" from the parent subprogram
-
-      if Is_Ghost_Entity (Alias (New_Subp)) then
-         Set_Is_Ghost_Entity (New_Subp);
-      end if;
-
       --  Derived subprograms of a tagged type must inherit the convention
       --  of the parent subprogram (a requirement of AI-117). Derived
       --  subprograms of untagged types simply get convention Ada by default.
@@ -15002,7 +15314,7 @@ package body Sem_Ch3 is
       --  the list of primitives of Derived_Type exactly in the same order.
 
       procedure Derive_Interface_Subprogram
-        (New_Subp    : in out Entity_Id;
+        (New_Subp    : out Entity_Id;
          Subp        : Entity_Id;
          Actual_Subp : Entity_Id);
       --  Derive New_Subp from the ultimate alias of the parent subprogram Subp
@@ -15010,6 +15322,10 @@ package body Sem_Ch3 is
       --  Actual_Subp is the actual subprogram corresponding with the generic
       --  subprogram Subp.
 
+      ------------------------
+      -- Check_Derived_Type --
+      ------------------------
+
       function Check_Derived_Type return Boolean is
          E        : Entity_Id;
          Elmt     : Elmt_Id;
@@ -15020,7 +15336,7 @@ package body Sem_Ch3 is
 
       begin
          --  Traverse list of entities in the current scope searching for
-         --  an incomplete type whose full-view is derived type
+         --  an incomplete type whose full-view is derived type.
 
          E := First_Entity (Scope (Derived_Type));
          while Present (E) and then E /= Derived_Type loop
@@ -15088,7 +15404,7 @@ package body Sem_Ch3 is
       ---------------------------------
 
       procedure Derive_Interface_Subprogram
-        (New_Subp    : in out Entity_Id;
+        (New_Subp    : out Entity_Id;
          Subp        : Entity_Id;
          Actual_Subp : Entity_Id)
       is
@@ -16372,63 +16688,93 @@ package body Sem_Ch3 is
 
    function Find_Type_Name (N : Node_Id) return Entity_Id is
       Id       : constant Entity_Id := Defining_Identifier (N);
-      Prev     : Entity_Id;
       New_Id   : Entity_Id;
+      Prev     : Entity_Id;
       Prev_Par : Node_Id;
 
       procedure Check_Duplicate_Aspects;
       --  Check that aspects specified in a completion have not been specified
-      --  already in the partial view. Type_Invariant and others can be
-      --  specified on either view but never on both.
+      --  already in the partial view.
 
       procedure Tag_Mismatch;
-      --  Diagnose a tagged partial view whose full view is untagged.
-      --  We post the message on the full view, with a reference to
-      --  the previous partial view. The partial view can be private
-      --  or incomplete, and these are handled in a different manner,
-      --  so we determine the position of the error message from the
-      --  respective slocs of both.
+      --  Diagnose a tagged partial view whose full view is untagged. We post
+      --  the message on the full view, with a reference to the previous
+      --  partial view. The partial view can be private or incomplete, and
+      --  these are handled in a different manner, so we determine the position
+      --  of the error message from the respective slocs of both.
 
       -----------------------------
       -- Check_Duplicate_Aspects --
       -----------------------------
 
       procedure Check_Duplicate_Aspects is
-         Prev_Aspects   : constant List_Id := Aspect_Specifications (Prev_Par);
-         Full_Aspects   : constant List_Id := Aspect_Specifications (N);
-         F_Spec, P_Spec : Node_Id;
+         function Get_Partial_View_Aspect (Asp : Node_Id) return Node_Id;
+         --  Return the corresponding aspect of the partial view which matches
+         --  the aspect id of Asp. Return Empty is no such aspect exists.
+
+         -----------------------------
+         -- Get_Partial_View_Aspect --
+         -----------------------------
+
+         function Get_Partial_View_Aspect (Asp : Node_Id) return Node_Id is
+            Asp_Id    : constant Aspect_Id := Get_Aspect_Id (Asp);
+            Prev_Asps : constant List_Id   := Aspect_Specifications (Prev_Par);
+            Prev_Asp  : Node_Id;
+
+         begin
+            if Present (Prev_Asps) then
+               Prev_Asp := First (Prev_Asps);
+               while Present (Prev_Asp) loop
+                  if Get_Aspect_Id (Prev_Asp) = Asp_Id then
+                     return Prev_Asp;
+                  end if;
+
+                  Next (Prev_Asp);
+               end loop;
+            end if;
+
+            return Empty;
+         end Get_Partial_View_Aspect;
+
+         --  Local variables
+
+         Full_Asps : constant List_Id := Aspect_Specifications (N);
+         Full_Asp  : Node_Id;
+         Part_Asp  : Node_Id;
+
+      --  Start of processing for Check_Duplicate_Aspects
 
       begin
-         if Present (Full_Aspects) then
-            F_Spec := First (Full_Aspects);
-            while Present (F_Spec) loop
-               if Present (Prev_Aspects) then
-                  P_Spec := First (Prev_Aspects);
-                  while Present (P_Spec) loop
-                     if Chars (Identifier (P_Spec)) =
-                       Chars (Identifier (F_Spec))
-                     then
-                        Error_Msg_N
-                          ("aspect already specified in private declaration",
-                            F_Spec);
-                        Remove (F_Spec);
-                        return;
-                     end if;
+         if Present (Full_Asps) then
+            Full_Asp := First (Full_Asps);
+            while Present (Full_Asp) loop
+               Part_Asp := Get_Partial_View_Aspect (Full_Asp);
 
-                     Next (P_Spec);
-                  end loop;
+               --  An aspect and its class-wide counterpart are two distinct
+               --  aspects and may apply to both views of an entity.
+
+               if Present (Part_Asp)
+                 and then Class_Present (Part_Asp) = Class_Present (Full_Asp)
+               then
+                  Error_Msg_N
+                    ("aspect already specified in private declaration",
+                     Full_Asp);
+
+                  Remove (Full_Asp);
+                  return;
                end if;
 
                if Has_Discriminants (Prev)
                  and then not Has_Unknown_Discriminants (Prev)
-                 and then Chars (Identifier (F_Spec)) =
-                   Name_Implicit_Dereference
+                 and then Get_Aspect_Id (Full_Asp) =
+                            Aspect_Implicit_Dereference
                then
-                  Error_Msg_N ("cannot specify aspect " &
-                    "if partial view has known discriminants", F_Spec);
+                  Error_Msg_N
+                    ("cannot specify aspect if partial view has known "
+                     & "discriminants", Full_Asp);
                end if;
 
-               Next (F_Spec);
+               Next (Full_Asp);
             end loop;
          end if;
       end Check_Duplicate_Aspects;
@@ -16551,9 +16897,9 @@ package body Sem_Ch3 is
                Set_Ekind (Id, Ekind (Prev));         --  will be reset later
                Set_Class_Wide_Type (Id, Class_Wide_Type (Prev));
 
-               --  The type of the classwide type is the current Id. Previously
+               --  Type of the class-wide type is the current Id. Previously
                --  this was not done for private declarations because of order-
-               --  of elaboration issues in the back-end, but gigi now handles
+               --  of-elaboration issues in the back end, but gigi now handles
                --  this properly.
 
                Set_Etype (Class_Wide_Type (Id), Id);
@@ -17853,8 +18199,9 @@ package body Sem_Ch3 is
    is
    begin
       case T_Kind is
-         when Enumeration_Kind |
-              Integer_Kind =>
+         when Enumeration_Kind
+            | Integer_Kind
+         =>
             return Constraint_Kind = N_Range_Constraint;
 
          when Decimal_Fixed_Point_Kind =>
@@ -17869,14 +18216,15 @@ package body Sem_Ch3 is
             return Nkind_In (Constraint_Kind, N_Digits_Constraint,
                                               N_Range_Constraint);
 
-         when Access_Kind       |
-              Array_Kind        |
-              E_Record_Type     |
-              E_Record_Subtype  |
-              Class_Wide_Kind   |
-              E_Incomplete_Type |
-              Private_Kind      |
-              Concurrent_Kind  =>
+         when Access_Kind
+            | Array_Kind
+            | Class_Wide_Kind
+            | Concurrent_Kind
+            | Private_Kind
+            | E_Incomplete_Type
+            | E_Record_Subtype
+            | E_Record_Type
+         =>
             return Constraint_Kind = N_Index_Or_Discriminant_Constraint;
 
          when others =>
@@ -17965,11 +18313,38 @@ package body Sem_Ch3 is
       then
          return True;
 
-      --  In the body of an instantiation, no need to check for the visibility
-      --  of a component.
+      --  In the body of an instantiation, check the visibility of a component
+      --  in case it has a homograph that is a primitive operation of a private
+      --  type which was not visible in the generic unit.
+
+      --  Should Is_Prefixed_Call be propagated from template to instance???
 
       elsif In_Instance_Body then
-         return True;
+         if not Is_Tagged_Type (Original_Type)
+           or else not Is_Private_Type (Original_Type)
+         then
+            return True;
+
+         else
+            declare
+               Subp_Elmt : Elmt_Id;
+
+            begin
+               Subp_Elmt := First_Elmt (Primitive_Operations (Original_Type));
+               while Present (Subp_Elmt) loop
+
+                  --  The component is hidden by a primitive operation
+
+                  if Chars (Node (Subp_Elmt)) = Chars (C) then
+                     return False;
+                  end if;
+
+                  Next_Elmt (Subp_Elmt);
+               end loop;
+
+               return True;
+            end;
+         end if;
 
       --  If the component has been declared in an ancestor which is currently
       --  a private type, then it is not visible. The same applies if the
@@ -18112,7 +18487,8 @@ package body Sem_Ch3 is
       Set_Freeze_Node (CW_Type, Empty);
 
       --  Customize the class-wide type: It has no prim. op., it cannot be
-      --  abstract and its Etype points back to the specific root type.
+      --  abstract, its Etype points back to the specific root type, and it
+      --  cannot have any invariants.
 
       Set_Ekind                       (CW_Type, E_Class_Wide_Type);
       Set_Is_Tagged_Type              (CW_Type, True);
@@ -18121,6 +18497,9 @@ package body Sem_Ch3 is
       Set_Is_Constrained              (CW_Type, False);
       Set_Is_First_Subtype            (CW_Type, Is_First_Subtype (T));
       Set_Default_SSO                 (CW_Type);
+      Set_Has_Inheritable_Invariants  (CW_Type, False);
+      Set_Has_Inherited_Invariants    (CW_Type, False);
+      Set_Has_Own_Invariants          (CW_Type, False);
 
       if Ekind (T) = E_Class_Wide_Subtype then
          Set_Etype (CW_Type, Etype (Base_Type (T)));
@@ -18143,12 +18522,6 @@ package body Sem_Ch3 is
       --  The class-wide type of a class-wide type is itself (RM 3.9(14))
 
       Set_Class_Wide_Type (CW_Type, CW_Type);
-
-      --  Inherit the "ghostness" from the root tagged type
-
-      if Ghost_Mode > None or else Is_Ghost_Entity (T) then
-         Set_Is_Ghost_Entity (CW_Type);
-      end if;
    end Make_Class_Wide_Type;
 
    ----------------
@@ -18656,11 +19029,14 @@ package body Sem_Ch3 is
    is
    begin
       --  An object of a limited interface type can be initialized with any
-      --  expression of a nonlimited descendant type.
+      --  expression of a nonlimited descendant type. However this does not
+      --  apply if this is a view conversion of some other expression. This
+      --  is checked below.
 
       if Is_Class_Wide_Type (Typ)
         and then Is_Limited_Interface (Typ)
         and then not Is_Limited_Type (Etype (Exp))
+        and then Nkind (Exp) /= N_Type_Conversion
       then
          return True;
       end if;
@@ -18684,7 +19060,11 @@ package body Sem_Ch3 is
       end if;
 
       case Nkind (Original_Node (Exp)) is
-         when N_Aggregate | N_Extension_Aggregate | N_Function_Call | N_Op =>
+         when N_Aggregate
+            | N_Extension_Aggregate
+            | N_Function_Call
+            | N_Op
+         =>
             return True;
 
          when N_Identifier =>
@@ -18704,16 +19084,18 @@ package body Sem_Ch3 is
          --  A return statement for a build-in-place function returning a
          --  synchronized type also introduces an unchecked conversion.
 
-         when N_Type_Conversion           |
-              N_Unchecked_Type_Conversion =>
+         when N_Type_Conversion
+            | N_Unchecked_Type_Conversion
+         =>
             return not Comes_From_Source (Exp)
               and then
                 OK_For_Limited_Init_In_05
                   (Typ, Expression (Original_Node (Exp)));
 
-         when N_Indexed_Component     |
-              N_Selected_Component    |
-              N_Explicit_Dereference  =>
+         when N_Explicit_Dereference
+            | N_Indexed_Component
+            | N_Selected_Component
+         =>
             return Nkind (Exp) = N_Function_Call;
 
          --  A use of 'Input is a function call, hence allowed. Normally the
@@ -19284,6 +19666,10 @@ package body Sem_Ch3 is
    -- Process_Full_View --
    -----------------------
 
+   --  WARNING: This routine manages Ghost regions. Return statements must be
+   --  replaced by gotos which jump to the end of the routine and restore the
+   --  Ghost mode.
+
    procedure Process_Full_View (N : Node_Id; Full_T, Priv_T : Entity_Id) is
       procedure Collect_Implemented_Interfaces
         (Typ    : Entity_Id;
@@ -19378,11 +19764,14 @@ package body Sem_Ch3 is
 
       Full_Indic  : Node_Id;
       Full_Parent : Entity_Id;
+      Mode        : Ghost_Mode_Type;
       Priv_Parent : Entity_Id;
 
    --  Start of processing for Process_Full_View
 
    begin
+      Mark_And_Set_Ghost_Completion (N, Priv_T, Mode);
+
       --  First some sanity checks that must be done after semantic
       --  decoration of the full view and thus cannot be placed with other
       --  similar checks in Find_Type_Name
@@ -19495,7 +19884,7 @@ package body Sem_Ch3 is
          --  error situation [7.3(8)].
 
          if Priv_Parent = Any_Type or else Full_Parent = Any_Type then
-            return;
+            goto Leave;
 
          --  Ada 2005 (AI-251): Interfaces in the full type can be given in
          --  any order. Therefore we don't have to check that its parent must
@@ -19515,8 +19904,8 @@ package body Sem_Ch3 is
            and then not Is_Ancestor (Base_Type (Priv_Parent), Full_Parent)
          then
             Error_Msg_N
-              ("parent of full type must descend from parent"
-                  & " of private extension", Full_Indic);
+              ("parent of full type must descend from parent of private "
+               & "extension", Full_Indic);
 
          --  First check a formal restriction, and then proceed with checking
          --  Ada rules. Since the formal restriction is not a serious error, we
@@ -19570,9 +19959,9 @@ package body Sem_Ch3 is
                   while Present (Priv_Discr) and then Present (Full_Discr) loop
                      if Original_Record_Component (Priv_Discr) =
                         Original_Record_Component (Full_Discr)
-                       or else
-                         Corresponding_Discriminant (Priv_Discr) =
-                         Corresponding_Discriminant (Full_Discr)
+                          or else
+                        Corresponding_Discriminant (Priv_Discr) =
+                        Corresponding_Discriminant (Full_Discr)
                      then
                         null;
                      else
@@ -19585,8 +19974,8 @@ package body Sem_Ch3 is
 
                   if Present (Priv_Discr) or else Present (Full_Discr) then
                      Error_Msg_N
-                       ("full view must inherit discriminants of the parent"
-                        & " type used in the private extension", Full_Indic);
+                       ("full view must inherit discriminants of the parent "
+                        & "type used in the private extension", Full_Indic);
 
                   elsif Priv_Constr and then not Full_Constr then
                      Error_Msg_N
@@ -19604,13 +19993,13 @@ package body Sem_Ch3 is
                --  known or unknown discriminants, then the full type
                --  declaration shall define a definite subtype.
 
-            elsif      not Has_Unknown_Discriminants (Priv_T)
+            elsif not Has_Unknown_Discriminants (Priv_T)
               and then not Has_Discriminants (Priv_T)
               and then not Is_Constrained (Full_T)
             then
                Error_Msg_N
-                 ("full view must define a constrained type if partial view"
-                  & " has no discriminants", Full_T);
+                 ("full view must define a constrained type if partial view "
+                  & "has no discriminants", Full_T);
             end if;
 
             --  ??????? Do we implement the following properly ?????
@@ -19828,8 +20217,8 @@ package body Sem_Ch3 is
                                    (Subp_Id => Prim,
                                     Obj_Typ => Conc_Typ,
                                     Formals =>
-                                      Parameter_Specifications (
-                                        Parent (Prim))));
+                                      Parameter_Specifications
+                                        (Parent (Prim))));
 
                            Insert_After (Curr_Nod, Wrap_Spec);
                            Curr_Nod := Wrap_Spec;
@@ -19847,7 +20236,7 @@ package body Sem_Ch3 is
                         Next_Elmt (Prim_Elmt);
                      end loop;
 
-                     return;
+                     goto Leave;
                   end;
 
                --  For non-concurrent types, transfer explicit primitives, but
@@ -19928,9 +20317,7 @@ package body Sem_Ch3 is
                Set_Class_Wide_Type
                  (Base_Type (Full_T), Class_Wide_Type (Priv_T));
 
-               Set_Has_Task (Class_Wide_Type (Priv_T), Has_Task      (Full_T));
-               Set_Has_Protected
-                            (Class_Wide_Type (Priv_T), Has_Protected (Full_T));
+               Propagate_Concurrent_Flags (Class_Wide_Type (Priv_T), Full_T);
             end if;
          end;
       end if;
@@ -19986,95 +20373,39 @@ package body Sem_Ch3 is
          Set_Has_Specified_Stream_Output (Full_T);
       end if;
 
-      --  Propagate the attributes related to pragma Default_Initial_Condition
-      --  from the private to the full view. Note that both flags are mutually
-      --  exclusive.
-
-      if Has_Default_Init_Cond (Priv_T)
-        or else Has_Inherited_Default_Init_Cond (Priv_T)
-      then
-         Propagate_Default_Init_Cond_Attributes
-           (From_Typ             => Priv_T,
-            To_Typ               => Full_T,
-            Private_To_Full_View => True);
-
-      --  In the case where the full view is derived from another private type,
-      --  the attributes related to pragma Default_Initial_Condition must be
-      --  propagated from the full to the private view to maintain consistency
-      --  of views.
-
-      --    package Pack is
-      --       type Parent_Typ is private
-      --         with Default_Initial_Condition ...;
-      --    private
-      --       type Parent_Typ is ...;
-      --    end Pack;
-
-      --    with Pack; use Pack;
-      --    package Pack_2 is
-      --       type Deriv_Typ is private;         --  must inherit
-      --    private
-      --       type Deriv_Typ is new Parent_Typ;  --  must inherit
-      --    end Pack_2;
-
-      elsif Has_Default_Init_Cond (Full_T)
-        or else Has_Inherited_Default_Init_Cond (Full_T)
-      then
-         Propagate_Default_Init_Cond_Attributes
-           (From_Typ             => Full_T,
-            To_Typ               => Priv_T,
-            Private_To_Full_View => True);
-      end if;
-
-      if Is_Ghost_Entity (Priv_T) then
-
-         --  The Ghost policy in effect at the point of declaration and at the
-         --  point of completion must match (SPARK RM 6.9(14)).
-
-         Check_Ghost_Completion (Priv_T, Full_T);
-
-         --  Propagate the attributes related to pragma Ghost from the private
-         --  to the full view.
-
-         Mark_Full_View_As_Ghost (Priv_T, Full_T);
-      end if;
+      --  Propagate Default_Initial_Condition-related attributes from the
+      --  partial view to the full view and its base type.
 
-      --  Propagate invariants to full type
+      Propagate_DIC_Attributes (Full_T, From_Typ => Priv_T);
+      Propagate_DIC_Attributes (Base_Type (Full_T), From_Typ => Priv_T);
 
-      if Has_Invariants (Priv_T) then
-         Set_Has_Invariants (Full_T);
-         Set_Invariant_Procedure (Full_T, Invariant_Procedure (Priv_T));
-      end if;
+      --  Propagate invariant-related attributes from the partial view to the
+      --  full view and its base type.
 
-      if Has_Inheritable_Invariants (Priv_T) then
-         Set_Has_Inheritable_Invariants (Full_T);
-      end if;
+      Propagate_Invariant_Attributes (Full_T, From_Typ => Priv_T);
+      Propagate_Invariant_Attributes (Base_Type (Full_T), From_Typ => Priv_T);
 
-      --  Check hidden inheritance of class-wide type invariants
+      --  AI12-0041: Detect an attempt to inherit a class-wide type invariant
+      --  in the full view without advertising the inheritance in the partial
+      --  view. This can only occur when the partial view has no parent type
+      --  and the full view has an interface as a parent. Any other scenarios
+      --  are illegal because implemented interfaces must match between the
+      --  two views.
 
-      if Ada_Version >= Ada_2012
-        and then not Has_Inheritable_Invariants (Full_T)
-        and then In_Private_Part (Current_Scope)
-        and then Has_Interfaces (Full_T)
-      then
+      if Is_Tagged_Type (Priv_T) and then Is_Tagged_Type (Full_T) then
          declare
-            Ifaces : Elist_Id;
-            AI     : Elmt_Id;
+            Full_Par : constant Entity_Id := Etype (Full_T);
+            Priv_Par : constant Entity_Id := Etype (Priv_T);
 
          begin
-            Collect_Interfaces (Full_T, Ifaces, Exclude_Parents => True);
-
-            AI := First_Elmt (Ifaces);
-            while Present (AI) loop
-               if Has_Inheritable_Invariants (Node (AI)) then
-                  Error_Msg_N
-                    ("hidden inheritance of class-wide type invariants " &
-                     "not allowed", N);
-                  exit;
-               end if;
-
-               Next_Elmt (AI);
-            end loop;
+            if not Is_Interface (Priv_Par)
+              and then Is_Interface (Full_Par)
+              and then Has_Inheritable_Invariants (Full_Par)
+            then
+               Error_Msg_N
+                 ("hidden inheritance of class-wide type invariants not "
+                  & "allowed", N);
+            end if;
          end;
       end if;
 
@@ -20090,6 +20421,9 @@ package body Sem_Ch3 is
             Set_Predicate_Function (Full_T, Predicate_Function (Priv_T));
          end if;
       end if;
+
+   <<Leave>>
+      Restore_Ghost_Mode (Mode);
    end Process_Full_View;
 
    -----------------------------------
@@ -20806,10 +21140,11 @@ package body Sem_Ch3 is
                Constrain_Integer (Def_Id, S);
                Inherit_Predicate_Flags (Def_Id, Subtype_Mark_Id);
 
-            when E_Record_Type     |
-                 E_Record_Subtype  |
-                 Class_Wide_Kind   |
-                 E_Incomplete_Type =>
+            when Class_Wide_Kind
+               | E_Incomplete_Type
+               | E_Record_Subtype
+               | E_Record_Type
+            =>
                Constrain_Discriminated_Type (Def_Id, S, Related_Nod);
 
                if Ekind (Def_Id) = E_Incomplete_Type then
@@ -20885,124 +21220,6 @@ package body Sem_Ch3 is
       end if;
    end Process_Subtype;
 
-   --------------------------------------------
-   -- Propagate_Default_Init_Cond_Attributes --
-   --------------------------------------------
-
-   procedure Propagate_Default_Init_Cond_Attributes
-     (From_Typ             : Entity_Id;
-      To_Typ               : Entity_Id;
-      Parent_To_Derivation : Boolean := False;
-      Private_To_Full_View : Boolean := False)
-   is
-      procedure Remove_Default_Init_Cond_Procedure (Typ : Entity_Id);
-      --  Remove the default initial procedure (if any) from the rep chain of
-      --  type Typ.
-
-      ----------------------------------------
-      -- Remove_Default_Init_Cond_Procedure --
-      ----------------------------------------
-
-      procedure Remove_Default_Init_Cond_Procedure (Typ : Entity_Id) is
-         Found : Boolean := False;
-         Prev  : Entity_Id;
-         Subp  : Entity_Id;
-
-      begin
-         Prev := Typ;
-         Subp := Subprograms_For_Type (Typ);
-         while Present (Subp) loop
-            if Is_Default_Init_Cond_Procedure (Subp) then
-               Found := True;
-               exit;
-            end if;
-
-            Prev := Subp;
-            Subp := Subprograms_For_Type (Subp);
-         end loop;
-
-         if Found then
-            Set_Subprograms_For_Type (Prev, Subprograms_For_Type (Subp));
-            Set_Subprograms_For_Type (Subp, Empty);
-         end if;
-      end Remove_Default_Init_Cond_Procedure;
-
-      --  Local variables
-
-      Inherit_Procedure : Boolean := False;
-
-   --  Start of processing for Propagate_Default_Init_Cond_Attributes
-
-   begin
-      if Has_Default_Init_Cond (From_Typ) then
-
-         --  A derived type inherits the attributes from its parent type
-
-         if Parent_To_Derivation then
-            Set_Has_Inherited_Default_Init_Cond (To_Typ);
-
-         --  A full view shares the attributes with its private view
-
-         else
-            Set_Has_Default_Init_Cond (To_Typ);
-         end if;
-
-         Inherit_Procedure := True;
-
-         --  Due to the order of expansion, a derived private type is processed
-         --  by two routines which both attempt to set the attributes related
-         --  to pragma Default_Initial_Condition - Build_Derived_Type and then
-         --  Process_Full_View.
-
-         --    package Pack is
-         --       type Parent_Typ is private
-         --         with Default_Initial_Condition ...;
-         --    private
-         --       type Parent_Typ is ...;
-         --    end Pack;
-
-         --    with Pack; use Pack;
-         --    package Pack_2 is
-         --       type Deriv_Typ is private
-         --         with Default_Initial_Condition ...;
-         --    private
-         --       type Deriv_Typ is new Parent_Typ;
-         --    end Pack_2;
-
-         --  When Build_Derived_Type operates, it sets the attributes on the
-         --  full view without taking into account that the private view may
-         --  define its own default initial condition procedure. This becomes
-         --  apparent in Process_Full_View which must undo some of the work by
-         --  Build_Derived_Type and propagate the attributes from the private
-         --  to the full view.
-
-         if Private_To_Full_View then
-            Set_Has_Inherited_Default_Init_Cond (To_Typ, False);
-            Remove_Default_Init_Cond_Procedure (To_Typ);
-         end if;
-
-      --  A type must inherit the default initial condition procedure from a
-      --  parent type when the parent itself is inheriting the procedure or
-      --  when it is defining one. This circuitry is also used when dealing
-      --  with the private / full view of a type.
-
-      elsif Has_Inherited_Default_Init_Cond (From_Typ)
-        or (Parent_To_Derivation
-              and Present (Get_Pragma
-                    (From_Typ, Pragma_Default_Initial_Condition)))
-      then
-         Set_Has_Inherited_Default_Init_Cond (To_Typ);
-         Inherit_Procedure := True;
-      end if;
-
-      if Inherit_Procedure
-        and then No (Default_Init_Cond_Procedure (To_Typ))
-      then
-         Set_Default_Init_Cond_Procedure
-           (To_Typ, Default_Init_Cond_Procedure (From_Typ));
-      end if;
-   end Propagate_Default_Init_Cond_Attributes;
-
    -----------------------------
    -- Record_Type_Declaration --
    -----------------------------
@@ -21286,13 +21503,7 @@ package body Sem_Ch3 is
             Init_Component_Location (Component);
          end if;
 
-         if Has_Task (Etype (Component)) then
-            Set_Has_Task (T);
-         end if;
-
-         if Has_Protected (Etype (Component)) then
-            Set_Has_Protected (T);
-         end if;
+         Propagate_Concurrent_Flags (T, Etype (Component));
 
          if Ekind (Component) /= E_Component then
             null;