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 --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index abf1c4993227ea65e64694b0b5b3b483c6bdcd7d..dc5ea1efe8a2ebe685576ece3c5368b550817eea 100644 (file)
--- 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 006dd0c4fbd85e00784f7d363576937422cb7d8b..7c4ef60dc2c253b2fa446db28b2368858cfe0e16 100644 (file)
--- 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 163d666ce104b05a1b8cec0b97a5e34f2d7d5ea0..f3395e1f62ab51a310726f0d2e3d68fa76e4b55b 100644 (file)
--- 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)