https://gcc.gnu.org/g:d256dc768066fabd41a672bbedf303d64d606436
commit r17-793-gd256dc768066fabd41a672bbedf303d64d606436 Author: Viljar Indus <[email protected]> Date: Tue Feb 10 12:04:31 2026 +0200 ada: Implement SPARK RM 6.9 (23) Implement the rule 23 for ghost code: A user-defined primitive equality operation on a non-ghost record type shall not be ghost, unless the record type has only limited views. In addition, a user-defined primitive equality operation on a ghost record type shall have a matching assertion level. gcc/ada/ChangeLog: * ghost.adb (Check_Ghost_Equality_Op): New function for the implementation of the rule. * ghost.ads (Check_Ghost_Equality_Op): Likewise. * sem_ch6.adb (Valid_Operator_Definition): Add check for rule 23. Diff: --- gcc/ada/ghost.adb | 44 ++++++++++++++++++++++++++++++++++++++++++++ gcc/ada/ghost.ads | 5 +++++ gcc/ada/sem_ch6.adb | 4 ++++ 3 files changed, 53 insertions(+) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index abf1c4993227..dc5ea1efe8a2 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -1118,6 +1118,50 @@ package body Ghost is Check_Valid_Assertion_Level (Id, N); end Check_Valid_Ghost_Declaration; + ----------------------------- + -- Check_Ghost_Equality_Op -- + ----------------------------- + + procedure Check_Ghost_Equality_Op (Eq_Op : Entity_Id) is + F : Entity_Id; + F_Typ : Entity_Id; + begin + if not Is_Ghost_Entity (Eq_Op) then + return; + end if; + + F := First_Formal (Eq_Op); + while Present (F) loop + F_Typ := Etype (F); + if Is_Record_Type (F_Typ) and then not Is_Limited_Record (F_Typ) then + if not Is_Ghost_Entity (F_Typ) then + Error_Msg_N + ("incompatible primitive equaility operation", Eq_Op); + + Error_Msg_N ("\equality operation is defined as ghost", Eq_Op); + + Error_Msg_Sloc := Sloc (F_Typ); + Error_Msg_N + ("\but applied to a non-ghost record type #", Eq_Op); + elsif Ghost_Assertion_Level (Eq_Op) + /= Ghost_Assertion_Level (F_Typ) + then + Error_Msg_N (Assertion_Level_Error_Msg, Eq_Op); + + Error_Msg_Name_1 := Chars (Ghost_Assertion_Level (Eq_Op)); + Error_Msg_N ("\equality operator declared with %", Eq_Op); + + Error_Msg_Name_1 := Chars (Ghost_Assertion_Level (F_Typ)); + Error_Msg_Sloc := Sloc (F_Typ); + Error_Msg_NE ("\record type & declared # with %", Eq_Op, F_Typ); + Error_Msg_N ("\& should have the same assertion level", Eq_Op); + end if; + end if; + + Next_Formal (F); + end loop; + end Check_Ghost_Equality_Op; + --------------------------------------------- -- Check_Ghost_Formal_Procedure_Or_Package -- --------------------------------------------- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 006dd0c4fbd8..7c4ef60dc2c2 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -61,6 +61,11 @@ package Ghost is -- Check that if Actual contains references to ghost entities, generic -- formal parameter Formal is ghost (SPARK RM 6.9(13)). + procedure Check_Ghost_Equality_Op (Eq_Op : Entity_Id); + -- A user-defined primitive equality operation on a + -- non-ghost record type shall not be ghost, unless the + -- record type has only limited views. (SPARK RM 6.9(23)) + procedure Check_Ghost_Formal_Procedure_Or_Package (N : Node_Id; Actual : Entity_Id; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 163d666ce104..f3395e1f62ab 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -14459,6 +14459,10 @@ package body Sem_Ch6 is ("incorrect number of arguments for operator", Designator); end if; + if Id = Name_Op_Eq then + Check_Ghost_Equality_Op (Designator); + end if; + if Id = Name_Op_Ne and then Base_Type (Etype (Designator)) = Standard_Boolean and then not Is_Intrinsic_Subprogram (Designator)
