[Ada] Implement inheritance for Default_Initial_Condition and address other gaps

gcc/ada/

	* einfo.ads (Is_Partial_DIC_Procedure): New function.
	(Partial_DIC_Procedure): New procedure.
	* einfo.adb (Is_Partial_DIC_Procedure): New function to return
	whether a subprogram is a partial Default_Initial_Condition
	procedure by checking the name (to avoid adding a new field).
	(DIC_Procedure): Add a test that excludes partial DIC procedures
	from being returned.
	(Partial_DIC_Procedure): New procedure to return the partial DIC
	procedure of a type, if it has one (otherwise returns Empty).
	(Set_DIC_Procedure): Remove check for duplicate DIC procedures.
	* exp_aggr.adb (Gen_Assign): Generate a call to the type's DIC
	procedure in the case where an array component is default
	initialized (due to an association with a box).
	(Build_Record_Aggr_Code): For an extension aggregate, generate a
	call to the ancestor type's DIC procedure (if any) when the
	ancestor part is a subtype mark. For a record component
	association that was specified with a box (tested for by
	checking the new flag Was_Default_Init_Box_Association),
	generate a call to the component type's DIC procedure (if it has
	one).
	* exp_ch4.adb (Expand_N_Allocator): When the allocated object is
	default initialized and the designated type has a DIC aspect,
	generate a call to the DIC procedure.
	* exp_util.ads (Build_DIC_Call): Change the formal Obj_Id to
	name Obj_Name, and change its type from Entity_Id to Node_Id
	(and update comment).
	(Build_DIC_Procedure_Body): Add formal Partial_DIC, remove
	formal For_Freeze, and update comment accordingly.
	(Build_DIC_Procedure_Declaration): Add formal Partial_DIC and
	update comment.
	* exp_util.adb
	(Build_DIC_Call): Revised to use its Obj_Name (formerly Obj_Id)
	formal directly rather than calling New_Occurrence_Of on it, to
	allow arbitrary names to be passed rather than being limited to
	Entity_Ids.
	(Build_DIC_Procedure_Body): Call Add_Parent_DICs to generate
	checks for DICs associated with any parent types, implementing
	the required "additive" semantics for DICs. When building a DIC
	procedure body for a partial view (when Partial_DIC is True),
	call Add_Own_DIC when the type has its own DIC.  In the case of
	"full" DIC procedures, a call is generated to any partial DIC
	procedure of the type (unless the procedure has a null body),
	along with checks for any DICs inherited by the full view.
	(Build_DIC_Procedure_Declaration): Add handling for partial DIC
	procedures.  For the suffix of a regular DIC procedure's name,
	use "DIC" (instead of "Default_Initial_Condition"), and for the
	suffix of a partial DIC procedure's name, use "Partial_DIC".
	(Add_DIC_Check): Add the DIC pragma to the list of seen pragmas
	(Pragmas_Seen).
	(Add_Inherited_Tagged_DIC): Remove the formals Par_Typ,
	Deriv_Typ, and Obj_Id, and add formal Expr, which denotes DIC's
	expression. Remove the call to Replace_References (which is now
	done in Add_Inherited_DICs).
	(Add_Inherited_DICs): New procedure to locate a DIC pragma
	associated with a parent type, replace its references
	appropriately (such as any current instance references), and add
	a check for the DIC.
	(Add_Own_DIC): Add an Obj_Id formal to allow caller to pass the
	_init formal of the generated DIC procedure.
	(Add_Parent_DICs): New procedure to traverse a type's parents,
	looking for DICs associated with those and calling
	Add_Inherited_DICs to apply the appropriate DIC checks.
	(Is_Verifiable_DIC_Pragma): Treat pragmas that have an Empty
	first argument the same as a pragma without any arguments
	(returning False for that case).
	* exp_ch3.adb (Init_One_Dimension): Generate calls to the
	component's DIC procedure when needed.
	(Possible_DIC_Call): New function nested in Init_One_Dimension
	to build a call to the array component type's DIC-checking
	function when appropriate.
	(Build_Array_Init_Proc): The presence of a DIC on the component
	type is an additional condition for generating an init proc for
	an array type.
	(Build_Init_Statements): When the record component's type has a
	DIC, and the component declaration does not have an
	initialization expression, generate a call to the component
	type's DIC procedure.
	(Expand_N_Object_Declaration): Modify the call to Build_DIC_Call
	to pass a new occurrence of the object's defining id rather than
	the id itself.
	(Freeze_Type): Only build a type's DIC procedure (if it has one)
	for types that are not interfaces.
	* exp_spark.adb (Expand_SPARK_N_Freeze_Type): Remove From_Freeze
	actual and add a ??? comment.
	(Expand_SPARK_N_Object_Declaration): Modify call to
	Build_DIC_Call to pass a new occurrence of the object id rather
	than the object id itself.
	* sem_aggr.adb (Resolve_Record_Aggregate): Declare local flag
	Is_Box_Init_By_Default and set it in cases where the component
	association has a box and the component is being initialized by
	default (as opposed to initialized by an initialization
	expression associated with the component's declaration).
	(Add_Association): If the association has a box for a component
	initialized by default, the flag
	Was_Default_Init_Box_Association is set on the new component
	association (for later testing during expansion).
	(Get_Value): Reset Is_Box_Init_By_Default to False.
	* sem_ch3.adb (Build_Assertion_Bodies_For_Type): Rearrange code
	to build DIC procedure bodies for a (noninterface) type that
	Has_Own_DIC (for partial type views) or Has_DIC (for full type
	views) as appropriate.
	* sem_ch13.adb (Analyze_Aspect_Specifications,
	Aspect_Default_Initial_Condition): Add an extra argument to the
	DIC pragma to denote the type associated with the pragma (for
	use in Build_DIC_Procedure_Body).
	* sem_prag.adb (Analyze_Pragma): Allow two arguments for pragma
	Default_Initial_Condition.  If not already present, add an extra
	argument denoting the type that the pragma is associated with.
	* sem_util.adb (Propagate_DIC_Attributes): Retrieve any partial
	DIC procedure associated with the type and add it to the type's
	list of subprograms (Subprograms_For_Type).
	* sinfo.ads (Was_Default_Init_Box_Association): New flag on
	N_Component_Association nodes.  Add subprograms to get and set
	flag, as well as updating the documentation.
	* sinfo.adb (Was_Default_Init_Box_Association): New function to
	retrieve the corresponding flag (Flag14).
	(Set_Was_Default_Init_Box_Association): New procedure to set the
	corresponding flag (Flag14).

15 files changed, 900 insertions, 268 deletions

diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 9e5b0ee..8949703 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -2543,6 +2543,29 @@ package body Einfo is
       return Flag215 (Base_Type (Id));
    end Is_Param_Block_Component_Type;
 
+   function Is_Partial_DIC_Procedure (Id : E) return B is
+      Partial_DIC_Suffix : constant String := "Partial_DIC";
+      DIC_Nam            : constant String := Get_Name_String (Chars (Id));
+
+   begin
+      pragma Assert (Ekind (Id) in E_Function | E_Procedure);
+
+      --  Instead of adding a new Entity_Id flag (which are in short supply),
+      --  we test the form of the subprogram name. When the node field and flag
+      --  situation is eased, this should be replaced with a flag. ???
+
+      if DIC_Nam'Length > Partial_DIC_Suffix'Length
+        and then
+          DIC_Nam
+            (DIC_Nam'Last - Partial_DIC_Suffix'Length + 1 .. DIC_Nam'Last) =
+               Partial_DIC_Suffix
+      then
+         return True;
+      else
+         return False;
+      end if;
+   end Is_Partial_DIC_Procedure;
+
    function Is_Partial_Invariant_Procedure (Id : E) return B is
    begin
       pragma Assert (Ekind (Id) in E_Function | E_Procedure);
@@ -7401,7 +7424,13 @@ package body Einfo is
          while Present (Subp_Elmt) loop
             Subp_Id := Node (Subp_Elmt);
 
-            if Is_DIC_Procedure (Subp_Id) then
+            --  Currently the flag Is_DIC_Procedure is set for both normal DIC
+            --  check procedures as well as for partial DIC check procedures,
+            --  and we don't have a flag for the partial procedures.
+
+            if Is_DIC_Procedure (Subp_Id)
+              and then not Is_Partial_DIC_Procedure (Subp_Id)
+            then
                return Subp_Id;
             end if;
 
@@ -8792,6 +8821,36 @@ package body Einfo is
       return Ekind (Id);
    end Parameter_Mode;
 
+   ---------------------------
+   -- Partial_DIC_Procedure --
+   ---------------------------
+
+   function Partial_DIC_Procedure (Id : E) return E is
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
+
+   begin
+      pragma Assert (Is_Type (Id));
+
+      Subps := Subprograms_For_Type (Base_Type (Id));
+
+      if Present (Subps) then
+         Subp_Elmt := First_Elmt (Subps);
+         while Present (Subp_Elmt) loop
+            Subp_Id := Node (Subp_Elmt);
+
+            if Is_Partial_DIC_Procedure (Subp_Id) then
+               return Subp_Id;
+            end if;
+
+            Next_Elmt (Subp_Elmt);
+         end loop;
+      end if;
+
+      return Empty;
+   end Partial_DIC_Procedure;
+
    ---------------------------------
    -- Partial_Invariant_Procedure --
    ---------------------------------
@@ -9271,8 +9330,6 @@ package body Einfo is
 
    procedure Set_DIC_Procedure (Id : E; V : E) is
       Base_Typ  : Entity_Id;
-      Subp_Elmt : Elmt_Id;
-      Subp_Id   : Entity_Id;
       Subps     : Elist_Id;
 
    begin
@@ -9286,21 +9343,17 @@ package body Einfo is
          Set_Subprograms_For_Type (Base_Typ, Subps);
       end if;
 
-      Subp_Elmt := First_Elmt (Subps);
       Prepend_Elmt (V, Subps);
+   end Set_DIC_Procedure;
 
-      --  Check for a duplicate default initial condition procedure
-
-      while Present (Subp_Elmt) loop
-         Subp_Id := Node (Subp_Elmt);
-
-         if Is_DIC_Procedure (Subp_Id) then
-            raise Program_Error;
-         end if;
+   -------------------------------------
+   -- Set_Partial_Invariant_Procedure --
+   -------------------------------------
 
-         Next_Elmt (Subp_Elmt);
-      end loop;
-   end Set_DIC_Procedure;
+   procedure Set_Partial_DIC_Procedure (Id : E; V : E) is
+   begin
+      Set_DIC_Procedure (Id, V);
+   end Set_Partial_DIC_Procedure;
 
    -----------------------------
    -- Set_Invariant_Procedure --
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index a4b4f0f..360ce7c 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3932,6 +3932,20 @@ package Einfo is
 --       of a single protected/task type, the references are examined as they
 --       must appear only within the type defintion and the corresponding body.
 
+--    Partial_DIC_Procedure (synthesized)
+--       Defined in type entities. Set for a private type and its full view
+--       when the type is subject to pragma Default_Initial_Condition (DIC), or
+--       when the type inherits a DIC pragma from a parent type. Points to the
+--       entity of a procedure that takes a single argument of the given type
+--       and verifies the assertion expression of the DIC pragma at run time.
+--       When present, the Partial_DIC_Procedure of a type only checks DICs
+--       associated with the partial (private) view of the type, and is invoked
+--       by the full DIC_Procedure (which may check additional DICs associated
+--       with the full view).
+
+--       Note: the reason this is marked as a synthesized attribute is that the
+--       way this is stored is as an element of the Subprograms_For_Type field.
+
 --    Partial_Invariant_Procedure (synthesized)
 --       Defined in types and subtypes. Set for private types when one or more
 --       [class-wide] type invariants apply to them. Points to the entity for a
@@ -5821,6 +5835,7 @@ package Einfo is
    --    Is_Full_Access                      (synth)
    --    Is_Controlled                       (synth)
    --    Object_Size_Clause                  (synth)
+   --    Partial_DIC_Procedure               (synth)
    --    Partial_Invariant_Procedure         (synth)
    --    Predicate_Function                  (synth)
    --    Predicate_Function_M                (synth)
@@ -6586,6 +6601,7 @@ package Einfo is
    --    Is_Invariant_Procedure              (Flag257)  (non-generic case only)
    --    Is_Machine_Code_Subprogram          (Flag137)  (non-generic case only)
    --    Is_Null_Init_Proc                   (Flag178)
+   --    Is_Partial_DIC_Procedure            (synth)    (non-generic case only)
    --    Is_Partial_Invariant_Procedure      (Flag292)  (non-generic case only)
    --    Is_Predicate_Function               (Flag255)  (non-generic case only)
    --    Is_Predicate_Function_M             (Flag256)  (non-generic case only)
@@ -7405,6 +7421,7 @@ package Einfo is
    function Is_Packed_Array_Impl_Type           (Id : E) return B;
    function Is_Potentially_Use_Visible          (Id : E) return B;
    function Is_Param_Block_Component_Type       (Id : E) return B;
+   function Is_Partial_DIC_Procedure            (Id : E) return B;
    function Is_Partial_Invariant_Procedure      (Id : E) return B;
    function Is_Predicate_Function               (Id : E) return B;
    function Is_Predicate_Function_M             (Id : E) return B;
@@ -8309,12 +8326,14 @@ package Einfo is
    ---------------------------------------------------
 
    function DIC_Procedure                        (Id : E) return E;
+   function Partial_DIC_Procedure                (Id : E) return E;
    function Invariant_Procedure                  (Id : E) return E;
    function Partial_Invariant_Procedure          (Id : E) return E;
    function Predicate_Function                   (Id : E) return E;
    function Predicate_Function_M                 (Id : E) return E;
 
    procedure Set_DIC_Procedure                   (Id : E; V : E);
+   procedure Set_Partial_DIC_Procedure           (Id : E; V : E);
    procedure Set_Invariant_Procedure             (Id : E; V : E);
    procedure Set_Partial_Invariant_Procedure     (Id : E; V : E);
    procedure Set_Predicate_Function              (Id : E; V : E);
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 986ccc9..30f6dd9 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -1865,6 +1865,21 @@ package body Exp_Aggr is
                    Typ               => Ctype,
                    With_Default_Init => True));
 
