* [COMMITTED] ada: Mark attribute Initialized as ghost code
@ 2023-06-13 7:38 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-06-13 7:38 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
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 --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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-06-13 7:38 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-06-13 7:38 [COMMITTED] ada: Mark attribute Initialized as ghost code Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).