]> git.ipfire.org Git - thirdparty/gcc.git/commit
ada: Incorrect creation of corresponding expression of class-wide contracts
authorGary Dismukes <dismukes@adacore.com>
Fri, 28 Feb 2025 00:08:19 +0000 (00:08 +0000)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Mon, 9 Jun 2025 06:32:05 +0000 (08:32 +0200)
commit250392311d5bc6d167f87d4ad65c3e9df8981fba
tree4330abebe50142727fd15499074b2df12a77df21
parent5fba1c986d619908174bb27dd1478c80e2007818
ada: Incorrect creation of corresponding expression of class-wide contracts

GNAT was incorrectly implementing the Ada rules for resolving calls to
primitive functions within inherited class-wide pre- and postconditions,
as specified in RM22 6.1.1 (relating to AI12-0113).  Only function calls
that involve formals of the associated primitive subprogram should be
treated using the "(notional) formal derived type" rules.  In particular,
calls that are tag-indeterminate (for example, "F(G)") should not be mapped
to call the corresponding primitives of the derived type (they should still
call the primitives of the ancestor type).  The fix for this involves a new
predicate function that recursively traverses calls to determine the calls
that satisfy the criteria for mapping.  These changes also completely remove
the mapping of formals that was done in Contracts.Merge_Class_Conditions
(in Inherit_Condition), since the mapping will be done later anyway by
Build_Class_Wide_Expression, and the earlier mapping interferes with that.

Note: The utility function Sem_Util.Check_Parents is no longer called
after removal of the single call to it from contracts.adb, but it's being
retained (along with the generic subprograms in Atree that it depends on)
for possible use in VAST.

gcc/ada/ChangeLog:

* contracts.adb (Inherit_Condition): Remove Assoc_List and its uses
along with function Check_Condition, since mapping of formals will
effectively be done in Build_Class_Wide_Expression (by Replace_Entity).
* exp_util.adb (Replace_Entity): Only rewrite entity references in
function calls that qualify according to the result of calling the
new function Call_To_Parent_Dispatching_Op_Must_Be_Mapped.
(Call_To_Parent_Dispatching_Op_Must_Be_Mapped): New function that
determines whether a function call to a primitive of Par_Subp
associated tagged type needs to be mapped (according to whether
it has any actuals that reference controlling formals of the
primitive).
gcc/ada/contracts.adb
gcc/ada/exp_util.adb