+               --  If Default_Initial_Condition applies to the component type,
+               --  add a DIC check after the component is default-initialized.
+               --  It will be analyzed and resolved before the code for
+               --  initialization of other components.
+
+               --  Theoretically this might also be needed for cases where
+               --  the component type doesn't have an init proc (such as for
+               --  Default_Value cases), but those should be uncommon, and for
+               --  now we only support the init proc case. ???
+
+               if Has_DIC (Ctype) and then Present (DIC_Procedure (Ctype)) then
+                  Append_To (Stmts,
+                    Build_DIC_Call (Loc, New_Copy_Tree (Indexed_Comp), Ctype));
+               end if;
+
                --  If the component type has invariants, add an invariant
                --  check after the component is default-initialized. It will
                --  be analyzed and resolved before the code for initialization
@@ -3504,6 +3519,18 @@ package body Exp_Aggr is
                   then
                      Check_Ancestor_Discriminants (Entity (Ancestor));
                   end if;
+
+                  --  If ancestor type has Default_Initialization_Condition,
+                  --  add a DIC check after the ancestor object is initialized
+                  --  by default.
+
+                  if Has_DIC (Entity (Ancestor))
+                    and then Present (DIC_Procedure (Entity (Ancestor)))
+                  then
+                     Append_To (L,
+                       Build_DIC_Call
+                         (Loc, New_Copy_Tree (Ref), Entity (Ancestor)));
+                  end if;
                end if;
 
             --  Handle calls to C++ constructors
@@ -4109,6 +4136,22 @@ package body Exp_Aggr is
             end;
          end if;
 
+         --  If the component association was specified with a box and the
+         --  component type has a Default_Initial_Condition, then generate
+         --  a call to the DIC procedure.
+
+         if Has_DIC (Etype (Selector))
+           and then Was_Default_Init_Box_Association (Comp)
+           and then Present (DIC_Procedure (Etype (Selector)))
+         then
+            Append_To (L,
+              Build_DIC_Call (Loc,
+                Make_Selected_Component (Loc,
+                  Prefix        => New_Copy_Tree (Target),
+                  Selector_Name => New_Occurrence_Of (Selector, Loc)),
+                Etype (Selector)));
+         end if;
+
          Next (Comp);
       end loop;
 
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index bd2de67..3fa0641 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -671,24 +671,85 @@ package body Exp_Ch3 is
       ------------------------
 
       function Init_One_Dimension (N : Int) return List_Id is
-         Index : Entity_Id;
+         Index       : Entity_Id;
+         DIC_Call    : Node_Id;
+         Result_List : List_Id;
+
+         function Possible_DIC_Call return Node_Id;
+         --  If the component type has Default_Initial_Conditions and a DIC
+         --  procedure that is not an empty body, then builds a call to the
+         --  DIC procedure and returns it.
+
+         -----------------------
+         -- Possible_DIC_Call --
+         -----------------------
+
+         function Possible_DIC_Call return Node_Id is
+         begin
+            --  When the component's type has a Default_Initial_Condition, then
+            --  create a call for the DIC check.
+
+            if Has_DIC (Comp_Type)
+              --  In GNATprove mode, the component DICs are checked by other
+              --  means. They should not be added to the record type DIC
+              --  procedure, so that the procedure can be used to check the
+              --  record type invariants or DICs if any.
+
+              and then not GNATprove_Mode
+
+              and then Present (DIC_Procedure (Comp_Type))
+
+              and then not Has_Null_Body (DIC_Procedure (Comp_Type))
+            then
+               return
+                 Build_DIC_Call (Loc,
+                   Make_Indexed_Component (Loc,
+                     Prefix      => Make_Identifier (Loc, Name_uInit),
+                     Expressions => Index_List),
+                   Comp_Type);
+            else
+               return Empty;
+            end if;
+         end Possible_DIC_Call;
+
+      --  Start of processing for Init_One_Dimension
 
       begin
          --  If the component does not need initializing, then there is nothing
          --  to do here, so we return a null body. This occurs when generating
          --  the dummy Init_Proc needed for Initialize_Scalars processing.
