public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-648] [Ada] Fix bug in handling of Predicate_Failure aspect
@ 2022-05-19 14:07 Pierre-Marie de Rodat
  0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-19 14:07 UTC (permalink / raw)
  To: gcc-cvs

https://gcc.gnu.org/g:55a11c7e345dd06d6975fe8f4dc0e11ecbb581ff

commit r13-648-g55a11c7e345dd06d6975fe8f4dc0e11ecbb581ff
Author: Steve Baird <baird@adacore.com>
Date:   Mon Apr 4 17:52:11 2022 -0700

    [Ada] Fix bug in handling of Predicate_Failure aspect
    
    The run-time behavior of the Ada 2022 Predicate_Failure aspect was
    incorrectly implemented. This could cause incorrect exception messages
    at execution time in the case of a predicate check failure, as
    demonstrated by ACATS test C324006. In addition, a new attribute
    (Predicate_Expression) is defined in order to improve the FE/SPARK
    interface.
    
    gcc/ada/
    
            * einfo-utils.ads, einfo-utils.adb: Delete Predicate_Function_M
            function and Set_Predicate_Function_M procedure.
            * einfo.ads: Delete comments for Is_Predicate_Function_M and
            Predicate_Function_M functions. Add comment for new
            Predicate_Expression function. Update comment describing
            predicate functions.
            * exp_util.ads, exp_util.adb (Make_Predicate_Call): Replace Mem
            formal parameter with Static_Mem and Dynamic_Mem formals.
            (Make_Predicate_Check): Delete Add_Failure_Expression and call
            to it.
            * exp_ch4.adb (Expand_N_In.Predicate_Check): Update
            Make_Predicate_Call call to match profile change.
            * gen_il-fields.ads: Delete Is_Predicate_Function_M field, add
            Predicate_Expression field.
            * gen_il-gen-gen_entities.adb: Delete Is_Predicate_Function_M
            use, add Predicate_Expression use.
            * sem_ch13.adb (Build_Predicate_Functions): Rename as singular,
            not plural; we no longer build a Predicate_M function. Delete
            Predicate_M references. Add new Boolean parameter for predicate
            functions when needed. Restructure body of generated predicate
            functions to implement required Predicate_Failure behavior and
            to set new Predicate_Expression attribute. Remove special
            treatment of raise expressions within predicate expressions.
            * sem_util.ads (Predicate_Failure_Expression,
            Predicate_Function_Needs_Membership_Parameter): New functions.
            * sem_util.adb (Is_Current_Instance): Fix bugs which caused
            wrong result.
            (Is_Current_Instance_Reference_In_Type_Aspect): Delete
            Is_Predicate_Function_M reference.
            (Predicate_Failure_Expression): New function.
            (Propagate_Predicate_Attributes): Delete Is_Predicate_Function_M
            references.

Diff:
---
 gcc/ada/einfo-utils.adb             |  84 ------
 gcc/ada/einfo-utils.ads             |   2 -
 gcc/ada/einfo.ads                   |  26 +-
 gcc/ada/exp_ch4.adb                 |   4 +-
 gcc/ada/exp_util.adb                | 203 ++-----------
 gcc/ada/exp_util.ads                |  16 +-
 gcc/ada/gen_il-fields.ads           |   2 +-
 gcc/ada/gen_il-gen-gen_entities.adb |   3 +-
 gcc/ada/sem_ch13.adb                | 565 ++++++++++++++++++------------------
 gcc/ada/sem_util.adb                |  88 +++++-
 gcc/ada/sem_util.ads                |  20 ++
 11 files changed, 436 insertions(+), 577 deletions(-)

diff --git a/gcc/ada/einfo-utils.adb b/gcc/ada/einfo-utils.adb
index cf61ec7de28..48a1bce817d 100644
--- a/gcc/ada/einfo-utils.adb
+++ b/gcc/ada/einfo-utils.adb
@@ -2390,53 +2390,6 @@ package body Einfo.Utils is
       return Empty;
    end Predicate_Function;
 
-   --------------------------
-   -- Predicate_Function_M --
-   --------------------------
-
-   function Predicate_Function_M (Id : E) return E is
-      Subp_Elmt : Elmt_Id;
-      Subp_Id   : Entity_Id;
-      Subps     : Elist_Id;
-      Typ       : Entity_Id;
-
-   begin
-      pragma Assert (Is_Type (Id));
-
-      --  If type is private and has a completion, predicate may be defined on
-      --  the full view.
-
-      if Is_Private_Type (Id)
-         and then
-           (not Has_Predicates (Id) or else No (Subprograms_For_Type (Id)))
-         and then Present (Full_View (Id))
-      then
-         Typ := Full_View (Id);
-
-      else
-         Typ := Id;
-      end if;
-
-      Subps := Subprograms_For_Type (Typ);
-
-      if Present (Subps) then
-         Subp_Elmt := First_Elmt (Subps);
-         while Present (Subp_Elmt) loop
-            Subp_Id := Node (Subp_Elmt);
-
-            if Ekind (Subp_Id) = E_Function
-              and then Is_Predicate_Function_M (Subp_Id)
-            then
-               return Subp_Id;
-            end if;
-
-            Next_Elmt (Subp_Elmt);
-         end loop;
-      end if;
-
-      return Empty;
-   end Predicate_Function_M;
-
    -------------------------
    -- Present_In_Rep_Item --
    -------------------------
@@ -2879,43 +2832,6 @@ package body Einfo.Utils is
       end loop;
    end Set_Predicate_Function;
 
-   ------------------------------
-   -- Set_Predicate_Function_M --
-   ------------------------------
-
-   procedure Set_Predicate_Function_M (Id : E; V : E) is
-      Subp_Elmt : Elmt_Id;
-      Subp_Id   : Entity_Id;
-      Subps     : Elist_Id;
-
-   begin
-      pragma Assert (Is_Type (Id) and then Has_Predicates (Id));
-
-      Subps := Subprograms_For_Type (Id);
-
-      if No (Subps) then
-         Subps := New_Elmt_List;
-         Set_Subprograms_For_Type (Id, Subps);
-      end if;
-
-      Subp_Elmt := First_Elmt (Subps);
-      Prepend_Elmt (V, Subps);
-
-      --  Check for a duplicate predication function
-
-      while Present (Subp_Elmt) loop
-         Subp_Id := Node (Subp_Elmt);
-
-         if Ekind (Subp_Id) = E_Function
-           and then Is_Predicate_Function_M (Subp_Id)
-         then
-            raise Program_Error;
-         end if;
-
-         Next_Elmt (Subp_Elmt);
-      end loop;
-   end Set_Predicate_Function_M;
-
    -----------------
    -- Size_Clause --
    -----------------
diff --git a/gcc/ada/einfo-utils.ads b/gcc/ada/einfo-utils.ads
index f914de7cc83..d830c8da259 100644
--- a/gcc/ada/einfo-utils.ads
+++ b/gcc/ada/einfo-utils.ads
@@ -437,14 +437,12 @@ package Einfo.Utils is
    function Invariant_Procedure                  (Id : E) return E;
    function Partial_Invariant_Procedure          (Id : E) return E;
    function Predicate_Function                   (Id : E) return E;
-   function Predicate_Function_M                 (Id : E) return E;
 
    procedure Set_DIC_Procedure                   (Id : E; V : E);
    procedure Set_Partial_DIC_Procedure           (Id : E; V : E);
    procedure Set_Invariant_Procedure             (Id : E; V : E);
    procedure Set_Partial_Invariant_Procedure     (Id : E; V : E);
    procedure Set_Predicate_Function              (Id : E; V : E);
