H.4 High Integrity Restrictions
This subclause defines restrictions that can be used with pragma Restrictions
); these facilitate the demonstration
of program correctness by allowing tailored versions of the run-time
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 might not be evident from the specification of a package
whether a restriction can be imposed.
There are no declarations of protected types or protected objects.
There are no occurrences of an allocator
are prohibited in subprograms, generic subprograms, tasks, and entry
are permitted only in expressions whose evaluation can only be performed
before the main subprogram is invoked.
There are no allocator
of anonymous access types.
There are no coextensions. See 3.10.2
are not permitted as the actual parameter to an access parameter. See
Except for storage occupied by objects created by allocator
and not deallocated via unchecked deallocation, any storage reserved
at run time for an object is immediately reclaimed when the object no
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.
are not allowed. No language-defined runtime checks are generated; however,
a runtime check performed automatically by the hardware is permitted.
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.
Uses of predefined floating point types and operations, and declarations
of new floating point types, are not allowed.
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.
Uses of predefined fixed point types and operations, and declarations
of new fixed point types, are not allowed.
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.
The declaration of access-to-subprogram types is not allowed.
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.
is not allowed.
Occurrences of T'Class are not allowed, for any (tagged) subtype T.
Semantic dependence on any of the library units Sequential_IO, Direct_IO,
Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, or Stream_IO,
or Directories is not allowed.
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
and semantic dependence on package Calendar are not allowed.
The purpose of this restriction is to avoid
the need for timing facilities within the run-time system.
As part of the execution of a subprogram, the same subprogram is not
During the execution of a subprogram by a task, no other task invokes
the same subprogram.
No library-level entity shall have a Global aspect
of Unspecified, either explicitly or by default. No library-level entity
shall have a Global'Class aspect of Unspecified, explicitly or by default,
if it is used as part of a dispatching call.
need not be specified on an operation if there are no dispatching calls
to the operation, or if all of the dispatching calls are covered by dispatching_operation_specifiers
for operations with such calls (see H.7).
When within a context where the applicable Global
aspect is neither Unspecified nor in out all, any execution within
such a context does neither of the following:
Update a variable
that is reachable via a sequence of zero or more dereferences of access-to-object
values from a formal parameter of mode in (after any overriding
– see H.7), or from a global that is
not within the applicable global variable set, or has mode in;
Read a variable
that is updatable via a sequence of zero or more dereferences of access-to-object
values from a global that is not within the applicable global variable
above two rules specify that any indirect references are covered by the
Global or formal parameter modes that apply, and are not subject
to alternative paths of access (such as aliasing) that could result in
For the purposes
of the above rules, if an applicable global variable set includes a package
name, and the collection of some pool-specific access type (see 7.6.1)
is implicitly declared in a part of the declarative region of the package
included within the global variable set, then all objects allocated from
that collection are considered included within the global variable set.
of violating the No_Hidden_Indirect_Globals restriction is implementation-defined.
Any aspects or other means for identifying such violations prior to or
during execution are implementation-defined.
The consequences of violating No_Hidden_Indirect_Globals.
do not make violations automatically erroneous, because if the implementation
chooses to never fully trust it, there is nothing erroneous that can
happen. If an implementation chooses to trust the restriction, and performs
some optimization as a result of the restriction, the implementation
would define such a violation as erroneous. Such an implementation might
also endeavor to detect most violations, perhaps by providing additional
aspects, thereby reducing the situations which result in erroneous execution.
Implementations might detect some but not all violations of the restrictions.
Implementations that completely ignore the restriction should treat the
restriction as an unsupported capability of Annex
H, “High Integrity Systems”.
Specifies the maximum length for the result of
an Image, Wide_Image, or Wide_Wide_Image attribute. Violation of this
restriction results in the raising of Program_Error at the point of the
invocation of an image attribute.
the restrictions defined in this subclause; and
the following restrictions defined in D.7
No_Task_Hierarchy, No_Abort_Statement, No_Implicit_Heap_Allocation, No_Standard_Allocators_After_Elaboration;
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
the following uses
defined in D.7
[, which are checked prior to
Max_Task_Entries => 0,
=> 0, and
Max_Tasks => 0.
If a Max_Image_Length restriction applies to any
compilation unit in the partition, then for any subtype S, S'Image, S'Wide_Image,
and S'Wide_Wide_Image shall be implemented within that partition without
any dynamic allocation.
Assuming the Implementation Advice is followed,
this can be accomplished by using an object of the Text_Buffers.Bounded.Buffer_Type
with the maximum characters as specified in the Max_Image_Length restriction.
If an implementation supports pragma
Restrictions for a particular argument, then except for the restrictions
No_Access_Subprograms, No_Unchecked_Access, No_Specification_of_Aspect,
No_Use_of_Attribute, No_Use_of_Pragma, No_Dependence
equivalent use of
No_Dependence => Ada.Unchecked_Deallocation
the associated restriction applies to the run-time system.
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.
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,
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.
If the run-time system is not written in Ada,
then the wording needs to be applied in an appropriate fashion.
"the equivalent use of No_Dependence"
refers to No_Dependence => Ada.Unchecked_Conversion and the
like, not all uses of No_Dependence.
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).
Documentation Requirement: If a pragma
Restrictions(No_Exceptions) is specified, the effects of all constructs
where language-defined checks are still performed.
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.
Program execution is erroneous
if pragma Restrictions(No_Exceptions) has been specified and the conditions
arise under which a generated language-defined runtime check would fail.
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!
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.
In practice, many implementations might 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.
Uses of restriction_parameter_identifier
No_Dependence defined in 13.12.1
=> 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.
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
Wording Changes from Ada 95
Wide_Wide_Text_IO (which is new) is added to the No_IO restriction.
The title of this subclause was changed to match the change to the Annex
title. Pragma Profile(Ravenscar) is part of this annex.
Restriction No_Dependence is used instead of special restriction_identifier
The old names are banished to Obsolescent Features (see J.13
The bizarre wording “apply in this Annex” (which no one quite
can explain the meaning of) is banished.
Extensions to Ada 2005
Restrictions No_Anonymous_Allocators, No_Coextensions,
and No_Access_Parameter_Allocators are new.
Wording Changes from Ada 2005
New restriction No_Standard_Allocators_After_Elaboration is added to
the list of restrictions that are required by this annex.
Ada 2005 restriction No_Dependence is added where
needed (this was missed in Ada 2005).
Restrictions against individual aspects, pragmas, and attributes do not
apply to the run-time system, in order that an implementation can use
whatever aspects, pragmas, and attributes are needed to do the job. For
instance, attempting to write a run-time system for Linux that does not
use the Import aspect would be very difficult and probably is not what
the user is trying to prevent anyway.
Incompatibilities With Ada 2012
No_IO now excludes use of Ada.Directories. If a program using No_IO used
Ada.Directories, it would be legal in Ada 2012 and illegal in Ada 202x.
However, given the role of Ada.Directories as a support package for the
other packages that are excluded by No_IO, it seems unlikely that any
use of the restriction would use this package (and it's possible that
implementations wouldn't support its use with No_IO anyway).
Extensions to Ada 2012
Restrictions No_Unspecified_Globals and No_Hidden_Indirect_Globals
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe