einfo.ads, einfo.adb: Remove uses of flags Has_Default_Init_Cond...

2017-01-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.ads, einfo.adb: Remove uses of flags Has_Default_Init_Cond,
	Is_Default_Init_Cond_Procedure, and
	Has_Inherited_Default_Init_Cond.  Add uses of flags
	Has_Own_DIC, Is_DIC_Procedure, and Has_Inherited_DIC.
	(Default_Init_Cond_Procedure): Removed.
	(DIC_Procedure): New routine.
	(Has_Default_Init_Cond): Removed.
	(Has_DIC): New routine.
	(Has_Inheritable_Invariants): The attribute applies to the base type.
	(Has_Inherited_Default_Init_Cond): Removed.
	(Has_Inherited_DIC): New routine.
	(Has_Inherited_Invariants): The attribute applies to the base type.
	(Has_Own_DIC): New routine.
	(Has_Own_Invariants): The attribute applies to the base type.
	(Is_Default_Init_Cond_Procedure): Removed.
	(Is_DIC_Procedure): New routine.
	(Set_Default_Init_Cond_Procedure): Removed.
	(Set_DIC_Procedure): New routine.
	(Set_Has_Default_Init_Cond): Removed.
	(Set_Has_Inheritable_Invariants): The attribute applies
	to the base type.
	(Set_Has_Inherited_Default_Init_Cond): Removed.
	(Set_Has_Inherited_DIC): New routine.
	(Set_Has_Inherited_Invariants): The attribute applies to the base type.
	(Set_Has_Own_DIC): New routine.
	(Set_Has_Own_Invariants): The attribute applies to the base type.
	(Set_Is_Default_Init_Cond_Procedure): Removed.
	(Set_Is_DIC_Procedure): New routine.
	(Write_Entity_Flags): Update the output of all flags related to
	default initial condition.
	* exp_ch3.adb (Expand_N_Object_Declaration): Update the generation
	of the call to the DIC procedure.
	(Freeze_Type): Generate the body of the DIC procedure.
	* exp_ch7.adb (Build_Invariant_Procedure_Body): Replace
	all occurrences of Create_Append with Append_New_To. Do
	not generate an invariant procedure for a class-wide type.
	The generated body acts as a freeze action of the working type.
	(Build_Invariant_Procedure_Declaration): Do not generate an
	invariant procedure for a class-wide type.
	(Create_Append): Removed.
	* exp_util.adb: Add with and use clauses for Sem_Ch3, sem_ch6,
	sem_Ch12, Sem_Disp, and GNAT.HTable. Move the handling of
	class-wide pre/postcondition description and data structures from
	Sem_Prag.
	(Build_Class_Wide_Expression): Moved from Sem_Prag.
	(Build_DIC_Call): New routine.
	(Build_DIC_Procedure_Body): New routine.
	(Build_DIC_Procedure_Declaration): New routine.
	(Entity_Hash): Moved from Sem_Prag.
	(Find_DIC_Type): New routine.
	(Update_Primitives_Mapping): Reimplemented.
	(Update_Primitives_Mapping_Of_Types): New routine.
	* exp_util.ads (Build_Class_Wide_Expression): Moved from Sem_Prag.
	(Build_DIC_Call): New routine.
	(Build_DIC_Procedure_Body): New routine.
	(Build_DIC_Procedure_Declaration): New routine.
	(Update_Primitives_Mapping): Moved from Sem_Prag.
	(Update_Primitives_Mapping_Of_Types): New routine.
	* nlists.adb (Append_New): New routine.
	(Append_New_To): New routine.
	* nlists.ads (Append_New): New routine.
	(Append_New_To): New routine.
	* sem_ch3.adb (Analyze_Declarations): Do not generate the bodies
	of DIC procedures here. This is now done at the end of the
	visible declarations, private declarations, and at the freeze
	point of a type.
	(Analyze_Private_Extension_Declaration):
	A private extension inherits the DIC pragma of a parent type.
	(Analyze_Subtype_Declaration): No need to propagate invariant
	attributes to a subtype as those apply to the base type.
	(Build_Derived_Record_Type): No need to inherit invariants here
	as this is now done in Build_Derived_Type.
	(Build_Derived_Type): Inherit both the DIC pragma and invariants from
	a parent type.
	(Process_Full_View): Update the propagation of DIC attributes.
	(Propagate_Default_Init_Cond_Attributes): Removed.
	* sem_ch7.adb Add with and use clauses for Exp_Util.
	(Analyze_Package_Specification): Create the body of the DIC
	procedure at the end of the visible and private declarations.
	(Preserve_Full_Attributes): Propagate DIC attributes.
	* sem_ch9.adb (Analyze_Protected_Type_Declaration): Propagate
	DIC attributes.
	(Analyze_Task_Type_Declaration): Propagate DIC attributes.
	* sem_elab.adb (Check_A_Call): Update the call to
	Is_Nontrivial_Default_Init_Cond_Procedure.
	* sem_prag.adb Remove the with and use clauses for
	GNAT.HTable. Move the handling of class- wide pre/postcondition
	description and data structures to Exp_Util.
	(Analyze_Pragma): Create the declaration of the DIC procedure. There
	is no need to propagate invariant-related attributes at this point
	as this is done in Build_Invariant_Procedure_Declaration.
	(Build_Class_Wide_Expression): Moved to Exp_Util.
	(Entity_Hash): Moved to Exp_Util.
	(Update_Primitives_Mapping): Moved to Exp_Util.
	* sem_prag.ads (Build_Class_Wide_Expression): Moved to Exp_Util.
	(Update_Primitives_Mapping): Moved to Exp_Util.
	* sem_util.adb: Remove with and use clauses for Ghost
	and Sem_Ch13.
	(Build_Default_Init_Cond_Call): Removed.
	(Build_Default_Init_Cond_Procedure_Bodies): Removed.
	(Build_Default_Init_Cond_Procedure_Declaration): Removed.
	(Get_Views): Reimplemented.
	(Has_Full_Default_Initialization): Reimplement the section on DIC.
	(Inherit_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_DIC_Procedure): New routine.
	(Is_Verifiable_DIC_Pragma): New routine.
	(Propagate_DIC_Attributes): New routine.
	* sem_util.ads (Build_Default_Init_Cond_Call): Removed.
	(Build_Default_Init_Cond_Procedure_Bodies): Removed.
	(Build_Default_Init_Cond_Procedure_Declaration): Removed.
	(Inherit_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_Default_Init_Cond_Procedure): Removed.
	(Is_Nontrivial_DIC_Procedure): New routine.
	(Is_Verifiable_DIC_Pragma): New routine.
	(Propagate_DIC_Attributes): New routine.
	* sem_warn.adb (Is_OK_Fully_Initialized): Reimplement the section
	on DIC.
	* sinfo.ads, sinfo.adb: Add new attribute Expression_Copy along with
	usage in nodes.
	(Expression_Copy): New routine along with pragma Inline.
	(Set_Expression_Copy): New routine along with pragma Inline.

