diff options
author | Yannick Moy <moy@adacore.com> | 2023-04-14 17:20:25 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-13 09:31:42 +0200 |
commit | 067d80d8d59c910a4f6373a23e9fa6904fbb748b (patch) | |
tree | 5c84a6364e69348ddc0da13218b4d999f8b76489 /gcc/ada/doc | |
parent | 230fef15abbbd37ae2ee339839f7b478d1ce2ab3 (diff) | |
download | gcc-067d80d8d59c910a4f6373a23e9fa6904fbb748b.zip gcc-067d80d8d59c910a4f6373a23e9fa6904fbb748b.tar.gz gcc-067d80d8d59c910a4f6373a23e9fa6904fbb748b.tar.bz2 |
ada: Support new GNAT-specific aspect Ghost_Predicate
New aspect Ghost_Predicate allows the use of ghost entities in the
predicate expression, even if the type is not ghost itself. As a result,
subtypes with a ghost predicate cannot be used in membership tests.
Subtypes with ghost predicates are subject to the same additional
restrictions as subtypes with aspect Dynamic_Predicate.
They are governed for compilation by assertion policy Ghost.
Checking of the predicate itself is governed by the usual assertion
policy (Static_Predicate/Dynamic_Predicate/Predicate) independently
of the ghost predicate.
gcc/ada/
* doc/gnat_rm/implementation_defined_aspects.rst: Document new
aspect.
* doc/gnat_rm/implementation_defined_pragmas.rst: Whitespace.
* aspects.adb (Init_Canonical_Aspect): Set it to Predicate.
* aspects.ads: Set global constants for new aspect.
* einfo.ads: Describe new flag related to new aspect.
* exp_ch6.adb (Can_Fold_Predicate_Call): Do not fold new aspect.
* exp_util.adb (Make_Predicate_Check): Add comment.
* gen_il-fields.ads: Add new flag.
* gen_il-gen-gen_entities.adb: Add new flag.
* ghost.adb (Is_OK_Ghost_Context): Ghost predicate is an OK
ghost context.
(Mark_Ghost_Pragma): Add overloading with ghost mode parameter.
* ghost.ads (Mark_Ghost_Pragma): Add overloading with ghpst mode
parameter.
(Name_To_Ghost_Mode): Make function public.
* sem_aggr.adb: Issue error for violation of valid use.
* sem_case.adb: Issue error for violation of valid use.
* sem_ch13.adb: Adapt for new aspect.
* sem_ch3.adb (Analyze_Full_Type_Declaration): Remove dead code
which was trying to propagate Has_Predicates flag in the wrong
direction (from derived to parent type).
(Analyze_Number_Declaration): Issue error for violation of valid
use.
(Build_Derived_Type): Cleanup inheritance of predicate flags from
parent to derived type.
(Build_Predicate_Function): Only add a predicate check when it
is not ignored as Ghost code.
* sem_ch4.adb (Analyze_Membership_Op): Issue an error for use of
a subtype with a ghost predicate as name in a membership test.
* sem_ch5.adb (Check_Predicate_Use): Issue error for violation of
valid use.
* sem_eval.adb: Adapt code for Dynamic_Predicate to account for
Ghost_Predicate too.
* sem_prag.adb (Analyze_Pragma): Make pragma ghost or not.
* sem_util.adb (Bad_Predicated_Subtype_Use): Adapt to new aspect.
(Inherit_Predicate_Flags): Add inheritance of flag. Add parameter
to apply to derived types.
* sem_util.ads (Inherit_Predicate_Flags): Change signature.
* snames.ads-tmpl: Add new aspect name.
* gnat_rm.texi: Regenerate.
Diffstat (limited to 'gcc/ada/doc')
-rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst | 10 | ||||
-rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst | 2 |
2 files changed, 11 insertions, 1 deletions
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst index 960c505..b37a158 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst @@ -255,6 +255,16 @@ Aspect Ghost This aspect is equivalent to :ref:`pragma Ghost<Pragma-Ghost>`. +Aspect Ghost_Predicate +====================== +.. index:: Ghost_Predicate + +This aspect introduces a subtype predicate that can reference ghost +entities. The subtype cannot appear as a subtype_mark in a membership test. + +For the detailed semantics of this aspect, see the entry for subtype predicates +in the SPARK Reference Manual, section 3.2.4. + Aspect Global ============= .. index:: Global diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst index a6c5600..35a3fe5 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst @@ -3530,7 +3530,7 @@ and the Ceiling_Locking locking policy is in effect, then the run-time actions associated with the Ceiling_Locking locking policy (described in Ada RM D.3) are not performed when a protected operation of the protected unit is executed. - + Pragma Loop_Invariant ===================== |