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 run-time checks are generated; however, 
a run-time check performed automatically by the hardware is permitted. 
 
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, or Stream_IO 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.
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 an implementation supports 
pragma 
Restrictions for a particular argument, then except for the restrictions 
No_Unchecked_Deallocation, No_Unchecked_Conversion, No_Access_Subprograms, 
No_Unchecked_Access, No_Specification_of_Aspect, No_Use_of_Attribute, 
No_Use_of_Pragma, and the equivalent use of No_Dependence, 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 run-time 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. 
 
10  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. 
 
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe