[Ada] Ada2022: AI12-0195 overriding class-wide pre/postconditions

gcc/ada/

	* contracts.ads (Make_Class_Precondition_Subps): New subprogram.
	(Merge_Class_Conditions): New subprogram.
	(Process_Class_Conditions_At_Freeze_Point): New subprogram.

	* contracts.adb (Check_Class_Condition): New subprogram.
	(Set_Class_Condition): New subprogram.
	(Analyze_Contracts): Remove code analyzing class-wide-clone
	subprogram since it is no longer built.
	(Process_Spec_Postconditions): Avoid processing twice seen
	subprograms.
	(Process_Preconditions): Simplify its functionality to
	non-class-wide preconditions.
	(Process_Preconditions_For): No action needed for wrappers and
	helpers.
	(Make_Class_Precondition_Subps): New subprogram.
	(Process_Class_Conditions_At_Freeze_Point): New subprogram.
	(Merge_Class_Conditions): New subprogram.
	* exp_ch6.ads (Install_Class_Preconditions_Check): New
	subprogram.
	* exp_ch6.adb (Expand_Call_Helper): Install class-wide
	preconditions check on dispatching primitives that have or
	inherit class-wide preconditions.
	(Freeze_Subprogram): Remove code for null procedures with
	preconditions.
	(Install_Class_Preconditions_Check): New subprogram.
	* exp_util.ads (Build_Class_Wide_Expression): Lower the
	complexity of this subprogram; out-mode formal Needs_Wrapper
	since this functionality is now provided by a new subprogram.
	(Get_Mapped_Entity): New subprogram.
	(Map_Formals): New subprogram.
	* exp_util.adb (Build_Class_Wide_Expression): Lower the
	complexity of this subprogram. Its previous functionality is now
	provided by subprograms Needs_Wrapper and Check_Class_Condition.
	(Add_Parent_DICs): Map the overridden primitive to the
	overriding one.
	(Get_Mapped_Entity): New subprogram.
	(Map_Formals): New subprogram.
	(Update_Primitives_Mapping): Adding assertion.
	* freeze.ads (Check_Inherited_Conditions): Subprogram made
	public with added formal to support late overriding.
	* freeze.adb (Check_Inherited_Conditions): New implementation;
	builds the dispatch table wrapper required for class-wide
	pre/postconditions; added support for late overriding.
	(Needs_Wrapper): New subprogram.
	* sem.ads (Inside_Class_Condition_Preanalysis): New global
	variable.
	* sem_disp.ads (Covered_Interface_Primitives): New subprogram.
	* sem_disp.adb (Covered_Interface_Primitives): New subprogram.
	(Check_Dispatching_Context): Skip checking context of
	dispatching calls during preanalysis of class-wide conditions
	since at that stage the expression is not installed yet on its
	definite context.
	(Check_Dispatching_Call): Skip checking 6.1.1(18.2/5) by
	AI12-0412 on helpers and wrappers internally built for
	supporting class-wide conditions; for late-overriding
	subprograms call Check_Inherited_Conditions to build the
	dispatch-table wrapper (if required).
	(Propagate_Tag): Adding call to
	Install_Class_Preconditions_Check.
	* sem_util.ads (Build_Class_Wide_Clone_Body): Removed.
	(Build_Class_Wide_Clone_Call): Removed.
	(Build_Class_Wide_Clone_Decl): Removed.
	(Class_Condition): New subprogram.
	(Nearest_Class_Condition_Subprogram): New subprogram.
	* sem_util.adb (Build_Class_Wide_Clone_Body): Removed.
	(Build_Class_Wide_Clone_Call): Removed.
	(Build_Class_Wide_Clone_Decl): Removed.
	(Class_Condition): New subprogram.
	(Nearest_Class_Condition_Subprogram): New subprogram.
	(Eligible_For_Conditional_Evaluation): No need to evaluate
	class-wide conditions during preanalysis since the expression is
	not installed on its definite context.
	* einfo.ads (Class_Wide_Clone): Removed.
	(Class_Postconditions): New attribute.
	(Class_Preconditions): New attribute.
	(Class_Preconditions_Subprogram): New attribute.
	(Dynamic_Call_Helper): New attribute.
	(Ignored_Class_Postconditions): New attribute.
	(Ignored_Class_Preconditions): New attribute.
	(Indirect_Call_Wrapper): New attribute.
	(Is_Dispatch_Table_Wrapper): New attribute.
	(Static_Call_Helper): New attribute.
	* exp_attr.adb (Expand_N_Attribute_Reference): When the prefix
	is of an access-to-subprogram type that has class-wide
	preconditions and an indirect-call wrapper of such subprogram is
	available, replace the prefix by the wrapper.
	* exp_ch3.adb (Build_Class_Condition_Subprograms): New
	subprogram.
	(Register_Dispatch_Table_Wrappers): New subprogram.
	* exp_disp.adb (Build_Class_Wide_Check): Removed; class-wide
	precondition checks now rely on internally built helpers.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Set initial
	value of attributes Class_Preconditions, Class_Postconditions,
	Ignored_Class_Preconditions and Ignored_Class_Postconditions.
	These values are later updated with the full pre/postcondition
	by Merge_Class_Conditions.
	(Freeze_Entity_Checks): Call
	Process_Class_Conditions_At_Freeze_Point.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove code
	building the body of the class-wide clone subprogram since it is
	no longer required.
	(Install_Entity): Adding assertion.
	* sem_prag.adb (Analyze_Pre_Post_Condition_In_Decl_Part): Remove
	code building and analyzing the class-wide clone subprogram; no
	longer required.
	(Build_Pragma_Check_Equivalent): Adjust call to
	Build_Class_Wide_Expression since the formal named Needs_Wrapper
	has been removed.
	* sem_attr.adb (Analyze_Attribute_Old_Result): Skip processing
	these attributes during preanalysis of class-wide conditions
	since at that stage the expression is not installed yet on its
	definite context.
	* sem_res.adb (Resolve_Actuals): Skip applying RM 3.9.2(9/1) and
	SPARK RM 6.1.7(3) on actuals of internal helpers and wrappers
	built to support class-wide preconditions.
	* sem_ch5.adb (Process_Bounds): Do not generate a constant
	declaration for the bounds when we are preanalyzing a class-wide
	condition.
	(Analyze_Loop_Parameter_Specification): Handle preanalysis of
	quantified expression placed in the outermost expression of a
	class-wide condition.
	* ghost.adb (Check_Ghost_Context): No check required during
	preanalysis of class-wide conditions.
	* gen_il-fields.ads (Opt_Field_Enum): Adding
	Class_Postconditions, Class_Preconditions,
	Class_Preconditions_Subprogram, Dynamic_Call_Helper,
	Ignored_Class_Postconditions, Ignored_Class_Preconditions,
	Indirect_Call_Wrapper, Is_Dispatch_Table_Wrapper,
	Static_Call_Helper.
	* gen_il-gen-gen_entities.adb (Is_Dispatch_Table_Wrapper):
	Adding semantic flag Is_Dispatch_Table_Wrapper; removing
	semantic field Class_Wide_Clone; adding semantic fields for
	Class_Postconditions, Class_Preconditions,
	Class_Preconditions_Subprogram, Dynamic_Call_Helper,
	Ignored_Class_Postconditions, Indirect_Call_Wrapper,
	Ignored_Class_Preconditions, and Static_Call_Helper.

1 files changed, 1348 insertions, 215 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 705f197..2726486 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -47,6 +47,8 @@ with Sem_Ch12;       use Sem_Ch12;
 with Sem_Ch13;       use Sem_Ch13;
 with Sem_Disp;       use Sem_Disp;
 with Sem_Prag;       use Sem_Prag;
+with Sem_Res;        use Sem_Res;
+with Sem_Type;       use Sem_Type;
 with Sem_Util;       use Sem_Util;
 with Sinfo;          use Sinfo;
 with Sinfo.Nodes;    use Sinfo.Nodes;
@@ -66,6 +68,16 @@ package body Contracts is
    --
    --    Part_Of
 
+   procedure Check_Class_Condition
+     (Cond            : Node_Id;
+      Subp            : Entity_Id;
+      Par_Subp        : Entity_Id;
+      Is_Precondition : Boolean);
+   --  Perform checking of class-wide pre/postcondition Cond inherited by Subp
+   --  from Par_Subp. Is_Precondition enables check specific for preconditions.
+   --  In SPARK_Mode, an inherited operation that is not overridden but has
+   --  inherited modified conditions pre/postconditions is illegal.
+
    procedure Check_Type_Or_Object_External_Properties
      (Type_Or_Obj_Id : Entity_Id);
    --  Perform checking of external properties pragmas that is common to both
