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