diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 94e729e9bcc..d84d114bef1 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -189,7 +189,7 @@ package body Debug is
    --  d_U  Disable prepending messages with "error:".
    --  d_V  Enable verifications on the expanded tree
    --  d_W
-   --  d_X
+   --  d_X  Disable assertions to check matching of extra formals
    --  d_Y
    --  d_Z
 
@@ -1044,6 +1044,10 @@ package body Debug is
    --  d_V  Enable verification of the expanded code before calling the backend
    --       and generate error messages on each inconsistency found.
 
+   --  d_X  Disable assertions to check matching of extra formals; switch added
+   --       temporarily to disable these checks until this work is complete if
+   --       they cause unexpected assertion failures.
+
    --  d1   Error messages have node numbers where possible. Normally error
    --       messages have only source locations. This option is useful when
    --       debugging errors caused by expanded code, where the source location
diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index 25f16276c5e..9c8d80ffe25 100644
--- a/gcc/ada/exp_attr.adb
+++ b/gcc/ada/exp_attr.adb
@@ -2316,19 +2316,40 @@ 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 subprogram that has class-wide preconditions
+               --  and an indirect-call wrapper (ICW) of the subprogram is
+               --  available then replace the prefix by the ICW.
+
+               if 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);
+               end if;
+
+               --  Ensure the availability of the extra formals to check that
+               --  they match.
+
+               if not Is_Frozen (Entity (Pref))
+                 or else From_Limited_With (Etype (Entity (Pref)))
+               then
+                  Create_Extra_Formals (Entity (Pref));
+               end if;
+
+               if not Is_Frozen (Btyp_DDT)
+                 or else From_Limited_With (Etype (Btyp_DDT))
+               then
+                  Create_Extra_Formals (Btyp_DDT);
+               end if;
+
+               pragma Assert
+                 (Extra_Formals_Match_OK
+                   (E => Entity (Pref), Ref_E => Btyp_DDT));
 
             --  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 1e70b584f22..90f01ca2747 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -44,7 +44,6 @@ with Exp_Dist;       use Exp_Dist;
 with Exp_Put_Image;
 with Exp_Smem;       use Exp_Smem;
 with Exp_Strm;       use Exp_Strm;
-with Exp_Tss;        use Exp_Tss;
 with Exp_Util;       use Exp_Util;
 with Freeze;         use Freeze;
 with Ghost;          use Ghost;
@@ -408,15 +407,6 @@ package body Exp_Ch3 is
    --  Freeze entities of all predefined primitive operations. This is needed
    --  because the bodies of these operations do not normally do any freezing.
 
-   function Stream_Operation_OK
-     (Typ       : Entity_Id;
-      Operation : TSS_Name_Type) return Boolean;
-   --  Check whether the named stream operation must be emitted for a given
-   --  type. The rules for inheritance of stream attributes by type extensions
-   --  are enforced by this function. Furthermore, various restrictions prevent
-   --  the generation of these operations, as a useful optimization or for
-   --  certification purposes and to save unnecessary generated code.
-
    --------------------------
    -- Adjust_Discriminants --
    --------------------------
@@ -5380,6 +5370,10 @@ package body Exp_Ch3 is
       procedure Register_Dispatch_Table_Wrappers (Typ : Entity_Id);
       --  Register dispatch-table wrappers in the dispatch table of Typ
 
+      procedure Validate_Tagged_Type_Extra_Formals (Typ : Entity_Id);
+      --  Check extra formals of dispatching primitives of tagged type Typ.
+      --  Used in pragma Debug.
+
       ---------------------------------------
       -- Build_Class_Condition_Subprograms --
       ---------------------------------------
@@ -5509,6 +5503,78 @@ package body Exp_Ch3 is
          end loop;
       end Register_Dispatch_Table_Wrappers;
 
+      ----------------------------------------
+      -- Validate_Tagged_Type_Extra_Formals --
+      ----------------------------------------
+
+      procedure Validate_Tagged_Type_Extra_Formals (Typ : Entity_Id) is
+         Ovr_Subp : Entity_Id;
+         Elmt     : Elmt_Id;
+         Subp     : Entity_Id;
+
+      begin
+         pragma Assert (not Is_Class_Wide_Type (Typ));
+
+         --  No check required if expansion is not active since we never
+         --  generate extra formals in such case.
+
+         if not Expander_Active then
+            return;
+         end if;
+
+         Elmt := First_Elmt (Primitive_Operations (Typ));
+         while Present (Elmt) loop
+            Subp := Node (Elmt);
+
+            --  Extra formals of a dispatching primitive must match:
+
+            --  1) The extra formals of its covered interface primitive
+
+            if Present (Interface_Alias (Subp)) then
+               pragma Assert
+                 (Extra_Formals_Match_OK
+                   (E     => Interface_Alias (Subp),
+                    Ref_E => Alias (Subp)));
+            end if;
+
+            --  2) The extra formals of its renamed primitive
+
+            if Present (Alias (Subp)) then
+               pragma Assert
+                 (Extra_Formals_Match_OK
+                   (E     => Subp,
+                    Ref_E => Ultimate_Alias (Subp)));
+            end if;
+
+            --  3) The extra formals of its overridden primitive
+
+            if Present (Overridden_Operation (Subp)) then
+               Ovr_Subp := Overridden_Operation (Subp);
+
+               --  Handle controlling function wrapper
+
+               if Is_Wrapper (Subp)
+                 and then Ultimate_Alias (Ovr_Subp) = Subp
+               then
+                  if Present (Overridden_Operation (Ovr_Subp)) then
+                     pragma Assert
+                       (Extra_Formals_Match_OK
+                         (E     => Subp,
+                          Ref_E => Overridden_Operation (Ovr_Subp)));
+                  end if;
+
+               else
+                  pragma Assert
+                    (Extra_Formals_Match_OK
+                      (E     => Subp,
+                       Ref_E => Ovr_Subp));
+               end if;
+            end if;
+
+            Next_Elmt (Elmt);
+         end loop;
+      end Validate_Tagged_Type_Extra_Formals;
+
       --  Local variables
 
       Typ      : constant Node_Id := Entity (N);
@@ -5897,28 +5963,58 @@ package body Exp_Ch3 is
          --  inherited functions, then add their bodies to the freeze actions.
 
          Append_Freeze_Actions (Typ, Wrapper_Body_List);
+      end if;
 
-         --  Create extra formals for the primitive operations of the type.
-         --  This must be done before analyzing the body of the initialization
-         --  procedure, because a self-referential type might call one of these
-         --  primitives in the body of the init_proc itself.
+      --  Create extra formals for the primitive operations of the type.
+      --  This must be done before analyzing the body of the initialization
+      --  procedure, because a self-referential type might call one of these
+      --  primitives in the body of the init_proc itself.
+      --
+      --  This is not needed:
+      --    1) If expansion is disabled, because extra formals are only added
+      --       when we are generating code.
+      --
+      --    2) For types with foreign convention since primitives with foreign
+      --       convention don't have extra formals and AI95-117 requires that
+      --       all primitives of a tagged type inherit the convention.
 
+      if Expander_Active
+        and then Is_Tagged_Type (Typ)
+        and then not Has_Foreign_Convention (Typ)
+      then
          declare
             Elmt : Elmt_Id;
-            Subp : Entity_Id;
+            E    : Entity_Id;
 
          begin
+            --  Add extra formals to primitive operations
+
             Elmt := First_Elmt (Primitive_Operations (Typ));
             while Present (Elmt) loop
-               Subp := Node (Elmt);
-               if not Has_Foreign_Convention (Subp)
-                 and then not Is_Predefined_Dispatching_Operation (Subp)
+               Create_Extra_Formals (Node (Elmt));
+               Next_Elmt (Elmt);
+            end loop;
+
+            --  Add extra formals to renamings of primitive operations. The
+            --  addition of extra formals is done in two steps to minimize
+            --  the compile time required for this action; the evaluation of
+            --  Find_Dispatching_Type() and Contains() is only done here for
+            --  renamings that are not primitive operations.
+
+            E := First_Entity (Scope (Typ));
+            while Present (E) loop
+               if Is_Dispatching_Operation (E)
+                 and then Present (Alias (E))
+                 and then Find_Dispatching_Type (E) = Typ
+                 and then not Contains (Primitive_Operations (Typ), E)
                then
-                  Create_Extra_Formals (Subp);
+                  Create_Extra_Formals (E);
                end if;
 
-               Next_Elmt (Elmt);
+               Next_Entity (E);
             end loop;
+
+            pragma Debug (Validate_Tagged_Type_Extra_Formals (Typ));
          end;
       end if;
 
diff --git a/gcc/ada/exp_ch3.ads b/gcc/ada/exp_ch3.ads
index f7d43c4aa7e..24e2263296d 100644
--- a/gcc/ada/exp_ch3.ads
+++ b/gcc/ada/exp_ch3.ads
@@ -25,9 +25,10 @@
 
 --  Expand routines for chapter 3 constructs
 
-with Types;  use Types;
-with Elists; use Elists;
-with Uintp;  use Uintp;
+with Types;   use Types;
+with Elists;  use Elists;
+with Exp_Tss; use Exp_Tss;
+with Uintp;   use Uintp;
 
 package Exp_Ch3 is
 
@@ -207,4 +208,13 @@ package Exp_Ch3 is
    --  Make_Predefined_Primitive_Eq_Spec; see there for description of
    --  the Renamed_Eq parameter.
 
+   function Stream_Operation_OK
+     (Typ       : Entity_Id;
+      Operation : TSS_Name_Type) return Boolean;
+   --  Check whether the named stream operation must be emitted for a given
+   --  type. The rules for inheritance of stream attributes by type extensions
+   --  are enforced by this function. Furthermore, various restrictions prevent
+   --  the generation of these operations, as a useful optimization or for
+   --  certification purposes and to save unnecessary generated code.
+
 end Exp_Ch3;
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 0fa97688c5b..fce7a7cebf5 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -214,7 +214,8 @@ package body Exp_Ch6 is
      (Subp_Call : Node_Id;
       Subp_Id   : Entity_Id) return Boolean;
    --  Given a subprogram call to the given subprogram return True if the
-   --  names of BIP extra actual and formal parameters match.
+   --  names of BIP extra actual and formal parameters match, and the number
+   --  of actuals (including extra actuals) matches the number of formals.
 
    function Check_Number_Of_Actuals
      (Subp_Call : Node_Id;
@@ -314,15 +315,6 @@ package body Exp_Ch6 is
    --  Expand simple return from function. In the case where we are returning
    --  from a function body this is called by Expand_N_Simple_Return_Statement.
 
-   function Has_BIP_Extra_Formal
-     (E    : Entity_Id;
-      Kind : BIP_Formal_Kind) return Boolean;
-   --  Given a frozen subprogram, subprogram type, entry or entry family,
-   --  return True if E has the BIP extra formal associated with Kind. It must
-   --  be invoked with a frozen entity or a subprogram type of a dispatching
-   --  call since we can only rely on the availability of the extra formals
-   --  on these entities.
-
    procedure Insert_Post_Call_Actions (N : Node_Id; Post_Call : List_Id);
    --  Insert the Post_Call list previously produced by routine Expand_Actuals
    --  or Expand_Call_Helper into the tree.
@@ -3342,9 +3334,53 @@ package body Exp_Ch6 is
       ------------------------------
 
       procedure Check_Subprogram_Variant is
+
+         function Duplicate_Params_Without_Extra_Actuals
+           (Call_Node : Node_Id) return List_Id;
+         --  Duplicate actual parameters of Call_Node into New_Call without
+         --  extra actuals.
+
+         --------------------------------------------
+         -- Duplicate_Params_Without_Extra_Actuals --
+         --------------------------------------------
+
+         function Duplicate_Params_Without_Extra_Actuals
+           (Call_Node : Node_Id) return List_Id
+         is
+            Proc_Id : constant Entity_Id := Entity (Name (Call_Node));
+            Actuals : constant List_Id := Parameter_Associations (Call_Node);
+            NL      : List_Id;
+            Actual  : Node_Or_Entity_Id;
+            Formal  : Entity_Id;
+
+         begin
+            if Actuals = No_List then
+               return No_List;
+
+            else
+               NL     := New_List;
+               Actual := First (Actuals);
+               Formal := First_Formal (Proc_Id);
+
+               while Present (Formal)
+                 and then Formal /= Extra_Formals (Proc_Id)
+               loop
+                  Append (New_Copy (Actual), NL);
+                  Next (Actual);
+
+                  Next_Formal (Formal);
+               end loop;
+
+               return NL;
+            end if;
+         end Duplicate_Params_Without_Extra_Actuals;
+
+         --  Local variables
+
          Variant_Prag : constant Node_Id :=
            Get_Pragma (Current_Scope, Pragma_Subprogram_Variant);
 
+         New_Call     : Node_Id;
          Pragma_Arg1  : Node_Id;
          Variant_Proc : Entity_Id;
 
@@ -3373,12 +3409,17 @@ package body Exp_Ch6 is
 
             Variant_Proc := Entity (Pragma_Arg1);
 
-            Insert_Action (Call_Node,
+            New_Call :=
               Make_Procedure_Call_Statement (Loc,
                  Name                   =>
                    New_Occurrence_Of (Variant_Proc, Loc),
                  Parameter_Associations =>
-                   New_Copy_List (Parameter_Associations (Call_Node))));
+                   Duplicate_Params_Without_Extra_Actuals (Call_Node));
+
+            Insert_Action (Call_Node, New_Call);
+
+            pragma Assert (Etype (New_Call) /= Any_Type
+              or else Serious_Errors_Detected > 0);
          end if;
       end Check_Subprogram_Variant;
 
