GNAT Reference Manual

Table of Contents

GNAT Reference Manual

GNAT Reference Manual , Dec 10, 2019

AdaCore

Copyright © 2008-2020, Free Software Foundation

`GNAT, The GNU Ada Development Environment'

GCC version 10.2.0
AdaCore

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, with the Front-Cover Texts being "GNAT Reference Manual", and with no Back-Cover Texts. A copy of the license is included in the section entitled GNU Free Documentation License.

 — The Detailed Node Listing —

About This Guide

Implementation Defined Pragmas

Implementation Defined Aspects

Implementation Defined Attributes

Standard and Implementation Defined Restrictions

Partition-Wide Restrictions

Program Unit Level Restrictions

Implementation Advice

Intrinsic Subprograms

Representation Clauses and Pragmas

The Implementation of Standard I/O

Text_IO

Wide_Text_IO

Wide_Wide_Text_IO

The GNAT Library

Interfacing to Other Languages

Implementation of Specific Ada Features

GNAT Implementation of Tasking

Code Generation for Array Aggregates

Obsolescent Features

Compatibility and Porting Guide

Compatibility with Ada 83

Implementation-dependent characteristics

1 About This Guide

This manual contains useful information in writing programs using the GNAT compiler. It includes information on implementation dependent characteristics of GNAT, including all the information required by Annex M of the Ada language standard.

GNAT implements Ada 95, Ada 2005 and Ada 2012, and it may also be invoked in Ada 83 compatibility mode. By default, GNAT assumes Ada 2012, but you can override with a compiler switch to explicitly specify the language version. (Please refer to the `GNAT User’s Guide' for details on these switches.) Throughout this manual, references to ’Ada’ without a year suffix apply to all the Ada versions of the language.

Ada is designed to be highly portable. In general, a program will have the same effect even when compiled by different compilers on different platforms. However, since Ada is designed to be used in a wide variety of applications, it also contains a number of system dependent features to be used in interfacing to the external world.

Note: Any program that makes use of implementation-dependent features may be non-portable. You should follow good programming practice and isolate and clearly document any sections of your program that make use of these features in a non-portable manner.

1.1 What This Reference Manual Contains

This reference manual contains the following chapters:

• * Implementation Defined Pragmas, lists GNAT implementation-dependent pragmas, which can be used to extend and enhance the functionality of the compiler.
• * Implementation Defined Attributes, lists GNAT implementation-dependent attributes, which can be used to extend and enhance the functionality of the compiler.
• * Standard and Implementation Defined Restrictions, lists GNAT implementation-dependent restrictions, which can be used to extend and enhance the functionality of the compiler.
• * Implementation Advice, provides information on generally desirable behavior which are not requirements that all compilers must follow since it cannot be provided on all systems, or which may be undesirable on some systems.
• * Implementation Defined Characteristics, provides a guide to minimizing implementation dependent features.
• * Intrinsic Subprograms, describes the intrinsic subprograms implemented by GNAT, and how they can be imported into user application programs.
• * Representation Clauses and Pragmas, describes in detail the way that GNAT represents data, and in particular the exact set of representation clauses and pragmas that is accepted.
• * Standard Library Routines, provides a listing of packages and a brief description of the functionality that is provided by Ada’s extensive set of standard library routines as implemented by GNAT.
• * The Implementation of Standard I/O, details how the GNAT implementation of the input-output facilities.
• * The GNAT Library, is a catalog of packages that complement the Ada predefined library.
• * Interfacing to Other Languages, describes how programs written in Ada using GNAT can be interfaced to other programming languages.
• * Specialized Needs Annexes, describes the GNAT implementation of all of the specialized needs annexes.
• * Implementation of Specific Ada Features, discusses issues related to GNAT’s implementation of machine code insertions, tasking, and several other features.
• * Implementation of Ada 2012 Features, describes the status of the GNAT implementation of the Ada 2012 language standard.
• * Obsolescent Features documents implementation dependent features, including pragmas and attributes, which are considered obsolescent, since there are other preferred ways of achieving the same results. These obsolescent forms are retained for backwards compatibility.
• * Compatibility and Porting Guide presents some guidelines for developing portable Ada code, describes the compatibility issues that may arise between GNAT and other Ada compilation systems (including those for Ada 83), and shows how GNAT can expedite porting applications developed in other Ada environments.
• * GNU Free Documentation License contains the license for this document.

