16. Language-Defined Pragmas (Annex L)
16.1. Ada Language-Defined Pragmas
The following Ada language-defined pragmas are supported as follows:
Pragma |
Allowed in SPARK |
Comment |
---|---|---|
All_Calls_Remote |
No |
|
Assert |
Yes |
|
Assertion_Policy |
Yes |
No effect on provability (see section “Assertion Pragmas” in the SPARK User’s Guide) |
Asynchronous |
No |
|
Atomic |
Yes |
|
Atomic_Components |
Yes |
|
Attach_Handler |
Yes |
|
Convention |
Yes |
|
CPU |
Yes |
|
Default_Storage_Pool |
No |
Restricted access types |
Detect_Blocking |
Yes |
|
Discard_Names |
No |
|
Dispatching_Domain |
No |
Ravenscar |
Elaborate |
Yes |
|
Elaborate_All |
Yes |
|
Elaborate_Body |
Yes |
|
Export |
Yes |
|
Import |
Yes |
|
Independent |
Yes |
|
Independent_Components |
Yes |
|
Inline |
Yes |
|
Inspection_Point |
Yes |
|
Interrupt_Handler |
Yes |
|
Interrupt_Priority |
Yes |
|
Linker_Options |
Yes |
|
List |
Yes |
|
Locking_Policy |
Yes |
|
No_Return |
Yes |
|
Normalize_Scalars |
Yes |
|
Optimize |
Yes |
|
Pack |
Yes |
|
Page |
Yes |
|
Partition_Elaboration_Policy |
Yes |
Ravenscar |
Preelaborable_Initialization |
Yes |
|
Preelaborate |
Yes |
|
Priority |
Yes |
|
Priority_Specific_Dispatching |
No |
Ravenscar |
Profile |
Yes |
|
Pure |
Yes |
|
Queuing_Policy |
Yes |
Ravenscar |
Relative_Deadline |
Yes |
|
Remote_Call_Interface |
No |
Distributed systems |
Remote_Types |
No |
Distributed systems |
Restrictions |
Yes |
|
Reviewable |
Yes |
|
Shared_Passive |
No |
Distributed systems |
Storage_Size |
Yes/No |
tasks, not access types |
Suppress |
Yes |
|
Task_Dispatching_Policy |
No |
Ravenscar |
Unchecked_Union |
Yes |
|
Unsuppress |
Yes |
|
Volatile |
Yes |
|
Volatile_Components |
Yes |
16.2. SPARK Language-Defined Pragmas
The following SPARK language-defined pragmas are defined:
Pragma |
Allowed in SPARK |
Comment |
---|---|---|
Abstract_State |
Yes |
|
Assert_And_Cut |
Yes |
|
Assume |
Yes |
|
Async_Readers |
Yes |
|
Async_Writers |
Yes |
|
Constant_After_Elaboration |
Yes |
|
Contract_Cases |
Yes |
|
Default_Initial_Condition |
Yes |
|
Depends |
Yes |
|
Effective_Reads |
Yes |
|
Effective_Writes |
Yes |
|
Extensions_Visible |
Yes |
|
Ghost |
Yes |
|
Global |
Yes |
|
Initial_Condition |
Yes |
|
Initializes |
Yes |
|
Loop_Invariant |
Yes |
|
Loop_Variant |
Yes |
|
No_Caching |
Yes |
|
Part_Of |
Yes |
|
Refined_Depends |
Yes |
|
Refined_Global |
Yes |
|
Refined_Post |
Yes |
|
Refined_State |
Yes |
|
SPARK_Mode |
Yes |
Language defined but implementation dependent |
Unevaluated_Use_Of_Old |
Yes |
|
Volatile_Function |
Yes |
16.3. GNAT Implementation-Defined Pragmas
The following GNAT implementation-defined pragmas are permitted in SPARK:
Pragma |
Allowed in SPARK |
Comment |
---|---|---|
Ada_83 |
Yes |
|
Ada_95 |
Yes |
|
Ada_05 |
Yes |
|
Ada_12 |
Yes |
|
Ada_2005 |
Yes |
|
Ada_2012 |
Yes |
|
Ada_2020 |
Yes |
|
Annotate |
Yes |
|
Check |
Yes |
|
Check_Policy |
Yes |
No effect on provability (see section “Assertion Pragmas” in the SPARK User’s Guide) |
Compile_Time_Error |
Yes |
Ignored (replaced by null statement) |
Compile_Time_Warning |
Yes |
Ignored (replaced by null statement) |
Debug |
Yes |
Ignored (replaced by null statement) |
Default_Scalar_Storage_Order |
Yes |
|
Export_Function |
Yes |
|
Export_Procedure |
Yes |
|
Ignore_Pragma |
Yes |
|
Inline_Always |
Yes |
|
Invariant |
Yes |
|
Linker_Section |
Yes |
|
Max_Queue_Length |
Yes |
Extended Ravenscar |
No_Elaboration_Code_All |
Yes |
|
No_Heap_Finalization |
Yes |
|
No_Inline |
Yes |
No effect on contextual analysis of subprograms |
No_Strict_Aliasing |
Yes |
|
No_Tagged_Streams |
Yes |
|
Overflow_Mode |
Yes |
|
Post |
Yes |
|
Postcondition |
Yes |
|
Post_Class |
Yes |
|
Pre |
Yes |
|
Precondition |
Yes |
|
Pre_Class |
Yes |
|
Predicate |
Yes |
|
Predicate_Failure |
Yes |
|
Provide_Shift_Operators |
Yes |
|
Pure_Function |
Yes |
|
Restriction_Warnings |
Yes |
|
Secondary_Stack_Size |
Yes |
|
Style_Checks |
Yes |
|
Test_Case |
Yes |
|
Type_Invariant |
Yes |
|
Type_Invariant_Class |
Yes |
|
Unmodified |
Yes |
|
Unreferenced |
Yes |
|
Unused |
Yes |
|
Validity_Checks |
Yes |
|
Volatile_Full_Access |
Yes |
|
Warnings |
Yes |
|
Weak_External |
Yes |