@@ -3679,6 +3720,12 @@ package body Exp_Ch6 is
          end if;
       end if;
 
+      --  Ensure that the called subprogram has all its formals
+
+      if not Is_Frozen (Subp) then
+         Create_Extra_Formals (Subp);
+      end if;
+
       --  Ada 2005 (AI-345): We have a procedure call as a triggering
       --  alternative in an asynchronous select or as an entry call in
       --  a conditional or timed select. Check whether the procedure call
@@ -3817,7 +3864,7 @@ package body Exp_Ch6 is
         and then Thunk_Entity (Current_Scope) = Subp
         and then Present (Extra_Formals (Subp))
       then
-         pragma Assert (Present (Extra_Formals (Current_Scope)));
+         pragma Assert (Extra_Formals_Match_OK (Current_Scope, Subp));
 
          declare
             Target_Formal : Entity_Id;
@@ -3839,6 +3886,13 @@ package body Exp_Ch6 is
                Add_Actual_Parameter (Remove_Head (Extra_Actuals));
             end loop;
 
+            --  Mark the call as processed build-in-place call; required
+            --  to avoid adding the extra formals twice.
+
+            if Nkind (Call_Node) = N_Function_Call then
+               Set_Is_Expanded_Build_In_Place_Call (Call_Node);
+            end if;
+
             Expand_Actuals (Call_Node, Subp, Post_Call);
             pragma Assert (Is_Empty_List (Post_Call));
             pragma Assert (Check_Number_Of_Actuals (Call_Node, Subp));
@@ -6401,8 +6455,13 @@ package body Exp_Ch6 is
 
       if Nkind (Exp) = N_Function_Call then
          pragma Assert (Ekind (Scope_Id) = E_Function);
+
+         --  This assertion works fine because Is_Build_In_Place_Function_Call
+         --  returns True for BIP function calls but also for function calls
+         --  that have BIP formals.
+
          pragma Assert
-           (Is_Build_In_Place_Function (Scope_Id) =
+           (Has_BIP_Formals (Scope_Id) =
             Is_Build_In_Place_Function_Call (Exp));
          null;
       end if;
@@ -6440,7 +6499,7 @@ package body Exp_Ch6 is
       pragma Assert
         (Comes_From_Extended_Return_Statement (N)
           or else not Is_Build_In_Place_Function_Call (Exp)
-          or else Is_Build_In_Place_Function (Scope_Id));
+          or else Has_BIP_Formals (Scope_Id));
 
       if not Comes_From_Extended_Return_Statement (N)
         and then Is_Build_In_Place_Function (Scope_Id)
@@ -7044,8 +7103,9 @@ package body Exp_Ch6 is
    --------------------------
 
    function Has_BIP_Extra_Formal
-     (E    : Entity_Id;
-      Kind : BIP_Formal_Kind) return Boolean
+     (E              : Entity_Id;
+      Kind           : BIP_Formal_Kind;
+      Must_Be_Frozen : Boolean := True) return Boolean
    is
       Extra_Formal : Entity_Id := Extra_Formals (E);
 
@@ -7055,7 +7115,7 @@ package body Exp_Ch6 is
       --  extra formals are added when the target subprogram is frozen; see
       --  Expand_Dispatching_Call).
 
-      pragma Assert (Is_Frozen (E)
+      pragma Assert ((Is_Frozen (E) or else not Must_Be_Frozen)
         or else (Ekind (E) = E_Subprogram_Type
                    and then Is_Dispatch_Table_Entity (E))
         or else (Is_Dispatching_Operation (E)
@@ -7684,7 +7744,7 @@ package body Exp_Ch6 is
                or else
              (Kind = E_Subprogram_Type and then Typ /= Standard_Void_Type))
         and then Is_Build_In_Place_Result_Type (Typ)
-        and then not (Is_Imported (E) and then Has_Foreign_Convention (E));
+        and then not Has_Foreign_Convention (E);
    end Is_Build_In_Place_Function;
 
    -------------------------------------
@@ -7739,12 +7799,29 @@ package body Exp_Ch6 is
          raise Program_Error;
       end if;
 
-      declare
-         Result : constant Boolean := Is_Build_In_Place_Function (Function_Id);
-         --  So we can stop here in the debugger
-      begin
-         return Result;
-      end;
+      if Is_Build_In_Place_Function (Function_Id) then
+         return True;
+
+      --  True also if the function has BIP Formals
+
+      else
+         declare
+            Kind : constant Entity_Kind := Ekind (Function_Id);
+
+         begin
+            if (Kind in E_Function | E_Generic_Function
+                  or else (Kind = E_Subprogram_Type
+                             and then
+                           Etype (Function_Id) /= Standard_Void_Type))
+              and then Has_BIP_Formals (Function_Id)
+            then
+               --  So we can stop here in the debugger
+               return True;
+            else
+               return False;
+            end if;
+         end;
+      end if;
    end Is_Build_In_Place_Function_Call;
 
    -----------------------------------
@@ -8413,6 +8490,11 @@ package body Exp_Ch6 is
       --  initialization expression of the object to Empty, which would be
       --  illegal Ada, and would cause gigi to misallocate X.
 
+      Is_OK_Return_Object : constant Boolean :=
+        Is_Return_Object (Obj_Def_Id)
+          and then
+        not Has_Foreign_Convention (Return_Applies_To (Scope (Obj_Def_Id)));
+
    --  Start of processing for Make_Build_In_Place_Call_In_Object_Declaration
 
    begin
@@ -8465,7 +8547,7 @@ package body Exp_Ch6 is
       --  the result object is in a different (transient) scope, so won't cause
       --  freezing.
 
-      if Definite and then not Is_Return_Object (Obj_Def_Id) then
+      if Definite and then not Is_OK_Return_Object then
 
          --  The presence of an address clause complicates the build-in-place
          --  expansion because the indicated address must be processed before
@@ -8548,7 +8630,7 @@ package body Exp_Ch6 is
       --  really be directly built in place in the aggregate and not in a
       --  temporary. ???)
 
-      if Is_Return_Object (Obj_Def_Id) then
+      if Is_OK_Return_Object then
          Pass_Caller_Acc := True;
 
          --  When the enclosing function has a BIP_Alloc_Form formal then we
@@ -8733,7 +8815,7 @@ package body Exp_Ch6 is
       --  itself the return expression of an enclosing BIP function, then mark
       --  the object as having no initialization.
 
-      if Definite and then not Is_Return_Object (Obj_Def_Id) then
+      if Definite and then not Is_OK_Return_Object then
 
          --  The related object declaration is encased in a transient block
          --  because the build-in-place function call contains at least one
@@ -9090,7 +9172,7 @@ package body Exp_Ch6 is
         and then not No_Run_Time_Mode
         and then (Has_Task (Typ)
                     or else (Is_Class_Wide_Type (Typ)
-                               and then Is_Limited_Record (Typ)
+                               and then Is_Limited_Record (Etype (Typ))
                                and then not Has_Aspect
                                  (Etype (Typ), Aspect_No_Task_Parts)));
    end Might_Have_Tasks;
@@ -9100,7 +9182,6 @@ package body Exp_Ch6 is
    ----------------------------
 
    function Needs_BIP_Task_Actuals (Func_Id : Entity_Id) return Boolean is
-      pragma Assert (Is_Build_In_Place_Function (Func_Id));
       Subp_Id  : Entity_Id;
       Func_Typ : Entity_Id;
 
@@ -9125,6 +9206,12 @@ package body Exp_Ch6 is
 
       Func_Typ := Underlying_Type (Etype (Subp_Id));
 
+      --  Functions returning types with foreign convention don't have extra
+      --  formals.
+
+      if Has_Foreign_Convention (Func_Typ) then
+         return False;
+
       --  At first sight, for all the following cases, we could add assertions
       --  to ensure that if Func_Id is frozen then the computed result matches
       --  with the availability of the task master extra formal; unfortunately
@@ -9132,7 +9219,7 @@ package body Exp_Ch6 is
       --  (that is, Is_Frozen has been set by Freeze_Entity but it has not
       --  completed its work).
 
-      if Has_Task (Func_Typ) then
+      elsif Has_Task (Func_Typ) then
          return True;
 
       elsif Ekind (Func_Id) = E_Function then
@@ -9164,8 +9251,6 @@ package body Exp_Ch6 is
       Typ : constant Entity_Id := Underlying_Type (Etype (Func_Id));
 
    begin
-      pragma Assert (Is_Build_In_Place_Function (Func_Id));
-
       --  A formal giving the finalization master is needed for build-in-place
       --  functions whose result type needs finalization or is a tagged type.
       --  Tagged primitive build-in-place functions need such a formal because
@@ -9177,7 +9262,8 @@ package body Exp_Ch6 is
       --  such build-in-place functions, primitive or not.
 
       return not Restriction_Active (No_Finalization)
-        and then (Needs_Finalization (Typ) or else Is_Tagged_Type (Typ));
+        and then (Needs_Finalization (Typ) or else Is_Tagged_Type (Typ))
+        and then not Has_Foreign_Convention (Typ);
    end Needs_BIP_Finalization_Master;
 
    --------------------------
@@ -9188,8 +9274,6 @@ package body Exp_Ch6 is
       Typ : constant Entity_Id := Underlying_Type (Etype (Func_Id));
 
    begin
-      pragma Assert (Is_Build_In_Place_Function (Func_Id));
-
       --  A formal giving the allocation method is needed for build-in-place
       --  functions whose result type is returned on the secondary stack or
       --  is a tagged type. Tagged primitive build-in-place functions need
@@ -9201,7 +9285,8 @@ package body Exp_Ch6 is
       --  to be passed to all such build-in-place functions, primitive or not.
 
       return not Restriction_Active (No_Secondary_Stack)
-        and then (Needs_Secondary_Stack (Typ) or else Is_Tagged_Type (Typ));
+        and then (Needs_Secondary_Stack (Typ) or else Is_Tagged_Type (Typ))
+        and then not Has_Foreign_Convention (Typ);
    end Needs_BIP_Alloc_Form;
 
    -------------------------------------
@@ -9496,6 +9581,161 @@ package body Exp_Ch6 is
       return Unqual_BIP_Function_Call (Expr);
    end Unqual_BIP_Iface_Function_Call;
 
+   -------------------------------
+   -- Validate_Subprogram_Calls --
+   -------------------------------
+
+   procedure Validate_Subprogram_Calls (N : Node_Id) is
+
+      function Process_Node (Nod : Node_Id) return Traverse_Result;
+      --  Function to traverse the subtree of N using Traverse_Proc.
+
+      ------------------
+      -- Process_Node --
+      ------------------
+
+      function Process_Node (Nod : Node_Id) return Traverse_Result is
+      begin
+         case Nkind (Nod) is
+            when N_Entry_Call_Statement
+               | N_Procedure_Call_Statement
+               | N_Function_Call
+              =>
+               declare
+                  Call_Node : Node_Id renames Nod;
+                  Subp      : Entity_Id;
+
+               begin
+                  --  Call using access to subprogram with explicit dereference
+
+                  if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
+                     Subp := Etype (Name (Call_Node));
+
+                  --  Prefix notation calls
+
+                  elsif Nkind (Name (Call_Node)) = N_Selected_Component then
+                     Subp := Entity (Selector_Name (Name (Call_Node)));
+
+                  --  Call to member of entry family, where Name is an indexed
+                  --  component, with the prefix being a selected component
+                  --  giving the task and entry family name, and the index
+                  --  being the entry index.
+
+                  elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
+                     Subp :=
+                       Entity (Selector_Name (Prefix (Name (Call_Node))));
+
+                  --  Normal case
+
+                  else
+                     Subp := Entity (Name (Call_Node));
+                  end if;
+
+                  pragma Assert (Check_BIP_Actuals (Call_Node, Subp));
+               end;
+
+            --  Skip generic bodies
+
+            when N_Package_Body =>
+               if Ekind (Unique_Defining_Entity (Nod)) = E_Generic_Package then
+                  return Skip;
+               end if;
+
+            when N_Subprogram_Body =>
+               if Ekind (Unique_Defining_Entity (Nod)) in E_Generic_Function
+                                                        | E_Generic_Procedure
+               then
+                  return Skip;
+               end if;
+
+            --  Nodes we want to ignore
+
+            --  Skip calls placed in the full declaration of record types since
+            --  the call will be performed by their Init Proc; for example,
+            --  calls initializing default values of discriminants or calls
+            --  providing the initial value of record type components. Other
+            --  full type declarations are processed because they may have
+            --  calls that must be checked. For example:
+
+            --    type T is array (1 .. Some_Function_Call (...)) of Some_Type;
+
+            --  ??? More work needed here to handle the following case:
+
+            --    type Rec is record
+            --       F : String (1 .. <some complicated expression>);
+            --    end record;
+
+            when N_Full_Type_Declaration =>
+               if Is_Record_Type (Defining_Entity (Nod)) then
+                  return Skip;
+               end if;
+
+            --  Skip calls placed in subprogram specifications since function
+            --  calls initializing default parameter values will be processed
+            --  when the call to the subprogram is found (if the default actual
+            --  parameter is required), and calls found in aspects will be
+            --  processed when their corresponding pragma is found, or in the
+            --  specific case of class-wide pre-/postconditions, when their
+            --  helpers are found.
+
+            when N_Procedure_Specification
+               | N_Function_Specification
+              =>
+               return Skip;
+
+            when N_Abstract_Subprogram_Declaration
+               | N_At_Clause
+               | N_Call_Marker
+               | N_Empty
+               | N_Enumeration_Representation_Clause
+               | N_Enumeration_Type_Definition
+               | N_Function_Instantiation
+               | N_Freeze_Generic_Entity
+               | N_Generic_Function_Renaming_Declaration
+               | N_Generic_Package_Renaming_Declaration
+               | N_Generic_Procedure_Renaming_Declaration
+               | N_Generic_Package_Declaration
+               | N_Generic_Subprogram_Declaration
+               | N_Itype_Reference
+               | N_Number_Declaration
+               | N_Package_Instantiation
+               | N_Package_Renaming_Declaration
+               | N_Pragma
+               | N_Procedure_Instantiation
+               | N_Protected_Type_Declaration
+               | N_Record_Representation_Clause
+               | N_Validate_Unchecked_Conversion
+               | N_Variable_Reference_Marker
+               | N_Use_Package_Clause
+               | N_Use_Type_Clause
+               | N_With_Clause
+              =>
+               return Skip;
+
+            when others =>
+               null;
+         end case;
+
+         return OK;
+      end Process_Node;
+
+      procedure Check_Calls is new Traverse_Proc (Process_Node);
+
+   --  Start of processing for Validate_Subprogram_Calls
+
+   begin
+      --  No action required if we are not generating code or compiling sources
+      --  that have errors.
+
+      if Serious_Errors_Detected > 0
+        or else Operating_Mode /= Generate_Code
+      then
+         return;
+      end if;
+
+      Check_Calls (N);
+   end Validate_Subprogram_Calls;
+
    --------------
    -- Warn_BIP --
    --------------
diff --git a/gcc/ada/exp_ch6.ads b/gcc/ada/exp_ch6.ads
index 19d0bc3ff69..66888c51a07 100644
--- a/gcc/ada/exp_ch6.ads
+++ b/gcc/ada/exp_ch6.ads
@@ -121,6 +121,18 @@ 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.
 
+   function Has_BIP_Extra_Formal
+     (E              : Entity_Id;
+      Kind           : BIP_Formal_Kind;
+      Must_Be_Frozen : Boolean := True) return Boolean;
+   --  Given a subprogram, subprogram type, entry or entry family, return True
+   --  if E has the BIP extra formal associated with Kind. In general this
+   --  subprogram must be invoked with a frozen entity or a subprogram type of
+   --  a dispatching call since we can only rely on the availability of extra
+   --  formals on these entities; this requirement can be relaxed using the
+   --  formal Must_Be_Frozen in scenarios where we know that the entity has
+   --  the extra formals.
+
    procedure Install_Class_Preconditions_Check (Call_Node : Node_Id);
    --  Install check of class-wide preconditions on the caller.
 
@@ -137,7 +149,8 @@ package Exp_Ch6 is
    function Is_Build_In_Place_Function_Call (N : Node_Id) return Boolean;
    --  Ada 2005 (AI-318-02): Returns True if N denotes a call to a function
    --  that requires handling as a build-in-place call (possibly qualified or
-   --  converted).
+   --  converted); that is, BIP function calls, and calls to functions with
+   --  inherited BIP formals.
 
    function Is_Build_In_Place_Result_Type (Typ : Entity_Id) return Boolean;
    --  Ada 2005 (AI-318-02): Returns True if functions returning the type use
