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;