-   procedure Set_Predicate_Function_M            (Id : E; V : E);
 
    ---------------
    -- Iterators --
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 3f990c3b831..b0601a9648d 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3106,11 +3106,6 @@ package Einfo is
 --       Present in functions and procedures. Set for generated predicate
 --       functions.
 
---    Is_Predicate_Function_M
---       Present in functions and procedures. Set for special version of
---       predicate function generated for use in membership tests, where
---       raise expressions are transformed to return False.
-
 --    Is_Preelaborated
 --       Defined in all entities, set in E_Package and E_Generic_Package
 --       entities to which a pragma Preelaborate is applied, and also in
@@ -4010,8 +4005,9 @@ package Einfo is
 --       Defined in all types. Set for types for which (Has_Predicates is True)
 --       and for which a predicate procedure has been built that tests that the
 --       specified predicates are True. Contains the entity for the function
---       which takes a single argument of the given type, and returns True if
---       the predicate holds and False if it does not.
+--       which takes a single argument of the given type (and sometimes an
+--       additional Boolean parameter), and returns True if the predicate
+--       holds and False if it does not.
 --
 --       Note: flag Has_Predicate does not imply that Predicate_Function is set
 --       to a non-empty entity; this happens, for example, for itypes created
@@ -4024,11 +4020,14 @@ package Einfo is
 --       Note: the reason this is marked as a synthesized attribute is that the
 --       way this is stored is as an element of the Subprograms_For_Type field.
 
---    Predicate_Function_M (synthesized)
---       Defined in all types. Present only if Predicate_Function is present,
---       and only if the predicate function has Raise_Expression nodes. It
---       is the special version created for membership tests, where if one of
---       these raise expressions is executed, the result is to return False.
+--    Predicate_Expression
+--      Defined on functions. For the defining identifier of the subprogram
+--      declaration (not of the subprogram body) of a predicate function,
+--      yields the expression for the noninherited portion of the given
+--      predicate (except in the case where the inherited portion is
+--      non-empty and the non-inherited portion is empty, in which case the
+--      expression for the inherited portion is returned). Otherwise yields
+--      empty.
 
 --    Predicated_Parent
 --       Defined on itypes created by subtype indications, when the parent
@@ -5115,7 +5114,6 @@ package Einfo is
    --    Partial_DIC_Procedure               (synth)
    --    Partial_Invariant_Procedure         (synth)
    --    Predicate_Function                  (synth)
-   --    Predicate_Function_M                (synth)
    --    Root_Type                           (synth)
    --    Size_Clause                         (synth)
 
@@ -5591,7 +5589,6 @@ package Einfo is
    --    Is_Machine_Code_Subprogram           (non-generic case only)
    --    Is_Partial_Invariant_Procedure       (non-generic case only)
    --    Is_Predicate_Function                (non-generic case only)
-   --    Is_Predicate_Function_M              (non-generic case only)
    --    Is_Primitive
    --    Is_Primitive_Wrapper                 (non-generic case only)
    --    Is_Private_Descendant
@@ -5956,7 +5953,6 @@ package Einfo is
    --    Is_Partial_DIC_Procedure             (synth) (non-generic case only)
    --    Is_Partial_Invariant_Procedure       (non-generic case only)
    --    Is_Predicate_Function                (non-generic case only)
-   --    Is_Predicate_Function_M              (non-generic case only)
    --    Is_Primitive
    --    Is_Primitive_Wrapper                 (non-generic case only)
    --    Is_Private_Descendant
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 14e9b0e508e..9e86b4d81a5 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -6962,7 +6962,9 @@ package body Exp_Ch4 is
            and then Nkind (Rop) /= N_Range
          then
             if not In_Range_Check then
-               R_Op := Make_Predicate_Call (Rtyp, Lop, Mem => True);
+               --  Indicate via Static_Mem parameter that this predicate
+               --  evaluation is for a membership test.
+               R_Op := Make_Predicate_Call (Rtyp, Lop, Static_Mem => True);
             else
                R_Op := New_Occurrence_Of (Standard_True, Loc);
             end if;
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 31a2d5c3165..290c3805627 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -9927,9 +9927,10 @@ package body Exp_Util is
    --  Ghost mode.
 
    function Make_Predicate_Call
-     (Typ  : Entity_Id;
-      Expr : Node_Id;
-      Mem  : Boolean := False) return Node_Id
+     (Typ         : Entity_Id;
+      Expr        : Node_Id;
+      Static_Mem  : Boolean := False;
+      Dynamic_Mem : Node_Id := Empty) return Node_Id
    is
       Loc : constant Source_Ptr := Sloc (Expr);
 
@@ -9937,9 +9938,9 @@ package body Exp_Util is
       Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
       --  Save the Ghost-related attributes to restore on exit
 
-      Call    : Node_Id;
-      Func_Id : Entity_Id;
-
+      Call         : Node_Id;
+      Func_Id      : Entity_Id;
+      Param_Assocs : List_Id;
    begin
       Func_Id := Predicate_Function (Typ);
       pragma Assert (Present (Func_Id));
@@ -9949,12 +9950,6 @@ package body Exp_Util is
 
       Set_Ghost_Mode (Typ);
 
-      --  Call special membership version if requested and available
-
-      if Mem and then Present (Predicate_Function_M (Typ)) then
-         Func_Id := Predicate_Function_M (Typ);
-      end if;
-
       --  Case of calling normal predicate function
 
       --  If the type is tagged, the expression may be class-wide, in which
@@ -9964,18 +9959,26 @@ package body Exp_Util is
       --  extensions are involved.
 
       if Is_Tagged_Type (Typ) then
-         Call :=
-           Make_Function_Call (Loc,
-             Name                   => New_Occurrence_Of (Func_Id, Loc),
-             Parameter_Associations =>
-               New_List (OK_Convert_To (Typ, Relocate_Node (Expr))));
+         Param_Assocs := New_List (OK_Convert_To (Typ, Relocate_Node (Expr)));
       else
-         Call :=
-           Make_Function_Call (Loc,
-             Name                   => New_Occurrence_Of (Func_Id, Loc),
-             Parameter_Associations => New_List (Relocate_Node (Expr)));
+         Param_Assocs := New_List (Relocate_Node (Expr));
       end if;
 
+      if Predicate_Function_Needs_Membership_Parameter (Typ) then
+         --  Pass in parameter indicating whether this call is for a
+         --  membership test.
+         Append ((if Present (Dynamic_Mem)
+                    then Dynamic_Mem
+                    else New_Occurrence_Of
+                           (Boolean_Literals (Static_Mem), Loc)),
+                 Param_Assocs);
+      end if;
+
+      Call :=
+        Make_Function_Call (Loc,
+          Name                   => New_Occurrence_Of (Func_Id, Loc),
+          Parameter_Associations => Param_Assocs);
+
       Restore_Ghost_Region (Saved_GM, Saved_IGR);
 
       return Call;
@@ -9991,161 +9994,6 @@ package body Exp_Util is
    is
       Loc : constant Source_Ptr := Sloc (Expr);
 
