Patchwork [Ada] Implement Invariant aspect and pragma

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 19, 2010, 10:40 a.m.
Message ID <20101019104017.GA17310@adacore.com>
Download mbox | patch
Permalink /patch/68309/
State New
Headers show

Comments

Arnaud Charlet - Oct. 19, 2010, 10:40 a.m.
This patch implements the Invariant aspect, from AI AI05-0146-1/04.
The implementation is complete except that inheritance of aspects
from interfaces is not yet done. Inheritance of Invariant'Class for
the normal case of derived tagged types does work. An Invariant
pragma has also been introduced, allowing use of this facility
in earlier versions of Ada (before Ada 2012).

The following test is for the Invariant aspect (non-inherited case)

     1. with Ada.Text_IO;    use Ada.Text_IO;
     2. with Ada.Assertions; use Ada.Assertions;
     3. with Ada.Exceptions; use Ada.Exceptions;
     4. procedure Simpleinv is
     5.    package X is
     6.       type R is private with
     7.          Invariant => Testr (R);
     8.       function Testr (X : R) return Boolean;
     9.       function Gen (X : Integer) return R;
    10.       procedure Make (X : out R);
    11.
    12.       type T1 is tagged private with
    13.         Invariant => Testt1 (T1);
    14.       type T2 is new T1 with private;
    15.       function Testt1 (X : T1) return Boolean;
    16.       function Maket2 return T2;
    17.
    18.    private
    19.       type R is record
    20.          Field : Integer := 4;
    21.       end record;
    22.
    23.       type T1 is tagged record
    24.          Field : Integer := 4;
    25.       end record;
    26.
    27.       type T2 is new T1 with record
    28.          Field2 : Integer := 4;
    29.       end record;
    30.    end X;
    31.
    32.    package body X is
    33.       function Testr (X : R) return Boolean is
    34.       begin
    35.          return X.Field mod 2 = 1;
    36.       end Testr;
    37.
    38.       function Gen (X : Integer) return R is
    39.       begin
    40.          return (Field => X);
    41.       end Gen;
    42.
    43.       procedure Make (X : out R) is
    44.       begin
    45.          X := (Field => 4);
    46.       end Make;
    47.
    48.       function Testt1 (X : T1) return Boolean is
    49.       begin
    50.          return X.Field mod 2 = 1;
    51.       end Testt1;
    52.
    53.       function Maket2 return T2 is
    54.       begin
    55.          return (Field => 4, Field2 => 3);
    56.       end Maket2;
    57.
    58.       --  No exception, private initialization
    59.
    60.       VPrivate : R := (Field => 6);
    61.    end X;
    62.
    63. begin
    64.    --  No exception, OK initialization
    65.
    66.    begin
    67.       declare
    68.          V1 : X.R := X.Gen (5);
    69.       begin
    70.          null;
    71.       end;
    72.       Put_Line ("V1: no exception");
    73.    end;
    74.
    75.    --  Bad result from public function
    76.
    77.    begin
    78.       declare
    79.          V2 : X.R := X.Gen (4);
    80.       begin
    81.          null;
    82.       end;
    83.       Put_Line ("V2: no exception");
    84.    exception
    85.       when E : Assertion_Error =>
    86.          Put_Line ("V2: " & Exception_Message (E));
    87.    end;
    88.
    89.    --  Bad default initialization
    90.
    91.    begin
    92.       declare
    93.          V3 : X.R;
    94.       begin
    95.          null;
    96.       end;
    97.       Put_Line ("V3: no exception");
    98.    exception
    99.       when E : Assertion_Error =>
   100.          Put_Line ("V3: " & Exception_Message (E));
   101.    end;
   102.
   103.    --  Bad OUT parameter
   104.
   105.    begin
   106.       declare
   107.          V4 : X.R := X.Gen (5);
   108.       begin
   109.          X.Make (V4);
   110.       end;
   111.       Put_Line ("V4: no exception");
   112.    exception
   113.       when E : Assertion_Error =>
   114.          Put_Line ("V4: " & Exception_Message (E));
   115.    end;
   116.
   117.    --  Bad conversion
   118.
   119.    begin
   120.       declare
   121.          TT : X.T2 := X.Maket2;
   122.          V5 : X.T1 := X.T1 (TT);
   123.       begin
   124.          null;
   125.       end;
   126.       Put_Line ("V5: no exception");
   127.    exception
   128.       when E : Assertion_Error =>
   129.          Put_Line ("V5: " & Exception_Message (E));
   130.    end;
   131. end Simpleinv;

The output when compiled with -gnata12 is:

V1: no exception
V2: failed invariant from simpleinv.adb:7
V3: failed invariant from simpleinv.adb:7
V4: failed invariant from simpleinv.adb:7
V5: failed invariant from simpleinv.adb:13

The following test is for Invariant'Class showing
inheritance and proper dispatching. This is compiled
with -gnata12 -gnatj60

     1. with Ada.Text_IO;    use Ada.Text_IO;
     2. with Ada.Assertions; use Ada.Assertions;
     3. with Ada.Exceptions; use Ada.Exceptions;
     4. procedure Inheritinv is
     5.    package X is
     6.
     7.       type T1 is tagged private with
     8.         Invariant'Class => Testt1 (T1);
     9.
    10.       function Testt1 (X : T1) return Boolean;
    11.       function Maket1 return T1;
    12.
    13.       type T2 is new T1 with private;
    14.
    15.       function Maket2 return T2;
    16.       function Testt1 (X : T2) return Boolean;
    17.       function Maket1 return T2;
    18.
    19.    private
    20.       type T1 is tagged record
    21.          Field1 : Integer := 4;
    22.       end record;
    23.
    24.       type T2 is new T1 with record
                   |
        >>> info: "T2" inherits "Invariant'Class" aspect
            from line 8

    25.          Field2 : Integer := 4;
    26.       end record;
    27.    end X;
    28.
    29.    package body X is
    30.
    31.       function Testt1 (X : T1) return Boolean is
    32.       begin
    33.          return X.Field1 mod 2 = 1;
    34.       end Testt1;
    35.
    36.       function Testt1 (X : T2) return Boolean is
    37.       begin
    38.          return X.Field1 mod 2 = 0;
    39.       end Testt1;
    40.
    41.       function Maket1 return T1 is
    42.       begin
    43.          return (Field1 => 4);
    44.       end Maket1;
    45.
    46.       function Maket1 return T2 is
    47.       begin
    48.          return (Field1 => 4, Field2 => 3);
    49.       end Maket1;
    50.
    51.       function Maket2 return T2 is
    52.       begin
    53.          return (Field1 => 5, Field2 => 3);
    54.       end Maket2;
    55.    end X;
    56.
    57. begin
    58.    --  Bad value from Maket1
    59.
    60.    begin
    61.       declare
    62.          V1 : X.T1 := X.Maket1;
    63.       begin
    64.          null;
    65.       end;
    66.       Put_Line ("V1: no exception");
    67.    exception
    68.       when E : Assertion_Error =>
    69.          Put_Line ("V1: " & Exception_Message (E));
    70.    end;
    71.
    72.    --  Bad value from Maket2
    73.    --  (tested with overridden testt1)
    74.
    75.    begin
    76.       declare
    77.          V2 : X.T2 := X.Maket2;
    78.       begin
    79.          null;
    80.       end;
    81.       Put_Line ("V2: no exception");
    82.    exception
    83.       when E : Assertion_Error =>
    84.          Put_Line ("V2: " & Exception_Message (E));
    85.    end;
    86.
    87.    --  OK value from overridden Maket1
    88.    --  (tested with overridden testt1)
    89.
    90.    begin
    91.       declare
    92.          V3 : X.T2 := X.Maket1;
    93.       begin
    94.          null;
    95.       end;
    96.       Put_Line ("V3: no exception");
    97.    exception
    98.       when E : Assertion_Error =>
    99.          Put_Line ("V3: " & Exception_Message (E));
   100.    end;
   101.
   102. end Inheritinv;

The output is:

V1: failed invariant from inheritinv.adb:8
V2: failed inherited invariant from inheritinv.adb:8
V3: no exception

The following checks

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

2010-10-19  Robert Dewar  <dewar@adacore.com>

	* atree.h (Field29): Fix incorrect definition.
	* einfo.adb (Invariant_Procedure): New attribute
	(Has_Invariants): New flag
	(Has_Inheritable_Invariants): New flag
	(OK_To_Reference): New flag
	Minor code reorganization (use Next_Rep_Item function)
	* einfo.ads (Invariant_Procedure): New attribute
	(Has_Invariants): New flag
	(Has_Inheritable_Invariants): New flag
	(OK_To_Reference): New flag
	* exp_ch3.adb (Expand_N_Object_Declaration): Add check for invariant
	* exp_ch4.adb (Expand_N_Type_Conversion): Check invariant on type
	conversion.  Minor reformatting.
	* exp_util.ads, exp_util.adb (Make_Invariant_Call): New procedure.
	* opt.ads (List_Inherited_Aspects): New name for List_Inherited_Pre_Post
	* par-prag.adb: Add dummy entry for pragma Invariant.
	* sem_ch13.adb (Build_Invariant_Procedure): New procedure
	(Analyze_Aspect_Specification): Add support for Invariant aspect
	* sem_ch13.ads (Build_Invariant_Procedure): New procedure
	* sem_ch3.adb (Build_Derived_Type): Propagate invariant information
	(Process_Full_View): Deal with invariants, building invariant procedure
	Minor reformatting
	* sem_ch6.adb (Process_PPCs): Add processing of invariants
	* sem_ch7.adb (Analyze_Package_Specification): Build invariant
	procedures.
	* sem_prag.adb: Implement pragma Invariant.
	* sem_res.adb (Resolve_Entity_Name): Allow type reference if
	OK_To_Reference set.
	* sem_warn.adb (List_Inherited_Aspects): New name for
	List_Inherited_Pre_Post.
	* snames.ads-tmpl: Add entries for pragma Invariant.
	* treepr.adb (Print_Entity_Information): Add handling of Field29.
	* usage.adb: Warning .l/.L applies to invariant as well as pre/post.

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 165692)
+++ sem_ch3.adb	(working copy)
@@ -3592,6 +3592,8 @@  package body Sem_Ch3 is
 
       Generate_Definition (T);
 
