[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.

26 files changed, 2804 insertions, 974 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;
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index bfd482e..eb26ebf 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -216,6 +216,31 @@ package Contracts is
    --  subprogram declaration template denoted by Templ. The instantiated
    --  pragmas are added to list L.
 
+   procedure Make_Class_Precondition_Subps
+     (Subp_Id         : Entity_Id;
+      Late_Overriding : Boolean := False);
+   --  Build helpers that at run time evaluate statically and dynamically the
+   --  class-wide preconditions of Subp_Id; build also the indirect-call
+   --  wrapper (ICW) required to check class-wide preconditions when the
+   --  subprogram is invoked through an access-to-subprogram, or when it
+   --  overrides an inherited class-wide precondition (see AI12-0195-1).
+   --  Late_Overriding enables special handling required for late-overriding
+   --  subprograms.
+
+   procedure Merge_Class_Conditions (Spec_Id : Entity_Id);
+   --  Merge and preanalyze all class-wide conditions of Spec_Id (class-wide
+   --  preconditions merged with operator or-else; class-wide postconditions
+   --  merged with operator and-then). Ignored pre/postconditions are also
+   --  merged since, although they are not required to generate code, their
+   --  preanalysis is required to perform semantic checks. Resulting merged
+   --  expressions are later installed by the expander in helper subprograms
+   --  which are invoked from the caller side; they are also used to build
+   --  the dispatch-table wrapper (DTW), if required.
+
+   procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id);
+   --  Merge, preanalyze, and check class-wide pre/postconditions of Typ
+   --  primitives.
+
    procedure Save_Global_References_In_Contract
      (Templ  : Node_Id;
       Gen_Id : Entity_Id);
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 94c5662..f890fe5 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -610,12 +610,23 @@ package Einfo is
 --       tables must be consulted to determine if there actually is an active
 --       Suppress or Unsuppress pragma that applies to the entity.
 
---    Class_Wide_Clone
---       Defined on subprogram entities. Set if the subprogram has a class-wide
---       pre- or postcondition, and the expression contains calls to other
---       primitive funtions of the type. Used to implement properly the
---       semantics of inherited operations whose class-wide condition may
---       be different from that of the ancestor (See AI012-0195).
+--    Class_Postconditions
+--       Defined on subprogram entities. Set if the subprogram has class-wide
+--       postconditions. Denotes the (and-then) expression built by merging
+--       inherited class-wide postconditions with its own class-wide
+--       postconditions.
+
+--    Class_Preconditions
+--       Defined on subprogram entities. Set if the subprogram has class-wide
+--       preconditions. Denotes the (or-else) expression built by merging
+--       inherited class-wide preconditions with its own class-wide
+--       preconditions.
+
+--    Class_Preconditions_Subprogram
+--       Defined on subprogram entities. Set on subprogram helpers and also on
+--       the indirect-call wrapper internally built for subprograms that have
+--       class-wide preconditions. References the subprogram that has the
+--       class-wide preconditions.
 
 --    Class_Wide_Type
 --       Defined in all type entities. For a tagged type or subtype, returns
@@ -1029,6 +1040,11 @@ package Einfo is
 --       associated with the tagged type. For an untagged record, contains
 --       No_Elist.
 
+--    Dynamic_Call_Helper
+--       Defined on subprogram entities. Set if the subprogram has class-wide
+--       preconditions. Denotes the helper that evaluates at run time the
+--       class-wide preconditions performing dispatching calls.
+
 --    DTC_Entity
 --       Defined in function and procedure entities. Set to Empty unless
 --       the subprogram is dispatching in which case it references the
@@ -2182,6 +2198,18 @@ package Einfo is
 --       "off" and indicates that all SPARK_Mode pragmas found within must
 --       be ignored.
 
+--    Ignored_Class_Postconditions
+--       Defined on subprogram entities. Set if the subprogram has class-wide
+--       postconditions. Denotes the (and-then) expression built by merging
+--       inherited ignored class-wide postconditions with its own ignored
+--       class-wide postconditions.
+
+--    Ignored_Class_Preconditions
+--       Defined on subprogram entities. Set if the subprogram has class-wide
+--       preconditions. Denotes the (or-else) expression built by merging
+--       inherited ignored class-wide preconditions with its own ignored
+--       class-wide preconditions.
+
 --    Implementation_Base_Type (synthesized)
 --       Applies to all entities. For types, similar to Base_Type, but never
 --       returns a private type when applied to a non-private type. Instead in
@@ -2216,6 +2244,12 @@ package Einfo is
 --       is relocated to the corresponding package body, which must have a
 --       corresponding nonlimited with_clause.
 
+--    Indirect_Call_Wrapper
+--       Defined on subprogram entities. Set if the subprogram has class-wide
+--       preconditions. Denotes the internal wrapper that checks preconditions
+--       and invokes the subprogram body. Subp'Access points to the indirect
+--       call wrapper if available.
+
 --    Initialization_Statements
 --       Defined in constants and variables. For a composite object initialized
 --       with an aggregate that has been converted to a sequence of
@@ -2507,6 +2541,11 @@ package Einfo is
 --       Applies to all entities. Set to indicate to the backend that this
 --       entity is associated with a dispatch table.
 
+--    Is_Dispatch_Table_Wrapper
+--       Applies to all entities. Set on wrappers built when the subprogram has
+--       class-wide preconditions or class-wide postconditions affected by
+--       overriding (AI12-0195).
+
 --    Is_Dispatching_Operation
 --       Defined in all entities. Set for procedures, functions, generic
 --       procedures, and generic functions if the corresponding operation
@@ -4401,6 +4440,11 @@ package Einfo is
 --       Default_Scalar_Storage_Order (High_Order_First) was active at the time
 --       the record or array was declared and therefore applies to it.
 
+--    Static_Call_Helper
+--       Defined on subprogram entities. Set if the subprogram has class-wide
+--       preconditions. Denotes the helper that evaluates at runtime the
+--       class-wide preconditions performing static calls.
+
 --    Static_Discrete_Predicate
 --       Defined in discrete types/subtypes with static predicates (with the
 --       two flags Has_Predicates and Has_Static_Predicate set). Set if the
@@ -4878,6 +4922,7 @@ package Einfo is
    --    Is_Discrim_SO_Function
    --    Is_Discriminant_Check_Function
    --    Is_Dispatch_Table_Entity
+   --    Is_Dispatch_Table_Wrapper
    --    Is_Dispatching_Operation
    --    Is_Entry_Formal
    --    Is_Exported
@@ -5484,7 +5529,14 @@ package Einfo is
    --    Linker_Section_Pragma
    --    Contract
    --    Import_Pragma                        (non-generic case only)
-   --    Class_Wide_Clone
+   --    Class_Postconditions
+   --    Class_Preconditions
+   --    Class_Preconditions_Subprogram
+   --    Dynamic_Call_Helper
+   --    Ignored_Class_Preconditions
+   --    Ignored_Class_Postconditions
+   --    Indirect_Call_Wrapper
+   --    Static_Call_Helper
    --    Protected_Subprogram                 (non-generic case only)
    --    SPARK_Pragma
    --    Original_Protected_Subprogram
@@ -5840,7 +5892,14 @@ package Einfo is
    --    Linker_Section_Pragma
    --    Contract
    --    Import_Pragma                        (non-generic case only)
-   --    Class_Wide_Clone
+   --    Class_Postconditions
+   --    Class_Preconditions
+   --    Class_Preconditions_Subprogram
+   --    Dynamic_Call_Helper
+   --    Ignored_Class_Preconditions
+   --    Ignored_Class_Postconditions
+   --    Indirect_Call_Wrapper
+   --    Static_Call_Helper
    --    Protected_Subprogram                 (non-generic case only)
    --    SPARK_Pragma
    --    Original_Protected_Subprogram
diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index c962c2a..3e7bb83 100644
--- a/gcc/ada/exp_attr.adb
+++ b/gcc/ada/exp_attr.adb
@@ -2216,6 +2216,20 @@ package body Exp_Attr is
             if Is_Access_Protected_Subprogram_Type (Btyp) then
                Expand_Access_To_Protected_Op (N, Pref, Typ);
 
+            --  If prefix is a subprogram that has class-wide preconditions and
+            --  an indirect-call wrapper (ICW) of such subprogram is available
+            --  then replace the prefix by the ICW.
+
+            elsif Is_Access_Subprogram_Type (Btyp)
+              and then Is_Entity_Name (Pref)
+              and then Present (Class_Preconditions (Entity (Pref)))
+              and then Present (Indirect_Call_Wrapper (Entity (Pref)))
+            then
+               Rewrite (Pref,
+                 New_Occurrence_Of
+                   (Indirect_Call_Wrapper (Entity (Pref)), Loc));
+               Analyze_And_Resolve (N, Typ);
+
             --  If prefix is a type name, this is a reference to the current
             --  instance of the type, within its initialization procedure.
 
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index 45d5baf..418306f 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -26,6 +26,7 @@
 with Aspects;        use Aspects;
 with Atree;          use Atree;
 with Checks;         use Checks;
+with Contracts;      use Contracts;
 with Einfo;          use Einfo;
 with Einfo.Entities; use Einfo.Entities;
 with Einfo.Utils;    use Einfo.Utils;
@@ -5352,10 +5353,66 @@ package body Exp_Ch3 is
    -------------------------------
 
    procedure Expand_Freeze_Record_Type (N : Node_Id) is
+
+      procedure Build_Class_Condition_Subprograms (Typ : Entity_Id);
+      --  Create internal subprograms of Typ primitives that have class-wide
+      --  preconditions or postconditions; they are invoked by the caller to
+      --  evaluate the conditions.
+
       procedure Build_Variant_Record_Equality (Typ  : Entity_Id);
       --  Create An Equality function for the untagged variant record Typ and
       --  attach it to the TSS list.
 
+      procedure Register_Dispatch_Table_Wrappers (Typ : Entity_Id);
+      --  Register dispatch-table wrappers in the dispatch table of Typ
+
+      ---------------------------------------
+      -- Build_Class_Condition_Subprograms --
+      ---------------------------------------
+
+      procedure Build_Class_Condition_Subprograms (Typ : Entity_Id) is
+         Prim_List : constant Elist_Id := Primitive_Operations (Typ);
+         Prim_Elmt : Elmt_Id           := First_Elmt (Prim_List);
+         Prim      : Entity_Id;
+
+      begin
+         while Present (Prim_Elmt) loop
+            Prim := Node (Prim_Elmt);
+
+            --  Primitive with class-wide preconditions
+
+            if Comes_From_Source (Prim)
+              and then Has_Significant_Contract (Prim)
+              and then
+                (Present (Class_Preconditions (Prim))
+                   or else Present (Ignored_Class_Preconditions (Prim)))
+            then
+               if Expander_Active then
+                  Make_Class_Precondition_Subps (Prim);
+               end if;
+
+            --  Wrapper of a primitive that has or inherits class-wide
+            --  preconditions.
+
+            elsif Is_Primitive_Wrapper (Prim)
+              and then
+                (Present (Nearest_Class_Condition_Subprogram
+                           (Spec_Id => Prim,
+                            Kind    => Class_Precondition))
+                   or else
+                 Present (Nearest_Class_Condition_Subprogram
+                           (Spec_Id => Prim,
+                            Kind    => Ignored_Class_Precondition)))
+            then
+               if Expander_Active then
+                  Make_Class_Precondition_Subps (Prim);
+               end if;
+            end if;
+
+            Next_Elmt (Prim_Elmt);
+         end loop;
+      end Build_Class_Condition_Subprograms;
+
       -----------------------------------
       -- Build_Variant_Record_Equality --
       -----------------------------------
@@ -5417,6 +5474,27 @@ package body Exp_Ch3 is
          end if;
       end Build_Variant_Record_Equality;
 
+      --------------------------------------
+      -- Register_Dispatch_Table_Wrappers --
+      --------------------------------------
+
+      procedure Register_Dispatch_Table_Wrappers (Typ : Entity_Id) is
+         Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ));
+         Subp : Entity_Id;
+
+      begin
+         while Present (Elmt) loop
+            Subp := Node (Elmt);
+
+            if Is_Dispatch_Table_Wrapper (Subp) then
+               Append_Freeze_Actions (Typ,
+                 Register_Primitive (Sloc (Subp), Subp));
+            end if;
+
+            Next_Elmt (Elmt);
+         end loop;
+      end Register_Dispatch_Table_Wrappers;
+
       --  Local variables
 
       Typ      : constant Node_Id := Entity (N);
@@ -5666,6 +5744,13 @@ package body Exp_Ch3 is
 
                if not Building_Static_DT (Typ) then
                   Append_Freeze_Actions (Typ, Make_DT (Typ));
+
+                  --  Register dispatch table wrappers in the dispatch table.
+                  --  It could not be done when these wrappers were built
+                  --  because, at that stage, the dispatch table was not
+                  --  available.
+
+                  Register_Dispatch_Table_Wrappers (Typ);
                end if;
             end if;
 
@@ -5857,6 +5942,13 @@ package body Exp_Ch3 is
             end loop;
          end;
       end if;
+
+      --  Build internal subprograms of primitives with class-wide
+      --  pre/postconditions.
+
+      if Is_Tagged_Type (Typ) then
+         Build_Class_Condition_Subprograms (Typ);
+      end if;
    end Expand_Freeze_Record_Type;
 
    ------------------------------------
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 7717fa7..ffd1475 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -73,8 +73,10 @@ with Sem_Util;       use Sem_Util;
 with Sinfo;          use Sinfo;
 with Sinfo.Nodes;    use Sinfo.Nodes;
 with Sinfo.Utils;    use Sinfo.Utils;
