diff mbox series

[COMMITTED,21/31] ada: Ignore ghost policy errors inside aspect Iterable

Message ID 20250911091904.1505690-21-poulhies@adacore.com
State Committed
Commit 354a1c35a20662215d282d20b0cdf68796debe7a
Headers
Series [COMMITTED,01/31] ada: Disable new warning for composite equality ops that can raise Program_Error |

Commit Message

Marc Poulhiès Sept. 11, 2025, 9:18 a.m. UTC 
  From: Viljar Indus <indus@adacore.com>

It is OK to define a checked ghost type with an iterable aspect
that has ignored Iterable functions.

gcc/ada/ChangeLog:

	* ghost.adb (Check_Ghost_Policy): Avoid triggering a ghost
	policy error if the policy is referenced within the Iterable
	aspect.

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

---
 gcc/ada/ghost.adb | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
diff mbox series

Patch

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 0fbcf20da7c1..0918d27daeb7 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -807,8 +807,28 @@  package body Ghost is
       ------------------------
 
       procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is
+         function Is_From_Aspect_Iterable (Ref : Node_Id) return Boolean;
+         --  Returns true when the node is contained within an Iterable aspect.
+
+         function Is_From_Aspect_Iterable (Ref : Node_Id) return Boolean is
+            P : Node_Id := Parent (Ref);
+         begin
+            while Present (P) loop
+               if Nkind (P) = N_Aspect_Specification then
+                  return Get_Aspect_Id (P) = Aspect_Iterable;
+               end if;
+               P := Parent (P);
+            end loop;
+            return False;
+         end Is_From_Aspect_Iterable;
+
+         --  Local variables
+
          Applic_Policy : Ghost_Mode_Type := Ghost_Config.Ghost_Mode;
          Ghost_Region  : constant Node_Id := Ghost_Config.Current_Region;
+
+      --  Start of processing for Check_Ghost_Policy
+
       begin
          --  The policy is allowed to change within renaming and instantiation
          --  statements.
@@ -844,6 +864,14 @@  package body Ghost is
             Error_Msg_NE ("\& used # with ghost policy `Ignore`",  Ref, Id);
          end if;
 
+         --  A ghost entity E shall not be referenced within an aspect
+         --  specification [(including an aspect-specifying pragma)] which
+         --  specifies an aspect of an entity that is either non-ghost or not
+         --  assertion-level-dependent on E except in the following cases the
+         --  specified aspect is either Global, Depends, Refined_Global,
+         --  Refined_Depends, Initializes, Refined_State, or Iterable (SPARK RM
+         --  6.9(15)).
+
          if No (Ghost_Region)
            or else (Nkind (Ghost_Region) = N_Pragma
                     and then Get_Pragma_Id (Ghost_Region)
@@ -853,6 +881,7 @@  package body Ghost is
                               | Pragma_Refined_Depends
                               | Pragma_Initializes
                               | Pragma_Refined_State)
+           or else Is_From_Aspect_Iterable (Ref)
          then
             return;
          end if;