+      --  For other than Ada 2012, just enter the name in the current scope
+
       if Ada_Version < Ada_2012 then
          Enter_Name (T);
 
@@ -7657,6 +7659,15 @@  package body Sem_Ch3 is
       Set_Is_Controlled  (Derived_Type, Is_Controlled  (Parent_Type));
       Set_Is_Tagged_Type (Derived_Type, Is_Tagged_Type (Parent_Type));
 
+      --  Propagate invariant information. The new type has invariants if
+      --  they are inherited from the parent type, and these invariants can
+      --  be further inherited, so both flags are set.
+
+      if Has_Inheritable_Invariants (Parent_Type) then
+         Set_Has_Inheritable_Invariants (Derived_Type);
+         Set_Has_Invariants (Derived_Type);
+      end if;
+
       --  The derived type inherits the representation clauses of the parent.
       --  However, for a private type that is completed by a derivation, there
       --  may be operation attributes that have been specified already (stream
@@ -14171,8 +14182,8 @@  package body Sem_Ch3 is
 
          elsif Ekind (Prev) = E_Incomplete_Type
            and then (Ada_Version < Ada_2012
-                       or else No (Full_View (Prev))
-                       or else not Is_Private_Type (Full_View (Prev)))
+                      or else No (Full_View (Prev))
+                      or else not Is_Private_Type (Full_View (Prev)))
          then
 
             --  Indicate that the incomplete declaration has a matching full
@@ -16038,14 +16049,16 @@  package body Sem_Ch3 is
          --  A return statement for a build-in-place function returning a
          --  synchronized type also introduces an unchecked conversion.
 
-         when N_Type_Conversion | N_Unchecked_Type_Conversion =>
+         when N_Type_Conversion           |
+              N_Unchecked_Type_Conversion =>
             return not Comes_From_Source (Exp)
               and then
                 OK_For_Limited_Init_In_05
                   (Typ, Expression (Original_Node (Exp)));
 
-         when N_Indexed_Component | N_Selected_Component |
-               N_Explicit_Dereference  =>
+         when N_Indexed_Component     |
+              N_Selected_Component    |
+              N_Explicit_Dereference  =>
             return Nkind (Exp) = N_Function_Call;
 
          --  A use of 'Input is a function call, hence allowed. Normally the
@@ -17106,18 +17119,76 @@  package body Sem_Ch3 is
       --  If the private view has user specified stream attributes, then so has
       --  the full view.
 
+      --  Why the test, how could these flags be already set in Full_T ???
+
       if Has_Specified_Stream_Read (Priv_T) then
          Set_Has_Specified_Stream_Read (Full_T);
       end if;
+
       if Has_Specified_Stream_Write (Priv_T) then
          Set_Has_Specified_Stream_Write (Full_T);
       end if;
+
       if Has_Specified_Stream_Input (Priv_T) then
          Set_Has_Specified_Stream_Input (Full_T);
       end if;
+
       if Has_Specified_Stream_Output (Priv_T) then
          Set_Has_Specified_Stream_Output (Full_T);
       end if;
+
+      --  Deal with invariants
+
+      if Has_Invariants (Full_T)
+           or else
+         Has_Invariants (Priv_T)
+      then
+         Set_Has_Invariants (Full_T);
+         Set_Has_Invariants (Priv_T);
+      end if;
+
+      if Has_Inheritable_Invariants (Full_T)
+           or else
+         Has_Inheritable_Invariants (Priv_T)
+      then
+         Set_Has_Inheritable_Invariants (Full_T);
+         Set_Has_Inheritable_Invariants (Priv_T);
+      end if;
+
+      --  This is where we build the invariant procedure if needed
+
+      if Has_Invariants (Priv_T) then
+         declare
+            PDecl : Entity_Id;
+            PBody : Entity_Id;
+            Packg : constant Node_Id := Declaration_Node (Scope (Priv_T));
+
+         begin
+            Build_Invariant_Procedure (Full_T, PDecl, PBody);
+
+            --  Error defense, normally these should be set
+
+            if Present (PDecl) and then Present (PBody) then
+
+               --  Spec goes at the end of the public part of the package.
+               --  That's behind us, so we have to manually analyze the
+               --  inserted spec.
+
+               Append_To (Visible_Declarations (Packg), PDecl);
+               Analyze (PDecl);
+
+               --  Body goes at the end of the private part of the package.
+               --  That's ahead of us so it will get analyzed later on when
+               --  we come to it.
+
+               Append_To (Private_Declarations (Packg), PBody);
+
+               --  Copy Invariant procedure to private declaration
+
+               Set_Invariant_Procedure (Priv_T, Invariant_Procedure (Full_T));
+            end if;
+         end;
+      end if;
    end Process_Full_View;
 
    -----------------------------------
Index: exp_util.adb
===================================================================
--- exp_util.adb	(revision 165687)
+++ exp_util.adb	(working copy)
@@ -45,6 +45,7 @@  with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Ch8;  use Sem_Ch8;
 with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Type; use Sem_Type;
 with Sem_Util; use Sem_Util;
@@ -3987,6 +3988,31 @@  package body Exp_Util is
       return Equiv_Type;
    end Make_CW_Equivalent_Type;
 
+   -------------------------
+   -- Make_Invariant_Call --
+   -------------------------
+
+   function Make_Invariant_Call (Expr : Node_Id) return Node_Id is
+      Loc : constant Source_Ptr := Sloc (Expr);
+      Typ : constant Entity_Id  := Etype (Expr);
+
+   begin
+      if Check_Enabled (Name_Invariant)
+           or else
+         Check_Enabled (Name_Assertion)
+      then
+         return
+           Make_Procedure_Call_Statement (Loc,
+             Name                   =>
+               New_Occurrence_Of (Invariant_Procedure (Typ), Loc),
+             Parameter_Associations => New_List (Relocate_Node (Expr)));
+
+      else
+         return
+           Make_Null_Statement (Loc);
+      end if;
+   end Make_Invariant_Call;
+
    ------------------------
    -- Make_Literal_Range --
    ------------------------
Index: exp_util.ads
===================================================================
--- exp_util.ads	(revision 165687)
+++ exp_util.ads	(working copy)
@@ -562,6 +562,12 @@  package Exp_Util is
    --  and returns True if so. Returns False otherwise. It is an error to call
    --  this function if N is not of an access type.
 
+   function Make_Invariant_Call (Expr : Node_Id) return Node_Id;
+   --  Expr is an object of a type which Has_Invariants set (and which thus
+   --  also has an Invariant_Procedure set). If invariants are enabled, this
+   --  function returns a call to the Invariant procedure passing Expr as the
+   --  argument.
+
    function Make_Subtype_From_Expr
      (E       : Node_Id;
       Unc_Typ : Entity_Id) return Node_Id;
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 165687)
+++ sem_ch7.adb	(working copy)
@@ -1159,7 +1159,6 @@  package body Sem_Ch7 is
          declare
             Orig_Spec : constant Node_Id := Specification (Orig_Decl);
             Save_Priv : constant List_Id := Private_Declarations (Orig_Spec);
-
          begin
             Set_Private_Declarations (Orig_Spec, Empty_List);
             Save_Global_References   (Orig_Decl);
@@ -1919,6 +1918,8 @@  package body Sem_Ch7 is
 
    procedure New_Private_Type (N : Node_Id; Id : Entity_Id; Def : Node_Id) is
    begin
+      --  For other than Ada 2012, enter tha name in the current scope
+
       if Ada_Version < Ada_2012 then
          Enter_Name (Id);
 
@@ -1928,14 +1929,12 @@  package body Sem_Ch7 is
       else
          declare
             Prev : Entity_Id;
-
          begin
             Prev := Find_Type_Name (N);
-
             pragma Assert (Prev = Id
               or else (Ekind (Prev) = E_Incomplete_Type
-                         and then Present (Full_View (Prev))
-                         and then Full_View (Prev) = Id));
+                        and then Present (Full_View (Prev))
+                        and then Full_View (Prev) = Id));
          end;
       end if;
 
Index: usage.adb
===================================================================
--- usage.adb	(revision 165687)
+++ usage.adb	(working copy)
@@ -438,10 +438,8 @@  begin
                                                   "elaboration pragma");
    Write_Line ("        L*   turn off warnings for missing " &
                                                   "elaboration pragma");
-   Write_Line ("        .l*  turn on info messages for inherited pre/" &
-                                                  "postconditions");
-   Write_Line ("        .L   turn off info messages for inherited pre/" &
-                                                  "postconditions");
+   Write_Line ("        .l*  turn on info messages for inherited aspects");
+   Write_Line ("        .L   turn off info messages for inherited aspects");
    Write_Line ("        m+   turn on warnings for variable assigned " &
                                                   "but not read");
    Write_Line ("        M*   turn off warnings for variable assigned " &
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 165689)
+++ einfo.adb	(working copy)
@@ -230,7 +230,7 @@  package body Einfo is
    --    Extra_Formals                   Node28
    --    Underlying_Record_View          Node28
 
-   --    (unused)                        Node29
+   --    Invariant_Procedure             Node29
 
    ---------------------------------------------
    -- Usage of Flags in Defining Entity Nodes --
@@ -241,7 +241,7 @@  package body Einfo is
    --  sense for them to be set true for certain subsets of entity kinds. See
    --  the spec of Einfo for further details.
 
-   --  Note: Flag1-Flag2 are absent from this list, for historical reasons
+   --  Note: Flag1-Flag3 are absent from this list, for historical reasons
 
    --    Is_Frozen                       Flag4
    --    Has_Discriminants               Flag5
@@ -494,6 +494,7 @@  package body Einfo is
    --    Has_Pragma_Inline_Always        Flag230
 
    --    Renamed_In_Spec                 Flag231
