|
111
|
1 .. _Standard_and_Implementation_Defined_Restrictions:
|
|
|
2
|
|
|
3 ************************************************
|
|
|
4 Standard and Implementation Defined Restrictions
|
|
|
5 ************************************************
|
|
|
6
|
|
|
7 All Ada Reference Manual-defined Restriction identifiers are implemented:
|
|
|
8
|
|
|
9 * language-defined restrictions (see 13.12.1)
|
|
|
10 * tasking restrictions (see D.7)
|
|
|
11 * high integrity restrictions (see H.4)
|
|
|
12
|
|
|
13 GNAT implements additional restriction identifiers. All restrictions, whether
|
|
|
14 language defined or GNAT-specific, are listed in the following.
|
|
|
15
|
|
|
16 .. _Partition-Wide_Restrictions:
|
|
|
17
|
|
|
18 Partition-Wide Restrictions
|
|
|
19 ===========================
|
|
|
20
|
|
|
21 There are two separate lists of restriction identifiers. The first
|
|
|
22 set requires consistency throughout a partition (in other words, if the
|
|
|
23 restriction identifier is used for any compilation unit in the partition,
|
|
|
24 then all compilation units in the partition must obey the restriction).
|
|
|
25
|
|
|
26 Immediate_Reclamation
|
|
|
27 ---------------------
|
|
|
28 .. index:: Immediate_Reclamation
|
|
|
29
|
|
|
30 [RM H.4] This restriction ensures that, except for storage occupied by
|
|
|
31 objects created by allocators and not deallocated via unchecked
|
|
|
32 deallocation, any storage reserved at run time for an object is
|
|
|
33 immediately reclaimed when the object no longer exists.
|
|
|
34
|
|
|
35 Max_Asynchronous_Select_Nesting
|
|
|
36 -------------------------------
|
|
|
37 .. index:: Max_Asynchronous_Select_Nesting
|
|
|
38
|
|
|
39 [RM D.7] Specifies the maximum dynamic nesting level of asynchronous
|
|
|
40 selects. Violations of this restriction with a value of zero are
|
|
|
41 detected at compile time. Violations of this restriction with values
|
|
|
42 other than zero cause Storage_Error to be raised.
|
|
|
43
|
|
|
44 Max_Entry_Queue_Length
|
|
|
45 ----------------------
|
|
|
46 .. index:: Max_Entry_Queue_Length
|
|
|
47
|
|
|
48 [RM D.7] This restriction is a declaration that any protected entry compiled in
|
|
|
49 the scope of the restriction has at most the specified number of
|
|
|
50 tasks waiting on the entry at any one time, and so no queue is required.
|
|
|
51 Note that this restriction is checked at run time. Violation of this
|
|
|
52 restriction results in the raising of Program_Error exception at the point of
|
|
|
53 the call.
|
|
|
54
|
|
|
55 .. index:: Max_Entry_Queue_Depth
|
|
|
56
|
|
|
57 The restriction ``Max_Entry_Queue_Depth`` is recognized as a
|
|
|
58 synonym for ``Max_Entry_Queue_Length``. This is retained for historical
|
|
|
59 compatibility purposes (and a warning will be generated for its use if
|
|
|
60 warnings on obsolescent features are activated).
|
|
|
61
|
|
|
62 Max_Protected_Entries
|
|
|
63 ---------------------
|
|
|
64 .. index:: Max_Protected_Entries
|
|
|
65
|
|
|
66 [RM D.7] Specifies the maximum number of entries per protected type. The
|
|
|
67 bounds of every entry family of a protected unit shall be static, or shall be
|
|
|
68 defined by a discriminant of a subtype whose corresponding bound is static.
|
|
|
69
|
|
|
70 Max_Select_Alternatives
|
|
|
71 -----------------------
|
|
|
72 .. index:: Max_Select_Alternatives
|
|
|
73
|
|
|
74 [RM D.7] Specifies the maximum number of alternatives in a selective accept.
|
|
|
75
|
|
|
76 Max_Storage_At_Blocking
|
|
|
77 -----------------------
|
|
|
78 .. index:: Max_Storage_At_Blocking
|
|
|
79
|
|
|
80 [RM D.7] Specifies the maximum portion (in storage elements) of a task's
|
|
|
81 Storage_Size that can be retained by a blocked task. A violation of this
|
|
|
82 restriction causes Storage_Error to be raised.
|
|
|
83
|
|
|
84 Max_Task_Entries
|
|
|
85 ----------------
|
|
|
86 .. index:: Max_Task_Entries
|
|
|
87
|
|
|
88 [RM D.7] Specifies the maximum number of entries
|
|
|
89 per task. The bounds of every entry family
|
|
|
90 of a task unit shall be static, or shall be
|
|
|
91 defined by a discriminant of a subtype whose
|
|
|
92 corresponding bound is static.
|
|
|
93
|
|
|
94 Max_Tasks
|
|
|
95 ---------
|
|
|
96 .. index:: Max_Tasks
|
|
|
97
|
|
|
98 [RM D.7] Specifies the maximum number of task that may be created, not
|
|
|
99 counting the creation of the environment task. Violations of this
|
|
|
100 restriction with a value of zero are detected at compile
|
|
|
101 time. Violations of this restriction with values other than zero cause
|
|
|
102 Storage_Error to be raised.
|
|
|
103
|
|
|
104 No_Abort_Statements
|
|
|
105 -------------------
|
|
|
106 .. index:: No_Abort_Statements
|
|
|
107
|
|
|
108 [RM D.7] There are no abort_statements, and there are
|
|
|
109 no calls to Task_Identification.Abort_Task.
|
|
|
110
|
|
|
111 No_Access_Parameter_Allocators
|
|
|
112 ------------------------------
|
|
|
113 .. index:: No_Access_Parameter_Allocators
|
|
|
114
|
|
|
115 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
116 occurrences of an allocator as the actual parameter to an access
|
|
|
117 parameter.
|
|
|
118
|
|
|
119 No_Access_Subprograms
|
|
|
120 ---------------------
|
|
|
121 .. index:: No_Access_Subprograms
|
|
|
122
|
|
|
123 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
124 declarations of access-to-subprogram types.
|
|
|
125
|
|
|
126 No_Allocators
|
|
|
127 -------------
|
|
|
128 .. index:: No_Allocators
|
|
|
129
|
|
|
130 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
131 occurrences of an allocator.
|
|
|
132
|
|
|
133 No_Anonymous_Allocators
|
|
|
134 -----------------------
|
|
|
135 .. index:: No_Anonymous_Allocators
|
|
|
136
|
|
|
137 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
138 occurrences of an allocator of anonymous access type.
|
|
|
139
|
|
|
140 No_Asynchronous_Control
|
|
|
141 -----------------------
|
|
|
142 .. index:: No_Asynchronous_Control
|
|
|
143
|
|
|
144 [RM J.13] This restriction ensures at compile time that there are no semantic
|
|
|
145 dependences on the predefined package Asynchronous_Task_Control.
|
|
|
146
|
|
|
147 No_Calendar
|
|
|
148 -----------
|
|
|
149 .. index:: No_Calendar
|
|
|
150
|
|
|
151 [GNAT] This restriction ensures at compile time that there are no semantic
|
|
|
152 dependences on package Calendar.
|
|
|
153
|
|
|
154 No_Coextensions
|
|
|
155 ---------------
|
|
|
156 .. index:: No_Coextensions
|
|
|
157
|
|
|
158 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
159 coextensions. See 3.10.2.
|
|
|
160
|
|
|
161 No_Default_Initialization
|
|
|
162 -------------------------
|
|
|
163 .. index:: No_Default_Initialization
|
|
|
164
|
|
|
165 [GNAT] This restriction prohibits any instance of default initialization
|
|
|
166 of variables. The binder implements a consistency rule which prevents
|
|
|
167 any unit compiled without the restriction from with'ing a unit with the
|
|
|
168 restriction (this allows the generation of initialization procedures to
|
|
|
169 be skipped, since you can be sure that no call is ever generated to an
|
|
|
170 initialization procedure in a unit with the restriction active). If used
|
|
|
171 in conjunction with Initialize_Scalars or Normalize_Scalars, the effect
|
|
|
172 is to prohibit all cases of variables declared without a specific
|
|
|
173 initializer (including the case of OUT scalar parameters).
|
|
|
174
|
|
|
175 No_Delay
|
|
|
176 --------
|
|
|
177 .. index:: No_Delay
|
|
|
178
|
|
|
179 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
180 delay statements and no semantic dependences on package Calendar.
|
|
|
181
|
|
|
182 No_Dependence
|
|
|
183 -------------
|
|
|
184 .. index:: No_Dependence
|
|
|
185
|
|
|
186 [RM 13.12.1] This restriction ensures at compile time that there are no
|
|
|
187 dependences on a library unit.
|
|
|
188
|
|
|
189 No_Direct_Boolean_Operators
|
|
|
190 ---------------------------
|
|
|
191 .. index:: No_Direct_Boolean_Operators
|
|
|
192
|
|
|
193 [GNAT] This restriction ensures that no logical operators (and/or/xor)
|
|
|
194 are used on operands of type Boolean (or any type derived from Boolean).
|
|
|
195 This is intended for use in safety critical programs where the certification
|
|
|
196 protocol requires the use of short-circuit (and then, or else) forms for all
|
|
|
197 composite boolean operations.
|
|
|
198
|
|
|
199 No_Dispatch
|
|
|
200 -----------
|
|
|
201 .. index:: No_Dispatch
|
|
|
202
|
|
|
203 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
204 occurrences of ``T'Class``, for any (tagged) subtype ``T``.
|
|
|
205
|
|
|
206 No_Dispatching_Calls
|
|
|
207 --------------------
|
|
|
208 .. index:: No_Dispatching_Calls
|
|
|
209
|
|
|
210 [GNAT] This restriction ensures at compile time that the code generated by the
|
|
|
211 compiler involves no dispatching calls. The use of this restriction allows the
|
|
|
212 safe use of record extensions, classwide membership tests and other classwide
|
|
|
213 features not involving implicit dispatching. This restriction ensures that
|
|
|
214 the code contains no indirect calls through a dispatching mechanism. Note that
|
|
|
215 this includes internally-generated calls created by the compiler, for example
|
|
|
216 in the implementation of class-wide objects assignments. The
|
|
|
217 membership test is allowed in the presence of this restriction, because its
|
|
|
218 implementation requires no dispatching.
|
|
|
219 This restriction is comparable to the official Ada restriction
|
|
|
220 ``No_Dispatch`` except that it is a bit less restrictive in that it allows
|
|
|
221 all classwide constructs that do not imply dispatching.
|
|
|
222 The following example indicates constructs that violate this restriction.
|
|
|
223
|
|
|
224
|
|
|
225 .. code-block:: ada
|
|
|
226
|
|
|
227 package Pkg is
|
|
|
228 type T is tagged record
|
|
|
229 Data : Natural;
|
|
|
230 end record;
|
|
|
231 procedure P (X : T);
|
|
|
232
|
|
|
233 type DT is new T with record
|
|
|
234 More_Data : Natural;
|
|
|
235 end record;
|
|
|
236 procedure Q (X : DT);
|
|
|
237 end Pkg;
|
|
|
238
|
|
|
239 with Pkg; use Pkg;
|
|
|
240 procedure Example is
|
|
|
241 procedure Test (O : T'Class) is
|
|
|
242 N : Natural := O'Size;-- Error: Dispatching call
|
|
|
243 C : T'Class := O; -- Error: implicit Dispatching Call
|
|
|
244 begin
|
|
|
245 if O in DT'Class then -- OK : Membership test
|
|
|
246 Q (DT (O)); -- OK : Type conversion plus direct call
|
|
|
247 else
|
|
|
248 P (O); -- Error: Dispatching call
|
|
|
249 end if;
|
|
|
250 end Test;
|
|
|
251
|
|
|
252 Obj : DT;
|
|
|
253 begin
|
|
|
254 P (Obj); -- OK : Direct call
|
|
|
255 P (T (Obj)); -- OK : Type conversion plus direct call
|
|
|
256 P (T'Class (Obj)); -- Error: Dispatching call
|
|
|
257
|
|
|
258 Test (Obj); -- OK : Type conversion
|
|
|
259
|
|
|
260 if Obj in T'Class then -- OK : Membership test
|
|
|
261 null;
|
|
|
262 end if;
|
|
|
263 end Example;
|
|
|
264
|
|
|
265
|
|
|
266 No_Dynamic_Attachment
|
|
|
267 ---------------------
|
|
|
268 .. index:: No_Dynamic_Attachment
|
|
|
269
|
|
|
270 [RM D.7] This restriction ensures that there is no call to any of the
|
|
|
271 operations defined in package Ada.Interrupts
|
|
|
272 (Is_Reserved, Is_Attached, Current_Handler, Attach_Handler, Exchange_Handler,
|
|
|
273 Detach_Handler, and Reference).
|
|
|
274
|
|
|
275 .. index:: No_Dynamic_Interrupts
|
|
|
276
|
|
|
277 The restriction ``No_Dynamic_Interrupts`` is recognized as a
|
|
|
278 synonym for ``No_Dynamic_Attachment``. This is retained for historical
|
|
|
279 compatibility purposes (and a warning will be generated for its use if
|
|
|
280 warnings on obsolescent features are activated).
|
|
|
281
|
|
|
282 No_Dynamic_Priorities
|
|
|
283 ---------------------
|
|
|
284 .. index:: No_Dynamic_Priorities
|
|
|
285
|
|
|
286 [RM D.7] There are no semantic dependencies on the package Dynamic_Priorities.
|
|
|
287
|
|
|
288 No_Entry_Calls_In_Elaboration_Code
|
|
|
289 ----------------------------------
|
|
|
290 .. index:: No_Entry_Calls_In_Elaboration_Code
|
|
|
291
|
|
|
292 [GNAT] This restriction ensures at compile time that no task or protected entry
|
|
|
293 calls are made during elaboration code. As a result of the use of this
|
|
|
294 restriction, the compiler can assume that no code past an accept statement
|
|
|
295 in a task can be executed at elaboration time.
|
|
|
296
|
|
|
297 No_Enumeration_Maps
|
|
|
298 -------------------
|
|
|
299 .. index:: No_Enumeration_Maps
|
|
|
300
|
|
|
301 [GNAT] This restriction ensures at compile time that no operations requiring
|
|
|
302 enumeration maps are used (that is Image and Value attributes applied
|
|
|
303 to enumeration types).
|
|
|
304
|
|
|
305 No_Exception_Handlers
|
|
|
306 ---------------------
|
|
|
307 .. index:: No_Exception_Handlers
|
|
|
308
|
|
|
309 [GNAT] This restriction ensures at compile time that there are no explicit
|
|
|
310 exception handlers. It also indicates that no exception propagation will
|
|
|
311 be provided. In this mode, exceptions may be raised but will result in
|
|
|
312 an immediate call to the last chance handler, a routine that the user
|
|
|
313 must define with the following profile:
|
|
|
314
|
|
|
315
|
|
|
316 .. code-block:: ada
|
|
|
317
|
|
|
318 procedure Last_Chance_Handler
|
|
|
319 (Source_Location : System.Address; Line : Integer);
|
|
|
320 pragma Export (C, Last_Chance_Handler,
|
|
|
321 "__gnat_last_chance_handler");
|
|
|
322
|
|
|
323
|
|
|
324 The parameter is a C null-terminated string representing a message to be
|
|
|
325 associated with the exception (typically the source location of the raise
|
|
|
326 statement generated by the compiler). The Line parameter when nonzero
|
|
|
327 represents the line number in the source program where the raise occurs.
|
|
|
328
|
|
|
329 No_Exception_Propagation
|
|
|
330 ------------------------
|
|
|
331 .. index:: No_Exception_Propagation
|
|
|
332
|
|
|
333 [GNAT] This restriction guarantees that exceptions are never propagated
|
|
|
334 to an outer subprogram scope. The only case in which an exception may
|
|
|
335 be raised is when the handler is statically in the same subprogram, so
|
|
|
336 that the effect of a raise is essentially like a goto statement. Any
|
|
|
337 other raise statement (implicit or explicit) will be considered
|
|
|
338 unhandled. Exception handlers are allowed, but may not contain an
|
|
|
339 exception occurrence identifier (exception choice). In addition, use of
|
|
|
340 the package GNAT.Current_Exception is not permitted, and reraise
|
|
|
341 statements (raise with no operand) are not permitted.
|
|
|
342
|
|
|
343 No_Exception_Registration
|
|
|
344 -------------------------
|
|
|
345 .. index:: No_Exception_Registration
|
|
|
346
|
|
|
347 [GNAT] This restriction ensures at compile time that no stream operations for
|
|
|
348 types Exception_Id or Exception_Occurrence are used. This also makes it
|
|
|
349 impossible to pass exceptions to or from a partition with this restriction
|
|
|
350 in a distributed environment. If this restriction is active, the generated
|
|
|
351 code is simplified by omitting the otherwise-required global registration
|
|
|
352 of exceptions when they are declared.
|
|
|
353
|
|
|
354 No_Exceptions
|
|
|
355 -------------
|
|
|
356 .. index:: No_Exceptions
|
|
|
357
|
|
|
358 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
359 raise statements and no exception handlers.
|
|
|
360
|
|
|
361 No_Finalization
|
|
|
362 ---------------
|
|
|
363 .. index:: No_Finalization
|
|
|
364
|
|
|
365 [GNAT] This restriction disables the language features described in
|
|
|
366 chapter 7.6 of the Ada 2005 RM as well as all form of code generation
|
|
|
367 performed by the compiler to support these features. The following types
|
|
|
368 are no longer considered controlled when this restriction is in effect:
|
|
|
369
|
|
|
370 *
|
|
|
371 ``Ada.Finalization.Controlled``
|
|
|
372 *
|
|
|
373 ``Ada.Finalization.Limited_Controlled``
|
|
|
374 *
|
|
|
375 Derivations from ``Controlled`` or ``Limited_Controlled``
|
|
|
376 *
|
|
|
377 Class-wide types
|
|
|
378 *
|
|
|
379 Protected types
|
|
|
380 *
|
|
|
381 Task types
|
|
|
382 *
|
|
|
383 Array and record types with controlled components
|
|
|
384
|
|
|
385 The compiler no longer generates code to initialize, finalize or adjust an
|
|
|
386 object or a nested component, either declared on the stack or on the heap. The
|
|
|
387 deallocation of a controlled object no longer finalizes its contents.
|
|
|
388
|
|
|
389 No_Fixed_Point
|
|
|
390 --------------
|
|
|
391 .. index:: No_Fixed_Point
|
|
|
392
|
|
|
393 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
394 occurrences of fixed point types and operations.
|
|
|
395
|
|
|
396 No_Floating_Point
|
|
|
397 -----------------
|
|
|
398 .. index:: No_Floating_Point
|
|
|
399
|
|
|
400 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
401 occurrences of floating point types and operations.
|
|
|
402
|
|
|
403 No_Implicit_Conditionals
|
|
|
404 ------------------------
|
|
|
405 .. index:: No_Implicit_Conditionals
|
|
|
406
|
|
|
407 [GNAT] This restriction ensures that the generated code does not contain any
|
|
|
408 implicit conditionals, either by modifying the generated code where possible,
|
|
|
409 or by rejecting any construct that would otherwise generate an implicit
|
|
|
410 conditional. Note that this check does not include run time constraint
|
|
|
411 checks, which on some targets may generate implicit conditionals as
|
|
|
412 well. To control the latter, constraint checks can be suppressed in the
|
|
|
413 normal manner. Constructs generating implicit conditionals include comparisons
|
|
|
414 of composite objects and the Max/Min attributes.
|
|
|
415
|
|
|
416 No_Implicit_Dynamic_Code
|
|
|
417 ------------------------
|
|
|
418 .. index:: No_Implicit_Dynamic_Code
|
|
|
419 .. index:: trampoline
|
|
|
420
|
|
|
421 [GNAT] This restriction prevents the compiler from building 'trampolines'.
|
|
|
422 This is a structure that is built on the stack and contains dynamic
|
|
|
423 code to be executed at run time. On some targets, a trampoline is
|
|
|
424 built for the following features: ``Access``,
|
|
|
425 ``Unrestricted_Access``, or ``Address`` of a nested subprogram;
|
|
|
426 nested task bodies; primitive operations of nested tagged types.
|
|
|
427 Trampolines do not work on machines that prevent execution of stack
|
|
|
428 data. For example, on windows systems, enabling DEP (data execution
|
|
|
429 protection) will cause trampolines to raise an exception.
|
|
|
430 Trampolines are also quite slow at run time.
|
|
|
431
|
|
|
432 On many targets, trampolines have been largely eliminated. Look at the
|
|
|
433 version of system.ads for your target --- if it has
|
|
|
434 Always_Compatible_Rep equal to False, then trampolines are largely
|
|
|
435 eliminated. In particular, a trampoline is built for the following
|
|
|
436 features: ``Address`` of a nested subprogram;
|
|
|
437 ``Access`` or ``Unrestricted_Access`` of a nested subprogram,
|
|
|
438 but only if pragma Favor_Top_Level applies, or the access type has a
|
|
|
439 foreign-language convention; primitive operations of nested tagged
|
|
|
440 types.
|
|
|
441
|
|
|
442 No_Implicit_Heap_Allocations
|
|
|
443 ----------------------------
|
|
|
444 .. index:: No_Implicit_Heap_Allocations
|
|
|
445
|
|
|
446 [RM D.7] No constructs are allowed to cause implicit heap allocation.
|
|
|
447
|
|
|
448 No_Implicit_Protected_Object_Allocations
|
|
|
449 ----------------------------------------
|
|
|
450 .. index:: No_Implicit_Protected_Object_Allocations
|
|
|
451
|
|
|
452 [GNAT] No constructs are allowed to cause implicit heap allocation of a
|
|
|
453 protected object.
|
|
|
454
|
|
|
455 No_Implicit_Task_Allocations
|
|
|
456 ----------------------------
|
|
|
457 .. index:: No_Implicit_Task_Allocations
|
|
|
458
|
|
|
459 [GNAT] No constructs are allowed to cause implicit heap allocation of a task.
|
|
|
460
|
|
|
461 No_Initialize_Scalars
|
|
|
462 ---------------------
|
|
|
463 .. index:: No_Initialize_Scalars
|
|
|
464
|
|
|
465 [GNAT] This restriction ensures that no unit in the partition is compiled with
|
|
|
466 pragma Initialize_Scalars. This allows the generation of more efficient
|
|
|
467 code, and in particular eliminates dummy null initialization routines that
|
|
|
468 are otherwise generated for some record and array types.
|
|
|
469
|
|
|
470 No_IO
|
|
|
471 -----
|
|
|
472 .. index:: No_IO
|
|
|
473
|
|
|
474 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
475 dependences on any of the library units Sequential_IO, Direct_IO,
|
|
|
476 Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, or Stream_IO.
|
|
|
477
|
|
|
478 No_Local_Allocators
|
|
|
479 -------------------
|
|
|
480 .. index:: No_Local_Allocators
|
|
|
481
|
|
|
482 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
483 occurrences of an allocator in subprograms, generic subprograms, tasks,
|
|
|
484 and entry bodies.
|
|
|
485
|
|
|
486 No_Local_Protected_Objects
|
|
|
487 --------------------------
|
|
|
488 .. index:: No_Local_Protected_Objects
|
|
|
489
|
|
|
490 [RM D.7] This restriction ensures at compile time that protected objects are
|
|
|
491 only declared at the library level.
|
|
|
492
|
|
|
493 No_Local_Timing_Events
|
|
|
494 ----------------------
|
|
|
495 .. index:: No_Local_Timing_Events
|
|
|
496
|
|
|
497 [RM D.7] All objects of type Ada.Timing_Events.Timing_Event are
|
|
|
498 declared at the library level.
|
|
|
499
|
|
|
500 No_Long_Long_Integers
|
|
|
501 ---------------------
|
|
|
502 .. index:: No_Long_Long_Integers
|
|
|
503
|
|
|
504 [GNAT] This partition-wide restriction forbids any explicit reference to
|
|
|
505 type Standard.Long_Long_Integer, and also forbids declaring range types whose
|
|
|
506 implicit base type is Long_Long_Integer, and modular types whose size exceeds
|
|
|
507 Long_Integer'Size.
|
|
|
508
|
|
|
509 No_Multiple_Elaboration
|
|
|
510 -----------------------
|
|
|
511 .. index:: No_Multiple_Elaboration
|
|
|
512
|
|
|
513 [GNAT] When this restriction is active, we are not requesting control-flow
|
|
|
514 preservation with -fpreserve-control-flow, and the static elaboration model is
|
|
|
515 used, the compiler is allowed to suppress the elaboration counter normally
|
|
|
516 associated with the unit, even if the unit has elaboration code. This counter
|
|
|
517 is typically used to check for access before elaboration and to control
|
|
|
518 multiple elaboration attempts. If the restriction is used, then the
|
|
|
519 situations in which multiple elaboration is possible, including non-Ada main
|
|
|
520 programs and Stand Alone libraries, are not permitted and will be diagnosed
|
|
|
521 by the binder.
|
|
|
522
|
|
|
523 No_Nested_Finalization
|
|
|
524 ----------------------
|
|
|
525 .. index:: No_Nested_Finalization
|
|
|
526
|
|
|
527 [RM D.7] All objects requiring finalization are declared at the library level.
|
|
|
528
|
|
|
529 No_Protected_Type_Allocators
|
|
|
530 ----------------------------
|
|
|
531 .. index:: No_Protected_Type_Allocators
|
|
|
532
|
|
|
533 [RM D.7] This restriction ensures at compile time that there are no allocator
|
|
|
534 expressions that attempt to allocate protected objects.
|
|
|
535
|
|
|
536 No_Protected_Types
|
|
|
537 ------------------
|
|
|
538 .. index:: No_Protected_Types
|
|
|
539
|
|
|
540 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
541 declarations of protected types or protected objects.
|
|
|
542
|
|
|
543 No_Recursion
|
|
|
544 ------------
|
|
|
545 .. index:: No_Recursion
|
|
|
546
|
|
|
547 [RM H.4] A program execution is erroneous if a subprogram is invoked as
|
|
|
548 part of its execution.
|
|
|
549
|
|
|
550 No_Reentrancy
|
|
|
551 -------------
|
|
|
552 .. index:: No_Reentrancy
|
|
|
553
|
|
|
554 [RM H.4] A program execution is erroneous if a subprogram is executed by
|
|
|
555 two tasks at the same time.
|
|
|
556
|
|
|
557 No_Relative_Delay
|
|
|
558 -----------------
|
|
|
559 .. index:: No_Relative_Delay
|
|
|
560
|
|
|
561 [RM D.7] This restriction ensures at compile time that there are no delay
|
|
|
562 relative statements and prevents expressions such as ``delay 1.23;`` from
|
|
|
563 appearing in source code.
|
|
|
564
|
|
|
565 No_Requeue_Statements
|
|
|
566 ---------------------
|
|
|
567 .. index:: No_Requeue_Statements
|
|
|
568
|
|
|
569 [RM D.7] This restriction ensures at compile time that no requeue statements
|
|
|
570 are permitted and prevents keyword ``requeue`` from being used in source
|
|
|
571 code.
|
|
|
572
|
|
|
573 .. index:: No_Requeue
|
|
|
574
|
|
|
575 The restriction ``No_Requeue`` is recognized as a
|
|
|
576 synonym for ``No_Requeue_Statements``. This is retained for historical
|
|
|
577 compatibility purposes (and a warning will be generated for its use if
|
|
|
578 warnings on oNobsolescent features are activated).
|
|
|
579
|
|
|
580 No_Secondary_Stack
|
|
|
581 ------------------
|
|
|
582 .. index:: No_Secondary_Stack
|
|
|
583
|
|
|
584 [GNAT] This restriction ensures at compile time that the generated code
|
|
|
585 does not contain any reference to the secondary stack. The secondary
|
|
|
586 stack is used to implement functions returning unconstrained objects
|
|
|
587 (arrays or records) on some targets. Suppresses the allocation of
|
|
|
588 secondary stacks for tasks (excluding the environment task) at run time.
|
|
|
589
|
|
|
590 No_Select_Statements
|
|
|
591 --------------------
|
|
|
592 .. index:: No_Select_Statements
|
|
|
593
|
|
|
594 [RM D.7] This restriction ensures at compile time no select statements of any
|
|
|
595 kind are permitted, that is the keyword ``select`` may not appear.
|
|
|
596
|
|
|
597 No_Specific_Termination_Handlers
|
|
|
598 --------------------------------
|
|
|
599 .. index:: No_Specific_Termination_Handlers
|
|
|
600
|
|
|
601 [RM D.7] There are no calls to Ada.Task_Termination.Set_Specific_Handler
|
|
|
602 or to Ada.Task_Termination.Specific_Handler.
|
|
|
603
|
|
|
604 No_Specification_of_Aspect
|
|
|
605 --------------------------
|
|
|
606 .. index:: No_Specification_of_Aspect
|
|
|
607
|
|
|
608 [RM 13.12.1] This restriction checks at compile time that no aspect
|
|
|
609 specification, attribute definition clause, or pragma is given for a
|
|
|
610 given aspect.
|
|
|
611
|
|
|
612 No_Standard_Allocators_After_Elaboration
|
|
|
613 ----------------------------------------
|
|
|
614 .. index:: No_Standard_Allocators_After_Elaboration
|
|
|
615
|
|
|
616 [RM D.7] Specifies that an allocator using a standard storage pool
|
|
|
617 should never be evaluated at run time after the elaboration of the
|
|
|
618 library items of the partition has completed. Otherwise, Storage_Error
|
|
|
619 is raised.
|
|
|
620
|
|
|
621 No_Standard_Storage_Pools
|
|
|
622 -------------------------
|
|
|
623 .. index:: No_Standard_Storage_Pools
|
|
|
624
|
|
|
625 [GNAT] This restriction ensures at compile time that no access types
|
|
|
626 use the standard default storage pool. Any access type declared must
|
|
|
627 have an explicit Storage_Pool attribute defined specifying a
|
|
|
628 user-defined storage pool.
|
|
|
629
|
|
|
630 No_Stream_Optimizations
|
|
|
631 -----------------------
|
|
|
632 .. index:: No_Stream_Optimizations
|
|
|
633
|
|
|
634 [GNAT] This restriction affects the performance of stream operations on types
|
|
|
635 ``String``, ``Wide_String`` and ``Wide_Wide_String``. By default, the
|
|
|
636 compiler uses block reads and writes when manipulating ``String`` objects
|
|
|
637 due to their supperior performance. When this restriction is in effect, the
|
|
|
638 compiler performs all IO operations on a per-character basis.
|
|
|
639
|
|
|
640 No_Streams
|
|
|
641 ----------
|
|
|
642 .. index:: No_Streams
|
|
|
643
|
|
|
644 [GNAT] This restriction ensures at compile/bind time that there are no
|
|
|
645 stream objects created and no use of stream attributes.
|
|
|
646 This restriction does not forbid dependences on the package
|
|
|
647 ``Ada.Streams``. So it is permissible to with
|
|
|
648 ``Ada.Streams`` (or another package that does so itself)
|
|
|
649 as long as no actual stream objects are created and no
|
|
|
650 stream attributes are used.
|
|
|
651
|
|
|
652 Note that the use of restriction allows optimization of tagged types,
|
|
|
653 since they do not need to worry about dispatching stream operations.
|
|
|
654 To take maximum advantage of this space-saving optimization, any
|
|
|
655 unit declaring a tagged type should be compiled with the restriction,
|
|
|
656 though this is not required.
|
|
|
657
|
|
|
658 No_Task_Allocators
|
|
|
659 ------------------
|
|
|
660 .. index:: No_Task_Allocators
|
|
|
661
|
|
|
662 [RM D.7] There are no allocators for task types
|
|
|
663 or types containing task subcomponents.
|
|
|
664
|
|
|
665 No_Task_At_Interrupt_Priority
|
|
|
666 -----------------------------
|
|
|
667 .. index:: No_Task_At_Interrupt_Priority
|
|
|
668
|
|
|
669 [GNAT] This restriction ensures at compile time that there is no
|
|
|
670 Interrupt_Priority aspect or pragma for a task or a task type. As
|
|
|
671 a consequence, the tasks are always created with a priority below
|
|
|
672 that an interrupt priority.
|
|
|
673
|
|
|
674 No_Task_Attributes_Package
|
|
|
675 --------------------------
|
|
|
676 .. index:: No_Task_Attributes_Package
|
|
|
677
|
|
|
678 [GNAT] This restriction ensures at compile time that there are no implicit or
|
|
|
679 explicit dependencies on the package ``Ada.Task_Attributes``.
|
|
|
680
|
|
|
681 .. index:: No_Task_Attributes
|
|
|
682
|
|
|
683 The restriction ``No_Task_Attributes`` is recognized as a synonym
|
|
|
684 for ``No_Task_Attributes_Package``. This is retained for historical
|
|
|
685 compatibility purposes (and a warning will be generated for its use if
|
|
|
686 warnings on obsolescent features are activated).
|
|
|
687
|
|
|
688 No_Task_Hierarchy
|
|
|
689 -----------------
|
|
|
690 .. index:: No_Task_Hierarchy
|
|
|
691
|
|
|
692 [RM D.7] All (non-environment) tasks depend
|
|
|
693 directly on the environment task of the partition.
|
|
|
694
|
|
|
695 No_Task_Termination
|
|
|
696 -------------------
|
|
|
697 .. index:: No_Task_Termination
|
|
|
698
|
|
|
699 [RM D.7] Tasks that terminate are erroneous.
|
|
|
700
|
|
|
701 No_Tasking
|
|
|
702 ----------
|
|
|
703 .. index:: No_Tasking
|
|
|
704
|
|
|
705 [GNAT] This restriction prevents the declaration of tasks or task types
|
|
|
706 throughout the partition. It is similar in effect to the use of
|
|
|
707 ``Max_Tasks => 0`` except that violations are caught at compile time
|
|
|
708 and cause an error message to be output either by the compiler or
|
|
|
709 binder.
|
|
|
710
|
|
|
711 No_Terminate_Alternatives
|
|
|
712 -------------------------
|
|
|
713 .. index:: No_Terminate_Alternatives
|
|
|
714
|
|
|
715 [RM D.7] There are no selective accepts with terminate alternatives.
|
|
|
716
|
|
|
717 No_Unchecked_Access
|
|
|
718 -------------------
|
|
|
719 .. index:: No_Unchecked_Access
|
|
|
720
|
|
|
721 [RM H.4] This restriction ensures at compile time that there are no
|
|
|
722 occurrences of the Unchecked_Access attribute.
|
|
|
723
|
|
|
724 No_Unchecked_Conversion
|
|
|
725 -----------------------
|
|
|
726 .. index:: No_Unchecked_Conversion
|
|
|
727
|
|
|
728 [RM J.13] This restriction ensures at compile time that there are no semantic
|
|
|
729 dependences on the predefined generic function Unchecked_Conversion.
|
|
|
730
|
|
|
731 No_Unchecked_Deallocation
|
|
|
732 -------------------------
|
|
|
733 .. index:: No_Unchecked_Deallocation
|
|
|
734
|
|
|
735 [RM J.13] This restriction ensures at compile time that there are no semantic
|
|
|
736 dependences on the predefined generic procedure Unchecked_Deallocation.
|
|
|
737
|
|
|
738 No_Use_Of_Entity
|
|
|
739 ----------------
|
|
|
740 .. index:: No_Use_Of_Entity
|
|
|
741
|
|
|
742 [GNAT] This restriction ensures at compile time that there are no references
|
|
|
743 to the entity given in the form ::
|
|
|
744
|
|
|
745 No_Use_Of_Entity => Name
|
|
|
746
|
|
|
747 where ``Name`` is the fully qualified entity, for example ::
|
|
|
748
|
|
|
749 No_Use_Of_Entity => Ada.Text_IO.Put_Line
|
|
|
750
|
|
|
751 Pure_Barriers
|
|
|
752 -------------
|
|
|
753 .. index:: Pure_Barriers
|
|
|
754
|
|
|
755 [GNAT] This restriction ensures at compile time that protected entry
|
|
|
756 barriers are restricted to:
|
|
|
757
|
|
|
758 * components of the protected object (excluding selection from dereferences),
|
|
|
759 * constant declarations,
|
|
|
760 * named numbers,
|
|
|
761 * enumeration literals,
|
|
|
762 * integer literals,
|
|
|
763 * real literals,
|
|
|
764 * character literals,
|
|
|
765 * implicitly defined comparison operators,
|
|
|
766 * uses of the Standard."not" operator,
|
|
|
767 * short-circuit operator,
|
|
|
768 * the Count attribute
|
|
|
769
|
|
|
770 This restriction is a relaxation of the Simple_Barriers restriction,
|
|
|
771 but still ensures absence of side effects, exceptions, and recursion
|
|
|
772 during the evaluation of the barriers.
|
|
|
773
|
|
|
774 Simple_Barriers
|
|
|
775 ---------------
|
|
|
776 .. index:: Simple_Barriers
|
|
|
777
|
|
|
778 [RM D.7] This restriction ensures at compile time that barriers in entry
|
|
|
779 declarations for protected types are restricted to either static boolean
|
|
|
780 expressions or references to simple boolean variables defined in the private
|
|
|
781 part of the protected type. No other form of entry barriers is permitted.
|
|
|
782
|
|
|
783 .. index:: Boolean_Entry_Barriers
|
|
|
784
|
|
|
785 The restriction ``Boolean_Entry_Barriers`` is recognized as a
|
|
|
786 synonym for ``Simple_Barriers``. This is retained for historical
|
|
|
787 compatibility purposes (and a warning will be generated for its use if
|
|
|
788 warnings on obsolescent features are activated).
|
|
|
789
|
|
|
790 Static_Priorities
|
|
|
791 -----------------
|
|
|
792 .. index:: Static_Priorities
|
|
|
793
|
|
|
794 [GNAT] This restriction ensures at compile time that all priority expressions
|
|
|
795 are static, and that there are no dependences on the package
|
|
|
796 ``Ada.Dynamic_Priorities``.
|
|
|
797
|
|
|
798 Static_Storage_Size
|
|
|
799 -------------------
|
|
|
800 .. index:: Static_Storage_Size
|
|
|
801
|
|
|
802 [GNAT] This restriction ensures at compile time that any expression appearing
|
|
|
803 in a Storage_Size pragma or attribute definition clause is static.
|
|
|
804
|
|
|
805 .. _Program_Unit_Level_Restrictions:
|
|
|
806
|
|
|
807
|
|
|
808 Program Unit Level Restrictions
|
|
|
809 ===============================
|
|
|
810
|
|
|
811 The second set of restriction identifiers
|
|
|
812 does not require partition-wide consistency.
|
|
|
813 The restriction may be enforced for a single
|
|
|
814 compilation unit without any effect on any of the
|
|
|
815 other compilation units in the partition.
|
|
|
816
|
|
|
817 No_Elaboration_Code
|
|
|
818 -------------------
|
|
|
819 .. index:: No_Elaboration_Code
|
|
|
820
|
|
|
821 [GNAT] This restriction ensures at compile time that no elaboration code is
|
|
|
822 generated. Note that this is not the same condition as is enforced
|
|
|
823 by pragma ``Preelaborate``. There are cases in which pragma
|
|
|
824 ``Preelaborate`` still permits code to be generated (e.g., code
|
|
|
825 to initialize a large array to all zeroes), and there are cases of units
|
|
|
826 which do not meet the requirements for pragma ``Preelaborate``,
|
|
|
827 but for which no elaboration code is generated. Generally, it is
|
|
|
828 the case that preelaborable units will meet the restrictions, with
|
|
|
829 the exception of large aggregates initialized with an others_clause,
|
|
|
830 and exception declarations (which generate calls to a run-time
|
|
|
831 registry procedure). This restriction is enforced on
|
|
|
832 a unit by unit basis, it need not be obeyed consistently
|
|
|
833 throughout a partition.
|
|
|
834
|
|
|
835 In the case of aggregates with others, if the aggregate has a dynamic
|
|
|
836 size, there is no way to eliminate the elaboration code (such dynamic
|
|
|
837 bounds would be incompatible with ``Preelaborate`` in any case). If
|
|
|
838 the bounds are static, then use of this restriction actually modifies
|
|
|
839 the code choice of the compiler to avoid generating a loop, and instead
|
|
|
840 generate the aggregate statically if possible, no matter how many times
|
|
|
841 the data for the others clause must be repeatedly generated.
|
|
|
842
|
|
|
843 It is not possible to precisely document
|
|
|
844 the constructs which are compatible with this restriction, since,
|
|
|
845 unlike most other restrictions, this is not a restriction on the
|
|
|
846 source code, but a restriction on the generated object code. For
|
|
|
847 example, if the source contains a declaration:
|
|
|
848
|
|
|
849
|
|
|
850 .. code-block:: ada
|
|
|
851
|
|
|
852 Val : constant Integer := X;
|
|
|
853
|
|
|
854
|
|
|
855 where X is not a static constant, it may be possible, depending
|
|
|
856 on complex optimization circuitry, for the compiler to figure
|
|
|
857 out the value of X at compile time, in which case this initialization
|
|
|
858 can be done by the loader, and requires no initialization code. It
|
|
|
859 is not possible to document the precise conditions under which the
|
|
|
860 optimizer can figure this out.
|
|
|
861
|
|
|
862 Note that this the implementation of this restriction requires full
|
|
|
863 code generation. If it is used in conjunction with "semantics only"
|
|
|
864 checking, then some cases of violations may be missed.
|
|
|
865
|
|
|
866 When this restriction is active, we are not requesting control-flow
|
|
|
867 preservation with -fpreserve-control-flow, and the static elaboration model is
|
|
|
868 used, the compiler is allowed to suppress the elaboration counter normally
|
|
|
869 associated with the unit. This counter is typically used to check for access
|
|
|
870 before elaboration and to control multiple elaboration attempts.
|
|
|
871
|
|
|
872 No_Dynamic_Sized_Objects
|
|
|
873 ------------------------
|
|
|
874 .. index:: No_Dynamic_Sized_Objects
|
|
|
875
|
|
|
876 [GNAT] This restriction disallows certain constructs that might lead to the
|
|
|
877 creation of dynamic-sized composite objects (or array or discriminated type).
|
|
|
878 An array subtype indication is illegal if the bounds are not static
|
|
|
879 or references to discriminants of an enclosing type.
|
|
|
880 A discriminated subtype indication is illegal if the type has
|
|
|
881 discriminant-dependent array components or a variant part, and the
|
|
|
882 discriminants are not static. In addition, array and record aggregates are
|
|
|
883 illegal in corresponding cases. Note that this restriction does not forbid
|
|
|
884 access discriminants. It is often a good idea to combine this restriction
|
|
|
885 with No_Secondary_Stack.
|
|
|
886
|
|
|
887 No_Entry_Queue
|
|
|
888 --------------
|
|
|
889 .. index:: No_Entry_Queue
|
|
|
890
|
|
|
891 [GNAT] This restriction is a declaration that any protected entry compiled in
|
|
|
892 the scope of the restriction has at most one task waiting on the entry
|
|
|
893 at any one time, and so no queue is required. This restriction is not
|
|
|
894 checked at compile time. A program execution is erroneous if an attempt
|
|
|
895 is made to queue a second task on such an entry.
|
|
|
896
|
|
|
897 No_Implementation_Aspect_Specifications
|
|
|
898 ---------------------------------------
|
|
|
899 .. index:: No_Implementation_Aspect_Specifications
|
|
|
900
|
|
|
901 [RM 13.12.1] This restriction checks at compile time that no
|
|
|
902 GNAT-defined aspects are present. With this restriction, the only
|
|
|
903 aspects that can be used are those defined in the Ada Reference Manual.
|
|
|
904
|
|
|
905 No_Implementation_Attributes
|
|
|
906 ----------------------------
|
|
|
907 .. index:: No_Implementation_Attributes
|
|
|
908
|
|
|
909 [RM 13.12.1] This restriction checks at compile time that no
|
|
|
910 GNAT-defined attributes are present. With this restriction, the only
|
|
|
911 attributes that can be used are those defined in the Ada Reference
|
|
|
912 Manual.
|
|
|
913
|
|
|
914 No_Implementation_Identifiers
|
|
|
915 -----------------------------
|
|
|
916 .. index:: No_Implementation_Identifiers
|
|
|
917
|
|
|
918 [RM 13.12.1] This restriction checks at compile time that no
|
|
|
919 implementation-defined identifiers (marked with pragma Implementation_Defined)
|
|
|
920 occur within language-defined packages.
|
|
|
921
|
|
|
922 No_Implementation_Pragmas
|
|
|
923 -------------------------
|
|
|
924 .. index:: No_Implementation_Pragmas
|
|
|
925
|
|
|
926 [RM 13.12.1] This restriction checks at compile time that no
|
|
|
927 GNAT-defined pragmas are present. With this restriction, the only
|
|
|
928 pragmas that can be used are those defined in the Ada Reference Manual.
|
|
|
929
|
|
|
930 No_Implementation_Restrictions
|
|
|
931 ------------------------------
|
|
|
932 .. index:: No_Implementation_Restrictions
|
|
|
933
|
|
|
934 [GNAT] This restriction checks at compile time that no GNAT-defined restriction
|
|
|
935 identifiers (other than ``No_Implementation_Restrictions`` itself)
|
|
|
936 are present. With this restriction, the only other restriction identifiers
|
|
|
937 that can be used are those defined in the Ada Reference Manual.
|
|
|
938
|
|
|
939 No_Implementation_Units
|
|
|
940 -----------------------
|
|
|
941 .. index:: No_Implementation_Units
|
|
|
942
|
|
|
943 [RM 13.12.1] This restriction checks at compile time that there is no
|
|
|
944 mention in the context clause of any implementation-defined descendants
|
|
|
945 of packages Ada, Interfaces, or System.
|
|
|
946
|
|
|
947 No_Implicit_Aliasing
|
|
|
948 --------------------
|
|
|
949 .. index:: No_Implicit_Aliasing
|
|
|
950
|
|
|
951 [GNAT] This restriction, which is not required to be partition-wide consistent,
|
|
|
952 requires an explicit aliased keyword for an object to which 'Access,
|
|
|
953 'Unchecked_Access, or 'Address is applied, and forbids entirely the use of
|
|
|
954 the 'Unrestricted_Access attribute for objects. Note: the reason that
|
|
|
955 Unrestricted_Access is forbidden is that it would require the prefix
|
|
|
956 to be aliased, and in such cases, it can always be replaced by
|
|
|
957 the standard attribute Unchecked_Access which is preferable.
|
|
|
958
|
|
|
959 No_Implicit_Loops
|
|
|
960 -----------------
|
|
|
961 .. index:: No_Implicit_Loops
|
|
|
962
|
|
|
963 [GNAT] This restriction ensures that the generated code of the unit marked
|
|
|
964 with this restriction does not contain any implicit ``for`` loops, either by
|
|
|
965 modifying the generated code where possible, or by rejecting any construct
|
|
|
966 that would otherwise generate an implicit ``for`` loop. If this restriction is
|
|
|
967 active, it is possible to build large array aggregates with all static
|
|
|
968 components without generating an intermediate temporary, and without generating
|
|
|
969 a loop to initialize individual components. Otherwise, a loop is created for
|
|
|
970 arrays larger than about 5000 scalar components. Note that if this restriction
|
|
|
971 is set in the spec of a package, it will not apply to its body.
|
|
|
972
|
|
|
973 No_Obsolescent_Features
|
|
|
974 -----------------------
|
|
|
975 .. index:: No_Obsolescent_Features
|
|
|
976
|
|
|
977 [RM 13.12.1] This restriction checks at compile time that no obsolescent
|
|
|
978 features are used, as defined in Annex J of the Ada Reference Manual.
|
|
|
979
|
|
|
980 No_Wide_Characters
|
|
|
981 ------------------
|
|
|
982 .. index:: No_Wide_Characters
|
|
|
983
|
|
|
984 [GNAT] This restriction ensures at compile time that no uses of the types
|
|
|
985 ``Wide_Character`` or ``Wide_String`` or corresponding wide
|
|
|
986 wide types
|
|
|
987 appear, and that no wide or wide wide string or character literals
|
|
|
988 appear in the program (that is literals representing characters not in
|
|
|
989 type ``Character``).
|
|
|
990
|
|
131
|
991 Static_Dispatch_Tables
|
|
|
992 ----------------------
|
|
|
993 .. index:: Static_Dispatch_Tables
|
|
|
994
|
|
|
995 [GNAT] This restriction checks at compile time that all the artifacts
|
|
|
996 associated with dispatch tables can be placed in read-only memory.
|
|
|
997
|
|
111
|
998 SPARK_05
|
|
|
999 --------
|
|
|
1000 .. index:: SPARK_05
|
|
|
1001
|
|
131
|
1002 [GNAT] This restriction checks at compile time that some constructs forbidden
|
|
|
1003 in SPARK 2005 are not present. Note that SPARK 2005 has been superseded by
|
|
|
1004 SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that
|
|
|
1005 a codebase respects SPARK 2014 restrictions, mark the code with pragma or
|
|
|
1006 aspect ``SPARK_Mode``, and run the tool GNATprove at Stone assurance level, as
|
|
|
1007 follows::
|
|
111
|
1008
|
|
131
|
1009 gnatprove -P project.gpr --mode=stone
|
|
|
1010
|
|
|
1011 or equivalently::
|
|
|
1012
|
|
|
1013 gnatprove -P project.gpr --mode=check_all
|
|
|
1014
|
|
|
1015 With restriction ``SPARK_05``, error messages related to SPARK 2005 restriction
|
|
|
1016 have the form:
|
|
111
|
1017
|
|
|
1018 ::
|
|
|
1019
|
|
|
1020 violation of restriction "SPARK_05" at <source-location>
|
|
|
1021 <error message>
|
|
|
1022
|
|
|
1023 .. index:: SPARK
|
|
|
1024
|
|
131
|
1025 The restriction ``SPARK`` is recognized as a synonym for ``SPARK_05``. This is
|
|
|
1026 retained for historical compatibility purposes (and an unconditional warning
|
|
|
1027 will be generated for its use, advising replacement by ``SPARK_05``).
|
|
111
|
1028
|
|
|
1029 This is not a replacement for the semantic checks performed by the
|
|
|
1030 SPARK Examiner tool, as the compiler currently only deals with code,
|
|
|
1031 not SPARK 2005 annotations, and does not guarantee catching all
|
|
|
1032 cases of constructs forbidden by SPARK 2005.
|
|
|
1033
|
|
|
1034 Thus it may well be the case that code which passes the compiler with
|
|
131
|
1035 the SPARK 2005 restriction is rejected by the SPARK Examiner, e.g. due to
|
|
111
|
1036 the different visibility rules of the Examiner based on SPARK 2005
|
|
|
1037 ``inherit`` annotations.
|
|
|
1038
|
|
|
1039 This restriction can be useful in providing an initial filter for code
|
|
|
1040 developed using SPARK 2005, or in examining legacy code to see how far
|
|
131
|
1041 it is from meeting SPARK 2005 restrictions.
|
|
111
|
1042
|
|
|
1043 The list below summarizes the checks that are performed when this
|
|
|
1044 restriction is in force:
|
|
|
1045
|
|
|
1046 * No block statements
|
|
|
1047 * No case statements with only an others clause
|
|
|
1048 * Exit statements in loops must respect the SPARK 2005 language restrictions
|
|
|
1049 * No goto statements
|
|
|
1050 * Return can only appear as last statement in function
|
|
|
1051 * Function must have return statement
|
|
|
1052 * Loop parameter specification must include subtype mark
|
|
|
1053 * Prefix of expanded name cannot be a loop statement
|
|
|
1054 * Abstract subprogram not allowed
|
|
|
1055 * User-defined operators not allowed
|
|
|
1056 * Access type parameters not allowed
|
|
|
1057 * Default expressions for parameters not allowed
|
|
|
1058 * Default expressions for record fields not allowed
|
|
|
1059 * No tasking constructs allowed
|
|
|
1060 * Label needed at end of subprograms and packages
|
|
|
1061 * No mixing of positional and named parameter association
|
|
|
1062 * No access types as result type
|
|
|
1063 * No unconstrained arrays as result types
|
|
|
1064 * No null procedures
|
|
|
1065 * Initial and later declarations must be in correct order (declaration can't come after body)
|
|
|
1066 * No attributes on private types if full declaration not visible
|
|
|
1067 * No package declaration within package specification
|
|
|
1068 * No controlled types
|
|
|
1069 * No discriminant types
|
|
|
1070 * No overloading
|
|
|
1071 * Selector name cannot be operator symbol (i.e. operator symbol cannot be prefixed)
|
|
|
1072 * Access attribute not allowed
|
|
|
1073 * Allocator not allowed
|
|
|
1074 * Result of catenation must be String
|
|
|
1075 * Operands of catenation must be string literal, static char or another catenation
|
|
|
1076 * No conditional expressions
|
|
|
1077 * No explicit dereference
|
|
|
1078 * Quantified expression not allowed
|
|
|
1079 * Slicing not allowed
|
|
|
1080 * No exception renaming
|
|
|
1081 * No generic renaming
|
|
|
1082 * No object renaming
|
|
|
1083 * No use clause
|
|
|
1084 * Aggregates must be qualified
|
|
|
1085 * Nonstatic choice in array aggregates not allowed
|
|
|
1086 * The only view conversions which are allowed as in-out parameters are conversions of a tagged type to an ancestor type
|
|
|
1087 * No mixing of positional and named association in aggregate, no multi choice
|
|
|
1088 * AND, OR and XOR for arrays only allowed when operands have same static bounds
|
|
|
1089 * Fixed point operands to * or / must be qualified or converted
|
|
|
1090 * Comparison operators not allowed for Booleans or arrays (except strings)
|
|
|
1091 * Equality not allowed for arrays with non-matching static bounds (except strings)
|
|
|
1092 * Conversion / qualification not allowed for arrays with non-matching static bounds
|
|
|
1093 * Subprogram declaration only allowed in package spec (unless followed by import)
|
|
|
1094 * Access types not allowed
|
|
|
1095 * Incomplete type declaration not allowed
|
|
131
|
1096 * Object and subtype declarations must respect SPARK 2005 restrictions
|
|
111
|
1097 * Digits or delta constraint not allowed
|
|
|
1098 * Decimal fixed point type not allowed
|
|
|
1099 * Aliasing of objects not allowed
|
|
|
1100 * Modular type modulus must be power of 2
|
|
|
1101 * Base not allowed on subtype mark
|
|
|
1102 * Unary operators not allowed on modular types (except not)
|
|
|
1103 * Untagged record cannot be null
|
|
|
1104 * No class-wide operations
|
|
131
|
1105 * Initialization expressions must respect SPARK 2005 restrictions
|
|
111
|
1106 * Nonstatic ranges not allowed except in iteration schemes
|
|
|
1107 * String subtypes must have lower bound of 1
|
|
|
1108 * Subtype of Boolean cannot have constraint
|
|
|
1109 * At most one tagged type or extension per package
|
|
|
1110 * Interface is not allowed
|
|
|
1111 * Character literal cannot be prefixed (selector name cannot be character literal)
|
|
|
1112 * Record aggregate cannot contain 'others'
|
|
|
1113 * Component association in record aggregate must contain a single choice
|
|
|
1114 * Ancestor part cannot be a type mark
|
|
|
1115 * Attributes 'Image, 'Width and 'Value not allowed
|
|
|
1116 * Functions may not update globals
|
|
|
1117 * Subprograms may not contain direct calls to themselves (prevents recursion within unit)
|
|
|
1118 * Call to subprogram not allowed in same unit before body has been seen (prevents recursion within unit)
|
|
|
1119
|
|
|
1120 The following restrictions are enforced, but note that they are actually more
|
|
|
1121 strict that the latest SPARK 2005 language definition:
|
|
|
1122
|
|
|
1123 * No derived types other than tagged type extensions
|
|
|
1124 * Subtype of unconstrained array must have constraint
|
|
|
1125
|
|
|
1126 This list summarises the main SPARK 2005 language rules that are not
|
|
|
1127 currently checked by the SPARK_05 restriction:
|
|
|
1128
|
|
131
|
1129 * SPARK 2005 annotations are treated as comments so are not checked at all
|
|
111
|
1130 * Based real literals not allowed
|
|
|
1131 * Objects cannot be initialized at declaration by calls to user-defined functions
|
|
|
1132 * Objects cannot be initialized at declaration by assignments from variables
|
|
|
1133 * Objects cannot be initialized at declaration by assignments from indexed/selected components
|
|
|
1134 * Ranges shall not be null
|
|
|
1135 * A fixed point delta expression must be a simple expression
|
|
|
1136 * Restrictions on where renaming declarations may be placed
|
|
|
1137 * Externals of mode 'out' cannot be referenced
|
|
|
1138 * Externals of mode 'in' cannot be updated
|
|
|
1139 * Loop with no iteration scheme or exits only allowed as last statement in main program or task
|
|
|
1140 * Subprogram cannot have parent unit name
|
|
|
1141 * SPARK 2005 inherited subprogram must be prefixed with overriding
|
|
|
1142 * External variables (or functions that reference them) may not be passed as actual parameters
|
|
|
1143 * Globals must be explicitly mentioned in contract
|
|
|
1144 * Deferred constants cannot be completed by pragma Import
|
|
|
1145 * Package initialization cannot read/write variables from other packages
|
|
|
1146 * Prefix not allowed for entities that are directly visible
|
|
|
1147 * Identifier declaration can't override inherited package name
|
|
|
1148 * Cannot use Standard or other predefined packages as identifiers
|
|
|
1149 * After renaming, cannot use the original name
|
|
|
1150 * Subprograms can only be renamed to remove package prefix
|
|
|
1151 * Pragma import must be immediately after entity it names
|
|
|
1152 * No mutual recursion between multiple units (this can be checked with gnatcheck)
|
|
|
1153
|
|
131
|
1154 Note that if a unit is compiled in Ada 95 mode with the SPARK 2005 restriction,
|
|
111
|
1155 violations will be reported for constructs forbidden in SPARK 95,
|
|
|
1156 instead of SPARK 2005.
|
