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 --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index ce9e80e09abfe72433a727c85cc0d9ee64498212..a87d044524bb041f04d067eea6b94ba6976c30b5 100644 (file)
--- 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 7c4ef60dc2c253b2fa446db28b2368858cfe0e16..8c58eeecf3c2c6ed06b0816e36bf79723a5316c4 100644 (file)
--- 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 f3395e1f62ab51a310726f0d2e3d68fa76e4b55b..ab85fd7af07cf2b350504506c19122e4e113f22b 100644 (file)
--- 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)