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