For the semantics of this pragma, see the entry for aspect ``Abstract_State`` in
the SPARK 2014 Reference Manual, section 7.1.4.
-Pragma Acc_Parallel
-===================
-Syntax:
-
-.. code-block:: ada
-
- pragma Acc_Parallel [( ACC_PARALLEL_CLAUSE [, ACC_PARALLEL_CLAUSE... ])];
-
- ACC_PARALLEL_CLAUSE ::=
- Acc_If => boolean_EXPRESSION
- | Acc_Private => IDENTIFIERS
- | Async => integer_EXPRESSION
- | Copy => IDENTIFIERS
- | Copy_In => IDENTIFIERS
- | Copy_Out => IDENTIFIERS
- | Create => IDENTIFIERS
- | Default => None
- | Device_Ptr => IDENTIFIERS
- | First_Private => IDENTIFIERS
- | Num_Gangs => integer_EXPRESSION
- | Num_Workers => integer_EXPRESSION
- | Present => IDENTIFIERS
- | Reduction => (REDUCTION_RECORD)
- | Vector_Length => integer_EXPRESSION
- | Wait => INTEGERS
-
- REDUCTION_RECORD ::=
- "+" => IDENTIFIERS
- | "*" => IDENTIFIERS
- | "min" => IDENTIFIERS
- | "max" => IDENTIFIERS
- | "or" => IDENTIFIERS
- | "and" => IDENTIFIERS
-
- IDENTIFIERS ::=
- | IDENTIFIER
- | (IDENTIFIER, IDENTIFIERS)
-
- INTEGERS ::=
- | integer_EXPRESSION
- | (integer_EXPRESSION, INTEGERS)
-
-Requires the :switch:`-fopenacc` flag.
-
-Equivalent to the ``parallel`` directive of the OpenAcc standard. This pragma
-should be placed in loops. It offloads the content of the loop to an
-accelerator device.
-
-For more information about the effect of the clauses, see the OpenAcc
-specification.
-
-Pragma Acc_Loop
-===============
-Syntax:
-
-.. code-block:: ada
-
- pragma Acc_Loop [( ACC_LOOP_CLAUSE [, ACC_LOOP_CLAUSE... ])];
-
- ACC_LOOP_CLAUSE ::=
- Auto
- | Collapse => INTEGER_LITERAL
- | Gang [=> GANG_ARG]
- | Independent
- | Private => IDENTIFIERS
- | Reduction => (REDUCTION_RECORD)
- | Seq
- | Tile => SIZE_EXPRESSION
- | Vector [=> integer_EXPRESSION]
- | Worker [=> integer_EXPRESSION]
-
- GANG_ARG ::=
- integer_EXPRESSION
- | Static => SIZE_EXPRESSION
-
- SIZE_EXPRESSION ::=
- *
- | integer_EXPRESSION
-
-Requires the :switch:`-fopenacc` flag.
-
-Equivalent to the ``loop`` directive of the OpenAcc standard. This pragma
-should be placed in for loops after the "Acc_Parallel" pragma. It tells the
-compiler how to parallelize the loop.
-
-For more information about the effect of the clauses, see the OpenAcc
-specification.
-
-Pragma Acc_Kernels
-==================
-Syntax:
-
-.. code-block:: ada
-
- pragma Acc_Kernels [( ACC_KERNELS_CLAUSE [, ACC_KERNELS_CLAUSE...])];
-
- ACC_KERNELS_CLAUSE ::=
- Acc_If => boolean_EXPRESSION
- | Async => integer_EXPRESSION
- | Copy => IDENTIFIERS
- | Copy_In => IDENTIFIERS
- | Copy_Out => IDENTIFIERS
- | Create => IDENTIFIERS
- | Default => None
- | Device_Ptr => IDENTIFIERS
- | Num_Gangs => integer_EXPRESSION
- | Num_Workers => integer_EXPRESSION
- | Present => IDENTIFIERS
- | Vector_Length => integer_EXPRESSION
- | Wait => INTEGERS
-
- IDENTIFIERS ::=
- | IDENTIFIER
- | (IDENTIFIER, IDENTIFIERS)
-
- INTEGERS ::=
- | integer_EXPRESSION
- | (integer_EXPRESSION, INTEGERS)
-
-Requires the :switch:`-fopenacc` flag.
-
-Equivalent to the kernels directive of the OpenAcc standard. This pragma should
-be placed in loops.
-
-For more information about the effect of the clauses, see the OpenAcc
-specification.
-
-Pragma Acc_Data
-===============
-Syntax:
-
-.. code-block:: ada
-
- pragma Acc_Data ([ ACC_DATA_CLAUSE [, ACC_DATA_CLAUSE...]]);
-
- ACC_DATA_CLAUSE ::=
- Copy => IDENTIFIERS
- | Copy_In => IDENTIFIERS
- | Copy_Out => IDENTIFIERS
- | Create => IDENTIFIERS
- | Device_Ptr => IDENTIFIERS
- | Present => IDENTIFIERS
-
-Requires the :switch:`-fopenacc` flag.
-
-Equivalent to the ``data`` directive of the OpenAcc standard. This pragma
-should be placed in loops.
-
-For more information about the effect of the clauses, see the OpenAcc
-specification.
-
-
Pragma Ada_83
=============
This configuration pragma is a synonym for pragma Ada_12 and has the
same syntax and effect.
+Pragma Aggregate_Individually_Assign
+====================================
+
+Syntax:
+
+.. code-block:: ada
+
+ pragma Aggregate_Individually_Assign;
+
+Where possible, GNAT will store the binary representation of a record aggregate
+in memory for space and performance reasons. This configuration pragma changes
+this behavior so that record aggregates are instead always converted into
+individual assignment statements.
+
+
Pragma Allow_Integer_Address
============================
unanalyzed, and by convention is used to control the action of the tool to
which the annotation is addressed. The remaining ARG arguments
can be either string literals or more generally expressions.
-String literals are assumed to be either of type
+String literals (and concatenations of string literals) are assumed to be
+either of type
``Standard.String`` or else ``Wide_String`` or ``Wide_Wide_String``
depending on the character literals they contain.
All other kinds of arguments are analyzed as expressions, and must be
.. code-block:: ada
- pragma Asynch_Readers [ (boolean_EXPRESSION) ];
+ pragma Async_Readers [ (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 Asynch_Writers [ (boolean_EXPRESSION) ];
+ pragma Async_Writers [ (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.
indicating that the necessary attribute for implementation of this
pragma is not available.
+.. _Compile_Time_Error:
+
Pragma Compile_Time_Error
=========================
error messages. It
is particularly useful in generics, where errors can be issued for
specific problematic instantiations. The first parameter is a boolean
-expression. The pragma is effective only if the value of this expression
-is known at compile time, and has the value True. The set of expressions
+expression. The pragma ensures that the value of an expression
+is known at compile time, and has the value False. The set of expressions
whose values are known at compile time includes all static boolean
expressions, and also other values which the compiler can determine
at compile time (e.g., the size of a record type set by an explicit
size representation clause, or the value of a variable which was
initialized to a constant and is known not to have been modified).
-If these conditions are met, an error message is generated using
+If these conditions are not met, an error message is generated using
the value given as the second argument. This string value may contain
embedded ASCII.LF characters to break the message into multiple lines.
Same as pragma Compile_Time_Error, except a warning is issued instead
-of an error message. Note that if this pragma is used in a package that
+of an error message. If switch *-gnatw_C* is used, a warning is only issued
+if the value of the expression is known to be True at compile time, not when
+the value of the expression is not known at compile time.
+Note that if this pragma is used in a package that
is with'ed by a client, the client will get the warning even though it
is issued by a with'ed package (normally warnings in with'ed units are
suppressed, but this is a special exception to that rule).
with a first parameter of True is to warn a client about use of a package,
for example that it is not fully implemented.
+In previous versions of the compiler, combining *-gnatwe* with
+Compile_Time_Warning resulted in a fatal error. Now the compiler always emits
+a warning. You can use :ref:`Compile_Time_Error` to force the generation of
+an error.
+
Pragma Compiler_Unit
====================
The precondition ensures that one and only one of the case guards is
satisfied on entry to the subprogram.
The postcondition ensures that for the case guard that was True on entry,
-the corrresponding consequence is True on exit. Other consequence expressions
+the corresponding consequence is True on exit. Other consequence expressions
are not evaluated.
A precondition ``P`` and postcondition ``Q`` can also be
particular family of scalar types using the optional arguments of the pragma.
The compile-time approach is intended to optimize the generated code for the
- pragma, by possibly using fast operations such as ``memset``.
+ pragma, by possibly using fast operations such as ``memset``. Note that such
+ optimizations require using values where the bytes all have the same binary
+ representation.
* At bind time, the programmer has several options:
The bind-time approach is intended to provide fast turnaround for testing
with different values, without having to recompile the program.
-* At execution time, the programmer can speify the invalid values using an
+* At execution time, the programmer can specify the invalid values using an
environment variable. See the GNAT User's Guide for details.
The execution-time approach is intended to provide fast turnaround for
Pragma ``Interrupt_State`` provides a general mechanism for overriding
such uses of interrupts. It subsumes the functionality of pragma
``Unreserve_All_Interrupts``. Pragma ``Interrupt_State`` is not
-available on Windows or VMS. On all other platforms than VxWorks,
+available on Windows. On all other platforms than VxWorks,
it applies to signals; on VxWorks, it applies to vectored hardware interrupts
and may be used to mark interrupts required by the board support package
as reserved.
Compilation fails if the compiler cannot generate lock-free code for the
operations.
+The current conditions required to support this pragma are:
+
+* Protected type declarations may not contain entries
+* Protected subprogram declarations may not have nonelementary parameters
+
+In addition, each protected subprogram body must satisfy:
+
+* May reference only one protected component
+* May not reference nonconstant entities outside the protected subprogram
+ scope.
+* May not contain address representation items, allocators, or quantified
+ expressions.
+* May not contain delay, goto, loop, or procedure-call statements.
+* May not contain exported and imported entities
+* May not dereferenced access values
+* Function calls and attribute references must be static
+
+
Pragma Loop_Invariant
=====================
This pragma is used to specify the maximum callers per entry queue for
individual protected entries and entry families. It accepts a single
-positive integer as a parameter and must appear after the declaration
-of an entry.
+integer (-1 or more) as a parameter and must appear after the declaration of an
+entry.
+
+A value of -1 represents no additional restriction on queue length.
Pragma No_Body
==============
dummy body with a No_Body pragma ensures that there is no interference from
earlier versions of the package body.
+.. _Pragma-No_Caching:
+
+Pragma No_Caching
+=================
+
+Syntax:
+
+.. code-block:: ada
+
+ pragma No_Caching [ (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.
+
Pragma No_Component_Reordering
==============================
available in all earlier versions of Ada as an implementation-defined
pragma.
-Pragma No_Run_Time
-==================
-
-Syntax:
-
-
-.. code-block:: ada
-
- pragma No_Run_Time;
-
-
-This is an obsolete configuration pragma that historically was used to
-set up a runtime library with no object code. It is now used only for
-internal testing. The pragma has been superseded by the reconfigurable
-runtime capability of GNAT.
-
Pragma No_Strict_Aliasing
=========================
Source_File_Name cannot appear after a :ref:`Pragma_Source_File_Name_Project`.
For more details on the use of the ``Source_File_Name`` pragma, see the
-sections on ``Using Other File Names`` and `Alternative File Naming Schemes'
+sections on `Using Other File Names` and `Alternative File Naming Schemes`
in the :title:`GNAT User's Guide`.
.. _Pragma_Source_File_Name_Project:
pragma Validity_Checks (On); -- turn validity checks back on
A := C; -- C will be validity checked
+.. _Pragma-Volatile:
Pragma Volatile
===============
This is similar in effect to pragma Volatile, except that any reference to the
object is guaranteed to be done only with instructions that read or write all
the bits of the object. Furthermore, if the object is of a composite type,
-then any reference to a component of the object is guaranteed to read and/or
-write all the bits of the object.
+then any reference to a subcomponent of the object is guaranteed to read
+and/or write all the bits of the object.
The intention is that this be suitable for use with memory-mapped I/O devices
on some machines. Note that there are two important respects in which this is
access only part of the object in this case.
It is not permissible to specify ``Atomic`` and ``Volatile_Full_Access`` for
-the same object.
+the same type or object.
It is not permissible to specify ``Volatile_Full_Access`` for a composite
-(record or array) type or object that has at least one ``Aliased`` component.
+(record or array) type or object that has an ``Aliased`` subcomponent.
.. _Pragma-Volatile_Function:
This configuration pragma allows the programmer to specify a set
-of warnings that will be treated as errors. Any warning which
+of warnings that will be treated as errors. Any warning that
matches the pattern given by the pragma argument will be treated
-as an error. This gives much more precise control that -gnatwe
-which treats all warnings as errors.
+as an error. This gives more precise control than -gnatwe,
+which treats warnings as errors.
-The pattern may contain asterisks, which match zero or more characters in
-the message. For example, you can use
-``pragma Warning_As_Error ("bits of*unused")`` to treat the warning
-message ``warning: 960 bits of "a" unused`` as an error. No other regular
-expression notations are permitted. All characters other than asterisk in
-these three specific cases are treated as literal characters in the match.
-The match is case insensitive, for example XYZ matches xyz.
+This pragma can apply to regular warnings (messages enabled by -gnatw)
+and to style warnings (messages that start with "(style)",
+enabled by -gnaty).
+
+The pattern may contain asterisks, which match zero or more characters
+in the message. For example, you can use ``pragma Warning_As_Error
+("bits of*unused")`` to treat the warning message ``warning: 960 bits of
+"a" unused`` as an error. All characters other than asterisk are treated
+as literal characters in the match. The match is case insensitive; for
+example XYZ matches xyz.
Note that the pattern matches if it occurs anywhere within the warning
message string (it is not necessary to put an asterisk at the start and
the end of the message, since this is implied).
Another possibility for the static_string_EXPRESSION which works whether
-or not error tags are enabled (*-gnatw.d*) is to use the
+or not error tags are enabled (*-gnatw.d*) is to use a single
*-gnatw* tag string, enclosed in brackets,
-as shown in the example below, to treat a class of warnings as errors.
+as shown in the example below, to treat one category of warnings as errors.
+Note that if you want to treat multiple categories of warnings as errors,
+you can use multiple pragma Warning_As_Error.
The above use of patterns to match the message applies only to warning
messages generated by the front end. This pragma can also be applied to
DETAILS ::= static_string_EXPRESSION
DETAILS ::= On | Off, static_string_EXPRESSION
- TOOL_NAME ::= GNAT | GNATProve
+ TOOL_NAME ::= GNAT | GNATprove
REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}
``pragma Warnings (On, "***")`` will be required. This can be
helpful in avoiding forgetting to turn warnings back on.
-Note: the debug flag :switch:`-gnatd.i` (``/NOWARNINGS_PRAGMAS`` in VMS) can be
+Note: the debug flag :switch:`-gnatd.i` can be
used to cause the compiler to entirely ignore all WARNINGS pragmas. This can
be useful in checking whether obsolete pragmas in existing programs are hiding
real problems.