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/range-op-float.cc | |
| 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/range-op-float.cc')
0 files changed, 0 insertions, 0 deletions