https://gcc.gnu.org/g:5af32cd1f251021cd4dba9a8e300dbc4e937978e
commit r17-799-g5af32cd1f251021cd4dba9a8e300dbc4e937978e Author: Viljar Indus <[email protected]> Date: Fri Feb 13 12:24:15 2026 +0200 ada: Fix SPARK RM 6.9 Rule 32 check Ensure that the ghost equality check is only applied to user defined equality operations. gcc/ada/ChangeLog: * ghost.adb (Check_Ghost_Equality_Op): Supply the type of the operation as an argument. * ghost.ads (Check_Ghost_Equality_Op): Likewise. * sem_ch6.adb (Valid_Operator_Definition): Remove call to Check_Ghost_Equality_Op. (Check_For_Primitive_Subprogram): Call Check_Ghost_Equality_Op. Diff: --- gcc/ada/ghost.adb | 46 ++++++++++++++++++---------------------------- gcc/ada/ghost.ads | 2 +- gcc/ada/sem_ch6.adb | 10 ++++++---- 3 files changed, 25 insertions(+), 33 deletions(-) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index ce9e80e09abf..a87d044524bb 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -1071,44 +1071,34 @@ package body Ghost is -- Check_Ghost_Equality_Op -- ----------------------------- - procedure Check_Ghost_Equality_Op (Eq_Op : Entity_Id) is - F : Entity_Id; - F_Typ : Entity_Id; + procedure Check_Ghost_Equality_Op (Eq_Op : Entity_Id; Typ : Entity_Id) is 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); + if not Is_Record_Type (Typ) or else Is_Limited_Record (Typ) then + return; + end if; - Error_Msg_N ("\equality operation is defined as ghost", Eq_Op); + if not Is_Ghost_Entity (Typ) then + Error_Msg_N ("incompatible primitive equaility operation", 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_N ("\equality operation is defined as ghost", Eq_Op); - Error_Msg_Name_1 := Chars (Ghost_Assertion_Level (Eq_Op)); - Error_Msg_N ("\equality operator declared with %", Eq_Op); + Error_Msg_Sloc := Sloc (Typ); + Error_Msg_N ("\but applied to a non-ghost record type #", Eq_Op); + elsif Ghost_Assertion_Level (Eq_Op) /= Ghost_Assertion_Level (Typ) then + Error_Msg_N (Assertion_Level_Error_Msg, 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; + Error_Msg_Name_1 := Chars (Ghost_Assertion_Level (Eq_Op)); + Error_Msg_N ("\equality operator declared with %", Eq_Op); - Next_Formal (F); - end loop; + Error_Msg_Name_1 := Chars (Ghost_Assertion_Level (Typ)); + Error_Msg_Sloc := Sloc (Typ); + Error_Msg_NE ("\record type & declared # with %", Eq_Op, Typ); + Error_Msg_N ("\& should have the same assertion level", Eq_Op); + end if; end Check_Ghost_Equality_Op; --------------------------------------------- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 7c4ef60dc2c2..8c58eeecf3c2 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -61,7 +61,7 @@ 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); + procedure Check_Ghost_Equality_Op (Eq_Op : Entity_Id; Typ : 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)) diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index f3395e1f62ab..ab85fd7af07c 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -12000,6 +12000,12 @@ package body Sem_Ch6 is -- (SPARK RM 6.9(21)). Check_Ghost_Primitive (S, B_Typ); + + -- 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)) + + Check_Ghost_Equality_Op (S, B_Typ); end if; end if; end Check_For_Primitive_Subprogram; @@ -14459,10 +14465,6 @@ 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)