+         --  An exception is if component type has a Default_Initial_Condition,
+         --  in which case we generate a call to the type's DIC procedure.
 
          if not Has_Non_Null_Base_Init_Proc (Comp_Type)
            and then not Comp_Simple_Init
            and then not Has_Task (Comp_Type)
            and then not Has_Default_Aspect (A_Type)
+           and then (not Has_DIC (Comp_Type)
+                      or else N > Number_Dimensions (A_Type))
          then
-            return New_List (Make_Null_Statement (Loc));
+            DIC_Call := Possible_DIC_Call;
+
+            if Present (DIC_Call) then
+               return New_List (DIC_Call);
+            else
+               return New_List (Make_Null_Statement (Loc));
+            end if;
 
          --  If all dimensions dealt with, we simply initialize the component
+         --  and append a call to component type's DIC procedure when needed.
 
          elsif N > Number_Dimensions (A_Type) then
-            return Init_Component;
+            DIC_Call := Possible_DIC_Call;
+
+            if Present (DIC_Call) then
+               Result_List := Init_Component;
+               Append (DIC_Call, Result_List);
+               return Result_List;
+
+            else
+               return Init_Component;
+            end if;
 
          --  Here we generate the required loop
 
@@ -753,6 +814,7 @@ package body Exp_Ch3 is
       --    3. Tasks are present
       --    4. The type is marked as a public entity
       --    5. The array type has a Default_Component_Value aspect
+      --    6. The array component type has a Default_Initialization_Condition
 
       --  The reason for the public entity test is to deal properly with the
       --  Initialize_Scalars pragma. This pragma can be set in the client and
@@ -771,7 +833,8 @@ package body Exp_Ch3 is
       Has_Default_Init := Has_Non_Null_Base_Init_Proc (Comp_Type)
                             or else Comp_Simple_Init
                             or else Has_Task (Comp_Type)
-                            or else Has_Default_Aspect (A_Type);
+                            or else Has_Default_Aspect (A_Type)
+                            or else Has_DIC (Comp_Type);
 
       if Has_Default_Init
         or else (not Restriction_Active (No_Initialize_Scalars)
@@ -3438,6 +3501,38 @@ package body Exp_Ch3 is
                   Actions := No_List;
                end if;
 
+               --  When the component's type has a Default_Initial_Condition,
+               --  and the component is default initialized, then check the
+               --  DIC here.
+
+               if Has_DIC (Typ)
+                 and then not Present (Expression (Decl))
+                 and then Present (DIC_Procedure (Typ))
+                 and then not Has_Null_Body (DIC_Procedure (Typ))
+
+                 --  The DICs of ancestors are checked as part of the type's
+                 --  DIC procedure.
+
+                 and then Chars (Id) /= Name_uParent
+
+                 --  In GNATprove mode, the component DICs are checked by other
+                 --  means. They should not be added to the record type DIC
+                 --  procedure, so that the procedure can be used to check the
+                 --  record type invariants or DICs if any.
+
+                 and then not GNATprove_Mode
+               then
+                  Append_New_To (Actions,
+                     Build_DIC_Call
+                       (Comp_Loc,
+                        Make_Selected_Component (Comp_Loc,
+                          Prefix        =>
+                            Make_Identifier (Comp_Loc, Name_uInit),
+                          Selector_Name =>
+                            New_Occurrence_Of (Id, Comp_Loc)),
+                        Typ));
+               end if;
+
                if Present (Checks) then
                   if Chars (Id) = Name_uParent then
                      Append_List_To (Parent_Stmts, Checks);
@@ -7552,12 +7647,14 @@ package body Exp_Ch3 is
       if Comes_From_Source (Def_Id)
         and then Has_DIC (Typ)
         and then Present (DIC_Procedure (Typ))
+        and then not Has_Null_Body (DIC_Procedure (Typ))
         and then not Has_Init_Expression (N)
         and then not Is_Imported (Def_Id)
       then
          declare
-            DIC_Call : constant Node_Id := Build_DIC_Call (Loc, Def_Id, Typ);
-
+            DIC_Call : constant Node_Id :=
+                         Build_DIC_Call
+                           (Loc, New_Occurrence_Of (Def_Id, Loc), Typ);
          begin
             if Present (Next_N) then
                Insert_Before_And_Analyze (Next_N, DIC_Call);
@@ -8331,13 +8428,6 @@ package body Exp_Ch3 is
       Process_Pending_Access_Types (Def_Id);
       Freeze_Stream_Operations (N, Def_Id);
 
-      --  Generate the [spec and] body of the procedure tasked with the runtime
-      --  verification of pragma Default_Initial_Condition's expression.
-
-      if Has_DIC (Def_Id) then
-         Build_DIC_Procedure_Body (Def_Id, For_Freeze => True);
-      end if;
-
       --  Generate the [spec and] body of the invariant procedure tasked with
       --  the runtime verification of all invariants that pertain to the type.
       --  This includes invariants on the partial and full view, inherited
@@ -8363,14 +8453,24 @@ package body Exp_Ch3 is
       --  subprograms, which may involve local declarations of local
       --  subtypes to which these checks do not apply.
 
-      elsif Has_Invariants (Def_Id) then
-         if not Predicate_Check_In_Scope (Def_Id)
-           or else (Ekind (Current_Scope) = E_Function
-                     and then Is_Predicate_Function (Current_Scope))
-         then
-            null;
-         else
-            Build_Invariant_Procedure_Body (Def_Id);
+      else
+         if Has_Invariants (Def_Id) then
+            if not Predicate_Check_In_Scope (Def_Id)
+              or else (Ekind (Current_Scope) = E_Function
+                        and then Is_Predicate_Function (Current_Scope))
+            then
+               null;
+            else
+               Build_Invariant_Procedure_Body (Def_Id);
+            end if;
+         end if;
+
+         --  Generate the [spec and] body of the procedure tasked with the
+         --  run-time verification of pragma Default_Initial_Condition's
+         --  expression.
+
+         if Has_DIC (Def_Id) then
+            Build_DIC_Procedure_Body (Def_Id);
          end if;
       end if;
 
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index d65dac9..ecaeeb2 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -5388,6 +5388,24 @@ package body Exp_Ch4 is
 
                Rewrite (N, New_Occurrence_Of (Temp, Loc));
                Analyze_And_Resolve (N, PtrT);
+
+               --  When designated type has Default_Initial_Condition aspects,
+               --  make a call to the type's DIC procedure to perform the
+               --  checks. Theoretically this might also be needed for cases
+               --  where the type doesn't have an init proc, but those should
+               --  be very uncommon, and for now we only support the init proc
+               --  case. ???
+
+               if Has_DIC (Dtyp)
+                 and then Present (DIC_Procedure (Dtyp))
+                 and then not Has_Null_Body (DIC_Procedure (Dtyp))
+               then
+                  Insert_Action (N,
+                                 Build_DIC_Call (Loc,
+                                   Make_Explicit_Dereference (Loc,
+                                     Prefix => New_Occurrence_Of (Temp, Loc)),
+                                 Dtyp));
+               end if;
             end if;
          end if;
       end;
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 7909944..d65136b 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -357,7 +357,10 @@ package body Exp_SPARK is
       --  procedure for it as done during regular expansion for compilation.
 
       if Has_DIC (E) and then Is_Tagged_Type (E) then
-         Build_DIC_Procedure_Body (E, For_Freeze => True);
+         --  Why is this needed for DIC, but not for other aspects (such as
+         --  Type_Invariant)???
+
+         Build_DIC_Procedure_Body (E);
       end if;
    end Expand_SPARK_N_Freeze_Type;
 
@@ -530,7 +533,7 @@ package body Exp_SPARK is
         and then Present (DIC_Procedure (Typ))
         and then not Has_Init_Expression (N)
       then
-         Call := Build_DIC_Call (Loc, Obj_Id, Typ);
+         Call := Build_DIC_Call (Loc, New_Occurrence_Of (Obj_Id, Loc), Typ);
 
          --  Partially insert the call into the tree by setting its parent
          --  pointer.
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 11efd46..9e08e9c 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1446,21 +1446,27 @@ package body Exp_Util is
    --------------------
 
    function Build_DIC_Call
-     (Loc    : Source_Ptr;
-      Obj_Id : Entity_Id;
-      Typ    : Entity_Id) return Node_Id
+     (Loc      : Source_Ptr;
+      Obj_Name : Node_Id;
+      Typ      : Entity_Id) return Node_Id
    is
       Proc_Id    : constant Entity_Id := DIC_Procedure (Typ);
       Formal_Typ : constant Entity_Id := Etype (First_Formal (Proc_Id));
 
    begin
+      --  The DIC procedure has a null body if assertions are disabled or
+      --  Assertion_Policy Ignore is in effect. In that case, it would be
+      --  nice to generate a null statement instead of a call to the DIC
+      --  procedure, but doing that seems to interfere with the determination
+      --  of ECRs (early call regions) in SPARK. ???
+
       return
         Make_Procedure_Call_Statement (Loc,
           Name                   => New_Occurrence_Of (Proc_Id, Loc),
           Parameter_Associations => New_List (
             Make_Unchecked_Type_Conversion (Loc,
               Subtype_Mark => New_Occurrence_Of (Formal_Typ, Loc),
-              Expression   => New_Occurrence_Of (Obj_Id, Loc))));
+              Expression   => Obj_Name)));
    end Build_DIC_Call;
 
    ------------------------------
