Annex H
(normative)
High Integrity Systems
1/2 {AI95-00347-01} {safety-critical systems} {secure systems} 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. {unspecified [partial]}
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.
6.a Discussion: The Annex tries to provide high assurance rather than
language features. However, it is not possible, in general, to
test for high assurance. For any specific language feature, it is
possible to demonstrate its presence by a functional test, as in
the ACVC. One can also check for the presence of some
documentation requirements, but it is not easy to determine
objectively that the documentation is "adequate".
Extensions to Ada 83
6.b {extensions to Ada 83} This Annex is new to Ada 95.
Wording Changes from Ada 95
6.c/2 {AI95-00347-01} The title of this annex was changed to better
reflect its purpose and scope. High integrity systems has become
the standard way of identifying systems that have high reliability
requirements; it subsumes terms such as safety and security.
Moreover, the annex does not include any security specific
features and as such the previous title is somewhat misleading.
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.
1.a Discussion: The goal of the pragma is to reduce the impact of a
bounded error that results from a reference to an uninitialized
scalar object, by having such a reference violate a range check
and thus raise Constraint_Error.
Syntax
2 The form of a pragma Normalize_Scalars is as follows:
3 pragma Normalize_Scalars;
Post-Compilation Rules
4 {configuration pragma (Normalize_Scalars) [partial]}
{pragma, configuration (Normalize_Scalars) [partial]} Pragma Normalize_Scalars
is a configuration pragma. It applies to all compilation_units included in a
partition.
Documentation Requirements
5/2 {AI95-00434-01} 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.
5.a/2 Documentation Requirement: If a pragma Normalize_Scalars applies,
the implicit initial values of scalar subtypes shall be
documented. Such a value should be an invalid representation when
possible; any cases when is it not shall be documented.
5.b To be honest: It's slightly inaccurate to say that the value is a
representation, but the point should be clear anyway.
5.c Discussion: By providing a type with a size specification so that
spare bits are present, it is possible to force an implementation
of Normalize_Scalars to use an out of range value. This can be
tested for by ensuring that Constraint_Error is raised. Similarly,
for an unconstrained integer type, in which no spare bit is surely
present, one can check that the initialization takes place to the
value specified in the documentation of the implementation. For a
floating point type, spare bits might not be available, but a
range constraint can provide the ability to use an out of range
value.
5.d If it is difficult to document the general rule for the implicit
initial value, the implementation might choose instead to record
the value on the object code listing or similar output produced
during compilation.
Implementation Advice
6/2 {AI95-00434-01} Whenever possible, the implicit initial values for a
scalar subtype should be an invalid representation (see 13.9.1).
6.a Discussion: When an out of range value is used for the
initialization, it is likely that constraint checks will detect
it. In addition, it can be detected by the Valid attribute.
6.b/2 This rule is included in the documentation requirements, and thus
does not need a separate summary item.
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).
9.a Discussion: Since the effect of an access to an out of range value
will often be to raise Constraint_Error, it is clear that
suppressing the exception mechanism could result in erroneous
execution. In particular, the assignment to an array, with the
array index out of range, will result in a write to an arbitrary
store location, having unpredictable effects.
H.2 Documentation of Implementation Decisions
Documentation Requirements
1 {unspecified [partial]} 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.]
1.a/2 This paragraph was deleted.
1.b/2 Documentation Requirement: The range of effects for each bounded
error and each unspecified effect. If the effects of a given
erroneous construct are constrained, the constraints shall be
documented.
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.
2.a Discussion: Look up "unspecified" and "erroneous execution" in the
index for a list of the cases.
2.b The management of run-time storage is particularly important. For
safety applications, it is often necessary to show that a program
cannot raise Storage_Error, and for security applications that
information cannot leak via the run-time system. Users are likely
to prefer a simple storage model that can be easily validated.
2.c The documentation could helpfully take into account that users may
well adopt a subset to avoid some forms of erroneous execution,
for instance, not using the abort statement, so that the effects
of a partly completed assignment_statement do not have to be
considered in the validation of a program (see 9.8). For this
reason documentation linked to an actual compilation may be most
useful. Similarly, an implementation may be able to take into
account use of the Restrictions pragma.
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.
1.a Discussion: Since the purpose of this pragma is to provide
information to the user, it is hard to objectively test for
conformity. In practice, users want the information in an easily
understood and convenient form, but neither of these properties
can be easily measured.
Syntax
2 The form of a pragma Reviewable is as follows:
3 pragma Reviewable;
Post-Compilation Rules
4 {configuration pragma (Reviewable) [partial]}
{pragma, configuration (Reviewable) [partial]} 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:
5.a Discussion: The list of requirements can be checked for, even if
issues like intelligibility are not addressed.
6 * Where compiler-generated run-time checks remain;
6.a Discussion: A constraint check which is implemented via a check on
the upper and lower bound should clearly be indicated. If a check
is implicit in the form of machine instructions used (such an
overflow checking), this should also be covered by the
documentation. It is particularly important to cover those checks
which are not obvious from the source code, such as that for stack
overflow.
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);
7.a Discussion: In this case, if the compiler determines that a check
must fail, the user should be informed of this. However, since it
is not in general possible to know what the compiler will detect,
it is not easy to test for this. In practice, it is thought that
compilers claiming conformity to this Annex will perform
significant optimizations and therefore will detect such
situations. Of course, such events could well indicate a
programmer error.
8/2 * {AI95-00209-01} 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;
8.a Discussion: This issue again raises the question as to what the
compiler has determined. A lazy implementation could clearly mark
all scalars as "possibly uninitialized", but this would be very
unhelpful to the user. It should be possible to analyze a range of
scalar uses and note the percentage in each class. Note that an
access marked "known to be initialized" does not imply that the
value is in range, since the initialization could be from an
(erroneous) call of unchecked conversion, or by means external to
the Ada program.
9 * Where run-time support routines are implicitly invoked;
9.a Discussion: Validators will need to know the calls invoked in
order to check for the correct functionality. For instance, for
some safety applications, it may be necessary to ensure that
certain sections of code can execute in a particular time.
10 * An object code listing, including:
11 * Machine instructions, with relative offsets;
11.a Discussion: The machine instructions should be in a format that is
easily understood, such as the symbolic format of the assembler.
The relative offsets are needed in numeric format, to check any
alignment restrictions that the architecture might impose.
12 * Where each data object is stored during its lifetime;
12.a Discussion: This requirement implies that if the optimizer assigns
a variable to a register, this needs to be evident.
13 * Correspondence with the source program, including an
identification of the code produced per declaration and per
statement.
13.a Discussion: This correspondence will be quite complex when
extensive optimization is performed. In particular, address
calculation to access some data structures could be moved from the
actual access. However, when all the machine code arising from a
statement or declaration is in one basic block, this must be
indicated by the implementation.
14 * An identification of each construct for which the implementation
detects the possibility of erroneous execution;
14.a Discussion: This requirement is quite vague. In general, it is
hard for compilers to detect erroneous execution and therefore the
requirement will be rarely invoked. However, if the pragma
Suppress is used and the compiler can show that a predefined
exception will be raised, then such an identification would be
useful.
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.
15.a Discussion: This requirement is vital for those requiring to show
that the storage available to a program is sufficient. This is
crucial in those cases in which the internal checks for stack
overflow are suppressed (perhaps by pragma
Restrictions(No_Exceptions)).
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;
17.a Discussion: The object code listing should enable a validator to
estimate upper bounds for the time taken by critical parts of a
program. Similarly, by an analysis of the entire partition, it
should be possible to ensure that the storage requirements are
suitably bounded, assuming that the partition was written in an
appropriate manner.
18 * A description of the run-time model relevant to the partition.
18.a Discussion: For example, a description of the storage model is
vital, since the Ada language does not explicitly define such a
model.
18.1 The implementation shall provide control- and data-flow information, both
within each compilation unit and across the compilation units of the
partition.
18.b Discussion: This requirement is quite vague, since it is unclear
what control and data flow information the compiler has produced.
It is really a plea not to throw away information that could be
useful to the validator. Note that the data flow information is
relevant to the detection of "possibly uninitialized" objects
referred to above.
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.
19.a/2 Implementation Advice: The information produced by pragma
Reviewable should be provided in both a human-readable and
machine-readable form, and the latter form should be documented.
20 Object code listings should be provided both in a symbolic format and also
in an appropriate numeric format (such as hexadecimal or octal).
20.a/2 Implementation Advice: Object code listings should be provided
both in a symbolic format and in a numeric format.
20.b Reason: This is to enable other tools to perform any analysis that
the user needed to aid validation. The format should be in some
agreed form.
NOTES
21 6 The order of elaboration of library units will be documented even
in the absence of pragma Reviewable (see 10.2).
21.a Discussion: There might be some interactions between pragma
Reviewable and compiler optimizations. For example, an
implementation may disable some optimizations when pragma
Reviewable is in force if it would be overly complicated to
provide the detailed information to allow review of the optimized
object code. See also pragma Optimize (2.8).
Wording Changes from Ada 95
21.b/2 {AI95-00209-01} The wording was clarified that pragma Reviewable
applies to each read of an object, as it makes no sense to talk
about the state of an object that will immediately be overwritten.
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.
1.a Discussion: Inspection points are a high level equivalent of break
points used by debuggers.
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.
4.a Discussion: The static denotation is required, since no dynamic
evaluation of a name is involved in this pragma.
Static Semantics
5/2 {8652/0093} {AI95-00207-01} {AI95-00434-01} {inspection point} An
inspection point is a point in the object code corresponding to the occurrence
of a pragma Inspection_Point in the compilation unit. {inspectable object} 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.
5.a Ramification: If a pragma Inspection_Point is in an in-lined
subprogram, there might be numerous inspection points in the
object code corresponding to the single occurrence of the pragma
in the source; similar considerations apply if such a pragma is in
a generic, or in a loop that has been "unrolled" by an optimizer.
5.a.1/1 {8652/0093} {AI95-00207-01} The short form of the pragma is a
convenient shorthand for listing all objects which could be
explicitly made inspectable by the long form of the pragma; thus
only visible objects are made inspectable by it. Objects that are
not visible at the point of the pragma are not made inspectable by
the short form pragma. This is necessary so that implementations
need not keep information about (or prevent optimizations on) a
unit simply because some other unit might contain a short form
Inspection_Point pragma.
5.b/1 Discussion: {8652/0093} {AI95-00207-01} If the short form of the
pragma is used, then all visible objects are inspectable. This
implies that global objects from other compilation units are
inspectable. A good interactive debugging system could provide
information similar to a post-mortem dump at such inspection
points. The annex does not require that any inspection facility is
provided, merely that the information is available to understand
the state of the machine at those points.
Dynamic Semantics
6 Execution of a pragma Inspection_Point has no effect.
6.a/2 Discussion: {AI95-00114-01} Although an inspection point has no
(semantic) effect, the removal or adding of a new point could
change the machine code generated by the compiler.
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).
7.a Ramification: The compiler is inhibited from moving an assignment
to an inspectable variable past an inspection point for that
variable. On the other hand, the evaluation of an expression that
might raise an exception may be moved past an inspection point
(see 11.6).
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.
8.a/2 This paragraph was deleted.
8.b/2 Documentation Requirement: For each inspection point, a mapping
between each inspectable object and the machine resources where
the object's value can be obtained shall be provided.
NOTES
9/2 7 {AI95-00209-01} 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.
10.a Discussion: Although it is not a requirement of the annex, it
would be useful if the state of the stack and heap could be
interrogated. This would allow users to check that a program did
not have a `storage leak'.
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.
11.a Discussion: In principle, it is easy to check an implementation
for this pragma, since one merely needs to check the content of
objects against those values known from the source listing. In
practice, one needs a tool similar to an interactive debugger to
perform the check.
Wording Changes from Ada 95
11.b/2 {8652/0093} {AI95-00207-01} Corrigendum: Corrected the definition
of the Inspection_Point pragma to apply to only variables visible
at the point of the pragma. Otherwise, the compiler would have to
assume that some other code somewhere could have a pragma
Inspection_Point, preventing many optimizations (such as unused
object elimination).
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.
1.a Discussion: Note that the restrictions are absolute. If a
partition has 100 library units and just one needs
Unchecked_Conversion, then the pragma cannot be used to ensure the
other 99 units do not use Unchecked_Conversion. Note also that
these are restrictions on all Ada code within a partition, and
therefore it may not be evident from the specification of a
package whether a restriction can be imposed.
Static Semantics
2/2 This paragraph was deleted.{AI95-00347-01} {AI95-00394-01}
3/2 {AI95-00394-01} The following restriction_identifiers are language defined:
4 Tasking-related restriction:
5 {Restrictions (No_Protected_Types)} No_Protected_Types
There are no declarations of protected types or protected
objects.
6 Memory-management related restrictions:
7 {Restrictions (No_Allocators)} No_Allocators
There are no occurrences of an allocator.
8/1 {8652/0042} {AI95-00130} {Restrictions (No_Local_Allocators)}
No_Local_Allocators
Allocators are prohibited in subprograms, generic subprograms,
tasks, and entry bodies.
8.a Ramification: Thus allocators are permitted only in expressions
whose evaluation can only be performed before the main subprogram
is invoked.
8.b/1 This paragraph was deleted.{8652/0042} {AI95-00130}
9/2 This paragraph was deleted.{AI95-00394-01}
9.a/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.
{Restrictions (Immediate_Reclamation)}
10.a Discussion: Immediate reclamation would apply to storage created
by the compiler, such as for a return value from a function whose
size is not known at the call site.
11 Exception-related restriction:
12 {Restrictions (No_Exceptions)} 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.
12.a Discussion: This restriction mirrors a method of working that is
quite common in the safety area. The programmer is required to
show that exceptions cannot be raised. Then a simplified run-time
system is used without exception handling. However, some hardware
checks may still be enforced. If the software check would have
failed, or if the hardware check actually fails, then the
execution of the program is unpredictable. There are obvious
dangers in this approach, but it is similar to programming at the
assembler level.
13 Other restrictions:
14 {Restrictions (No_Floating_Point)} No_Floating_Point
Uses of predefined floating point types and operations, and
declarations of new floating point types, are not allowed.
14.a/2 Discussion: {AI95-00114-01} The intention is to avoid the use of
floating point hardware at run time, but this is expressed in
language terms. It is conceivable that floating point is used
implicitly in some contexts, say fixed point type conversions of
high accuracy. However, the Implementation Requirements below make
it clear that the restriction would apply to the "run-time
system" and hence not be allowed. This restriction could be used to
inform a compiler that a variant of the architecture is being used
which does not have floating point instructions.
15 {Restrictions (No_Fixed_Point)} No_Fixed_Point
Uses of predefined fixed point types and operations, and
declarations of new fixed point types, are not allowed.
15.a Discussion: This restriction would have the side-effect of
prohibiting the delay_relative_statement. As with the
No_Floating_Point restriction, this might be used to avoid any
question of rounding errors. Unless an Ada run-time is written in
Ada, it seems hard to rule out implicit use of fixed point, since
at the machine level, fixed point is virtually the same as integer
arithmetic.
16/2 This paragraph was deleted.{AI95-00394-01}
16.a/2 This paragraph was deleted.
17 No_Access_Subprograms
The declaration of access-to-subprogram types is not allowed.
{Restrictions (No_Access_Subprograms)}
17.a.1/2 Discussion: Most critical applications would require some
restrictions or additional validation checks on uses of
access-to-subprogram types. If the application does not require
the functionality, then this restriction provides a means of
ensuring the design requirement has been satisfied. The same
applies to several of the following restrictions, and to
restriction No_Dependence => Ada.Unchecked_Conversion.
18 {Restrictions (No_Unchecked_Access)} No_Unchecked_Access
The Unchecked_Access attribute is not allowed.
19 {Restrictions (No_Dispatch)} No_Dispatch
Occurrences of T'Class are not allowed, for any (tagged)
subtype T.
20/2 {AI95-00285-01} {Restrictions (No_IO)} 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.
20.a Discussion: Excluding the input-output facilities of an
implementation may be needed in those environments which cannot
support the supplied functionality. A program in such an
environment is likely to require some low level facilities or a
call on a non-Ada feature.
21 {Restrictions (No_Delay)} No_Delay
Delay_Statements and semantic dependence on package Calendar
are not allowed.
21.a Ramification: This implies that delay_alternatives in a
select_statement are prohibited.
21.b The purpose of this restriction is to avoid the need for timing
facilities within the run-time system.
22 {Restrictions (No_Recursion)} No_Recursion
As part of the execution of a subprogram, the same subprogram
is not invoked.
23 {Restrictions (No_Reentrancy)} No_Reentrancy
During the execution of a subprogram by a task, no other task
invokes the same subprogram.
Implementation Requirements
23.1/2 {AI95-00394-01} 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 * {AI95-00347-01} the pragma Profile(Ravenscar); and
23.a/2 Discussion: {AI95-00347-01} The reference to pragma
Profile(Ravenscar) is intended to show that properly restricted
tasking is appropriate for use in high integrity systems. The Ada
95 Annex seemed to suggest that tasking was inappropriate for such
systems.
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.
24.a Reason: Permission is granted for the run-time system to use the
specified otherwise-restricted features, since the use of these
features may simplify the run-time system by allowing more of it
to be written in Ada.
24.b Discussion: The restrictions that are applied to the partition are
also applied to the run-time system. For example, if
No_Floating_Point is specified, then an implementation that uses
floating point for implementing the delay statement (say) would
require that No_Floating_Point is only used in conjunction with
No_Delay. It is clearly important that restrictions are effective
so that Max_Tasks=0 does imply that tasking is not used, even
implicitly (for input-output, say).
24.c An implementation of tasking could be produced based upon a
run-time system written in Ada in which the rendezvous was
controlled by protected types. In this case, No_Protected_Types
could only be used in conjunction with Max_Task_Entries=0. Other
implementation dependencies could be envisaged.
24.d If the run-time system is not written in Ada, then the wording
needs to be applied in an appropriate fashion.
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).
25.a/2 This paragraph was deleted.
25.b/2 Documentation Requirement: If a pragma Restrictions(No_Exceptions)
is specified, the effects of all constructs where language-defined
checks are still performed.
25.c/2 Discussion: {AI95-00114-01} The documentation requirements here
are quite difficult to satisfy. One method is to review the object
code generated and determine the checks that are still present,
either explicitly, or implicitly within the architecture. As
another example from that of overflow, consider the question of
dereferencing a null pointer. This could be undertaken by a memory
access trap when checks are performed. When checks are suppressed
via the argument No_Exceptions, it would not be necessary to have
the memory access trap mechanism enabled.
Erroneous Execution
26 {erroneous execution (cause) [partial]} 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.
26.a Discussion: The situation here is very similar to the application
of pragma Suppress. Since users are removing some of the
protection the language provides, they had better be careful!
27 {erroneous execution (cause) [partial]} 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.
27.a Discussion: In practice, many implementations may not exploit the
absence of recursion or need for reentrancy, in which case the
program execution would be unaffected by the use of recursion or
reentrancy, even though the program is still formally erroneous.
27.b/2 This paragraph was deleted.
NOTES
28/2 10 {AI95-00394-01} 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.
28.a/2 Discussion: The specific mention of these two uses is meant to
replace the identifiers now banished to J.13, "
Dependence Restriction Identifiers".
28.b/2 Restriction No_Dependence => Ada.Unchecked_Deallocation would be
useful in those contexts in which heap storage is needed on
program start-up, but need not be increased subsequently. The
danger of a dangling pointer can therefore be avoided.
Extensions to Ada 95
28.c/2 {8652/0042} {AI95-00130-01} {extensions to Ada 95}
No_Local_Allocators no longer prohibits generic instantiations.
Wording Changes from Ada 95
28.d/2 {AI95-00285-01} Wide_Wide_Text_IO (which is new) is added to the
No_IO restriction.
28.e/2 {AI95-00347-01} The title of this clause was changed to match the
change to the Annex title. Pragma Profile(Ravenscar) is part of
this annex.
28.f/2 {AI95-00394-01} Restriction No_Dependence is used instead of
special restriction_identifiers. The old names are banished to
Obsolescent Features (see J.13).
28.g/2 {AI95-00394-01} The bizarre wording "apply in this Annex" (which
no one quite can explain the meaning of) is banished.
H.5 Pragma Detect_Blocking
1/2 {AI95-00305-01} The following pragma forces an implementation to detect
potentially blocking operations within a protected operation.
Syntax
2/2 {AI95-00305-01} The form of a pragma Detect_Blocking is as follows:
3/2 pragma Detect_Blocking;
Post-Compilation Rules
4/2 {AI95-00305-01} {configuration pragma (Detect_Blocking) [partial]}
{pragma, configuration (Detect_Blocking) [partial]} A pragma Detect_Blocking is
a configuration pragma.
Dynamic Semantics
5/2 {AI95-00305-01} 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 {AI95-00305-01} 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 {AI95-00305-01} 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.
Extensions to Ada 95
7.a/2 {AI95-00305-01} {extensions to Ada 95} Pragma Detect_Blocking is
new.
H.6 Pragma Partition_Elaboration_Policy
1/2 {AI95-00265-01} This clause defines a pragma for user control over
elaboration policy.
Syntax
2/2 {AI95-00265-01} 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.
4.a/2 Implementation defined: Implementation-defined policy_identifiers
allowed in a pragma Partition_Elaboration_Policy.
Post-Compilation Rules
5/2 {AI95-00265-01} {configuration pragma (Partition_Elaboration_Policy)
[partial]} {pragma, configuration (Partition_Elaboration_Policy) [partial]} 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 {AI95-00265-01} 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 {AI95-00265-01} 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 {AI95-00265-01} {AI95-00421-01} 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 {AI95-00265-01} {AI95-00421-01} 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 {AI95-00265-01} {AI95-00421-01} 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 {AI95-00265-01} 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.
15.a/2 Implementation Advice: If the partition elaboration policy is
Sequential and the Environment task becomes permanently blocked
during elaboration then the partition should be immediately
terminated.
Implementation Permissions
16/2 {AI95-00265-01} 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 {AI95-00421-01} 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.
Extensions to Ada 95
17.a/2 {AI95-00265-01} {AI95-00421-01} {extensions to Ada 95} Pragma
Partition_Elaboration_Policy is new.
Generated by dwww version 1.15 on Wed May 22 21:40:21 CEST 2024.