@@ -265,6 +278,11 @@ package Exp_Ch6 is
    --  to reference the secondary dispatch table of an interface; otherwise
    --  return Empty.
 
+   procedure Validate_Subprogram_Calls (N : Node_Id);
+   --  Check that the number of actuals (including extra actuals) of calls in
+   --  the subtree N match their corresponding formals; check also that the
+   --  names of BIP extra actuals and formals match.
+
 private
    pragma Inline (Is_Build_In_Place_Return_Object);
 
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 1fdc9d0d60e..032c73d3dfb 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -4984,6 +4984,7 @@ package body Freeze is
               and then Convention (Desig) /= Convention_Protected
             then
                Set_Is_Frozen (Desig);
+               Create_Extra_Formals (Desig);
             end if;
          end Check_Itype;
 
@@ -7131,11 +7132,11 @@ package body Freeze is
 
                Check_Debug_Info_Needed (E);
 
-               --  AI-117 requires that the convention of a partial view be the
-               --  same as the convention of the full view. Note that this is a
-               --  recognized breach of privacy, but it's essential for logical
-               --  consistency of representation, and the lack of a rule in
-               --  RM95 was an oversight.
+               --  AI95-117 requires that the convention of a partial view be
+               --  the same as the convention of the full view. Note that this
+               --  is a recognized breach of privacy, but it's essential for
+               --  logical consistency of representation, and the lack of a
+               --  rule in RM95 was an oversight.
 
                Set_Convention (E, Convention (Full_View (E)));
 
@@ -7360,7 +7361,7 @@ package body Freeze is
 
          if Is_Composite_Type (E) then
 
