| commit | 5c266974094ec997a0e83fc763fa4a6ff4b96005 | |
| author | Yannick Moy <moy@adacore.com> | |
| Tue, 11 Apr 2023 09:24:32 +0000 (11 11:24 +0200) | ||
| committer | Marc Poulhiès <poulhies@adacore.com> | |
| Tue, 13 Jun 2023 07:31:43 +0000 (13 09:31 +0200) | ||
| tree | df9bd143567d8fdb736bc5ca592561900a9b37ff | treesnapshot (tar.gz zip) |
| parent | 416bb154d5c36f25dd6f54fb0d81bf6b0132ee20 | commitdiff |
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.
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.
| gcc/ada/ghost.adb | diffblobblamehistory | |
| gcc/ada/ghost.ads | diffblobblamehistory | |
| gcc/ada/sem_attr.adb | diffblobblamehistory |