Annex H
(normative)
High Integrity Systems
1/2 This Annex addresses requirements for high integrity systems (including
safety-critical systems and security-critical systems). It provides facilities
and specifies documentation requirements that relate to several needs:
2 * Understanding program execution;
3 * Reviewing object code;
4 * Restricting language constructs whose usage might complicate the
demonstration of program correctness
4.1 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.
5 The pragmas Reviewable and Restrictions relate to the other requirements
addressed by this Annex.
NOTES
6 1 The Valid attribute (see 13.9.2) is also useful in addressing these
needs, to avoid problems that could otherwise arise from scalars that
have values outside their declared range constraints.
H.1 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/2 If a pragma Normalize_Scalars applies, the implementation shall document
the implicit initial values for scalar subtypes, and shall identify each case
in which such a value is used and is not an invalid representation.
Implementation Advice
6/2 Whenever possible, the implicit initial values for a scalar subtype should
be an invalid representation (see 13.9.1).
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
6.4.1.
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
B.1).
9 4 The use of pragma Normalize_Scalars in conjunction with Pragma
Restrictions(No_Exceptions) may result in erroneous execution (see
H.4).
H.2 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 1.1.3, and 1.1.2.
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.
H.3 Reviewable Object Code
1 Object code review and validation are supported by pragmas Reviewable and
Inspection_Point.
H.3.1 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:
6 * Where compiler-generated run-time checks remain;
7 * 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);
8/2 * For each read of a scalar object, an identification of the read as
either "known to be initialized," or "possibly uninitialized,"
independent of whether pragma Normalize_Scalars applies;
9 * Where run-time support routines are implicitly invoked;
10 * An object code listing, including:
11 * Machine instructions, with relative offsets;
12 * Where each data object is stored during its lifetime;
13 * Correspondence with the source program, including an
identification of the code produced per declaration and per
statement.
14 * An identification of each construct for which the implementation
detects the possibility of erroneous execution;
15 * 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.
16 The implementation shall provide the following information for any
partition to which the pragma applies:
17 * 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;
18 * A description of the run-time model relevant to the partition.
18.1 The implementation shall provide control- and data-flow information, both
within each compilation unit and across the compilation units of the
partition.
Implementation Advice
19 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.
20 Object code listings should be provided both in a symbolic format and also
in an appropriate numeric format (such as hexadecimal or octal).
NOTES
21 6 The order of elaboration of library units will be documented even
in the absence of pragma Reviewable (see 10.2).
H.3.2 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/2 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 and the declaration of the object is visible at the inspection
point.
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 1.1.3).
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/2 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 read of 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.
H.4 High Integrity Restrictions
1 This clause defines restrictions that can be used with pragma Restrictions
(see 13.12); these facilitate the demonstration of program correctness by
allowing tailored versions of the run-time system.
Static Semantics
2/2 This paragraph was deleted.
3/2 The following restriction_identifiers are language defined:
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/1 No_Local_Allocators
Allocators are prohibited in subprograms, generic subprograms,
tasks, and entry bodies.
9/2 This paragraph was deleted.
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/2 This paragraph was deleted.
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/2 No_IO Semantic dependence on any of the library units Sequential_IO,
Direct_IO, Text_IO, Wide_Text_IO, Wide_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
23.1/2 An implementation of this Annex shall support:
23.2/2 * the restrictions defined in this subclause; and
23.3/2 * the following restrictions defined in D.7: No_Task_Hierarchy,
No_Abort_Statement, No_Implicit_Heap_Allocation; and
23.4/2 * the pragma Profile(Ravenscar); and
23.5/2 * the following uses of restriction_parameter_identifiers defined in
D.7, which are checked prior to program execution:
23.6/2 * Max_Task_Entries => 0,
23.7/2 * Max_Asynchronous_Select_Nesting => 0, and
23.8/2 * Max_Tasks => 0.
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.
NOTES
28/2 10 Uses of restriction_parameter_identifier No_Dependence defined in
13.12.1: No_Dependence => Ada.Unchecked_Deallocation and No_Dependence
=> Ada.Unchecked_Conversion may be appropriate for high-integrity
systems. Other uses of No_Dependence can also be appropriate for
high-integrity systems.
H.5 Pragma Detect_Blocking
1/2 The following pragma forces an implementation to detect potentially
blocking operations within a protected operation.
Syntax
2/2 The form of a pragma Detect_Blocking is as follows:
3/2 pragma Detect_Blocking;
Post-Compilation Rules
4/2 A pragma Detect_Blocking is a configuration pragma.
Dynamic Semantics
5/2 An implementation is required to detect a potentially blocking operation
within a protected operation, and to raise Program_Error (see 9.5.1).
Implementation Permissions
6/2 An implementation is allowed to reject a compilation_unit if a potentially
blocking operation is present directly within an entry_body or the body of a
protected subprogram.
NOTES
7/2 11 An operation that causes a task to be blocked within a foreign
language domain is not defined to be potentially blocking, and need
not be detected.
H.6 Pragma Partition_Elaboration_Policy
1/2 This clause defines a pragma for user control over elaboration policy.
Syntax
2/2 The form of a pragma Partition_Elaboration_Policy is as follows:
3/2 pragma Partition_Elaboration_Policy (policy_identifier);
4/2 The policy_identifier shall be either Sequential, Concurrent or an
implementation-defined identifier.
Post-Compilation Rules
5/2 A pragma Partition_Elaboration_Policy is a configuration pragma. It
specifies the elaboration policy for a partition. At most one elaboration
policy shall be specified for a partition.
6/2 If the Sequential policy is specified for a partition then pragma
Restrictions (No_Task_Hierarchy) shall also be specified for the partition.
Dynamic Semantics
7/2 Notwithstanding what this International Standard says elsewhere, this
pragma allows partition elaboration rules concerning task activation and
interrupt attachment to be changed. If the policy_identifier is Concurrent, or
if there is no pragma Partition_Elaboration_Policy defined for the partition,
then the rules defined elsewhere in this Standard apply.
8/2 If the partition elaboration policy is Sequential, then task activation
and interrupt attachment are performed in the following sequence of steps:
9/2 * The activation of all library-level tasks and the attachment of
interrupt handlers are deferred until all library units are elaborated.
10/2 * The interrupt handlers are attached by the environment task.
11/2 * The environment task is suspended while the library-level tasks are
activated.
12/2 * The environment task executes the main subprogram (if any)
concurrently with these executing tasks.
13/2 If several dynamic interrupt handler attachments for the same interrupt
are deferred, then the most recent call of Attach_Handler or Exchange_Handler
determines which handler is attached.
14/2 If any deferred task activation fails, Tasking_Error is raised at the
beginning of the sequence of statements of the body of the environment task
prior to calling the main subprogram.
Implementation Advice
15/2 If the partition elaboration policy is Sequential and the Environment
task becomes permanently blocked during elaboration then the partition is
deadlocked and it is recommended that the partition be immediately terminated.
Implementation Permissions
16/2 If the partition elaboration policy is Sequential and any task activation
fails then an implementation may immediately terminate the active partition to
mitigate the hazard posed by continuing to execute with a subset of the tasks
being active.
NOTES
17/2 12 If any deferred task activation fails, the environment task is
unable to handle the Tasking_Error exception and completes
immediately. By contrast, if the partition elaboration policy is
Concurrent, then this exception could be handled within a library
unit.
Generated by dwww version 1.15 on Wed May 22 15:54:55 CEST 2024.