]> git.ipfire.org Git - thirdparty/gcc.git/commit
ada: Fix SPARK test failures caused by new handling of inherited class-wide pre/post
authorGary Dismukes <dismukes@adacore.com>
Fri, 7 Mar 2025 19:35:25 +0000 (19:35 +0000)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Mon, 9 Jun 2025 06:32:10 +0000 (08:32 +0200)
commitbb9cd860cb1ff3d497e37764ffa035b4e4e2165d
tree1c2065b67557266acac03ae4af44cb748127a9c3
parent0ab32e590fa97e7dc54e171f1a7b5f9b7069c309
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.
gcc/ada/exp_util.adb