This reference manual assumes a basic familiarity with the Ada 95 language, as described in the International Standard ANSI/ISO/IEC-8652:1995. It does not require knowledge of the new features introduced by Ada 2005 or Ada 2012. All three reference manuals are included in the GNAT documentation package.

1.2 Conventions

Following are examples of the typographical and graphic conventions used in this guide:

• * Functions, utility program names, standard names, and classes.
• * Option flags
• * File names
• * Variables
• * `Emphasis'
• * [optional information or parameters]
• * Examples are described by text

  and then shown this way.
  

• * Commands that are entered by the user are shown as preceded by a prompt string comprising the $ character followed by a space.

1.3 Related Information

See the following documents for further information on GNAT:

• * GNAT User’s Guide for Native Platforms, which provides information on how to use the GNAT development environment.
• * Ada 95 Reference Manual, the Ada 95 programming language standard.
• * Ada 95 Annotated Reference Manual, which is an annotated version of the Ada 95 standard. The annotations describe detailed aspects of the design decision, and in particular contain useful sections on Ada 83 compatibility.
• * Ada 2005 Reference Manual, the Ada 2005 programming language standard.
• * Ada 2005 Annotated Reference Manual, which is an annotated version of the Ada 2005 standard. The annotations describe detailed aspects of the design decision.
• * Ada 2012 Reference Manual, the Ada 2012 programming language standard.
• * DEC Ada, Technical Overview and Comparison on DIGITAL Platforms, which contains specific information on compatibility between GNAT and DEC Ada 83 systems.
• * DEC Ada, Language Reference Manual, part number AA-PYZAB-TK, which describes in detail the pragmas and attributes provided by the DEC Ada 83 compiler system.

2 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.

2.1 Pragma Abort_Defer

Syntax:

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).

2.2 Pragma Abstract_State

Syntax:

pragma Abstract_State (ABSTRACT_STATE_LIST);

ABSTRACT_STATE_LIST ::=
     null
  |  STATE_NAME_WITH_OPTIONS
  | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} )

STATE_NAME_WITH_OPTIONS ::=
     STATE_NAME
  | (STATE_NAME with OPTION_LIST)

OPTION_LIST ::= OPTION {, OPTION}

OPTION ::=
    SIMPLE_OPTION
  | NAME_VALUE_OPTION

SIMPLE_OPTION ::= Ghost | Synchronous

NAME_VALUE_OPTION ::=
    Part_Of => ABSTRACT_STATE
  | External [=> EXTERNAL_PROPERTY_LIST]

EXTERNAL_PROPERTY_LIST ::=
     EXTERNAL_PROPERTY
  | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} )

EXTERNAL_PROPERTY ::=
    Async_Readers    [=> boolean_EXPRESSION]
  | Async_Writers    [=> boolean_EXPRESSION]
  | Effective_Reads  [=> boolean_EXPRESSION]
  | Effective_Writes [=> boolean_EXPRESSION]
    others            => boolean_EXPRESSION

STATE_NAME ::= defining_identifier

ABSTRACT_STATE ::= name

For the semantics of this pragma, see the entry for aspect Abstract_State in the SPARK 2014 Reference Manual, section 7.1.4.

2.3 Pragma Acc_Parallel

Syntax:

pragma Acc_Parallel [( ACC_PARALLEL_CLAUSE [, ACC_PARALLEL_CLAUSE... ])];

ACC_PARALLEL_CLAUSE ::=
    Acc_If        => boolean_EXPRESSION
  | Acc_Private   => IDENTIFIERS
  | Async         => integer_EXPRESSION
  | Copy          => IDENTIFIERS
  | Copy_In       => IDENTIFIERS
  | Copy_Out      => IDENTIFIERS
  | Create        => IDENTIFIERS
  | Default       => None
  | Device_Ptr    => IDENTIFIERS
  | First_Private => IDENTIFIERS
  | Num_Gangs     => integer_EXPRESSION
  | Num_Workers   => integer_EXPRESSION
  | Present       => IDENTIFIERS
  | Reduction     => (REDUCTION_RECORD)
  | Vector_Length => integer_EXPRESSION
  | Wait          => INTEGERS

REDUCTION_RECORD ::=
    "+"   => IDENTIFIERS
  | "*"   => IDENTIFIERS
  | "min" => IDENTIFIERS
  | "max" => IDENTIFIERS
  | "or"  => IDENTIFIERS
  | "and" => IDENTIFIERS

IDENTIFIERS ::=
  | IDENTIFIER
  | (IDENTIFIER, IDENTIFIERS)

INTEGERS ::=
  | integer_EXPRESSION
  | (integer_EXPRESSION, INTEGERS)

Requires the -fopenacc flag.

Equivalent to the parallel directive of the OpenAcc standard. This pragma should be placed in loops. It offloads the content of the loop to an accelerator device.

For more information about the effect of the clauses, see the OpenAcc specification.

2.4 Pragma Acc_Loop

Syntax:

pragma Acc_Loop [( ACC_LOOP_CLAUSE [, ACC_LOOP_CLAUSE... ])];

ACC_LOOP_CLAUSE ::=
    Auto
  | Collapse        => INTEGER_LITERAL
  | Gang            [=> GANG_ARG]
  | Independent
  | Private         => IDENTIFIERS
  | Reduction       => (REDUCTION_RECORD)
  | Seq
  | Tile            => SIZE_EXPRESSION
  | Vector          [=> integer_EXPRESSION]
  | Worker          [=> integer_EXPRESSION]

GANG_ARG ::=
    integer_EXPRESSION
  | Static => SIZE_EXPRESSION

SIZE_EXPRESSION ::=
    *
  | integer_EXPRESSION

Requires the -fopenacc flag.

Equivalent to the loop directive of the OpenAcc standard. This pragma should be placed in for loops after the "Acc_Parallel" pragma. It tells the compiler how to parallelize the loop.

For more information about the effect of the clauses, see the OpenAcc specification.

2.5 Pragma Acc_Kernels

Syntax:

pragma Acc_Kernels [( ACC_KERNELS_CLAUSE [, ACC_KERNELS_CLAUSE...])];

ACC_KERNELS_CLAUSE ::=
    Acc_If        => boolean_EXPRESSION
  | Async         => integer_EXPRESSION
  | Copy          => IDENTIFIERS
  | Copy_In       => IDENTIFIERS
  | Copy_Out      => IDENTIFIERS
  | Create        => IDENTIFIERS
  | Default       => None
  | Device_Ptr    => IDENTIFIERS
  | Num_Gangs     => integer_EXPRESSION
  | Num_Workers   => integer_EXPRESSION
  | Present       => IDENTIFIERS
  | Vector_Length => integer_EXPRESSION
  | Wait          => INTEGERS

IDENTIFIERS ::=
  | IDENTIFIER
  | (IDENTIFIER, IDENTIFIERS)

INTEGERS ::=
  | integer_EXPRESSION
  | (integer_EXPRESSION, INTEGERS)

Requires the -fopenacc flag.

Equivalent to the kernels directive of the OpenAcc standard. This pragma should be placed in loops.

For more information about the effect of the clauses, see the OpenAcc specification.

2.6 Pragma Acc_Data

Syntax:

pragma Acc_Data ([ ACC_DATA_CLAUSE [, ACC_DATA_CLAUSE...]]);

ACC_DATA_CLAUSE ::=
    Copy          => IDENTIFIERS
  | Copy_In       => IDENTIFIERS
  | Copy_Out      => IDENTIFIERS
  | Create        => IDENTIFIERS
  | Device_Ptr    => IDENTIFIERS
  | Present       => IDENTIFIERS

Requires the -fopenacc flag.

Equivalent to the data directive of the OpenAcc standard. This pragma should be placed in loops.

For more information about the effect of the clauses, see the OpenAcc specification.

2.7 Pragma Ada_83

Syntax:

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.

2.8 Pragma Ada_95

Syntax:

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.

2.9 Pragma Ada_05

Syntax:

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.

2.10 Pragma Ada_2005

Syntax:

pragma Ada_2005;

This configuration pragma is a synonym for pragma Ada_05 and has the same syntax and effect.

2.11 Pragma Ada_12

Syntax:

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_2012 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.

2.12 Pragma Ada_2012

Syntax:

pragma Ada_2012;

This configuration pragma is a synonym for pragma Ada_12 and has the same syntax and effect.

2.13 Pragma Aggregate_Individually_Assign

Syntax:

pragma Aggregate_Individually_Assign;

Where possible, GNAT will store the binary representation of a record aggregate in memory for space and performance reasons. This configuration pragma changes this behavior so that record aggregates are instead always converted into individual assignment statements.

2.14 Pragma Allow_Integer_Address

Syntax:

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:

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.

2.15 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 (and concatenations of string literals) are assumed to be either of type Standard.String or else Wide_String or Wide_Wide_String depending on the character literals they contain. All other kinds of arguments are analyzed as expressions, and must be 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.

2.16 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:

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.

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.

2.17 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.

2.18 Pragma Assertion_Policy

Syntax:

pragma Assertion_Policy (CHECK | DISABLE | IGNORE | SUPPRESSIBLE);

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                |
                      Ghost                |
                      Invariant            |
                      Invariant'Class      |
                      Loop_Invariant       |
                      Loop_Variant         |
                      Postcondition        |
                      Precondition         |
                      Predicate            |
                      Refined_Post         |
                      Statement_Assertions

POLICY_IDENTIFIER ::= Check | Disable | Ignore | Suppressible

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. If the policy is SUPPRESSIBLE, then assertions are enabled by default, however, if the `-gnatp' switch is specified all assertions are ignored.

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.