-            --  AI-117 requires that all new primitives of a tagged type must
+            --  AI95-117 requires that all new primitives of a tagged type must
             --  inherit the convention of the full view of the type. Inherited
             --  and overriding operations are defined to inherit the convention
             --  of their parent or overridden subprogram (also specified in
@@ -8268,7 +8269,7 @@ package body Freeze is
             if Present (Nam)
               and then Ekind (Nam) = E_Function
               and then Nkind (Parent (N)) = N_Function_Call
-              and then Convention (Nam) = Convention_Ada
+              and then not Has_Foreign_Convention (Nam)
             then
                Create_Extra_Formals (Nam);
             end if;
@@ -9875,77 +9876,11 @@ package body Freeze is
    -----------------------
 
    procedure Freeze_Subprogram (E : Entity_Id) is
-      function Check_Extra_Formals (E : Entity_Id) return Boolean;
-      --  Return True if the decoration of the attributes associated with extra
-      --  formals are properly set.
 
       procedure Set_Profile_Convention (Subp_Id : Entity_Id);
       --  Set the conventions of all anonymous access-to-subprogram formals and
       --  result subtype of subprogram Subp_Id to the convention of Subp_Id.
 
-      -------------------------
-      -- Check_Extra_Formals --
-      -------------------------
-
-      function Check_Extra_Formals (E : Entity_Id) return Boolean is
-         Last_Formal       : Entity_Id := Empty;
-         Formal            : Entity_Id;
-         Has_Extra_Formals : Boolean := False;
-
-      begin
-         --  No check required if expansion is disabled because extra
-         --  formals are only generated when we are generating code.
-         --  See Create_Extra_Formals.
-
-         if not Expander_Active then
-            return True;
-         end if;
-
-         --  Check attribute Extra_Formal: If available, it must be set only
-         --  on the last formal of E.
-
-         Formal := First_Formal (E);
-         while Present (Formal) loop
-            if Present (Extra_Formal (Formal)) then
-               if Has_Extra_Formals then
-                  return False;
-               end if;
-
-               Has_Extra_Formals := True;
-            end if;
-
-            Last_Formal := Formal;
-            Next_Formal (Formal);
-         end loop;
-
-         --  Check attribute Extra_Accessibility_Of_Result
-
-         if Ekind (E) in E_Function | E_Subprogram_Type
-           and then Needs_Result_Accessibility_Level (E)
-           and then No (Extra_Accessibility_Of_Result (E))
-         then
-            return False;
-         end if;
-
-         --  Check attribute Extra_Formals: If E has extra formals, then this
-         --  attribute must point to the first extra formal of E.
-
-         if Has_Extra_Formals then
-            return Present (Extra_Formals (E))
-              and then Present (Extra_Formal (Last_Formal))
-              and then Extra_Formal (Last_Formal) = Extra_Formals (E);
-
-         --  When E has no formals, the first extra formal is available through
-         --  the Extra_Formals attribute.
-
-         elsif Present (Extra_Formals (E)) then
-            return No (First_Formal (E));
-
-         else
-            return True;
-         end if;
-      end Check_Extra_Formals;
-
       ----------------------------
       -- Set_Profile_Convention --
       ----------------------------
@@ -10084,30 +10019,26 @@ package body Freeze is
       --  that we know the convention.
 
       if not Has_Foreign_Convention (E) then
-         if No (Extra_Formals (E)) then
 
-            --  Extra formals are shared by derived subprograms; therefore, if
-            --  the ultimate alias of E has been frozen before E then the extra
-            --  formals have been added, but the attribute Extra_Formals is
-            --  still unset (and must be set now).
+         --  Extra formals of dispatching operations are added later by
+         --  Expand_Freeze_Record_Type, which also adds extra formals to
+         --  internal entities built to handle interface types.
 
-            if Present (Alias (E))
-              and then Is_Frozen (Ultimate_Alias (E))
-              and then Present (Extra_Formals (Ultimate_Alias (E)))
-              and then Last_Formal (Ultimate_Alias (E)) = Last_Formal (E)
-            then
-               Set_Extra_Formals (E, Extra_Formals (Ultimate_Alias (E)));
+         if not Is_Dispatching_Operation (E) then
+            Create_Extra_Formals (E);
 
-               if Ekind (E) = E_Function then
-                  Set_Extra_Accessibility_Of_Result (E,
-                    Extra_Accessibility_Of_Result (Ultimate_Alias (E)));
-               end if;
-            else
-               Create_Extra_Formals (E);
-            end if;
+            pragma Assert
+              ((Ekind (E) = E_Subprogram_Type
+                  and then Extra_Formals_OK (E))
+               or else
+                 (Is_Subprogram (E)
+                   and then Extra_Formals_OK (E)
+                   and then
+                     (No (Overridden_Operation (E))
+                       or else Extra_Formals_Match_OK (E,
+                                 Ultimate_Alias (Overridden_Operation (E))))));
          end if;
 
-         pragma Assert (Check_Extra_Formals (E));
          Set_Mechanisms (E);
 
          --  If this is convention Ada and a Valued_Procedure, that's odd
diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb
index 12c91b11d9a..cdca67bf397 100644
--- a/gcc/ada/frontend.adb
+++ b/gcc/ada/frontend.adb
@@ -30,6 +30,7 @@ with Checks;
 with CStand;
 with Debug;          use Debug;
 with Elists;
+with Exp_Ch6;
 with Exp_Dbug;
 with Exp_Unst;
 with Fmap;
@@ -523,6 +524,16 @@ begin
       VAST.Check_Tree (Cunit (Main_Unit));
    end if;
 
+   --  Validate all the subprogram calls; this work will be done by VAST; in
+   --  the meantime it is done to check extra formals and it can be disabled
+   --  using -gnatd_X (which also disables all the other assertions on extra
+   --  formals). It is invoked using pragma Debug to avoid adding any cost
+   --  when the compiler is built with assertions disabled.
+
+   if not Debug_Flag_Underscore_XX then
+      pragma Debug (Exp_Ch6.Validate_Subprogram_Calls (Cunit (Main_Unit)));
+   end if;
+
    --  Dump the source now. Note that we do this as soon as the analysis
    --  of the tree is complete, because it is not just a dump in the case
    --  of -gnatD, where it rewrites all source locations in the tree.
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 95ffbe00ba4..dbe4d72626e 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1318,7 +1318,8 @@ package body Sem_Ch3 is
 
       Check_Restriction (No_Access_Subprograms, T_Def);
 
-      Create_Extra_Formals (Desig_Type);
+      --  Addition of extra formals must be delayed till the freeze point so
+      --  that we know the convention.
    end Access_Subprogram_Declaration;
 
    ----------------------------
@@ -11788,11 +11789,9 @@ package body Sem_Ch3 is
          Insert_Before (Typ_Decl, Decl);
          Analyze (Decl);
 
-         --  If an access to subprogram, create the extra formals
-
-         if Present (Acc_Def) then
-            Create_Extra_Formals (Designated_Type (Anon_Access));
-         end if;
+         --  At first sight we could add here the extra formals of an access to
+         --  subprogram; however, it must delayed till the freeze point so that
+         --  we know the convention.
 
          if Nkind (Comp_Def) = N_Component_Definition then
             Rewrite (Comp_Def,
@@ -16053,12 +16052,12 @@ package body Sem_Ch3 is
          Next_Formal (Formal);
       end loop;
 
-      --  Extra formals are shared between the parent subprogram and the
-      --  derived subprogram (implicit in the above copy of formals), unless
-      --  the parent type is a limited interface type; hence we must inherit
-      --  also the reference to the first extra formal. When the parent type is
-      --  an interface the extra formals will be added when the subprogram is
-      --  frozen (see Freeze.Freeze_Subprogram).
+      --  Extra formals are shared between the parent subprogram and this
+      --  internal entity built by Derive_Subprogram (implicit in the above
+      --  copy of formals), unless the parent type is a limited interface type;
+      --  hence we must inherit also the reference to the first extra formal.
+      --  When the parent type is an interface, the extra formals will be added
+      --  when the tagged type is frozen (see Expand_Freeze_Record_Type).
 
       if not Is_Limited_Interface (Parent_Type) then
          Set_Extra_Formals (New_Subp, Extra_Formals (Parent_Subp));
@@ -16099,7 +16098,7 @@ package body Sem_Ch3 is
       Copy_Strub_Mode (New_Subp, Alias (New_Subp));
 
       --  Derived subprograms of a tagged type must inherit the convention
-      --  of the parent subprogram (a requirement of AI-117). Derived
+      --  of the parent subprogram (a requirement of AI95-117). Derived
       --  subprograms of untagged types simply get convention Ada by default.
 
       --  If the derived type is a tagged generic formal type with unknown
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index d28de10d3d6..454db66dd2c 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -34,6 +34,7 @@ with Einfo.Utils;    use Einfo.Utils;
 with Elists;         use Elists;
 with Errout;         use Errout;
 with Expander;       use Expander;
+with Exp_Ch3;        use Exp_Ch3;
 with Exp_Ch6;        use Exp_Ch6;
 with Exp_Ch9;        use Exp_Ch9;
 with Exp_Dbug;       use Exp_Dbug;
@@ -200,6 +201,13 @@ package body Sem_Ch6 is
    --  This procedure makes S, a new overloaded entity, into the first visible
    --  entity with that name.
 
+   function Has_Reliable_Extra_Formals (E : Entity_Id) return Boolean;
+   --  E is the entity for a subprogram spec. Returns False for abstract
+   --  predefined dispatching primitives of Root_Controlled since they
+   --  cannot have extra formals (this is required to build the runtime);
+   --  it also returns False for predefined stream dispatching operations
+   --  not emitted by the frontend. Otherwise returns True.
+
    function Is_Non_Overriding_Operation
      (Prev_E : Entity_Id;
       New_E  : Entity_Id) return Boolean;
@@ -3352,7 +3360,8 @@ package body Sem_Ch6 is
                       or else
                         (Is_Class_Wide_Type (Designated_Type (Etype (Scop)))
                            and then
-                         Is_Limited_Record (Designated_Type (Etype (Scop)))))
+                         Is_Limited_Record
+                           (Etype (Designated_Type (Etype (Scop))))))
            and then Expander_Active
          then
             Decl := Build_Master_Declaration (Loc);
@@ -8471,6 +8480,253 @@ package body Sem_Ch6 is
         (New_Id, Old_Id, Type_Conformant, True, Result, Err_Loc);
    end Check_Type_Conformant;
 
+   -----------------------------
+   -- Check_Untagged_Equality --
+   -----------------------------
+
+   procedure Check_Untagged_Equality (Eq_Op : Entity_Id) is
+      Eq_Decl : constant Node_Id   := Unit_Declaration_Node (Eq_Op);
+      Typ     : constant Entity_Id := Etype (First_Formal (Eq_Op));
+
+      procedure Freezing_Point_Warning (N : Node_Id; S : String);
+      --  Output a warning about the freezing point N of Typ
+
+      function Is_Actual_Of_Instantiation
+        (E    : Entity_Id;
+         Inst : Node_Id) return Boolean;
+      --  Return True if E is an actual parameter of instantiation Inst
+
+      -----------------------------------
+      -- Output_Freezing_Point_Warning --
+      -----------------------------------
+
+      procedure Freezing_Point_Warning (N : Node_Id; S : String) is
+      begin
+         Error_Msg_String (1 .. S'Length) := S;
+         Error_Msg_Strlen := S'Length;
+
+         if Ada_Version >= Ada_2012 then
+            Error_Msg_NE ("type& is frozen by ~??", N, Typ);
+            Error_Msg_N
+              ("\an equality operator cannot be declared after this point??",
+               N);
+
+         else
+            Error_Msg_NE ("type& is frozen by ~ (Ada 2012)?y?", N, Typ);
+            Error_Msg_N
+              ("\an equality operator cannot be declared after this point"
+               & " (Ada 2012)?y?", N);
+         end if;
+      end Freezing_Point_Warning;
+
+      --------------------------------
+      -- Is_Actual_Of_Instantiation --
+      --------------------------------
+
+      function Is_Actual_Of_Instantiation
+        (E    : Entity_Id;
+         Inst : Node_Id) return Boolean
+      is
+         Assoc : Node_Id;
+
+      begin
+         if Present (Generic_Associations (Inst)) then
+            Assoc := First (Generic_Associations (Inst));
+
+            while Present (Assoc) loop
+               if Present (Explicit_Generic_Actual_Parameter (Assoc))
+                 and then
+                   Is_Entity_Name (Explicit_Generic_Actual_Parameter (Assoc))
+                 and then
+                   Entity (Explicit_Generic_Actual_Parameter (Assoc)) = E
+               then
+                  return True;
+               end if;
+
+               Next (Assoc);
+            end loop;
+         end if;
+
+         return False;
+      end Is_Actual_Of_Instantiation;
+
+      --  Local variable
+
+      Decl : Node_Id;
+
+   --  Start of processing for Check_Untagged_Equality
+
+   begin
+      --  This check applies only if we have a subprogram declaration or a
+      --  subprogram body that is not a completion, for an untagged record
+      --  type, and that is conformant with the predefined operator.
+
+      if (Nkind (Eq_Decl) /= N_Subprogram_Declaration
+           and then not (Nkind (Eq_Decl) = N_Subprogram_Body
+                          and then Acts_As_Spec (Eq_Decl)))
+        or else not Is_Record_Type (Typ)
+        or else Is_Tagged_Type (Typ)
+        or else not Is_User_Defined_Equality (Eq_Op)
+      then
+         return;
+      end if;
+
+      --  In Ada 2012 case, we will output errors or warnings depending on
+      --  the setting of debug flag -gnatd.E.
+
+      if Ada_Version >= Ada_2012 then
+         Error_Msg_Warn := Debug_Flag_Dot_EE;
+
+      --  In earlier versions of Ada, nothing to do unless we are warning on
+      --  Ada 2012 incompatibilities (Warn_On_Ada_2012_Incompatibility set).
+
+      else
+         if not Warn_On_Ada_2012_Compatibility then
+            return;
+         end if;
+      end if;
+
+      --  Cases where the type has already been frozen
+
+      if Is_Frozen (Typ) then
+
+         --  The check applies to a primitive operation, so check that type
+         --  and equality operation are in the same scope.
+
+         if Scope (Typ) /= Current_Scope then
+            return;
+
+         --  If the type is a generic actual (sub)type, the operation is not
+         --  primitive either because the base type is declared elsewhere.
+
+         elsif Is_Generic_Actual_Type (Typ) then
+            return;
+
+         --  Here we may have an error of declaration after freezing, but we
+         --  must make sure not to flag the equality operator itself causing
+         --  the freezing when it is a subprogram body.
+
+         else
+            Decl := Next (Declaration_Node (Typ));
+
+            while Present (Decl) and then Decl /= Eq_Decl loop
+
+               --  The declaration of an object of the type
+
+               if Nkind (Decl) = N_Object_Declaration
+                 and then Etype (Defining_Identifier (Decl)) = Typ
+               then
+                  Freezing_Point_Warning (Decl, "declaration");
+                  exit;
+
+               --  The instantiation of a generic on the type
+
+               elsif Nkind (Decl) in N_Generic_Instantiation
+                 and then Is_Actual_Of_Instantiation (Typ, Decl)
+               then
+                  Freezing_Point_Warning (Decl, "instantiation");
+                  exit;
+
+               --  A noninstance proper body, body stub or entry body
+
+               elsif Nkind (Decl) in N_Proper_Body
+                                   | N_Body_Stub
+                                   | N_Entry_Body
+                 and then not Is_Generic_Instance (Defining_Entity (Decl))
+               then
+                  Freezing_Point_Warning (Decl, "body");
+                  exit;
+
+               --  If we have reached the freeze node and immediately after we
+               --  have the body or generated code for the body, then it is the
+               --  body that caused the freezing and this is legal.
+
+               elsif Nkind (Decl) = N_Freeze_Entity
+                 and then Entity (Decl) = Typ
+                 and then (Next (Decl) = Eq_Decl
+                            or else
+                           Sloc (Next (Decl)) = Sloc (Eq_Decl))
+               then
+                  return;
+               end if;
+
+               Next (Decl);
+            end loop;
+
+            --  Here we have a definite error of declaration after freezing
+
+            if Ada_Version >= Ada_2012 then
+               Error_Msg_NE
+                 ("equality operator must be declared before type & is "
+                  & "frozen (RM 4.5.2 (9.8)) (Ada 2012)<<", Eq_Op, Typ);
+
+               --  In Ada 2012 mode with error turned to warning, output one
+               --  more warning to warn that the equality operation may not
+               --  compose. This is the consequence of ignoring the error.
+
+               if Error_Msg_Warn then
+                  Error_Msg_N ("\equality operation may not compose??", Eq_Op);
+               end if;
+
+            else
+               Error_Msg_NE
+                 ("equality operator must be declared before type& is "
+                  & "frozen (RM 4.5.2 (9.8)) (Ada 2012)?y?", Eq_Op, Typ);
+            end if;
+
+            --  If we have found no freezing point and the declaration of the
+            --  operator could not be reached from that of the type and we are
+            --  in a package body, this must be because the type is declared
+            --  in the spec of the package. Add a message tailored to this.
+
+            if No (Decl) and then In_Package_Body (Scope (Typ)) then
+               if Ada_Version >= Ada_2012 then
+                  if Nkind (Eq_Decl) = N_Subprogram_Body then
+                     Error_Msg_N
+                       ("\put declaration in package spec<<", Eq_Op);
+                  else
+                     Error_Msg_N
+                       ("\move declaration to package spec<<", Eq_Op);
+                  end if;
+
+               else
+                  if Nkind (Eq_Decl) = N_Subprogram_Body then
+                     Error_Msg_N
+                       ("\put declaration in package spec (Ada 2012)?y?",
+                        Eq_Op);
+                  else
+                     Error_Msg_N
+                       ("\move declaration to package spec (Ada 2012)?y?",
+                        Eq_Op);
+                  end if;
+               end if;
+            end if;
+         end if;
+
+      --  Now check for AI12-0352: the declaration of a user-defined primitive
+      --  equality operation for a record type T is illegal if it occurs after
+      --  a type has been derived from T.
+
+      else
+         Decl := Next (Declaration_Node (Typ));
+
+         while Present (Decl) and then Decl /= Eq_Decl loop
+            if Nkind (Decl) = N_Full_Type_Declaration
+              and then Etype (Defining_Identifier (Decl)) = Typ
+            then
+               Error_Msg_N
+                 ("equality operator cannot appear after derivation", Eq_Op);
+               Error_Msg_NE
+                 ("an equality operator for& cannot be declared after "
+                  & "this point??",
+                  Decl, Typ);
+            end if;
+
+            Next (Decl);
+         end loop;
+      end if;
+   end Check_Untagged_Equality;
+
    ---------------------------
    -- Can_Override_Operator --
    ---------------------------
@@ -8950,6 +9206,26 @@ package body Sem_Ch6 is
       --  BIP_xxx denotes an extra formal for a build-in-place function. See
       --  the full list in exp_ch6.BIP_Formal_Kind.
 
+      function Has_Extra_Formals (E : Entity_Id) return Boolean;
+      --  Determines if E has its extra formals
+
+      function Needs_Accessibility_Check_Extra
+        (E      : Entity_Id;
+         Formal : Node_Id) return Boolean;
+      --  Determines whether the given formal of E needs an extra formal for
+      --  supporting accessibility checking. Returns True for both anonymous
+      --  access formals and formals of named access types that are marked as
+      --  controlling formals. The latter case can occur when the subprogram
+      --  Expand_Dispatching_Call creates a subprogram-type and substitutes
+      --  the types of access-to-class-wide actuals for the anonymous access-
+      --  to-specific-type of controlling formals.
+
+      function Parent_Subprogram (Subp_Id : Entity_Id) return Entity_Id;
+      --  Subp_Id is a subprogram of a derived type; return its parent
+      --  subprogram if Subp_Id overrides a parent primitive or derives
+      --  from a parent primitive, and such parent primitive can have extra
+      --  formals. Otherwise return Empty.
+
       ----------------------
       -- Add_Extra_Formal --
       ----------------------
@@ -8960,10 +9236,7 @@ package body Sem_Ch6 is
          Scope        : Entity_Id;
          Suffix       : String) return Entity_Id
       is