-      procedure Add_Failure_Expression (Args : List_Id);
-      --  Add the failure expression of pragma Predicate_Failure (if any) to
-      --  list Args.
-
-      ----------------------------
-      -- Add_Failure_Expression --
-      ----------------------------
-
-      procedure Add_Failure_Expression (Args : List_Id) is
-         function Failure_Expression return Node_Id;
-         pragma Inline (Failure_Expression);
-         --  Find aspect or pragma Predicate_Failure that applies to type Typ
-         --  and return its expression. Return Empty if no such annotation is
-         --  available.
-
-         function Is_OK_PF_Aspect (Asp : Node_Id) return Boolean;
-         pragma Inline (Is_OK_PF_Aspect);
-         --  Determine whether aspect Asp is a suitable Predicate_Failure
-         --  aspect that applies to type Typ.
-
-         function Is_OK_PF_Pragma (Prag : Node_Id) return Boolean;
-         pragma Inline (Is_OK_PF_Pragma);
-         --  Determine whether pragma Prag is a suitable Predicate_Failure
-         --  pragma that applies to type Typ.
-
-         procedure Replace_Subtype_Reference (N : Node_Id);
-         --  Replace the current instance of type Typ denoted by N with
-         --  expression Expr.
-
-         ------------------------
-         -- Failure_Expression --
-         ------------------------
-
-         function Failure_Expression return Node_Id is
-            Item : Node_Id;
-
-         begin
-            --  The management of the rep item chain involves "inheritance" of
-            --  parent type chains. If a parent [sub]type is already subject to
-            --  pragma Predicate_Failure, then the pragma will also appear in
-            --  the chain of the child [sub]type, which in turn may possess a
-            --  pragma of its own. Avoid order-dependent issues by inspecting
-            --  the rep item chain directly. Note that routine Get_Pragma may
-            --  return a parent pragma.
-
-            Item := First_Rep_Item (Typ);
-            while Present (Item) loop
-
-               --  Predicate_Failure appears as an aspect
-
-               if Nkind (Item) = N_Aspect_Specification
-                 and then Is_OK_PF_Aspect (Item)
-               then
-                  return Expression (Item);
-
-               --  Predicate_Failure appears as a pragma
-
-               elsif Nkind (Item) = N_Pragma
-                 and then Is_OK_PF_Pragma (Item)
-               then
-                  return
-                    Get_Pragma_Arg
-                      (Next (First (Pragma_Argument_Associations (Item))));
-               end if;
-
-               Next_Rep_Item (Item);
-            end loop;
-
-            return Empty;
-         end Failure_Expression;
-
-         ---------------------
-         -- Is_OK_PF_Aspect --
-         ---------------------
-
-         function Is_OK_PF_Aspect (Asp : Node_Id) return Boolean is
-         begin
-            --  To qualify, the aspect must apply to the type subjected to the
-            --  predicate check.
-
-            return
-              Chars (Identifier (Asp)) = Name_Predicate_Failure
-                and then Present (Entity (Asp))
-                and then Entity (Asp) = Typ;
-         end Is_OK_PF_Aspect;
-
-         ---------------------
-         -- Is_OK_PF_Pragma --
-         ---------------------
-
-         function Is_OK_PF_Pragma (Prag : Node_Id) return Boolean is
-            Args    : constant List_Id := Pragma_Argument_Associations (Prag);
-            Typ_Arg : Node_Id;
-
-         begin
-            --  Nothing to do when the pragma does not denote Predicate_Failure
-
-            if Pragma_Name (Prag) /= Name_Predicate_Failure then
-               return False;
-
-            --  Nothing to do when the pragma lacks arguments, in which case it
-            --  is illegal.
-
-            elsif Is_Empty_List (Args) then
-               return False;
-            end if;
-
-            Typ_Arg := Get_Pragma_Arg (First (Args));
-
-            --  To qualify, the local name argument of the pragma must denote
-            --  the type subjected to the predicate check.
-
-            return
-              Is_Entity_Name (Typ_Arg)
-                and then Present (Entity (Typ_Arg))
-                and then Entity (Typ_Arg) = Typ;
-         end Is_OK_PF_Pragma;
-
-         --------------------------------
-         --  Replace_Subtype_Reference --
-         --------------------------------
-
-         procedure Replace_Subtype_Reference (N : Node_Id) is
-         begin
-            Rewrite (N, New_Copy_Tree (Expr));
-         end Replace_Subtype_Reference;
-
-         procedure Replace_Subtype_References is
-           new Replace_Type_References_Generic (Replace_Subtype_Reference);
-
-         --  Local variables
-
-         PF_Expr : constant Node_Id := Failure_Expression;
-         Expr    : Node_Id;
-
-      --  Start of processing for Add_Failure_Expression
-
-      begin
-         if Present (PF_Expr) then
-
-            --  Replace any occurrences of the current instance of the type
-            --  with the object subjected to the predicate check.
-
-            Expr := New_Copy_Tree (PF_Expr);
-            Replace_Subtype_References (Expr, Typ);
-
-            --  The failure expression appears as the third argument of the
-            --  Check pragma.
-
-            Append_To (Args,
-              Make_Pragma_Argument_Association (Loc,
-                Expression => Expr));
-         end if;
-      end Add_Failure_Expression;
-
       --  Local variables
 
       Args : List_Id;
@@ -10188,8 +10036,6 @@ package body Exp_Util is
       --  If the subtype is subject to pragma Predicate_Failure, add the
       --  failure expression as an additional parameter.
 
-      Add_Failure_Expression (Args);
-
       return
         Make_Pragma (Loc,
           Chars                        => Name_Check,
@@ -14339,7 +14185,6 @@ package body Exp_Util is
 
          elsif Get_TSS_Name (S) /= TSS_Null
            and then not Is_Predicate_Function (S)
-           and then not Is_Predicate_Function_M (S)
          then
             return False;
          end if;
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index f3456b3f455..464f66f7420 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -876,13 +876,19 @@ package Exp_Util is
    --  expression Expr. Expr is passed as an actual parameter in the call.
 
    function Make_Predicate_Call
-     (Typ  : Entity_Id;
-      Expr : Node_Id;
-      Mem  : Boolean := False) return Node_Id;
+     (Typ         : Entity_Id;
+      Expr        : Node_Id;
+      Static_Mem  : Boolean := False;
+      Dynamic_Mem : Node_Id := Empty) return Node_Id;
    --  Typ is a type with Predicate_Function set. This routine builds a call to
    --  this function passing Expr as the argument, and returns it unanalyzed.
-   --  If Mem is set True, this is the special call for the membership case,
-   --  and the function called is the Predicate_Function_M if present.
+   --  If the callee takes a second parameter (as determined by
+   --  Sem_Util.Predicate_Function_Needs_Membership_Parameter), then the
+   --  actual parameter is determined by the two Mem parameters.
+   --  If Dynamic_Mem is nonempty, then Dynamic_Mem is the actual parameter.
+   --  Otherwise, the value of the Static_Mem parameter is passed in as
+   --  a Boolean literal. It is an error if Dynamic_Mem is nonempty but
+   --  the callee does not take a second parameter.
 
    function Make_Predicate_Check
      (Typ  : Entity_Id;
diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads
index eedae64ed33..878755bf34e 100644
--- a/gcc/ada/gen_il-fields.ads
+++ b/gcc/ada/gen_il-fields.ads
@@ -756,7 +756,6 @@ package Gen_IL.Fields is
       Is_Partial_Invariant_Procedure,
       Is_Potentially_Use_Visible,
       Is_Predicate_Function,
-      Is_Predicate_Function_M,
       Is_Preelaborated,
       Is_Primitive,
       Is_Primitive_Wrapper,
@@ -851,6 +850,7 @@ package Gen_IL.Fields is
       Partial_View_Has_Unknown_Discr,
       Pending_Access_Types,
       Postconditions_Proc,
+      Predicate_Expression,
       Prev_Entity,
       Prival,
       Prival_Link,
diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb
index 5b8603b85b0..89d86594c52 100644
--- a/gcc/ada/gen_il-gen-gen_entities.adb
+++ b/gcc/ada/gen_il-gen-gen_entities.adb
@@ -1031,7 +1031,6 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Is_Invariant_Procedure, Flag),
         Sm (Is_Partial_Invariant_Procedure, Flag),
         Sm (Is_Predicate_Function, Flag),
-        Sm (Is_Predicate_Function_M, Flag),
         Sm (Is_Primitive_Wrapper, Flag),
         Sm (Is_Private_Primitive, Flag),
         Sm (LSP_Subprogram, Node_Id),
@@ -1039,6 +1038,7 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Next_Inlined_Subprogram, Node_Id),
         Sm (Original_Protected_Subprogram, Node_Id),
         Sm (Postconditions_Proc, Node_Id),