+with Sinput;         use Sinput;
 with Snames;         use Snames;
 with Stand;          use Stand;
+with Stringt;        use Stringt;
 with Tbuild;         use Tbuild;
 with Uintp;          use Uintp;
 with Validsw;        use Validsw;
@@ -4065,7 +4067,7 @@ package body Exp_Ch6 is
             end;
          end if;
 
-         --  If the formal is class wide and the actual is an aggregate, force
+         --  If the formal is class-wide and the actual is an aggregate, force
          --  evaluation so that the back end who does not know about class-wide
          --  type, does not generate a temporary of the wrong size.
 
@@ -4250,6 +4252,16 @@ package body Exp_Ch6 is
          Expand_Interface_Actuals (Call_Node);
       end if;
 
+      --  Install class-wide preconditions runtime check when this is a
+      --  dispatching primitive that has or inherits class-wide preconditions;
+      --  otherwise no runtime check is installed.
+
+      if Nkind (Call_Node) in N_Subprogram_Call
+        and then Is_Dispatching_Operation (Subp)
+      then
+         Install_Class_Preconditions_Check (Call_Node);
+      end if;
+
       --  Deals with Dispatch_Call if we still have a call, before expanding
       --  extra actuals since this will be done on the re-analysis of the
       --  dispatching call. Note that we do not try to shorten the actual list
@@ -7855,18 +7867,6 @@ package body Exp_Ch6 is
       --  returned type may not be known yet (for private types).
 
       Compute_Returns_By_Ref (Subp);
-
-      --  When freezing a null procedure, analyze its delayed aspects now
-      --  because we may not have reached the end of the declarative list when
-      --  delayed aspects are normally analyzed. This ensures that dispatching
-      --  calls are properly rewritten when the generated _Postcondition
-      --  procedure is analyzed in the null procedure body.
-
-      if Nkind (Parent (Subp)) = N_Procedure_Specification
-        and then Null_Present (Parent (Subp))
-      then
-         Analyze_Entry_Or_Subprogram_Contract (Subp);
-      end if;
    end Freeze_Subprogram;
 
    --------------------------
@@ -8101,6 +8101,367 @@ package body Exp_Ch6 is
       end if;
    end Insert_Post_Call_Actions;
 
+   ---------------------------------------
+   -- Install_Class_Preconditions_Check --
+   ---------------------------------------
+
+   procedure Install_Class_Preconditions_Check (Call_Node : Node_Id) is
+      Loc : constant Source_Ptr := Sloc (Call_Node);
+
+      function Build_Dynamic_Check_Helper_Call return Node_Id;
+      --  Build call to the helper runtime function of the nearest ancestor
+      --  of the target subprogram that dynamically evaluates the merged
+      --  or-else preconditions.
+
+      function Build_Error_Message (Subp_Id : Entity_Id) return Node_Id;
+      --  Build message associated with the class-wide precondition of Subp_Id
+      --  indicating the call that caused it.
+
+      function Build_Static_Check_Helper_Call return Node_Id;
+      --  Build call to the helper runtime function of the nearest ancestor
+      --  of the target subprogram that dynamically evaluates the merged
+      --  or-else preconditions.
+
+      function Class_Preconditions_Subprogram
+        (Spec_Id : Entity_Id;
+         Dynamic : Boolean) return Node_Id;
+      --  Return the nearest ancestor of Spec_Id defining a helper function
+      --  that evaluates a combined or-else expression containing all the
+      --  inherited class-wide preconditions; Dynamic enables searching for
+      --  the helper that dynamically evaluates preconditions using dispatching
+      --  calls; if False it searches for the helper that statically evaluates
+      --  preconditions; return Empty when not available (which means that no
+      --  preconditions check is required).
+
+      -------------------------------------
+      -- Build_Dynamic_Check_Helper_Call --
+      -------------------------------------
+
+      function Build_Dynamic_Check_Helper_Call return Node_Id is
+         Spec_Id   : constant Entity_Id := Entity (Name (Call_Node));
+         CW_Subp   : constant Entity_Id :=
+                       Class_Preconditions_Subprogram (Spec_Id,
+                         Dynamic => True);
+         Helper_Id : constant Entity_Id :=
+                       Dynamic_Call_Helper (CW_Subp);
+         Actuals   : constant List_Id := New_List;
+         A         : Node_Id   := First_Actual (Call_Node);
+         F         : Entity_Id := First_Formal (Helper_Id);
+
+      begin
+         while Present (A) loop
+
+            --  Ensure that the evaluation of the actuals will not produce
+            --  side effects.
+
+            Remove_Side_Effects (A);
+
+            Append_To (Actuals, New_Copy_Tree (A));
+            Next_Formal (F);
+            Next_Actual (A);
+         end loop;
+
+         return
+           Make_Function_Call (Loc,
+             Name => New_Occurrence_Of (Helper_Id, Loc),
+             Parameter_Associations => Actuals);
+      end Build_Dynamic_Check_Helper_Call;
+
+      -------------------------
+      -- Build_Error_Message --
+      -------------------------
+
+      function Build_Error_Message (Subp_Id : Entity_Id) return Node_Id is
+
+         procedure Append_Message
+           (Id       : Entity_Id;
+            Is_First : in out Boolean);
+         --  Build the fragment of the message associated with subprogram Id;
+         --  Is_First facilitates identifying continuation messages.
+
+         --------------------
+         -- Append_Message --
+         --------------------
+
+         procedure Append_Message
+           (Id       : Entity_Id;
+            Is_First : in out Boolean)
+         is
+            Prag   : constant Node_Id := Get_Class_Wide_Pragma (Id,
+                                         Pragma_Precondition);
+            Msg    : Node_Id;
+            Str_Id : String_Id;
+
+         begin
+            if No (Prag) or else Is_Ignored (Prag) then
+               return;
+            end if;
+
+            Msg    := Expression (Last (Pragma_Argument_Associations (Prag)));
+            Str_Id := Strval (Msg);
+
+            if Is_First then
+               Is_First := False;
+
+               Append (Global_Name_Buffer, Strval (Msg));
+
+               if Id /= Subp_Id
+                 and then Name_Buffer (1 .. 19) = "failed precondition"
+               then
+                  Insert_Str_In_Name_Buffer ("inherited ", 8);
+               end if;
+
+            else
+               declare
+                  Str      : constant String := To_String (Str_Id);
+                  From_Idx : Integer;
+
+               begin
+                  Append (Global_Name_Buffer, ASCII.LF);
+                  Append (Global_Name_Buffer, "  or ");
+
+                  From_Idx := Name_Len;
+                  Append (Global_Name_Buffer, Str_Id);
+
+                  if Str (1 .. 19) = "failed precondition" then
+                     Insert_Str_In_Name_Buffer ("inherited ", From_Idx + 8);
+                  end if;
+               end;
+            end if;
+         end Append_Message;
+
+         --  Local variables
+
+         Str_Loc  : constant String := Build_Location_String (Loc);
+         Subps    : constant Subprogram_List :=
+                      Inherited_Subprograms (Subp_Id);
+         Is_First : Boolean := True;
+
+      --  Start of processing for Build_Error_Message
+
+      begin
+         Name_Len := 0;
+         Append_Message (Subp_Id, Is_First);
+
+         for Index in Subps'Range loop
+            Append_Message (Subps (Index), Is_First);
+         end loop;
+
+         if Present (Controlling_Argument (Call_Node)) then
+            Append (Global_Name_Buffer, " in dispatching call at ");
+         else
+            Append (Global_Name_Buffer, " in call at ");
+         end if;
+
+         Append (Global_Name_Buffer, Str_Loc);
+
+         return Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len));
+      end Build_Error_Message;
+
+      ------------------------------------
+      -- Build_Static_Check_Helper_Call --
+      ------------------------------------
+
+      function Build_Static_Check_Helper_Call return Node_Id is
+         Actuals   : constant List_Id := New_List;
+         A         : Node_Id;
+         Helper_Id : Entity_Id;
+         F         : Entity_Id;
+         CW_Subp   : Entity_Id;
+         Spec_Id   : constant Entity_Id := Entity (Name (Call_Node));
+
+      begin
+         --  The target is the wrapper built to support inheriting body but
+         --  overriding pre/postconditions (AI12-0195).
+
+         if Is_Dispatch_Table_Wrapper (Spec_Id) then
+            CW_Subp := Spec_Id;
+
+         --  Common case
+
+         else
+            CW_Subp := Class_Preconditions_Subprogram (Spec_Id,
+                         Dynamic => False);
+         end if;
+
+         Helper_Id := Static_Call_Helper (CW_Subp);
+
+         F := First_Formal (Helper_Id);
+         A := First_Actual (Call_Node);
+         while Present (A) loop
+
+            --  Ensure that the evaluation of the actuals will not produce
+            --  side effects.
+
+            Remove_Side_Effects (A);
+
+            if Is_Controlling_Actual (A)
+              and then Etype (F) /= Etype (A)
+            then
+               Append_To (Actuals,
+                 Make_Unchecked_Type_Conversion (Loc,
+                   New_Occurrence_Of (Etype (F), Loc),
+                   New_Copy_Tree (A)));
+            else
+               Append_To (Actuals, New_Copy_Tree (A));
+            end if;
+
+            Next_Formal (F);
+            Next_Actual (A);
+         end loop;
+
+         return
+           Make_Function_Call (Loc,
+             Name => New_Occurrence_Of (Helper_Id, Loc),
+             Parameter_Associations => Actuals);
+      end Build_Static_Check_Helper_Call;
+
+      ------------------------------------
+      -- Class_Preconditions_Subprogram --
+      ------------------------------------
+
+      function Class_Preconditions_Subprogram
+        (Spec_Id : Entity_Id;
+         Dynamic : Boolean) return Node_Id
+      is
+         Subp_Id : constant Entity_Id := Ultimate_Alias (Spec_Id);
+
+      begin
+         --  Prevent cascaded errors
+
+         if not Is_Dispatching_Operation (Subp_Id) then
+            return Empty;
+
+         --  No need to search if this subprogram has the helper we are
+         --  searching
+
+         elsif Dynamic then
+            if Present (Dynamic_Call_Helper (Subp_Id)) then
+               return Subp_Id;
+            end if;
+         else
+            if Present (Static_Call_Helper (Subp_Id)) then
+               return Subp_Id;
+            end if;
+         end if;
+
+         --  Process inherited subprograms looking for class-wide
+         --  preconditions.
+
+         declare
+            Subps   : constant Subprogram_List :=
+                        Inherited_Subprograms (Subp_Id);
+            Subp_Id : Entity_Id;
+
+         begin
+            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/postconditions 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;
+
+               if Dynamic then
+                  if Present (Dynamic_Call_Helper (Subp_Id)) then
+                     return Subp_Id;
+                  end if;
+               else
+                  if Present (Static_Call_Helper (Subp_Id)) then
+                     return Subp_Id;
+                  end if;
+               end if;
+            end loop;
+         end;
+
+         return Empty;
+      end Class_Preconditions_Subprogram;
+
+      --  Local variables
+
+      Dynamic_Check : constant Boolean :=
+                        Present (Controlling_Argument (Call_Node));
+      Class_Subp    : Entity_Id;
+      Cond          : Node_Id;
+      Subp          : Entity_Id;
+
+   --  Start of processing for Install_Class_Preconditions_Check
+
+   begin
+      --  Do not expand the check if we are compiling under restriction
+      --  No_Dispatching_Calls; the semantic analyzer has previously
+      --  notified the violation of this restriction.
+
+      if Dynamic_Check
+        and then Restriction_Active (No_Dispatching_Calls)
+      then
+         return;
+
+      --  Class-wide precondition check not needed in interface thunks since
+      --  they are installed in the dispatching call that caused invoking the
+      --  thunk.
+
+      elsif Is_Thunk (Current_Scope) then
+         return;
+      end if;
+
+      Subp := Entity (Name (Call_Node));
+
+      --  No check needed for this subprogram call if no class-wide
+      --  preconditions apply (or if the unique available preconditions
+      --  are ignored preconditions).
+
+      Class_Subp := Class_Preconditions_Subprogram (Subp, Dynamic_Check);
+
+      if No (Class_Subp)
+        or else No (Class_Preconditions (Class_Subp))
+      then
+         return;
+      end if;
+
+      --  Build and install the check
+
+      if Dynamic_Check then
+         Cond := Build_Dynamic_Check_Helper_Call;
+      else
+         Cond := Build_Static_Check_Helper_Call;
+      end if;
+
+      if Exception_Locations_Suppressed then
+         Insert_Action (Call_Node,
+           Make_If_Statement (Loc,
+             Condition       => Make_Op_Not (Loc, Cond),
+             Then_Statements => New_List (
+               Make_Raise_Statement (Loc,
+                 Name =>
+                   New_Occurrence_Of
+                     (RTE (RE_Assert_Failure), Loc)))));
+
+      --  Failed check with message indicating the failed precondition and the
+      --  call that caused it.
+
+      else
+         Insert_Action (Call_Node,
+           Make_If_Statement (Loc,
+             Condition       => Make_Op_Not (Loc, Cond),
+             Then_Statements => New_List (
+               Make_Procedure_Call_Statement (Loc,
+                 Name                   =>
+                   New_Occurrence_Of
+                     (RTE (RE_Raise_Assert_Failure), Loc),
+                 Parameter_Associations =>
+                   New_List (Build_Error_Message (Subp))))));
+      end if;
+   end Install_Class_Preconditions_Check;
+
    -----------------------------------
    -- Is_Build_In_Place_Result_Type --
    -----------------------------------