-         EF : constant Entity_Id :=
-                Make_Defining_Identifier (Sloc (Assoc_Entity),
-                  Chars  => New_External_Name (Chars (Assoc_Entity),
-                                               Suffix => Suffix));
+         EF : Entity_Id;
 
       begin
          --  A little optimization. Never generate an extra formal for the
@@ -8974,6 +9247,10 @@ package body Sem_Ch6 is
             return Empty;
          end if;
 
+         EF := Make_Defining_Identifier (Sloc (Assoc_Entity),
+                 Chars => New_External_Name (Chars (Assoc_Entity),
+                                             Suffix => Suffix));
+
          Mutate_Ekind        (EF, E_In_Parameter);
          Set_Actual_Subtype  (EF, Typ);
          Set_Etype           (EF, Typ);
@@ -8995,49 +9272,266 @@ package body Sem_Ch6 is
          return EF;
       end Add_Extra_Formal;
 
-      --  Local variables
+      -----------------------
+      -- Has_Extra_Formals --
+      -----------------------
 
-      Formal_Type : Entity_Id;
-      P_Formal    : Entity_Id;
+      function Has_Extra_Formals (E : Entity_Id) return Boolean is
+      begin
+         return Present (Extra_Formals (E))
+           or else
+             (Ekind (E) = E_Function
+                and then Present (Extra_Accessibility_Of_Result (E)));
+      end Has_Extra_Formals;
+
+      -------------------------------------
+      -- Needs_Accessibility_Check_Extra --
+      -------------------------------------
+
+      function Needs_Accessibility_Check_Extra
+        (E      : Entity_Id;
+         Formal : Node_Id) return Boolean is
+
+      begin
+         --  For dispatching operations this extra formal is not suppressed
+         --  since all the derivations must have matching formals.
+
+         --  For nondispatching operations it is suppressed if we specifically
+         --  suppress accessibility checks at the package level for either the
+         --  subprogram, or the package in which it resides. However, we do
+         --  not suppress it simply if the scope has accessibility checks
+         --  suppressed, since this could cause trouble when clients are
+         --  compiled with a different suppression setting. The explicit checks
+         --  at the package level are safe from this point of view.
+
+         if not Is_Dispatching_Operation (E)
+           and then
+             (Explicit_Suppress (E, Accessibility_Check)
+                or else Explicit_Suppress (Scope (E), Accessibility_Check))
+         then
+            return False;
+         end if;
+
+         --  Base_Type is applied to handle cases where there is a null
+         --  exclusion the formal may have an access subtype.
+
+         return
+           Ekind (Base_Type (Etype (Formal))) = E_Anonymous_Access_Type
+             or else
+               (Is_Controlling_Formal (Formal)
+                  and then Is_Access_Type (Base_Type (Etype (Formal))));
+      end Needs_Accessibility_Check_Extra;
+
+      -----------------------
+      -- Parent_Subprogram --
+      -----------------------
+
+      function Parent_Subprogram (Subp_Id : Entity_Id) return Entity_Id is
+         pragma Assert (not Is_Thunk (Subp_Id));
+         Ovr_E     : Entity_Id := Overridden_Operation (Subp_Id);
+         Ovr_Alias : Entity_Id;
+
+      begin
+         if Present (Ovr_E) then
+            Ovr_Alias := Ultimate_Alias (Ovr_E);
+
+            --  There is no real overridden subprogram if there is a mutual
+            --  reference between the E and its overridden operation. This
+            --  weird scenery occurs in the following cases:
+
+            --  1) Controlling function wrappers internally built by
+            --     Make_Controlling_Function_Wrappers.
+
+            --  2) Hidden overridden primitives of type extensions or private
+            --     extensions (cf. Find_Hidden_Overridden_Primitive). These
+            --     hidden primitives have suffix 'P'.
+
+            --  3) Overriding primitives of stub types (see the subprogram
+            --     Add_RACW_Primitive_Declarations_And_Bodies).
+
+            if Ovr_Alias = Subp_Id then
+               pragma Assert
+                 ((Is_Wrapper (Subp_Id)
+                     and then Has_Controlling_Result (Subp_Id))
+                   or else Has_Suffix (Ovr_E, 'P')
+                   or else Is_RACW_Stub_Type
+                             (Find_Dispatching_Type (Subp_Id)));
+
+               if Present (Overridden_Operation (Ovr_E)) then
+                  Ovr_E := Overridden_Operation (Ovr_E);
+
+               --  Ovr_E is an internal entity built by Derive_Subprogram and
+               --  we have no direct way to climb to the corresponding parent
+               --  subprogram but this internal entity has the extra formals
+               --  (if any) required for the purpose of checking the extra
+               --  formals of Subp_Id.
+
+               else
+                  pragma Assert (not Comes_From_Source (Ovr_E));
+               end if;
+
+            --  Use as our reference entity the ultimate renaming of the
+            --  overridden subprogram.
+
+            elsif Present (Alias (Ovr_E)) then
+               pragma Assert (No (Overridden_Operation (Ovr_Alias))
+                 or else Overridden_Operation (Ovr_Alias) /= Ovr_E);
+
+               Ovr_E := Ovr_Alias;
+            end if;
+         end if;
+
+         if Present (Ovr_E) and then Has_Reliable_Extra_Formals (Ovr_E) then
+            return Ovr_E;
+         else
+            return Empty;
+         end if;
+      end Parent_Subprogram;
+
+      --  Local variables
+
+      Formal_Type      : Entity_Id;
+      May_Have_Alias   : Boolean;
+      Alias_Formal     : Entity_Id := Empty;
+      Alias_Subp       : Entity_Id := Empty;
+      Parent_Formal    : Entity_Id := Empty;
+      Parent_Subp      : Entity_Id := Empty;
+      Ref_E            : Entity_Id;
 
    --  Start of processing for Create_Extra_Formals
 
    begin
+      pragma Assert (Is_Subprogram_Or_Entry (E)
+        or else Ekind (E) in E_Subprogram_Type);
+
       --  We never generate extra formals if expansion is not active because we
       --  don't need them unless we are generating code.
 
       if not Expander_Active then
          return;
-      end if;
+
+      --  Enumeration literals have no extra formal; this case occurs when
+      --  a function renames it.
+
+      elsif Ekind (E) = E_Function
+        and then Ekind (Ultimate_Alias (E)) = E_Enumeration_Literal
+      then
+         return;
+
+      --  Initialization procedures don't have extra formals
+
+      elsif Is_Init_Proc (E) then
+         return;
 
       --  No need to generate extra formals in thunks whose target has no extra
       --  formals, but we can have two of them chained (interface and stack).
 
-      if Is_Thunk (E) and then No (Extra_Formals (Thunk_Target (E))) then
+      elsif Is_Thunk (E) and then No (Extra_Formals (Thunk_Target (E))) then
          return;
-      end if;
 
-      --  If this is a derived subprogram then the subtypes of the parent
-      --  subprogram's formal parameters will be used to determine the need
-      --  for extra formals.
+      --  If Extra_Formals were already created, don't do it again. This
+      --  situation may arise for subprogram types created as part of
+      --  dispatching calls (see Expand_Dispatching_Call).
 
-      if Is_Overloadable (E) and then Present (Alias (E)) then
-         P_Formal := First_Formal (Alias (E));
-      else
-         P_Formal := Empty;
+      elsif Has_Extra_Formals (E) then
+         return;
+
+      --  Extra formals of renamings of generic actual subprograms and
+      --  renamings of instances of generic subprograms are shared. The
+      --  check performed on the last formal is required to ensure that
+      --  this is the renaming built by Analyze_Instance_And_Renamings
+      --  (which shares all the formals); otherwise this would be wrong.
+
+      elsif Ekind (E) in E_Function | E_Procedure
+        and then Is_Generic_Instance (E)
+        and then Present (Alias (E))
+        and then Last_Formal (Ultimate_Alias (E)) = Last_Formal (E)
+      then
+         pragma Assert (Is_Generic_Instance (E)
+           = Is_Generic_Instance (Ultimate_Alias (E)));
+
+         Create_Extra_Formals (Ultimate_Alias (E));
+
+         --  Share the extra formals
+
+         Set_Extra_Formals (E, Extra_Formals (Ultimate_Alias (E)));
+
+         if Ekind (E) = E_Function then
+            Set_Extra_Accessibility_Of_Result (E,
+              Extra_Accessibility_Of_Result (Ultimate_Alias (E)));
+         end if;
+
+         pragma Assert (Extra_Formals_OK (E));
+         return;
       end if;
 