From-SVN: r244224

gcc/ada/ChangeLog

+2017-01-09  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* einfo.ads, einfo.adb: Remove uses of flags Has_Default_Init_Cond,
+	Is_Default_Init_Cond_Procedure, and
+	Has_Inherited_Default_Init_Cond.  Add uses of flags
+	Has_Own_DIC, Is_DIC_Procedure, and Has_Inherited_DIC.
+	(Default_Init_Cond_Procedure): Removed.
+	(DIC_Procedure): New routine.
+	(Has_Default_Init_Cond): Removed.
+	(Has_DIC): New routine.
+	(Has_Inheritable_Invariants): The attribute applies to the base type.
+	(Has_Inherited_Default_Init_Cond): Removed.
+	(Has_Inherited_DIC): New routine.
+	(Has_Inherited_Invariants): The attribute applies to the base type.
+	(Has_Own_DIC): New routine.
+	(Has_Own_Invariants): The attribute applies to the base type.
+	(Is_Default_Init_Cond_Procedure): Removed.
+	(Is_DIC_Procedure): New routine.
+	(Set_Default_Init_Cond_Procedure): Removed.
+	(Set_DIC_Procedure): New routine.
+	(Set_Has_Default_Init_Cond): Removed.
+	(Set_Has_Inheritable_Invariants): The attribute applies
+	to the base type.
+	(Set_Has_Inherited_Default_Init_Cond): Removed.
+	(Set_Has_Inherited_DIC): New routine.
+	(Set_Has_Inherited_Invariants): The attribute applies to the base type.
+	(Set_Has_Own_DIC): New routine.
+	(Set_Has_Own_Invariants): The attribute applies to the base type.
+	(Set_Is_Default_Init_Cond_Procedure): Removed.
+	(Set_Is_DIC_Procedure): New routine.
+	(Write_Entity_Flags): Update the output of all flags related to
+	default initial condition.
+	* exp_ch3.adb (Expand_N_Object_Declaration): Update the generation
+	of the call to the DIC procedure.
+	(Freeze_Type): Generate the body of the DIC procedure.
+	* exp_ch7.adb (Build_Invariant_Procedure_Body): Replace
+	all occurrences of Create_Append with Append_New_To. Do
+	not generate an invariant procedure for a class-wide type.
+	The generated body acts as a freeze action of the working type.
+	(Build_Invariant_Procedure_Declaration): Do not generate an
+	invariant procedure for a class-wide type.
+	(Create_Append): Removed.
+	* exp_util.adb: Add with and use clauses for Sem_Ch3, sem_ch6,
+	sem_Ch12, Sem_Disp, and GNAT.HTable. Move the handling of
+	class-wide pre/postcondition description and data structures from
+	Sem_Prag.
+	(Build_Class_Wide_Expression): Moved from Sem_Prag.
+	(Build_DIC_Call): New routine.
+	(Build_DIC_Procedure_Body): New routine.
+	(Build_DIC_Procedure_Declaration): New routine.
+	(Entity_Hash): Moved from Sem_Prag.
+	(Find_DIC_Type): New routine.
+	(Update_Primitives_Mapping): Reimplemented.
+	(Update_Primitives_Mapping_Of_Types): New routine.
+	* exp_util.ads (Build_Class_Wide_Expression): Moved from Sem_Prag.
+	(Build_DIC_Call): New routine.
+	(Build_DIC_Procedure_Body): New routine.
+	(Build_DIC_Procedure_Declaration): New routine.
+	(Update_Primitives_Mapping): Moved from Sem_Prag.
+	(Update_Primitives_Mapping_Of_Types): New routine.
+	* nlists.adb (Append_New): New routine.
+	(Append_New_To): New routine.
+	* nlists.ads (Append_New): New routine.
+	(Append_New_To): New routine.
+	* sem_ch3.adb (Analyze_Declarations): Do not generate the bodies
+	of DIC procedures here. This is now done at the end of the
+	visible declarations, private declarations, and at the freeze
+	point of a type.
+	(Analyze_Private_Extension_Declaration):
+	A private extension inherits the DIC pragma of a parent type.
+	(Analyze_Subtype_Declaration): No need to propagate invariant
+	attributes to a subtype as those apply to the base type.
+	(Build_Derived_Record_Type): No need to inherit invariants here
+	as this is now done in Build_Derived_Type.
+	(Build_Derived_Type): Inherit both the DIC pragma and invariants from
+	a parent type.
+	(Process_Full_View): Update the propagation of DIC attributes.
+	(Propagate_Default_Init_Cond_Attributes): Removed.
+	* sem_ch7.adb Add with and use clauses for Exp_Util.
+	(Analyze_Package_Specification): Create the body of the DIC
+	procedure at the end of the visible and private declarations.
+	(Preserve_Full_Attributes): Propagate DIC attributes.
+	* sem_ch9.adb (Analyze_Protected_Type_Declaration): Propagate
+	DIC attributes.
+	(Analyze_Task_Type_Declaration): Propagate DIC attributes.
+	* sem_elab.adb (Check_A_Call): Update the call to
+	Is_Nontrivial_Default_Init_Cond_Procedure.
+	* sem_prag.adb Remove the with and use clauses for
+	GNAT.HTable. Move the handling of class- wide pre/postcondition
+	description and data structures to Exp_Util.
+	(Analyze_Pragma): Create the declaration of the DIC procedure. There
+	is no need to propagate invariant-related attributes at this point
+	as this is done in Build_Invariant_Procedure_Declaration.
+	(Build_Class_Wide_Expression): Moved to Exp_Util.
+	(Entity_Hash): Moved to Exp_Util.
+	(Update_Primitives_Mapping): Moved to Exp_Util.
+	* sem_prag.ads (Build_Class_Wide_Expression): Moved to Exp_Util.
+	(Update_Primitives_Mapping): Moved to Exp_Util.
+	* sem_util.adb: Remove with and use clauses for Ghost
+	and Sem_Ch13.
+	(Build_Default_Init_Cond_Call): Removed.
+	(Build_Default_Init_Cond_Procedure_Bodies): Removed.
+	(Build_Default_Init_Cond_Procedure_Declaration): Removed.
+	(Get_Views): Reimplemented.
+	(Has_Full_Default_Initialization): Reimplement the section on DIC.
+	(Inherit_Default_Init_Cond_Procedure): Removed.
+	(Is_Nontrivial_Default_Init_Cond_Procedure): Removed.
+	(Is_Nontrivial_DIC_Procedure): New routine.
+	(Is_Verifiable_DIC_Pragma): New routine.
+	(Propagate_DIC_Attributes): New routine.
+	* sem_util.ads (Build_Default_Init_Cond_Call): Removed.
+	(Build_Default_Init_Cond_Procedure_Bodies): Removed.
+	(Build_Default_Init_Cond_Procedure_Declaration): Removed.
+	(Inherit_Default_Init_Cond_Procedure): Removed.
+	(Is_Nontrivial_Default_Init_Cond_Procedure): Removed.
+	(Is_Nontrivial_DIC_Procedure): New routine.
+	(Is_Verifiable_DIC_Pragma): New routine.
+	(Propagate_DIC_Attributes): New routine.
+	* sem_warn.adb (Is_OK_Fully_Initialized): Reimplement the section
+	on DIC.
+	* sinfo.ads, sinfo.adb: Add new attribute Expression_Copy along with
+	usage in nodes.
+	(Expression_Copy): New routine along with pragma Inline.
+	(Set_Expression_Copy): New routine along with pragma Inline.
+
 2017-01-06  Bob Duff  <duff@adacore.com>
 
 	* bindgen.adb (Gen_Adainit, Gen_Adafinal): Change

