diff mbox

[Ada] Aspect/pragma Default_Initial_Condition

Message ID 20140804100009.GA24038@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2014, 10 a.m. UTC
This patch implements aspect/pragma Default_Initial_Condition. The construct
has the following semantics and runtime behavior:

The Default_Initial_Condition aspect is introduced by an aspect_specification
where the aspect_mark is Default_Initial_Condition. The aspect may be specified
only as part the aspect_specification of a private_type_declaration. The
aspect_definition, if any, of such an aspect specification shall be either a
null literal or a Boolean_expression.

The aspect_definition may be omitted; this is semantically equivalent to
specifying a static Boolean_expression having the value True. An aspect
specification of "null" indicates that the partial view of the type does not
define full default initialization.

Conversely, an aspect specification of a Boolean_expression indicates that the
partial view of the type does define full default initialization. In this case,
the completion of the private type shall define full default initialization.
Unlike the null literal case, this case has associated dynamic semantics. The
Boolean_expression (which might typically mention the current instance of the
type, although this is not required) is an assertion which is checked (at run
time) after any object of the given type (or of any descendant of the given
type for which the specified aspect is inherited and not overridden), is
?–?
8?ninitialized by default?–?
8?o (see Ada RM 3.3.1).

The Boolean_expression, if any, causes freezing in the same way as the
default_expression of a component_declaration.

Default_Initial_Condition assertion is an assertion aspect, which means that it
may be used in an Assertion_Policy pragma.

------------
-- Source --
------------

--  checker.ads

generic
   type Typ is private;
   Test : String;
procedure Checker;

--  checker.adb

with Ada.Assertions; use Ada.Assertions;
with Ada.Exceptions; use Ada.Exceptions;
with Ada.Text_IO;    use Ada.Text_IO;

procedure Checker is
begin
   declare
      Obj : Typ;
      pragma Unreferenced (Obj);
   begin
      Put_Line ("ERROR " & Test & ": Assertion_Error not raised");
   end;

exception
   when Ex : Assertion_Error =>
      Put_Line (Test & " OK");
      Put_Line (Exception_Information (Ex));

   when others =>
      Put_Line ("ERROR " & Test & ": unexpected exception");
end Checker;

--  derivations.ads

package Derivations is
   type T1 is tagged private
     with Default_Initial_Condition => Crash_1 (T1);
   type T2 is new T1 with private;      --  inherits Crash_1
   type T3 is new T1 with private       --  overrides with Crash_3
     with Default_Initial_Condition => Crash_3 (T3);
   type T4 is new T2 with private       --  overrides with Crash_4
     with Default_Initial_Condition => Crash_4 (T4);

   function Crash_1 (Obj : T1) return Boolean;
   function Crash_3 (Obj : T3) return Boolean;
   function Crash_4 (Obj : T4) return Boolean;
   procedure Force_Body;

private
   type T1 is tagged null record;
   function Crash_1 (Obj : T1) return Boolean is (False);
   type T2 is new T1 with null record;
   type T3 is new T1 with null record;
   function Crash_3 (Obj : T3) return Boolean is (False);
   type T4 is new T2 with null record;
   function Crash_4 (Obj : T4) return Boolean is (False);

   type T5 is new T1 with null record;  --  inherits Crash_1
   type T6 is new T2 with null record;  --  inherits Crash_2
   type T7 is new T3 with null record;  --  inherits Crash_3
   type T8 is new T4 with null record;  --  inherits Crash_4

   subtype T9  is T5;                   --  inherits Crash_1
   subtype T10 is T6;                   --  inherits Crash_2
   subtype T11 is T7;                   --  inherits Crash_3
   subtype T12 is T8;                   --  inherits Crash_4
end Derivations;

--  derivations.adb

with Checker;

package body Derivations is
   procedure Check_T1  is new Checker (T1,  "Test 1");
   procedure Check_T2  is new Checker (T2,  "Test 2");
   procedure Check_T3  is new Checker (T3,  "Test 3");
   procedure Check_T4  is new Checker (T4,  "Test 4");
   procedure Check_T5  is new Checker (T5,  "Test 5");
   procedure Check_T6  is new Checker (T6,  "Test 6");
   procedure Check_T7  is new Checker (T7,  "Test 7");
   procedure Check_T8  is new Checker (T8,  "Test 8");
   procedure Check_T9  is new Checker (T9,  "Test 9");
   procedure Check_T10 is new Checker (T10, "Test 10");
   procedure Check_T11 is new Checker (T11, "Test 11");
   procedure Check_T12 is new Checker (T12, "Test 12");
   procedure Force_Body is begin null; end Force_Body;

begin
   Check_T1;
   Check_T2;
   Check_T3;
   Check_T4;
   Check_T5;
   Check_T6;
   Check_T7;
   Check_T8;
   Check_T9;
   Check_T10;
   Check_T11;
   Check_T12;
end Derivations;

--  runtime_checks.adb

with Derivations;

procedure Runtime_Checks is begin null; end Runtime_Checks;

----------------------------
-- Compilation and output --
----------------------------

$ gnatmake -q -gnata runtime_checks.adb
$ ./runtime_checks
Test 1 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 2 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 3 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:6

Test 4 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:8

Test 5 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 6 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 7 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:6

Test 8 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:8

Test 9 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 10 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 11 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:6

Test 12 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:8

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb Add an entry in table Canonical_Aspect for
	Default_Initial_Condition.
	* aspects.ads Add an entry in tables Aspect_Id, Aspect_Argument,
	Aspect_Names and Aspect_Delay for Default_Initial_Condition.
	* einfo.adb Flag3 is now Has_Default_Init_Cond. Flag132
	is now Is_Default_Init_Cond_ Procedure. Flag133 is now
	Has_Inherited_Default_Init_Cond.
	(Default_Init_Cond_Procedure): New routine.
	(Has_Default_Init_Cond): New routine.
	(Has_Inherited_Default_Init_Cond): New routine.
	(Is_Default_Init_Cond_Procedure): New routine.
	(Set_Default_Init_Cond_Procedure): New routine.
	(Set_Has_Default_Init_Cond): New routine.
	(Set_Has_Inherited_Default_Init_Cond): New routine.
	(Set_Is_Default_Init_Cond_Procedure): New routine.
	(Write_Entity_Flags): Output all the new flags.
	* einfo.ads New attributes Default_Init_Cond_Procedure,
	Has_Inherited_Default_Init_Cond and Is_Default_Init_Cond_Procedure
	along with usage in nodes.
	(Default_Init_Cond_Procedure): New routine.
	(Has_Default_Init_Cond): New routine and pragma Inline.
	(Has_Inherited_Default_Init_Cond): New routine and
	pragma Inline.
	(Is_Default_Init_Cond_Procedure): New routine and
	pragma Inline.
	(Set_Default_Init_Cond_Procedure): New routine.
	(Set_Has_Default_Init_Cond): New routine and pragma Inline.
	(Set_Has_Inherited_Default_Init_Cond): New routine and pragma Inline.
	(Set_Is_Default_Init_Cond_Procedure): New routine and pragma Inline.
	* exp_ch3.adb (Expand_N_Object_Declaration): New constant
	Next_N. Generate a call to the default initial condition procedure
	if the object's type is subject to the pragma.	(Freeze_Type):
	Generate the body of the default initial condition procedure or
	inherit the spec from a parent type.
	* exp_ch7.adb Add with and use clause for Exp_Prag.
	(Expand_Pragma_Initial_Condition): Removed.
	* exp_prag.ads, exp_prag.adb (Expand_Pragma_Initial_Condition): New
	routine.
	* par-prag.adb (Prag): Pragma Default_Initial_Condition does
	not need special treatment by the parser.
	* sem_ch3.adb (Build_Derived_Record_Type): Propagate the
	attributes related to pragma Default_Initial_Condition to the
	derived type.
	(Process_Full_View): Propagate the attributes
	related to pragma Default_Initial_Condition to the full view.
	* sem_ch7.adb (Analyze_Package_Specification): Build the
	declaration of the default initial condition procedure for all
	types that qualify or inherit the one from the parent type.
	* sem_ch13.adb (Analyze_Aspect_Specifications):
	Add processing for aspect Default_Initial_Condition.
	(Check_Aspect_At_Freeze_Point): Aspect
	Default_Initial_Condition does not require delayed analysis.
	(Replace_Type_References_Generic): Moved to spec.
	* sem_ch13.ads (Replace_Type_References_Generic): Moved from body.
	* sem_prag.adb Add an entry in table Sif_Glags for
	Default_Initial_Condition.
	(Analyze_Pragma): Pragma
	Default_Initial_Condition is now part of assertion
	policy. Add processing for pragma Default_Initial_Condition.
	(Is_Valid_Assertion_Kind): Pragma Default_Initial_Condition is
	now recognized as a proper assertion policy.
	* sem_util.ads, sem_util.adb (Build_Default_Init_Cond_Call): New
	routine.
	(Build_Default_Init_Cond_Procedure_Body): New routine.
	(Build_Default_Init_Cond_Procedure_Declaration): New routine.
	(Inherit_Default_Init_Cond_Procedure): New routine.
	* snames.ads-tmpl Add new predefined name and pragma id for
	Default_Initial_Condition.
diff mbox

Patch

Index: exp_prag.adb
===================================================================
--- exp_prag.adb	(revision 213536)
+++ exp_prag.adb	(working copy)
@@ -1152,17 +1152,17 @@ 
       --  Insert the pragma
 
       Insert_After_And_Analyze (N,
-         Make_Pragma (Loc,
-           Chars                        => Name_Machine_Attribute,
-           Pragma_Argument_Associations => New_List (
-             Make_Pragma_Argument_Association (Iloc,
-               Expression => New_Copy_Tree (Internal)),
-             Make_Pragma_Argument_Association (Eloc,
-               Expression =>
-                 Make_String_Literal (Sloc => Ploc,
-                   Strval => "common_object")),
-             Make_Pragma_Argument_Association (Ploc,
-               Expression => New_Copy_Tree (Psect)))));
+        Make_Pragma (Loc,
+          Chars                        => Name_Machine_Attribute,
+          Pragma_Argument_Associations => New_List (
+            Make_Pragma_Argument_Association (Iloc,
+              Expression => New_Copy_Tree (Internal)),
+            Make_Pragma_Argument_Association (Eloc,
+              Expression =>
+                Make_String_Literal (Sloc => Ploc,
+                  Strval => "common_object")),
+            Make_Pragma_Argument_Association (Ploc,
+              Expression => New_Copy_Tree (Psect)))));
    end Expand_Pragma_Common_Object;
 
    ---------------------------------------
@@ -1283,6 +1283,88 @@ 
       end if;
    end Expand_Pragma_Import_Or_Interface;
 