+   --    Has_Invariants                  Flag232
    --    Has_Pragma_Unmodified           Flag233
    --    Is_Dispatch_Table_Entity        Flag234
    --    Is_Trivial_Subprogram           Flag235
@@ -510,10 +511,9 @@  package body Einfo is
    --    Is_Private_Primitive            Flag245
    --    Is_Underlying_Record_View       Flag246
    --    OK_To_Rename                    Flag247
+   --    Has_Inheritable_Invariants      Flag248
+   --    OK_To_Reference                 Flag249
 
-   --    (unused)                        Flag232
-   --    (unused)                        Flag248
-   --    (unused)                        Flag249
    --    (unused)                        Flag250
    --    (unused)                        Flag251
    --    (unused)                        Flag252
@@ -543,7 +543,7 @@  package body Einfo is
          then
             return Ritem;
          else
-            Ritem := Next_Rep_Item (Ritem);
+            Next_Rep_Item (Ritem);
          end if;
       end loop;
 
@@ -1273,13 +1273,24 @@  package body Einfo is
       return Flag56 (Id);
    end Has_Homonym;
 
+   function Has_Inheritable_Invariants (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag248 (Id);
+   end Has_Inheritable_Invariants;
+
    function Has_Initial_Value (Id : E) return B is
    begin
-      pragma Assert
-        (Ekind (Id) = E_Variable or else Is_Formal (Id));
+      pragma Assert (Ekind (Id) = E_Variable or else Is_Formal (Id));
       return Flag219 (Id);
    end Has_Initial_Value;
 
+   function Has_Invariants (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag232 (Id);
+   end Has_Invariants;
+
    function Has_Machine_Radix_Clause (Id : E) return B is
    begin
       pragma Assert (Is_Decimal_Fixed_Point_Type (Id));
@@ -1555,6 +1566,12 @@  package body Einfo is
       return Elist25 (Id);
    end Interfaces;
 
+   function Invariant_Procedure (Id : E) return N is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Node29 (Id);
+   end Invariant_Procedure;
+
    function In_Package_Body (Id : E) return B is
    begin
       return Flag48 (Id);
@@ -2286,6 +2303,12 @@  package body Einfo is
       return Uint10 (Id);
    end Normalized_Position_Max;
 
+   function OK_To_Reference (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag249 (Id);
+   end OK_To_Reference;
+
    function OK_To_Rename (Id : E) return B is
    begin
       pragma Assert (Ekind (Id) = E_Variable);
@@ -3685,12 +3708,24 @@  package body Einfo is
       Set_Flag56 (Id, V);
    end Set_Has_Homonym;
 
+   procedure Set_Has_Inheritable_Invariants (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag248 (Id, V);
+   end Set_Has_Inheritable_Invariants;
+
    procedure Set_Has_Initial_Value (Id : E; V : B := True) is
    begin
       pragma Assert (Ekind_In (Id, E_Variable, E_Out_Parameter));
       Set_Flag219 (Id, V);
    end Set_Has_Initial_Value;
 
+   procedure Set_Has_Invariants (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag232 (Id, V);
+   end Set_Has_Invariants;
+
    procedure Set_Has_Machine_Radix_Clause (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Decimal_Fixed_Point_Type (Id));
@@ -3977,6 +4012,12 @@  package body Einfo is
       Set_Elist25 (Id, V);
    end Set_Interfaces;
 
+   procedure Set_Invariant_Procedure (Id : E; V : N) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Node29 (Id, V);
+   end Set_Invariant_Procedure;
+
    procedure Set_In_Package_Body (Id : E; V : B := True) is
    begin
       Set_Flag48 (Id, V);
@@ -4743,6 +4784,12 @@  package body Einfo is
       Set_Uint10 (Id, V);
    end Set_Normalized_Position_Max;
 
+   procedure Set_OK_To_Reference (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag249 (Id, V);
+   end Set_OK_To_Reference;
+
    procedure Set_OK_To_Rename (Id : E; V : B := True) is
    begin
       pragma Assert (Ekind (Id) = E_Variable);
@@ -5899,7 +5946,7 @@  package body Einfo is
          then
             return True;
          else
-            Ritem := Next_Rep_Item (Ritem);
+            Next_Rep_Item (Ritem);
          end if;
       end loop;
 
@@ -5972,7 +6019,7 @@  package body Einfo is
          then
             return True;
          else
-            Ritem := Next_Rep_Item (Ritem);
+            Next_Rep_Item (Ritem);
          end if;
       end loop;
 
@@ -6991,7 +7038,9 @@  package body Einfo is
       W ("Has_Fully_Qualified_Name",        Flag173 (Id));
       W ("Has_Gigi_Rep_Item",               Flag82  (Id));
       W ("Has_Homonym",                     Flag56  (Id));
+      W ("Has_Inheritable_Invariants",      Flag248 (Id));
       W ("Has_Initial_Value",               Flag219 (Id));
+      W ("Has_Invariants",                  Flag232 (Id));
       W ("Has_Machine_Radix_Clause",        Flag83  (Id));
       W ("Has_Master_Entity",               Flag21  (Id));
       W ("Has_Missing_Return",              Flag142 (Id));
@@ -7156,6 +7205,7 @@  package body Einfo is
       W ("No_Strict_Aliasing",              Flag136 (Id));
       W ("Non_Binary_Modulus",              Flag58  (Id));
       W ("Nonzero_Is_True",                 Flag162 (Id));
+      W ("OK_To_Reference",                 Flag249 (Id));
       W ("OK_To_Rename",                    Flag247 (Id));
       W ("OK_To_Reorder_Components",        Flag239 (Id));
       W ("Optimize_Alignment_Space",        Flag241 (Id));
@@ -8143,7 +8193,6 @@  package body Einfo is
 
          when E_Procedure                                  |
               E_Function                                   =>
-
             if Is_Dispatching_Operation (Id) then
                Write_Str ("Overridden_Operation");
             else
@@ -8197,6 +8246,9 @@  package body Einfo is
    procedure Write_Field28_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when Private_Kind =>
+            Write_Str ("Invariant_Procedure");
+
          when E_Procedure | E_Function | E_Entry           =>
             Write_Str ("Extra_Formals");
 
@@ -8208,6 +8260,17 @@  package body Einfo is
       end case;
    end Write_Field28_Name;
 
+   procedure Write_Field29_Name (Id : Entity_Id) is
+   begin
+      case Ekind (Id) is
+         when Type_Kind =>
+            Write_Str ("Invariant_Procedure");
+
+         when others                                       =>
+            Write_Str ("Field29??");
+      end case;
+   end Write_Field29_Name;
+
    -------------------------
    -- Iterator Procedures --
    -------------------------
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 165689)
+++ einfo.ads	(working copy)
@@ -504,7 +504,7 @@  package Einfo is
 --       which can never have a null value. This is set True for constant
 --       access values initialized to a non-null value. This is also True for
 --       all access parameters in Ada 83 and Ada 95 modes, and for access
---       parameters that explicily exlude null in Ada 2005.
+--       parameters that explicily exclude null in Ada 2005.
 --
 --       This is used to avoid unnecessary resetting of the Is_Known_Non_Null
 --       flag for such entities. In Ada 2005 mode, this is also used when
@@ -1505,6 +1505,25 @@  package Einfo is
 --       definition contains at least one procedure to which a pragma
 --       Interrupt_Handler applies.
 
+--    Has_Invariants (Flag232)
+--       Present in all type entities. Set True in private types if an
+--       Invariant or Invariant'Class aspect applies to the type, or if the
+--       type inherits one or more Invariant'Class aspects. Also set in the
+--       corresponding full type. Note: if this flag is set True, then usually
+--       the Invariant_Procedure field is set once the type is frozen, however
+--       this may not be true in some error situations. Note that it might be
+--       the full type which has inheritable invariants, and then the flag will
+--       also be set in the private type.
+
+--    Has_Inheritable_Invariants (Flag248)
+--       Present in all type entities. Set True in private types from which one
+--       or more Invariant'Class aspects will be inherited if a another type is
+--       derived from the type (i.e. those types which have an Invariant'Class
+--       aspect, or which inherit one or more Invariant'Class aspects). Also
+--       set in the corresponding full types. Note that it might be the full
+--       type which has inheritable invariants, and in this case the flag will
+--       also be set in the private type.
+
 --    Has_Machine_Radix_Clause (Flag83)
 --       Present in decimal types and subtypes, set if a Machine_Radix
 --       representation clause is present. This flag is used to detect
@@ -1716,10 +1735,10 @@  package Einfo is
 --       representation clause, and thus is not inherited by a derived type.
 --       This flag is always False for non-record types.
 
---    Has_Specified_Stream_Input  (Flag190)
+--    Has_Specified_Stream_Input (Flag190)
 --    Has_Specified_Stream_Output (Flag191)
---    Has_Specified_Stream_Read   (Flag192)
---    Has_Specified_Stream_Write  (Flag193)
+--    Has_Specified_Stream_Read (Flag192)
+--    Has_Specified_Stream_Write (Flag193)
 --       Present in all type and subtype entities. Set for a given view if the
 --       corresponding stream-oriented attribute has been defined by an
 --       attribute definition clause. When such a clause occurs, a TSS is set
@@ -1880,6 +1899,16 @@  package Einfo is
 --       External_Name of the imported Java field (which is generally needed,
 --       because Java names are case sensitive).
 
+--    Invariant_Procedure (Node29)
+--       Present in types and subtypes. Set for private types if one or more
+--       Invariant, or Invariant'Class, or inherited Invariant'Class aspects
+--       apply to the type. Points to the entity for a procedure which checks
+--       the invariant. This invariant procedure takes a single argument of the
+--       given type, and returns if the invariant holds, or raises exception
+--       Assertion_Error with an appropriate message if it does not hold. This
+--       field is present but always empty for private subtypes. This field is
+--       also set for the corresponding full type.
+
 --    In_Use (Flag8)
 --       Present in packages and types. Set when analyzing a use clause for
 --       the corresponding entity. Reset at end of corresponding declarative
@@ -3108,6 +3137,12 @@  package Einfo is
 --       Applies to subprograms and subprogram types. Yields the number of
 --       formals as a value of type Pos.
 
+--    OK_To_Reference (Flag249)
+--       Present in all entities for types and subtypes. If set it indicates
+--       that a naked reference to the type is permitted within an expression
+--       that is being analyzed or preanalyed (for example, a type name may
+--       be referenced within the Invariant aspect expression for the type).
+
 --    OK_To_Rename (Flag247)
 --       Present only in entities for variables. If this flag is set, it
 --       means that if the entity is used as the initial value of an object
@@ -4697,6 +4732,7 @@  package Einfo is
    --    Alignment                           (Uint14)
    --    Related_Expression                  (Node24)
    --    Current_Use_Clause                  (Node27)
+   --    Invariant_Procedure                 (Node29)
 
    --    Depends_On_Private                  (Flag14)
    --    Discard_Names                       (Flag88)
@@ -4709,6 +4745,8 @@  package Einfo is
    --    Has_Complex_Representation          (Flag140)  (base type only)
    --    Has_Constrained_Partial_View        (Flag187)
    --    Has_Discriminants                   (Flag5)
+   --    Has_Inheritable_Invariants          (Flag248)
+   --    Has_Invariants                      (Flag232)
    --    Has_Non_Standard_Rep                (Flag75)   (base type only)
    --    Has_Object_Size_Clause              (Flag172)
    --    Has_Pragma_Preelab_Init             (Flag221)
@@ -4743,6 +4781,7 @@  package Einfo is
    --    Known_To_Have_Preelab_Init          (Flag207)
    --    Must_Be_On_Byte_Boundary            (Flag183)
    --    Must_Have_Preelab_Init              (Flag208)
+   --    OK_To_Reference                     (Flag249)
    --    Optimize_Alignment_Space            (Flag241)
    --    Optimize_Alignment_Time             (Flag242)
    --    Size_Depends_On_Discriminant        (Flag177)
@@ -5897,7 +5936,9 @@  package Einfo is
    function Has_Fully_Qualified_Name            (Id : E) return B;
    function Has_Gigi_Rep_Item                   (Id : E) return B;
    function Has_Homonym                         (Id : E) return B;
+   function Has_Inheritable_Invariants          (Id : E) return B;
    function Has_Initial_Value                   (Id : E) return B;
+   function Has_Invariants                      (Id : E) return B;
    function Has_Interrupt_Handler               (Id : E) return B;
    function Has_Machine_Radix_Clause            (Id : E) return B;
    function Has_Master_Entity                   (Id : E) return B;
@@ -5954,6 +5995,7 @@  package Einfo is
    function Interface_Alias                     (Id : E) return E;
    function Interfaces                          (Id : E) return L;
    function Interface_Name                      (Id : E) return N;
+   function Invariant_Procedure                 (Id : E) return N;
    function Is_AST_Entry                        (Id : E) return B;
    function Is_Abstract_Subprogram              (Id : E) return B;
    function Is_Abstract_Type                    (Id : E) return B;
@@ -6075,6 +6117,7 @@  package Einfo is
    function Normalized_First_Bit                (Id : E) return U;
    function Normalized_Position                 (Id : E) return U;
    function Normalized_Position_Max             (Id : E) return U;
+   function OK_To_Reference                     (Id : E) return B;
    function OK_To_Rename                        (Id : E) return B;
    function OK_To_Reorder_Components            (Id : E) return B;
    function Optimize_Alignment_Space            (Id : E) return B;
@@ -6460,7 +6503,9 @@  package Einfo is
    procedure Set_Has_Fully_Qualified_Name        (Id : E; V : B := True);
    procedure Set_Has_Gigi_Rep_Item               (Id : E; V : B := True);
    procedure Set_Has_Homonym                     (Id : E; V : B := True);
+   procedure Set_Has_Inheritable_Invariants      (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_Machine_Radix_Clause        (Id : E; V : B := True);
    procedure Set_Has_Master_Entity               (Id : E; V : B := True);
    procedure Set_Has_Missing_Return              (Id : E; V : B := True);
@@ -6517,6 +6562,7 @@  package Einfo is
    procedure Set_Inner_Instances                 (Id : E; V : L);
    procedure Set_Interface_Alias                 (Id : E; V : E);
    procedure Set_Interface_Name                  (Id : E; V : N);
+   procedure Set_Invariant_Procedure             (Id : E; V : N);
    procedure Set_Is_AST_Entry                    (Id : E; V : B := True);
    procedure Set_Is_Abstract_Subprogram          (Id : E; V : B := True);
    procedure Set_Is_Abstract_Type                (Id : E; V : B := True);
@@ -6645,6 +6691,7 @@  package Einfo is
    procedure Set_Normalized_First_Bit            (Id : E; V : U);
    procedure Set_Normalized_Position             (Id : E; V : U);
    procedure Set_Normalized_Position_Max         (Id : E; V : U);
+   procedure Set_OK_To_Reference                 (Id : E; V : B := True);
    procedure Set_OK_To_Rename                    (Id : E; V : B := True);
    procedure Set_OK_To_Reorder_Components        (Id : E; V : B := True);
    procedure Set_Optimize_Alignment_Space        (Id : E; V : B := True);
@@ -7002,9 +7049,10 @@  package Einfo is
    procedure Write_Field26_Name (Id : Entity_Id);
    procedure Write_Field27_Name (Id : Entity_Id);
    procedure Write_Field28_Name (Id : Entity_Id);
-   --  These routines are used to output a nice symbolic name for the given
-   --  field, depending on the Ekind. No blanks or end of lines are output,
-   --  just the characters of the field name.
+   procedure Write_Field29_Name (Id : Entity_Id);
+   --  These routines are used in Treepr to output a nice symbolic name for
+   --  the given field, depending on the Ekind. No blanks or end of lines are
+   --  output, just the characters of the field name.
 
    --------------------
    -- Inline Pragmas --
@@ -7135,7 +7183,9 @@  package Einfo is
    pragma Inline (Has_Fully_Qualified_Name);
    pragma Inline (Has_Gigi_Rep_Item);
    pragma Inline (Has_Homonym);
+   pragma Inline (Has_Inheritable_Invariants);
    pragma Inline (Has_Initial_Value);
+   pragma Inline (Has_Invariants);
    pragma Inline (Has_Machine_Radix_Clause);
    pragma Inline (Has_Master_Entity);
    pragma Inline (Has_Missing_Return);
@@ -7192,6 +7242,7 @@  package Einfo is
    pragma Inline (Inner_Instances);
    pragma Inline (Interface_Alias);
    pragma Inline (Interface_Name);
+   pragma Inline (Invariant_Procedure);
    pragma Inline (Is_AST_Entry);
    pragma Inline (Is_Abstract_Subprogram);
    pragma Inline (Is_Abstract_Type);
@@ -7362,6 +7413,7 @@  package Einfo is
    pragma Inline (Normalized_First_Bit);
    pragma Inline (Normalized_Position);
    pragma Inline (Normalized_Position_Max);
+   pragma Inline (OK_To_Reference);
    pragma Inline (OK_To_Rename);
    pragma Inline (OK_To_Reorder_Components);
    pragma Inline (Optimize_Alignment_Space);
@@ -7568,7 +7620,9 @@  package Einfo is
    pragma Inline (Set_Has_Fully_Qualified_Name);
    pragma Inline (Set_Has_Gigi_Rep_Item);
    pragma Inline (Set_Has_Homonym);
+   pragma Inline (Set_Has_Inheritable_Invariants);
    pragma Inline (Set_Has_Initial_Value);
+   pragma Inline (Set_Has_Invariants);
    pragma Inline (Set_Has_Machine_Radix_Clause);
    pragma Inline (Set_Has_Master_Entity);
    pragma Inline (Set_Has_Missing_Return);
@@ -7625,6 +7679,7 @@  package Einfo is
    pragma Inline (Set_Inner_Instances);
    pragma Inline (Set_Interface_Alias);
    pragma Inline (Set_Interface_Name);
+   pragma Inline (Set_Invariant_Procedure);
    pragma Inline (Set_Is_AST_Entry);
    pragma Inline (Set_Is_Abstract_Subprogram);
    pragma Inline (Set_Is_Abstract_Type);
@@ -7754,6 +7809,7 @@  package Einfo is
    pragma Inline (Set_Normalized_Position);
    pragma Inline (Set_Normalized_Position_Max);
    pragma Inline (Set_OK_To_Reorder_Components);
+   pragma Inline (Set_OK_To_Reference);
    pragma Inline (Set_OK_To_Rename);
    pragma Inline (Set_Optimize_Alignment_Space);
    pragma Inline (Set_Optimize_Alignment_Time);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 165687)
+++ sem_prag.adb	(working copy)
@@ -7133,8 +7133,11 @@  package body Sem_Prag is
 
             if Nkind (Expression (Arg1)) = N_Null then
                Analyze (Expression (Arg1));
+
+               --  This is an odd case, this is not really an expression, so
+               --  we don't have a type for it. So just set the type to Empty.
+
                Set_Etype (Expression (Arg1), Empty);
-               --  It's not really an expression, and we have no type for it
 
             --  Case of Default_Storage_Pool (storage_pool_NAME);
 
@@ -9272,6 +9275,67 @@  package body Sem_Prag is
             end loop;
          end Interrupt_State;
 
+         ---------------
+         -- Invariant --
+         ---------------
+
+         --  pragma Invariant
+         --    ([Entity =>]    type_LOCAL_NAME,
+         --     [Check  =>]    EXPRESSION
+         --     [,[Message =>] String_Expression]);
+
+         when Pragma_Invariant => Invariant : declare
+            Type_Id : Node_Id;
+            Typ     : Entity_Id;
+
+            Discard : Boolean;
+            pragma Unreferenced (Discard);
+
+         begin
+            GNAT_Pragma;
+            Check_At_Least_N_Arguments (2);
+            Check_At_Most_N_Arguments (3);
+            Check_Optional_Identifier (Arg1, Name_Entity);
+            Check_Optional_Identifier (Arg2, Name_Check);
+
+            if Arg_Count = 3 then
+               Check_Optional_Identifier (Arg3, Name_Message);
+               Check_Arg_Is_Static_Expression (Arg3, Standard_String);
+            end if;
+
+            Check_Arg_Is_Local_Name (Arg1);
+
+            Type_Id := Get_Pragma_Arg (Arg1);
+            Find_Type (Type_Id);
+            Typ := Entity (Type_Id);
+
+            if Typ = Any_Type then
+               return;
+
+            elsif not Ekind_In (Typ, E_Private_Type,
+                                     E_Record_Type_With_Private,
+                                     E_Limited_Private_Type)
+            then
+               Error_Pragma_Arg
+                 ("pragma% only allowed for private type", Arg1);
+            end if;
+
+            --  Note that the type has at least one invariant, and also that
+            --  it has inheritable invariants if we have Invariant'Class.
+
+            Set_Has_Invariants (Typ);
+
+            if Class_Present (N) then
+               Set_Has_Inheritable_Invariants (Typ);
+            end if;
+
+            --  The remaining processing is simply to link the pragma on to
+            --  the rep item chain, for processing when the type is frozen.
+            --  This is accomplished by a call to Rep_Item_Too_Late.
+
+            Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
+         end Invariant;
+
          ----------------------
          -- Java_Constructor --
          ----------------------
@@ -13707,6 +13771,7 @@  package body Sem_Prag is
       Pragma_Interrupt_Handler             => -1,
       Pragma_Interrupt_Priority            => -1,
       Pragma_Interrupt_State               => -1,
+      Pragma_Invariant                     => -1,
       Pragma_Java_Constructor              => -1,
       Pragma_Java_Interface                => -1,
       Pragma_Keep_Names                    =>  0,
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 165692)
+++ sem_res.adb	(working copy)
@@ -5930,16 +5930,28 @@  package body Sem_Res is
          Set_Entity_With_Style_Check (N, E);
          Eval_Entity_Name (N);
 
-      --  Allow use of subtype only if it is a concurrent type where we are
-      --  currently inside the body. This will eventually be expanded into a
-      --  call to Self (for tasks) or _object (for protected objects). Any
-      --  other use of a subtype is invalid.
+      --  Case of subtype name appearing as an operand in expression
 
       elsif Is_Type (E) then
+
+         --  Allow use of subtype if it is a concurrent type where we are
+         --  currently inside the body. This will eventually be expanded into a
+         --  call to Self (for tasks) or _object (for protected objects). Any
+         --  other use of a subtype is invalid.
+
          if Is_Concurrent_Type (E)
            and then In_Open_Scopes (E)
          then
             null;
+
+         --  Allow reference to type specifically marked as being OK in this
+         --  context (this is used for example for type names in invariants).
+
+         elsif OK_To_Reference (E) then
+            null;
+
+         --  Any other use is an eror
+
          else
             Error_Msg_N
                ("invalid use of subtype mark in expression or call", N);
Index: exp_ch4.adb
===================================================================
--- exp_ch4.adb	(revision 165693)
+++ exp_ch4.adb	(working copy)
@@ -4349,12 +4349,17 @@  package body Exp_Ch4 is
 
          begin
             if (Is_Entity_Name (Alt) and then Is_Type (Entity (Alt)))
-               or else Nkind (Alt) = N_Range
+              or else Nkind (Alt) = N_Range
             then
-               Cond := Make_In (Sloc (Alt), Left_Opnd  => L, Right_Opnd => R);
+               Cond :=
+                 Make_In (Sloc (Alt),
+                   Left_Opnd  => L,
+                   Right_Opnd => R);
             else
                Cond :=
-                 Make_Op_Eq (Sloc (Alt), Left_Opnd  => L, Right_Opnd => R);
+                 Make_Op_Eq (Sloc (Alt),
+                   Left_Opnd  => L,
+                   Right_Opnd => R);
             end if;
 
             return Cond;
@@ -4472,17 +4477,17 @@  package body Exp_Ch4 is
          begin
             --  If test is explicit x'First .. x'Last, replace by valid check
 
+            --  Could use some individual comments for this complex test ???
+
             if Is_Scalar_Type (Ltyp)
               and then Nkind (Lo_Orig) = N_Attribute_Reference
               and then Attribute_Name (Lo_Orig) = Name_First
               and then Nkind (Prefix (Lo_Orig)) in N_Has_Entity
               and then Entity (Prefix (Lo_Orig)) = Ltyp
-
               and then Nkind (Hi_Orig) = N_Attribute_Reference
               and then Attribute_Name (Hi_Orig) = Name_Last
               and then Nkind (Prefix (Hi_Orig)) in N_Has_Entity
               and then Entity (Prefix (Hi_Orig)) = Ltyp
-
               and then Comes_From_Source (N)
               and then VM_Target = No_VM
             then
@@ -8143,7 +8148,7 @@  package body Exp_Ch4 is
          end if;
 
          Rewrite (N, Relocate_Node (Operand));
-         return;
+         goto Done;
       end if;
 
       --  Nothing to do if this is the second argument of read. This is a
@@ -8154,7 +8159,34 @@  package body Exp_Ch4 is
         and then Attribute_Name (Parent (N)) = Name_Read
         and then Next (First (Expressions (Parent (N)))) = N
       then
-         return;
+         goto Done;
+      end if;
+
+      --  Check for case of converting to a type that has an invariant
+      --  associated with it. This required an invariant check. We convert
+
+      --    typ (expr)
+
+      --  into
+
+      --    do invariant_check (typ (expr)) in typ (expr);
+
+      --  using Duplicate_Subexpr to avoid multiple side effects
+
+      --  Note: the Comes_From_Source check, and then the resetting of this
+      --  flag prevents what would otherwise be an infinite recursion.
+
+      if Present (Invariant_Procedure (Target_Type))
+        and then Comes_From_Source (N)
+      then
+         Set_Comes_From_Source (N, False);
+         Rewrite (N,
+           Make_Expression_With_Actions (Loc,
+             Actions    => New_List (
+               Make_Invariant_Call (Duplicate_Subexpr (N))),
+             Expression => Duplicate_Subexpr_No_Checks (N)));
+         Analyze_And_Resolve (N, Target_Type);
+         goto Done;
       end if;
 
       --  Here if we may need to expand conversion
@@ -8227,7 +8259,7 @@  package body Exp_Ch4 is
                 Expression   => Opnd));
 
             Analyze_And_Resolve (N, Target_Type);
-            return;
+            goto Done;
          end;
       end if;
 
@@ -8300,7 +8332,7 @@  package body Exp_Ch4 is
                       Type_Access_Level (Target_Type)
          then
             Raise_Accessibility_Error;
-            return;
+            goto Done;
          end if;
       end if;
 
@@ -8328,7 +8360,7 @@  package body Exp_Ch4 is
          --  Sem_Ch8, and the expansion can interfere with this error check.
 
          if Is_Access_Type (Target_Type) and then Is_Renamed_Object (N) then
-            return;
+            goto Done;
          end if;
 
          --  Otherwise, proceed with processing tagged conversion
@@ -8410,7 +8442,7 @@  package body Exp_Ch4 is
 
             if Is_Interface (Actual_Op_Typ) then
                Expand_Interface_Conversion (N, Is_Static => False);
-               return;
+               goto Done;
             end if;
 
             if not Tag_Checks_Suppressed (Actual_Targ_Typ) then
@@ -8764,8 +8796,13 @@  package body Exp_Ch4 is
         and then (Vax_Float (Operand_Type) or else Vax_Float (Target_Type))
       then
          Expand_Vax_Conversion (N);
-         return;
+         goto Done;
       end if;
+
+      --  Here at end of processing
+
+      <<Done>>
+         null;
    end Expand_N_Type_Conversion;
 
    -----------------------------------
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 165692)
+++ sem_ch6.adb	(working copy)
@@ -207,7 +207,8 @@  package body Sem_Ch6 is
    --  conditions for the body and assembling and inserting the _postconditions
    --  procedure. N is the node for the subprogram body and Body_Id/Spec_Id are
    --  the entities for the body and separate spec (if there is no separate
-   --  spec, Spec_Id is Empty).
+   --  spec, Spec_Id is Empty). Note that invariants also provide a source
+   --  of postconditions, which are also handled in this procedure.
 
    procedure Set_Formal_Validity (Formal_Id : Entity_Id);
    --  Formal_Id is an formal parameter entity. This procedure deals with
@@ -2940,7 +2941,6 @@  package body Sem_Ch6 is
       if Nkind (N) = N_Function_Specification then
          Set_Ekind (Designator, E_Function);
          Set_Mechanism (Designator, Default_Mechanism);
-
       else
          Set_Ekind (Designator, E_Procedure);
          Set_Etype (Designator, Standard_Void_Type);
@@ -3011,13 +3011,16 @@  package body Sem_Ch6 is
 
       elsif Nkind (N) = N_Function_Specification then
          Push_Scope (Designator);
-
          Analyze_Return_Type (N);
-
          End_Scope;
       end if;
 
+      --  Function case
+
       if Nkind (N) = N_Function_Specification then
+
+         --  Deal with operator symbol case
+
          if Nkind (Designator) = N_Defining_Operator_Symbol then
             Valid_Operator_Definition (Designator);
          end if;
@@ -3041,7 +3044,7 @@  package body Sem_Ch6 is
                Error_Msg_N
                  ("function that returns abstract type must be abstract", N);
 
-            --  Ada 2012 (AI-0073): extend this test to subprograms with an
+            --  Ada 2012 (AI-0073): Extend this test to subprograms with an
             --  access result whose designated type is abstract.
 
             elsif Nkind (Result_Definition (N)) = N_Access_Definition
@@ -6944,7 +6947,7 @@  package body Sem_Ch6 is
 
    procedure List_Inherited_Pre_Post_Aspects (E : Entity_Id) is
    begin
-      if Opt.List_Inherited_Pre_Post
+      if Opt.List_Inherited_Aspects
         and then (Is_Subprogram (E) or else Is_Generic_Subprogram (E))
       then
          declare
@@ -8621,9 +8624,11 @@  package body Sem_Ch6 is
    is
       Loc   : constant Source_Ptr := Sloc (N);
       Prag  : Node_Id;
-      Subp  : Entity_Id;
       Parms : List_Id;
 
+      Designator : Entity_Id;
+      --  Subprogram designator, set from Spec_Id if present, else Body_Id
+
       Precond : Node_Id := Empty;
       --  Set non-Empty if we prepend precondition to the declarations. This
       --  is used to hook up inherited preconditions (adding the condition
@@ -8633,8 +8638,8 @@  package body Sem_Ch6 is
       --  Precondition inherited from parent subprogram
 
       Inherited : constant Subprogram_List :=
-                    Inherited_Subprograms (Spec_Id);
-      --  List of subprograms inherited by this subprogram, null if no Spec_Id
+                     Inherited_Subprograms (Spec_Id);
+      --  List of subprograms inherited by this subprogram
 
       Plist : List_Id := No_List;
       --  List of generated postconditions
@@ -8647,6 +8652,10 @@  package body Sem_Ch6 is
       --  references to parameters of the inherited subprogram to point to the
       --  corresponding parameters of the current subprogram.
 
+      function Invariants_Present return Boolean;
+      --  Determines if any invariants are present for any OUT or IN OUT
+      --  parameters of the subprogram, or (for a function) for the return.
+
       --------------
       -- Grab_PPC --
       --------------
@@ -8672,7 +8681,7 @@  package body Sem_Ch6 is
             begin
                Map := New_Elmt_List;
                PF := First_Formal (Pspec);
-               CF := First_Formal (Spec_Id);
+               CF := First_Formal (Designator);
                while Present (PF) loop
                   Append_Elmt (PF, Map);
                   Append_Elmt (CF, Map);
@@ -8744,9 +8753,49 @@  package body Sem_Ch6 is
          return CP;
       end Grab_PPC;
 
+      ------------------------
+      -- Invariants_Present --
+      ------------------------
+
+      function Invariants_Present return Boolean is
+         Formal     : Entity_Id;
+
+      begin
+         --  Check function return result
+
+         if Ekind (Designator) /= E_Procedure
+           and then Has_Invariants (Etype (Designator))
+         then
+            return True;
+         end if;
+
+         --  Check parameters
+
+         Formal := First_Formal (Designator);
+         while Present (Formal) loop
+            if Ekind (Formal) /= E_In_Parameter
+              and then Has_Invariants (Etype (Formal))
+            then
+               return True;
+            end if;
+
+            Next_Formal (Formal);
+         end loop;
+
+         return False;
+      end Invariants_Present;
+
    --  Start of processing for Process_PPCs
 
    begin
+      --  Capture designator from spec if present, else from body
+
+      if Present (Spec_Id) then
+         Designator := Spec_Id;
+      else
+         Designator := Body_Id;
+      end if;
+
       --  Grab preconditions from spec
 
       if Present (Spec_Id) then
@@ -8882,6 +8931,9 @@  package body Sem_Ch6 is
       --        pragma Check (Postcondition, condition [,message]);
       --        pragma Check (Postcondition, condition [,message]);
       --        ...
+      --        Invariant_Procedure (_Result) ...
+      --        Invariant_Procedure (Arg1)
+      --        ...
       --     end;
 
       --  First we deal with the postconditions in the body
@@ -8933,7 +8985,7 @@  package body Sem_Ch6 is
       --  Now deal with any postconditions from the spec
 
       if Present (Spec_Id) then
-         declare
+         Spec_Postconditions : declare
             procedure Process_Post_Conditions
               (Spec  : Node_Id;
                Class : Boolean);
@@ -8983,6 +9035,8 @@  package body Sem_Ch6 is
                end loop;
             end Process_Post_Conditions;
 
+         --  Start of processing for Spec_Postconditions
+
          begin
             if Present (Spec_PPC_List (Spec_Id)) then
                Process_Post_Conditions (Spec_Id, Class => False);
@@ -8995,32 +9049,79 @@  package body Sem_Ch6 is
                   Process_Post_Conditions (Inherited (J), Class => True);
                end if;
             end loop;
-         end;
+         end Spec_Postconditions;
       end if;
 
-      --  If we had any postconditions and expansion is enabled, build
-      --  the _Postconditions procedure.
+      --  If we had any postconditions and expansion is enabled, or if the
+      --  procedure has invariants, then build the _Postconditions procedure.
 
-      if Present (Plist)
+      if (Present (Plist) or else Invariants_Present)
         and then Expander_Active
       then
-         Subp := Defining_Entity (N);
+         if No (Plist) then
+            Plist := Empty_List;
+         end if;
+
+         --  Special processing for function case
+
+         if Ekind (Designator) /= E_Procedure then
+            declare
+               Rent : constant Entity_Id :=
+                        Make_Defining_Identifier (Loc,
+                          Chars => Name_uResult);
+               Ftyp : constant Entity_Id := Etype (Designator);
+
+            begin
+               Set_Etype (Rent, Ftyp);
+
+               --  Add argument for return
+
+               Parms :=
+                 New_List (
+                   Make_Parameter_Specification (Loc,
+                     Parameter_Type      => New_Occurrence_Of (Ftyp, Loc),
+                     Defining_Identifier => Rent));
+
+               --  Add invariant call if returning type with invariants
+
+               if Present (Invariant_Procedure (Etype (Rent))) then
+                  Append_To (Plist,
+                    Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
+               end if;
+            end;
+
+         --  Procedure rather than a function
 
-         if Etype (Subp) /= Standard_Void_Type then
-            Parms := New_List (
-              Make_Parameter_Specification (Loc,
-                Defining_Identifier =>
-                  Make_Defining_Identifier (Loc,
-                    Chars => Name_uResult),
-                Parameter_Type => New_Occurrence_Of (Etype (Subp), Loc)));
          else
             Parms := No_List;
          end if;
 
+         --  Add invariant calls for parameters. Note that this is done for
+         --  functions as well, since in Ada 2012 they can have IN OUT args.
+
+         declare
+            Formal : Entity_Id;
+
+         begin
+            Formal := First_Formal (Designator);
+            while Present (Formal) loop
+               if Ekind (Formal) /= E_In_Parameter
+                 and then Present (Invariant_Procedure (Etype (Formal)))
+               then
+                  Append_To (Plist,
+                    Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)));
+               end if;
+
+               Next_Formal (Formal);
+            end loop;
+         end;
+
+         --  Build and insert postcondition procedure
+
          declare
             Post_Proc : constant Entity_Id :=
-                   Make_Defining_Identifier (Loc,
-                     Chars => Name_uPostconditions);
+                          Make_Defining_Identifier (Loc,
+                            Chars => Name_uPostconditions);
             --  The entity for the _Postconditions procedure
 
          begin
@@ -9040,20 +9141,12 @@  package body Sem_Ch6 is
             --  If this is a procedure, set the Postcondition_Proc attribute on
             --  the proper defining entity for the subprogram.
 
-            if Etype (Subp) = Standard_Void_Type then
-               if Present (Spec_Id) then
-                  Set_Postcondition_Proc (Spec_Id, Post_Proc);
-               else
-                  Set_Postcondition_Proc (Body_Id, Post_Proc);
-               end if;
+            if Ekind (Designator) = E_Procedure then
+               Set_Postcondition_Proc (Designator, Post_Proc);
             end if;
          end;
 
-         if Present (Spec_Id) then
-            Set_Has_Postconditions (Spec_Id);
-         else
-            Set_Has_Postconditions (Body_Id);
-         end if;
+         Set_Has_Postconditions (Designator);
       end if;
    end Process_PPCs;
 
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 165687)
+++ par-prag.adb	(working copy)
@@ -1172,6 +1172,7 @@  begin
            Pragma_Interrupt_Handler             |
            Pragma_Interrupt_State               |
            Pragma_Interrupt_Priority            |
