| .. _Implementation_Defined_Pragmas: |
| |
| ****************************** |
| Implementation Defined Pragmas |
| ****************************** |
| |
| Ada defines a set of pragmas that can be used to supply additional |
| information to the compiler. These language defined pragmas are |
| implemented in GNAT and work as described in the Ada Reference Manual. |
| |
| In addition, Ada allows implementations to define additional pragmas |
| whose meaning is defined by the implementation. GNAT provides a number |
| of these implementation-defined pragmas, which can be used to extend |
| and enhance the functionality of the compiler. This section of the GNAT |
| Reference Manual describes these additional pragmas. |
| |
| Note that any program using these pragmas might not be portable to other |
| compilers (although GNAT implements this set of pragmas on all |
| platforms). Therefore if portability to other compilers is an important |
| consideration, the use of these pragmas should be minimized. |
| |
| Pragma Abort_Defer |
| ================== |
| |
| .. index:: Deferring aborts |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Abort_Defer; |
| |
| |
| This pragma must appear at the start of the statement sequence of a |
| handled sequence of statements (right after the `begin`). It has |
| the effect of deferring aborts for the sequence of statements (but not |
| for the declarations or handlers, if any, associated with this statement |
| sequence). |
| |
| Pragma Abstract_State |
| ===================== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.1.4. |
| |
| Pragma Ada_83 |
| ============= |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Ada_83; |
| |
| |
| A configuration pragma that establishes Ada 83 mode for the unit to |
| which it applies, regardless of the mode set by the command line |
| switches. In Ada 83 mode, GNAT attempts to be as compatible with |
| the syntax and semantics of Ada 83, as defined in the original Ada |
| 83 Reference Manual as possible. In particular, the keywords added by Ada 95 |
| and Ada 2005 are not recognized, optional package bodies are allowed, |
| and generics may name types with unknown discriminants without using |
| the `(<>)` notation. In addition, some but not all of the additional |
| restrictions of Ada 83 are enforced. |
| |
| Ada 83 mode is intended for two purposes. Firstly, it allows existing |
| Ada 83 code to be compiled and adapted to GNAT with less effort. |
| Secondly, it aids in keeping code backwards compatible with Ada 83. |
| However, there is no guarantee that code that is processed correctly |
| by GNAT in Ada 83 mode will in fact compile and execute with an Ada |
| 83 compiler, since GNAT does not enforce all the additional checks |
| required by Ada 83. |
| |
| Pragma Ada_95 |
| ============= |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Ada_95; |
| |
| |
| A configuration pragma that establishes Ada 95 mode for the unit to which |
| it applies, regardless of the mode set by the command line switches. |
| This mode is set automatically for the `Ada` and `System` |
| packages and their children, so you need not specify it in these |
| contexts. This pragma is useful when writing a reusable component that |
| itself uses Ada 95 features, but which is intended to be usable from |
| either Ada 83 or Ada 95 programs. |
| |
| Pragma Ada_05 |
| ============= |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Ada_05; |
| pragma Ada_05 (local_NAME); |
| |
| |
| A configuration pragma that establishes Ada 2005 mode for the unit to which |
| it applies, regardless of the mode set by the command line switches. |
| This pragma is useful when writing a reusable component that |
| itself uses Ada 2005 features, but which is intended to be usable from |
| either Ada 83 or Ada 95 programs. |
| |
| The one argument form (which is not a configuration pragma) |
| is used for managing the transition from |
| Ada 95 to Ada 2005 in the run-time library. If an entity is marked |
| as Ada_2005 only, then referencing the entity in Ada_83 or Ada_95 |
| mode will generate a warning. In addition, in Ada_83 or Ada_95 |
| mode, a preference rule is established which does not choose |
| such an entity unless it is unambiguously specified. This avoids |
| extra subprograms marked this way from generating ambiguities in |
| otherwise legal pre-Ada_2005 programs. The one argument form is |
| intended for exclusive use in the GNAT run-time library. |
| |
| Pragma Ada_2005 |
| =============== |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Ada_2005; |
| |
| |
| This configuration pragma is a synonym for pragma Ada_05 and has the |
| same syntax and effect. |
| |
| Pragma Ada_12 |
| ============= |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Ada_12; |
| pragma Ada_12 (local_NAME); |
| |
| |
| A configuration pragma that establishes Ada 2012 mode for the unit to which |
| it applies, regardless of the mode set by the command line switches. |
| This mode is set automatically for the `Ada` and `System` |
| packages and their children, so you need not specify it in these |
| contexts. This pragma is useful when writing a reusable component that |
| itself uses Ada 2012 features, but which is intended to be usable from |
| Ada 83, Ada 95, or Ada 2005 programs. |
| |
| The one argument form, which is not a configuration pragma, |
| is used for managing the transition from Ada |
| 2005 to Ada 2012 in the run-time library. If an entity is marked |
| as Ada_201 only, then referencing the entity in any pre-Ada_2012 |
| mode will generate a warning. In addition, in any pre-Ada_2012 |
| mode, a preference rule is established which does not choose |
| such an entity unless it is unambiguously specified. This avoids |
| extra subprograms marked this way from generating ambiguities in |
| otherwise legal pre-Ada_2012 programs. The one argument form is |
| intended for exclusive use in the GNAT run-time library. |
| |
| Pragma Ada_2012 |
| =============== |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Ada_2012; |
| |
| |
| This configuration pragma is a synonym for pragma Ada_12 and has the |
| same syntax and effect. |
| |
| Pragma Allow_Integer_Address |
| ============================ |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Allow_Integer_Address; |
| |
| |
| In almost all versions of GNAT, `System.Address` is a private |
| type in accordance with the implementation advice in the RM. This |
| means that integer values, |
| in particular integer literals, are not allowed as address values. |
| If the configuration pragma |
| `Allow_Integer_Address` is given, then integer expressions may |
| be used anywhere a value of type `System.Address` is required. |
| The effect is to introduce an implicit unchecked conversion from the |
| integer value to type `System.Address`. The reverse case of using |
| an address where an integer type is required is handled analogously. |
| The following example compiles without errors: |
| |
| |
| .. code-block:: ada |
| |
| pragma Allow_Integer_Address; |
| with System; use System; |
| package AddrAsInt is |
| X : Integer; |
| Y : Integer; |
| for X'Address use 16#1240#; |
| for Y use at 16#3230#; |
| m : Address := 16#4000#; |
| n : constant Address := 4000; |
| p : constant Address := Address (X + Y); |
| v : Integer := y'Address; |
| w : constant Integer := Integer (Y'Address); |
| type R is new integer; |
| RR : R := 1000; |
| Z : Integer; |
| for Z'Address use RR; |
| end AddrAsInt; |
| |
| |
| Note that pragma `Allow_Integer_Address` is ignored if `System.Address` |
| is not a private type. In implementations of `GNAT` where |
| System.Address is a visible integer type, |
| this pragma serves no purpose but is ignored |
| rather than rejected to allow common sets of sources to be used |
| in the two situations. |
| |
| Pragma Annotate |
| =============== |
| |
| Syntax:: |
| |
| pragma Annotate (IDENTIFIER [, IDENTIFIER {, ARG}] [, entity => local_NAME]); |
| |
| ARG ::= NAME | EXPRESSION |
| |
| |
| This pragma is used to annotate programs. `identifier` identifies |
| the type of annotation. GNAT verifies that it is an identifier, but does |
| not otherwise analyze it. The second optional identifier is also left |
| 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 |
| `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 |
| unambiguous. The last argument if present must have the identifier |
| `Entity` and GNAT verifies that a local name is given. |
| |
| The analyzed pragma is retained in the tree, but not otherwise processed |
| by any part of the GNAT compiler, except to generate corresponding note |
| lines in the generated ALI file. For the format of these note lines, see |
| the compiler source file lib-writ.ads. This pragma is intended for use by |
| external tools, including ASIS. The use of pragma Annotate does not |
| affect the compilation process in any way. This pragma may be used as |
| a configuration pragma. |
| |
| Pragma Assert |
| ============= |
| |
| Syntax:: |
| |
| pragma Assert ( |
| boolean_EXPRESSION |
| [, string_EXPRESSION]); |
| |
| |
| The effect of this pragma depends on whether the corresponding command |
| line switch is set to activate assertions. The pragma expands into code |
| equivalent to the following: |
| |
| .. code-block:: ada |
| |
| if assertions-enabled then |
| if not boolean_EXPRESSION then |
| System.Assertions.Raise_Assert_Failure |
| (string_EXPRESSION); |
| end if; |
| end if; |
| |
| |
| The string argument, if given, is the message that will be associated |
| with the exception occurrence if the exception is raised. If no second |
| argument is given, the default message is `file`:`nnn`, |
| where `file` is the name of the source file containing the assert, |
| and `nnn` is the line number of the assert. A pragma is not a |
| statement, so if a statement sequence contains nothing but a pragma |
| assert, then a null statement is required in addition, as in: |
| |
| .. code-block:: ada |
| |
| ... |
| if J > 3 then |
| pragma Assert (K > 3, "Bad value for K"); |
| null; |
| end if; |
| |
| |
| Note that, as with the `if` statement to which it is equivalent, the |
| type of the expression is either `Standard.Boolean`, or any type derived |
| from this standard type. |
| |
| Assert checks can be either checked or ignored. By default they are ignored. |
| They will be checked if either the command line switch *-gnata* is |
| used, or if an `Assertion_Policy` or `Check_Policy` pragma is used |
| to enable `Assert_Checks`. |
| |
| If assertions are ignored, then there |
| is no run-time effect (and in particular, any side effects from the |
| expression will not occur at run time). (The expression is still |
| analyzed at compile time, and may cause types to be frozen if they are |
| mentioned here for the first time). |
| |
| If assertions are checked, then the given expression is tested, and if |
| it is `False` then `System.Assertions.Raise_Assert_Failure` is called |
| which results in the raising of `Assert_Failure` with the given message. |
| |
| You should generally avoid side effects in the expression arguments of |
| this pragma, because these side effects will turn on and off with the |
| setting of the assertions mode, resulting in assertions that have an |
| effect on the program. However, the expressions are analyzed for |
| semantic correctness whether or not assertions are enabled, so turning |
| assertions on and off cannot affect the legality of a program. |
| |
| Note that the implementation defined policy `DISABLE`, given in a |
| pragma `Assertion_Policy`, can be used to suppress this semantic analysis. |
| |
| Note: this is a standard language-defined pragma in versions |
| of Ada from 2005 on. In GNAT, it is implemented in all versions |
| of Ada, and the DISABLE policy is an implementation-defined |
| addition. |
| |
| Pragma Assert_And_Cut |
| ===================== |
| |
| Syntax:: |
| |
| pragma Assert_And_Cut ( |
| boolean_EXPRESSION |
| [, string_EXPRESSION]); |
| |
| |
| The effect of this pragma is identical to that of pragma `Assert`, |
| except that in an `Assertion_Policy` pragma, the identifier |
| `Assert_And_Cut` is used to control whether it is ignored or checked |
| (or disabled). |
| |
| The intention is that this be used within a subprogram when the |
| given test expresion sums up all the work done so far in the |
| subprogram, so that the rest of the subprogram can be verified |
| (informally or formally) using only the entry preconditions, |
| and the expression in this pragma. This allows dividing up |
| a subprogram into sections for the purposes of testing or |
| formal verification. The pragma also serves as useful |
| documentation. |
| |
| Pragma Assertion_Policy |
| ======================= |
| |
| Syntax:: |
| |
| pragma Assertion_Policy (CHECK | DISABLE | IGNORE); |
| |
| pragma Assertion_Policy ( |
| ASSERTION_KIND => POLICY_IDENTIFIER |
| {, ASSERTION_KIND => POLICY_IDENTIFIER}); |
| |
| ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND |
| |
| RM_ASSERTION_KIND ::= Assert | |
| Static_Predicate | |
| Dynamic_Predicate | |
| Pre | |
| Pre'Class | |
| Post | |
| Post'Class | |
| Type_Invariant | |
| Type_Invariant'Class |
| |
| ID_ASSERTION_KIND ::= Assertions | |
| Assert_And_Cut | |
| Assume | |
| Contract_Cases | |
| Debug | |
| Invariant | |
| Invariant'Class | |
| Loop_Invariant | |
| Loop_Variant | |
| Postcondition | |
| Precondition | |
| Predicate | |
| Refined_Post | |
| Statement_Assertions |
| |
| POLICY_IDENTIFIER ::= Check | Disable | Ignore |
| |
| |
| This is a standard Ada 2012 pragma that is available as an |
| implementation-defined pragma in earlier versions of Ada. |
| The assertion kinds `RM_ASSERTION_KIND` are those defined in |
| the Ada standard. The assertion kinds `ID_ASSERTION_KIND` |
| are implementation defined additions recognized by the GNAT compiler. |
| |
| The pragma applies in both cases to pragmas and aspects with matching |
| names, e.g. `Pre` applies to the Pre aspect, and `Precondition` |
| applies to both the `Precondition` pragma |
| and the aspect `Precondition`. Note that the identifiers for |
| pragmas Pre_Class and Post_Class are Pre'Class and Post'Class (not |
| Pre_Class and Post_Class), since these pragmas are intended to be |
| identical to the corresponding aspects). |
| |
| If the policy is `CHECK`, then assertions are enabled, i.e. |
| the corresponding pragma or aspect is activated. |
| If the policy is `IGNORE`, then assertions are ignored, i.e. |
| the corresponding pragma or aspect is deactivated. |
| This pragma overrides the effect of the *-gnata* switch on the |
| command line. |
| |
| The implementation defined policy `DISABLE` is like |
| `IGNORE` except that it completely disables semantic |
| checking of the corresponding pragma or aspect. This is |
| useful when the pragma or aspect argument references subprograms |
| in a with'ed package which is replaced by a dummy package |
| for the final build. |
| |
| The implementation defined assertion kind `Assertions` applies to all |
| assertion kinds. The form with no assertion kind given implies this |
| choice, so it applies to all assertion kinds (RM defined, and |
| implementation defined). |
| |
| The implementation defined assertion kind `Statement_Assertions` |
| applies to `Assert`, `Assert_And_Cut`, |
| `Assume`, `Loop_Invariant`, and `Loop_Variant`. |
| |
| Pragma Assume |
| ============= |
| |
| Syntax: |
| |
| :: |
| |
| pragma Assume ( |
| boolean_EXPRESSION |
| [, string_EXPRESSION]); |
| |
| |
| The effect of this pragma is identical to that of pragma `Assert`, |
| except that in an `Assertion_Policy` pragma, the identifier |
| `Assume` is used to control whether it is ignored or checked |
| (or disabled). |
| |
| The intention is that this be used for assumptions about the |
| external environment. So you cannot expect to verify formally |
| or informally that the condition is met, this must be |
| established by examining things outside the program itself. |
| For example, we may have code that depends on the size of |
| `Long_Long_Integer` being at least 64. So we could write: |
| |
| .. code-block:: ada |
| |
| pragma Assume (Long_Long_Integer'Size >= 64); |
| |
| |
| This assumption cannot be proved from the program itself, |
| but it acts as a useful run-time check that the assumption |
| is met, and documents the need to ensure that it is met by |
| reference to information outside the program. |
| |
| Pragma Assume_No_Invalid_Values |
| =============================== |
| .. index:: Invalid representations |
| |
| .. index:: Invalid values |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Assume_No_Invalid_Values (On | Off); |
| |
| |
| This is a configuration pragma that controls the assumptions made by the |
| compiler about the occurrence of invalid representations (invalid values) |
| in the code. |
| |
| The default behavior (corresponding to an Off argument for this pragma), is |
| to assume that values may in general be invalid unless the compiler can |
| prove they are valid. Consider the following example: |
| |
| .. code-block:: ada |
| |
| V1 : Integer range 1 .. 10; |
| V2 : Integer range 11 .. 20; |
| ... |
| for J in V2 .. V1 loop |
| ... |
| end loop; |
| |
| |
| if V1 and V2 have valid values, then the loop is known at compile |
| time not to execute since the lower bound must be greater than the |
| upper bound. However in default mode, no such assumption is made, |
| and the loop may execute. If `Assume_No_Invalid_Values (On)` |
| is given, the compiler will assume that any occurrence of a variable |
| other than in an explicit `'Valid` test always has a valid |
| value, and the loop above will be optimized away. |
| |
| The use of `Assume_No_Invalid_Values (On)` is appropriate if |
| you know your code is free of uninitialized variables and other |
| possible sources of invalid representations, and may result in |
| more efficient code. A program that accesses an invalid representation |
| with this pragma in effect is erroneous, so no guarantees can be made |
| about its behavior. |
| |
| It is peculiar though permissible to use this pragma in conjunction |
| with validity checking (-gnatVa). In such cases, accessing invalid |
| values will generally give an exception, though formally the program |
| is erroneous so there are no guarantees that this will always be the |
| case, and it is recommended that these two options not be used together. |
| |
| Pragma Async_Readers |
| ==================== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.1.2. |
| |
| Pragma Async_Writers |
| ==================== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.1.2. |
| |
| Pragma Attribute_Definition |
| =========================== |
| |
| Syntax: |
| |
| :: |
| |
| pragma Attribute_Definition |
| ([Attribute =>] ATTRIBUTE_DESIGNATOR, |
| [Entity =>] LOCAL_NAME, |
| [Expression =>] EXPRESSION | NAME); |
| |
| |
| If `Attribute` is a known attribute name, this pragma is equivalent to |
| the attribute definition clause: |
| |
| |
| .. code-block:: ada |
| |
| for Entity'Attribute use Expression; |
| |
| |
| If `Attribute` is not a recognized attribute name, the pragma is |
| ignored, and a warning is emitted. This allows source |
| code to be written that takes advantage of some new attribute, while remaining |
| compilable with earlier compilers. |
| |
| Pragma C_Pass_By_Copy |
| ===================== |
| .. index:: Passing by copy |
| |
| |
| Syntax: |
| |
| :: |
| |
| pragma C_Pass_By_Copy |
| ([Max_Size =>] static_integer_EXPRESSION); |
| |
| |
| Normally the default mechanism for passing C convention records to C |
| convention subprograms is to pass them by reference, as suggested by RM |
| B.3(69). Use the configuration pragma `C_Pass_By_Copy` to change |
| this default, by requiring that record formal parameters be passed by |
| copy if all of the following conditions are met: |
| |
| * |
| The size of the record type does not exceed the value specified for |
| `Max_Size`. |
| * |
| The record type has `Convention C`. |
| * |
| The formal parameter has this record type, and the subprogram has a |
| foreign (non-Ada) convention. |
| |
| If these conditions are met the argument is passed by copy; i.e., in a |
| manner consistent with what C expects if the corresponding formal in the |
| C prototype is a struct (rather than a pointer to a struct). |
| |
| You can also pass records by copy by specifying the convention |
| `C_Pass_By_Copy` for the record type, or by using the extended |
| `Import` and `Export` pragmas, which allow specification of |
| passing mechanisms on a parameter by parameter basis. |
| |
| Pragma Check |
| ============ |
| .. index:: Assertions |
| |
| .. index:: Named assertions |
| |
| |
| Syntax: |
| |
| :: |
| |
| pragma Check ( |
| [Name =>] CHECK_KIND, |
| [Check =>] Boolean_EXPRESSION |
| [, [Message =>] string_EXPRESSION] ); |
| |
| CHECK_KIND ::= IDENTIFIER | |
| Pre'Class | |
| Post'Class | |
| Type_Invariant'Class | |
| Invariant'Class |
| |
| |
| This pragma is similar to the predefined pragma `Assert` except that an |
| extra identifier argument is present. In conjunction with pragma |
| `Check_Policy`, this can be used to define groups of assertions that can |
| be independently controlled. The identifier `Assertion` is special, it |
| refers to the normal set of pragma `Assert` statements. |
| |
| Checks introduced by this pragma are normally deactivated by default. They can |
| be activated either by the command line option *-gnata*, which turns on |
| all checks, or individually controlled using pragma `Check_Policy`. |
| |
| The identifiers `Assertions` and `Statement_Assertions` are not |
| permitted as check kinds, since this would cause confusion with the use |
| of these identifiers in `Assertion_Policy` and `Check_Policy` |
| pragmas, where they are used to refer to sets of assertions. |
| |
| Pragma Check_Float_Overflow |
| =========================== |
| .. index:: Floating-point overflow |
| |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Check_Float_Overflow; |
| |
| |
| In Ada, the predefined floating-point types (`Short_Float`, |
| `Float`, `Long_Float`, `Long_Long_Float`) are |
| defined to be *unconstrained*. This means that even though each |
| has a well-defined base range, an operation that delivers a result |
| outside this base range is not required to raise an exception. |
| This implementation permission accommodates the notion |
| of infinities in IEEE floating-point, and corresponds to the |
| efficient execution mode on most machines. GNAT will not raise |
| overflow exceptions on these machines; instead it will generate |
| infinities and NaN's as defined in the IEEE standard. |
| |
| Generating infinities, although efficient, is not always desirable. |
| Often the preferable approach is to check for overflow, even at the |
| (perhaps considerable) expense of run-time performance. |
| This can be accomplished by defining your own constrained floating-point subtypes -- i.e., by supplying explicit |
| range constraints -- and indeed such a subtype |
| can have the same base range as its base type. For example: |
| |
| |
| .. code-block:: ada |
| |
| subtype My_Float is Float range Float'Range; |
| |
| |
| Here `My_Float` has the same range as |
| `Float` but is constrained, so operations on |
| `My_Float` values will be checked for overflow |
| against this range. |
| |
| This style will achieve the desired goal, but |
| it is often more convenient to be able to simply use |
| the standard predefined floating-point types as long |
| as overflow checking could be guaranteed. |
| The `Check_Float_Overflow` |
| configuration pragma achieves this effect. If a unit is compiled |
| subject to this configuration pragma, then all operations |
| on predefined floating-point types including operations on |
| base types of these floating-point types will be treated as |
| though those types were constrained, and overflow checks |
| will be generated. The `Constraint_Error` |
| exception is raised if the result is out of range. |
| |
| This mode can also be set by use of the compiler |
| switch *-gnateF*. |
| |
| Pragma Check_Name |
| ================= |
| .. index:: Defining check names |
| |
| .. index:: Check names, defining |
| |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Check_Name (check_name_IDENTIFIER); |
| |
| |
| This is a configuration pragma that defines a new implementation |
| defined check name (unless IDENTIFIER matches one of the predefined |
| check names, in which case the pragma has no effect). Check names |
| are global to a partition, so if two or more configuration pragmas |
| are present in a partition mentioning the same name, only one new |
| check name is introduced. |
| |
| An implementation defined check name introduced with this pragma may |
| be used in only three contexts: `pragma Suppress`, |
| `pragma Unsuppress`, |
| and as the prefix of a `Check_Name'Enabled` attribute reference. For |
| any of these three cases, the check name must be visible. A check |
| name is visible if it is in the configuration pragmas applying to |
| the current unit, or if it appears at the start of any unit that |
| is part of the dependency set of the current unit (e.g., units that |
| are mentioned in `with` clauses). |
| |
| Check names introduced by this pragma are subject to control by compiler |
| switches (in particular -gnatp) in the usual manner. |
| |
| Pragma Check_Policy |
| =================== |
| .. index:: Controlling assertions |
| |
| .. index:: Assertions, control |
| |
| .. index:: Check pragma control |
| |
| .. index:: Named assertions |
| |
| |
| Syntax: |
| |
| :: |
| |
| pragma Check_Policy |
| ([Name =>] CHECK_KIND, |
| [Policy =>] POLICY_IDENTIFIER); |
| |
| pragma Check_Policy ( |
| CHECK_KIND => POLICY_IDENTIFIER |
| {, CHECK_KIND => POLICY_IDENTIFIER}); |
| |
| ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND |
| |
| CHECK_KIND ::= IDENTIFIER | |
| Pre'Class | |
| Post'Class | |
| Type_Invariant'Class | |
| Invariant'Class |
| |
| The identifiers Name and Policy are not allowed as CHECK_KIND values. This |
| avoids confusion between the two possible syntax forms for this pragma. |
| |
| POLICY_IDENTIFIER ::= ON | OFF | CHECK | DISABLE | IGNORE |
| |
| |
| This pragma is used to set the checking policy for assertions (specified |
| by aspects or pragmas), the `Debug` pragma, or additional checks |
| to be checked using the `Check` pragma. It may appear either as |
| a configuration pragma, or within a declarative part of package. In the |
| latter case, it applies from the point where it appears to the end of |
| the declarative region (like pragma `Suppress`). |
| |
| The `Check_Policy` pragma is similar to the |
| predefined `Assertion_Policy` pragma, |
| and if the check kind corresponds to one of the assertion kinds that |
| are allowed by `Assertion_Policy`, then the effect is identical. |
| |
| If the first argument is Debug, then the policy applies to Debug pragmas, |
| disabling their effect if the policy is `OFF`, `DISABLE`, or |
| `IGNORE`, and allowing them to execute with normal semantics if |
| the policy is `ON` or `CHECK`. In addition if the policy is |
| `DISABLE`, then the procedure call in `Debug` pragmas will |
| be totally ignored and not analyzed semantically. |
| |
| Finally the first argument may be some other identifier than the above |
| possibilities, in which case it controls a set of named assertions |
| that can be checked using pragma `Check`. For example, if the pragma: |
| |
| |
| .. code-block:: ada |
| |
| pragma Check_Policy (Critical_Error, OFF); |
| |
| |
| is given, then subsequent `Check` pragmas whose first argument is also |
| `Critical_Error` will be disabled. |
| |
| The check policy is `OFF` to turn off corresponding checks, and `ON` |
| to turn on corresponding checks. The default for a set of checks for which no |
| `Check_Policy` is given is `OFF` unless the compiler switch |
| *-gnata* is given, which turns on all checks by default. |
| |
| The check policy settings `CHECK` and `IGNORE` are recognized |
| as synonyms for `ON` and `OFF`. These synonyms are provided for |
| compatibility with the standard `Assertion_Policy` pragma. The check |
| policy setting `DISABLE` causes the second argument of a corresponding |
| `Check` pragma to be completely ignored and not analyzed. |
| |
| Pragma CIL_Constructor |
| ====================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma CIL_Constructor ([Entity =>] function_LOCAL_NAME); |
| |
| |
| This pragma is used to assert that the specified Ada function should be |
| mapped to the .NET constructor for some Ada tagged record type. |
| |
| See section 4.1 of the |
| `GNAT User's Guide: Supplement for the .NET Platform.` |
| for related information. |
| |
| Pragma Comment |
| ============== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Comment (static_string_EXPRESSION); |
| |
| |
| This is almost identical in effect to pragma `Ident`. It allows the |
| placement of a comment into the object file and hence into the |
| executable file if the operating system permits such usage. The |
| difference is that `Comment`, unlike `Ident`, has |
| no limitations on placement of the pragma (it can be placed |
| anywhere in the main source unit), and if more than one pragma |
| is used, all comments are retained. |
| |
| Pragma Common_Object |
| ==================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Common_Object ( |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Size =>] EXTERNAL_SYMBOL] ); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| |
| |
| This pragma enables the shared use of variables stored in overlaid |
| linker areas corresponding to the use of `COMMON` |
| in Fortran. The single |
| object `LOCAL_NAME` is assigned to the area designated by |
| the `External` argument. |
| You may define a record to correspond to a series |
| of fields. The `Size` argument |
| is syntax checked in GNAT, but otherwise ignored. |
| |
| `Common_Object` is not supported on all platforms. If no |
| support is available, then the code generator will issue a message |
| indicating that the necessary attribute for implementation of this |
| pragma is not available. |
| |
| Pragma Compile_Time_Error |
| ========================= |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Compile_Time_Error |
| (boolean_EXPRESSION, static_string_EXPRESSION); |
| |
| |
| This pragma can be used to generate additional compile time |
| 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 |
| 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 |
| the value given as the second argument. This string value may contain |
| embedded ASCII.LF characters to break the message into multiple lines. |
| |
| Pragma Compile_Time_Warning |
| =========================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Compile_Time_Warning |
| (boolean_EXPRESSION, static_string_EXPRESSION); |
| |
| |
| 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 |
| 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). |
| |
| One typical use is within a generic where compile time known characteristics |
| of formal parameters are tested, and warnings given appropriately. Another use |
| with a first parameter of True is to warn a client about use of a package, |
| for example that it is not fully implemented. |
| |
| Pragma Compiler_Unit |
| ==================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Compiler_Unit; |
| |
| |
| This pragma is obsolete. It is equivalent to Compiler_Unit_Warning. It is |
| retained so that old versions of the GNAT run-time that use this pragma can |
| be compiled with newer versions of the compiler. |
| |
| Pragma Compiler_Unit_Warning |
| ============================ |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Compiler_Unit_Warning; |
| |
| |
| This pragma is intended only for internal use in the GNAT run-time library. |
| It indicates that the unit is used as part of the compiler build. The effect |
| is to generate warnings for the use of constructs (for example, conditional |
| expressions) that would cause trouble when bootstrapping using an older |
| version of GNAT. For the exact list of restrictions, see the compiler sources |
| and references to Check_Compiler_Unit. |
| |
| Pragma Complete_Representation |
| ============================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Complete_Representation; |
| |
| |
| This pragma must appear immediately within a record representation |
| clause. Typical placements are before the first component clause |
| or after the last component clause. The effect is to give an error |
| message if any component is missing a component clause. This pragma |
| may be used to ensure that a record representation clause is |
| complete, and that this invariant is maintained if fields are |
| added to the record in the future. |
| |
| Pragma Complex_Representation |
| ============================= |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Complex_Representation |
| ([Entity =>] LOCAL_NAME); |
| |
| |
| The `Entity` argument must be the name of a record type which has |
| two fields of the same floating-point type. The effect of this pragma is |
| to force gcc to use the special internal complex representation form for |
| this record, which may be more efficient. Note that this may result in |
| the code for this type not conforming to standard ABI (application |
| binary interface) requirements for the handling of record types. For |
| example, in some environments, there is a requirement for passing |
| records by pointer, and the use of this pragma may result in passing |
| this type in floating-point registers. |
| |
| Pragma Component_Alignment |
| ========================== |
| .. index:: Alignments of components |
| .. index:: Pragma Component_Alignment |
| |
| |
| Syntax: |
| |
| :: |
| |
| pragma Component_Alignment ( |
| [Form =>] ALIGNMENT_CHOICE |
| [, [Name =>] type_LOCAL_NAME]); |
| |
| ALIGNMENT_CHOICE ::= |
| Component_Size |
| | Component_Size_4 |
| | Storage_Unit |
| | Default |
| |
| |
| Specifies the alignment of components in array or record types. |
| The meaning of the `Form` argument is as follows: |
| |
| |
| .. index:: Component_Size (in pragma Component_Alignment) |
| |
| *Component_Size* |
| Aligns scalar components and subcomponents of the array or record type |
| on boundaries appropriate to their inherent size (naturally |
| aligned). For example, 1-byte components are aligned on byte boundaries, |
| 2-byte integer components are aligned on 2-byte boundaries, 4-byte |
| integer components are aligned on 4-byte boundaries and so on. These |
| alignment rules correspond to the normal rules for C compilers on all |
| machines except the VAX. |
| |
| .. index:: Component_Size_4 (in pragma Component_Alignment) |
| |
| *Component_Size_4* |
| Naturally aligns components with a size of four or fewer |
| bytes. Components that are larger than 4 bytes are placed on the next |
| 4-byte boundary. |
| |
| .. index:: Storage_Unit (in pragma Component_Alignment) |
| |
| *Storage_Unit* |
| Specifies that array or record components are byte aligned, i.e., |
| aligned on boundaries determined by the value of the constant |
| `System.Storage_Unit`. |
| |
| .. index:: Default (in pragma Component_Alignment) |
| |
| *Default* |
| Specifies that array or record components are aligned on default |
| boundaries, appropriate to the underlying hardware or operating system or |
| both. The `Default` choice is the same as `Component_Size` (natural |
| alignment). |
| |
| If the `Name` parameter is present, `type_LOCAL_NAME` must |
| refer to a local record or array type, and the specified alignment |
| choice applies to the specified type. The use of |
| `Component_Alignment` together with a pragma `Pack` causes the |
| `Component_Alignment` pragma to be ignored. The use of |
| `Component_Alignment` together with a record representation clause |
| is only effective for fields not specified by the representation clause. |
| |
| If the `Name` parameter is absent, the pragma can be used as either |
| a configuration pragma, in which case it applies to one or more units in |
| accordance with the normal rules for configuration pragmas, or it can be |
| used within a declarative part, in which case it applies to types that |
| are declared within this declarative part, or within any nested scope |
| within this declarative part. In either case it specifies the alignment |
| to be applied to any record or array type which has otherwise standard |
| representation. |
| |
| If the alignment for a record or array type is not specified (using |
| pragma `Pack`, pragma `Component_Alignment`, or a record rep |
| clause), the GNAT uses the default alignment as described previously. |
| |
| Pragma Contract_Cases |
| ===================== |
| .. index:: Contract cases |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Contract_Cases ( |
| Condition => Consequence |
| {,Condition => Consequence}); |
| |
| |
| The `Contract_Cases` pragma allows defining fine-grain specifications |
| that can complement or replace the contract given by a precondition and a |
| postcondition. Additionally, the `Contract_Cases` pragma can be used |
| by testing and formal verification tools. The compiler checks its validity and, |
| depending on the assertion policy at the point of declaration of the pragma, |
| it may insert a check in the executable. For code generation, the contract |
| cases |
| |
| |
| .. code-block:: ada |
| |
| pragma Contract_Cases ( |
| Cond1 => Pred1, |
| Cond2 => Pred2); |
| |
| |
| are equivalent to |
| |
| |
| .. code-block:: ada |
| |
| C1 : constant Boolean := Cond1; -- evaluated at subprogram entry |
| C2 : constant Boolean := Cond2; -- evaluated at subprogram entry |
| pragma Precondition ((C1 and not C2) or (C2 and not C1)); |
| pragma Postcondition (if C1 then Pred1); |
| pragma Postcondition (if C2 then Pred2); |
| |
| |
| The precondition ensures that one and only one of the conditions is |
| satisfied on entry to the subprogram. |
| The postcondition ensures that for the condition that was True on entry, |
| the corrresponding consequence is True on exit. Other consequence expressions |
| are not evaluated. |
| |
| A precondition `P` and postcondition `Q` can also be |
| expressed as contract cases: |
| |
| .. code-block:: ada |
| |
| pragma Contract_Cases (P => Q); |
| |
| |
| The placement and visibility rules for `Contract_Cases` pragmas are |
| identical to those described for preconditions and postconditions. |
| |
| The compiler checks that boolean expressions given in conditions and |
| consequences are valid, where the rules for conditions are the same as |
| the rule for an expression in `Precondition` and the rules for |
| consequences are the same as the rule for an expression in |
| `Postcondition`. In particular, attributes `'Old` and |
| `'Result` can only be used within consequence expressions. |
| The condition for the last contract case may be `others`, to denote |
| any case not captured by the previous cases. The |
| following is an example of use within a package spec: |
| |
| |
| .. code-block:: ada |
| |
| package Math_Functions is |
| ... |
| function Sqrt (Arg : Float) return Float; |
| pragma Contract_Cases ((Arg in 0 .. 99) => Sqrt'Result < 10, |
| Arg >= 100 => Sqrt'Result >= 10, |
| others => Sqrt'Result = 0); |
| ... |
| end Math_Functions; |
| |
| |
| The meaning of contract cases is that only one case should apply at each |
| call, as determined by the corresponding condition evaluating to True, |
| and that the consequence for this case should hold when the subprogram |
| returns. |
| |
| Pragma Convention_Identifier |
| ============================ |
| .. index:: Conventions, synonyms |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Convention_Identifier ( |
| [Name =>] IDENTIFIER, |
| [Convention =>] convention_IDENTIFIER); |
| |
| |
| This pragma provides a mechanism for supplying synonyms for existing |
| convention identifiers. The `Name` identifier can subsequently |
| be used as a synonym for the given convention in other pragmas (including |
| for example pragma `Import` or another `Convention_Identifier` |
| pragma). As an example of the use of this, suppose you had legacy code |
| which used Fortran77 as the identifier for Fortran. Then the pragma: |
| |
| |
| .. code-block:: ada |
| |
| pragma Convention_Identifier (Fortran77, Fortran); |
| |
| |
| would allow the use of the convention identifier `Fortran77` in |
| subsequent code, avoiding the need to modify the sources. As another |
| example, you could use this to parameterize convention requirements |
| according to systems. Suppose you needed to use `Stdcall` on |
| windows systems, and `C` on some other system, then you could |
| define a convention identifier `Library` and use a single |
| `Convention_Identifier` pragma to specify which convention |
| would be used system-wide. |
| |
| Pragma CPP_Class |
| ================ |
| .. index:: Interfacing with C++ |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma CPP_Class ([Entity =>] LOCAL_NAME); |
| |
| |
| The argument denotes an entity in the current declarative region that is |
| declared as a record type. It indicates that the type corresponds to an |
| externally declared C++ class type, and is to be laid out the same way |
| that C++ would lay out the type. If the C++ class has virtual primitives |
| then the record must be declared as a tagged record type. |
| |
| Types for which `CPP_Class` is specified do not have assignment or |
| equality operators defined (such operations can be imported or declared |
| as subprograms as required). Initialization is allowed only by constructor |
| functions (see pragma `CPP_Constructor`). Such types are implicitly |
| limited if not explicitly declared as limited or derived from a limited |
| type, and an error is issued in that case. |
| |
| See :ref:`Interfacing_to_C++` for related information. |
| |
| Note: Pragma `CPP_Class` is currently obsolete. It is supported |
| for backward compatibility but its functionality is available |
| using pragma `Import` with `Convention` = `CPP`. |
| |
| Pragma CPP_Constructor |
| ====================== |
| .. index:: Interfacing with C++ |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma CPP_Constructor ([Entity =>] LOCAL_NAME |
| [, [External_Name =>] static_string_EXPRESSION ] |
| [, [Link_Name =>] static_string_EXPRESSION ]); |
| |
| |
| This pragma identifies an imported function (imported in the usual way |
| with pragma `Import`) as corresponding to a C++ constructor. If |
| `External_Name` and `Link_Name` are not specified then the |
| `Entity` argument is a name that must have been previously mentioned |
| in a pragma `Import` with `Convention` = `CPP`. Such name |
| must be of one of the following forms: |
| |
| * |
| **function** `Fname` **return** T` |
| |
| * |
| **function** `Fname` **return** T'Class |
| |
| * |
| **function** `Fname` (...) **return** T` |
| |
| * |
| **function** `Fname` (...) **return** T'Class |
| |
| where `T` is a limited record type imported from C++ with pragma |
| `Import` and `Convention` = `CPP`. |
| |
| The first two forms import the default constructor, used when an object |
| of type `T` is created on the Ada side with no explicit constructor. |
| The latter two forms cover all the non-default constructors of the type. |
| See the GNAT User's Guide for details. |
| |
| If no constructors are imported, it is impossible to create any objects |
| on the Ada side and the type is implicitly declared abstract. |
| |
| Pragma `CPP_Constructor` is intended primarily for automatic generation |
| using an automatic binding generator tool (such as the `-fdump-ada-spec` |
| GCC switch). |
| See :ref:`Interfacing_to_C++` for more related information. |
| |
| Note: The use of functions returning class-wide types for constructors is |
| currently obsolete. They are supported for backward compatibility. The |
| use of functions returning the type T leave the Ada sources more clear |
| because the imported C++ constructors always return an object of type T; |
| that is, they never return an object whose type is a descendant of type T. |
| |
| Pragma CPP_Virtual |
| ================== |
| .. index:: Interfacing to C++ |
| |
| |
| This pragma is now obsolete and, other than generating a warning if warnings |
| on obsolescent features are enabled, is completely ignored. |
| It is retained for compatibility |
| purposes. It used to be required to ensure compoatibility with C++, but |
| is no longer required for that purpose because GNAT generates |
| the same object layout as the G++ compiler by default. |
| |
| See :ref:`Interfacing_to_C++` for related information. |
| |
| Pragma CPP_Vtable |
| ================= |
| .. index:: Interfacing with C++ |
| |
| |
| This pragma is now obsolete and, other than generating a warning if warnings |
| on obsolescent features are enabled, is completely ignored. |
| It used to be required to ensure compatibility with C++, but |
| is no longer required for that purpose because GNAT generates |
| the same object layout as the G++ compiler by default. |
| |
| See :ref:`Interfacing_to_C++` for related information. |
| |
| Pragma CPU |
| ========== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma CPU (EXPRESSION); |
| |
| |
| This pragma is standard in Ada 2012, but is available in all earlier |
| versions of Ada as an implementation-defined pragma. |
| See Ada 2012 Reference Manual for details. |
| |
| Pragma Debug |
| ============ |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Debug ([CONDITION, ]PROCEDURE_CALL_WITHOUT_SEMICOLON); |
| |
| PROCEDURE_CALL_WITHOUT_SEMICOLON ::= |
| PROCEDURE_NAME |
| | PROCEDURE_PREFIX ACTUAL_PARAMETER_PART |
| |
| |
| The procedure call argument has the syntactic form of an expression, meeting |
| the syntactic requirements for pragmas. |
| |
| If debug pragmas are not enabled or if the condition is present and evaluates |
| to False, this pragma has no effect. If debug pragmas are enabled, the |
| semantics of the pragma is exactly equivalent to the procedure call statement |
| corresponding to the argument with a terminating semicolon. Pragmas are |
| permitted in sequences of declarations, so you can use pragma `Debug` to |
| intersperse calls to debug procedures in the middle of declarations. Debug |
| pragmas can be enabled either by use of the command line switch *-gnata* |
| or by use of the pragma `Check_Policy` with a first argument of |
| `Debug`. |
| |
| Pragma Debug_Policy |
| =================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Debug_Policy (CHECK | DISABLE | IGNORE | ON | OFF); |
| |
| |
| This pragma is equivalent to a corresponding `Check_Policy` pragma |
| with a first argument of `Debug`. It is retained for historical |
| compatibility reasons. |
| |
| Pragma Default_Scalar_Storage_Order |
| =================================== |
| .. index:: Default_Scalar_Storage_Order |
| |
| .. index:: Scalar_Storage_Order |
| |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Default_Scalar_Storage_Order (High_Order_First | Low_Order_First); |
| |
| |
| Normally if no explicit `Scalar_Storage_Order` is given for a record |
| type or array type, then the scalar storage order defaults to the ordinary |
| default for the target. But this default may be overridden using this pragma. |
| The pragma may appear as a configuration pragma, or locally within a package |
| spec or declarative part. In the latter case, it applies to all subsequent |
| types declared within that package spec or declarative part. |
| |
| The following example shows the use of this pragma: |
| |
| |
| .. code-block:: ada |
| |
| pragma Default_Scalar_Storage_Order (High_Order_First); |
| with System; use System; |
| package DSSO1 is |
| type H1 is record |
| a : Integer; |
| end record; |
| |
| type L2 is record |
| a : Integer; |
| end record; |
| for L2'Scalar_Storage_Order use Low_Order_First; |
| |
| type L2a is new L2; |
| |
| package Inner is |
| type H3 is record |
| a : Integer; |
| end record; |
| |
| pragma Default_Scalar_Storage_Order (Low_Order_First); |
| |
| type L4 is record |
| a : Integer; |
| end record; |
| end Inner; |
| |
| type H4a is new Inner.L4; |
| |
| type H5 is record |
| a : Integer; |
| end record; |
| end DSSO1; |
| |
| |
| In this example record types L.. have `Low_Order_First` scalar |
| storage order, and record types H.. have `High_Order_First`. |
| Note that in the case of `H4a`, the order is not inherited |
| from the parent type. Only an explicitly set `Scalar_Storage_Order` |
| gets inherited on type derivation. |
| |
| If this pragma is used as a configuration pragma which appears within a |
| configuration pragma file (as opposed to appearing explicitly at the start |
| of a single unit), then the binder will require that all units in a partition |
| be compiled in a similar manner, other than run-time units, which are not |
| affected by this pragma. Note that the use of this form is discouraged because |
| it may significantly degrade the run-time performance of the software, instead |
| the default scalar storage order ought to be changed only on a local basis. |
| |
| Pragma Default_Storage_Pool |
| =========================== |
| .. index:: Default_Storage_Pool |
| |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Default_Storage_Pool (storage_pool_NAME | null); |
| |
| |
| This pragma is standard in Ada 2012, but is available in all earlier |
| versions of Ada as an implementation-defined pragma. |
| See Ada 2012 Reference Manual for details. |
| |
| Pragma Depends |
| ============== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 6.1.5. |
| |
| Pragma Detect_Blocking |
| ====================== |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Detect_Blocking; |
| |
| |
| This is a standard pragma in Ada 2005, that is available in all earlier |
| versions of Ada as an implementation-defined pragma. |
| |
| This is a configuration pragma that forces the detection of potentially |
| blocking operations within a protected operation, and to raise Program_Error |
| if that happens. |
| |
| Pragma Disable_Atomic_Synchronization |
| ===================================== |
| |
| .. index:: Atomic Synchronization |
| |
| Syntax: |
| |
| :: |
| |
| pragma Disable_Atomic_Synchronization [(Entity)]; |
| |
| |
| Ada requires that accesses (reads or writes) of an atomic variable be |
| regarded as synchronization points in the case of multiple tasks. |
| Particularly in the case of multi-processors this may require special |
| handling, e.g. the generation of memory barriers. This capability may |
| be turned off using this pragma in cases where it is known not to be |
| required. |
| |
| The placement and scope rules for this pragma are the same as those |
| for `pragma Suppress`. In particular it can be used as a |
| configuration pragma, or in a declaration sequence where it applies |
| till the end of the scope. If an `Entity` argument is present, |
| the action applies only to that entity. |
| |
| Pragma Dispatching_Domain |
| ========================= |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Dispatching_Domain (EXPRESSION); |
| |
| |
| This pragma is standard in Ada 2012, but is available in all earlier |
| versions of Ada as an implementation-defined pragma. |
| See Ada 2012 Reference Manual for details. |
| |
| Pragma Effective_Reads |
| ====================== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.1.2. |
| |
| Pragma Effective_Writes |
| ======================= |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.1.2. |
| |
| Pragma Elaboration_Checks |
| ========================= |
| .. index:: Elaboration control |
| |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Elaboration_Checks (Dynamic | Static); |
| |
| |
| This is a configuration pragma that provides control over the |
| elaboration model used by the compilation affected by the |
| pragma. If the parameter is `Dynamic`, |
| then the dynamic elaboration |
| model described in the Ada Reference Manual is used, as though |
| the *-gnatE* switch had been specified on the command |
| line. If the parameter is `Static`, then the default GNAT static |
| model is used. This configuration pragma overrides the setting |
| of the command line. For full details on the elaboration models |
| used by the GNAT compiler, see the chapter on elaboration order handling |
| in the *GNAT User's Guide*. |
| |
| Pragma Eliminate |
| ================ |
| .. index:: Elimination of unused subprograms |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Eliminate ([Entity =>] DEFINING_DESIGNATOR, |
| [Source_Location =>] STRING_LITERAL); |
| |
| |
| The string literal given for the source location is a string which |
| specifies the line number of the occurrence of the entity, using |
| the syntax for SOURCE_TRACE given below: |
| |
| |
| :: |
| |
| SOURCE_TRACE ::= SOURCE_REFERENCE [LBRACKET SOURCE_TRACE RBRACKET] |
| |
| LBRACKET ::= [ |
| RBRACKET ::= ] |
| |
| SOURCE_REFERENCE ::= FILE_NAME : LINE_NUMBER |
| |
| LINE_NUMBER ::= DIGIT {DIGIT} |
| |
| |
| Spaces around the colon in a `Source_Reference` are optional. |
| |
| The `DEFINING_DESIGNATOR` matches the defining designator used in an |
| explicit subprogram declaration, where the `entity` name in this |
| designator appears on the source line specified by the source location. |
| |
| The source trace that is given as the `Source_Location` shall obey the |
| following rules. The `FILE_NAME` is the short name (with no directory |
| information) of an Ada source file, given using exactly the required syntax |
| for the underlying file system (e.g. case is important if the underlying |
| operating system is case sensitive). `LINE_NUMBER` gives the line |
| number of the occurrence of the `entity` |
| as a decimal literal without an exponent or point. If an `entity` is not |
| declared in a generic instantiation (this includes generic subprogram |
| instances), the source trace includes only one source reference. If an entity |
| is declared inside a generic instantiation, its source trace (when parsing |
| from left to right) starts with the source location of the declaration of the |
| entity in the generic unit and ends with the source location of the |
| instantiation (it is given in square brackets). This approach is recursively |
| used in case of nested instantiations: the rightmost (nested most deeply in |
| square brackets) element of the source trace is the location of the outermost |
| instantiation, the next to left element is the location of the next (first |
| nested) instantiation in the code of the corresponding generic unit, and so |
| on, and the leftmost element (that is out of any square brackets) is the |
| location of the declaration of the entity to eliminate in a generic unit. |
| |
| Note that the `Source_Location` argument specifies which of a set of |
| similarly named entities is being eliminated, dealing both with overloading, |
| and also appearance of the same entity name in different scopes. |
| |
| This pragma indicates that the given entity is not used in the program to be |
| compiled and built. The effect of the pragma is to allow the compiler to |
| eliminate the code or data associated with the named entity. Any reference to |
| an eliminated entity causes a compile-time or link-time error. |
| |
| The intention of pragma `Eliminate` is to allow a program to be compiled |
| in a system-independent manner, with unused entities eliminated, without |
| needing to modify the source text. Normally the required set of |
| `Eliminate` pragmas is constructed automatically using the gnatelim tool. |
| |
| Any source file change that removes, splits, or |
| adds lines may make the set of Eliminate pragmas invalid because their |
| `Source_Location` argument values may get out of date. |
| |
| Pragma `Eliminate` may be used where the referenced entity is a dispatching |
| operation. In this case all the subprograms to which the given operation can |
| dispatch are considered to be unused (are never called as a result of a direct |
| or a dispatching call). |
| |
| Pragma Enable_Atomic_Synchronization |
| ==================================== |
| .. index:: Atomic Synchronization |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Enable_Atomic_Synchronization [(Entity)]; |
| |
| |
| Ada requires that accesses (reads or writes) of an atomic variable be |
| regarded as synchronization points in the case of multiple tasks. |
| Particularly in the case of multi-processors this may require special |
| handling, e.g. the generation of memory barriers. This synchronization |
| is performed by default, but can be turned off using |
| `pragma Disable_Atomic_Synchronization`. The |
| `Enable_Atomic_Synchronization` pragma can be used to turn |
| it back on. |
| |
| The placement and scope rules for this pragma are the same as those |
| for `pragma Unsuppress`. In particular it can be used as a |
| configuration pragma, or in a declaration sequence where it applies |
| till the end of the scope. If an `Entity` argument is present, |
| the action applies only to that entity. |
| |
| Pragma Export_Function |
| ====================== |
| .. index:: Argument passing mechanisms |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Export_Function ( |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Parameter_Types =>] PARAMETER_TYPES] |
| [, [Result_Type =>] result_SUBTYPE_MARK] |
| [, [Mechanism =>] MECHANISM] |
| [, [Result_Mechanism =>] MECHANISM_NAME]); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| | "" |
| |
| PARAMETER_TYPES ::= |
| null |
| | TYPE_DESIGNATOR {, TYPE_DESIGNATOR} |
| |
| TYPE_DESIGNATOR ::= |
| subtype_NAME |
| | subtype_Name ' Access |
| |
| MECHANISM ::= |
| MECHANISM_NAME |
| | (MECHANISM_ASSOCIATION {, MECHANISM_ASSOCIATION}) |
| |
| MECHANISM_ASSOCIATION ::= |
| [formal_parameter_NAME =>] MECHANISM_NAME |
| |
| MECHANISM_NAME ::= Value | Reference |
| |
| |
| Use this pragma to make a function externally callable and optionally |
| provide information on mechanisms to be used for passing parameter and |
| result values. We recommend, for the purposes of improving portability, |
| this pragma always be used in conjunction with a separate pragma |
| `Export`, which must precede the pragma `Export_Function`. |
| GNAT does not require a separate pragma `Export`, but if none is |
| present, `Convention Ada` is assumed, which is usually |
| not what is wanted, so it is usually appropriate to use this |
| pragma in conjunction with a `Export` or `Convention` |
| pragma that specifies the desired foreign convention. |
| Pragma `Export_Function` |
| (and `Export`, if present) must appear in the same declarative |
| region as the function to which they apply. |
| |
| `internal_name` must uniquely designate the function to which the |
| pragma applies. If more than one function name exists of this name in |
| the declarative part you must use the `Parameter_Types` and |
| `Result_Type` parameters is mandatory to achieve the required |
| unique designation. `subtype_mark`s in these parameters must |
| exactly match the subtypes in the corresponding function specification, |
| using positional notation to match parameters with subtype marks. |
| The form with an `'Access` attribute can be used to match an |
| anonymous access parameter. |
| |
| .. index:: Suppressing external name |
| |
| Special treatment is given if the EXTERNAL is an explicit null |
| string or a static string expressions that evaluates to the null |
| string. In this case, no external name is generated. This form |
| still allows the specification of parameter mechanisms. |
| |
| Pragma Export_Object |
| ==================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Export_Object |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Size =>] EXTERNAL_SYMBOL] |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| |
| |
| This pragma designates an object as exported, and apart from the |
| extended rules for external symbols, is identical in effect to the use of |
| the normal `Export` pragma applied to an object. You may use a |
| separate Export pragma (and you probably should from the point of view |
| of portability), but it is not required. `Size` is syntax checked, |
| but otherwise ignored by GNAT. |
| |
| Pragma Export_Procedure |
| ======================= |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Export_Procedure ( |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Parameter_Types =>] PARAMETER_TYPES] |
| [, [Mechanism =>] MECHANISM]); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| | "" |
| |
| PARAMETER_TYPES ::= |
| null |
| | TYPE_DESIGNATOR {, TYPE_DESIGNATOR} |
| |
| TYPE_DESIGNATOR ::= |
| subtype_NAME |
| | subtype_Name ' Access |
| |
| MECHANISM ::= |
| MECHANISM_NAME |
| | (MECHANISM_ASSOCIATION {, MECHANISM_ASSOCIATION}) |
| |
| MECHANISM_ASSOCIATION ::= |
| [formal_parameter_NAME =>] MECHANISM_NAME |
| |
| MECHANISM_NAME ::= Value | Reference |
| |
| |
| This pragma is identical to `Export_Function` except that it |
| applies to a procedure rather than a function and the parameters |
| `Result_Type` and `Result_Mechanism` are not permitted. |
| GNAT does not require a separate pragma `Export`, but if none is |
| present, `Convention Ada` is assumed, which is usually |
| not what is wanted, so it is usually appropriate to use this |
| pragma in conjunction with a `Export` or `Convention` |
| pragma that specifies the desired foreign convention. |
| |
| .. index:: Suppressing external name |
| |
| Special treatment is given if the EXTERNAL is an explicit null |
| string or a static string expressions that evaluates to the null |
| string. In this case, no external name is generated. This form |
| still allows the specification of parameter mechanisms. |
| |
| Pragma Export_Value |
| =================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Export_Value ( |
| [Value =>] static_integer_EXPRESSION, |
| [Link_Name =>] static_string_EXPRESSION); |
| |
| |
| This pragma serves to export a static integer value for external use. |
| The first argument specifies the value to be exported. The Link_Name |
| argument specifies the symbolic name to be associated with the integer |
| value. This pragma is useful for defining a named static value in Ada |
| that can be referenced in assembly language units to be linked with |
| the application. This pragma is currently supported only for the |
| AAMP target and is ignored for other targets. |
| |
| Pragma Export_Valued_Procedure |
| ============================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Export_Valued_Procedure ( |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Parameter_Types =>] PARAMETER_TYPES] |
| [, [Mechanism =>] MECHANISM]); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| | "" |
| |
| PARAMETER_TYPES ::= |
| null |
| | TYPE_DESIGNATOR {, TYPE_DESIGNATOR} |
| |
| TYPE_DESIGNATOR ::= |
| subtype_NAME |
| | subtype_Name ' Access |
| |
| MECHANISM ::= |
| MECHANISM_NAME |
| | (MECHANISM_ASSOCIATION {, MECHANISM_ASSOCIATION}) |
| |
| MECHANISM_ASSOCIATION ::= |
| [formal_parameter_NAME =>] MECHANISM_NAME |
| |
| MECHANISM_NAME ::= Value | Reference |
| |
| |
| This pragma is identical to `Export_Procedure` except that the |
| first parameter of `LOCAL_NAME`, which must be present, must be of |
| mode `OUT`, and externally the subprogram is treated as a function |
| with this parameter as the result of the function. GNAT provides for |
| this capability to allow the use of `OUT` and `IN OUT` |
| parameters in interfacing to external functions (which are not permitted |
| in Ada functions). |
| GNAT does not require a separate pragma `Export`, but if none is |
| present, `Convention Ada` is assumed, which is almost certainly |
| not what is wanted since the whole point of this pragma is to interface |
| with foreign language functions, so it is usually appropriate to use this |
| pragma in conjunction with a `Export` or `Convention` |
| pragma that specifies the desired foreign convention. |
| |
| .. index:: Suppressing external name |
| |
| Special treatment is given if the EXTERNAL is an explicit null |
| string or a static string expressions that evaluates to the null |
| string. In this case, no external name is generated. This form |
| still allows the specification of parameter mechanisms. |
| |
| Pragma Extend_System |
| ==================== |
| .. index:: System, extending |
| |
| .. index:: DEC Ada 83 |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Extend_System ([Name =>] IDENTIFIER); |
| |
| |
| This pragma is used to provide backwards compatibility with other |
| implementations that extend the facilities of package `System`. In |
| GNAT, `System` contains only the definitions that are present in |
| the Ada RM. However, other implementations, notably the DEC Ada 83 |
| implementation, provide many extensions to package `System`. |
| |
| For each such implementation accommodated by this pragma, GNAT provides a |
| package `Aux_`xxx``, e.g., `Aux_DEC` for the DEC Ada 83 |
| implementation, which provides the required additional definitions. You |
| can use this package in two ways. You can `with` it in the normal |
| way and access entities either by selection or using a `use` |
| clause. In this case no special processing is required. |
| |
| However, if existing code contains references such as |
| `System.`xxx`` where `xxx` is an entity in the extended |
| definitions provided in package `System`, you may use this pragma |
| to extend visibility in `System` in a non-standard way that |
| provides greater compatibility with the existing code. Pragma |
| `Extend_System` is a configuration pragma whose single argument is |
| the name of the package containing the extended definition |
| (e.g., `Aux_DEC` for the DEC Ada case). A unit compiled under |
| control of this pragma will be processed using special visibility |
| processing that looks in package `System.Aux_`xxx`` where |
| `Aux_`xxx`` is the pragma argument for any entity referenced in |
| package `System`, but not found in package `System`. |
| |
| You can use this pragma either to access a predefined `System` |
| extension supplied with the compiler, for example `Aux_DEC` or |
| you can construct your own extension unit following the above |
| definition. Note that such a package is a child of `System` |
| and thus is considered part of the implementation. |
| To compile it you will have to use the *-gnatg* switch |
| for compiling System units, as explained in the |
| GNAT User's Guide. |
| |
| Pragma Extensions_Allowed |
| ========================= |
| .. index:: Ada Extensions |
| |
| .. index:: GNAT Extensions |
| |
| |
| Syntax: |
| |
| .. code-block:: ada |
| |
| pragma Extensions_Allowed (On | Off); |
| |
| |
| This configuration pragma enables or disables the implementation |
| extension mode (the use of Off as a parameter cancels the effect |
| of the *-gnatX* command switch). |
| |
| In extension mode, the latest version of the Ada language is |
| implemented (currently Ada 2012), and in addition a small number |
| of GNAT specific extensions are recognized as follows: |
| |
| |
| |
| *Constrained attribute for generic objects* |
| The `Constrained` attribute is permitted for objects of |
| generic types. The result indicates if the corresponding actual |
| is constrained. |
| |
| |
| Pragma External |
| =============== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma External ( |
| [ Convention =>] convention_IDENTIFIER, |
| [ Entity =>] LOCAL_NAME |
| [, [External_Name =>] static_string_EXPRESSION ] |
| [, [Link_Name =>] static_string_EXPRESSION ]); |
| |
| |
| This pragma is identical in syntax and semantics to pragma |
| `Export` as defined in the Ada Reference Manual. It is |
| provided for compatibility with some Ada 83 compilers that |
| used this pragma for exactly the same purposes as pragma |
| `Export` before the latter was standardized. |
| |
| Pragma External_Name_Casing |
| =========================== |
| .. index:: Dec Ada 83 casing compatibility |
| |
| .. index:: External Names, casing |
| |
| .. index:: Casing of External names |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma External_Name_Casing ( |
| Uppercase | Lowercase |
| [, Uppercase | Lowercase | As_Is]); |
| |
| |
| This pragma provides control over the casing of external names associated |
| with Import and Export pragmas. There are two cases to consider: |
| |
| |
| |
| * Implicit external names |
| |
| Implicit external names are derived from identifiers. The most common case |
| arises when a standard Ada Import or Export pragma is used with only two |
| arguments, as in: |
| |
| .. code-block:: ada |
| |
| pragma Import (C, C_Routine); |
| |
| Since Ada is a case-insensitive language, the spelling of the identifier in |
| the Ada source program does not provide any information on the desired |
| casing of the external name, and so a convention is needed. In GNAT the |
| default treatment is that such names are converted to all lower case |
| letters. This corresponds to the normal C style in many environments. |
| The first argument of pragma `External_Name_Casing` can be used to |
| control this treatment. If `Uppercase` is specified, then the name |
| will be forced to all uppercase letters. If `Lowercase` is specified, |
| then the normal default of all lower case letters will be used. |
| |
| This same implicit treatment is also used in the case of extended DEC Ada 83 |
| compatible Import and Export pragmas where an external name is explicitly |
| specified using an identifier rather than a string. |
| |
| |
| * Explicit external names |
| |
| Explicit external names are given as string literals. The most common case |
| arises when a standard Ada Import or Export pragma is used with three |
| arguments, as in: |
| |
| .. code-block:: ada |
| |
| pragma Import (C, C_Routine, "C_routine"); |
| |
| In this case, the string literal normally provides the exact casing required |
| for the external name. The second argument of pragma |
| `External_Name_Casing` may be used to modify this behavior. |
| If `Uppercase` is specified, then the name |
| will be forced to all uppercase letters. If `Lowercase` is specified, |
| then the name will be forced to all lowercase letters. A specification of |
| `As_Is` provides the normal default behavior in which the casing is |
| taken from the string provided. |
| |
| This pragma may appear anywhere that a pragma is valid. In particular, it |
| can be used as a configuration pragma in the :file:`gnat.adc` file, in which |
| case it applies to all subsequent compilations, or it can be used as a program |
| unit pragma, in which case it only applies to the current unit, or it can |
| be used more locally to control individual Import/Export pragmas. |
| |
| It was primarily intended for use with OpenVMS systems, where many |
| compilers convert all symbols to upper case by default. For interfacing to |
| such compilers (e.g., the DEC C compiler), it may be convenient to use |
| the pragma: |
| |
| .. code-block:: ada |
| |
| pragma External_Name_Casing (Uppercase, Uppercase); |
| |
| |
| to enforce the upper casing of all external symbols. |
| |
| Pragma Fast_Math |
| ================ |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Fast_Math; |
| |
| |
| This is a configuration pragma which activates a mode in which speed is |
| considered more important for floating-point operations than absolutely |
| accurate adherence to the requirements of the standard. Currently the |
| following operations are affected: |
| |
| |
| |
| *Complex Multiplication* |
| The normal simple formula for complex multiplication can result in intermediate |
| overflows for numbers near the end of the range. The Ada standard requires that |
| this situation be detected and corrected by scaling, but in Fast_Math mode such |
| cases will simply result in overflow. Note that to take advantage of this you |
| must instantiate your own version of `Ada.Numerics.Generic_Complex_Types` |
| under control of the pragma, rather than use the preinstantiated versions. |
| |
| Pragma Favor_Top_Level |
| ====================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Favor_Top_Level (type_NAME); |
| |
| |
| The named type must be an access-to-subprogram type. This pragma is an |
| efficiency hint to the compiler, regarding the use of 'Access or |
| 'Unrestricted_Access on nested (non-library-level) subprograms. The |
| pragma means that nested subprograms are not used with this type, or |
| are rare, so that the generated code should be efficient in the |
| top-level case. When this pragma is used, dynamically generated |
| trampolines may be used on some targets for nested subprograms. |
| See also the No_Implicit_Dynamic_Code restriction. |
| |
| Pragma Finalize_Storage_Only |
| ============================ |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Finalize_Storage_Only (first_subtype_LOCAL_NAME); |
| |
| |
| This pragma allows the compiler not to emit a Finalize call for objects |
| defined at the library level. This is mostly useful for types where |
| finalization is only used to deal with storage reclamation since in most |
| environments it is not necessary to reclaim memory just before terminating |
| execution, hence the name. |
| |
| Pragma Float_Representation |
| =========================== |
| |
| Syntax:: |
| |
| pragma Float_Representation (FLOAT_REP[, float_type_LOCAL_NAME]); |
| |
| FLOAT_REP ::= VAX_Float | IEEE_Float |
| |
| |
| In the one argument form, this pragma is a configuration pragma which |
| allows control over the internal representation chosen for the predefined |
| floating point types declared in the packages `Standard` and |
| `System`. This pragma is only provided for compatibility and has no effect. |
| |
| The two argument form specifies the representation to be used for |
| the specified floating-point type. The argument must |
| be `IEEE_Float` to specify the use of IEEE format, as follows: |
| |
| * |
| For a digits value of 6, 32-bit IEEE short format will be used. |
| * |
| For a digits value of 15, 64-bit IEEE long format will be used. |
| * |
| No other value of digits is permitted. |
| |
| Pragma Global |
| ============= |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 6.1.4. |
| |
| Pragma Ident |
| ============ |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Ident (static_string_EXPRESSION); |
| |
| |
| This pragma is identical in effect to pragma `Comment`. It is provided |
| for compatibility with other Ada compilers providing this pragma. |
| |
| Pragma Ignore_Pragma |
| ==================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Ignore_Pragma (pragma_IDENTIFIER); |
| |
| This is a configuration pragma |
| that takes a single argument that is a simple identifier. Any subsequent |
| use of a pragma whose pragma identifier matches this argument will be |
| silently ignored. This may be useful when legacy code or code intended |
| for compilation with some other compiler contains pragmas that match the |
| name, but not the exact implementation, of a `GNAT` pragma. The use of this |
| pragma allows such pragmas to be ignored, which may be useful in `CodePeer` |
| mode, or during porting of legacy code. |
| |
| Pragma Implementation_Defined |
| ============================= |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Implementation_Defined (local_NAME); |
| |
| |
| This pragma marks a previously declared entioty as implementation-defined. |
| For an overloaded entity, applies to the most recent homonym. |
| |
| |
| .. code-block:: ada |
| |
| pragma Implementation_Defined; |
| |
| |
| The form with no arguments appears anywhere within a scope, most |
| typically a package spec, and indicates that all entities that are |
| defined within the package spec are Implementation_Defined. |
| |
| This pragma is used within the GNAT runtime library to identify |
| implementation-defined entities introduced in language-defined units, |
| for the purpose of implementing the No_Implementation_Identifiers |
| restriction. |
| |
| Pragma Implemented |
| ================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Implemented (procedure_LOCAL_NAME, implementation_kind); |
| |
| implementation_kind ::= By_Entry | By_Protected_Procedure | By_Any |
| |
| |
| This is an Ada 2012 representation pragma which applies to protected, task |
| and synchronized interface primitives. The use of pragma Implemented provides |
| a way to impose a static requirement on the overriding operation by adhering |
| to one of the three implementation kinds: entry, protected procedure or any of |
| the above. This pragma is available in all earlier versions of Ada as an |
| implementation-defined pragma. |
| |
| |
| .. code-block:: ada |
| |
| type Synch_Iface is synchronized interface; |
| procedure Prim_Op (Obj : in out Iface) is abstract; |
| pragma Implemented (Prim_Op, By_Protected_Procedure); |
| |
| protected type Prot_1 is new Synch_Iface with |
| procedure Prim_Op; -- Legal |
| end Prot_1; |
| |
| protected type Prot_2 is new Synch_Iface with |
| entry Prim_Op; -- Illegal |
| end Prot_2; |
| |
| task type Task_Typ is new Synch_Iface with |
| entry Prim_Op; -- Illegal |
| end Task_Typ; |
| |
| |
| When applied to the procedure_or_entry_NAME of a requeue statement, pragma |
| Implemented determines the runtime behavior of the requeue. Implementation kind |
| By_Entry guarantees that the action of requeueing will proceed from an entry to |
| another entry. Implementation kind By_Protected_Procedure transforms the |
| requeue into a dispatching call, thus eliminating the chance of blocking. Kind |
| By_Any shares the behavior of By_Entry and By_Protected_Procedure depending on |
| the target's overriding subprogram kind. |
| |
| Pragma Implicit_Packing |
| ======================= |
| .. index:: Rational Profile |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Implicit_Packing; |
| |
| |
| This is a configuration pragma that requests implicit packing for packed |
| arrays for which a size clause is given but no explicit pragma Pack or |
| specification of Component_Size is present. It also applies to records |
| where no record representation clause is present. Consider this example: |
| |
| |
| .. code-block:: ada |
| |
| type R is array (0 .. 7) of Boolean; |
| for R'Size use 8; |
| |
| |
| In accordance with the recommendation in the RM (RM 13.3(53)), a Size clause |
| does not change the layout of a composite object. So the Size clause in the |
| above example is normally rejected, since the default layout of the array uses |
| 8-bit components, and thus the array requires a minimum of 64 bits. |
| |
| If this declaration is compiled in a region of code covered by an occurrence |
| of the configuration pragma Implicit_Packing, then the Size clause in this |
| and similar examples will cause implicit packing and thus be accepted. For |
| this implicit packing to occur, the type in question must be an array of small |
| components whose size is known at compile time, and the Size clause must |
| specify the exact size that corresponds to the number of elements in the array |
| multiplied by the size in bits of the component type (both single and |
| multi-dimensioned arrays can be controlled with this pragma). |
| |
| .. index:: Array packing |
| |
| Similarly, the following example shows the use in the record case |
| |
| |
| .. code-block:: ada |
| |
| type r is record |
| a, b, c, d, e, f, g, h : boolean; |
| chr : character; |
| end record; |
| for r'size use 16; |
| |
| |
| Without a pragma Pack, each Boolean field requires 8 bits, so the |
| minimum size is 72 bits, but with a pragma Pack, 16 bits would be |
| sufficient. The use of pragma Implicit_Packing allows this record |
| declaration to compile without an explicit pragma Pack. |
| |
| Pragma Import_Function |
| ====================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Import_Function ( |
| [Internal =>] LOCAL_NAME, |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Parameter_Types =>] PARAMETER_TYPES] |
| [, [Result_Type =>] SUBTYPE_MARK] |
| [, [Mechanism =>] MECHANISM] |
| [, [Result_Mechanism =>] MECHANISM_NAME]); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| |
| PARAMETER_TYPES ::= |
| null |
| | TYPE_DESIGNATOR {, TYPE_DESIGNATOR} |
| |
| TYPE_DESIGNATOR ::= |
| subtype_NAME |
| | subtype_Name ' Access |
| |
| MECHANISM ::= |
| MECHANISM_NAME |
| | (MECHANISM_ASSOCIATION {, MECHANISM_ASSOCIATION}) |
| |
| MECHANISM_ASSOCIATION ::= |
| [formal_parameter_NAME =>] MECHANISM_NAME |
| |
| MECHANISM_NAME ::= |
| Value |
| | Reference |
| |
| |
| This pragma is used in conjunction with a pragma `Import` to |
| specify additional information for an imported function. The pragma |
| `Import` (or equivalent pragma `Interface`) must precede the |
| `Import_Function` pragma and both must appear in the same |
| declarative part as the function specification. |
| |
| The `Internal` argument must uniquely designate |
| the function to which the |
| pragma applies. If more than one function name exists of this name in |
| the declarative part you must use the `Parameter_Types` and |
| `Result_Type` parameters to achieve the required unique |
| designation. Subtype marks in these parameters must exactly match the |
| subtypes in the corresponding function specification, using positional |
| notation to match parameters with subtype marks. |
| The form with an `'Access` attribute can be used to match an |
| anonymous access parameter. |
| |
| You may optionally use the `Mechanism` and `Result_Mechanism` |
| parameters to specify passing mechanisms for the |
| parameters and result. If you specify a single mechanism name, it |
| applies to all parameters. Otherwise you may specify a mechanism on a |
| parameter by parameter basis using either positional or named |
| notation. If the mechanism is not specified, the default mechanism |
| is used. |
| |
| Pragma Import_Object |
| ==================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Import_Object |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Size =>] EXTERNAL_SYMBOL]); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| |
| |
| This pragma designates an object as imported, and apart from the |
| extended rules for external symbols, is identical in effect to the use of |
| the normal `Import` pragma applied to an object. Unlike the |
| subprogram case, you need not use a separate `Import` pragma, |
| although you may do so (and probably should do so from a portability |
| point of view). `size` is syntax checked, but otherwise ignored by |
| GNAT. |
| |
| Pragma Import_Procedure |
| ======================= |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Import_Procedure ( |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Parameter_Types =>] PARAMETER_TYPES] |
| [, [Mechanism =>] MECHANISM]); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| |
| PARAMETER_TYPES ::= |
| null |
| | TYPE_DESIGNATOR {, TYPE_DESIGNATOR} |
| |
| TYPE_DESIGNATOR ::= |
| subtype_NAME |
| | subtype_Name ' Access |
| |
| MECHANISM ::= |
| MECHANISM_NAME |
| | (MECHANISM_ASSOCIATION {, MECHANISM_ASSOCIATION}) |
| |
| MECHANISM_ASSOCIATION ::= |
| [formal_parameter_NAME =>] MECHANISM_NAME |
| |
| MECHANISM_NAME ::= Value | Reference |
| |
| |
| This pragma is identical to `Import_Function` except that it |
| applies to a procedure rather than a function and the parameters |
| `Result_Type` and `Result_Mechanism` are not permitted. |
| |
| Pragma Import_Valued_Procedure |
| ============================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Import_Valued_Procedure ( |
| [Internal =>] LOCAL_NAME |
| [, [External =>] EXTERNAL_SYMBOL] |
| [, [Parameter_Types =>] PARAMETER_TYPES] |
| [, [Mechanism =>] MECHANISM]); |
| |
| EXTERNAL_SYMBOL ::= |
| IDENTIFIER |
| | static_string_EXPRESSION |
| |
| PARAMETER_TYPES ::= |
| null |
| | TYPE_DESIGNATOR {, TYPE_DESIGNATOR} |
| |
| TYPE_DESIGNATOR ::= |
| subtype_NAME |
| | subtype_Name ' Access |
| |
| MECHANISM ::= |
| MECHANISM_NAME |
| | (MECHANISM_ASSOCIATION {, MECHANISM_ASSOCIATION}) |
| |
| MECHANISM_ASSOCIATION ::= |
| [formal_parameter_NAME =>] MECHANISM_NAME |
| |
| MECHANISM_NAME ::= Value | Reference |
| |
| |
| This pragma is identical to `Import_Procedure` except that the |
| first parameter of `LOCAL_NAME`, which must be present, must be of |
| mode `OUT`, and externally the subprogram is treated as a function |
| with this parameter as the result of the function. The purpose of this |
| capability is to allow the use of `OUT` and `IN OUT` |
| parameters in interfacing to external functions (which are not permitted |
| in Ada functions). You may optionally use the `Mechanism` |
| parameters to specify passing mechanisms for the parameters. |
| If you specify a single mechanism name, it applies to all parameters. |
| Otherwise you may specify a mechanism on a parameter by parameter |
| basis using either positional or named notation. If the mechanism is not |
| specified, the default mechanism is used. |
| |
| Note that it is important to use this pragma in conjunction with a separate |
| pragma Import that specifies the desired convention, since otherwise the |
| default convention is Ada, which is almost certainly not what is required. |
| |
| Pragma Independent |
| ================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Independent (Local_NAME); |
| |
| |
| This pragma is standard in Ada 2012 mode (which also provides an aspect |
| of the same name). It is also available as an implementation-defined |
| pragma in all earlier versions. It specifies that the |
| designated object or all objects of the designated type must be |
| independently addressable. This means that separate tasks can safely |
| manipulate such objects. For example, if two components of a record are |
| independent, then two separate tasks may access these two components. |
| This may place |
| constraints on the representation of the object (for instance prohibiting |
| tight packing). |
| |
| Pragma Independent_Components |
| ============================= |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Independent_Components (Local_NAME); |
| |
| |
| This pragma is standard in Ada 2012 mode (which also provides an aspect |
| of the same name). It is also available as an implementation-defined |
| pragma in all earlier versions. It specifies that the components of the |
| designated object, or the components of each object of the designated |
| type, must be |
| independently addressable. This means that separate tasks can safely |
| manipulate separate components in the composite object. This may place |
| constraints on the representation of the object (for instance prohibiting |
| tight packing). |
| |
| Pragma Initial_Condition |
| ======================== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.1.6. |
| |
| Pragma Initialize_Scalars |
| ========================= |
| .. index:: debugging with Initialize_Scalars |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Initialize_Scalars; |
| |
| |
| This pragma is similar to `Normalize_Scalars` conceptually but has |
| two important differences. First, there is no requirement for the pragma |
| to be used uniformly in all units of a partition, in particular, it is fine |
| to use this just for some or all of the application units of a partition, |
| without needing to recompile the run-time library. |
| |
| In the case where some units are compiled with the pragma, and some without, |
| then a declaration of a variable where the type is defined in package |
| Standard or is locally declared will always be subject to initialization, |
| as will any declaration of a scalar variable. For composite variables, |
| whether the variable is initialized may also depend on whether the package |
| in which the type of the variable is declared is compiled with the pragma. |
| |
| The other important difference is that you can control the value used |
| for initializing scalar objects. At bind time, you can select several |
| options for initialization. You can |
| initialize with invalid values (similar to Normalize_Scalars, though for |
| Initialize_Scalars it is not always possible to determine the invalid |
| values in complex cases like signed component fields with non-standard |
| sizes). You can also initialize with high or |
| low values, or with a specified bit pattern. See the GNAT |
| User's Guide for binder options for specifying these cases. |
| |
| This means that you can compile a program, and then without having to |
| recompile the program, you can run it with different values being used |
| for initializing otherwise uninitialized values, to test if your program |
| behavior depends on the choice. Of course the behavior should not change, |
| and if it does, then most likely you have an incorrect reference to an |
| uninitialized value. |
| |
| It is even possible to change the value at execution time eliminating even |
| the need to rebind with a different switch using an environment variable. |
| See the GNAT User's Guide for details. |
| |
| Note that pragma `Initialize_Scalars` is particularly useful in |
| conjunction with the enhanced validity checking that is now provided |
| in GNAT, which checks for invalid values under more conditions. |
| Using this feature (see description of the *-gnatV* flag in the |
| GNAT User's Guide) in conjunction with |
| pragma `Initialize_Scalars` |
| provides a powerful new tool to assist in the detection of problems |
| caused by uninitialized variables. |
| |
| Note: the use of `Initialize_Scalars` has a fairly extensive |
| effect on the generated code. This may cause your code to be |
| substantially larger. It may also cause an increase in the amount |
| of stack required, so it is probably a good idea to turn on stack |
| checking (see description of stack checking in the GNAT |
| User's Guide) when using this pragma. |
| |
| Pragma Initializes |
| ================== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.1.5. |
| |
| Pragma Inline_Always |
| ==================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Inline_Always (NAME [, NAME]); |
| |
| |
| Similar to pragma `Inline` except that inlining is not subject to |
| the use of option *-gnatn* or *-gnatN* and the inlining |
| happens regardless of whether these options are used. |
| |
| Pragma Inline_Generic |
| ===================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Inline_Generic (GNAME {, GNAME}); |
| |
| GNAME ::= generic_unit_NAME | generic_instance_NAME |
| |
| |
| This pragma is provided for compatibility with Dec Ada 83. It has |
| no effect in `GNAT` (which always inlines generics), other |
| than to check that the given names are all names of generic units or |
| generic instances. |
| |
| Pragma Interface |
| ================ |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Interface ( |
| [Convention =>] convention_identifier, |
| [Entity =>] local_NAME |
| [, [External_Name =>] static_string_expression] |
| [, [Link_Name =>] static_string_expression]); |
| |
| |
| This pragma is identical in syntax and semantics to |
| the standard Ada pragma `Import`. It is provided for compatibility |
| with Ada 83. The definition is upwards compatible both with pragma |
| `Interface` as defined in the Ada 83 Reference Manual, and also |
| with some extended implementations of this pragma in certain Ada 83 |
| implementations. The only difference between pragma `Interface` |
| and pragma `Import` is that there is special circuitry to allow |
| both pragmas to appear for the same subprogram entity (normally it |
| is illegal to have multiple `Import` pragmas. This is useful in |
| maintaining Ada 83/Ada 95 compatibility and is compatible with other |
| Ada 83 compilers. |
| |
| Pragma Interface_Name |
| ===================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Interface_Name ( |
| [Entity =>] LOCAL_NAME |
| [, [External_Name =>] static_string_EXPRESSION] |
| [, [Link_Name =>] static_string_EXPRESSION]); |
| |
| |
| This pragma provides an alternative way of specifying the interface name |
| for an interfaced subprogram, and is provided for compatibility with Ada |
| 83 compilers that use the pragma for this purpose. You must provide at |
| least one of `External_Name` or `Link_Name`. |
| |
| Pragma Interrupt_Handler |
| ======================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Interrupt_Handler (procedure_LOCAL_NAME); |
| |
| |
| This program unit pragma is supported for parameterless protected procedures |
| as described in Annex C of the Ada Reference Manual. On the AAMP target |
| the pragma can also be specified for nonprotected parameterless procedures |
| that are declared at the library level (which includes procedures |
| declared at the top level of a library package). In the case of AAMP, |
| when this pragma is applied to a nonprotected procedure, the instruction |
| `IERET` is generated for returns from the procedure, enabling |
| maskable interrupts, in place of the normal return instruction. |
| |
| Pragma Interrupt_State |
| ====================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Interrupt_State |
| ([Name =>] value, |
| [State =>] SYSTEM | RUNTIME | USER); |
| |
| |
| Normally certain interrupts are reserved to the implementation. Any attempt |
| to attach an interrupt causes Program_Error to be raised, as described in |
| RM C.3.2(22). A typical example is the `SIGINT` interrupt used in |
| many systems for an :kbd:`Ctrl-C` interrupt. Normally this interrupt is |
| reserved to the implementation, so that :kbd:`Ctrl-C` can be used to |
| interrupt execution. Additionally, signals such as `SIGSEGV`, |
| `SIGABRT`, `SIGFPE` and `SIGILL` are often mapped to specific |
| Ada exceptions, or used to implement run-time functions such as the |
| `abort` statement and stack overflow checking. |
| |
| 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, |
| 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. |
| |
| Interrupts can be in one of three states: |
| |
| * System |
| |
| The interrupt is reserved (no Ada handler can be installed), and the |
| Ada run-time may not install a handler. As a result you are guaranteed |
| standard system default action if this interrupt is raised. |
| |
| * Runtime |
| |
| The interrupt is reserved (no Ada handler can be installed). The run time |
| is allowed to install a handler for internal control purposes, but is |
| not required to do so. |
| |
| * User |
| |
| The interrupt is unreserved. The user may install a handler to provide |
| some other action. |
| |
| These states are the allowed values of the `State` parameter of the |
| pragma. The `Name` parameter is a value of the type |
| `Ada.Interrupts.Interrupt_ID`. Typically, it is a name declared in |
| `Ada.Interrupts.Names`. |
| |
| This is a configuration pragma, and the binder will check that there |
| are no inconsistencies between different units in a partition in how a |
| given interrupt is specified. It may appear anywhere a pragma is legal. |
| |
| The effect is to move the interrupt to the specified state. |
| |
| By declaring interrupts to be SYSTEM, you guarantee the standard system |
| action, such as a core dump. |
| |
| By declaring interrupts to be USER, you guarantee that you can install |
| a handler. |
| |
| Note that certain signals on many operating systems cannot be caught and |
| handled by applications. In such cases, the pragma is ignored. See the |
| operating system documentation, or the value of the array `Reserved` |
| declared in the spec of package `System.OS_Interface`. |
| |
| Overriding the default state of signals used by the Ada runtime may interfere |
| with an application's runtime behavior in the cases of the synchronous signals, |
| and in the case of the signal used to implement the `abort` statement. |
| |
| Pragma Invariant |
| ================ |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Invariant |
| ([Entity =>] private_type_LOCAL_NAME, |
| [Check =>] EXPRESSION |
| [,[Message =>] String_Expression]); |
| |
| |
| This pragma provides exactly the same capabilities as the Type_Invariant aspect |
| defined in AI05-0146-1, and in the Ada 2012 Reference Manual. The |
| Type_Invariant aspect is fully implemented in Ada 2012 mode, but since it |
| requires the use of the aspect syntax, which is not available except in 2012 |
| mode, it is not possible to use the Type_Invariant aspect in earlier versions |
| of Ada. However the Invariant pragma may be used in any version of Ada. Also |
| note that the aspect Invariant is a synonym in GNAT for the aspect |
| Type_Invariant, but there is no pragma Type_Invariant. |
| |
| The pragma must appear within the visible part of the package specification, |
| after the type to which its Entity argument appears. As with the Invariant |
| aspect, the Check expression is not analyzed until the end of the visible |
| part of the package, so it may contain forward references. The Message |
| argument, if present, provides the exception message used if the invariant |
| is violated. If no Message parameter is provided, a default message that |
| identifies the line on which the pragma appears is used. |
| |
| It is permissible to have multiple Invariants for the same type entity, in |
| which case they are and'ed together. It is permissible to use this pragma |
| in Ada 2012 mode, but you cannot have both an invariant aspect and an |
| invariant pragma for the same entity. |
| |
| For further details on the use of this pragma, see the Ada 2012 documentation |
| of the Type_Invariant aspect. |
| |
| Pragma Java_Constructor |
| ======================= |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Java_Constructor ([Entity =>] function_LOCAL_NAME); |
| |
| |
| This pragma is used to assert that the specified Ada function should be |
| mapped to the Java constructor for some Ada tagged record type. |
| |
| See section 7.3.2 of the |
| `GNAT User's Guide: Supplement for the JVM Platform.` |
| for related information. |
| |
| Pragma Java_Interface |
| ===================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Java_Interface ([Entity =>] abstract_tagged_type_LOCAL_NAME); |
| |
| |
| This pragma is used to assert that the specified Ada abstract tagged type |
| is to be mapped to a Java interface name. |
| |
| See sections 7.1 and 7.2 of the |
| `GNAT User's Guide: Supplement for the JVM Platform.` |
| for related information. |
| |
| Pragma Keep_Names |
| ================= |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Keep_Names ([On =>] enumeration_first_subtype_LOCAL_NAME); |
| |
| |
| The `LOCAL_NAME` argument |
| must refer to an enumeration first subtype |
| in the current declarative part. The effect is to retain the enumeration |
| literal names for use by `Image` and `Value` even if a global |
| `Discard_Names` pragma applies. This is useful when you want to |
| generally suppress enumeration literal names and for example you therefore |
| use a `Discard_Names` pragma in the :file:`gnat.adc` file, but you |
| want to retain the names for specific enumeration types. |
| |
| Pragma License |
| ============== |
| .. index:: License checking |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma License (Unrestricted | GPL | Modified_GPL | Restricted); |
| |
| |
| This pragma is provided to allow automated checking for appropriate license |
| conditions with respect to the standard and modified GPL. A pragma |
| `License`, which is a configuration pragma that typically appears at |
| the start of a source file or in a separate :file:`gnat.adc` file, specifies |
| the licensing conditions of a unit as follows: |
| |
| * Unrestricted |
| This is used for a unit that can be freely used with no license restrictions. |
| Examples of such units are public domain units, and units from the Ada |
| Reference Manual. |
| |
| * GPL |
| This is used for a unit that is licensed under the unmodified GPL, and which |
| therefore cannot be `with`'ed by a restricted unit. |
| |
| * Modified_GPL |
| This is used for a unit licensed under the GNAT modified GPL that includes |
| a special exception paragraph that specifically permits the inclusion of |
| the unit in programs without requiring the entire program to be released |
| under the GPL. |
| |
| * Restricted |
| This is used for a unit that is restricted in that it is not permitted to |
| depend on units that are licensed under the GPL. Typical examples are |
| proprietary code that is to be released under more restrictive license |
| conditions. Note that restricted units are permitted to `with` units |
| which are licensed under the modified GPL (this is the whole point of the |
| modified GPL). |
| |
| |
| Normally a unit with no `License` pragma is considered to have an |
| unknown license, and no checking is done. However, standard GNAT headers |
| are recognized, and license information is derived from them as follows. |
| |
| A GNAT license header starts with a line containing 78 hyphens. The following |
| comment text is searched for the appearance of any of the following strings. |
| |
| If the string 'GNU General Public License' is found, then the unit is assumed |
| to have GPL license, unless the string 'As a special exception' follows, in |
| which case the license is assumed to be modified GPL. |
| |
| If one of the strings |
| 'This specification is adapted from the Ada Semantic Interface' or |
| 'This specification is derived from the Ada Reference Manual' is found |
| then the unit is assumed to be unrestricted. |
| |
| These default actions means that a program with a restricted license pragma |
| will automatically get warnings if a GPL unit is inappropriately |
| `with`'ed. For example, the program: |
| |
| .. code-block:: ada |
| |
| with Sem_Ch3; |
| with GNAT.Sockets; |
| procedure Secret_Stuff is |
| ... |
| end Secret_Stuff |
| |
| |
| if compiled with pragma `License` (`Restricted`) in a |
| :file:`gnat.adc` file will generate the warning:: |
| |
| 1. with Sem_Ch3; |
| | |
| >>> license of withed unit "Sem_Ch3" is incompatible |
| |
| 2. with GNAT.Sockets; |
| 3. procedure Secret_Stuff is |
| |
| |
| Here we get a warning on `Sem_Ch3` since it is part of the GNAT |
| compiler and is licensed under the |
| GPL, but no warning for `GNAT.Sockets` which is part of the GNAT |
| run time, and is therefore licensed under the modified GPL. |
| |
| Pragma Link_With |
| ================ |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Link_With (static_string_EXPRESSION {,static_string_EXPRESSION}); |
| |
| |
| This pragma is provided for compatibility with certain Ada 83 compilers. |
| It has exactly the same effect as pragma `Linker_Options` except |
| that spaces occurring within one of the string expressions are treated |
| as separators. For example, in the following case: |
| |
| .. code-block:: ada |
| |
| pragma Link_With ("-labc -ldef"); |
| |
| |
| results in passing the strings `-labc` and `-ldef` as two |
| separate arguments to the linker. In addition pragma Link_With allows |
| multiple arguments, with the same effect as successive pragmas. |
| |
| Pragma Linker_Alias |
| =================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Linker_Alias ( |
| [Entity =>] LOCAL_NAME, |
| [Target =>] static_string_EXPRESSION); |
| |
| |
| `LOCAL_NAME` must refer to an object that is declared at the library |
| level. This pragma establishes the given entity as a linker alias for the |
| given target. It is equivalent to `__attribute__((alias))` in GNU C |
| and causes `LOCAL_NAME` to be emitted as an alias for the symbol |
| `static_string_EXPRESSION` in the object file, that is to say no space |
| is reserved for `LOCAL_NAME` by the assembler and it will be resolved |
| to the same address as `static_string_EXPRESSION` by the linker. |
| |
| The actual linker name for the target must be used (e.g., the fully |
| encoded name with qualification in Ada, or the mangled name in C++), |
| or it must be declared using the C convention with `pragma Import` |
| or `pragma Export`. |
| |
| Not all target machines support this pragma. On some of them it is accepted |
| only if `pragma Weak_External` has been applied to `LOCAL_NAME`. |
| |
| |
| .. code-block:: ada |
| |
| -- Example of the use of pragma Linker_Alias |
| |
| package p is |
| i : Integer := 1; |
| pragma Export (C, i); |
| |
| new_name_for_i : Integer; |
| pragma Linker_Alias (new_name_for_i, "i"); |
| end p; |
| |
| |
| Pragma Linker_Constructor |
| ========================= |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Linker_Constructor (procedure_LOCAL_NAME); |
| |
| |
| `procedure_LOCAL_NAME` must refer to a parameterless procedure that |
| is declared at the library level. A procedure to which this pragma is |
| applied will be treated as an initialization routine by the linker. |
| It is equivalent to `__attribute__((constructor))` in GNU C and |
| causes `procedure_LOCAL_NAME` to be invoked before the entry point |
| of the executable is called (or immediately after the shared library is |
| loaded if the procedure is linked in a shared library), in particular |
| before the Ada run-time environment is set up. |
| |
| Because of these specific contexts, the set of operations such a procedure |
| can perform is very limited and the type of objects it can manipulate is |
| essentially restricted to the elementary types. In particular, it must only |
| contain code to which pragma Restrictions (No_Elaboration_Code) applies. |
| |
| This pragma is used by GNAT to implement auto-initialization of shared Stand |
| Alone Libraries, which provides a related capability without the restrictions |
| listed above. Where possible, the use of Stand Alone Libraries is preferable |
| to the use of this pragma. |
| |
| Pragma Linker_Destructor |
| ======================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Linker_Destructor (procedure_LOCAL_NAME); |
| |
| |
| `procedure_LOCAL_NAME` must refer to a parameterless procedure that |
| is declared at the library level. A procedure to which this pragma is |
| applied will be treated as a finalization routine by the linker. |
| It is equivalent to `__attribute__((destructor))` in GNU C and |
| causes `procedure_LOCAL_NAME` to be invoked after the entry point |
| of the executable has exited (or immediately before the shared library |
| is unloaded if the procedure is linked in a shared library), in particular |
| after the Ada run-time environment is shut down. |
| |
| See `pragma Linker_Constructor` for the set of restrictions that apply |
| because of these specific contexts. |
| |
| Pragma Linker_Section |
| ===================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Linker_Section ( |
| [Entity =>] LOCAL_NAME, |
| [Section =>] static_string_EXPRESSION); |
| |
| |
| `LOCAL_NAME` must refer to an object, type, or subprogram that is |
| declared at the library level. This pragma specifies the name of the |
| linker section for the given entity. It is equivalent to |
| `__attribute__((section))` in GNU C and causes `LOCAL_NAME` to |
| be placed in the `static_string_EXPRESSION` section of the |
| executable (assuming the linker doesn't rename the section). |
| GNAT also provides an implementation defined aspect of the same name. |
| |
| In the case of specifying this aspect for a type, the effect is to |
| specify the corresponding for all library level objects of the type which |
| do not have an explicit linker section set. Note that this only applies to |
| whole objects, not to components of composite objects. |
| |
| In the case of a subprogram, the linker section applies to all previously |
| declared matching overloaded subprograms in the current declarative part |
| which do not already have a linker section assigned. The linker section |
| aspect is useful in this case for specifying different linker sections |
| for different elements of such an overloaded set. |
| |
| Note that an empty string specifies that no linker section is specified. |
| This is not quite the same as omitting the pragma or aspect, since it |
| can be used to specify that one element of an overloaded set of subprograms |
| has the default linker section, or that one object of a type for which a |
| linker section is specified should has the default linker section. |
| |
| The compiler normally places library-level entities in standard sections |
| depending on the class: procedures and functions generally go in the |
| `.text` section, initialized variables in the `.data` section |
| and uninitialized variables in the `.bss` section. |
| |
| Other, special sections may exist on given target machines to map special |
| hardware, for example I/O ports or flash memory. This pragma is a means to |
| defer the final layout of the executable to the linker, thus fully working |
| at the symbolic level with the compiler. |
| |
| Some file formats do not support arbitrary sections so not all target |
| machines support this pragma. The use of this pragma may cause a program |
| execution to be erroneous if it is used to place an entity into an |
| inappropriate section (e.g., a modified variable into the `.text` |
| section). See also `pragma Persistent_BSS`. |
| |
| |
| .. code-block:: ada |
| |
| -- Example of the use of pragma Linker_Section |
| |
| package IO_Card is |
| Port_A : Integer; |
| pragma Volatile (Port_A); |
| pragma Linker_Section (Port_A, ".bss.port_a"); |
| |
| Port_B : Integer; |
| pragma Volatile (Port_B); |
| pragma Linker_Section (Port_B, ".bss.port_b"); |
| |
| type Port_Type is new Integer with Linker_Section => ".bss"; |
| PA : Port_Type with Linker_Section => ".bss.PA"; |
| PB : Port_Type; -- ends up in linker section ".bss" |
| |
| procedure Q with Linker_Section => "Qsection"; |
| end IO_Card; |
| |
| |
| Pragma Lock_Free |
| ================ |
| |
| Syntax: |
| This pragma may be specified for protected types or objects. It specifies that |
| the implementation of protected operations must be implemented without locks. |
| Compilation fails if the compiler cannot generate lock-free code for the |
| operations. |
| |
| Pragma Loop_Invariant |
| ===================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Loop_Invariant ( boolean_EXPRESSION ); |
| |
| |
| The effect of this pragma is similar to that of pragma `Assert`, |
| except that in an `Assertion_Policy` pragma, the identifier |
| `Loop_Invariant` is used to control whether it is ignored or checked |
| (or disabled). |
| |
| `Loop_Invariant` can only appear as one of the items in the sequence |
| of statements of a loop body, or nested inside block statements that |
| appear in the sequence of statements of a loop body. |
| The intention is that it be used to |
| represent a "loop invariant" assertion, i.e. something that is true each |
| time through the loop, and which can be used to show that the loop is |
| achieving its purpose. |
| |
| Multiple `Loop_Invariant` and `Loop_Variant` pragmas that |
| apply to the same loop should be grouped in the same sequence of |
| statements. |
| |
| To aid in writing such invariants, the special attribute `Loop_Entry` |
| may be used to refer to the value of an expression on entry to the loop. This |
| attribute can only be used within the expression of a `Loop_Invariant` |
| pragma. For full details, see documentation of attribute `Loop_Entry`. |
| |
| Pragma Loop_Optimize |
| ==================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Loop_Optimize (OPTIMIZATION_HINT {, OPTIMIZATION_HINT}); |
| |
| OPTIMIZATION_HINT ::= Ivdep | No_Unroll | Unroll | No_Vector | Vector |
| |
| |
| This pragma must appear immediately within a loop statement. It allows the |
| programmer to specify optimization hints for the enclosing loop. The hints |
| are not mutually exclusive and can be freely mixed, but not all combinations |
| will yield a sensible outcome. |
| |
| There are five supported optimization hints for a loop: |
| |
| * Ivdep |
| |
| The programmer asserts that there are no loop-carried dependencies |
| which would prevent consecutive iterations of the loop from being |
| executed simultaneously. |
| |
| * No_Unroll |
| |
| The loop must not be unrolled. This is a strong hint: the compiler will not |
| unroll a loop marked with this hint. |
| |
| * Unroll |
| |
| The loop should be unrolled. This is a weak hint: the compiler will try to |
| apply unrolling to this loop preferably to other optimizations, notably |
| vectorization, but there is no guarantee that the loop will be unrolled. |
| |
| * No_Vector |
| |
| The loop must not be vectorized. This is a strong hint: the compiler will not |
| vectorize a loop marked with this hint. |
| |
| * Vector |
| |
| The loop should be vectorized. This is a weak hint: the compiler will try to |
| apply vectorization to this loop preferably to other optimizations, notably |
| unrolling, but there is no guarantee that the loop will be vectorized. |
| |
| |
| These hints do not remove the need to pass the appropriate switches to the |
| compiler in order to enable the relevant optimizations, that is to say |
| *-funroll-loops* for unrolling and *-ftree-vectorize* for |
| vectorization. |
| |
| Pragma Loop_Variant |
| =================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Loop_Variant ( LOOP_VARIANT_ITEM {, LOOP_VARIANT_ITEM } ); |
| LOOP_VARIANT_ITEM ::= CHANGE_DIRECTION => discrete_EXPRESSION |
| CHANGE_DIRECTION ::= Increases | Decreases |
| |
| |
| `Loop_Variant` can only appear as one of the items in the sequence |
| of statements of a loop body, or nested inside block statements that |
| appear in the sequence of statements of a loop body. |
| It allows the specification of quantities which must always |
| decrease or increase in successive iterations of the loop. In its simplest |
| form, just one expression is specified, whose value must increase or decrease |
| on each iteration of the loop. |
| |
| In a more complex form, multiple arguments can be given which are intepreted |
| in a nesting lexicographic manner. For example: |
| |
| .. code-block:: ada |
| |
| pragma Loop_Variant (Increases => X, Decreases => Y); |
| |
| |
| specifies that each time through the loop either X increases, or X stays |
| the same and Y decreases. A `Loop_Variant` pragma ensures that the |
| loop is making progress. It can be useful in helping to show informally |
| or prove formally that the loop always terminates. |
| |
| `Loop_Variant` is an assertion whose effect can be controlled using |
| an `Assertion_Policy` with a check name of `Loop_Variant`. The |
| policy can be `Check` to enable the loop variant check, `Ignore` |
| to ignore the check (in which case the pragma has no effect on the program), |
| or `Disable` in which case the pragma is not even checked for correct |
| syntax. |
| |
| Multiple `Loop_Invariant` and `Loop_Variant` pragmas that |
| apply to the same loop should be grouped in the same sequence of |
| statements. |
| |
| The `Loop_Entry` attribute may be used within the expressions of the |
| `Loop_Variant` pragma to refer to values on entry to the loop. |
| |
| Pragma Machine_Attribute |
| ======================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Machine_Attribute ( |
| [Entity =>] LOCAL_NAME, |
| [Attribute_Name =>] static_string_EXPRESSION |
| [, [Info =>] static_EXPRESSION] ); |
| |
| |
| Machine-dependent attributes can be specified for types and/or |
| declarations. This pragma is semantically equivalent to |
| `__attribute__((`attribute_name`))` (if `info` is not |
| specified) or `__attribute__((`attribute_name`(`info`))) |
| in GNU C, where ``attribute_name`` is recognized by the |
| compiler middle-end or the `TARGET_ATTRIBUTE_TABLE` machine |
| specific macro. A string literal for the optional parameter `info` |
| is transformed into an identifier, which may make this pragma unusable |
| for some attributes. |
| For further information see :title:`GNU Compiler Collection (GCC) Internals`. |
| |
| Pragma Main |
| =========== |
| |
| Syntax:: |
| |
| pragma Main |
| (MAIN_OPTION [, MAIN_OPTION]); |
| |
| MAIN_OPTION ::= |
| [Stack_Size =>] static_integer_EXPRESSION |
| | [Task_Stack_Size_Default =>] static_integer_EXPRESSION |
| | [Time_Slicing_Enabled =>] static_boolean_EXPRESSION |
| |
| |
| This pragma is provided for compatibility with OpenVMS VAX Systems. It has |
| no effect in GNAT, other than being syntax checked. |
| |
| Pragma Main_Storage |
| =================== |
| |
| Syntax:: |
| |
| pragma Main_Storage |
| (MAIN_STORAGE_OPTION [, MAIN_STORAGE_OPTION]); |
| |
| MAIN_STORAGE_OPTION ::= |
| [WORKING_STORAGE =>] static_SIMPLE_EXPRESSION |
| | [TOP_GUARD =>] static_SIMPLE_EXPRESSION |
| |
| |
| This pragma is provided for compatibility with OpenVMS VAX Systems. It has |
| no effect in GNAT, other than being syntax checked. |
| |
| Pragma No_Body |
| ============== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma No_Body; |
| |
| |
| There are a number of cases in which a package spec does not require a body, |
| and in fact a body is not permitted. GNAT will not permit the spec to be |
| compiled if there is a body around. The pragma No_Body allows you to provide |
| a body file, even in a case where no body is allowed. The body file must |
| contain only comments and a single No_Body pragma. This is recognized by |
| the compiler as indicating that no body is logically present. |
| |
| This is particularly useful during maintenance when a package is modified in |
| such a way that a body needed before is no longer needed. The provision of a |
| dummy body with a No_Body pragma ensures that there is no interference from |
| earlier versions of the package body. |
| |
| Pragma No_Elaboration_Code_All |
| ============================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma No_Elaboration_Code_All [(program_unit_NAME)]; |
| |
| |
| This is a program unit pragma (there is also an equivalent aspect of the |
| same name) that establishes the restriction `No_Elaboration_Code` for |
| the current unit and any extended main source units (body and subunits. |
| It also has has the effect of enforcing a transitive application of this |
| aspect, so that if any unit is implicitly or explicitly WITH'ed by the |
| current unit, it must also have the No_Elaboration_Code_All aspect set. |
| It may be applied to package or subprogram specs or their generic versions. |
| |
| Pragma No_Inline |
| ================ |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma No_Inline (NAME {, NAME}); |
| |
| |
| This pragma suppresses inlining for the callable entity or the instances of |
| the generic subprogram designated by `NAME`, including inlining that |
| results from the use of pragma `Inline`. This pragma is always active, |
| in particular it is not subject to the use of option *-gnatn* or |
| *-gnatN*. It is illegal to specify both pragma `No_Inline` and |
| pragma `Inline_Always` for the same `NAME`. |
| |
| Pragma No_Return |
| ================ |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma No_Return (procedure_LOCAL_NAME {, procedure_LOCAL_NAME}); |
| |
| |
| Each `procedure_LOCAL_NAME` argument must refer to one or more procedure |
| declarations in the current declarative part. A procedure to which this |
| pragma is applied may not contain any explicit `return` statements. |
| In addition, if the procedure contains any implicit returns from falling |
| off the end of a statement sequence, then execution of that implicit |
| return will cause Program_Error to be raised. |
| |
| One use of this pragma is to identify procedures whose only purpose is to raise |
| an exception. Another use of this pragma is to suppress incorrect warnings |
| about missing returns in functions, where the last statement of a function |
| statement sequence is a call to such a procedure. |
| |
| Note that in Ada 2005 mode, this pragma is part of the language. It is |
| 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 |
| ========================= |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma No_Strict_Aliasing [([Entity =>] type_LOCAL_NAME)]; |
| |
| |
| `type_LOCAL_NAME` must refer to an access type |
| declaration in the current declarative part. The effect is to inhibit |
| strict aliasing optimization for the given type. The form with no |
| arguments is a configuration pragma which applies to all access types |
| declared in units to which the pragma applies. For a detailed |
| description of the strict aliasing optimization, and the situations |
| in which it must be suppressed, see the section on Optimization and Strict Aliasing |
| in the :title:`GNAT User's Guide`. |
| |
| This pragma currently has no effects on access to unconstrained array types. |
| |
| Pragma No_Tagged_Streams |
| ======================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma No_Tagged_Streams; |
| pragma No_Tagged_Streams [([Entity =>] tagged_type_LOCAL_NAME)]; |
| |
| |
| Normally when a tagged type is introduced using a full type declaration, |
| part of the processing includes generating stream access routines to be |
| used by stream attributes referencing the type (or one of its subtypes |
| or derived types). This can involve the generation of significant amounts |
| of code which is wasted space if stream routines are not needed for the |
| type in question. |
| |
| The `No_Tagged_Streams` pragma causes the generation of these stream |
| routines to be skipped, and any attempt to use stream operations on |
| types subject to this pragma will be statically rejected as illegal. |
| |
| There are two forms of the pragma. The form with no arguments must appear |
| in a declarative sequence or in the declarations of a package spec. This |
| pragma affects all subsequent root tagged types declared in the declaration |
| sequence, and specifies that no stream routines be generated. The form with |
| an argument (for which there is also a corresponding aspect) specifies a |
| single root tagged type for which stream routines are not to be generated. |
| |
| Once the pragma has been given for a particular root tagged type, all subtypes |
| and derived types of this type inherit the pragma automatically, so the effect |
| applies to a complete hierarchy (this is necessary to deal with the class-wide |
| dispatching versions of the stream routines). |
| |
| Pragma Normalize_Scalars |
| ======================== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Normalize_Scalars; |
| |
| |
| This is a language defined pragma which is fully implemented in GNAT. The |
| effect is to cause all scalar objects that are not otherwise initialized |
| to be initialized. The initial values are implementation dependent and |
| are as follows: |
| |
| |
| |
| *Standard.Character* |
| Objects whose root type is Standard.Character are initialized to |
| Character'Last unless the subtype range excludes NUL (in which case |
| NUL is used). This choice will always generate an invalid value if |
| one exists. |
| |
| |
| *Standard.Wide_Character* |
| Objects whose root type is Standard.Wide_Character are initialized to |
| Wide_Character'Last unless the subtype range excludes NUL (in which case |
| NUL is used). This choice will always generate an invalid value if |
| one exists. |
| |
| |
| *Standard.Wide_Wide_Character* |
| Objects whose root type is Standard.Wide_Wide_Character are initialized to |
| the invalid value 16#FFFF_FFFF# unless the subtype range excludes NUL (in |
| which case NUL is used). This choice will always generate an invalid value if |
| one exists. |
| |
| |
| *Integer types* |
| Objects of an integer type are treated differently depending on whether |
| negative values are present in the subtype. If no negative values are |
| present, then all one bits is used as the initial value except in the |
| special case where zero is excluded from the subtype, in which case |
| all zero bits are used. This choice will always generate an invalid |
| value if one exists. |
| |
| For subtypes with negative values present, the largest negative number |
| is used, except in the unusual case where this largest negative number |
| is in the subtype, and the largest positive number is not, in which case |
| the largest positive value is used. This choice will always generate |
| an invalid value if one exists. |
| |
| |
| *Floating-Point Types* |
| Objects of all floating-point types are initialized to all 1-bits. For |
| standard IEEE format, this corresponds to a NaN (not a number) which is |
| indeed an invalid value. |
| |
| |
| *Fixed-Point Types* |
| Objects of all fixed-point types are treated as described above for integers, |
| with the rules applying to the underlying integer value used to represent |
| the fixed-point value. |
| |
| |
| *Modular types* |
| Objects of a modular type are initialized to all one bits, except in |
| the special case where zero is excluded from the subtype, in which |
| case all zero bits are used. This choice will always generate an |
| invalid value if one exists. |
| |
| |
| *Enumeration types* |
| Objects of an enumeration type are initialized to all one-bits, i.e., to |
| the value `2 ** typ'Size - 1` unless the subtype excludes the literal |
| whose Pos value is zero, in which case a code of zero is used. This choice |
| will always generate an invalid value if one exists. |
| |
| .. _Pragma_Obsolescent: |
| |
| Pragma Obsolescent |
| ================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Obsolescent; |
| |
| pragma Obsolescent ( |
| [Message =>] static_string_EXPRESSION |
| [,[Version =>] Ada_05]]); |
| |
| pragma Obsolescent ( |
| [Entity =>] NAME |
| [,[Message =>] static_string_EXPRESSION |
| [,[Version =>] Ada_05]] ); |
| |
| |
| This pragma can occur immediately following a declaration of an entity, |
| including the case of a record component. If no Entity argument is present, |
| then this declaration is the one to which the pragma applies. If an Entity |
| parameter is present, it must either match the name of the entity in this |
| declaration, or alternatively, the pragma can immediately follow an enumeration |
| type declaration, where the Entity argument names one of the enumeration |
| literals. |
| |
| This pragma is used to indicate that the named entity |
| is considered obsolescent and should not be used. Typically this is |
| used when an API must be modified by eventually removing or modifying |
| existing subprograms or other entities. The pragma can be used at an |
| intermediate stage when the entity is still present, but will be |
| removed later. |
| |
| The effect of this pragma is to output a warning message on a reference to |
| an entity thus marked that the subprogram is obsolescent if the appropriate |
| warning option in the compiler is activated. If the Message parameter is |
| present, then a second warning message is given containing this text. In |
| addition, a reference to the entity is considered to be a violation of pragma |
| Restrictions (No_Obsolescent_Features). |
| |
| This pragma can also be used as a program unit pragma for a package, |
| in which case the entity name is the name of the package, and the |
| pragma indicates that the entire package is considered |
| obsolescent. In this case a client `with`'ing such a package |
| violates the restriction, and the `with` statement is |
| flagged with warnings if the warning option is set. |
| |
| If the Version parameter is present (which must be exactly |
| the identifier Ada_05, no other argument is allowed), then the |
| indication of obsolescence applies only when compiling in Ada 2005 |
| mode. This is primarily intended for dealing with the situations |
| in the predefined library where subprograms or packages |
| have become defined as obsolescent in Ada 2005 |
| (e.g., in Ada.Characters.Handling), but may be used anywhere. |
| |
| The following examples show typical uses of this pragma: |
| |
| |
| .. code-block:: ada |
| |
| package p is |
| pragma Obsolescent (p, Message => "use pp instead of p"); |
| end p; |
| |
| package q is |
| procedure q2; |
| pragma Obsolescent ("use q2new instead"); |
| |
| type R is new integer; |
| pragma Obsolescent |
| (Entity => R, |
| Message => "use RR in Ada 2005", |
| Version => Ada_05); |
| |
| type M is record |
| F1 : Integer; |
| F2 : Integer; |
| pragma Obsolescent; |
| F3 : Integer; |
| end record; |
| |
| type E is (a, bc, 'd', quack); |
| pragma Obsolescent (Entity => bc) |
| pragma Obsolescent (Entity => 'd') |
| |
| function "+" |
| (a, b : character) return character; |
| pragma Obsolescent (Entity => "+"); |
| end; |
| |
| |
| Note that, as for all pragmas, if you use a pragma argument identifier, |
| then all subsequent parameters must also use a pragma argument identifier. |
| So if you specify "Entity =>" for the Entity argument, and a Message |
| argument is present, it must be preceded by "Message =>". |
| |
| Pragma Optimize_Alignment |
| ========================= |
| .. index:: Alignment, default settings |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Optimize_Alignment (TIME | SPACE | OFF); |
| |
| |
| This is a configuration pragma which affects the choice of default alignments |
| for types and objects where no alignment is explicitly specified. There is a |
| time/space trade-off in the selection of these values. Large alignments result |
| in more efficient code, at the expense of larger data space, since sizes have |
| to be increased to match these alignments. Smaller alignments save space, but |
| the access code is slower. The normal choice of default alignments for types |
| and individual alignment promotions for objects (which is what you get if you |
| do not use this pragma, or if you use an argument of OFF), tries to balance |
| these two requirements. |
| |
| Specifying SPACE causes smaller default alignments to be chosen in two cases. |
| First any packed record is given an alignment of 1. Second, if a size is given |
| for the type, then the alignment is chosen to avoid increasing this size. For |
| example, consider: |
| |
| |
| .. code-block:: ada |
| |
| type R is record |
| X : Integer; |
| Y : Character; |
| end record; |
| |
| for R'Size use 5*8; |
| |
| |
| In the default mode, this type gets an alignment of 4, so that access to the |
| Integer field X are efficient. But this means that objects of the type end up |
| with a size of 8 bytes. This is a valid choice, since sizes of objects are |
| allowed to be bigger than the size of the type, but it can waste space if for |
| example fields of type R appear in an enclosing record. If the above type is |
| compiled in `Optimize_Alignment (Space)` mode, the alignment is set to 1. |
| |
| However, there is one case in which SPACE is ignored. If a variable length |
| record (that is a discriminated record with a component which is an array |
| whose length depends on a discriminant), has a pragma Pack, then it is not |
| in general possible to set the alignment of such a record to one, so the |
| pragma is ignored in this case (with a warning). |
| |
| Specifying SPACE also disables alignment promotions for standalone objects, |
| which occur when the compiler increases the alignment of a specific object |
| without changing the alignment of its type. |
| |
| Specifying TIME causes larger default alignments to be chosen in the case of |
| small types with sizes that are not a power of 2. For example, consider: |
| |
| |
| .. code-block:: ada |
| |
| type R is record |
| A : Character; |
| B : Character; |
| C : Boolean; |
| end record; |
| |
| pragma Pack (R); |
| for R'Size use 17; |
| |
| |
| The default alignment for this record is normally 1, but if this type is |
| compiled in `Optimize_Alignment (Time)` mode, then the alignment is set |
| to 4, which wastes space for objects of the type, since they are now 4 bytes |
| long, but results in more efficient access when the whole record is referenced. |
| |
| As noted above, this is a configuration pragma, and there is a requirement |
| that all units in a partition be compiled with a consistent setting of the |
| optimization setting. This would normally be achieved by use of a configuration |
| pragma file containing the appropriate setting. The exception to this rule is |
| that units with an explicit configuration pragma in the same file as the source |
| unit are excluded from the consistency check, as are all predefined units. The |
| latter are compiled by default in pragma Optimize_Alignment (Off) mode if no |
| pragma appears at the start of the file. |
| |
| Pragma Ordered |
| ============== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Ordered (enumeration_first_subtype_LOCAL_NAME); |
| |
| |
| Most enumeration types are from a conceptual point of view unordered. |
| For example, consider: |
| |
| |
| .. code-block:: ada |
| |
| type Color is (Red, Blue, Green, Yellow); |
| |
| |
| By Ada semantics `Blue > Red` and `Green > Blue`, |
| but really these relations make no sense; the enumeration type merely |
| specifies a set of possible colors, and the order is unimportant. |
| |
| For unordered enumeration types, it is generally a good idea if |
| clients avoid comparisons (other than equality or inequality) and |
| explicit ranges. (A *client* is a unit where the type is referenced, |
| other than the unit where the type is declared, its body, and its subunits.) |
| For example, if code buried in some client says: |
| |
| |
| .. code-block:: ada |
| |
| if Current_Color < Yellow then ... |
| if Current_Color in Blue .. Green then ... |
| |
| |
| then the client code is relying on the order, which is undesirable. |
| It makes the code hard to read and creates maintenance difficulties if |
| entries have to be added to the enumeration type. Instead, |
| the code in the client should list the possibilities, or an |
| appropriate subtype should be declared in the unit that declares |
| the original enumeration type. E.g., the following subtype could |
| be declared along with the type `Color`: |
| |
| |
| .. code-block:: ada |
| |
| subtype RBG is Color range Red .. Green; |
| |
| |
| and then the client could write: |
| |
| |
| .. code-block:: ada |
| |
| if Current_Color in RBG then ... |
| if Current_Color = Blue or Current_Color = Green then ... |
| |
| |
| However, some enumeration types are legitimately ordered from a conceptual |
| point of view. For example, if you declare: |
| |
| |
| .. code-block:: ada |
| |
| type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun); |
| |
| |
| then the ordering imposed by the language is reasonable, and |
| clients can depend on it, writing for example: |
| |
| |
| .. code-block:: ada |
| |
| if D in Mon .. Fri then ... |
| if D < Wed then ... |
| |
| |
| The pragma *Ordered* is provided to mark enumeration types that |
| are conceptually ordered, alerting the reader that clients may depend |
| on the ordering. GNAT provides a pragma to mark enumerations as ordered |
| rather than one to mark them as unordered, since in our experience, |
| the great majority of enumeration types are conceptually unordered. |
| |
| The types `Boolean`, `Character`, `Wide_Character`, |
| and `Wide_Wide_Character` |
| are considered to be ordered types, so each is declared with a |
| pragma `Ordered` in package `Standard`. |
| |
| Normally pragma `Ordered` serves only as documentation and a guide for |
| coding standards, but GNAT provides a warning switch *-gnatw.u* that |
| requests warnings for inappropriate uses (comparisons and explicit |
| subranges) for unordered types. If this switch is used, then any |
| enumeration type not marked with pragma `Ordered` will be considered |
| as unordered, and will generate warnings for inappropriate uses. |
| |
| Note that generic types are not considered ordered or unordered (since the |
| template can be instantiated for both cases), so we never generate warnings |
| for the case of generic enumerated types. |
| |
| For additional information please refer to the description of the |
| *-gnatw.u* switch in the GNAT User's Guide. |
| |
| Pragma Overflow_Mode |
| ==================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Overflow_Mode |
| ( [General =>] MODE |
| [,[Assertions =>] MODE]); |
| |
| MODE ::= STRICT | MINIMIZED | ELIMINATED |
| |
| |
| This pragma sets the current overflow mode to the given setting. For details |
| of the meaning of these modes, please refer to the |
| 'Overflow Check Handling in GNAT' appendix in the |
| GNAT User's Guide. If only the `General` parameter is present, |
| the given mode applies to all expressions. If both parameters are present, |
| the `General` mode applies to expressions outside assertions, and |
| the `Eliminated` mode applies to expressions within assertions. |
| |
| The case of the `MODE` parameter is ignored, |
| so `MINIMIZED`, `Minimized` and |
| `minimized` all have the same effect. |
| |
| The `Overflow_Mode` pragma has the same scoping and placement |
| rules as pragma `Suppress`, so it can occur either as a |
| configuration pragma, specifying a default for the whole |
| program, or in a declarative scope, where it applies to the |
| remaining declarations and statements in that scope. |
| |
| The pragma `Suppress (Overflow_Check)` suppresses |
| overflow checking, but does not affect the overflow mode. |
| |
| The pragma `Unsuppress (Overflow_Check)` unsuppresses (enables) |
| overflow checking, but does not affect the overflow mode. |
| |
| Pragma Overriding_Renamings |
| =========================== |
| .. index:: Rational profile |
| |
| .. index:: Rational compatibility |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Overriding_Renamings; |
| |
| |
| This is a GNAT configuration pragma to simplify porting |
| legacy code accepted by the Rational |
| Ada compiler. In the presence of this pragma, a renaming declaration that |
| renames an inherited operation declared in the same scope is legal if selected |
| notation is used as in: |
| |
| |
| .. code-block:: ada |
| |
| pragma Overriding_Renamings; |
| ... |
| package R is |
| function F (..); |
| ... |
| function F (..) renames R.F; |
| end R; |
| |
| |
| even though |
| RM 8.3 (15) stipulates that an overridden operation is not visible within the |
| declaration of the overriding operation. |
| |
| Pragma Partition_Elaboration_Policy |
| =================================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Partition_Elaboration_Policy (POLICY_IDENTIFIER); |
| |
| POLICY_IDENTIFIER ::= Concurrent | Sequential |
| |
| |
| This pragma is standard in Ada 2005, but is available in all earlier |
| versions of Ada as an implementation-defined pragma. |
| See Ada 2012 Reference Manual for details. |
| |
| Pragma Part_Of |
| ============== |
| |
| For the description of this pragma, see SPARK 2014 Reference Manual, |
| section 7.2.6. |
| |
| Pragma Passive |
| ============== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Passive [(Semaphore | No)]; |
| |
| |
| Syntax checked, but otherwise ignored by GNAT. This is recognized for |
| compatibility with DEC Ada 83 implementations, where it is used within a |
| task definition to request that a task be made passive. If the argument |
| `Semaphore` is present, or the argument is omitted, then DEC Ada 83 |
| treats the pragma as an assertion that the containing task is passive |
| and that optimization of context switch with this task is permitted and |
| desired. If the argument `No` is present, the task must not be |
| optimized. GNAT does not attempt to optimize any tasks in this manner |
| (since protected objects are available in place of passive tasks). |
| |
| For more information on the subject of passive tasks, see the section |
| 'Passive Task Optimization' in the GNAT Users Guide. |
| |
| Pragma Persistent_BSS |
| ===================== |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Persistent_BSS [(LOCAL_NAME)] |
| |
| |
| This pragma allows selected objects to be placed in the `.persistent_bss` |
| section. On some targets the linker and loader provide for special |
| treatment of this section, allowing a program to be reloaded without |
| affecting the contents of this data (hence the name persistent). |
| |
| There are two forms of usage. If an argument is given, it must be the |
| local name of a library level object, with no explicit initialization |
| and whose type is potentially persistent. If no argument is given, then |
| the pragma is a configuration pragma, and applies to all library level |
| objects with no explicit initialization of potentially persistent types. |
| |
| A potentially persistent type is a scalar type, or an untagged, |
| non-discriminated record, all of whose components have no explicit |
| initialization and are themselves of a potentially persistent type, |
| or an array, all of whose constraints are static, and whose component |
| type is potentially persistent. |
| |
| If this pragma is used on a target where this feature is not supported, |
| then the pragma will be ignored. See also `pragma Linker_Section`. |
| |
| Pragma Polling |
| ============== |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Polling (ON | OFF); |
| |
| |
| This pragma controls the generation of polling code. This is normally off. |
| If `pragma Polling (ON)` is used then periodic calls are generated to |
| the routine `Ada.Exceptions.Poll`. This routine is a separate unit in the |
| runtime library, and can be found in file :file:`a-excpol.adb`. |
| |
| Pragma `Polling` can appear as a configuration pragma (for example it |
| can be placed in the :file:`gnat.adc` file) to enable polling globally, or it |
| can be used in the statement or declaration sequence to control polling |
| more locally. |
| |
| A call to the polling routine is generated at the start of every loop and |
| at the start of every subprogram call. This guarantees that the `Poll` |
| routine is called frequently, and places an upper bound (determined by |
| the complexity of the code) on the period between two `Poll` calls. |
| |
| The primary purpose of the polling interface is to enable asynchronous |
| aborts on targets that cannot otherwise support it (for example Windows |
| NT), but it may be used for any other purpose requiring periodic polling. |
| The standard version is null, and can be replaced by a user program. This |
| will require re-compilation of the `Ada.Exceptions` package that can |
| be found in files :file:`a-except.ads` and :file:`a-except.adb`. |
| |
| A standard alternative unit (in file :file:`4wexcpol.adb` in the standard GNAT |
| distribution) is used to enable the asynchronous abort capability on |
| targets that do not normally support the capability. The version of |
| `Poll` in this file makes a call to the appropriate runtime routine |
| to test for an abort condition. |
| |
| Note that polling can also be enabled by use of the *-gnatP* switch. |
| See the section on switches for gcc in the :title:`GNAT User's Guide`. |
| |
| Pragma Post |
| =========== |
| .. index:: Post |
| |
| .. index:: Checks, postconditions |
| |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Post (Boolean_Expression); |
| |
| |
| The `Post` pragma is intended to be an exact replacement for |
| the language-defined |
| `Post` aspect, and shares its restrictions and semantics. |
| It must appear either immediately following the corresponding |
| subprogram declaration (only other pragmas may intervene), or |
| if there is no separate subprogram declaration, then it can |
| appear at the start of the declarations in a subprogram body |
| (preceded only by other pragmas). |
| |
| Pragma Postcondition |
| ==================== |
| .. index:: Postcondition |
| |
| .. index:: Checks, postconditions |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Postcondition ( |
| [Check =>] Boolean_Expression |
| [,[Message =>] String_Expression]); |
| |
| |
| The `Postcondition` pragma allows specification of automatic |
| postcondition checks for subprograms. These checks are similar to |
| assertions, but are automatically inserted just prior to the return |
| statements of the subprogram with which they are associated (including |
| implicit returns at the end of procedure bodies and associated |
| exception handlers). |
| |
| In addition, the boolean expression which is the condition which |
| must be true may contain references to function'Result in the case |
| of a function to refer to the returned value. |
| |
| `Postcondition` pragmas may appear either immediately following the |
| (separate) declaration of a subprogram, or at the start of the |
| declarations of a subprogram body. Only other pragmas may intervene |
| (that is appear between the subprogram declaration and its |
| postconditions, or appear before the postcondition in the |
| declaration sequence in a subprogram body). In the case of a |
| postcondition appearing after a subprogram declaration, the |
| formal arguments of the subprogram are visible, and can be |
| referenced in the postcondition expressions. |
| |
| The postconditions are collected and automatically tested just |
| before any return (implicit or explicit) in the subprogram body. |
| A postcondition is only recognized if postconditions are active |
| at the time the pragma is encountered. The compiler switch *gnata* |
| turns on all postconditions by default, and pragma `Check_Policy` |
| with an identifier of `Postcondition` can also be used to |
| control whether postconditions are active. |
| |
| The general approach is that postconditions are placed in the spec |
| if they represent functional aspects which make sense to the client. |
| For example we might have: |
| |
| |
| .. code-block:: ada |
| |
| function Direction return Integer; |
| pragma Postcondition |
| (Direction'Result = +1 |
| or else |
| Direction'Result = -1); |
| |
| |
| which serves to document that the result must be +1 or -1, and |
| will test that this is the case at run time if postcondition |
| checking is active. |
| |
| Postconditions within the subprogram body can be used to |
| check that some internal aspect of the implementation, |
| not visible to the client, is operating as expected. |
| For instance if a square root routine keeps an internal |
| counter of the number of times it is called, then we |
| might have the following postcondition: |
| |
| |
| .. code-block:: ada |
| |
| Sqrt_Calls : Natural := 0; |
| |
| function Sqrt (Arg : Float) return Float is |
| pragma Postcondition |
| (Sqrt_Calls = Sqrt_Calls'Old + 1); |
| ... |
| end Sqrt |
| |
| |
| As this example, shows, the use of the `Old` attribute |
| is often useful in postconditions to refer to the state on |
| entry to the subprogram. |
| |
| Note that postconditions are only checked on normal returns |
| from the subprogram. If an abnormal return results from |
| raising an exception, then the postconditions are not checked. |
| |
| If a postcondition fails, then the exception |
| `System.Assertions.Assert_Failure` is raised. If |
| a message argument was supplied, then the given string |
| will be used as the exception message. If no message |
| argument was supplied, then the default message has |
| the form "Postcondition failed at file_name:line". The |
| exception is raised in the context of the subprogram |
| body, so it is possible to catch postcondition failures |
| within the subprogram body itself. |
| |
| Within a package spec, normal visibility rules |
| in Ada would prevent forward references within a |
| postcondition pragma to functions defined later in |
| the same package. This would introduce undesirable |
| ordering constraints. To avoid this problem, all |
| postcondition pragmas are analyzed at the end of |
| the package spec, allowing forward references. |
| |
| The following example shows that this even allows |
| mutually recursive postconditions as in: |
| |
| |
| .. code-block:: ada |
| |
| package Parity_Functions is |
| function Odd (X : Natural) return Boolean; |
| pragma Postcondition |
| (Odd'Result = |
| (x = 1 |
| or else |
| (x /= 0 and then Even (X - 1)))); |
| |
| function Even (X : Natural) return Boolean; |
| pragma Postcondition |
| (Even'Result = |
| (x = 0 |
| or else |
| (x /= 1 and then Odd (X - 1)))); |
| |
| end Parity_Functions; |
| |
| |
| There are no restrictions on the complexity or form of |
| conditions used within `Postcondition` pragmas. |
| The following example shows that it is even possible |
| to verify performance behavior. |
| |
| |
| .. code-block:: ada |
| |
| package Sort is |
| |
| Performance : constant Float; |
| -- Performance constant set by implementation |
| -- to match target architecture behavior. |
| |
| procedure Treesort (Arg : String); |
| -- Sorts characters of argument using N*logN sort |
| pragma Postcondition |
| (Float (Clock - Clock'Old) <= |
| Float (Arg'Length) * |
| log (Float (Arg'Length)) * |
| Performance); |
| end Sort; |
| |
| |
| Note: postcondition pragmas associated with subprograms that are |
| marked as Inline_Always, or those marked as Inline with front-end |
| inlining (-gnatN option set) are accepted and legality-checked |
| by the compiler, but are ignored at run-time even if postcondition |
| checking is enabled. |
| |
| Note that pragma `Postcondition` differs from the language-defined |
| `Post` aspect (and corresponding `Post` pragma) in allowing |
| multiple occurrences, allowing occurences in the body even if there |
| is a separate spec, and allowing a second string parameter, and the |
| use of the pragma identifier `Check`. Historically, pragma |
| `Postcondition` was implemented prior to the development of |
| Ada 2012, and has been retained in its original form for |
| compatibility purposes. |
| |
| Pragma Post_Class |
| ================= |
| .. index:: Post |
| |
| .. index:: Checks, postconditions |
| |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Post_Class (Boolean_Expression); |
| |
| |
| The `Post_Class` pragma is intended to be an exact replacement for |
| the language-defined |
| `Post'Class` aspect, and shares its restrictions and semantics. |
| It must appear either immediately following the corresponding |
| subprogram declaration (only other pragmas may intervene), or |
| if there is no separate subprogram declaration, then it can |
| appear at the start of the declarations in a subprogram body |
| (preceded only by other pragmas). |
| |
| Note: This pragma is called `Post_Class` rather than |
| `Post'Class` because the latter would not be strictly |
| conforming to the allowed syntax for pragmas. The motivation |
| for provinding pragmas equivalent to the aspects is to allow a program |
| to be written using the pragmas, and then compiled if necessary |
| using an Ada compiler that does not recognize the pragmas or |
| aspects, but is prepared to ignore the pragmas. The assertion |
| policy that controls this pragma is `Post'Class`, not |
| `Post_Class`. |
| |
| Pragma Pre |
| ========== |
| .. index:: Pre |
| |
| .. index:: Checks, preconditions |
| |
| |
| Syntax: |
| |
| |
| .. code-block:: ada |
| |
| pragma Pre (Boolean_Expression); |
| |
| |
| The `Pre` pragma is intended to be an exact replacement for |
| the language-defined |
| `Pre` aspect, and shares its restrictions and semantics. |
| It must appear either immediately following the corresponding |
| subprogram declaration (only other pragmas may intervene), or |
| if there is no separate subprogram declaration, then it can |
| appear at the start of the declarations in a subprogram body |
| (preceded only by other pragmas). |
| |
| Pragma Precondition |
| =================== |
| .. index:: Preconditions |
| |
| .. index:: Checks, preconditions |
| |
| |
| Syntax: |
| |
| |
| :: |
| |
| pragma Precondition ( |
| [Check =>] Boolean_Expression |
| [,[Message =>] String_Expression]); |
| |
| |
| The `Precondition` pragma is similar to `Postcondition` |
| except that the corresponding checks take pla
|