+      --  Locate the last formal; required by Add_Extra_Formal.
+
       Formal := First_Formal (E);
       while Present (Formal) loop
          Last_Extra := Formal;
          Next_Formal (Formal);
       end loop;
 
-      --  If Extra_Formals were already created, don't do it again. This
-      --  situation may arise for subprogram types created as part of
-      --  dispatching calls (see Expand_Dispatching_Call).
+      --  We rely on three entities to ensure consistency of extra formals of
+      --  entity E:
+      --
+      --    1. A reference entity (Ref_E). For thunks it is their target
+      --       primitive since this ensures that they have exactly the
+      --       same extra formals; otherwise it is the identity.
+      --
+      --    2. The parent subprogram; only for derived types and references
+      --       either the overridden subprogram or the internal entity built
+      --       by Derive_Subprogram that has the extra formals of the parent
+      --       subprogram; otherwise it is Empty. This entity ensures matching
+      --       extra formals in derived types.
+      --
+      --    3. For renamings, their ultimate alias; this ensures taking the
+      --       same decision in all the renamings (independently of the Ada
+      --       mode on which they are compiled). For example:
+      --
+      --          pragma Ada_2012;
+      --          function Id_A (I : access Integer) return access Integer;
+      --
+      --          pragma Ada_2005;
+      --          function Id_B (I : access Integer) return access Integer
+      --             renames Id_A;
 
-      if Present (Last_Extra) and then Present (Extra_Formal (Last_Extra)) then
+      if Is_Thunk (E) then
+         Ref_E := Thunk_Target (E);
+      else
+         Ref_E := E;
+      end if;
+
+      if Is_Subprogram (Ref_E) then
+         Parent_Subp := Parent_Subprogram (Ref_E);
+      end if;
+
+      May_Have_Alias :=
+        (Is_Subprogram (Ref_E) or else Ekind (Ref_E) = E_Subprogram_Type);
+
+      --  If the parent subprogram is available then its ultimate alias of
+      --  Ref_E is not needed since it will not be used to check its extra
+      --  formals.
+
+      if No (Parent_Subp)
+        and then May_Have_Alias
+        and then Present (Alias (Ref_E))
+        and then Has_Reliable_Extra_Formals (Ultimate_Alias (Ref_E))
+      then
+         Alias_Subp := Ultimate_Alias (Ref_E);
+      end if;
+
+      --  Cannot add extra formals to subprograms and access types that have
+      --  foreign convention nor to subprograms overriding primitives that
+      --  have foreign convention since the foreign language does not know
+      --  how to handle these extra formals; same for renamings of entities
+      --  with foreign convention.
+
+      if Has_Foreign_Convention (Ref_E)
+        or else (Present (Alias_Subp)
+                   and then Has_Foreign_Convention (Alias_Subp))
+      then
          return;
       end if;
 
@@ -9052,20 +9546,74 @@ package body Sem_Ch6 is
          goto Test_For_Func_Result_Extras;
       end if;
 
+      --  Process the formals relying on the formals of our reference entities:
+      --  Parent_Formal, Alias_Formal and Formal. Notice that we don't use the
+      --  formal of Ref_E; we must use the formal of E which is the entity to
+      --  which we are adding the extra formals.
+
+      --  If this is a derived subprogram then the subtypes of the parent
+      --  subprogram's formal parameters will be used to determine the need
+      --  for extra formals.
+
+      if Present (Parent_Subp) then
+         Parent_Formal := First_Formal (Parent_Subp);
+
+         --  For concurrent types, the controlling argument of a dispatching
+         --  primitive implementing an interface primitive is implicit. For
+         --  example:
+         --
+         --     type Iface is protected interface;
+         --     function Prim
+         --       (Obj   : Iface;
+         --        Value : Integer) return Natural is abstract;
+         --
+         --     protected type PO is new Iface with
+         --        function Prim (Value : Integer) return Natural;
+         --     end PO;
+
+         if Convention (Ref_E) = Convention_Protected
+           and then Is_Abstract_Subprogram (Parent_Subp)
+           and then Is_Interface (Find_Dispatching_Type (Parent_Subp))
+         then
+            Parent_Formal := Next_Formal (Parent_Formal);
+
+            --  This is the nondispatching subprogram of a concurrent type
+            --  that overrides the interface primitive; the expander will
+            --  create the dispatching primitive (without Convention_Protected)
+            --  with all the matching formals (see exp_ch9.Build_Wrapper_Specs)
+
+            pragma Assert (not Is_Dispatching_Operation (Ref_E));
+         end if;
+
+      --  Ensure that the ultimate alias has all its extra formals
+
+      elsif Present (Alias_Subp) then
+         Create_Extra_Formals (Alias_Subp);
+         Alias_Formal := First_Formal (Alias_Subp);
+      end if;
+
       Formal := First_Formal (E);
       while Present (Formal) loop
 
+         --  Here we establish our priority for deciding on the extra
+         --  formals: 1) Parent primitive 2) Aliased primitive 3) Identity
+
+         if Present (Parent_Formal) then
+            Formal_Type := Etype (Parent_Formal);
+
+         elsif Present (Alias_Formal) then
+            Formal_Type := Etype (Alias_Formal);
+
+         else
+            Formal_Type := Etype (Formal);
+         end if;
+
          --  Create extra formal for supporting the attribute 'Constrained.
          --  The case of a private type view without discriminants also
          --  requires the extra formal if the underlying type has defaulted
          --  discriminants.
 
          if Ekind (Formal) /= E_In_Parameter then
-            if Present (P_Formal) then
-               Formal_Type := Etype (P_Formal);
-            else
-               Formal_Type := Etype (Formal);
-            end if;
 
             --  Do not produce extra formals for Unchecked_Union parameters.
             --  Jump directly to the end of the loop.
@@ -9110,36 +9658,22 @@ package body Sem_Ch6 is
             end if;
          end if;
 
-         --  Create extra formal for supporting accessibility checking. This
-         --  is done for both anonymous access formals and formals of named
-         --  access types that are marked as controlling formals. The latter
-         --  case can occur when Expand_Dispatching_Call creates a subprogram
-         --  type and substitutes the types of access-to-class-wide actuals
-         --  for the anonymous access-to-specific-type of controlling formals.
-         --  Base_Type is applied because in cases where there is a null
-         --  exclusion the formal may have an access subtype.
+         --  Extra formal for supporting accessibility checking
+
+         if Needs_Accessibility_Check_Extra (Ref_E, Formal) then
+            pragma Assert (No (Parent_Formal)
+              or else Present (Extra_Accessibility (Parent_Formal)));
+            pragma Assert (No (Alias_Formal)
+              or else Present (Extra_Accessibility (Alias_Formal)));
 
-         --  This is suppressed if we specifically suppress accessibility
-         --  checks at the package level for either the subprogram, or the
-         --  package in which it resides. However, we do not suppress it
-         --  simply if the scope has accessibility checks suppressed, since
-         --  this could cause trouble when clients are compiled with a
-         --  different suppression setting. The explicit checks at the
-         --  package level are safe from this point of view.
-
-         if (Ekind (Base_Type (Etype (Formal))) = E_Anonymous_Access_Type
-              or else (Is_Controlling_Formal (Formal)
-                        and then Is_Access_Type (Base_Type (Etype (Formal)))))
-           and then not
-             (Explicit_Suppress (E, Accessibility_Check)
-               or else
-              Explicit_Suppress (Scope (E), Accessibility_Check))
-           and then
-             (No (P_Formal)
-               or else Present (Extra_Accessibility (P_Formal)))
-         then
             Set_Extra_Accessibility
               (Formal, Add_Extra_Formal (Formal, Standard_Natural, E, "L"));
+
+         else
+            pragma Assert (No (Parent_Formal)
+              or else No (Extra_Accessibility (Parent_Formal)));
+            pragma Assert (No (Alias_Formal)
+              or else No (Extra_Accessibility (Alias_Formal)));
          end if;
 
          --  This label is required when skipping extra formal generation for
@@ -9147,8 +9681,12 @@ package body Sem_Ch6 is
 
          <<Skip_Extra_Formal_Generation>>
 
-         if Present (P_Formal) then
-            Next_Formal (P_Formal);
+         if Present (Parent_Formal) then
+            Next_Formal (Parent_Formal);
+         end if;
+
+         if Present (Alias_Formal) then
+            Next_Formal (Alias_Formal);
          end if;
 
          Next_Formal (Formal);
@@ -9156,20 +9694,47 @@ package body Sem_Ch6 is
 
       <<Test_For_Func_Result_Extras>>
 
-      --  Ada 2012 (AI05-234): "the accessibility level of the result of a
-      --  function call is ... determined by the point of call ...".
+      --  Assume the worst case (Ada 2022) to evaluate this extra formal;
+      --  required to ensure matching of extra formals between subprograms
+      --  and access-to-subprogram types in projects with mixed Ada dialects.
 
-      if Needs_Result_Accessibility_Level (E) then
-         Set_Extra_Accessibility_Of_Result
-           (E, Add_Extra_Formal (E, Standard_Natural, E, "L"));
-      end if;
+      declare
+         Save_Ada_Version : constant Ada_Version_Type := Ada_Version;
+
+      begin
+         Ada_Version := Ada_2022;
+
+         if Needs_Result_Accessibility_Level (Ref_E) then
+            pragma Assert (No (Parent_Subp)
+              or else Needs_Result_Accessibility_Level (Parent_Subp));
+            pragma Assert (No (Alias_Subp)
+              or else Needs_Result_Accessibility_Level (Alias_Subp));
+
+            Set_Extra_Accessibility_Of_Result (E,
+              Add_Extra_Formal (E, Standard_Natural, E, "L"));
+
+         else
+            pragma Assert (No (Parent_Subp)
+              or else not Needs_Result_Accessibility_Level (Parent_Subp));
+            pragma Assert (No (Alias_Subp)
+              or else not Needs_Result_Accessibility_Level (Alias_Subp));
+         end if;
+
+         Ada_Version := Save_Ada_Version;
+      end;
 
       --  Ada 2005 (AI-318-02): In the case of build-in-place functions, add
       --  appropriate extra formals. See type Exp_Ch6.BIP_Formal_Kind.
 
-      if Is_Build_In_Place_Function (E) then
+      if (Present (Parent_Subp) and then Has_BIP_Formals (Parent_Subp))
+            or else
+         (Present (Alias_Subp) and then Has_BIP_Formals (Alias_Subp))
+            or else
+         (Is_Build_In_Place_Function (Ref_E)
+            and then Has_Reliable_Extra_Formals (Ref_E))
+      then
          declare
-            Result_Subt : constant Entity_Id := Etype (E);
+            Result_Subt : constant Entity_Id := Etype (Ref_E);
             Formal_Typ  : Entity_Id;
             Subp_Decl   : Node_Id;
             Discard     : Entity_Id;
@@ -9187,7 +9752,14 @@ package body Sem_Ch6 is
             --  dispatching context and such calls must be handled like calls
             --  to a class-wide function.
 