+   -------------------------------------
+   -- Expand_Pragma_Initial_Condition --
+   -------------------------------------
+
+   procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
+      Loc       : constant Source_Ptr := Sloc (Spec_Or_Body);
+      Check     : Node_Id;
+      Expr      : Node_Id;
+      Init_Cond : Node_Id;
+      List      : List_Id;
+      Pack_Id   : Entity_Id;
+
+   begin
+      if Nkind (Spec_Or_Body) = N_Package_Body then
+         Pack_Id := Corresponding_Spec (Spec_Or_Body);
+
+         if Present (Handled_Statement_Sequence (Spec_Or_Body)) then
+            List := Statements (Handled_Statement_Sequence (Spec_Or_Body));
+
+         --  The package body lacks statements, create an empty list
+
+         else
+            List := New_List;
+
+            Set_Handled_Statement_Sequence (Spec_Or_Body,
+              Make_Handled_Sequence_Of_Statements (Loc, Statements => List));
+         end if;
+
+      elsif Nkind (Spec_Or_Body) = N_Package_Declaration then
+         Pack_Id := Defining_Entity (Spec_Or_Body);
+
+         if Present (Visible_Declarations (Specification (Spec_Or_Body))) then
+            List := Visible_Declarations (Specification (Spec_Or_Body));
+
+         --  The package lacks visible declarations, create an empty list
+
+         else
+            List := New_List;
+
+            Set_Visible_Declarations (Specification (Spec_Or_Body), List);
+         end if;
+
+      --  This routine should not be used on anything other than packages
+
+      else
+         raise Program_Error;
+      end if;
+
+      Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
+
+      --  The caller should check whether the package is subject to pragma
+      --  Initial_Condition.
+
+      pragma Assert (Present (Init_Cond));
+
+      Expr :=
+        Get_Pragma_Arg (First (Pragma_Argument_Associations (Init_Cond)));
+
+      --  The assertion expression was found to be illegal, do not generate the
+      --  runtime check as it will repeat the illegality.
+
+      if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
+         return;
+      end if;
+
+      --  Generate:
+      --    pragma Check (Initial_Condition, <Expr>);
+
+      Check :=
+        Make_Pragma (Loc,
+          Chars                        => Name_Check,
+          Pragma_Argument_Associations => New_List (
+            Make_Pragma_Argument_Association (Loc,
+              Expression => Make_Identifier (Loc, Name_Initial_Condition)),
+
+            Make_Pragma_Argument_Association (Loc,
+              Expression => New_Copy_Tree (Expr))));
+
+      Append_To (List, Check);
+      Analyze (Check);
+   end Expand_Pragma_Initial_Condition;
+
    ------------------------------------
    -- Expand_Pragma_Inspection_Point --
    ------------------------------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 213537)
+++ sem_ch3.adb	(working copy)
@@ -92,8 +92,8 @@ 
    --  record type.
 
    procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
-   --  Analyze all delayed aspects chained on the contract of object Obj_Id as
-   --  if they appeared at the end of the declarative region. The aspects to be
+   --  Analyze all delayed pragmas chained on the contract of object Obj_Id as
+   --  if they appeared at the end of the declarative region. The pragmas to be
    --  considered are:
    --    Async_Readers
    --    Async_Writers
@@ -8508,6 +8508,23 @@ 
       end if;
 
       Check_Function_Writable_Actuals (N);
+
+      --  Propagate the attributes related to pragma Default_Initial_Condition
+      --  from the parent type to the private extension. A derived type always
+      --  inherits the default initial condition flag from the parent type. If
+      --  the derived type carries its own Default_Initial_Condition pragma,
+      --  the flag is later reset in Analyze_Pragma. Note that both flags are
+      --  mutually exclusive.
+
+      if Has_Inherited_Default_Init_Cond (Parent_Type)
+        or else Present (Get_Pragma
+                  (Parent_Type, Pragma_Default_Initial_Condition))
+      then
+         Set_Has_Inherited_Default_Init_Cond (Derived_Type);
+
+      elsif Has_Default_Init_Cond (Parent_Type) then
+         Set_Has_Default_Init_Cond (Derived_Type);
+      end if;
    end Build_Derived_Record_Type;
 
    ------------------------
@@ -18945,6 +18962,21 @@ 
          Set_Has_Specified_Stream_Output (Full_T);
       end if;
 
+      --  Propagate the attributes related to pragma Default_Initial_Condition
+      --  from the private to the full view. Note that both flags are mutually
+      --  exclusive.
+
+      if Has_Inherited_Default_Init_Cond (Priv_T) then
+         Set_Has_Inherited_Default_Init_Cond (Full_T);
+         Set_Default_Init_Cond_Procedure
+           (Full_T, Default_Init_Cond_Procedure (Priv_T));
+
+      elsif Has_Default_Init_Cond (Priv_T) then
+         Set_Has_Default_Init_Cond (Full_T);
+         Set_Default_Init_Cond_Procedure
+           (Full_T, Default_Init_Cond_Procedure (Priv_T));
+      end if;
+
       --  Propagate invariants to full type
 
       if Has_Invariants (Priv_T) then
Index: exp_prag.ads
===================================================================
--- exp_prag.ads	(revision 213536)
+++ exp_prag.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, 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- --
@@ -42,4 +42,15 @@ 
    --  Subp_Id's body. All generated code is added to list Stmts. If Stmts is
    --  No_List on entry, a new list is created.
 
+   procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id);
+   --  Generate a runtime check needed to verify the assumption of introduced
+   --  by pragma Initial_Condition. Spec_Or_Body denotes the spec or body of
+   --  the package where the pragma appears. The check is inserted according
+   --  to the following precedence rules:
+   --    1) If the package has a body with a statement sequence, the check is
+   --       inserted at the end of the statments.
+   --    2) If the package has a body, the check is inserted at the end of the
+   --       body declarations.
+   --    3) The check is inserted at the end of the visible declarations.
+
 end Exp_Prag;
Index: exp_ch7.adb
===================================================================
--- exp_ch7.adb	(revision 213536)
+++ exp_ch7.adb	(working copy)
@@ -38,6 +38,7 @@ 
 with Exp_Dbug; use Exp_Dbug;
 with Exp_Dist; use Exp_Dist;
 with Exp_Disp; use Exp_Disp;
+with Exp_Prag; use Exp_Prag;
 with Exp_Tss;  use Exp_Tss;
 with Exp_Util; use Exp_Util;
 with Freeze;   use Freeze;
@@ -379,11 +380,6 @@ 
    --  Given an arbitrary entity, traverse the scope chain looking for the
    --  first enclosing function. Return Empty if no function was found.
 
-   procedure Expand_Pragma_Initial_Condition (N : Node_Id);
-   --  Subsidiary to the expansion of package specs and bodies. Generate a
-   --  runtime check needed to verify the assumption introduced by pragma
-   --  Initial_Condition. N denotes the package spec or body.
-
    function Make_Call
      (Loc       : Source_Ptr;
       Proc_Id   : Entity_Id;
@@ -4263,88 +4259,6 @@ 
       end if;
    end Expand_N_Package_Declaration;
 
-   -------------------------------------
-   -- Expand_Pragma_Initial_Condition --
-   -------------------------------------
-
-   procedure Expand_Pragma_Initial_Condition (N : Node_Id) is
-      Loc       : constant Source_Ptr := Sloc (N);
-      Check     : Node_Id;
-      Expr      : Node_Id;
-      Init_Cond : Node_Id;
-      List      : List_Id;
-      Pack_Id   : Entity_Id;
-
-   begin
-      if Nkind (N) = N_Package_Body then
-         Pack_Id := Corresponding_Spec (N);
-
-         if Present (Handled_Statement_Sequence (N)) then
-            List := Statements (Handled_Statement_Sequence (N));
-
-         --  The package body lacks statements, create an empty list
-
-         else
-            List := New_List;
-
-            Set_Handled_Statement_Sequence (N,
-              Make_Handled_Sequence_Of_Statements (Loc, Statements => List));
-         end if;
-
-      elsif Nkind (N) = N_Package_Declaration then
-         Pack_Id := Defining_Entity (N);
-
-         if Present (Visible_Declarations (Specification (N))) then
-            List := Visible_Declarations (Specification (N));
-
-         --  The package lacks visible declarations, create an empty list
-
-         else
-            List := New_List;
-
-            Set_Visible_Declarations (Specification (N), List);
-         end if;
-
-      --  This routine should not be used on anything other than packages
-
-      else
-         raise Program_Error;
-      end if;
-
-      Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
-
-      --  The caller should check whether the package is subject to pragma
-      --  Initial_Condition.
-
-      pragma Assert (Present (Init_Cond));
-
-      Expr :=
-        Get_Pragma_Arg (First (Pragma_Argument_Associations (Init_Cond)));
-
-      --  The assertion expression was found to be illegal, do not generate the
-      --  runtime check as it will repeat the illegality.
-
-      if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
-         return;
-      end if;
-
-      --  Generate:
-      --    pragma Check (Initial_Condition, <Expr>);
-
-      Check :=
-        Make_Pragma (Loc,
-          Chars                        => Name_Check,
-          Pragma_Argument_Associations => New_List (
-            Make_Pragma_Argument_Association (Loc,
-              Expression => Make_Identifier (Loc, Name_Initial_Condition)),
-
-            Make_Pragma_Argument_Association (Loc,
-              Expression => New_Copy_Tree (Expr))));
-
-      Append_To (List, Check);
-      Analyze (Check);
-   end Expand_Pragma_Initial_Condition;
-
    -----------------------------
    -- Find_Node_To_Be_Wrapped --
    -----------------------------
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 213537)
+++ sem_ch7.adb	(working copy)
@@ -1350,8 +1350,10 @@ 
          Analyze_Declarations (Vis_Decls);
       end if;
 
-      --  Verify that incomplete types have received full declarations and
-      --  also build invariant procedures for any types with invariants.
+      --  Inspect the entities defined in the package and ensure that all
+      --  incomplete types have received full declarations. Build default
+      --  initial condition and invariant procedures for all types that
+      --  qualify.
 
       E := First_Entity (Id);
       while Present (E) loop
@@ -1367,10 +1369,26 @@ 
             Error_Msg_N ("no declaration in visible part for incomplete}", E);
          end if;
 
-         --  Build invariant procedures
+         if Is_Type (E) then
 
-         if Is_Type (E) and then Has_Invariants (E) then
-            Build_Invariant_Procedure (E, N);
+            --  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.
+
+            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);
+            end if;
+
+            if Has_Invariants (E) then
+               Build_Invariant_Procedure (E, N);
+            end if;
          end if;
 
          Next_Entity (E);
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 213540)
+++ einfo.adb	(working copy)
@@ -270,6 +270,7 @@ 
 
    --    Is_Inlined_Always               Flag1
    --    Is_Hidden_Non_Overridden_Subpgm Flag2