diff --git a/gcc/ada/exp_ch6.ads b/gcc/ada/exp_ch6.ads
index 76cec4d..196f7e6 100644
--- a/gcc/ada/exp_ch6.ads
+++ b/gcc/ada/exp_ch6.ads
@@ -121,6 +121,9 @@ package Exp_Ch6 is
    --  The returned node is the root of the procedure body which will replace
    --  the original function body, which is not needed for the C program.
 
+   procedure Install_Class_Preconditions_Check (Call_Node : Node_Id);
+   --  Install check of class-wide preconditions on the caller.
+
    function Is_Build_In_Place_Entity (E : Entity_Id) return Boolean;
    --  Ada 2005 (AI-318-02): Returns True if E is a BIP entity.
 
diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb
index 7cce41b..72f4e7c9 100644
--- a/gcc/ada/exp_disp.adb
+++ b/gcc/ada/exp_disp.adb
@@ -63,7 +63,6 @@ with Sem_Util;       use Sem_Util;
 with Sinfo;          use Sinfo;
 with Sinfo.Nodes;    use Sinfo.Nodes;
 with Sinfo.Utils;    use Sinfo.Utils;
-with Sinput;         use Sinput;
 with Snames;         use Snames;
 with Stand;          use Stand;
 with Stringt;        use Stringt;
@@ -697,233 +696,11 @@ package body Exp_Disp is
       Eq_Prim_Op      : Entity_Id := Empty;
       Controlling_Tag : Node_Id;
 
-      procedure Build_Class_Wide_Check (E : Entity_Id);
-      --  If the denoted subprogram has a class-wide precondition, generate a
-      --  check using that precondition before the dispatching call, because
-      --  this is the only class-wide precondition that applies to the call;
-      --  otherwise climb to the ancestors searching for the enclosing
-      --  overridden primitive of E that has a class-wide precondition (and
-      --  use it to generate the check).
-
       function New_Value (From : Node_Id) return Node_Id;
       --  From is the original Expression. New_Value is equivalent to a call
       --  to Duplicate_Subexpr with an explicit dereference when From is an
       --  access parameter.
 
-      ----------------------------
-      -- Build_Class_Wide_Check --
-      ----------------------------
-
-      procedure Build_Class_Wide_Check (E : Entity_Id) is
-         Subp : Entity_Id := E;
-
-         function Has_Class_Wide_Precondition
-           (Subp : Entity_Id) return Boolean;
-         --  Evaluates if the dispatching subprogram Subp has a class-wide
-         --  precondition.
-
-         function Replace_Formals (N : Node_Id) return Traverse_Result;
-         --  Replace occurrences of the formals of the subprogram by the
-         --  corresponding actuals in the call, given that this check is
-         --  performed outside of the body of the subprogram.
-
-         --  If the dispatching call appears in the same scope as the
-         --  declaration of the dispatching subprogram (for example in
-         --  the expression of a local expression function), the spec
-         --  has not been analyzed yet, in which case we use the Chars
-         --  field to recognize intended occurrences of the formals.
-
-         ---------------------------------
-         -- Has_Class_Wide_Precondition --
-         ---------------------------------
-
-         function Has_Class_Wide_Precondition
-           (Subp : Entity_Id) return Boolean
-         is
-            Prec : Node_Id := Empty;
-
-         begin
-            if Present (Contract (Subp))
-              and then Present (Pre_Post_Conditions (Contract (Subp)))
-            then
-               Prec := Pre_Post_Conditions (Contract (Subp));
-
-               while Present (Prec) loop
-                  exit when Pragma_Name (Prec) = Name_Precondition
-                    and then Class_Present (Prec);
-                  Prec := Next_Pragma (Prec);
-               end loop;
-            end if;
-
-            return Present (Prec)
-              and then not Is_Ignored (Prec);
-         end Has_Class_Wide_Precondition;
-
-         ---------------------
-         -- Replace_Formals --
-         ---------------------
-
-         function Replace_Formals (N : Node_Id) return Traverse_Result is
-            A : Node_Id;
-            F : Entity_Id;
-         begin
-            if Is_Entity_Name (N) then
-               F := First_Formal (Subp);
-               A := First_Actual (Call_Node);
-
-               if Present (Entity (N)) and then Is_Formal (Entity (N)) then
-                  while Present (F) loop
-                     if F = Entity (N) then
-                        if not Is_Controlling_Actual (N) then
-                           Rewrite (N, New_Copy_Tree (A));
-
-                           --  If the formal is class-wide, and thus not a
-                           --  controlling argument, preserve its type because
-                           --  it may appear in a nested call with a class-wide
-                           --  parameter.
-
-                           if Is_Class_Wide_Type (Etype (F)) then
-                              Set_Etype (N, Etype (F));
-
-                           --  Conversely, if this is a controlling argument
-                           --  (in a dispatching call in the condition) that
-                           --  is a dereference, the source is an access-to-
-                           --  -class-wide type, so preserve the dispatching
-                           --  nature of the call in the rewritten condition.
-
-                           elsif Nkind (Parent (N)) = N_Explicit_Dereference
-                             and then Is_Controlling_Actual (Parent (N))
-                           then
-                              Set_Controlling_Argument (Parent (Parent (N)),
-                                 Parent (N));
-                           end if;
-
-                        --  Ensure that the type of the controlling actual
-                        --  matches the type of the controlling formal of the
-                        --  parent primitive Subp defining the class-wide
-                        --  precondition.
-
-                        elsif Is_Class_Wide_Type (Etype (A)) then
-                           Rewrite (N,
-                             Convert_To
-                               (Class_Wide_Type (Etype (F)),
-                                New_Copy_Tree (A)));
-
-                        else
-                           Rewrite (N,
-                             Convert_To
-                               (Etype (F),
-                                New_Copy_Tree (A)));
-                        end if;
-
-                        exit;
-                     end if;
-
-                     Next_Formal (F);
-                     Next_Actual (A);
-                  end loop;
-
-               --  If the node is not analyzed, recognize occurrences of a
-               --  formal by name, as would be done when resolving the aspect
-               --  expression in the context of the subprogram.
-
-               elsif not Analyzed (N)
-                 and then Nkind (N) = N_Identifier
-                 and then No (Entity (N))
-               then
-                  while Present (F) loop
-                     if Chars (N) = Chars (F) then
-                        Rewrite (N, New_Copy_Tree (A));
-                        return Skip;
-                     end if;
-
-                     Next_Formal (F);
-                     Next_Actual (A);
-                  end loop;
-               end if;
-            end if;
-
-            return OK;
-         end Replace_Formals;
-
-         procedure Update is new Traverse_Proc (Replace_Formals);
-
-         --  Local variables
-
-         Str_Loc : constant String := Build_Location_String (Loc);
-
-         A    : Node_Id;
-         Cond : Node_Id;
-         Msg  : Node_Id;
-         Prec : Node_Id;
-
-      --  Start of processing for Build_Class_Wide_Check
-
-      begin
-         --  Climb searching for the enclosing class-wide precondition
-
-         while not Has_Class_Wide_Precondition (Subp)
-           and then Present (Overridden_Operation (Subp))
-         loop
-            Subp := Overridden_Operation (Subp);
-         end loop;
-
-         --  Locate class-wide precondition, if any
-
-         if Present (Contract (Subp))
-           and then Present (Pre_Post_Conditions (Contract (Subp)))
-         then
-            Prec := Pre_Post_Conditions (Contract (Subp));
-
-            while Present (Prec) loop
-               exit when Pragma_Name (Prec) = Name_Precondition
-                 and then Class_Present (Prec);
-               Prec := Next_Pragma (Prec);
-            end loop;
-
-            if No (Prec) or else Is_Ignored (Prec) then
-               return;
-            end if;
-
-            --  Ensure that the evaluation of the actuals will not produce side
-            --  effects (since the check will use a copy of the actuals).
-
-            A := First_Actual (Call_Node);
-            while Present (A) loop
-               Remove_Side_Effects (A);
-               Next_Actual (A);
-            end loop;
-
-            --  The expression for the precondition is analyzed within the
-            --  generated pragma. The message text is the last parameter of
-            --  the generated pragma, indicating source of precondition.
-
-            Cond :=
-              New_Copy_Tree
-                (Expression (First (Pragma_Argument_Associations (Prec))));
-            Update (Cond);
-
-            --  Build message indicating the failed precondition and the
-            --  dispatching call that caused it.
-
-            Msg := Expression (Last (Pragma_Argument_Associations (Prec)));
-            Name_Len := 0;
-            Append (Global_Name_Buffer, Strval (Msg));
-            Append (Global_Name_Buffer, " in dispatching call at ");
-            Append (Global_Name_Buffer, Str_Loc);
-            Msg := Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len));
-
-            Insert_Action (Call_Node,
-              Make_If_Statement (Loc,
-                Condition       => Make_Op_Not (Loc, Cond),
-                Then_Statements => New_List (
-                  Make_Procedure_Call_Statement (Loc,
-                    Name                   =>
-                      New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc),
-                    Parameter_Associations => New_List (Msg)))));
-         end if;
-      end Build_Class_Wide_Check;
-
       ---------------
       -- New_Value --
       ---------------
@@ -984,8 +761,6 @@ package body Exp_Disp is
          Subp := Alias (Subp);
       end if;
 
-      Build_Class_Wide_Check (Subp);
-
       --  Definition of the class-wide type and the tagged type
 
       --  If the controlling argument is itself a tag rather than a tagged
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 807afb2..7c36666 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1270,11 +1270,10 @@ package body Exp_Util is
    ---------------------------------
 
    procedure Build_Class_Wide_Expression
-     (Prag          : Node_Id;
-      Subp          : Entity_Id;
-      Par_Subp      : Entity_Id;
-      Adjust_Sloc   : Boolean;
-      Needs_Wrapper : out Boolean)
+     (Pragma_Or_Expr : Node_Id;
+      Subp           : Entity_Id;
+      Par_Subp       : Entity_Id;
+      Adjust_Sloc    : Boolean)
    is
       function Replace_Entity (N : Node_Id) return Traverse_Result;
       --  Replace reference to formal of inherited operation or to primitive
@@ -1319,84 +1318,6 @@ package body Exp_Util is
 
             if Present (New_E) then
                Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
-
-               --  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.
-               --  Move this check to sem???
-
-               if 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)
-                 and then Chars (Pragma_Identifier (Prag)) = Name_Precondition
-               then
-                  Error_Msg_Node_2 := Wrapped_Entity (Subp);
-                  Error_Msg_NE
-                    ("internal call to& cannot appear in inherited "
-                     & "precondition of protected operation&",
-                     N, Wrapped_Entity (New_E));
-               end if;
-
-               --  If the entity is an overridden primitive and we are not
-               --  in GNATprove mode, we must build a wrapper for the current
-               --  inherited operation. If the reference is the prefix of an
-               --  attribute such as 'Result (or others ???) there is no need
-               --  for a wrapper: the condition is just rewritten in terms of
-               --  the inherited subprogram.
-
-               if Is_Subprogram (New_E)
-                  and then Nkind (Parent (N)) /= N_Attribute_Reference
-                  and then not GNATprove_Mode
-               then
-                  Needs_Wrapper := True;
-               end if;
-            end if;
-
-            --  Check that there are no calls left to abstract operations if
-            --  the current subprogram is not abstract.
-            --  Move this check to sem???
-
-            if Nkind (Parent (N)) = N_Function_Call
-              and then N = Name (Parent (N))
-            then
-               if not Is_Abstract_Subprogram (Subp)
-                 and then Is_Abstract_Subprogram (Entity (N))
-               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, Entity (N));
-                  else
-                     Error_Msg_NE
-                       ("cannot call abstract subprogram & in inherited "
-                        & "condition for inherited&#", Subp, Entity (N));
-                  end if;
-
-               --  In SPARK mode, reject an 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;
 
             --  Update type of function call node, which should be the same as
@@ -1422,26 +1343,17 @@ package body Exp_Util is
 
       --  Local variables
 
-      Par_Formal  : Entity_Id;
-      Subp_Formal : Entity_Id;
+      Par_Typ  : constant Entity_Id := Find_Dispatching_Type (Par_Subp);
+      Subp_Typ : constant Entity_Id := Find_Dispatching_Type (Subp);
 
    --  Start of processing for Build_Class_Wide_Expression
 
    begin
-      Needs_Wrapper := False;
-
-      --  Add mapping from old formals to new formals
+      pragma Assert (Par_Typ /= Subp_Typ);
 
-      Par_Formal  := First_Formal (Par_Subp);
-      Subp_Formal := First_Formal (Subp);
-
-      while Present (Par_Formal) and then Present (Subp_Formal) loop
-         Type_Map.Set (Par_Formal, Subp_Formal);
-         Next_Formal (Par_Formal);
-         Next_Formal (Subp_Formal);
-      end loop;
-
-      Replace_Condition_Entities (Prag);
+      Update_Primitives_Mapping (Par_Subp, Subp);
+      Map_Formals (Par_Subp, Subp);
+      Replace_Condition_Entities (Pragma_Or_Expr);
    end Build_Class_Wide_Expression;
 
    --------------------
@@ -1895,7 +1807,33 @@ package body Exp_Util is
          Priv_Typ : Entity_Id;
          --  The partial view of Par_Typ
 
+         Op_Node  : Elmt_Id;
+         Par_Prim : Entity_Id;
+         Prim     : Entity_Id;
+
       begin