@@ -1472,9 +1478,13 @@ package body Exp_Util is
    --  Ghost mode.
 
    procedure Build_DIC_Procedure_Body
-     (Typ        : Entity_Id;
-      For_Freeze : Boolean := False)
+     (Typ         : Entity_Id;
+      Partial_DIC : Boolean := False)
    is
+      Pragmas_Seen : Elist_Id := No_Elist;
+      --  This list contains all DIC pragmas processed so far. The list is used
+      --  to avoid redundant Default_Initial_Condition checks.
+
       procedure Add_DIC_Check
         (DIC_Prag : Node_Id;
          DIC_Expr : Node_Id;
@@ -1494,24 +1504,46 @@ package body Exp_Util is
       --  pragma. All generated code is added to list Stmts.
 
       procedure Add_Inherited_Tagged_DIC
-        (DIC_Prag  : Node_Id;
-         Par_Typ   : Entity_Id;
-         Deriv_Typ : Entity_Id;
-         Stmts     : in out List_Id);
+        (DIC_Prag : Node_Id;
+         Expr     : Node_Id;
+         Stmts    : in out List_Id);
       --  Add a runtime check to verify assertion expression DIC_Expr of
-      --  inherited pragma DIC_Prag. This routine applies class-wide pre- and
-      --  postcondition-like runtime semantics to the check. Par_Typ is the
-      --  parent type whose DIC pragma is being inherited. Deriv_Typ is the
-      --  derived type inheriting the DIC pragma. All generated code is added
-      --  to list Stmts.
+      --  inherited pragma DIC_Prag. This routine applies class-wide pre-
+      --  and postcondition-like runtime semantics to the check. Expr is
+      --  the assertion expression after substitition has been performed
+      --  (via Replace_References). All generated code is added to list Stmts.
+
+      procedure Add_Inherited_DICs
+        (T         : Entity_Id;
+         Priv_Typ  : Entity_Id;
+         Full_Typ  : Entity_Id;
+         Obj_Id    : Entity_Id;
+         Checks    : in out List_Id);
+      --  Generate a DIC check for each inherited Default_Initial_Condition
+      --  coming from all parent types of type T. Priv_Typ and Full_Typ denote
+      --  the partial and full view of the parent type. Obj_Id denotes the
+      --  entity of the _object formal parameter of the DIC procedure. All
+      --  created checks are added to list Checks.
 
       procedure Add_Own_DIC
         (DIC_Prag : Node_Id;
          DIC_Typ  : Entity_Id;
+         Obj_Id   : Entity_Id;
          Stmts    : in out List_Id);
       --  Add a runtime check to verify the assertion expression of pragma
-      --  DIC_Prag. DIC_Typ is the owner of the DIC pragma. All generated code
-      --  is added to list Stmts.
+      --  DIC_Prag. DIC_Typ is the owner of the DIC pragma. Obj_Id is the
+      --  object to substitute in the assertion expression for any references
+      --  to the current instance of the type All generated code is added to
+      --  list Stmts.
+
+      procedure Add_Parent_DICs
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate a Default_Initial_Condition check for each inherited DIC
+      --  aspect coming from all parent types of type T. Obj_Id denotes the
+      --  entity of the _object formal parameter of the DIC procedure. All
+      --  created checks are added to list Checks.
 
       -------------------
       -- Add_DIC_Check --
@@ -1549,6 +1581,10 @@ package body Exp_Util is
                   Make_Pragma_Argument_Association (Loc,
                     Expression => DIC_Expr))));
          end if;
+
+         --  Add the pragma to the list of processed pragmas
+
+         Append_New_Elmt (DIC_Prag, Pragmas_Seen);
       end Add_DIC_Check;
 
       -----------------------
@@ -1590,65 +1626,172 @@ package body Exp_Util is
       ------------------------------
 
       procedure Add_Inherited_Tagged_DIC
-        (DIC_Prag  : Node_Id;
-         Par_Typ   : Entity_Id;
-         Deriv_Typ : Entity_Id;
-         Stmts     : in out List_Id)
+        (DIC_Prag : Node_Id;
+         Expr     : Node_Id;
+         Stmts    : in out List_Id)
       is
-         Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ);
-         DIC_Args   : constant List_Id   :=
-                        Pragma_Argument_Associations (DIC_Prag);
-         DIC_Arg    : constant Node_Id   := First (DIC_Args);
-         DIC_Expr   : constant Node_Id   := Expression_Copy (DIC_Arg);
-         Par_Proc   : constant Entity_Id := DIC_Procedure (Par_Typ);
+      begin
+         --  Once the DIC assertion expression is fully processed, add a check
+         --  to the statements of the DIC procedure.
 
-         Expr : Node_Id;
+         Add_DIC_Check
+           (DIC_Prag => DIC_Prag,
+            DIC_Expr => Expr,
+            Stmts    => Stmts);
+      end Add_Inherited_Tagged_DIC;
+
+      ------------------------
+      -- Add_Inherited_DICs --
+      ------------------------
+
+      procedure Add_Inherited_DICs
+        (T         : Entity_Id;
+         Priv_Typ  : Entity_Id;
+         Full_Typ  : Entity_Id;
+         Obj_Id    : Entity_Id;
+         Checks    : in out List_Id)
+      is
+         Deriv_Typ     : Entity_Id;
+         Expr          : Node_Id;
+         Prag          : Node_Id;
+         Prag_Expr     : Node_Id;
+         Prag_Expr_Arg : Node_Id;
+         Prag_Typ      : Node_Id;
+         Prag_Typ_Arg  : Node_Id;
+
+         Par_Proc : Entity_Id;
+         --  The "partial" invariant procedure of Par_Typ
+
+         Par_Typ : Entity_Id;
+         --  The suitable view of the parent type used in the substitution of
+         --  type attributes.
 
       begin
-         --  The processing of an inherited DIC assertion expression starts off
-         --  with a copy of the original parent expression where all references
-         --  to the parent type have already been replaced with references to
-         --  the _object formal parameter of the parent type's DIC procedure.
+         if not Present (Priv_Typ) and then not Present (Full_Typ) then
+            return;
+         end if;
 
-         pragma Assert (Present (DIC_Expr));
-         Expr := New_Copy_Tree (DIC_Expr);
+         --  When the type inheriting the class-wide invariant is a concurrent
+         --  type, use the corresponding record type because it contains all
+         --  primitive operations of the concurrent type and allows for proper
+         --  substitution.
 
-         --  Perform the following substitutions:
+         if Is_Concurrent_Type (T) then
+            Deriv_Typ := Corresponding_Record_Type (T);
+         else
+            Deriv_Typ := T;
+         end if;
 
-         --    * Replace a reference to the _object parameter of the parent
-         --      type's DIC procedure with a reference to the _object parameter
-         --      of the derived types' DIC procedure.
+         pragma Assert (Present (Deriv_Typ));
 
-         --    * Replace a reference to a discriminant of the parent type with
-         --      a suitable value from the point of view of the derived type.
+         --  Determine which rep item chain to use. Precedence is given to that
+         --  of the parent type's partial view since it usually carries all the
+         --  class-wide invariants.
 
-         --    * Replace a call to an overridden parent primitive with a call
-         --      to the overriding derived type primitive.
+         if Present (Priv_Typ) then
+            Prag := First_Rep_Item (Priv_Typ);
+         else
+            Prag := First_Rep_Item (Full_Typ);
+         end if;
 
-         --    * Replace a call to an inherited parent primitive with a call to
-         --      the internally-generated inherited derived type primitive.
+         while Present (Prag) loop
+            if Nkind (Prag) = N_Pragma
+              and then Pragma_Name (Prag) = Name_Default_Initial_Condition
+            then
+               --  Nothing to do if the pragma was already processed
 