+   --    Has_Default_Init_Cond           Flag3
    --    Is_Frozen                       Flag4
    --    Has_Discriminants               Flag5
    --    Is_Dispatching_Operation        Flag6
@@ -411,6 +412,8 @@ 
    --    Is_Generic_Instance             Flag130
 
    --    No_Pool_Assigned                Flag131
+   --    Is_Default_Init_Cond_Procedure  Flag132
+   --    Has_Inherited_Default_Init_Cond Flag133
    --    Has_Aliased_Components          Flag135
    --    No_Strict_Aliasing              Flag136
    --    Is_Machine_Code_Subprogram      Flag137
@@ -569,10 +572,6 @@ 
    --    No_Predicate_On_Actual          Flag275
    --    No_Dynamic_Predicate_On_Actual  Flag276
 
-   --    (unused)                        Flag3
-
-   --    (unused)                        Flag132
-   --    (unused)                        Flag133
    --    (unused)                        Flag134
 
    --    (unused)                        Flag275
@@ -1394,6 +1393,11 @@ 
       return Flag39 (Base_Type (Id));
    end Has_Default_Aspect;
 
+   function Has_Default_Init_Cond (Id : E) return B is
+   begin
+      return Flag3 (Id);
+   end Has_Default_Init_Cond;
+
    function Has_Delayed_Aspects (Id : E) return B is
    begin
       pragma Assert (Nkind (Id) in N_Entity);
@@ -1478,6 +1482,12 @@ 
       return Flag248 (Id);
    end Has_Inheritable_Invariants;
 
+   function Has_Inherited_Default_Init_Cond (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag133 (Id);
+   end Has_Inherited_Default_Init_Cond;
+
    function Has_Initial_Value (Id : E) return B is
    begin
       pragma Assert (Ekind (Id) = E_Variable or else Is_Formal (Id));
@@ -1975,6 +1985,12 @@ 
       return Flag74 (Id);
    end Is_CPP_Class;
 
+   function Is_Default_Init_Cond_Procedure (Id : E) return B is
+   begin
+      pragma Assert (Ekind_In (Id, E_Function, E_Procedure));
+      return Flag132 (Id);
+   end Is_Default_Init_Cond_Procedure;
+
    function Is_Descendent_Of_Address (Id : E) return B is
    begin
       return Flag223 (Id);
@@ -2137,7 +2153,7 @@ 
 
    function Is_Invariant_Procedure (Id : E) return B is
    begin
-      pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure);
+      pragma Assert (Ekind_In (Id, E_Function, E_Procedure));
       return Flag257 (Id);
    end Is_Invariant_Procedure;
 
@@ -4140,6 +4156,12 @@ 
       Set_Flag39 (Id, V);
    end Set_Has_Default_Aspect;
 
+   procedure Set_Has_Default_Init_Cond (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag3 (Id, V);
+   end Set_Has_Default_Init_Cond;
+
    procedure Set_Has_Delayed_Aspects (Id : E; V : B := True) is
    begin
       pragma Assert (Nkind (Id) in N_Entity);
@@ -4226,6 +4248,12 @@ 
       Set_Flag248 (Id, V);
    end Set_Has_Inheritable_Invariants;
 
+   procedure Set_Has_Inherited_Default_Init_Cond (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag133 (Id, V);
+   end Set_Has_Inherited_Default_Init_Cond;
+
    procedure Set_Has_Initial_Value (Id : E; V : B := True) is
    begin
       pragma Assert (Ekind_In (Id, E_Variable, E_Out_Parameter));
@@ -4748,6 +4776,12 @@ 
       Set_Flag74 (Id, V);
    end Set_Is_CPP_Class;
 
+   procedure Set_Is_Default_Init_Cond_Procedure (Id : E; V : B := True) is
+   begin
+      pragma Assert (Ekind (Id) = E_Procedure);
+      Set_Flag132 (Id, V);
+   end Set_Is_Default_Init_Cond_Procedure;
+
    procedure Set_Is_Descendent_Of_Address (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Type (Id));
@@ -4920,7 +4954,7 @@ 
 
    procedure Set_Is_Invariant_Procedure (Id : E; V : B := True) is
    begin
-      pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure);
+      pragma Assert (Ekind (Id) = E_Procedure);
       Set_Flag257 (Id, V);
    end Set_Is_Invariant_Procedure;
 
@@ -6410,6 +6444,31 @@ 
       end loop;
    end Declaration_Node;
 
+   ---------------------------------
+   -- Default_Init_Cond_Procedure --
+   ---------------------------------
+
+   function Default_Init_Cond_Procedure (Id : E) return E is
+      S : Entity_Id;
+
+   begin
+      pragma Assert
+        (Is_Type (Id)
+           and then (Has_Default_Init_Cond (Id)
+                       or Has_Inherited_Default_Init_Cond (Id)));
+
+      S := Subprograms_For_Type (Id);
+      while Present (S) loop
+         if Is_Default_Init_Cond_Procedure (S) then
+            return S;
+         end if;
+
+         S := Subprograms_For_Type (S);
+      end loop;
+
+      return Empty;
+   end Default_Init_Cond_Procedure;
+
    ---------------------
    -- Designated_Type --
    ---------------------
@@ -7913,6 +7972,34 @@ 
       end case;
    end Set_Component_Alignment;
 
+   -------------------------------------
+   -- Set_Default_Init_Cond_Procedure --
+   -------------------------------------
+
+   procedure Set_Default_Init_Cond_Procedure (Id : E; V : E) is
+      S : Entity_Id;
+
+   begin
+      pragma Assert
+        (Is_Type (Id)
+           and then (Has_Default_Init_Cond (Id)
+                       or Has_Inherited_Default_Init_Cond (Id)));
+
+      S := Subprograms_For_Type (Id);
+      Set_Subprograms_For_Type (Id, V);
+      Set_Subprograms_For_Type (V, S);
+
+      --  Check for a duplicate procedure
+
+      while Present (S) loop
+         if Is_Default_Init_Cond_Procedure (S) then
+            raise Program_Error;
+         end if;
+
+         S := Subprograms_For_Type (S);
+      end loop;
+   end Set_Default_Init_Cond_Procedure;
+
    -----------------------------
    -- Set_Invariant_Procedure --
    -----------------------------
@@ -8252,6 +8339,7 @@ 
       W ("Has_Controlling_Result",          Flag98  (Id));
       W ("Has_Convention_Pragma",           Flag119 (Id));
       W ("Has_Default_Aspect",              Flag39  (Id));
+      W ("Has_Default_Init_Cond",           Flag3   (Id));
       W ("Has_Delayed_Aspects",             Flag200 (Id));
       W ("Has_Delayed_Freeze",              Flag18  (Id));
       W ("Has_Delayed_Rep_Aspects",         Flag261 (Id));
@@ -8267,6 +8355,7 @@ 
       W ("Has_Implicit_Dereference",        Flag251 (Id));
       W ("Has_Independent_Components",      Flag34  (Id));
       W ("Has_Inheritable_Invariants",      Flag248 (Id));
+      W ("Has_Inherited_Default_Init_Cond", Flag133 (Id));
       W ("Has_Initial_Value",               Flag219 (Id));
       W ("Has_Invariants",                  Flag232 (Id));
       W ("Has_Loop_Entry_Attributes",       Flag260 (Id));
@@ -8327,8 +8416,7 @@ 
       W ("In_Private_Part",                 Flag45  (Id));
       W ("In_Use",                          Flag8   (Id));
       W ("Is_Abstract_Subprogram",          Flag19  (Id));
-      W ("Is_Abstract_Type",                Flag146  (Id));
-      W ("Is_Local_Anonymous_Access",       Flag194 (Id));
+      W ("Is_Abstract_Type",                Flag146 (Id));
       W ("Is_Access_Constant",              Flag69  (Id));
       W ("Is_Ada_2005_Only",                Flag185 (Id));
       W ("Is_Ada_2012_Only",                Flag199 (Id));
@@ -8350,6 +8438,7 @@ 
       W ("Is_Constructor",                  Flag76  (Id));
       W ("Is_Controlled",                   Flag42  (Id));
       W ("Is_Controlling_Formal",           Flag97  (Id));
+      W ("Is_Default_Init_Cond_Procedure",  Flag132 (Id));
       W ("Is_Descendent_Of_Address",        Flag223 (Id));
       W ("Is_Discrim_SO_Function",          Flag176 (Id));
       W ("Is_Discriminant_Check_Function",  Flag264 (Id));
@@ -8388,6 +8477,7 @@ 
       W ("Is_Limited_Composite",            Flag106 (Id));
       W ("Is_Limited_Interface",            Flag197 (Id));
       W ("Is_Limited_Record",               Flag25  (Id));
+      W ("Is_Local_Anonymous_Access",       Flag194 (Id));
       W ("Is_Machine_Code_Subprogram",      Flag137 (Id));
       W ("Is_Non_Static_Subtype",           Flag109 (Id));
       W ("Is_Null_Init_Proc",               Flag178 (Id));
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 213536)
+++ einfo.ads	(working copy)
@@ -772,6 +772,16 @@ 
 --       default expressions (see Freeze.Process_Default_Expressions), which
 --       would not only waste time, but also generate false error messages.
 
+--    Default_Init_Cond_Procedure (synthesized)
+--       Defined in all types. Set for private [sub]types subject to pragma
+--       Default_Initial_Condition, their corresponding full views and derived
+--       types with at least one parent subject to the pragma. Contains the
+--       entity of the procedure which takes a single argument of the given
+--       type and verifies the assumption of the pragma.
+--
+--       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.
+
 --    Default_Value (Node20)
 --       Defined in formal parameters. Points to the node representing the
 --       expression for the default value for the parameter. Empty if the
@@ -1474,6 +1484,17 @@ 
 --       Convention, Import, or Export has been given. Used to prevent more
 --       than one such pragma appearing for a given entity (RM B.1(45)).
 
+--    Has_Default_Aspect (Flag39) [base type only]
+--       Defined in entities for types and subtypes, set for scalar types with
+--       a Default_Value aspect and array types with a Default_Component_Value
+--       apsect. If this flag is set, then a corresponding aspect specification
+--       node will be present on the rep item chain for the entity.
+
+--    Has_Default_Init_Cond (Flag3)
+--       Defined in type and subtype entities. Set if pragma Default_Initial_
+--       Condition applies to the type or subtype. This flag must be mutually
+--       exclusive with Has_Inherited_Default_Init_Cond.
+
 --    Has_Delayed_Aspects (Flag200)
 --      Defined in all entities. Set if the Rep_Item chain for the entity has
 --      one or more N_Aspect_Definition nodes chained which are not to be
