public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-184] [Ada] Refine description of SPARK with static Boolean expressions
@ 2022-05-09 9:31 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-09 9:31 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:28fffc452eedb284d047b83adc7f8772b15bb0f8
commit r13-184-g28fffc452eedb284d047b83adc7f8772b15bb0f8
Author: Piotr Trojanek <trojanek@adacore.com>
Date: Wed Jan 12 10:44:28 2022 +0100
[Ada] Refine description of SPARK with static Boolean expressions
A number of SPARK pragmas controlled by an optional Boolean expression
require those expressions to be static. This is now clarified in the
GNAT RM.
gcc/ada/
* doc/gnat_rm/implementation_defined_pragmas.rst
(Abstract_State, Async_Readers, Async_Writers,
Constant_After_Elaboration, Effective_Reads, Effective_Writes,
Extensions_Visible, Ghost, No_Caching, Volatile_Function): Only
static Boolean expressions are allowed.
* gnat_rm.texi: Regenerate.
Diff:
---
.../doc/gnat_rm/implementation_defined_pragmas.rst | 28 +++++++++++-----------
gcc/ada/gnat_rm.texi | 28 +++++++++++-----------
2 files changed, 28 insertions(+), 28 deletions(-)
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
index 895180e6763..25bfbc7ad21 100644
--- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -90,11 +90,11 @@ Syntax:
| (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
@@ -600,7 +600,7 @@ Syntax:
.. 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.
@@ -614,7 +614,7 @@ Syntax:
.. 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.
@@ -1132,7 +1132,7 @@ Syntax:
.. 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.
@@ -1656,7 +1656,7 @@ Syntax:
.. 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.
@@ -1670,7 +1670,7 @@ Syntax:
.. 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.
@@ -2401,7 +2401,7 @@ Syntax:
.. 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.
@@ -2615,7 +2615,7 @@ Syntax:
.. 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.
@@ -3969,7 +3969,7 @@ Syntax:
.. 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.
@@ -7430,7 +7430,7 @@ Syntax:
.. 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.
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 4bee272dfd4..495c13db044 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -1457,11 +1457,11 @@ EXTERNAL_PROPERTY_LIST ::=
| (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
@@ -1983,7 +1983,7 @@ case, and it is recommended that these two options not be used together.
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
@@ -1997,7 +1997,7 @@ the SPARK 2014 Reference Manual, section 7.1.2.
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
@@ -2533,7 +2533,7 @@ clause), the GNAT uses the default alignment as described previously.
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
@@ -3060,7 +3060,7 @@ See Ada 2012 Reference Manual for details.
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
@@ -3074,7 +3074,7 @@ the SPARK 2014 Reference Manual, section 7.1.2.
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}
@@ -3852,7 +3852,7 @@ end Stacks;
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}
@@ -4079,7 +4079,7 @@ No other value of digits is permitted.
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
@@ -5485,7 +5485,7 @@ earlier versions of the package body.
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
@@ -8948,7 +8948,7 @@ access only part of the object in this case.
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}
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-09 9:31 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-09 9:31 [gcc r13-184] [Ada] Refine description of SPARK with static Boolean expressions Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).