gcc/ada/exp_ch3.adb

@@ -6528,19 +6528,18 @@ package body Exp_Ch3 is
       --  pragma Default_Initial_Condition, add a runtime check to verify
       --  the assumption of the pragma (SPARK RM 7.3.3). Generate:
 
-      --    <Base_Typ>Default_Init_Cond (<Base_Typ> (Def_Id));
+      --    <Base_Typ>DIC (<Base_Typ> (Def_Id));
 
       --  Note that the check is generated for source objects only
 
       if Comes_From_Source (Def_Id)
-        and then (Has_Default_Init_Cond (Typ)
-                   or else Has_Inherited_Default_Init_Cond (Typ))
+        and then Has_DIC (Typ)
+        and then Present (DIC_Procedure (Typ))
         and then not Has_Init_Expression (N)
-        and then Present (Default_Init_Cond_Procedure (Typ))
       then
          declare
-            DIC_Call : constant Node_Id :=
-                         Build_Default_Init_Cond_Call (Loc, Def_Id, Typ);
+            DIC_Call : constant Node_Id := Build_DIC_Call (Loc, Def_Id, Typ);
+
          begin
             if Present (Next_N) then
                Insert_Before_And_Analyze (Next_N, DIC_Call);
@@ -7320,6 +7319,13 @@ 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);
+      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

gcc/ada/exp_ch7.adb

@@ -3525,9 +3525,6 @@ package body Exp_Ch7 is
       --  inherited class-wide invariants. Priv_Item denotes the first rep
       --  item of the private type.
 
-      procedure Create_Append (L : in out List_Id; N : Node_Id);
-      --  Append arbitrary node N to list L. If there is no list, create one.
-
       function Is_Untagged_Private_Derivation
         (Priv_Typ : Entity_Id;
          Full_Typ : Entity_Id) return Boolean;
