ada: Mark attribute Initialized as ghost code

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.

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index ee98126de81c2a133c203562b91121c483023e44..6cf87ce29b158f39704309a185a23fe4f9137932 100644 (file)
--- 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 1532117955e1186205029c154a7f7893724d1aa4..663e70cffe27f6f01bc772290181ba7f4fba6150 100644 (file)
--- 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 f5ee275e23f3ff31ffee921528eed1b2bad312ab..24f57ac43ff54708dd4fbffa4c0c959a1d32870c 100644 (file)
--- 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