.. role:: switch(samp) .. |GNAT_Users_Guide| replace:: :title:`GNAT User's Guide for Native Platforms` .. index:: Certified Systems .. _Support_for_Certified_Systems: ***************************** Support for Certified Systems ***************************** .. _The_Certification_Philosophy: The Certification Philosophy ============================ GNAT is intended to reduce costs and risks in meeting software safety or security certification standards for applications written in Ada. One way this goal is met is through the use of language profiles: using one of the language profiles designed for certification, or an appropriately constrained Ada subset selected by the programmer. The following GNAT defined-profiles have been designed with certification in mind and are know in this chapter as the *Certifiable Profiles*: * Light Profile * Light-Tasking Profile .. index:: Light Profile The Light Profile provides a flexible Ada subset that is supported by a certifiable Ada run-time. Depending on application requirements, this profile can be further restricted through the Restrictions pragma, with the application only including run-time code that is used by the application. The Light Profile run-times can also be customized directly to suit certification requirements: unneeded packages can be removed to allow for self-certification of the run-time while the `-nostdlib` linker switch can be used to prevent the use of the run-time. Do note that when the run-time library is suppressed some run-time sources are still required to provide compiler-time definitions. While this code produces no object code, be aware that the certification protocol may still require tests to ensure correct access to these definitions. .. index:: Light-Tasking Profile The Light-Tasking Profile expands the Light Profile to include Ravenscar tasking support, allowing users to make use concurrency in their certification applications. .. index:: Certifiable Profiles .. index:: Generic templates (permitted in Certifiable Profiles) .. index:: Child units (permitted in Certifiable Profiles) .. index:: Tagged types at library level (permitted in Certifiable Profiles) .. index:: Object-Oriented Programming (and the Certifiable Profiles) .. index:: pragma Restrictions Although limited in terms of dynamic Ada semantics, all Certifiable Profiles fully support static Ada constructs such as private types, generic templates, and child units. Some dynamic semantics are also supported. For example, these profiles allow the use of tagged types (at library level) and other Object-Oriented Programming features, including dynamic dispatching. Note that you can prohibit the general use of dynamic dispatching at the application level using pragma ``Restrictions``. A traditional problem with predefined profiles is their inflexibility: if you need to use a feature that is outside a given profile, then it is your responsibility to address the certification issues deriving from its use. GNAT for cross platforms accommodate this need by allowing you to define a profile for the specific set of features you will use. Typically this will be for features with run-time libraries that require associated certification materials. Thus your program will have a tailored run-time library supporting only those features that you have specified. .. _Using_GNAT_Pro_Features_Relevant_to_Certification: Using GNAT Pro Features Relevant to Certification ================================================= GNAT Pro contain a number of features especially useful for certified software: .. index:: -gnatD (gcc) .. index:: -gnatG (gcc) * With the ``-gnatD`` or ``-gnatG`` options, the compiler generates a low-level version of the source program in an Ada-like format. This serves as an intermediate form between the original source program and the generated object code. This intermediate representation may be used to understand the assembly code and verify some of the origins of non-traceable code. This expanded low-level generated code can also be used as the reference point for run-time debugging. .. index:: -gnatR (gcc) * With the ``-gnatR`` option, the compiler generates information about the choice of data representations. * The compiler produces an extensive set of warning messages to diagnose situations that are likely to be errors, even though they do not correspond to illegalities in Ada Reference Manual terms. .. index:: pragma Restrictions .. index:: No_Implicit_Loops restriction .. index:: No_Implicit_Conditionals restriction * Two restriction identifiers for ``pragma Restrictions`` prohibit constructs that would generate implicit loops (``No_Implicit_Loops``) or implicit conditionals (``No_Implicit_Conditionals``). If these restrictions are specified, then either alternative code is generated without the implicit code, or the construct in question is rejected, forcing the programmer to make the loop or conditional explicit in the source. This is desirable in ensuring full testing of conditionals. See :ref:`Controlling_Implicit_Conditionals_and_Loops`. * A restriction identifier for ``pragma Restrictions`` can be used to restrict the form of explicit conditionals. Using the restriction identifier ``No_Direct_Boolean_Operators`` prohibits the use of ``and`` and ``or`` operators, forcing instead the use of ``and then`` and ``or else``. This can be useful in some certification procedures in order to reduce the number of test cases needed to fully exercise compound conditions. .. index:: -gnaty (gcc) * With the :samp:`-gnaty{x}` options, the compiler performs various style checks that can be used to enforce rigorous coding standards, easing the verification process by ensuring that the source is formatted in a uniform manner. .. index:: Reviewable object code .. index:: Annex H (Ada Reference Manual) * Annex H of the :title:`Ada Reference Manual` is fully implemented, and all implementation-dependent characteristics of the GNAT Pro implementation are defined in the :title:`GNAT Reference Manual`, further supporting the goal of reviewable object code. .. index:: Exceptions and the Certifiable Profiles .. index Light profile .. index Light-Tasking profile .. index Pragma Restrictions (No_Exception_Propagation) .. index No_Exception_Propagation (pragma Restrictions argument) .. _Exceptions_and_the_Certifiable_Profiles: Exceptions ---------- The Certifiable Profiles provide limited local exception handling through the implicit application of `pragma Restrictions (No_Exception_Propagation)``. This restriction allows exceptions to be raised and handled only if the handler is in the same subprogram (more generally in the same scope not counting packages and blocks). This limits the handling of exceptions to cases where raising the exception corresponds to a simple goto to the exception handler. This is especially useful for predefined exceptions. For example, the following is allowed with the Light and Light-Tasking: .. code-block:: ada begin X := Y + Z; exception when Constraint_Error => ... result of addition outside range of X end; With this restriction in place, handlers are allowed, but can only be entered if the raise is local to the scope with the handler. The handler may not have a choice parameter, use of GNAT.Current_Exception is not permitted, and use of reraise statements (raise with no operand) is not permitted. Warnings are given if an implicit or explicit exception raise is not covered by a local handler, or if an exception handler does not cover a case of a local raise. The following example shows these warnings in action: :: 1. pragma Restrictions (No_Exception_Propagation); 2. procedure p (C : in out Natural) is 3. begin 4. begin 5. C := C - 1; 6. exception 7. when Constraint_Error => 8. null; 9. when Tasking_Error => | >>> warning: pragma Restrictions (No_Exception_Propagation) in effect, this handler can never be entered, and has been removed 10. null; 11. end; 12. 13. begin 14. C := C - 1; | >>> warning: pragma Restrictions (No_Exception_Propagation) in effect, "Constraint_Error" may call Last_Chance_Handler 15. end; 16. 17. begin 18. raise Program_Error; | >>> warning: pragma Restrictions (No_Exception_Propagation) in effect, Last_Chance_Handler will be called on exception 19. end; 20. end p; .. index -gnatw.X (gcc) .. index pragma Warnings (Off) These warnings may be turned off globally using the switch -gnatw.X, or by using pragma Warnings (Off) locally. As shown by the warnings above, if any other exception is raised, it is treated as unhandled, and causes the 'last chance handler' to be invoked. This routine is described below. Exception handling can also be forbidden entirely while still allow the raising of exceptions by using: .. code-block:: ada pragma Restrictions (No_Exception_Handlers); .. index Pragma Restrictions (No_Exception_Handlers) .. index No_Exception_Handlers (pragma Restrictions argument) .. index:: Constraint_Error .. index:: Program_Error .. index:: Storage_Error No handlers are permitted in a program if this restriction is specified, so exceptions can never be handled in the usual Ada way. If run-time checking is enabled, then it is possible for the predefined exceptions ``Constraint_Error``, ``Program_Error``, or ``Storage_Error`` to be raised at run time. When such an exception is raised, a global 'last chance handler' routine is invoked automatically to deal with the fatal errors represented by these exception occurrences. The term 'last chance' is used because the handler routine is the last code executed. A default implementation is included with the profile implementation and does nothing other than terminate the application. This default version can be replaced by the user. The replacement routine can be written in either Ada or C, and must have the link-time symbol ``__gnat_last_chance_handler``. For example, a user-defined Ada procedure can be specified via pragma Export to have the required symbol name. Note that the parameters to the handler routine are profile-specific. Details are provided in the sections specific to the individual profiles. All last chance handler implementations must effectively terminate the application. For example, on a bareboard target, it could enter an infinite loop. Alternatively, it could restart the hardware, thereby invoking a new instance of the application. In no case, however, may the application instance experiencing the exception continue execution after the last chance handler routine executes. .. index:: raise statement (permitted under No_Exception_Handlers) .. index:: Exception declaration (permitted under No_Exception_Handlers) Exception declarations and ``raise`` statements are still permitted under this restriction. A ``raise`` statement is compiled into a call of ``__gnat_last_chance_handler``. To suppress all run-time error checking and generation of implicit calls to the last chance handler, and to disallow all ``raise`` statements, you may use: .. code-block:: ada pragma Restrictions (No_Exceptions); The following switch is not relevant if the program has ``pragma Restrictions (No_Exception_Handlers)`` or ``pragma Restrictions (No_Exception_Propagation)``: .. index:: -E (gnatbind) * :samp:`-E` This switch causes traceback information to be stored with exception occurrences and is only applicable when there are exception handlers. The following switches are not relevant if the program has ``pragma Restrictions (No_Exceptions)`` or ``pragma Restrictions (No_Exception_Propagation)``: * :samp:`-E` See above. .. index:: -gnatE (gcc) * :samp:`-gnatE` This switch enables run-time checks for 'Access-Before-Elaboration' errors. .. index:: Allocator .. index:: Unchecked_Deallocation generic .. index:: Ada.Unchecked_Deallocation generic .. _Allocators_and_the_Certifiable_Profiles: Allocators ---------- Allocators and unchecked deallocation are permitted in a certification context. Use of these features will generate calls on one of the following C convention functions: .. index:: __gnat_malloc .. index:: __gnat_free .. code-block:: c void *__gnat_malloc (size_t size); void __gnat_free (void *ptr); The corresponding Ada subprogram declarations are: .. index Gnat_Malloc .. index Gnat_Free .. code-block:: ada type Pointer is access Character; -- This is really a void pointer type, the result from -- Gnat_Malloc will always be maximally aligned. function Gnat_Malloc (size : Interfaces.C.size_t) return Pointer; pragma Export (C, Gnat_Malloc, "__gnat_malloc"); procedure Gnat_Free (Ptr : Pointer); pragma Export (C, Gnat_Free, "__gnat_free"); The *Light* and *Light Tasking* run-times provide default implementations of these functions in :file:`s-memory.adb`. Deallocation is not supported, with the function ``__gnat_free`` implemented as a no-op. See :ref:`The_GNAT_Runtimes` for more information. The default implementations of __gnat_malloc and __gnat_free can be replaced with user implementations if different behavior is required. Simply provide your own implementation of these functions in your application and they will be used instead of the run-time defaults. .. index:: memLib .. index:: memNoMoreAllocations For example, on VxWorks Cert, one approach (if no deallocation is to be allowed) is for the user to implement ``Gnat_Malloc`` through calls on ``memLib`` routines. The ``memNoMoreAllocations`` function can be invoked to prevent further allocations, for example at the end of package elaboration. To prohibit the use of allocators or unchecked deallocation, you can use ``pragma Restrictions`` with the following restriction identifiers (these are defined in the :title:`Ada Reference Manual`): .. index:: No_Local_Allocators restriction .. index:: No_Allocators restriction .. index:: No_Implicit_Heap_Allocators restriction .. index:: No_Unchecked_Deallocation restriction +------------------------------------------------------+--------------------------------------------------+ | Restriction | Effect | +======================================================+==================================================+ | *pragma Restrictions (No_Local_Allocators)* | This prohibits the use of allocators except at | | | the library level (thus allocations occur only | | | at elaboration time, and not after the | | | invocation of the main subprogram) | +------------------------------------------------------+--------------------------------------------------+ | *pragma Restrictions (No_Allocators)* | This prohibits all explicit use of allocators, | | | thus preventing allocators both at the local | | | and library level | +------------------------------------------------------+--------------------------------------------------+ | *pragma Restrictions (No_Implicit_Heap_Allocations)* | This prohibits implicit allocations (for example | | | an array with nonstatic subscript bounds | | | declared at library level) | +------------------------------------------------------+--------------------------------------------------+ | *pragma Restrictions (No_Unchecked_Deallocation)* | This prohibits all use of the generic procedure | | | ``Ada.Unchecked_Deallocation`` | +------------------------------------------------------+--------------------------------------------------+ .. index:: gnat.adc file If any or all of these pragmas appear in the :file:`gnat.adc` file, the corresponding construct(s) will be forbidden throughout the application. If all four of the above restrictions are in place, then no calls to either ``__gnat_malloc`` or ``__gnat_free`` will be generated. .. index:: Array and record assignments and the Certifiable Profiles .. index:: Record and array assignments and the Certifiable Profiles .. _Array_and_Record_Assignments_and_certification: Array and Record Assignments ---------------------------- .. index:: memcpy .. index:: memmove .. index:: memset .. index:: bcopy The use of whole-object assignments of arrays and records is permitted. However, on some targets such constructs may generate calls on the C library functions ``memcpy``, ``memmove``, ``memset``, or ``bcopy``. There are two ways to deal with this issue. First, such assignments can be avoided at the source code level. You can replace an array assignment by an explicit loop, and a record assignment by a series of assignments to individual components. You can encapsulate such statements in a procedure if many such assignments occur. Second, you can reuse or define an appropriate replacement for one (or more) of the routines. For example, if certification protocols permit, you can reuse the ``memcpy``, ``memset``, ``memmove``, and/or ``bcopy`` routine(s) from the C library. An an example of defining one's own implementation, the following Ada procedure will supply the needed ``memcpy`` functionality: .. index:: Example - memcpy function in Ada .. code-block:: ada with System; use System; with Interfaces.C; use Interfaces.C; function memcpy (dest, src : Address; n : size_t) return Address; pragma Export (C, memcpy, "memcpy"); with Ada.Unchecked_Conversion; function memcpy (dest, src : Address; n : size_t) return Address is subtype mem is char_array (size_t); type memptr is access mem; function to_memptr is new Ada.Unchecked_Conversion (address, memptr); dest_p : constant memptr := to_memptr (dest); src_p : constant memptr := to_memptr (src); begin if n > 0 then -- need to guard against n=0 since size_t is a modular type for J in 0 .. n - 1 loop dest_p (J) := src_p (J); end loop; end if; return dest; end memcpy; The above ``memcpy`` routine provides the minimal required functionality. A more elaborate version that deals with alignments and moves by words rather than bytes where possible would improve performance. On some targets there may be hardware instructions (e.g. ``rep movsb`` on the x86 architecture) that can be used to provide the needed functionality. Note that ``memcpy`` is not required to handle the overlap case, and the GNAT Pro compiler ensures that any call to ``memcpy`` meets the requirement that the operands do not overlap. On the other hand, ``memmove`` and ``bcopy`` are required to handle overlaps. Note that the order of the arguments of ``bcopy`` differs from ``memcpy`` and ``memmove``. A user-supplied version of ``bcopy`` should take into account these differences. .. index:: Object-Oriented Programming and the Certifiable Profiles .. _Object-Oriented_Programming_and_certification: Object-Oriented Programming --------------------------- Large part of Ada's object-oriented programming facilities is supported on the Certifiable Profiles. Objects of tagged and class-wide types may be declared. Dispatching and class-wide subprograms are allowed. Restrictions are: * Tagged types must be declared at the library level. * No controlled types. * ``Ada.Tags.Internal_Tag`` and ``Ada.Tags.Tag_Error`` are not available in the default implementations of these profiles. The method invocation syntax of ``Object.Operation (...)`` is fully supported under the Light profile. Generic dispatching constructors are not supported under the Light profile. A subset of interface types is supported under the Light profile, with the following restrictions: * No task interfaces, protected interfaces or synchronized interfaces. * No dynamic membership test applied to interfaces (only those cases in which the evaluation can be performed at compile-time are supported). * No class-wide interface conversions. * No declaration of a tagged type covering interfaces in which its parent type has variable-size components. * The ``Address`` attribute is not supported on objects whose visible type is a class-wide interface. Note: Dispatch tables are used to implement dynamic dispatching. Each tagged type has an associated data structure including a table containing the address of each of its primitive operations. The format of dispatch tables is compatible with the format described in the Itanium C++ ABI. This means, in particular, that the dispatching mechanism is deterministic and bounded in time, with a performance similar to an indirect call. Furthermore, dispatch tables are generated by the compiler as static data that is placed in a read-only data section of the object code; restriction Static_Dispatch_Tables can be used to identify tagged type declarations that cannot be placed in a read-only section. Appropriate linker scripts can be used to ensure that such sections are placed in ROM. Placing such tables in ROM is recommended because it offers some level of robustness to the dispatching mechanism: it prevents the possibility of unintended changes in such tables that could affect the control flow of the code. In addition, declarations of tagged types in this profile are statically elaborable and thus can be used in the presence of the restriction No_Elaboration_Code. In order for the debugger to be able to print the complete type description of a tagged type, the program must have Ada.Tags as part of its closure. Otherwise, the debugger will not be able to print the name of the type from which the tagged type has been derived. This limitation can easily be addressed by introducing an artificial dependency on the Ada.Tags unit. Another option is to compile one unit that declares a tagged type with -fno-eliminate-unused-debug-types. This does not affect the ability to print the value of tagged objects, which should work without problem regardless. .. index:: Functions returning unconstrained objects .. index:: Unconstrained objects, returned by functions .. index:: Secondary stack (for unconstrained objects returned by functions) .. _Functions_Returning_Unconstrained_Objects: Functions Returning Unconstrained Objects ----------------------------------------- By default, the cross and bareboard run-times allow functions returning objects of unconstrained types, such as unconstrained array types or discriminated record types without default values for the discriminants. For such functions, the amount of storage required for the result is not known at the point of the call. To implement this capability, the compiler generates references to a secondary-stack mechanism that requires run-time support. .. index:: System.Secondary_Stack .. index:: s-secsta.ads (package spec System.Secondary_Stack) If you need to use this capability, you should refer to the relevant section in :ref:`The_Predefined_Profiles`, to see if it is already provided in the run-time library or if you are responsible for providing an appropriate implementation of this unit for a given profile. The specification of the secondary-stack mechanism is described in the Ada package ``System.Secondary_Stack``, which is in the file :file:`s-secsta.ads`. .. index:: No_Secondary_Stack restriction .. index:: pragma Restrictions (No_Secondary_Stack) If you wish to disable this capability, you can use the ``pragma Restrictions (No_Secondary_Stack)``; this will generate an error at compile time for each call to a function returning an unconstrained object. .. index:: Implicit conditionals .. index:: Implicit loops .. _Controlling_Implicit_Conditionals_and_Loops: Controlling Implicit Conditionals and Loops ------------------------------------------- Certain complex constructs in Ada result in generated code that contains implicit conditionals, or implicit ``for`` loops. ('Implicit' means that the conditionals/loops are not present in the Ada source code.) For example, slice assignments result in both kinds of generated code. In some certification protocols, conditionals and loops require special treatment. For example, in the case of a conditional, it may be necessary to ensure that the test suite contains cases that branch in both directions for a given conditional. A question arises as to whether implicit conditionals and loops generated by the compiler are subject to the same verification requirements. To address this issue, GNAT define two restriction identifiers that control whether the compiler is permitted to generate implicit conditionals and loops : .. index:: No_Implicit_Conditionals restriction .. index:: No_Implicit_Loops restriction .. code-block:: ada pragma Restrictions (No_Implicit_Conditionals); pragma Restrictions (No_Implicit_Loops); These are partition-wide restrictions that ensure that the generated code respectively contains no conditionals and no loops. This is achieved in one of two ways. Either the compiler generates alternative code to avoid the implicit construct (possibly with some loss of efficiency) or, if it cannot find an equivalent code sequence, it rejects the program and flags the offending construct. In the latter situation, the programmer will need to revise the source program to avoid the implicit conditional or loop. .. index:: Slice assignment and implicit loops and conditionals As an example, consider the slice assignment: .. code-block:: ada Data (J .. K) := Data (R .. S); Ada language semantics requires that a slice assignment of this type be performed nondestructively, as though the right-hand side were computed first into a temporary, with the value then assigned to the left-hand side. In practice it is more efficient to use a single loop, but the direction of the loop needs to depend on the values of ``J`` and ``R``. If ``J`` is less than ``R`` then the move can take place left to right; otherwise it needs to be done right to left. The normal code generated by GNAT Pro reflects this requirement: .. code-block:: ada if J < R then for L in J .. K loop Data (L) := Data (L - J + R); end loop; else for L in reverse J .. K loop Data (L) := Data (L - J + R); end loop; end if; This code clearly contains both implicit conditionals and implicit loops. If the restriction ``No_Implicit_Conditionals`` is active, then the effect is to generate code that uses a temporary: .. code-block::ada for L in R .. S loop Temp (L - R) := Data (L); end loop; for L in J .. K loop Data (L) := Temp (L - J); end loop; This code avoids an implicit conditional at the expense of doing twice as many moves. If the restriction ``No_Implicit_Loops`` is also specified, then the slice assignment above would not be permitted, and would be rejected as illegal. This means that the programmer would need to modify the source program to have an explicit loop (in the appropriate direction). This loop could then be treated in whatever manner is required by the certification protocols in use. .. index:: No_Implicit_Conditionals, features excluded by The following constructs are not permitted in the presence of ``No_Implicit_Conditionals`` (note that some are in any event excluded from the Certifiable Profiles): * Comparison of record or array values * Array concatenation * Controlled types * Protected types * Asynchronous select * Conditional entry call * Delay statement * Selective accept * Timed entry call * Tagged types * Distributed System Annex features (shared passive partitions, etc.) * ``Width`` attribute applied to real type * Absolute value operator if checks are on * ``rem``, ``mod``, and division operators if checks are on * ``Is_Negative`` intrinsic function * Dynamic elaboration check .. index:: No_Implicit_Loops, features excluded by The following constructs are not permitted in the presence of ``No_Implicit_Loops`` (note that entry families are in any event excluded from some or all Certifiable Profiles): * Array aggregate with ``others`` clause * Array types with implicit component initialization * Array equality test * Array concatenation * Logical operations on array types * Array assignments * Controlled array types * Entry families * Default array stream attributes .. index:: conditional operators .. index:: and/or usage control .. index:: MC/DC (in DO-178B and DO-178C) .. index:: Modified Condition/Decision Coverage .. _Controlling_Use_of_Conditional_Operators: Controlling Use of Conditional Operators ---------------------------------------- Some testing procedures for certification can be more efficient if application programs avoid the explicit use of ``and`` / ``or`` and instead use ``and then`` / ``or else``. This can facilitate meeting the requirement for MCDC ('Modified Condition / Decision Coverage') testing. The net effect of using the short-circuit versions is a significant reduction in the number of test cases needed to demonstrate code and condition coverage. GNAT provide an additional restriction identifier that addresses this issue by controlling the presence of direct boolean conditional operators: .. index:: No_Direct_Boolean_Operators restriction .. code-block:: ada pragma Restrictions (No_Direct_Boolean_Operators); These are partition-wide restrictions that ensure that the source code does not contain any instances of the direct boolean operators ``and`` or ``or``. This will alert the programmer to the requirement to use ``and then`` or ``or else`` as appropriate .. index:: Elaboration code .. index:: Avoiding elaboration code .. _Avoiding_Elaboration_Code: Avoiding Elaboration Code ------------------------- Ada allows constructs (e.g., variables with implicit initializations) for which so-called *elaboration code* must be generated. In a certification context the need to certify elaboration code will increase costs, as it will be necessary to address questions such as why the compiler implicitly generated the elaboration code, which Ada requirement it met, which test cases are needed. GNAT provides the pragma ``Restrictions (No_Elaboration_Code)``, which alerts you to constructs for which elaboration code would be generated by the compiler. When this pragma is specified for a compilation unit, the compiler outputs an error message whenever it needs to generate elaboration code. You must then revise the program so that no elaboration code is generated. As an example consider the following: .. code-block:: ada package List is type Elmt; type Temperature is range 0 .. 1_000; type Elmt_Ptr is access all Elmt; type Elmt is record T : Temperature; Next : Elmt_Ptr; end record; X : Elmt; end List; When compiling unit ``List``, the compiler will generate the error message: :: list.ads:11:04: violation of restriction "No_Elaboration_Code" at line 1 .. index:: -gnatG (gcc) In this example GNAT Pro needs to generate elaboration code for object ``X``. To see the elaboration code that would be generated you can remove the ``No_Elaboration_Code`` restriction and use the ``-gnatG`` switch to view the low-level version of the Ada code generated by GNAT Pro. In this case we obtain: .. -- The following fragment has "::" versus "code-block:: ada" because of the .. -- '[' and ']' characters :: package list is type list__elmt; type list__temperature is range 0 .. 1000; type list__elmt_ptr is access all list__elmt; type list__elmt is record t : list__temperature; next : list__elmt_ptr; end record; [type list__TtemperatureB is new short_integer] freeze list__TtemperatureB [] freeze list__elmt [ procedure list__elmtIP (_init : out list__elmt) is begin _init.next := null; return; end list__elmtIP; ] list__x : list__elmt; list__elmtIP (list__x); end list; Elaboration code is generated inside package ``List`` to *null*-initialize the access value inside ``X``, by calling the initialization procedure for the type, namely ``list__elmtIP``. To avoid generating elaboration code, you can add explicit initialization as follows: .. code-block:: ada pragma Restrictions (No_Elaboration_Code); package List is type Elmt; type Temperature is range 0 .. 1_000; type Elmt_Ptr is access all Elmt; type Elmt is record T : Temperature; Next : Elmt_Ptr; end record; X : Elmt := (0, null); end List; Since the initialization is now explicit, it becomes part of the requirements mapping and application design. In a certification context it is preferable to certify code that you write explicitly rather than code that gets generated implicitly. .. index:: Removal of Deactivated Code .. index:: Deactivated code .. index:: DO-178B .. _Removal_of_Deactivated_Code: Removal of Deactivated Code --------------------------- Deactivated code in the executable requires specific treatment with standards such ED12/DO-178B (see 6.4.4.3d). This treatment can be simplified by diminishing the footprint of deactivated code in the final executable. This section summarizes the various features that can be used to minimize the footprint of deactivated code in the final executable program. * Automatic Removal The compiler automatically removes local nested subprograms that are never used at all levels of optimization. It also removes unused library-level subprograms declared within package bodies at optimization level -O1 or higher. * Static Boolean conditionals The compiler eliminates automatically all code protected by conditionals, if and case statements, that are statically detected to be false. For instance, with those declarations: .. code-block:: ada type Configs is (config1, config2, config3); ... C : constant Configs := config2; the following code .. code-block:: ada if C = config1 then some_code0; end if; case C is when config1 => some_code1; when config2 => some_code2; when config3 => some_code3; end case; is transformed into: .. index:: -gnatwt (gcc) .. code-block:: ada some_code2; The elimination done by the compiler can be traced using an optional compiler warning enabled with ``-gnatwt``. * Pragma Eliminate The user can prevent code generation for subprograms that are known to be deactivated by placing Eliminate pragmas in the configuration pragmas file: .. code-block:: ada pragma Eliminate (Unit, Unused_Subp, Source_Location => "unit.adb:19") The compiler will issue an error if an attempt is made to call an eliminated subprogram. * Linker Level Removal .. index:: -ffunction-sections (gcc) .. index:: -fdata-sections (gcc) .. index:: -Wl (gnatlink) .. index:: --gc-sections (gnatlink) .. index:: -M (gnatlink) Some configurations support linker level removal of unused subprograms and data. The source code needs to be compiled with the options ``-ffunction-sections`` and ``-fdata-sections`` and the linking must be performed with option ``-Wl,--gc-sections``. Traceability of the code removal is provided through a chapter called "Discarded Input sections" in the map file that can be produced by the linker with option ``-Wl,-M``. These methods can be used to reduce the amount of code in the final executable corresponding to deactivated source code. The last three offer means of tracing the removed code and thus can be used for traceability purposes or as documentation of the deactivation mechanism. The last method can also remove code added by the compiler such as the implicit initialization procedures associated with composite types when they are not used. It therefore simplifies the reverse traceability from object to source. .. index:: Traceability from Source Code to Object Code .. _Traceability_from_Source_Code_to_Object_Code: Traceability from Source Code to Object Code -------------------------------------------- During the build process, the GNAT Pro toolchain manipulates several program representations, in particular: * The initial source code; * The expanded code, which is low level Ada pseudo-code; * Assembler code; and * Object code. In order to help the traceability process, GNAT Pro gives access to the intermediate format, through the following options: .. index:: -gnatD (gcc) * :samp:`-gnatD` This switch causes a listing of a pseudo-Ada low-level version of the compilation unit to be directed to a file. .. index:: -gnatG (gcc) * :samp:`-gnatG` This switch produces a listing of a pseudo-Ada low-level version of the compilation unit. .. index:: -gnatL (gcc) * :samp:`-gnatL` This switch enhances traceability of the expanded code by adding the original source code as comments just before the corresponding expansion. It has to be used in conjunction with ``-gnatD`` or ``-gnatG``. .. index:: -S (gcc) * :samp:`-S` This switch causes generation of an assembly language version of the compilation unit, instead of an object file. .. index:: -save-temps (gcc) * :samp:`-save-temps` This switch causes the compiler to save temporary files (in particular, the :file:`.s` file) while still generating :file:`.o` and :file:`ALI` files. .. index:: -fverbose-asm (gcc) * :samp:`-fverbose-asm` This switch causes the compiler to decorate the assembly output with comments containing the names of the entities (e.g. local variables) being manipulated by the current assembly instruction. .. index:: -mregnames (gcc) * :samp:`-mregnames` This switch causes the compiler to emit symbolic names for register in the assembly output. This switch is specific to PowerPC and even though it is not directly related to traceability, it is worth mentioning because it greatly improves assembly code readability. .. index:: -Wa (gcc) .. index:: -adhl (gcc) * :samp:`-Wa,-adhl` This switch instructs the GNU assembler to produce a text listing of the generated code containing the high-level source and the assembly while excluding debugger directives (for readability reasons). The listing goes to standard output and can be redirected to a file using the syntax ``-Wa,-adhl=file.lst`` which save it in the file ``file.lst``. .. index:: -gnatR (gcc) * :samp:`-gnatR` This switch causes representation information to be generated for declared types and objects. These options can be combined in various ways. A fairly complete source to object traceability is provided by: :: $ -gcc -c -gnatDL -Wa,-adhl -fverbose-asm -mregnames prg.adb .. index:: Optimization issues .. _Optimization_issues: Optimization issues ------------------- .. index:: -O (gcc) The :samp:`-O{n}` compiler switch sets the optimization level to ``n``, where ``n`` is an integer between 0 and 3. If ``n`` is omitted, it is set to 1. Generally you should use the :samp:`-O{n}` switch to enable optimization, because this is the level at which you can most easily track the correspondence between source code and object code. Although for safety-critical programs optimizations are often regarded with suspicion, the fundamental reason for this concern is traceability. At the :samp:`-O0` level, traceability is in fact more difficult due to the large amount of naive code that is generated. The optimizations performed at level :samp:`-O1` eliminate redundant code, but avoid the kind of code-shuffling transformations that can obscure the correspondence between source and object code. .. index:: -fno-short-circuit-optimize (gcc) .. index:: -fno-if-conversion (gcc) .. index:: -fno-if-conversion2 (gcc) If you consider coverage, it can be useful to disable optimizations on conditional statements. The option *-fno-short-circuit-optimize* specifically disables boolean operator optimizations (those which transform ``or else`` into ``or`` or ``and then`` into ``and``), and the options *-fno-if-conversion* and *-fno-if-conversion2* disable optimization passes that try to remove conditional jumps for if statements and use conditional move instead. These switches help to preserve the original jump structure implied by the source, thus helping source-to-object traceability, and facilitating certification and coverage analysis at the object level. .. _Other_useful_features: Other useful features --------------------- .. index:: -gnaty (gcc) The *-gnaty* compiler switches direct the compiler to enforce style consistency checks, which can be useful in ensuring a uniform lexical appearance (and easing program readability) across a project. .. index:: Annex H restrictions Annex H in the :title:`Ada Reference Manual` defines a set of restrictions identifiers, many of which are relevant for code that needs to be certified. If you provide a ``pragma Restrictions`` with any of these identifiers, the compiler will prohibit your program from using the corresponding construct. .. _Program_Build_Options_with_the_Certifiable_Profiles: Program Build Options --------------------- For the most part, you can build programs using the Certifiable Profiles in the same way, and with the same set of switches, as in a full Ada environment. However, certain switches are not relevant for the Certifiable Profiles. This section lists these switches; a complete description of the compiler switches appears in the :title:`GNAT User's Guide for Native Platforms` and, in the case of general gcc switches, the :title:`Using GNU GCC` manual. .. index:: Compiler switches .. _Compiler_Switches: Compiler Switches ^^^^^^^^^^^^^^^^^ .. index:: Light mode .. index:: Light-Tasking mode The following switches are not relevant in certain Certifiable Profiles, since they are associated with features that are outside these profiles: .. index:: -fstack-check (gcc) * :samp:`-fstack-check` This switch enables stack overflow checking .. index:: -gnata (gcc) * :samp:`-gnata` This switch enables pragma ``Assert``, subject to exception propagation and handling restrictions. .. index:: -gnato (gcc) * :samp:`-gnato` This switch enables run-time checks for integer overflow, subject to exception propagation and handling restrictions. .. index:: -gnatT (gcc) * :samp:`-gnatT` This switch sets the timeslice in a tasking program. .. index:: -gnatz (gcc) * :samp:`-gnatz` This switch is used for distributed Ada programs. .. index:: Binder switches .. index:: gnatbind switches .. _gnatbind_Switches: ``gnatbind`` Switches ^^^^^^^^^^^^^^^^^^^^^ .. index:: Light mode .. index:: Light-Tasking mode The following switches are not relevant in Light and Light-Tasking modes: .. index:: -static (gnatbind) * :samp:`-static` This switch specifies linking with a static GNAT run-time library. .. index:: -shared (gnatbind) * :samp:`-shared` This switch specifies linking with a shared GNAT run-time library. .. index:: -T (gnatbind) * :samp:`-T` This switch sets the timeslice for a tasking program. .. index:: -t (gnatbind) In addition, the :samp:`-t` switch overrides standard Ada unit consistency checks and would generally not be used for high-integrity applications. .. index:: -f (gnatbind) The :samp:`-f` switch for elaboration-order control should not be used; see the discussion of elaboration-order issues in :title:`GNAT User's Guide for Native Platforms`.