+           Pragma_Invariant                     |
            Pragma_Java_Constructor              |
            Pragma_Java_Interface                |
            Pragma_Keep_Names                    |
Index: sem_warn.adb
===================================================================
--- sem_warn.adb	(revision 165687)
+++ sem_warn.adb	(working copy)
@@ -3068,7 +3068,7 @@  package body Sem_Warn is
             Elab_Warnings                       := True;
             Implementation_Unit_Warnings        := True;
             Ineffective_Inline_Warnings         := True;
-            List_Inherited_Pre_Post             := True;
+            List_Inherited_Aspects              := True;
             Warn_On_Ada_2005_Compatibility      := True;
             Warn_On_Ada_2012_Compatibility      := True;
             Warn_On_All_Unread_Out_Parameters   := True;
@@ -3115,10 +3115,10 @@  package body Sem_Warn is
             Warn_On_Overlap                     := False;
 
          when 'l' =>
-            List_Inherited_Pre_Post             := True;
+            List_Inherited_Aspects              := True;
 
          when 'L' =>
-            List_Inherited_Pre_Post             := False;
+            List_Inherited_Aspects              := False;
 
          when 'm' =>
             Warn_On_Suspicious_Modulus_Value    := True;
@@ -3196,7 +3196,7 @@  package body Sem_Warn is
       Elab_Warnings                       := False;
       Implementation_Unit_Warnings        := False;
       Ineffective_Inline_Warnings         := True;