+         --  Map the overridden primitive to the overriding one; required by
+         --  Replace_References (called by Add_Inherited_DICs) to handle calls
+         --  to parent primitives.
+
+         Op_Node := First_Elmt (Primitive_Operations (T));
+         while Present (Op_Node) loop
+            Prim := Node (Op_Node);
+
+            if Present (Overridden_Operation (Prim))
+              and then Comes_From_Source (Prim)
+            then
+               Par_Prim := Overridden_Operation (Prim);
+
+               --  Create a mapping of the form:
+               --    parent type primitive -> derived type primitive
+
+               Type_Map.Set (Par_Prim, Prim);
+            end if;
+
+            Next_Elmt (Op_Node);
+         end loop;
+
          --  Climb the parent type chain
 
          Curr_Typ := T;
@@ -7073,6 +7011,15 @@ package body Exp_Util is
       return Etype (Indx);
    end Get_Index_Subtype;
 
+   -----------------------
+   -- Get_Mapped_Entity --
+   -----------------------
+
+   function Get_Mapped_Entity (E : Entity_Id) return Entity_Id is
+   begin
+      return Type_Map.Get (E);
+   end Get_Mapped_Entity;
+
    ---------------------
    -- Get_Stream_Size --
    ---------------------
@@ -10350,6 +10297,36 @@ package body Exp_Util is
       end if;
    end Make_Variant_Comparison;
 
+   -----------------
+   -- Map_Formals --
+   -----------------
+
+   procedure Map_Formals
+     (Parent_Subp  : Entity_Id;
+      Derived_Subp : Entity_Id;
+      Force_Update : Boolean := False)
+   is
+      Par_Formal  : Entity_Id := First_Formal (Parent_Subp);
+      Subp_Formal : Entity_Id := First_Formal (Derived_Subp);
+
+   begin
+      if Force_Update then
+         Type_Map.Set (Parent_Subp, Derived_Subp);
+      end if;
+
+      --  At this stage either we are under regular processing and the caller
+      --  has previously ensured that these primitives are already mapped (by
+      --  means of calling previously to Update_Primitives_Mapping), or we are
+      --  processing a late-overriding primitive and Force_Update updated above
+      --  the mapping of these primitives.
+
+      while Present (Par_Formal) and then Present (Subp_Formal) loop
+         Type_Map.Set (Par_Formal, Subp_Formal);
+         Next_Formal (Par_Formal);
+         Next_Formal (Subp_Formal);
+      end loop;
+   end Map_Formals;
+
    ---------------
    -- Map_Types --
    ---------------
@@ -10861,7 +10838,7 @@ package body Exp_Util is
          --  they relate to the primitives of the parent type. If there is a
          --  meaningful relation, create a mapping of the form:
 
-         --    parent type primitive -> perived type primitive
+         --    parent type primitive -> derived type primitive
 
          if Present (Direct_Primitive_Operations (Deriv_Typ)) then
             Prim_Elmt := First_Elmt (Direct_Primitive_Operations (Deriv_Typ));
@@ -14123,10 +14100,12 @@ package body Exp_Util is
      (Inher_Id : Entity_Id;
       Subp_Id  : Entity_Id)
    is
+      Parent_Type  : constant Entity_Id := Find_Dispatching_Type (Inher_Id);
+      Derived_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
+
    begin
-      Map_Types
-        (Parent_Type  => Find_Dispatching_Type (Inher_Id),
-         Derived_Type => Find_Dispatching_Type (Subp_Id));
+      pragma Assert (Parent_Type /= Derived_Type);
+      Map_Types (Parent_Type, Derived_Type);
    end Update_Primitives_Mapping;
 
    ----------------------------------
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 56ff61f..eddf314 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -270,28 +270,16 @@ package Exp_Util is
    --  not install a call to Abort_Defer.
 
    procedure Build_Class_Wide_Expression
-     (Prag          : Node_Id;
-      Subp          : Entity_Id;
-      Par_Subp      : Entity_Id;
-      Adjust_Sloc   : Boolean;
-      Needs_Wrapper : out Boolean);
-   --  Build the expression for an inherited class-wide condition. Prag is
-   --  the pragma constructed from the corresponding aspect of the parent
-   --  subprogram, and Subp is the overriding operation, and Par_Subp is
-   --  the overridden operation that has the condition. Adjust_Sloc is True
-   --  when the sloc of nodes traversed should be adjusted for the inherited
-   --  pragma. The routine is also called to check whether an inherited
-   --  operation that is not overridden but has inherited conditions needs
-   --  a wrapper, because the inherited condition includes calls to other
-   --  primitives that have been overridden. In that case the first argument
-   --  is the expression of the original class-wide aspect. In SPARK_Mode, such
-   --  operation which are just inherited but have modified pre/postconditions
-   --  are illegal.
-   --  If there are calls to overridden operations in the condition, and the
-   --  pragma applies to an inherited operation, a wrapper must be built for
-   --  it to capture the new inherited condition. The flag Needs_Wrapper is
-   --  set in that case so that the wrapper can be built, when the controlling
-   --  type is frozen.
+     (Pragma_Or_Expr : Node_Id;
+      Subp           : Entity_Id;
+      Par_Subp       : Entity_Id;
+      Adjust_Sloc    : Boolean);
+   --  Build the expression for an inherited class-wide condition. Pragma_Or_
+   --  _Expr is either the pragma constructed from the corresponding aspect of
+   --  the parent subprogram or the class-wide pre/postcondition built from the
+   --  parent, Subp is the overriding operation, and Par_Subp is the overridden
+   --  operation that has the condition. Adjust_Sloc is True when the sloc of
+   --  nodes traversed should be adjusted for the inherited pragma.
 
    function Build_DIC_Call
      (Loc      : Source_Ptr;
@@ -612,7 +600,7 @@ package Exp_Util is
    function Find_Prim_Op (T : Entity_Id; Name : Name_Id) return Entity_Id;
    --  Find the first primitive operation of a tagged type T with name Name.
    --  This function allows the use of a primitive operation which is not
-   --  directly visible. If T is a class wide type, then the reference is to an
+   --  directly visible. If T is a class-wide type, then the reference is to an
    --  operation of the corresponding root type. It is an error if no primitive
    --  operation with the given name is found.
 
@@ -739,6 +727,10 @@ package Exp_Util is
    --  Used for First, Last, and Length, when the prefix is an array type.
    --  Obtains the corresponding index subtype.
 
+   function Get_Mapped_Entity (E : Entity_Id) return Entity_Id;
+   --  Return the mapped entity of E; used to check inherited class-wide
+   --  pre/postconditions.
+
    function Get_Stream_Size (E : Entity_Id) return Uint;
    --  Return the stream size value of the subtype E
 
@@ -918,6 +910,15 @@ package Exp_Util is
    --  Subprogram_Variant. Generate a comparison between Curr_Val and Old_Val
    --  depending on the variant mode (Increases / Decreases).
 
+   procedure Map_Formals
+     (Parent_Subp  : Entity_Id;
+      Derived_Subp : Entity_Id;
+      Force_Update : Boolean := False);
+   --  Establish the mapping from the formals of Parent_Subp to the formals
+   --  of Derived_Subp; if Force_Update is True then mapping of Parent_Subp to
+   --  Derived_Subp is also updated; used to update mapping of late-overriding
+   --  primitives of a tagged type.
+
    procedure Map_Types (Parent_Type : Entity_Id; Derived_Type : Entity_Id);
    --  Establish the following mapping between the attributes of tagged parent
    --  type Parent_Type and tagged derived type Derived_Type.
@@ -1205,5 +1206,6 @@ package Exp_Util is
 private
    pragma Inline (Duplicate_Subexpr);
    pragma Inline (Force_Evaluation);
+   pragma Inline (Get_Mapped_Entity);
    pragma Inline (Is_Library_Level_Tagged_Type);
 end Exp_Util;
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 5b7607d..5f81d9e 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -35,6 +35,7 @@ with Elists;         use Elists;
 with Errout;         use Errout;
 with Exp_Ch3;        use Exp_Ch3;
 with Exp_Ch7;        use Exp_Ch7;
+with Exp_Disp;       use Exp_Disp;
 with Exp_Pakd;       use Exp_Pakd;
 with Exp_Util;       use Exp_Util;
 with Exp_Tss;        use Exp_Tss;
@@ -56,6 +57,7 @@ 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_Disp;       use Sem_Disp;
 with Sem_Eval;       use Sem_Eval;
 with Sem_Mech;       use Sem_Mech;
 with Sem_Prag;       use Sem_Prag;
@@ -132,11 +134,6 @@ package body Freeze is
    --  Attribute references to outer types are freeze points for those types;
    --  this routine generates the required freeze nodes for them.
 
-   procedure Check_Inherited_Conditions (R : Entity_Id);
-   --  For a tagged derived type, create wrappers for inherited operations
-   --  that have a class-wide condition, so it can be properly rewritten if
-   --  it involves calls to other overriding primitives.
-
    procedure Check_Strict_Alignment (E : Entity_Id);
    --  E is a base type. If E is tagged or has a component that is aliased
    --  or tagged or contains something this is aliased or tagged, set
@@ -160,7 +157,7 @@ package body Freeze is
    procedure Freeze_Enumeration_Type (Typ : Entity_Id);
    --  Freeze enumeration type. The Esize field is set as processing
    --  proceeds (i.e. set by default when the type is declared and then
-   --  adjusted by rep clauses. What this procedure does is to make sure
+   --  adjusted by rep clauses). What this procedure does is to make sure
    --  that if a foreign convention is specified, and no specific size
    --  is given, then the size must be at least Integer'Size.
 
@@ -1483,90 +1480,322 @@ package body Freeze is
    -- Check_Inherited_Conditions --
    --------------------------------
 
-   procedure Check_Inherited_Conditions (R : Entity_Id) is
-      Prim_Ops      : constant Elist_Id := Primitive_Operations (R);
-      Decls         : List_Id;
-      Needs_Wrapper : Boolean;
-      Op_Node       : Elmt_Id;
-      Par_Prim      : Entity_Id;
-      Prim          : Entity_Id;
-
-      procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id);
+   procedure Check_Inherited_Conditions
+     (R               : Entity_Id;
+      Late_Overriding : Boolean := False)
+   is
+      Prim_Ops       : constant Elist_Id := Primitive_Operations (R);
+      Decls          : List_Id;
+      Op_Node        : Elmt_Id;
+      Par_Prim       : Entity_Id;
+      Prim           : Entity_Id;
+      Wrapper_Needed : Boolean;
+
+      function Build_DTW_Body
+        (Loc          : Source_Ptr;
+         DTW_Spec     : Node_Id;
+         DTW_Decls    : List_Id;
+         Par_Prim     : Entity_Id;
+         Wrapped_Subp : Entity_Id) return Node_Id;
+      --  Build the body of the dispatch table wrapper containing the given
+      --  spec and declarations; the call to the wrapped subprogram includes
+      --  the proper type conversion.
+
+      function Build_DTW_Spec (Par_Prim : Entity_Id) return Node_Id;
+      --  Build the spec of the dispatch table wrapper
+
+      procedure Build_Inherited_Condition_Pragmas
+        (Subp           : Entity_Id;
+         Wrapper_Needed : out Boolean);
       --  Build corresponding pragmas for an operation whose ancestor has
-      --  class-wide pre/postconditions. If the operation is inherited, the
-      --  pragmas force the creation of a wrapper for the inherited operation.
-      --  If the ancestor is being overridden, the pragmas are constructed only
-      --  to verify their legality, in case they contain calls to other
-      --  primitives that may have been overridden.
+      --  class-wide pre/postconditions. If the operation is inherited then
+      --  Wrapper_Needed is returned True to force the creation of a wrapper
+      --  for the inherited operation. If the ancestor is being overridden,
+      --  the pragmas are constructed only to verify their legality, in case
+      --  they contain calls to other primitives that may have been overridden.
+
+      function Needs_Wrapper
+        (Class_Cond : Node_Id;
+         Subp       : Entity_Id;
+         Par_Subp   : Entity_Id) return Boolean;
+      --  Checks whether the dispatch-table wrapper (DTW) for Subp must be
+      --  built to evaluate the given class-wide condition.
+
+      --------------------
+      -- Build_DTW_Body --
+      --------------------
+
+      function Build_DTW_Body
+        (Loc          : Source_Ptr;
+         DTW_Spec     : Node_Id;
+         DTW_Decls    : List_Id;
+         Par_Prim     : Entity_Id;
+         Wrapped_Subp : Entity_Id) return Node_Id
+      is
+         Par_Typ    : constant Entity_Id := Find_Dispatching_Type (Par_Prim);
+         Actuals    : constant List_Id   := Empty_List;
+         Call       : Node_Id;
+         Formal     : Entity_Id := First_Formal (Par_Prim);
+         New_F_Spec : Entity_Id := First (Parameter_Specifications (DTW_Spec));
+         New_Formal : Entity_Id;
+
+      begin
+         --  Build parameter association for call to wrapped subprogram
+
+         while Present (Formal) loop
+            New_Formal := Defining_Identifier (New_F_Spec);
+
+            --  If the controlling argument is inherited, add conversion to
+            --  parent type for the call.
+
+            if Etype (Formal) = Par_Typ
+              and then Is_Controlling_Formal (Formal)
+            then
+               Append_To (Actuals,
+                 Make_Type_Conversion (Loc,
+                   New_Occurrence_Of (Par_Typ, Loc),
+                   New_Occurrence_Of (New_Formal, Loc)));
+            else
+               Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
+            end if;
+
+            Next_Formal (Formal);
+            Next (New_F_Spec);
+         end loop;
+
+         if Ekind (Wrapped_Subp) = E_Procedure then
+            Call :=
+              Make_Procedure_Call_Statement (Loc,
+                Name => New_Occurrence_Of (Wrapped_Subp, Loc),
+                Parameter_Associations => Actuals);
+         else
+            Call :=
+              Make_Simple_Return_Statement (Loc,
+                Expression =>
+                  Make_Function_Call (Loc,
+                    Name => New_Occurrence_Of (Wrapped_Subp, Loc),
+                    Parameter_Associations => Actuals));
+         end if;
+
+         return
+           Make_Subprogram_Body (Loc,
+             Specification              => Copy_Subprogram_Spec (DTW_Spec),
+             Declarations               => DTW_Decls,
+             Handled_Statement_Sequence =>
+               Make_Handled_Sequence_Of_Statements (Loc,
+                 Statements => New_List (Call),
+                 End_Label  => Make_Identifier (Loc,
+                                 Chars (Defining_Entity (DTW_Spec)))));
+      end Build_DTW_Body;
+
+      --------------------
+      -- Build_DTW_Spec --
+      --------------------
+
+      function Build_DTW_Spec (Par_Prim : Entity_Id) return Node_Id is
+         DTW_Id   : Entity_Id;
+         DTW_Spec : Node_Id;
+
+      begin
+         DTW_Spec := Build_Overriding_Spec (Par_Prim, R);
+         DTW_Id   := Defining_Entity (DTW_Spec);
+
+         --  Add minimal decoration of fields
+
+         Mutate_Ekind (DTW_Id, Ekind (Par_Prim));
+         Set_LSP_Subprogram (DTW_Id, Par_Prim);
+         Set_Is_Dispatch_Table_Wrapper (DTW_Id);
+         Set_Is_Wrapper (DTW_Id);
+
+         --  The DTW wrapper is never a null procedure
+
+         if Nkind (DTW_Spec) = N_Procedure_Specification then
+            Set_Null_Present (DTW_Spec, False);
+         end if;
+
+         return DTW_Spec;
+      end Build_DTW_Spec;
 
       ---------------------------------------
       -- Build_Inherited_Condition_Pragmas --
       ---------------------------------------
 
