From: Yannick Moy <m...@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 --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
--
2.40.0
