diff mbox series

[COMMITTED] ada: Mark attribute Initialized as ghost code

Message ID 20230613073802.239593-1-poulhies@adacore.com
State Accepted
Headers
Series [COMMITTED] ada: Mark attribute Initialized as ghost code |

Checks

Context Check Description
snail/gcc-patch-check success Github commit url

Commit Message

Marc Poulhiès June 13, 2023, 7:38 a.m. UTC 
  From: Yannick Moy <moy@adacore.com>

Implement the SPARK RM change that defines attribute Initialized
as being ghost, i.e. only allowed where a ghost entity would be allowed.

gcc/ada/

	* ghost.adb (Check_Ghost_Context): Allow absence of Ghost_Id
	for attribute. Update error message to mention Ghost_Predicate.
	(Is_Ghost_Attribute_Reference): New query.
	* ghost.ads (Is_Ghost_Attribute_Reference): New query.
	* sem_attr.adb (Resolve_Attribute): Check ghost context for ghost
	attributes.

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

---
 gcc/ada/ghost.adb    | 15 ++++++++++++++-
 gcc/ada/ghost.ads    |  4 ++++
 gcc/ada/sem_attr.adb |  7 +++++++
 3 files changed, 25 insertions(+), 1 deletion(-)
diff mbox series

Patch

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index ee98126de81..6cf87ce29b1 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -655,7 +655,9 @@  package body Ghost is
       --  declaration and at the point of use match.
 
       if Is_OK_Ghost_Context (Ghost_Ref) then
-         Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
+         if Present (Ghost_Id) then
+            Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
+         end if;
 
       --  Otherwise the Ghost entity appears in a non-Ghost context and affects
       --  its behavior or value (SPARK RM 6.9(10,11)).
@@ -673,6 +675,7 @@  package body Ghost is
                Ghost_Ref);
             Error_Msg_N
               ("\either make the type ghost "
+               & "or use a Ghost_Predicate "
                & "or use a type invariant on a private type", Ghost_Ref);
          end if;
       end if;
@@ -1194,6 +1197,16 @@  package body Ghost is
       return False;
    end Is_Ghost_Assignment;
 
+   ----------------------------------
+   -- Is_Ghost_Attribute_Reference --
+   ----------------------------------
+
+   function Is_Ghost_Attribute_Reference (N : Node_Id) return Boolean is
+   begin
+      return Nkind (N) = N_Attribute_Reference
+        and then Attribute_Name (N) = Name_Initialized;
+   end Is_Ghost_Attribute_Reference;
+
    --------------------------
    -- Is_Ghost_Declaration --
    --------------------------
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index 1532117955e..663e70cffe2 100644
--- a/gcc/ada/ghost.ads
+++ b/gcc/ada/ghost.ads
@@ -111,6 +111,10 @@  package Ghost is
    --  Determine whether arbitrary node N denotes an assignment statement whose
    --  target is a Ghost entity.
 
+   function Is_Ghost_Attribute_Reference (N : Node_Id) return Boolean;
+   --  Determine whether arbitrary node N denotes an attribute reference which
+   --  denotes a Ghost attribute.
+
    function Is_Ghost_Declaration (N : Node_Id) return Boolean;
    --  Determine whether arbitrary node N denotes a declaration which defines
    --  a Ghost entity.
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index f5ee275e23f..24f57ac43ff 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -41,6 +41,7 @@  with Exp_Dist;       use Exp_Dist;
 with Exp_Util;       use Exp_Util;
 with Expander;       use Expander;
 with Freeze;         use Freeze;
+with Ghost;          use Ghost;
 with Gnatvsn;        use Gnatvsn;
 with Itypes;         use Itypes;
 with Lib;            use Lib;
@@ -11068,6 +11069,12 @@  package body Sem_Attr is
          Set_Etype (N, Typ);
       end if;
 
+      --  A Ghost attribute must appear in a specific context
+
+      if Is_Ghost_Attribute_Reference (N) then
+         Check_Ghost_Context (Empty, N);
+      end if;
+
       --  Remaining processing depends on attribute
 
       case Attr_Id is