-            if Needs_BIP_Alloc_Form (E) then
+            if Needs_BIP_Alloc_Form (Ref_E) then
+               pragma Assert (No (Parent_Subp)
+                 or else Has_BIP_Extra_Formal (Parent_Subp, BIP_Alloc_Form,
+                           Must_Be_Frozen => False));
+               pragma Assert (No (Alias_Subp)
+                 or else Has_BIP_Extra_Formal (Alias_Subp, BIP_Alloc_Form,
+                           Must_Be_Frozen => False));
+
                Discard :=
                  Add_Extra_Formal
                    (E, Standard_Natural,
@@ -9203,23 +9775,66 @@ package body Sem_Ch6 is
                       (E, RTE (RE_Root_Storage_Pool_Ptr),
                        E, BIP_Formal_Suffix (BIP_Storage_Pool));
                end if;
+
+            else
+               pragma Assert (No (Parent_Subp)
+                 or else not
+                   Has_BIP_Extra_Formal (Parent_Subp, BIP_Alloc_Form,
+                     Must_Be_Frozen => False));
+               pragma Assert (No (Alias_Subp)
+                 or else not
+                   Has_BIP_Extra_Formal (Alias_Subp, BIP_Alloc_Form,
+                     Must_Be_Frozen => False));
             end if;
 
             --  In the case of functions whose result type needs finalization,
             --  add an extra formal which represents the finalization master.
 
-            if Needs_BIP_Finalization_Master (E) then
+            if Needs_BIP_Finalization_Master (Ref_E) then
+               pragma Assert (No (Parent_Subp)
+                 or else Has_BIP_Extra_Formal (Parent_Subp,
+                           Kind           => BIP_Finalization_Master,
+                           Must_Be_Frozen => False));
+               pragma Assert (No (Alias_Subp)
+                 or else Has_BIP_Extra_Formal (Alias_Subp,
+                           Kind           => BIP_Finalization_Master,
+                           Must_Be_Frozen => False));
+
                Discard :=
                  Add_Extra_Formal
                    (E, RTE (RE_Finalization_Master_Ptr),
                     E, BIP_Formal_Suffix (BIP_Finalization_Master));
+
+            else
+               pragma Assert (No (Parent_Subp)
+                 or else not
+                   Has_BIP_Extra_Formal (Parent_Subp,
+                     Kind           => BIP_Finalization_Master,
+                     Must_Be_Frozen => False));
+               pragma Assert (No (Alias_Subp)
+                 or else not
+                   Has_BIP_Extra_Formal (Alias_Subp,
+                     Kind           => BIP_Finalization_Master,
+                     Must_Be_Frozen => False));
             end if;
 
             --  When the result type contains tasks, add two extra formals: the
             --  master of the tasks to be created, and the caller's activation
             --  chain.
 
-            if Needs_BIP_Task_Actuals (E) then
+            if Needs_BIP_Task_Actuals (Ref_E) then
+               pragma Assert (No (Parent_Subp)
+                 or else Has_BIP_Extra_Formal (Parent_Subp, BIP_Task_Master,
+                           Must_Be_Frozen => False));
+               pragma Assert (No (Alias_Subp)
+                 or else Has_BIP_Extra_Formal (Alias_Subp, BIP_Task_Master,
+                           Must_Be_Frozen => False)
+                 or else
+                   (Is_Abstract_Subprogram (Ref_E)
+                      and then Is_Predefined_Dispatching_Operation (Ref_E)
+                      and then Is_Interface
+                                 (Find_Dispatching_Type (Alias_Subp))));
+
                Discard :=
                  Add_Extra_Formal
                    (E, Standard_Integer,
@@ -9231,6 +9846,16 @@ package body Sem_Ch6 is
                  Add_Extra_Formal
                    (E, RTE (RE_Activation_Chain_Access),
                     E, BIP_Formal_Suffix (BIP_Activation_Chain));
+
+            else
+               pragma Assert (No (Parent_Subp)
+                 or else not
+                   Has_BIP_Extra_Formal (Parent_Subp, BIP_Task_Master,
+                     Must_Be_Frozen => False));
+               pragma Assert (No (Alias_Subp)
+                 or else not
+                   Has_BIP_Extra_Formal (Alias_Subp, BIP_Task_Master,
+                     Must_Be_Frozen => False));
             end if;
 
             --  All build-in-place functions get an extra formal that will be
@@ -9296,6 +9921,14 @@ package body Sem_Ch6 is
       if Is_Generic_Instance (E) and then Present (Alias (E)) then
          Set_Extra_Formals (Alias (E), Extra_Formals (E));
       end if;
+
+      pragma Assert (No (Alias_Subp)
+        or else Extra_Formals_Match_OK (E, Alias_Subp));
+
+      pragma Assert (No (Parent_Subp)
+        or else Extra_Formals_Match_OK (E, Parent_Subp));
+
+      pragma Assert (Extra_Formals_OK (E));
    end Create_Extra_Formals;
 
    -----------------------------
@@ -9526,252 +10159,162 @@ package body Sem_Ch6 is
       end if;
    end Enter_Overloaded_Entity;
 
-   -----------------------------
-   -- Check_Untagged_Equality --
-   -----------------------------
-
-   procedure Check_Untagged_Equality (Eq_Op : Entity_Id) is
-      Eq_Decl : constant Node_Id   := Unit_Declaration_Node (Eq_Op);
-      Typ     : constant Entity_Id := Etype (First_Formal (Eq_Op));
-
-      procedure Freezing_Point_Warning (N : Node_Id; S : String);
-      --  Output a warning about the freezing point N of Typ
-
-      function Is_Actual_Of_Instantiation
-        (E    : Entity_Id;
-         Inst : Node_Id) return Boolean;
-      --  Return True if E is an actual parameter of instantiation Inst
-
-      -----------------------------------
-      -- Output_Freezing_Point_Warning --
-      -----------------------------------
-
-      procedure Freezing_Point_Warning (N : Node_Id; S : String) is
-      begin
-         Error_Msg_String (1 .. S'Length) := S;
-         Error_Msg_Strlen := S'Length;
-
-         if Ada_Version >= Ada_2012 then
-            Error_Msg_NE ("type& is frozen by ~??", N, Typ);
-            Error_Msg_N
-              ("\an equality operator cannot be declared after this point??",
-               N);
-
-         else
-            Error_Msg_NE ("type& is frozen by ~ (Ada 2012)?y?", N, Typ);
-            Error_Msg_N
-              ("\an equality operator cannot be declared after this point"
-               & " (Ada 2012)?y?", N);
-         end if;
-      end Freezing_Point_Warning;
-
-      --------------------------------
-      -- Is_Actual_Of_Instantiation --
-      --------------------------------
-
-      function Is_Actual_Of_Instantiation
-        (E    : Entity_Id;
-         Inst : Node_Id) return Boolean
-      is
-         Assoc : Node_Id;
-
-      begin
-         if Present (Generic_Associations (Inst)) then
-            Assoc := First (Generic_Associations (Inst));
-
-            while Present (Assoc) loop
-               if Present (Explicit_Generic_Actual_Parameter (Assoc))
-                 and then
-                   Is_Entity_Name (Explicit_Generic_Actual_Parameter (Assoc))
-                 and then
-                   Entity (Explicit_Generic_Actual_Parameter (Assoc)) = E
-               then
-                  return True;
-               end if;
-
-               Next (Assoc);
-            end loop;
-         end if;
-
-         return False;
-      end Is_Actual_Of_Instantiation;
-
-      --  Local variable
-
-      Decl : Node_Id;
-
-   --  Start of processing for Check_Untagged_Equality
+   ----------------------------
+   -- Extra_Formals_Match_OK --
+   ----------------------------
 
+   function Extra_Formals_Match_OK
+     (E     : Entity_Id;
+      Ref_E : Entity_Id) return Boolean is
    begin
-      --  This check applies only if we have a subprogram declaration or a
-      --  subprogram body that is not a completion, for an untagged record
-      --  type, and that is conformant with the predefined operator.
+      pragma Assert (Is_Subprogram (E));
+
+      --  Cases where no check can be performed:
+      --    1) When expansion is not active (since we never generate extra
+      --       formals if expansion is not active because we don't need them
+      --       unless we are generating code).
+      --    2) On abstract predefined dispatching operations of Root_Controlled
+      --       and predefined stream operations not emitted by the frontend.
+      --    3) On renamings of abstract predefined dispatching operations of
+      --       interface types (since limitedness is not inherited in such
+      --       case (AI-419)).
+      --    4) The controlling formal of the nondispatching subprogram of
+      --       a concurrent type that overrides an interface primitive is
+      --       implicit and hence we cannot check here if all its extra
+      --       formals match; the expander will create the dispatching
+      --       primitive (without Convention_Protected) with the matching
+      --       formals (see exp_ch9.Build_Wrapper_Specs) which will be
+      --       checked later.
+
+      if Debug_Flag_Underscore_XX
+        or else not Expander_Active
+        or else
+          (Is_Predefined_Dispatching_Operation (E)
+             and then (not Has_Reliable_Extra_Formals (E)
+                         or else not Has_Reliable_Extra_Formals (Ref_E)))
+        or else
+          (Is_Predefined_Dispatching_Operation (E)
+             and then Is_Abstract_Subprogram (E)
+             and then Is_Interface (Find_Dispatching_Type (Ref_E)))
+      then
+         return True;
 
-      if (Nkind (Eq_Decl) /= N_Subprogram_Declaration
-           and then not (Nkind (Eq_Decl) = N_Subprogram_Body
-                          and then Acts_As_Spec (Eq_Decl)))
-        or else not Is_Record_Type (Typ)
-        or else Is_Tagged_Type (Typ)
-        or else not Is_User_Defined_Equality (Eq_Op)
+      elsif Convention (E) = Convention_Protected
+        and then not Is_Dispatching_Operation (E)
+        and then Is_Abstract_Subprogram (Ref_E)
+        and then Is_Interface (Find_Dispatching_Type (Ref_E))
       then
-         return;
+         return True;
       end if;
 
-      --  In Ada 2012 case, we will output errors or warnings depending on
-      --  the setting of debug flag -gnatd.E.
-
-      if Ada_Version >= Ada_2012 then
-         Error_Msg_Warn := Debug_Flag_Dot_EE;
+      --  Perform the checks
 
-      --  In earlier versions of Ada, nothing to do unless we are warning on
-      --  Ada 2012 incompatibilities (Warn_On_Ada_2012_Incompatibility set).
-
-      else
-         if not Warn_On_Ada_2012_Compatibility then
-            return;
-         end if;
+      if No (Extra_Formals (E)) then
+         return No (Extra_Formals (Ref_E));
       end if;
 
-      --  Cases where the type has already been frozen
-
-      if Is_Frozen (Typ) then
-
-         --  The check applies to a primitive operation, so check that type
-         --  and equality operation are in the same scope.
-
-         if Scope (Typ) /= Current_Scope then
-            return;
-
-         --  If the type is a generic actual (sub)type, the operation is not
-         --  primitive either because the base type is declared elsewhere.
+      if Ekind (E) in E_Function | E_Subprogram_Type
+        and then Present (Extra_Accessibility_Of_Result (E))
+                   /= Present (Extra_Accessibility_Of_Result (Ref_E))
+      then
+         return False;
+      end if;
 
-         elsif Is_Generic_Actual_Type (Typ) then
-            return;
+      declare
+         Formal_1 : Entity_Id := Extra_Formals (E);
+         Formal_2 : Entity_Id := Extra_Formals (Ref_E);
 
-         --  Here we may have an error of declaration after freezing, but we
-         --  must make sure not to flag the equality operator itself causing
-         --  the freezing when it is a subprogram body.
+      begin
+         while Present (Formal_1) and then Present (Formal_2) loop
+            if Has_Suffix (Formal_1, 'L') then
+               if not Has_Suffix (Formal_2, 'L') then
+                  return False;
+               end if;
 
-         else
-            Decl := Next (Declaration_Node (Typ));
+            elsif Has_Suffix (Formal_1, 'O') then
+               if not Has_Suffix (Formal_2, 'O') then
+                  return False;
+               end if;
 
-            while Present (Decl) and then Decl /= Eq_Decl loop
+            elsif BIP_Suffix_Kind (Formal_1) /= BIP_Suffix_Kind (Formal_2) then
+               return False;
+            end if;
 
-               --  The declaration of an object of the type
+            Formal_1 := Next_Formal_With_Extras (Formal_1);
+            Formal_2 := Next_Formal_With_Extras (Formal_2);
+         end loop;
 
