Prev | Up | ____ | Back | Forward
TOC -- / --.-- / --.--.-- | Index | Search | Syntax | Help


H.4 Safety and Security Restrictions

(1)
This clause 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)
The following restrictions, the same as in D.7, apply in this Annex: No_Task_Hierarchy, No_Abort_Statement, No_Implicit_Heap_Allocation, Max_Task_Entries is 0, Max_Asynchronous_Select_Nesting is 0, and Max_Tasks is 0. The last three restrictions are checked prior to program execution.
(3)
The following additional restrictions apply in this Annex.
(4)
Tasking-related restriction:
(5)
No_Protected_Types
(6)
Memory-management related restrictions:
(7)
No_Allocators
(8)
No_Local_Allocators
(9)
No_Unchecked_Deallocation
(10)
Immediate_Reclamation
(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)
       No_Unchecked_Conversion
                   Semantic dependence on the predefined generic Unchecked_Conversion is not allowed.
(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)
       No_IO
                   Semantic dependence on any of the library units
                   Sequential_IO, Direct_IO, Text_IO, 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
(24)
If an implementation supports pragma Restrictions for a particular argument, then except for the restrictions No_Unchecked_Deallocation, No_Unchecked_Conversion, No_Access_Subprograms, and No_Unchecked_Access, 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.


Prev | Up | ____ | Back | Forward
TOC -- / --.-- / --.--.-- | Index | Search | Syntax | Help

Ada WWW Home -- Email comments, additions, corrections, gripes, kudos, etc. to:

Magnus Kempe -- Magnus.Kempe@di.epfl.ch
Copyright statement
Page last generated: 95-03-12