-      List_Inherited_Pre_Post             := False;
+      List_Inherited_Aspects              := False;
       Warn_On_Ada_2005_Compatibility      := True;
       Warn_On_Ada_2012_Compatibility      := True;
       Warn_On_All_Unread_Out_Parameters   := False;
@@ -3239,7 +3239,7 @@  package body Sem_Warn is
             Constant_Condition_Warnings         := True;
             Implementation_Unit_Warnings        := True;
             Ineffective_Inline_Warnings         := True;
-            List_Inherited_Pre_Post             := True;
+            List_Inherited_Aspects              := True;
             Warn_On_Ada_2005_Compatibility      := True;
             Warn_On_Ada_2012_Compatibility      := True;
             Warn_On_Assertion_Failure           := True;
@@ -3270,7 +3270,7 @@  package body Sem_Warn is
             Elab_Warnings                       := False;
             Implementation_Unit_Warnings        := False;
             Ineffective_Inline_Warnings         := False;
-            List_Inherited_Pre_Post             := False;
+            List_Inherited_Aspects              := False;
             Warn_On_Ada_2005_Compatibility      := False;
             Warn_On_Ada_2012_Compatibility      := False;
             Warn_On_All_Unread_Out_Parameters   := False;
Index: opt.ads
===================================================================
--- opt.ads	(revision 165692)
+++ opt.ads	(working copy)
@@ -739,10 +739,10 @@  package Opt is
    --  Set to True to skip compile and bind steps (except when Bind_Only is
    --  set to True).
 
