Ada Reference Manual (Ada 2022)
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:
No_Protected_Types
There are no declarations of protected types or protected objects.
Memory-management related restrictions:
No_Allocators
There are no occurrences of an allocator.
No_Local_Allocators
Allocators are prohibited in subprograms, generic subprograms, tasks, and entry bodies.
No_Anonymous_Allocators
There are no allocators of anonymous access types.
No_Coextensions
There are no coextensions. See 3.10.2.
No_Access_Parameter_Allocators
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:
No_Exceptions
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:
No_Floating_Point
Uses of predefined floating point types and operations, and declarations of new floating point types, are not allowed.
No_Fixed_Point
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.
No_Unchecked_Access
The Unchecked_Access attribute is not allowed.
No_Dispatch
Occurrences of T'Class are not allowed, for any (tagged) subtype T.
No_IO
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.
No_Delay
Delay_Statements and semantic dependence on package Calendar are not allowed.
No_Recursion
As part of the execution of a subprogram, the same subprogram is not invoked.
No_Reentrancy
During the execution of a subprogram by a task, no other task invokes the same subprogram.
No_Unspecified_Globals
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:
Max_Image_Length
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.
