https://gcc.gnu.org/g:97298de9fbdd71885d2117a240c04784584295e7
commit r17-1180-g97298de9fbdd71885d2117a240c04784584295e7 Author: Viljar Indus <[email protected]> Date: Wed Apr 1 10:36:46 2026 +0300 ada: Fix SPARK RM 6.9(23) check for limited private types The Check_Ghost_Equality_Op predicate was checking the type directly instead of its underlying type, so a limited private type whose full view is a non-limited record was incorrectly bypassing the check. Additionally, the check was never deferred to Process_Full_View, so equality operators declared in the visible part of a package were not re-checked once the full view became available. gcc/ada/ChangeLog: * ghost.adb (Check_Ghost_Equality_Op): Use Underlying_Type to look through the private view before checking Is_Record_Type and Is_Limited_Record. * sem_ch3.adb (Process_Full_View): After completing the full view, re-check any primitive equality operators on the private type against SPARK RM 6.9(23) via Check_Ghost_Equality_Op. Diff: --- gcc/ada/ghost.adb | 10 +++++++++- gcc/ada/sem_ch3.adb | 21 +++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index a87d044524bb..afa6b97947f4 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -1072,12 +1072,20 @@ package body Ghost is ----------------------------- procedure Check_Ghost_Equality_Op (Eq_Op : Entity_Id; Typ : Entity_Id) is + Underlying : constant Entity_Id := Underlying_Type (Typ); begin if not Is_Ghost_Entity (Eq_Op) then return; end if; - if not Is_Record_Type (Typ) or else Is_Limited_Record (Typ) then + -- Look through any private view to get the underlying record type, + -- since a limited private type whose full view is a non-limited record + -- does not have "only limited views" and must be checked. + + if No (Underlying) + or else not Is_Record_Type (Underlying) + or else Is_Limited_Record (Underlying) + then return; end if; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 99799431d87e..bc02601fe0c0 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -22515,6 +22515,27 @@ package body Sem_Ch3 is (Underlying_Full_View (Full_T), Priv_T); end if; + -- Now that the full view is known, check any primitive equality + -- operators declared in the visible part against SPARK RM 6.9(23). + -- This check is deferred from Check_For_Primitive_Subprogram because + -- the full view of a private type is not available when the operator + -- is declared in the visible part of the package. + + if Has_Primitive_Operations (Priv_T) then + declare + Prim : Elmt_Id := First_Elmt (Primitive_Operations (Priv_T)); + Op : Entity_Id; + begin + while Present (Prim) loop + Op := Node (Prim); + if Chars (Op) = Name_Op_Eq then + Check_Ghost_Equality_Op (Op, Priv_T); + end if; + Next_Elmt (Prim); + end loop; + end; + end if; + <<Leave>> Restore_Ghost_Region (Saved_Ghost_Config); end Process_Full_View;
