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