@@ -1486,12 +1507,6 @@ 
 --       node must be generated for the entity at its freezing point. See
 --       separate section ("Delayed Freezing and Elaboration") for details.
 
---    Has_Default_Aspect (Flag39) [base type only]
---       Defined in entities for types and subtypes, set for scalar types with
---       a Default_Value aspect and array types with a Default_Component_Value
---       apsect. If this flag is set, then a corresponding aspect specification
---       node will be present on the rep item chain for the entity.
-
 --    Has_Delayed_Rep_Aspects (Flag261)
 --       Defined in all type and subtypes. This flag is set if there is at
 --       least one aspect for a representation characteristic that has to be
@@ -1605,6 +1620,11 @@ 
 --       type which has inheritable invariants, and in this case the flag will
 --       also be set in the private type.
 
+--    Has_Inherited_Default_Init_Cond (Flag133)
+--       Defined in type and subtype entities. Set if a derived type inherits
+--       pragma Default_Initial_Condition from its parent type. This flag must
+--       be mutually exclusive with Had_Default_Init_Cond.
+
 --    Has_Initial_Value (Flag219)
 --       Defined in entities for variables and out parameters. Set if there
 --       is an explicit initial value expression in the declaration of the
@@ -2255,6 +2275,10 @@ 
 --       Applies to all type entities, true for decimal fixed point
 --       types and subtypes.
 
+--    Is_Default_Init_Cond_Procedure (Flag132)
+--       Defined in functions and procedures. Set for a generated procedure
+--       which verifies the assumption of pragma Default_Initial_Condition.
+
 --    Is_Descendent_Of_Address (Flag223)
 --       Defined in all entities. True if the entity is type System.Address,
 --       or (recursively) a subtype or derived type of System.Address.
@@ -5230,11 +5254,13 @@ 
    --    Has_Constrained_Partial_View        (Flag187)
    --    Has_Controlled_Component            (Flag43)   (base type only)
    --    Has_Default_Aspect                  (Flag39)   (base type only)
+   --    Has_Default_Init_Cond               (Flag3)
    --    Has_Delayed_Rep_Aspects             (Flag261)
    --    Has_Discriminants                   (Flag5)
    --    Has_Dynamic_Predicate_Aspect        (Flag258)
    --    Has_Independent_Components          (Flag34)   (base type only)
    --    Has_Inheritable_Invariants          (Flag248)
+   --    Has_Inherited_Default_Init_Cond     (Flag133)
    --    Has_Invariants                      (Flag232)
    --    Has_Non_Standard_Rep                (Flag75)   (base type only)
    --    Has_Object_Size_Clause              (Flag172)
@@ -5286,6 +5312,7 @@ 
 
    --    Alignment_Clause                    (synth)
    --    Base_Type                           (synth)
+   --    Default_Init_Cond_Procedure         (synth)
    --    Implementation_Base_Type            (synth)
    --    Invariant_Procedure                 (synth)
    --    Is_Access_Protected_Subprogram_Type (synth)
@@ -5953,6 +5980,7 @@ 
    --    Is_Asynchronous                     (Flag81)
    --    Is_Called                           (Flag102)  (non-generic case only)
    --    Is_Constructor                      (Flag76)
+   --    Is_Default_Init_Cond_Procedure      (Flag132)  (non-generic case only)
    --    Is_Eliminated                       (Flag124)
    --    Is_Generic_Actual_Subprogram        (Flag274)  (non-generic case only)
    --    Is_Hidden_Non_Overridden_Subpgm     (Flag2)    (non-generic case only)
@@ -6550,6 +6578,7 @@ 
    function Has_Controlling_Result              (Id : E) return B;
    function Has_Convention_Pragma               (Id : E) return B;
    function Has_Default_Aspect                  (Id : E) return B;
+   function Has_Default_Init_Cond               (Id : E) return B;
    function Has_Delayed_Aspects                 (Id : E) return B;
    function Has_Delayed_Freeze                  (Id : E) return B;
    function Has_Delayed_Rep_Aspects             (Id : E) return B;
@@ -6565,6 +6594,7 @@ 
    function Has_Implicit_Dereference            (Id : E) return B;
    function Has_Independent_Components          (Id : E) return B;
    function Has_Inheritable_Invariants          (Id : E) return B;
+   function Has_Inherited_Default_Init_Cond     (Id : E) return B;
    function Has_Initial_Value                   (Id : E) return B;
    function Has_Interrupt_Handler               (Id : E) return B;
    function Has_Invariants                      (Id : E) return B;
@@ -6655,6 +6685,7 @@ 
    function Is_Constructor                      (Id : E) return B;
    function Is_Controlled                       (Id : E) return B;
    function Is_Controlling_Formal               (Id : E) return B;
+   function Is_Default_Init_Cond_Procedure      (Id : E) return B;
    function Is_Descendent_Of_Address            (Id : E) return B;
    function Is_Discrim_SO_Function              (Id : E) return B;
    function Is_Discriminant_Check_Function      (Id : E) return B;
@@ -7183,6 +7214,7 @@ 
    procedure Set_Has_Controlling_Result          (Id : E; V : B := True);
    procedure Set_Has_Convention_Pragma           (Id : E; V : B := True);
    procedure Set_Has_Default_Aspect              (Id : E; V : B := True);
+   procedure Set_Has_Default_Init_Cond           (Id : E; V : B := True);
    procedure Set_Has_Delayed_Aspects             (Id : E; V : B := True);
    procedure Set_Has_Delayed_Freeze              (Id : E; V : B := True);
    procedure Set_Has_Delayed_Rep_Aspects         (Id : E; V : B := True);
@@ -7198,6 +7230,7 @@ 
    procedure Set_Has_Implicit_Dereference        (Id : E; V : B := True);
    procedure Set_Has_Independent_Components      (Id : E; V : B := True);
    procedure Set_Has_Inheritable_Invariants      (Id : E; V : B := True);
+   procedure Set_Has_Inherited_Default_Init_Cond (Id : E; V : B := True);
    procedure Set_Has_Initial_Value               (Id : E; V : B := True);
    procedure Set_Has_Invariants                  (Id : E; V : B := True);
    procedure Set_Has_Loop_Entry_Attributes       (Id : E; V : B := True);
@@ -7288,6 +7321,7 @@ 
    procedure Set_Is_Constructor                  (Id : E; V : B := True);
    procedure Set_Is_Controlled                   (Id : E; V : B := True);
    procedure Set_Is_Controlling_Formal           (Id : E; V : B := True);
+   procedure Set_Is_Default_Init_Cond_Procedure  (Id : E; V : B := True);
    procedure Set_Is_Descendent_Of_Address        (Id : E; V : B := True);
    procedure Set_Is_Discrim_SO_Function          (Id : E; V : B := True);
    procedure Set_Is_Discriminant_Check_Function  (Id : E; V : B := True);
@@ -7502,10 +7536,12 @@ 
    -- Access to Subprograms in Subprograms_For_Type --
    ---------------------------------------------------
 
-   function Invariant_Procedure                 (Id : E) return N;
-   function Predicate_Function                  (Id : E) return N;
-   function Predicate_Function_M                (Id : E) return N;
+   function Default_Init_Cond_Procedure         (Id : E) return E;
+   function Invariant_Procedure                 (Id : E) return E;
+   function Predicate_Function                  (Id : E) return E;
+   function Predicate_Function_M                (Id : E) return E;
 
+   procedure Set_Default_Init_Cond_Procedure    (Id : E; V : E);
    procedure Set_Invariant_Procedure            (Id : E; V : E);
    procedure Set_Predicate_Function             (Id : E; V : E);
    procedure Set_Predicate_Function_M           (Id : E; V : E);
@@ -7929,6 +7965,7 @@ 
    pragma Inline (Has_Controlling_Result);
    pragma Inline (Has_Convention_Pragma);
    pragma Inline (Has_Default_Aspect);
+   pragma Inline (Has_Default_Init_Cond);
    pragma Inline (Has_Delayed_Aspects);
    pragma Inline (Has_Delayed_Freeze);
    pragma Inline (Has_Delayed_Rep_Aspects);
@@ -7944,6 +7981,7 @@ 
    pragma Inline (Has_Implicit_Dereference);
    pragma Inline (Has_Independent_Components);
    pragma Inline (Has_Inheritable_Invariants);
+   pragma Inline (Has_Inherited_Default_Init_Cond);
    pragma Inline (Has_Initial_Value);
    pragma Inline (Has_Invariants);
    pragma Inline (Has_Loop_Entry_Attributes);
@@ -8044,6 +8082,7 @@ 
    pragma Inline (Is_Controlled);
    pragma Inline (Is_Controlling_Formal);
    pragma Inline (Is_Decimal_Fixed_Point_Type);
+   pragma Inline (Is_Default_Init_Cond_Procedure);
    pragma Inline (Is_Descendent_Of_Address);
    pragma Inline (Is_Digits_Type);
    pragma Inline (Is_Discrete_Or_Fixed_Point_Type);
@@ -8409,6 +8448,7 @@ 
    pragma Inline (Set_Has_Controlling_Result);
    pragma Inline (Set_Has_Convention_Pragma);
    pragma Inline (Set_Has_Default_Aspect);
+   pragma Inline (Set_Has_Default_Init_Cond);
    pragma Inline (Set_Has_Delayed_Aspects);
    pragma Inline (Set_Has_Delayed_Freeze);
    pragma Inline (Set_Has_Delayed_Rep_Aspects);
@@ -8424,6 +8464,7 @@ 
    pragma Inline (Set_Has_Implicit_Dereference);
    pragma Inline (Set_Has_Independent_Components);
    pragma Inline (Set_Has_Inheritable_Invariants);
+   pragma Inline (Set_Has_Inherited_Default_Init_Cond);
    pragma Inline (Set_Has_Initial_Value);
    pragma Inline (Set_Has_Invariants);
    pragma Inline (Set_Has_Loop_Entry_Attributes);
@@ -8513,6 +8554,7 @@ 
    pragma Inline (Set_Is_Constructor);
    pragma Inline (Set_Is_Controlled);
    pragma Inline (Set_Is_Controlling_Formal);
+   pragma Inline (Set_Is_Default_Init_Cond_Procedure);
    pragma Inline (Set_Is_Descendent_Of_Address);
    pragma Inline (Set_Is_Discrim_SO_Function);
    pragma Inline (Set_Is_Discriminant_Check_Function);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 213548)
+++ sem_prag.adb	(working copy)
@@ -2363,7 +2363,7 @@ 
       --  final place yet. A direct analysis may generate side effects and this
       --  is not desired at this point.
 
-      Preanalyze_And_Resolve (Expr, Standard_Boolean);
+      Preanalyze_Assert_Expression (Expr, Standard_Boolean);
    end Analyze_Initial_Condition_In_Decl_Part;
 
    --------------------------------------