-         --  Note that primitives defined in the private part are automatically
-         --  handled by the overriding/inheritance mechanism and do not require
-         --  an extra replacement pass.
+               if Contains (Pragmas_Seen, Prag) then
+                  return;
+               end if;
 
-         pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc));
+               --  Extract arguments of the Default_Initial_Condition pragma
 
-         Replace_References
-           (Expr      => Expr,
-            Par_Typ   => Par_Typ,
-            Deriv_Typ => Deriv_Typ,
-            Par_Obj   => First_Formal (Par_Proc),
-            Deriv_Obj => First_Formal (Deriv_Proc));
+               Prag_Expr_Arg := First (Pragma_Argument_Associations (Prag));
+               Prag_Expr     := Expression_Copy (Prag_Expr_Arg);
 
-         --  Once the DIC assertion expression is fully processed, add a check
-         --  to the statements of the DIC procedure.
+               --  Pick up the implicit second argument of the pragma, which
+               --  indicates the type that the pragma applies to.
 
-         Add_DIC_Check
-           (DIC_Prag => DIC_Prag,
-            DIC_Expr => Expr,
-            Stmts    => Stmts);
-      end Add_Inherited_Tagged_DIC;
+               Prag_Typ_Arg  := Next (Prag_Expr_Arg);
+               if Present (Prag_Typ_Arg) then
+                  Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg);
+               else
+                  Prag_Typ := Empty;
+               end if;
+
+               --  The pragma applies to the partial view of the parent type
+
+               if Present (Priv_Typ)
+                 and then Present (Prag_Typ)
+                 and then Entity (Prag_Typ) = Priv_Typ
+               then
+                  Par_Typ := Priv_Typ;
+
+               --  The pragma applies to the full view of the parent type
+
+               elsif Present (Full_Typ)
+                 and then Present (Prag_Typ)
+                 and then Entity (Prag_Typ) = Full_Typ
+               then
+                  Par_Typ := Full_Typ;
+
+               --  Otherwise the pragma does not belong to the parent type and
+               --  should not be considered.
+
+               else
+                  return;
+               end if;
+
+               --  Substitute references in the DIC expression that are related
+               --  to the partial type with corresponding references related to
+               --  the derived type (call to Replace_References below).
+
+               Expr := New_Copy_Tree (Prag_Expr);
+
+               Par_Proc := Partial_DIC_Procedure (Par_Typ);
+
+               --  If there's not a partial DIC procedure (such as when a
+               --  full type doesn't have its own DIC, but is inherited from
+               --  a type with DIC), get the full DIC procedure.
+
+               if not Present (Par_Proc) then
+                  Par_Proc := DIC_Procedure (Par_Typ);
+               end if;
+
+               Replace_References
+                 (Expr      => Expr,
+                  Par_Typ   => Par_Typ,
+                  Deriv_Typ => Deriv_Typ,
+                  Par_Obj   => First_Formal (Par_Proc),
+                  Deriv_Obj => Obj_Id);
+
+               --  Why are there different actions depending on whether T is
+               --  tagged? Can these be unified? ???
+
+               if Is_Tagged_Type (T) then
+                  Add_Inherited_Tagged_DIC
+                    (DIC_Prag  => Prag,
+                     Expr      => Expr,
+                     Stmts     => Checks);
+
+               else
+                  Add_Inherited_DIC
+                    (DIC_Prag  => Prag,
+                     Par_Typ   => Par_Typ,
+                     Deriv_Typ => Deriv_Typ,
+                     Stmts     => Checks);
+               end if;
+
+               --  Leave as soon as we get a DIC pragma, since we'll visit
+               --  the pragmas of the parents, so will get to any "inherited"
+               --  pragmas that way.
+
+               return;
+            end if;
+
+            Next_Rep_Item (Prag);
+         end loop;
+      end Add_Inherited_DICs;
 
       -----------------
       -- Add_Own_DIC --
@@ -1657,6 +1800,7 @@ package body Exp_Util is
       procedure Add_Own_DIC
         (DIC_Prag : Node_Id;
          DIC_Typ  : Entity_Id;
+         Obj_Id   : Entity_Id;
          Stmts    : in out List_Id)
       is
          DIC_Args : constant List_Id   :=
@@ -1664,8 +1808,6 @@ package body Exp_Util is
          DIC_Arg  : constant Node_Id   := First (DIC_Args);
          DIC_Asp  : constant Node_Id   := Corresponding_Aspect (DIC_Prag);
          DIC_Expr : constant Node_Id   := Get_Pragma_Arg (DIC_Arg);
-         DIC_Proc : constant Entity_Id := DIC_Procedure (DIC_Typ);
-         Obj_Id   : constant Entity_Id := First_Formal (DIC_Proc);
 
          --  Local variables
 
@@ -1722,6 +1864,66 @@ package body Exp_Util is
             Stmts    => Stmts);
       end Add_Own_DIC;
 
+      ---------------------
+      -- Add_Parent_DICs --
+      ---------------------
+
+      procedure Add_Parent_DICs
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         Dummy_1 : Entity_Id;
+         Dummy_2 : Entity_Id;
+
+         Curr_Typ : Entity_Id;
+         --  The entity of the current type being examined
+
+         Full_Typ : Entity_Id;
+         --  The full view of Par_Typ
+
+         Par_Typ : Entity_Id;
+         --  The entity of the parent type
+
+         Priv_Typ : Entity_Id;
+         --  The partial view of Par_Typ
+
+      begin
+         --  Climb the parent type chain
+
+         Curr_Typ := T;
+         loop
+            --  Do not consider subtypes, as they inherit the DICs from their
+            --  base types.
+
+            Par_Typ := Base_Type (Etype (Base_Type (Curr_Typ)));
+
+            --  Stop the climb once the root of the parent chain is
+            --  reached.
+
+            exit when Curr_Typ = Par_Typ;
+
+            --  Process the DICs of the parent type
+
+            Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
+
+            --  Only try to inherit a DIC pragma from the parent type Par_Typ
+            --  if it Has_Own_DIC pragma. The loop will proceed up the parent
+            --  chain to find all types that have their own DIC.
+
+            if Has_Own_DIC (Par_Typ) then
+               Add_Inherited_DICs
+                 (T         => T,
+                  Priv_Typ  => Priv_Typ,
+                  Full_Typ  => Full_Typ,
+                  Obj_Id    => Obj_Id,
+                  Checks    => Checks);
+            end if;
+
+            Curr_Typ := Par_Typ;
+         end loop;
+      end Add_Parent_DICs;
+
       --  Local variables
 
       Loc : constant Source_Ptr := Sloc (Typ);
@@ -1740,8 +1942,20 @@ package body Exp_Util is
       Proc_Id      : Entity_Id;
       Stmts        : List_Id := No_List;
 
-      Build_Body : Boolean := False;
-      --  Flag set when the type requires a DIC procedure body to be built
+      CRec_Typ : Entity_Id := Empty;
+      --  The corresponding record type of Full_Typ
+
+      Full_Typ : Entity_Id := Empty;
+      --  The full view of the working type
+
+      Obj_Id : Entity_Id := Empty;
+      --  The _object formal parameter of the invariant procedure
+
+      Part_Proc : Entity_Id := Empty;
+      --  The entity of the "partial" invariant procedure
+
+      Priv_Typ : Entity_Id := Empty;
+      --  The partial view of the working type
 
       Work_Typ : Entity_Id;
       --  The working type
@@ -1805,25 +2019,41 @@ package body Exp_Util is
          goto Leave;
       end if;
 
-      --  The working type may lack a DIC procedure declaration. This may be
-      --  due to several reasons:
+      --  Obtain both views of the type
+
+      Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy_1, CRec_Typ);
 
-      --    * The working type's own DIC pragma does not contain a verifiable
-      --      assertion expression. In this case there is no need to build a
-      --      DIC procedure because there is nothing to check.
+      --  The caller requests a body for the partial DIC procedure
 
-      --    * The working type derives from a parent type. In this case a DIC
-      --      procedure should be built only when the inherited DIC pragma has
-      --      a verifiable assertion expression.
+      if Partial_DIC then
+         Proc_Id   := Partial_DIC_Procedure (Work_Typ);
 
-      Proc_Id := DIC_Procedure (Work_Typ);
+         --  The "full" DIC procedure body was already created
 
-      --  Build a DIC procedure declaration when the working type derives from
-      --  a parent type.
+         --  Create a declaration for the "partial" DIC procedure if it
+         --  is not available.
+
+         if No (Proc_Id) then
+            Build_DIC_Procedure_Declaration
+              (Typ         => Work_Typ,
+               Partial_DIC => True);
 
