[multiple changes]
[platform/upstream/gcc.git] / gcc / ada / sem_ch3.adb
index f41b8e9..dbbb25e 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -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;
@@ -1415,7 +1405,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 +1427,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 +1848,6 @@ package body Sem_Ch3 is
 
             when others =>
                return False;
-
          end case;
       end Contains_POC;
 
@@ -2164,16 +2154,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 +2207,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 +2417,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 +2464,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;
@@ -2344,12 +2534,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 +2557,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 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 +2608,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.
@@ -2451,6 +2659,12 @@ package body Sem_Ch3 is
             end if;
 
             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;
@@ -2458,11 +2672,13 @@ package body Sem_Ch3 is
          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 +2689,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,7 +2719,32 @@ 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
+         --  the input declarative list have proper refinements. The check is
+         --  performed only when the context denotes a block, entry, package,
+         --  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;
 
@@ -2802,7 +3034,6 @@ package body Sem_Ch3 is
 
             when others =>
                raise Program_Error;
-
          end case;
       end if;
 
@@ -2816,13 +3047,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));
@@ -2982,13 +3206,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.
 
@@ -3096,13 +3313,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
@@ -3234,6 +3444,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);
@@ -3345,8 +3559,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
 
@@ -3395,20 +3610,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');
@@ -3416,7 +3641,7 @@ package body Sem_Ch3 is
 
          if Error_Posted (N) then
 
-            --  Type mismatch or illegal redeclaration, Do not analyze
+            --  Type mismatch or illegal redeclaration; do not analyze
             --  expression to avoid cascaded errors.
 
             T := Find_Type_Of_Object (Object_Definition (N), N);
@@ -3453,13 +3678,13 @@ package body Sem_Ch3 is
       end if;
 
       --  Ada 2005 (AI-231): Propagate the null-excluding attribute and carry
-      --  out some static checks
+      --  out some static checks.
 
       if Ada_Version >= Ada_2005 and then Can_Never_Be_Null (T) then
 
          --  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
@@ -3553,9 +3778,7 @@ package body Sem_Ch3 is
 
       --  Special checks for protected objects not at library level
 
-      if Is_Protected_Type (T)
-        and then not Is_Library_Level_Entity (Id)
-      then
+      if Has_Protected (T) and then not Is_Library_Level_Entity (Id) then
          Check_Restriction (No_Local_Protected_Objects, Id);
 
          --  Protected objects with interrupt handlers must be at library level
@@ -3567,12 +3790,21 @@ package body Sem_Ch3 is
          --  AI05-0303: The AI is in fact a binding interpretation, and thus
          --  applies to the '95 version of the language as well.
 
-         if Has_Interrupt_Handler (T) and then Ada_Version < Ada_95 then
+         if Is_Protected_Type (T)
+           and then Has_Interrupt_Handler (T)
+           and then Ada_Version < Ada_95
+         then
             Error_Msg_N
               ("interrupt object can only be declared at library level", Id);
          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.
 
@@ -3695,8 +3927,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
@@ -3784,8 +4015,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;
 
@@ -3807,14 +4038,15 @@ package body Sem_Ch3 is
       --  do this in the analyzer and not the expander because the analyzer
       --  does some substantial rewriting in some cases.
 
-      --  We need a predicate check if the type has predicates, and if either
-      --  there is an initializing expression, or for default initialization
-      --  when we have at least one case of an explicit default initial value
-      --  and then this is not an internal declaration whose initialization
-      --  comes later (as for an aggregate expansion).
+      --  We need a predicate check if the type has predicates that are not
+      --  ignored, and if either there is an initializing expression, or for
+      --  default initialization when we have at least one case of an explicit
+      --  default initial value and then this is not an internal declaration
+      --  whose initialization comes later (as for an aggregate expansion).
 
       if not Suppress_Assignment_Checks (N)
         and then Present (Predicate_Function (T))
+        and then not Predicates_Ignored (T)
         and then not No_Initialization (N)
         and then
           (Present (E)
@@ -3828,8 +4060,16 @@ package body Sem_Ch3 is
             Check_Expression_Against_Static_Predicate (E, T);
          end if;
 
-         Insert_After (N,
-           Make_Predicate_Check (T, New_Occurrence_Of (Id, Loc)));
+         --  If the type is a null record and there is no explicit initial
+         --  expression, no predicate check applies.
+
+         if No (E) and then Is_Null_Record_Type (T) then
+            null;
+
+         else
+            Insert_After (N,
+              Make_Predicate_Check (T, New_Occurrence_Of (Id, Loc)));
+         end if;
       end if;
 
       --  Case of unconstrained type
@@ -3945,23 +4185,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,
@@ -3971,9 +4194,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
@@ -4010,7 +4231,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);
@@ -4040,9 +4264,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;
 
@@ -4144,22 +4369,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
@@ -4294,7 +4503,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
@@ -4341,15 +4550,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.
@@ -4371,7 +4571,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;
 
    ---------------------------
@@ -4394,6 +4596,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;
 
@@ -4459,8 +4663,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);
@@ -4481,7 +4685,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;
@@ -4494,9 +4697,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));
@@ -4509,13 +4711,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_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;
 
-      if Has_Inheritable_Invariants (Parent_Type) then
-         Set_Has_Inheritable_Invariants (T);
-         Set_Has_Invariants (T);
+            Next_Elmt (Iface_Elmt);
+         end loop;
       end if;
 
       --  Ada 2005 (AI-443): Synchronized private extension or a rewritten
@@ -4537,33 +4761,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
@@ -4702,6 +4922,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
@@ -4773,8 +5011,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);
@@ -4846,7 +5084,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
@@ -5001,7 +5241,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:
@@ -5063,6 +5303,31 @@ package body Sem_Ch3 is
          Set_Is_Generic_Actual_Type (Id, Is_Generic_Actual_Type (T));
       end if;
 
+      --  If this is a subtype declaration for an actual in an instance,
+      --  inherit static and dynamic predicates if any.
+
+      --  If declaration has no aspect specifications, inherit predicate
+      --  info as well. Unclear how to handle the case of both specified
+      --  and inherited predicates ??? Other inherited aspects, such as
+      --  invariants, should be OK, but the combination with later pragmas
+      --  may also require special merging.
+
+      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)))
+      then
+         Set_Subprograms_For_Type (Id, Subprograms_For_Type (T));
+
+         if Has_Static_Predicate (T) then
+            Set_Has_Static_Predicate (Id);
+            Set_Static_Discrete_Predicate (Id, Static_Discrete_Predicate (T));
+         end if;
+      end if;
+
+      --  Remaining processing depends on characteristics of base type
+
       T := Etype (Id);
 
       Set_Is_Immediately_Visible   (Id, True);
@@ -5122,9 +5387,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),
@@ -5195,28 +5460,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);
 
@@ -5352,13 +5595,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
@@ -5414,8 +5657,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');
@@ -5541,23 +5784,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));
+         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);
 
-         --  Inherit the "ghostness" from the constrained array type
-
-         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
 
@@ -5570,8 +5810,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
@@ -5713,9 +5952,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);
 
@@ -5808,15 +6048,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
@@ -5931,6 +6176,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));
@@ -5962,16 +6212,6 @@ package body Sem_Ch3 is
       if Null_Exclusion_Present (Type_Definition (N)) then
          Set_Can_Never_Be_Null (Derived_Type);
 
-         --  What is with the "AND THEN FALSE" here ???
-
-         if Can_Never_Be_Null (Parent_Type)
-           and then False
-         then
-            Error_Msg_NE
-              ("`NOT NULL` not allowed (& already excludes null)",
-                N, Parent_Type);
-         end if;
-
       elsif Can_Never_Be_Null (Parent_Type) then
          Set_Can_Never_Be_Null (Derived_Type);
       end if;
@@ -5983,6 +6223,7 @@ package body Sem_Ch3 is
       --  ??? THIS CODE SHOULD NOT BE HERE REALLY.
 
       Desig_Type := Designated_Type (Derived_Type);
+
       if Is_Composite_Type (Desig_Type)
         and then (not Is_Array_Type (Desig_Type))
         and then Has_Discriminants (Desig_Type)
@@ -6036,12 +6277,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
@@ -6620,8 +6855,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);
@@ -8695,36 +8934,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
@@ -8917,12 +9126,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));
@@ -8957,13 +9165,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.
 
-      --  We similarly inherit predicates
+      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;
 
-      if Has_Predicates (Parent_Type) then
+            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);
+
+                     if Has_Inheritable_Invariants (Iface) then
+                        Set_Has_Inherited_Invariants (Derived_Type);
+                        exit;
+                     end if;
+
+                     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;
 
@@ -8971,18 +9228,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.
 
@@ -8990,8 +9235,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);
@@ -9006,9 +9252,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;
@@ -9078,6 +9325,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);
@@ -11562,12 +11810,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
@@ -11775,9 +12024,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
@@ -11786,16 +12037,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);
@@ -11829,8 +12090,18 @@ package body Sem_Ch3 is
       --  in particular when the full type is a scalar type for which an
       --  anonymous base type is constructed.
 
+      --  The predicate functions are generated either at the freeze point
+      --  of the type or at the end of the visible part, and we must avoid
+      --  generating them twice.
+
       if Has_Predicates (Priv) then
          Set_Has_Predicates (Full);
+
+         if Present (Predicate_Function (Priv))
+           and then No (Predicate_Function (Full))
+         then
+            Set_Predicate_Function (Full, Predicate_Function (Priv));
+         end if;
       end if;
 
       if Has_Delayed_Aspects (Priv) then
@@ -12999,15 +13270,13 @@ package body Sem_Ch3 is
       Related_Nod : Node_Id;
       For_Access  : Boolean := False)
    is
-      E     : constant Entity_Id := Entity (Subtype_Mark (S));
-      T     : Entity_Id;
-      C     : Node_Id;
-      Elist : Elist_Id := New_Elmt_List;
+      E : Entity_Id := Entity (Subtype_Mark (S));
+      T : Entity_Id;
 
       procedure Fixup_Bad_Constraint;
-      --  This is called after finding a bad constraint, and after having
-      --  posted an appropriate error message. The mission is to leave the
-      --  entity T in as reasonable state as possible.
+      --  Called after finding a bad constraint, and after having posted an
+      --  appropriate error message. The goal is to leave type Def_Id in as
+      --  reasonable state as possible.
 
       --------------------------
       -- Fixup_Bad_Constraint --
@@ -13031,6 +13300,11 @@ package body Sem_Ch3 is
          Set_Error_Posted (Def_Id);
       end Fixup_Bad_Constraint;
 
+      --  Local variables
+
+      C      : Node_Id;
+      Constr : Elist_Id := New_Elmt_List;
+
    --  Start of processing for Constrain_Discriminated_Type
 
    begin
@@ -13048,17 +13322,36 @@ package body Sem_Ch3 is
          T := Designated_Type (T);
       end if;
 
-      --  Ada 2005 (AI-412): Constrained incomplete subtypes are illegal.
-      --  Avoid generating an error for access-to-incomplete subtypes.
+      --  In an instance it may be necessary to retrieve the full view of a
+      --  type with unknown discriminants, or a full view with defaulted
+      --  discriminants. In other contexts the constraint is illegal.
+
+      if In_Instance
+        and then Is_Private_Type (T)
+        and then Present (Full_View (T))
+        and then
+          (Has_Unknown_Discriminants (T)
+            or else
+              (not Has_Discriminants (T)
+                and then Has_Discriminants (Full_View (T))
+                and then Present (Discriminant_Default_Value
+                           (First_Discriminant (Full_View (T))))))
+      then
+         T := Full_View (T);
+         E := Full_View (E);
+      end if;
+
+      --  Ada 2005 (AI-412): Constrained incomplete subtypes are illegal. Avoid
+      --  generating an error for access-to-incomplete subtypes.
 
       if Ada_Version >= Ada_2005
         and then Ekind (T) = E_Incomplete_Type
         and then Nkind (Parent (S)) = N_Subtype_Declaration
         and then not Is_Itype (Def_Id)
       then
-         --  A little sanity check, emit an error message if the type
-         --  has discriminants to begin with. Type T may be a regular
-         --  incomplete type or imported via a limited with clause.
+         --  A little sanity check: emit an error message if the type has
+         --  discriminants to begin with. Type T may be a regular incomplete
+         --  type or imported via a limited with clause.
 
          if Has_Discriminants (T)
            or else (From_Limited_With (T)
@@ -13099,23 +13392,23 @@ package body Sem_Ch3 is
          return;
       end if;
 
-      --  T may be an unconstrained subtype (e.g. a generic actual).
-      --  Constraint applies to the base type.
+      --  T may be an unconstrained subtype (e.g. a generic actual). Constraint
+      --  applies to the base type.
 
       T := Base_Type (T);
 
-      Elist := Build_Discriminant_Constraints (T, S);
+      Constr := Build_Discriminant_Constraints (T, S);
 
       --  If the list returned was empty we had an error in building the
       --  discriminant constraint. We have also already signalled an error
       --  in the incomplete type case
 
-      if Is_Empty_Elmt_List (Elist) then
+      if Is_Empty_Elmt_List (Constr) then
          Fixup_Bad_Constraint;
          return;
       end if;
 
-      Build_Discriminated_Subtype (T, Def_Id, Elist, Related_Nod, For_Access);
+      Build_Discriminated_Subtype (T, Def_Id, Constr, Related_Nod, For_Access);
    end Constrain_Discriminated_Type;
 
    ---------------------------
@@ -13647,8 +13940,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));
@@ -13871,8 +14163,8 @@ package body Sem_Ch3 is
       --  Inherit the discriminants of the parent type
 
       Add_Discriminants : declare