@@ -11016,17 +11016,18 @@ 
          --                        Type_Invariant       |
          --                        Type_Invariant'Class
 
-         --  ID_ASSERTION_KIND ::= Assert_And_Cut       |
-         --                        Assume               |
-         --                        Contract_Cases       |
-         --                        Debug                |
-         --                        Initial_Condition    |
-         --                        Loop_Invariant       |
-         --                        Loop_Variant         |
-         --                        Postcondition        |
-         --                        Precondition         |
-         --                        Predicate            |
-         --                        Refined_Post         |
+         --  ID_ASSERTION_KIND ::= Assert_And_Cut            |
+         --                        Assume                    |
+         --                        Contract_Cases            |
+         --                        Debug                     |
+         --                        Default_Initial_Condition |
+         --                        Initial_Condition         |
+         --                        Loop_Invariant            |
+         --                        Loop_Variant              |
+         --                        Postcondition             |
+         --                        Precondition              |
+         --                        Predicate                 |
+         --                        Refined_Post              |
          --                        Statement_Assertions
 
          --  Note: The RM_ASSERTION_KIND list is language-defined, and the
@@ -12755,101 +12756,67 @@ 
                     Expression => Get_Pragma_Arg (Arg1)))));
             Analyze (N);
 
-         -------------
-         -- Depends --
-         -------------
+         --------------------------------------
+         -- Pragma_Default_Initial_Condition --
+         --------------------------------------
 
-         --  pragma Depends (DEPENDENCY_RELATION);
+         --  pragma Pragma_Default_Initial_Condition
+         --           [ (null | boolean_EXPRESSION) ];
 
-         --  DEPENDENCY_RELATION ::=
-         --    null
-         --  | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}
+         when Pragma_Default_Initial_Condition => Default_Init_Cond : declare
+            Discard : Boolean;
+            Stmt    : Node_Id;
+            Typ     : Entity_Id;
 
-         --  DEPENDENCY_CLAUSE ::=
-         --    OUTPUT_LIST =>[+] INPUT_LIST
-         --  | NULL_DEPENDENCY_CLAUSE
-
-         --  NULL_DEPENDENCY_CLAUSE ::= null => INPUT_LIST
-
-         --  OUTPUT_LIST ::= OUTPUT | (OUTPUT {, OUTPUT})
-
-         --  INPUT_LIST ::= null | INPUT | (INPUT {, INPUT})
-
-         --  OUTPUT ::= NAME | FUNCTION_RESULT
-         --  INPUT  ::= NAME
-
-         --  where FUNCTION_RESULT is a function Result attribute_reference
-
-         when Pragma_Depends => Depends : declare
-            Subp_Decl : Node_Id;
-
          begin
             GNAT_Pragma;
-            Check_Arg_Count (1);
-            Ensure_Aggregate_Form (Arg1);
+            Check_At_Most_N_Arguments (1);
 
-            --  Ensure the proper placement of the pragma. Depends must be
-            --  associated with a subprogram declaration or a body that acts
-            --  as a spec.
+            Stmt := Prev (N);
+            while Present (Stmt) loop
 
-            Subp_Decl :=
-              Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+               --  Skip prior pragmas, but check for duplicates
 
-            if Nkind (Subp_Decl) = N_Subprogram_Declaration then
-               null;
+               if Nkind (Stmt) = N_Pragma then
+                  if Pragma_Name (Stmt) = Pname then
+                     Error_Msg_Name_1 := Pname;
+                     Error_Msg_Sloc   := Sloc (Stmt);
+                     Error_Msg_N ("pragma % duplicates pragma declared #", N);
+                  end if;
 
-            --  Body acts as spec
+               --  Skip internally generated code
 
-            elsif Nkind (Subp_Decl) = N_Subprogram_Body
-              and then No (Corresponding_Spec (Subp_Decl))
-            then
-               null;
+               elsif not Comes_From_Source (Stmt) then
+                  null;
 
-            --  Body stub acts as spec
+               --  The associated private type [extension] has been found, stop
+               --  the search.
 
-            elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
-              and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
-            then
-               null;
+               elsif Nkind_In (Stmt, N_Private_Extension_Declaration,
+                                     N_Private_Type_Declaration)
+               then
+                  Typ := Defining_Entity (Stmt);
+                  exit;
 
-            else
-               Pragma_Misplaced;
-               return;
-            end if;
+               --  The pragma does not apply to a legal construct, issue an
+               --  error and stop the analysis.
 
-            --  When the pragma appears on a subprogram body, perform the full
-            --  analysis now.
+               else
+                  Pragma_Misplaced;
+                  return;
+               end if;
 
-            if Nkind (Subp_Decl) = N_Subprogram_Body then
-               Analyze_Depends_In_Decl_Part (N);
+               Stmt := Prev (Stmt);
+            end loop;
 
-            --  When Depends applies to a subprogram compilation unit, the
-            --  corresponding pragma is placed after the unit's declaration
-            --  node and needs to be analyzed immediately.
+            Set_Has_Default_Init_Cond (Typ);
+            Set_Has_Inherited_Default_Init_Cond (Typ, False);
 
-            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
-              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
-            then
-               Analyze_Depends_In_Decl_Part (N);
-            end if;
+            --  Chain the pragma on the rep item chain for further processing
 
-            --  Chain the pragma on the contract for further processing
+            Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
+         end Default_Init_Cond;
 
-            Add_Contract_Item (N, Defining_Entity (Subp_Decl));
-         end Depends;
-
-         ---------------------
-         -- Detect_Blocking --
-         ---------------------
-
-         --  pragma Detect_Blocking;
-
-         when Pragma_Detect_Blocking =>
-            Ada_2005_Pragma;
-            Check_Arg_Count (0);
-            Check_Valid_Configuration_Pragma;
-            Detect_Blocking := True;
-
          ----------------------------------
          -- Default_Scalar_Storage_Order --
          ----------------------------------
@@ -12946,6 +12913,101 @@ 
 
             Default_Pool := Expression (Arg1);
 
+         -------------
+         -- Depends --
+         -------------
+
+         --  pragma Depends (DEPENDENCY_RELATION);
+
+         --  DEPENDENCY_RELATION ::=
+         --    null
+         --  | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}
+
+         --  DEPENDENCY_CLAUSE ::=
+         --    OUTPUT_LIST =>[+] INPUT_LIST
+         --  | NULL_DEPENDENCY_CLAUSE
+
+         --  NULL_DEPENDENCY_CLAUSE ::= null => INPUT_LIST
+
+         --  OUTPUT_LIST ::= OUTPUT | (OUTPUT {, OUTPUT})
+
+         --  INPUT_LIST ::= null | INPUT | (INPUT {, INPUT})
+
+         --  OUTPUT ::= NAME | FUNCTION_RESULT
+         --  INPUT  ::= NAME
+
+         --  where FUNCTION_RESULT is a function Result attribute_reference
+
+         when Pragma_Depends => Depends : declare
+            Subp_Decl : Node_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_Arg_Count (1);
+            Ensure_Aggregate_Form (Arg1);
+
+            --  Ensure the proper placement of the pragma. Depends must be
+            --  associated with a subprogram declaration or a body that acts
+            --  as a spec.
+
+            Subp_Decl :=
+              Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+
+            if Nkind (Subp_Decl) = N_Subprogram_Declaration then
+               null;
+
+            --  Body acts as spec
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Body
+              and then No (Corresponding_Spec (Subp_Decl))
+            then
+               null;
+
+            --  Body stub acts as spec
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+              and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
+            then
+               null;
+
+            else
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            --  When the pragma appears on a subprogram body, perform the full
+            --  analysis now.
+
+            if Nkind (Subp_Decl) = N_Subprogram_Body then
+               Analyze_Depends_In_Decl_Part (N);
+
+            --  When Depends applies to a subprogram compilation unit, the
+            --  corresponding pragma is placed after the unit's declaration
+            --  node and needs to be analyzed immediately.
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
+              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
+            then
+               Analyze_Depends_In_Decl_Part (N);
+            end if;
+
+            --  Chain the pragma on the contract for further processing
+
+            Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+         end Depends;
+
+         ---------------------
+         -- Detect_Blocking --
+         ---------------------
+
+         --  pragma Detect_Blocking;
+
+         when Pragma_Detect_Blocking =>
+            Ada_2005_Pragma;
+            Check_Arg_Count (0);
+            Check_Valid_Configuration_Pragma;
+            Detect_Blocking := True;
+
          ------------------------------------
          -- Disable_Atomic_Synchronization --
          ------------------------------------
@@ -15208,7 +15270,6 @@ 
          when Pragma_Invariant => Invariant : declare
             Type_Id : Node_Id;
             Typ     : Entity_Id;
-            PDecl   : Node_Id;
             Discard : Boolean;
 
          begin
@@ -15265,11 +15326,9 @@ 
             --  procedure declaration, so that calls to it can be generated
             --  before the body is built (e.g. within an expression function).
 
-            PDecl := Build_Invariant_Procedure_Declaration (Typ);
+            Insert_After_And_Analyze
+              (N, Build_Invariant_Procedure_Declaration (Typ));
 
-            Insert_After (N, PDecl);
-            Analyze (PDecl);
-
             if Class_Present (N) then
                Set_Has_Inheritable_Invariants (Typ);
             end if;
@@ -24719,6 +24778,7 @@ 
       Pragma_Debug                          => -1,
       Pragma_Debug_Policy                   =>  0,
       Pragma_Detect_Blocking                => -1,
+      Pragma_Default_Initial_Condition      => -1,
       Pragma_Default_Scalar_Storage_Order   =>  0,
       Pragma_Default_Storage_Pool           => -1,
       Pragma_Depends                        => -1,
@@ -25105,34 +25165,35 @@ 
          when
             --  RM defined
 
-            Name_Assert               |
-            Name_Static_Predicate     |
-            Name_Dynamic_Predicate    |
-            Name_Pre                  |
-            Name_uPre                 |
-            Name_Post                 |
-            Name_uPost                |
-            Name_Type_Invariant       |
-            Name_uType_Invariant      |
+            Name_Assert                    |
+            Name_Static_Predicate          |
+            Name_Dynamic_Predicate         |
+            Name_Pre                       |
+            Name_uPre                      |
+            Name_Post                      |
+            Name_uPost                     |
+            Name_Type_Invariant            |
+            Name_uType_Invariant           |
 
             --  Impl defined
 
