[COMMITTED 14/51] ada: Fix SPARK RM 6.9(23) check for limited private types

[Marc Poulhiès]

From: Viljar Indus <in...@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 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 a87d044524b..afa6b97947f 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 99799431d87..bc02601fe0c 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;
-- 
2.53.0