Aspect Ghost_Predicate (GNAT Reference Manual) (original) (raw)

Next: Aspect Global, Previous: Aspect Ghost, Up: Implementation Defined Aspects [Contents][Index]

3.20 Aspect 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.