-      procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is
-         A_Post   : Node_Id;
-         A_Pre    : Node_Id;
-         New_Prag : Node_Id;
+      procedure Build_Inherited_Condition_Pragmas
+        (Subp           : Entity_Id;
+         Wrapper_Needed : out Boolean)
+      is
+         Class_Pre  : constant Node_Id :=
+                        Class_Preconditions (Ultimate_Alias (Subp));
+         Class_Post : Node_Id := Class_Postconditions (Par_Prim);
+         A_Post     : Node_Id;
+         New_Prag   : Node_Id;
 
       begin
-         A_Pre := Get_Class_Wide_Pragma (Par_Prim, Pragma_Precondition);
+         Wrapper_Needed := False;
 
-         if Present (A_Pre) then
-            New_Prag := New_Copy_Tree (A_Pre);
-            Build_Class_Wide_Expression
-              (Prag          => New_Prag,
-               Subp          => Prim,
-               Par_Subp      => Par_Prim,
-               Adjust_Sloc   => False,
-               Needs_Wrapper => Needs_Wrapper);
-
-            if Needs_Wrapper
-              and then not Comes_From_Source (Subp)
-              and then Expander_Active
-            then
-               Append (New_Prag, Decls);
-            end if;
+         if No (Class_Pre) and then No (Class_Post) then
+            return;
          end if;
 
-         A_Post := Get_Class_Wide_Pragma (Par_Prim, Pragma_Postcondition);
+         --  For class-wide preconditions we just evaluate whether the wrapper
+         --  is needed; there is no need to build the pragma since the check
+         --  is performed on the caller side.
 
-         if Present (A_Post) then
-            New_Prag := New_Copy_Tree (A_Post);
+         if Present (Class_Pre)
+           and then Needs_Wrapper (Class_Pre, Subp, Par_Prim)
+         then
+            Wrapper_Needed := True;
+         end if;
+
+         --  For class-wide postconditions we evaluate whether the wrapper is
+         --  needed and we build the class-wide postcondition pragma to install
+         --  it in the wrapper.
+
+         if Present (Class_Post)
+           and then Needs_Wrapper (Class_Post, Subp, Par_Prim)
+         then
+            Wrapper_Needed := True;
+
+            --  Update the class-wide postcondition
+
+            Class_Post := New_Copy_Tree (Class_Post);
             Build_Class_Wide_Expression
-              (Prag           => New_Prag,
-               Subp           => Prim,
+              (Pragma_Or_Expr => Class_Post,
+               Subp           => Subp,
                Par_Subp       => Par_Prim,
-               Adjust_Sloc    => False,
-               Needs_Wrapper  => Needs_Wrapper);
+               Adjust_Sloc    => False);
 
-            if Needs_Wrapper
-              and then not Comes_From_Source (Subp)
-              and then Expander_Active
-            then
-               Append (New_Prag, Decls);
+            --  Install the updated class-wide postcondition in a copy of the
+            --  pragma postcondition defined for the nearest ancestor.
+
+            A_Post := Get_Class_Wide_Pragma (Par_Prim,
+                        Pragma_Postcondition);
+
+            if No (A_Post) then
+               declare
+                  Subps : constant Subprogram_List :=
+                            Inherited_Subprograms (Subp);
+               begin
+                  for Index in Subps'Range loop
+                     A_Post := Get_Class_Wide_Pragma (Subps (Index),
+                                 Pragma_Postcondition);
+                     exit when Present (A_Post);
+                  end loop;
+               end;
             end if;
+
+            New_Prag := New_Copy_Tree (A_Post);
+            Rewrite
+              (Expression (First (Pragma_Argument_Associations (New_Prag))),
+               Class_Post);
+            Append (New_Prag, Decls);
          end if;
       end Build_Inherited_Condition_Pragmas;
 
+      -------------------
+      -- Needs_Wrapper --
+      -------------------
+
+      function Needs_Wrapper
+        (Class_Cond : Node_Id;
+         Subp       : Entity_Id;
+         Par_Subp   : Entity_Id) return Boolean
+      is
+         Result : Boolean := False;
+
+         function Check_Entity (N : Node_Id) return Traverse_Result;
+         --  Check calls to overridden primitives
+
+         --------------------
+         -- Replace_Entity --
+         --------------------
+
+         function Check_Entity (N : Node_Id) return Traverse_Result is
+            New_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
+               --  The check does 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
+
+               New_E := Get_Mapped_Entity (Entity (N));
+
+               --  If the entity is an overridden primitive and we are not
+               --  in GNATprove mode, we must build a wrapper for the current
+               --  inherited operation. If the reference is the prefix of an
+               --  attribute such as 'Result (or others ???) there is no need
+               --  for a wrapper: the condition is just rewritten in terms of
+               --  the inherited subprogram.
+
+               if Present (New_E)
+                 and then Comes_From_Source (New_E)
+                 and then Is_Subprogram (New_E)
+                 and then Nkind (Parent (N)) /= N_Attribute_Reference
+                 and then not GNATprove_Mode
+               then
+                  Result := True;
+                  return Abandon;
+               end if;
+            end if;
+
+            return OK;
+         end Check_Entity;
+
+         procedure Check_Condition_Entities is
+           new Traverse_Proc (Check_Entity);
+
+      --  Start of processing for Needs_Wrapper
+
+      begin
+         Update_Primitives_Mapping (Par_Subp, Subp);
+
+         Map_Formals (Par_Subp, Subp);
+         Check_Condition_Entities (Class_Cond);
+
+         return Result;
+      end Needs_Wrapper;
+
    --  Start of processing for Check_Inherited_Conditions
 
    begin
-      Op_Node := First_Elmt (Prim_Ops);
-      while Present (Op_Node) loop
-         Prim := Node (Op_Node);
+      if Late_Overriding then
+         Op_Node := First_Elmt (Prim_Ops);
+         while Present (Op_Node) loop
+            Prim := Node (Op_Node);
 
-         --  Map the overridden primitive to the overriding one. This takes
-         --  care of all overridings and is done only once.
+            --  Map the overridden primitive to the overriding one
 
-         if Present (Overridden_Operation (Prim))
-           and then Comes_From_Source (Prim)
-         then
-            Par_Prim := Overridden_Operation (Prim);
-            Update_Primitives_Mapping (Par_Prim, Prim);
-         end if;
+            if Present (Overridden_Operation (Prim))
+              and then Comes_From_Source (Prim)
+            then
+               Par_Prim := Overridden_Operation (Prim);
+               Update_Primitives_Mapping (Par_Prim, Prim);
 
-         Next_Elmt (Op_Node);
-      end loop;
+               --  Force discarding previous mappings of its formals
+
+               Map_Formals (Par_Prim, Prim, Force_Update => True);
+            end if;
+
+            Next_Elmt (Op_Node);
+         end loop;
+      end if;
 
       --  Perform validity checks on the inherited conditions of overriding
       --  operations, for conformance with LSP, and apply SPARK-specific
@@ -1602,12 +1831,6 @@ package body Freeze is
 
             if GNATprove_Mode then
                Collect_Inherited_Class_Wide_Conditions (Prim);
-
-            --  Otherwise build the corresponding pragmas to check for legality
-            --  of the inherited condition.
-
-            else
-               Build_Inherited_Condition_Pragmas (Prim);
             end if;
          end if;
 
@@ -1621,12 +1844,17 @@ package body Freeze is
       Op_Node := First_Elmt (Prim_Ops);
 
       while Present (Op_Node) loop
-         Decls         := Empty_List;
-         Prim          := Node (Op_Node);
-         Needs_Wrapper := False;
+         Decls          := Empty_List;
+         Prim           := Node (Op_Node);
+         Wrapper_Needed := False;
+
+         --  Skip internal entities built for mapping interface primitives
 
-         if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then
-            Par_Prim := Alias (Prim);
+         if not Comes_From_Source (Prim)
+           and then Present (Alias (Prim))
+           and then No (Interface_Alias (Prim))
+         then
+            Par_Prim := Ultimate_Alias (Prim);
 
             --  When the primitive is an LSP wrapper we climb to the parent
             --  primitive that has the inherited contract.
@@ -1644,39 +1872,39 @@ package body Freeze is
             --  in the loop above.
 
             Analyze_Entry_Or_Subprogram_Contract (Par_Prim);
-            Build_Inherited_Condition_Pragmas (Prim);
+            Build_Inherited_Condition_Pragmas (Prim, Wrapper_Needed);
          end if;
 
-         if Needs_Wrapper
+         if Wrapper_Needed
            and then not Is_Abstract_Subprogram (Par_Prim)
            and then Expander_Active
          then
-            --  We need to build a new primitive that overrides the inherited
-            --  one, and whose inherited expression has been updated above.
-            --  These expressions are the arguments of pragmas that are part
-            --  of the declarations of the wrapper. The wrapper holds a single
-            --  statement that is a call to the class-wide clone, where the
-            --  controlling actuals are conversions to the corresponding type
-            --  in the parent primitive:
-
-            --    procedure New_Prim (F1 : T1; ...);
-            --    procedure New_Prim (F1 : T1; ...) is
-            --       pragma Check (Precondition, Expr);
-            --    begin
-            --       Par_Prim_Clone (Par_Type (F1), ...);
-            --    end;
-
-            --  If the primitive is a function the statement is a return
-            --  statement with a call.
+            --  Build the dispatch-table wrapper (DTW). The support for
+            --  AI12-0195 relies on two kind of wrappers: one for indirect
+            --  calls (also used for AI12-0220), and one for putting in the
+            --  dispatch table:
+            --
+            --    1) "indirect-call wrapper" (ICW) is needed anytime there are
+            --       class-wide preconditions. Prim'Access will point directly
+            --       at the ICW if any, or at the "pristine" body if Prim has
+            --       no class-wide preconditions.
+            --
+            --    2) "dispatch-table wrapper" (DTW) is needed anytime the class
+            --       wide preconditions *or* the class-wide postconditions are
+            --       affected by overriding.
+            --
+            --  The DTW holds a single statement that is a single call where
+            --  the controlling actuals are conversions to the corresponding
+            --  type in the parent primitive. If the primitive is a function
+            --  the statement is a return statement with a call.
 
             declare
                Alias_Id : constant Entity_Id  := Ultimate_Alias (Prim);
                Loc      : constant Source_Ptr := Sloc (R);
-               Par_R    : constant Node_Id    := Parent (R);
-               New_Body : Node_Id;
-               New_Decl : Node_Id;
-               New_Id   : Entity_Id;
-               New_Spec : Node_Id;
+               DTW_Body : Node_Id;
+               DTW_Decl : Node_Id;
+               DTW_Id   : Entity_Id;
+               DTW_Spec : Node_Id;
 
             begin
                --  The wrapper must be analyzed in the scope of its wrapped
@@ -1684,47 +1912,130 @@ package body Freeze is
 
                Push_Scope (Scope (Prim));
 
