H.4 High Integrity RestrictionsSafety and Security 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}
The following restrictions, the same as in D.7,
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/2
{
AI95-00394-01}
The following
restriction_identifiers
are language defined: additional restrictions
apply in this Annex.
4
Tasking-related
restriction:
5
There are no declarations of protected types or protected objects.
6
Memory-management
related restrictions:
7
There are no occurrences of an
allocator.
8/1
Allocators
are prohibited in subprograms, generic subprograms, tasks, and entry
bodies
; instantiations of generic packages are
also prohibited in these contexts.
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.Reason: {
8652/0042}
{
AI95-00130}
The reason for the prohibition against instantiations
of generic packages is to avoid contract model violations. An alternative
would be to prohibit allocators
from generic packages, but it seems preferable to allow generality on
the defining side and then place the restrictions on the usage (instantiation),
rather than inhibiting what can be in the generic while liberalizing
where they can be instantiated.
8.1/3
There are no allocators
of anonymous access types.
8.2/3
There are no coextensions. See 3.10.2.
8.3/3
Allocators
are not permitted as the actual parameter to an access parameter. See
6.1.
9/2
This paragraph
was deleted.{
AI95-00394-01}
No_Unchecked_Deallocation
Semantic dependence on Unchecked_Deallocation is
not allowed.
9.a/2
Discussion: This
restriction 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.
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.
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
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
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 parameter
could be used to inform a compiler that a variant of the architecture
is being used which does not have floating point instructions.
15
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}
No_Unchecked_Conversion
Semantic dependence on the predefined generic Unchecked_Conversion
is not allowed.
16.a/2
Discussion: Most
critical applications would require some restrictions or additional validation
checks on uses of unchecked conversion. 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.
17
No_Access_Subprograms
The declaration of access-to-subprogram types is not allowed.
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
The
Unchecked_Access attribute
is not allowed.
19
Occurrences of T'Class are not allowed, for any (tagged) subtype T.
20/2
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
Delay_Statements
and semantic dependence on package Calendar are not allowed.
21.a
21.b
The purpose of this restriction is to avoid
the need for timing facilities within the run-time system.
22
As part of the execution of a subprogram, the same subprogram is not
invoked.
23
During the execution of a subprogram by a task, no other task invokes
the same subprogram.
Implementation Requirements
23.1/2
23.2/2
the restrictions defined
in this subclause; and
23.3/3
{
AI05-0189-1}
the following restrictions defined in D.7:
No_Task_Hierarchy, No_Abort_Statement, No_Implicit_Heap_Allocation,
No_Standard_Allocators_After_Elaboration;
and
23.4/2
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/3
{
AI05-0263-1}
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,
and
the equivalent use of No_Dependence, 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.Implementation defined:
Implementation-defined aspects of pragma
Restrictions.
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 deferencing
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
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
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.Implementation defined:
Any restrictions on pragma Restrictions.
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
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
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.
Extensions to Ada 2005
28.h/3
{
AI05-0152-1}
{
AI05-0190-1}
Restrictions No_Anonymous_Allocators,
No_Coextensions, and No_Access_Parameter_Allocators are new.
Wording Changes from Ada 2005
28.i/3
{
AI05-0189-1}
New restriction No_Standard_Allocators_After_Elaboration
is added to the list of restrictions that are required by this annex.
28.j/3
{
AI05-0263-1}
Correction: Ada 2005 restriction No_Dependence
is added where needed (this was missed in Ada 2005).
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe