Go to the first, previous, next, last section, table of contents.


Safety and Security (normative)

  1. This Annex addresses requirements for systems that are safety critical or have security constraints. It provides facilities and specifies documentation requirements that relate to several needs:
    1. Understanding program execution;
    2. Reviewing object code;
    3. Restricting language constructs whose usage might complicate the demonstration of program correctness
    Execution understandability is supported by pragma Normalize_Scalars, and also by requirements for the implementation to document the effect of a program in the presence of a bounded error or where the language rules leave the effect unspecified.
  1. The pragmas Reviewable and Restrictions relate to the other requirements addressed by this Annex. NOTES
  2. (1) The Valid attribute, see section The Valid Attribute, is also useful in addressing these needs, to avoid problems that could otherwise arise from scalars that have values outside their declared range constraints.

Pragma Normalize_Scalars

  1. This pragma ensures that an otherwise uninitialized scalar object is set to a predictable value, but out of range if possible. Syntax
  2. The form of a pragma Normalize_Scalars is as follows:
  3. pragma Normalize_Scalars;
    
    Post-Compilation Rules
  4. Pragma Normalize_Scalars is a configuration pragma. It applies to all compilation_units included in a partition. Documentation Requirements
  5. If a pragma Normalize_Scalars applies, the implementation shall document the implicit initial value for scalar subtypes, and shall identify each case in which such a value is used and is not an invalid representation. Implementation Advice
  6. Whenever possible, the implicit initial value for a scalar subtype should be an invalid representation, see section Data Validity. NOTES
  7. (2) The initialization requirement applies to uninitialized scalar objects that are subcomponents of composite objects, to allocated objects, and to stand-alone objects. It also applies to scalar out parameters. Scalar subcomponents of composite out parameters are initialized to the corresponding part of the actual, by virtue of See section Parameter Associations.
  8. (3) The initialization requirement does not apply to a scalar for which pragma Import has been specified, since initialization of an imported object is performed solely by the foreign language environment, See section Interfacing Pragmas.
  9. (4) The use of pragma Normalize_Scalars in conjunction with Pragma Restrictions(No_Exceptions) may result in erroneous execution, See section Safety and Security Restrictions.

Documentation of Implementation Decisions

Documentation Requirements

  1. The implementation shall document the range of effects for each situation that the language rules identify as either a bounded error or as having an unspecified effect. If the implementation can constrain the effects of erroneous execution for a given construct, then it shall document such constraints. The documentation might be provided either independently of any compilation unit or partition, or as part of an annotated listing for a given unit or partition. See also See section Conformity of an Implementation with the Standard, and section Structure. NOTES
  2. (5) Among the situations to be documented are the conventions chosen for parameter passing, the methods used for the management of run-time storage, and the method used to evaluate numeric expressions if this involves extended range or extra precision.

Reviewable Object Code

  1. Object code review and validation are supported by pragmas Reviewable and Inspection_Point.

Pragma Reviewable

  1. This pragma directs the implementation to provide information to facilitate analysis and review of a program's object code, in particular to allow determination of execution time and storage usage and to identify the correspondence between the source and object programs. Syntax
  2. The form of a pragma Reviewable is as follows:
  3. pragma Reviewable;
    
    Post-Compilation Rules
  4. Pragma Reviewable is a configuration pragma. It applies to all compilation_units included in a partition. Implementation Requirements
  5. The implementation shall provide the following information for any compilation unit to which such a pragma applies:
    1. Where compiler-generated run-time checks remain;
    2. An identification of any construct with a language-defined check that is recognized prior to run time as certain to fail if executed (even if the generation of run-time checks has been suppressed);
    3. For each reference to a scalar object, an identification of the reference as either "known to be initialized," or "possibly uninitialized," independent of whether pragma Normalize_Scalars applies;
    4. Where run-time support routines are implicitly invoked;
    5. An object code listing, including:
      1. Machine instructions, with relative offsets;
      2. Where each data object is stored during its lifetime;
      3. Correspondence with the source program, including an identification of the code produced per declaration and per statement.
    1. An identification of each construct for which the implementation detects the possibility of erroneous execution;
    2. For each subprogram, block, task, or other construct implemented by reserving and subsequently freeing an area on a run-time stack, an identification of the length of the fixed-size portion of the area and an indication of whether the non-fixed size portion is reserved on the stack or in a dynamically-managed storage region.
  1. The implementation shall provide the following information for any partition to which the pragma applies:
    1. An object code listing of the entire partition, including initialization and finalization code as well as run-time system components, and with an identification of those instructions and data that will be relocated at load time;
    2. A description of the run-time model relevant to the partition.
    The implementation shall provide control- and data-flow information, both within each compilation unit and across the compilation units of the partition. Implementation Advice
  1. The implementation should provide the above information in both a human-readable and machine-readable form, and should document the latter so as to ease further processing by automated tools.
  2. Object code listings should be provided both in a symbolic format and also in an appropriate numeric format (such as hexadecimal or octal). NOTES
  3. (6) The order of elaboration of library units will be documented even in the absence of pragma Reviewable, see section Program Execution.

Pragma Inspection_Point

  1. An occurrence of a pragma Inspection_Point identifies a set of objects each of whose values is to be available at the point(s) during program execution corresponding to the position of the pragma in the compilation unit. The purpose of such a pragma is to facilitate code validation. Syntax
  2. The form of a pragma Inspection_Point is as follows:
  3. pragma Inspection_Point[(object_name {, object_name})];
    
    Legality Rules
  4. A pragma Inspection_Point is allowed wherever a declarative_item or statement is allowed. Each object_name shall statically denote the declaration of an object. Static Semantics
  5. An inspection point is a point in the object code corresponding to the occurrence of a pragma Inspection_Point in the compilation unit. An object is inspectable at an inspection point if the corresponding pragma Inspection_Point either has an argument denoting that object, or has no arguments. Dynamic Semantics
  6. Execution of a pragma Inspection_Point has no effect. Implementation Requirements
  7. Reaching an inspection point is an external interaction with respect to the values of the inspectable objects at that point, see section Conformity of an Implementation with the Standard. Documentation Requirements
  8. For each inspection point, the implementation shall identify a mapping between each inspectable object and the machine resources (such as memory locations or registers) from which the object's value can be obtained. NOTES
  9. (7) The implementation is not allowed to perform "dead store elimination" on the last assignment to a variable prior to a point where the variable is inspectable. Thus an inspection point has the effect of an implicit reference to each of its inspectable objects.
  10. (8) Inspection points are useful in maintaining a correspondence between the state of the program in source code terms, and the machine state during the program's execution. Assertions about the values of program objects can be tested in machine terms at inspection points. Object code between inspection points can be processed by automated tools to verify programs mechanically.
  11. (9) The identification of the mapping from source program objects to machine resources is allowed to be in the form of an annotated object listing, in human-readable or tool-processable form.

Safety and Security Restrictions

  1. This clause defines restrictions that can be used with pragma Restrictions, see section Pragma Restrictions, these facilitate the demonstration of program correctness by allowing tailored versions of the run-time system. Static Semantics
  2. The following restrictions, the same as in section Tasking Restrictions, apply in this Annex: No_Task_Hierarchy, No_Abort_Statement, No_Implicit_Heap_Allocation, Max_Task_Entries is 0, Max_Asynchronous_Select_Nesting is 0, and Max_Tasks is 0. The last three restrictions are checked prior to program execution.
  3. The following additional restrictions apply in this Annex.
  4. Tasking-related restriction:
  5. No_Protected_Types
    There are no declarations of protected types or protected
    objects.
    
  6. Memory-management related restrictions:
  7. No_Allocators
    There are no occurrences of an allocator.
    
  8. No_Local_Allocators
    Allocators are prohibited in subprograms, generic sub-programs,
    tasks, and entry bodies; instantiations of generic
    packages are also prohibited in these contexts.
    
  9. No_Unchecked_Deallocation
    Semantic dependence on Unchecked_Deallocation is not allowed.
    
  10. Immediate_Reclamation
    Except for storage occupied by objects created by allocators
    and not deallocated via unchecked deallocation, any storage
    reserved at run time for an object is immediately reclaimed
    when the object no longer exists.
    
  11. Exception-related restriction:
  12. No_Exceptions
    Raise_statements and exception_handlers are not allowed. No
    language-defined run-time checks are generated; however, a
    run-time check performed automatically by the hardware is
    permitted.
    
  13. Other restrictions:
  14. No_Floating_Point
    Uses of predefined floating point types and operations, and
    declarations of new floating point types, are not allowed.
    
  15. No_Fixed_Point
    Uses of predefined fixed point types and operations, and
    declarations of new fixed point types, are not allowed.
    
  16. No_Unchecked_Conversion
    Semantic dependence on the predefined generic
    Unchecked_Conversion is not allowed.
    
  17. No_Access_Subprograms
    The declaration of access-to-subprogram types is not allowed.
    
  18. No_Unchecked_Access
    The Unchecked_Access attribute is not allowed.
    
  19. No_Dispatch
    Occurrences of T'Class are not allowed, for any (tagged)
    subtype T.
    
  20. No_IO
    Semantic dependence on any of the library units
    Sequential_IO, Direct_IO, Text_IO, Wide_Text_IO, or Stream_IO
    is not allowed.
    
  21. No_Delay
    Delay_Statements and semantic dependence on package Calendar
    are not allowed.
    
  22. No_Recursion
    As part of the execution of a subprogram, the same subprogram
    is not invoked.
    
  23. No_Reentrancy
    During the execution of a subprogram by a task, no other task
    invokes the same subprogram.
    
    Implementation Requirements
  24. If an implementation supports pragma Restrictions for a particular argument, then except for the restrictions No_Unchecked_Deallocation, No_Unchecked_Conversion, No_Access_Subprograms, and No_Unchecked_Access, the associated restriction applies to the run-time system. Documentation Requirements
  25. If a pragma Restrictions(No_Exceptions) is specified, the implementation shall document the effects of all constructs where language-defined checks are still performed automatically (for example, an overflow check performed by the processor). Erroneous Execution
  26. Program execution is erroneous if pragma Restrictions(No_Exceptions) has been specified and the conditions arise under which a generated language-defined run-time check would fail.
  27. Program execution is erroneous if pragma Restrictions(No_Recursion) has been specified and a subprogram is invoked as part of its own execution, or if pragma Restrictions(No_Reentrancy) has been specified and during the execution of a subprogram by a task, another task invokes the same subprogram.


Go to the first, previous, next, last section, table of contents.