[Ada] Reimplementation of type invariants

Arnaud Charlet charlet@adacore.com
Mon Jun 20 12:22:00 GMT 2016


This patch reimplements the processing of type invariants in order to plug
various static and run-time semantic holes. The invariants of a private type
are resolved and checked at run-time by a "partial" invariant procedure. The
invariants of a private type's full view, any inherited class-wide invariants
of parent types or interfaces, any invariants on array elements or record
components, and the invariants of the partial view are resolved and checked at
run-time by a "full" invariant procedure.

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

--  tester.ads

package Tester is
   type Type_Id is
     (Ext_1_Id,
      Ext_1_FV_Id,
      Ext_2_Id,
      Ext_3_Id,
      Ext_4_Id,
      Ext_4_FV_Id,
      Ext_5_Id,
      Ext_6_Id,
      Ext_6_FV_Id,
      Ext_7_Id,
      Ext_8_Id,
      Iface_1_Id,
      Iface_2_Id,
      Iface_3_Id,
      Iface_4_Id,
      Par_1_Id,
      Par_2_FV_Id,
      Par_3_Id,
      Par_4_Id,
      Par_4_FV_Id,
      Prot_1_FV_Id,
      Prot_2_Id,
      Prot_3_Id,
      Prot_3_FV_Id,
      Synch_1_Id,
      Synch_2_Id,
      Tag_1_Id,
      Tag_2_Id,
      Tag_3_Id,
      Tag_4_Id,
      Tag_4_FV_Id,
      Tag_5_Id,
      Tag_6_Id,
      Tag_7_Id,
      Tag_8_Id,
      Tag_9_Id,
      Tag_10_Id,
      Tag_11_Id,
      Tag_12_Id,
      Tag_13_Id,
      Tag_14_Id,
      Tag_15_Id,
      Tag_15_FV_Id,
      Tag_16_Id,
      Tag_17_Id,
      Tag_18_Id,
      Tag_19_Id,
      Tag_20_Id,
      Tag_20_FV_Id,
      Tag_21_Id,
      Tag_22_Id,
      Tag_23_Id,
      Tag_24_Id,
      Tag_24_FV_Id,
      Tag_25_Id,
      Tag_26_Id,
      Tag_27_Id,
      Tag_28_Id,
      Task_1_Id,
      Task_2_Id,
      Task_2_FV_Id,
      Untag_1_Id,
      Untag_2_Id,
      Untag_3_Id,
      Untag_4_Id,
      Untag_5_Id,
      Untag_6_Id,
      Untag_7_Id,
      Untag_8_Id,
      Untag_9_Id);

   type Results is array (Type_Id) of Boolean;

   function Mark (Typ : Type_Id) return Boolean;
   --  Mark the result for a particular type as verified. The function always
   --  returns True.

   procedure Reset_Results;
   --  Reset the internally kept result state

   procedure Test_Results (Test_Id : String; Exp : Results);
   --  Ensure that the internally kept result state agrees with expected
   --  results Exp. Emit an error if this is not the case.
end Tester;

--  tester.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Tester is
   State : Results;

   ----------
   -- Mark --
   ----------

   function Mark (Typ : Type_Id) return Boolean is
   begin
      State (Typ) := True;
      return True;
   end Mark;

   -------------------
   -- Reset_Results --
   -------------------

   procedure Reset_Results is
   begin
      State := (others => False);
   end Reset_Results;

   ------------------
   -- Test_Results --
   ------------------

   procedure Test_Results (Test_Id : String; Exp : Results) is
      Exp_Val   : Boolean;
      Posted    : Boolean := False;
      State_Val : Boolean;

   begin
      for Index in Results'Range loop
         Exp_Val   := Exp (Index);
         State_Val := State (Index);

         if State_Val /= Exp_Val then
            if not Posted then
               Posted := True;
               Put_Line (Test_Id & ": ERROR");
            end if;

            Put_Line ("  Expected: " & Exp_Val'Img & " for " & Index'Img);
            Put_Line ("  Got:      " & State_Val'Img);
         end if;
      end loop;

      if not Posted then
         Put_Line (Test_Id & ": OK");
      end if;
   end Test_Results;
end Tester;

--  invariants_aspects.ads

with Tester; use Tester;

package Invariants_Aspects is

   ----------------
   -- Interfaces --
   ----------------

   type Iface_1 is interface
     with Type_Invariant'Class => Mark (Iface_1_Id);

   type Iface_2 is interface
     with Type_Invariant'Class => Mark (Iface_2_Id);

   type Iface_3 is interface and Iface_1 and Iface_2;

   type Iface_4 is interface and Iface_3
     with Type_Invariant'Class => Mark (Iface_4_Id);

   type Synch_1 is synchronized interface
     with Type_Invariant'Class => Mark (Synch_1_Id);

   type Synch_2 is synchronized interface and Synch_1
     with Type_Invariant'Class => Mark (Synch_2_Id);

   ------------------
   -- Tagged types --
   ------------------

   type Tag_1 is tagged private;

   type Tag_2 is tagged private;

   type Tag_3 is tagged private
     with Type_Invariant => Mark (Tag_3_Id);

   type Tag_4 is tagged private
     with Type_Invariant'Class => Mark (Tag_4_Id);

   --  Derivations without invariants

   type Tag_5 is new Tag_2 with private;
   type Tag_6 is new Tag_3 with private;
   type Tag_7 is new Tag_4 with private;

   --  Derivations with invariants on the full view

   type Tag_8  is new Tag_2 with private;
   type Tag_9  is new Tag_3 with private;
   type Tag_10 is new Tag_4 with private;

   --  Derivations with invariants

   type Tag_11 is new Tag_2 with private
     with Type_Invariant => Mark (Tag_11_Id);

   type Tag_12 is new Tag_3 with private
     with Type_Invariant => Mark (Tag_12_Id);

   type Tag_13 is new Tag_4 with private
     with Type_Invariant => Mark (Tag_13_Id);

   --  Derivations with class-wide invariants

   type Tag_14 is new Tag_2 with private
     with Type_Invariant'Class => Mark (Tag_14_Id);

   type Tag_15 is new Tag_3 with private
     with Type_Invariant'Class => Mark (Tag_15_Id);

   type Tag_16 is new Tag_4 with private
     with Type_Invariant'Class => Mark (Tag_16_Id);

   --  Derivations with interfaces

   type Tag_17 is new Tag_1 and Iface_1 and Iface_2
                            and Iface_3 and Iface_4 with private;

   type Tag_18 is new Tag_6 and Iface_1 and Iface_4 with private;

   type Tag_19 is new Tag_10 and Iface_2 and Iface_3 with private
     with Type_Invariant => Mark (Tag_19_Id);

   type Tag_20 is new Tag_11 and Iface_4 with private
     with Type_Invariant'Class => Mark (Tag_20_Id);

   --  Derivations with a hidden parent

   type Tag_21 is tagged private;

   type Tag_22 is tagged private;

   type Tag_23 is tagged private
     with Type_Invariant => Mark (Tag_23_Id);

   type Tag_24 is tagged private
     with Type_Invariant'Class => Mark (Tag_24_Id);

   --  Derivations with more derived parents

   type Tag_25 is new Tag_4 with private;

   type Tag_26 is new Tag_3 with private;

   type Tag_27 is new Tag_2 with private
     with Type_Invariant => Mark (Tag_27_Id);

   type Tag_28 is new Tag_4 with private
     with Type_Invariant'Class => Mark (Tag_28_Id);

   --  Parents of extensions

   type Par_1 (Discr_1 : Boolean) is tagged private;

   type Par_2 is tagged private;

   type Par_3 is tagged private
     with Type_Invariant => Mark (Par_3_Id);

   type Par_4 (Discr_1 : Boolean) is tagged private
     with Type_Invariant'Class => Mark (Par_4_Id);

   --  Extensions

   type Ext_1 is new Par_1 with private;

   type Ext_2 is new Par_1 with private
     with Type_Invariant => Mark (Ext_2_Id);

   type Ext_3 is new Par_2 with private;

   type Ext_4 is new Par_2 with private
     with Type_Invariant'Class => Mark (Ext_4_Id);

   type Ext_5 is new Par_3 with private
     with Type_Invariant => Mark (Ext_5_Id);

   type Ext_6 is new Par_3 with private;

   type Ext_7 is new Par_4 with private;

   type Ext_8 is new Par_4 with private
     with Type_Invariant => Mark (Ext_8_Id);

   --  Protected types

   type Prot_1 is limited private;

   type Prot_2 is limited private
     with Type_Invariant => Mark (Prot_2_Id);

   type Prot_3 is synchronized new Synch_2 with private
     with Type_Invariant'Class => Mark (Prot_3_Id);

   --  Task types

   type Task_1 is limited private
     with Type_Invariant => Mark (Task_1_Id);

   type Task_2 is synchronized new Synch_1 with private
     with Type_Invariant'Class => Mark (Task_2_Id);

   --------------------
   -- Untagged types --
   --------------------

   type Untag_1 is private;

   type Untag_2 is private;

   type Untag_3 is private
     with Type_Invariant => Mark (Untag_3_Id);

   --  Composite types with invariants carrying invariants

   type Untag_4 is private;

   type Untag_5 is private;

   type Untag_6 is private;

   type Untag_7 is private;

   type Untag_8 (Discr : Boolean) is private;

   type Untag_9 (<>) is private;

   procedure Test_Deriv_1;
   procedure Test_Deriv_2;
   procedure Test_Deriv_3;
   procedure Test_Deriv_4;
   procedure Test_Deriv_5;

   procedure Test_Sub_1;
   procedure Test_Sub_2;
   procedure Test_Sub_3;
   procedure Test_Sub_4;
   procedure Test_Sub_5;

   procedure Test_Untag_9_TT;
   procedure Test_Untag_9_TF;
   procedure Test_Untag_9_FT;
   procedure Test_Untag_9_FF;

private
   type Tag_1 is tagged null record;
   --  none

   type Tag_2 is tagged null record
     with Type_Invariant => Mark (Tag_2_Id);
   --  own: Tag_2_Id

   type Tag_3 is tagged null record;
   --  own: Tag_3_Id

   type Tag_4 is tagged null record
     with Type_Invariant => Mark (Tag_4_FV_Id);
   --  own:         Tag_4_Id, Tag_4_FV_Id
   --  inheritable: Tag_4_Id

   type Tag_5 is new Tag_2 with null record;
   --  none

   type Tag_6 is new Tag_3 with null record;
   --  none

   type Tag_7 is new Tag_4 with null record;
   --  inherited: Tag_4_Id

   type Tag_8 is new Tag_2 with null record
     with Type_Invariant => Mark (Tag_8_Id);
   --  own: Tag_8_Id

   type Tag_9 is new Tag_3 with null record
     with Type_Invariant => Mark (Tag_9_Id);
   --  own: Tag_9_Id

   type Tag_10 is new Tag_4 with null record
     with Type_Invariant => Mark (Tag_10_Id);
   --  own:       Tag_10_Id
   --  inherited: Tag_4_Id

   type Tag_11 is new Tag_2 with null record;
   --  own: Tag_11_Id

   type Tag_12 is new Tag_3 with null record;
   --  own: Tag_12_Id

   type Tag_13 is new Tag_4 with null record;
   --  own:       Tag_13_Id
   --  inherited: Tag_4_Id

   type Tag_14 is new Tag_2 with null record;
   --  own: Tag_14_Id

   type Tag_15 is new Tag_3 with null record
     with Type_Invariant => Mark (Tag_15_FV_Id);
   --  own: Tag_15_Id, Tag_15_FV_Id

   type Tag_16 is new Tag_4 with null record;
   --  own:         Tag_16_Id
   --  inheritable: Tag_16_Id
   --  inherited:   Tag_4_Id

   type Tag_17 is new Tag_1 and Iface_1 and Iface_2
                            and Iface_3 and Iface_4 with null record;
   --  inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id

   type Tag_18 is new Tag_6 and Iface_1 and Iface_4 with null record
     with Type_Invariant => Mark (Tag_18_Id);
   --  own:       Tag_18_Id
   --  inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id

   type Tag_19 is new Tag_10 and Iface_2 and Iface_3 with null record;
   --  own:       Tag_19_Id
   --  inherited: Iface_1_Id, Iface_2_Id, Tag_4_Id

   type Tag_20 is new Tag_11 and Iface_4 with null record
     with Type_Invariant => Mark (Tag_20_FV_Id);
   --  own:         Tag_20_Id, Tag_20_FV_Id
   --  inheritable: Tag_20_Id
   --  inherited  : Iface_1_Id, Iface_2_Id, Iface_4_Id

   type Tag_21 is new Tag_15 with null record;
   --  inherited: Tag_15_Id

   type Tag_22 is new Tag_13 with null record
     with Type_Invariant => Mark (Tag_22_Id);
   --  own:       Tag_22_Id
   --  inherited: Tag_4_Id

   type Tag_23 is new Tag_9 with null record;
   --  own: Tag_23_Id

   type Tag_24 is new Tag_15 with null record
     with Type_Invariant => Mark (Tag_24_FV_Id);
   --  own:         Tag_24_Id, Tag_24_FV_Id
   --  inheritable: Tag_24_Id
   --  inherited:   Tag_15_Id

   type Tag_25 is new Tag_13 with null record;
   --  inherited: Tag_4_Id

   type Tag_26 is new Tag_15 with null record
     with Type_Invariant => Mark (Tag_26_Id);
   --  own:       Tag_26_Id
   --  inherited: Tag_15_Id

   type Tag_27 is new Tag_14 with null record;
   --  own:       Tag_27_Id
   --  inherited: Tag_14_Id

   type Tag_28 is new Tag_13 with null record;
   --  own:       Tag_28_Id
   --  inherited: Tag_4_Id

   type Par_1 (Discr_1 : Boolean) is tagged record
      Comp_1 : Tag_8;  --  Tag_8_Id

      case Discr_1 is
         when True =>
            Comp_2 : Tag_10;  --  Tag_4_Id, Tag_10_Id

         when others =>
            Comp_3 : Tag_19;  --  Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id
      end case;
   end record;

   type Par_2 is tagged record
      Comp_1 : Tag_22;  --  Tag_4_Id, Tag_22_Id
      Comp_2 : Tag_24;  --  Tag_15_Id, Tag_24_Id, Tag_24_FV_Id
   end record
     with Type_Invariant => Mark (Par_2_FV_Id);
   --  own:   Par_2_FV_Id
   --  calls: Tag_4_Id, Tag_15_Id, Tag_22_Id, Tag_24_Id, Tag_24_FV_Id

   type Par_3 is tagged record
      Comp_1 : Tag_1;  --  none
      Comp_2 : Tag_6;  --  none
   end record;
   --  own: Par_3_Id

   type Par_4 (Discr_1 : Boolean) is tagged record
      case Discr_1 is
         when True =>
            Comp_1 : Tag_5;  --  none

         when others =>
            Comp_2 : Tag_6;  --  none
      end case;
   end record
     with Type_Invariant => Mark (Par_4_FV_Id);
   --  own:         Par_4_Id, Par_4_FV_Id
   --  inheritable: Par_4_Id

   type Ext_1 is new Par_1 with record
      Comp_4 : Tag_26;  --  Tag_15_Id, Tag_26_Id
      Comp_5 : Tag_20;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_20_Id,
                        --  Tag_20_FV_Id
   end record
     with Type_Invariant => Mark (Ext_1_FV_Id);
   --  calls: must be calculated
   --  own:   Ext_1_FV_Id

   type Ext_2 is new Par_1 with record
      Comp_4 : Tag_1;  --  none
   end record;
   --  calls: must be calculated
   --  own:   Ext_2_Id

   type Ext_3 is new Par_2 with record
      Comp_3 : Tag_19;  --  Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id
   end record;
   --  calls: Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_15_Id, Tag_19_Id,
   --         Tag_22_Id, Tag_24_Id, Tag_24_FV_Id

   type Ext_4 is new Par_2 with record
      Comp_3 : Tag_14;  --  Tag_14_Id
      Comp_4 : Tag_25;  --  Tag_4_Id
   end record
     with Type_Invariant => Mark (Ext_4_FV_Id);
   --  calls:       Tag_4_Id, Tag_14_Id, Tag_15_Id, Tag_22_Id, Tag_24_Id,
   --               Tag_24_FV_Id
   --  own:         Ext_4_Id, Ext_4_FV_Id
   --  inheritable: Ext_4_Id

   type Ext_5 is new Par_3 with record
      Comp_3 : Tag_18;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
   end record;
   --  calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
   --  own:   Ext_5_Id

   type Ext_6 is new Par_3 with record
      Comp_4 : Tag_4;  --  Tag_4_Id, Tag_4_FV_Id
   end record
     with Type_Invariant => Mark (Ext_6_FV_Id);
   --  calls: Tag_4_Id, Tag_4_FV_Id
   --  own:   Ext_6_FV_Id

   type Ext_7 is new Par_4 with record
      Comp_3 : Tag_6;   --  none
      Comp_4 : Tag_28;  --  Tag_4_Id, Tag_28_Id
   end record;
   --  calls: must be calculated

   type Ext_8 is new Par_4 with record
      Comp_3 : Tag_20;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_20_Id,
                        --  Tag_20_FV_Id
   end record;
   --  calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Par_4_Id, Tag_20_Id,
   --         Tag_20_FV_Id
   --  own:   Ext_8_Id

   protected type Prot_1
     with Type_Invariant => Mark (Prot_1_FV_Id)
   is
      entry E;
   private
      Comp_1 : Tag_18;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
   end Prot_1;
   --  calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
   --  own:   Prot_1_FV_Id

   protected type Prot_2 is
      entry E;
   private
      Comp_1 : Tag_5;   --  none
      Comp_2 : Tag_21;  --  Tag_15_Id
   end Prot_2;
   --  calls: Tag_15_Id
   --  own:   Prot_2_Id

   protected type Prot_3
     with Type_Invariant => Mark (Prot_3_FV_Id) is new Synch_2
   with
      entry E;
   private
      Comp_1 : Tag_24;  --  Tag_15_Id, Tag_24_Id, Tag_24_FV_Id
   end Prot_3;
   --  calls:       Tag_15_Id, Tag_24_Id, Tag_24_FV_Id
   --  own:         Prot_3_Id, Prot_3_FV_Id
   --  inheritable: Prot_3_Id
   --  inherited:   Synch_1_Id, Synch_2_Id

   task type Task_1 is
      entry E;
   end Task_1;
   --  own: Task_1_Id

   task type Task_2
     with Type_Invariant => Mark (Task_2_FV_Id) is new Synch_1
   with
      entry E;
   end Task_2;
   --  own:       Task_2_Id, Task_2_FV_Id
   --  inherited: Synch_1_Id

   type Untag_1 is new Integer;
   --  none

   type Untag_2 is record
      Comp : Integer;
   end record
     with Type_Invariant => Mark (Untag_2_Id);
   --  own: Untag_2_Id

   type Untag_3 is array (1 .. 5) of Boolean;
   --  own: Untag_3_Id

   type Untag_4 is record
      Comp_1 : Tag_16;  --  Tag_4_Id, Tag_16_Id
      Comp_2 : Tag_18;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
      Comp_3 : Tag_26;  --  Tag_15_Id, Tag_26_Id
   end record;
   --  calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_15_Id,
   --         Tag_16_Id, Tag_18_Id, Tag_26_Id

   type Untag_5 is record
      Comp_1 : Tag_17;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id
      Comp_2 : Tag_19;  --  Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id
      Comp_3 : Tag_27;  --  Tag_14_Id, Tag_27_Id
   end record
     with Type_Invariant => Mark (Untag_5_Id);
   --  own:   Untag_5_Id
   --  calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_14_Id,
   --         Tag_19_Id, Tag_27_Id

   type Untag_6 is array (1 .. 3, 5 .. 9) of Tag_10;
   --  calls: Tag_4_Id, Tag_10_Id

   type Untag_7 is array (1 .. 3) of Tag_13
     with Type_Invariant => Mark (Untag_7_Id);
   --  own:   Untag_7_Id
   --  calls: Tag_4_Id, Tag_13_Id

   type Untag_8 (Discr : Boolean) is record
      Comp_1 : Tag_18;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id

      case Discr is
         when True =>
            Comp_2 : Tag_1;  --  none
         when others =>
            Comp_3 : Untag_5;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id,
                               --  Tag_4_Id, Tag_14_Id, Tag_19_Id, Tag_27_Id,
                               --  Untag_5_Id
      end case;
   end record;

   type Untag_9 (Discr_1 : Boolean; Discr_2 : Boolean) is record
      Comp_1 : Tag_22;  --  Tag_4_Id, Tag_22_Id

      case Discr_1 is
         when True =>
            Comp_2 : Tag_28;  --  Tag_4_Id, Tag_28_Id

            case Discr_2 is
               when True =>
                  Comp_3 : Untag_1;  --  none
               when others =>
                  Comp_4 : Tag_1;  --  none
            end case;

         when others =>
            Comp_5 : Tag_4;   --  Tag_4_Id, Tag_4_FV_Id
            Comp_6 : Tag_24;  --  Tag_15_Id, Tag_24_Id, Tag_24_FV_Id

            case Discr_2 is
               when True =>
                  Comp_7 : Tag_27;  --  Tag_14_Id, Tag_27_Id
               when others =>
                  Comp_8 : Untag_4;  --  Iface_1_Id, Iface_2_Id, Iface_4_Id,
                                     --  Tag_4_Id, Tag_15_Id, Tag_16_Id,
                                     --  Tag_18_Id, Tag_26_Id
            end case;
      end case;
   end record
     with Type_Invariant => Mark (Untag_9_Id);
   --  own: Untag_9_Id

   -------------------
   -- Derived types --
   -------------------

   type Deriv_1 is new Tag_4 with null record;
   --  inherited: Tag_4_Id

   type Deriv_2 is new Tag_16 with null record;
   --  inherited: Tag_4_Id, Tag_16_Id

   type Deriv_3 is new Tag_18 with null record;
   --  inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id

   type Deriv_4 is new Untag_4;
   --  inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_15_Id,
   --             Tag_16_Id,  Tag_18_Id, Tag_26_Id

   type Deriv_5 is new Untag_7;
   --  inherited: Tag_4_Id, Tag_13_Id, Untag_7_Id

   --------------
   -- Subtypes --
   --------------

   subtype Sub_1 is Tag_9;
   --  inherited: Tag_9_Id

   subtype Sub_2 is Tag_17;
   --  inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id

   subtype Sub_3 is Untag_2;
   --  inherited: Untag_2_Id

   subtype Sub_4 is Untag_5;
   --  inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_14_Id,
   --             Tag_19_Id, Tag_27_Id, Untag_5_Id

   subtype Sub_5 is Untag_6;
   --  inherited: Tag_4_Id, Tag_10_Id
end Invariants_Aspects;

--  invariants_aspects.adb

package body Invariants_Aspects is
   protected body Prot_1 is
      entry E when True is begin null; end E;
   end Prot_1;

   protected body Prot_2 is
      entry E when True is begin null; end E;
   end Prot_2;

   protected body Prot_3 is
      entry E when True is begin null; end E;
   end Prot_3;

   task body Task_1 is
   begin
      select
         accept E do null; end E;
      or
         terminate;
      end select;
   end Task_1;

   task body Task_2 is
   begin
      select
         accept E do null; end E;
      or
         terminate;
      end select;
   end Task_2;

   procedure Test_Deriv_1 is
   begin
      Reset_Results;
      declare
         Obj : Deriv_1;
      begin
         Test_Results ("Deriv_1", (Tag_4_Id => True,
                                   others   => False));
      end;
   end Test_Deriv_1;

   procedure Test_Deriv_2 is
   begin
      Reset_Results;
      declare
         Obj : Deriv_2;
      begin
         Test_Results ("Deriv_2", (Tag_4_Id  => True,
                                   Tag_16_Id => True,
                                   others   => False));
      end;
   end Test_Deriv_2;

   procedure Test_Deriv_3 is
   begin
      Reset_Results;
      declare
         Obj : Deriv_3;
      begin
         Test_Results ("Deriv_3", (Iface_1_Id => True,
                                   Iface_2_Id => True,
                                   Iface_4_Id => True,
                                   others     => False));
      end;
   end Test_Deriv_3;

   procedure Test_Deriv_4 is
   begin
      Reset_Results;
      declare
         Obj : Deriv_4;
      begin
         Test_Results ("Deriv_4", (Iface_1_Id => True,
                                   Iface_2_Id => True,
                                   Iface_4_Id => True,
                                   Tag_4_Id   => True,
                                   Tag_15_Id  => True,
                                   Tag_16_Id  => True,
                                   Tag_18_Id  => True,
                                   Tag_26_Id  => True,
                                   others     => False));
      end;
   end Test_Deriv_4;

   procedure Test_Deriv_5 is
   begin
      Reset_Results;
      declare
         Obj : Deriv_5;
      begin
         Test_Results ("Deriv_5", (Tag_4_Id  => True,
                                   Tag_13_Id => True,
                                   others    => False));
      end;
   end Test_Deriv_5;

   procedure Test_Sub_1 is
   begin
      Reset_Results;
      declare
         Obj : Sub_1;
      begin
         Test_Results ("Sub_1", (Tag_9_Id => True,
                                 others   => False));
      end;
   end Test_Sub_1;

   procedure Test_Sub_2 is
   begin
      Reset_Results;
      declare
         Obj : Sub_2;
      begin
         Test_Results ("Sub_2", (Iface_1_Id => True,
                                 Iface_2_Id => True,
                                 Iface_4_Id => True,
                                 others     => False));
      end;
   end Test_Sub_2;

   procedure Test_Sub_3 is
   begin
      Reset_Results;
      declare
         Obj : Sub_3;
      begin
         Test_Results ("Sub_3", (Untag_2_Id => True,
                                 others     => False));
      end;
   end Test_Sub_3;

   procedure Test_Sub_4 is
   begin
      Reset_Results;
      declare
         Obj : Sub_4;
      begin
         Test_Results ("Sub_4", (Iface_1_Id => True,
                                 Iface_2_Id => True,
                                 Iface_4_Id => True,
                                 Tag_4_Id   => True,
                                 Tag_14_Id  => True,
                                 Tag_19_Id  => True,
                                 Tag_27_Id  => True,
                                 Untag_5_Id => True,
                                 others     => False));
      end;
   end Test_Sub_4;

   procedure Test_Sub_5 is
   begin
      Reset_Results;
      declare
         Obj : Sub_5;
      begin
         Test_Results ("Sub_5", (Tag_4_Id  => True,
                                 Tag_10_Id => True,
                                 others    => False));
      end;
   end Test_Sub_5;

   procedure Test_Untag_9_TT is
   begin
      Reset_Results;
      declare
         Obj : Untag_9 (True, True);
      begin
         Test_Results ("Untag_9_TT", (Tag_4_Id   => True,
                                      Tag_22_Id  => True,
                                      Tag_28_Id  => True,
                                      Untag_9_Id => True,
                                      others     => False));
      end;
   end Test_Untag_9_TT;

   procedure Test_Untag_9_TF is
   begin
      Reset_Results;
      declare
         Obj : Untag_9 (True, False);
      begin
         Test_Results ("Untag_9_TF", (Tag_4_Id   => True,
                                      Tag_22_Id  => True,
                                      Tag_28_Id  => True,
                                      Untag_9_Id => True,
                                      others     => False));
      end;
   end Test_Untag_9_TF;

   procedure Test_Untag_9_FT is
   begin
      Reset_Results;
      declare
         Obj : Untag_9 (False, True);
      begin
         Test_Results ("Untag_9_FT", (Tag_4_Id     => True,
                                      Tag_4_FV_Id  => True,
                                      Tag_14_Id    => True,
                                      Tag_15_Id    => True,
                                      Tag_22_Id    => True,
                                      Tag_24_Id    => True,
                                      Tag_24_FV_Id => True,
                                      Tag_27_Id    => True,
                                      Untag_9_Id   => True,
                                      others       => False));
      end;
   end Test_Untag_9_FT;

   procedure Test_Untag_9_FF is
   begin
      Reset_Results;
      declare
         Obj : Untag_9 (False, False);
      begin
         Test_Results ("Untag_9_FF", (Iface_1_Id   => True,
                                      Iface_2_Id   => True,
                                      Iface_4_Id   => True,
                                      Tag_4_Id     => True,
                                      Tag_4_FV_Id  => True,
                                      Tag_15_Id    => True,
                                      Tag_16_Id    => True,
                                      Tag_18_Id    => True,
                                      Tag_22_Id    => True,
                                      Tag_24_Id    => True,
                                      Tag_24_FV_Id => True,
                                      Tag_26_Id    => True,
                                      Untag_9_Id   => True,
                                      others       => False));
      end;
   end Test_Untag_9_FF;
end Invariants_Aspects;

--  invariants_main.adb

with Invariants_Aspects; use Invariants_Aspects;
with Tester;             use Tester;

procedure Invariants_Main is
begin
   Reset_Results;
   declare
      Obj : Tag_1;
   begin
      Test_Results ("Tag_1", (others => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_2;
   begin
      Test_Results ("Tag_2", (Tag_2_Id => True,
                              others   => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_3;
   begin
      Test_Results ("Tag_3", (Tag_3_Id => True,
                              others   => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_4;
   begin
      Test_Results ("Tag_4", (Tag_4_Id    => True,
                              Tag_4_FV_Id => True,
                              others      => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_5;
   begin
      Test_Results ("Tag_5", (others => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_6;
   begin
      Test_Results ("Tag_6", (others => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_7;
   begin
      Test_Results ("Tag_7", (Tag_4_Id => True,
                              others   => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_8;
   begin
      Test_Results ("Tag_8", (Tag_8_Id => True,
                              others   => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_9;
   begin
      Test_Results ("Tag_9", (Tag_9_Id => True,
                              others   => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_10;
   begin
      Test_Results ("Tag_10", (Tag_4_Id  => True,
                               Tag_10_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_11;
   begin
      Test_Results ("Tag_11", (Tag_11_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_12;
   begin
      Test_Results ("Tag_12", (Tag_12_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_13;
   begin
      Test_Results ("Tag_13", (Tag_4_Id  => True,
                               Tag_13_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_14;
   begin
      Test_Results ("Tag_14", (Tag_14_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_15;
   begin
      Test_Results ("Tag_15", (Tag_15_Id    => True,
                               Tag_15_FV_Id => True,
                               others       => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_16;
   begin
      Test_Results ("Tag_16", (Tag_4_Id  => True,
                               Tag_16_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_17;
   begin
      Test_Results ("Tag_17", (Iface_1_Id => True,
                               Iface_2_Id => True,
                               Iface_4_Id => True,
                               others     => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_18;
   begin
      Test_Results ("Tag_18", (Iface_1_Id => True,
                               Iface_2_Id => True,
                               Iface_4_Id => True,
                               Tag_18_Id  => True,
                               others     => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_19;
   begin
      Test_Results ("Tag_19", (Iface_1_Id => True,
                               Iface_2_Id => True,
                               Tag_4_Id   => True,
                               Tag_19_Id  => True,
                               others     => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_20;
   begin
      Test_Results ("Tag_20", (Iface_1_Id   => True,
                               Iface_2_Id   => True,
                               Iface_4_Id   => True,
                               Tag_20_Id    => True,
                               Tag_20_FV_Id => True,
                               others       => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_21;
   begin
      Test_Results ("Tag_21", (Tag_15_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_22;
   begin
      Test_Results ("Tag_22", (Tag_4_Id  => True,
                               Tag_22_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_23;
   begin
      Test_Results ("Tag_23", (Tag_23_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_24;
   begin
      Test_Results ("Tag_24", (Tag_15_Id    => True,
                               Tag_24_Id    => True,
                               Tag_24_FV_Id => True,
                               others       => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_25;
   begin
      Test_Results ("Tag_25", (Tag_4_Id => True,
                               others   => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_26;
   begin
      Test_Results ("Tag_26", (Tag_15_Id => True,
                               Tag_26_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_27;
   begin
      Test_Results ("Tag_27", (Tag_14_Id => True,
                               Tag_27_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Tag_28;
   begin
      Test_Results ("Tag_28", (Tag_4_Id  => True,
                               Tag_28_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_1 (True);
   begin
      Test_Results ("Ext_1_T", (Ext_1_FV_Id  => True,
                                Iface_1_Id   => True,
                                Iface_2_Id   => True,
                                Iface_4_Id   => True,
                                Tag_4_Id     => True,
                                Tag_8_Id     => True,
                                Tag_10_Id    => True,
                                Tag_15_Id    => True,
                                Tag_20_Id    => True,
                                Tag_20_FV_Id => True,
                                Tag_26_Id    => True,
                                others       => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_1 (False);
   begin
      Test_Results ("Ext_1_F", (Ext_1_FV_Id  => True,
                                Iface_1_Id   => True,
                                Iface_2_Id   => True,
                                Iface_4_Id   => True,
                                Tag_4_Id     => True,
                                Tag_8_Id     => True,
                                Tag_15_Id    => True,
                                Tag_19_Id    => True,
                                Tag_20_Id    => True,
                                Tag_20_FV_Id => True,
                                Tag_26_Id    => True,
                                others       => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_2 (True);
   begin
      Test_Results ("Ext_2_T", (Ext_2_Id  => True,
                                Tag_4_Id  => True,
                                Tag_8_Id  => True,
                                Tag_10_Id => True,
                                others    => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_2 (False);
   begin
      Test_Results ("Ext_2_F", (Ext_2_Id   => True,
                                Iface_1_Id => True,
                                Iface_2_Id => True,
                                Tag_4_Id   => True,
                                Tag_8_Id   => True,
                                Tag_19_Id  => True,
                                others     => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_3;
   begin
      Test_Results ("Ext_3", (Iface_1_Id   => True,
                              Iface_2_Id   => True,
                              Tag_4_Id     => True,
                              Tag_15_Id    => True,
                              Tag_19_Id    => True,
                              Tag_22_Id    => True,
                              Tag_24_Id    => True,
                              Tag_24_FV_Id => True,
                              others       => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_4;
   begin
      Test_Results ("Ext_4", (Ext_4_Id     => True,
                              Ext_4_FV_Id  => True,
                              Tag_4_Id     => True,
                              Tag_14_Id    => True,
                              Tag_15_Id    => True,
                              Tag_22_Id    => True,
                              Tag_24_Id    => True,
                              Tag_24_FV_Id => True,
                              others       => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_5;
   begin
      Test_Results ("Ext_5", (Ext_5_Id   => True,
                              Iface_1_Id => True,
                              Iface_2_Id => True,
                              Iface_4_Id => True,
                              Tag_18_Id  => True,
                              others     => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_6;
   begin
      Test_Results ("Ext_6", (Ext_6_FV_Id => True,
                              Tag_4_Id    => True,
                              Tag_4_FV_Id => True,
                              others      => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_7 (True);
   begin
      Test_Results ("Ext_7_T", (Par_4_Id  => True,
                                Tag_4_Id  => True,
                                Tag_28_Id => True,
                                others    => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_7 (False);
   begin
      Test_Results ("Ext_7_F", (Par_4_Id   => True,
                                Tag_4_Id  => True,
                                Tag_28_Id => True,
                                others     => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_8 (True);
   begin
      Test_Results ("Ext_8_T", (Ext_8_Id     => True,
                                Iface_1_Id   => True,
                                Iface_2_Id   => True,
                                Iface_4_Id   => True,
                                Par_4_Id     => True,
                                Tag_20_Id    => True,
                                Tag_20_FV_Id => True,
                                others       => False));
   end;

   Reset_Results;
   declare
      Obj : Ext_8 (False);
   begin
      Test_Results ("Ext_8_F", (Ext_8_Id     => True,
                                Iface_1_Id   => True,
                                Iface_2_Id   => True,
                                Iface_4_Id   => True,
                                Par_4_Id     => True,
                                Tag_20_Id    => True,
                                Tag_20_FV_Id => True,
                                others       => False));
   end;

   Reset_Results;
   declare
      Obj : Prot_1;
   begin
      Test_Results ("Prot_1", (Iface_1_Id   => True,
                               Iface_2_Id   => True,
                               Iface_4_Id   => True,
                               Prot_1_FV_Id => True,
                               Tag_18_Id    => True,
                               others       => False));
   end;

   Reset_Results;
   declare
      Obj : Prot_2;
   begin
      Test_Results ("Prot_2", (Prot_2_Id => True,
                               Tag_15_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Prot_3;
   begin
      Test_Results ("Prot_3", (Prot_3_Id    => True,
                               Prot_3_FV_Id => True,
                               Synch_1_Id   => True,
                               Synch_2_Id   => True,
                               Tag_15_Id    => True,
                               Tag_24_Id    => True,
                               Tag_24_FV_Id => True,
                               others       => False));
   end;

   Reset_Results;
   declare
      Obj : Task_1;
   begin
      Test_Results ("Task_1", (Task_1_Id => True,
                               others    => False));
   end;

   Reset_Results;
   declare
      Obj : Task_2;
   begin
      Test_Results ("Task_2", (Synch_1_Id   => True,
                               Task_2_Id    => True,
                               Task_2_FV_Id => True,
                               others       => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_1;
   begin
      Test_Results ("Untag_1", (others => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_2;
   begin
      Test_Results ("Untag_2", (Untag_2_Id => True,
                                others     => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_3;
   begin
      Test_Results ("Untag_3", (Untag_3_Id => True,
                                others     => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_4;
   begin
      Test_Results ("Untag_4", (Iface_1_Id => True,
                                Iface_2_Id => True,
                                Iface_4_Id => True,
                                Tag_4_Id   => True,
                                Tag_15_Id  => True,
                                Tag_16_Id  => True,
                                Tag_18_Id  => True,
                                Tag_26_Id  => True,
                                others     => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_5;
   begin
      Test_Results ("Untag_5", (Iface_1_Id => True,
                                Iface_2_Id => True,
                                Iface_4_Id => True,
                                Tag_4_Id   => True,
                                Tag_14_Id  => True,
                                Tag_19_Id  => True,
                                Tag_27_Id  => True,
                                Untag_5_Id => True,
                                others     => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_6;
   begin
      Test_Results ("Untag_6", (Tag_4_Id  => True,
                                Tag_10_Id => True,
                                others    => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_7;
   begin
      Test_Results ("Untag_7", (Tag_4_Id   => True,
                                Tag_13_Id  => True,
                                Untag_7_Id => True,
                                others     => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_8 (True);
   begin
      Test_Results ("Untag_8_T", (Iface_1_Id => True,
                                  Iface_2_Id => True,
                                  Iface_4_Id => True,
                                  Tag_18_Id  => True,
                                  others     => False));
   end;

   Reset_Results;
   declare
      Obj : Untag_8 (False);
   begin
      Test_Results ("Untag_8_F", (Iface_1_Id => True,
                                  Iface_2_Id => True,
                                  Iface_4_Id => True,
                                  Tag_4_Id   => True,
                                  Tag_14_Id  => True,
                                  Tag_18_Id  => True,
                                  Tag_19_Id  => True,
                                  Tag_27_Id  => True,
                                  Untag_5_Id => True,
                                  others     => False));
   end;

   Test_Untag_9_TT;
   Test_Untag_9_TF;
   Test_Untag_9_FT;
   Test_Untag_9_FF;

   Test_Deriv_1;
   Test_Deriv_2;
   Test_Deriv_3;
   Test_Deriv_4;
   Test_Deriv_5;

   Test_Sub_1;
   Test_Sub_2;
   Test_Sub_3;
   Test_Sub_4;
   Test_Sub_5;
end Invariants_Main;

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

$ gnatmake -q -gnata -gnatws invariants_main.adb
$ ./invariants_main
Tag_1: OK
Tag_2: OK
Tag_3: OK
Tag_4: OK
Tag_5: OK
Tag_6: OK
Tag_7: OK
Tag_8: OK
Tag_9: OK
Tag_10: OK
Tag_11: OK
Tag_12: OK
Tag_13: OK
Tag_14: OK
Tag_15: OK
Tag_16: OK
Tag_17: OK
Tag_18: OK
Tag_19: OK
Tag_20: OK
Tag_21: OK
Tag_22: OK
Tag_23: OK
Tag_24: OK
Tag_25: OK
Tag_26: OK
Tag_27: OK
Tag_28: OK
Ext_1_T: OK
Ext_1_F: OK
Ext_2_T: OK
Ext_2_F: OK
Ext_3: OK
Ext_4: OK
Ext_5: OK
Ext_6: OK
Ext_7_T: OK
Ext_7_F: OK
Ext_8_T: OK
Ext_8_F: OK
Prot_1: OK
Prot_2: OK
Prot_3: OK
Task_1: OK
Task_2: OK
Untag_1: OK
Untag_2: OK
Untag_3: OK
Untag_4: OK
Untag_5: OK
Untag_6: OK
Untag_7: OK
Untag_8_T: OK
Untag_8_F: OK
Untag_9_TT: OK
Untag_9_TF: OK
Untag_9_FT: OK
Untag_9_FF: OK
Deriv_1: OK
Deriv_2: OK
Deriv_3: OK
Deriv_4: OK
Deriv_5: OK
Sub_1: OK
Sub_2: OK
Sub_3: OK
Sub_4: OK
Sub_5: OK

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

2016-06-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* atree.ads, atree.adb (Elist29): New routine.
	(Set_Elist29): New routine.
	* atree.h New definition for Elist29.
	* einfo.adb Subprograms_For_Type is now an Elist rather than
	a node. Has_Invariants is now a synthesized attribute
	and does not require a flag. Has_Own_Invariants
	is now Flag232. Has_Inherited_Invariants is
	Flag291. Is_Partial_Invariant_Procedure is Flag292.
	(Default_Init_Cond_Procedure): Reimplemented.
	(Has_Inherited_Invariants): New routine.
	(Has_Invariants): Reimplemented.
	(Has_Own_Invariants): New routine.
	(Invariant_Procedure): Reimplemented.
	(Is_Partial_Invariant_Procedure): New routine.
	(Partial_Invariant_Procedure): Reimplemented.
	(Predicate_Function): Reimplemented.
	(Predicate_Function_M): Reimplemented.
	(Set_Default_Init_Cond_Procedure): Reimplemented.
	(Set_Has_Inherited_Invariants): New routine.
	(Set_Has_Invariants): Removed.
	(Set_Has_Own_Invariants): New routine.
	(Set_Invariant_Procedure): Reimplemented.
	(Set_Is_Partial_Invariant_Procedure): New routine.
	(Set_Partial_Invariant_Procedure): Reimplemented.
	(Set_Predicate_Function): Reimplemented.
	(Set_Predicate_Function_M): Reimplemented.
	(Set_Subprograms_For_Type): Reimplemented.
	(Subprograms_For_Type): Reimplemented.
	(Write_Entity_Flags): Output Flag232 and Flag291.
	* einfo.ads Add new attributes Has_Inherited_Invariants
	Has_Own_Invariants Is_Partial_Invariant_Procedure
	Partial_Invariant_Procedure Change the documentation
	of attributes Has_Inheritable_Invariants Has_Invariants
	Invariant_Procedure Is_Invariant_Procedure Subprograms_For_Type
	(Has_Inherited_Invariants): New routine along with pragma Inline.
	(Has_Own_Invariants): New routine along with pragma Inline.
	(Is_Partial_Invariant_Procedure): New routine along with pragma Inline.
	(Partial_Invariant_Procedure): New routine.
	(Set_Has_Inherited_Invariants): New routine along with pragma Inline.
	(Set_Has_Invariants): Removed along with pragma Inline.
	(Set_Has_Own_Invariants): New routine along with pragma Inline.
	(Set_Is_Partial_Invariant_Procedure): New routine
	along with pragma Inline.
	(Set_Partial_Invariant_Procedure): New routine.
	(Set_Subprograms_For_Type): Update the signature.
	(Subprograms_For_Type): Update the signature.
	* exp_ch3.adb Remove with and use clauses for Sem_Ch13.
	(Build_Array_Invariant_Proc): Removed.
	(Build_Record_Invariant_Proc): Removed.
	(Freeze_Type): Build the body of the invariant procedure.
	(Insert_Component_Invariant_Checks): Removed.
	* exp_ch7.adb Add with and use clauses for Sem_Ch6, Sem_Ch13,
	and Stringt.
	(Build_Invariant_Procedure_Body): New routine.
	(Build_Invariant_Procedure_Declaration): New routine.
	* exp_ch7.ads (Build_Invariant_Procedure_Body): New routine.
	(Build_Invariant_Procedure_Declaration): New routine.
	* exp_ch9.adb (Build_Corresponding_Record): Do not propagate
	attributes related to invariants to the corresponding record
	when building the corresponding record. This is done by
	Build_Invariant_Procedure_Declaration.
	* exp_util.adb (Make_Invariant_Call): Reimplemented.
	* freeze.adb (Freeze_Array_Type): An array type requires an
	invariant procedure when its component type has invariants.
	(Freeze_Record_Type): A record type requires an invariant
	procedure when at least one of its components has an invariant.
	* sem_ch3.adb (Analyze_Private_Extension_Declaration): Inherit
	invariant-related attributes.
	(Analyze_Subtype_Declaration):
	Inherit invariant-related attributes.
	(Build_Derived_Record_Type): Inherit invariant-related attributes.
	(Check_Duplicate_Aspects): Reimplemented.
	(Get_Partial_View_Aspect): New routine.
	(Process_Full_View): Inherit invariant-related attributes. Reimplement
	the check on hidden inheritance of class-wide invariants.
	(Remove_Default_Init_Cond_Procedure): Reimplemented.
	* sem_ch6.adb (Analyze_Subprogram_Specification): Do not modify
	the controlling type for an invariant procedure declaration
	or body.
	(Is_Invariant_Procedure_Or_Body): New routine.
	* sem_ch7.adb (Analyze_Package_Specification): Build the partial
	invariant body in order to preanalyze and resolve all invariants
	of a private type at the end of the visible declarations. Build
	the full invariant body in order to preanalyze and resolve
	all invariants of a private type's full view at the end of
	the private declarations.
	(Preserve_Full_Attributes): Inherit invariant-related attributes.
	* sem_ch9.adb (Analyze_Protected_Type_Declaration): Ensure that
	aspects are analyzed with the proper view when the protected type
	is a completion of a private type. Inherit invariant-related attributes.
	(Analyze_Task_Type_Declaration): Ensure that
	aspects are analyzed with the proper view when the task type
	is a completion of a private type. Inherit invariant-related
	attributes.
	* sem_ch13.adb Remove with and use clauses for Stringt.
	(Build_Invariant_Procedure_Declaration): Removed.
	(Build_Invariant_Procedure): Removed.
	(Freeze_Entity_Checks): Do not build the body of the invariant
	procedure here.
	The body is built when the type is frozen in Freeze_Type.
	(Inherit_Aspects_At_Freeze_Point): Do not inherit any attributes
	related to invariants here because this leads to erroneous
	inheritance.
	(Replace_Node): Rename to Replace_Type_Ref.
	* sem_ch13.ads (Build_Invariant_Procedure_Declaration): Removed.
	(Build_Invariant_Procedure): Removed.
	* sem_prag.adb Add with and use clauses for Exp_Ch7.
	(Analyze_Pragma): Reimplement the analysis of pragma Invariant.
	* sem_res.adb (Resolve_Actuals): Emit a specialized error when
	the context is an invariant.
	* sem_util.adb (Get_Views): New routine.
	(Incomplete_Or_Partial_View): Consider generic packages when
	examining declarations.
	(Inspect_Decls): Consider full type
	declarations because they may denote a derivation from a
	private type.
	(Propagate_Invariant_Attributes): New routine.
	* sem_util.ads (Get_Views): New routine.
	(Propagate_Invariant_Attributes): New routine.

-------------- next part --------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 237595)
+++ sem_ch3.adb	(working copy)
@@ -4475,6 +4475,8 @@
    procedure Analyze_Private_Extension_Declaration (N : Node_Id) is
       Indic       : constant Node_Id   := Subtype_Indication (N);
       T           : constant Entity_Id := Defining_Identifier (N);
+      Iface       : Entity_Id;
+      Iface_Elmt  : Elmt_Id;
       Parent_Base : Entity_Id;
       Parent_Type : Entity_Id;
 
@@ -4540,8 +4542,8 @@
 
       elsif Is_Concurrent_Type (Parent_Type) then
          Error_Msg_N
-           ("parent type of a private extension cannot be "
-            & "a synchronized tagged type (RM 3.9.1 (3/1))", N);
+           ("parent type of a private extension cannot be a synchronized "
+            & "tagged type (RM 3.9.1 (3/1))", N);
 
          Set_Etype              (T, Any_Type);
          Set_Ekind              (T, E_Limited_Private_Type);
@@ -4562,7 +4564,6 @@
       if (not Is_Package_Or_Generic_Package (Current_Scope)
            and then Nkind (Parent (N)) /= N_Generic_Subprogram_Declaration)
         or else In_Private_Part (Current_Scope)
-
       then
          Error_Msg_N ("invalid context for private extension", N);
       end if;
@@ -4589,13 +4590,26 @@
 
       Build_Derived_Record_Type (N, Parent_Type, T);
 
-      --  Propagate inherited invariant information. The new type has
-      --  invariants, if the parent type has inheritable invariants,
-      --  and these invariants can in turn be inherited.
+      --  A private extension inherits any class-wide invariants coming from a
+      --  parent type or an interface. Note that the invariant procedure of the
+      --  parent type should not be inherited because the private extension may
+      --  define invariants of its own.
 
       if Has_Inheritable_Invariants (Parent_Type) then
-         Set_Has_Inheritable_Invariants (T);
-         Set_Has_Invariants (T);
+         Set_Has_Inherited_Invariants (T);
+
+      elsif Present (Interfaces (T)) then
+         Iface_Elmt := First_Elmt (Interfaces (T));
+         while Present (Iface_Elmt) loop
+            Iface := Node (Iface_Elmt);
+
+            if Has_Inheritable_Invariants (Iface) then
+               Set_Has_Inherited_Invariants (T);
+               exit;
+            end if;
+
+            Next_Elmt (Iface_Elmt);
+         end loop;
       end if;
 
       --  Ada 2005 (AI-443): Synchronized private extension or a rewritten
@@ -4617,33 +4631,29 @@
                 (not Is_Interface (Parent_Type)
                   or else not Is_Synchronized_Interface (Parent_Type))
             then
-               Error_Msg_NE ("parent type of & must be tagged limited " &
-                             "or synchronized", N, T);
+               Error_Msg_NE
+                 ("parent type of & must be tagged limited or synchronized",
+                  N, T);
             end if;
 
             --  The progenitors (if any) must be limited or synchronized
             --  interfaces.
 
             if Present (Interfaces (T)) then
-               declare
-                  Iface      : Entity_Id;
-                  Iface_Elmt : Elmt_Id;
+               Iface_Elmt := First_Elmt (Interfaces (T));
+               while Present (Iface_Elmt) loop
+                  Iface := Node (Iface_Elmt);
 
-               begin
-                  Iface_Elmt := First_Elmt (Interfaces (T));
-                  while Present (Iface_Elmt) loop
-                     Iface := Node (Iface_Elmt);
+                  if not Is_Limited_Interface (Iface)
+                    and then not Is_Synchronized_Interface (Iface)
+                  then
+                     Error_Msg_NE
+                       ("progenitor & must be limited or synchronized",
+                        N, Iface);
+                  end if;
 
-                     if not Is_Limited_Interface (Iface)
-                       and then not Is_Synchronized_Interface (Iface)
-                     then
-                        Error_Msg_NE ("progenitor & must be limited " &
-                                      "or synchronized", N, Iface);
-                     end if;
-
-                     Next_Elmt (Iface_Elmt);
-                  end loop;
-               end;
+                  Next_Elmt (Iface_Elmt);
+               end loop;
             end if;
 
          --  Regular derived extension, the parent must be a limited or
@@ -5154,10 +5164,9 @@
 
       if Has_Predicates (T)
         and then Present (Predicate_Function (T))
-
-         and then
-           ((In_Instance and then not Comes_From_Source (N))
-              or else No (Aspect_Specifications (N)))
+        and then
+          ((In_Instance and then not Comes_From_Source (N))
+             or else No (Aspect_Specifications (N)))
       then
          Set_Subprograms_For_Type (Id, Subprograms_For_Type (T));
 
@@ -5167,6 +5176,11 @@
          end if;
       end if;
 
+      --  Propagate invariant-related attributes from the base type to the
+      --  subtype.
+
+      Propagate_Invariant_Attributes (Id, From_Typ => Base_Type (T));
+
       --  Remaining processing depends on characteristics of base type
 
       T := Etype (Id);
@@ -5228,9 +5242,9 @@
 
       if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
          if Is_Scalar_Type (Etype (Id))
-            and then Scalar_Range (Id) /=
-                     Scalar_Range (Etype (Subtype_Mark
-                                           (Subtype_Indication (N))))
+           and then Scalar_Range (Id) /=
+                    Scalar_Range
+                      (Etype (Subtype_Mark (Subtype_Indication (N))))
          then
             Apply_Range_Check
               (Scalar_Range (Id),
@@ -5301,14 +5315,6 @@
          end if;
       end if;
 
-      --  A type invariant applies to any subtype in its scope, in particular
-      --  to a generic actual.
-
-      if Has_Invariants (T) and then In_Open_Scopes (Scope (T)) then
-         Set_Has_Invariants (Id);
-         Set_Invariant_Procedure (Id, Invariant_Procedure (T));
-      end if;
-
       Set_Optimize_Alignment_Flags (Id);
       Check_Eliminated (Id);
 
@@ -5633,16 +5639,20 @@
 
          --  Complete setup of implicit base type
 
-         Set_First_Index       (Implicit_Base, First_Index (T));
-         Set_Component_Type    (Implicit_Base, Element_Type);
+         Set_Component_Size (Implicit_Base, Uint_0);
+         Set_Component_Type (Implicit_Base, Element_Type);
+         Set_Finalize_Storage_Only
+                            (Implicit_Base,
+                              Finalize_Storage_Only (Element_Type));
+         Set_First_Index    (Implicit_Base, First_Index (T));
+         Set_Has_Controlled_Component
+                            (Implicit_Base,
+                              Has_Controlled_Component (Element_Type)
+                                or else Is_Controlled_Active  (Element_Type));
+         Set_Packed_Array_Impl_Type
+                            (Implicit_Base, Empty);
+
          Propagate_Concurrent_Flags (Implicit_Base, Element_Type);
-         Set_Component_Size    (Implicit_Base, Uint_0);
-         Set_Packed_Array_Impl_Type (Implicit_Base, Empty);
-         Set_Has_Controlled_Component (Implicit_Base,
-           Has_Controlled_Component (Element_Type)
-             or else Is_Controlled_Active  (Element_Type));
-         Set_Finalize_Storage_Only (Implicit_Base,
-           Finalize_Storage_Only (Element_Type));
 
          --  Inherit the "ghostness" from the constrained array type
 
@@ -8786,31 +8796,35 @@
                   end;
                end if;
 
-               --  Propagate inherited invariant information of parents
-               --  and progenitors
+               --  A derived type inherits any class-wide invariants coming
+               --  from a parent type or an interface. Note that the invariant
+               --  procedure of the parent type should not be inherited because
+               --  the derived type may define invariants of its own.
 
                if Ada_Version >= Ada_2012
                  and then not Is_Interface (Derived_Type)
                then
-                  if Has_Inheritable_Invariants (Parent_Type) then
-                     Set_Has_Invariants (Derived_Type);
-                     Set_Has_Inheritable_Invariants (Derived_Type);
+                  if Has_Inherited_Invariants (Parent_Type)
+                    or else Has_Inheritable_Invariants (Parent_Type)
+                  then
+                     Set_Has_Inherited_Invariants (Derived_Type);
 
                   elsif not Is_Empty_Elmt_List (Ifaces_List) then
                      declare
-                        AI : Elmt_Id;
+                        Iface      : Entity_Id;
+                        Iface_Elmt : Elmt_Id;
 
                      begin
-                        AI := First_Elmt (Ifaces_List);
-                        while Present (AI) loop
-                           if Has_Inheritable_Invariants (Node (AI)) then
-                              Set_Has_Invariants (Derived_Type);
-                              Set_Has_Inheritable_Invariants (Derived_Type);
+                        Iface_Elmt := First_Elmt (Ifaces_List);
+                        while Present (Iface_Elmt) loop
+                           Iface := Node (Iface_Elmt);
 
+                           if Has_Inheritable_Invariants (Iface) then
+                              Set_Has_Inherited_Invariants (Derived_Type);
                               exit;
                            end if;
 
-                           Next_Elmt (AI);
+                           Next_Elmt (Iface_Elmt);
                         end loop;
                      end;
                   end if;
@@ -16427,63 +16441,93 @@
 
    function Find_Type_Name (N : Node_Id) return Entity_Id is
       Id       : constant Entity_Id := Defining_Identifier (N);
+      New_Id   : Entity_Id;
       Prev     : Entity_Id;
-      New_Id   : Entity_Id;
       Prev_Par : Node_Id;
 
       procedure Check_Duplicate_Aspects;
       --  Check that aspects specified in a completion have not been specified
-      --  already in the partial view. Type_Invariant and others can be
-      --  specified on either view but never on both.
+      --  already in the partial view.
 
       procedure Tag_Mismatch;
-      --  Diagnose a tagged partial view whose full view is untagged.
-      --  We post the message on the full view, with a reference to
-      --  the previous partial view. The partial view can be private
-      --  or incomplete, and these are handled in a different manner,
-      --  so we determine the position of the error message from the
-      --  respective slocs of both.
+      --  Diagnose a tagged partial view whose full view is untagged. We post
+      --  the message on the full view, with a reference to the previous
+      --  partial view. The partial view can be private or incomplete, and
+      --  these are handled in a different manner, so we determine the position
+      --  of the error message from the respective slocs of both.
 
       -----------------------------
       -- Check_Duplicate_Aspects --
       -----------------------------
 
       procedure Check_Duplicate_Aspects is
-         Prev_Aspects   : constant List_Id := Aspect_Specifications (Prev_Par);
-         Full_Aspects   : constant List_Id := Aspect_Specifications (N);
-         F_Spec, P_Spec : Node_Id;
+         function Get_Partial_View_Aspect (Asp : Node_Id) return Node_Id;
+         --  Return the corresponding aspect of the partial view which matches
+         --  the aspect id of Asp. Return Empty is no such aspect exists.
 
+         -----------------------------
+         -- Get_Partial_View_Aspect --
+         -----------------------------
+
+         function Get_Partial_View_Aspect (Asp : Node_Id) return Node_Id is
+            Asp_Id    : constant Aspect_Id := Get_Aspect_Id (Asp);
+            Prev_Asps : constant List_Id   := Aspect_Specifications (Prev_Par);
+            Prev_Asp  : Node_Id;
+
+         begin
+            if Present (Prev_Asps) then
+               Prev_Asp := First (Prev_Asps);
+               while Present (Prev_Asp) loop
+                  if Get_Aspect_Id (Prev_Asp) = Asp_Id then
+                     return Prev_Asp;
+                  end if;
+
+                  Next (Prev_Asp);
+               end loop;
+            end if;
+
+            return Empty;
+         end Get_Partial_View_Aspect;
+
+         --  Local variables
+
+         Full_Asps : constant List_Id := Aspect_Specifications (N);
+         Full_Asp  : Node_Id;
+         Part_Asp  : Node_Id;
+
+      --  Start of processing for Check_Duplicate_Aspects
+
       begin
-         if Present (Full_Aspects) then
-            F_Spec := First (Full_Aspects);
-            while Present (F_Spec) loop
-               if Present (Prev_Aspects) then
-                  P_Spec := First (Prev_Aspects);
-                  while Present (P_Spec) loop
-                     if Chars (Identifier (P_Spec)) =
-                       Chars (Identifier (F_Spec))
-                     then
-                        Error_Msg_N
-                          ("aspect already specified in private declaration",
-                            F_Spec);
-                        Remove (F_Spec);
-                        return;
-                     end if;
+         if Present (Full_Asps) then
+            Full_Asp := First (Full_Asps);
+            while Present (Full_Asp) loop
+               Part_Asp := Get_Partial_View_Aspect (Full_Asp);
 
-                     Next (P_Spec);
-                  end loop;
+               --  An aspect and its class-wide counterpart are two distinct
+               --  aspects and may apply to both views of an entity.
+
+               if Present (Part_Asp)
+                 and then Class_Present (Part_Asp) = Class_Present (Full_Asp)
+               then
+                  Error_Msg_N
+                    ("aspect already specified in private declaration",
+                     Full_Asp);
+
+                  Remove (Full_Asp);
+                  return;
                end if;
 
                if Has_Discriminants (Prev)
                  and then not Has_Unknown_Discriminants (Prev)
-                 and then Chars (Identifier (F_Spec)) =
-                   Name_Implicit_Dereference
+                 and then Get_Aspect_Id (Full_Asp) =
+                            Aspect_Implicit_Dereference
                then
-                  Error_Msg_N ("cannot specify aspect " &
-                    "if partial view has known discriminants", F_Spec);
+                  Error_Msg_N
+                    ("cannot specify aspect if partial view has known "
+                     & "discriminants", Full_Asp);
                end if;
 
-               Next (F_Spec);
+               Next (Full_Asp);
             end loop;
          end if;
       end Check_Duplicate_Aspects;
@@ -19573,8 +19617,8 @@
            and then not Is_Ancestor (Base_Type (Priv_Parent), Full_Parent)
          then
             Error_Msg_N
-              ("parent of full type must descend from parent"
-                  & " of private extension", Full_Indic);
+              ("parent of full type must descend from parent of private "
+               & "extension", Full_Indic);
 
          --  First check a formal restriction, and then proceed with checking
          --  Ada rules. Since the formal restriction is not a serious error, we
@@ -19628,9 +19672,9 @@
                   while Present (Priv_Discr) and then Present (Full_Discr) loop
                      if Original_Record_Component (Priv_Discr) =
                         Original_Record_Component (Full_Discr)
-                       or else
-                         Corresponding_Discriminant (Priv_Discr) =
-                         Corresponding_Discriminant (Full_Discr)
+                          or else
+                        Corresponding_Discriminant (Priv_Discr) =
+                        Corresponding_Discriminant (Full_Discr)
                      then
                         null;
                      else
@@ -19643,8 +19687,8 @@
 
                   if Present (Priv_Discr) or else Present (Full_Discr) then
                      Error_Msg_N
-                       ("full view must inherit discriminants of the parent"
-                        & " type used in the private extension", Full_Indic);
+                       ("full view must inherit discriminants of the parent "
+                        & "type used in the private extension", Full_Indic);
 
                   elsif Priv_Constr and then not Full_Constr then
                      Error_Msg_N
@@ -19662,13 +19706,13 @@
                --  known or unknown discriminants, then the full type
                --  declaration shall define a definite subtype.
 
-            elsif      not Has_Unknown_Discriminants (Priv_T)
+            elsif not Has_Unknown_Discriminants (Priv_T)
               and then not Has_Discriminants (Priv_T)
               and then not Is_Constrained (Full_T)
             then
                Error_Msg_N
-                 ("full view must define a constrained type if partial view"
-                  & " has no discriminants", Full_T);
+                 ("full view must define a constrained type if partial view "
+                  & "has no discriminants", Full_T);
             end if;
 
             --  ??????? Do we implement the following properly ?????
@@ -20095,42 +20139,33 @@
          Mark_Full_View_As_Ghost (Priv_T, Full_T);
       end if;
 
-      --  Propagate invariants to full type
+      --  Propagate invariant-related attributes from the private view to the
+      --  full view and its base type.
 
-      if Has_Invariants (Priv_T) then
-         Set_Has_Invariants (Full_T);
-         Set_Invariant_Procedure (Full_T, Invariant_Procedure (Priv_T));
-      end if;
+      Propagate_Invariant_Attributes (Full_T, From_Typ => Priv_T);
+      Propagate_Invariant_Attributes (Base_Type (Full_T), From_Typ => Priv_T);
 
-      if Has_Inheritable_Invariants (Priv_T) then
-         Set_Has_Inheritable_Invariants (Full_T);
-      end if;
+      --  AI12-0041: Detect an attempt to inherit a class-wide type invariant
+      --  in the full view without advertising the inheritance in the partial
+      --  view. This can only occur when the partial view has no parent type
+      --  and the full view has an interface as a parent. Any other scenarios
+      --  are illegal because implemented interfaces must match between the
+      --  two views.
 
-      --  Check hidden inheritance of class-wide type invariants
-
-      if Ada_Version >= Ada_2012
-        and then not Has_Inheritable_Invariants (Full_T)
-        and then In_Private_Part (Current_Scope)
-        and then Has_Interfaces (Full_T)
-      then
+      if Is_Tagged_Type (Priv_T) and then Is_Tagged_Type (Full_T) then
          declare
-            Ifaces : Elist_Id;
-            AI     : Elmt_Id;
+            Full_Par : constant Entity_Id := Etype (Full_T);
+            Priv_Par : constant Entity_Id := Etype (Priv_T);
 
          begin
-            Collect_Interfaces (Full_T, Ifaces, Exclude_Parents => True);
-
-            AI := First_Elmt (Ifaces);
-            while Present (AI) loop
-               if Has_Inheritable_Invariants (Node (AI)) then
-                  Error_Msg_N
-                    ("hidden inheritance of class-wide type invariants " &
-                     "not allowed", N);
-                  exit;
-               end if;
-
-               Next_Elmt (AI);
-            end loop;
+            if not Is_Interface (Priv_Par)
+              and then Is_Interface (Full_Par)
+              and then Has_Inheritable_Invariants (Full_Par)
+            then
+               Error_Msg_N
+                 ("hidden inheritance of class-wide type invariants not "
+                  & "allowed", N);
+            end if;
          end;
       end if;
 
@@ -20952,34 +20987,31 @@
       Private_To_Full_View : Boolean := False)
    is
       procedure Remove_Default_Init_Cond_Procedure (Typ : Entity_Id);
-      --  Remove the default initial procedure (if any) from the rep chain of
-      --  type Typ.
+      --  Remove the default initial condition procedure (if any) from the
+      --  Subprograms_For_Type chain of type Typ.
 
       ----------------------------------------
       -- Remove_Default_Init_Cond_Procedure --
       ----------------------------------------
 
       procedure Remove_Default_Init_Cond_Procedure (Typ : Entity_Id) is
-         Found : Boolean := False;
-         Prev  : Entity_Id;
-         Subp  : Entity_Id;
+         Subps     : constant Elist_Id := Subprograms_For_Type (Typ);
+         Subp_Elmt : Elmt_Id;
+         Subp_Id   : Entity_Id;
 
       begin
-         Prev := Typ;
-         Subp := Subprograms_For_Type (Typ);
-         while Present (Subp) loop
-            if Is_Default_Init_Cond_Procedure (Subp) then
-               Found := True;
-               exit;
-            end if;
+         if Present (Subps) then
+            Subp_Elmt := First_Elmt (Subps);
+            while Present (Subp_Elmt) loop
+               Subp_Id := Node (Subp_Elmt);
 
-            Prev := Subp;
-            Subp := Subprograms_For_Type (Subp);
-         end loop;
+               if Is_Default_Init_Cond_Procedure (Subp_Id) then
+                  Remove_Elmt (Subps, Subp_Elmt);
+                  exit;
+               end if;
 
-         if Found then
-            Set_Subprograms_For_Type (Prev, Subprograms_For_Type (Subp));
-            Set_Subprograms_For_Type (Subp, Empty);
+               Next_Elmt (Subp_Elmt);
+            end loop;
          end if;
       end Remove_Default_Init_Cond_Procedure;
 
Index: exp_ch7.adb
===================================================================
--- exp_ch7.adb	(revision 237595)
+++ exp_ch7.adb	(working copy)
@@ -55,12 +55,15 @@
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Ch3;  use Sem_Ch3;
+with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch7;  use Sem_Ch7;
 with Sem_Ch8;  use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Snames;   use Snames;
 with Stand;    use Stand;
+with Stringt;  use Stringt;
 with Tbuild;   use Tbuild;
 with Ttypes;   use Ttypes;
 with Uintp;    use Uintp;
@@ -3438,6 +3441,1518 @@
       Expand_At_End_Handler (HSS, Empty);
    end Build_Finalizer_Call;
 
+   ------------------------------------
+   -- Build_Invariant_Procedure_Body --
+   ------------------------------------
+
+   procedure Build_Invariant_Procedure_Body
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False)
+   is
+      Loc : constant Source_Ptr := Sloc (Typ);
+
+      Pragmas_Seen : Elist_Id := No_Elist;
+      --  This list contains all invariant pragmas processed so far. The list
+      --  is used to avoid generating redundant invariant checks.
+
+      Produced_Check : Boolean := False;
+      --  This flag tracks whether the type has produced at least one invariant
+      --  check. The flag is used as a sanity check at the end of the routine.
+
+      --  NOTE: most of the routines in Build_Invariant_Procedure_Body are
+      --  intentionally unnested to avoid deep indentation of code.
+
+      --  NOTE: all Add_xxx_Invariants routines are reactive. In other words
+      --  they emit checks, loops (for arrays) and case statements (for record
+      --  variant parts) only when there are invariants to verify. This keeps
+      --  the body of the invariant procedure free from useless code.
+
+      procedure Add_Array_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each component of array type T.
+      --  Obj_Id denotes the entity of the _object formal parameter of the
+      --  invariant procedure. All created checks are added to list Checks.
+
+      procedure Add_Interface_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each inherited class-wide invariant
+      --  coming from all interfaces implemented by type T. Obj_Id denotes the
+      --  entity of the _object formal parameter of the invariant procedure.
+      --  All created checks are added to list Checks.
+
+      procedure Add_Parent_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each inherited class-wide invariant
+      --  coming from all parent types of type T. Obj_Id denotes the entity of
+      --  the _object formal parameter of the invariant procedure. All created
+      --  checks are added to list Checks.
+
+      procedure Add_Record_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id);
+      --  Generate an invariant check for each component of record type T.
+      --  Obj_Id denotes the entity of the _object formal parameter of the
+      --  invariant procedure. All created checks are added to list Checks.
+
+      procedure Add_Type_Invariants
+        (Priv_Typ  : Entity_Id;
+         Full_Typ  : Entity_Id;
+         CRec_Typ  : Entity_Id;
+         Obj_Id    : Entity_Id;
+         Checks    : in out List_Id;
+         Inherit   : Boolean := False;
+         Priv_Item : Node_Id := Empty);
+      --  Generate an invariant check for each invariant found in one of the
+      --  following types (if available):
+      --
+      --    Priv_Typ - the partial view of a type
+      --    Full_Typ - the full view of a type
+      --    CRec_Typ - the corresponding record of a protected or a task type
+      --
+      --  Obj_Id denotes the entity of the _object formal parameter of the
+      --  invariant procedure. All created checks are added to list Checks.
+      --  Flag Inherit should be set when generating invariant checks for
+      --  inherited class-wide invariants. Priv_Item denotes the first rep
+      --  item of the private type.
+
+      procedure Create_Append (L : in out List_Id; N : Node_Id);
+      --  Append arbitrary node N to list L. If there is no list, create one.
+
+      function Is_Untagged_Private_Derivation
+        (Priv_Typ : Entity_Id;
+         Full_Typ : Entity_Id) return Boolean;
+      --  Determine whether private type Priv_Typ and its full view Full_Typ
+      --  represent an untagged derivation from a private parent.
+
+      ------------------------------------
+      -- Add_Array_Component_Invariants --
+      ------------------------------------
+
+      procedure Add_Array_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         Comp_Typ : constant Entity_Id := Component_Type (T);
+         Dims     : constant Pos       := Number_Dimensions (T);
+
+         procedure Process_Array_Component
+           (Indices     : List_Id;
+            Comp_Checks : in out List_Id);
+         --  Generate an invariant check for an array component identified by
+         --  the indices in list Indices. All created checks are added to list
+         --  Comp_Checks.
+
+         procedure Process_One_Dimension
+           (Dim        : Pos;
+            Indices    : List_Id;
+            Dim_Checks : in out List_Id);
+         --  Generate a loop over the Nth dimension Dim of an array type. List
+         --  Indices contains all array indices for the dimension. All created
+         --  checks are added to list Dim_Checks.
+
+         -----------------------------
+         -- Process_Array_Component --
+         -----------------------------
+
+         procedure Process_Array_Component
+           (Indices     : List_Id;
+            Comp_Checks : in out List_Id)
+         is
+            Proc_Id : Entity_Id;
+
+         begin
+            if Has_Invariants (Comp_Typ) then
+               Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
+
+               --  The component type should have an invariant procedure if it
+               --  has invariants of its own or inherits class-wide invariants
+               --  from parent or interface types.
+
+               pragma Assert (Present (Proc_Id));
+
+               --  Generate:
+               --    <Comp_Typ>Invariant (_object (<Indices>));
+
+               --  Note that the invariant procedure may have a null body if
+               --  assertions are disabled or Assertion_Polity Ignore is in
+               --  effect.
+
+               if not Has_Null_Body (Proc_Id) then
+                  Create_Append (Comp_Checks,
+                    Make_Procedure_Call_Statement (Loc,
+                      Name                   =>
+                        New_Occurrence_Of (Proc_Id, Loc),
+                      Parameter_Associations => New_List (
+                        Make_Indexed_Component (Loc,
+                          Prefix      => New_Occurrence_Of (Obj_Id, Loc),
+                          Expressions => New_Copy_List (Indices)))));
+               end if;
+
+               Produced_Check := True;
+            end if;
+
+            --  In a rare case the designated type of an access component may
+            --  have an invariant. In this case verify the dereference of the
+            --  component.
+
+            if Is_Access_Type (Comp_Typ)
+              and then Has_Invariants (Designated_Type (Comp_Typ))
+            then
+               Proc_Id :=
+                 Invariant_Procedure (Base_Type (Designated_Type (Comp_Typ)));
+
+               --  The designated type should have an invariant procedure if it
+               --  has invariants of its own or inherits class-wide invariants
+               --  from parent or interface types.
+
+               pragma Assert (Present (Proc_Id));
+
+               --  Generate:
+               --    if _object (<Indexes>) /= null then
+               --       <Desig_Comp_Typ>Invariant (_object (<Indices>).all);
+               --    end if;
+
+               --  Note that the invariant procedure may have a null body if
+               --  assertions are disabled or Assertion_Polity Ignore is in
+               --  effect.
+
+               if not Has_Null_Body (Proc_Id) then
+                  Create_Append (Comp_Checks,
+                    Make_If_Statement (Loc,
+                      Condition       =>
+                        Make_Op_Ne (Loc,
+                          Left_Opnd  =>
+                            Make_Indexed_Component (Loc,
+                              Prefix      => New_Occurrence_Of (Obj_Id, Loc),
+                              Expressions => New_Copy_List (Indices)),
+                          Right_Opnd => Make_Null (Loc)),
+
+                      Then_Statements => New_List (
+                        Make_Procedure_Call_Statement (Loc,
+                          Name                   =>
+                            New_Occurrence_Of (Proc_Id, Loc),
+
+                          Parameter_Associations => New_List (
+                            Make_Explicit_Dereference (Loc,
+                              Prefix =>
+                                Make_Indexed_Component (Loc,
+                                  Prefix      =>
+                                    New_Occurrence_Of (Obj_Id, Loc),
+                                  Expressions =>
+                                    New_Copy_List (Indices))))))));
+               end if;
+
+               Produced_Check := True;
+            end if;
+         end Process_Array_Component;
+
+         ---------------------------
+         -- Process_One_Dimension --
+         ---------------------------
+
+         procedure Process_One_Dimension
+           (Dim        : Pos;
+            Indices    : List_Id;
+            Dim_Checks : in out List_Id)
+         is
+            Comp_Checks : List_Id := No_List;
+            Index       : Entity_Id;
+
+         begin
+            --  Generate the invariant checks for the array component after all
+            --  dimensions have produced their respective loops.
+
+            if Dim > Dims then
+               Process_Array_Component
+                 (Indices     => Indices,
+                  Comp_Checks => Dim_Checks);
+
+            --  Otherwise create a loop for the current dimension
+
+            else
+               --  Create a new loop variable for each dimension
+
+               Index :=
+                 Make_Defining_Identifier (Loc,
+                   Chars => New_External_Name ('I', Dim));
+               Append_To (Indices, New_Occurrence_Of (Index, Loc));
+
+               Process_One_Dimension
+                 (Dim        => Dim + 1,
+                  Indices    => Indices,
+                  Dim_Checks => Comp_Checks);
+
+               --  Generate:
+               --    for I<Dim> in _object'Range (<Dim>) loop
+               --       <Comp_Checks>
+               --    end loop;
+
+               --  Note that the invariant procedure may have a null body if
+               --  assertions are disabled or Assertion_Polity Ignore is in
+               --  effect.
+
+               if Present (Comp_Checks) then
+                  Create_Append (Dim_Checks,
+                    Make_Implicit_Loop_Statement (T,
+                      Identifier       => Empty,
+                      Iteration_Scheme =>
+                        Make_Iteration_Scheme (Loc,
+                          Loop_Parameter_Specification =>
+                            Make_Loop_Parameter_Specification (Loc,
+                              Defining_Identifier         => Index,
+                              Discrete_Subtype_Definition =>
+                                Make_Attribute_Reference (Loc,
+                                  Prefix         =>
+                                    New_Occurrence_Of (Obj_Id, Loc),
+                                  Attribute_Name => Name_Range,
+                                  Expressions    => New_List (
+                                    Make_Integer_Literal (Loc, Dim))))),
+
+                      Statements => Comp_Checks));
+               end if;
+            end if;
+         end Process_One_Dimension;
+
+      --  Start of processing for Add_Array_Component_Invariants
+
+      begin
+         Process_One_Dimension
+           (Dim        => 1,
+            Indices    => New_List,
+            Dim_Checks => Checks);
+      end Add_Array_Component_Invariants;
+
+      ------------------------------
+      -- Add_Interface_Invariants --
+      ------------------------------
+
+      procedure Add_Interface_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         Iface_Elmt : Elmt_Id;
+         Ifaces     : Elist_Id;
+
+      begin
+         if Is_Tagged_Type (T) then
+            Collect_Interfaces (T, Ifaces);
+
+            --  Process the class-wide invariants of all implemented interfaces
+
+            Iface_Elmt := First_Elmt (Ifaces);
+            while Present (Iface_Elmt) loop
+               Add_Type_Invariants
+                 (Priv_Typ => Empty,
+                  Full_Typ => Node (Iface_Elmt),
+                  CRec_Typ => Empty,
+                  Obj_Id   => Obj_Id,
+                  Checks   => Checks,
+                  Inherit  => True);
+
+               Next_Elmt (Iface_Elmt);
+            end loop;
+         end if;
+      end Add_Interface_Invariants;
+
+      ---------------------------
+      -- Add_Parent_Invariants --
+      ---------------------------
+
+      procedure Add_Parent_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         Dummy_1 : Entity_Id;
+         Dummy_2 : Entity_Id;
+
+         Curr_Typ : Entity_Id;
+         --  The entity of the current type being examined
+
+         Full_Typ : Entity_Id;
+         --  The full view of Par_Typ
+
+         Par_Typ : Entity_Id;
+         --  The entity of the parent type
+
+         Priv_Typ : Entity_Id;
+         --  The partial view of Par_Typ
+
+      begin
+         --  Climb the parent type chain
+
+         Curr_Typ := T;
+         loop
+            --  Do not consider subtypes as they inherit the invariants from
+            --  their base types.
+
+            Par_Typ := Base_Type (Etype (Curr_Typ));
+
+            --  Stop the climb once the root of the parent chain is reached
+
+            exit when Curr_Typ = Par_Typ;
+
+            --  Process the class-wide invariants of the parent type
+
+            Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
+
+            Add_Type_Invariants
+              (Priv_Typ => Priv_Typ,
+               Full_Typ => Full_Typ,
+               CRec_Typ => Empty,
+               Obj_Id   => Obj_Id,
+               Checks   => Checks,
+               Inherit  => True);
+
+            Curr_Typ := Par_Typ;
+         end loop;
+      end Add_Parent_Invariants;
+
+      -------------------------------------
+      -- Add_Record_Component_Invariants --
+      -------------------------------------
+
+      procedure Add_Record_Component_Invariants
+        (T      : Entity_Id;
+         Obj_Id : Entity_Id;
+         Checks : in out List_Id)
+      is
+         procedure Process_Component_List
+           (Comp_List : Node_Id;
+            CL_Checks : in out List_Id);
+         --  Generate invariant checks for all record components found in
+         --  component list Comp_List, including variant parts. All created
+         --  checks are added to list CL_Checks.
+
+         procedure Process_Record_Component
+           (Comp_Id     : Entity_Id;
+            Comp_Checks : in out List_Id);
+         --  Generate an invariant check for a record component identified by
+         --  Comp_Id. All created checks are added to list Comp_Checks.
+
+         ----------------------------
+         -- Process_Component_List --
+         ----------------------------
+
+         procedure Process_Component_List
+           (Comp_List : Node_Id;
+            CL_Checks : in out List_Id)
+         is
+            Comp       : Node_Id;
+            Var        : Node_Id;
+            Var_Alts   : List_Id := No_List;
+            Var_Checks : List_Id := No_List;
+            Var_Stmts  : List_Id;
+
+            Produced_Variant_Check : Boolean := False;
+            --  This flag tracks whether the component has produced at least
+            --  one invariant check.
+
+         begin
+            --  Traverse the component items
+
+            Comp := First (Component_Items (Comp_List));
+            while Present (Comp) loop
+               if Nkind (Comp) = N_Component_Declaration then
+
+                  --  Generate the component invariant check
+
+                  Process_Record_Component
+                    (Comp_Id     => Defining_Entity (Comp),
+                     Comp_Checks => CL_Checks);
+               end if;
+
+               Next (Comp);
+            end loop;
+
+            --  Traverse the variant part
+
+            if Present (Variant_Part (Comp_List)) then
+               Var := First (Variants (Variant_Part (Comp_List)));
+               while Present (Var) loop
+                  Var_Checks := No_List;
+
+                  --  Generate invariant checks for all components and variant
+                  --  parts that qualify.
+
+                  Process_Component_List
+                    (Comp_List => Component_List (Var),
+                     CL_Checks => Var_Checks);
+
+                  --  The components of the current variant produced at least
+                  --  one invariant check.
+
+                  if Present (Var_Checks) then
+                     Var_Stmts := Var_Checks;
+                     Produced_Variant_Check := True;
+
+                  --  Otherwise there are either no components with invariants,
+                  --  assertions are disabled, or Assertion_Policy Ignore is in
+                  --  effect.
+
+                  else
+                     Var_Stmts := New_List (Make_Null_Statement (Loc));
+                  end if;
+
+                  Create_Append (Var_Alts,
+                    Make_Case_Statement_Alternative (Loc,
+                      Discrete_Choices =>
+                        New_Copy_List (Discrete_Choices (Var)),
+                      Statements       => Var_Stmts));
+
+                  Next (Var);
+               end loop;
+
+               --  Create a case statement which verifies the invariant checks
+               --  of a particular component list depending on the discriminant
+               --  values only when there is at least one real invariant check.
+
+               if Produced_Variant_Check then
+                  Create_Append (CL_Checks,
+                    Make_Case_Statement (Loc,
+                      Expression   =>
+                        Make_Selected_Component (Loc,
+                          Prefix        => New_Occurrence_Of (Obj_Id, Loc),
+                          Selector_Name =>
+                            New_Occurrence_Of
+                              (Entity (Name (Variant_Part (Comp_List))), Loc)),
+                      Alternatives => Var_Alts));
+               end if;
+            end if;
+         end Process_Component_List;
+
+         ------------------------------
+         -- Process_Record_Component --
+         ------------------------------
+
+         procedure Process_Record_Component
+           (Comp_Id     : Entity_Id;
+            Comp_Checks : in out List_Id)
+         is
+            Comp_Typ : constant Entity_Id := Etype (Comp_Id);
+            Proc_Id  : Entity_Id;
+
+            Produced_Component_Check : Boolean := False;
+            --  This flag tracks whether the component has produced at least
+            --  one invariant check.
+
+         begin
+            --  Nothing to do for internal component _parent. Note that it is
+            --  not desirable to check whether the component comes from source
+            --  because protected type components are relocated to an internal
+            --  corresponding record, but still need processing.
+
+            if Chars (Comp_Id) = Name_uParent then
+               return;
+            end if;
+
+            --  Verify the invariant of the component. Note that an access
+            --  type may have an invariant when it acts as the full view of a
+            --  private type and the invariant appears on the partial view. In
+            --  this case verify the access value itself.
+
+            if Has_Invariants (Comp_Typ) then
+               Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
+
+               --  The component type should have an invariant procedure if it
+               --  has invariants of its own or inherits class-wide invariants
+               --  from parent or interface types.
+
+               pragma Assert (Present (Proc_Id));
+
+               --  Generate:
+               --    <Comp_Typ>Invariant (T (_object).<Comp_Id>);
+
+               --  Note that the invariant procedure may have a null body if
+               --  assertions are disabled or Assertion_Polity Ignore is in
+               --  effect.
+
+               if not Has_Null_Body (Proc_Id) then
+                  Create_Append (Comp_Checks,
+                    Make_Procedure_Call_Statement (Loc,
+                      Name                   =>
+                        New_Occurrence_Of (Proc_Id, Loc),
+                      Parameter_Associations => New_List (
+                        Make_Selected_Component (Loc,
+                          Prefix        =>
+                            Unchecked_Convert_To
+                              (T, New_Occurrence_Of (Obj_Id, Loc)),
+                          Selector_Name =>
+                            New_Occurrence_Of (Comp_Id, Loc)))));
+               end if;
+
+               Produced_Check           := True;
+               Produced_Component_Check := True;
+            end if;
+
+            --  In a rare case the designated type of an access component may
+            --  have a invariant. In this case verify the dereference of the
+            --  component.
+
+            if Is_Access_Type (Comp_Typ)
+              and then Has_Invariants (Designated_Type (Comp_Typ))
+            then
+               Proc_Id :=
+                 Invariant_Procedure (Base_Type (Designated_Type (Comp_Typ)));
+
+               --  The designated type should have an invariant procedure if it
+               --  has invariants of its own or inherits class-wide invariants
+               --  from parent or interface types.
+
+               pragma Assert (Present (Proc_Id));
+
+               --  Generate:
+               --    if T (_object).<Comp_Id> /= null then
+               --       <Desig_Comp_Typ>Invariant (T (_object).<Comp_Id>.all);
+               --    end if;
+
+               --  Note that the invariant procedure may have a null body if
+               --  assertions are disabled or Assertion_Polity Ignore is in
+               --  effect.
+
+               if not Has_Null_Body (Proc_Id) then
+                  Create_Append (Comp_Checks,
+                    Make_If_Statement (Loc,
+                      Condition       =>
+                        Make_Op_Ne (Loc,
+                          Left_Opnd  =>
+                            Make_Selected_Component (Loc,
+                              Prefix        =>
+                                Unchecked_Convert_To
+                                  (T, New_Occurrence_Of (Obj_Id, Loc)),
+                              Selector_Name =>
+                                New_Occurrence_Of (Comp_Id, Loc)),
+                          Right_Opnd => Make_Null (Loc)),
+
+                      Then_Statements => New_List (
+                        Make_Procedure_Call_Statement (Loc,
+                          Name                   =>
+                            New_Occurrence_Of (Proc_Id, Loc),
+
+                          Parameter_Associations => New_List (
+                            Make_Explicit_Dereference (Loc,
+                              Prefix =>
+                                Make_Selected_Component (Loc,
+                                  Prefix        =>
+                                    Unchecked_Convert_To
+                                      (T, New_Occurrence_Of (Obj_Id, Loc)),
+                                  Selector_Name =>
+                                    New_Occurrence_Of (Comp_Id, Loc))))))));
+               end if;
+
+               Produced_Check           := True;
+               Produced_Component_Check := True;
+            end if;
+
+            if Produced_Component_Check and then Has_Unchecked_Union (T) then
+               Error_Msg_NE
+                 ("invariants cannot be checked on components of "
+                  & "unchecked_union type &?", Comp_Id, T);
+            end if;
+         end Process_Record_Component;
+
+         --  Local variables
+
+         Comps : Node_Id;
+         Def   : Node_Id;
+
+      --  Start of processing for Add_Record_Component_Invariants
+
+      begin
+         --  An untagged derived type inherits the components of its parent
+         --  type. In order to avoid creating redundant invariant checks, do
+         --  not process the components now. Instead wait until the ultimate
+         --  parent of the untagged derivation chain is reached.
+
+         if not Is_Untagged_Derivation (T) then
+            Def := Type_Definition (Parent (T));
+
+            if Nkind (Def) = N_Derived_Type_Definition then
+               Def := Record_Extension_Part (Def);
+            end if;
+
+            pragma Assert (Nkind (Def) = N_Record_Definition);
+            Comps := Component_List (Def);
+
+            if Present (Comps) then
+               Process_Component_List
+                 (Comp_List => Comps,
+                  CL_Checks => Checks);
+            end if;
+         end if;
+      end Add_Record_Component_Invariants;
+
+      -------------------------
+      -- Add_Type_Invariants --
+      -------------------------
+
+      procedure Add_Type_Invariants
+        (Priv_Typ  : Entity_Id;
+         Full_Typ  : Entity_Id;
+         CRec_Typ  : Entity_Id;
+         Obj_Id    : Entity_Id;
+         Checks    : in out List_Id;
+         Inherit   : Boolean := False;
+         Priv_Item : Node_Id := Empty)
+      is
+         procedure Add_Invariant (Prag : Node_Id);
+         --  Create a runtime check to verify the invariant exression of pragma
+         --  Prag. All generated code is added to list Checks.
+
+         procedure Process_Type (T : Entity_Id; Stop_Item : Node_Id := Empty);
+         --  Generate invariant checks for type T by inspecting the rep item
+         --  chain of the type. Stop_Item denotes a rep item which once seen
+         --  will stop the inspection.
+
+         -------------------
+         -- Add_Invariant --
+         -------------------
+
+         procedure Add_Invariant (Prag : Node_Id) is
+            Rep_Typ : Entity_Id;
+            --  The replacement type used in the substitution of the current
+            --  instance of a type with the _object formal parameter.
+
+            procedure Replace_Type_Ref (N : Node_Id);
+            --  Substitute the occurrence of a type name denoted by N with a
+            --  reference to the _object formal parameter.
+
+            ----------------------
+            -- Replace_Type_Ref --
+            ----------------------
+
+            procedure Replace_Type_Ref (N : Node_Id) is
+               Nloc : constant Source_Ptr := Sloc (N);
+               Ref  : Node_Id;
+
+            begin
+               --  Decorate the reference to Ref_Typ even though it may be
+               --  rewritten further down. This is done for two reasons:
+
+               --    1) ASIS has all necessary semantic information in the
+               --    original tree.
+
+               --    2) Routines which examine properties of the Original_Node
+               --    have some semantic information.
+
+               if Nkind (N) = N_Identifier then
+                  Set_Entity (N, Rep_Typ);
+                  Set_Etype  (N, Rep_Typ);
+
+               elsif Nkind (N) = N_Selected_Component then
+                  Analyze (Prefix (N));
+                  Set_Entity (Selector_Name (N), Rep_Typ);
+                  Set_Etype  (Selector_Name (N), Rep_Typ);
+               end if;
+
+               --  Do not alter the tree for ASIS. As a result all references
+               --  to Ref_Typ remain as is, but they have sufficent semantic
+               --  information.
+
+               if not ASIS_Mode then
+
+                  --  Perform the following substitution:
+
+                  --    Ref_Typ  -->  _object
+
+                  Ref := Make_Identifier (Nloc, Chars (Obj_Id));
+                  Set_Entity (Ref, Obj_Id);
+                  Set_Etype  (Ref, Rep_Typ);
+
+                  --  When the pragma denotes a class-wide invariant, perform
+                  --  the following substitution:
+
+                  --    Rep_Typ  -->  Rep_Typ'Class (_object)
+
+                  if Class_Present (Prag) then
+                     Ref :=
+                       Make_Type_Conversion (Nloc,
+                         Subtype_Mark =>
+                           Make_Attribute_Reference (Nloc,
+                             Prefix         =>
+                               New_Occurrence_Of (Rep_Typ, Nloc),
+                             Attribute_Name => Name_Class),
+                         Expression   => Ref);
+                  end if;
+
+                  Rewrite (N, Ref);
+                  Set_Comes_From_Source (N, True);
+               end if;
+            end Replace_Type_Ref;
+
+            procedure Replace_Type_Refs is
+              new Replace_Type_References_Generic (Replace_Type_Ref);
+
+            --  Local variables
+
+            Asp  : constant Node_Id    := Corresponding_Aspect (Prag);
+            Nam  : constant Name_Id    := Original_Aspect_Pragma_Name (Prag);
+            Ploc : constant Source_Ptr := Sloc (Prag);
+
+            Arg1      : Node_Id;
+            Arg2      : Node_Id;
+            Arg3      : Node_Id;
+            ASIS_Expr : Node_Id;
+            Assoc     : List_Id;
+            Expr      : Node_Id;
+            Str       : String_Id;
+
+         --  Start of processing for Add_Invariant
+
+         begin
+            --  Nothing to do if the pragma was already processed
+
+            if Contains (Pragmas_Seen, Prag) then
+               return;
+            end if;
+
+            --  Extract the arguments of the invariant pragma
+
+            Arg1 := First (Pragma_Argument_Associations (Prag));
+            Arg2 := Next (Arg1);
+            Arg3 := Next (Arg2);
+
+            Arg1 := Get_Pragma_Arg (Arg1);
+            Arg2 := Get_Pragma_Arg (Arg2);
+
+            --  The pragma applies to the partial view
+
+            if Present (Priv_Typ) and then Entity (Arg1) = Priv_Typ then
+               Rep_Typ := Priv_Typ;
+
+            --  The pragma applies to the full view
+
+            elsif Present (Full_Typ) and then Entity (Arg1) = Full_Typ then
+               Rep_Typ := Full_Typ;
+
+            --  Otherwise the pragma applies to a parent type in which case it
+            --  will be processed at a later stage by Add_Parent_Invariants or
+            --  Add_Interface_Invariants.
+
+            else
+               return;
+            end if;
+
+            --  Nothing to do when the caller requests the processing of all
+            --  inherited class-wide invariants, but the pragma does not fall
+            --  in this category.
+
+            if Inherit and then not Class_Present (Prag) then
+               return;
+            end if;
+
+            Expr := New_Copy_Tree (Arg2);
+
+            --  Substitute all references to type Rep_Typ with references to
+            --  the _object formal parameter.
+
+            Replace_Type_Refs (Expr, Rep_Typ);
+
+            --  Additional processing for non-class-wide invariants
+
+            if not Inherit then
+
+               --  Preanalyze the invariant expression to detect errors and at
+               --  the same time capture the visibility of the proper package
+               --  part.
+
+               --  Historical note: the old implementation of invariants used
+               --  node N as the parent, but a package specification as parent
+               --  of an expression is bizarre.
+
+               Set_Parent (Expr, Parent (Arg2));
+               Preanalyze_Assert_Expression (Expr, Any_Boolean);
+
+               --  If the pragma comes from an aspect specification, replace
+               --  the saved expression because all type references must be
+               --  substituted for the call to Preanalyze_Spec_Expression in
+               --  Check_Aspect_At_xxx routines.
+
+               if Present (Asp) then
+                  Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
+               end if;
+
+               --  Analyze the original invariant expression for ASIS
+
+               if ASIS_Mode then
+                  ASIS_Expr := Empty;
+
+                  if Comes_From_Source (Prag) then
+                     ASIS_Expr := Arg2;
+                  elsif Present (Asp) then
+                     ASIS_Expr := Expression (Asp);
+                  end if;
+
+                  if Present (ASIS_Expr) then
+                     Replace_Type_Refs (ASIS_Expr, Rep_Typ);
+                     Preanalyze_Assert_Expression (ASIS_Expr, Any_Boolean);
+                  end if;
+               end if;
+
+               --  A class-wide invariant may be inherited in a separate unit,
+               --  where the corresponding expression cannot be resolved by
+               --  visibility, because it refers to a local function. Propagate
+               --  semantic information to the original representation item, to
+               --  be used when an invariant procedure for a derived type is
+               --  constructed.
+
+               --  ??? Unclear how to handle class-wide invariants that are not
+               --  function calls.
+
+               if Class_Present (Prag)
+                 and then Nkind (Expr) = N_Function_Call
+                 and then Nkind (Arg2) = N_Indexed_Component
+               then
+                  Rewrite (Arg2,
+                    Make_Function_Call (Ploc,
+                      Name                   =>
+                        New_Occurrence_Of (Entity (Name (Expr)), Ploc),
+                      Parameter_Associations => Expressions (Arg2)));
+               end if;
+            end if;
+
+            --  The invariant is ignored, nothing left to do
+
+            if Is_Ignored (Prag) then
+               null;
+
+            --  Otherwise the invariant is checked. Build a Check pragma to
+            --  verify the expression at runtime.
+
+            else
+               Assoc := New_List (
+                 Make_Pragma_Argument_Association (Ploc,
+                   Expression => Make_Identifier (Ploc, Nam)),
+                 Make_Pragma_Argument_Association (Ploc,
+                   Expression => Expr));
+
+               --  Handle the String argument (if any)
+
+               if Present (Arg3) then
+                  Str := Strval (Get_Pragma_Arg (Arg3));
+
+                  --  When inheriting an invariant, modify the message from
+                  --  "failed invariant" to "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 (Ploc,
+                      Expression => Make_String_Literal (Ploc, Str)));
+               end if;
+
+               --  Generate:
+               --    pragma Check (<Nam>, <Expr>, <Str>);
+
+               Create_Append (Checks,
+                 Make_Pragma (Ploc,
+                   Pragma_Identifier            =>
+                     Make_Identifier (Ploc, Name_Check),
+                   Pragma_Argument_Associations => Assoc));
+            end if;
+
+            --  Output an info message when inheriting an invariant and the
+            --  listing option is enabled.
+
+            if Inherit and Opt.List_Inherited_Aspects then
+               Error_Msg_Sloc := Sloc (Prag);
+               Error_Msg_N
+                 ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
+            end if;
+
+            --  Add the pragma to the list of processed pragmas
+
+            Append_New_Elmt (Prag, Pragmas_Seen);
+            Produced_Check := True;
+         end Add_Invariant;
+
+         ------------------
+         -- Process_Type --
+         ------------------
+
+         procedure Process_Type
+           (T         : Entity_Id;
+            Stop_Item : Node_Id := Empty)
+         is
+            Rep_Item : Node_Id;
+
+         begin
+            Rep_Item := First_Rep_Item (T);
+            while Present (Rep_Item) loop
+               if Nkind (Rep_Item) = N_Pragma
+                 and then Pragma_Name (Rep_Item) = Name_Invariant
+               then
+                  --  Stop the traversal of the rep item chain once a specific
+                  --  item is encountered.
+
+                  if Present (Stop_Item) and then Rep_Item = Stop_Item then
+                     exit;
+
+                  --  Otherwise generate an invariant check
+
+                  else
+                     Add_Invariant (Rep_Item);
+                  end if;
+               end if;
+
+               Next_Rep_Item (Rep_Item);
+            end loop;
+         end Process_Type;
+
+      --  Start of processing for Add_Type_Invariants
+
+      begin
+         --  Process the invariants of the partial view
+
+         if Present (Priv_Typ) then
+            Process_Type (Priv_Typ);
+         end if;
+
+         --  Process the invariants of the full view
+
+         if Present (Full_Typ) then
+            Process_Type (Full_Typ, Stop_Item => Priv_Item);
+
+            --  Process the elements of an array type
+
+            if Is_Array_Type (Full_Typ) then
+               Add_Array_Component_Invariants (Full_Typ, Obj_Id, Checks);
+
+            --  Process the components of a record type
+
+            elsif Ekind (Full_Typ) = E_Record_Type then
+               Add_Record_Component_Invariants (Full_Typ, Obj_Id, Checks);
+            end if;
+         end if;
+
+         --  Process the components of a corresponding record type
+
+         if Present (CRec_Typ) then
+            Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Checks);
+         end if;
+      end Add_Type_Invariants;
+
+      -------------------
+      -- Create_Append --
+      -------------------
+
+      procedure Create_Append (L : in out List_Id; N : Node_Id) is
+      begin
+         if No (L) then
+            L := New_List;
+         end if;
+
+         Append_To (L, N);
+      end Create_Append;
+
+      ------------------------------------
+      -- Is_Untagged_Private_Derivation --
+      ------------------------------------
+
+      function Is_Untagged_Private_Derivation
+        (Priv_Typ : Entity_Id;
+         Full_Typ : Entity_Id) return Boolean
+      is
+      begin
+         return
+           Present (Priv_Typ)
+             and then Is_Untagged_Derivation (Priv_Typ)
+             and then Is_Private_Type (Etype (Priv_Typ))
+             and then Present (Full_Typ)
+             and then Is_Itype (Full_Typ);
+      end Is_Untagged_Private_Derivation;
+
+      --  Local variables
+
+      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
+      Dummy        : Entity_Id;
+      Priv_Item    : Node_Id;
+      Proc_Body    : Node_Id;
+      Proc_Body_Id : Entity_Id;
+      Proc_Decl    : Node_Id;
+      Proc_Id      : Entity_Id;
+      Stmts        : List_Id := No_List;
+
+      CRec_Typ : Entity_Id;
+      --  The corresponding record type of Full_Typ
+
+      Full_Proc : Entity_Id;
+      --  The entity of the "full" invariant procedure
+
+      Full_Typ : Entity_Id;
+      --  The full view of the working type
+
+      Freeze_Typ : Entity_Id;
+      --  The freeze type whose freeze node carries the invariant procedure
+      --  body. This is either the partial or the full view of the working
+      --  type.
+
+      Obj_Id : Entity_Id;
+      --  The _object formal parameter of the invariant procedure
+
+      Part_Proc : Entity_Id;
+      --  The entity of the "partial" invariant procedure
+
+      Priv_Typ : Entity_Id;
+      --  The partial view of the working type
+
+      Work_Typ : Entity_Id;
+      --  The working type
+
+   --  Start of processing for Build_Invariant_Procedure_Body
+
+   begin
+      Work_Typ := Typ;
+
+      --  The input type denotes the implementation base type of a constrained
+      --  array type. Work with the first subtype as all invariant pragmas are
+      --  on its rep item chain.
+
+      if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
+         Work_Typ := First_Subtype (Work_Typ);
+
+      --  The input type denotes the corresponding record type of a protected
+      --  or task type. Work with the concurrent type because the corresponding
+      --  record type may not be visible to clients of the type.
+
+      elsif Ekind (Work_Typ) = E_Record_Type
+        and then Is_Concurrent_Record_Type (Work_Typ)
+      then
+         Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
+      end if;
+
+      --  The type must either have invariants of its own, inherit class-wide
+      --  invariants from parent types or interfaces, or be an array or record
+      --  type whose components have invariants.
+
+      pragma Assert (Has_Invariants (Work_Typ));
+
+      --  Nothing to do for interface types as their class-wide invariants are
+      --  inherited by implementing types.
+
+      if Is_Interface (Work_Typ) then
+         return;
+      end if;
+
+      --  Obtain both views of the type
+
+      Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ);
+
+      --  The caller requests a body for the partial invariant procedure
+
+      if Partial_Invariant then
+         Full_Proc := Invariant_Procedure (Work_Typ);
+         Proc_Id   := Partial_Invariant_Procedure (Work_Typ);
+
+         --  The "full" invariant procedure body was already created
+
+         if Present (Full_Proc)
+           and then Present
+                      (Corresponding_Body (Unit_Declaration_Node (Full_Proc)))
+         then
+            --  This scenario happens only when the type is an untagged
+            --  derivation from a private parent and the underlying full
+            --  view was processed before the partial view.
+
+            pragma Assert
+              (Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ));
+
+            --  Nothing to do because the processing of the underlying full
+            --  view already checked the invariants of the partial view.
+
+            return;
+         end if;
+
+         --  Create a declaration for the "partial" invariant procedure if it
+         --  is not available.
+
+         if No (Proc_Id) then
+            Build_Invariant_Procedure_Declaration
+              (Typ               => Work_Typ,
+               Partial_Invariant => True);
+
+            Proc_Id := Partial_Invariant_Procedure (Work_Typ);
+         end if;
+
+      --  The caller requests a body for the "full" invariant procedure
+
+      else
+         Proc_Id   := Invariant_Procedure (Work_Typ);
+         Part_Proc := Partial_Invariant_Procedure (Work_Typ);
+
+         --  Create a declaration for the "full" invariant procedure if it is
+         --  not available.
+
+         if No (Proc_Id) then
+            Build_Invariant_Procedure_Declaration (Work_Typ);
+            Proc_Id := Invariant_Procedure (Work_Typ);
+         end if;
+      end if;
+
+      --  At this point there should be an invariant procedure declaration
+
+      pragma Assert (Present (Proc_Id));
+      Proc_Decl := Unit_Declaration_Node (Proc_Id);
+
+      --  Nothing to do if the invariant procedure already has a body
+
+      if Present (Corresponding_Body (Proc_Decl)) then
+         return;
+      end if;
+
+      --  The working type may be subject to pragma Ghost. Set the mode now to
+      --  ensure that the invariant procedure is properly marked as Ghost.
+
+      Set_Ghost_Mode_From_Entity (Work_Typ);
+
+      Obj_Id := First_Formal (Proc_Id);
+
+      --  The "partial" invariant procedure verifies the invariants of the
+      --  partial view only.
+
+      if Partial_Invariant then
+         pragma Assert (Present (Priv_Typ));
+         Freeze_Typ := Priv_Typ;
+
+         --  Emulate the environment of the invariant procedure by installing
+         --  its scope and formal parameters. Note that this is not need, but
+         --  having the scope of the invariant procedure installed helps with
+         --  the detection of invariant-related errors.
+
+         Push_Scope (Proc_Id);
+         Install_Formals (Proc_Id);
+
+         Add_Type_Invariants
+           (Priv_Typ => Priv_Typ,
+            Full_Typ => Empty,
+            CRec_Typ => Empty,
+            Obj_Id   => Obj_Id,
+            Checks   => Stmts);
+
+         End_Scope;
+
+      --  Otherwise the "full" invariant procedure verifies the invariants of
+      --  the full view, all array or record components, as well as class-wide
+      --  invariants inherited from parent types or interfaces. In addition, it
+      --  indirectly verifies the invariants of the partial view by calling the
+      --  "partial" invariant procedure.
+
+      else
+         pragma Assert (Present (Full_Typ));
+         Freeze_Typ := Full_Typ;
+
+         --  Check the invariants of the partial view by calling the "partial"
+         --  invariant procedure. Generate:
+
+         --    <Work_Typ>Partial_Invariant (_object);
+
+         if Present (Part_Proc) then
+            Create_Append (Stmts,
+              Make_Procedure_Call_Statement (Loc,
+                Name                   => New_Occurrence_Of (Part_Proc, Loc),
+                Parameter_Associations => New_List (
+                  New_Occurrence_Of (Obj_Id, Loc))));
+
+            Produced_Check := True;
+         end if;
+
+         Priv_Item := Empty;
+
+         --  Derived subtypes do not have a partial view
+
+         if Present (Priv_Typ) then
+
+            --  The processing of the "full" invariant procedure intentionally
+            --  skips the partial view because a) this may result in changes of
+            --  visibility and b) lead to duplicate checks. However, when the
+            --  full view is the underlying full view of an untagged derived
+            --  type whose parent type is private, partial invariants appear on
+            --  the rep item chain of the partial view only.
+
+            --    package Pack_1 is
+            --       type Root ... is private;
+            --    private
+            --       <full view of Root>
+            --    end Pack_1;
+
+            --    with Pack_1;
+            --    package Pack_2 is
+            --       type Child is new Pack_1.Root with Type_Invariant => ...;
+            --       <underlying full view of Child>
+            --    end Pack_2;
+
+            --  As a result, the processing of the full view must also consider
+            --  all invariants of the partial view.
+
+            if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then
+               null;
+
+            --  Otherwise the invariants of the partial view are ignored
+
+            else
+               --  Note that the rep item chain is shared between the partial
+               --  and full views of a type. To avoid processing the invariants
+               --  of the partial view, signal the logic to stop when the first
+               --  rep item of the partial view has been reached.
+
+               Priv_Item := First_Rep_Item (Priv_Typ);
+
+               --  Ignore the invariants of the partial view by eliminating the
+               --  view.
+
+               Priv_Typ := Empty;
+            end if;
+         end if;
+
+         --  Process the invariants of the full view and in certain cases those
+         --  of the partial view. This also handles any invariants on array or
+         --  record components.
+
+         Add_Type_Invariants
+           (Priv_Typ  => Priv_Typ,
+            Full_Typ  => Full_Typ,
+            CRec_Typ  => CRec_Typ,
+            Obj_Id    => Obj_Id,
+            Checks    => Stmts,
+            Priv_Item => Priv_Item);
+
+         --  Process the inherited class-wide invariants of all parent types.
+         --  This also handles any invariants on record components.
+
+         Add_Parent_Invariants (Full_Typ, Obj_Id, Stmts);
+
+         --  Process the inherited class-wide invariants of all implemented
+         --  interface types.
+
+         Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts);
+      end if;
+
+      --  At this point there should be at least one invariant check. If this
+      --  is not the case, then the invariant-related flags were not properly
+      --  set, or there is a missing invariant procedure on one of the array
+      --  or record components.
+
+      pragma Assert (Produced_Check);
+
+      --  Account for the case where assertions are disabled or all invariant
+      --  checks are subject to Assertion_Policy Ignore. Produce a completing
+      --  empty body.
+
+      if No (Stmts) then
+         Stmts := New_List (Make_Null_Statement (Loc));
+      end if;
+
+      Proc_Body :=
+        Make_Subprogram_Body (Loc,
+          Specification                =>
+            Copy_Subprogram_Spec (Parent (Proc_Id)),
+          Declarations                 => Empty_List,
+            Handled_Statement_Sequence =>
+              Make_Handled_Sequence_Of_Statements (Loc,
+                Statements => Stmts));
+      Proc_Body_Id := Defining_Entity (Proc_Body);
+
+      --  Link both spec and body to avoid generating duplicates
+
+      Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
+      Set_Corresponding_Spec (Proc_Body, Proc_Id);
+
+      Append_Freeze_Action (Freeze_Typ, Proc_Body);
+      Ghost_Mode := Save_Ghost_Mode;
+   end Build_Invariant_Procedure_Body;
+
+   -------------------------------------------
+   -- Build_Invariant_Procedure_Declaration --
+   -------------------------------------------
+
+   procedure Build_Invariant_Procedure_Declaration
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False)
+   is
+      Loc : constant Source_Ptr := Sloc (Typ);
+
+      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
+      Proc_Id  : Entity_Id;
+      Typ_Decl : Node_Id;
+
+      CRec_Typ : Entity_Id;
+      --  The corresponding record type of Full_Typ
+
+      Full_Base : Entity_Id;
+      --  The base type of Full_Typ
+
+      Full_Typ : Entity_Id;
+      --  The full view of working type
+
+      Obj_Id : Entity_Id;
+      --  The _object formal parameter of the invariant procedure
+
+      Priv_Typ : Entity_Id;
+      --  The partial view of working type
+
+      Work_Typ : Entity_Id;
+      --  The working type
+
+   begin
+      Work_Typ := Typ;
+
+      --  The input type denotes the implementation base type of a constrained
+      --  array type. Work with the first subtype as all invariant pragmas are
+      --  on its rep item chain.
+
+      if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
+         Work_Typ := First_Subtype (Work_Typ);
+
+      --  The input denotes the corresponding record type of a protected or a
+      --  task type. Work with the concurrent type because the corresponding
+      --  record type may not be visible to clients of the type.
+
+      elsif Ekind (Work_Typ) = E_Record_Type
+        and then Is_Concurrent_Record_Type (Work_Typ)
+      then
+         Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
+      end if;
+
+      --  The type must either have invariants of its own, inherit class-wide
+      --  invariants from parent or interface types, or be an array or record
+      --  type whose components have invariants.
+
+      pragma Assert (Has_Invariants (Work_Typ));
+
+      --  Nothing to do for interface types as their class-wide invariants are
+      --  inherited by implementing types.
+
+      if Is_Interface (Work_Typ) then
+         return;
+
+      --  Nothing to do if the type already has a "partial" invariant procedure
+
+      elsif Partial_Invariant then
+         if Present (Partial_Invariant_Procedure (Work_Typ)) then
+            return;
+         end if;
+
+      --  Nothing to do if the type already has a "full" invariant procedure
+
+      elsif Present (Invariant_Procedure (Work_Typ)) then
+         return;
+      end if;
+
+      --  The working type may be subject to pragma Ghost. Set the mode now to
+      --  ensure that the invariant procedure is properly marked as Ghost.
+
+      Set_Ghost_Mode_From_Entity (Work_Typ);
+
+      --  The caller requests the declaration of the "partial" invariant
+      --  procedure.
+
+      if Partial_Invariant then
+         Proc_Id :=
+           Make_Defining_Identifier (Loc,
+             Chars =>
+               New_External_Name (Chars (Work_Typ), "Partial_Invariant"));
+
+         Set_Ekind (Proc_Id, E_Procedure);
+         Set_Is_Partial_Invariant_Procedure (Proc_Id);
+         Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
+
+      --  Otherwise the caller requests the declaration of the "full" invariant
+      --  procedure.
+
+      else
+         Proc_Id :=
+           Make_Defining_Identifier (Loc,
+             Chars => New_External_Name (Chars (Work_Typ), "Invariant"));
+
+         Set_Ekind (Proc_Id, E_Procedure);
+         Set_Is_Invariant_Procedure (Proc_Id);
+         Set_Invariant_Procedure (Work_Typ, Proc_Id);
+      end if;
+
+      --  The invariant procedure requires debug info when the invariants are
+      --  subject to Source Coverage Obligations.
+
+      if Opt.Generate_SCO then
+         Set_Needs_Debug_Info (Proc_Id);
+      end if;
+
+      --  Mark the invariant procedure explicitly as Ghost because it does not
+      --  come from source.
+
+      if Ghost_Mode > None then
+         Set_Is_Ghost_Entity (Proc_Id);
+      end if;
+
+      --  Obtain all views of the input type
+
+      Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
+
+      --  Associate the invariant procedure with all views
+
+      Propagate_Invariant_Attributes (Priv_Typ,  From_Typ => Work_Typ);
+      Propagate_Invariant_Attributes (Full_Typ,  From_Typ => Work_Typ);
+      Propagate_Invariant_Attributes (Full_Base, From_Typ => Work_Typ);
+      Propagate_Invariant_Attributes (CRec_Typ,  From_Typ => Work_Typ);
+
+      --  The declaration of the invariant procedure is inserted after the
+      --  declaration of the partial view as this allows for proper external
+      --  visibility.
+
+      if Present (Priv_Typ) then
+         Typ_Decl := Declaration_Node (Priv_Typ);
+
+      --  Derived types with the full view as parent do not have a partial
+      --  view. Insert the invariant procedure after the derived type.
+
+      else
+         Typ_Decl := Declaration_Node (Full_Typ);
+      end if;
+
+      --  The type should have a declarative node
+
+      pragma Assert (Present (Typ_Decl));
+
+      --  Create the formal parameter which emulates the variable-like behavior
+      --  of the current type instance.
+
+      Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
+      Set_Ekind (Obj_Id, E_In_Parameter);
+
+      --  Generate:
+      --    procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>);
+
+      Insert_After_And_Analyze (Typ_Decl,
+        Make_Subprogram_Declaration (Loc,
+          Specification =>
+            Make_Procedure_Specification (Loc,
+              Defining_Unit_Name       => Proc_Id,
+              Parameter_Specifications => New_List (
+                Make_Parameter_Specification (Loc,
+                  Defining_Identifier => Obj_Id,
+                  Parameter_Type      =>
+                    New_Occurrence_Of (Work_Typ, Loc))))));
+
+      Ghost_Mode := Save_Ghost_Mode;
+   end Build_Invariant_Procedure_Declaration;
+
    ---------------------
    -- Build_Late_Proc --
    ---------------------
Index: exp_ch7.ads
===================================================================
--- exp_ch7.ads	(revision 237595)
+++ exp_ch7.ads	(working copy)
@@ -118,9 +118,24 @@
    --  finalization master must be analyzed. Insertion_Node is the insertion
    --  point before which the master is to be inserted.
 
+   procedure Build_Invariant_Procedure_Body
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False);
+   --  Create the body of the procedure which verifies the invariants of type
+   --  Typ at runtime. Flag Partial_Invariant should be set when Typ denotes a
+   --  private type, otherwise it is assumed that Typ denotes the full view of
+   --  a private type.
+
+   procedure Build_Invariant_Procedure_Declaration
+     (Typ               : Entity_Id;
+      Partial_Invariant : Boolean := False);
+   --  Create the declaration of the procedure which verifies the invariants of
+   --  type Typ at runtime. Flag Partial_Invariant should be set when building
+   --  the invariant procedure for a private type.
+
    procedure Build_Late_Proc (Typ : Entity_Id; Nam : Name_Id);
-   --  Build one controlling procedure when a late body overrides one of
-   --  the controlling operations.
+   --  Build one controlling procedure when a late body overrides one of the
+   --  controlling operations.
 
    procedure Build_Object_Declarations
      (Data        : out Finalization_Exception_Data;
Index: exp_util.adb
===================================================================
--- exp_util.adb	(revision 237595)
+++ exp_util.adb	(working copy)
@@ -6405,30 +6405,19 @@
    -------------------------
 
    function Make_Invariant_Call (Expr : Node_Id) return Node_Id is
-      Loc : constant Source_Ptr := Sloc (Expr);
-      Typ : Entity_Id;
+      Loc     : constant Source_Ptr := Sloc (Expr);
+      Typ     : constant Entity_Id  := Base_Type (Etype (Expr));
+      Proc_Id : Entity_Id;
 
    begin
-      Typ := Etype (Expr);
+      pragma Assert (Has_Invariants (Typ));
 
-      --  Subtypes may be subject to invariants coming from their respective
-      --  base types. The subtype may be fully or partially private.
+      Proc_Id := Invariant_Procedure (Typ);
+      pragma Assert (Present (Proc_Id));
 
-      if Ekind_In (Typ, E_Array_Subtype,
-                        E_Private_Subtype,
-                        E_Record_Subtype,
-                        E_Record_Subtype_With_Private)
-      then
-         Typ := Base_Type (Typ);
-      end if;
-
-      pragma Assert
-        (Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)));
-
       return
         Make_Procedure_Call_Statement (Loc,
-          Name                   =>
-            New_Occurrence_Of (Invariant_Procedure (Typ), Loc),
+          Name                   => New_Occurrence_Of (Proc_Id, Loc),
           Parameter_Associations => New_List (Relocate_Node (Expr)));
    end Make_Invariant_Call;
 
Index: exp_ch9.adb
===================================================================
--- exp_ch9.adb	(revision 237595)
+++ exp_ch9.adb	(working copy)
@@ -1526,12 +1526,6 @@
       Set_Stored_Constraint             (Rec_Ent, No_Elist);
       Cdecls := New_List;
 
-      --  Propagate type invariants to the corresponding record type
-
-      Set_Has_Invariants                (Rec_Ent, Has_Invariants (Ctyp));
-      Set_Has_Inheritable_Invariants    (Rec_Ent,
-        Has_Inheritable_Invariants (Ctyp));
-
       --  Use discriminals to create list of discriminants for record, and
       --  create new discriminals for use in default expressions, etc. It is
       --  worth noting that a task discriminant gives rise to 5 entities;
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 237595)
+++ sem_ch7.adb	(working copy)
@@ -35,6 +35,7 @@
 with Einfo;     use Einfo;
 with Elists;    use Elists;
 with Errout;    use Errout;
+with Exp_Ch7;   use Exp_Ch7;
 with Exp_Disp;  use Exp_Disp;
 with Exp_Dist;  use Exp_Dist;
 with Exp_Dbug;  use Exp_Dbug;
@@ -1457,15 +1458,17 @@
                Inherit_Default_Init_Cond_Procedure (E);
             end if;
 
-            --  If invariants are present, build the invariant procedure for a
-            --  private type, but not any of its subtypes or interface types.
+            --  Preanalyze and resolve the invariants of a private type at the
+            --  end of the visible declarations to catch potential errors. Note
+            --  that inherited class-wide invariants are not considered because
+            --  they have already been resolved.
 
-            if Has_Invariants (E) then
-               if Ekind (E) = E_Private_Subtype then
-                  null;
-               else
-                  Build_Invariant_Procedure (E, N);
-               end if;
+            if Ekind_In (E, E_Limited_Private_Type,
+                            E_Private_Type,
+                            E_Record_Type_With_Private)
+              and then Has_Own_Invariants (E)
+            then
+               Build_Invariant_Procedure_Body (E, Partial_Invariant => True);
             end if;
          end if;
 
@@ -1473,7 +1476,7 @@
       end loop;
 
       if Is_Remote_Call_Interface (Id)
-         and then Nkind (Parent (Parent (N))) = N_Compilation_Unit
+        and then Nkind (Parent (Parent (N))) = N_Compilation_Unit
       then
          Validate_RCI_Declarations (Id);
       end if;
@@ -1544,7 +1547,6 @@
       if Is_Compilation_Unit (Id) then
          Install_Private_With_Clauses (Id);
       else
-
          --  The current compilation unit may include private with_clauses,
          --  which are visible in the private part of the current nested
          --  package, and have to be installed now. This is not done for
@@ -1636,48 +1638,18 @@
               ("full view of & does not have preelaborable initialization", E);
          end if;
 
-         --  An invariant may appear on a full view of a type
+         --  Preanalyze and resolve the invariants of a private type's full
+         --  view at the end of the private declarations in case freezing did
+         --  not take place either due to errors or because the context is a
+         --  generic unit.
 
          if Is_Type (E)
+           and then not Is_Private_Type (E)
            and then Has_Private_Declaration (E)
-           and then Nkind (Parent (E)) = N_Full_Type_Declaration
+           and then Has_Invariants (E)
+           and then Serious_Errors_Detected > 0
          then
-            declare
-               IP_Built : Boolean := False;
-
-            begin
-               if Has_Aspects (Parent (E)) then
-                  declare
-                     ASN : Node_Id;
-
-                  begin
-                     ASN := First (Aspect_Specifications (Parent (E)));
-                     while Present (ASN) loop
-                        if Nam_In (Chars (Identifier (ASN)),
-                             Name_Invariant,
-                             Name_Type_Invariant)
-                        then
-                           Build_Invariant_Procedure (E, N);
-                           IP_Built := True;
-                           exit;
-                        end if;
-
-                        Next (ASN);
-                     end loop;
-                  end;
-               end if;
-
-               --  Invariants may have been inherited from progenitors
-
-               if not IP_Built
-                 and then Has_Interfaces (E)
-                 and then Has_Inheritable_Invariants (E)
-                 and then not Is_Interface (E)
-                 and then not Is_Class_Wide_Type (E)
-               then
-                  Build_Invariant_Procedure (E, N);
-               end if;
-            end;
+            Build_Invariant_Procedure_Body (E);
          end if;
 
          Next_Entity (E);
@@ -2543,7 +2515,7 @@
       Priv_Elmt : Elmt_Id;
       Priv_Sub  : Entity_Id;
 
-      procedure Preserve_Full_Attributes (Priv, Full : Entity_Id);
+      procedure Preserve_Full_Attributes (Priv : Entity_Id; Full : Entity_Id);
       --  Copy to the private declaration the attributes of the full view that
       --  need to be available for the partial view also.
 
@@ -2554,12 +2526,16 @@
       -- Preserve_Full_Attributes --
       ------------------------------
 
-      procedure Preserve_Full_Attributes (Priv, Full : Entity_Id) is
-         Priv_Is_Base_Type : constant Boolean := Is_Base_Type (Priv);
+      procedure Preserve_Full_Attributes
+        (Priv : Entity_Id;
+         Full : Entity_Id)
+      is
+         Full_Base         : constant Entity_Id := Base_Type (Full);
+         Priv_Is_Base_Type : constant Boolean   := Is_Base_Type (Priv);
 
       begin
-         Set_Size_Info (Priv, (Full));
-         Set_RM_Size                 (Priv, RM_Size (Full));
+         Set_Size_Info               (Priv,                             Full);
+         Set_RM_Size                 (Priv, RM_Size                    (Full));
          Set_Size_Known_At_Compile_Time
                                      (Priv, Size_Known_At_Compile_Time (Full));
          Set_Is_Volatile             (Priv, Is_Volatile                (Full));
@@ -2581,27 +2557,31 @@
          end if;
 
          if Priv_Is_Base_Type then
-            Set_Is_Controlled (Priv, Is_Controlled (Base_Type (Full)));
+            Set_Is_Controlled (Priv, Is_Controlled            (Full_Base));
             Set_Finalize_Storage_Only
-                              (Priv, Finalize_Storage_Only
-                                                   (Base_Type (Full)));
-            Propagate_Concurrent_Flags
-                              (Priv,                Base_Type (Full));
+                              (Priv, Finalize_Storage_Only    (Full_Base));
             Set_Has_Controlled_Component
-                              (Priv, Has_Controlled_Component
-                                                   (Base_Type (Full)));
+                              (Priv, Has_Controlled_Component (Full_Base));
+
+            Propagate_Concurrent_Flags (Priv, Base_Type (Full));
          end if;
 
          Set_Freeze_Node (Priv, Freeze_Node (Full));
 
-         --  Propagate information of type invariants, which may be specified
-         --  for the full view.
+         --  Propagate invariant-related attributes from the base type of the
+         --  full view to the full view and vice versa. This may seem strange,
+         --  but is necessary depending on which type triggered the generation
+         --  of the invariant procedure body. As a result, both the full view
+         --  and its base type carry the same invariant-related information.
 
-         if Has_Invariants (Full) and not Has_Invariants (Priv) then
-            Set_Has_Invariants (Priv);
-            Set_Subprograms_For_Type (Priv, Subprograms_For_Type (Full));
-         end if;
+         Propagate_Invariant_Attributes (Full, From_Typ => Full_Base);
+         Propagate_Invariant_Attributes (Full_Base, From_Typ => Full);
 
+         --  Propagate invariant-related attributes from the full view to the
+         --  private view.
+
+         Propagate_Invariant_Attributes (Priv, From_Typ => Full);
+
          if Is_Tagged_Type (Priv)
            and then Is_Tagged_Type (Full)
            and then not Error_Posted (Full)
@@ -2943,7 +2923,7 @@
                   if Is_Overloadable (Subp) and then Is_Primitive (Subp) then
                      Error_Msg_NE
                        ("type& must be completed in the private part",
-                         Parent (Subp), Id);
+                        Parent (Subp), Id);
 
                   --  The result type of an access-to-function type cannot be a
                   --  Taft-amendment type, unless the version is Ada 2012 or
Index: sem_ch9.adb
===================================================================
--- sem_ch9.adb	(revision 237595)
+++ sem_ch9.adb	(working copy)
@@ -2037,11 +2037,21 @@
 
       Set_Is_Constrained (T, not Has_Discriminants (T));
 
-      --  If aspects are present, analyze them now. They can make references
-      --  to the discriminants of the type, but not to any components.
+      --  If aspects are present, analyze them now. They can make references to
+      --  the discriminants of the type, but not to any components.
 
       if Has_Aspects (N) then
-         Analyze_Aspect_Specifications (N, Def_Id);
+
+         --  The protected type is the full view of a private type. Analyze the
+         --  aspects with the entity of the private type to ensure that after
+         --  both views are exchanged, the aspect are actually associated with
+         --  the full view.
+
+         if T /= Def_Id and then Is_Private_Type (Def_Id) then
+            Analyze_Aspect_Specifications (N, T);
+         else
+            Analyze_Aspect_Specifications (N, Def_Id);
+         end if;
       end if;
 
       Analyze (Protected_Definition (N));
@@ -2194,6 +2204,11 @@
             Set_Must_Have_Preelab_Init (T);
          end if;
 
+         --  Propagate invariant-related attributes from the private type to
+         --  the protected type.
+
+         Propagate_Invariant_Attributes (T, From_Typ => Def_Id);
+
          --  Create corresponding record now, because some private dependents
          --  may be subtypes of the partial view.
 
@@ -3071,7 +3086,17 @@
       Set_Is_Constrained (T, not Has_Discriminants (T));
 
       if Has_Aspects (N) then
-         Analyze_Aspect_Specifications (N, Def_Id);
+
+         --  The task type is the full view of a private type. Analyze the
+         --  aspects with the entity of the private type to ensure that after
+         --  both views are exchanged, the aspect are actually associated with
+         --  the full view.
+
+         if T /= Def_Id and then Is_Private_Type (Def_Id) then
+            Analyze_Aspect_Specifications (N, T);
+         else
+            Analyze_Aspect_Specifications (N, Def_Id);
+         end if;
       end if;
 
       if Present (Task_Definition (N)) then
@@ -3102,9 +3127,8 @@
 
       --  Case of a completion of a private declaration
 
-      if T /= Def_Id
-        and then Is_Private_Type (Def_Id)
-      then
+      if T /= Def_Id and then Is_Private_Type (Def_Id) then
+
          --  Deal with preelaborable initialization. Note that this processing
          --  is done by Process_Full_View, but as can be seen below, in this
          --  case the call to Process_Full_View is skipped if any serious
@@ -3114,6 +3138,11 @@
             Set_Must_Have_Preelab_Init (T);
          end if;
 
+         --  Propagate invariant-related attributes from the private type to
+         --  task type.
+
+         Propagate_Invariant_Attributes (T, From_Typ => Def_Id);
+
          --  Create corresponding record now, because some private dependents
          --  may be subtypes of the partial view.
 
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 237595)
+++ einfo.adb	(working copy)
@@ -245,7 +245,7 @@
    --    Underlying_Record_View          Node28
 
    --    BIP_Initialization_Call         Node29
-   --    Subprograms_For_Type            Node29
+   --    Subprograms_For_Type            Elist29
 
    --    Anonymous_Object                Node30
    --    Corresponding_Equality          Node30
@@ -539,7 +539,7 @@
    --    Has_Pragma_Inline_Always        Flag230
 
    --    Renamed_In_Spec                 Flag231
-   --    Has_Invariants                  Flag232
+   --    Has_Own_Invariants              Flag232
    --    Has_Pragma_Unmodified           Flag233
    --    Is_Dispatch_Table_Entity        Flag234
    --    Is_Trivial_Subprogram           Flag235
@@ -603,10 +603,11 @@
    --    Predicates_Ignored              Flag288
    --    Has_Timing_Event                Flag289
 
-   --    (unused)                        Flag290
+   --    (unused)                        Flag290  --  ??? flag breaks einfo.h
 
-   --    (unused)                        Flag291
-   --    (unused)                        Flag292
+   --    Has_Inherited_Invariants        Flag291
+   --    Is_Partial_Invariant_Procedure  Flag292
+
    --    (unused)                        Flag293
    --    (unused)                        Flag294
    --    (unused)                        Flag295
@@ -614,8 +615,8 @@
    --    (unused)                        Flag297
    --    (unused)                        Flag298
    --    (unused)                        Flag299
+   --    (unused)                        Flag300
 
-   --    (unused)                        Flag300
    --    (unused)                        Flag301
    --    (unused)                        Flag302
    --    (unused)                        Flag303
@@ -1610,18 +1611,18 @@
       return Flag133 (Base_Type (Id));
    end Has_Inherited_Default_Init_Cond;
 
+   function Has_Inherited_Invariants (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag291 (Id);
+   end Has_Inherited_Invariants;
+
    function Has_Initial_Value (Id : E) return B is
    begin
       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_Loop_Entry_Attributes (Id : E) return B is
    begin
       pragma Assert (Ekind (Id) = E_Loop);
@@ -1675,6 +1676,12 @@
       return Flag110 (Id);
    end Has_Out_Or_In_Out_Parameter;
 
+   function Has_Own_Invariants (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag232 (Id);
+   end Has_Own_Invariants;
+
    function Has_Per_Object_Constraint (Id : E) return B is
    begin
       return Flag154 (Id);
@@ -2388,6 +2395,12 @@
       return Flag215 (Base_Type (Id));
    end Is_Param_Block_Component_Type;
 
+   function Is_Partial_Invariant_Procedure (Id : E) return B is
+   begin
+      pragma Assert (Ekind_In (Id, E_Function, E_Procedure));
+      return Flag292 (Id);
+   end Is_Partial_Invariant_Procedure;
+
    function Is_Potentially_Use_Visible (Id : E) return B is
    begin
       pragma Assert (Nkind (Id) in N_Entity);
@@ -3314,10 +3327,10 @@
       return Node18 (Id);
    end String_Literal_Low_Bound;
 
-   function Subprograms_For_Type (Id : E) return E is
+   function Subprograms_For_Type (Id : E) return L is
    begin
-      pragma Assert (Is_Type (Id) or else Is_Subprogram (Id));
-      return Node29 (Id);
+      pragma Assert (Is_Type (Id));
+      return Elist29 (Id);
    end Subprograms_For_Type;
 
    function Subps_Index (Id : E) return U is
@@ -4596,18 +4609,18 @@
       Set_Flag133 (Base_Type (Id), V);
    end Set_Has_Inherited_Default_Init_Cond;
 
+   procedure Set_Has_Inherited_Invariants (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag291 (Id, V);
+   end Set_Has_Inherited_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_Loop_Entry_Attributes (Id : E; V : B := True) is
    begin
       pragma Assert (Ekind (Id) = E_Loop);
@@ -4662,6 +4675,12 @@
       Set_Flag110 (Id, V);
    end Set_Has_Out_Or_In_Out_Parameter;
 
+   procedure Set_Has_Own_Invariants (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag232 (Id, V);
+   end Set_Has_Own_Invariants;
+
    procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True) is
    begin
       Set_Flag154 (Id, V);
@@ -5442,6 +5461,12 @@
       Set_Flag215 (Id, V);
    end Set_Is_Param_Block_Component_Type;
 
+   procedure Set_Is_Partial_Invariant_Procedure (Id : E; V : B := True) is
+   begin
+      pragma Assert (Ekind (Id) = E_Procedure);
+      Set_Flag292 (Id, V);
+   end Set_Is_Partial_Invariant_Procedure;
+
    procedure Set_Is_Potentially_Use_Visible (Id : E; V : B := True) is
    begin
       pragma Assert (Nkind (Id) in N_Entity);
@@ -5450,7 +5475,7 @@
 
    procedure Set_Is_Predicate_Function (Id : E; V : B := True) is
    begin
-      pragma Assert (Ekind_In (Id, E_Function, E_Procedure));
+      pragma Assert (Ekind (Id) = E_Function);
       Set_Flag255 (Id, V);
    end Set_Is_Predicate_Function;
 
@@ -6404,10 +6429,10 @@
       Set_Node18 (Id, V);
    end Set_String_Literal_Low_Bound;
 
-   procedure Set_Subprograms_For_Type (Id : E; V : E) is
+   procedure Set_Subprograms_For_Type (Id : E; V : L) is
    begin
-      pragma Assert (Is_Type (Id) or else Is_Subprogram (Id));
-      Set_Node29 (Id, V);
+      pragma Assert (Is_Type (Id));
+      Set_Elist29 (Id, V);
    end Set_Subprograms_For_Type;
 
    procedure Set_Subps_Index (Id : E; V : U) is
@@ -6945,23 +6970,31 @@
    ---------------------------------
 
    function Default_Init_Cond_Procedure (Id : E) return E is
-      Subp_Id : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
 
    begin
       pragma Assert
         (Is_Type (Id)
           and then (Has_Default_Init_Cond (Id)
-                     or Has_Inherited_Default_Init_Cond (Id)));
+                     or else Has_Inherited_Default_Init_Cond (Id)));
 
-      Subp_Id := Subprograms_For_Type (Base_Type (Id));
-      while Present (Subp_Id) loop
-         if Is_Default_Init_Cond_Procedure (Subp_Id) then
-            return Subp_Id;
-         end if;
+      Subps := Subprograms_For_Type (Base_Type (Id));
 
-         Subp_Id := Subprograms_For_Type (Subp_Id);
-      end loop;
+      if Present (Subps) then
+         Subp_Elmt := First_Elmt (Subps);
+         while Present (Subp_Elmt) loop
+            Subp_Id := Node (Subp_Elmt);
 
+            if Is_Default_Init_Cond_Procedure (Subp_Id) then
+               return Subp_Id;
+            end if;
+
+            Next_Elmt (Subp_Elmt);
+         end loop;
+      end if;
+
       return Empty;
    end Default_Init_Cond_Procedure;
 
@@ -7370,6 +7403,15 @@
       return False;
    end Has_Interrupt_Handler;
 
+   --------------------
+   -- Has_Invariants --
+   --------------------
+
+   function Has_Invariants (Id : E) return B is
+   begin
+      return Has_Own_Invariants (Id) or else Has_Inherited_Invariants (Id);
+   end Has_Invariants;
+
    --------------------------
    -- Has_Non_Limited_View --
    --------------------------
@@ -7533,26 +7575,29 @@
    -------------------------
 
    function Invariant_Procedure (Id : E) return E is
-      S : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
 
    begin
-      pragma Assert (Is_Type (Id) and then Has_Invariants (Id));
+      pragma Assert (Is_Type (Id));
 
-      if No (Subprograms_For_Type (Id)) then
-         return Empty;
+      Subps := Subprograms_For_Type (Id);
 
-      else
-         S := Subprograms_For_Type (Id);
-         while Present (S) loop
-            if Is_Invariant_Procedure (S) then
-               return S;
-            else
-               S := Subprograms_For_Type (S);
+      if Present (Subps) then
+         Subp_Elmt := First_Elmt (Subps);
+         while Present (Subp_Elmt) loop
+            Subp_Id := Node (Subp_Elmt);
+
+            if Is_Invariant_Procedure (Subp_Id) then
+               return Subp_Id;
             end if;
+
+            Next_Elmt (Subp_Elmt);
          end loop;
+      end if;
 
-         return Empty;
-      end if;
+      return Empty;
    end Invariant_Procedure;
 
    ----------------------
@@ -8261,46 +8306,81 @@
       return Ekind (Id);
    end Parameter_Mode;
 
+   ---------------------------------
+   -- Partial_Invariant_Procedure --
+   ---------------------------------
+
+   function Partial_Invariant_Procedure (Id : E) return E is
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
+
+   begin
+      pragma Assert (Is_Type (Id));
+
+      Subps := Subprograms_For_Type (Id);
+
+      if Present (Subps) then
+         Subp_Elmt := First_Elmt (Subps);
+         while Present (Subp_Elmt) loop
+            Subp_Id := Node (Subp_Elmt);
+
+            if Is_Partial_Invariant_Procedure (Subp_Id) then
+               return Subp_Id;
+            end if;
+
+            Next_Elmt (Subp_Elmt);
+         end loop;
+      end if;
+
+      return Empty;
+   end Partial_Invariant_Procedure;
+
    ------------------------
    -- Predicate_Function --
    ------------------------
 
    function Predicate_Function (Id : E) return E is
-      S : Entity_Id;
-      T : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
+      Typ       : Entity_Id;
 
    begin
       pragma Assert (Is_Type (Id));
 
-      --  If type is private and has a completion, predicate may be defined
-      --  on the full view.
+      --  If type is private and has a completion, predicate may be defined on
+      --  the full view.
 
       if Is_Private_Type (Id)
          and then
            (not Has_Predicates (Id) or else No (Subprograms_For_Type (Id)))
          and then Present (Full_View (Id))
       then
-         T := Full_View (Id);
+         Typ := Full_View (Id);
 
       else
-         T := Id;
+         Typ := Id;
       end if;
 
-      if No (Subprograms_For_Type (T)) then
-         return Empty;
+      Subps := Subprograms_For_Type (Typ);
 
-      else
-         S := Subprograms_For_Type (T);
-         while Present (S) loop
-            if Is_Predicate_Function (S) then
-               return S;
-            else
-               S := Subprograms_For_Type (S);
+      if Present (Subps) then
+         Subp_Elmt := First_Elmt (Subps);
+         while Present (Subp_Elmt) loop
+            Subp_Id := Node (Subp_Elmt);
+
+            if Ekind (Subp_Id) = E_Function
+              and then Is_Predicate_Function (Subp_Id)
+            then
+               return Subp_Id;
             end if;
+
+            Next_Elmt (Subp_Elmt);
          end loop;
+      end if;
 
-         return Empty;
-      end if;
+      return Empty;
    end Predicate_Function;
 
    --------------------------
@@ -8308,36 +8388,46 @@
    --------------------------
 
    function Predicate_Function_M (Id : E) return E is
-      S : Entity_Id;
-      T : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
+      Typ       : Entity_Id;
 
    begin
       pragma Assert (Is_Type (Id));
 
-      --  If type is private and has a completion, predicate may be defined
-      --  on the full view.
+      --  If type is private and has a completion, predicate may be defined on
+      --  the full view.
 
-      if Is_Private_Type (Id) and then Present (Full_View (Id)) then
-         T := Full_View (Id);
+      if Is_Private_Type (Id)
+         and then
+           (not Has_Predicates (Id) or else No (Subprograms_For_Type (Id)))
+         and then Present (Full_View (Id))
+      then
+         Typ := Full_View (Id);
+
       else
-         T := Id;
+         Typ := Id;
       end if;
 
-      if No (Subprograms_For_Type (T)) then
-         return Empty;
+      Subps := Subprograms_For_Type (Typ);
 
-      else
-         S := Subprograms_For_Type (T);
-         while Present (S) loop
-            if Is_Predicate_Function_M (S) then
-               return S;
-            else
-               S := Subprograms_For_Type (S);
+      if Present (Subps) then
+         Subp_Elmt := First_Elmt (Subps);
+         while Present (Subp_Elmt) loop
+            Subp_Id := Node (Subp_Elmt);
+
+            if Ekind (Subp_Id) = E_Function
+              and then Is_Predicate_Function_M (Subp_Id)
+            then
+               return Subp_Id;
             end if;
+
+            Next_Elmt (Subp_Elmt);
          end loop;
+      end if;
 
-         return Empty;
-      end if;
+      return Empty;
    end Predicate_Function_M;
 
    -------------------------
@@ -8563,8 +8653,10 @@
    -------------------------------------
 
    procedure Set_Default_Init_Cond_Procedure (Id : E; V : E) is
-      Base_Typ : Entity_Id;
-      Subp_Id  : Entity_Id;
+      Base_Typ  : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
 
    begin
       --  Once set, this attribute cannot be reset
@@ -8577,21 +8669,29 @@
       pragma Assert
         (Is_Type (Id)
           and then (Has_Default_Init_Cond (Id)
-                     or Has_Inherited_Default_Init_Cond (Id)));
+                     or else Has_Inherited_Default_Init_Cond (Id)));
+
       Base_Typ := Base_Type (Id);
+      Subps    := Subprograms_For_Type (Base_Typ);
 
-      Subp_Id := Subprograms_For_Type (Base_Typ);
-      Set_Subprograms_For_Type (Base_Typ, V);
-      Set_Subprograms_For_Type (V, Subp_Id);
+      if No (Subps) then
+         Subps := New_Elmt_List;
+         Set_Subprograms_For_Type (Base_Typ, Subps);
+      end if;
 
-      --  Check for a duplicate procedure
+      Subp_Elmt := First_Elmt (Subps);
+      Prepend_Elmt (V, Subps);
 
-      while Present (Subp_Id) loop
+      --  Check for a duplicate default initial condition procedure
+
+      while Present (Subp_Elmt) loop
+         Subp_Id := Node (Subp_Elmt);
+
          if Is_Default_Init_Cond_Procedure (Subp_Id) then
             raise Program_Error;
          end if;
 
-         Subp_Id := Subprograms_For_Type (Subp_Id);
+         Next_Elmt (Subp_Elmt);
       end loop;
    end Set_Default_Init_Cond_Procedure;
 
@@ -8600,46 +8700,105 @@
    -----------------------------
 
    procedure Set_Invariant_Procedure (Id : E; V : E) is
-      S : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
 
    begin
-      pragma Assert (Is_Type (Id) and then Has_Invariants (Id));
+      pragma Assert (Is_Type (Id));
 
-      S := Subprograms_For_Type (Id);
-      Set_Subprograms_For_Type (Id, V);
-      Set_Subprograms_For_Type (V, S);
+      Subps := Subprograms_For_Type (Id);
 
-      --  Check for duplicate entry
+      if No (Subps) then
+         Subps := New_Elmt_List;
+         Set_Subprograms_For_Type (Id, Subps);
+      end if;
 
-      while Present (S) loop
-         if Is_Invariant_Procedure (S) then
+      Subp_Elmt := First_Elmt (Subps);
+      Prepend_Elmt (V, Subps);
+
+      --  Check for a duplicate invariant procedure
+
+      while Present (Subp_Elmt) loop
+         Subp_Id := Node (Subp_Elmt);
+
+         if Is_Invariant_Procedure (Subp_Id) then
             raise Program_Error;
-         else
-            S := Subprograms_For_Type (S);
          end if;
+
+         Next_Elmt (Subp_Elmt);
       end loop;
    end Set_Invariant_Procedure;
 
+   -------------------------------------
+   -- Set_Partial_Invariant_Procedure --
+   -------------------------------------
+
+   procedure Set_Partial_Invariant_Procedure (Id : E; V : E) is
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
+
+   begin
+      pragma Assert (Is_Type (Id));
+
+      Subps := Subprograms_For_Type (Id);
+
+      if No (Subps) then
+         Subps := New_Elmt_List;
+         Set_Subprograms_For_Type (Id, Subps);
+      end if;
+
+      Subp_Elmt := First_Elmt (Subps);
+      Prepend_Elmt (V, Subps);
+
+      --  Check for a duplicate partial invariant procedure
+
+      while Present (Subp_Elmt) loop
+         Subp_Id := Node (Subp_Elmt);
+
+         if Is_Partial_Invariant_Procedure (Subp_Id) then
+            raise Program_Error;
+         end if;
+
+         Next_Elmt (Subp_Elmt);
+      end loop;
+   end Set_Partial_Invariant_Procedure;
+
    ----------------------------
    -- Set_Predicate_Function --
    ----------------------------
 
    procedure Set_Predicate_Function (Id : E; V : E) is
-      S : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
 
    begin
       pragma Assert (Is_Type (Id) and then Has_Predicates (Id));
 
-      S := Subprograms_For_Type (Id);
-      Set_Subprograms_For_Type (Id, V);
-      Set_Subprograms_For_Type (V, S);
+      Subps := Subprograms_For_Type (Id);
 
-      while Present (S) loop
-         if Is_Predicate_Function (S) then
+      if No (Subps) then
+         Subps := New_Elmt_List;
+         Set_Subprograms_For_Type (Id, Subps);
+      end if;
+
+      Subp_Elmt := First_Elmt (Subps);
+      Prepend_Elmt (V, Subps);
+
+      --  Check for a duplicate predication function
+
+      while Present (Subp_Elmt) loop
+         Subp_Id := Node (Subp_Elmt);
+
+         if Ekind (Subp_Id) = E_Function
+           and then Is_Predicate_Function (Subp_Id)
+         then
             raise Program_Error;
-         else
-            S := Subprograms_For_Type (S);
          end if;
+
+         Next_Elmt (Subp_Elmt);
       end loop;
    end Set_Predicate_Function;
 
@@ -8648,23 +8807,35 @@
    ------------------------------
 
    procedure Set_Predicate_Function_M (Id : E; V : E) is
-      S : Entity_Id;
+      Subp_Elmt : Elmt_Id;
+      Subp_Id   : Entity_Id;
+      Subps     : Elist_Id;
 
    begin
       pragma Assert (Is_Type (Id) and then Has_Predicates (Id));
 
-      S := Subprograms_For_Type (Id);
-      Set_Subprograms_For_Type (Id, V);
-      Set_Subprograms_For_Type (V, S);
+      Subps := Subprograms_For_Type (Id);
 
-      --  Check for duplicates
+      if No (Subps) then
+         Subps := New_Elmt_List;
+         Set_Subprograms_For_Type (Id, Subps);
+      end if;
 
-      while Present (S) loop
-         if Is_Predicate_Function_M (S) then
+      Subp_Elmt := First_Elmt (Subps);
+      Prepend_Elmt (V, Subps);
+
+      --  Check for a duplicate predication function
+
+      while Present (Subp_Elmt) loop
+         Subp_Id := Node (Subp_Elmt);
+
+         if Ekind (Subp_Id) = E_Function
+           and then Is_Predicate_Function_M (Subp_Id)
+         then
             raise Program_Error;
-         else
-            S := Subprograms_For_Type (S);
          end if;
+
+         Next_Elmt (Subp_Elmt);
       end loop;
    end Set_Predicate_Function_M;
 
@@ -8952,8 +9123,8 @@
       W ("Has_Independent_Components",      Flag34  (Id));
       W ("Has_Inheritable_Invariants",      Flag248 (Id));
       W ("Has_Inherited_Default_Init_Cond", Flag133 (Id));
+      W ("Has_Inherited_Invariants",        Flag291 (Id));
       W ("Has_Initial_Value",               Flag219 (Id));
-      W ("Has_Invariants",                  Flag232 (Id));
       W ("Has_Loop_Entry_Attributes",       Flag260 (Id));
       W ("Has_Machine_Radix_Clause",        Flag83  (Id));
       W ("Has_Master_Entity",               Flag21  (Id));
@@ -8963,6 +9134,7 @@
       W ("Has_Non_Standard_Rep",            Flag75  (Id));
       W ("Has_Out_Or_In_Out_Parameter",     Flag110 (Id));
       W ("Has_Object_Size_Clause",          Flag172 (Id));
+      W ("Has_Own_Invariants",              Flag232 (Id));
       W ("Has_Per_Object_Constraint",       Flag154 (Id));
       W ("Has_Pragma_Controlled",           Flag27  (Id));
       W ("Has_Pragma_Elaborate_Body",       Flag150 (Id));
@@ -9086,6 +9258,7 @@
       W ("Is_Packed",                       Flag51  (Id));
       W ("Is_Packed_Array_Impl_Type",       Flag138 (Id));
       W ("Is_Param_Block_Component_Type",   Flag215 (Id));
+      W ("Is_Partial_Invariant_Procedure",  Flag292 (Id));
       W ("Is_Potentially_Use_Visible",      Flag9   (Id));
       W ("Is_Predicate_Function",           Flag255 (Id));
       W ("Is_Predicate_Function_M",         Flag256 (Id));
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 237595)
+++ einfo.ads	(working copy)
@@ -1698,19 +1698,22 @@
 --       usual manner.
 
 --    Has_Inheritable_Invariants (Flag248)
---       Defined in all type entities. Set 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.
+--       Defined in all type entities. Set on private types and interface types
+--       which define at least one class-wide invariant. Such invariants must
+--       be inherited by derived types. The flag is also set on the full view
+--       of a private type for completeness.
 
 --    Has_Inherited_Default_Init_Cond (Flag133) [base type only]
 --       Defined in all type entities. Set when a derived type inherits pragma
 --       Default_Initial_Condition from its parent type. This flag is mutually
 --       exclusive with flag Has_Default_Init_Cond.
 
+--    Has_Inherited_Invariants (Flag291)
+--       Defined in all type entities. Set on private extensions and derived
+--       types which inherit at least on class-wide invariant from a parent or
+--       an interface type. The flag is also set on the full view of a private
+--       extension for completeness.
+
 --    Has_Initial_Value (Flag219)
 --       Defined in entities for variables and out parameters. Set if there
 --       is an explicit initial value expression in the declaration of the
@@ -1725,15 +1728,10 @@
 --       definition contains at least one procedure to which a pragma
 --       Interrupt_Handler applies.
 
---    Has_Invariants (Flag232)
---       Defined in all type entities and in subprogram entities. Set 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 attribute 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_Invariants (synthesized)
+--       Defined in all type entities. True if the type defines at least one
+--       invariant of its own or inherits at least one class-wide invariant
+--       from a parent type or an interface.
 
 --    Has_Loop_Entry_Attributes (Flag260)
 --       Defined in E_Loop entities. Set when the loop is subject to at least
@@ -1809,6 +1807,11 @@
 --       families. Set if they have at least one OUT or IN OUT parameter
 --       (allowed for functions only in Ada 2012).
 
+--    Has_Own_Invariants (Flag232)
+--       Defined in all type entities. Set on any type which defines at least
+--       one invariant of its own. The flag is also set on the full view of a
+--       private extension or a private type for completeness.
+
 --    Has_Per_Object_Constraint (Flag154)
 --       Defined in E_Component entities. Set if the subtype of the component
 --       has a per object constraint. Per object constraints result from the
@@ -2189,15 +2192,18 @@
 --       ancestors (Ada 2005: AI-251).
 
 --    Invariant_Procedure (synthesized)
---       Defined 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
---       attribute is defined but always empty for private subtypes. This
---       attribute is also set for the corresponding full type.
---
+--       Defined in types and subtypes. Set for private types and their full
+--       views if one or more [class-wide] invariants apply to the type, or
+--       when the type inherits class-wide invariants from a parent type or
+--       an interface, or when the type is an array and its component type is
+--       subject to an invariant, or when the type is record and contains a
+--       component subject to an invariant (property is recursive). Points to
+--       to the entity for a procedure which checks all these invariants. The
+--       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 attribute is
+--       defined but always Empty for private subtypes.
+
 --       Note: the reason this is marked as a synthesized attribute is that the
 --       way this is stored is as an element of the Subprograms_For_Type field.
 
@@ -2267,7 +2273,7 @@
 --       applies to both the partial view and the full view.
 
 --    Is_Base_Type (synthesized)
---       Applies to type and subtype entities. True if entity is a base type
+--       Applies to type and subtype entities. True if entity is a base type.
 
 --    Is_Bit_Packed_Array (Flag122) [implementation base type only]
 --       Defined in all entities. This flag is set for a packed array type that
@@ -2325,9 +2331,9 @@
 --       which are not Completely_Hidden (e.g. discriminants of a root type).
 
 --    Is_Composite_Type (synthesized)
---       Applies to all entities, true for all composite types and
---       subtypes. Either Is_Composite_Type or Is_Elementary_Type (but
---       not both) is true of any type.
+--       Applies to all entities, true for all composite types and subtypes.
+--       Either Is_Composite_Type or Is_Elementary_Type (but not both) is true
+--       of any type.
 
 --    Is_Concurrent_Record_Type (Flag20)
 --       Defined in record types and subtypes. Set if the type was created
@@ -2686,7 +2692,9 @@
 
 --    Is_Invariant_Procedure (Flag257)
 --       Defined in functions and procedures. Set for a generated invariant
---       procedure to identify it easily.
+--       procedure which verifies the invariants of both the partial and full
+--       views of a private type or private extension as well as any inherited
+--       class-wide invariants from parent types or interfaces.
 
 --    Is_Itype (Flag91)
 --       Defined in all entities. Set to indicate that a type is an Itype,
@@ -2912,6 +2920,11 @@
 --       component of the parameter block record type generated by the compiler
 --       for an entry or a select statement. Read by CodePeer.
 
+--    Is_Partial_Invariant_Procedure (Flag292)
+--       Defined in functions and procedures. Set for a generated invariant
+--       procedure which verifies the invariants of the partial view of a
+--       private type or private extension.
+
 --    Is_Potentially_Use_Visible (Flag9)
 --       Defined in all entities. Set if entity is potentially use visible,
 --       i.e. it is defined in a package that appears in a currently active
@@ -3738,6 +3751,18 @@
 --       of a single protected/task type, the references are examined as they
 --       must appear only within the type defintion and the corresponding body.
 
+--    Partial_Invariant_Procedure (synthesized)
+--       Defined in types and subtypes. Set for private types when one or more
+--       [class-wide] type invariants apply to them. Points to the entity for a
+--       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 attribute is defined but always Empty for private
+--       subtypes. This attribute is also set for the corresponding full type.
+--
+--       Note: the reason this is marked as a synthesized attribute is that the
+--       way this is stored is as an element of the Subprograms_For_Type field.
+
 --    Partial_View_Has_Unknown_Discr (Flag280)
 --       Present in all types. Set to Indicate that the partial view of a type
 --       has unknown discriminants. A default initialization of an object of
@@ -4263,15 +4288,14 @@
 --       the low bound of the applicable index constraint if there is one,
 --       or a copy of the low bound of the index base type if not.
 
---    Subprograms_For_Type (Node29)
---       Defined in all type and subprogram entities. This is used to hold
---       a list of subprogram entities for subprograms associated with the
---       type, linked through the Subprograms_For_Type field of the subprogram
---       entity. Basically this is a way of multiplexing the single field to
---       hold more than one entity (since we ran out of space in some type
---       entities). This is currently used for Invariant_Procedure and also
---       for Predicate_Function, and clients will always use the latter two
---       names to access entries in this list.
+--    Subprograms_For_Type (Elist29)
+--       Defined in all types. The list may contain the entities of the default
+--       initial condition procedure, invariant procedure, and the two versions
+--       of the predicate function.
+--
+--       Historical note: This attribute used to be a direct linked list of
+--       entities rather than an Elist. The Elist allows greater flexibility
+--       in inheritance of subprograms between views of the same type.
 
 --    Subps_Index (Uint24)
 --       Present in subprogram entries. Set if the subprogram contains nested
@@ -5471,7 +5495,7 @@
    --    Pending_Access_Types                (Elist15)
    --    Related_Expression                  (Node24)
    --    Current_Use_Clause                  (Node27)
-   --    Subprograms_For_Type                (Node29)
+   --    Subprograms_For_Type                (Elist29)
    --    Derived_Type_Link                   (Node31)
    --    No_Tagged_Streams_Pragma            (Node32)
    --    Linker_Section_Pragma               (Node33)
@@ -5495,11 +5519,12 @@
    --    Has_Discriminants                   (Flag5)
    --    Has_Dynamic_Predicate_Aspect        (Flag258)
    --    Has_Independent_Components          (Flag34)   (base type only)
-   --    Has_Inheritable_Invariants          (Flag248)
+   --    Has_Inheritable_Invariants          (Flag248)  (base type only)
    --    Has_Inherited_Default_Init_Cond     (Flag133)  (base type only)
-   --    Has_Invariants                      (Flag232)
+   --    Has_Inherited_Invariants            (Flag291)  (base type only)
    --    Has_Non_Standard_Rep                (Flag75)   (base type only)
    --    Has_Object_Size_Clause              (Flag172)
+   --    Has_Own_Invariants                  (Flag232)  (base type only)
    --    Has_Pragma_Preelab_Init             (Flag221)
    --    Has_Pragma_Unreferenced_Objects     (Flag212)
    --    Has_Predicates                      (Flag250)
@@ -5553,11 +5578,13 @@
    --    Alignment_Clause                    (synth)
    --    Base_Type                           (synth)
    --    Default_Init_Cond_Procedure         (synth)
+   --    Has_Invariants                      (synth)
    --    Implementation_Base_Type            (synth)
    --    Invariant_Procedure                 (synth)
    --    Is_Access_Protected_Subprogram_Type (synth)
    --    Is_Atomic_Or_VFA                    (synth)
    --    Is_Controlled_Active                (synth)
+   --    Partial_Invariant_Procedure         (synth)
    --    Predicate_Function                  (synth)
    --    Predicate_Function_M                (synth)
    --    Root_Type                           (synth)
@@ -5921,7 +5948,6 @@
    --    Overridden_Operation                (Node26)
    --    Wrapped_Entity                      (Node27)   (non-generic case only)
    --    Extra_Formals                       (Node28)
-   --    Subprograms_For_Type                (Node29)
    --    Corresponding_Equality              (Node30)   (implicit /= only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
    --    Corresponding_Procedure             (Node32)   (generate C code only)
@@ -5942,7 +5968,6 @@
    --    Has_Completion                      (Flag26)
    --    Has_Controlling_Result              (Flag98)
    --    Has_Expanded_Contract               (Flag240)  (non-generic case only)
-   --    Has_Invariants                      (Flag232)
    --    Has_Master_Entity                   (Flag21)
    --    Has_Missing_Return                  (Flag142)
    --    Has_Nested_Block_With_Handler       (Flag101)
@@ -5952,6 +5977,7 @@
    --    Is_Abstract_Subprogram              (Flag19)   (non-generic case only)
    --    Is_Called                           (Flag102)  (non-generic case only)
    --    Is_Constructor                      (Flag76)
+   --    Is_Default_Init_Cond_Procedure      (Flag132)  (non-generic case only)
    --    Is_Discrim_SO_Function              (Flag176)
    --    Is_Discriminant_Check_Function      (Flag264)
    --    Is_Eliminated                       (Flag124)
@@ -5962,6 +5988,7 @@
    --    Is_Intrinsic_Subprogram             (Flag64)
    --    Is_Invariant_Procedure              (Flag257)  (non-generic case only)
    --    Is_Machine_Code_Subprogram          (Flag137)  (non-generic case only)
+   --    Is_Partial_Invariant_Procedure      (Flag292)  (non-generic case only)
    --    Is_Predicate_Function               (Flag255)  (non-generic case only)
    --    Is_Predicate_Function_M             (Flag256)  (non-generic case only)
    --    Is_Primitive                        (Flag218)
@@ -6094,13 +6121,11 @@
    --    Last_Entity                         (Node20)
    --    Subps_Index                         (Uint24)
    --    Overridden_Operation                (Node26)
-   --    Subprograms_For_Type                (Node29)
    --    Linker_Section_Pragma               (Node33)
    --    Contract                            (Node34)
    --    Import_Pragma                       (Node35)
    --    SPARK_Pragma                        (Node40)
    --    Default_Expressions_Processed       (Flag108)
-   --    Has_Invariants                      (Flag232)
    --    Has_Nested_Subprogram               (Flag282)
    --    Is_Intrinsic_Subprogram             (Flag64)
    --    Is_Machine_Code_Subprogram          (Flag137)
@@ -6254,7 +6279,6 @@
    --    Discard_Names                       (Flag88)
    --    Has_Completion                      (Flag26)
    --    Has_Expanded_Contract               (Flag240)  (non-generic case only)
-   --    Has_Invariants                      (Flag232)
    --    Has_Master_Entity                   (Flag21)
    --    Has_Nested_Block_With_Handler       (Flag101)
    --    Has_Nested_Subprogram               (Flag282)
@@ -6273,6 +6297,7 @@
    --    Is_Invariant_Procedure              (Flag257)  (non-generic case only)
    --    Is_Machine_Code_Subprogram          (Flag137)  (non-generic case only)
    --    Is_Null_Init_Proc                   (Flag178)
+   --    Is_Partial_Invariant_Procedure      (Flag292)  (non-generic case only)
    --    Is_Predicate_Function               (Flag255)  (non-generic case only)
    --    Is_Predicate_Function_M             (Flag256)  (non-generic case only)
    --    Is_Primitive                        (Flag218)
@@ -6918,6 +6943,7 @@
    function Has_Independent_Components          (Id : E) return B;
    function Has_Inheritable_Invariants          (Id : E) return B;
    function Has_Inherited_Default_Init_Cond     (Id : E) return B;
+   function Has_Inherited_Invariants            (Id : E) return B;
    function Has_Initial_Value                   (Id : E) return B;
    function Has_Interrupt_Handler               (Id : E) return B;
    function Has_Invariants                      (Id : E) return B;
@@ -6930,6 +6956,7 @@
    function Has_Non_Standard_Rep                (Id : E) return B;
    function Has_Object_Size_Clause              (Id : E) return B;
    function Has_Out_Or_In_Out_Parameter         (Id : E) return B;
+   function Has_Own_Invariants                  (Id : E) return B;
    function Has_Per_Object_Constraint           (Id : E) return B;
    function Has_Pragma_Controlled               (Id : E) return B;
    function Has_Pragma_Elaborate_Body           (Id : E) return B;
@@ -7058,6 +7085,7 @@
    function Is_Packed_Array_Impl_Type           (Id : E) return B;
    function Is_Potentially_Use_Visible          (Id : E) return B;
    function Is_Param_Block_Component_Type       (Id : E) return B;
+   function Is_Partial_Invariant_Procedure      (Id : E) return B;
    function Is_Predicate_Function               (Id : E) return B;
    function Is_Predicate_Function_M             (Id : E) return B;
    function Is_Preelaborated                    (Id : E) return B;
@@ -7208,7 +7236,7 @@
    function Strict_Alignment                    (Id : E) return B;
    function String_Literal_Length               (Id : E) return U;
    function String_Literal_Low_Bound            (Id : E) return N;
-   function Subprograms_For_Type                (Id : E) return E;
+   function Subprograms_For_Type                (Id : E) return L;
    function Subps_Index                         (Id : E) return U;
    function Suppress_Elaboration_Warnings       (Id : E) return B;
    function Suppress_Initialization             (Id : E) return B;
@@ -7589,8 +7617,8 @@
    procedure Set_Has_Independent_Components      (Id : E; V : B := True);
    procedure Set_Has_Inheritable_Invariants      (Id : E; V : B := True);
    procedure Set_Has_Inherited_Default_Init_Cond (Id : E; V : B := True);
+   procedure Set_Has_Inherited_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_Loop_Entry_Attributes       (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);
@@ -7600,6 +7628,7 @@
    procedure Set_Has_Non_Standard_Rep            (Id : E; V : B := True);
    procedure Set_Has_Object_Size_Clause          (Id : E; V : B := True);
    procedure Set_Has_Out_Or_In_Out_Parameter     (Id : E; V : B := True);
+   procedure Set_Has_Own_Invariants              (Id : E; V : B := True);
    procedure Set_Has_Per_Object_Constraint       (Id : E; V : B := True);
    procedure Set_Has_Pragma_Controlled           (Id : E; V : B := True);
    procedure Set_Has_Pragma_Elaborate_Body       (Id : E; V : B := True);
@@ -7732,6 +7761,7 @@
    procedure Set_Is_Packed                       (Id : E; V : B := True);
    procedure Set_Is_Packed_Array_Impl_Type       (Id : E; V : B := True);
    procedure Set_Is_Param_Block_Component_Type   (Id : E; V : B := True);
+   procedure Set_Is_Partial_Invariant_Procedure  (Id : E; V : B := True);
    procedure Set_Is_Potentially_Use_Visible      (Id : E; V : B := True);
    procedure Set_Is_Predicate_Function           (Id : E; V : B := True);
    procedure Set_Is_Predicate_Function_M         (Id : E; V : B := True);
@@ -7882,7 +7912,7 @@
    procedure Set_Strict_Alignment                (Id : E; V : B := True);
    procedure Set_String_Literal_Length           (Id : E; V : U);
    procedure Set_String_Literal_Low_Bound        (Id : E; V : N);
-   procedure Set_Subprograms_For_Type            (Id : E; V : E);
+   procedure Set_Subprograms_For_Type            (Id : E; V : L);
    procedure Set_Subps_Index                     (Id : E; V : U);
    procedure Set_Suppress_Elaboration_Warnings   (Id : E; V : B := True);
    procedure Set_Suppress_Initialization         (Id : E; V : B := True);
@@ -7911,11 +7941,13 @@
 
    function Default_Init_Cond_Procedure         (Id : E) return E;
    function Invariant_Procedure                 (Id : E) return E;
+   function Partial_Invariant_Procedure         (Id : E) return E;
    function Predicate_Function                  (Id : E) return E;
    function Predicate_Function_M                (Id : E) return E;
 
    procedure Set_Default_Init_Cond_Procedure    (Id : E; V : E);
    procedure Set_Invariant_Procedure            (Id : E; V : E);
+   procedure Set_Partial_Invariant_Procedure    (Id : E; V : E);
    procedure Set_Predicate_Function             (Id : E; V : E);
    procedure Set_Predicate_Function_M           (Id : E; V : E);
 
@@ -8374,8 +8406,8 @@
    pragma Inline (Has_Independent_Components);
    pragma Inline (Has_Inheritable_Invariants);
    pragma Inline (Has_Inherited_Default_Init_Cond);
+   pragma Inline (Has_Inherited_Invariants);
    pragma Inline (Has_Initial_Value);
-   pragma Inline (Has_Invariants);
    pragma Inline (Has_Loop_Entry_Attributes);
    pragma Inline (Has_Machine_Radix_Clause);
    pragma Inline (Has_Master_Entity);
@@ -8385,6 +8417,7 @@
    pragma Inline (Has_Non_Standard_Rep);
    pragma Inline (Has_Object_Size_Clause);
    pragma Inline (Has_Out_Or_In_Out_Parameter);
+   pragma Inline (Has_Own_Invariants);
    pragma Inline (Has_Per_Object_Constraint);
    pragma Inline (Has_Pragma_Controlled);
    pragma Inline (Has_Pragma_Elaborate_Body);
@@ -8550,6 +8583,7 @@
    pragma Inline (Is_Packed);
    pragma Inline (Is_Packed_Array_Impl_Type);
    pragma Inline (Is_Param_Block_Component_Type);
+   pragma Inline (Is_Partial_Invariant_Procedure);
    pragma Inline (Is_Potentially_Use_Visible);
    pragma Inline (Is_Predicate_Function);
    pragma Inline (Is_Predicate_Function_M);
@@ -8884,8 +8918,8 @@
    pragma Inline (Set_Has_Independent_Components);
    pragma Inline (Set_Has_Inheritable_Invariants);
    pragma Inline (Set_Has_Inherited_Default_Init_Cond);
+   pragma Inline (Set_Has_Inherited_Invariants);
    pragma Inline (Set_Has_Initial_Value);
-   pragma Inline (Set_Has_Invariants);
    pragma Inline (Set_Has_Loop_Entry_Attributes);
    pragma Inline (Set_Has_Machine_Radix_Clause);
    pragma Inline (Set_Has_Master_Entity);
@@ -8895,6 +8929,7 @@
    pragma Inline (Set_Has_Non_Standard_Rep);
    pragma Inline (Set_Has_Object_Size_Clause);
    pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
+   pragma Inline (Set_Has_Own_Invariants);
    pragma Inline (Set_Has_Per_Object_Constraint);
    pragma Inline (Set_Has_Pragma_Controlled);
    pragma Inline (Set_Has_Pragma_Elaborate_Body);
@@ -9026,6 +9061,7 @@
    pragma Inline (Set_Is_Packed);
    pragma Inline (Set_Is_Packed_Array_Impl_Type);
    pragma Inline (Set_Is_Param_Block_Component_Type);
+   pragma Inline (Set_Is_Partial_Invariant_Procedure);
    pragma Inline (Set_Is_Potentially_Use_Visible);
    pragma Inline (Set_Is_Predicate_Function);
    pragma Inline (Set_Is_Predicate_Function_M);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 237595)
+++ sem_prag.adb	(working copy)
@@ -39,6 +39,7 @@
 with Einfo;     use Einfo;
 with Elists;    use Elists;
 with Errout;    use Errout;
+with Exp_Ch7;   use Exp_Ch7;
 with Exp_Dist;  use Exp_Dist;
 with Exp_Util;  use Exp_Util;
 with Freeze;    use Freeze;
@@ -16503,8 +16504,20 @@
          when Pragma_Invariant => Invariant : declare
             Discard : Boolean;
             Typ     : Entity_Id;
-            Type_Id : Node_Id;
+            Typ_Arg : Node_Id;
 
+            CRec_Typ : Entity_Id;
+            --  The corresponding record type of Full_Typ
+
+            Full_Base : Entity_Id;
+            --  The base type of Full_Typ
+
+            Full_Typ : Entity_Id;
+            --  The full view of Typ
+
+            Priv_Typ : Entity_Id;
+            --  The partial view of Typ
+
          begin
             GNAT_Pragma;
             Check_At_Least_N_Arguments (2);
@@ -16519,14 +16532,16 @@
 
             Check_Arg_Is_Local_Name (Arg1);
 
-            Type_Id := Get_Pragma_Arg (Arg1);
-            Find_Type (Type_Id);
-            Typ := Entity (Type_Id);
+            Typ_Arg := Get_Pragma_Arg (Arg1);
+            Find_Type (Typ_Arg);
+            Typ := Entity (Typ_Arg);
 
+            --  Nothing to do of the related type is erroneous in some way
+
             if Typ = Any_Type then
                return;
 
-            --  Invariants allowed in interface types (RM 7.3.2(3/3))
+            --  AI12-0041: Invariants are allowed in interface types
 
             elsif Is_Interface (Typ) then
                null;
@@ -16536,64 +16551,86 @@
             --  a class-wide invariant can only appear on a private declaration
             --  or private extension, not a completion.
 
-            elsif Ekind_In (Typ, E_Private_Type,
-                                 E_Record_Type_With_Private,
-                                 E_Limited_Private_Type)
+            --  A [class-wide] invariant may be associated a [limited] private
+            --  type or a private extension.
+
+            elsif Ekind_In (Typ, E_Limited_Private_Type,
+                                 E_Private_Type,
+                                 E_Record_Type_With_Private)
             then
                null;
 
-            elsif In_Private_Part (Current_Scope)
-              and then Has_Private_Declaration (Typ)
+            --  A non-class-wide invariant may be associated with the full view
+            --  of a [limited] private type or a private extension.
+
+            elsif Has_Private_Declaration (Typ)
               and then not Class_Present (N)
             then
                null;
 
-            elsif In_Private_Part (Current_Scope) then
+            --  A class-wide invariant may appear on the partial view only
+
+            elsif Class_Present (N) then
                Error_Pragma_Arg
-                 ("pragma% only allowed for private type declared in "
-                  & "visible part", Arg1);
+                 ("pragma % only allowed for private type", Arg1);
+               return;
 
+            --  A regular invariant may appear on both views
+
             else
                Error_Pragma_Arg
-                 ("pragma% only allowed for private type", Arg1);
+                 ("pragma % only allowed for private type or corresponding "
+                  & "full view", Arg1);
+               return;
             end if;
 
+            --  An invariant associated with an abstract type (this includes
+            --  interfaces) must be class-wide.
+
+            if Is_Abstract_Type (Typ) and then not Class_Present (N) then
+               Error_Pragma_Arg
+                 ("pragma % not allowed for abstract type", Arg1);
+               return;
+            end if;
+
             --  A pragma that applies to a Ghost entity becomes Ghost for the
             --  purposes of legality checks and removal of ignored Ghost code.
 
             Mark_Pragma_As_Ghost (N, Typ);
 
-            --  Not allowed for abstract type in the non-class case (it is
-            --  allowed to use Invariant'Class for abstract types).
+            --  The pragma defines a type-specific invariant, the type is said
+            --  to have invariants of its "own".
 
-            if Is_Abstract_Type (Typ) and then not Class_Present (N) then
-               Error_Pragma_Arg
-                 ("pragma% not allowed for abstract type", Arg1);
+            Set_Has_Own_Invariants (Typ);
+
+            --  If the invariant is class-wide, then it can be inherited by
+            --  derived or interface implementing types. The type is said to
+            --  have "inheritable" invariants.
+
+            if Class_Present (N) then
+               Set_Has_Inheritable_Invariants (Typ);
             end if;
 
-            --  Link the pragma on to the rep item chain, for processing when
+            Get_Views (Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
+
+            --  Propagate invariant-related attributes to all views of the type
+            --  and any additional types that may have been created.
+
+            Propagate_Invariant_Attributes (Priv_Typ,  From_Typ => Typ);
+            Propagate_Invariant_Attributes (Full_Typ,  From_Typ => Typ);
+            Propagate_Invariant_Attributes (Full_Base, From_Typ => Typ);
+            Propagate_Invariant_Attributes (CRec_Typ,  From_Typ => Typ);
+
+            --  Chain the pragma on to the rep item chain, for processing when
             --  the type is frozen.
 
             Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
 
-            --  Note that the type has at least one invariant, and also that
-            --  it has inheritable invariants if we have Invariant'Class
-            --  or Type_Invariant'Class. Build the corresponding invariant
-            --  procedure declaration, so that calls to it can be generated
-            --  before the body is built (e.g. within an expression function).
+            --  Create the declaration of the invariant procedure which will
+            --  verify the invariant at run-time. Note that interfaces do not
+            --  carry such a declaration.
 
-            --  Interface types have no invariant procedure; their invariants
-            --  are propagated to the build invariant procedure of all the
-            --  types covering the interface type.
-
-            if not Is_Interface (Typ) then
-               Insert_After_And_Analyze
-                 (N, Build_Invariant_Procedure_Declaration (Typ));
-            end if;
-
-            if Class_Present (N) then
-               Set_Has_Inheritable_Invariants (Typ);
-            end if;
+            Build_Invariant_Procedure_Declaration (Typ);
          end Invariant;
 
          ----------------
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 237595)
+++ freeze.adb	(working copy)
@@ -2290,6 +2290,25 @@
                Set_Has_Unchecked_Union (Arr);
             end if;
 
+            --  The array type requires its own invariant procedure in order to
+            --  verify the component invariant over all elements.
+
+            if Has_Invariants (Component_Type (Arr))
+              or else
+                (Is_Access_Type (Component_Type (Arr))
+                  and then Has_Invariants
+                             (Designated_Type (Component_Type (Arr))))
+            then
+               Set_Has_Own_Invariants (Arr);
+
+               --  The array type is an implementation base type. Propagate the
+               --  same property to the first subtype.
+
+               if Is_Itype (Arr) then
+                  Set_Has_Own_Invariants (First_Subtype (Arr));
+               end if;
+            end if;
+
             --  Warn for pragma Pack overriding foreign convention
 
             if Has_Foreign_Convention (Ctyp)
@@ -4165,7 +4184,8 @@
                Freeze_And_Append (Corresponding_Remote_Type (Rec), N, Result);
             end if;
 
-            --  Check for controlled components and unchecked unions.
+            --  Check for controlled components, unchecked unions, and type
+            --  invariants.
 
             Comp := First_Component (Rec);
             while Present (Comp) loop
@@ -4194,6 +4214,22 @@
                   Set_Has_Unchecked_Union (Rec);
                end if;
 
+               --  The record type requires its own invariant procedure in
+               --  order to verify the invariant of each individual component.
+               --  Do not consider internal components such as _parent because
+               --  parent class-wide invariants are always inherited.
+
+               if Comes_From_Source (Comp)
+                 and then
+                   (Has_Invariants (Etype (Comp))
+                     or else
+                       (Is_Access_Type (Etype (Comp))
+                         and then Has_Invariants
+                                    (Designated_Type (Etype (Comp)))))
+               then
+                  Set_Has_Own_Invariants (Rec);
+               end if;
+
                --  Scan component declaration for likely misuses of current
                --  instance, either in a constraint or a default expression.
 
@@ -5224,8 +5260,7 @@
               and then not Is_Tagged_Type (E)
             then
                Error_Msg_NE
-                 ("Type_Invariant''Class cannot be specified for &",
-                  Prag, E);
+                 ("Type_Invariant''Class cannot be specified for &", Prag, E);
                Error_Msg_N
                  ("\can only be specified for a tagged type", Prag);
             end if;
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 237595)
+++ sem_util.adb	(working copy)
@@ -8622,6 +8622,76 @@
       return Empty;
    end Get_User_Defined_Eq;
 
+   ---------------
+   -- Get_Views --
+   ---------------
+
+   procedure Get_Views
+     (Typ       : Entity_Id;
+      Priv_Typ  : out Entity_Id;
+      Full_Typ  : out Entity_Id;
+      Full_Base : out Entity_Id;
+      CRec_Typ  : out Entity_Id)
+   is
+   begin
+      --  Assume that none of the views can be recovered
+
+      Priv_Typ  := Empty;
+      Full_Typ  := Empty;
+      Full_Base := Empty;
+      CRec_Typ  := Empty;
+
+      --  The input type is private
+
+      if Is_Private_Type (Typ) then
+         Priv_Typ := Typ;
+         Full_Typ := Full_View (Priv_Typ);
+
+         if Present (Full_Typ) then
+            Full_Base := Base_Type (Full_Typ);
+
+            if Ekind_In (Full_Typ, E_Protected_Type, E_Task_Type) then
+               CRec_Typ := Corresponding_Record_Type (Full_Typ);
+            end if;
+         end if;
+
+      --  The input type is the corresponding record type of a protected or a
+      --  task type.
+
+      elsif Ekind (Typ) = E_Record_Type
+        and then Is_Concurrent_Record_Type (Typ)
+      then
+         CRec_Typ  := Typ;
+         Full_Typ  := Corresponding_Concurrent_Type (CRec_Typ);
+         Full_Base := Base_Type (Full_Typ);
+         Priv_Typ  := Incomplete_Or_Partial_View (Full_Typ);
+
+      --  Otherwise the input type could be the full view of a private type
+
+      else
+         Full_Typ  := Typ;
+         Full_Base := Base_Type (Full_Typ);
+
+         if Ekind_In (Full_Typ, E_Protected_Type, E_Task_Type) then
+            CRec_Typ := Corresponding_Record_Type (Full_Typ);
+         end if;
+
+         --  The type is the full view of a private type, obtain the partial
+         --  view.
+
+         if Has_Private_Declaration (Full_Typ)
+           and then not Is_Private_Type (Full_Typ)
+         then
+            Priv_Typ := Incomplete_Or_Partial_View (Full_Typ);
+
+            --  The full view of a private type should always have a partial
+            --  view.
+
+            pragma Assert (Present (Priv_Typ));
+         end if;
+      end if;
+   end Get_Views;
+
    -----------------------
    -- Has_Access_Values --
    -----------------------
@@ -10988,20 +11058,31 @@
          while Present (Decl) loop
             Match := Empty;
 
+            --  The partial view of a Taft-amendment type is an incomplete
+            --  type.
+
             if Taft then
                if Nkind (Decl) = N_Incomplete_Type_Declaration then
                   Match := Defining_Identifier (Decl);
                end if;
 
-            else
-               if Nkind_In (Decl, N_Private_Extension_Declaration,
+            --  Otherwise look for a private type whose full view matches the
+            --  input type. Note that this checks full_type_declaration nodes
+            --  to account for derivations from a private type where the type
+            --  declaration hold the partial view and the full view is an
+            --  itype.
+
+            elsif Nkind_In (Decl, N_Full_Type_Declaration,
+                                  N_Private_Extension_Declaration,
                                   N_Private_Type_Declaration)
-               then
-                  Match := Defining_Identifier (Decl);
-               end if;
+            then
+               Match := Defining_Identifier (Decl);
             end if;
 
+            --  Guard against unanalyzed entities
+
             if Present (Match)
+              and then Is_Type (Match)
               and then Present (Full_View (Match))
               and then Full_View (Match) = Id
             then
@@ -11040,7 +11121,9 @@
          Pkg_Decl : Node_Id := Pkg;
 
       begin
-         if Present (Pkg) and then Ekind (Pkg) = E_Package then
+         if Present (Pkg)
+           and then Ekind_In (Pkg, E_Generic_Package, E_Package)
+         then
             while Nkind (Pkg_Decl) /= N_Package_Specification loop
                Pkg_Decl := Parent (Pkg_Decl);
             end loop;
@@ -18519,13 +18602,71 @@
       Set_Sloc (Endl, Loc);
    end Process_End_Label;
 
+   ------------------------------------
+   -- Propagate_Invariant_Attributes --
+   ------------------------------------
+
+   procedure Propagate_Invariant_Attributes
+     (Typ      : Entity_Id;
+      From_Typ : Entity_Id)
+   is
+      Full_IP : Entity_Id;
+      Part_IP : Entity_Id;
+
+   begin
+      if Present (Typ) and then Present (From_Typ) then
+         pragma Assert (Is_Type (Typ) and then Is_Type (From_Typ));
+
+         --  Nothing to do if both the source and the destination denote the
+         --  same type.
+
+         if From_Typ = Typ then
+            return;
+         end if;
+
+         Full_IP := Invariant_Procedure (From_Typ);
+         Part_IP := Partial_Invariant_Procedure (From_Typ);
+
+         --  The setting of the attributes is intentionally conservative. This
+         --  prevents accidental clobbering of enabled attributes.
+
+         if Has_Inheritable_Invariants (From_Typ)
+           and then not Has_Inheritable_Invariants (Typ)
+         then
+            Set_Has_Inheritable_Invariants (Typ, True);
+         end if;
+
+         if Has_Inherited_Invariants (From_Typ)
+           and then not Has_Inherited_Invariants (Typ)
+         then
+            Set_Has_Inherited_Invariants (Typ, True);
+         end if;
+
+         if Has_Own_Invariants (From_Typ)
+           and then not Has_Own_Invariants (Typ)
+         then
+            Set_Has_Own_Invariants (Typ, True);
+         end if;
+
+         if Present (Full_IP) and then No (Invariant_Procedure (Typ)) then
+            Set_Invariant_Procedure (Typ, Full_IP);
+         end if;
+
+         if Present (Part_IP) and then No (Partial_Invariant_Procedure (Typ))
+         then
+            Set_Partial_Invariant_Procedure (Typ, Part_IP);
+         end if;
+      end if;
+   end Propagate_Invariant_Attributes;
+
    --------------------------------
    -- Propagate_Concurrent_Flags --
    --------------------------------
 
    procedure Propagate_Concurrent_Flags
      (Typ      : Entity_Id;
-      Comp_Typ : Entity_Id) is
+      Comp_Typ : Entity_Id)
+   is
    begin
       if Has_Task (Comp_Typ) then
          Set_Has_Task (Typ);
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 237595)
+++ sem_util.ads	(working copy)
@@ -1005,6 +1005,20 @@
    --  For a type entity, return the entity of the primitive equality function
    --  for the type if it exists, otherwise return Empty.
 
+   procedure Get_Views
+     (Typ       : Entity_Id;
+      Priv_Typ  : out Entity_Id;
+      Full_Typ  : out Entity_Id;
+      Full_Base : out Entity_Id;
+      CRec_Typ  : out Entity_Id);
+   --  Obtain the partial and full view of type Typ and in addition any extra
+   --  types the full view may have. The return entities are as follows:
+   --
+   --    Priv_Typ  - the partial view (a private type)
+   --    Full_Typ  - the full view
+   --    Full_Base - the base type of the full view
+   --    CRec_Typ  - the corresponding record type of the full view
+
    function Has_Access_Values (T : Entity_Id) return Boolean;
    --  Returns true if type or subtype T is an access type, or has a component
    --  (at any recursive level) that is an access type. This is a conservative
@@ -2022,6 +2036,12 @@
    --  parameter Ent gives the entity to which the End_Label refers,
    --  and to which cross-references are to be generated.
 
+   procedure Propagate_Invariant_Attributes
+     (Typ      : Entity_Id;
+      From_Typ : Entity_Id);
+   --  Inherit all invariant-related attributes form type From_Typ. Typ is the
+   --  destination type.
+
    procedure Propagate_Concurrent_Flags
      (Typ      : Entity_Id;
       Comp_Typ : Entity_Id);
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 237595)
+++ sem_res.adb	(working copy)
@@ -4223,14 +4223,19 @@
                then
                   Error_Msg_NE ("actual for& must be a variable", A, F);
 
-                  if Is_Subprogram (Current_Scope)
-                    and then
-                      (Is_Invariant_Procedure (Current_Scope)
-                        or else Is_Predicate_Function (Current_Scope))
-                  then
-                     Error_Msg_N
-                       ("function used in predicate cannot "
-                        & "modify its argument", F);
+                  if Is_Subprogram (Current_Scope) then
+                     if Is_Invariant_Procedure (Current_Scope)
+                       or else Is_Partial_Invariant_Procedure (Current_Scope)
+                     then
+                        Error_Msg_N
+                          ("function used in invariant cannot modify its "
+                           & "argument", F);
+
+                     elsif Is_Predicate_Function (Current_Scope) then
+                        Error_Msg_N
+                          ("function used in predicate cannot modify its "
+                           & "argument", F);
+                     end if;
                   end if;
                end if;
 
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 237595)
+++ sem_ch6.adb	(working copy)
@@ -4428,6 +4428,34 @@
    --  both subprogram bodies and subprogram declarations (specs).
 
    function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id is
+      function Is_Invariant_Procedure_Or_Body (E : Entity_Id) return Boolean;
+      --  Determine whether entity E denotes the spec or body of an invariant
+      --  procedure.
+
+      ------------------------------------
+      -- Is_Invariant_Procedure_Or_Body --
+      ------------------------------------
+
+      function Is_Invariant_Procedure_Or_Body (E : Entity_Id) return Boolean is
+         Decl : constant Node_Id := Unit_Declaration_Node (E);
+         Spec : Entity_Id;
+
+      begin
+         if Nkind (Decl) = N_Subprogram_Body then
+            Spec := Corresponding_Spec (Decl);
+         else
+            Spec := E;
+         end if;
+
+         return
+           Present (Spec)
+             and then Ekind (Spec) = E_Procedure
+             and then (Is_Partial_Invariant_Procedure (Spec)
+                        or else Is_Invariant_Procedure (Spec));
+      end Is_Invariant_Procedure_Or_Body;
+
+      --  Local variables
+
       Designator : constant Entity_Id := Defining_Entity (N);
       Formals    : constant List_Id   := Parameter_Specifications (N);
 
@@ -4487,7 +4515,27 @@
          --  Same processing for an access parameter whose designated type is
          --  derived from a synchronized interface.
 
-         if Ada_Version >= Ada_2005 then
+         --  This modification is not done for invariant procedures because
+         --  the corresponding record may not necessarely be visible when the
+         --  concurrent type acts as the full view of a private type.
+
+         --    package Pack is
+         --       type Prot is private with Type_Invariant => ...;
+         --       procedure ConcInvariant (Obj : Prot);
+         --    private
+         --       protected type Prot is ...;
+         --       type Concurrent_Record_Prot is record ...;
+         --       procedure ConcInvariant (Obj : Prot) is
+         --          ...
+         --       end ConcInvariant;
+         --    end Pack;
+
+         --  In the example above, both the spec and body of the invariant
+         --  procedure must utilize the private type as the controlling type.
+
+         if Ada_Version >= Ada_2005
+           and then not Is_Invariant_Procedure_Or_Body (Designator)
+         then
             declare
                Formal     : Entity_Id;
                Formal_Typ : Entity_Id;
Index: atree.adb
===================================================================
--- atree.adb	(revision 237595)
+++ atree.adb	(working copy)
@@ -3317,6 +3317,17 @@
          end if;
       end Elist26;
 
+      function Elist29 (N : Node_Id) return Elist_Id is
+         pragma Assert (Nkind (N) in N_Entity);
+         Value : constant Union_Id := Nodes.Table (N + 4).Field11;
+      begin
+         if Value = 0 then
+            return No_Elist;
+         else
+            return Elist_Id (Value);
+         end if;
+      end Elist29;
+
       function Elist36 (N : Node_Id) return Elist_Id is
          pragma Assert (Nkind (N) in N_Entity);
          Value : constant Union_Id := Nodes.Table (N + 6).Field6;
@@ -6109,6 +6120,12 @@
          Nodes.Table (N + 4).Field8 := Union_Id (Val);
       end Set_Elist26;
 
+      procedure Set_Elist29 (N : Node_Id; Val : Elist_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 4).Field11 := Union_Id (Val);
+      end Set_Elist29;
+
       procedure Set_Elist36 (N : Node_Id; Val : Elist_Id) is
       begin
          pragma Assert (Nkind (N) in N_Entity);
Index: atree.ads
===================================================================
--- atree.ads	(revision 237595)
+++ atree.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -1473,6 +1473,9 @@
       function Elist26 (N : Node_Id) return Elist_Id;
       pragma Inline (Elist26);
 
+      function Elist29 (N : Node_Id) return Elist_Id;
+      pragma Inline (Elist29);
+
       function Elist36 (N : Node_Id) return Elist_Id;
       pragma Inline (Elist36);
 
@@ -2836,6 +2839,9 @@
       procedure Set_Elist26 (N : Node_Id; Val : Elist_Id);
       pragma Inline (Set_Elist26);
 
+      procedure Set_Elist29 (N : Node_Id; Val : Elist_Id);
+      pragma Inline (Set_Elist29);
+
       procedure Set_Elist36 (N : Node_Id; Val : Elist_Id);
       pragma Inline (Set_Elist36);
 
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 237595)
+++ sem_ch13.adb	(working copy)
@@ -62,7 +62,6 @@
 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;
@@ -8080,577 +8079,7 @@
       return Prag;
    end Build_Export_Import_Pragma;
 
-   -------------------------------------------
-   -- Build_Invariant_Procedure_Declaration --
-   -------------------------------------------
-
-   function Build_Invariant_Procedure_Declaration
-     (Typ : Entity_Id) return Node_Id
-   is
-      Loc    : constant Source_Ptr := Sloc (Typ);
-      Decl   : Node_Id;
-      Obj_Id : Entity_Id;
-      SId    : Entity_Id;
-
-      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-   begin
-      --  Check for duplicate definitions
-
-      if Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)) then
-         return Empty;
-      end if;
-
-      --  The related type may be subject to pragma Ghost. Set the mode now to
-      --  ensure that the invariant procedure is properly marked as Ghost.
-
-      Set_Ghost_Mode_From_Entity (Typ);
-
-      SId :=
-        Make_Defining_Identifier (Loc,
-          Chars => New_External_Name (Chars (Typ), "Invariant"));
-      Set_Has_Invariants (Typ);
-      Set_Ekind (SId, E_Procedure);
-      Set_Etype (SId, Standard_Void_Type);
-      Set_Is_Invariant_Procedure (SId);
-      Set_Invariant_Procedure (Typ, SId);
-
-      --  Source Coverage Obligations might be attached to the invariant
-      --  expression this procedure evaluates, and we need debug info to be
-      --  able to assess the coverage achieved by evaluations.
-
-      if Opt.Generate_SCO then
-         Set_Needs_Debug_Info (SId);
-      end if;
-
-      --  Mark the invariant procedure explicitly as Ghost because it does not
-      --  come from source.
-
-      if Ghost_Mode > None then
-         Set_Is_Ghost_Entity (SId);
-      end if;
-
-      Obj_Id := Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
-      Set_Etype (Obj_Id, Typ);
-
-      Decl :=
-        Make_Subprogram_Declaration (Loc,
-          Make_Procedure_Specification (Loc,
-            Defining_Unit_Name       => SId,
-            Parameter_Specifications => New_List (
-              Make_Parameter_Specification (Loc,
-                Defining_Identifier => Obj_Id,
-                Parameter_Type      => New_Occurrence_Of (Typ, Loc)))));
-
-      Ghost_Mode := Save_Ghost_Mode;
-
-      return Decl;
-   end Build_Invariant_Procedure_Declaration;
-
    -------------------------------
-   -- 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; N : Node_Id) is
-      procedure Add_Invariants
-        (T       : Entity_Id;
-         Obj_Id  : Entity_Id;
-         Stmts   : in out List_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.
-
-      --------------------
-      -- Add_Invariants --
-      --------------------
-
-      procedure Add_Invariants
-        (T       : Entity_Id;
-         Obj_Id  : Entity_Id;
-         Stmts   : in out List_Id;
-         Inherit : Boolean)
-      is
-         procedure Add_Invariant (Prag : Node_Id);
-         --  Create a runtime check to verify the exression of invariant pragma
-         --  Prag. All generated code is added to list Stmts.
-
-         -------------------
-         -- Add_Invariant --
-         -------------------
-
-         procedure Add_Invariant (Prag : Node_Id) is
-            procedure Replace_Type_Reference (N : Node_Id);
-            --  Replace a single occurrence N of the subtype name with a
-            --  reference to the formal of the predicate function. N can be an
-            --  identifier referencing the subtype, or a selected component,
-            --  representing an appropriately qualified occurrence of the
-            --  subtype name.
-
-            procedure Replace_Type_References is
-              new Replace_Type_References_Generic (Replace_Type_Reference);
-            --  Traverse an expression replacing all occurrences of the subtype
-            --  name with appropriate references to the formal of the predicate
-            --  function. Note that we must ensure that the type and entity
-            --  information is properly set in the replacement node, since we
-            --  will do a Preanalyze call of this expression without proper
-            --  visibility of the procedure argument.
-
-            ----------------------------
-            -- Replace_Type_Reference --
-            ----------------------------
-
-            --  Note: See comments in Add_Predicates.Replace_Type_Reference
-            --  regarding handling of Sloc and Comes_From_Source.
-
-            procedure Replace_Type_Reference (N : Node_Id) is
-               Nloc : constant Source_Ptr := Sloc (N);
-
-            begin
-               --  Add semantic information to node to be rewritten, for ASIS
-               --  navigation needs.
-
-               if Nkind (N) = N_Identifier then
-                  Set_Entity (N, T);
-                  Set_Etype  (N, T);
-
-               elsif Nkind (N) = N_Selected_Component then
-                  Analyze (Prefix (N));
-                  Set_Entity (Selector_Name (N), T);
-                  Set_Etype  (Selector_Name (N), T);
-               end if;
-
-               --  Invariant'Class, replace with T'Class (obj)
-
-               if Class_Present (Prag) then
-
-                  --  In ASIS mode, an inherited item is already analyzed,
-                  --  and the replacement has been done, so do not repeat
-                  --  the transformation to prevent a malformed tree.
-
-                  if ASIS_Mode
-                    and then Nkind (Parent (N)) = N_Attribute_Reference
-                    and then Attribute_Name (Parent (N)) = Name_Class
-                  then
-                     null;
-
-                  else
-                     Rewrite (N,
-                       Make_Type_Conversion (Nloc,
-                         Subtype_Mark =>
-                           Make_Attribute_Reference (Nloc,
-                             Prefix         => New_Occurrence_Of (T, Nloc),
-                             Attribute_Name => Name_Class),
-                         Expression   =>
-                           Make_Identifier (Nloc, Chars (Obj_Id))));
-
-                     Set_Entity (Expression (N), Obj_Id);
-                     Set_Etype  (Expression (N), Typ);
-                  end if;
-
-               --  Invariant, replace with obj
-
-               else
-                  Rewrite (N, Make_Identifier (Nloc, Chars (Obj_Id)));
-                  Set_Entity (N, Obj_Id);
-                  Set_Etype  (N, Typ);
-               end if;
-
-               Set_Comes_From_Source (N, True);
-            end Replace_Type_Reference;
-
-            --  Local variables
-
-            Asp   : constant Node_Id    := Corresponding_Aspect (Prag);
-            Nam   : constant Name_Id    := Original_Aspect_Pragma_Name (Prag);
-            Ploc  : constant Source_Ptr := Sloc (Prag);
-            Arg1  : Node_Id;
-            Arg2  : Node_Id;
-            Arg3  : Node_Id;
-            Assoc : List_Id;
-            Expr  : Node_Id;
-            Str   : String_Id;
-
-         --  Start of processing for Add_Invariant
-
-         begin
-            --  Extract the arguments of the invariant pragma
-
-            Arg1 := First (Pragma_Argument_Associations (Prag));
-            Arg2 := Next (Arg1);
-            Arg3 := Next (Arg2);
-
-            Arg1 := Get_Pragma_Arg (Arg1);
-            Arg2 := Get_Pragma_Arg (Arg2);
-
-            --  The caller requests processing of all Invariant'Class pragmas,
-            --  but the current pragma does not fall in this category. Return
-            --  as there is nothing left to do.
-
-            if Inherit then
-               if not Class_Present (Prag) then
-                  return;
-               end if;
-
-            --  Otherwise the pragma must apply to the current type
-
-            elsif Entity (Arg1) /= T then
-               return;
-            end if;
-
-            Expr := New_Copy_Tree (Arg2);
-
-            --  Replace all occurrences of the type's name with references to
-            --  the formal parameter of the invariant procedure.
-
-            Replace_Type_References (Expr, T);
-
-            --  If the invariant pragma comes from an aspect, replace the saved
-            --  expression because we need the subtype references replaced for
-            --  the calls to Preanalyze_Spec_Expression in Check_Aspect_At_xxx
-            --  routines. This is not done for interited class-wide invariants
-            --  because the original pragma of the parent type must remain
-            --  unchanged.
-
-            if not Inherit and then Present (Asp) then
-               Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
-            end if;
-
-            --  Preanalyze the invariant expression to capture the visibility
-            --  of the proper package part. In general the expression is not
-            --  fully analyzed until the body of the invariant procedure is
-            --  analyzed at the end of the private part, but that yields the
-            --  wrong visibility.
-
-            --  Historical note: we used to set N as the parent, but a package
-            --  specification as the parent of an expression is bizarre.
-
-            Set_Parent (Expr, Parent (Arg2));
-            Preanalyze_Assert_Expression (Expr, Any_Boolean);
-
-            --  Both modifications performed below are not done for inherited
-            --  class-wide invariants because the origial aspect/pragma of the
-            --  parent type must remain unchanged.
-
-            if not Inherit then
-
-               --  A class-wide invariant may be inherited in a separate unit,
-               --  where the corresponding expression cannot be resolved by
-               --  visibility, because it refers to a local function. Propagate
-               --  semantic information to the original representation item, to
-               --  be used when an invariant procedure for a derived type is
-               --  constructed.
-
-               --  ??? Unclear how to handle class-wide invariants that are not
-               --  function calls.
-
-               if Class_Present (Prag)
-                 and then Nkind (Expr) = N_Function_Call
-                 and then Nkind (Arg2) = N_Indexed_Component
-               then
-                  Rewrite (Arg2,
-                    Make_Function_Call (Ploc,
-                      Name                   =>
-                        New_Occurrence_Of (Entity (Name (Expr)), Ploc),
-                      Parameter_Associations => Expressions (Arg2)));
-               end if;
-
-               --  In ASIS mode, even if assertions are not enabled, we must
-               --  analyze the original expression in the aspect specification
-               --  because it is part of the original tree.
-
-               if ASIS_Mode and then Present (Asp) then
-                  declare
-                     Asp_Expr : constant Node_Id := Expression (Asp);
-
-                  begin
-                     Replace_Type_References (Asp_Expr, T);
-                     Preanalyze_Assert_Expression (Asp_Expr, Any_Boolean);
-                  end;
-               end if;
-            end if;
-
-            --  An ignored invariant must not generate a runtime check. Add a
-            --  null statement to ensure that the invariant procedure does get
-            --  a completing body.
-
-            if No (Stmts) then
-               Stmts := Empty_List;
-            end if;
-
-            if Is_Ignored (Prag) then
-               Append_To (Stmts, Make_Null_Statement (Ploc));
-
-            --  Otherwise the invariant is checked. Build a Check pragma to
-            --  verify the expression at runtime.
-
-            else
-               Assoc := New_List (
-                 Make_Pragma_Argument_Association (Ploc,
-                   Expression => Make_Identifier (Ploc, Nam)),
-                 Make_Pragma_Argument_Association (Ploc,
-                   Expression => Expr));
-
-               --  Handle the String argument (if any)
-
-               if Present (Arg3) then
-                  Str := Strval (Get_Pragma_Arg (Arg3));
-
-                  --  When inheriting an invariant, modify the message from
-                  --  "failed invariant" to "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 (Ploc,
-                      Expression => Make_String_Literal (Ploc, Str)));
-               end if;
-
-               --  Generate:
-               --    pragma Check (Nam, Expr, Str);
-
-               Append_To (Stmts,
-                 Make_Pragma (Ploc,
-                   Pragma_Identifier            =>
-                     Make_Identifier (Ploc, Name_Check),
-                   Pragma_Argument_Associations => Assoc));
-            end if;
-
-            --  Output an info message when inheriting an invariant and the
-            --  listing option is enabled.
-
-            if Inherit and Opt.List_Inherited_Aspects then
-               Error_Msg_Sloc := Sloc (Prag);
-               Error_Msg_N
-                 ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
-            end if;
-         end Add_Invariant;
-
-         --  Local variables
-
-         Ritem : Node_Id;
-
-      --  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
-               Add_Invariant (Ritem);
-            end if;
-
-            Next_Rep_Item (Ritem);
-         end loop;
-      end Add_Invariants;
-
-      --  Local variables
-
-      Loc        : constant Source_Ptr := Sloc (Typ);
-      Priv_Decls : constant List_Id    := Private_Declarations (N);
-      Vis_Decls  : constant List_Id    := Visible_Declarations (N);
-
-      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-      PBody : Node_Id;
-      PDecl : Node_Id;
-      SId   : Entity_Id;
-      Spec  : Node_Id;
-      Stmts : List_Id;
-
-      Obj_Id : Node_Id;
-      --  The entity of the formal for the procedure
-
-   --  Start of processing for Build_Invariant_Procedure
-
-   begin
-      --  The related type may be subject to pragma Ghost. Set the mode now to
-      --  ensure that the invariant procedure is properly marked as Ghost.
-
-      Set_Ghost_Mode_From_Entity (Typ);
-
-      Stmts := No_List;
-      PDecl := Empty;
-      PBody := Empty;
-      SId   := Empty;
-
-      --  If the aspect specification exists for some view of the type, the
-      --  declaration for the procedure has been created.
-
-      if Has_Invariants (Typ) then
-         SId := Invariant_Procedure (Typ);
-      end if;
-
-      --  If the body is already present, nothing to do. This will occur when
-      --  the type is already frozen, which is the case when the invariant
-      --  appears in a private part, and the freezing takes place before the
-      --  final pass over full declarations.
-
-      --  See Exp_Ch3.Insert_Component_Invariant_Checks for details.
-
-      if Present (SId) then
-         PDecl := Unit_Declaration_Node (SId);
-
-         if Present (PDecl)
-           and then Nkind (PDecl) = N_Subprogram_Declaration
-           and then Present (Corresponding_Body (PDecl))
-         then
-            Ghost_Mode := Save_Ghost_Mode;
-            return;
-         end if;
-
-      else
-         PDecl := Build_Invariant_Procedure_Declaration (Typ);
-      end if;
-
-      --  Recover formal of procedure, for use in the calls to invariant
-      --  functions (including inherited ones).
-
-      Obj_Id :=
-        Defining_Identifier
-          (First (Parameter_Specifications (Specification (PDecl))));
-
-      --  Add invariants for the current type
-
-      Add_Invariants
-        (T       => Typ,
-         Obj_Id  => Obj_Id,
-         Stmts   => Stmts,
-         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
-              (T       => Current_Typ,
-               Obj_Id  => Obj_Id,
-               Stmts   => Stmts,
-               Inherit => True);
-         end loop;
-      end;
-
-      --  Add invariants of progenitors
-
-      if Is_Tagged_Type (Typ) and then not Is_Interface (Typ) then
-         declare
-            Ifaces_List : Elist_Id;
-            AI          : Elmt_Id;
-            Iface       : Entity_Id;
-
-         begin
-            Collect_Interfaces (Typ, Ifaces_List);
-
-            AI := First_Elmt (Ifaces_List);
-            while Present (AI) loop
-               Iface := Node (AI);
-
-               if not Is_Ancestor (Iface, Typ, Use_Full_View => True) then
-                  Add_Invariants
-                    (T       => Iface,
-                     Obj_Id  => Obj_Id,
-                     Stmts   => Stmts,
-                     Inherit => True);
-               end if;
-
-               Next_Elmt (AI);
-            end loop;
-         end;
-      end if;
-
-      --  Build the procedure if we generated at least one Check pragma
-
-      if Stmts /= No_List then
-         Spec := Copy_Separate_Tree (Specification (PDecl));
-
-         PBody :=
-           Make_Subprogram_Body (Loc,
-             Specification              => Spec,
-             Declarations               => Empty_List,
-             Handled_Statement_Sequence =>
-               Make_Handled_Sequence_Of_Statements (Loc,
-                 Statements => Stmts));
-
-         --  The processing of an invariant pragma immediately generates the
-         --  invariant procedure spec, inserts it into the tree, and analyzes
-         --  it. If the spec has not been analyzed, then the invariant pragma
-         --  is being inherited and requires manual insertion and analysis.
-
-         if not Analyzed (PDecl) then
-            Append_To (Vis_Decls, PDecl);
-            Analyze (PDecl);
-         end if;
-
-         --  The invariant procedure body is inserted at the end of the private
-         --  declarations.
-
-         if Present (Priv_Decls) then
-            Append_To (Priv_Decls, PBody);
-
-            --  If the invariant appears on the full view of a private type,
-            --  then the analysis of the private part is already completed.
-            --  Manually analyze the new body in this case, otherwise wait
-            --  for the analysis of the private declarations to process the
-            --  body.
-
-            if In_Private_Part (Current_Scope) then
-               Analyze (PBody);
-            end if;
-
-         --  Otherwise there are no private declarations. This is either an
-         --  error or the related type is a private extension, in which case
-         --  it does not need a completion in a private part. Insert the body
-         --  at the end of the visible declarations and analyze immediately
-         --  because the related type is about to be frozen.
-
-         else
-            Append_To (Vis_Decls, PBody);
-            Analyze (PBody);
-         end if;
-      end if;
-
-      Ghost_Mode := Save_Ghost_Mode;
-   end Build_Invariant_Procedure;
-
-   -------------------------------
    -- Build_Predicate_Functions --
    -------------------------------
 
@@ -11159,9 +10588,7 @@
          end if;
       end Hide_Non_Overridden_Subprograms;
 
-      ---------------------
-      -- Local variables --
-      ---------------------
+      --  Local variables
 
       E : constant Entity_Id := Entity (N);
 
@@ -11324,14 +10751,14 @@
 
       Inside_Freezing_Actions := Inside_Freezing_Actions - 1;
 
-      --  If we have a type with predicates, build predicate function. This
-      --  is not needed in the generic case, and is not needed within TSS
-      --  subprograms and other predefined primitives.
+      --  If we have a type with predicates, build predicate function. This is
+      --  not needed in the generic case, nor within TSS subprograms and other
+      --  predefined primitives.
 
-      if Non_Generic_Case
-        and then Is_Type (E)
-        and then Has_Predicates (E)
+      if Is_Type (E)
+        and then Non_Generic_Case
         and then not Within_Internal_Subprogram
+        and then Has_Predicates (E)
       then
          Build_Predicate_Functions (E, N);
       end if;
@@ -11830,30 +11257,6 @@
          Set_Discard_Names (Typ);
       end if;
 
-      --  Invariants
-
-      if not Has_Rep_Item (Typ, Name_Invariant, False)
-        and then Has_Rep_Item (Typ, Name_Invariant)
-        and then Is_Pragma_Or_Corr_Pragma_Present_In_Rep_Item
-                   (Get_Rep_Item (Typ, Name_Invariant))
-      then
-         Set_Has_Invariants (Typ);
-
-         if Class_Present (Get_Rep_Item (Typ, Name_Invariant)) then
-            Set_Has_Inheritable_Invariants (Typ);
-         end if;
-
-      --  If we have a subtype with invariants, whose base type does not have
-      --  invariants, copy these invariants to the base type. This happens for
-      --  the case of implicit base types created for scalar and array types.
-
-      elsif Has_Invariants (Typ)
-        and then not Has_Invariants (Base_Type (Typ))
-      then
-         Set_Has_Invariants (Base_Type (Typ));
-         Set_Invariant_Procedure (Base_Type (Typ), Invariant_Procedure (Typ));
-      end if;
-
       --  Volatile
 
       if not Has_Rep_Item (Typ, Name_Volatile, False)
@@ -12636,7 +12039,7 @@
       if Has_Discriminants (E) then
          Push_Scope (E);
 
-         --  Make discriminants visible for type declarations and protected
+         --  Make the discriminants visible for type declarations and protected
          --  type declarations, not for subtype declarations (RM 13.1.1 (12/3))
 
          if Nkind (Parent (E)) /= N_Subtype_Declaration then
@@ -12891,18 +12294,15 @@
    procedure Replace_Type_References_Generic (N : Node_Id; T : Entity_Id) is
       TName : constant Name_Id := Chars (T);
 
-      function Replace_Node (N : Node_Id) return Traverse_Result;
+      function Replace_Type_Ref (N : Node_Id) return Traverse_Result;
       --  Processes a single node in the traversal procedure below, checking
       --  if node N should be replaced, and if so, doing the replacement.
 
-      procedure Replace_Type_Refs is new Traverse_Proc (Replace_Node);
-      --  This instantiation provides the body of Replace_Type_References
+      ----------------------
+      -- Replace_Type_Ref --
+      ----------------------
 
-      ------------------
-      -- Replace_Node --
-      ------------------
-
-      function Replace_Node (N : Node_Id) return Traverse_Result is
+      function Replace_Type_Ref (N : Node_Id) return Traverse_Result is
          S : Entity_Id;
          P : Node_Id;
 
@@ -12911,10 +12311,10 @@
 
          if Nkind (N) = N_Identifier then
 
-            --  If not the type name, check whether it is a reference to
-            --  some other type, which must be frozen before the predicate
-            --  function is analyzed, i.e. before the freeze node of the
-            --  type to which the predicate applies.
+            --  If not the type name, check whether it is a reference to some
+            --  other type, which must be frozen before the predicate function
+            --  is analyzed, i.e. before the freeze node of the type to which
+            --  the predicate applies.
 
             if Chars (N) /= TName then
                if Present (Current_Entity (N))
@@ -12932,13 +12332,13 @@
                return Skip;
             end if;
 
-         --  Case of selected component (which is what a qualification
-         --  looks like in the unanalyzed tree, which is what we have.
+         --  Case of selected component (which is what a qualification looks
+         --  like in the unanalyzed tree, which is what we have.
 
          elsif Nkind (N) = N_Selected_Component then
 
-            --  If selector name is not our type, keeping going (we might
-            --  still have an occurrence of the type in the prefix).
+            --  If selector name is not our type, keeping going (we might still
+            --  have an occurrence of the type in the prefix).
 
             if Nkind (Selector_Name (N)) /= N_Identifier
               or else Chars (Selector_Name (N)) /= TName
@@ -12959,8 +12359,8 @@
                      return OK;
                   end if;
 
-                  --  Do replace if prefix is an identifier matching the
-                  --  scope that we are currently looking at.
+                  --  Do replace if prefix is an identifier matching the scope
+                  --  that we are currently looking at.
 
                   if Nkind (P) = N_Identifier
                     and then Chars (P) = Chars (S)
@@ -12969,9 +12369,9 @@
                      return Skip;
                   end if;
 
-                  --  Go check scope above us if prefix is itself of the
-                  --  form of a selected component, whose selector matches
-                  --  the scope we are currently looking at.
+                  --  Go check scope above us if prefix is itself of the form
+                  --  of a selected component, whose selector matches the scope
+                  --  we are currently looking at.
 
                   if Nkind (P) = N_Selected_Component
                     and then Nkind (Selector_Name (P)) = N_Identifier
@@ -12995,8 +12395,10 @@
          else
             return OK;
          end if;
-      end Replace_Node;
+      end Replace_Type_Ref;
 
+      procedure Replace_Type_Refs is new Traverse_Proc (Replace_Type_Ref);
+
    begin
       Replace_Type_Refs (N);
    end Replace_Type_References_Generic;
@@ -13057,17 +12459,18 @@
             Expr := Expression (ASN);
 
             case A_Id is
+
                --  For now we only deal with aspects that do not generate
                --  subprograms, or that may mention current instances of
                --  types. These will require special handling (???TBD).
 
                when Aspect_Predicate         |
                     Aspect_Predicate_Failure |
-                    Aspect_Invariant =>
+                    Aspect_Invariant         =>
                   null;
 
-               when Aspect_Static_Predicate |
-                    Aspect_Dynamic_Predicate =>
+               when Aspect_Dynamic_Predicate |
+                    Aspect_Static_Predicate  =>
 
                   --  Build predicate function specification and preanalyze
                   --  expression after type replacement.
Index: sem_ch13.ads
===================================================================
--- sem_ch13.ads	(revision 237595)
+++ sem_ch13.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -53,25 +53,6 @@
    --  order is specified and there is at least one component clause. Adjusts
    --  component positions according to either Ada 95 or Ada 2005 (AI-133).
 
-   function Build_Invariant_Procedure_Declaration
-     (Typ : Entity_Id) return Node_Id;
-   --  If a type declaration has a specified invariant aspect, build the
-   --  declaration for the procedure at once, so that calls to it can be
-   --  generated before the body of the invariant procedure is built. This
-   --  is needed in the presence of public expression functions that return
-   --  the type in question.
-
-   procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id);
-   --  Typ is a private type with invariants (indicated by Has_Invariants being
-   --  set for Typ, indicating the presence of pragma Invariant entries on the
-   --  rep chain, note that Invariant aspects have already been converted to
-   --  pragma Invariant), then this procedure builds the spec and body for the
-   --  corresponding Invariant procedure, inserting them at appropriate points
-   --  in the package specification N. Invariant_Procedure is set for Typ. Note
-   --  that this procedure is called at the end of processing the declarations
-   --  in the visible part (i.e. the right point for visibility analysis of
-   --  the invariant expression).
-
    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: atree.h
===================================================================
--- atree.h	(revision 237595)
+++ atree.h	(working copy)
@@ -6,7 +6,7 @@
  *                                                                          *
  *                              C Header File                               *
  *                                                                          *
- *          Copyright (C) 1992-2015, Free Software Foundation, Inc.         *
+ *          Copyright (C) 1992-2016, Free Software Foundation, Inc.         *
  *                                                                          *
  * GNAT is free software;  you can  redistribute it  and/or modify it under *
  * terms of the  GNU General Public License as published  by the Free Soft- *
@@ -526,6 +526,7 @@
 #define Elist24(N)    Field24 (N)
 #define Elist25(N)    Field25 (N)
 #define Elist26(N)    Field26 (N)
+#define Elist29(N)    Field29 (N)
 #define Elist36(N)    Field36 (N)
 
 #define Name1(N)      Field1  (N)
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb	(revision 237595)
+++ exp_ch3.adb	(working copy)
@@ -59,7 +59,6 @@
 with Sem_Ch3;  use Sem_Ch3;
 with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch8;  use Sem_Ch8;
-with Sem_Ch13; use Sem_Ch13;
 with Sem_Disp; use Sem_Disp;
 with Sem_Eval; use Sem_Eval;
 with Sem_Mech; use Sem_Mech;
@@ -92,22 +91,6 @@
    --  used for attachment of any actions required in its construction.
    --  It also supplies the source location used for the procedure.
 
-   function Build_Array_Invariant_Proc
-     (A_Type : Entity_Id;
-      Nod    : Node_Id) return Node_Id;
-   --  If the component of type of array type has invariants, build procedure
-   --  that checks invariant on all components of the array. Ada 2012 specifies
-   --  that an invariant on some type T must be applied to in-out parameters
-   --  and return values that include a part of type T. If the array type has
-   --  an otherwise specified invariant, the component check procedure is
-   --  called from within the user-specified invariant. Otherwise this becomes
-   --  the invariant procedure for the array type.
-
-   function Build_Record_Invariant_Proc
-     (R_Type : Entity_Id;
-      Nod    : Node_Id) return Node_Id;
-   --  Ditto for record types.
-
    function Build_Discriminant_Formals
      (Rec_Id : Entity_Id;
       Use_Dl : Boolean) return List_Id;
@@ -200,14 +183,6 @@
    --  Treat user-defined stream operations as renaming_as_body if the
    --  subprogram they rename is not frozen when the type is frozen.
 
-   procedure Insert_Component_Invariant_Checks
-     (N    : Node_Id;
-      Typ  : Entity_Id;
-      Proc : Node_Id);
-   --  If a composite type has invariants and also has components with defined
-   --  invariants. the component invariant procedure is inserted into the user-
-   --  defined invariant procedure and added to the checks to be performed.
-
    procedure Initialization_Warning (E : Entity_Id);
    --  If static elaboration of the package is requested, indicate
    --  when a type does meet the conditions for static initialization. If
@@ -795,138 +770,6 @@
    end Build_Array_Init_Proc;
 
    --------------------------------
-   -- Build_Array_Invariant_Proc --
-   --------------------------------
-
-   function Build_Array_Invariant_Proc
-     (A_Type : Entity_Id;
-      Nod    : Node_Id) return Node_Id
-   is
-      Loc : constant Source_Ptr := Sloc (Nod);
-
-      Object_Name : constant Name_Id := New_Internal_Name ('I');
-      --  Name for argument of invariant procedure
-
-      Object_Entity : constant Node_Id :=
-                        Make_Defining_Identifier (Loc, Object_Name);
-      --  The procedure declaration entity for the argument
-
-      Body_Stmts : List_Id;
-      Index_List : List_Id;
-      Proc_Id    : Entity_Id;
-      Proc_Body  : Node_Id;
-
-      function Build_Component_Invariant_Call return Node_Id;
-      --  Create one statement to verify invariant on one array component,
-      --  designated by a full set of indexes.
-
-      function Check_One_Dimension (N : Int) return List_Id;
-      --  Create loop to check on one dimension of the array. The single
-      --  statement in the loop body checks the inner dimensions if any, or
-      --  else a single component. This procedure is called recursively, with
-      --  N being the dimension to be initialized. A call with N greater than
-      --  the number of dimensions generates the component initialization
-      --  and terminates the recursion.
-
-      ------------------------------------
-      -- Build_Component_Invariant_Call --
-      ------------------------------------
-
-      function Build_Component_Invariant_Call return Node_Id is
-         Comp : Node_Id;
-      begin
-         Comp :=
-           Make_Indexed_Component (Loc,
-             Prefix      => New_Occurrence_Of (Object_Entity, Loc),
-             Expressions => Index_List);
-         return
-           Make_Procedure_Call_Statement (Loc,
-             Name                   =>
-               New_Occurrence_Of
-                 (Invariant_Procedure (Component_Type (A_Type)), Loc),
-             Parameter_Associations => New_List (Comp));
-      end Build_Component_Invariant_Call;
-
-      -------------------------
-      -- Check_One_Dimension --
-      -------------------------
-
-      function Check_One_Dimension (N : Int) return List_Id is
-         Index : Entity_Id;
-
-      begin
-         --  If all dimensions dealt with, we simply check invariant of the
-         --  component.
-
-         if N > Number_Dimensions (A_Type) then
-            return New_List (Build_Component_Invariant_Call);
-
-         --  Else generate one loop and recurse
-
-         else
-            Index :=
-              Make_Defining_Identifier (Loc, New_External_Name ('J', N));
-
-            Append (New_Occurrence_Of (Index, Loc), Index_List);
-
-            return New_List (
-              Make_Implicit_Loop_Statement (Nod,
-                Identifier       => Empty,
-                Iteration_Scheme =>
-                  Make_Iteration_Scheme (Loc,
-                    Loop_Parameter_Specification =>
-                      Make_Loop_Parameter_Specification (Loc,
-                        Defining_Identifier         => Index,
-                        Discrete_Subtype_Definition =>
-                          Make_Attribute_Reference (Loc,
-                            Prefix          =>
-                              New_Occurrence_Of (Object_Entity, Loc),
-                            Attribute_Name  => Name_Range,
-                            Expressions     => New_List (
-                              Make_Integer_Literal (Loc, N))))),
-                Statements       =>  Check_One_Dimension (N + 1)));
-         end if;
-      end Check_One_Dimension;
-
-   --  Start of processing for Build_Array_Invariant_Proc
-
-   begin
-      Index_List := New_List;
-
-      Proc_Id :=
-        Make_Defining_Identifier (Loc,
-           Chars => New_External_Name (Chars (A_Type), "CInvariant"));
-
-      Body_Stmts := Check_One_Dimension (1);
-
-      Proc_Body :=
-        Make_Subprogram_Body (Loc,
-          Specification =>
-            Make_Procedure_Specification (Loc,
-              Defining_Unit_Name       => Proc_Id,
-              Parameter_Specifications => New_List (
-                Make_Parameter_Specification (Loc,
-                  Defining_Identifier => Object_Entity,
-                  Parameter_Type      => New_Occurrence_Of (A_Type, Loc)))),
-
-          Declarations               => Empty_List,
-          Handled_Statement_Sequence =>
-            Make_Handled_Sequence_Of_Statements (Loc,
-              Statements => Body_Stmts));
-
-      Set_Ekind          (Proc_Id, E_Procedure);
-      Set_Is_Public      (Proc_Id, Is_Public (A_Type));
-      Set_Is_Internal    (Proc_Id);
-      Set_Has_Completion (Proc_Id);
-
-      if not Debug_Generated_Code then
-         Set_Debug_Info_Off (Proc_Id);
-      end if;
-
-      return Proc_Body;
-   end Build_Array_Invariant_Proc;
-
-   --------------------------------
    -- Build_Discr_Checking_Funcs --
    --------------------------------
 
@@ -3671,242 +3514,6 @@
       end if;
    end Build_Record_Init_Proc;
 
-   --------------------------------
-   -- Build_Record_Invariant_Proc --
-   --------------------------------
-
-   function Build_Record_Invariant_Proc
-     (R_Type : Entity_Id;
-      Nod    : Node_Id) return Node_Id
-   is
-      Loc : constant Source_Ptr := Sloc (Nod);
-
-      Object_Name : constant Name_Id := New_Internal_Name ('I');
-      --  Name for argument of invariant procedure
-
-      Object_Entity : constant Node_Id :=
-        Make_Defining_Identifier (Loc, Object_Name);
-      --  The procedure declaration entity for the argument
-
-      Invariant_Found : Boolean;
-      --  Set if any component needs an invariant check.
-
-      Proc_Id   : Entity_Id;
-      Proc_Body : Node_Id;
-      Stmts     : List_Id;
-      Type_Def  : Node_Id;
-
-      function Build_Invariant_Checks (Comp_List : Node_Id) return List_Id;
-      --  Recursive procedure that generates a list of checks for components
-      --  that need it, and recurses through variant parts when present.
-
-      function Build_Component_Invariant_Call
-        (Comp : Entity_Id) return Node_Id;
-      --  Build call to invariant procedure for a record component
-
-      ------------------------------------
-      -- Build_Component_Invariant_Call --
-      ------------------------------------
-
-      function Build_Component_Invariant_Call
-        (Comp : Entity_Id) return Node_Id
-      is
-         Call     : Node_Id;
-         Proc     : Entity_Id;
-         Sel_Comp : Node_Id;
-         Typ      : Entity_Id;
-
-      begin
-         Typ := Etype (Comp);
-
-         Sel_Comp :=
-           Make_Selected_Component (Loc,
-             Prefix        => New_Occurrence_Of (Object_Entity, Loc),
-             Selector_Name => New_Occurrence_Of (Comp, Loc));
-
-         if Is_Access_Type (Typ) then
-
-            --  If the access component designates a type with an invariant,
-            --  the check applies to the designated object. The access type
-            --  itself may have an invariant, in which case it applies to the
-            --  access value directly.
-
-            --  Note: we are assuming that invariants will not occur on both
-            --  the access type and the type that it designates. This is not
-            --  really justified but it is hard to imagine that this case will
-            --  ever cause trouble ???
-
-            if not (Has_Invariants (Typ)) then
-               Sel_Comp := Make_Explicit_Dereference (Loc, Sel_Comp);
-               Typ := Designated_Type (Typ);
-            end if;
-         end if;
-
-         --  The aspect is type-specific, so retrieve it from the base type
-
-         Proc := Invariant_Procedure (Base_Type (Typ));
-
-         if Has_Null_Body (Proc) then
-            return Make_Null_Statement (Loc);
-         end if;
-
-         Invariant_Found := True;
-         Call :=
-           Make_Procedure_Call_Statement (Loc,
-             Name                   => New_Occurrence_Of (Proc, Loc),
-             Parameter_Associations => New_List (Sel_Comp));
-
-         if Is_Access_Type (Etype (Comp)) then
-            Call :=
-              Make_If_Statement (Loc,
-                Condition       =>
-                  Make_Op_Ne (Loc,
-                    Left_Opnd   => Make_Null (Loc),
-                    Right_Opnd  =>
-                      Make_Selected_Component (Loc,
-                        Prefix        =>
-                          New_Occurrence_Of (Object_Entity, Loc),
-                        Selector_Name => New_Occurrence_Of (Comp, Loc))),
-                Then_Statements => New_List (Call));
-         end if;
-
-         return Call;
-      end Build_Component_Invariant_Call;
-
-      ----------------------------
-      -- Build_Invariant_Checks --
-      ----------------------------
-
-      function Build_Invariant_Checks (Comp_List : Node_Id) return List_Id is
-         Decl     : Node_Id;
-         Id       : Entity_Id;
-         Stmts    : List_Id;
-
-      begin
-         Stmts := New_List;
-         Decl := First_Non_Pragma (Component_Items (Comp_List));
-         while Present (Decl) loop
-            if Nkind (Decl) = N_Component_Declaration then
-               Id := Defining_Identifier (Decl);
-
-               if Has_Invariants (Etype (Id))
-                 and then In_Open_Scopes (Scope (R_Type))
-               then
-                  if Has_Unchecked_Union (R_Type) then
-                     Error_Msg_NE
-                       ("invariants cannot be checked on components of "
-                         & "unchecked_union type&?", Decl, R_Type);
-                     return Empty_List;
-
-                  else
-                     Append_To (Stmts, Build_Component_Invariant_Call (Id));
-                  end if;
-
-               elsif Is_Access_Type (Etype (Id))
-                 and then not Is_Access_Constant (Etype (Id))
-                 and then Has_Invariants (Designated_Type (Etype (Id)))
-                 and then In_Open_Scopes (Scope (Designated_Type (Etype (Id))))
-               then
-                  Append_To (Stmts, Build_Component_Invariant_Call (Id));
-               end if;
-            end if;
-
-            Next (Decl);
-         end loop;
-
-         if Present (Variant_Part (Comp_List)) then
-            declare
-               Variant_Alts  : constant List_Id := New_List;
-               Var_Loc       : Source_Ptr;
-               Variant       : Node_Id;
-               Variant_Stmts : List_Id;
-
-            begin
-               Variant :=
-                 First_Non_Pragma (Variants (Variant_Part (Comp_List)));
-               while Present (Variant) loop
-                  Variant_Stmts :=
-                    Build_Invariant_Checks (Component_List (Variant));
-                  Var_Loc := Sloc (Variant);
-                  Append_To (Variant_Alts,
-                    Make_Case_Statement_Alternative (Var_Loc,
-                      Discrete_Choices =>
-                        New_Copy_List (Discrete_Choices (Variant)),
-                      Statements => Variant_Stmts));
-
-                  Next_Non_Pragma (Variant);
-               end loop;
-
-               --  The expression in the case statement is the reference to
-               --  the discriminant of the target object.
-
-               Append_To (Stmts,
-                 Make_Case_Statement (Var_Loc,
-                   Expression =>
-                     Make_Selected_Component (Var_Loc,
-                      Prefix => New_Occurrence_Of (Object_Entity, Var_Loc),
-                      Selector_Name => New_Occurrence_Of
-                        (Entity
-                          (Name (Variant_Part (Comp_List))), Var_Loc)),
-                      Alternatives => Variant_Alts));
-            end;
-         end if;
-
-         return Stmts;
-      end Build_Invariant_Checks;
-
-   --  Start of processing for Build_Record_Invariant_Proc
-
-   begin
-      Invariant_Found := False;
-      Type_Def := Type_Definition (Parent (R_Type));
-
-      if Nkind (Type_Def) = N_Record_Definition
-        and then not Null_Present (Type_Def)
-      then
-         Stmts := Build_Invariant_Checks (Component_List (Type_Def));
-      else
-         return Empty;
-      end if;
-
-      if not Invariant_Found then
-         return Empty;
-      end if;
-
-      --  The name of the invariant procedure reflects the fact that the
-      --  checks correspond to invariants on the component types. The
-      --  record type itself may have invariants that will create a separate
-      --  procedure whose name carries the Invariant suffix.
-
-      Proc_Id :=
-        Make_Defining_Identifier (Loc,
-           Chars => New_External_Name (Chars (R_Type), "CInvariant"));
-
-      Proc_Body :=
-        Make_Subprogram_Body (Loc,
-          Specification =>
-            Make_Procedure_Specification (Loc,
-              Defining_Unit_Name       => Proc_Id,
-              Parameter_Specifications => New_List (
-                Make_Parameter_Specification (Loc,
-                  Defining_Identifier => Object_Entity,
-                  Parameter_Type      => New_Occurrence_Of (R_Type, Loc)))),
-
-          Declarations               => Empty_List,
-          Handled_Statement_Sequence =>
-            Make_Handled_Sequence_Of_Statements (Loc,
-              Statements => Stmts));
-
-      Set_Ekind          (Proc_Id, E_Procedure);
-      Set_Is_Public      (Proc_Id, Is_Public (R_Type));
-      Set_Is_Internal    (Proc_Id);
-      Set_Has_Completion (Proc_Id);
-
-      return Proc_Body;
-      --  Insert_After (Nod, Proc_Body);
-      --  Analyze (Proc_Body);
-   end Build_Record_Invariant_Proc;
-
    ----------------------------
    -- Build_Slice_Assignment --
    ----------------------------
@@ -4680,21 +4287,6 @@
          Build_Array_Init_Proc (Base, N);
       end if;
 
-      if Has_Invariants (Component_Type (Base))
-        and then Typ = Base
-        and then In_Open_Scopes (Scope (Component_Type (Base)))
-      then
-         --  Generate component invariant checking procedure. This is only
-         --  relevant if the array type is within the scope of the component
-         --  type. Otherwise an array object can only be built using the public
-         --  subprograms for the component type, and calls to those will have
-         --  invariant checks. The invariant procedure is only generated for
-         --  a base type, not a subtype.
-
-         Insert_Component_Invariant_Checks
-           (N, Base, Build_Array_Invariant_Proc (Base, N));
-      end if;
-
       Ghost_Mode := Save_Ghost_Mode;
    end Expand_Freeze_Array_Type;
 
@@ -5551,24 +5143,6 @@
          end;
       end if;
 
-      --  Check whether individual components have a defined invariant, and add
-      --  the corresponding component invariant checks.
-
-      --  Do not create an invariant procedure for some internally generated
-      --  subtypes, in particular those created for objects of a class-wide
-      --  type. Such types may have components to which invariant apply, but
-      --  the corresponding checks will be applied when an object of the parent
-      --  type is constructed.
-
-      --  Such objects will show up in a class-wide postcondition, and the
-      --  invariant will be checked, if necessary, upon return from the
-      --  enclosing subprogram.
-
-      if not Is_Class_Wide_Equivalent_Type (Typ) then
-         Insert_Component_Invariant_Checks
-           (N, Typ, Build_Record_Invariant_Proc (Typ, N));
-      end if;
-
       Ghost_Mode := Save_Ghost_Mode;
    end Expand_Freeze_Record_Type;
 
@@ -7476,11 +7050,11 @@
 
       elsif Ekind_In (Def_Id, E_Access_Type, E_General_Access_Type) then
          declare
-            Loc         : constant Source_Ptr := Sloc (N);
-            Desig_Type  : constant Entity_Id  := Designated_Type (Def_Id);
-            Pool_Object : Entity_Id;
+            Loc        : constant Source_Ptr := Sloc (N);
+            Desig_Type : constant Entity_Id  := Designated_Type (Def_Id);
 
             Freeze_Action_Typ : Entity_Id;
+            Pool_Object       : Entity_Id;
 
          begin
             --  Case 1
@@ -7500,8 +7074,8 @@
 
             elsif Has_Storage_Size_Clause (Def_Id) then
                declare
-                  DT_Size  : Node_Id;
                   DT_Align : Node_Id;
+                  DT_Size  : Node_Id;
 
                begin
                   --  For unconstrained composite types we give a size of zero
@@ -7746,6 +7320,16 @@
       Process_Pending_Access_Types (Def_Id);
       Freeze_Stream_Operations (N, Def_Id);
 
+      --  Generate the [spec and] body of the invariant procedure tasked with
+      --  the runtime verification of all invariants that pertain to the type.
+      --  This includes invariants on the partial and full view, inherited
+      --  class-wide invariants from parent types or interfaces, and invariants
+      --  on array elements or record components.
+
+      if Has_Invariants (Def_Id) then
+         Build_Invariant_Procedure_Body (Def_Id);
+      end if;
+
       Ghost_Mode := Save_Ghost_Mode;
       return Result;
 
@@ -8164,77 +7748,6 @@
       return Is_RTU (S1, System) or else Is_RTU (S1, Ada);
    end In_Runtime;
 
-   ---------------------------------------
-   -- Insert_Component_Invariant_Checks --
-   ---------------------------------------
-
-   procedure Insert_Component_Invariant_Checks
-     (N   : Node_Id;
-     Typ  : Entity_Id;
-     Proc : Node_Id)
-   is
-      Loc     : constant Source_Ptr := Sloc (Typ);
-      Proc_Id : Entity_Id;
-
-   begin
-      if Present (Proc) then
-         Proc_Id := Defining_Entity (Proc);
-
-         if not Has_Invariants (Typ) then
-            Set_Has_Invariants (Typ);
-            Set_Is_Invariant_Procedure (Proc_Id);
-            Set_Invariant_Procedure (Typ, Proc_Id);
-            Insert_After (N, Proc);
-            Analyze (Proc);
-
-         else
-
-            --  Find already created invariant subprogram, insert body of
-            --  component invariant proc in its body, and add call after
-            --  other checks.
-
-            declare
-               Bod    : Node_Id;
-               Inv_Id : constant Entity_Id := Invariant_Procedure (Typ);
-               Call   : constant Node_Id   :=
-                 Make_Procedure_Call_Statement (Sloc (N),
-                   Name                   => New_Occurrence_Of (Proc_Id, Loc),
-                   Parameter_Associations =>
-                     New_List
-                       (New_Occurrence_Of (First_Formal (Inv_Id), Loc)));
-
-            begin
-               --  The invariant  body has not been analyzed yet, so we do a
-               --  sequential search forward, and retrieve it by name.
-
-               Bod := Next (N);
-               while Present (Bod) loop
-                  exit when Nkind (Bod) = N_Subprogram_Body
-                    and then Chars (Defining_Entity (Bod)) = Chars (Inv_Id);
-                  Next (Bod);
-               end loop;
-
-               --  If the body is not found, it is the case of an invariant
-               --  appearing on a full declaration in a private part, in
-               --  which case the type has been frozen but the invariant
-               --  procedure for the composite type not created yet. Create
-               --  body now.
-
-               if No (Bod) then
-                  Build_Invariant_Procedure (Typ, Parent (Current_Scope));
-                  Bod := Unit_Declaration_Node
-                    (Corresponding_Body (Unit_Declaration_Node (Inv_Id)));
-               end if;
-
-               Append_To (Declarations (Bod), Proc);
-               Append_To (Statements (Handled_Statement_Sequence (Bod)), Call);
-               Analyze (Proc);
-               Analyze (Call);
-            end;
-         end if;
-      end if;
-   end Insert_Component_Invariant_Checks;
-
    ----------------------------
    -- Initialization_Warning --
    ----------------------------


More information about the Gcc-patches mailing list