+        Sm (Predicate_Expression, Node_Id),
         Sm (Protected_Subprogram, Node_Id),
         Sm (Protection_Object, Node_Id),
         Sm (Related_Expression, Node_Id),
@@ -1080,7 +1080,6 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Is_Null_Init_Proc, Flag),
         Sm (Is_Partial_Invariant_Procedure, Flag),
         Sm (Is_Predicate_Function, Flag),
-        Sm (Is_Predicate_Function_M, Flag),
         Sm (Is_Primitive_Wrapper, Flag),
         Sm (Is_Private_Primitive, Flag),
         Sm (Is_Valued_Procedure, Flag),
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 8bd0c866fd4..54f32a2fc49 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -133,7 +133,7 @@ package body Sem_Ch13 is
    --  may be before the freeze point of the type. The predicate expression is
    --  preanalyzed at this point, to catch visibility errors.
 
-   procedure Build_Predicate_Functions (Typ : Entity_Id; N : Node_Id);
+   procedure Build_Predicate_Function (Typ : Entity_Id; N : Node_Id);
    --  If Typ has predicates (indicated by Has_Predicates being set for Typ),
    --  then either there are pragma Predicate entries on the rep chain for the
    --  type (note that Predicate aspects are converted to pragma Predicate), or
@@ -141,9 +141,7 @@ package body Sem_Ch13 is
    --  This procedure builds body for the Predicate function that tests these
    --  predicates. N is the freeze node for the type. The spec of the function
    --  is inserted before the freeze node, and the body of the function is
-   --  inserted after the freeze node. If the predicate expression has a least
-   --  one Raise_Expression, then this procedure also builds the M version of
-   --  the predicate function for use in membership tests.
+   --  inserted after the freeze node.
 
    procedure Check_Pool_Size_Clash (Ent : Entity_Id; SP, SS : Node_Id);
    --  Called if both Storage_Pool and Storage_Size attribute definition
@@ -9462,10 +9460,7 @@ package body Sem_Ch13 is
                   declare
                      Ent : constant Entity_Id := Entity (Name (Exp));
                   begin
-                     if Is_Predicate_Function (Ent)
-                          or else
-                        Is_Predicate_Function_M (Ent)
-                     then
+                     if Is_Predicate_Function (Ent) then
                         return Stat_Pred (Etype (First_Formal (Ent)), Static);
                      end if;
                   end;
@@ -10006,11 +10001,11 @@ package body Sem_Ch13 is
       return Prag;
    end Build_Export_Import_Pragma;
 
-   -------------------------------
-   -- Build_Predicate_Functions --
-   -------------------------------
+   ------------------------------
+   -- Build_Predicate_Function --
+   ------------------------------
 
-   --  The functions that are constructed here have the form:
+   --  The function constructed here has the form:
 
    --    function typPredicate (Ixxx : typ) return Boolean is
    --    begin
@@ -10021,6 +10016,18 @@ package body Sem_Ch13 is
    --          and then exp1 and then exp2 and then ...;
    --    end typPredicate;
 
+   --  If Predicate_Function_Needs_Membership_Parameter is true, then this
+   --  function takes an additional boolean parameter; the parameter
+   --  indicates whether the predicate evaluation is part of a membership
+   --  test. This parameter is used in two cases: 1) It is passed along
+   --  if another predicate function is called and that predicate function
+   --  expects to be passed a boolean parameter. 2) If the Predicate_Failure
+   --  aspect is directly specified for typ, then we replace the return
+   --  expression described above with
+   --      (if <expression described above> then True
+   --       elsif For_Membership_Test then False
+   --       else (raise Assertion_Error
+   --                     with <Predicate_Failure expression>))
    --  Here exp1, and exp2 are expressions from Predicate pragmas. Note that
    --  this is the point at which these expressions get analyzed, providing the
    --  required delay, and typ1, typ2, are entities from which predicates are
@@ -10033,26 +10040,17 @@ package body Sem_Ch13 is
    --  Note that Sem_Eval.Real_Or_String_Static_Predicate_Matches depends on
    --  the form of this return expression.
 
-   --  If the expression has at least one Raise_Expression, then we also build
-   --  the typPredicateM version of the function, in which any occurrence of a
-   --  Raise_Expression is converted to "return False".
-
    --  WARNING: This routine manages Ghost regions. Return statements must be
    --  replaced by gotos which jump to the end of the routine and restore the
    --  Ghost mode.
 
-   procedure Build_Predicate_Functions (Typ : Entity_Id; N : Node_Id) is
+   procedure Build_Predicate_Function (Typ : Entity_Id; N : Node_Id) is
       Loc : constant Source_Ptr := Sloc (Typ);
 
       Expr : Node_Id;
       --  This is the expression for the result of the function. It is
       --  is build by connecting the component predicates with AND THEN.
 
-      Expr_M : Node_Id := Empty; -- init to avoid warning
-      --  This is the corresponding return expression for the Predicate_M
-      --  function. It differs in that raise expressions are marked for
-      --  special expansion (see Process_REs).
-
       Object_Name : Name_Id;
       --  Name for argument of Predicate procedure. Note that we use the same
       --  name for both predicate functions. That way the reference within the
@@ -10061,18 +10059,15 @@ package body Sem_Ch13 is
       Object_Entity : Entity_Id;
       --  Entity for argument of Predicate procedure
 
-      Object_Entity_M : Entity_Id;
-      --  Entity for argument of separate Predicate procedure when exceptions
-      --  are present in expression.
-
       FDecl : Node_Id;
       --  The function declaration
 
       SId : Entity_Id;
       --  Its entity
 