-               New_Spec := Build_Overriding_Spec (Par_Prim, R);
-               New_Id   := Defining_Entity (New_Spec);
-               New_Decl :=
-                 Make_Subprogram_Declaration (Loc,
-                   Specification => New_Spec);
+               DTW_Spec := Build_DTW_Spec (Par_Prim);
+               DTW_Id   := Defining_Entity (DTW_Spec);
+               DTW_Decl := Make_Subprogram_Declaration (Loc,
+                             Specification => DTW_Spec);
+
+               --  For inherited class-wide preconditions the DTW wrapper
+               --  reuses the ICW of the parent (which checks the parent
+               --  interpretation of the class-wide preconditions); the
+               --  interpretation of the class-wide preconditions for the
+               --  inherited subprogram is checked at the caller side.
+
+               --  When the subprogram inherits class-wide postconditions
+               --  the DTW also checks the interpretation of the class-wide
+               --  postconditions for the inherited subprogram, and the body
+               --  of the parent checks its interpretation of the parent for
+               --  the class-wide postconditions.
+
+               --      procedure Prim (F1 : T1; ...) is
+               --         [ pragma Check (Postcondition, Expr); ]
+               --      begin
+               --         Par_Prim_ICW (Par_Type (F1), ...);
+               --      end;
+
+               if Present (Indirect_Call_Wrapper (Par_Prim)) then
+                  DTW_Body :=
+                    Build_DTW_Body (Loc,
+                      DTW_Spec     => DTW_Spec,
+                      DTW_Decls    => Decls,
+                      Par_Prim     => Par_Prim,
+                      Wrapped_Subp => Indirect_Call_Wrapper (Par_Prim));
+
+               --  For subprograms that only inherit class-wide postconditions
+               --  the DTW wrapper calls the parent primitive (which on its
+               --  body checks the interpretation of the class-wide post-
+               --  conditions for the parent subprogram), and the DTW checks
+               --  the interpretation of the class-wide postconditions for the
+               --  inherited subprogram.
+
+               --      procedure Prim (F1 : T1; ...) is
+               --         pragma Check (Postcondition, Expr);
+               --      begin
+               --         Par_Prim (Par_Type (F1), ...);
+               --      end;
 
-               --  Insert the declaration and the body of the wrapper after
-               --  type declaration that generates inherited operation. For
-               --  a null procedure, the declaration implies a null body.
-
-               --  Before insertion, do some minimal decoration of fields
+               else
+                  DTW_Body :=
+                    Build_DTW_Body (Loc,
+                      DTW_Spec     => DTW_Spec,
+                      DTW_Decls    => Decls,
+                      Par_Prim     => Par_Prim,
+                      Wrapped_Subp => Par_Prim);
+               end if;
 
-               Mutate_Ekind (New_Id, Ekind (Par_Prim));
-               Set_LSP_Subprogram (New_Id, Par_Prim);
-               Set_Is_Wrapper (New_Id);
+               --  Insert the declaration of the wrapper before the freezing
+               --  node of the record type declaration to ensure that it will
+               --  override the internal primitive built by Derive_Subprogram.
 
-               if Nkind (New_Spec) = N_Procedure_Specification
-                 and then Null_Present (New_Spec)
-               then
-                  Insert_After_And_Analyze (Par_R, New_Decl);
+               Ensure_Freeze_Node (R);
 
+               if Late_Overriding then
+                  Insert_Before_And_Analyze (Freeze_Node (R), DTW_Decl);
                else
-                  --  Build body as wrapper to a call to the already built
-                  --  class-wide clone.
+                  Append_Freeze_Action (R, DTW_Decl);
+               end if;
+
+               Analyze (DTW_Decl);
+
+               --  Insert the body of the wrapper in the freeze actions of
+               --  its record type declaration to ensure that it is placed
+               --  in the scope of its declaration but not too early to cause
+               --  premature freezing of other entities.
+
+               Append_Freeze_Action (R, DTW_Body);
+               Analyze (DTW_Body);
+
+               --  Ensure correct decoration
+
+               pragma Assert (Is_Dispatching_Operation (DTW_Id));
+               pragma Assert (Present (Overridden_Operation (DTW_Id)));
+               pragma Assert (Overridden_Operation (DTW_Id) = Alias_Id);
 
-                  New_Body :=
-                    Build_Class_Wide_Clone_Call
-                      (Loc, Decls, Par_Prim, New_Spec);
+               --  Inherit dispatch table slot
 
-                  Insert_List_After_And_Analyze
-                    (Par_R, New_List (New_Decl, New_Body));
+               Set_DTC_Entity_Value (R, DTW_Id);
+               Set_DT_Position (DTW_Id, DT_Position (Alias_Id));
 
-                  --  Ensure correct decoration
+               --  Register the wrapper in the dispatch table
 
-                  pragma Assert (Present (Alias (Prim)));
-                  pragma Assert (Present (Overridden_Operation (New_Id)));
-                  pragma Assert (Overridden_Operation (New_Id) = Alias_Id);
+               if Late_Overriding
+                 and then not Building_Static_DT (R)
+               then
+                  Insert_List_After_And_Analyze (Freeze_Node (R),
+                    Register_Primitive (Loc, DTW_Id));
                end if;
 
-               pragma Assert (Is_Dispatching_Operation (Prim));
-               pragma Assert (Is_Dispatching_Operation (New_Id));
+               --  Build the helper and ICW for the DTW
+
+               if Present (Indirect_Call_Wrapper (Par_Prim)) then
+                  declare
+                     CW_Subp : Entity_Id;
+                     Decl_N  : Node_Id;
+                     Body_N  : Node_Id;
+
+                  begin
+                     Merge_Class_Conditions (DTW_Id);
+                     Make_Class_Precondition_Subps (DTW_Id,
+                       Late_Overriding => Late_Overriding);
+
+                     CW_Subp := Static_Call_Helper (DTW_Id);
+                     Decl_N  := Unit_Declaration_Node (CW_Subp);
+                     Analyze (Decl_N);
+
+                     --  If the DTW was built for a late-overriding primitive
+                     --  its body must be analyzed now (since the tagged type
+                     --  is already frozen).
+
+                     if Late_Overriding then
+                        Body_N :=
+                          Unit_Declaration_Node
+                            (Corresponding_Body (Decl_N));
+                        Analyze (Body_N);
+                     end if;
+                  end;
+               end if;
 
                Pop_Scope;
             end;
@@ -7417,7 +7728,7 @@ package body Freeze is
       if Is_Type (E) then
          Freeze_And_Append (First_Subtype (E), N, Result);
 
-         --  If we just froze a tagged non-class wide record, then freeze the
+         --  If we just froze a tagged non-class-wide record, then freeze the
          --  corresponding class-wide type. This must be done after the tagged
          --  type itself is frozen, because the class-wide type refers to the
          --  tagged type which generates the class.
diff --git a/gcc/ada/freeze.ads b/gcc/ada/freeze.ads
index 6f4feca..0174756 100644
--- a/gcc/ada/freeze.ads
+++ b/gcc/ada/freeze.ads
@@ -174,6 +174,15 @@ package Freeze is
    --  do not allow a size clause if the size would not otherwise be known at
    --  compile time in any case.
 
+   procedure Check_Inherited_Conditions
+    (R               : Entity_Id;
+     Late_Overriding : Boolean := False);
+   --  For a tagged derived type R, create wrappers for inherited operations
+   --  that have class-wide conditions, so it can be properly rewritten if
+   --  it involves calls to other overriding primitives. Late_Overriding is
+   --  True when we are processing the body of a primitive with no previous
+   --  spec defined after R is frozen (see Check_Dispatching_Operation).
+
    function Is_Full_Access_Aggregate (N : Node_Id) return Boolean;
    --  If a full access object is initialized with an aggregate or is assigned
    --  an aggregate, we have to prevent a piecemeal access or assignment to the
diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads
index 360e2e1..24f57b4 100644
--- a/gcc/ada/gen_il-fields.ads
+++ b/gcc/ada/gen_il-fields.ads
@@ -461,7 +461,9 @@ package Gen_IL.Fields is
       Can_Never_Be_Null,
       Can_Use_Internal_Rep,
       Checks_May_Be_Suppressed,
-      Class_Wide_Clone,
+      Class_Postconditions,
+      Class_Preconditions,
+      Class_Preconditions_Subprogram,
       Class_Wide_Type,
       Cloned_Subtype,
       Component_Alignment,
@@ -509,6 +511,7 @@ package Gen_IL.Fields is
       Discriminant_Default_Value,
       Discriminant_Number,
       Dispatch_Table_Wrappers,
+      Dynamic_Call_Helper,
       DT_Entry_Count,
       DT_Offset_To_Top_Func,
       DT_Position,
@@ -649,9 +652,12 @@ package Gen_IL.Fields is
       Hiding_Loop_Variable,
       Hidden_In_Formal_Instance,
       Homonym,
+      Ignored_Class_Postconditions,
+      Ignored_Class_Preconditions,
       Ignore_SPARK_Mode_Pragmas,
       Import_Pragma,
       Incomplete_Actuals,
+      Indirect_Call_Wrapper,
       In_Package_Body,
       In_Private_Part,
       In_Use,
@@ -693,6 +699,7 @@ package Gen_IL.Fields is
       Is_Discrim_SO_Function,
       Is_Discriminant_Check_Function,
       Is_Dispatch_Table_Entity,
+      Is_Dispatch_Table_Wrapper,
       Is_Dispatching_Operation,
       Is_Elaboration_Checks_OK_Id,
       Is_Elaboration_Warnings_OK_Id,
@@ -892,6 +899,7 @@ package Gen_IL.Fields is
       Spec_Entity,
       SSO_Set_High_By_Default,
       SSO_Set_Low_By_Default,
+      Static_Call_Helper,
       Static_Discrete_Predicate,
       Static_Elaboration_Desired,
       Static_Initialization,
diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb
index 0b70dae..bf0997e 100644
--- a/gcc/ada/gen_il-gen-gen_entities.adb
+++ b/gcc/ada/gen_il-gen-gen_entities.adb
@@ -139,6 +139,7 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Is_Discrim_SO_Function, Flag),
         Sm (Is_Discriminant_Check_Function, Flag),
         Sm (Is_Dispatch_Table_Entity, Flag),
+        Sm (Is_Dispatch_Table_Wrapper, Flag),
         Sm (Is_Dispatching_Operation, Flag),
         Sm (Is_Eliminated, Flag),
         Sm (Is_Entry_Formal, Flag),
@@ -977,8 +978,11 @@ begin -- Gen_IL.Gen.Gen_Entities
 
    Ab (Subprogram_Kind, Overloadable_Kind,
        (Sm (Body_Needed_For_SAL, Flag),
-        Sm (Class_Wide_Clone, Node_Id),
+        Sm (Class_Postconditions, Node_Id),
+        Sm (Class_Preconditions, Node_Id),
+        Sm (Class_Preconditions_Subprogram, Node_Id),
         Sm (Contract, Node_Id),
+        Sm (Dynamic_Call_Helper, Node_Id),
         Sm (Elaboration_Entity, Node_Id),
         Sm (Elaboration_Entity_Required, Flag),
         Sm (First_Entity, Node_Id),
@@ -986,8 +990,11 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Has_Nested_Subprogram, Flag),
         Sm (Has_Out_Or_In_Out_Parameter, Flag),
         Sm (Has_Recursive_Call, Flag),
+        Sm (Ignored_Class_Postconditions, Node_Id),
+        Sm (Ignored_Class_Preconditions, Node_Id),
         Sm (Ignore_SPARK_Mode_Pragmas, Flag),
         Sm (Import_Pragma, Node_Id),
+        Sm (Indirect_Call_Wrapper, Node_Id),
         Sm (Interface_Alias, Node_Id),
         Sm (Interface_Name, Node_Id),
         Sm (Is_Elaboration_Checks_OK_Id, Flag),
@@ -998,6 +1005,7 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Overridden_Operation, Node_Id),
         Sm (Protected_Body_Subprogram, Node_Id),
         Sm (Scope_Depth_Value, Uint),
+        Sm (Static_Call_Helper, Node_Id),
         Sm (SPARK_Pragma, Node_Id),
         Sm (SPARK_Pragma_Inherited, Flag),
         Sm (Subps_Index, Uint)));
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 42ea0f5..1720fe0 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -584,6 +584,15 @@ package body Ghost is
    --  Start of processing for Check_Ghost_Context
 
    begin
+      --  Class-wide pre/postconditions of ignored pragmas are preanalyzed
+      --  to report errors on wrong conditions; however, ignored pragmas may
+      --  also have references to ghost entities and we must disable checking
+      --  their context to avoid reporting spurious errors.
+
+      if Inside_Class_Condition_Preanalysis then
+         return;
+      end if;
+
       --  Once it has been established that the reference to the Ghost entity
       --  is within a suitable context, ensure that the policy at the point of
       --  declaration and at the point of use match.
diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads
index 2fdccf7..699f685 100644
--- a/gcc/ada/sem.ads
+++ b/gcc/ada/sem.ads
@@ -291,6 +291,10 @@ package Sem is
    --  freezing nodes can modify the status of this flag, any other client
    --  should regard it as read-only.
 
+   Inside_Class_Condition_Preanalysis : Boolean := False;
+   --  Flag indicating whether we are preanalyzing a class-wide precondition
+   --  or postcondition.
+
    Inside_Preanalysis_Without_Freezing : Nat := 0;
    --  Flag indicating whether we are preanalyzing an expression performing no
    --  freezing. Non-zero means we are inside (it is actually a level counter
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index d954d46..7b6dc21 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -1339,6 +1339,16 @@ package body Sem_Attr is
          Legal   := False;
          Spec_Id := Empty;
 
+         --  Skip processing during preanalysis of class-wide preconditions and
+         --  postconditions since at this stage the expression is not installed
+         --  yet on its definite context.
+
+         if Inside_Class_Condition_Preanalysis then
+            Legal   := True;
+            Spec_Id := Current_Scope;
+            return;
+         end if;
+
          --  Traverse the parent chain to find the aspect or pragma where the
          --  attribute resides.
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 595a741..15b3c44 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -26,6 +26,7 @@
 with Aspects;        use Aspects;
 with Atree;          use Atree;
 with Checks;         use Checks;
+with Contracts;      use Contracts;
 with Debug;          use Debug;
 with Einfo;          use Einfo;
 with Einfo.Entities; use Einfo.Entities;
@@ -4446,6 +4447,38 @@ package body Sem_Ch13 is
                      goto Continue;
                   end if;
 
+                  --  Remember class-wide conditions; they will be merged
+                  --  with inherited conditions.
+
+                  if Class_Present (Aspect)
+                    and then A_Id in Aspect_Pre | Aspect_Post
+                    and then Is_Subprogram (E)
+                    and then not Is_Ignored_Ghost_Entity (E)
+                  then
+                     if A_Id = Aspect_Pre then
+                        if Is_Ignored (Aspect) then
+                           Set_Ignored_Class_Preconditions (E,
+                             New_Copy_Tree (Expr));
+                        else
+                           Set_Class_Preconditions (E, New_Copy_Tree (Expr));
+                        end if;
+
+                     --  Postconditions may split into separate aspects, and we
+                     --  remember the expression before such split (i.e. when
+                     --  the first postcondition is processed).
+
+                     elsif No (Class_Postconditions (E))
+                       and then No (Ignored_Class_Postconditions (E))
+                     then
+                        if Is_Ignored (Aspect) then
+                           Set_Ignored_Class_Postconditions (E,
+                             New_Copy_Tree (Expr));
+                        else
+                           Set_Class_Postconditions (E, New_Copy_Tree (Expr));
+                        end if;
+                     end if;
+                  end if;
+
                   --  If the expressions is of the form A and then B, then
                   --  we generate separate Pre/Post aspects for the separate
                   --  clauses. Since we allow multiple pragmas, there is no
@@ -13169,6 +13202,13 @@ package body Sem_Ch13 is
             end if;
          end Check_Variant_Part;
       end if;
+
+      if not In_Generic_Scope (E)
+        and then Ekind (E) = E_Record_Type
+        and then Is_Tagged_Type (E)
+      then
+         Process_Class_Conditions_At_Freeze_Point (E);
+      end if;
    end Freeze_Entity_Checks;
 
    -------------------------
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 7a8d0cc..63bb80c 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -3028,6 +3028,10 @@ package body Sem_Ch5 is
             then
                Analyze_And_Resolve (Original_Bound, Typ);
                return Original_Bound;
+
+            elsif Inside_Class_Condition_Preanalysis then
+               Analyze_And_Resolve (Original_Bound, Typ);
+               return Original_Bound;
             end if;
 
             --  Normally, the best approach is simply to generate a constant
@@ -3333,11 +3337,17 @@ package body Sem_Ch5 is
       --  or post-condition has been expanded. Update the type of the loop
       --  variable to reflect the proper itype at each stage of analysis.
 
+      --  Loop_Nod might not be present when we are preanalyzing a class-wide
+      --  pre/postcondition since preanalysis occurs in a place unrelated to
+      --  the actual code and the quantified expression may be the outermost
+      --  expression of the class-wide condition.
+
       if No (Etype (Id))
         or else Etype (Id) = Any_Type
         or else
           (Present (Etype (Id))
             and then Is_Itype (Etype (Id))
+            and then Present (Loop_Nod)
             and then Nkind (Parent (Loop_Nod)) = N_Expression_With_Actions
             and then Nkind (Original_Node (Parent (Loop_Nod))) =
                                                    N_Quantified_Expression)
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 0292834..1fcbdfb 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -4498,29 +4498,6 @@ package body Sem_Ch6 is
          end if;
       end if;
 
-      --  If the subprogram has a class-wide clone, build its body as a copy
-      --  of the original body, and rewrite body of original subprogram as a
-      --  wrapper that calls the clone. If N is a stub, this construction will
-      --  take place when the proper body is analyzed. No action needed if this
-      --  subprogram has been eliminated.
-
-      if Present (Spec_Id)
-        and then Present (Class_Wide_Clone (Spec_Id))
-        and then (Comes_From_Source (N) or else Was_Expression_Function (N))
-        and then Nkind (N) /= N_Subprogram_Body_Stub
-        and then not (Expander_Active and then Is_Eliminated (Spec_Id))
-      then
-         Build_Class_Wide_Clone_Body (Spec_Id, N);
-
-         --  This is the new body for the existing primitive operation
-
-         Rewrite (N, Build_Class_Wide_Clone_Call
-           (Sloc (N), New_List, Spec_Id, Parent (Spec_Id)));
-         Set_Has_Completion (Spec_Id, False);
-         Analyze (N);
-         return;
-      end if;
-
       --  Place subprogram on scope stack, and make formals visible. If there
       --  is a spec, the visible entity remains that of the spec.
 
@@ -10413,6 +10390,7 @@ package body Sem_Ch6 is
    begin
       Set_Is_Immediately_Visible (E);
       Set_Current_Entity (E);
+      pragma Assert (Prev /= E);
       Set_Homonym (E, Prev);
    end Install_Entity;
 
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index cc612db..cba3c9d 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -32,9 +32,11 @@ with Einfo.Entities; use Einfo.Entities;
 with Einfo.Utils;    use Einfo.Utils;
 with Exp_Disp;       use Exp_Disp;
 with Exp_Util;       use Exp_Util;
+with Exp_Ch6;        use Exp_Ch6;
 with Exp_Ch7;        use Exp_Ch7;
 with Exp_Tss;        use Exp_Tss;
 with Errout;         use Errout;
+with Freeze;         use Freeze;
 with Lib.Xref;       use Lib.Xref;
 with Namet;          use Namet;
 with Nlists;         use Nlists;
@@ -197,6 +199,91 @@ package body Sem_Disp is
       return Empty;
    end Covered_Interface_Op;
 
+   ----------------------------------
+   -- Covered_Interface_Primitives --
+   ----------------------------------
+
+   function Covered_Interface_Primitives (Prim : Entity_Id) return Elist_Id is
+      Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Prim);
+      Elmt        : Elmt_Id;
+      E           : Entity_Id;
+      Result      : Elist_Id := No_Elist;
+
+   begin
+      pragma Assert (Is_Dispatching_Operation (Prim));
+
+      --  Although this is a dispatching primitive we must check if its
+      --  dispatching type is available because it may be the primitive
+      --  of a private type not defined as tagged in its partial view.
+
+      if Present (Tagged_Type) and then Has_Interfaces (Tagged_Type) then
+
+         --  If the tagged type is frozen then the internal entities associated
+         --  with interfaces are available in the list of primitives of the
+         --  tagged type and can be used to speed up this search.
+
+         if Is_Frozen (Tagged_Type) then
+            Elmt := First_Elmt (Primitive_Operations (Tagged_Type));
+            while Present (Elmt) loop
+               E := Node (Elmt);
+
+               if Present (Interface_Alias (E))
+                 and then Alias (E) = Prim
+               then
+                  if No (Result) then
+                     Result := New_Elmt_List;
+                  end if;
+
+                  Append_Elmt (Interface_Alias (E), Result);
+               end if;
+
+               Next_Elmt (Elmt);
+            end loop;
+
+         --  Otherwise we must collect all the interface primitives and check
+         --  whether the Prim overrides (implements) some interface primitive.
+
+         else
+            declare
+               Ifaces_List : Elist_Id;
+               Iface_Elmt  : Elmt_Id;
+               Iface       : Entity_Id;
+               Iface_Prim  : Entity_Id;
+
+            begin
+               Collect_Interfaces (Tagged_Type, Ifaces_List);
+
+               Iface_Elmt := First_Elmt (Ifaces_List);
+               while Present (Iface_Elmt) loop
+                  Iface := Node (Iface_Elmt);
+
+                  Elmt := First_Elmt (Primitive_Operations (Iface));
+                  while Present (Elmt) loop
+                     Iface_Prim := Node (Elmt);
+
+                     if Chars (Iface_Prim) = Chars (Prim)
+                       and then Is_Interface_Conformant
+                                  (Tagged_Type, Iface_Prim, Prim)
+                     then
+                        if No (Result) then
+                           Result := New_Elmt_List;
+                        end if;
+
+                        Append_Elmt (Iface_Prim, Result);
+                     end if;
+
+                     Next_Elmt (Elmt);
+                  end loop;
+
+                  Next_Elmt (Iface_Elmt);
+               end loop;
+            end;
+         end if;
+      end if;
+
+      return Result;
+   end Covered_Interface_Primitives;
+
    -------------------------------
    -- Check_Controlling_Formals --
    -------------------------------
@@ -592,6 +679,14 @@ package body Sem_Disp is
       --  Start of processing for Check_Dispatching_Context
 
       begin
+         --  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.
+
+         if Inside_Class_Condition_Preanalysis then
+            return;
+         end if;
+
          --  If the called subprogram is a private overriding, replace it
          --  with its alias, which has the correct body. Verify that the
          --  two subprograms have the same controlling type (this is not the
@@ -992,10 +1087,17 @@ package body Sem_Disp is
          --  nonstatic values, then report an error. This is specified by
          --  RM 6.1.1(18.2/5) (by AI12-0412).
 
+         --  Skip reporting this error on helpers and indirect-call wrappers
+         --  built to support class-wide preconditions.
+
          if No (Control)
            and then not Is_Abstract_Subprogram (Subp_Entity)
            and then
              Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Subp_Entity)