-   List_Inherited_Pre_Post : Boolean := True;
+   List_Inherited_Aspects : Boolean := True;
    --  GNAT
-   --  List inherited preconditions and postconditions from Pre'Class and
-   --  Post'Class aspects for ancestor subprograms.
+   --  List inherited invariants, preconditions, and postconditions from
+   --  Invariant'Class, Pre'Class, and Post'Class aspects.
 
    List_Restrictions : Boolean := False;
    --  GNATBIND
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 165687)
+++ sem_ch13.adb	(working copy)
@@ -54,6 +54,7 @@  with Sinput;   use Sinput;
 with Snames;   use Snames;
 with Stand;    use Stand;
 with Sinfo;    use Sinfo;
+with Stringt;  use Stringt;
 with Targparm; use Targparm;
 with Ttypes;   use Ttypes;
 with Tbuild;   use Tbuild;
@@ -740,9 +741,9 @@  package body Sem_Ch13 is
                when No_Aspect =>
                   raise Program_Error;
 
-                  --  Aspects taking an optional boolean argument. For all of
-                  --  these we just create a matching pragma and insert it,
-                  --  setting flag Cancel_Aspect if the expression is False.
+               --  Aspects taking an optional boolean argument. For all of
+               --  these we just create a matching pragma and insert it,
+               --  setting flag Cancel_Aspect if the expression is False.
 
                when Aspect_Ada_2005                     |
                     Aspect_Ada_2012                     |