@@ -77,6 +89,12 @@ package body Contracts is
    --  well as Contract_Cases, Subprogram_Variant, invariants and predicates.
    --  Body_Id denotes the entity of the subprogram body.
 
+   procedure Set_Class_Condition
+     (Kind : Condition_Kind;
+      Subp : Entity_Id;
+      Cond : Node_Id);
+   --  Set the class-wide Kind condition of Subp
+
    -----------------------
    -- Add_Contract_Item --
    -----------------------
@@ -386,23 +404,7 @@ package body Contracts is
                           | N_Generic_Subprogram_Declaration
                           | N_Subprogram_Declaration
          then
-            declare
-               Subp_Id : constant Entity_Id := Defining_Entity (Decl);
-
-            begin
-               Analyze_Entry_Or_Subprogram_Contract (Subp_Id);
-
-               --  If analysis of a class-wide pre/postcondition indicates
-               --  that a class-wide clone is needed, analyze its declaration
-               --  now. Its body is created when the body of the original
-               --  operation is analyzed (and rewritten).
-
-               if Is_Subprogram (Subp_Id)
-                 and then Present (Class_Wide_Clone (Subp_Id))
-               then
-                  Analyze (Unit_Declaration_Node (Class_Wide_Clone (Subp_Id)));
-               end if;
-            end;
+            Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
 
          --  Entry or subprogram bodies
 
@@ -1491,6 +1493,141 @@ package body Contracts is
         (Type_Or_Obj_Id => Type_Id);
    end Analyze_Type_Contract;
 
+   ---------------------------
+   -- Check_Class_Condition --
+   ---------------------------
+
+   procedure Check_Class_Condition
+     (Cond            : Node_Id;
+      Subp            : Entity_Id;
+      Par_Subp        : Entity_Id;
+      Is_Precondition : Boolean)
+   is
+      function Check_Entity (N : Node_Id) return Traverse_Result;
+      --  Check reference to formal of inherited operation or to primitive
+      --  operation of root type.
+
+      ------------------
+      -- Check_Entity --
+      ------------------
+
+      function Check_Entity (N : Node_Id) return Traverse_Result is
+         New_E  : Entity_Id;
+         Orig_E : Entity_Id;
+
+      begin
+         if Nkind (N) = N_Identifier
+           and then Present (Entity (N))
+           and then
+             (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
+           and then
+             (Nkind (Parent (N)) /= N_Attribute_Reference
+               or else Attribute_Name (Parent (N)) /= Name_Class)
+         then
+            --  These checks do not apply to dispatching calls within the
+            --  condition, but only to calls whose static tag is that of
+            --  the parent type.
+
+            if Is_Subprogram (Entity (N))
+              and then Nkind (Parent (N)) = N_Function_Call
+              and then Present (Controlling_Argument (Parent (N)))
+            then
+               return OK;
+            end if;
+
+            --  Determine whether entity has a renaming
+
+            Orig_E := Entity (N);
+            New_E  := Get_Mapped_Entity (Orig_E);
+
+            if Present (New_E) then
+
+               --  AI12-0166: A precondition for a protected operation
+               --  cannot include an internal call to a protected function
+               --  of the type. In the case of an inherited condition for an
+               --  overriding operation, both the operation and the function
+               --  are given by primitive wrappers.
+
+               if Is_Precondition
+                 and then Ekind (New_E) = E_Function
+                 and then Is_Primitive_Wrapper (New_E)
+                 and then Is_Primitive_Wrapper (Subp)
+                 and then Scope (Subp) = Scope (New_E)
+               then
+                  Error_Msg_Node_2 := Wrapped_Entity (Subp);
+                  Error_Msg_NE
+                    ("internal call to& cannot appear in inherited "
+                     & "precondition of protected operation&",
+                     Subp, Wrapped_Entity (New_E));
+               end if;
+            end if;
+
+            --  Check that there are no calls left to abstract operations if
+            --  the current subprogram is not abstract.
+
+            if Present (New_E)
+              and then Nkind (Parent (N)) = N_Function_Call
+              and then N = Name (Parent (N))
+            then
+               if not Is_Abstract_Subprogram (Subp)
+                 and then Is_Abstract_Subprogram (New_E)
+               then
+                  Error_Msg_Sloc   := Sloc (Current_Scope);
+                  Error_Msg_Node_2 := Subp;
+
+                  if Comes_From_Source (Subp) then
+                     Error_Msg_NE
+                       ("cannot call abstract subprogram & in inherited "
+                        & "condition for&#", Subp, New_E);
+                  else
+                     Error_Msg_NE
+                       ("cannot call abstract subprogram & in inherited "
+                        & "condition for inherited&#", Subp, New_E);
+                  end if;
+
+               --  In SPARK mode, report error on inherited condition for an
+               --  inherited operation if it contains a call to an overriding
+               --  operation, because this implies that the pre/postconditions
+               --  of the inherited operation have changed silently.
+
+               elsif SPARK_Mode = On
+                 and then Warn_On_Suspicious_Contract
+                 and then Present (Alias (Subp))
+                 and then Present (New_E)
+                 and then Comes_From_Source (New_E)
+               then
+                  Error_Msg_N
+                    ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
+                     Parent (Subp));
+                  Error_Msg_Sloc   := Sloc (New_E);
+                  Error_Msg_Node_2 := Subp;
+                  Error_Msg_NE
+                    ("\overriding of&# forces overriding of&",
+                     Parent (Subp), New_E);
+               end if;
+            end if;
+         end if;
+
+         return OK;
+      end Check_Entity;
+
+      procedure Check_Condition_Entities is
+        new Traverse_Proc (Check_Entity);
+
+   --  Start of processing for Check_Class_Condition
+
+   begin
+      --  No check required if the subprograms match
+
+      if Par_Subp = Subp then
+         return;
+      end if;
+
+      Update_Primitives_Mapping (Par_Subp, Subp);
+      Map_Formals (Par_Subp, Subp);
+      Check_Condition_Entities (Cond);
+   end Check_Class_Condition;
+
    -----------------------------
    -- Create_Generic_Contract --
    -----------------------------
@@ -1900,7 +2037,7 @@ package body Contracts is
       procedure Add_Stable_Property_Contracts
         (Subp_Id : Entity_Id; Class_Present : Boolean)
       is
-         Loc         : constant Source_Ptr := Sloc (Subp_Id);
+         Loc : constant Source_Ptr := Sloc (Subp_Id);
 
          procedure Insert_Stable_Property_Check
            (Formal : Entity_Id; Property_Function : Entity_Id);
@@ -2552,13 +2689,38 @@ package body Contracts is
          ---------------------------------
 
          procedure Process_Spec_Postconditions is
-            Subps   : constant Subprogram_List :=
-                        Inherited_Subprograms (Spec_Id);
+            Subps : constant Subprogram_List :=
+                      Inherited_Subprograms (Spec_Id);
+            Seen  : Subprogram_List (Subps'Range) := (others => Empty);
+
+            function Seen_Subp (Subp_Id : Entity_Id) return Boolean;
+            --  Return True if the contract of subprogram Subp_Id has been
+            --  processed.
+
+            ---------------
+            -- Seen_Subp --
+            ---------------
+
+            function Seen_Subp (Subp_Id : Entity_Id) return Boolean is
+            begin
+               for Index in Seen'Range loop
+                  if Seen (Index) = Subp_Id then
+                     return True;
+                  end if;
+               end loop;
+
+               return False;
+            end Seen_Subp;
+
+            --  Local variables
+
             Item    : Node_Id;
             Items   : Node_Id;
             Prag    : Node_Id;
             Subp_Id : Entity_Id;
 
+         --  Start of processing for Process_Spec_Postconditions
+
          begin
             --  Process the contract
 
@@ -2589,7 +2751,7 @@ package body Contracts is
                   Subp_Id := Ultimate_Alias (Subp_Id);
                end if;
 
-               --  Wrappers of class-wide pre/post conditions reference the
+               --  Wrappers of class-wide pre/postconditions reference the
                --  parent primitive that has the inherited contract.
 
                if Is_Wrapper (Subp_Id)
@@ -2600,7 +2762,9 @@ package body Contracts is
 
                Items := Contract (Subp_Id);
 
-               if Present (Items) then
+               if not Seen_Subp (Subp_Id) and then Present (Items) then
+                  Seen (Index) := Subp_Id;
+
                   Prag := Pre_Post_Conditions (Items);
                   while Present (Prag) loop
                      if Pragma_Name (Prag) = Name_Postcondition
@@ -2657,10 +2821,6 @@ package body Contracts is
       ---------------------------
 
       procedure Process_Preconditions is
-         Class_Pre : Node_Id := Empty;
-         --  The sole [inherited] class-wide precondition pragma that applies
-         --  to the subprogram.
-
          Insert_Node : Node_Id := Empty;
          --  The insertion node after which all pragma Check equivalents are
          --  inserted.
@@ -2669,21 +2829,12 @@ package body Contracts is
          --  Determine whether arbitrary declaration Decl denotes a renaming of
          --  a discriminant or protection field _object.
 
-         procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
-         --  Merge two class-wide preconditions by "or else"-ing them. The
-         --  changes are accumulated in parameter Into. Update the error
-         --  message of Into.
-
          procedure Prepend_To_Decls (Item : Node_Id);
          --  Prepend a single item to the declarations of the subprogram body
 
-         procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
-         --  Save a class-wide precondition into Class_Pre, or prepend a normal
-         --  precondition to the declarations of the body and analyze it.
-
-         procedure Process_Inherited_Preconditions;
-         --  Collect all inherited class-wide preconditions and merge them into
-         --  one big precondition to be evaluated as pragma Check.
+         procedure Prepend_Pragma_To_Decls (Prag : Node_Id);
+         --  Prepend a normal precondition to the declarations of the body and
+         --  analyze it.
 
          procedure Process_Preconditions_For (Subp_Id : Entity_Id);
          --  Collect all preconditions of subprogram Subp_Id and prepend their
@@ -2737,78 +2888,6 @@ package body Contracts is
             return False;
          end Is_Prologue_Renaming;
 
-         -------------------------
-         -- Merge_Preconditions --
-         -------------------------
-
-         procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
-            function Expression_Arg (Prag : Node_Id) return Node_Id;
-            --  Return the boolean expression argument of a precondition while
-            --  updating its parentheses count for the subsequent merge.
-
-            function Message_Arg (Prag : Node_Id) return Node_Id;
-            --  Return the message argument of a precondition
-
-            --------------------
-            -- Expression_Arg --
-            --------------------
-
-            function Expression_Arg (Prag : Node_Id) return Node_Id is
-               Args : constant List_Id := Pragma_Argument_Associations (Prag);
-               Arg  : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
-
-            begin
-               if Paren_Count (Arg) = 0 then
-                  Set_Paren_Count (Arg, 1);
-               end if;
-
-               return Arg;
-            end Expression_Arg;
-
-            -----------------
-            -- Message_Arg --
-            -----------------
-
-            function Message_Arg (Prag : Node_Id) return Node_Id is
-               Args : constant List_Id := Pragma_Argument_Associations (Prag);
-            begin
-               return Get_Pragma_Arg (Last (Args));
-            end Message_Arg;
-
-            --  Local variables
-
-            From_Expr : constant Node_Id := Expression_Arg (From);
-            From_Msg  : constant Node_Id := Message_Arg    (From);
-            Into_Expr : constant Node_Id := Expression_Arg (Into);
-            Into_Msg  : constant Node_Id := Message_Arg    (Into);
-            Loc       : constant Source_Ptr := Sloc (Into);
-
-         --  Start of processing for Merge_Preconditions
-
-         begin
-            --  Merge the two preconditions by "or else"-ing them
-
-            Rewrite (Into_Expr,
-              Make_Or_Else (Loc,
-                Right_Opnd => Relocate_Node (Into_Expr),
-                Left_Opnd  => From_Expr));
-
-            --  Merge the two error messages to produce a single message of the
-            --  form:
-
-            --    failed precondition from ...
-            --      also failed inherited precondition from ...
-
-            if not Exception_Locations_Suppressed then
-               Start_String (Strval (Into_Msg));
-               Store_String_Char (ASCII.LF);
-               Store_String_Chars ("  also ");
-               Store_String_Chars (Strval (From_Msg));
-
-               Set_Strval (Into_Msg, End_String);
-            end if;
-         end Merge_Preconditions;
-
          ----------------------
          -- Prepend_To_Decls --
          ----------------------
@@ -2829,28 +2908,27 @@ package body Contracts is
             Prepend_To (Decls, Item);
          end Prepend_To_Decls;
 
-         ------------------------------
-         -- Prepend_To_Decls_Or_Save --
-         ------------------------------
+         -----------------------------
+         -- Prepend_Pragma_To_Decls --
+         -----------------------------
 
-         procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
+         procedure Prepend_Pragma_To_Decls (Prag : Node_Id) is
             Check_Prag : Node_Id;
 
          begin
-            Check_Prag := Build_Pragma_Check_Equivalent (Prag);
-
-            --  Save the sole class-wide precondition (if any) for the next
-            --  step, where it will be merged with inherited preconditions.
+            --  Skip the sole class-wide precondition (if any) since it is
+            --  processed by Merge_Class_Conditions.
 
             if Class_Present (Prag) then
-               pragma Assert (No (Class_Pre));
-               Class_Pre := Check_Prag;
+               null;
 
             --  Accumulate the corresponding Check pragmas at the top of the
             --  declarations. Prepending the items ensures that they will be
             --  evaluated in their original order.
 
             else
+               Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+
                if Present (Insert_Node) then
                   Insert_After (Insert_Node, Check_Prag);
                else
@@ -2859,87 +2937,7 @@ package body Contracts is
 
                Analyze (Check_Prag);
             end if;
-         end Prepend_To_Decls_Or_Save;
-
-         -------------------------------------
-         -- Process_Inherited_Preconditions --
-         -------------------------------------
-
-         procedure Process_Inherited_Preconditions is
-            Subps : constant Subprogram_List :=
-                      Inherited_Subprograms (Spec_Id);
-
-            Item    : Node_Id;
-            Items   : Node_Id;
-            Prag    : Node_Id;
-            Subp_Id : Entity_Id;
-
-         begin
-            --  Process the contracts of all inherited subprograms, looking for
-            --  class-wide preconditions.
-
-            for Index in Subps'Range loop
-               Subp_Id := Subps (Index);
-
-               if Present (Alias (Subp_Id)) then
-                  Subp_Id := Ultimate_Alias (Subp_Id);
-               end if;
-
-               --  Wrappers of class-wide pre/post conditions reference the
-               --  parent primitive that has the inherited contract.
-
-               if Is_Wrapper (Subp_Id)
-                 and then Present (LSP_Subprogram (Subp_Id))
-               then
-                  Subp_Id := LSP_Subprogram (Subp_Id);
-               end if;
-
-               Items := Contract (Subp_Id);
-
-               if Present (Items) then
-                  Prag := Pre_Post_Conditions (Items);
-                  while Present (Prag) loop
-                     if Pragma_Name (Prag) = Name_Precondition
-                       and then Class_Present (Prag)
-                     then
-                        Item :=
-                          Build_Pragma_Check_Equivalent
-                            (Prag     => Prag,
-                             Subp_Id  => Spec_Id,
-                             Inher_Id => Subp_Id);
-
-                        --  The pragma Check equivalent of the class-wide
-                        --  precondition is still created even though the
-                        --  pragma may be ignored because the equivalent
-                        --  performs semantic checks.
-
-                        if Is_Checked (Prag) then
-
-                           --  The spec of an inherited subprogram already
-                           --  yielded a class-wide precondition. Merge the
-                           --  existing precondition with the current one
-                           --  using "or else".
-
-                           if Present (Class_Pre) then
-                              Merge_Preconditions (Item, Class_Pre);
-                           else
-                              Class_Pre := Item;
-                           end if;
-                        end if;
-                     end if;
-
-                     Prag := Next_Pragma (Prag);
-                  end loop;
-               end if;
-            end loop;
-
-            --  Add the merged class-wide preconditions
-
-            if Present (Class_Pre) then
-               Prepend_To_Decls (Class_Pre);
-               Analyze (Class_Pre);
-            end if;
-         end Process_Inherited_Preconditions;
+         end Prepend_Pragma_To_Decls;
 
          -------------------------------
          -- Process_Preconditions_For --
@@ -2983,7 +2981,7 @@ package body Contracts is
                            N      => Body_Decl);
                      end if;
 
-                     Prepend_To_Decls_Or_Save (Prag);
+                     Prepend_Pragma_To_Decls (Prag);
                   end if;
 
                   Prag := Next_Pragma (Prag);
@@ -3008,7 +3006,7 @@ package body Contracts is
                      if Pragma_Name (Decl) = Name_Precondition
                        and then Is_Checked (Decl)
                      then
-                        Prepend_To_Decls_Or_Save (Decl);
+                        Prepend_Pragma_To_Decls (Decl);
                      end if;
 
                   --  Skip internally generated code
@@ -3073,22 +3071,21 @@ package body Contracts is
 
                Next (Decl);
             end loop;
-         end if;
 
-         --  The processing of preconditions is done in reverse order (body
-         --  first), because each pragma Check equivalent is inserted at the
-         --  top of the declarations. This ensures that the final order is
-         --  consistent with following diagram:
+            --  The processing of preconditions is done in reverse order (body
+            --  first), because each pragma Check equivalent is inserted at the
+            --  top of the declarations. This ensures that the final order is
+            --  consistent with following diagram:
 
-         --    <inherited preconditions>
-         --    <preconditions from spec>
-         --    <preconditions from body>
+            --    <inherited preconditions>
+            --    <preconditions from spec>
+            --    <preconditions from body>
 
-         Process_Preconditions_For (Body_Id);
+            Process_Preconditions_For (Body_Id);
+         end if;
 
          if Present (Spec_Id) then
             Process_Preconditions_For (Spec_Id);
-            Process_Inherited_Preconditions;
          end if;
       end Process_Preconditions;
 
@@ -3139,6 +3136,12 @@ package body Contracts is
       elsif Is_Ignored_Ghost_Entity (Subp_Id) then
          return;
 
+      --  No action needed for helpers and indirect-call wrapper built to
+      --  support class-wide preconditions.
+
+      elsif Present (Class_Preconditions_Subprogram (Subp_Id)) then
+         return;
+
       --  Do not re-expand the same contract. This scenario occurs when a
       --  construct is rewritten into something else during its analysis
       --  (expression functions for instance).
@@ -3605,6 +3608,1112 @@ package body Contracts is
       end if;
    end Instantiate_Subprogram_Contract;
 
