Ada Reference ManualLegal Information
Contents   Index   References   Search   Previous   Next 

H.4 High Integrity Restrictions

1/3
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

2/2
This paragraph was deleted.
3/2
The following restriction_identifiers are language defined:
4
Tasking-related restriction:
5
No_Protected_Types

There are no declarations of protected types or protected objects. 
6
Memory-management related restrictions:
7
No_Allocators
There are no occurrences of an allocator.
8/1
No_Local_Allocators

Allocators are prohibited in subprograms, generic subprograms, tasks, and entry bodies. 
8.1/3
  No_Anonymous_Allocators

There are no allocators of anonymous access types.
8.2/3
  No_Coextensions

There are no coextensions. See 3.10.2.
8.3/3
  No_Access_Parameter_Allocators

Allocators are not permitted as the actual parameter to an access parameter. See 6.1.
9/2
This paragraph was deleted.
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.
11
Exception-related restriction:
12
No_Exceptions
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.
13
Other restrictions:
14
No_Floating_Point

Uses of predefined floating point types and operations, and declarations of new floating point types, are not allowed. 
15
No_Fixed_Point

Uses of predefined fixed point types and operations, and declarations of new fixed point types, are not allowed. 
16/2
 
This paragraph was deleted.
17
No_Access_Subprograms 

The declaration of access-to-subprogram types is not allowed.
18
No_Unchecked_Access

The Unchecked_Access attribute is not allowed.
19
No_Dispatch
Occurrences of T'Class are not allowed, for any (tagged) subtype T.
20/2
 No_IO
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.
21
No_Delay
Delay_Statements and semantic dependence on package Calendar are not allowed. 
22
No_Recursion
As part of the execution of a subprogram, the same subprogram is not invoked.
23
No_Reentrancy
During the execution of a subprogram by a task, no other task invokes the same subprogram.

Implementation Requirements

23.1/2
   An implementation of this Annex shall support: 
23.2/2
the restrictions defined in this subclause; and
23.3/3
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
the pragma Profile(Ravenscar); and 
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
 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

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). 

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.
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. 
NOTES
28/2
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. 

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe