]>
Commit | Line | Data |
---|---|---|
cb2d884d AC |
1 | .. _Implementation_Defined_Aspects: |
2 | ||
3 | ****************************** | |
4 | Implementation Defined Aspects | |
5 | ****************************** | |
6 | ||
7 | Ada defines (throughout the Ada 2012 reference manual, summarized | |
8 | in Annex K) a set of aspects that can be specified for certain entities. | |
9 | These language defined aspects are implemented in GNAT in Ada 2012 mode | |
10 | and work as described in the Ada 2012 Reference Manual. | |
11 | ||
12 | In addition, Ada 2012 allows implementations to define additional aspects | |
13 | whose meaning is defined by the implementation. GNAT provides | |
14 | a number of these implementation-defined aspects which can be used | |
15 | to extend and enhance the functionality of the compiler. This section of | |
16 | the GNAT reference manual describes these additional aspects. | |
17 | ||
18 | Note that any program using these aspects may not be portable to | |
19 | other compilers (although GNAT implements this set of aspects on all | |
20 | platforms). Therefore if portability to other compilers is an important | |
21 | consideration, you should minimize the use of these aspects. | |
22 | ||
23 | Note that for many of these aspects, the effect is essentially similar | |
24 | to the use of a pragma or attribute specification with the same name | |
25 | applied to the entity. For example, if we write: | |
26 | ||
27 | ||
28 | .. code-block:: ada | |
29 | ||
30 | type R is range 1 .. 100 | |
31 | with Value_Size => 10; | |
32 | ||
33 | ||
34 | then the effect is the same as: | |
35 | ||
36 | .. code-block:: ada | |
37 | ||
38 | type R is range 1 .. 100; | |
39 | for R'Value_Size use 10; | |
40 | ||
41 | ||
42 | and if we write: | |
43 | ||
44 | .. code-block:: ada | |
45 | ||
46 | type R is new Integer | |
47 | with Shared => True; | |
48 | ||
49 | ||
50 | then the effect is the same as: | |
51 | ||
52 | .. code-block:: ada | |
53 | ||
54 | type R is new Integer; | |
55 | pragma Shared (R); | |
56 | ||
57 | ||
58 | In the documentation below, such cases are simply marked | |
59 | as being boolean aspects equivalent to the corresponding pragma | |
60 | or attribute definition clause. | |
61 | ||
62 | Aspect Abstract_State | |
63 | ===================== | |
64 | ||
65 | .. index:: Abstract_State | |
66 | ||
c25f170d | 67 | This aspect is equivalent to :ref:`pragma Abstract_State<Pragma-Abstract_State>`. |
cb2d884d | 68 | |
9c533e7d AC |
69 | Aspect Annotate |
70 | =============== | |
71 | ||
cb2d884d AC |
72 | .. index:: Annotate |
73 | ||
74 | There are three forms of this aspect (where ID is an identifier, | |
c25f170d AC |
75 | and ARG is a general expression), |
76 | corresponding to :ref:`pragma Annotate<Pragma-Annotate>`. | |
cb2d884d AC |
77 | |
78 | ||
79 | ||
80 | *Annotate => ID* | |
08705a15 | 81 | Equivalent to ``pragma Annotate (ID, Entity => Name);`` |
cb2d884d AC |
82 | |
83 | ||
84 | *Annotate => (ID)* | |
08705a15 | 85 | Equivalent to ``pragma Annotate (ID, Entity => Name);`` |
cb2d884d AC |
86 | |
87 | ||
88 | *Annotate => (ID ,ID {, ARG})* | |
08705a15 | 89 | Equivalent to ``pragma Annotate (ID, ID {, ARG}, Entity => Name);`` |
cb2d884d AC |
90 | |
91 | Aspect Async_Readers | |
92 | ==================== | |
93 | .. index:: Async_Readers | |
94 | ||
c25f170d | 95 | This boolean aspect is equivalent to :ref:`pragma Async_Readers<Pragma-Async_Readers>`. |
cb2d884d AC |
96 | |
97 | Aspect Async_Writers | |
98 | ==================== | |
99 | .. index:: Async_Writers | |
100 | ||
c25f170d | 101 | This boolean aspect is equivalent to :ref:`pragma Async_Writers<Pragma-Async_Writers>`. |
cb2d884d | 102 | |
abcb651b AC |
103 | Aspect Constant_After_Elaboration |
104 | ================================= | |
105 | .. index:: Constant_After_Elaboration | |
106 | ||
c25f170d | 107 | This aspect is equivalent to :ref:`pragma Constant_After_Elaboration<Pragma-Constant_After_Elaboration>`. |
abcb651b | 108 | |
cb2d884d AC |
109 | Aspect Contract_Cases |
110 | ===================== | |
111 | .. index:: Contract_Cases | |
112 | ||
c25f170d | 113 | This aspect is equivalent to :ref:`pragma Contract_Cases<Pragma-Contract_Cases>`, the sequence |
cb2d884d AC |
114 | of clauses being enclosed in parentheses so that syntactically it is an |
115 | aggregate. | |
116 | ||
117 | Aspect Depends | |
118 | ============== | |
119 | .. index:: Depends | |
120 | ||
c25f170d | 121 | This aspect is equivalent to :ref:`pragma Depends<Pragma-Depends>`. |
cb2d884d | 122 | |
abcb651b AC |
123 | Aspect Default_Initial_Condition |
124 | ================================ | |
125 | .. index:: Default_Initial_Condition | |
126 | ||
c25f170d | 127 | This aspect is equivalent to :ref:`pragma Default_Initial_Condition<Pragma-Default_Initial_Condition>`. |
abcb651b | 128 | |
cb2d884d AC |
129 | Aspect Dimension |
130 | ================ | |
131 | .. index:: Dimension | |
132 | ||
08705a15 | 133 | The ``Dimension`` aspect is used to specify the dimensions of a given |
cb2d884d AC |
134 | subtype of a dimensioned numeric type. The aspect also specifies a symbol |
135 | used when doing formatted output of dimensioned quantities. The syntax is:: | |
136 | ||
137 | with Dimension => | |
138 | ([Symbol =>] SYMBOL, DIMENSION_VALUE {, DIMENSION_Value}) | |
139 | ||
140 | SYMBOL ::= STRING_LITERAL | CHARACTER_LITERAL | |
141 | ||
142 | DIMENSION_VALUE ::= | |
143 | RATIONAL | |
144 | | others => RATIONAL | |
145 | | DISCRETE_CHOICE_LIST => RATIONAL | |
146 | ||
147 | RATIONAL ::= [-] NUMERIC_LITERAL [/ NUMERIC_LITERAL] | |
148 | ||
149 | ||
150 | This aspect can only be applied to a subtype whose parent type has | |
08705a15 | 151 | a ``Dimension_System`` aspect. The aspect must specify values for |
cb2d884d AC |
152 | all dimensions of the system. The rational values are the powers of the |
153 | corresponding dimensions that are used by the compiler to verify that | |
154 | physical (numeric) computations are dimensionally consistent. For example, | |
155 | the computation of a force must result in dimensions (L => 1, M => 1, T => -2). | |
156 | For further examples of the usage | |
08705a15 | 157 | of this aspect, see package ``System.Dim.Mks``. |
cb2d884d AC |
158 | Note that when the dimensioned type is an integer type, then any |
159 | dimension value must be an integer literal. | |
160 | ||
161 | Aspect Dimension_System | |
162 | ======================= | |
163 | .. index:: Dimension_System | |
164 | ||
08705a15 | 165 | The ``Dimension_System`` aspect is used to define a system of |
cb2d884d | 166 | dimensions that will be used in subsequent subtype declarations with |
08705a15 | 167 | ``Dimension`` aspects that reference this system. The syntax is:: |
cb2d884d AC |
168 | |
169 | with Dimension_System => (DIMENSION {, DIMENSION}); | |
170 | ||
171 | DIMENSION ::= ([Unit_Name =>] IDENTIFIER, | |
172 | [Unit_Symbol =>] SYMBOL, | |
173 | [Dim_Symbol =>] SYMBOL) | |
174 | ||
175 | SYMBOL ::= CHARACTER_LITERAL | STRING_LITERAL | |
176 | ||
177 | ||
178 | This aspect is applied to a type, which must be a numeric derived type | |
179 | (typically a floating-point type), that | |
08705a15 | 180 | will represent values within the dimension system. Each ``DIMENSION`` |
cb2d884d | 181 | corresponds to one particular dimension. A maximum of 7 dimensions may |
08705a15 AC |
182 | be specified. ``Unit_Name`` is the name of the dimension (for example |
183 | ``Meter``). ``Unit_Symbol`` is the shorthand used for quantities | |
184 | of this dimension (for example ``m`` for ``Meter``). | |
185 | ``Dim_Symbol`` gives | |
cb2d884d | 186 | the identification within the dimension system (typically this is a |
08705a15 AC |
187 | single letter, e.g. ``L`` standing for length for unit name ``Meter``). |
188 | The ``Unit_Symbol`` is used in formatted output of dimensioned quantities. | |
189 | The ``Dim_Symbol`` is used in error messages when numeric operations have | |
cb2d884d AC |
190 | inconsistent dimensions. |
191 | ||
192 | GNAT provides the standard definition of the International MKS system in | |
08705a15 | 193 | the run-time package ``System.Dim.Mks``. You can easily define |
cb2d884d AC |
194 | similar packages for cgs units or British units, and define conversion factors |
195 | between values in different systems. The MKS system is characterized by the | |
196 | following aspect: | |
197 | ||
198 | .. code-block:: ada | |
199 | ||
200 | type Mks_Type is new Long_Long_Float with | |
201 | Dimension_System => ( | |
202 | (Unit_Name => Meter, Unit_Symbol => 'm', Dim_Symbol => 'L'), | |
203 | (Unit_Name => Kilogram, Unit_Symbol => "kg", Dim_Symbol => 'M'), | |
204 | (Unit_Name => Second, Unit_Symbol => 's', Dim_Symbol => 'T'), | |
205 | (Unit_Name => Ampere, Unit_Symbol => 'A', Dim_Symbol => 'I'), | |
206 | (Unit_Name => Kelvin, Unit_Symbol => 'K', Dim_Symbol => '@'), | |
207 | (Unit_Name => Mole, Unit_Symbol => "mol", Dim_Symbol => 'N'), | |
208 | (Unit_Name => Candela, Unit_Symbol => "cd", Dim_Symbol => 'J')); | |
209 | ||
210 | ||
08705a15 | 211 | Note that in the above type definition, we use the ``at`` symbol (``@``) to |
cb2d884d AC |
212 | represent a theta character (avoiding the use of extended Latin-1 |
213 | characters in this context). | |
214 | ||
215 | See section 'Performing Dimensionality Analysis in GNAT' in the GNAT Users | |
216 | Guide for detailed examples of use of the dimension system. | |
217 | ||
74e9ae98 AC |
218 | Aspect Disable_Controlled |
219 | ========================= | |
220 | .. index:: Disable_Controlled | |
221 | ||
08705a15 AC |
222 | The aspect ``Disable_Controlled`` is defined for controlled record types. If |
223 | active, this aspect causes suppression of all related calls to ``Initialize``, | |
224 | ``Adjust``, and ``Finalize``. The intended use is for conditional compilation, | |
74e9ae98 AC |
225 | where for example you might want a record to be controlled or not depending on |
226 | whether some run-time check is enabled or suppressed. | |
227 | ||
cb2d884d AC |
228 | Aspect Effective_Reads |
229 | ====================== | |
230 | .. index:: Effective_Reads | |
231 | ||
c25f170d | 232 | This aspect is equivalent to :ref:`pragma Effective_Reads<Pragma-Effective_Reads>`. |
cb2d884d AC |
233 | |
234 | Aspect Effective_Writes | |
235 | ======================= | |
236 | .. index:: Effective_Writes | |
237 | ||
c25f170d | 238 | This aspect is equivalent to :ref:`pragma Effective_Writes<Pragma-Effective_Writes>`. |
cb2d884d | 239 | |
abcb651b AC |
240 | Aspect Extensions_Visible |
241 | ========================= | |
242 | .. index:: Extensions_Visible | |
243 | ||
c25f170d | 244 | This aspect is equivalent to :ref:`pragma Extensions_Visible<Pragma-Extensions_Visible>`. |
abcb651b | 245 | |
cb2d884d AC |
246 | Aspect Favor_Top_Level |
247 | ====================== | |
248 | .. index:: Favor_Top_Level | |
249 | ||
c25f170d | 250 | This boolean aspect is equivalent to :ref:`pragma Favor_Top_Level<Pragma-Favor_Top_Level>`. |
cb2d884d | 251 | |
abcb651b AC |
252 | Aspect Ghost |
253 | ============= | |
254 | .. index:: Ghost | |
255 | ||
c25f170d | 256 | This aspect is equivalent to :ref:`pragma Ghost<Pragma-Ghost>`. |
abcb651b | 257 | |
067d80d8 YM |
258 | Aspect Ghost_Predicate |
259 | ====================== | |
260 | .. index:: Ghost_Predicate | |
261 | ||
262 | This aspect introduces a subtype predicate that can reference ghost | |
263 | entities. The subtype cannot appear as a subtype_mark in a membership test. | |
264 | ||
265 | For the detailed semantics of this aspect, see the entry for subtype predicates | |
266 | in the SPARK Reference Manual, section 3.2.4. | |
267 | ||
cb2d884d AC |
268 | Aspect Global |
269 | ============= | |
270 | .. index:: Global | |
271 | ||
c25f170d | 272 | This aspect is equivalent to :ref:`pragma Global<Pragma-Global>`. |
cb2d884d AC |
273 | |
274 | Aspect Initial_Condition | |
275 | ======================== | |
276 | .. index:: Initial_Condition | |
277 | ||
c25f170d | 278 | This aspect is equivalent to :ref:`pragma Initial_Condition<Pragma-Initial_Condition>`. |
cb2d884d AC |
279 | |
280 | Aspect Initializes | |
281 | ================== | |
282 | .. index:: Initializes | |
283 | ||
c25f170d | 284 | This aspect is equivalent to :ref:`pragma Initializes<Pragma-Initializes>`. |
cb2d884d AC |
285 | |
286 | Aspect Inline_Always | |
287 | ==================== | |
288 | .. index:: Inline_Always | |
289 | ||
c25f170d | 290 | This boolean aspect is equivalent to :ref:`pragma Inline_Always<Pragma-Inline_Always>`. |
cb2d884d AC |
291 | |
292 | Aspect Invariant | |
293 | ================ | |
294 | .. index:: Invariant | |
295 | ||
c25f170d | 296 | This aspect is equivalent to :ref:`pragma Invariant<Pragma-Invariant>`. It is a |
08705a15 AC |
297 | synonym for the language defined aspect ``Type_Invariant`` except |
298 | that it is separately controllable using pragma ``Assertion_Policy``. | |
cb2d884d AC |
299 | |
300 | Aspect Invariant'Class | |
301 | ====================== | |
302 | .. index:: Invariant'Class | |
303 | ||
c25f170d | 304 | This aspect is equivalent to :ref:`pragma Type_Invariant_Class<Pragma-Type_Invariant_Class>`. It is a |
08705a15 AC |
305 | synonym for the language defined aspect ``Type_Invariant'Class`` except |
306 | that it is separately controllable using pragma ``Assertion_Policy``. | |
cb2d884d AC |
307 | |
308 | Aspect Iterable | |
309 | =============== | |
310 | .. index:: Iterable | |
311 | ||
312 | This aspect provides a light-weight mechanism for loops and quantified | |
313 | expressions over container types, without the overhead imposed by the tampering | |
314 | checks of standard Ada 2012 iterators. The value of the aspect is an aggregate | |
f5c31a46 BB |
315 | with six named components, of which the last three are optional: ``First``, |
316 | ``Next``, ``Has_Element``, ``Element``, ``Last``, and ``Previous``. | |
2e60feb5 PMR |
317 | When only the first three components are specified, only the |
318 | ``for .. in`` form of iteration over cursors is available. When ``Element`` | |
319 | is specified, both this form and the ``for .. of`` form of iteration over | |
320 | elements are available. If the last two components are specified, reverse | |
321 | iterations over the container can be specified (analogous to what can be done | |
f5c31a46 | 322 | over predefined containers that support the ``Reverse_Iterator`` interface). |
2e60feb5 | 323 | The following is a typical example of use: |
cb2d884d AC |
324 | |
325 | .. code-block:: ada | |
326 | ||
327 | type List is private with | |
9b7f7fa7 PT |
328 | Iterable => (First => First_Cursor, |
329 | Next => Advance, | |
8b9bbdc3 PT |
330 | Has_Element => Cursor_Has_Element |
331 | [,Element => Get_Element] | |
332 | [,Last => Last_Cursor] | |
333 | [,Previous => Retreat]); | |
cb2d884d | 334 | |
8b9bbdc3 PT |
335 | * The values of ``First`` and ``Last`` are primitive operations of the |
336 | container type that return a ``Cursor``, which must be a type declared in | |
cb2d884d AC |
337 | the container package or visible from it. For example: |
338 | ||
339 | .. code-block:: ada | |
340 | ||
341 | function First_Cursor (Cont : Container) return Cursor; | |
8b9bbdc3 | 342 | function Last_Cursor (Cont : Container) return Cursor; |
cb2d884d | 343 | |
8b9bbdc3 PT |
344 | * The values of ``Next`` and ``Previous`` are primitive operations of the container type that take |
345 | both a container and a cursor and yield a cursor. For example: | |
cb2d884d AC |
346 | |
347 | .. code-block:: ada | |
348 | ||
349 | function Advance (Cont : Container; Position : Cursor) return Cursor; | |
8b9bbdc3 | 350 | function Retreat (Cont : Container; Position : Cursor) return Cursor; |
cb2d884d | 351 | |
08705a15 | 352 | * The value of ``Has_Element`` is a primitive operation of the container type |
cb2d884d AC |
353 | that takes both a container and a cursor and yields a boolean. For example: |
354 | ||
355 | .. code-block:: ada | |
356 | ||
357 | function Cursor_Has_Element (Cont : Container; Position : Cursor) return Boolean; | |
358 | ||
08705a15 AC |
359 | * The value of ``Element`` is a primitive operation of the container type that |
360 | takes both a container and a cursor and yields an ``Element_Type``, which must | |
cb2d884d AC |
361 | be a type declared in the container package or visible from it. For example: |
362 | ||
363 | .. code-block:: ada | |
364 | ||
365 | function Get_Element (Cont : Container; Position : Cursor) return Element_Type; | |
366 | ||
367 | This aspect is used in the GNAT-defined formal container packages. | |
368 | ||
369 | Aspect Linker_Section | |
370 | ===================== | |
371 | .. index:: Linker_Section | |
372 | ||
c25f170d | 373 | This aspect is equivalent to :ref:`pragma Linker_Section<Pragma-Linker_Section>`. |
cb2d884d | 374 | |
9daee425 SB |
375 | Aspect Local_Restrictions |
376 | ========================= | |
377 | .. index:: Local_Restrictions | |
378 | ||
379 | This aspect may be specified for a subprogram (and for other declarations | |
380 | as described below). It is used to specify that a particular subprogram does | |
381 | not violate one or more local restrictions, nor can it call a subprogram | |
382 | that is not subject to the same requirement. Positional aggregate syntax | |
383 | (with parentheses, not square brackets) may be used to specify more than one | |
384 | local restriction, as in | |
385 | ||
386 | .. code-block:: ada | |
387 | ||
388 | procedure Do_Something | |
389 | with Local_Restrictions => (Some_Restriction, Another_Restriction); | |
390 | ||
391 | Parentheses are currently required even in the case of specifying a single | |
392 | local restriction (this requirement may be relaxed in the future). | |
393 | Supported local restrictions currently include (only) No_Heap_Allocations and | |
394 | No_Secondary_Stack. | |
395 | No_Secondary_Stack corresponds to the GNAT-defined (global) restriction | |
396 | of the same name. No_Heap_Allocations corresponds to the conjunction of the | |
397 | Ada-defined restrictions No_Allocators and No_Implicit_Heap_Allocations. | |
398 | ||
399 | Additional requirements are imposed in order to ensure that restriction | |
400 | violations cannot be achieved via overriding dispatching operations, | |
401 | calling through an access-to-subprogram value, calling a generic formal | |
402 | subprogram, or calling through a subprogram renaming. | |
403 | For a dispatching operation, an overrider must be subject to (at least) the | |
404 | same restrictions as the overridden inherited subprogram; similarly, the | |
405 | actual subprogram corresponding to a generic formal subprogram | |
406 | in an instantiation must be subject to (at least) the same restrictions | |
407 | as the formal subprogram. A call through an access-to-subprogram value | |
408 | is conservatively assumed to violate all local restrictions; tasking-related | |
409 | constructs (notably entry calls) are treated similarly. A renaming-as-body is | |
410 | treated like a subprogram body containing a call to the renamed subprogram. | |
411 | ||
412 | The Local_Restrictions aspect can be specified for a package specification, | |
413 | in which case the aspect specification also applies to all eligible entities | |
414 | declared with the package. This includes types. Default initialization of an | |
415 | object of a given type is treated like a call to an implicitly-declared | |
416 | initialization subprogram. Such a "call" is subject to the same local | |
417 | restriction checks as any other call. If a type is subject to a local | |
418 | restriction, then any violations of that restriction within the default | |
419 | initialization expressions (if any) of the type are rejected. This may | |
420 | include "calls" to the default initialization subprograms of other types. | |
421 | ||
422 | Local_Restrictions aspect specifications are additive (for example, in the | |
423 | case of a declaration that occurs within nested packages that each have | |
424 | a Local_Restrictions specification). | |
425 | ||
426 | ||
cb2d884d AC |
427 | Aspect Lock_Free |
428 | ================ | |
429 | .. index:: Lock_Free | |
430 | ||
c25f170d | 431 | This boolean aspect is equivalent to :ref:`pragma Lock_Free<Pragma-Lock_Free>`. |
cb2d884d | 432 | |
33c51287 AC |
433 | Aspect Max_Queue_Length |
434 | ======================= | |
33c51287 AC |
435 | .. index:: Max_Queue_Length |
436 | ||
437 | This aspect is equivalent to :ref:`pragma Max_Queue_Length<Pragma-Max_Queue_Length>`. | |
438 | ||
9dfc6c55 YM |
439 | Aspect No_Caching |
440 | ================= | |
441 | .. index:: No_Caching | |
442 | ||
443 | This boolean aspect is equivalent to :ref:`pragma No_Caching<Pragma-No_Caching>`. | |
444 | ||
cb2d884d AC |
445 | Aspect No_Elaboration_Code_All |
446 | ============================== | |
447 | .. index:: No_Elaboration_Code_All | |
448 | ||
c25f170d AC |
449 | This aspect is equivalent to :ref:`pragma No_Elaboration_Code_All<Pragma-No_Elaboration_Code_All>` |
450 | for a program unit. | |
cb2d884d | 451 | |
08705a15 AC |
452 | Aspect No_Inline |
453 | ================ | |
454 | .. index:: No_Inline | |
455 | ||
456 | This boolean aspect is equivalent to :ref:`pragma No_Inline<Pragma-No_Inline>`. | |
457 | ||
cb2d884d AC |
458 | Aspect No_Tagged_Streams |
459 | ======================== | |
460 | .. index:: No_Tagged_Streams | |
461 | ||
c25f170d | 462 | This aspect is equivalent to :ref:`pragma No_Tagged_Streams<Pragma-No_Tagged_Streams>` with an |
cb2d884d AC |
463 | argument specifying a root tagged type (thus this aspect can only be |
464 | applied to such a type). | |
465 | ||
811b8aa5 BD |
466 | Aspect No_Task_Parts |
467 | ======================== | |
468 | .. index:: No_Task_Parts | |
469 | ||
470 | Applies to a type. If True, requires that the type and any descendants | |
471 | do not have any task parts. The rules for this aspect are the same as | |
472 | for the language-defined No_Controlled_Parts aspect (see RM-H.4.1), | |
473 | replacing "controlled" with "task". | |
474 | ||
475 | If No_Task_Parts is True for a type T, then the compiler can optimize | |
476 | away certain tasking-related code that would otherwise be needed | |
477 | for T'Class, because descendants of T might contain tasks. | |
478 | ||
cb2d884d AC |
479 | Aspect Object_Size |
480 | ================== | |
481 | .. index:: Object_Size | |
482 | ||
c25f170d | 483 | This aspect is equivalent to :ref:`attribute Object_Size<Attribute-Object_Size>`. |
cb2d884d AC |
484 | |
485 | Aspect Obsolescent | |
486 | ================== | |
1d201131 | 487 | .. index:: Obsolescent |
cb2d884d | 488 | |
c25f170d | 489 | This aspect is equivalent to :ref:`pragma Obsolescent<Pragma_Obsolescent>`. Note that the |
cb2d884d AC |
490 | evaluation of this aspect happens at the point of occurrence, it is not |
491 | delayed until the freeze point. | |
492 | ||
493 | Aspect Part_Of | |
494 | ============== | |
495 | .. index:: Part_Of | |
496 | ||
c25f170d | 497 | This aspect is equivalent to :ref:`pragma Part_Of<Pragma-Part_Of>`. |
cb2d884d AC |
498 | |
499 | Aspect Persistent_BSS | |
500 | ===================== | |
501 | .. index:: Persistent_BSS | |
502 | ||
c25f170d | 503 | This boolean aspect is equivalent to :ref:`pragma Persistent_BSS<Pragma-Persistent_BSS>`. |
cb2d884d AC |
504 | |
505 | Aspect Predicate | |
506 | ================ | |
507 | .. index:: Predicate | |
508 | ||
c25f170d | 509 | This aspect is equivalent to :ref:`pragma Predicate<Pragma-Predicate>`. It is thus |
08705a15 AC |
510 | similar to the language defined aspects ``Dynamic_Predicate`` |
511 | and ``Static_Predicate`` except that whether the resulting | |
cb2d884d AC |
512 | predicate is static or dynamic is controlled by the form of the |
513 | expression. It is also separately controllable using pragma | |
08705a15 | 514 | ``Assertion_Policy``. |
cb2d884d AC |
515 | |
516 | Aspect Pure_Function | |
517 | ==================== | |
518 | .. index:: Pure_Function | |
519 | ||
c25f170d | 520 | This boolean aspect is equivalent to :ref:`pragma Pure_Function<Pragma-Pure_Function>`. |
cb2d884d AC |
521 | |
522 | Aspect Refined_Depends | |
523 | ====================== | |
524 | .. index:: Refined_Depends | |
525 | ||
c25f170d | 526 | This aspect is equivalent to :ref:`pragma Refined_Depends<Pragma-Refined_Depends>`. |
cb2d884d AC |
527 | |
528 | Aspect Refined_Global | |
529 | ===================== | |
530 | .. index:: Refined_Global | |
531 | ||
c25f170d | 532 | This aspect is equivalent to :ref:`pragma Refined_Global<Pragma-Refined_Global>`. |
cb2d884d AC |
533 | |
534 | Aspect Refined_Post | |
535 | =================== | |
536 | .. index:: Refined_Post | |
537 | ||
c25f170d | 538 | This aspect is equivalent to :ref:`pragma Refined_Post<Pragma-Refined_Post>`. |
cb2d884d AC |
539 | |
540 | Aspect Refined_State | |
541 | ==================== | |
542 | .. index:: Refined_State | |
543 | ||
c25f170d | 544 | This aspect is equivalent to :ref:`pragma Refined_State<Pragma-Refined_State>`. |
cb2d884d | 545 | |
6ba3247d PT |
546 | Aspect Relaxed_Initialization |
547 | ============================= | |
548 | .. index:: Refined_Initialization | |
549 | ||
550 | For the syntax and semantics of this aspect, see the SPARK 2014 Reference | |
551 | Manual, section 6.10. | |
552 | ||
cb2d884d AC |
553 | Aspect Remote_Access_Type |
554 | ========================= | |
555 | .. index:: Remote_Access_Type | |
556 | ||
c25f170d | 557 | This aspect is equivalent to :ref:`pragma Remote_Access_Type<Pragma-Remote_Access_Type>`. |
cb2d884d | 558 | |
33c51287 AC |
559 | Aspect Secondary_Stack_Size |
560 | =========================== | |
561 | ||
562 | .. index:: Secondary_Stack_Size | |
563 | ||
564 | This aspect is equivalent to :ref:`pragma Secondary_Stack_Size<Pragma-Secondary_Stack_Size>`. | |
565 | ||
566 | ||
cb2d884d AC |
567 | Aspect Scalar_Storage_Order |
568 | =========================== | |
569 | .. index:: Scalar_Storage_Order | |
570 | ||
c25f170d | 571 | This aspect is equivalent to a :ref:`attribute Scalar_Storage_Order<Attribute-Scalar_Storage_Order>`. |
cb2d884d AC |
572 | |
573 | Aspect Shared | |
574 | ============= | |
575 | .. index:: Shared | |
576 | ||
c25f170d | 577 | This boolean aspect is equivalent to :ref:`pragma Shared<Pragma-Shared>` |
08705a15 | 578 | and is thus a synonym for aspect ``Atomic``. |
cb2d884d | 579 | |
04d6c745 YM |
580 | Aspect Side_Effects |
581 | =================== | |
582 | .. index:: Side_Effects | |
583 | ||
584 | This aspect is equivalent to :ref:`pragma Side_Effects<Pragma-Side_Effects>`. | |
585 | ||
cb2d884d AC |
586 | Aspect Simple_Storage_Pool |
587 | ========================== | |
588 | .. index:: Simple_Storage_Pool | |
589 | ||
c25f170d | 590 | This aspect is equivalent to :ref:`attribute Simple_Storage_Pool<Attribute_Simple_Storage_Pool>`. |
cb2d884d AC |
591 | |
592 | Aspect Simple_Storage_Pool_Type | |
593 | =============================== | |
594 | .. index:: Simple_Storage_Pool_Type | |
595 | ||
c25f170d | 596 | This boolean aspect is equivalent to :ref:`pragma Simple_Storage_Pool_Type<Pragma-Simple_Storage_Pool_Type>`. |
cb2d884d AC |
597 | |
598 | Aspect SPARK_Mode | |
599 | ================= | |
600 | .. index:: SPARK_Mode | |
601 | ||
c25f170d | 602 | This aspect is equivalent to :ref:`pragma SPARK_Mode<Pragma-SPARK_Mode>` and |
cb2d884d AC |
603 | may be specified for either or both of the specification and body |
604 | of a subprogram or package. | |
605 | ||
606 | Aspect Suppress_Debug_Info | |
607 | ========================== | |
608 | .. index:: Suppress_Debug_Info | |
609 | ||
c25f170d | 610 | This boolean aspect is equivalent to :ref:`pragma Suppress_Debug_Info<Pragma-Suppress_Debug_Info>`. |
cb2d884d AC |
611 | |
612 | Aspect Suppress_Initialization | |
613 | ============================== | |
614 | .. index:: Suppress_Initialization | |
615 | ||
c25f170d | 616 | This boolean aspect is equivalent to :ref:`pragma Suppress_Initialization<Pragma-Suppress_Initialization>`. |
cb2d884d AC |
617 | |
618 | Aspect Test_Case | |
619 | ================ | |
620 | .. index:: Test_Case | |
621 | ||
c25f170d | 622 | This aspect is equivalent to :ref:`pragma Test_Case<Pragma-Test_Case>`. |
cb2d884d AC |
623 | |
624 | Aspect Thread_Local_Storage | |
625 | =========================== | |
626 | .. index:: Thread_Local_Storage | |
627 | ||
c25f170d | 628 | This boolean aspect is equivalent to :ref:`pragma Thread_Local_Storage<Pragma-Thread_Local_Storage>`. |
cb2d884d AC |
629 | |
630 | Aspect Universal_Aliasing | |
631 | ========================= | |
632 | .. index:: Universal_Aliasing | |
633 | ||
c25f170d | 634 | This boolean aspect is equivalent to :ref:`pragma Universal_Aliasing<Pragma-Universal_Aliasing>`. |
cb2d884d | 635 | |
cb2d884d AC |
636 | Aspect Unmodified |
637 | ================= | |
638 | .. index:: Unmodified | |
639 | ||
c25f170d | 640 | This boolean aspect is equivalent to :ref:`pragma Unmodified<Pragma-Unmodified>`. |
cb2d884d AC |
641 | |
642 | Aspect Unreferenced | |
643 | =================== | |
644 | .. index:: Unreferenced | |
645 | ||
71400efc AC |
646 | This boolean aspect is equivalent to :ref:`pragma Unreferenced<Pragma-Unreferenced>`. |
647 | ||
81e68a19 | 648 | When using the ``-gnat2022`` switch, this aspect is also supported on formal |
71400efc AC |
649 | parameters, which is in particular the only form possible for expression |
650 | functions. | |
cb2d884d AC |
651 | |
652 | Aspect Unreferenced_Objects | |
653 | =========================== | |
654 | .. index:: Unreferenced_Objects | |
655 | ||
c25f170d | 656 | This boolean aspect is equivalent to :ref:`pragma Unreferenced_Objects<Pragma-Unreferenced_Objects>`. |
cb2d884d | 657 | |
9daee425 SB |
658 | Aspect User_Aspect |
659 | ================== | |
660 | .. index:: User_Aspect | |
661 | ||
662 | This aspect takes an argument that is the name of an aspect defined by a | |
663 | User_Aspect_Definition configuration pragma. | |
664 | A User_Aspect aspect specification is semantically equivalent to | |
665 | replicating the set of aspect specifications associated with the named | |
666 | pragma-defined aspect. | |
667 | ||
cb2d884d AC |
668 | Aspect Value_Size |
669 | ================= | |
670 | .. index:: Value_Size | |
671 | ||
c25f170d | 672 | This aspect is equivalent to :ref:`attribute Value_Size<Attribute-Value_Size>`. |
cb2d884d | 673 | |
74e9ae98 AC |
674 | Aspect Volatile_Full_Access |
675 | =========================== | |
676 | .. index:: Volatile_Full_Access | |
677 | ||
c25f170d | 678 | This boolean aspect is equivalent to :ref:`pragma Volatile_Full_Access<Pragma-Volatile_Full_Access>`. |
74e9ae98 | 679 | |
abcb651b AC |
680 | Aspect Volatile_Function |
681 | =========================== | |
682 | .. index:: Volatile_Function | |
683 | ||
c25f170d | 684 | This boolean aspect is equivalent to :ref:`pragma Volatile_Function<Pragma-Volatile_Function>`. |
abcb651b | 685 | |
cb2d884d AC |
686 | Aspect Warnings |
687 | =============== | |
688 | .. index:: Warnings | |
689 | ||
c25f170d | 690 | This aspect is equivalent to the two argument form of :ref:`pragma Warnings<Pragma_Warnings>`, |
08705a15 | 691 | where the first argument is ``ON`` or ``OFF`` and the second argument |
cb2d884d | 692 | is the entity. |