2.19 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:

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.

2.20 Pragma Assume_No_Invalid_Values

Syntax:

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:

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.

2.21 Pragma Async_Readers

Syntax:

pragma Async_Readers [ (boolean_EXPRESSION) ];

For the semantics of this pragma, see the entry for aspect Async_Readers in the SPARK 2014 Reference Manual, section 7.1.2.

2.22 Pragma Async_Writers

Syntax:

pragma Async_Writers [ (boolean_EXPRESSION) ];

For the semantics of this pragma, see the entry for aspect Async_Writers in the SPARK 2014 Reference Manual, section 7.1.2.

2.23 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:

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.

2.24 Pragma C_Pass_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.

2.25 Pragma Check

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.

2.26 Pragma Check_Float_Overflow

Syntax:

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:

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'.

2.27 Pragma Check_Name

Syntax:

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.

2.28 Pragma Check_Policy

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:

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.

2.29 Pragma Comment

Syntax:

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.

2.30 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.

2.31 Pragma Compile_Time_Error

Syntax:

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.

2.32 Pragma Compile_Time_Warning

Syntax:

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.

2.33 Pragma Compiler_Unit

Syntax:

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.

2.34 Pragma Compiler_Unit_Warning

Syntax:

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.

2.35 Pragma Complete_Representation

Syntax:

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.

2.36 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.

2.37 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:

`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.

`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.

`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.

`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.

2.38 Pragma Constant_After_Elaboration

Syntax:

pragma Constant_After_Elaboration [ (boolean_EXPRESSION) ];

For the semantics of this pragma, see the entry for aspect Constant_After_Elaboration in the SPARK 2014 Reference Manual, section 3.3.1.

2.39 Pragma Contract_Cases

Syntax:

pragma Contract_Cases ((CONTRACT_CASE {, CONTRACT_CASE));

CONTRACT_CASE ::= CASE_GUARD => CONSEQUENCE

CASE_GUARD ::= boolean_EXPRESSION | others

CONSEQUENCE ::= boolean_EXPRESSION

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