+   -----------------------------------
+   -- Make_Class_Precondition_Subps --
+   -----------------------------------
+
+   procedure Make_Class_Precondition_Subps
+     (Subp_Id         : Entity_Id;
+      Late_Overriding : Boolean := False)
+   is
+      Loc         : constant Source_Ptr := Sloc (Subp_Id);
+      Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
+
+      procedure Add_Indirect_Call_Wrapper;
+      --  Build the indirect-call wrapper and append it to the freezing actions
+      --  of Tagged_Type.
+
+      procedure Add_Call_Helper
+        (Helper_Id  : Entity_Id;
+         Is_Dynamic : Boolean);
+      --  Factorizes code for building a call helper with the given identifier
+      --  and append it to the freezing actions of Tagged_Type. Is_Dynamic
+      --  controls building the static or dynamic version of the helper.
+
+      -------------------------------
+      -- Add_Indirect_Call_Wrapper --
+      -------------------------------
+
+      procedure Add_Indirect_Call_Wrapper is
+
+         function Build_ICW_Body return Node_Id;
+         --  Build the body of the indirect call wrapper
+
+         function Build_ICW_Decl return Node_Id;
+         --  Build the declaration of the indirect call wrapper
+
+         --------------------
+         -- Build_ICW_Body --
+         --------------------
+
+         function Build_ICW_Body return Node_Id is
+            ICW_Id    : constant Entity_Id := Indirect_Call_Wrapper (Subp_Id);
+            Spec      : constant Node_Id   := Parent (ICW_Id);
+            Body_Spec : Node_Id;
+            Call      : Node_Id;
+            ICW_Body  : Node_Id;
+
+         begin
+            Body_Spec := Copy_Subprogram_Spec (Spec);
+
+            --  Build call to wrapped subprogram
+
+            declare
+               Actuals     : constant List_Id := Empty_List;
+               Formal_Spec : Entity_Id :=
+                               First (Parameter_Specifications (Spec));
+            begin
+               --  Build parameter association & call
+
+               while Present (Formal_Spec) loop
+                  Append_To (Actuals,
+                    New_Occurrence_Of
+                      (Defining_Identifier (Formal_Spec), Loc));
+                  Next (Formal_Spec);
+               end loop;
+
+               if Ekind (ICW_Id) = E_Procedure then
+                  Call :=
+                    Make_Procedure_Call_Statement (Loc,
+                      Name => New_Occurrence_Of (Subp_Id, Loc),
+                      Parameter_Associations => Actuals);
+               else
+                  Call :=
+                    Make_Simple_Return_Statement (Loc,
+                      Expression =>
+                        Make_Function_Call (Loc,
+                          Name => New_Occurrence_Of (Subp_Id, Loc),
+                          Parameter_Associations => Actuals));
+               end if;
+            end;
+
+            ICW_Body :=
+              Make_Subprogram_Body (Loc,
+                Specification              => Body_Spec,
+                Declarations               => New_List,
+                Handled_Statement_Sequence =>
+                  Make_Handled_Sequence_Of_Statements (Loc,
+                    Statements => New_List (Call)));
+
+            --  The new operation is internal and overriding indicators do not
+            --  apply.
+
+            Set_Must_Override (Body_Spec, False);
+
+            return ICW_Body;
+         end Build_ICW_Body;
+
+         --------------------
+         -- Build_ICW_Decl --
+         --------------------
+
+         function Build_ICW_Decl return Node_Id is
+            ICW_Id : constant Entity_Id  :=
+                       Make_Defining_Identifier (Loc,
+                         New_External_Name (Chars (Subp_Id),
+                           Suffix       => "ICW",
+                           Suffix_Index => Source_Offset (Loc)));
+            Decl   : Node_Id;
+            Spec   : Node_Id;
+
+         begin
+            Spec := Copy_Subprogram_Spec (Parent (Subp_Id));
+            Set_Must_Override      (Spec, False);
+            Set_Must_Not_Override  (Spec, False);
+            Set_Defining_Unit_Name (Spec, ICW_Id);
+            Mutate_Ekind  (ICW_Id, Ekind (Subp_Id));
+            Set_Is_Public (ICW_Id);
+
+            --  The indirect call wrapper is commonly used for indirect calls
+            --  but inlined for direct calls performed from the DTW.
+
+            Set_Is_Inlined (ICW_Id);
+
+            if Nkind (Spec) = N_Procedure_Specification then
+               Set_Null_Present (Spec, False);
+            end if;
+
+            Decl := Make_Subprogram_Declaration (Loc, Spec);
+
+            --  Link original subprogram to indirect wrapper and vice versa
+
+            Set_Indirect_Call_Wrapper (Subp_Id, ICW_Id);
+            Set_Class_Preconditions_Subprogram (ICW_Id, Subp_Id);
+
+            --  Inherit debug info flag to allow debugging the wrapper
+
+            if Needs_Debug_Info (Subp_Id) then
+               Set_Debug_Info_Needed (ICW_Id);
+            end if;
+
+            return Decl;
+         end Build_ICW_Decl;
+
+         --  Local Variables
+
+         ICW_Body : Node_Id;
+         ICW_Decl : Node_Id;
+
+      --  Start of processing for Add_Indirect_Call_Wrapper
+
+      begin
+         pragma Assert (No (Indirect_Call_Wrapper (Subp_Id)));
+
+         ICW_Decl := Build_ICW_Decl;
+
+         Ensure_Freeze_Node (Tagged_Type);
+         Append_Freeze_Action (Tagged_Type, ICW_Decl);
+         Analyze (ICW_Decl);
+
+         ICW_Body := Build_ICW_Body;
+         Append_Freeze_Action (Tagged_Type, ICW_Body);
+
+         --  We cannot defer the analysis of this ICW wrapper when it is
+         --  built as a consequence of building its partner DTW wrapper
+         --  at the freezing point of the tagged type.
+
+         if Is_Dispatch_Table_Wrapper (Subp_Id) then
+            Analyze (ICW_Body);
+         end if;
+      end Add_Indirect_Call_Wrapper;
+
+      ---------------------
+      -- Add_Call_Helper --
+      ---------------------
+
+      procedure Add_Call_Helper
+        (Helper_Id  : Entity_Id;
+         Is_Dynamic : Boolean)
+      is
+         function Build_Call_Helper_Body return Node_Id;
+         --  Build the body of a call helper
+
+         function Build_Call_Helper_Decl return Node_Id;
+         --  Build the declaration of a call helper
+
+         function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id;
+         --  Build the specification of the helper
+
+         ----------------------------
+         -- Build_Call_Helper_Body --
+         ----------------------------
+
+         function Build_Call_Helper_Body return Node_Id is
+
+            function Copy_And_Update_References
+              (Expr : Node_Id) return Node_Id;
+            --  Copy Expr updating references to formals of Helper_Id; update
+            --  also references to loop identifiers of quantified expressions.
+
+            --------------------------------
+            -- Copy_And_Update_References --
+            --------------------------------
+
+            function Copy_And_Update_References
+              (Expr : Node_Id) return Node_Id
+            is
+               Assoc_List : constant Elist_Id := New_Elmt_List;
+
+               procedure Map_Quantified_Expression_Loop_Identifiers;
+               --  Traverse Expr and append to Assoc_List the mapping of loop
+               --  identifers of quantified expressions with its new copy.
+
+               ------------------------------------------------
+               -- Map_Quantified_Expression_Loop_Identifiers --
+               ------------------------------------------------
+
+               procedure Map_Quantified_Expression_Loop_Identifiers is
+                  function Map_Loop_Param (N : Node_Id) return Traverse_Result;
+                  --  Append to Assoc_List the mapping of loop identifers of
+                  --  quantified expressions with its new copy.
+
+                  --------------------
+                  -- Map_Loop_Param --
+                  --------------------
+
+                  function Map_Loop_Param (N : Node_Id) return Traverse_Result
+                  is
+                  begin
+                     if Nkind (N) = N_Loop_Parameter_Specification
+                       and then Nkind (Parent (N)) = N_Quantified_Expression
+                     then
+                        declare
+                           Def_Id : constant Entity_Id :=
+                                      Defining_Identifier (N);
+                        begin
+                           Append_Elmt (Def_Id, Assoc_List);
+                           Append_Elmt (New_Copy (Def_Id), Assoc_List);
+                        end;
+                     end if;
+
+                     return OK;
+                  end Map_Loop_Param;
+
+                  procedure Map_Quantified_Expressions is
+                     new Traverse_Proc (Map_Loop_Param);
+
+               begin
+                  Map_Quantified_Expressions (Expr);
+               end Map_Quantified_Expression_Loop_Identifiers;
+
+               --  Local variables
+
+               Subp_Formal_Id   : Entity_Id := First_Formal (Subp_Id);
+               Helper_Formal_Id : Entity_Id := First_Formal (Helper_Id);
+
+            --  Start of processing for Copy_And_Update_References
+
+            begin
+               while Present (Subp_Formal_Id) loop
+                  Append_Elmt (Subp_Formal_Id,   Assoc_List);
+                  Append_Elmt (Helper_Formal_Id, Assoc_List);
+
+                  Next_Formal (Subp_Formal_Id);
+                  Next_Formal (Helper_Formal_Id);
+               end loop;
+
+               Map_Quantified_Expression_Loop_Identifiers;
+
+               return New_Copy_Tree (Expr, Map => Assoc_List);
+            end Copy_And_Update_References;
+
+            --  Local variables
+
+            Helper_Decl : constant Node_Id := Parent (Parent (Helper_Id));
+            Body_Id     : Entity_Id;
+            Body_Spec   : Node_Id;
+            Body_Stmts  : Node_Id;
+            Helper_Body : Node_Id;
+            Return_Expr : Node_Id;
+
+         --  Start of processing for Build_Call_Helper_Body
+
+         begin
+            pragma Assert (Analyzed (Unit_Declaration_Node (Helper_Id)));
+            pragma Assert (No (Corresponding_Body (Helper_Decl)));
+
+            Body_Id   := Make_Defining_Identifier (Loc, Chars (Helper_Id));
+            Body_Spec := Build_Call_Helper_Spec (Body_Id);
+
+            Set_Corresponding_Body (Helper_Decl, Body_Id);
+            Set_Must_Override (Body_Spec, False);
+
+            if Present (Class_Preconditions (Subp_Id)) then
+               Return_Expr :=
+                 Copy_And_Update_References (Class_Preconditions (Subp_Id));
+
+            --  When the subprogram is compiled with assertions disabled the
+            --  helper just returns True; done to avoid reporting errors at
+            --  link time since a unit may be compiled with assertions disabled
+            --  and another (which depends on it) compiled with assertions
+            --  enabled.
+
+            else
+               pragma Assert (Present (Ignored_Class_Preconditions (Subp_Id)));
+               Return_Expr := New_Occurrence_Of (Standard_True, Loc);
+            end if;
+
+            Body_Stmts :=
+              Make_Handled_Sequence_Of_Statements (Loc,
+                Statements => New_List (
+                  Make_Simple_Return_Statement (Loc, Return_Expr)));
+
+            Helper_Body :=
+              Make_Subprogram_Body (Loc,
+                Specification              => Body_Spec,
+                Declarations               => New_List,
+                Handled_Statement_Sequence => Body_Stmts);
+
+            return Helper_Body;
+         end Build_Call_Helper_Body;
+
+         ----------------------------
+         -- Build_Call_Helper_Decl --
+         ----------------------------
+
+         function Build_Call_Helper_Decl return Node_Id is
+            Decl : Node_Id;
+            Spec : Node_Id;
+
+         begin
+            Spec := Build_Call_Helper_Spec (Helper_Id);
+            Set_Must_Override      (Spec, False);
+            Set_Must_Not_Override  (Spec, False);
+            Set_Is_Inlined (Helper_Id);
+            Set_Is_Public  (Helper_Id);
+
+            Decl := Make_Subprogram_Declaration (Loc, Spec);
+
+            --  Inherit debug info flag from Subp_Id to Helper_Id to allow
+            --  debugging of the helper subprogram.
+
+            if Needs_Debug_Info (Subp_Id) then
+               Set_Debug_Info_Needed (Helper_Id);
+            end if;
+
+            return Decl;
+         end Build_Call_Helper_Decl;
+
+         ----------------------------
+         -- Build_Call_Helper_Spec --
+         ----------------------------
+
+         function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id
+         is
+            Spec         : constant Node_Id := Parent (Subp_Id);
+            Def_Id       : constant Node_Id := Defining_Unit_Name (Spec);
+            Formal       : Entity_Id;
+            Func_Formals : constant List_Id := New_List;
+            P_Spec       : constant List_Id := Parameter_Specifications (Spec);
+            Par_Formal   : Node_Id;
+            Param        : Node_Id;
+            Param_Type   : Node_Id;
+
+         begin
+            --  Create a list of formal parameters with the same types as the
+            --  original subprogram but changing the controlling formal.
+
+            Param  := First (P_Spec);
+            Formal := First_Formal (Def_Id);
+            while Present (Formal) loop
+               Par_Formal := Parent (Formal);
+
+               if Is_Dynamic and then Is_Controlling_Formal (Formal) then
+                  if Nkind (Parameter_Type (Par_Formal))
+                    = N_Access_Definition
+                  then
+                     Param_Type :=
+                       Copy_Separate_Tree (Parameter_Type (Par_Formal));
+                     Rewrite (Subtype_Mark (Param_Type),
+                       Make_Attribute_Reference (Loc,
+                         Prefix => Relocate_Node (Subtype_Mark (Param_Type)),
+                         Attribute_Name => Name_Class));
+
+                  else
+                     Param_Type :=
+                       Make_Attribute_Reference (Loc,
+                         Prefix => New_Occurrence_Of (Etype (Formal), Loc),
+                         Attribute_Name => Name_Class);
+                  end if;
+               else
+                  Param_Type := New_Occurrence_Of (Etype (Formal), Loc);
+               end if;
+
+               Append_To (Func_Formals,
+                 Make_Parameter_Specification (Loc,
+                   Defining_Identifier    =>
+                     Make_Defining_Identifier (Loc, Chars (Formal)),
+                   In_Present             => In_Present (Par_Formal),
+                   Out_Present            => Out_Present (Par_Formal),
+                   Null_Exclusion_Present => Null_Exclusion_Present
+                                               (Par_Formal),
+                   Parameter_Type         => Param_Type));
+
+               Next (Param);
+               Next_Formal (Formal);
+            end loop;
+
+            return
+              Make_Function_Specification (Loc,
+                Defining_Unit_Name       => Spec_Id,
+                Parameter_Specifications => Func_Formals,
+                Result_Definition        =>
+                  New_Occurrence_Of (Standard_Boolean, Loc));
+         end Build_Call_Helper_Spec;
+
+         --  Local variables
+
+         Helper_Body : Node_Id;
+         Helper_Decl : Node_Id;
+
+      --  Start of processing for Add_Call_Helper
+
+      begin
+         Helper_Decl := Build_Call_Helper_Decl;
+         Mutate_Ekind (Helper_Id, Ekind (Subp_Id));
+
+         --  Add the helper to the freezing actions of the tagged type
+
+         Ensure_Freeze_Node   (Tagged_Type);
+         Append_Freeze_Action (Tagged_Type, Helper_Decl);
+         Analyze (Helper_Decl);
+
+         Helper_Body := Build_Call_Helper_Body;
+         Append_Freeze_Action (Tagged_Type, Helper_Body);
+
+         --  If this helper is built as part of building the DTW at the
+         --  freezing point of its tagged type then we cannot defer
+         --  its analysis.
+
+         if Late_Overriding then
+            pragma Assert (Is_Dispatch_Table_Wrapper (Subp_Id));
+            Analyze (Helper_Body);
+         end if;
+      end Add_Call_Helper;
+
+      --  Local variables
+
+      Helper_Id : Entity_Id;
+
+   --  Start of processing for Make_Class_Precondition_Subps
+
+   begin
+      if Present (Class_Preconditions (Subp_Id))
+        or Present (Ignored_Class_Preconditions (Subp_Id))
+      then
+         pragma Assert
+           (Comes_From_Source (Subp_Id)
+              or else Is_Dispatch_Table_Wrapper (Subp_Id));
+
+         if No (Dynamic_Call_Helper (Subp_Id)) then
+
+            --  Build and add to the freezing actions of Tagged_Type its
+            --  dynamic-call helper.
+
+            Helper_Id :=
+              Make_Defining_Identifier (Loc,
+                New_External_Name (Chars (Subp_Id),
+                Suffix       => "DP",
+                Suffix_Index => Source_Offset (Loc)));
+            Add_Call_Helper (Helper_Id, Is_Dynamic => True);
+
+            --  Link original subprogram to helper and vice versa
+
+            Set_Dynamic_Call_Helper (Subp_Id, Helper_Id);
+            Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
+         end if;
+
+         if not Is_Abstract_Subprogram (Subp_Id)
+           and then No (Static_Call_Helper (Subp_Id))
+         then
+            --  Build and add to the freezing actions of Tagged_Type its
+            --  static-call helper.
+
+            Helper_Id :=
+              Make_Defining_Identifier (Loc,
+                New_External_Name (Chars (Subp_Id),
+                Suffix       => "SP",
+                Suffix_Index => Source_Offset (Loc)));
+
+            Add_Call_Helper (Helper_Id, Is_Dynamic => False);
+
+            --  Link original subprogram to helper and vice versa
+
+            Set_Static_Call_Helper (Subp_Id, Helper_Id);
+            Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
+
+            --  Build and add to the freezing actions of Tagged_Type the
+            --  indirect-call wrapper.
+
+            Add_Indirect_Call_Wrapper;
+         end if;
+      end if;
+   end Make_Class_Precondition_Subps;
+
+   ----------------------------------------------
+   -- Process_Class_Conditions_At_Freeze_Point --
+   ----------------------------------------------
+
+   procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id) is
+
+      procedure Check_Class_Conditions (Spec_Id : Entity_Id);
+      --  Check class-wide pre/postconditions of Spec_Id
+
+      function Has_Class_Postconditions_Subprogram
+        (Spec_Id : Entity_Id) return Boolean;
+      --  Return True if Spec_Id has (or inherits) a postconditions subprogram.
+
+      function Has_Class_Preconditions_Subprogram
+        (Spec_Id : Entity_Id) return Boolean;
+      --  Return True if Spec_Id has (or inherits) a preconditions subprogram.
+
+      ----------------------------
+      -- Check_Class_Conditions --
+      ----------------------------
+
+      procedure Check_Class_Conditions (Spec_Id : Entity_Id) is
+         Par_Subp : Entity_Id;
+
+      begin
+         for Kind in Condition_Kind loop
+            Par_Subp := Nearest_Class_Condition_Subprogram (Kind, Spec_Id);
+
+            if Present (Par_Subp) then
+               Check_Class_Condition
+                 (Cond            => Class_Condition (Kind, Par_Subp),
+                  Subp            => Spec_Id,
+                  Par_Subp        => Par_Subp,
+                  Is_Precondition => Kind in Ignored_Class_Precondition
+                                           | Class_Precondition);
+            end if;
+         end loop;
+      end Check_Class_Conditions;
+
+      -----------------------------------------
+      -- Has_Class_Postconditions_Subprogram --
+      -----------------------------------------
+
+      function Has_Class_Postconditions_Subprogram
+        (Spec_Id : Entity_Id) return Boolean is
+      begin
+         return
+           Present (Nearest_Class_Condition_Subprogram
+                     (Spec_Id => Spec_Id,
+                      Kind    => Class_Postcondition))
+             or else
+           Present (Nearest_Class_Condition_Subprogram
+                     (Spec_Id => Spec_Id,
+                      Kind    => Ignored_Class_Postcondition));
+      end Has_Class_Postconditions_Subprogram;
+
+      ----------------------------------------
+      -- Has_Class_Preconditions_Subprogram --
+      ----------------------------------------
+
+      function Has_Class_Preconditions_Subprogram
+        (Spec_Id : Entity_Id) return Boolean is
+      begin
+         return
+           Present (Nearest_Class_Condition_Subprogram
+                     (Spec_Id => Spec_Id,
+                      Kind    => Class_Precondition))
+             or else
+           Present (Nearest_Class_Condition_Subprogram
+                     (Spec_Id => Spec_Id,
+                      Kind    => Ignored_Class_Precondition));
+      end Has_Class_Preconditions_Subprogram;
+
+      --  Local variables
+
+      Prim_Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ));
+      Prim      : Entity_Id;
+
+   --  Start of processing for Process_Class_Conditions_At_Freeze_Point
+
+   begin
+      while Present (Prim_Elmt) loop
+         Prim := Node (Prim_Elmt);
+
+         if Has_Class_Preconditions_Subprogram (Prim)
+           or else Has_Class_Postconditions_Subprogram (Prim)
+         then
+            if Comes_From_Source (Prim) then
+               if Has_Significant_Contract (Prim) then
+                  Merge_Class_Conditions (Prim);
+               end if;
+
+            --  Handle wrapper of protected operation
+
+            elsif Is_Primitive_Wrapper (Prim) then
+               Merge_Class_Conditions (Prim);
+
+            --  Check inherited class-wide conditions, excluding internal
+            --  entities built for mapping of interface primitives.
+
+            elsif Is_Derived_Type (Typ)
+              and then Present (Alias (Prim))
+              and then No (Interface_Alias (Prim))
+            then
+               Check_Class_Conditions (Prim);
+            end if;
+         end if;
+
+         Next_Elmt (Prim_Elmt);
+      end loop;
+   end Process_Class_Conditions_At_Freeze_Point;
+
+   ----------------------------
+   -- Merge_Class_Conditions --
+   ----------------------------
+
+   procedure Merge_Class_Conditions (Spec_Id : Entity_Id) is
+
+      procedure Preanalyze_Condition
+        (Subp : Entity_Id;
+         Expr : Node_Id);
+      --  Preanalyze the class-wide condition Expr of Subp
+
+      procedure Process_Inherited_Conditions (Kind : Condition_Kind);
+      --  Collect all inherited class-wide conditions of Spec_Id and merge
+      --  them into one big condition.
+
+      --------------------------
+      -- Preanalyze_Condition --
+      --------------------------
+
+      procedure Preanalyze_Condition
+        (Subp : Entity_Id;
+         Expr : Node_Id)
+      is
+         procedure Clear_Unset_References;
+         --  Clear unset references on formals of Subp since preanalysis
+         --  occurs in a place unrelated to the actual code.
+
+         procedure Remove_Controlling_Arguments;
+         --  Traverse Expr and clear the Controlling_Argument of calls to
+         --  nonabstract functions.
+
+         procedure Remove_Formals (Id : Entity_Id);
+         --  Remove formals from homonym chains and make them not visible
+
+         ----------------------------
+         -- Clear_Unset_References --
+         ----------------------------
+
+         procedure Clear_Unset_References is
+            F : Entity_Id := First_Formal (Subp);
+
+         begin
+            while Present (F) loop
+               Set_Unset_Reference (F, Empty);
+               Next_Formal (F);
+            end loop;
+         end Clear_Unset_References;
+
+         ----------------------------------
+         -- Remove_Controlling_Arguments --
+         ----------------------------------
+
+         procedure Remove_Controlling_Arguments is
+            function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result;
+            --  Reset the Controlling_Argument of calls to nonabstract
+            --  function calls.
+
+            ---------------------
+            -- Remove_Ctrl_Arg --
+            ---------------------
+
+            function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result is
+            begin
+               if Nkind (N) = N_Function_Call
+                 and then Present (Controlling_Argument (N))
+                 and then not Is_Abstract_Subprogram (Entity (Name (N)))
+               then
+                  Set_Controlling_Argument (N, Empty);
+               end if;
+
+               return OK;
+            end Remove_Ctrl_Arg;
+
+            procedure Remove_Ctrl_Args is new Traverse_Proc (Remove_Ctrl_Arg);
+         begin
+            Remove_Ctrl_Args (Expr);
+         end Remove_Controlling_Arguments;
+
+         --------------------
+         -- Remove_Formals --
+         --------------------
+
+         procedure Remove_Formals (Id : Entity_Id) is
+            F : Entity_Id := First_Formal (Id);
+
+         begin
+            while Present (F) loop
+               Set_Is_Immediately_Visible (F, False);
+               Remove_Homonym (F);
+               Next_Formal (F);
+            end loop;
+         end Remove_Formals;
+
+      --  Start of processing for Preanalyze_Condition
+
+      begin
+         pragma Assert (Present (Expr));
+         pragma Assert (Inside_Class_Condition_Preanalysis = False);
+
+         Push_Scope (Subp);
+         Install_Formals (Subp);
+         Inside_Class_Condition_Preanalysis := True;
+
+         Preanalyze_And_Resolve (Expr, Standard_Boolean);
+
+         Inside_Class_Condition_Preanalysis := False;
+         Remove_Formals (Subp);
+         Pop_Scope;
+
+         --  Traverse Expr and clear the Controlling_Argument of calls to
+         --  nonabstract functions. Required since the preanalyzed condition
+         --  is not yet installed on its definite context and will be cloned
+         --  and extended in derivations with additional conditions.
+
+         Remove_Controlling_Arguments;
+
+         --  Clear also attribute Unset_Reference; again because preanalysis
+         --  occurs in a place unrelated to the actual code.
+
+         Clear_Unset_References;
+      end Preanalyze_Condition;
+
+      ----------------------------------
+      -- Process_Inherited_Conditions --
+      ----------------------------------
+
+      procedure Process_Inherited_Conditions (Kind : Condition_Kind) is
+         Tag_Typ : constant Entity_Id       := Find_Dispatching_Type (Spec_Id);
+         Subps   : constant Subprogram_List := Inherited_Subprograms (Spec_Id);
+         Seen    : Subprogram_List (Subps'Range) := (others => Empty);
+
+         function Inherit_Condition
+           (Par_Subp : Entity_Id;
+            Subp     : Entity_Id) return Node_Id;
+         --  Inherit the class-wide condition from Par_Subp to Subp and adjust
+         --  all the references to formals in the inherited condition.
+
+         procedure Merge_Conditions (From : Node_Id; Into : Node_Id);
+         --  Merge two class-wide preconditions or postconditions (the former
+         --  are merged using "or else", and the latter are merged using "and-
+         --  then"). The changes are accumulated in parameter Into.
+
+         function Seen_Subp (Id : Entity_Id) return Boolean;
+         --  Return True if the contract of subprogram Id has been processed
+
+         -----------------------
+         -- Inherit_Condition --
+         -----------------------
+
+         function Inherit_Condition
+           (Par_Subp : Entity_Id;
+            Subp     : Entity_Id) return Node_Id
+         is
+            Installed_Calls : constant Elist_Id := New_Elmt_List;
+
+            procedure Install_Original_Selected_Component (Expr : Node_Id);
+            --  Traverse the given expression searching for dispatching calls
+            --  to functions whose original nodes was a selected component,
+            --  and replacing them temporarily by a copy of their original
+            --  node. Modified calls are stored in the list Installed_Calls
+            --  (to undo this work later).
+
+            procedure Restore_Dispatching_Calls (Expr : Node_Id);
+            --  Undo the work done by Install_Original_Selected_Component.
+
+            -----------------------------------------
+            -- Install_Original_Selected_Component --
+            -----------------------------------------
+
+            procedure Install_Original_Selected_Component (Expr : Node_Id) is
+               function Install_Node (N : Node_Id) return Traverse_Result;
+               --  Process a single node
+
+               ------------------
+               -- Install_Node --
+               ------------------
+
+               function Install_Node (N : Node_Id) return Traverse_Result is
+                  New_N    : Node_Id;
+                  Orig_Nod : Node_Id;
+
+               begin
+                  if Nkind (N) = N_Function_Call
+                    and then Nkind (Original_Node (N)) = N_Selected_Component
+                    and then Is_Dispatching_Operation (Entity (Name (N)))
+                  then
+                     Orig_Nod := Original_Node (N);
+
+                     --  Temporarily use the original node field to keep the
+                     --  reference to this node (to undo this work later!).
+
+                     New_N := New_Copy (N);
+                     Set_Original_Node (New_N, Orig_Nod);
+                     Append_Elmt (New_N, Installed_Calls);
+
+                     Rewrite (N, Orig_Nod);
+                     Set_Original_Node (N, New_N);
+                  end if;
+
+                  return OK;
+               end Install_Node;
+
+               procedure Install_Nodes is new Traverse_Proc (Install_Node);
+
+            begin
+               Install_Nodes (Expr);
+            end Install_Original_Selected_Component;
+
+            -------------------------------
+            -- Restore_Dispatching_Calls --
+            -------------------------------
+
+            procedure Restore_Dispatching_Calls (Expr : Node_Id) is
+               function Restore_Node (N : Node_Id) return Traverse_Result;
+               --  Process a single node
+
+               ------------------
+               -- Restore_Node --
+               ------------------
+
+               function Restore_Node (N : Node_Id) return Traverse_Result is
+                  Orig_Sel_N : Node_Id;
+
+               begin
+                  if Nkind (N) = N_Selected_Component
+                    and then Nkind (Original_Node (N)) = N_Function_Call
+                    and then Contains (Installed_Calls, Original_Node (N))
+                  then
+                     Orig_Sel_N := Original_Node (Original_Node (N));
+                     pragma Assert (Nkind (Orig_Sel_N) = N_Selected_Component);
+                     Rewrite (N, Original_Node (N));
+                     Set_Original_Node (N, Orig_Sel_N);
+                  end if;
+
+                  return OK;
+               end Restore_Node;
+
+               procedure Restore_Nodes is new Traverse_Proc (Restore_Node);
+
+            begin
+               Restore_Nodes (Expr);
+            end Restore_Dispatching_Calls;
+
+            --  Local variables
+
+            Assoc_List     : constant Elist_Id := New_Elmt_List;
+            Par_Formal_Id  : Entity_Id := First_Formal (Par_Subp);
+            Subp_Formal_Id : Entity_Id := First_Formal (Subp);
+            New_Expr       : Node_Id;
+            Class_Cond     : Node_Id;
+
+         --  Start of processing for Inherit_Condition
+
+         begin
+            while Present (Par_Formal_Id) loop
+               Append_Elmt (Par_Formal_Id,  Assoc_List);
+               Append_Elmt (Subp_Formal_Id, Assoc_List);
+
+               Next_Formal (Par_Formal_Id);
+               Next_Formal (Subp_Formal_Id);
+            end loop;
+
+            --  In order to properly preanalyze an inherited preanalyzed
+            --  condition that has occurrences of the Object.Operation
+            --  notation we must restore the original node; otherwise we
+            --  would report spurious errors.
+
+            Class_Cond := Class_Condition (Kind, Par_Subp);
+
+            Install_Original_Selected_Component (Class_Cond);
+            New_Expr := New_Copy_Tree (Class_Cond);
+            Restore_Dispatching_Calls (Class_Cond);
+
+            return New_Copy_Tree (New_Expr, Map => Assoc_List);
+         end Inherit_Condition;
+
+         ----------------------
+         -- Merge_Conditions --
+         ----------------------
+
+         procedure Merge_Conditions (From : Node_Id; Into : Node_Id) is
+            function Expression_Arg (Expr : Node_Id) return Node_Id;
+            --  Return the boolean expression argument of a condition while
+            --  updating its parentheses count for the subsequent merge.
+
+            --------------------
+            -- Expression_Arg --
+            --------------------
+
+            function Expression_Arg (Expr : Node_Id) return Node_Id is
+            begin
+               if Paren_Count (Expr) = 0 then
+                  Set_Paren_Count (Expr, 1);
+               end if;
+
+               return Expr;
+            end Expression_Arg;
+
+            --  Local variables
+
+            From_Expr : constant Node_Id := Expression_Arg (From);
+            Into_Expr : constant Node_Id := Expression_Arg (Into);
+            Loc       : constant Source_Ptr := Sloc (Into);
+
+         --  Start of processing for Merge_Conditions
+
+         begin
+            case Kind is
+
+               --  Merge the two preconditions by "or else"-ing them
+
+               when Ignored_Class_Precondition
+                  | Class_Precondition
+               =>
+                  Rewrite (Into_Expr,
+                    Make_Or_Else (Loc,
+                      Right_Opnd => Relocate_Node (Into_Expr),
+                      Left_Opnd  => From_Expr));
+
+               --  Merge the two postconditions by "and then"-ing them
+
+               when Ignored_Class_Postcondition
+                  | Class_Postcondition
+               =>
+                  Rewrite (Into_Expr,
+                    Make_And_Then (Loc,
+                      Right_Opnd => Relocate_Node (Into_Expr),
+                      Left_Opnd  => From_Expr));
+            end case;
+         end Merge_Conditions;
+
+         ---------------
+         -- Seen_Subp --
+         ---------------
+
+         function Seen_Subp (Id : Entity_Id) return Boolean is
+         begin
+            for Index in Seen'Range loop
+               if Seen (Index) = Id then
+                  return True;
+               end if;
+            end loop;
+
+            return False;
+         end Seen_Subp;
+
+         --  Local variables
+
+         Class_Cond      : Node_Id;
+         Cond            : Node_Id;
+         Subp_Id         : Entity_Id;
+         Par_Prim        : Entity_Id := Empty;
+         Par_Iface_Prims : Elist_Id  := No_Elist;
+
+      --  Start of processing for Process_Inherited_Conditions
+
+      begin
+         Class_Cond := Class_Condition (Kind, Spec_Id);
+
+         --  Process parent primitives looking for nearest ancestor with
+         --  class-wide conditions.
+
+         for Index in Subps'Range loop
+            Subp_Id := Subps (Index);
+
+            if No (Par_Prim)
+              and then Is_Ancestor (Find_Dispatching_Type (Subp_Id), Tag_Typ)
+            then
+               if Present (Alias (Subp_Id)) then
+                  Subp_Id := Ultimate_Alias (Subp_Id);
+               end if;
+
+               --  Wrappers of class-wide pre/postconditions reference the
+               --  parent primitive that has the inherited contract and help
+               --  us to climb fast.
+
+               if Is_Wrapper (Subp_Id)
+                 and then Present (LSP_Subprogram (Subp_Id))
+               then
+                  Subp_Id := LSP_Subprogram (Subp_Id);
+               end if;
+
+               if not Seen_Subp (Subp_Id)
+                 and then Present (Class_Condition (Kind, Subp_Id))
+               then
+                  Seen (Index)    := Subp_Id;
+                  Par_Prim        := Subp_Id;
+                  Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim);
+
+                  Cond := Inherit_Condition
+                            (Subp     => Spec_Id,
+                             Par_Subp => Subp_Id);
+
+                  if Present (Class_Cond) then
+                     Merge_Conditions (Cond, Class_Cond);
+                  else
+                     Class_Cond := Cond;
+                  end if;
+
+                  Check_Class_Condition
+                    (Cond            => Class_Cond,
+                     Subp            => Spec_Id,
+                     Par_Subp        => Subp_Id,
+                     Is_Precondition => Kind in Ignored_Class_Precondition
+                                              | Class_Precondition);
+                  Build_Class_Wide_Expression
+                    (Pragma_Or_Expr  => Class_Cond,
+                     Subp            => Spec_Id,
+                     Par_Subp        => Subp_Id,
+                     Adjust_Sloc     => False);
+
+                  --  We are done as soon as we process the nearest ancestor
+
+                  exit;
+               end if;
+            end if;
+         end loop;
+
+         --  Process the contract of interface primitives not covered by
+         --  the nearest ancestor.
+
+         for Index in Subps'Range loop
+            Subp_Id := Subps (Index);
+
+            if Is_Interface (Find_Dispatching_Type (Subp_Id)) then
+               if Present (Alias (Subp_Id)) then
+                  Subp_Id := Ultimate_Alias (Subp_Id);
+               end if;
+
+               if not Seen_Subp (Subp_Id)
+                 and then Present (Class_Condition (Kind, Subp_Id))
+                 and then not Contains (Par_Iface_Prims, Subp_Id)
+               then
+                  Seen (Index) := Subp_Id;
+
+                  Cond := Inherit_Condition
+                            (Subp     => Spec_Id,
+                             Par_Subp => Subp_Id);
+
+                  Check_Class_Condition
+                    (Cond            => Cond,
+                     Subp            => Spec_Id,
+                     Par_Subp        => Subp_Id,
+                     Is_Precondition => Kind in Ignored_Class_Precondition
+                                              | Class_Precondition);
+                  Build_Class_Wide_Expression
+                    (Pragma_Or_Expr  => Cond,
+                     Subp            => Spec_Id,
+                     Par_Subp        => Subp_Id,
+                     Adjust_Sloc     => False);
+
+                  if Present (Class_Cond) then
+                     Merge_Conditions (Cond, Class_Cond);
+                  else
+                     Class_Cond := Cond;
+                  end if;
+               end if;
+            end if;
+         end loop;
+
+         Set_Class_Condition (Kind, Spec_Id, Class_Cond);
+      end Process_Inherited_Conditions;
+
+      --  Local variables
+
+      Cond : Node_Id;
+
+   --  Start of processing for Merge_Class_Conditions
+
+   begin
+      for Kind in Condition_Kind loop
+         Cond := Class_Condition (Kind, Spec_Id);
+
+         --  If this subprogram has class-wide conditions then preanalyze
+         --  them before processing inherited conditions since conditions
+         --  are checked and merged from right to left.
+
+         if Present (Cond) then
+            Preanalyze_Condition (Spec_Id, Cond);
+         end if;
+
+         Process_Inherited_Conditions (Kind);
+
+         --  Preanalyze merged inherited conditions
+
+         if Cond /= Class_Condition (Kind, Spec_Id) then
+            Preanalyze_Condition (Spec_Id,
+              Class_Condition (Kind, Spec_Id));
+         end if;
+      end loop;
+   end Merge_Class_Conditions;
+
    ----------------------------------------
    -- Save_Global_References_In_Contract --
    ----------------------------------------
@@ -3622,10 +4731,9 @@ package body Contracts is
       ------------------------------------
 
       procedure Save_Global_References_In_List (First_Prag : Node_Id) is
-         Prag : Node_Id;
+         Prag : Node_Id := First_Prag;
 
       begin
-         Prag := First_Prag;
          while Present (Prag) loop
             if Is_Generic_Contract_Pragma (Prag) then
                Save_Global_References (Prag);
@@ -3662,4 +4770,29 @@ package body Contracts is
       Pop_Scope;
    end Save_Global_References_In_Contract;
 
+   -------------------------
+   -- Set_Class_Condition --
+   -------------------------
+
+   procedure Set_Class_Condition
+     (Kind : Condition_Kind;
+      Subp : Entity_Id;
+      Cond : Node_Id)
+   is
+   begin
+      case Kind is
+         when Class_Postcondition =>
+            Set_Class_Postconditions (Subp, Cond);
+
+         when Class_Precondition =>
+            Set_Class_Preconditions (Subp, Cond);
+
+         when Ignored_Class_Postcondition =>
+            Set_Ignored_Class_Postconditions (Subp, Cond);
+
+         when Ignored_Class_Precondition =>
+            Set_Ignored_Class_Preconditions (Subp, Cond);
+      end case;
+   end Set_Class_Condition;
+
 end Contracts;