H.4 High Integrity Restrictions
This subclause 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
This paragraph was
deleted.
The following
restriction_identifiers
are language defined:
Tasking-related
restriction:
There are no declarations of protected types or protected objects.
Memory-management
related restrictions:
There are no occurrences of an
allocator.
Allocators
are prohibited in subprograms, generic subprograms, tasks, and entry
bodies.
There are no
allocators
of anonymous access types.
There are no coextensions. See
3.10.2.
No_Access_Parameter_Allocators
Allocators
are not permitted as the actual parameter to an access parameter. See
6.1.
This paragraph was deleted.
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.
Exception-related
restriction:
Raise_statements
and
exception_handlers
are not allowed. No language-defined runtime checks are generated; however,
a runtime check performed automatically by the hardware is permitted.
The callable entity associated with a
procedural_iterator
(see
5.5.3) is considered to not allow exit,
independent of the value of its Allows_Exit aspect.
Other restrictions:
Uses of predefined floating point types and operations, and declarations
of new floating point types, are not allowed.
Uses of predefined fixed point types and operations, and declarations
of new fixed point types, are not allowed.
This paragraph was deleted.
No_Access_Subprograms
The declaration of access-to-subprogram types is not allowed.
The
Unchecked_Access attribute
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, Stream_IO, or Directories is
not allowed.
Delay_Statements
and semantic dependence on package Calendar are not allowed.
As part of the execution of a subprogram, the same subprogram is not
invoked.
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.
No_Hidden_Indirect_Globals
When within a context where an applicable global aspect is neither Unspecified
nor in out all, any execution within such a context does neither
of the following:
Update (or return a writable reference
to) a variable that is reachable via a sequence of zero or more dereferences
of access-to-object values from a parameter of a visibly access-to-constant
type, from a part of a non-access-type formal parameter of mode
in
(after any
overriding – see
H.7),
or from a global that has mode
in or is not within the applicable
global variable set, unless the initial dereference is of a part of a
formal parameter or global that is visibly of an access-to-variable type;
Read (or return a readable reference to)
a variable that is reachable via a sequence of zero or more dereferences
of access-to-object values from a global that is not within the applicable
global variable set, unless the initial dereference is of a part of a
formal parameter or global that is visibly of an access-to-object type.
For the purposes
of the above rules:
a part of an object is
visibly of an
access type if the type of the object is declared
immediately within the visible part of a package specification, and at
the point of declaration of the type the part is visible and of an access
type;
a function
returns a writable reference
to V if it returns a result with a part that
is visibly of an access-to-variable type designating
V; similarly,
a function
returns a readable reference to V
if it returns a result with a part that is visibly of an access-to-constant
type designating
V;
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.
The consequences 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.
Dynamic Semantics
The following
restriction_parameter_identifier
is language defined:
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.
Implementation Requirements
An implementation
of this Annex shall support:
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;
and
the pragma Profile(Ravenscar); and
the following uses
of
restriction_parameter_identifiers
defined in
D.7, which are checked prior to
program execution:
Max_Task_Entries => 0,
Max_Asynchronous_Select_Nesting
=> 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.
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 => Ada.Unchecked_Conversion,
and No_Dependence => Ada.Unchecked_Deallocation, the associated restriction
applies to the run-time system.
Documentation Requirements
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
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.
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.
NOTE Uses of
restriction_parameter_identifier
No_Dependence defined in
13.12.1: No_Dependence
=> Ada.Unchecked_Deallocation and No_Dependence => Ada.Unchecked_Conversion
can be appropriate for high-integrity systems. Other uses of No_Dependence
can also be appropriate for high-integrity systems.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