-         Num_Disc : Int;
-         Num_Gird : Int;
+         Num_Disc : Nat;
+         Num_Gird : Nat;
 
       begin
          Num_Disc := 0;
@@ -13967,7 +14259,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;
 
@@ -14355,7 +14648,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;
@@ -14594,9 +14887,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;
 
@@ -14732,12 +15026,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.
@@ -14936,7 +15224,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
@@ -14944,6 +15232,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;
@@ -14954,7 +15246,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
@@ -15022,7 +15314,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
@@ -16306,63 +16598,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;
@@ -16485,9 +16807,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);
@@ -17787,8 +18109,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 =>
@@ -17803,14 +18126,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 =>
@@ -17899,11 +18223,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
@@ -18046,7 +18397,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);
@@ -18055,6 +18407,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)));
@@ -18077,12 +18432,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;
 
    ----------------
@@ -18590,11 +18939,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;
@@ -18618,7 +18970,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 =>
@@ -18638,16 +18994,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
@@ -19218,6 +19576,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;
@@ -19312,11 +19674,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
@@ -19429,7 +19794,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
@@ -19449,8 +19814,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
@@ -19504,9 +19869,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
@@ -19519,8 +19884,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
@@ -19538,13 +19903,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 ?????
@@ -19762,19 +20127,26 @@ 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;
 
                            Analyze (Wrap_Spec);
+
+                           --  Remove the wrapper from visibility to avoid
+                           --  spurious conflict with the wrapped entity.
+
+                           Set_Is_Immediately_Visible
+                             (Defining_Entity (Specification (Wrap_Spec)),
+                              False);
                         end if;
 
                         Next_Elmt (Prim_Elmt);
                      end loop;
 
-                     return;
+                     goto Leave;
                   end;
 
                --  For non-concurrent types, transfer explicit primitives, but
@@ -19855,9 +20227,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;
@@ -19913,95 +20283,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)).
+      --  Propagate Default_Initial_Condition-related attributes from the
+      --  partial view to the full view and its base type.
 
-         Check_Ghost_Completion (Priv_T, Full_T);
+      Propagate_DIC_Attributes (Full_T, From_Typ => Priv_T);
+      Propagate_DIC_Attributes (Base_Type (Full_T), From_Typ => Priv_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 invariant-related attributes from the partial view to the
+      --  full view and its base type.
 
-      --  Propagate invariants to full type
+      Propagate_Invariant_Attributes (Full_T, From_Typ => Priv_T);
+      Propagate_Invariant_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;
-
-      if Has_Inheritable_Invariants (Priv_T) then
-         Set_Has_Inheritable_Invariants (Full_T);
-      end if;
+      --  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.
 
-      --  Check hidden inheritance of class-wide type invariants
-
-      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;
 
@@ -20011,12 +20325,15 @@ package body Sem_Ch3 is
       --  built. Still it is a cheap check and seems safer to make it.
 
       if Has_Predicates (Priv_T) then
+         Set_Has_Predicates (Full_T);
+
          if Present (Predicate_Function (Priv_T)) then
             Set_Predicate_Function (Full_T, Predicate_Function (Priv_T));
          end if;
-
-         Set_Has_Predicates (Full_T);
       end if;
+
+   <<Leave>>
+      Restore_Ghost_Mode (Mode);
    end Process_Full_View;
 
    -----------------------------------
@@ -20476,14 +20793,14 @@ package body Sem_Ch3 is
 
       May_Have_Null_Exclusion : Boolean;
 
-      procedure Check_Incomplete (T : Entity_Id);
+      procedure Check_Incomplete (T : Node_Id);
       --  Called to verify that an incomplete type is not used prematurely
 
       ----------------------
       -- Check_Incomplete --
       ----------------------
 
-      procedure Check_Incomplete (T : Entity_Id) is
+      procedure Check_Incomplete (T : Node_Id) is
       begin
          --  Ada 2005 (AI-412): Incomplete subtypes are legal
 
@@ -20733,10 +21050,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
@@ -20745,7 +21063,13 @@ package body Sem_Ch3 is
 
             when Private_Kind =>
                Constrain_Discriminated_Type (Def_Id, S, Related_Nod);
-               Set_Private_Dependents (Def_Id, New_Elmt_List);
+
+               --  The base type may be private but Def_Id may be a full view
+               --  in an instance.
+
+               if Is_Private_Type (Def_Id) then
+                  Set_Private_Dependents (Def_Id, New_Elmt_List);
+               end if;
 
                --  In case of an invalid constraint prevent further processing
                --  since the type constructed is missing expected fields.
@@ -20806,124 +21130,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 --
    -----------------------------
@@ -21207,13 +21413,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;