1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
|
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S E M _ P R A G --
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2024, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
-- for more details. You should have received a copy of the GNU General --
-- Public License distributed with GNAT; see file COPYING3. If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
-- Pragma handling is isolated in a separate package
-- (logically this processing belongs in chapter 4)
with Namet; use Namet;
with Opt; use Opt;
with Snames; use Snames;
with Types; use Types;
package Sem_Prag is
-- The following table lists all pragmas that emulate an Ada 2012 aspect
Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean :=
(Pragma_Abstract_State => True,
Pragma_All_Calls_Remote => True,
Pragma_Always_Terminates => True,
Pragma_Annotate => True,
Pragma_Async_Readers => True,
Pragma_Async_Writers => True,
Pragma_Asynchronous => True,
Pragma_Atomic => True,
Pragma_Atomic_Components => True,
Pragma_Attach_Handler => True,
Pragma_Constant_After_Elaboration => True,
Pragma_Contract_Cases => True,
Pragma_Convention => True,
Pragma_CPU => True,
Pragma_CUDA_Device => True,
Pragma_CUDA_Global => True,
Pragma_Default_Initial_Condition => True,
Pragma_Default_Storage_Pool => True,
Pragma_Depends => True,
Pragma_Discard_Names => True,
Pragma_Dispatching_Domain => True,
Pragma_Effective_Reads => True,
Pragma_Effective_Writes => True,
Pragma_Elaborate_Body => True,
Pragma_Exceptional_Cases => True,
Pragma_Export => True,
Pragma_Extensions_Visible => True,
Pragma_Favor_Top_Level => True,
Pragma_Ghost => True,
Pragma_Global => True,
Pragma_GNAT_Annotate => True,
Pragma_Import => True,
Pragma_Independent => True,
Pragma_Independent_Components => True,
Pragma_Initial_Condition => True,
Pragma_Initializes => True,
Pragma_Inline => True,
Pragma_Inline_Always => True,
Pragma_Interrupt_Handler => True,
Pragma_Interrupt_Priority => True,
Pragma_Invariant => True,
Pragma_Linker_Section => True,
Pragma_Lock_Free => True,
Pragma_No_Elaboration_Code_All => True,
Pragma_No_Return => True,
Pragma_Obsolescent => True,
Pragma_Pack => True,
Pragma_Part_Of => True,
Pragma_Persistent_BSS => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Predicate => True,
Pragma_Preelaborable_Initialization => True,
Pragma_Preelaborate => True,
Pragma_Priority => True,
Pragma_Pure => True,
Pragma_Pure_Function => True,
Pragma_Refined_Depends => True,
Pragma_Refined_Global => True,
Pragma_Refined_Post => True,
Pragma_Refined_State => True,
Pragma_Relative_Deadline => True,
Pragma_Remote_Access_Type => True,
Pragma_Remote_Call_Interface => True,
Pragma_Remote_Types => True,
Pragma_Secondary_Stack_Size => True,
Pragma_Shared => True,
Pragma_Shared_Passive => True,
Pragma_Simple_Storage_Pool_Type => True,
Pragma_SPARK_Mode => True,
Pragma_Storage_Size => True,
Pragma_Subprogram_Variant => True,
Pragma_Suppress => True,
Pragma_Suppress_Debug_Info => True,
Pragma_Suppress_Initialization => True,
Pragma_Test_Case => True,
Pragma_Thread_Local_Storage => True,
Pragma_Type_Invariant => True,
Pragma_Unchecked_Union => True,
Pragma_Universal_Aliasing => True,
Pragma_Unmodified => True,
Pragma_Unreferenced => True,
Pragma_Unreferenced_Objects => True,
Pragma_Unsuppress => True,
Pragma_Volatile => True,
Pragma_Volatile_Components => True,
Pragma_Volatile_Full_Access => True,
Pragma_Warnings => True,
others => False);
-- The following table lists all pragmas that act as an assertion
-- expression.
Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean :=
(Pragma_Always_Terminates => True,
Pragma_Assert => True,
Pragma_Assert_And_Cut => True,
Pragma_Assume => True,
Pragma_Check => True,
Pragma_Compile_Time_Error => True,
Pragma_Contract_Cases => True,
Pragma_Default_Initial_Condition => True,
Pragma_Exceptional_Cases => True,
Pragma_Initial_Condition => True,
Pragma_Invariant => True,
Pragma_Loop_Invariant => True,
Pragma_Loop_Variant => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Predicate => True,
Pragma_Refined_Post => True,
Pragma_Subprogram_Variant => True,
Pragma_Test_Case => True,
Pragma_Type_Invariant => True,
Pragma_Type_Invariant_Class => True,
others => False);
-- Should to following constant arrays be renamed to better suit their
-- use as a predicate (e.g. Is_Pragma_*) ???
-- The following table lists all the implementation-defined pragmas that
-- should apply to the anonymous object produced by the analysis of a
-- single protected or task type. The table should be synchronized with
-- Aspect_On_Anonymous_Object_OK in unit Aspects.
Pragma_On_Anonymous_Object_OK : constant array (Pragma_Id) of Boolean :=
(Pragma_Depends => True,
Pragma_Global => True,
Pragma_Part_Of => True,
others => False);
-- The following table lists all the implementation-defined pragmas that
-- may apply to a body stub (no language defined pragmas apply). The table
-- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects.
Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
(Pragma_Refined_Depends => True,
Pragma_Refined_Global => True,
Pragma_Refined_Post => True,
Pragma_SPARK_Mode => True,
Pragma_Warnings => True,
others => False);
-- The following table lists all pragmas which are significant in SPARK and
-- as a result get translated into verification conditions. The table is an
-- amalgamation of the pragmas listed in SPARK RM 16.1 and internally added
-- entries.
Pragma_Significant_In_SPARK : constant array (Pragma_Id) of Boolean :=
(Pragma_All_Calls_Remote => False,
Pragma_Asynchronous => False,
Pragma_Default_Storage_Pool => False,
Pragma_Discard_Names => False,
Pragma_Dispatching_Domain => False,
Pragma_Priority_Specific_Dispatching => False,
Pragma_Remote_Call_Interface => False,
Pragma_Remote_Types => False,
Pragma_Shared_Passive => False,
Pragma_Task_Dispatching_Policy => False,
Pragma_Unmodified => False,
Pragma_Unreferenced => False,
Pragma_Warnings => False,
others => True);
-- The following table lists all pragmas which are relevant to the analysis
-- of subprogram bodies.
Pragma_Significant_To_Subprograms : constant array (Pragma_Id) of Boolean :=
(Pragma_Always_Terminates => True,
Pragma_Contract_Cases => True,
Pragma_Depends => True,
Pragma_Exceptional_Cases => True,
Pragma_Ghost => True,
Pragma_Global => True,
Pragma_Inline => True,
Pragma_Inline_Always => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Pure => True,
Pragma_Pure_Function => True,
Pragma_Refined_Depends => True,
Pragma_Refined_Global => True,
Pragma_Refined_Post => True,
Pragma_Refined_State => True,
Pragma_Side_Effects => True,
Pragma_Subprogram_Variant => True,
Pragma_Volatile => True,
Pragma_Volatile_Function => True,
others => False);
-----------------
-- Subprograms --
-----------------
procedure Analyze_Pragma (N : Node_Id);
-- Analyze procedure for pragma reference node N
procedure Analyze_Pragmas_If_Present (Decl : Node_Id; Id : Pragma_Id);
-- Inspect the list of pragmas after declaration Decl and look for a pragma
-- that matches Id. If found, analyze the pragma.
procedure Analyze_Always_Terminates_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Always_Terminates. Freeze_Id is
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Contract_Cases_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Contract_Cases. Freeze_Id is the
-- entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Depends_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Depends. This routine is also
-- capable of performing basic analysis of pragma Refined_Depends.
procedure Analyze_Exceptional_Cases_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Exceptional_Cases. Freeze_Id is
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_External_Property_In_Decl_Part
(N : Node_Id;
Expr_Val : out Boolean);
-- Perform full analysis of delayed pragmas Async_Readers, Async_Writers,
-- Effective_Reads, Effective_Writes and No_Caching. Flag Expr_Val contains
-- the Boolean argument of the pragma or a default True if no argument
-- is present.
procedure Analyze_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Global. This routine is also
-- capable of performing basic analysis of pragma Refined_Global.
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initial_Condition
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initializes
procedure Analyze_Part_Of_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Part_Of. Freeze_Id is the entity
-- of [generic] package body or [generic] subprogram body which caused the
-- "freezing" of the related contract where the pragma resides.
procedure Analyze_Pre_Post_Condition_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of pragmas Precondition and Postcondition.
-- Freeze_Id denotes the entity of [generic] package body or [generic]
-- subprogram body which caused "freezing" of the related contract where
-- the pragma resides.
procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
-- Preform full analysis of delayed pragma Refined_Depends. This routine
-- uses Analyze_Depends_In_Decl_Part as a starting point, then performs
-- various consistency checks between Depends and Refined_Depends.
procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Refined_Global. This routine
-- uses Analyze_Global_In_Decl_Part as a starting point, then performs
-- various consistency checks between Global and Refined_Global.
procedure Analyze_Refined_State_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Refined_State. Freeze_Id denotes
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Subprogram_Variant_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Subprogram_Variant. Freeze_Id is
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
-- Perform preanalysis of pragma Test_Case
function Build_Pragma_Check_Equivalent
(Prag : Node_Id;
Subp_Id : Entity_Id := Empty;
Inher_Id : Entity_Id := Empty;
Keep_Pragma_Id : Boolean := False) return Node_Id;
-- Transform a pre- or [refined] postcondition denoted by Prag into an
-- equivalent pragma Check. When the pre- or postcondition is inherited,
-- the routine replaces the references of all formals of Inher_Id
-- and primitive operations of its controlling type by references
-- to the corresponding entities of Subp_Id and the descendant type.
-- Keep_Pragma_Id is True when the newly created pragma should be
-- in fact of the same kind as the source pragma Prag. This is used
-- in GNATprove_Mode to generate the inherited pre- and postconditions.
procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
-- the name of the aspect or pragma is not one of those recognized as
-- an assertion kind by an Assertion_Policy pragma, then the call has
-- no effect. Note that in the case of a pragma derived from an aspect,
-- the name we use for the purpose of this procedure is the aspect name,
-- which may be different from the pragma name (e.g. Precondition for
-- Pre aspect). In addition, 'Class aspects are recognized (and the
-- corresponding special names used in the processing).
--
-- If the name is a valid assertion kind name, then the Check_Policy pragma
-- chain is checked for a matching entry (or for an Assertion entry which
-- matches all possibilities). If a matching entry is found then the policy
-- is checked. If it is On or Check, then the Is_Checked flag is set in
-- the aspect or pragma node. If it is Off, Ignore, or Disable, then the
-- Is_Ignored flag is set in the aspect or pragma node. Additionally for
-- policy Disable, the Is_Disabled flag is set.
--
-- If no matching Check_Policy pragma is found then the effect depends on
-- whether -gnata was used, if so, then the call has no effect, otherwise
-- Is_Ignored (but not Is_Disabled) is set True.
procedure Check_External_Properties
(Item : Node_Id;
AR : Boolean;
AW : Boolean;
ER : Boolean;
EW : Boolean);
-- Flags AR, AW, ER and EW denote the static values of external properties
-- Async_Readers, Async_Writers, Effective_Reads and Effective_Writes. Item
-- is the related variable or state. Ensure legality of the combination and
-- issue an error for an illegal combination.
function Check_Kind (Nam : Name_Id) return Name_Id;
-- This function is used in connection with pragmas Assert, Check,
-- and assertion aspects and pragmas, to determine if Check pragmas
-- (or corresponding assertion aspects or pragmas) are currently active
-- as determined by the presence of -gnata on the command line (which
-- sets the default), and the appearance of pragmas Check_Policy and
-- Assertion_Policy as configuration pragmas either in a configuration
-- pragma file, or at the start of the current unit, or locally given
-- Check_Policy and Assertion_Policy pragmas that are currently active.
--
-- The value returned is one of the names Check, Ignore, Disable (On
-- returns Check, and Off returns Ignore).
--
-- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
-- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
-- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
-- _Post, _Invariant, or _Type_Invariant, which are special names used
-- in identifiers to represent these attribute references.
procedure Check_Missing_Part_Of (Item_Id : Entity_Id);
-- Determine whether the placement within the state space of an abstract
-- state, variable or package instantiation denoted by Item_Id requires the
-- use of indicator/option Part_Of. If this is the case, emit an error.
procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id);
-- In GNATprove mode, when analyzing an overriding subprogram, check
-- whether the overridden operations have class-wide pre/postconditions,
-- and generate the corresponding pragmas. The pragmas are inserted after
-- the subprogram declaration, together with those generated for other
-- aspects of the subprogram.
procedure Collect_Subprogram_Inputs_Outputs
(Subp_Id : Entity_Id;
Synthesize : Boolean := False;
Subp_Inputs : in out Elist_Id;
Subp_Outputs : in out Elist_Id;
Global_Seen : out Boolean);
-- Subsidiary to the analysis of pragmas Depends, Global, Refined_Depends
-- and Refined_Global. Collect all inputs and outputs of subprogram Subp_Id
-- in lists Subp_Inputs (inputs) and Subp_Outputs (outputs). The inputs and
-- outputs are gathered from:
-- 1) The formal parameters of the subprogram
-- 2) The generic formal parameters of the generic subprogram
-- 3) The current instance of a concurrent type
-- 4) The items of pragma [Refined_]Global
-- or
-- 5) The items of pragma [Refined_]Depends if there is no pragma
-- [Refined_]Global present and flag Synthesize is set to True.
-- If the subprogram has no inputs and/or outputs, then the returned list
-- is No_Elist. Flag Global_Seen is set when the related subprogram has
-- pragma [Refined_]Global.
function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean;
-- N is a pragma appearing in a configuration pragma file. Most such
-- pragmas are analyzed when the file is read, before parsing and analyzing
-- the main unit. However, the analysis of certain pragmas results in
-- adding information to the compiled main unit, and this cannot be done
-- till the main unit is processed. Such pragmas return True from this
-- function and in Frontend pragmas where Delay_Config_Pragma_Analyze is
-- True have their analysis delayed until after the main program is parsed
-- and analyzed.
function Find_Related_Package_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas
-- Abstract_State
-- Initial_Condition
-- Initializes
-- Refined_State
-- Find the declaration of the related package [body] subject to pragma
-- Prag. The return value is either N_Package_Declaration, N_Package_Body,
-- or Empty if the placement of the pragma is illegal. If flag Do_Checks is
-- set, the routine reports duplicate pragmas.
function Find_Related_Declaration_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas
-- Always_Terminates
-- Contract_Cases
-- Depends
-- Exceptional_Cases
-- Extensions_Visible
-- Global
-- Initializes
-- Max_Entry_Queue_Length
-- Max_Queue_Length
-- Post
-- Post_Class
-- Postcondition
-- Pre
-- Pre_Class
-- Precondition
-- Refined_Depends
-- Refined_Global
-- Refined_Post
-- Refined_State
-- Side_Effects
-- Subprogram_Variant
-- Test_Case
-- Volatile_Function
-- as well as attributes 'Old and 'Result. Find the declaration of the
-- related entry, subprogram or task type [body] subject to pragma Prag.
-- If flag Do_Checks is set, the routine reports duplicate pragmas and
-- detects improper use of refinement pragmas in stand alone expression
-- functions.
function Get_Argument
(Prag : Node_Id;
Context_Id : Entity_Id := Empty) return Node_Id;
-- Obtain the argument of pragma Prag depending on context and the nature
-- of the pragma. The argument is extracted in the following manner:
--
-- When the pragma is generated from an aspect, return the corresponding
-- aspect when Context_Id denotes a generic unit.
--
-- Otherwise return the first argument of Prag
--
-- Context denotes the entity of the function, package or procedure where
-- Prag resides.
function Get_SPARK_Mode_From_Annotation
(N : Node_Id) return SPARK_Mode_Type;
-- Given an aspect or pragma SPARK_Mode node, return corresponding mode id
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called
-- before analyzing each new main source program.
function Is_Config_Static_String (Arg : Node_Id) return Boolean;
-- This is called for a configuration pragma that requires either string
-- literal or a concatenation of string literals. We cannot use normal
-- static string processing because it is too early in the case of the
-- pragma appearing in a configuration pragmas file. If Arg is of an
-- appropriate form, then this call obtains the string (doing any necessary
-- concatenations) and places it in Name_Buffer, setting Name_Len to its
-- length, and then returns True. If it is not of the correct form, then an
-- appropriate error message is posted, and False is returned.
function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean;
-- Determine whether pragma SPARK_Mode appears in the statement part of a
-- package body.
function Is_Enabled_Pragma (Prag : Node_Id) return Boolean;
-- Determine whether a Boolean-like SPARK pragma Prag is enabled. To be
-- considered enabled, the pragma must either:
-- * Appear without its Boolean expression
-- * The Boolean expression evaluates to "True"
--
-- Boolean-like SPARK pragmas differ from pure Boolean Ada pragmas in that
-- their optional Boolean expression must be static and cannot benefit from
-- forward references. The following are Boolean-like SPARK pragmas:
-- Async_Readers
-- Async_Writers
-- Constant_After_Elaboration
-- Effective_Reads
-- Effective_Writes
-- Extensions_Visible
-- Volatile_Function
function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
-- The node N is a node for an entity and the issue is whether the
-- occurrence is a reference for the purposes of giving warnings about
-- unreferenced variables. This function returns True if the reference is
-- not a reference from this point of view (e.g. the occurrence in a pragma
-- Pack) and False if it is a real reference (e.g. the occurrence in a
-- pragma Export);
function Is_Pragma_String_Literal (Par : Node_Id) return Boolean;
-- Given an N_Pragma_Argument_Association node, Par, which has the form of
-- an operator symbol, determines whether or not it should be treated as an
-- string literal. This is called by Sem_Ch6.Analyze_Operator_Symbol. If
-- True is returned, the argument is converted to a string literal. If
-- False is returned, then the argument is treated as an entity reference
-- to the operator.
function Is_Private_SPARK_Mode (N : Node_Id) return Boolean;
-- Determine whether pragma SPARK_Mode appears in the private part of a
-- package.
function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
-- Returns True if Nam is one of the names recognized as a valid assertion
-- kind by the Assertion_Policy pragma. Note that the 'Class cases are
-- represented by the corresponding special names Name_uPre, Name_uPost,
-- Name_uInvariant, and Name_uType_Invariant (_Pre, _Post, _Invariant,
-- and _Type_Invariant).
procedure Process_Compilation_Unit_Pragmas (N : Node_Id);
-- Called at the start of processing compilation unit N to deal with any
-- special issues regarding pragmas. In particular, we have to deal with
-- Suppress_All at this stage, since it can appear after the unit instead
-- of before (actually we allow it to appear anywhere).
procedure Relocate_Pragmas_To_Anonymous_Object
(Typ_Decl : Node_Id;
Obj_Decl : Node_Id);
-- Relocate all pragmas that appear in the visible declarations of task or
-- protected type declaration Typ_Decl after the declaration of anonymous
-- object Obj_Decl. Table Pragmas_On_Anonymous_Object_OK contains the list
-- of candidate pragmas.
procedure Relocate_Pragmas_To_Body
(Subp_Body : Node_Id;
Target_Body : Node_Id := Empty);
-- Resocate all pragmas that follow and apply to subprogram body Subp_Body
-- to its own declaration list. Candidate pragmas are classified in table
-- Pragma_On_Body_Or_Stub_OK. If Target_Body is set, the pragma are moved
-- to the declarations of Target_Body. This formal should be set when
-- dealing with subprogram body stubs or expression functions.
procedure Set_Encoded_Interface_Name (E : Entity_Id; S : Node_Id);
-- This routine is used to set an encoded interface name. The node S is
-- an N_String_Literal node for the external name to be set, and E is an
-- entity whose Interface_Name field is to be set. In the normal case where
-- S contains a name that is a valid C identifier, then S is simply set as
-- the value of the Interface_Name. Otherwise it is encoded as needed by
-- particular operating systems. See the body for details of the encoding.
procedure Set_Overflow_Mode (N : Node_Id);
-- Sets Sem.Scope_Suppress according to the overflow modes specified in
-- the pragma Overflow_Mode passed in argument. This should only be called
-- after N has been successfully analyzed.
function Test_Case_Arg
(Prag : Node_Id;
Arg_Nam : Name_Id;
From_Aspect : Boolean := False) return Node_Id;
-- Obtain argument "Name", "Mode", "Ensures" or "Requires" from Test_Case
-- pragma Prag as denoted by Arg_Nam. When From_Aspect is set, an attempt
-- is made to retrieve the argument from the corresponding aspect if there
-- is one. The returned argument has several formats:
--
-- N_Pragma_Argument_Association if retrieved directly from the pragma
--
-- N_Component_Association if retrieved from the corresponding aspect and
-- the argument appears in a named association form.
--
-- An arbitrary expression if retrieved from the corresponding aspect and
-- the argument appears in positional form.
--
-- Empty if there is no such argument
procedure Validate_Compile_Time_Warning_Errors;
-- This routine is called after calling the back end to validate pragmas
-- Compile_Time_Error and Compile_Time_Warning for size and alignment
-- appropriateness. The reason it is called that late is to take advantage
-- of any back-annotation of size and alignment performed by the back end.
end Sem_Prag;
|