-            Name_Assert_And_Cut       |
-            Name_Assume               |
-            Name_Contract_Cases       |
-            Name_Debug                |
-            Name_Initial_Condition    |
-            Name_Invariant            |
-            Name_uInvariant           |
-            Name_Loop_Invariant       |
-            Name_Loop_Variant         |
-            Name_Postcondition        |
-            Name_Precondition         |
-            Name_Predicate            |
-            Name_Refined_Post         |
-            Name_Statement_Assertions => return True;
+            Name_Assert_And_Cut            |
+            Name_Assume                    |
+            Name_Contract_Cases            |
+            Name_Debug                     |
+            Name_Default_Initial_Condition |
+            Name_Initial_Condition         |
+            Name_Invariant                 |
+            Name_uInvariant                |
+            Name_Loop_Invariant            |
+            Name_Loop_Variant              |
+            Name_Postcondition             |
+            Name_Precondition              |
+            Name_Predicate                 |
+            Name_Refined_Post              |
+            Name_Statement_Assertions      => return True;
 
-         when others                  => return False;
+         when others                       => return False;
       end case;
    end Is_Valid_Assertion_Kind;
 
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 213538)
+++ sem_util.adb	(working copy)
@@ -48,6 +48,7 @@ 
 with Sem_Aux;  use Sem_Aux;
 with Sem_Attr; use Sem_Attr;
 with Sem_Ch8;  use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
 with Sem_Disp; use Sem_Disp;
 with Sem_Eval; use Sem_Eval;
 with Sem_Prag; use Sem_Prag;
@@ -1229,6 +1230,189 @@ 
       return Decl;
    end Build_Component_Subtype;
 
+   ----------------------------------
+   -- Build_Default_Init_Cond_Call --
+   ----------------------------------
+
+   function Build_Default_Init_Cond_Call
+     (Loc    : Source_Ptr;
+      Obj_Id : Entity_Id;
+      Typ    : Entity_Id) return Node_Id
+   is
+      Proc_Id    : constant Entity_Id := Default_Init_Cond_Procedure (Typ);
+      Formal_Typ : constant Entity_Id := Etype (First_Formal (Proc_Id));
+
+   begin
+      return
+        Make_Procedure_Call_Statement (Loc,
+          Name                   => New_Occurrence_Of (Proc_Id, Loc),
+          Parameter_Associations => New_List (
+            Make_Type_Conversion (Loc,
+              Subtype_Mark => New_Occurrence_Of (Formal_Typ, Loc),
+              Expression   => New_Occurrence_Of (Obj_Id, Loc))));
+   end Build_Default_Init_Cond_Call;
+
+   --------------------------------------------
+   -- Build_Default_Init_Cond_Procedure_Body --
+   --------------------------------------------
+
+   procedure Build_Default_Init_Cond_Procedure_Body (Typ : Entity_Id) is
+      Param_Id : Entity_Id;
+      --  The entity of the formal parameter of the default initial condition
+      --  procedure.
+
+      procedure Replace_Type_Reference (N : Node_Id);
+      --  Replace a single reference to type Typ with a reference to Param_Id
+
+      ----------------------------
+      -- Replace_Type_Reference --
+      ----------------------------
+
+      procedure Replace_Type_Reference (N : Node_Id) is
+      begin
+         Rewrite (N, New_Occurrence_Of (Param_Id, Sloc (N)));
+      end Replace_Type_Reference;
+
+      procedure Replace_Type_References is
+        new Replace_Type_References_Generic (Replace_Type_Reference);
+
+      --  Local variables
+
+      Loc       : constant Source_Ptr := Sloc (Typ);
+      Prag      : constant Node_Id    :=
+                    Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+      Proc_Id   : constant Entity_Id  := Default_Init_Cond_Procedure (Typ);
+      Spec_Decl : constant Node_Id    := Unit_Declaration_Node (Proc_Id);
+      Body_Decl : Node_Id;
+      Expr      : Node_Id;
+      Stmt      : Node_Id;
+
+   --  Start of processing for Build_Default_Init_Cond_Procedure
+
+   begin
+      --  The procedure should be generated only for types subject to pragma
+      --  Default_Initial_Condition. Types that inherit the pragma do not get
+      --  this specialized procedure.
+
+      pragma Assert (Has_Default_Init_Cond (Typ));
+      pragma Assert (Present (Prag));
+      pragma Assert (Present (Proc_Id));
+
+      --  Nothing to do if the body was already built
+
+      if Present (Corresponding_Body (Spec_Decl)) then
+         return;
+      end if;
+
+      Param_Id := First_Formal (Proc_Id);
+
+      --  The pragma has an argument. Note that the argument is analyzed after
+      --  all references to the current instance of the type are replaced.
+
+      if Present (Pragma_Argument_Associations (Prag)) then
+         Expr := Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
+
+         if Nkind (Expr) = N_Null then
+            Stmt := Make_Null_Statement (Loc);
+
+         --  Preserve the original argument of the pragma by replicating it.
+         --  Replace all references to the current instance of the type with
+         --  references to the formal parameter.
+
+         else
+            Expr := New_Copy_Tree (Expr);
+            Replace_Type_References (Expr, Typ);
+
+            --  Generate:
+            --    pragma Check (Default_Initial_Condition, <Expr>);
+
+            Stmt :=
+              Make_Pragma (Loc,
+                Pragma_Identifier            =>
+                  Make_Identifier (Loc, Name_Check),
+
+                Pragma_Argument_Associations => New_List (
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression =>
+                      Make_Identifier (Loc, Name_Default_Initial_Condition)),
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Expr)));
+         end if;
+
+      --  Otherwise the pragma appears without an argument
+
+      else
+         Stmt := Make_Null_Statement (Loc);
+      end if;
+
+      --  Generate:
+      --    procedure <Typ>Default_Init_Cond (I : <Typ>) is
+      --    begin
+      --       <Stmt>;
+      --    end <Typ>Default_Init_Cond;
+
+      Body_Decl :=
+        Make_Subprogram_Body (Loc,
+          Specification              =>
+            Copy_Separate_Tree (Specification (Spec_Decl)),
+          Declarations               => Empty_List,
+          Handled_Statement_Sequence =>
+            Make_Handled_Sequence_Of_Statements (Loc,
+              Statements => New_List (Stmt)));
+
+      --  Link the spec and body of the default initial condition procedure
+      --  to prevent the generation of a duplicate body in case there is an
+      --  attempt to freeze the related type again.
+
+      Set_Corresponding_Body (Spec_Decl, Defining_Entity (Body_Decl));
+      Set_Corresponding_Spec (Body_Decl, Proc_Id);
+
+      Append_Freeze_Action (Typ, Body_Decl);
+   end Build_Default_Init_Cond_Procedure_Body;
+
+   ---------------------------------------------------
+   -- Build_Default_Init_Cond_Procedure_Declaration --
+   ---------------------------------------------------
+
+   procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id) is
+      Loc     : constant Source_Ptr := Sloc (Typ);
+      Prag    : constant Node_Id    :=
+                  Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+      Proc_Id : Entity_Id;
+
+   begin
+      --  The procedure should be generated only for types subject to pragma
+      --  Default_Initial_Condition. Types that inherit the pragma do not get
+      --  this specialized procedure.
+
+      pragma Assert (Has_Default_Init_Cond (Typ));
+      pragma Assert (Present (Prag));
+
+      Proc_Id  :=
+        Make_Defining_Identifier (Loc,
+          Chars => New_External_Name (Chars (Typ), "Default_Init_Cond"));
+
+      --  Associate the default initial condition procedure with the private
+      --  type.
+
+      Set_Ekind (Proc_Id, E_Procedure);
+      Set_Is_Default_Init_Cond_Procedure (Proc_Id);
+      Set_Default_Init_Cond_Procedure (Typ, Proc_Id);
+
+      --  Generate:
+      --    procedure <Typ>Default_Init_Cond (Inn : <Typ>);
+
+      Insert_After_And_Analyze (Prag,
+        Make_Subprogram_Declaration (Loc,
+          Specification =>
+            Make_Procedure_Specification (Loc,
+              Defining_Unit_Name       => Proc_Id,
+              Parameter_Specifications => New_List (
+                Make_Parameter_Specification (Loc,
+                  Defining_Identifier => Make_Temporary (Loc, 'I'),
+                  Parameter_Type      => New_Occurrence_Of (Typ, Loc))))));
+   end Build_Default_Init_Cond_Procedure_Declaration;
+
    ---------------------------
    -- Build_Default_Subtype --
    ---------------------------
@@ -9066,6 +9250,23 @@ 
       return Empty;
    end Incomplete_Or_Private_View;
 
+   -----------------------------------------
+   -- Inherit_Default_Init_Cond_Procedure --
+   -----------------------------------------
+
+   procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id) is
+      Par_Typ : constant Entity_Id := Etype (Typ);
+
+   begin
+      --  A derived type inherits the default initial condition procedure of
+      --  its parent type.
+
+      if No (Default_Init_Cond_Procedure (Typ)) then
+         Set_Default_Init_Cond_Procedure
+           (Typ, Default_Init_Cond_Procedure (Par_Typ));
+      end if;
+   end Inherit_Default_Init_Cond_Procedure;
+
    ---------------------------------
    -- Insert_Explicit_Dereference --
    ---------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 213537)
+++ sem_util.ads	(working copy)
@@ -211,6 +211,25 @@ 
    --  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_Body (Typ : Entity_Id);
+   --  If private type Typ is subject to pragma Default_Initial_Condition,
+   --  build the body of the procedure which verifies the assumption of the
+   --  pragma at runtime. The generated body is added to the freeze actions
+   --  of the type.
+
+   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;
@@ -1065,6 +1084,10 @@ 
    --  the same type. Note that Typ may not have a partial view to begin with,
    --  in that case the function returns Empty.
 