-               if Nkind (Decl) = N_Object_Declaration
-                 and then Etype (Defining_Identifier (Decl)) = Typ
-               then
-                  Freezing_Point_Warning (Decl, "declaration");
-                  exit;
+         return No (Formal_1) and then No (Formal_2);
+      end;
+   end Extra_Formals_Match_OK;
 
-               --  The instantiation of a generic on the type
+   ----------------------
+   -- Extra_Formals_OK --
+   ----------------------
 
-               elsif Nkind (Decl) in N_Generic_Instantiation
-                 and then Is_Actual_Of_Instantiation (Typ, Decl)
-               then
-                  Freezing_Point_Warning (Decl, "instantiation");
-                  exit;
+   function Extra_Formals_OK (E : Entity_Id) return Boolean is
+      Last_Formal       : Entity_Id := Empty;
+      Formal            : Entity_Id;
+      Has_Extra_Formals : Boolean := False;
 
-               --  A noninstance proper body, body stub or entry body
+   begin
+      --  No check required if explicitly disabled
 
-               elsif Nkind (Decl) in N_Proper_Body
-                                   | N_Body_Stub
-                                   | N_Entry_Body
-                 and then not Is_Generic_Instance (Defining_Entity (Decl))
-               then
-                  Freezing_Point_Warning (Decl, "body");
-                  exit;
+      if Debug_Flag_Underscore_XX then
+         return True;
 
-               --  If we have reached the freeze node and immediately after we
-               --  have the body or generated code for the body, then it is the
-               --  body that caused the freezing and this is legal.
+      --  No check required if expansion is disabled because extra
+      --  formals are only generated when we are generating code.
+      --  See Create_Extra_Formals.
 
-               elsif Nkind (Decl) = N_Freeze_Entity
-                 and then Entity (Decl) = Typ
-                 and then (Next (Decl) = Eq_Decl
-                            or else
-                           Sloc (Next (Decl)) = Sloc (Eq_Decl))
-               then
-                  return;
-               end if;
+      elsif not Expander_Active then
+         return True;
+      end if;
 
-               Next (Decl);
-            end loop;
+      --  Check attribute Extra_Formal: If available, it must be set only
+      --  on the last formal of E.
 
-            --  Here we have a definite error of declaration after freezing
+      Formal := First_Formal (E);
+      while Present (Formal) loop
+         if Present (Extra_Formal (Formal)) then
+            if Has_Extra_Formals then
+               return False;
+            end if;
 
-            if Ada_Version >= Ada_2012 then
-               Error_Msg_NE
-                 ("equality operator must be declared before type & is "
-                  & "frozen (RM 4.5.2 (9.8)) (Ada 2012)<<", Eq_Op, Typ);
+            Has_Extra_Formals := True;
+         end if;
 
-               --  In Ada 2012 mode with error turned to warning, output one
-               --  more warning to warn that the equality operation may not
-               --  compose. This is the consequence of ignoring the error.
+         Last_Formal := Formal;
+         Next_Formal (Formal);
+      end loop;
 
-               if Error_Msg_Warn then
-                  Error_Msg_N ("\equality operation may not compose??", Eq_Op);
-               end if;
+      --  Check attribute Extra_Accessibility_Of_Result
 
-            else
-               Error_Msg_NE
-                 ("equality operator must be declared before type& is "
-                  & "frozen (RM 4.5.2 (9.8)) (Ada 2012)?y?", Eq_Op, Typ);
-            end if;
+      if Ekind (E) in E_Function | E_Subprogram_Type
+        and then Needs_Result_Accessibility_Level (E)
+        and then No (Extra_Accessibility_Of_Result (E))
+      then
+         return False;
+      end if;
 
-            --  If we have found no freezing point and the declaration of the
-            --  operator could not be reached from that of the type and we are
-            --  in a package body, this must be because the type is declared
-            --  in the spec of the package. Add a message tailored to this.
+      --  Check attribute Extra_Formals: If E has extra formals, then this
+      --  attribute must point to the first extra formal of E.
 
-            if No (Decl) and then In_Package_Body (Scope (Typ)) then
-               if Ada_Version >= Ada_2012 then
-                  if Nkind (Eq_Decl) = N_Subprogram_Body then
-                     Error_Msg_N
-                       ("\put declaration in package spec<<", Eq_Op);
-                  else
-                     Error_Msg_N
-                       ("\move declaration to package spec<<", Eq_Op);
-                  end if;
+      if Has_Extra_Formals then
+         return Present (Extra_Formals (E))
+           and then Present (Extra_Formal (Last_Formal))
+           and then Extra_Formal (Last_Formal) = Extra_Formals (E);
 
-               else
-                  if Nkind (Eq_Decl) = N_Subprogram_Body then
-                     Error_Msg_N
-                       ("\put declaration in package spec (Ada 2012)?y?",
-                        Eq_Op);
-                  else
-                     Error_Msg_N
-                       ("\move declaration to package spec (Ada 2012)?y?",
-                        Eq_Op);
-                  end if;
-               end if;
-            end if;
-         end if;
+      --  When E has no formals, the first extra formal is available through
+      --  the Extra_Formals attribute.
 
-      --  Now check for AI12-0352: the declaration of a user-defined primitive
-      --  equality operation for a record type T is illegal if it occurs after
-      --  a type has been derived from T.
+      elsif Present (Extra_Formals (E)) then
+         return No (First_Formal (E));
 
       else
-         Decl := Next (Declaration_Node (Typ));
-
-         while Present (Decl) and then Decl /= Eq_Decl loop
-            if Nkind (Decl) = N_Full_Type_Declaration
-              and then Etype (Defining_Identifier (Decl)) = Typ
-            then
-               Error_Msg_N
-                 ("equality operator cannot appear after derivation", Eq_Op);
-               Error_Msg_NE
-                 ("an equality operator for& cannot be declared after "
-                  & "this point??",
-                  Decl, Typ);
-            end if;
-
-            Next (Decl);
-         end loop;
+         return True;
       end if;
-   end Check_Untagged_Equality;
+   end Extra_Formals_OK;
 
    -----------------------------
    -- Find_Corresponding_Spec --
@@ -10656,6 +11199,89 @@ package body Sem_Ch6 is
       end if;
    end Fully_Conformant_Discrete_Subtypes;
 
+   ---------------------
+   -- Has_BIP_Formals --
+   ---------------------
+
+   function Has_BIP_Formals (E : Entity_Id) return Boolean is
+      Formal : Entity_Id := First_Formal_With_Extras (E);
+
+   begin
+      while Present (Formal) loop
+         if Is_Build_In_Place_Entity (Formal) then
+            return True;
+         end if;
+
+         Next_Formal_With_Extras (Formal);
+      end loop;
+
+      return False;
+   end Has_BIP_Formals;
+
+   --------------------------------
+   -- Has_Reliable_Extra_Formals --
+   --------------------------------
+
+   function Has_Reliable_Extra_Formals (E : Entity_Id) return Boolean is
+      Alias_E : Entity_Id;
+
+   begin
+      --  Extra formals are not added if expansion is not active (and hence if
+      --  available they are not reliable for extra formals check).
+
+      if not Expander_Active then
+         return False;
+
+      --  Currently the unique cases where extra formals are not reliable
+      --  are associated with predefined dispatching operations; otherwise
+      --  they are properly added when required.
+
+      elsif not Is_Predefined_Dispatching_Operation (E) then
+         return True;
+      end if;
+
+      Alias_E := Ultimate_Alias (E);
+
+      --  Abstract predefined primitives of Root_Controlled don't have
+      --  extra formals; this is required to build the runtime.
+
+      if Ekind (Alias_E) = E_Function
+        and then Is_Abstract_Subprogram (Alias_E)
+        and then Is_RTE (Underlying_Type (Etype (Alias_E)),
+                           RE_Root_Controlled)
+      then
+         return False;
+
+      --  Predefined stream dispatching operations that are not emitted by
+      --  the frontend; they have a renaming of the corresponding primitive
+      --  of their parent type and hence they don't have extra formals.
+
+      else
+         declare
+            Typ : constant Entity_Id :=
+                    Underlying_Type (Find_Dispatching_Type (Alias_E));
+
+         begin
+            if (Get_TSS_Name (E) = TSS_Stream_Input
+                  and then not Stream_Operation_OK (Typ, TSS_Stream_Input))
+              or else
+                (Get_TSS_Name (E) = TSS_Stream_Output
+                   and then not Stream_Operation_OK (Typ, TSS_Stream_Output))
+              or else
+                (Get_TSS_Name (E) = TSS_Stream_Read
+                   and then not Stream_Operation_OK (Typ, TSS_Stream_Read))
+              or else
+                (Get_TSS_Name (E) = TSS_Stream_Write
+                   and then not Stream_Operation_OK (Typ, TSS_Stream_Write))
+            then
+               return False;
+            end if;
+         end;
+      end if;
+
+      return True;
+   end Has_Reliable_Extra_Formals;
+
    --------------------
    -- Install_Entity --
    --------------------
@@ -12527,7 +13153,7 @@ package body Sem_Ch6 is
                   if Is_Dispatching_Operation (E) then
 
                      --  An overriding dispatching subprogram inherits the
-                     --  convention of the overridden subprogram (AI-117).
+                     --  convention of the overridden subprogram (AI95-117).
 
                      Set_Convention (S, Convention (E));
                      Check_Dispatching_Operation (S, E);
diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads
index da56ce6ab72..5f0e1baa4f9 100644
--- a/gcc/ada/sem_ch6.ads
+++ b/gcc/ada/sem_ch6.ads
@@ -174,6 +174,22 @@ package Sem_Ch6 is
    --  the end of Subp's parameter list (with each subsequent extra formal
    --  being attached to the preceding extra formal).
 
+   function Extra_Formals_Match_OK
+     (E     : Entity_Id;
+      Ref_E : Entity_Id) return Boolean;
+   --  Return True if the extra formals of the given entities match. E is a
+   --  subprogram, and Ref_E is the reference entity that will be used to check
+   --  the extra formals of E: a subprogram type or another subprogram. For
+   --  example, if E is a dispatching primitive of a tagged type then Ref_E
+   --  may be the overridden primitive of its parent type or its ultimate
+   --  renamed entity; however, if E is a subprogram to which 'Access is
+   --  applied then Ref_E is its corresponding subprogram type. Used in
+   --  assertions.
+
+   function Extra_Formals_OK (E : Entity_Id) return Boolean;
+   --  Return True if the decoration of the attributes associated with extra
+   --  formals are properly set. Used in assertions.
+
    function Find_Corresponding_Spec
      (N          : Node_Id;
       Post_Error : Boolean := True) return Entity_Id;
@@ -197,6 +213,9 @@ package Sem_Ch6 is
    --  Determines if two subtype definitions are fully conformant. Used
    --  for entry family conformance checks (RM 6.3.1 (24)).
 
+   function Has_BIP_Formals (E : Entity_Id) return Boolean;
+   --  Determines if a given entity has build-in-place formals
+
    procedure Install_Entity (E : Entity_Id);
    --  Place a single entity on the visibility chain
 
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index 195f27e14d6..5d9b2d0484d 100644
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -1823,6 +1823,7 @@ package body Sem_Eval is
          return False;
 
       elsif Op = Error
+        or else Nkind (Op) not in N_Has_Etype
         or else Etype (Op) = Any_Type
         or else Raises_Constraint_Error (Op)
       then
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index c00490cf55e..71548dcca17 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -23312,9 +23312,12 @@ package body Sem_Util is
 
          return Present (Extra_Accessibility_Of_Result (Alias (Func_Id)));
 
-      --  Remaining cases require Ada 2012 mode
+      --  Remaining cases require Ada 2012 mode, unless they are dispatching
+      --  operations, since they may be overridden by Ada_2012 primitives.
 
-      elsif Ada_Version < Ada_2012 then
+      elsif Ada_Version < Ada_2012
+        and then not Is_Dispatching_Operation (Func_Id)
+      then
          return False;
 
       --  Handle the situation where a result is an anonymous access type