@@ -803,8 +804,7 @@  package body Sem_Ch13 is
                      end if;
                   end if;
 
-               --  Aspects corresponding to attribute definition clauses with
-               --  the exception of Address which is treated specially.
+               --  Aspects corresponding to attribute definition clauses
 
                when Aspect_Address        |
                     Aspect_Alignment      |
@@ -924,7 +924,8 @@  package body Sem_Ch13 is
                --  with a first argument that is the expression, and a second
                --  argument that is an informative message if the test fails.
                --  This is inserted right after the declaration, to get the
-               --  required pragma placement.
+               --  required pragma placement. The processing for the pragmas
+               --  takes care of the required delay.
 
                when Aspect_Pre | Aspect_Post => declare
                   Pname : Name_Id;
@@ -1007,11 +1008,48 @@  package body Sem_Ch13 is
                   goto Continue;
                end;
 
-                  --  Aspects currently unimplemented
+               --  Invariant aspect generates an Invariant pragma with a first
+               --  argument that is the entity, and the second argument is the
+               --  expression. This is inserted right after the declaration, to
+               --  get the required pragma placement. The processing for the
+               --  pragma takes care of the required delay.
 
-               when Aspect_Invariant |
-                    Aspect_Predicate =>
+               when Aspect_Invariant =>
 
+                  --  Construct the pragma
+
+                  Aitem :=
+                    Make_Pragma (Loc,
+                      Pragma_Argument_Associations =>
+                        New_List (Ent, Relocate_Node (Expr)),
+                      Class_Present                => Class_Present (Aspect),
+                      Pragma_Identifier            =>
+                        Make_Identifier (Sloc (Id), Name_Invariant));
+
+                  --  Add message unless exception messages are suppressed
+
+                  if not Opt.Exception_Locations_Suppressed then
+                     Append_To (Pragma_Argument_Associations (Aitem),
+                       Make_Pragma_Argument_Association (Eloc,
+                         Chars     => Name_Message,
+                         Expression =>
+                           Make_String_Literal (Eloc,
+                             Strval => "failed invariant from "
+                                       & Build_Location_String (Eloc))));
+                  end if;
+
+                  Set_From_Aspect_Specification (Aitem, True);
+
+                  --  For Invariant case, insert immediately after the entity
+                  --  declaration. We do not have to worry about delay issues
+                  --  since the pragma processing takes care of this.
+
+                  Insert_After (N, Aitem);
+                  goto Continue;
+
+               --  Aspects currently unimplemented
+
+               when Aspect_Predicate =>
                   Error_Msg_N ("aspect& not implemented", Identifier (Aspect));
                   goto Continue;
             end case;
@@ -3393,6 +3431,329 @@  package body Sem_Ch13 is
       end if;
    end Analyze_Record_Representation_Clause;
 
+   -------------------------------
+   -- Build_Invariant_Procedure --
+   -------------------------------
+
+   --  The procedure that is constructed here has the form
+
+   --  procedure typInvariant (Ixxx : typ) is
+   --  begin
+   --     pragma Check (Invariant, exp, "failed invariant from xxx");
+   --     pragma Check (Invariant, exp, "failed invariant from xxx");
+   --     ...
+   --     pragma Check (Invariant, exp, "failed inherited invariant from xxx");
+   --     ...
+   --  end typInvariant;
+
+   procedure Build_Invariant_Procedure
+     (Typ   : Entity_Id;
+      PDecl : out Node_Id;
+      PBody : out Node_Id)
+   is
+      Loc   : constant Source_Ptr := Sloc (Typ);
+      Stmts : List_Id;
+      Spec  : Node_Id;
+      SId   : Entity_Id;
+
+      procedure Add_Invariants (T : Entity_Id; Inherit : Boolean);
+      --  Appends statements to Stmts for any invariants in the rep item chain
+      --  of the given type. If Inherit is False, then we only process entries
+      --  on the chain for the type Typ. If Inherit is True, then we ignore any
+      --  Invariant aspects, but we process all Invariant'Class aspects, adding
+      --  "inherited" to the exception message and generating an informational
+      --  message about the inheritance of an invariant.
+
+      Object_Name : constant Name_Id := New_Internal_Name ('I');
+      --  Name for argument of invariant procedure
+
+      --------------------
+      -- Add_Invariants --
+      --------------------
+
+      procedure Add_Invariants (T : Entity_Id; Inherit : Boolean) is
+         Ritem : Node_Id;
+         Arg1  : Node_Id;
+         Arg2  : Node_Id;
+         Arg3  : Node_Id;
+         Exp   : Node_Id;
+         Loc   : Source_Ptr;
+         Assoc : List_Id;
+         Str   : String_Id;
+
+         function Replace_Node (N : Node_Id) return Traverse_Result;
+         --  Process single node for traversal to replace type references
+
+         procedure Replace_Type is new Traverse_Proc (Replace_Node);
+         --  Traverse an expression changing every occurrence of an entity
+         --  reference to type T with a reference to the object argument.
+
+         ------------------
+         -- Replace_Node --
+         ------------------
+
+         function Replace_Node (N : Node_Id) return Traverse_Result is
+         begin
+            --  Case of entity name referencing the type
+
+            if Is_Entity_Name (N)
+              and then Entity (N) = T
+            then
+               --  Invariant'Class, replace with T'Class (obj)
+
+               if Class_Present (Ritem) then
+                  Rewrite (N,
+                    Make_Type_Conversion (Loc,
+                      Subtype_Mark =>
+                        Make_Attribute_Reference (Loc,
+                          Prefix         =>
+                            New_Occurrence_Of (T, Loc),
+                          Attribute_Name => Name_Class),
+                      Expression =>
+                        Make_Identifier (Loc,
+                          Chars => Object_Name)));
+
+               --  Invariant, replace with obj
+
+               else
+                  Rewrite (N,
+                    Make_Identifier (Loc,
+                      Chars => Object_Name));
+               end if;
+
+               --  All done with this node
+
+               return Skip;
+
+            --  Not an instance of the type entity, keep going
+
+            else
+               return OK;
+            end if;
+         end Replace_Node;
+
+      --  Start of processing for Add_Invariants
+
+      begin
+         Ritem := First_Rep_Item (T);
+         while Present (Ritem) loop
+            if Nkind (Ritem) = N_Pragma
+              and then Pragma_Name (Ritem) = Name_Invariant
+            then
+               Arg1 := First (Pragma_Argument_Associations (Ritem));
+               Arg2 := Next (Arg1);
+               Arg3 := Next (Arg2);
+
+               Arg1 := Get_Pragma_Arg (Arg1);
+               Arg2 := Get_Pragma_Arg (Arg2);
+
+               --  For Inherit case, ignore Invariant, process only Class case
+
+               if Inherit then
+                  if not Class_Present (Ritem) then
+                     goto Continue;
+                  end if;
+
+               --  For Inherit false, process only item for right type
+
+               else
+                  if Entity (Arg1) /= Typ then
+                     goto Continue;
+                  end if;
+               end if;
+
+               if No (Stmts) then
+                  Stmts := Empty_List;
+               end if;
+
+               Exp := New_Copy_Tree (Arg2);
+               Loc := Sloc (Exp);
+
+               --  We need to replace any occurrences of the name of the type
+               --  with references to the object, converted to type'Class in
+               --  the case of Invariant'Class aspects. We do this by first
+               --  doing a preanalysis, to identify all the entities, then
+               --  we traverse looking for the type entity, and doing the
+               --  necessary substitution. The preanalysis is done with the
+               --  special OK_To_Reference flag set on the type, so that if
+               --  we get an occurrence of this type, it will be reognized
+               --  as legitimate.
+
+               Set_OK_To_Reference (T, True);
+               Preanalyze_Spec_Expression (Exp, Standard_Boolean);
+               Set_OK_To_Reference (T, False);
+
+               --  Do the traversal
+
+               Replace_Type (Exp);
+
+               --  Build first two arguments for Check pragma
+
+               Assoc := New_List (
+                 Make_Pragma_Argument_Association (Loc,
+                    Expression =>
+                      Make_Identifier (Loc,
+                        Chars => Name_Invariant)),
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Exp));
+
+               --  Add message if present in Invariant pragma
+
+               if Present (Arg3) then
+                  Str := Strval (Get_Pragma_Arg (Arg3));
+
+                  --  If inherited case, and message starts "failed invariant",
+                  --  change it to be "failed inherited invariant".
+
+                  if Inherit then
+                     String_To_Name_Buffer (Str);
+
+                     if Name_Buffer (1 .. 16) = "failed invariant" then
+                        Insert_Str_In_Name_Buffer ("inherited ", 8);
+                        Str := String_From_Name_Buffer;
+                     end if;
+                  end if;
+
+                  Append_To (Assoc,
+                    Make_Pragma_Argument_Association (Loc,
+                      Expression => Make_String_Literal (Loc, Str)));
+               end if;
+
+               --  Add Check pragma to list of statements
+
+               Append_To (Stmts,
+                 Make_Pragma (Loc,
+                   Pragma_Identifier            =>
+                     Make_Identifier (Loc,
+                       Chars => Name_Check),
+                   Pragma_Argument_Associations => Assoc));
+
+               --  If Inherited case and option enabled, output info msg. Note
+               --  that we know this is a case of Invariant'Class.
+
+               if Inherit and Opt.List_Inherited_Aspects then
+                  Error_Msg_Sloc := Sloc (Ritem);
+                  Error_Msg_N
+                    ("?info: & inherits `Invariant''Class` aspect from #",
+                     Typ);
+               end if;
+            end if;
+
+         <<Continue>>
+            Next_Rep_Item (Ritem);
+         end loop;
+      end Add_Invariants;
+
+   --  Start of processing for Build_Invariant_Procedure
+
+   begin
+      Stmts := No_List;
+      PDecl := Empty;
+      PBody := Empty;
+
+      --  Add invariants for the current type
+
+      Add_Invariants (Typ, Inherit => False);
+
+      --  Add invariants for parent types
+
+      declare
+         Current_Typ : Entity_Id;
+         Parent_Typ  : Entity_Id;
+
+      begin
+         Current_Typ := Typ;
+         loop
+            Parent_Typ := Etype (Current_Typ);
+
+            if Is_Private_Type (Parent_Typ)
+              and then Present (Full_View (Base_Type (Parent_Typ)))
+            then
+               Parent_Typ := Full_View (Base_Type (Parent_Typ));
+            end if;
+
+            exit when Parent_Typ = Current_Typ;
+
+            Current_Typ := Parent_Typ;
+            Add_Invariants (Current_Typ, Inherit => True);
+         end loop;
+      end;
+
+      --  Add invariants for inherited interfaces
+      --  (commented out because it blows up on simpleinv in J701-022)
+
+--        declare
+--           Ifaces : Elist_Id;
+--           Iface  : Elmt_Id;
+--
+--        begin
+--           Collect_Interfaces
+--             (T               => Typ,
+--              Ifaces_List     => Ifaces,
+--              Exclude_Parents => True,
+--              Use_Full_View   => True);
+--
+--           loop
+--              Iface := First_Elmt (Ifaces);
+--              exit when Iface = No_Elmt;
+--              Add_Invariants (Node (Iface), Inherit => True);
+--              Remove_Elmt (Ifaces, Iface);
+--           end loop;
+--        end;
+
+      --  Build the procedure if we generated at least one Check pragma
+
+      if Stmts /= No_List then
+
+         --  Build procedure declaration
+
+         SId :=
+           Make_Defining_Identifier (Loc,
+             Chars => New_External_Name (Chars (Typ), "Invariant"));
+         Set_Invariant_Procedure (Typ, SId);
+
+         Spec :=
+           Make_Procedure_Specification (Loc,
+             Defining_Unit_Name       => SId,
+             Parameter_Specifications => New_List (
+               Make_Parameter_Specification (Loc,
+                 Defining_Identifier =>
+                   Make_Defining_Identifier (Loc,
+                     Chars => Object_Name),
+                 Parameter_Type =>
+                   New_Occurrence_Of (Typ, Loc))));
+
+         PDecl :=
+           Make_Subprogram_Declaration (Loc,
+             Specification => Spec);
+
+         --  Build procedure body
+
+         SId :=
+           Make_Defining_Identifier (Loc,
+             Chars => New_External_Name (Chars (Typ), "Invariant"));
+
+         Spec :=
+           Make_Procedure_Specification (Loc,
+             Defining_Unit_Name       => SId,
+             Parameter_Specifications => New_List (
+               Make_Parameter_Specification (Loc,
+                 Defining_Identifier =>
+                   Make_Defining_Identifier (Loc,
+                     Chars => Object_Name),
+                 Parameter_Type =>
+                   New_Occurrence_Of (Typ, Loc))));
+
+         PBody :=
+           Make_Subprogram_Body (Loc,
+             Specification              => Spec,
+             Declarations               => Empty_List,
+             Handled_Statement_Sequence =>
+               Make_Handled_Sequence_Of_Statements (Loc,
+                 Statements => Stmts));
+      end if;
+   end Build_Invariant_Procedure;
+
    -----------------------------------
    -- Check_Constant_Address_Clause --
    -----------------------------------
Index: sem_ch13.ads
===================================================================
--- sem_ch13.ads	(revision 165687)
+++ sem_ch13.ads	(working copy)
@@ -52,6 +52,17 @@  package Sem_Ch13 is
    --  order is specified and there is at least one component clause. Adjusts
    --  component positions according to either Ada 95 or Ada 2005 (AI-133).
 
+   procedure Build_Invariant_Procedure
+     (Typ   : Entity_Id;
+      PDecl : out Node_Id;
+      PBody : out Node_Id);
+   --  If Typ has Invariants (indicated by Has_Invariants being set for Typ,
+   --  indicating the presence of Pragma Invariant entries on the rep chain,
+   --  note that Invariant aspects are converted to pragma Invariant), then
+   --  this procedure builds the spec and body for the corresponding Invariant
+   --  procedure, returning themn in PDecl and PBody. In some error situations
+   --  no procedure is built, in which case PDecl/PBody are empty on return.
+
    procedure Check_Record_Representation_Clause (N : Node_Id);
    --  This procedure completes the analysis of a record representation clause
    --  N. It is called at freeze time after adjustment of component clause bit
Index: treepr.adb
===================================================================
--- treepr.adb	(revision 165687)
+++ treepr.adb	(working copy)
@@ -636,6 +636,14 @@  package body Treepr is
          Print_Eol;
       end if;
 
+      if Field_Present (Field29 (Ent)) then
+         Print_Str (Prefix);
+         Write_Field29_Name (Ent);
+         Write_Str (" = ");
+         Print_Field (Field29 (Ent));
+         Print_Eol;
+      end if;
+
       Write_Entity_Flags (Ent, Prefix);
    end Print_Entity_Info;
 
Index: atree.h
===================================================================
--- atree.h	(revision 165689)
+++ atree.h	(working copy)
@@ -382,7 +382,7 @@  extern Node_Id Current_Error_Node;
 #define Field26(N)    (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field8)
 #define Field27(N)    (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field9)
 #define Field28(N)    (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field10)
-#define Field29(N)    (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field11)
+#define Field29(N)    (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.X.field11)
 
 #define Node1(N)      Field1  (N)
 #define Node2(N)      Field2  (N)
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 165692)
+++ snames.ads-tmpl	(working copy)
@@ -137,7 +137,6 @@  package Snames is
    --  Names of aspects for which there are no matching pragmas or attributes
    --  so that they need to be included for aspect specification use.
 
-   Name_Invariant                      : constant Name_Id := N + $;
    Name_Post                           : constant Name_Id := N + $;
    Name_Pre                            : constant Name_Id := N + $;
    Name_Predicate                      : constant Name_Id := N + $;
@@ -483,6 +482,7 @@  package Snames is
    Name_Interface_Name                 : constant Name_Id := N + $; -- GNAT
    Name_Interrupt_Handler              : constant Name_Id := N + $;
    Name_Interrupt_Priority             : constant Name_Id := N + $;
+   Name_Invariant                      : constant Name_Id := N + $; -- GNAT
    Name_Java_Constructor               : constant Name_Id := N + $; -- GNAT
    Name_Java_Interface                 : constant Name_Id := N + $; -- GNAT
    Name_Keep_Names                     : constant Name_Id := N + $; -- GNAT
@@ -1566,6 +1566,7 @@  package Snames is
       Pragma_Interface_Name,
       Pragma_Interrupt_Handler,
       Pragma_Interrupt_Priority,
+      Pragma_Invariant,
       Pragma_Java_Constructor,
       Pragma_Java_Interface,
       Pragma_Keep_Names,
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb	(revision 165687)
+++ exp_ch3.adb	(working copy)
@@ -4570,6 +4570,19 @@  package body Exp_Ch3 is
 
       if No (Expr) then
 
+         --  For the default initialization case, if we have a private type
+         --  with invariants, and invariant checks are enabled, then insert an
+         --  invariant check after the object declaration. Note that it is OK
+         --  to clobber the object with an invalid value since if the exception
+         --  is raised, then the object will go out of scope.
+
+         if Is_Private_Type (Typ)
+           and then Present (Invariant_Procedure (Typ))
+         then
+            Insert_After (N,
+              Make_Invariant_Call (New_Occurrence_Of (Def_Id, Loc)));
+         end if;
+
          --  Expand Initialize call for controlled objects. One may wonder why
          --  the Initialize Call is not done in the regular Init procedure
          --  attached to the record type. That's because the init procedure is
@@ -5176,9 +5189,10 @@  package body Exp_Ch3 is
             Set_Renamed_Object (Defining_Identifier (N), Expr_Q);
             Set_Analyzed (N);
          end if;
-
       end if;
 
+   --  Exception on library entity not available
+
    exception
       when RE_Not_Available =>
          return;