+   procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id);
+   --  Inherit the default initial condition procedure from the parent type of
+   --  derived type Typ.
+
    procedure Insert_Explicit_Dereference (N : Node_Id);
    --  In a context that requires a composite or subprogram type and where a
    --  prefix is an access type, rewrite the access type node N (which is the
@@ -1596,17 +1619,17 @@ 
    --  (e.g. target of assignment, or out parameter), and to False if the
    --  modification is only potential (e.g. address of entity taken).
 
+   function Object_Access_Level (Obj : Node_Id) return Uint;
+   --  Return the accessibility level of the view of the object Obj. For
+   --  convenience, qualified expressions applied to object names are also
+   --  allowed as actuals for this function.
+
    function Original_Corresponding_Operation (S : Entity_Id) return Entity_Id;
    --  [Ada 2012: AI05-0125-1]: If S is an inherited dispatching primitive S2,
    --  or overrides an inherited dispatching primitive S2, the original
    --  corresponding operation of S is the original corresponding operation of
    --  S2. Otherwise, it is S itself.
 
-   function Object_Access_Level (Obj : Node_Id) return Uint;
-   --  Return the accessibility level of the view of the object Obj. For
-   --  convenience, qualified expressions applied to object names are also
-   --  allowed as actuals for this function.
-
    function Original_Aspect_Name (N : Node_Id) return Name_Id;
    --  N is a pragma node or aspect specification node. This function returns
    --  the name of the pragma or aspect in original source form, taking into
Index: aspects.adb
===================================================================
--- aspects.adb	(revision 213536)
+++ aspects.adb	(working copy)
@@ -509,6 +509,7 @@ 
     Aspect_Convention                   => Aspect_Convention,
     Aspect_CPU                          => Aspect_CPU,
     Aspect_Default_Component_Value      => Aspect_Default_Component_Value,
+    Aspect_Default_Initial_Condition    => Aspect_Default_Initial_Condition,
     Aspect_Default_Iterator             => Aspect_Default_Iterator,
     Aspect_Default_Value                => Aspect_Default_Value,
     Aspect_Depends                      => Aspect_Depends,
Index: aspects.ads
===================================================================
--- aspects.ads	(revision 213536)
+++ aspects.ads	(working copy)
@@ -86,6 +86,7 @@ 
       Aspect_Convention,
       Aspect_CPU,
       Aspect_Default_Component_Value,
+      Aspect_Default_Initial_Condition,     -- GNAT
       Aspect_Default_Iterator,
       Aspect_Default_Value,
       Aspect_Depends,                       -- GNAT
@@ -296,76 +297,77 @@ 
    --  The following array indicates what argument type is required
 
    Aspect_Argument : constant array (Aspect_Id) of Aspect_Expression :=
-     (No_Aspect                      => Optional_Expression,
-      Aspect_Abstract_State          => Expression,
-      Aspect_Address                 => Expression,
-      Aspect_Alignment               => Expression,
-      Aspect_Annotate                => Expression,
-      Aspect_Attach_Handler          => Expression,
-      Aspect_Bit_Order               => Expression,
-      Aspect_Component_Size          => Expression,
-      Aspect_Constant_Indexing       => Name,
-      Aspect_Contract_Cases          => Expression,
-      Aspect_Convention              => Name,
-      Aspect_CPU                     => Expression,
-      Aspect_Default_Component_Value => Expression,
-      Aspect_Default_Iterator        => Name,
-      Aspect_Default_Value           => Expression,
-      Aspect_Depends                 => Expression,
-      Aspect_Dimension               => Expression,
-      Aspect_Dimension_System        => Expression,
-      Aspect_Dispatching_Domain      => Expression,
-      Aspect_Dynamic_Predicate       => Expression,
-      Aspect_External_Name           => Expression,
-      Aspect_External_Tag            => Expression,
-      Aspect_Global                  => Expression,
-      Aspect_Implicit_Dereference    => Name,
-      Aspect_Initial_Condition       => Expression,
-      Aspect_Initializes             => Expression,
-      Aspect_Input                   => Name,
-      Aspect_Interrupt_Priority      => Expression,
-      Aspect_Invariant               => Expression,
-      Aspect_Iterable                => Expression,
-      Aspect_Iterator_Element        => Name,
-      Aspect_Link_Name               => Expression,
-      Aspect_Linker_Section          => Expression,
-      Aspect_Machine_Radix           => Expression,
-      Aspect_Object_Size             => Expression,
-      Aspect_Output                  => Name,
-      Aspect_Part_Of                 => Expression,
-      Aspect_Post                    => Expression,
-      Aspect_Postcondition           => Expression,
-      Aspect_Pre                     => Expression,
-      Aspect_Precondition            => Expression,
-      Aspect_Predicate               => Expression,
-      Aspect_Priority                => Expression,
-      Aspect_Read                    => Name,
-      Aspect_Refined_Depends         => Expression,
-      Aspect_Refined_Global          => Expression,
-      Aspect_Refined_Post            => Expression,
-      Aspect_Refined_State           => Expression,
-      Aspect_Relative_Deadline       => Expression,
-      Aspect_Scalar_Storage_Order    => Expression,
-      Aspect_Simple_Storage_Pool     => Name,
-      Aspect_Size                    => Expression,
-      Aspect_Small                   => Expression,
-      Aspect_SPARK_Mode              => Optional_Name,
-      Aspect_Static_Predicate        => Expression,
-      Aspect_Storage_Pool            => Name,
-      Aspect_Storage_Size            => Expression,
-      Aspect_Stream_Size             => Expression,
-      Aspect_Suppress                => Name,
-      Aspect_Synchronization         => Name,
-      Aspect_Test_Case               => Expression,
-      Aspect_Type_Invariant          => Expression,
-      Aspect_Unsuppress              => Name,
-      Aspect_Value_Size              => Expression,
-      Aspect_Variable_Indexing       => Name,
-      Aspect_Warnings                => Name,
-      Aspect_Write                   => Name,
+     (No_Aspect                        => Optional_Expression,
+      Aspect_Abstract_State            => Expression,
+      Aspect_Address                   => Expression,
+      Aspect_Alignment                 => Expression,
+      Aspect_Annotate                  => Expression,
+      Aspect_Attach_Handler            => Expression,
+      Aspect_Bit_Order                 => Expression,
+      Aspect_Component_Size            => Expression,
+      Aspect_Constant_Indexing         => Name,
+      Aspect_Contract_Cases            => Expression,
+      Aspect_Convention                => Name,
+      Aspect_CPU                       => Expression,
+      Aspect_Default_Component_Value   => Expression,
+      Aspect_Default_Initial_Condition => Optional_Expression,
+      Aspect_Default_Iterator          => Name,
+      Aspect_Default_Value             => Expression,
+      Aspect_Depends                   => Expression,
+      Aspect_Dimension                 => Expression,
+      Aspect_Dimension_System          => Expression,
+      Aspect_Dispatching_Domain        => Expression,
+      Aspect_Dynamic_Predicate         => Expression,
+      Aspect_External_Name             => Expression,
+      Aspect_External_Tag              => Expression,
+      Aspect_Global                    => Expression,
+      Aspect_Implicit_Dereference      => Name,
+      Aspect_Initial_Condition         => Expression,
+      Aspect_Initializes               => Expression,
+      Aspect_Input                     => Name,
+      Aspect_Interrupt_Priority        => Expression,
+      Aspect_Invariant                 => Expression,
+      Aspect_Iterable                  => Expression,
+      Aspect_Iterator_Element          => Name,
+      Aspect_Link_Name                 => Expression,
+      Aspect_Linker_Section            => Expression,
+      Aspect_Machine_Radix             => Expression,
+      Aspect_Object_Size               => Expression,
+      Aspect_Output                    => Name,
+      Aspect_Part_Of                   => Expression,
+      Aspect_Post                      => Expression,
+      Aspect_Postcondition             => Expression,
+      Aspect_Pre                       => Expression,
+      Aspect_Precondition              => Expression,
+      Aspect_Predicate                 => Expression,
+      Aspect_Priority                  => Expression,
+      Aspect_Read                      => Name,
+      Aspect_Refined_Depends           => Expression,
+      Aspect_Refined_Global            => Expression,
+      Aspect_Refined_Post              => Expression,
+      Aspect_Refined_State             => Expression,
+      Aspect_Relative_Deadline         => Expression,
+      Aspect_Scalar_Storage_Order      => Expression,
+      Aspect_Simple_Storage_Pool       => Name,
+      Aspect_Size                      => Expression,
+      Aspect_Small                     => Expression,
+      Aspect_SPARK_Mode                => Optional_Name,
+      Aspect_Static_Predicate          => Expression,
+      Aspect_Storage_Pool              => Name,
+      Aspect_Storage_Size              => Expression,
+      Aspect_Stream_Size               => Expression,
+      Aspect_Suppress                  => Name,
+      Aspect_Synchronization           => Name,
+      Aspect_Test_Case                 => Expression,
+      Aspect_Type_Invariant            => Expression,
+      Aspect_Unsuppress                => Name,
+      Aspect_Value_Size                => Expression,
+      Aspect_Variable_Indexing         => Name,
+      Aspect_Warnings                  => Name,
+      Aspect_Write                     => Name,
 
-      Boolean_Aspects                => Optional_Expression,
-      Library_Unit_Aspects           => Optional_Expression);
+      Boolean_Aspects                  => Optional_Expression,
+      Library_Unit_Aspects             => Optional_Expression);
 
    -----------------------------------------
    -- Table Linking Names and Aspect_Id's --
@@ -392,9 +394,10 @@ 
       Aspect_Contract_Cases               => Name_Contract_Cases,
       Aspect_Convention                   => Name_Convention,
       Aspect_CPU                          => Name_CPU,
+      Aspect_Default_Component_Value      => Name_Default_Component_Value,
+      Aspect_Default_Initial_Condition    => Name_Default_Initial_Condition,
       Aspect_Default_Iterator             => Name_Default_Iterator,
       Aspect_Default_Value                => Name_Default_Value,
-      Aspect_Default_Component_Value      => Name_Default_Component_Value,
       Aspect_Depends                      => Name_Depends,
       Aspect_Dimension                    => Name_Dimension,
       Aspect_Dimension_System             => Name_Dimension_System,
@@ -675,6 +678,7 @@ 
       Aspect_Async_Writers                => Never_Delay,
       Aspect_Contract_Cases               => Never_Delay,
       Aspect_Convention                   => Never_Delay,
+      Aspect_Default_Initial_Condition    => Never_Delay,
       Aspect_Depends                      => Never_Delay,
       Aspect_Dimension                    => Never_Delay,
       Aspect_Dimension_System             => Never_Delay,
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 213536)
+++ par-prag.adb	(working copy)
@@ -1186,6 +1186,7 @@ 
            Pragma_Debug_Policy                   |
            Pragma_Depends                        |
            Pragma_Detect_Blocking                |
+           Pragma_Default_Initial_Condition      |
            Pragma_Default_Scalar_Storage_Order   |
            Pragma_Default_Storage_Pool           |
            Pragma_Disable_Atomic_Synchronization |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 213545)
+++ sem_ch13.adb	(working copy)
@@ -182,17 +182,6 @@ 
    --  renaming_as_body. For tagged types, the specification is one of the
    --  primitive specs.
 
-   generic
-      with procedure Replace_Type_Reference (N : Node_Id);
-   procedure Replace_Type_References_Generic (N : Node_Id; T : Entity_Id);
-   --  This is used to scan an expression for a predicate or invariant aspect
-   --  replacing occurrences of the name of the subtype to which the aspect
-   --  applies with appropriate references to the parameter of the predicate
-   --  function or invariant procedure. The procedure passed as a generic
-   --  parameter does the actual replacement of node N, which is either a
-   --  simple direct reference to T, or a selected component that represents
-   --  an appropriately qualified occurrence of T.
-
    procedure Resolve_Iterable_Operation
      (N      : Node_Id;
       Cursor : Entity_Id;
@@ -2221,6 +2210,26 @@ 
                   goto Continue;
                end Abstract_State;
 
+               --  Aspect Default_Internal_Condition is never delayed because
+               --  it is equivalent to a source pragma which appears after the
+               --  related private type. To deal with forward references, the
+               --  generated pragma is stored in the rep chain of the related
+               --  private type as types do not carry contracts. The pragma is
+               --  wrapped inside of a procedure at the freeze point of the
+               --  private type's full view.
+
+               when Aspect_Default_Initial_Condition =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  =>
+                       Name_Default_Initial_Condition);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
                --  Depends
 
                --  Aspect Depends is never delayed because it is equivalent to