-      if No (Proc_Id) then
-         Build_DIC_Procedure_Declaration (Work_Typ);
-         Proc_Id := DIC_Procedure (Work_Typ);
+            Proc_Id := Partial_DIC_Procedure (Work_Typ);
+         end if;
+
+      --  The caller requests a body for the "full" DIC procedure
+
+      else
+         Proc_Id   := DIC_Procedure (Work_Typ);
+         Part_Proc := Partial_DIC_Procedure (Work_Typ);
+
+         --  Create a declaration for the "full" DIC procedure if it is
+         --  not available.
+
+         if No (Proc_Id) then
+            Build_DIC_Procedure_Declaration (Work_Typ);
+            Proc_Id := DIC_Procedure (Work_Typ);
+         end if;
       end if;
 
       --  At this point there should be a DIC procedure declaration
@@ -1843,123 +2073,146 @@ package body Exp_Util is
       Push_Scope (Proc_Id);
       Install_Formals (Proc_Id);
 
-      --  The working type defines its own DIC pragma. Replace the current
-      --  instance of the working type with the formal of the DIC procedure.
-      --  Note that there is no need to consider inherited DIC pragmas from
-      --  parent types because the working type's DIC pragma "hides" all
-      --  inherited DIC pragmas.
+      Obj_Id := First_Formal (Proc_Id);
+      pragma Assert (Present (Obj_Id));
 
-      if Has_Own_DIC (Work_Typ) then
-         pragma Assert (DIC_Typ = Work_Typ);
+      --  The "partial" DIC procedure verifies the DICs of the partial view
+      --  only.
 
-         Add_Own_DIC
-           (DIC_Prag => DIC_Prag,
-            DIC_Typ  => DIC_Typ,
-            Stmts    => Stmts);
+      if Partial_DIC then
+         pragma Assert (Present (Priv_Typ));
+
+         if Has_Own_DIC (Work_Typ) then  -- If we're testing this then maybe
+            Add_Own_DIC        -- we shouldn't be calling Find_DIC_Typ above???
+              (DIC_Prag => DIC_Prag,
+               DIC_Typ  => DIC_Typ,  -- Should this just be Work_Typ???
+               Obj_Id   => Obj_Id,
+               Stmts    => Stmts);
+         end if;
 
-         Build_Body := True;
+      --  Otherwise the "full" DIC procedure verifies the DICs of the full
+      --  view, well as DICs inherited from parent types. In addition, it
+      --  indirectly verifies the DICs of the partial view by calling the
+      --  "partial" DIC procedure.
 
-      --  Otherwise the working type inherits a DIC pragma from a parent type.
-      --  This processing is carried out when the type is frozen because the
-      --  state of all parent discriminants is known at that point. Note that
-      --  it is semantically sound to delay the creation of the DIC procedure
-      --  body till the freeze point. If the type has a DIC pragma of its own,
-      --  then the DIC procedure body would have already been constructed at
-      --  the end of the visible declarations and all parent DIC pragmas are
-      --  effectively "hidden" and irrelevant.
+      else
+         pragma Assert (Present (Full_Typ));
 
-      elsif For_Freeze then
-         pragma Assert (Has_Inherited_DIC (Work_Typ));
-         pragma Assert (DIC_Typ /= Work_Typ);
+         --  Check the DIC of the partial view by calling the "partial" DIC
+         --  procedure, unless the partial DIC body is empty. Generate:
 
-         --  The working type is tagged. The verification of the assertion
-         --  expression is subject to the same semantics as class-wide pre-
-         --  and postconditions.
+         --    <Work_Typ>Partial_DIC (_object);
+
+         if Present (Part_Proc) and then not Has_Null_Body (Part_Proc) then
+            Append_New_To (Stmts,
+              Make_Procedure_Call_Statement (Loc,
+                Name                   => New_Occurrence_Of (Part_Proc, Loc),
+                Parameter_Associations => New_List (
+                  New_Occurrence_Of (Obj_Id, Loc))));
+         end if;
 
-         if Is_Tagged_Type (Work_Typ) then
-            Add_Inherited_Tagged_DIC
-              (DIC_Prag  => DIC_Prag,
-               Par_Typ   => DIC_Typ,
-               Deriv_Typ => Work_Typ,
-               Stmts     => Stmts);
+         --  Derived subtypes do not have a partial view
 
-         --  Otherwise the working type is not tagged. Verify the assertion
-         --  expression of the inherited DIC pragma by directly calling the
-         --  DIC procedure of the parent type.
+         if Present (Priv_Typ) then
 
-         else
-            Add_Inherited_DIC
-              (DIC_Prag  => DIC_Prag,
-               Par_Typ   => DIC_Typ,
-               Deriv_Typ => Work_Typ,
-               Stmts     => Stmts);
+            --  The processing of the "full" DIC procedure intentionally
+            --  skips the partial view because a) this may result in changes of
+            --  visibility and b) lead to duplicate checks. However, when the
+            --  full view is the underlying full view of an untagged derived
+            --  type whose parent type is private, partial DICs appear on
+            --  the rep item chain of the partial view only.
+
+            --    package Pack_1 is
+            --       type Root ... is private;
+            --    private
+            --       <full view of Root>
+            --    end Pack_1;
+
+            --    with Pack_1;
+            --    package Pack_2 is
+            --       type Child is new Pack_1.Root with Type_DIC => ...;
+            --       <underlying full view of Child>
+            --    end Pack_2;
+
+            --  As a result, the processing of the full view must also consider
+            --  all DICs of the partial view.
+
+            if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then
+               null;
+
+            --  Otherwise the DICs of the partial view are ignored
+
+            else
+               --  Ignore the DICs of the partial view by eliminating the view
+
+               Priv_Typ := Empty;
+            end if;
          end if;
 
-         Build_Body := True;
+         --  Process inherited Default_Initial_Conditions for all parent types
+
+         Add_Parent_DICs (Work_Typ, Obj_Id, Stmts);
       end if;
 
       End_Scope;
 
-      if Build_Body then
+      --  Produce an empty completing body in the following cases:
+      --    * Assertions are disabled
+      --    * The DIC Assertion_Policy is Ignore
 
-         --  Produce an empty completing body in the following cases:
-         --    * Assertions are disabled
-         --    * The DIC Assertion_Policy is Ignore
+      if No (Stmts) then
+         Stmts := New_List (Make_Null_Statement (Loc));
+      end if;
 
-         if No (Stmts) then
-            Stmts := New_List (Make_Null_Statement (Loc));
-         end if;
+      --  Generate:
+      --    procedure <Work_Typ>DIC (_object : <Work_Typ>) is
+      --    begin
+      --       <Stmts>
+      --    end <Work_Typ>DIC;
 
-         --  Generate:
-         --    procedure <Work_Typ>DIC (_object : <Work_Typ>) is
-         --    begin
-         --       <Stmts>
-         --    end <Work_Typ>DIC;
-
-         Proc_Body :=
-           Make_Subprogram_Body (Loc,
-             Specification                =>
-               Copy_Subprogram_Spec (Parent (Proc_Id)),
-             Declarations                 => Empty_List,
-               Handled_Statement_Sequence =>
-                 Make_Handled_Sequence_Of_Statements (Loc,
-                   Statements => Stmts));
-         Proc_Body_Id := Defining_Entity (Proc_Body);
-
-         --  Perform minor decoration in case the body is not analyzed
-
-         Set_Ekind        (Proc_Body_Id, E_Subprogram_Body);
-         Set_Etype        (Proc_Body_Id, Standard_Void_Type);
-         Set_Scope        (Proc_Body_Id, Current_Scope);
-         Set_SPARK_Pragma (Proc_Body_Id, SPARK_Pragma (Proc_Id));
-         Set_SPARK_Pragma_Inherited
-                          (Proc_Body_Id, SPARK_Pragma_Inherited (Proc_Id));
-
-         --  Link both spec and body to avoid generating duplicates
-
-         Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
-         Set_Corresponding_Spec (Proc_Body, Proc_Id);
-
-         --  The body should not be inserted into the tree when the context
-         --  is a generic unit because it is not part of the template.
-         --  Note that the body must still be generated in order to resolve the
-         --  DIC assertion expression.
-
-         if Inside_A_Generic then
-            null;
+      Proc_Body :=
+        Make_Subprogram_Body (Loc,
+          Specification                =>
+            Copy_Subprogram_Spec (Parent (Proc_Id)),
+          Declarations                 => Empty_List,
+            Handled_Statement_Sequence =>
+              Make_Handled_Sequence_Of_Statements (Loc,
+                Statements => Stmts));
+      Proc_Body_Id := Defining_Entity (Proc_Body);
 
-         --  Semi-insert the body into the tree for GNATprove by setting its
-         --  Parent field. This allows for proper upstream tree traversals.
+      --  Perform minor decoration in case the body is not analyzed
 
