diff options
| author | Yannick Moy <moy@adacore.com> | 2023-04-11 11:24:32 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-13 09:31:43 +0200 |
| commit | 5c266974094ec997a0e83fc763fa4a6ff4b96005 (patch) | |
| tree | df9bd143567d8fdb736bc5ca592561900a9b37ff /gcc/ada/ghost.ads | |
| parent | 416bb154d5c36f25dd6f54fb0d81bf6b0132ee20 (diff) | |
| download | gcc-5c266974094ec997a0e83fc763fa4a6ff4b96005.zip gcc-5c266974094ec997a0e83fc763fa4a6ff4b96005.tar.gz gcc-5c266974094ec997a0e83fc763fa4a6ff4b96005.tar.bz2 | |
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.
Diffstat (limited to 'gcc/ada/ghost.ads')
| -rw-r--r-- | gcc/ada/ghost.ads | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 1532117..663e70c 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. |