https://gcc.gnu.org/g:bb9cd860cb1ff3d497e37764ffa035b4e4e2165d
commit r16-1330-gbb9cd860cb1ff3d497e37764ffa035b4e4e2165d
Author: Gary Dismukes <dismu...@adacore.com>
Date: Fri Mar 7 19:35:25 2025 +0000
ada: Fix SPARK test failures caused by new handling of inherited class-wide
pre/post
The revised handling of inherited class-wide pre/postconditions (for
properly implementing the rules of RM 6.1.1(7/5)) broke two SPARK tests
(N709-001__contracts and V516-041__private_ownership). This change fixes
that, by refining the test for detecting formal parameters used as actuals
in calls to primitive functions, as well as adding handling for 'Result
attributes given as actuals in such calls.
gcc/ada/ChangeLog:
* exp_util.adb (Call_To_Parent_Dispatching_Op_Must_Be_Mapped):
Replace
test of Covers with test of Is_Controlling_Formal. Add handling for
'Result actuals. Remove Actual_Type and its uses.
Diff:
---
gcc/ada/exp_util.adb | 23 ++++++++++++++---------
1 file changed, 14 insertions(+), 9 deletions(-)
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index b76d387c5a5d..8ac1b9001a45 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1552,7 +1552,6 @@ package body Exp_Util is
pragma Assert (Nkind (Call_Node) = N_Function_Call);
Actual : Node_Id := First_Actual (Call_Node);
- Actual_Type : Entity_Id;
Actual_Or_Prefix : Node_Id;
begin
@@ -1579,11 +1578,11 @@ package body Exp_Util is
Actual_Or_Prefix := Actual;
end if;
- Actual_Type := Etype (Actual);
-
- if Is_Anonymous_Access_Type (Actual_Type) then
- Actual_Type := Designated_Type (Actual_Type);
- end if;
+ -- If at least one actual is a controlling formal
+ -- parameter of a class-wide Pre/Post aspect's
+ -- subprogram, the rule in RM 6.1.1(7) applies,
+ -- and we want to map the call to target the
+ -- corresponding function of the derived type.
if Nkind (Actual_Or_Prefix)
in N_Identifier
@@ -1592,11 +1591,17 @@ package body Exp_Util is
and then Is_Formal (Entity (Actual_Or_Prefix))
- and then Covers (Ctrl_Type, Actual_Type)
+ and then Is_Controlling_Formal
+ (Entity (Actual_Or_Prefix))
then
- -- At least one actual is a formal parameter of
- -- Par_Subp with type Ctrl_Type.
+ return True;
+ -- RM 6.1.1(7) also applies to Result attributes
+ -- of primitive functions with controlling results.
+
+ elsif Is_Attribute_Result (Actual)
+ and then Has_Controlling_Result (Subp)
+ then
return True;
end if;