-      Raise_Expression_Present : Boolean := False;
-      --  Set True if Expr has at least one Raise_Expression
+      Ancestor_Predicate_Function_Called : Boolean := False;
+      --  Does this predicate function include a call to the
+      --  predication function of an ancestor subtype?
 
       procedure Add_Condition (Cond : Node_Id);
       --  Append Cond to Expr using "and then" (or just copy Cond to Expr if
@@ -10088,19 +10083,11 @@ package body Sem_Ch13 is
       --  Includes a call to the predicate function for type T in Expr if
       --  Predicate_Function (T) is non-empty.
 
-      function Process_RE (N : Node_Id) return Traverse_Result;
-      --  Used in Process REs, tests if node N is a raise expression, and if
-      --  so, marks it to be converted to return False.
-
-      procedure Process_REs is new Traverse_Proc (Process_RE);
-      --  Marks any raise expressions in Expr_M to return False
-
-      function Test_RE (N : Node_Id) return Traverse_Result;
-      --  Used in Test_REs, tests one node for being a raise expression, and if
-      --  so sets Raise_Expression_Present True.
-
-      procedure Test_REs is new Traverse_Proc (Test_RE);
-      --  Tests to see if Expr contains any raise expressions
+      procedure Replace_Current_Instance_References
+         (N : Node_Id; Typ, New_Entity : Entity_Id);
+      --  Replace all references to Typ in the tree rooted at N with
+      --  references to Param. [New_Entity will be a formal parameter of a
+      --  predicate function.]
 
       --------------
       -- Add_Call --
@@ -10116,16 +10103,34 @@ package body Sem_Ch13 is
             --  Build the call to the predicate function of T. The type may be
             --  derived, so use an unchecked conversion for the actual.
 
-            Exp :=
-              Make_Predicate_Call
-                (Typ  => T,
-                 Expr =>
-                   Unchecked_Convert_To (T,
-                     Make_Identifier (Loc, Object_Name)));
+            declare
+               Dynamic_Mem : Node_Id := Empty;
+               Second_Formal : constant Entity_Id :=
+                 Next_Entity (Object_Entity);
+            begin
+               --  Some predicate functions require a second parameter;
+               --  If one predicate function calls another and the second
+               --  requires two parameters, then the first should also
+               --  take two parameters (so that the first function has
+               --  something to pass to the second function).
+               if Predicate_Function_Needs_Membership_Parameter (T) then
+                  pragma Assert (Present (Second_Formal));
+                  Dynamic_Mem := New_Occurrence_Of (Second_Formal, Loc);
+               end if;
+
+               Exp :=
+                 Make_Predicate_Call
+                   (Typ  => T,
+                    Expr =>
+                      Unchecked_Convert_To (T,
+                        Make_Identifier (Loc, Object_Name)),
+                    Dynamic_Mem => Dynamic_Mem);
+            end;
 
             --  "and"-in the call to evolving expression
 
             Add_Condition (Exp);
+            Ancestor_Predicate_Function_Called := True;
 
             --  Output info message on inheritance if required. Note we do not
             --  give this information for generic actual types, since it is
@@ -10182,32 +10187,6 @@ package body Sem_Ch13 is
          -------------------
 
          procedure Add_Predicate (Prag : Node_Id) is
-            procedure Replace_Type_Reference (N : Node_Id);
-            --  Replace a single occurrence N of the subtype name with a
-            --  reference to the formal of the predicate function. N can be an
-            --  identifier referencing the subtype, or a selected component,
-            --  representing an appropriately qualified occurrence of the
-            --  subtype name.
-
-            procedure Replace_Type_References is
-              new Replace_Type_References_Generic (Replace_Type_Reference);
-            --  Traverse an expression changing every occurrence of an
-            --  identifier whose name matches the name of the subtype with a
-            --  reference to the formal parameter of the predicate function.
-
-            ----------------------------
-            -- Replace_Type_Reference --
-            ----------------------------
-
-            procedure Replace_Type_Reference (N : Node_Id) is
-            begin
-               Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
-               --  Use the Sloc of the usage name, not the defining name
-
-               Set_Etype (N, Typ);
-               Set_Entity (N, Object_Entity);
-            end Replace_Type_Reference;
-
             --  Local variables
 
             Asp  : constant Node_Id := Corresponding_Aspect (Prag);
@@ -10236,20 +10215,25 @@ package body Sem_Ch13 is
             if Entity (Arg1) = Typ
               or else Full_View (Entity (Arg1)) = Typ
             then
-               Replace_Type_References (Arg2, Typ);
+               declare
+                  Arg2_Copy : constant Node_Id := New_Copy_Tree (Arg2);
+               begin
+                  Replace_Current_Instance_References
+                   (Arg2_Copy, Typ => Typ, New_Entity => Object_Entity);
 
-               --  If the predicate pragma comes from an aspect, replace the
-               --  saved expression because we need the subtype references
-               --  replaced for the calls to Preanalyze_Spec_Expression in
-               --  Check_Aspect_At_xxx routines.
+                  --  If the predicate pragma comes from an aspect, replace the
+                  --  saved expression because we need the subtype references
+                  --  replaced for the calls to Preanalyze_Spec_Expression in
+                  --  Check_Aspect_At_xxx routines.
 
-               if Present (Asp) then
-                  Set_Entity (Identifier (Asp), New_Copy_Tree (Arg2));
-               end if;
+                  if Present (Asp) then
+                     Set_Entity (Identifier (Asp), New_Copy_Tree (Arg2_Copy));
+                  end if;
 
-               --  "and"-in the Arg2 condition to evolving expression
+                  --  "and"-in the Arg2 condition to evolving expression
 
-               Add_Condition (Relocate_Node (Arg2));
+                  Add_Condition (Arg2_Copy);
+               end;
             end if;
          end Add_Predicate;
 
@@ -10303,33 +10287,34 @@ package body Sem_Ch13 is
          end loop;
       end Add_Predicates;
 
-      ----------------
-      -- Process_RE --
-      ----------------
+      -----------------------------------------
+      -- Replace_Current_Instance_References --
+      -----------------------------------------
 
-      function Process_RE (N : Node_Id) return Traverse_Result is
-      begin
-         if Nkind (N) = N_Raise_Expression then
-            Set_Convert_To_Return_False (N);
-            return Skip;
-         else
-            return OK;
-         end if;
-      end Process_RE;
+      procedure Replace_Current_Instance_References
+         (N : Node_Id; Typ, New_Entity : Entity_Id)
+      is
+         Root : Node_Id renames N;
 
-      -------------
-      -- Test_RE --
-      -------------
+         procedure Replace_One_Reference (N : Node_Id);
+         --  Actual parameter for Replace_Type_References_Generic instance
 
-      function Test_RE (N : Node_Id) return Traverse_Result is
+         ---------------------------
+         -- Replace_One_Reference --
+         ---------------------------
+
+         procedure Replace_One_Reference (N : Node_Id) is
+            pragma Assert (In_Subtree (N, Root => Root));
+         begin
+            Rewrite (N, New_Occurrence_Of (New_Entity, Sloc (N)));
+            --  Use the Sloc of the usage name, not the defining name
+         end Replace_One_Reference;
+
+         procedure Replace_Type_References is
+           new Replace_Type_References_Generic (Replace_One_Reference);
       begin
-         if Nkind (N) = N_Raise_Expression then
-            Raise_Expression_Present := True;
-            return Abandon;
-         else
-            return OK;
-         end if;
-      end Test_RE;
+         Replace_Type_References (N, Typ);
+      end Replace_Current_Instance_References;
 
       --  Local variables
 
@@ -10337,7 +10322,7 @@ package body Sem_Ch13 is
       Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
       --  Save the Ghost-related attributes to restore on exit
 
-   --  Start of processing for Build_Predicate_Functions
+   --  Start of processing for Build_Predicate_Function
 
    begin
       --  Return if already built, if type does not have predicates,
@@ -10399,8 +10384,7 @@ package body Sem_Ch13 is
          Defining_Identifier
            (First (Parameter_Specifications (Specification (FDecl))));
 
-      Object_Name     := Chars (Object_Entity);
-      Object_Entity_M := Make_Defining_Identifier (Loc, Chars => Object_Name);
+      Object_Name   := Chars (Object_Entity);
 
       --  Add predicates for ancestor if present. These must come before the
       --  ones for the current type, as required by AI12-0071-1.
@@ -10432,25 +10416,6 @@ package body Sem_Ch13 is
 
       if Present (Expr) then
 
-         --  Test for raise expression present
-
-         Test_REs (Expr);
-
-         --  If raise expression is present, capture a copy of Expr for use
-         --  in building the predicateM function version later on. For this
-         --  copy we replace references to Object_Entity by Object_Entity_M.
-
-         if Raise_Expression_Present then
-            declare
-               Map : constant Elist_Id := New_Elmt_List;
-
-            begin
-               Append_Elmt (Object_Entity, Map);
-               Append_Elmt (Object_Entity_M, Map);
-               Expr_M := New_Copy_Tree (Expr, Map => Map);
-            end;
-         end if;
-
          --  Build the main predicate function
 
          declare
@@ -10468,27 +10433,179 @@ package body Sem_Ch13 is
 
             --  Build function body
 
-            Spec :=
-              Make_Function_Specification (Loc,
-                Defining_Unit_Name       => SIdB,
-                Parameter_Specifications => New_List (
-                  Make_Parameter_Specification (Loc,
-                    Defining_Identifier =>
-                      Make_Defining_Identifier (Loc, Object_Name),
-                    Parameter_Type =>
-                      New_Occurrence_Of (Typ, Loc))),
-                Result_Definition        =>
-                  New_Occurrence_Of (Standard_Boolean, Loc));
-
-            FBody :=
-              Make_Subprogram_Body (Loc,
-                Specification              => Spec,
-                Declarations               => Empty_List,
-                Handled_Statement_Sequence =>
-                  Make_Handled_Sequence_Of_Statements (Loc,
-                    Statements => New_List (
-                      Make_Simple_Return_Statement (Loc,
-                        Expression => Expr))));
+            declare
+               Param_Specs : constant List_Id := New_List (
+                 Make_Parameter_Specification (Loc,
+                   Defining_Identifier =>
+                     Make_Defining_Identifier (Loc, Object_Name),
+                   Parameter_Type =>
+                     New_Occurrence_Of (Typ, Loc)));
+            begin
+               --  if Spec has 2 parameters, then body should too
+               if Present (Next_Entity (Object_Entity)) then
+                  Append (Make_Parameter_Specification (Loc,
+                            Defining_Identifier =>
+                              Make_Defining_Identifier
+                                (Loc, Chars (Next_Entity (Object_Entity))),
+                            Parameter_Type      =>
+                              New_Occurrence_Of (Standard_Boolean, Loc)),
+                          Param_Specs);
+               end if;
+
+               Spec :=
+                 Make_Function_Specification (Loc,
+                   Defining_Unit_Name       => SIdB,
+                   Parameter_Specifications => Param_Specs,
+                   Result_Definition        =>
+                     New_Occurrence_Of (Standard_Boolean, Loc));
+            end;
+
+            --  The Predicate_Expression attribute is used by SPARK.
+            --
+            --  If Ancestor_Predicate_Function_Called is True, then
+            --  we try to exclude that call to the ancestor's
+            --  predicate function by calling Right_Opnd.
+            --  The call is not excluded in the case where
+            --  it is not "and"ed with anything else (so we don't have
+            --  an N_And_Then node). This exclusion is required if the
+            --  Predicate_Failure aspect is specified for Typ because
+            --  in that case we are going to drop the N_And_Then node
+            --  on the floor. Otherwise, it is a question of what is
+            --  most convenient for SPARK.
+
+            Set_Predicate_Expression
+              (SId, (if Ancestor_Predicate_Function_Called
+                       and then Nkind (Expr) = N_And_Then
+                     then Right_Opnd (Expr)
+                     else Expr));
+
+            declare
+               Result_Expr   : Node_Id := Expr;
+               PF_Expr       : Node_Id := Predicate_Failure_Expression
+                                            (Typ, Inherited_OK => False);
+               PF_Expr_Copy  : Node_Id;
+               Second_Formal : constant Entity_Id :=
+                 Next_Entity (Object_Entity);
+            begin
+               if Present (PF_Expr) then
+                  pragma Assert (Present (Second_Formal));
+
+                  --  This is an ugly hack to cope with an ugly situation.
+                  --  PF_Expr may have children whose Parent attribute
+                  --  does not point back to PF_Expr. If we pass such a
+                  --  tree to New_Copy_Tree, then it does not make a deep
+                  --  copy. But we need a deep copy. So we need to find a
+                  --  tree for which New_Copy_Tree *will* make a deep copy.
+
+                  declare
+                     function Check_Node_Parent (Parent_Node, Node : Node_Id)
+                       return Traverse_Result;
+                     function Check_Node_Parent (Parent_Node, Node : Node_Id)
+                       return Traverse_Result is
+                     begin
+                        if Parent_Node = PF_Expr
+                          and then not Is_List_Member (Node)
+                        then
+                           pragma Assert
+                             (Nkind (PF_Expr) = Nkind (Parent (Node)));
+
+                           --  We need PF_Expr to be a node for which
+                           --  New_Copy_Tree will make a deep copy.
+                           PF_Expr := Parent (Node);
+                           return Abandon;
+                        end if;
+                        return OK;
+                     end Check_Node_Parent;
+                     procedure Check_Parentage is
+                       new Traverse_Proc_With_Parent (Check_Node_Parent);
+                  begin
+                     Check_Parentage (PF_Expr);
+                     PF_Expr_Copy := New_Copy_Tree (PF_Expr);
+                  end;
+
+                  --  Current instance uses need to have their Entity
+                  --  fields set so that Replace_Current_Instance_References
+                  --  can find them. So we preanalyze. Just for purposes of
+                  --  calls to Is_Current_Instance during this preanalysis,
+                  --  we set the Parent field.
+                  Set_Parent (PF_Expr_Copy, Parent (PF_Expr));
+                  Preanalyze (PF_Expr_Copy);
+                  Set_Parent (PF_Expr_Copy, Empty);
+
+                  Replace_Current_Instance_References
+                    (PF_Expr_Copy, Typ => Typ, New_Entity => Object_Entity);
+
+                  if Ancestor_Predicate_Function_Called then
+                     --  If the call to an ancestor predicate function
+                     --  returns False, we do not want to raise an
+                     --  exception here. Our Predicate_Failure aspect does
+                     --  not apply in that case. So we have to build a
+                     --  more complicated result expression:
+                     --   (if not Ancestor_Predicate_Function (...) then False
+                     --    elsif Noninherited_Predicates (...) then True
+                     --    elsif Is_Membership_Test then False
+                     --    else (raise Assertion_Error with PF text))
+
+                     declare
+                        Ancestor_Call : constant Node_Id :=
+                          Left_Opnd (Result_Expr);
+                        Local_Preds   : constant Node_Id :=
+                          Right_Opnd (Result_Expr);
+                     begin
+                        Result_Expr :=
+                          Make_If_Expression (Loc,
+                            Expressions => New_List (
+                              Make_Op_Not (Loc, Ancestor_Call),
+                              New_Occurrence_Of (Standard_False, Loc),
+                              Make_If_Expression (Loc,
+                                Is_Elsif => True,
+                                Expressions => New_List (
+                                  Local_Preds,
+                                  New_Occurrence_Of (Standard_True, Loc),
+                                  Make_If_Expression (Loc,
+                                    Is_Elsif => True,
+                                    Expressions => New_List (
+                                      New_Occurrence_Of (Second_Formal, Loc),
+                                      New_Occurrence_Of (Standard_False, Loc),
+                                      Make_Raise_Expression (Loc,
+                                        New_Occurrence_Of (RTE
+                                          (RE_Assert_Failure), Loc),
+                                        PF_Expr_Copy)))))));
+                     end;
+
+                  else
+                     --  Build a conditional expression:
+                     --   (if <predicate evaluates to True> then True
+                     --    elsif Is_Membership_Test then False
+                     --    else (raise Assertion_Error with PF text))
+
+                     Result_Expr :=
+                       Make_If_Expression (Loc,
+                         Expressions => New_List (
+                           Result_Expr,
+                           New_Occurrence_Of (Standard_True, Loc),
+                           Make_If_Expression (Loc,
+                             Is_Elsif => True,
+                             Expressions => New_List (
+                               New_Occurrence_Of (Second_Formal, Loc),
+                               New_Occurrence_Of (Standard_False, Loc),
+                               Make_Raise_Expression (Loc,
+                                 New_Occurrence_Of (RTE
+                                   (RE_Assert_Failure), Loc),
+                                 PF_Expr_Copy)))));
+                  end if;
+               end if;
+
+               FBody :=
+                 Make_Subprogram_Body (Loc,
+                   Specification              => Spec,
+                   Declarations               => Empty_List,
+                   Handled_Statement_Sequence =>
+                     Make_Handled_Sequence_Of_Statements (Loc,
+                       Statements => New_List (
+                         Make_Simple_Return_Statement (Loc,
+                           Expression => Result_Expr))));
+            end;
 
             --  The declaration has been analyzed when created, and placed
             --  after type declaration. Insert body itself after freeze node,
@@ -10559,121 +10676,6 @@ package body Sem_Ch13 is
             end if;
          end;
 
-         --  Test for raise expressions present and if so build M version
-
-         if Raise_Expression_Present then
-            declare
-               SId : constant Entity_Id :=
-                 Make_Defining_Identifier (Loc,
-                   Chars => New_External_Name (Chars (Typ), "PredicateM"));
-               --  The entity for the function spec
-
-               SIdB : constant Entity_Id :=
-                 Make_Defining_Identifier (Loc,
-                   Chars => New_External_Name (Chars (Typ), "PredicateM"));
-               --  The entity for the function body
-
-               Spec  : Node_Id;
-               FBody : Node_Id;
-               FDecl : Node_Id;
-               BTemp : Entity_Id;
-
-               CRec_Typ : Entity_Id;
-               --  The corresponding record type of Full_Typ
-
-               Full_Typ : Entity_Id;
-               --  The full view of Typ
-
-               Priv_Typ : Entity_Id;
-               --  The partial view of Typ
-
-               UFull_Typ : Entity_Id;
-               --  The underlying full view of Full_Typ
-
-            begin
-               --  Mark any raise expressions for special expansion
-
-               Process_REs (Expr_M);
-
-               --  Build function declaration
-
-               Mutate_Ekind (SId, E_Function);
-               Set_Is_Predicate_Function_M (SId);
-               Set_Predicate_Function_M (Typ, SId);
-
-               --  Obtain all views of the input type
-
-               Get_Views (Typ, Priv_Typ, Full_Typ, UFull_Typ, CRec_Typ);
-
-               --  Associate the predicate function with all views
-
-               Propagate_Predicate_Attributes (Priv_Typ,  From_Typ => Typ);
-               Propagate_Predicate_Attributes (Full_Typ,  From_Typ => Typ);
-               Propagate_Predicate_Attributes (UFull_Typ, From_Typ => Typ);
-               Propagate_Predicate_Attributes (CRec_Typ,  From_Typ => Typ);
-
-               Spec :=
-                 Make_Function_Specification (Loc,
-                   Defining_Unit_Name       => SId,
-                   Parameter_Specifications => New_List (
-                     Make_Parameter_Specification (Loc,
-                       Defining_Identifier => Object_Entity_M,
-                       Parameter_Type      => New_Occurrence_Of (Typ, Loc))),
-                   Result_Definition        =>
-                     New_Occurrence_Of (Standard_Boolean, Loc));
-
-               FDecl :=
-                 Make_Subprogram_Declaration (Loc,
-                   Specification => Spec);
-
-               --  Build function body
-
-               Spec :=
-                 Make_Function_Specification (Loc,
-                   Defining_Unit_Name       => SIdB,
-                   Parameter_Specifications => New_List (
-                     Make_Parameter_Specification (Loc,
-                       Defining_Identifier =>
-                         Make_Defining_Identifier (Loc, Object_Name),
-                       Parameter_Type =>
-                         New_Occurrence_Of (Typ, Loc))),
-                   Result_Definition        =>
-                     New_Occurrence_Of (Standard_Boolean, Loc));
-
-               --  Build the body, we declare the boolean expression before
-               --  doing the return, because we are not really confident of
-               --  what happens if a return appears within a return.
-
-               BTemp :=
-                 Make_Temporary (Loc, 'B');
-
-               FBody :=
-                 Make_Subprogram_Body (Loc,
-                   Specification              => Spec,
-
-                   Declarations               => New_List (
-                     Make_Object_Declaration (Loc,
-                       Defining_Identifier => BTemp,
-                       Constant_Present    => True,
-                         Object_Definition =>
-                           New_Occurrence_Of (Standard_Boolean, Loc),
-                         Expression        => Expr_M)),
-
-                   Handled_Statement_Sequence =>
-                     Make_Handled_Sequence_Of_Statements (Loc,
-                       Statements => New_List (
-                         Make_Simple_Return_Statement (Loc,
-                           Expression => New_Occurrence_Of (BTemp, Loc)))));
-
-               --  Insert declaration before freeze node and body after
-
-               Insert_Before_And_Analyze (N, FDecl);
-               Insert_After_And_Analyze  (N, FBody);
-
-               --  Should quantified expressions be handled here as well ???
-            end;
-         end if;
-
          --  See if we have a static predicate. Note that the answer may be
          --  yes even if we have an explicit Dynamic_Predicate present.
 
@@ -10766,7 +10768,7 @@ package body Sem_Ch13 is
       end if;
 
       Restore_Ghost_Region (Saved_GM, Saved_IGR);
-   end Build_Predicate_Functions;
+   end Build_Predicate_Function;
 
    ------------------------------------------
    -- Build_Predicate_Function_Declaration --
@@ -10835,15 +10837,28 @@ package body Sem_Ch13 is
       Propagate_Predicate_Attributes (UFull_Typ, From_Typ => Typ);
       Propagate_Predicate_Attributes (CRec_Typ,  From_Typ => Typ);
 
-      Spec :=
-        Make_Function_Specification (Loc,
-          Defining_Unit_Name       => Func_Id,
-          Parameter_Specifications => New_List (
-            Make_Parameter_Specification (Loc,
-              Defining_Identifier => Make_Temporary (Loc, 'I'),
-              Parameter_Type      => New_Occurrence_Of (Typ, Loc))),
-          Result_Definition        =>
-            New_Occurrence_Of (Standard_Boolean, Loc));
+      declare
+         Param_Specs : constant List_Id := New_List (
+           Make_Parameter_Specification (Loc,
+             Defining_Identifier => Make_Temporary (Loc, 'I'),
+             Parameter_Type      => New_Occurrence_Of (Typ, Loc)));
+      begin
+         if Predicate_Function_Needs_Membership_Parameter (Typ) then
+            --  Add Boolean-valued For_Membership_Test param
+            Append (Make_Parameter_Specification (Loc,
+                      Defining_Identifier => Make_Temporary (Loc, 'M'),
+                      Parameter_Type      =>
+                        New_Occurrence_Of (Standard_Boolean, Loc)),
+                    Param_Specs);
+         end if;
+
+         Spec :=
+           Make_Function_Specification (Loc,
+             Defining_Unit_Name       => Func_Id,
+             Parameter_Specifications => Param_Specs,
+             Result_Definition        =>
+               New_Occurrence_Of (Standard_Boolean, Loc));
+      end;
 
       Func_Decl := Make_Subprogram_Declaration (Loc, Specification => Spec);
 
@@ -13107,7 +13122,7 @@ package body Sem_Ch13 is
             end if;
          end;
 
-         Build_Predicate_Functions (E, N);
+         Build_Predicate_Function (E, N);
       end if;
 
       --  If type has delayed aspects, this is where we do the preanalysis at
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index c306e2779a4..0a809154296 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -16892,6 +16892,8 @@ package body Sem_Util is
 
             elsif Nkind (P) = N_Aspect_Specification
               and then Nkind (Parent (P)) = N_Subtype_Declaration
+              and then Underlying_Type (Defining_Identifier (Parent (P))) =
+                       Underlying_Type (Typ)
             then
                return True;
 
@@ -16899,7 +16901,14 @@ package body Sem_Util is
               and then Get_Pragma_Id (P) in Pragma_Predicate
                                           | Pragma_Predicate_Failure
             then
-               return True;
+               declare
+                  Arg : constant Entity_Id :=
+                    Entity (Expression (Get_Argument (P)));
+               begin
+                  if Underlying_Type (Arg) = Underlying_Type (Typ) then
+                     return True;
+                  end if;
+               end;
             end if;
 
             P := Parent (P);
@@ -16933,7 +16942,6 @@ package body Sem_Util is
            and then Ekind (Scope (Entity (N))) in E_Function | E_Procedure
            and then
              (Is_Predicate_Function (Scope (Entity (N)))
-               or else Is_Predicate_Function_M (Scope (Entity (N)))
                or else Is_Invariant_Procedure (Scope (Entity (N)))
                or else Is_Partial_Invariant_Procedure (Scope (Entity (N)))
                or else Is_DIC_Procedure (Scope (Entity (N))));
@@ -26539,6 +26547,69 @@ package body Sem_Util is
         and then not Predicate_Checks_Suppressed (Empty);
    end Predicate_Enabled;
 
+   ----------------------------------
+   -- Predicate_Failure_Expression --
+   ----------------------------------
+
+   function Predicate_Failure_Expression
+    (Typ : Entity_Id; Inherited_OK : Boolean) return Node_Id
+   is
+      PF_Aspect : constant Node_Id :=
+        Find_Aspect (Typ, Aspect_Predicate_Failure);
+   begin
+      --  Check for Predicate_Failure aspect specification via an
+      --  aspect_specification (as opposed to via a pragma).
+
+      if Present (PF_Aspect) then
+         if Inherited_OK or else Entity (PF_Aspect) = Typ then
+            return Expression (PF_Aspect);
+         else
+            return Empty;
+         end if;
+      end if;
+
+      --  Check for Predicate_Failure aspect specification via a pragma.
+
+      declare
+         Rep_Item : Node_Id := First_Rep_Item (Typ);
+      begin
+         while Present (Rep_Item) loop
+            if Nkind (Rep_Item) = N_Pragma
+               and then Get_Pragma_Id (Rep_Item) = Pragma_Predicate_Failure
+            then
+               declare
+                  Arg1 : constant Node_Id :=
+                    Get_Pragma_Arg
+                      (First (Pragma_Argument_Associations (Rep_Item)));
+                  Arg2 : constant Node_Id :=
+                    Get_Pragma_Arg
+                      (Next (First (Pragma_Argument_Associations (Rep_Item))));
+               begin
+                  if Inherited_OK or else
+                     (Nkind (Arg1) in N_Has_Entity
+                      and then Entity (Arg1) = Typ)
+                  then
+                     return Arg2;
+                  end if;
+               end;
+            end if;
+
+            Next_Rep_Item (Rep_Item);
+         end loop;
+      end;
+
+      --  If we are interested in an inherited Predicate_Failure aspect
+      --  and we have an ancestor to inherit from, then recursively check
+      --  for that case.
+
+      if Inherited_OK and then Present (Nearest_Ancestor (Typ)) then
+         return Predicate_Failure_Expression (Nearest_Ancestor (Typ),
+                                              Inherited_OK => True);
+      end if;
+
+      return Empty;
+   end Predicate_Failure_Expression;
+
    ----------------------------------
    -- Predicate_Tests_On_Arguments --
    ----------------------------------
@@ -26574,9 +26645,7 @@ package body Sem_Util is
       --  would cause infinite recursion.
 
       elsif Ekind (Subp) = E_Function
-        and then (Is_Predicate_Function   (Subp)
-                    or else
-                  Is_Predicate_Function_M (Subp))
+        and then Is_Predicate_Function (Subp)
       then
          return False;
 
@@ -27029,9 +27098,7 @@ package body Sem_Util is
      (Typ      : Entity_Id;
       From_Typ : Entity_Id)
    is
-      Pred_Func   : Entity_Id;
-      Pred_Func_M : Entity_Id;
-
+      Pred_Func : Entity_Id;
    begin
       if Present (Typ) and then Present (From_Typ) then
          pragma Assert (Is_Type (Typ) and then Is_Type (From_Typ));
@@ -27044,7 +27111,6 @@ package body Sem_Util is
          end if;
 
          Pred_Func   := Predicate_Function (From_Typ);
-         Pred_Func_M := Predicate_Function_M (From_Typ);
 
          --  The setting of the attributes is intentionally conservative. This
          --  prevents accidental clobbering of enabled attributes.
@@ -27056,10 +27122,6 @@ package body Sem_Util is
          if Present (Pred_Func) and then No (Predicate_Function (Typ)) then
             Set_Predicate_Function (Typ, Pred_Func);
          end if;
-
-         if Present (Pred_Func_M) and then No (Predicate_Function_M (Typ)) then
-            Set_Predicate_Function_M (Typ, Pred_Func_M);
-         end if;
       end if;
    end Propagate_Predicate_Attributes;
 
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 1eca815c9d6..7038f1188ba 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -2930,6 +2930,26 @@ package Sem_Util is
    --  Typ, taking into account Predicates_Ignored and
    --  Predicate_Checks_Suppressed.
 
+   function Predicate_Failure_Expression
+    (Typ : Entity_Id; Inherited_OK : Boolean) return Node_Id;
+   --  If the given type or subtype is subject to a Predicate_Failure
+   --  aspect specification, then returns the specified expression.
+   --  Otherwise, if Inherited_OK is False then returns Empty.
+   --  Otherwise, if Typ denotes a subtype or a derived type then
+   --  returns the result of recursing on the ancestor subtype.
+   --  Otherwise, returns Empty.
+
+   function Predicate_Function_Needs_Membership_Parameter (Typ : Entity_Id)
+     return Boolean is
+     (Present (Predicate_Failure_Expression (Typ, Inherited_OK => True)));
+   --  The predicate function for some, but not all, subtypes needs to
+   --  know whether the predicate is being evaluated as part of a membership
+   --  test. The predicate function for such a subtype takes an additional
+   --  boolean to convey this information. This function returns True if this
+   --  additional parameter is needed. More specifically, this function
+   --  returns true if the Predicate_Failure aspect is specified for the
+   --  given subtype or for any of its "ancestor" subtypes.
+
    function Predicate_Tests_On_Arguments (Subp : Entity_Id) return Boolean;
    --  Subp is the entity for a subprogram call. This function returns True if
    --  predicate tests are required for the arguments in this call (this is the


^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2022-05-19 14:07 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-19 14:07 [gcc r13-648] [Ada] Fix bug in handling of Predicate_Failure aspect Pierre-Marie de Rodat

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).