@@ -8737,25 +8746,26 @@ 
 
          --  Here is the list of aspects that don't require delay analysis
 
-         when Aspect_Abstract_State       |
-              Aspect_Annotate             |
-              Aspect_Contract_Cases       |
-              Aspect_Dimension            |
-              Aspect_Dimension_System     |
-              Aspect_Implicit_Dereference |
-              Aspect_Initial_Condition    |
-              Aspect_Initializes          |
-              Aspect_Part_Of              |
-              Aspect_Post                 |
-              Aspect_Postcondition        |
-              Aspect_Pre                  |
-              Aspect_Precondition         |
-              Aspect_Refined_Depends      |
-              Aspect_Refined_Global       |
-              Aspect_Refined_Post         |
-              Aspect_Refined_State        |
-              Aspect_SPARK_Mode           |
-              Aspect_Test_Case            =>
+         when Aspect_Abstract_State            |
+              Aspect_Annotate                  |
+              Aspect_Contract_Cases            |
+              Aspect_Default_Initial_Condition |
+              Aspect_Dimension                 |
+              Aspect_Dimension_System          |
+              Aspect_Implicit_Dereference      |
+              Aspect_Initial_Condition         |
+              Aspect_Initializes               |
+              Aspect_Part_Of                   |
+              Aspect_Post                      |
+              Aspect_Postcondition             |
+              Aspect_Pre                       |
+              Aspect_Precondition              |
+              Aspect_Refined_Depends           |
+              Aspect_Refined_Global            |
+              Aspect_Refined_Post              |
+              Aspect_Refined_State             |
+              Aspect_SPARK_Mode                |
+              Aspect_Test_Case                 =>
             raise Program_Error;
 
       end case;
@@ -10555,9 +10565,10 @@ 
         (Rep_Item : Node_Id) return Boolean
       is
       begin
-         return Nkind (Rep_Item) = N_Pragma
-           or else Present_In_Rep_Item
-                     (Entity (Rep_Item), Aspect_Rep_Item (Rep_Item));
+         return
+           Nkind (Rep_Item) = N_Pragma
+             or else Present_In_Rep_Item
+                       (Entity (Rep_Item), Aspect_Rep_Item (Rep_Item));
       end Is_Pragma_Or_Corr_Pragma_Present_In_Rep_Item;
 
    --  Start of processing for Inherit_Aspects_At_Freeze_Point
@@ -11746,7 +11757,7 @@ 
                end loop;
             end if;
 
-            --  Continue for any other node kind
+         --  Continue for any other node kind
 
          else
             return OK;
Index: sem_ch13.ads
===================================================================
--- sem_ch13.ads	(revision 213536)
+++ sem_ch13.ads	(working copy)
@@ -144,6 +144,17 @@ 
    --  type. Returns False if no such error occurs. If this error does occur,
    --  appropriate error messages are posted on node N, and True is returned.
 
+   generic
+      with procedure Replace_Type_Reference (N : Node_Id);
+   procedure Replace_Type_References_Generic (N : Node_Id; T : Entity_Id);
+   --  This is used to scan an expression for a predicate or invariant aspect
+   --  replacing occurrences of the name of the subtype to which the aspect
+   --  applies with appropriate references to the parameter of the predicate
+   --  function or invariant procedure. The procedure passed as a generic
+   --  parameter does the actual replacement of node N, which is either a
+   --  simple direct reference to T, or a selected component that represents
+   --  an appropriately qualified occurrence of T.
+
    function Rep_Item_Too_Late
      (T     : Entity_Id;
       N     : Node_Id;
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 213549)
+++ snames.ads-tmpl	(working copy)
@@ -479,6 +479,7 @@ 
    --  pragma.
 
    Name_Debug                          : constant Name_Id := N + $; -- GNAT
+   Name_Default_Initial_Condition      : constant Name_Id := N + $; -- GNAT
    Name_Depends                        : constant Name_Id := N + $; -- GNAT
    Name_Effective_Reads                : constant Name_Id := N + $; -- GNAT
    Name_Effective_Writes               : constant Name_Id := N + $; -- GNAT
@@ -1810,6 +1811,7 @@ 
       Pragma_CPP_Virtual,
       Pragma_CPP_Vtable,
       Pragma_Debug,
+      Pragma_Default_Initial_Condition,
       Pragma_Depends,
       Pragma_Effective_Reads,
       Pragma_Effective_Writes,
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb	(revision 213549)
+++ exp_ch3.adb	(working copy)
@@ -165,11 +165,6 @@ 
    --  needed after an initialization. Typ is the component type, and Proc_Id
    --  the initialization procedure for the enclosing composite type.
 
-   procedure Expand_Tagged_Root (T : Entity_Id);
-   --  Add a field _Tag at the beginning of the record. This field carries
-   --  the value of the access to the Dispatch table. This procedure is only
-   --  called on root type, the _Tag field being inherited by the descendants.
-
    procedure Expand_Freeze_Array_Type (N : Node_Id);
    --  Freeze an array type. Deals with building the initialization procedure,
    --  creating the packed array type for a packed array and also with the
@@ -193,6 +188,11 @@ 
    --  applies only to E_Record_Type entities, not to class wide types,
    --  record subtypes, or private types.
 
+   procedure Expand_Tagged_Root (T : Entity_Id);
+   --  Add a field _Tag at the beginning of the record. This field carries
+   --  the value of the access to the Dispatch table. This procedure is only
+   --  called on root type, the _Tag field being inherited by the descendants.
+
    procedure Freeze_Stream_Operations (N : Node_Id; Typ : Entity_Id);
    --  Treat user-defined stream operations as renaming_as_body if the
    --  subprogram they rename is not frozen when the type is frozen.
@@ -632,19 +632,20 @@ 
 
             return New_List (
               Make_Implicit_Loop_Statement (Nod,
-                Identifier => Empty,
+                Identifier       => Empty,
                 Iteration_Scheme =>
                   Make_Iteration_Scheme (Loc,
                     Loop_Parameter_Specification =>
                       Make_Loop_Parameter_Specification (Loc,
-                        Defining_Identifier => Index,
+                        Defining_Identifier         => Index,
                         Discrete_Subtype_Definition =>
                           Make_Attribute_Reference (Loc,
-                            Prefix => Make_Identifier (Loc, Name_uInit),
+                            Prefix          =>
+                              Make_Identifier (Loc, Name_uInit),
                             Attribute_Name  => Name_Range,
                             Expressions     => New_List (
                               Make_Integer_Literal (Loc, N))))),
-                Statements =>  Init_One_Dimension (N + 1)));
+                Statements       => Init_One_Dimension (N + 1)));
          end if;
       end Init_One_Dimension;
 
@@ -4664,7 +4665,6 @@ 
    ------------------------------------
 
    procedure Expand_N_Full_Type_Declaration (N : Node_Id) is
-
       procedure Build_Master (Ptr_Typ : Entity_Id);
       --  Create the master associated with Ptr_Typ
 
@@ -5313,6 +5313,7 @@ 
 
       --  Local variables
 
+      Next_N  : constant Node_Id := Next (N);
       Id_Ref  : Node_Id;
       New_Ref : Node_Id;
 
@@ -5563,7 +5564,7 @@ 
                   --  by
                   --     Tmp : T := Obj;
                   --     type Ityp is not null access I'Class;
-                  --     CW  : I'Class renames Ityp(Tmp.I_Tag'Address).all;
+                  --     CW  : I'Class renames Ityp (Tmp.I_Tag'Address).all;
 
                   if Comes_From_Source (Expr_N)
                     and then Nkind (Expr_N) = N_Identifier
@@ -5672,7 +5673,8 @@ 
                     Make_Object_Renaming_Declaration (Loc,
                       Defining_Identifier => Make_Temporary (Loc, 'D'),
                       Subtype_Mark        => New_Occurrence_Of (Typ, Loc),
-                      Name => Convert_Tag_To_Interface (Typ, Tag_Comp)));
+                      Name                =>
+                        Convert_Tag_To_Interface (Typ, Tag_Comp)));
 
                   --  If the original entity comes from source, then mark the
                   --  new entity as needing debug information, even though it's
@@ -6026,6 +6028,37 @@ 
          end;
       end if;
 
+      --  At this point the object is fully initialized by either invoking the
+      --  related type init proc, routine [Deep_]Initialize or performing in-
+      --  place assingments for an array object. If the related type is subject
+      --  to pragma Default_Initial_Condition, add a runtime check to verify
+      --  the assumption of the pragma. Generate:
+
+      --    <Base_Typ>Default_Init_Cond (<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 (Base_Typ)
+                    or else Has_Inherited_Default_Init_Cond (Base_Typ))
+      then
+         declare
+            DIC_Call : constant Node_Id :=
+                         Build_Default_Init_Cond_Call (Loc, Def_Id, Base_Typ);
+         begin
+            if Present (Next_N) then
+               Insert_Before_And_Analyze (Next_N, DIC_Call);
+
+            --  The object declaration is the last node in a declarative or a
+            --  statement list.
+
+            else
+               Append_To (List_Containing (N), DIC_Call);
+               Analyze (DIC_Call);
+            end if;
+         end;
+      end if;
+
    --  Exception on library entity not available
 
    exception
@@ -7357,14 +7390,27 @@ 
             end loop;
          end;
 
+         --  If there are RACWs designating this type, make stubs now
+
          if RACW_Seen then
-
-            --  If there are RACWs designating this type, make stubs now
-
             Remote_Types_Tagged_Full_View_Encountered (Def_Id);
          end if;
       end if;
 
+      --  If the type is subject to pragma Default_Initial_Condition, generate
+      --  the body of the procedure which verifies the assertion of the pragma
+      --  at runtime.
+
+      if Has_Default_Init_Cond (Def_Id) then
+         Build_Default_Init_Cond_Procedure_Body (Def_Id);
+
+      --  A derived type inherits the default initial condition procedure from
+      --  its parent type.
+
+      elsif Has_Inherited_Default_Init_Cond (Def_Id) then
+         Inherit_Default_Init_Cond_Procedure (Def_Id);
+      end if;
+
       --  Freeze processing for record types
 
       if Is_Record_Type (Def_Id) then