@@ -3589,7 +3586,7 @@ package body Exp_Ch7 is
                --  effect.
 
                if not Has_Null_Body (Proc_Id) then
-                  Create_Append (Comp_Checks,
+                  Append_New_To (Comp_Checks,
                     Make_Procedure_Call_Statement (Loc,
                       Name                   =>
                         New_Occurrence_Of (Proc_Id, Loc),
@@ -3628,7 +3625,7 @@ package body Exp_Ch7 is
                --  effect.
 
                if not Has_Null_Body (Proc_Id) then
-                  Create_Append (Comp_Checks,
+                  Append_New_To (Comp_Checks,
                     Make_If_Statement (Loc,
                       Condition       =>
                         Make_Op_Ne (Loc,
@@ -3703,7 +3700,7 @@ package body Exp_Ch7 is
                --  effect.
 
                if Present (Comp_Checks) then
-                  Create_Append (Dim_Checks,
+                  Append_New_To (Dim_Checks,
                     Make_Implicit_Loop_Statement (T,
                       Identifier       => Empty,
                       Iteration_Scheme =>
@@ -3906,7 +3903,7 @@ package body Exp_Ch7 is
                      Var_Stmts := New_List (Make_Null_Statement (Loc));
                   end if;
 
-                  Create_Append (Var_Alts,
+                  Append_New_To (Var_Alts,
                     Make_Case_Statement_Alternative (Loc,
                       Discrete_Choices =>
                         New_Copy_List (Discrete_Choices (Var)),
@@ -3920,7 +3917,7 @@ package body Exp_Ch7 is
                --  values only when there is at least one real invariant check.
 
                if Produced_Variant_Check then
-                  Create_Append (CL_Checks,
+                  Append_New_To (CL_Checks,
                     Make_Case_Statement (Loc,
                       Expression   =>
                         Make_Selected_Component (Loc,
@@ -3980,7 +3977,7 @@ package body Exp_Ch7 is
                --  effect.
 
                if not Has_Null_Body (Proc_Id) then
-                  Create_Append (Comp_Checks,
+                  Append_New_To (Comp_Checks,
                     Make_Procedure_Call_Statement (Loc,
                       Name                   =>
                         New_Occurrence_Of (Proc_Id, Loc),
@@ -4023,7 +4020,7 @@ package body Exp_Ch7 is
                --  effect.
 
                if not Has_Null_Body (Proc_Id) then
-                  Create_Append (Comp_Checks,
+                  Append_New_To (Comp_Checks,
                     Make_If_Statement (Loc,
                       Condition       =>
                         Make_Op_Ne (Loc,
@@ -4356,7 +4353,7 @@ package body Exp_Ch7 is
                --  Generate:
                --    pragma Check (<Nam>, <Expr>, <Str>);
 
-               Create_Append (Checks,
+               Append_New_To (Checks,
                  Make_Pragma (Ploc,
                    Chars                        => Name_Check,
                    Pragma_Argument_Associations => Assoc));
@@ -4443,19 +4440,6 @@ package body Exp_Ch7 is
          end if;
       end Add_Type_Invariants;
 
-      -------------------
-      -- Create_Append --
-      -------------------
-
-      procedure Create_Append (L : in out List_Id; N : Node_Id) is
-      begin
-         if No (L) then
-            L := New_List;
-         end if;
-
-         Append_To (L, N);
-      end Create_Append;
-
       ------------------------------------
       -- Is_Untagged_Private_Derivation --
       ------------------------------------
@@ -4494,11 +4478,6 @@ package body Exp_Ch7 is
       Full_Typ : Entity_Id;
       --  The full view of the working type
 
-      Freeze_Typ : Entity_Id;
-      --  The freeze type whose freeze node carries the invariant procedure
-      --  body. This is either the partial or the full view of the working
-      --  type.
-
       Obj_Id : Entity_Id;
       --  The _object formal parameter of the invariant procedure
 
@@ -4539,10 +4518,15 @@ package body Exp_Ch7 is
 
       pragma Assert (Has_Invariants (Work_Typ));
 
+      --  ??? invariants of class-wide types are not properly implemented
+
+      if Is_Class_Wide_Type (Work_Typ) then
+         return;
+
       --  Nothing to do for interface types as their class-wide invariants are
       --  inherited by implementing types.
 
-      if Is_Interface (Work_Typ) then
+      elsif Is_Interface (Work_Typ) then
          return;
       end if;
 
@@ -4633,7 +4617,6 @@ package body Exp_Ch7 is
 
       if Partial_Invariant then
          pragma Assert (Present (Priv_Typ));
-         Freeze_Typ := Priv_Typ;
 
          Add_Type_Invariants
            (Priv_Typ => Priv_Typ,
@@ -4650,7 +4633,6 @@ package body Exp_Ch7 is
 
       else
          pragma Assert (Present (Full_Typ));
-         Freeze_Typ := Full_Typ;
 
          --  Check the invariants of the partial view by calling the "partial"
          --  invariant procedure. Generate:
@@ -4658,7 +4640,7 @@ package body Exp_Ch7 is
          --    <Work_Typ>Partial_Invariant (_object);
 
          if Present (Part_Proc) then
-            Create_Append (Stmts,
+            Append_New_To (Stmts,
               Make_Procedure_Call_Statement (Loc,
                 Name                   => New_Occurrence_Of (Part_Proc, Loc),
                 Parameter_Associations => New_List (
@@ -4793,7 +4775,7 @@ package body Exp_Ch7 is
       --  Otherwise the body is part of the freezing actions of the type
 
       else
-         Append_Freeze_Action (Freeze_Typ, Proc_Body);
+         Append_Freeze_Action (Work_Typ, Proc_Body);
       end if;
 
       Ghost_Mode := Save_Ghost_Mode;
@@ -4860,10 +4842,15 @@ package body Exp_Ch7 is
 
       pragma Assert (Has_Invariants (Work_Typ));
 
+      --  ??? invariants of class-wide types are not properly implemented
+
+      if Is_Class_Wide_Type (Work_Typ) then
+         return;
+
       --  Nothing to do for interface types as their class-wide invariants are
       --  inherited by implementing types.
 
-      if Is_Interface (Work_Typ) then
+      elsif Is_Interface (Work_Typ) then
          return;
 
       --  Nothing to do if the type already has a "partial" invariant procedure

gcc/ada/exp_util.ads

@@ -247,6 +247,39 @@ package Exp_Util is
    --  inlining of the abort undefer routine. Note that this routine does
    --  not install a call to Abort_Defer.
 
+   procedure Build_Class_Wide_Expression
+     (Prag        : Node_Id;
+      Subp        : Entity_Id;
+      Par_Subp    : Entity_Id;
+      Adjust_Sloc : Boolean);
+   --  Build the expression for an inherited class-wide condition. Prag is
+   --  the pragma constructed from the corresponding aspect of the parent
+   --  subprogram, and Subp is the overriding operation and Par_Subp is
+   --  the overridden operation that has the condition. Adjust_Sloc is True
+   --  when the sloc of nodes traversed should be adjusted for the inherited
+   --  pragma. The routine is also called to check whether an inherited
+   --  operation that is not overridden but has inherited conditions need
+   --  a wrapper, because the inherited condition includes calls to other
+   --  primitives that have been overridden. In that case the first argument
+   --  is the expression of the original class-wide aspect. In SPARK_Mode, such
+   --  operation which are just inherited but have modified pre/postconditions
+   --  are illegal.
+
+   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
+   --  parameter.
+
+   procedure Build_DIC_Procedure_Body (Typ : Entity_Id);
+   --  Create the body of the procedure which verifies the assertion expression
+   --  of pragma Default_Initial_Condition at runtime.
+
+   procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id);
+   --  Create the declaration of the procedure which verifies the assertion
+   --  expression of pragma Default_Initial_Condition at runtime.
+
    procedure Build_Procedure_Form (N : Node_Id);
    --  Create a procedure declaration which emulates the behavior of a function
    --  that returns an array type, for C-compatible generation.
@@ -1055,6 +1088,21 @@ package Exp_Util is
    --  is conservative, in that a result of False is decisive. A result of True
    --  means that such a component may or may not be present.
 
+   procedure Update_Primitives_Mapping
+     (Inher_Id : Entity_Id;
+      Subp_Id  : Entity_Id);
+   --  Map primitive operations of the parent type to the corresponding
+   --  operations of the descendant. Note that the descendant type may not be
+   --  frozen yet, so we cannot use the dispatch table directly. This is called
+   --  when elaborating a contract for a subprogram, and when freezing a type
+   --  extension to verify legality rules on inherited conditions.
+
+   procedure Update_Primitives_Mapping_Of_Types
+     (Par_Typ   : Entity_Id;
+      Deriv_Typ : Entity_Id);
+   --  Map the primitive operations of parent type Par_Typ to the corresponding
+   --  primitives of derived type Deriv_Typ.
+
    function Within_Case_Or_If_Expression (N : Node_Id) return Boolean;
    --  Determine whether arbitrary node N is within a case or an if expression
 

gcc/ada/nlists.adb

@@ -203,7 +203,6 @@ package body Nlists is
    -----------------
 
    procedure Append_List (List : List_Id; To : List_Id) is
-
       procedure Append_List_Debug;
       pragma Inline (Append_List_Debug);
       --  Output debug information if Debug_Flag_N set
@@ -269,6 +268,28 @@ package body Nlists is
       Append_List (List, To);
    end Append_List_To;
 
+   ----------------
+   -- Append_New --
+   ----------------
+
+   procedure Append_New (Node : Node_Or_Entity_Id; To : in out List_Id) is
+   begin
+      if No (To) then
+         To := New_List;
+      end if;
+
+      Append (Node, To);
+   end Append_New;
+
+   -------------------
+   -- Append_New_To --
+   -------------------
+
+   procedure Append_New_To (To : in out List_Id; Node : Node_Or_Entity_Id) is
+   begin
+      Append_New (Node, To);
+   end Append_New_To;
+
    ---------------
    -- Append_To --
    ---------------

gcc/ada/nlists.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2014, 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- --
@@ -229,6 +229,16 @@ package Nlists is
    --  An attempt to append an error node is ignored without complaint and the
    --  list is unchanged.
 
+   procedure Append_New (Node : Node_Or_Entity_Id; To : in out List_Id);
+   pragma Inline (Append_New);
+   --  Appends Node at the end of node list To. If To is non-existent list, a
+   --  list is created. Node must be a non-empty node that is not already a
+   --  member of a node list, and To must be a node list.
+
+   procedure Append_New_To (To : in out List_Id; Node : Node_Or_Entity_Id);
+   pragma Inline (Append_New_To);
+   --  Like Append_New, but the arguments are in reverse order
+
    procedure Append_To (To : List_Id; Node : Node_Or_Entity_Id);
    pragma Inline (Append_To);
    --  Like Append, but arguments are the other way round

gcc/ada/sem_ch7.adb

@@ -39,6 +39,7 @@ with Exp_Ch7;   use Exp_Ch7;
 with Exp_Disp;  use Exp_Disp;
 with Exp_Dist;  use Exp_Dist;
 with Exp_Dbug;  use Exp_Dbug;
+with Exp_Util;  use Exp_Util;
 with Freeze;    use Freeze;
 with Ghost;     use Ghost;
 with Lib;       use Lib;
@@ -1453,19 +1454,12 @@ package body Sem_Ch7 is
 
          if Is_Type (E) then
 
-            --  Each private type subject to pragma Default_Initial_Condition
-            --  declares a specialized procedure which verifies the assumption
-            --  of the pragma. The declaration appears in the visible part of
-            --  the package to allow for being called from the outside.
+            --  Preanalyze and resolve the Default_Initial_Condition assertion
+            --  expression at the end of the visible declarations to catch any
+            --  errors.
 
-            if Has_Default_Init_Cond (E) then
-               Build_Default_Init_Cond_Procedure_Declaration (E);
-
-            --  A private extension inherits the default initial condition
-            --  procedure from its parent type.
-
-            elsif Has_Inherited_Default_Init_Cond (E) then
-               Inherit_Default_Init_Cond_Procedure (E);
+            if Has_DIC (E) then
+               Build_DIC_Procedure_Body (E);
             end if;
 
             --  Preanalyze and resolve the invariants of a private type at the
@@ -1661,18 +1655,28 @@ package body Sem_Ch7 is
               ("full view of & does not have preelaborable initialization", E);
          end if;
 
-         --  Preanalyze and resolve the invariants of a private type's full
-         --  view at the end of the private declarations in case freezing did
-         --  not take place either due to errors or because the context is a
-         --  generic unit.
+         if Is_Type (E) and then Serious_Errors_Detected > 0 then
 
-         if Is_Type (E)
-           and then not Is_Private_Type (E)
-           and then Has_Private_Declaration (E)
-           and then Has_Invariants (E)
-           and then Serious_Errors_Detected > 0
-         then
-            Build_Invariant_Procedure_Body (E);
+            --  Preanalyze and resolve the Default_Initial_Condition assertion
+            --  expression at the end of the private declarations when freezing
+            --  did not take place due to errors or because the context is a
+            --  generic unit.
+
+            if Has_DIC (E) then
+               Build_DIC_Procedure_Body (E);
+            end if;
+
+            --  Preanalyze and resolve the invariants of a private type's full
+            --  view at the end of the private declarations in case freezing
+            --  did not take place either due to errors or because the context
+            --  is a generic unit.
+
+            if not Is_Private_Type (E)
+              and then Has_Private_Declaration (E)
+              and then Has_Invariants (E)
+            then
+               Build_Invariant_Procedure_Body (E);
+            end if;
          end if;
 
          Next_Entity (E);
@@ -2630,6 +2634,16 @@ package body Sem_Ch7 is
 
          Set_Freeze_Node (Priv, Freeze_Node (Full));
 
+         --  Propagate Default_Initial_Condition-related attributes from the
+         --  base type of the full view to the full view and vice versa. This
+         --  may seem strange, but is necessary depending on which type
+         --  triggered the generation of the DIC procedure body. As a result,
+         --  both the full view and its base type carry the same DIC-related
+         --  information.
+
+         Propagate_DIC_Attributes (Full, From_Typ => Full_Base);
+         Propagate_DIC_Attributes (Full_Base, From_Typ => Full);
+
          --  Propagate invariant-related attributes from the base type of the
          --  full view to the full view and vice versa. This may seem strange,
          --  but is necessary depending on which type triggered the generation

gcc/ada/sem_ch9.adb

@@ -2212,6 +2212,11 @@ package body Sem_Ch9 is
             Set_Must_Have_Preelab_Init (T);
          end if;
 
+         --  Propagate Default_Initial_Condition-related attributes from the
+         --  private type to the protected type.
+
+         Propagate_DIC_Attributes (T, From_Typ => Def_Id);
+
          --  Propagate invariant-related attributes from the private type to
          --  the protected type.
 
@@ -3146,6 +3151,11 @@ package body Sem_Ch9 is
             Set_Must_Have_Preelab_Init (T);
          end if;
 
+         --  Propagate Default_Initial_Condition-related attributes from the
+         --  private type to the task type.
+
+         Propagate_DIC_Attributes (T, From_Typ => Def_Id);
+
          --  Propagate invariant-related attributes from the private type to
          --  task type.
 

gcc/ada/sem_elab.adb

@@ -1016,7 +1016,7 @@ package body Sem_Elab is
          return;
       end if;
 
-      Is_DIC_Proc := Is_Nontrivial_Default_Init_Cond_Procedure (Ent);
+      Is_DIC_Proc := Is_Nontrivial_DIC_Procedure (Ent);
 
       --  Elaboration issues in SPARK are reported only for source constructs
       --  and for nontrivial Default_Initial_Condition procedures. The latter

gcc/ada/sem_prag.ads

@@ -244,24 +244,6 @@ package Sem_Prag is
    procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
    --  Perform preanalysis of pragma Test_Case
 
-   procedure Build_Class_Wide_Expression
-     (Prag        : Node_Id;
-      Subp        : Entity_Id;
-      Par_Subp    : Entity_Id;
-      Adjust_Sloc : Boolean);
-   --  Build the expression for an inherited class-wide condition. Prag is
-   --  the pragma constructed from the corresponding aspect of the parent
-   --  subprogram, and Subp is the overriding operation and Par_Subp is
-   --  the overridden operation that has the condition. Adjust_Sloc is True
-   --  when the sloc of nodes traversed should be adjusted for the inherited
-   --  pragma. The routine is also called to check whether an inherited
-   --  operation that is not overridden but has inherited conditions need
-   --  a wrapper, because the inherited condition includes calls to other
-   --  primitives that have been overridden. In that case the first argument
-   --  is the expression of the original class-wide aspect. In SPARK_Mode, such
-   --  operation which are just inherited but have modified pre/postconditions
-   --  are illegal.
-
    function Build_Pragma_Check_Equivalent
      (Prag           : Node_Id;
       Subp_Id        : Entity_Id := Empty;
@@ -543,13 +525,4 @@ package Sem_Prag is
    --
    --    Empty if there is no such argument
 
-   procedure Update_Primitives_Mapping
-     (Inher_Id : Entity_Id;
-      Subp_Id  : Entity_Id);
-   --  Map primitive operations of the parent type to the corresponding
-   --  operations of the descendant. Note that the descendant type may not be
-   --  frozen yet, so we cannot use the dispatch table directly. This is called
-   --  when elaborating a contract for a subprogram, and when freezing a type
-   --  extension to verify legality rules on inherited conditions.
-
 end Sem_Prag;

gcc/ada/sem_util.ads

@@ -209,24 +209,6 @@ package Sem_Util is
    --  Determine whether a selected component has a type that depends on
    --  discriminants, and build actual subtype for it if so.
 
-   function Build_Default_Init_Cond_Call
-     (Loc    : Source_Ptr;
-      Obj_Id : Entity_Id;
-      Typ    : Entity_Id) return Node_Id;
-   --  Build a call to the default initial condition procedure of type Typ with
-   --  Obj_Id as the actual parameter.
-
-   procedure Build_Default_Init_Cond_Procedure_Bodies (Priv_Decls : List_Id);
-   --  Inspect the contents of private declarations Priv_Decls and build the
-   --  bodies the default initial condition procedures for all types subject
-   --  to pragma Default_Initial_Condition.
-
-   procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id);
-   --  If private type Typ is subject to pragma Default_Initial_Condition,
-   --  build the declaration of the procedure which verifies the assumption
-   --  of the pragma at runtime. The declaration is inserted after the related
-   --  pragma.
-
    function Build_Default_Subtype
      (T : Entity_Id;
       N : Node_Id) return Entity_Id;
@@ -1266,10 +1248,6 @@ package Sem_Util is
    --  either the value is not yet known before back-end processing or it is
    --  not known at compile time after back-end processing.
 
-   procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id);
-   --  Inherit the default initial condition procedure from the parent type of
-   --  derived type Typ.
-
    procedure Inherit_Rep_Item_Chain (Typ : Entity_Id; From_Typ : Entity_Id);
    --  Inherit the rep item chain of type From_Typ without clobbering any
    --  existing rep items on Typ's chain. Typ is the destination type.
@@ -1528,8 +1506,7 @@ package Sem_Util is
    --  parameter of the current enclosing subprogram.
    --  Why are OUT parameters not considered here ???
 
-   function Is_Nontrivial_Default_Init_Cond_Procedure
-     (Id : Entity_Id) return Boolean;
+   function Is_Nontrivial_DIC_Procedure (Id : Entity_Id) return Boolean;
    --  Determine whether entity Id denotes the procedure that verifies the
    --  assertion expression of pragma Default_Initial_Condition and if it does,
    --  the encapsulated expression is nontrivial.
@@ -1751,6 +1728,10 @@ package Sem_Util is
    --  default is True since this routine is commonly invoked as part of the
    --  semantic analysis and it must not be disturbed by the rewriten nodes.
 
+   function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean;
+   --  Determine whether pragma Default_Initial_Condition denoted by Prag has
+   --  an assertion expression which should be verified at runtime.
+
    function Is_Visibly_Controlled (T : Entity_Id) return Boolean;
    --  Check whether T is derived from a visibly controlled type. This is true
    --  if the root type is declared in Ada.Finalization. If T is derived
@@ -2050,12 +2031,6 @@ package Sem_Util is
    --  parameter Ent gives the entity to which the End_Label refers,
    --  and to which cross-references are to be generated.
 
-   procedure Propagate_Invariant_Attributes
-     (Typ      : Entity_Id;
-      From_Typ : Entity_Id);
-   --  Inherit all invariant-related attributes form type From_Typ. Typ is the
-   --  destination type.
-
    procedure Propagate_Concurrent_Flags
      (Typ      : Entity_Id;
       Comp_Typ : Entity_Id);
@@ -2065,6 +2040,18 @@ package Sem_Util is
    --  by one of these flags. This procedure can only set flags for Typ, and
    --  never clear them. Comp_Typ is the type of a component or a parent.
 
+   procedure Propagate_DIC_Attributes
+     (Typ      : Entity_Id;
+      From_Typ : Entity_Id);
+   --  Inherit all Default_Initial_Condition-related attributes from type
+   --  From_Typ. Typ is the destination type.
+
+   procedure Propagate_Invariant_Attributes
+     (Typ      : Entity_Id;
+      From_Typ : Entity_Id);
+   --  Inherit all invariant-related attributes form type From_Typ. Typ is the
+   --  destination type.
+
    procedure Record_Possible_Part_Of_Reference
      (Var_Id : Entity_Id;
       Ref    : Node_Id);

gcc/ada/sem_warn.adb

@@ -1702,20 +1702,21 @@ package body Sem_Warn is
       -----------------------------
 
       function Is_OK_Fully_Initialized return Boolean is
+         Prag : Node_Id;
+
       begin
          if Is_Access_Type (Typ) and then Is_Dereferenced (N) then
             return False;
 
-         --  If a type has Default_Initial_Condition set, or it inherits it,
-         --  DIC might be specified with a boolean value, meaning that the type
-         --  is considered to be fully default initialized (SPARK RM 3.1 and
-         --  SPARK RM 7.3.3). To avoid generating spurious warnings in this
-         --  case, consider all types with DIC as fully initialized.
+         --  A type subject to pragma Default_Initial_Condition is fully
+         --  default initialized when the pragma appears with a non-null
+         --  argument (SPARK RM 3.1 and SPARK RM 7.3.3).
 
-         elsif Has_Default_Init_Cond (Typ)
-           or else Has_Inherited_Default_Init_Cond (Typ)
-         then
-            return True;
+         elsif Has_DIC (Typ) then
+            Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+            pragma Assert (Present (Prag));
+
+            return Is_Verifiable_DIC_Pragma (Prag);
 
          else
             return Is_Fully_Initialized_Type (Typ);

gcc/ada/sinfo.adb

@@ -1284,6 +1284,14 @@ package body Sinfo is
       return Node3 (N);
    end Expression;
 
+   function Expression_Copy
+      (N : Node_Id) return Node_Id is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Pragma_Argument_Association);
+      return Node2 (N);
+   end Expression_Copy;
+
    function Expressions
       (N : Node_Id) return List_Id is
    begin
@@ -4555,6 +4563,14 @@ package body Sinfo is
       Set_Node3_With_Parent (N, Val);
    end Set_Expression;
 
+   procedure Set_Expression_Copy
+      (N : Node_Id; Val : Node_Id) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Pragma_Argument_Association);
+      Set_Node2 (N, Val);  -- semantic field, no parent set
+   end Set_Expression_Copy;
+
    procedure Set_Expressions
       (N : Node_Id; Val : List_Id) is
    begin

gcc/ada/sinfo.ads

@@ -1281,6 +1281,12 @@ package Sinfo is
    --    target of the assignment or initialization is used to generate the
    --    left-hand side of individual assignment to each sub-component.
 
+   --  Expression_Copy (Node2-Sem)
+   --    Present in N_Pragma_Argument_Association nodes. Contains a copy of the
+   --    original expression. This field is best used to store pragma-dependent
+   --    modifications performed on the original expression such as replacement
+   --    of the current type instance or substitutions of primitives.
+
    --  First_Inlined_Subprogram (Node3-Sem)
    --    Present in the N_Compilation_Unit node for the main program. Points
    --    to a chain of entities for subprograms that are to be inlined. The
@@ -2571,6 +2577,7 @@ package Sinfo is
       --  N_Pragma_Argument_Association
       --  Sloc points to first token in association
       --  Chars (Name1) (set to No_Name if no pragma argument identifier)
+      --  Expression_Copy (Node2-Sem)
       --  Expression (Node3)
 
       ------------------------
@@ -9181,6 +9188,9 @@ package Sinfo is
    function Expression
      (N : Node_Id) return Node_Id;    -- Node3
 
+   function Expression_Copy
+     (N : Node_Id) return Node_Id;    -- Node2
+
    function Expressions
      (N : Node_Id) return List_Id;    -- List1
 
@@ -10227,6 +10237,9 @@ package Sinfo is
    procedure Set_Expression
      (N : Node_Id; Val : Node_Id);            -- Node3
 
+   procedure Set_Expression_Copy
+     (N : Node_Id; Val : Node_Id);            -- Node2
+
    procedure Set_Expressions
      (N : Node_Id; Val : List_Id);            -- List1
 
@@ -11082,7 +11095,7 @@ package Sinfo is
 
      N_Pragma_Argument_Association =>
        (1 => True,    --  Chars (Name1)
-        2 => False,   --  unused
+        2 => False,   --  Expression_Copy (Node2-Sem)
         3 => True,    --  Expression (Node3)
         4 => False,   --  unused
         5 => False),  --  unused
@@ -12544,14 +12557,14 @@ package Sinfo is
         5 => False),  --  unused
 
      N_Push_Program_Error_Label =>
-       (1 => False,   --  Exception_Label
+       (1 => False,   --  unused
         2 => False,   --  unused
         3 => False,   --  unused
         4 => False,   --  unused
         5 => False),  --  Exception_Label
 
      N_Push_Storage_Error_Label =>
-       (1 => False,   --  Exception_Label
+       (1 => False,   --  unused
         2 => False,   --  unused
         3 => False,   --  unused
         4 => False,   --  unused
@@ -12790,6 +12803,7 @@ package Sinfo is
    pragma Inline (Explicit_Actual_Parameter);
    pragma Inline (Explicit_Generic_Actual_Parameter);
    pragma Inline (Expression);
+   pragma Inline (Expression_Copy);
    pragma Inline (Expressions);
    pragma Inline (First_Bit);
    pragma Inline (First_Inlined_Subprogram);
@@ -13136,6 +13150,7 @@ package Sinfo is
    pragma Inline (Set_Explicit_Actual_Parameter);
    pragma Inline (Set_Explicit_Generic_Actual_Parameter);
    pragma Inline (Set_Expression);
+   pragma Inline (Set_Expression_Copy);
    pragma Inline (Set_Expressions);
    pragma Inline (Set_First_Bit);
    pragma Inline (Set_First_Inlined_Subprogram);