-         elsif GNATprove_Mode then
-            Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+      Set_Ekind        (Proc_Body_Id, E_Subprogram_Body);
+      Set_Etype        (Proc_Body_Id, Standard_Void_Type);
+      Set_Scope        (Proc_Body_Id, Current_Scope);
+      Set_SPARK_Pragma (Proc_Body_Id, SPARK_Pragma (Proc_Id));
+      Set_SPARK_Pragma_Inherited
+                       (Proc_Body_Id, SPARK_Pragma_Inherited (Proc_Id));
 
-         --  Otherwise the body is part of the freezing actions of the working
-         --  type.
+      --  Link both spec and body to avoid generating duplicates
 
-         else
-            Append_Freeze_Action (Work_Typ, Proc_Body);
-         end if;
+      Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
+      Set_Corresponding_Spec (Proc_Body, Proc_Id);
+
+      --  The body should not be inserted into the tree when the context
+      --  is a generic unit because it is not part of the template.
+      --  Note that the body must still be generated in order to resolve the
+      --  DIC assertion expression.
+
+      if Inside_A_Generic then
+         null;
+
+      --  Semi-insert the body into the tree for GNATprove by setting its
+      --  Parent field. This allows for proper upstream tree traversals.
+
+      elsif GNATprove_Mode then
+         Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+
+      --  Otherwise the body is part of the freezing actions of the working
+      --  type.
+
+      else
+         Append_Freeze_Action (Work_Typ, Proc_Body);
       end if;
 
    <<Leave>>
@@ -1974,7 +2227,10 @@ package body Exp_Util is
    --  replaced by gotos which jump to the end of the routine and restore the
    --  Ghost mode.
 
-   procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is
+   procedure Build_DIC_Procedure_Declaration
+     (Typ         : Entity_Id;
+      Partial_DIC : Boolean := False)
+   is
       Loc : constant Source_Ptr := Sloc (Typ);
 
       Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
@@ -1985,6 +2241,7 @@ package body Exp_Util is
       DIC_Typ   : Entity_Id;
       Proc_Decl : Node_Id;
       Proc_Id   : Entity_Id;
+      Proc_Nam  : Name_Id;
       Typ_Decl  : Node_Id;
 
       CRec_Typ : Entity_Id;
@@ -2060,17 +2317,35 @@ package body Exp_Util is
 
       if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
          goto Leave;
+      end if;
+
+      --  Nothing to do if the type already has a "partial" DIC procedure
+
+      if Partial_DIC then
+         if Present (Partial_DIC_Procedure (Work_Typ)) then
+            goto Leave;
+         end if;
 
-      --  Nothing to do if the type already has a DIC procedure
+      --  Nothing to do if the type already has a "full" DIC procedure
 
       elsif Present (DIC_Procedure (Work_Typ)) then
          goto Leave;
       end if;
 
+      --  The caller requests the declaration of the "partial" DIC procedure
+
+      if Partial_DIC then
+         Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_DIC");
+
+      --  Otherwise the caller requests the declaration of the "full" DIC
+      --  procedure.
+
+      else
+         Proc_Nam := New_External_Name (Chars (Work_Typ), "DIC");
+      end if;
+
       Proc_Id :=
-        Make_Defining_Identifier (Loc,
-          Chars =>
-            New_External_Name (Chars (Work_Typ), "Default_Initial_Condition"));
+        Make_Defining_Identifier (Loc, Chars => Proc_Nam);
 
       --  Perform minor decoration in case the declaration is not analyzed
 
@@ -8908,6 +9183,13 @@ package body Exp_Util is
 
       return
         Present (Args)
+
+          --  If there are args, but the first arg is Empty, then treat the
+          --  pragma the same as having no args (there may be a second arg that
+          --  is an implicitly added type arg, and Empty is a placeholder).
+
+          and then Present (Get_Pragma_Arg (First (Args)))
+
           and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
    end Is_Verifiable_DIC_Pragma;
 
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 37eb86f..202ac3c 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -293,23 +293,29 @@ package Exp_Util is
    --  type is frozen.
 
    function Build_DIC_Call
-     (Loc    : Source_Ptr;
-      Obj_Id : Entity_Id;
-      Typ    : Entity_Id) return Node_Id;
-   --  Build a call to the DIC procedure of type Typ with Obj_Id as the actual
+     (Loc      : Source_Ptr;
+      Obj_Name : Node_Id;
+      Typ      : Entity_Id) return Node_Id;
+   --  Build a call to the DIC procedure for Typ with Obj_Name as the actual
    --  parameter.
 
    procedure Build_DIC_Procedure_Body
-     (Typ        : Entity_Id;
-      For_Freeze : Boolean := False);
+     (Typ         : Entity_Id;
+      Partial_DIC : Boolean := False);
    --  Create the body of the procedure which verifies the assertion expression
-   --  of pragma Default_Initial_Condition at run time. Flag For_Freeze should
-   --  be set when the body is constructed as part of the freezing actions for
-   --  Typ.
-
-   procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id);
+   --  of pragma Default_Initial_Condition at run time. Partial_DIC indicates
+   --  that a partial DIC-checking procedure body should be built, for checking
+   --  a DIC associated with the type's partial view, and which will be called
+   --  by the main DIC procedure.
+
+   procedure Build_DIC_Procedure_Declaration
+     (Typ         : Entity_Id;
+      Partial_DIC : Boolean := False);
    --  Create the declaration of the procedure which verifies the assertion
-   --  expression of pragma Default_Initial_Condition at run time.
+   --  expression of pragma Default_Initial_Condition at run time. Partial_DIC
+   --  indicates that a partial DIC-checking procedure should be declared,
+   --  for checking a DIC associated with the type's partial view, and which
+   --  will be called by the main DIC procedure.
 
    procedure Build_Invariant_Procedure_Body
      (Typ               : Entity_Id;
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 5a1f8c4..3caa84f 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -3715,9 +3715,10 @@ package body Sem_Aggr is
       --
       --  This variable is updated as a side effect of function Get_Value.
 
-      Box_Node       : Node_Id := Empty;
-      Is_Box_Present : Boolean := False;
-      Others_Box     : Natural := 0;
+      Box_Node               : Node_Id := Empty;
+      Is_Box_Present         : Boolean := False;
+      Is_Box_Init_By_Default : Boolean := False;
+      Others_Box             : Natural := 0;
       --  Ada 2005 (AI-287): Variables used in case of default initialization
       --  to provide a functionality similar to Others_Etype. Box_Present
       --  indicates that the component takes its default initialization;
@@ -3842,6 +3843,17 @@ package body Sem_Aggr is
              Choices     => Choice_List,
              Expression  => Expr,
              Box_Present => Is_Box_Present));
+
+         --  If this association has a box for a component that is initialized
+         --  by default, then set flag on the new association to indicate that
+         --  the original association was for such a box-initialized component.
+
+         if Resolve_Record_Aggregate.Is_Box_Present
+           and then not Is_Box_Present
+           and then Is_Box_Init_By_Default  -- ???
+         then
+            Set_Was_Default_Init_Box_Association (Last (Assoc_List));
+         end if;
       end Add_Association;
 
       -----------------------------
@@ -4059,6 +4071,7 @@ package body Sem_Aggr is
 
       begin
          Is_Box_Present := False;
+         Is_Box_Init_By_Default := False;
 
          if No (From) then
             return Empty;
@@ -5054,6 +5067,11 @@ package body Sem_Aggr is
                Ctyp : constant Entity_Id := Etype (Component);
 
             begin
+               --  Initially assume that the box is for a default-initialized
+               --  component and reset to False in cases where that's not true.
+
+               Is_Box_Init_By_Default := True;
+
                --  If there is a default expression for the aggregate, copy
                --  it into a new association. This copy must modify the scopes
                --  of internal types that may be attached to the expression
@@ -5077,6 +5095,11 @@ package body Sem_Aggr is
                  and then Nkind (Parent (Component)) = N_Component_Declaration
                  and then Present (Expression (Parent (Component)))
                then
+                  --  If component declaration has an initialization expression
+                  --  then this is not a case of default initialization.
+
+                  Is_Box_Init_By_Default := False;
+
                   Expr :=
                     New_Copy_Tree_And_Copy_Dimensions
                       (Expression (Parent (Component)),
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index ba7f5b8..b48aeb4 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -3606,11 +3606,17 @@ package body Sem_Ch13 is
                --  wrapped inside of a procedure at the freeze point of the
                --  private type's full view.
 
+               --  A type entity argument is appended to facilitate inheriting
+               --  the aspect from parent types (see Build_DIC_Procedure_Body),
+               --  though that extra argument isn't documented for the pragma.
+
                when Aspect_Default_Initial_Condition =>
                   Aitem := Make_Aitem_Pragma
                     (Pragma_Argument_Associations => New_List (
                        Make_Pragma_Argument_Association (Loc,
-                         Expression => Relocate_Node (Expr))),
+                         Expression => Relocate_Node (Expr)),
+                       Make_Pragma_Argument_Association (Sloc (Ent),
+                         Expression => Ent)),
                      Pragma_Name                  =>
                        Name_Default_Initial_Condition);
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index f487f73..00834ce 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2312,13 +2312,6 @@ package body Sem_Ch3 is
 
          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 class-wide invariants of an
