| (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} )
EXTERNAL_PROPERTY ::=
- Async_Readers [=> boolean_EXPRESSION]
- | Async_Writers [=> boolean_EXPRESSION]
- | Effective_Reads [=> boolean_EXPRESSION]
- | Effective_Writes [=> boolean_EXPRESSION]
- others => boolean_EXPRESSION
+ Async_Readers [=> static_boolean_EXPRESSION]
+ | Async_Writers [=> static_boolean_EXPRESSION]
+ | Effective_Reads [=> static_boolean_EXPRESSION]
+ | Effective_Writes [=> static_boolean_EXPRESSION]
+ others => static_boolean_EXPRESSION
STATE_NAME ::= defining_identifier
.. code-block:: ada
- pragma Async_Readers [ (boolean_EXPRESSION) ];
+ pragma Async_Readers [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``Async_Readers`` in
the SPARK 2014 Reference Manual, section 7.1.2.
.. code-block:: ada
- pragma Async_Writers [ (boolean_EXPRESSION) ];
+ pragma Async_Writers [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``Async_Writers`` in
the SPARK 2014 Reference Manual, section 7.1.2.
.. code-block:: ada
- pragma Constant_After_Elaboration [ (boolean_EXPRESSION) ];
+ pragma Constant_After_Elaboration [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect
``Constant_After_Elaboration`` in the SPARK 2014 Reference Manual, section 3.3.1.
.. code-block:: ada
- pragma Effective_Reads [ (boolean_EXPRESSION) ];
+ pragma Effective_Reads [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``Effective_Reads`` in
the SPARK 2014 Reference Manual, section 7.1.2.
.. code-block:: ada
- pragma Effective_Writes [ (boolean_EXPRESSION) ];
+ pragma Effective_Writes [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``Effective_Writes``
in the SPARK 2014 Reference Manual, section 7.1.2.
.. code-block:: ada
- pragma Extensions_Visible [ (boolean_EXPRESSION) ];
+ pragma Extensions_Visible [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``Extensions_Visible``
in the SPARK 2014 Reference Manual, section 6.1.7.
.. code-block:: ada
- pragma Ghost [ (boolean_EXPRESSION) ];
+ pragma Ghost [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``Ghost`` in the SPARK
2014 Reference Manual, section 6.9.
.. code-block:: ada
- pragma No_Caching [ (boolean_EXPRESSION) ];
+ pragma No_Caching [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``No_Caching`` in
the SPARK 2014 Reference Manual, section 7.1.2.
.. code-block:: ada
- pragma Volatile_Function [ (boolean_EXPRESSION) ];
+ pragma Volatile_Function [ (static_boolean_EXPRESSION) ];
For the semantics of this pragma, see the entry for aspect ``Volatile_Function``
in the SPARK 2014 Reference Manual, section 7.1.2.
| (EXTERNAL_PROPERTY @{, EXTERNAL_PROPERTY@} )
EXTERNAL_PROPERTY ::=
- Async_Readers [=> boolean_EXPRESSION]
- | Async_Writers [=> boolean_EXPRESSION]
- | Effective_Reads [=> boolean_EXPRESSION]
- | Effective_Writes [=> boolean_EXPRESSION]
- others => boolean_EXPRESSION
+ Async_Readers [=> static_boolean_EXPRESSION]
+ | Async_Writers [=> static_boolean_EXPRESSION]
+ | Effective_Reads [=> static_boolean_EXPRESSION]
+ | Effective_Writes [=> static_boolean_EXPRESSION]
+ others => static_boolean_EXPRESSION
STATE_NAME ::= defining_identifier
Syntax:
@example
-pragma Async_Readers [ (boolean_EXPRESSION) ];
+pragma Async_Readers [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{Async_Readers} in
Syntax:
@example
-pragma Async_Writers [ (boolean_EXPRESSION) ];
+pragma Async_Writers [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{Async_Writers} in
Syntax:
@example
-pragma Constant_After_Elaboration [ (boolean_EXPRESSION) ];
+pragma Constant_After_Elaboration [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect
Syntax:
@example
-pragma Effective_Reads [ (boolean_EXPRESSION) ];
+pragma Effective_Reads [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{Effective_Reads} in
Syntax:
@example
-pragma Effective_Writes [ (boolean_EXPRESSION) ];
+pragma Effective_Writes [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{Effective_Writes}
Syntax:
@example
-pragma Extensions_Visible [ (boolean_EXPRESSION) ];
+pragma Extensions_Visible [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{Extensions_Visible}
Syntax:
@example
-pragma Ghost [ (boolean_EXPRESSION) ];
+pragma Ghost [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{Ghost} in the SPARK
Syntax:
@example
-pragma No_Caching [ (boolean_EXPRESSION) ];
+pragma No_Caching [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{No_Caching} in
Syntax:
@example
-pragma Volatile_Function [ (boolean_EXPRESSION) ];
+pragma Volatile_Function [ (static_boolean_EXPRESSION) ];
@end example
For the semantics of this pragma, see the entry for aspect @code{Volatile_Function}