+           and then not
+             (Is_Subprogram (Current_Scope)
+                and then
+              Present (Class_Preconditions_Subprogram (Current_Scope)))
          then
             Error_Msg_N
               ("nondispatching call to nonabstract subprogram of "
@@ -1463,6 +1565,9 @@ package body Sem_Disp is
                               end;
                            end if;
                         end if;
+
+                        Check_Inherited_Conditions (Tagged_Type,
+                          Late_Overriding => True);
                      end if;
                   end if;
                end;
@@ -2925,6 +3030,11 @@ package body Sem_Disp is
          Next_Actual (Arg);
       end loop;
 
+      --  Add class-wide precondition check if the target of this dispatching
+      --  call has or inherits class-wide preconditions.
+
+      Install_Class_Preconditions_Check (Call_Node);
+
       --  Expansion of dispatching calls is suppressed on VM targets, because
       --  the VM back-ends directly handle the generation of dispatching calls
       --  and would have to undo any expansion to an indirect call.
diff --git a/gcc/ada/sem_disp.ads b/gcc/ada/sem_disp.ads
index 7b42cf5..f37391b 100644
--- a/gcc/ada/sem_disp.ads
+++ b/gcc/ada/sem_disp.ads
@@ -74,6 +74,10 @@ package Sem_Disp is
    --  The Alias of Old_Subp is adjusted to point to the inherited procedure
    --  of the full view because it is always this one which has to be called.
 
+   function Covered_Interface_Primitives (Prim : Entity_Id) return Elist_Id;
+   --  Returns all the interface primitives covered by Prim, when its
+   --  controlling type has progenitors.
+
    function Covered_Interface_Op (Prim : Entity_Id) return Entity_Id;
    --  Returns the interface primitive that Prim covers, when its controlling
    --  type has progenitors.
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0228717..7386ecc 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -25896,23 +25896,6 @@ package body Sem_Prag is
                        ("operation in class-wide condition must be primitive "
                         & "of &", Nod, Disp_Typ);
                   end if;
-
-               --  Otherwise we have a call to an overridden primitive, and we
-               --  will create a common class-wide clone for the body of
-               --  original operation and its eventual inherited versions. If
-               --  the original operation dispatches on result it is never
-               --  inherited and there is no need for a clone. There is not
-               --  need for a clone either in GNATprove mode, as cases that
-               --  would require it are rejected (when an inherited primitive
-               --  calls an overridden operation in a class-wide contract), and
-               --  the clone would make proof impossible in some cases.
-
-               elsif not Is_Abstract_Subprogram (Spec_Id)
-                 and then No (Class_Wide_Clone (Spec_Id))
-                 and then not Has_Controlling_Result (Spec_Id)
-                 and then not GNATprove_Mode
-               then
-                  Build_Class_Wide_Clone_Decl (Spec_Id);
                end if;
             end;
 
@@ -26033,15 +26016,6 @@ package body Sem_Prag is
          End_Scope;
       end if;
 
-      --  If analysis of the condition indicates that a class-wide clone
-      --  has been created, build and analyze its declaration.
-
-      if Is_Subprogram (Spec_Id)
-        and then Present (Class_Wide_Clone (Spec_Id))
-      then
-         Analyze (Unit_Declaration_Node (Class_Wide_Clone (Spec_Id)));
-      end if;
-
       --  Currently it is not possible to inline pre/postconditions on a
       --  subprogram subject to pragma Inline_Always.
 
@@ -29528,9 +29502,6 @@ package body Sem_Prag is
       Msg_Arg    : Node_Id;
       Nam        : Name_Id;
 
-      Needs_Wrapper : Boolean;
-      pragma Unreferenced (Needs_Wrapper);
-
    --  Start of processing for Build_Pragma_Check_Equivalent
 
    begin
@@ -29557,11 +29528,10 @@ package body Sem_Prag is
          --  Build the inherited class-wide condition
 
          Build_Class_Wide_Expression
-           (Prag          => Check_Prag,
-            Subp          => Subp_Id,
-            Par_Subp      => Inher_Id,
-            Adjust_Sloc   => True,
-            Needs_Wrapper => Needs_Wrapper);
+           (Pragma_Or_Expr => Check_Prag,
+            Subp           => Subp_Id,
+            Par_Subp       => Inher_Id,
+            Adjust_Sloc    => True);
 
       --  If not an inherited condition simply copy the original pragma
 
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 7b9f8ab..0d013ba 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -4891,10 +4891,15 @@ package body Sem_Res is
 
             --  Apply legality rule 3.9.2  (9/1)
 
+            --  Skip this check on helpers and indirect-call wrappers built to
+            --  support class-wide preconditions.
+
             if (Is_Class_Wide_Type (A_Typ) or else Is_Dynamically_Tagged (A))
               and then not Is_Class_Wide_Type (F_Typ)
               and then not Is_Controlling_Formal (F)
               and then not In_Instance
+              and then (not Is_Subprogram (Nam)
+                         or else No (Class_Preconditions_Subprogram (Nam)))
             then
                Error_Msg_N ("class-wide argument not allowed here!", A);
 
@@ -4992,9 +4997,13 @@ package body Sem_Res is
             --  "False" cannot act as an actual in a subprogram with value
             --  "True" (SPARK RM 6.1.7(3)).
 
+            --  No check needed for helpers and indirect-call wrappers built to
+            --  support class-wide preconditions.
+
             if Is_EVF_Expression (A)
               and then Extensions_Visible_Status (Nam) =
                        Extensions_Visible_True
+              and then No (Class_Preconditions_Subprogram (Current_Scope))
             then
                Error_Msg_N
                  ("formal parameter cannot act as actual parameter when "
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 816fb45..98e68779 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -2212,180 +2212,6 @@ package body Sem_Util is
       return Empty;
    end Build_Actual_Subtype_Of_Component;
 
-   ---------------------------------
-   -- Build_Class_Wide_Clone_Body --
-   ---------------------------------
-
-   procedure Build_Class_Wide_Clone_Body
-     (Spec_Id : Entity_Id;
-      Bod     : Node_Id)
-   is
-      Loc        : constant Source_Ptr := Sloc (Bod);
-      Clone_Id   : constant Entity_Id  := Class_Wide_Clone (Spec_Id);
-      Clone_Body : Node_Id;
-      Assoc_List : constant Elist_Id := New_Elmt_List;
-
-   begin
-      --  The declaration of the class-wide clone was created when the
-      --  corresponding class-wide condition was analyzed.
-
-      --  The body of the original condition may contain references to
-      --  the formals of Spec_Id. In the body of the class-wide clone,
-      --  these must be replaced with the corresponding formals of
-      --  the clone.
-
-      declare
-         Spec_Formal_Id  : Entity_Id := First_Formal (Spec_Id);
-         Clone_Formal_Id : Entity_Id := First_Formal (Clone_Id);
-      begin
-         while Present (Spec_Formal_Id) loop
-            Append_Elmt (Spec_Formal_Id,  Assoc_List);
-            Append_Elmt (Clone_Formal_Id, Assoc_List);
-
-            Next_Formal (Spec_Formal_Id);
-            Next_Formal (Clone_Formal_Id);
-         end loop;
-      end;
-
-      Clone_Body :=
-        Make_Subprogram_Body (Loc,
-          Specification              =>
-            Copy_Subprogram_Spec (Parent (Clone_Id)),
-          Declarations               => Declarations (Bod),
-          Handled_Statement_Sequence =>
-            New_Copy_Tree (Handled_Statement_Sequence (Bod),
-              Map => Assoc_List));
-
-      --  The new operation is internal and overriding indicators do not apply
-      --  (the original primitive may have carried one).
-
-      Set_Must_Override (Specification (Clone_Body), False);
-
-      --  If the subprogram body is the proper body of a stub, insert the
-      --  subprogram after the stub, i.e. the same declarative region as
-      --  the original sugprogram.
-
-      if Nkind (Parent (Bod)) = N_Subunit then
-         Insert_After (Corresponding_Stub (Parent (Bod)), Clone_Body);
-
-      else
-         Insert_Before (Bod, Clone_Body);
-      end if;
-
-      Analyze (Clone_Body);
-   end Build_Class_Wide_Clone_Body;
-
-   ---------------------------------
-   -- Build_Class_Wide_Clone_Call --
-   ---------------------------------
-
-   function Build_Class_Wide_Clone_Call
-     (Loc     : Source_Ptr;
-      Decls   : List_Id;
-      Spec_Id : Entity_Id;
-      Spec    : Node_Id) return Node_Id
-   is
-      Clone_Id : constant Entity_Id := Class_Wide_Clone (Spec_Id);
-      Par_Type : constant Entity_Id := Find_Dispatching_Type (Spec_Id);
-
-      Actuals    : List_Id;
-      Call       : Node_Id;
-      Formal     : Entity_Id;
-      New_Body   : Node_Id;
-      New_F_Spec : Entity_Id;
-      New_Formal : Entity_Id;
-
-   begin
-      Actuals    := Empty_List;
-      Formal     := First_Formal (Spec_Id);
-      New_F_Spec := First (Parameter_Specifications (Spec));
-
-      --  Build parameter association for call to class-wide clone.
-
-      while Present (Formal) loop
-         New_Formal := Defining_Identifier (New_F_Spec);
-
-         --  If controlling argument and operation is inherited, add conversion
-         --  to parent type for the call.
-
-         if Etype (Formal) = Par_Type
-           and then not Is_Empty_List (Decls)
-         then
-            Append_To (Actuals,
-              Make_Type_Conversion (Loc,
-                New_Occurrence_Of (Par_Type, Loc),
-                New_Occurrence_Of (New_Formal, Loc)));
-
-         else
-            Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
-         end if;
-
-         Next_Formal (Formal);
-         Next (New_F_Spec);
-      end loop;
-
-      if Ekind (Spec_Id) = E_Procedure then
-         Call :=
-           Make_Procedure_Call_Statement (Loc,
-             Name                   => New_Occurrence_Of (Clone_Id, Loc),
-             Parameter_Associations => Actuals);
-      else
-         Call :=
-           Make_Simple_Return_Statement (Loc,
-            Expression =>
-              Make_Function_Call (Loc,
-                Name                   => New_Occurrence_Of (Clone_Id, Loc),
-                Parameter_Associations => Actuals));
-      end if;
-
-      New_Body :=
-        Make_Subprogram_Body (Loc,
-          Specification              =>
-            Copy_Subprogram_Spec (Spec),
-          Declarations               => Decls,
-          Handled_Statement_Sequence =>
-            Make_Handled_Sequence_Of_Statements (Loc,
-              Statements => New_List (Call),
-              End_Label  => Make_Identifier (Loc, Chars (Spec_Id))));
-
-      return New_Body;
-   end Build_Class_Wide_Clone_Call;
-
-   ---------------------------------
-   -- Build_Class_Wide_Clone_Decl --
-   ---------------------------------
-
-   procedure Build_Class_Wide_Clone_Decl (Spec_Id : Entity_Id) is
-      Loc      : constant Source_Ptr := Sloc (Spec_Id);
-      Clone_Id : constant Entity_Id  :=
-                   Make_Defining_Identifier (Loc,
-                     New_External_Name (Chars (Spec_Id), Suffix => "CL"));
-
-      Decl : Node_Id;
-      Spec : Node_Id;
-
-   begin
-      Spec := Copy_Subprogram_Spec (Parent (Spec_Id));
-      Set_Must_Override      (Spec, False);
-      Set_Must_Not_Override  (Spec, False);
-      Set_Defining_Unit_Name (Spec, Clone_Id);
-
-      Decl := Make_Subprogram_Declaration (Loc, Spec);
-      Append (Decl, List_Containing (Unit_Declaration_Node (Spec_Id)));
-
-      --  Link clone to original subprogram, for use when building body and
-      --  wrapper call to inherited operation.
-
-      Set_Class_Wide_Clone (Spec_Id, Clone_Id);
-
-      --  Inherit debug info flag from Spec_Id to Clone_Id to allow debugging
-      --  of the class-wide clone subprogram.
-
-      if Needs_Debug_Info (Spec_Id) then
-         Set_Debug_Info_Needed (Clone_Id);
-      end if;
-   end Build_Class_Wide_Clone_Decl;
-
    -----------------------------
    -- Build_Component_Subtype --
    -----------------------------
@@ -5878,6 +5704,30 @@ package body Sem_Util is
       end if;
    end Choice_List;
 
+   ---------------------
+   -- Class_Condition --
+   ---------------------
+
+   function Class_Condition
+     (Kind : Condition_Kind;
+      Subp : Entity_Id) return Node_Id is
+
+   begin
+      case Kind is
+         when Class_Postcondition =>
+            return Class_Postconditions (Subp);
+
+         when Class_Precondition =>
+            return Class_Preconditions (Subp);
+
+         when Ignored_Class_Postcondition =>
+            return Ignored_Class_Postconditions (Subp);
+
+         when Ignored_Class_Precondition =>
+            return Ignored_Class_Preconditions (Subp);
+      end case;
+   end Class_Condition;
+
    -------------------------
    -- Collect_Body_States --
    -------------------------
@@ -22789,6 +22639,61 @@ package body Sem_Util is
       return Result;
    end Might_Raise;
 
+   ----------------------------------------
+   -- Nearest_Class_Condition_Subprogram --
+   ----------------------------------------
+
+   function Nearest_Class_Condition_Subprogram
+     (Kind    : Condition_Kind;
+      Spec_Id : Entity_Id) return Entity_Id
+   is
+      Subp_Id : constant Entity_Id := Ultimate_Alias (Spec_Id);
+
+   begin
+      --  Prevent cascaded errors
+
+      if not Is_Dispatching_Operation (Subp_Id) then
+         return Empty;
+
+      --  No need to search if this subprogram has class-wide postconditions
+
+      elsif Present (Class_Condition (Kind, Subp_Id)) then
+         return Subp_Id;
+      end if;
+
+      --  Process the contracts of inherited subprograms, looking for
+      --  class-wide pre/postconditions.
+
+      declare
+         Subps   : constant Subprogram_List := Inherited_Subprograms (Subp_Id);
+         Subp_Id : Entity_Id;
+
+      begin
+         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/postconditions 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;
+
+            if Present (Class_Condition (Kind, Subp_Id)) then
+               return Subp_Id;
+            end if;
+         end loop;
+      end;
+
+      return Empty;
+   end Nearest_Class_Condition_Subprogram;
+
    --------------------------------
    -- Nearest_Enclosing_Instance --
    --------------------------------
@@ -31535,8 +31440,16 @@ package body Sem_Util is
                --  type case correctly, so we avoid that problem by
                --  returning True here.
                return True;
+
             elsif Ada_Version < Ada_2022 then
                return False;
+
+            elsif Inside_Class_Condition_Preanalysis then
+               --  No need to evaluate it during preanalysis of a class-wide
+               --  pre/postcondition since the expression is not installed yet
+               --  on its definite context.
+               return False;
+
             elsif not Is_Conditionally_Evaluated (Expr) then
                return False;
             else
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 4e896a35..7a77715 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -283,30 +283,6 @@ package Sem_Util is
    --  take care of constructing declaration and body of the clone, and
    --  building the calls to it within the appropriate wrappers.
 
-   procedure Build_Class_Wide_Clone_Body
-     (Spec_Id  : Entity_Id;
-      Bod      : Node_Id);
-   --  Build body of subprogram that has a class-wide condition that contains
-   --  calls to other primitives. Spec_Id is the Id of the subprogram, and B
-   --  is its source body, which becomes the body of the clone.
-
-   function Build_Class_Wide_Clone_Call
-    (Loc      : Source_Ptr;
-     Decls    : List_Id;
-     Spec_Id  : Entity_Id;
-     Spec     : Node_Id) return Node_Id;
-   --  Build a call to the common class-wide clone of a subprogram with
-   --  class-wide conditions. The body of the subprogram becomes a wrapper
-   --  for a call to the clone. The inherited operation becomes a similar
-   --  wrapper to which modified conditions apply, and the call to the
-   --  clone includes the proper conversion in a call the parent operation.
-
-   procedure Build_Class_Wide_Clone_Decl (Spec_Id : Entity_Id);
-   --  For a subprogram that has a class-wide condition that contains calls
-   --  to other primitives, build an internal subprogram that is invoked
-   --  through a type-specific wrapper for all inherited subprograms that
-   --  may have a modified condition.
-
    procedure Build_Constrained_Itype
      (N              : Node_Id;
       Typ            : Entity_Id;
@@ -527,6 +503,18 @@ package Sem_Util is
    --  reasons these nodes have a different structure even though they play
    --  similar roles in array aggregates.
 
+   type Condition_Kind is
+     (Ignored_Class_Precondition,
+      Ignored_Class_Postcondition,
+      Class_Precondition,
+      Class_Postcondition);
+   --  Kind of class-wide conditions
+
+   function Class_Condition
+     (Kind : Condition_Kind;
+      Subp : Entity_Id) return Node_Id;
+   --  Class-wide Kind condition of Subp
+
    function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id;
    --  Gather the entities of all abstract states and objects declared in the
    --  body state space of package body Body_Id.
@@ -2621,6 +2609,12 @@ package Sem_Util is
    --  if we're not sure, we return True. If N is a subprogram body, this is
    --  about whether execution of that body can raise.
 
+   function Nearest_Class_Condition_Subprogram
+     (Kind    : Condition_Kind;
+      Spec_Id : Entity_Id) return Entity_Id;
+   --  Return the nearest ancestor containing the merged class-wide conditions
+   --  that statically apply to Spec_Id; return Empty otherwise.
+
    function Nearest_Enclosing_Instance (E : Entity_Id) return Entity_Id;
    --  Return the entity of the nearest enclosing instance which encapsulates
    --  entity E. If no such instance exits, return Empty.