@@ -2341,32 +2334,57 @@ package body Sem_Ch3 is
                         Partial_Invariant => True);
                   end if;
 
-               --  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.
+               elsif Decls = Visible_Declarations (Context) 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.
 
-               elsif Decls = Visible_Declarations (Context)
-                 and then Ekind (Typ) in 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)
-                            or else Present (Underlying_Full_View (Typ)))
-                 and then Has_Private_Declaration (Typ)
-                 and then Has_Invariants (Typ)
-               then
-                  Build_Invariant_Procedure_Body (Typ);
+                  if Ekind (Typ) in 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);
+                  end if;
+
+                  --  Preanalyze and resolve the Default_Initial_Condition
+                  --  assertion expression at the end of the declarations to
+                  --  catch any errors.
+
+                  if Ekind (Typ) in E_Limited_Private_Type
+                                  | E_Private_Type
+                                  | E_Record_Type_With_Private
+                     and then Has_Own_DIC (Typ)
+                  then
+                     Build_DIC_Procedure_Body
+                       (Typ         => Typ,
+                        Partial_DIC => True);
+                  end if;
+
+               elsif Decls = Private_Declarations (Context) then
+
+                  --  Preanalyze and resolve the invariants of a private type's
+                  --  full view at the end of the private declarations to catch
+                  --  potential errors.
+
+                  if (not Is_Private_Type (Typ)
+                       or else Present (Underlying_Full_View (Typ)))
+                    and then Has_Private_Declaration (Typ)
+                    and then Has_Invariants (Typ)
+                  then
+                     Build_Invariant_Procedure_Body (Typ);
+                  end if;
+
+                  if (not Is_Private_Type (Typ)
+                       or else Present (Underlying_Full_View (Typ)))
+                    and then Has_Private_Declaration (Typ)
+                    and then Has_DIC (Typ)
+                  then
+                     Build_DIC_Procedure_Body (Typ);
+                  end if;
                end if;
             end if;
          end Build_Assertion_Bodies_For_Type;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 02369bc3..1bcbb25 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -15111,7 +15111,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
-            Check_At_Most_N_Arguments (1);
+            Check_At_Most_N_Arguments (2);  -- Accounts for implicit type arg
 
             Typ  := Empty;
             Stmt := Prev (N);
@@ -15174,6 +15174,27 @@ package body Sem_Prag is
 
             Set_Has_Own_DIC (Typ);
 
+            --  A type entity argument is appended to facilitate inheriting the
+            --  aspect/pragma from parent types (see Build_DIC_Procedure_Body),
+            --  though that extra argument isn't documented for the pragma.
+
+            if not Present (Arg2) then
+               --  When the pragma has no arguments, create an argument with
+               --  the value Empty, so the type name argument can be appended
+               --  following it (since it's expected as the second argument).
+
+               if not Present (Arg1) then
+                  Set_Pragma_Argument_Associations (N, New_List (
+                    Make_Pragma_Argument_Association (Sloc (Typ),
+                      Expression => Empty)));
+               end if;
+
+               Append_To
+                 (Pragma_Argument_Associations (N),
+                  Make_Pragma_Argument_Association (Sloc (Typ),
+                    Expression => New_Occurrence_Of (Typ, Sloc (Typ))));
+            end if;
+
             --  Chain the pragma on the rep item chain for further processing
 
             Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index e1535e2..72dbc68 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -26184,7 +26184,8 @@ package body Sem_Util is
      (Typ      : Entity_Id;
       From_Typ : Entity_Id)
    is
-      DIC_Proc : Entity_Id;
+      DIC_Proc         : Entity_Id;
+      Partial_DIC_Proc : Entity_Id;
 
    begin
       if Present (Typ) and then Present (From_Typ) then
@@ -26205,6 +26206,7 @@ package body Sem_Util is
          end if;
 
          DIC_Proc := DIC_Procedure (From_Typ);
+         Partial_DIC_Proc := Partial_DIC_Procedure (From_Typ);
 
          --  The setting of the attributes is intentionally conservative. This
          --  prevents accidental clobbering of enabled attributes.
@@ -26220,6 +26222,12 @@ package body Sem_Util is
          if Present (DIC_Proc) and then No (DIC_Procedure (Typ)) then
             Set_DIC_Procedure (Typ, DIC_Proc);
          end if;
+
+         if Present (Partial_DIC_Proc)
+           and then No (Partial_DIC_Procedure (Typ))
+         then
+            Set_Partial_DIC_Procedure (Typ, Partial_DIC_Proc);
+         end if;
       end if;
    end Propagate_DIC_Attributes;
 
diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb
index c88d9a9..2d0a957 100644
--- a/gcc/ada/sinfo.adb
+++ b/gcc/ada/sinfo.adb
@@ -3535,6 +3535,14 @@ package body Sinfo is
       return Flag2 (N);
    end Was_Attribute_Reference;
 
+   function Was_Default_Init_Box_Association
+     (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Component_Association);
+      return Flag14 (N);
+   end Was_Default_Init_Box_Association;
+
    function Was_Expression_Function
       (N : Node_Id) return Boolean is
    begin
@@ -7036,6 +7044,14 @@ package body Sinfo is
       Set_Flag2 (N, Val);
    end Set_Was_Attribute_Reference;
 
+   procedure Set_Was_Default_Init_Box_Association
+     (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Component_Association);
+      Set_Flag14 (N, Val);
+   end Set_Was_Default_Init_Box_Association;
+
    procedure Set_Was_Expression_Function
       (N : Node_Id; Val : Boolean := True) is
    begin
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 439eef4..f9b0667 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -2412,6 +2412,11 @@ package Sinfo is
    --    instantiation prologue renames these attributes, and expansion later
    --    converts them into subprogram bodies.
 
+   --  Was_Default_Init_Box_Association (Flag14-Sem)
+   --    Present in N_Component_Association. Set to True if the original source
+   --    is an aggregate component association with a box (<>) for a component
+   --    that is initialized by default.
+
    --  Was_Expression_Function (Flag18-Sem)
    --    Present in N_Subprogram_Body. True if the original source had an
    --    N_Expression_Function, which was converted to the N_Subprogram_Body
@@ -4120,6 +4125,7 @@ package Sinfo is
       --  Expression (Node3) (empty if Box_Present)
       --  Loop_Actions (List5-Sem)
       --  Box_Present (Flag15)
+      --  Was_Default_Init_Box_Association (Flag14)
       --  Inherited_Discriminant (Flag13)
 
       --  Note: this structure is used for both record component associations
@@ -4128,7 +4134,9 @@ package Sinfo is
       --  list of selector names in the record aggregate case, or a list of
       --  discrete choices in the array aggregate case or an N_Others_Choice
       --  node (which appears as a singleton list). Box_Present gives support
-      --  to Ada 2005 (AI-287).
+      --  to Ada 2005 (AI-287). Was_Default_Init_Box_Association is used for
+      --  determining the need for Default_Initial_Condition check on component
+      --  associations with a box.
 
       ----------------------------------
       -- 4.3.1  Component Choice List --
@@ -10254,6 +10262,9 @@ package Sinfo is
    function Was_Attribute_Reference
      (N : Node_Id) return Boolean;    -- Flag2
 
+   function Was_Default_Init_Box_Association
+     (N : Node_Id) return Boolean;    -- Flag14
+
    function Was_Expression_Function
      (N : Node_Id) return Boolean;    -- Flag18
 
@@ -11366,6 +11377,9 @@ package Sinfo is
    procedure Set_Was_Attribute_Reference
      (N : Node_Id; Val : Boolean := True);    -- Flag2
 
+   procedure Set_Was_Default_Init_Box_Association
+     (N : Node_Id; Val : Boolean := True);    -- Flag14
+
    procedure Set_Was_Expression_Function
      (N : Node_Id; Val : Boolean := True);    -- Flag18
 
@@ -13477,6 +13491,7 @@ package Sinfo is
    pragma Inline (Visible_Declarations);
    pragma Inline (Used_Operations);
    pragma Inline (Was_Attribute_Reference);
+   pragma Inline (Was_Default_Init_Box_Association);
    pragma Inline (Was_Expression_Function);
    pragma Inline (Was_Originally_Stub);
 
@@ -13842,6 +13857,7 @@ package Sinfo is
    pragma Inline (Set_Variants);
    pragma Inline (Set_Visible_Declarations);
    pragma Inline (Set_Was_Attribute_Reference);
+   pragma Inline (Set_Was_Default_Init_Box_Association);
    pragma Inline (Set_Was_Expression_Function);
    pragma Inline (Set_Was_Originally_Stub);