]>
Commit | Line | Data |
---|---|---|
879ac954 AC |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
5 | -- C O N T R A C T S -- | |
6 | -- -- | |
7 | -- B o d y -- | |
8 | -- -- | |
884f97cc | 9 | -- Copyright (C) 2015-2017, Free Software Foundation, Inc. -- |
879ac954 AC |
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- -- | |
13 | -- ware Foundation; either version 3, or (at your option) any later ver- -- | |
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 -- | |
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. -- | |
20 | -- -- | |
21 | -- GNAT was originally developed by the GNAT team at New York University. -- | |
22 | -- Extensive contributions were provided by Ada Core Technologies Inc. -- | |
23 | -- -- | |
24 | ------------------------------------------------------------------------------ | |
25 | ||
26 | with Aspects; use Aspects; | |
27 | with Atree; use Atree; | |
5f325af2 | 28 | with Debug; use Debug; |
879ac954 AC |
29 | with Einfo; use Einfo; |
30 | with Elists; use Elists; | |
31 | with Errout; use Errout; | |
32 | with Exp_Prag; use Exp_Prag; | |
33 | with Exp_Tss; use Exp_Tss; | |
34 | with Exp_Util; use Exp_Util; | |
35 | with Namet; use Namet; | |
36 | with Nlists; use Nlists; | |
37 | with Nmake; use Nmake; | |
38 | with Opt; use Opt; | |
39 | with Sem; use Sem; | |
40 | with Sem_Aux; use Sem_Aux; | |
41 | with Sem_Ch6; use Sem_Ch6; | |
42 | with Sem_Ch8; use Sem_Ch8; | |
43 | with Sem_Ch12; use Sem_Ch12; | |
05662a06 | 44 | with Sem_Ch13; use Sem_Ch13; |
879ac954 AC |
45 | with Sem_Disp; use Sem_Disp; |
46 | with Sem_Prag; use Sem_Prag; | |
47 | with Sem_Util; use Sem_Util; | |
48 | with Sinfo; use Sinfo; | |
49 | with Snames; use Snames; | |
50 | with Stringt; use Stringt; | |
5f325af2 | 51 | with SCIL_LL; use SCIL_LL; |
879ac954 AC |
52 | with Tbuild; use Tbuild; |
53 | ||
54 | package body Contracts is | |
55 | ||
e645cb39 AC |
56 | procedure Analyze_Contracts |
57 | (L : List_Id; | |
58 | Freeze_Nod : Node_Id; | |
59 | Freeze_Id : Entity_Id); | |
60 | -- Subsidiary to the one parameter version of Analyze_Contracts and routine | |
61 | -- Analyze_Previous_Constracts. Analyze the contracts of all constructs in | |
62 | -- the list L. If Freeze_Nod is set, then the analysis stops when the node | |
63 | -- is reached. Freeze_Id is the entity of some related context which caused | |
4404c282 | 64 | -- freezing up to node Freeze_Nod. |
e645cb39 | 65 | |
82e5c243 AC |
66 | procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id); |
67 | -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the | |
68 | -- contract-only subprogram body of eligible subprograms found in L, adds | |
69 | -- them to their corresponding list of declarations, and analyzes them. | |
70 | ||
879ac954 AC |
71 | procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); |
72 | -- Expand the contracts of a subprogram body and its correspoding spec (if | |
73 | -- any). This routine processes all [refined] pre- and postconditions as | |
74 | -- well as Contract_Cases, invariants and predicates. Body_Id denotes the | |
75 | -- entity of the subprogram body. | |
76 | ||
77 | ----------------------- | |
78 | -- Add_Contract_Item -- | |
79 | ----------------------- | |
80 | ||
81 | procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is | |
82 | Items : Node_Id := Contract (Id); | |
83 | ||
84 | procedure Add_Classification; | |
85 | -- Prepend Prag to the list of classifications | |
86 | ||
87 | procedure Add_Contract_Test_Case; | |
88 | -- Prepend Prag to the list of contract and test cases | |
89 | ||
90 | procedure Add_Pre_Post_Condition; | |
91 | -- Prepend Prag to the list of pre- and postconditions | |
92 | ||
93 | ------------------------ | |
94 | -- Add_Classification -- | |
95 | ------------------------ | |
96 | ||
97 | procedure Add_Classification is | |
98 | begin | |
99 | Set_Next_Pragma (Prag, Classifications (Items)); | |
100 | Set_Classifications (Items, Prag); | |
101 | end Add_Classification; | |
102 | ||
103 | ---------------------------- | |
104 | -- Add_Contract_Test_Case -- | |
105 | ---------------------------- | |
106 | ||
107 | procedure Add_Contract_Test_Case is | |
108 | begin | |
109 | Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); | |
110 | Set_Contract_Test_Cases (Items, Prag); | |
111 | end Add_Contract_Test_Case; | |
112 | ||
113 | ---------------------------- | |
114 | -- Add_Pre_Post_Condition -- | |
115 | ---------------------------- | |
116 | ||
117 | procedure Add_Pre_Post_Condition is | |
118 | begin | |
119 | Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); | |
120 | Set_Pre_Post_Conditions (Items, Prag); | |
121 | end Add_Pre_Post_Condition; | |
122 | ||
123 | -- Local variables | |
124 | ||
879ac954 AC |
125 | -- A contract must contain only pragmas |
126 | ||
127 | pragma Assert (Nkind (Prag) = N_Pragma); | |
6e759c2a | 128 | Prag_Nam : constant Name_Id := Pragma_Name (Prag); |
533e3abc BD |
129 | |
130 | -- Start of processing for Add_Contract_Item | |
879ac954 | 131 | |
533e3abc | 132 | begin |
879ac954 AC |
133 | -- Create a new contract when adding the first item |
134 | ||
135 | if No (Items) then | |
136 | Items := Make_Contract (Sloc (Id)); | |
137 | Set_Contract (Id, Items); | |
138 | end if; | |
139 | ||
f99ff327 | 140 | -- Constants, the applicable pragmas are: |
879ac954 AC |
141 | -- Part_Of |
142 | ||
143 | if Ekind (Id) = E_Constant then | |
144 | if Prag_Nam = Name_Part_Of then | |
145 | Add_Classification; | |
146 | ||
147 | -- The pragma is not a proper contract item | |
148 | ||
149 | else | |
150 | raise Program_Error; | |
151 | end if; | |
152 | ||
f99ff327 AC |
153 | -- Entry bodies, the applicable pragmas are: |
154 | -- Refined_Depends | |
155 | -- Refined_Global | |
156 | -- Refined_Post | |
879ac954 | 157 | |
f99ff327 AC |
158 | elsif Is_Entry_Body (Id) then |
159 | if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then | |
879ac954 AC |
160 | Add_Classification; |
161 | ||
f99ff327 AC |
162 | elsif Prag_Nam = Name_Refined_Post then |
163 | Add_Pre_Post_Condition; | |
879ac954 AC |
164 | |
165 | -- The pragma is not a proper contract item | |
166 | ||
167 | else | |
168 | raise Program_Error; | |
169 | end if; | |
170 | ||
f99ff327 | 171 | -- Entry or subprogram declarations, the applicable pragmas are: |
c0dd5b38 | 172 | -- Attach_Handler |
879ac954 AC |
173 | -- Contract_Cases |
174 | -- Depends | |
175 | -- Extensions_Visible | |
176 | -- Global | |
c0dd5b38 | 177 | -- Interrupt_Handler |
879ac954 AC |
178 | -- Postcondition |
179 | -- Precondition | |
180 | -- Test_Case | |
181 | -- Volatile_Function | |
182 | ||
f99ff327 AC |
183 | elsif Is_Entry_Declaration (Id) |
184 | or else Ekind_In (Id, E_Function, | |
185 | E_Generic_Function, | |
186 | E_Generic_Procedure, | |
187 | E_Procedure) | |
879ac954 | 188 | then |
c0dd5b38 AC |
189 | if Nam_In (Prag_Nam, Name_Attach_Handler, Name_Interrupt_Handler) |
190 | and then Ekind_In (Id, E_Generic_Procedure, E_Procedure) | |
191 | then | |
192 | Add_Classification; | |
879ac954 AC |
193 | |
194 | elsif Nam_In (Prag_Nam, Name_Depends, | |
195 | Name_Extensions_Visible, | |
196 | Name_Global) | |
197 | then | |
198 | Add_Classification; | |
199 | ||
200 | elsif Prag_Nam = Name_Volatile_Function | |
201 | and then Ekind_In (Id, E_Function, E_Generic_Function) | |
202 | then | |
203 | Add_Classification; | |
204 | ||
c0dd5b38 AC |
205 | elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then |
206 | Add_Contract_Test_Case; | |
207 | ||
208 | elsif Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then | |
209 | Add_Pre_Post_Condition; | |
210 | ||
879ac954 AC |
211 | -- The pragma is not a proper contract item |
212 | ||
213 | else | |
214 | raise Program_Error; | |
215 | end if; | |
216 | ||
f99ff327 AC |
217 | -- Packages or instantiations, the applicable pragmas are: |
218 | -- Abstract_States | |
219 | -- Initial_Condition | |
220 | -- Initializes | |
221 | -- Part_Of (instantiation only) | |
222 | ||
223 | elsif Ekind_In (Id, E_Generic_Package, E_Package) then | |
224 | if Nam_In (Prag_Nam, Name_Abstract_State, | |
225 | Name_Initial_Condition, | |
226 | Name_Initializes) | |
227 | then | |
228 | Add_Classification; | |
229 | ||
230 | -- Indicator Part_Of must be associated with a package instantiation | |
231 | ||
232 | elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then | |
233 | Add_Classification; | |
234 | ||
235 | -- The pragma is not a proper contract item | |
236 | ||
237 | else | |
238 | raise Program_Error; | |
239 | end if; | |
240 | ||
241 | -- Package bodies, the applicable pragmas are: | |
242 | -- Refined_States | |
243 | ||
244 | elsif Ekind (Id) = E_Package_Body then | |
245 | if Prag_Nam = Name_Refined_State then | |
246 | Add_Classification; | |
247 | ||
248 | -- The pragma is not a proper contract item | |
249 | ||
250 | else | |
251 | raise Program_Error; | |
252 | end if; | |
253 | ||
75b87c16 AC |
254 | -- Protected units, the applicable pragmas are: |
255 | -- Part_Of | |
256 | ||
257 | elsif Ekind (Id) = E_Protected_Type then | |
258 | if Prag_Nam = Name_Part_Of then | |
259 | Add_Classification; | |
260 | ||
261 | -- The pragma is not a proper contract item | |
262 | ||
263 | else | |
264 | raise Program_Error; | |
265 | end if; | |
266 | ||
f99ff327 | 267 | -- Subprogram bodies, the applicable pragmas are: |
879ac954 AC |
268 | -- Postcondition |
269 | -- Precondition | |
270 | -- Refined_Depends | |
271 | -- Refined_Global | |
272 | -- Refined_Post | |
273 | ||
274 | elsif Ekind (Id) = E_Subprogram_Body then | |
275 | if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then | |
276 | Add_Classification; | |
277 | ||
278 | elsif Nam_In (Prag_Nam, Name_Postcondition, | |
279 | Name_Precondition, | |
280 | Name_Refined_Post) | |
281 | then | |
282 | Add_Pre_Post_Condition; | |
283 | ||
284 | -- The pragma is not a proper contract item | |
285 | ||
286 | else | |
287 | raise Program_Error; | |
288 | end if; | |
289 | ||
f99ff327 AC |
290 | -- Task bodies, the applicable pragmas are: |
291 | -- Refined_Depends | |
292 | -- Refined_Global | |
293 | ||
294 | elsif Ekind (Id) = E_Task_Body then | |
295 | if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then | |
296 | Add_Classification; | |
297 | ||
298 | -- The pragma is not a proper contract item | |
299 | ||
300 | else | |
301 | raise Program_Error; | |
302 | end if; | |
303 | ||
304 | -- Task units, the applicable pragmas are: | |
305 | -- Depends | |
306 | -- Global | |
75b87c16 | 307 | -- Part_Of |
f99ff327 AC |
308 | |
309 | elsif Ekind (Id) = E_Task_Type then | |
75b87c16 | 310 | if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then |
f99ff327 AC |
311 | Add_Classification; |
312 | ||
313 | -- The pragma is not a proper contract item | |
314 | ||
315 | else | |
316 | raise Program_Error; | |
317 | end if; | |
318 | ||
319 | -- Variables, the applicable pragmas are: | |
879ac954 AC |
320 | -- Async_Readers |
321 | -- Async_Writers | |
322 | -- Constant_After_Elaboration | |
75b87c16 | 323 | -- Depends |
879ac954 AC |
324 | -- Effective_Reads |
325 | -- Effective_Writes | |
75b87c16 | 326 | -- Global |
879ac954 AC |
327 | -- Part_Of |
328 | ||
329 | elsif Ekind (Id) = E_Variable then | |
330 | if Nam_In (Prag_Nam, Name_Async_Readers, | |
331 | Name_Async_Writers, | |
332 | Name_Constant_After_Elaboration, | |
75b87c16 | 333 | Name_Depends, |
879ac954 AC |
334 | Name_Effective_Reads, |
335 | Name_Effective_Writes, | |
75b87c16 | 336 | Name_Global, |
879ac954 AC |
337 | Name_Part_Of) |
338 | then | |
339 | Add_Classification; | |
340 | ||
341 | -- The pragma is not a proper contract item | |
342 | ||
343 | else | |
344 | raise Program_Error; | |
345 | end if; | |
346 | end if; | |
347 | end Add_Contract_Item; | |
348 | ||
e645cb39 AC |
349 | ----------------------- |
350 | -- Analyze_Contracts -- | |
351 | ----------------------- | |
352 | ||
353 | procedure Analyze_Contracts (L : List_Id) is | |
354 | begin | |
5f325af2 AC |
355 | if CodePeer_Mode and then Debug_Flag_Dot_KK then |
356 | Build_And_Analyze_Contract_Only_Subprograms (L); | |
357 | end if; | |
358 | ||
e645cb39 AC |
359 | Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty); |
360 | end Analyze_Contracts; | |
879ac954 | 361 | |
e645cb39 AC |
362 | procedure Analyze_Contracts |
363 | (L : List_Id; | |
364 | Freeze_Nod : Node_Id; | |
365 | Freeze_Id : Entity_Id) | |
366 | is | |
367 | Decl : Node_Id; | |
879ac954 AC |
368 | |
369 | begin | |
e645cb39 AC |
370 | Decl := First (L); |
371 | while Present (Decl) loop | |
879ac954 | 372 | |
e645cb39 AC |
373 | -- The caller requests that the traversal stops at a particular node |
374 | -- that causes contract "freezing". | |
879ac954 | 375 | |
e645cb39 AC |
376 | if Present (Freeze_Nod) and then Decl = Freeze_Nod then |
377 | exit; | |
879ac954 AC |
378 | end if; |
379 | ||
e645cb39 AC |
380 | -- Entry or subprogram declarations |
381 | ||
382 | if Nkind_In (Decl, N_Abstract_Subprogram_Declaration, | |
383 | N_Entry_Declaration, | |
384 | N_Generic_Subprogram_Declaration, | |
385 | N_Subprogram_Declaration) | |
386 | then | |
387 | Analyze_Entry_Or_Subprogram_Contract | |
388 | (Subp_Id => Defining_Entity (Decl), | |
389 | Freeze_Id => Freeze_Id); | |
390 | ||
391 | -- Entry or subprogram bodies | |
392 | ||
393 | elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then | |
394 | Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl)); | |
395 | ||
396 | -- Objects | |
397 | ||
398 | elsif Nkind (Decl) = N_Object_Declaration then | |
399 | Analyze_Object_Contract | |
400 | (Obj_Id => Defining_Entity (Decl), | |
401 | Freeze_Id => Freeze_Id); | |
402 | ||
5f325af2 | 403 | -- Protected units |
e645cb39 AC |
404 | |
405 | elsif Nkind_In (Decl, N_Protected_Type_Declaration, | |
406 | N_Single_Protected_Declaration) | |
407 | then | |
408 | Analyze_Protected_Contract (Defining_Entity (Decl)); | |
409 | ||
410 | -- Subprogram body stubs | |
411 | ||
412 | elsif Nkind (Decl) = N_Subprogram_Body_Stub then | |
413 | Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); | |
414 | ||
415 | -- Task units | |
416 | ||
417 | elsif Nkind_In (Decl, N_Single_Task_Declaration, | |
418 | N_Task_Type_Declaration) | |
419 | then | |
420 | Analyze_Task_Contract (Defining_Entity (Decl)); | |
05662a06 ES |
421 | |
422 | -- For type declarations, we need to do the pre-analysis of | |
423 | -- Iterable aspect specifications. | |
424 | -- Other type aspects need to be resolved here??? | |
425 | ||
426 | elsif Nkind (Decl) = N_Private_Type_Declaration | |
427 | and then Present (Aspect_Specifications (Decl)) | |
428 | then | |
429 | declare | |
430 | E : constant Entity_Id := Defining_Identifier (Decl); | |
431 | It : constant Node_Id := Find_Aspect (E, Aspect_Iterable); | |
432 | begin | |
433 | if Present (It) then | |
434 | Validate_Iterable_Aspect (E, It); | |
435 | end if; | |
436 | end; | |
e645cb39 AC |
437 | end if; |
438 | ||
439 | Next (Decl); | |
879ac954 | 440 | end loop; |
e645cb39 | 441 | end Analyze_Contracts; |
879ac954 | 442 | |
f99ff327 AC |
443 | ----------------------------------------------- |
444 | -- Analyze_Entry_Or_Subprogram_Body_Contract -- | |
445 | ----------------------------------------------- | |
446 | ||
447 | procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is | |
448 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
449 | Items : constant Node_Id := Contract (Body_Id); | |
450 | Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); | |
451 | Mode : SPARK_Mode_Type; | |
452 | ||
453 | begin | |
454 | -- When a subprogram body declaration is illegal, its defining entity is | |
455 | -- left unanalyzed. There is nothing left to do in this case because the | |
456 | -- body lacks a contract, or even a proper Ekind. | |
457 | ||
458 | if Ekind (Body_Id) = E_Void then | |
459 | return; | |
460 | ||
f99ff327 AC |
461 | -- Do not analyze a contract multiple times |
462 | ||
463 | elsif Present (Items) then | |
464 | if Analyzed (Items) then | |
465 | return; | |
466 | else | |
467 | Set_Analyzed (Items); | |
468 | end if; | |
469 | end if; | |
470 | ||
471 | -- Due to the timing of contract analysis, delayed pragmas may be | |
472 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
473 | -- context. To remedy this, restore the original SPARK_Mode of the | |
474 | -- related subprogram body. | |
475 | ||
476 | Save_SPARK_Mode_And_Set (Body_Id, Mode); | |
477 | ||
478 | -- Ensure that the contract cases or postconditions mention 'Result or | |
479 | -- define a post-state. | |
480 | ||
481 | Check_Result_And_Post_State (Body_Id); | |
482 | ||
483 | -- A stand-alone nonvolatile function body cannot have an effectively | |
484 | -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This | |
485 | -- check is relevant only when SPARK_Mode is on, as it is not a standard | |
486 | -- legality rule. The check is performed here because Volatile_Function | |
332429c8 AC |
487 | -- is processed after the analysis of the related subprogram body. The |
488 | -- check only applies to source subprograms and not to generated TSS | |
489 | -- subprograms. | |
f99ff327 AC |
490 | |
491 | if SPARK_Mode = On | |
492 | and then Ekind_In (Body_Id, E_Function, E_Generic_Function) | |
332429c8 | 493 | and then Comes_From_Source (Spec_Id) |
f99ff327 AC |
494 | and then not Is_Volatile_Function (Body_Id) |
495 | then | |
496 | Check_Nonvolatile_Function_Profile (Body_Id); | |
497 | end if; | |
498 | ||
499 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
500 | -- pragmas have been analyzed. | |
501 | ||
502 | Restore_SPARK_Mode (Mode); | |
503 | ||
504 | -- Capture all global references in a generic subprogram body now that | |
505 | -- the contract has been analyzed. | |
506 | ||
507 | if Is_Generic_Declaration_Or_Body (Body_Decl) then | |
508 | Save_Global_References_In_Contract | |
509 | (Templ => Original_Node (Body_Decl), | |
510 | Gen_Id => Spec_Id); | |
511 | end if; | |
512 | ||
513 | -- Deal with preconditions, [refined] postconditions, Contract_Cases, | |
514 | -- invariants and predicates associated with body and its spec. Do not | |
515 | -- expand the contract of subprogram body stubs. | |
516 | ||
517 | if Nkind (Body_Decl) = N_Subprogram_Body then | |
518 | Expand_Subprogram_Contract (Body_Id); | |
519 | end if; | |
520 | end Analyze_Entry_Or_Subprogram_Body_Contract; | |
521 | ||
522 | ------------------------------------------ | |
523 | -- Analyze_Entry_Or_Subprogram_Contract -- | |
524 | ------------------------------------------ | |
525 | ||
e645cb39 AC |
526 | procedure Analyze_Entry_Or_Subprogram_Contract |
527 | (Subp_Id : Entity_Id; | |
528 | Freeze_Id : Entity_Id := Empty) | |
529 | is | |
f99ff327 AC |
530 | Items : constant Node_Id := Contract (Subp_Id); |
531 | Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); | |
8a0183fd HK |
532 | |
533 | Skip_Assert_Exprs : constant Boolean := | |
534 | Ekind_In (Subp_Id, E_Entry, E_Entry_Family) | |
535 | and then not ASIS_Mode | |
536 | and then not GNATprove_Mode; | |
537 | ||
538 | Depends : Node_Id := Empty; | |
539 | Global : Node_Id := Empty; | |
540 | Mode : SPARK_Mode_Type; | |
541 | Prag : Node_Id; | |
542 | Prag_Nam : Name_Id; | |
f99ff327 AC |
543 | |
544 | begin | |
f99ff327 AC |
545 | -- Do not analyze a contract multiple times |
546 | ||
e310115e | 547 | if Present (Items) then |
f99ff327 AC |
548 | if Analyzed (Items) then |
549 | return; | |
550 | else | |
551 | Set_Analyzed (Items); | |
552 | end if; | |
553 | end if; | |
554 | ||
555 | -- Due to the timing of contract analysis, delayed pragmas may be | |
556 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
557 | -- context. To remedy this, restore the original SPARK_Mode of the | |
558 | -- related subprogram body. | |
559 | ||
560 | Save_SPARK_Mode_And_Set (Subp_Id, Mode); | |
561 | ||
562 | -- All subprograms carry a contract, but for some it is not significant | |
563 | -- and should not be processed. | |
564 | ||
565 | if not Has_Significant_Contract (Subp_Id) then | |
566 | null; | |
567 | ||
568 | elsif Present (Items) then | |
569 | ||
e310115e | 570 | -- Do not analyze the pre/postconditions of an entry declaration |
8a0183fd HK |
571 | -- unless annotating the original tree for ASIS or GNATprove. The |
572 | -- real analysis occurs when the pre/postconditons are relocated to | |
573 | -- the contract wrapper procedure (see Build_Contract_Wrapper). | |
f99ff327 | 574 | |
8a0183fd | 575 | if Skip_Assert_Exprs then |
e310115e AC |
576 | null; |
577 | ||
578 | -- Otherwise analyze the pre/postconditions | |
579 | ||
580 | else | |
581 | Prag := Pre_Post_Conditions (Items); | |
582 | while Present (Prag) loop | |
e645cb39 | 583 | Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id); |
e310115e AC |
584 | Prag := Next_Pragma (Prag); |
585 | end loop; | |
586 | end if; | |
f99ff327 AC |
587 | |
588 | -- Analyze contract-cases and test-cases | |
589 | ||
590 | Prag := Contract_Test_Cases (Items); | |
591 | while Present (Prag) loop | |
6e759c2a | 592 | Prag_Nam := Pragma_Name (Prag); |
f99ff327 AC |
593 | |
594 | if Prag_Nam = Name_Contract_Cases then | |
8a0183fd HK |
595 | |
596 | -- Do not analyze the contract cases of an entry declaration | |
597 | -- unless annotating the original tree for ASIS or GNATprove. | |
598 | -- The real analysis occurs when the contract cases are moved | |
599 | -- to the contract wrapper procedure (Build_Contract_Wrapper). | |
600 | ||
601 | if Skip_Assert_Exprs then | |
602 | null; | |
603 | ||
604 | -- Otherwise analyze the contract cases | |
605 | ||
606 | else | |
e645cb39 | 607 | Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id); |
8a0183fd | 608 | end if; |
f99ff327 AC |
609 | else |
610 | pragma Assert (Prag_Nam = Name_Test_Case); | |
611 | Analyze_Test_Case_In_Decl_Part (Prag); | |
612 | end if; | |
613 | ||
614 | Prag := Next_Pragma (Prag); | |
615 | end loop; | |
616 | ||
617 | -- Analyze classification pragmas | |
618 | ||
619 | Prag := Classifications (Items); | |
620 | while Present (Prag) loop | |
6e759c2a | 621 | Prag_Nam := Pragma_Name (Prag); |
f99ff327 AC |
622 | |
623 | if Prag_Nam = Name_Depends then | |
624 | Depends := Prag; | |
625 | ||
626 | elsif Prag_Nam = Name_Global then | |
627 | Global := Prag; | |
628 | end if; | |
629 | ||
630 | Prag := Next_Pragma (Prag); | |
631 | end loop; | |
632 | ||
633 | -- Analyze Global first, as Depends may mention items classified in | |
634 | -- the global categorization. | |
635 | ||
636 | if Present (Global) then | |
637 | Analyze_Global_In_Decl_Part (Global); | |
638 | end if; | |
639 | ||
640 | -- Depends must be analyzed after Global in order to see the modes of | |
641 | -- all global items. | |
642 | ||
643 | if Present (Depends) then | |
644 | Analyze_Depends_In_Decl_Part (Depends); | |
645 | end if; | |
646 | ||
647 | -- Ensure that the contract cases or postconditions mention 'Result | |
648 | -- or define a post-state. | |
649 | ||
650 | Check_Result_And_Post_State (Subp_Id); | |
651 | end if; | |
652 | ||
653 | -- A nonvolatile function cannot have an effectively volatile formal | |
654 | -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant | |
655 | -- only when SPARK_Mode is on, as it is not a standard legality rule. | |
656 | -- The check is performed here because pragma Volatile_Function is | |
657 | -- processed after the analysis of the related subprogram declaration. | |
658 | ||
659 | if SPARK_Mode = On | |
660 | and then Ekind_In (Subp_Id, E_Function, E_Generic_Function) | |
884f97cc | 661 | and then Comes_From_Source (Subp_Id) |
f99ff327 AC |
662 | and then not Is_Volatile_Function (Subp_Id) |
663 | then | |
664 | Check_Nonvolatile_Function_Profile (Subp_Id); | |
665 | end if; | |
666 | ||
667 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
668 | -- pragmas have been analyzed. | |
669 | ||
670 | Restore_SPARK_Mode (Mode); | |
671 | ||
672 | -- Capture all global references in a generic subprogram now that the | |
673 | -- contract has been analyzed. | |
674 | ||
675 | if Is_Generic_Declaration_Or_Body (Subp_Decl) then | |
676 | Save_Global_References_In_Contract | |
677 | (Templ => Original_Node (Subp_Decl), | |
678 | Gen_Id => Subp_Id); | |
679 | end if; | |
680 | end Analyze_Entry_Or_Subprogram_Contract; | |
681 | ||
879ac954 AC |
682 | ----------------------------- |
683 | -- Analyze_Object_Contract -- | |
684 | ----------------------------- | |
685 | ||
e645cb39 AC |
686 | procedure Analyze_Object_Contract |
687 | (Obj_Id : Entity_Id; | |
688 | Freeze_Id : Entity_Id := Empty) | |
689 | is | |
75b87c16 AC |
690 | Obj_Typ : constant Entity_Id := Etype (Obj_Id); |
691 | AR_Val : Boolean := False; | |
692 | AW_Val : Boolean := False; | |
75b87c16 AC |
693 | ER_Val : Boolean := False; |
694 | EW_Val : Boolean := False; | |
695 | Items : Node_Id; | |
696 | Mode : SPARK_Mode_Type; | |
697 | Prag : Node_Id; | |
fdc54be6 | 698 | Ref_Elmt : Elmt_Id; |
75b87c16 AC |
699 | Restore_Mode : Boolean := False; |
700 | Seen : Boolean := False; | |
879ac954 AC |
701 | |
702 | begin | |
703 | -- The loop parameter in an element iterator over a formal container | |
e96b7045 | 704 | -- is declared with an object declaration, but no contracts apply. |
879ac954 AC |
705 | |
706 | if Ekind (Obj_Id) = E_Loop_Parameter then | |
707 | return; | |
708 | end if; | |
709 | ||
e96b7045 | 710 | -- Do not analyze a contract multiple times |
879ac954 AC |
711 | |
712 | Items := Contract (Obj_Id); | |
713 | ||
714 | if Present (Items) then | |
715 | if Analyzed (Items) then | |
716 | return; | |
717 | else | |
718 | Set_Analyzed (Items); | |
719 | end if; | |
720 | end if; | |
721 | ||
58996b09 HK |
722 | -- The anonymous object created for a single concurrent type inherits |
723 | -- the SPARK_Mode from the type. Due to the timing of contract analysis, | |
724 | -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that | |
725 | -- of the enclosing context. To remedy this, restore the original mode | |
726 | -- of the related anonymous object. | |
727 | ||
728 | if Is_Single_Concurrent_Object (Obj_Id) | |
729 | and then Present (SPARK_Pragma (Obj_Id)) | |
730 | then | |
731 | Restore_Mode := True; | |
732 | Save_SPARK_Mode_And_Set (Obj_Id, Mode); | |
733 | end if; | |
734 | ||
e96b7045 | 735 | -- Constant-related checks |
879ac954 AC |
736 | |
737 | if Ekind (Obj_Id) = E_Constant then | |
738 | ||
58996b09 HK |
739 | -- Analyze indicator Part_Of |
740 | ||
741 | Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); | |
742 | ||
743 | -- Check whether the lack of indicator Part_Of agrees with the | |
744 | -- placement of the constant with respect to the state space. | |
745 | ||
746 | if No (Prag) then | |
747 | Check_Missing_Part_Of (Obj_Id); | |
748 | end if; | |
749 | ||
879ac954 | 750 | -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)). |
e96b7045 AC |
751 | -- This check is relevant only when SPARK_Mode is on, as it is not |
752 | -- a standard Ada legality rule. Internally-generated constants that | |
879ac954 AC |
753 | -- map generic formals to actuals in instantiations are allowed to |
754 | -- be volatile. | |
755 | ||
756 | if SPARK_Mode = On | |
757 | and then Comes_From_Source (Obj_Id) | |
758 | and then Is_Effectively_Volatile (Obj_Id) | |
759 | and then No (Corresponding_Generic_Association (Parent (Obj_Id))) | |
760 | then | |
761 | Error_Msg_N ("constant cannot be volatile", Obj_Id); | |
762 | end if; | |
763 | ||
e96b7045 | 764 | -- Variable-related checks |
879ac954 AC |
765 | |
766 | else pragma Assert (Ekind (Obj_Id) = E_Variable); | |
767 | ||
75b87c16 AC |
768 | -- Analyze all external properties |
769 | ||
770 | Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); | |
771 | ||
772 | if Present (Prag) then | |
773 | Analyze_External_Property_In_Decl_Part (Prag, AR_Val); | |
774 | Seen := True; | |
775 | end if; | |
776 | ||
777 | Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); | |
778 | ||
779 | if Present (Prag) then | |
780 | Analyze_External_Property_In_Decl_Part (Prag, AW_Val); | |
781 | Seen := True; | |
782 | end if; | |
783 | ||
784 | Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); | |
785 | ||
786 | if Present (Prag) then | |
787 | Analyze_External_Property_In_Decl_Part (Prag, ER_Val); | |
788 | Seen := True; | |
789 | end if; | |
790 | ||
791 | Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); | |
792 | ||
793 | if Present (Prag) then | |
794 | Analyze_External_Property_In_Decl_Part (Prag, EW_Val); | |
795 | Seen := True; | |
796 | end if; | |
797 | ||
798 | -- Verify the mutual interaction of the various external properties | |
799 | ||
800 | if Seen then | |
801 | Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); | |
802 | end if; | |
803 | ||
804 | -- The anonymous object created for a single concurrent type carries | |
805 | -- pragmas Depends and Globat of the type. | |
806 | ||
807 | if Is_Single_Concurrent_Object (Obj_Id) then | |
808 | ||
809 | -- Analyze Global first, as Depends may mention items classified | |
810 | -- in the global categorization. | |
811 | ||
812 | Prag := Get_Pragma (Obj_Id, Pragma_Global); | |
813 | ||
814 | if Present (Prag) then | |
815 | Analyze_Global_In_Decl_Part (Prag); | |
816 | end if; | |
817 | ||
818 | -- Depends must be analyzed after Global in order to see the modes | |
819 | -- of all global items. | |
820 | ||
821 | Prag := Get_Pragma (Obj_Id, Pragma_Depends); | |
822 | ||
823 | if Present (Prag) then | |
824 | Analyze_Depends_In_Decl_Part (Prag); | |
825 | end if; | |
826 | end if; | |
827 | ||
828 | Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); | |
829 | ||
830 | -- Analyze indicator Part_Of | |
831 | ||
832 | if Present (Prag) then | |
e645cb39 | 833 | Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id); |
75b87c16 | 834 | |
fdc54be6 AC |
835 | -- The variable is a constituent of a single protected/task type |
836 | -- and behaves as a component of the type. Verify that references | |
837 | -- to the variable occur within the definition or body of the type | |
838 | -- (SPARK RM 9.3). | |
839 | ||
840 | if Present (Encapsulating_State (Obj_Id)) | |
841 | and then Is_Single_Concurrent_Object | |
842 | (Encapsulating_State (Obj_Id)) | |
843 | and then Present (Part_Of_References (Obj_Id)) | |
844 | then | |
845 | Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id)); | |
846 | while Present (Ref_Elmt) loop | |
847 | Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt)); | |
848 | Next_Elmt (Ref_Elmt); | |
849 | end loop; | |
850 | end if; | |
851 | ||
75b87c16 AC |
852 | -- Otherwise check whether the lack of indicator Part_Of agrees with |
853 | -- the placement of the variable with respect to the state space. | |
854 | ||
855 | else | |
856 | Check_Missing_Part_Of (Obj_Id); | |
857 | end if; | |
858 | ||
e96b7045 | 859 | -- The following checks are relevant only when SPARK_Mode is on, as |
879ac954 AC |
860 | -- they are not standard Ada legality rules. Internally generated |
861 | -- temporaries are ignored. | |
862 | ||
863 | if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then | |
864 | if Is_Effectively_Volatile (Obj_Id) then | |
865 | ||
866 | -- The declaration of an effectively volatile object must | |
867 | -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). | |
868 | ||
869 | if not Is_Library_Level_Entity (Obj_Id) then | |
870 | Error_Msg_N | |
871 | ("volatile variable & must be declared at library level", | |
872 | Obj_Id); | |
873 | ||
874 | -- An object of a discriminated type cannot be effectively | |
875 | -- volatile except for protected objects (SPARK RM 7.1.3(5)). | |
876 | ||
877 | elsif Has_Discriminants (Obj_Typ) | |
878 | and then not Is_Protected_Type (Obj_Typ) | |
879 | then | |
880 | Error_Msg_N | |
881 | ("discriminated object & cannot be volatile", Obj_Id); | |
879ac954 AC |
882 | end if; |
883 | ||
884 | -- The object is not effectively volatile | |
885 | ||
886 | else | |
887 | -- A non-effectively volatile object cannot have effectively | |
888 | -- volatile components (SPARK RM 7.1.3(6)). | |
889 | ||
890 | if not Is_Effectively_Volatile (Obj_Id) | |
891 | and then Has_Volatile_Component (Obj_Typ) | |
892 | then | |
893 | Error_Msg_N | |
894 | ("non-volatile object & cannot have volatile components", | |
895 | Obj_Id); | |
896 | end if; | |
897 | end if; | |
898 | end if; | |
58996b09 | 899 | end if; |
879ac954 | 900 | |
58996b09 | 901 | -- Common checks |
879ac954 | 902 | |
58996b09 | 903 | if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then |
879ac954 | 904 | |
58996b09 HK |
905 | -- A Ghost object cannot be of a type that yields a synchronized |
906 | -- object (SPARK RM 6.9(19)). | |
879ac954 | 907 | |
58996b09 HK |
908 | if Yields_Synchronized_Object (Obj_Typ) then |
909 | Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id); | |
879ac954 | 910 | |
4179af27 | 911 | -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and |
58996b09 | 912 | -- SPARK RM 6.9(19)). |
879ac954 | 913 | |
58996b09 HK |
914 | elsif Is_Effectively_Volatile (Obj_Id) then |
915 | Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); | |
879ac954 | 916 | |
4179af27 | 917 | -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)). |
58996b09 HK |
918 | -- One exception to this is the object that represents the dispatch |
919 | -- table of a Ghost tagged type, as the symbol needs to be exported. | |
879ac954 | 920 | |
58996b09 | 921 | elsif Is_Exported (Obj_Id) then |
879ac954 AC |
922 | Error_Msg_N ("ghost object & cannot be exported", Obj_Id); |
923 | ||
924 | elsif Is_Imported (Obj_Id) then | |
925 | Error_Msg_N ("ghost object & cannot be imported", Obj_Id); | |
926 | end if; | |
927 | end if; | |
58996b09 HK |
928 | |
929 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
930 | -- pragmas have been analyzed. | |
931 | ||
932 | if Restore_Mode then | |
933 | Restore_SPARK_Mode (Mode); | |
934 | end if; | |
879ac954 AC |
935 | end Analyze_Object_Contract; |
936 | ||
937 | ----------------------------------- | |
938 | -- Analyze_Package_Body_Contract -- | |
939 | ----------------------------------- | |
940 | ||
941 | procedure Analyze_Package_Body_Contract | |
942 | (Body_Id : Entity_Id; | |
943 | Freeze_Id : Entity_Id := Empty) | |
944 | is | |
945 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
946 | Items : constant Node_Id := Contract (Body_Id); | |
947 | Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); | |
948 | Mode : SPARK_Mode_Type; | |
949 | Ref_State : Node_Id; | |
950 | ||
951 | begin | |
e96b7045 | 952 | -- Do not analyze a contract multiple times |
879ac954 AC |
953 | |
954 | if Present (Items) then | |
955 | if Analyzed (Items) then | |
956 | return; | |
957 | else | |
958 | Set_Analyzed (Items); | |
959 | end if; | |
960 | end if; | |
961 | ||
962 | -- Due to the timing of contract analysis, delayed pragmas may be | |
963 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
964 | -- context. To remedy this, restore the original SPARK_Mode of the | |
965 | -- related package body. | |
966 | ||
967 | Save_SPARK_Mode_And_Set (Body_Id, Mode); | |
968 | ||
969 | Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State); | |
970 | ||
971 | -- The analysis of pragma Refined_State detects whether the spec has | |
972 | -- abstract states available for refinement. | |
973 | ||
974 | if Present (Ref_State) then | |
975 | Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id); | |
879ac954 AC |
976 | end if; |
977 | ||
978 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
979 | -- pragmas have been analyzed. | |
980 | ||
981 | Restore_SPARK_Mode (Mode); | |
982 | ||
983 | -- Capture all global references in a generic package body now that the | |
984 | -- contract has been analyzed. | |
985 | ||
986 | if Is_Generic_Declaration_Or_Body (Body_Decl) then | |
987 | Save_Global_References_In_Contract | |
988 | (Templ => Original_Node (Body_Decl), | |
989 | Gen_Id => Spec_Id); | |
990 | end if; | |
991 | end Analyze_Package_Body_Contract; | |
992 | ||
993 | ------------------------------ | |
994 | -- Analyze_Package_Contract -- | |
995 | ------------------------------ | |
996 | ||
997 | procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is | |
998 | Items : constant Node_Id := Contract (Pack_Id); | |
999 | Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id); | |
1000 | Init : Node_Id := Empty; | |
1001 | Init_Cond : Node_Id := Empty; | |
1002 | Mode : SPARK_Mode_Type; | |
1003 | Prag : Node_Id; | |
1004 | Prag_Nam : Name_Id; | |
1005 | ||
1006 | begin | |
e96b7045 | 1007 | -- Do not analyze a contract multiple times |
879ac954 AC |
1008 | |
1009 | if Present (Items) then | |
1010 | if Analyzed (Items) then | |
1011 | return; | |
1012 | else | |
1013 | Set_Analyzed (Items); | |
1014 | end if; | |
1015 | end if; | |
1016 | ||
1017 | -- Due to the timing of contract analysis, delayed pragmas may be | |
1018 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
1019 | -- context. To remedy this, restore the original SPARK_Mode of the | |
1020 | -- related package. | |
1021 | ||
1022 | Save_SPARK_Mode_And_Set (Pack_Id, Mode); | |
1023 | ||
1024 | if Present (Items) then | |
1025 | ||
e96b7045 | 1026 | -- Locate and store pragmas Initial_Condition and Initializes, since |
879ac954 AC |
1027 | -- their order of analysis matters. |
1028 | ||
1029 | Prag := Classifications (Items); | |
1030 | while Present (Prag) loop | |
6e759c2a | 1031 | Prag_Nam := Pragma_Name (Prag); |
879ac954 AC |
1032 | |
1033 | if Prag_Nam = Name_Initial_Condition then | |
1034 | Init_Cond := Prag; | |
1035 | ||
1036 | elsif Prag_Nam = Name_Initializes then | |
1037 | Init := Prag; | |
1038 | end if; | |
1039 | ||
1040 | Prag := Next_Pragma (Prag); | |
1041 | end loop; | |
1042 | ||
e96b7045 | 1043 | -- Analyze the initialization-related pragmas. Initializes must come |
879ac954 AC |
1044 | -- before Initial_Condition due to item dependencies. |
1045 | ||
1046 | if Present (Init) then | |
1047 | Analyze_Initializes_In_Decl_Part (Init); | |
1048 | end if; | |
1049 | ||
1050 | if Present (Init_Cond) then | |
1051 | Analyze_Initial_Condition_In_Decl_Part (Init_Cond); | |
1052 | end if; | |
1053 | end if; | |
1054 | ||
1055 | -- Check whether the lack of indicator Part_Of agrees with the placement | |
1056 | -- of the package instantiation with respect to the state space. | |
1057 | ||
1058 | if Is_Generic_Instance (Pack_Id) then | |
1059 | Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); | |
1060 | ||
1061 | if No (Prag) then | |
1062 | Check_Missing_Part_Of (Pack_Id); | |
1063 | end if; | |
1064 | end if; | |
1065 | ||
1066 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
1067 | -- pragmas have been analyzed. | |
1068 | ||
1069 | Restore_SPARK_Mode (Mode); | |
1070 | ||
1071 | -- Capture all global references in a generic package now that the | |
1072 | -- contract has been analyzed. | |
1073 | ||
1074 | if Is_Generic_Declaration_Or_Body (Pack_Decl) then | |
1075 | Save_Global_References_In_Contract | |
1076 | (Templ => Original_Node (Pack_Decl), | |
1077 | Gen_Id => Pack_Id); | |
1078 | end if; | |
1079 | end Analyze_Package_Contract; | |
1080 | ||
e645cb39 AC |
1081 | -------------------------------- |
1082 | -- Analyze_Previous_Contracts -- | |
1083 | -------------------------------- | |
1084 | ||
1085 | procedure Analyze_Previous_Contracts (Body_Decl : Node_Id) is | |
3603fa5c AC |
1086 | Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); |
1087 | Orig_Decl : constant Node_Id := Original_Node (Body_Decl); | |
1088 | ||
1089 | Par : Node_Id; | |
e645cb39 AC |
1090 | |
1091 | begin | |
1092 | -- A body that is in the process of being inlined appears from source, | |
1093 | -- but carries name _parent. Such a body does not cause "freezing" of | |
1094 | -- contracts. | |
1095 | ||
1096 | if Chars (Body_Id) = Name_uParent then | |
1097 | return; | |
1098 | end if; | |
1099 | ||
1100 | -- Climb the parent chain looking for an enclosing package body. Do not | |
1101 | -- use the scope stack, as a body uses the entity of its corresponding | |
1102 | -- spec. | |
1103 | ||
1104 | Par := Parent (Body_Decl); | |
1105 | while Present (Par) loop | |
1106 | if Nkind (Par) = N_Package_Body then | |
1107 | Analyze_Package_Body_Contract | |
1108 | (Body_Id => Defining_Entity (Par), | |
1109 | Freeze_Id => Defining_Entity (Body_Decl)); | |
1110 | ||
1111 | exit; | |
3603fa5c AC |
1112 | |
1113 | -- Do not look for an enclosing package body when the construct which | |
1114 | -- causes freezing is a body generated for an expression function and | |
1115 | -- it appears within a package spec. This ensures that the traversal | |
1116 | -- will not reach too far up the parent chain and attempt to freeze a | |
1117 | -- package body which should not be frozen. | |
1118 | ||
1119 | -- package body Enclosing_Body | |
1120 | -- with Refined_State => (State => Var) | |
1121 | -- is | |
1122 | -- package Nested is | |
1123 | -- type Some_Type is ...; | |
1124 | -- function Cause_Freezing return ...; | |
1125 | -- private | |
1126 | -- function Cause_Freezing is (...); | |
1127 | -- end Nested; | |
1128 | -- | |
1129 | -- Var : Nested.Some_Type; | |
1130 | ||
1131 | elsif Nkind (Par) = N_Package_Declaration | |
1132 | and then Nkind (Orig_Decl) = N_Expression_Function | |
1133 | then | |
1134 | exit; | |
e645cb39 AC |
1135 | end if; |
1136 | ||
1137 | Par := Parent (Par); | |
1138 | end loop; | |
1139 | ||
4404c282 | 1140 | -- Analyze the contracts of all eligible construct up to the body which |
e645cb39 AC |
1141 | -- caused the "freezing". |
1142 | ||
1143 | if Is_List_Member (Body_Decl) then | |
1144 | Analyze_Contracts | |
1145 | (L => List_Containing (Body_Decl), | |
1146 | Freeze_Nod => Body_Decl, | |
1147 | Freeze_Id => Body_Id); | |
1148 | end if; | |
1149 | end Analyze_Previous_Contracts; | |
1150 | ||
75b87c16 AC |
1151 | -------------------------------- |
1152 | -- Analyze_Protected_Contract -- | |
1153 | -------------------------------- | |
1154 | ||
1155 | procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is | |
1156 | Items : constant Node_Id := Contract (Prot_Id); | |
75b87c16 AC |
1157 | |
1158 | begin | |
1159 | -- Do not analyze a contract multiple times | |
1160 | ||
1161 | if Present (Items) then | |
1162 | if Analyzed (Items) then | |
1163 | return; | |
1164 | else | |
1165 | Set_Analyzed (Items); | |
1166 | end if; | |
1167 | end if; | |
75b87c16 AC |
1168 | end Analyze_Protected_Contract; |
1169 | ||
f99ff327 AC |
1170 | ------------------------------------------- |
1171 | -- Analyze_Subprogram_Body_Stub_Contract -- | |
1172 | ------------------------------------------- | |
879ac954 | 1173 | |
f99ff327 AC |
1174 | procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is |
1175 | Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); | |
1176 | Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); | |
879ac954 AC |
1177 | |
1178 | begin | |
f99ff327 AC |
1179 | -- A subprogram body stub may act as its own spec or as the completion |
1180 | -- of a previous declaration. Depending on the context, the contract of | |
1181 | -- the stub may contain two sets of pragmas. | |
879ac954 | 1182 | |
f99ff327 AC |
1183 | -- The stub is a completion, the applicable pragmas are: |
1184 | -- Refined_Depends | |
1185 | -- Refined_Global | |
879ac954 | 1186 | |
f99ff327 AC |
1187 | if Present (Spec_Id) then |
1188 | Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id); | |
879ac954 | 1189 | |
f99ff327 AC |
1190 | -- The stub acts as its own spec, the applicable pragmas are: |
1191 | -- Contract_Cases | |
1192 | -- Depends | |
1193 | -- Global | |
1194 | -- Postcondition | |
1195 | -- Precondition | |
1196 | -- Test_Case | |
879ac954 | 1197 | |
f99ff327 AC |
1198 | else |
1199 | Analyze_Entry_Or_Subprogram_Contract (Stub_Id); | |
879ac954 | 1200 | end if; |
f99ff327 | 1201 | end Analyze_Subprogram_Body_Stub_Contract; |
879ac954 | 1202 | |
f99ff327 AC |
1203 | --------------------------- |
1204 | -- Analyze_Task_Contract -- | |
1205 | --------------------------- | |
879ac954 | 1206 | |
f99ff327 AC |
1207 | procedure Analyze_Task_Contract (Task_Id : Entity_Id) is |
1208 | Items : constant Node_Id := Contract (Task_Id); | |
1209 | Mode : SPARK_Mode_Type; | |
1210 | Prag : Node_Id; | |
879ac954 AC |
1211 | |
1212 | begin | |
e96b7045 | 1213 | -- Do not analyze a contract multiple times |
879ac954 AC |
1214 | |
1215 | if Present (Items) then | |
1216 | if Analyzed (Items) then | |
1217 | return; | |
1218 | else | |
1219 | Set_Analyzed (Items); | |
1220 | end if; | |
1221 | end if; | |
1222 | ||
1223 | -- Due to the timing of contract analysis, delayed pragmas may be | |
1224 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
1225 | -- context. To remedy this, restore the original SPARK_Mode of the | |
75b87c16 | 1226 | -- related task unit. |
879ac954 | 1227 | |
f99ff327 | 1228 | Save_SPARK_Mode_And_Set (Task_Id, Mode); |
879ac954 | 1229 | |
f99ff327 AC |
1230 | -- Analyze Global first, as Depends may mention items classified in the |
1231 | -- global categorization. | |
879ac954 | 1232 | |
f99ff327 | 1233 | Prag := Get_Pragma (Task_Id, Pragma_Global); |
879ac954 | 1234 | |
f99ff327 AC |
1235 | if Present (Prag) then |
1236 | Analyze_Global_In_Decl_Part (Prag); | |
879ac954 AC |
1237 | end if; |
1238 | ||
f99ff327 AC |
1239 | -- Depends must be analyzed after Global in order to see the modes of |
1240 | -- all global items. | |
879ac954 | 1241 | |
f99ff327 AC |
1242 | Prag := Get_Pragma (Task_Id, Pragma_Depends); |
1243 | ||
1244 | if Present (Prag) then | |
1245 | Analyze_Depends_In_Decl_Part (Prag); | |
879ac954 AC |
1246 | end if; |
1247 | ||
1248 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
1249 | -- pragmas have been analyzed. | |
1250 | ||
1251 | Restore_SPARK_Mode (Mode); | |
f99ff327 | 1252 | end Analyze_Task_Contract; |
879ac954 | 1253 | |
82e5c243 AC |
1254 | ------------------------------------------------- |
1255 | -- Build_And_Analyze_Contract_Only_Subprograms -- | |
1256 | ------------------------------------------------- | |
879ac954 | 1257 | |
82e5c243 AC |
1258 | procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is |
1259 | procedure Analyze_Contract_Only_Subprograms; | |
1260 | -- Analyze the contract-only subprograms of L | |
879ac954 | 1261 | |
82e5c243 AC |
1262 | procedure Append_Contract_Only_Subprograms (Subp_List : List_Id); |
1263 | -- Append the contract-only bodies of Subp_List to its declarations list | |
879ac954 | 1264 | |
82e5c243 AC |
1265 | function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id; |
1266 | -- If E is an entity for a non-imported subprogram specification with | |
1267 | -- pre/postconditions and we are compiling with CodePeer mode, then | |
1268 | -- this procedure will create a wrapper to help Gnat2scil process its | |
1269 | -- contracts. Return Empty if the wrapper cannot be built. | |
879ac954 | 1270 | |
82e5c243 AC |
1271 | function Build_Contract_Only_Subprograms (L : List_Id) return List_Id; |
1272 | -- Build the contract-only subprograms of all eligible subprograms found | |
1273 | -- in list L. | |
879ac954 | 1274 | |
82e5c243 AC |
1275 | function Has_Private_Declarations (N : Node_Id) return Boolean; |
1276 | -- Return True for package specs, task definitions, and protected type | |
1277 | -- definitions whose list of private declarations is not empty. | |
879ac954 | 1278 | |
82e5c243 AC |
1279 | --------------------------------------- |
1280 | -- Analyze_Contract_Only_Subprograms -- | |
1281 | --------------------------------------- | |
879ac954 | 1282 | |
82e5c243 AC |
1283 | procedure Analyze_Contract_Only_Subprograms is |
1284 | procedure Analyze_Contract_Only_Bodies; | |
1285 | -- Analyze all the contract-only bodies of L | |
879ac954 | 1286 | |
82e5c243 AC |
1287 | ---------------------------------- |
1288 | -- Analyze_Contract_Only_Bodies -- | |
1289 | ---------------------------------- | |
879ac954 | 1290 | |
82e5c243 AC |
1291 | procedure Analyze_Contract_Only_Bodies is |
1292 | Decl : Node_Id; | |
879ac954 | 1293 | |
82e5c243 AC |
1294 | begin |
1295 | Decl := First (L); | |
1296 | while Present (Decl) loop | |
1297 | if Nkind (Decl) = N_Subprogram_Body | |
1298 | and then Is_Contract_Only_Body | |
1299 | (Defining_Unit_Name (Specification (Decl))) | |
1300 | then | |
1301 | Analyze (Decl); | |
1302 | end if; | |
879ac954 | 1303 | |
82e5c243 AC |
1304 | Next (Decl); |
1305 | end loop; | |
1306 | end Analyze_Contract_Only_Bodies; | |
879ac954 | 1307 | |
82e5c243 AC |
1308 | -- Start of processing for Analyze_Contract_Only_Subprograms |
1309 | ||
1310 | begin | |
1311 | if Ekind (Current_Scope) /= E_Package then | |
1312 | Analyze_Contract_Only_Bodies; | |
879ac954 AC |
1313 | |
1314 | else | |
82e5c243 AC |
1315 | declare |
1316 | Pkg_Spec : constant Node_Id := | |
1317 | Package_Specification (Current_Scope); | |
879ac954 | 1318 | |
82e5c243 AC |
1319 | begin |
1320 | if not Has_Private_Declarations (Pkg_Spec) then | |
1321 | Analyze_Contract_Only_Bodies; | |
879ac954 | 1322 | |
82e5c243 AC |
1323 | -- For packages with private declarations, the contract-only |
1324 | -- bodies of subprograms defined in the visible part of the | |
1325 | -- package are added to its private declarations (to ensure | |
1326 | -- that they do not cause premature freezing of types and also | |
1327 | -- that they are analyzed with proper visibility). Hence they | |
1328 | -- will be analyzed later. | |
879ac954 | 1329 | |
82e5c243 AC |
1330 | elsif Visible_Declarations (Pkg_Spec) = L then |
1331 | null; | |
879ac954 | 1332 | |
82e5c243 AC |
1333 | elsif Private_Declarations (Pkg_Spec) = L then |
1334 | Analyze_Contract_Only_Bodies; | |
1335 | end if; | |
1336 | end; | |
1337 | end if; | |
1338 | end Analyze_Contract_Only_Subprograms; | |
879ac954 | 1339 | |
82e5c243 AC |
1340 | -------------------------------------- |
1341 | -- Append_Contract_Only_Subprograms -- | |
1342 | -------------------------------------- | |
879ac954 | 1343 | |
82e5c243 AC |
1344 | procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is |
1345 | begin | |
1346 | if No (Subp_List) then | |
1347 | return; | |
879ac954 AC |
1348 | end if; |
1349 | ||
82e5c243 AC |
1350 | if Ekind (Current_Scope) /= E_Package then |
1351 | Append_List (Subp_List, To => L); | |
879ac954 | 1352 | |
82e5c243 AC |
1353 | else |
1354 | declare | |
1355 | Pkg_Spec : constant Node_Id := | |
1356 | Package_Specification (Current_Scope); | |
879ac954 | 1357 | |
82e5c243 AC |
1358 | begin |
1359 | if not Has_Private_Declarations (Pkg_Spec) then | |
1360 | Append_List (Subp_List, To => L); | |
879ac954 | 1361 | |
82e5c243 AC |
1362 | -- If the package has private declarations then append them to |
1363 | -- its private declarations; they will be analyzed when the | |
1364 | -- contracts of its private declarations are analyzed. | |
879ac954 | 1365 | |
82e5c243 AC |
1366 | else |
1367 | Append_List | |
1368 | (List => Subp_List, | |
1369 | To => Private_Declarations (Pkg_Spec)); | |
1370 | end if; | |
1371 | end; | |
879ac954 | 1372 | end if; |
82e5c243 | 1373 | end Append_Contract_Only_Subprograms; |
879ac954 | 1374 | |
82e5c243 AC |
1375 | ------------------------------------ |
1376 | -- Build_Contract_Only_Subprogram -- | |
1377 | ------------------------------------ | |
879ac954 | 1378 | |
82e5c243 AC |
1379 | -- This procedure takes care of building a wrapper to generate better |
1380 | -- analysis results in the case of a call to a subprogram whose body | |
1381 | -- is unavailable to CodePeer but whose specification includes Pre/Post | |
1382 | -- conditions. The body might be unavailable for any of a number or | |
1383 | -- reasons (it is imported, the .adb file is simply missing, or the | |
1384 | -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis) | |
1385 | -- pragma). The built subprogram has the following contents: | |
1386 | -- * check preconditions | |
1387 | -- * call the subprogram | |
1388 | -- * check postconditions | |
879ac954 | 1389 | |
82e5c243 AC |
1390 | function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is |
1391 | Loc : constant Source_Ptr := Sloc (E); | |
879ac954 | 1392 | |
82e5c243 AC |
1393 | Missing_Body_Name : constant Name_Id := |
1394 | New_External_Name (Chars (E), "__missing_body"); | |
879ac954 | 1395 | |
82e5c243 AC |
1396 | function Build_Missing_Body_Decls return List_Id; |
1397 | -- Build the declaration of the missing body subprogram and its | |
1398 | -- corresponding pragma Import. | |
879ac954 | 1399 | |
82e5c243 AC |
1400 | function Build_Missing_Body_Subprogram_Call return Node_Id; |
1401 | -- Build the call to the missing body subprogram | |
879ac954 | 1402 | |
82e5c243 AC |
1403 | function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean; |
1404 | -- Return True for cases where the wrapper is not needed or we cannot | |
1405 | -- build it. | |
879ac954 | 1406 | |
82e5c243 AC |
1407 | ------------------------------ |
1408 | -- Build_Missing_Body_Decls -- | |
1409 | ------------------------------ | |
879ac954 | 1410 | |
82e5c243 AC |
1411 | function Build_Missing_Body_Decls return List_Id is |
1412 | Spec : constant Node_Id := Declaration_Node (E); | |
1413 | Decl : Node_Id; | |
1414 | Prag : Node_Id; | |
879ac954 | 1415 | |
82e5c243 AC |
1416 | begin |
1417 | Decl := | |
1418 | Make_Subprogram_Declaration (Loc, Copy_Subprogram_Spec (Spec)); | |
1419 | Set_Chars (Defining_Entity (Decl), Missing_Body_Name); | |
879ac954 | 1420 | |
82e5c243 AC |
1421 | Prag := |
1422 | Make_Pragma (Loc, | |
1423 | Chars => Name_Import, | |
1424 | Pragma_Argument_Associations => New_List ( | |
1425 | Make_Pragma_Argument_Association (Loc, | |
1426 | Expression => Make_Identifier (Loc, Name_Ada)), | |
879ac954 | 1427 | |
82e5c243 AC |
1428 | Make_Pragma_Argument_Association (Loc, |
1429 | Expression => Make_Identifier (Loc, Missing_Body_Name)))); | |
879ac954 | 1430 | |
82e5c243 AC |
1431 | return New_List (Decl, Prag); |
1432 | end Build_Missing_Body_Decls; | |
879ac954 | 1433 | |
82e5c243 AC |
1434 | ---------------------------------------- |
1435 | -- Build_Missing_Body_Subprogram_Call -- | |
1436 | ---------------------------------------- | |
879ac954 | 1437 | |
82e5c243 AC |
1438 | function Build_Missing_Body_Subprogram_Call return Node_Id is |
1439 | Forml : Entity_Id; | |
1440 | Parms : List_Id; | |
879ac954 | 1441 | |
82e5c243 AC |
1442 | begin |
1443 | Parms := New_List; | |
879ac954 | 1444 | |
82e5c243 | 1445 | -- Build parameter list that we need |
879ac954 | 1446 | |
82e5c243 AC |
1447 | Forml := First_Formal (E); |
1448 | while Present (Forml) loop | |
1449 | Append_To (Parms, Make_Identifier (Loc, Chars (Forml))); | |
1450 | Next_Formal (Forml); | |
1451 | end loop; | |
879ac954 | 1452 | |
82e5c243 | 1453 | -- Build the call to the missing body subprogram |
879ac954 | 1454 | |
82e5c243 AC |
1455 | if Ekind_In (E, E_Function, E_Generic_Function) then |
1456 | return | |
1457 | Make_Simple_Return_Statement (Loc, | |
1458 | Expression => | |
1459 | Make_Function_Call (Loc, | |
1460 | Name => | |
1461 | Make_Identifier (Loc, Missing_Body_Name), | |
1462 | Parameter_Associations => Parms)); | |
879ac954 | 1463 | |
82e5c243 AC |
1464 | else |
1465 | return | |
1466 | Make_Procedure_Call_Statement (Loc, | |
1467 | Name => | |
1468 | Make_Identifier (Loc, Missing_Body_Name), | |
1469 | Parameter_Associations => Parms); | |
1470 | end if; | |
1471 | end Build_Missing_Body_Subprogram_Call; | |
879ac954 | 1472 | |
82e5c243 AC |
1473 | ----------------------------------- |
1474 | -- Skip_Contract_Only_Subprogram -- | |
1475 | ----------------------------------- | |
879ac954 | 1476 | |
82e5c243 AC |
1477 | function Skip_Contract_Only_Subprogram |
1478 | (E : Entity_Id) return Boolean | |
1479 | is | |
1480 | function Depends_On_Enclosing_Private_Type return Boolean; | |
1481 | -- Return True if some formal of E (or its return type) are | |
1482 | -- private types defined in an enclosing package. | |
879ac954 | 1483 | |
82e5c243 AC |
1484 | function Some_Enclosing_Package_Has_Private_Decls return Boolean; |
1485 | -- Return True if some enclosing package of the current scope has | |
1486 | -- private declarations. | |
879ac954 | 1487 | |
82e5c243 AC |
1488 | --------------------------------------- |
1489 | -- Depends_On_Enclosing_Private_Type -- | |
1490 | --------------------------------------- | |
879ac954 | 1491 | |
82e5c243 AC |
1492 | function Depends_On_Enclosing_Private_Type return Boolean is |
1493 | function Defined_In_Enclosing_Package | |
1494 | (Typ : Entity_Id) return Boolean; | |
1495 | -- Return True if Typ is an entity defined in an enclosing | |
1496 | -- package of the current scope. | |
879ac954 | 1497 | |
82e5c243 AC |
1498 | ---------------------------------- |
1499 | -- Defined_In_Enclosing_Package -- | |
1500 | ---------------------------------- | |
879ac954 | 1501 | |
82e5c243 AC |
1502 | function Defined_In_Enclosing_Package |
1503 | (Typ : Entity_Id) return Boolean | |
1504 | is | |
1505 | Scop : Entity_Id := Scope (Current_Scope); | |
879ac954 | 1506 | |
82e5c243 AC |
1507 | begin |
1508 | while Scop /= Scope (Typ) | |
1509 | and then not Is_Compilation_Unit (Scop) | |
1510 | loop | |
1511 | Scop := Scope (Scop); | |
1512 | end loop; | |
879ac954 | 1513 | |
82e5c243 AC |
1514 | return Scop = Scope (Typ); |
1515 | end Defined_In_Enclosing_Package; | |
879ac954 | 1516 | |
82e5c243 | 1517 | -- Local variables |
879ac954 | 1518 | |
82e5c243 AC |
1519 | Param_E : Entity_Id; |
1520 | Typ : Entity_Id; | |
879ac954 | 1521 | |
82e5c243 | 1522 | -- Start of processing for Depends_On_Enclosing_Private_Type |
879ac954 | 1523 | |
82e5c243 AC |
1524 | begin |
1525 | Param_E := First_Entity (E); | |
1526 | while Present (Param_E) loop | |
1527 | Typ := Etype (Param_E); | |
879ac954 | 1528 | |
82e5c243 AC |
1529 | if Is_Private_Type (Typ) |
1530 | and then Defined_In_Enclosing_Package (Typ) | |
1531 | then | |
1532 | return True; | |
1533 | end if; | |
879ac954 | 1534 | |
82e5c243 AC |
1535 | Next_Entity (Param_E); |
1536 | end loop; | |
879ac954 | 1537 | |
82e5c243 AC |
1538 | return |
1539 | Ekind (E) = E_Function | |
1540 | and then Is_Private_Type (Etype (E)) | |
1541 | and then Defined_In_Enclosing_Package (Etype (E)); | |
1542 | end Depends_On_Enclosing_Private_Type; | |
879ac954 | 1543 | |
82e5c243 AC |
1544 | ---------------------------------------------- |
1545 | -- Some_Enclosing_Package_Has_Private_Decls -- | |
1546 | ---------------------------------------------- | |
879ac954 | 1547 | |
82e5c243 AC |
1548 | function Some_Enclosing_Package_Has_Private_Decls return Boolean is |
1549 | Scop : Entity_Id := Current_Scope; | |
1550 | Pkg_Spec : Node_Id := Package_Specification (Scop); | |
879ac954 | 1551 | |
82e5c243 AC |
1552 | begin |
1553 | loop | |
1554 | if Ekind (Scop) = E_Package | |
1555 | and then Has_Private_Declarations | |
1556 | (Package_Specification (Scop)) | |
1557 | then | |
1558 | Pkg_Spec := Package_Specification (Scop); | |
1559 | end if; | |
879ac954 | 1560 | |
82e5c243 AC |
1561 | exit when Is_Compilation_Unit (Scop); |
1562 | Scop := Scope (Scop); | |
1563 | end loop; | |
879ac954 | 1564 | |
82e5c243 AC |
1565 | return Pkg_Spec /= Package_Specification (Current_Scope); |
1566 | end Some_Enclosing_Package_Has_Private_Decls; | |
879ac954 | 1567 | |
82e5c243 | 1568 | -- Start of processing for Skip_Contract_Only_Subprogram |
879ac954 AC |
1569 | |
1570 | begin | |
82e5c243 AC |
1571 | if not CodePeer_Mode |
1572 | or else Inside_A_Generic | |
1573 | or else not Is_Subprogram (E) | |
1574 | or else Is_Abstract_Subprogram (E) | |
1575 | or else Is_Imported (E) | |
1576 | or else No (Contract (E)) | |
1577 | or else No (Pre_Post_Conditions (Contract (E))) | |
1578 | or else Is_Contract_Only_Body (E) | |
1579 | or else Convention (E) = Convention_Protected | |
1580 | then | |
1581 | return True; | |
879ac954 | 1582 | |
82e5c243 AC |
1583 | -- We do not support building the contract-only subprogram if E |
1584 | -- is a subprogram declared in a nested package that has some | |
1585 | -- formal or return type depending on a private type defined in | |
1586 | -- an enclosing package. | |
879ac954 | 1587 | |
82e5c243 AC |
1588 | elsif Ekind (Current_Scope) = E_Package |
1589 | and then Some_Enclosing_Package_Has_Private_Decls | |
1590 | and then Depends_On_Enclosing_Private_Type | |
1591 | then | |
1592 | if Debug_Flag_Dot_KK then | |
1593 | declare | |
1594 | Saved_Mode : constant Warning_Mode_Type := Warning_Mode; | |
879ac954 | 1595 | |
82e5c243 AC |
1596 | begin |
1597 | -- Warnings are disabled by default under CodePeer_Mode | |
1598 | -- (see switch-c). Enable them temporarily. | |
879ac954 | 1599 | |
82e5c243 AC |
1600 | Warning_Mode := Normal; |
1601 | Error_Msg_N | |
1602 | ("cannot generate contract-only subprogram?", E); | |
1603 | Warning_Mode := Saved_Mode; | |
1604 | end; | |
1605 | end if; | |
879ac954 | 1606 | |
82e5c243 AC |
1607 | return True; |
1608 | end if; | |
879ac954 | 1609 | |
82e5c243 AC |
1610 | return False; |
1611 | end Skip_Contract_Only_Subprogram; | |
879ac954 | 1612 | |
82e5c243 | 1613 | -- Start of processing for Build_Contract_Only_Subprogram |
879ac954 | 1614 | |
82e5c243 AC |
1615 | begin |
1616 | -- Test cases where the wrapper is not needed and cases where we | |
1617 | -- cannot build it. | |
879ac954 | 1618 | |
82e5c243 AC |
1619 | if Skip_Contract_Only_Subprogram (E) then |
1620 | return Empty; | |
1621 | end if; | |
879ac954 | 1622 | |
82e5c243 AC |
1623 | -- Note on calls to Copy_Separate_Tree. The trees we are copying |
1624 | -- here are fully analyzed, but we definitely want fully syntactic | |
1625 | -- unanalyzed trees in the body we construct, so that the analysis | |
1626 | -- generates the right visibility, and that is exactly what the | |
1627 | -- calls to Copy_Separate_Tree give us. | |
879ac954 | 1628 | |
82e5c243 AC |
1629 | declare |
1630 | Name : constant Name_Id := | |
1631 | New_External_Name (Chars (E), "__contract_only"); | |
1632 | Id : Entity_Id; | |
1633 | Bod : Node_Id; | |
879ac954 | 1634 | |
82e5c243 AC |
1635 | begin |
1636 | Bod := | |
1637 | Make_Subprogram_Body (Loc, | |
1638 | Specification => | |
1639 | Copy_Subprogram_Spec (Declaration_Node (E)), | |
1640 | Declarations => | |
1641 | Build_Missing_Body_Decls, | |
1642 | Handled_Statement_Sequence => | |
1643 | Make_Handled_Sequence_Of_Statements (Loc, | |
1644 | Statements => New_List ( | |
1645 | Build_Missing_Body_Subprogram_Call), | |
1646 | End_Label => Make_Identifier (Loc, Name))); | |
879ac954 | 1647 | |
82e5c243 | 1648 | Id := Defining_Unit_Name (Specification (Bod)); |
879ac954 | 1649 | |
82e5c243 AC |
1650 | -- Copy only the pre/postconditions of the original contract |
1651 | -- since it is what we need, but also because pragmas stored in | |
1652 | -- the other fields have N_Pragmas with N_Aspect_Specifications | |
1653 | -- that reference their associated pragma (thus causing an endless | |
1654 | -- loop when trying to copy the subtree). | |
879ac954 | 1655 | |
82e5c243 AC |
1656 | declare |
1657 | New_Contract : constant Node_Id := Make_Contract (Sloc (E)); | |
879ac954 | 1658 | |
82e5c243 AC |
1659 | begin |
1660 | Set_Pre_Post_Conditions (New_Contract, | |
1661 | Copy_Separate_Tree (Pre_Post_Conditions (Contract (E)))); | |
1662 | Set_Contract (Id, New_Contract); | |
1663 | end; | |
879ac954 | 1664 | |
82e5c243 AC |
1665 | -- Fix the name of this new subprogram and link the original |
1666 | -- subprogram with its Contract_Only_Body subprogram. | |
879ac954 | 1667 | |
82e5c243 AC |
1668 | Set_Chars (Id, Name); |
1669 | Set_Is_Contract_Only_Body (Id); | |
1670 | Set_Contract_Only_Body (E, Id); | |
879ac954 | 1671 | |
82e5c243 AC |
1672 | return Bod; |
1673 | end; | |
1674 | end Build_Contract_Only_Subprogram; | |
879ac954 | 1675 | |
82e5c243 AC |
1676 | ------------------------------------- |
1677 | -- Build_Contract_Only_Subprograms -- | |
1678 | ------------------------------------- | |
879ac954 | 1679 | |
82e5c243 AC |
1680 | function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is |
1681 | Decl : Node_Id; | |
1682 | New_Subp : Node_Id; | |
1683 | Result : List_Id := No_List; | |
1684 | Subp_Id : Entity_Id; | |
879ac954 | 1685 | |
879ac954 | 1686 | begin |
82e5c243 AC |
1687 | Decl := First (L); |
1688 | while Present (Decl) loop | |
1689 | if Nkind (Decl) = N_Subprogram_Declaration then | |
1690 | Subp_Id := Defining_Unit_Name (Specification (Decl)); | |
1691 | New_Subp := Build_Contract_Only_Subprogram (Subp_Id); | |
879ac954 | 1692 | |
82e5c243 AC |
1693 | if Present (New_Subp) then |
1694 | if No (Result) then | |
1695 | Result := New_List; | |
1696 | end if; | |
879ac954 | 1697 | |
82e5c243 AC |
1698 | Append_To (Result, New_Subp); |
1699 | end if; | |
879ac954 AC |
1700 | end if; |
1701 | ||
82e5c243 AC |
1702 | Next (Decl); |
1703 | end loop; | |
879ac954 | 1704 | |
82e5c243 AC |
1705 | return Result; |
1706 | end Build_Contract_Only_Subprograms; | |
879ac954 | 1707 | |
82e5c243 AC |
1708 | ------------------------------ |
1709 | -- Has_Private_Declarations -- | |
1710 | ------------------------------ | |
879ac954 | 1711 | |
82e5c243 AC |
1712 | function Has_Private_Declarations (N : Node_Id) return Boolean is |
1713 | begin | |
1714 | if not Nkind_In (N, N_Package_Specification, | |
1715 | N_Protected_Definition, | |
1716 | N_Task_Definition) | |
1717 | then | |
1718 | return False; | |
1719 | else | |
1720 | return | |
1721 | Present (Private_Declarations (N)) | |
1722 | and then Is_Non_Empty_List (Private_Declarations (N)); | |
1723 | end if; | |
1724 | end Has_Private_Declarations; | |
879ac954 | 1725 | |
82e5c243 | 1726 | -- Local variables |
879ac954 | 1727 | |
82e5c243 | 1728 | Subp_List : List_Id; |
879ac954 | 1729 | |
82e5c243 | 1730 | -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms |
879ac954 | 1731 | |
82e5c243 AC |
1732 | begin |
1733 | Subp_List := Build_Contract_Only_Subprograms (L); | |
1734 | Append_Contract_Only_Subprograms (Subp_List); | |
1735 | Analyze_Contract_Only_Subprograms; | |
1736 | end Build_And_Analyze_Contract_Only_Subprograms; | |
879ac954 | 1737 | |
82e5c243 AC |
1738 | ----------------------------- |
1739 | -- Create_Generic_Contract -- | |
1740 | ----------------------------- | |
879ac954 | 1741 | |
82e5c243 AC |
1742 | procedure Create_Generic_Contract (Unit : Node_Id) is |
1743 | Templ : constant Node_Id := Original_Node (Unit); | |
1744 | Templ_Id : constant Entity_Id := Defining_Entity (Templ); | |
879ac954 | 1745 | |
82e5c243 AC |
1746 | procedure Add_Generic_Contract_Pragma (Prag : Node_Id); |
1747 | -- Add a single contract-related source pragma Prag to the contract of | |
1748 | -- generic template Templ_Id. | |
879ac954 | 1749 | |
82e5c243 AC |
1750 | --------------------------------- |
1751 | -- Add_Generic_Contract_Pragma -- | |
1752 | --------------------------------- | |
879ac954 | 1753 | |
82e5c243 AC |
1754 | procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is |
1755 | Prag_Templ : Node_Id; | |
879ac954 | 1756 | |
82e5c243 AC |
1757 | begin |
1758 | -- Mark the pragma to prevent the premature capture of global | |
1759 | -- references when capturing global references of the context | |
1760 | -- (see Save_References_In_Pragma). | |
879ac954 | 1761 | |
82e5c243 | 1762 | Set_Is_Generic_Contract_Pragma (Prag); |
879ac954 | 1763 | |
82e5c243 AC |
1764 | -- Pragmas that apply to a generic subprogram declaration are not |
1765 | -- part of the semantic structure of the generic template: | |
879ac954 | 1766 | |
82e5c243 AC |
1767 | -- generic |
1768 | -- procedure Example (Formal : Integer); | |
1769 | -- pragma Precondition (Formal > 0); | |
879ac954 | 1770 | |
82e5c243 AC |
1771 | -- Create a generic template for such pragmas and link the template |
1772 | -- of the pragma with the generic template. | |
879ac954 | 1773 | |
82e5c243 AC |
1774 | if Nkind (Templ) = N_Generic_Subprogram_Declaration then |
1775 | Rewrite | |
1776 | (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); | |
1777 | Prag_Templ := Original_Node (Prag); | |
c37e6613 | 1778 | |
82e5c243 AC |
1779 | Set_Is_Generic_Contract_Pragma (Prag_Templ); |
1780 | Add_Contract_Item (Prag_Templ, Templ_Id); | |
c37e6613 | 1781 | |
82e5c243 AC |
1782 | -- Otherwise link the pragma with the generic template |
1783 | ||
1784 | else | |
1785 | Add_Contract_Item (Prag, Templ_Id); | |
c37e6613 | 1786 | end if; |
82e5c243 | 1787 | end Add_Generic_Contract_Pragma; |
879ac954 | 1788 | |
82e5c243 | 1789 | -- Local variables |
879ac954 | 1790 | |
82e5c243 AC |
1791 | Context : constant Node_Id := Parent (Unit); |
1792 | Decl : Node_Id := Empty; | |
879ac954 | 1793 | |
82e5c243 | 1794 | -- Start of processing for Create_Generic_Contract |
c37e6613 | 1795 | |
82e5c243 AC |
1796 | begin |
1797 | -- A generic package declaration carries contract-related source pragmas | |
1798 | -- in its visible declarations. | |
c37e6613 | 1799 | |
82e5c243 AC |
1800 | if Nkind (Templ) = N_Generic_Package_Declaration then |
1801 | Set_Ekind (Templ_Id, E_Generic_Package); | |
879ac954 | 1802 | |
82e5c243 AC |
1803 | if Present (Visible_Declarations (Specification (Templ))) then |
1804 | Decl := First (Visible_Declarations (Specification (Templ))); | |
1805 | end if; | |
c37e6613 | 1806 | |
82e5c243 AC |
1807 | -- A generic package body carries contract-related source pragmas in its |
1808 | -- declarations. | |
879ac954 | 1809 | |
82e5c243 AC |
1810 | elsif Nkind (Templ) = N_Package_Body then |
1811 | Set_Ekind (Templ_Id, E_Package_Body); | |
c37e6613 | 1812 | |
82e5c243 AC |
1813 | if Present (Declarations (Templ)) then |
1814 | Decl := First (Declarations (Templ)); | |
1815 | end if; | |
879ac954 | 1816 | |
82e5c243 | 1817 | -- Generic subprogram declaration |
879ac954 | 1818 | |
82e5c243 AC |
1819 | elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then |
1820 | if Nkind (Specification (Templ)) = N_Function_Specification then | |
1821 | Set_Ekind (Templ_Id, E_Generic_Function); | |
1822 | else | |
1823 | Set_Ekind (Templ_Id, E_Generic_Procedure); | |
1824 | end if; | |
879ac954 | 1825 | |
82e5c243 AC |
1826 | -- When the generic subprogram acts as a compilation unit, inspect |
1827 | -- the Pragmas_After list for contract-related source pragmas. | |
879ac954 | 1828 | |
82e5c243 AC |
1829 | if Nkind (Context) = N_Compilation_Unit then |
1830 | if Present (Aux_Decls_Node (Context)) | |
1831 | and then Present (Pragmas_After (Aux_Decls_Node (Context))) | |
1832 | then | |
1833 | Decl := First (Pragmas_After (Aux_Decls_Node (Context))); | |
1834 | end if; | |
879ac954 | 1835 | |
82e5c243 AC |
1836 | -- Otherwise inspect the successive declarations for contract-related |
1837 | -- source pragmas. | |
879ac954 | 1838 | |
82e5c243 AC |
1839 | else |
1840 | Decl := Next (Unit); | |
1841 | end if; | |
879ac954 | 1842 | |
82e5c243 AC |
1843 | -- A generic subprogram body carries contract-related source pragmas in |
1844 | -- its declarations. | |
879ac954 | 1845 | |
82e5c243 AC |
1846 | elsif Nkind (Templ) = N_Subprogram_Body then |
1847 | Set_Ekind (Templ_Id, E_Subprogram_Body); | |
879ac954 | 1848 | |
82e5c243 AC |
1849 | if Present (Declarations (Templ)) then |
1850 | Decl := First (Declarations (Templ)); | |
879ac954 | 1851 | end if; |
82e5c243 | 1852 | end if; |
879ac954 | 1853 | |
82e5c243 AC |
1854 | -- Inspect the relevant declarations looking for contract-related source |
1855 | -- pragmas and add them to the contract of the generic unit. | |
879ac954 | 1856 | |
82e5c243 AC |
1857 | while Present (Decl) loop |
1858 | if Comes_From_Source (Decl) then | |
1859 | if Nkind (Decl) = N_Pragma then | |
879ac954 | 1860 | |
82e5c243 | 1861 | -- The source pragma is a contract annotation |
879ac954 | 1862 | |
82e5c243 AC |
1863 | if Is_Contract_Annotation (Decl) then |
1864 | Add_Generic_Contract_Pragma (Decl); | |
1865 | end if; | |
879ac954 | 1866 | |
82e5c243 AC |
1867 | -- The region where a contract-related source pragma may appear |
1868 | -- ends with the first source non-pragma declaration or statement. | |
879ac954 | 1869 | |
82e5c243 AC |
1870 | else |
1871 | exit; | |
1872 | end if; | |
1873 | end if; | |
879ac954 | 1874 | |
82e5c243 AC |
1875 | Next (Decl); |
1876 | end loop; | |
1877 | end Create_Generic_Contract; | |
879ac954 | 1878 | |
82e5c243 AC |
1879 | -------------------------------- |
1880 | -- Expand_Subprogram_Contract -- | |
1881 | -------------------------------- | |
879ac954 | 1882 | |
82e5c243 AC |
1883 | procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is |
1884 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
1885 | Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); | |
879ac954 | 1886 | |
82e5c243 AC |
1887 | procedure Add_Invariant_And_Predicate_Checks |
1888 | (Subp_Id : Entity_Id; | |
1889 | Stmts : in out List_Id; | |
1890 | Result : out Node_Id); | |
1891 | -- Process the result of function Subp_Id (if applicable) and all its | |
1892 | -- formals. Add invariant and predicate checks where applicable. The | |
1893 | -- routine appends all the checks to list Stmts. If Subp_Id denotes a | |
1894 | -- function, Result contains the entity of parameter _Result, to be | |
1895 | -- used in the creation of procedure _Postconditions. | |
879ac954 | 1896 | |
82e5c243 AC |
1897 | procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); |
1898 | -- Append a node to a list. If there is no list, create a new one. When | |
1899 | -- the item denotes a pragma, it is added to the list only when it is | |
1900 | -- enabled. | |
879ac954 | 1901 | |
82e5c243 AC |
1902 | procedure Build_Postconditions_Procedure |
1903 | (Subp_Id : Entity_Id; | |
1904 | Stmts : List_Id; | |
1905 | Result : Entity_Id); | |
1906 | -- Create the body of procedure _Postconditions which handles various | |
1907 | -- assertion actions on exit from subprogram Subp_Id. Stmts is the list | |
1908 | -- of statements to be checked on exit. Parameter Result is the entity | |
1909 | -- of parameter _Result when Subp_Id denotes a function. | |
879ac954 | 1910 | |
82e5c243 AC |
1911 | procedure Process_Contract_Cases (Stmts : in out List_Id); |
1912 | -- Process pragma Contract_Cases. This routine prepends items to the | |
1913 | -- body declarations and appends items to list Stmts. | |
879ac954 | 1914 | |
82e5c243 AC |
1915 | procedure Process_Postconditions (Stmts : in out List_Id); |
1916 | -- Collect all [inherited] spec and body postconditions and accumulate | |
1917 | -- their pragma Check equivalents in list Stmts. | |
879ac954 | 1918 | |
82e5c243 AC |
1919 | procedure Process_Preconditions; |
1920 | -- Collect all [inherited] spec and body preconditions and prepend their | |
1921 | -- pragma Check equivalents to the declarations of the body. | |
879ac954 | 1922 | |
82e5c243 AC |
1923 | ---------------------------------------- |
1924 | -- Add_Invariant_And_Predicate_Checks -- | |
1925 | ---------------------------------------- | |
879ac954 | 1926 | |
82e5c243 AC |
1927 | procedure Add_Invariant_And_Predicate_Checks |
1928 | (Subp_Id : Entity_Id; | |
1929 | Stmts : in out List_Id; | |
1930 | Result : out Node_Id) | |
1931 | is | |
1932 | procedure Add_Invariant_Access_Checks (Id : Entity_Id); | |
1933 | -- Id denotes the return value of a function or a formal parameter. | |
1934 | -- Add an invariant check if the type of Id is access to a type with | |
1935 | -- invariants. The routine appends the generated code to Stmts. | |
1936 | ||
1937 | function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; | |
1938 | -- Determine whether type Typ can benefit from invariant checks. To | |
1939 | -- qualify, the type must have a non-null invariant procedure and | |
1940 | -- subprogram Subp_Id must appear visible from the point of view of | |
1941 | -- the type. | |
879ac954 AC |
1942 | |
1943 | --------------------------------- | |
82e5c243 | 1944 | -- Add_Invariant_Access_Checks -- |
879ac954 AC |
1945 | --------------------------------- |
1946 | ||
82e5c243 AC |
1947 | procedure Add_Invariant_Access_Checks (Id : Entity_Id) is |
1948 | Loc : constant Source_Ptr := Sloc (Body_Decl); | |
1949 | Ref : Node_Id; | |
1950 | Typ : Entity_Id; | |
879ac954 AC |
1951 | |
1952 | begin | |
82e5c243 | 1953 | Typ := Etype (Id); |
879ac954 | 1954 | |
82e5c243 AC |
1955 | if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then |
1956 | Typ := Designated_Type (Typ); | |
879ac954 | 1957 | |
82e5c243 AC |
1958 | if Invariant_Checks_OK (Typ) then |
1959 | Ref := | |
1960 | Make_Explicit_Dereference (Loc, | |
1961 | Prefix => New_Occurrence_Of (Id, Loc)); | |
1962 | Set_Etype (Ref, Typ); | |
1963 | ||
1964 | -- Generate: | |
1965 | -- if <Id> /= null then | |
1966 | -- <invariant_call (<Ref>)> | |
1967 | -- end if; | |
1968 | ||
1969 | Append_Enabled_Item | |
1970 | (Item => | |
1971 | Make_If_Statement (Loc, | |
1972 | Condition => | |
1973 | Make_Op_Ne (Loc, | |
1974 | Left_Opnd => New_Occurrence_Of (Id, Loc), | |
1975 | Right_Opnd => Make_Null (Loc)), | |
1976 | Then_Statements => New_List ( | |
1977 | Make_Invariant_Call (Ref))), | |
1978 | List => Stmts); | |
1979 | end if; | |
879ac954 | 1980 | end if; |
82e5c243 | 1981 | end Add_Invariant_Access_Checks; |
879ac954 | 1982 | |
82e5c243 AC |
1983 | ------------------------- |
1984 | -- Invariant_Checks_OK -- | |
1985 | ------------------------- | |
879ac954 | 1986 | |
82e5c243 AC |
1987 | function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is |
1988 | function Has_Public_Visibility_Of_Subprogram return Boolean; | |
1989 | -- Determine whether type Typ has public visibility of subprogram | |
1990 | -- Subp_Id. | |
879ac954 | 1991 | |
82e5c243 AC |
1992 | ----------------------------------------- |
1993 | -- Has_Public_Visibility_Of_Subprogram -- | |
1994 | ----------------------------------------- | |
879ac954 | 1995 | |
82e5c243 AC |
1996 | function Has_Public_Visibility_Of_Subprogram return Boolean is |
1997 | Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); | |
879ac954 | 1998 | |
82e5c243 AC |
1999 | begin |
2000 | -- An Initialization procedure must be considered visible even | |
2001 | -- though it is internally generated. | |
879ac954 | 2002 | |
82e5c243 AC |
2003 | if Is_Init_Proc (Defining_Entity (Subp_Decl)) then |
2004 | return True; | |
879ac954 | 2005 | |
82e5c243 AC |
2006 | elsif Ekind (Scope (Typ)) /= E_Package then |
2007 | return False; | |
879ac954 | 2008 | |
82e5c243 AC |
2009 | -- Internally generated code is never publicly visible except |
2010 | -- for a subprogram that is the implementation of an expression | |
2011 | -- function. In that case the visibility is determined by the | |
2012 | -- last check. | |
879ac954 | 2013 | |
82e5c243 AC |
2014 | elsif not Comes_From_Source (Subp_Decl) |
2015 | and then | |
2016 | (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function | |
2017 | or else not | |
2018 | Comes_From_Source (Defining_Entity (Subp_Decl))) | |
2019 | then | |
2020 | return False; | |
879ac954 | 2021 | |
82e5c243 | 2022 | -- Determine whether the subprogram is declared in the visible |
bfda9ccd AC |
2023 | -- declarations of the package containing the type, or in the |
2024 | -- visible declaration of a child unit of that package. | |
879ac954 | 2025 | |
82e5c243 | 2026 | else |
bfda9ccd AC |
2027 | declare |
2028 | Decls : constant List_Id := | |
2029 | List_Containing (Subp_Decl); | |
2030 | Subp_Scope : constant Entity_Id := | |
2031 | Scope (Defining_Entity (Subp_Decl)); | |
2032 | Typ_Scope : constant Entity_Id := Scope (Typ); | |
2033 | ||
2034 | begin | |
2035 | return | |
2036 | Decls = Visible_Declarations | |
2037 | (Specification (Unit_Declaration_Node (Typ_Scope))) | |
2038 | ||
2039 | or else | |
2040 | (Ekind (Subp_Scope) = E_Package | |
2041 | and then Typ_Scope /= Subp_Scope | |
2042 | and then Is_Child_Unit (Subp_Scope) | |
2043 | and then | |
2044 | Is_Ancestor_Package (Typ_Scope, Subp_Scope) | |
2045 | and then | |
2046 | Decls = Visible_Declarations | |
2047 | (Specification | |
2048 | (Unit_Declaration_Node (Subp_Scope)))); | |
2049 | end; | |
82e5c243 AC |
2050 | end if; |
2051 | end Has_Public_Visibility_Of_Subprogram; | |
879ac954 | 2052 | |
82e5c243 | 2053 | -- Start of processing for Invariant_Checks_OK |
879ac954 | 2054 | |
82e5c243 AC |
2055 | begin |
2056 | return | |
2057 | Has_Invariants (Typ) | |
2058 | and then Present (Invariant_Procedure (Typ)) | |
2059 | and then not Has_Null_Body (Invariant_Procedure (Typ)) | |
2060 | and then Has_Public_Visibility_Of_Subprogram; | |
2061 | end Invariant_Checks_OK; | |
a6363ed3 | 2062 | |
82e5c243 | 2063 | -- Local variables |
879ac954 | 2064 | |
82e5c243 AC |
2065 | Loc : constant Source_Ptr := Sloc (Body_Decl); |
2066 | -- Source location of subprogram body contract | |
879ac954 | 2067 | |
82e5c243 AC |
2068 | Formal : Entity_Id; |
2069 | Typ : Entity_Id; | |
879ac954 | 2070 | |
82e5c243 | 2071 | -- Start of processing for Add_Invariant_And_Predicate_Checks |
879ac954 | 2072 | |
82e5c243 AC |
2073 | begin |
2074 | Result := Empty; | |
879ac954 | 2075 | |
82e5c243 | 2076 | -- Process the result of a function |
a6363ed3 | 2077 | |
82e5c243 AC |
2078 | if Ekind (Subp_Id) = E_Function then |
2079 | Typ := Etype (Subp_Id); | |
a6363ed3 | 2080 | |
82e5c243 AC |
2081 | -- Generate _Result which is used in procedure _Postconditions to |
2082 | -- verify the return value. | |
a6363ed3 | 2083 | |
82e5c243 AC |
2084 | Result := Make_Defining_Identifier (Loc, Name_uResult); |
2085 | Set_Etype (Result, Typ); | |
a6363ed3 | 2086 | |
82e5c243 AC |
2087 | -- Add an invariant check when the return type has invariants and |
2088 | -- the related function is visible to the outside. | |
a6363ed3 | 2089 | |
82e5c243 AC |
2090 | if Invariant_Checks_OK (Typ) then |
2091 | Append_Enabled_Item | |
2092 | (Item => | |
2093 | Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), | |
2094 | List => Stmts); | |
2095 | end if; | |
a6363ed3 | 2096 | |
82e5c243 AC |
2097 | -- Add an invariant check when the return type is an access to a |
2098 | -- type with invariants. | |
a6363ed3 | 2099 | |
82e5c243 AC |
2100 | Add_Invariant_Access_Checks (Result); |
2101 | end if; | |
07820c51 | 2102 | |
82e5c243 AC |
2103 | -- Add invariant and predicates for all formals that qualify |
2104 | ||
2105 | Formal := First_Formal (Subp_Id); | |
2106 | while Present (Formal) loop | |
2107 | Typ := Etype (Formal); | |
2108 | ||
2109 | if Ekind (Formal) /= E_In_Parameter | |
2110 | or else Is_Access_Type (Typ) | |
2111 | then | |
2112 | if Invariant_Checks_OK (Typ) then | |
2113 | Append_Enabled_Item | |
2114 | (Item => | |
2115 | Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), | |
2116 | List => Stmts); | |
a6363ed3 | 2117 | end if; |
a6363ed3 | 2118 | |
82e5c243 | 2119 | Add_Invariant_Access_Checks (Formal); |
a6363ed3 | 2120 | |
82e5c243 AC |
2121 | -- Note: we used to add predicate checks for OUT and IN OUT |
2122 | -- formals here, but that was misguided, since such checks are | |
2123 | -- performed on the caller side, based on the predicate of the | |
2124 | -- actual, rather than the predicate of the formal. | |
879ac954 | 2125 | |
82e5c243 | 2126 | end if; |
879ac954 | 2127 | |
82e5c243 AC |
2128 | Next_Formal (Formal); |
2129 | end loop; | |
2130 | end Add_Invariant_And_Predicate_Checks; | |
879ac954 | 2131 | |
82e5c243 AC |
2132 | ------------------------- |
2133 | -- Append_Enabled_Item -- | |
2134 | ------------------------- | |
879ac954 | 2135 | |
82e5c243 AC |
2136 | procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is |
2137 | begin | |
2138 | -- Do not chain ignored or disabled pragmas | |
879ac954 | 2139 | |
82e5c243 AC |
2140 | if Nkind (Item) = N_Pragma |
2141 | and then (Is_Ignored (Item) or else Is_Disabled (Item)) | |
2142 | then | |
2143 | null; | |
879ac954 | 2144 | |
82e5c243 | 2145 | -- Otherwise, add the item |
879ac954 | 2146 | |
82e5c243 AC |
2147 | else |
2148 | if No (List) then | |
2149 | List := New_List; | |
2150 | end if; | |
879ac954 | 2151 | |
82e5c243 AC |
2152 | -- If the pragma is a conjunct in a composite postcondition, it |
2153 | -- has been processed in reverse order. In the postcondition body | |
2154 | -- it must appear before the others. | |
879ac954 | 2155 | |
82e5c243 AC |
2156 | if Nkind (Item) = N_Pragma |
2157 | and then From_Aspect_Specification (Item) | |
2158 | and then Split_PPC (Item) | |
2159 | then | |
2160 | Prepend (Item, List); | |
2161 | else | |
2162 | Append (Item, List); | |
2163 | end if; | |
2164 | end if; | |
2165 | end Append_Enabled_Item; | |
879ac954 | 2166 | |
82e5c243 AC |
2167 | ------------------------------------ |
2168 | -- Build_Postconditions_Procedure -- | |
2169 | ------------------------------------ | |
879ac954 | 2170 | |
82e5c243 AC |
2171 | procedure Build_Postconditions_Procedure |
2172 | (Subp_Id : Entity_Id; | |
2173 | Stmts : List_Id; | |
2174 | Result : Entity_Id) | |
2175 | is | |
2176 | procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id); | |
2177 | -- Insert node Stmt before the first source declaration of the | |
2178 | -- related subprogram's body. If no such declaration exists, Stmt | |
2179 | -- becomes the last declaration. | |
2180 | ||
2181 | -------------------------------------------- | |
2182 | -- Insert_Before_First_Source_Declaration -- | |
2183 | -------------------------------------------- | |
2184 | ||
2185 | procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is | |
2186 | Decls : constant List_Id := Declarations (Body_Decl); | |
2187 | Decl : Node_Id; | |
879ac954 AC |
2188 | |
2189 | begin | |
82e5c243 AC |
2190 | -- Inspect the declarations of the related subprogram body looking |
2191 | -- for the first source declaration. | |
879ac954 | 2192 | |
82e5c243 AC |
2193 | if Present (Decls) then |
2194 | Decl := First (Decls); | |
2195 | while Present (Decl) loop | |
2196 | if Comes_From_Source (Decl) then | |
2197 | Insert_Before (Decl, Stmt); | |
2198 | return; | |
2199 | end if; | |
879ac954 | 2200 | |
82e5c243 AC |
2201 | Next (Decl); |
2202 | end loop; | |
879ac954 | 2203 | |
82e5c243 AC |
2204 | -- If we get there, then the subprogram body lacks any source |
2205 | -- declarations. The body of _Postconditions now acts as the | |
2206 | -- last declaration. | |
879ac954 | 2207 | |
82e5c243 | 2208 | Append (Stmt, Decls); |
879ac954 | 2209 | |
82e5c243 AC |
2210 | -- Ensure that the body has a declaration list |
2211 | ||
2212 | else | |
2213 | Set_Declarations (Body_Decl, New_List (Stmt)); | |
879ac954 | 2214 | end if; |
82e5c243 | 2215 | end Insert_Before_First_Source_Declaration; |
879ac954 | 2216 | |
82e5c243 | 2217 | -- Local variables |
879ac954 | 2218 | |
82e5c243 AC |
2219 | Loc : constant Source_Ptr := Sloc (Body_Decl); |
2220 | Params : List_Id := No_List; | |
2221 | Proc_Bod : Node_Id; | |
2222 | Proc_Decl : Node_Id; | |
2223 | Proc_Id : Entity_Id; | |
2224 | Proc_Spec : Node_Id; | |
879ac954 | 2225 | |
82e5c243 | 2226 | -- Start of processing for Build_Postconditions_Procedure |
879ac954 | 2227 | |
82e5c243 AC |
2228 | begin |
2229 | -- Nothing to do if there are no actions to check on exit | |
879ac954 | 2230 | |
82e5c243 AC |
2231 | if No (Stmts) then |
2232 | return; | |
2233 | end if; | |
879ac954 | 2234 | |
82e5c243 AC |
2235 | Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); |
2236 | Set_Debug_Info_Needed (Proc_Id); | |
2237 | Set_Postconditions_Proc (Subp_Id, Proc_Id); | |
879ac954 | 2238 | |
82e5c243 AC |
2239 | -- Force the front-end inlining of _Postconditions when generating C |
2240 | -- code, since its body may have references to itypes defined in the | |
2241 | -- enclosing subprogram, which would cause problems for unnesting | |
2242 | -- routines in the absence of inlining. | |
879ac954 | 2243 | |
c63a2ad6 | 2244 | if Modify_Tree_For_C then |
82e5c243 AC |
2245 | Set_Has_Pragma_Inline (Proc_Id); |
2246 | Set_Has_Pragma_Inline_Always (Proc_Id); | |
2247 | Set_Is_Inlined (Proc_Id); | |
2248 | end if; | |
879ac954 | 2249 | |
82e5c243 AC |
2250 | -- The related subprogram is a function: create the specification of |
2251 | -- parameter _Result. | |
879ac954 | 2252 | |
82e5c243 AC |
2253 | if Present (Result) then |
2254 | Params := New_List ( | |
2255 | Make_Parameter_Specification (Loc, | |
2256 | Defining_Identifier => Result, | |
2257 | Parameter_Type => | |
2258 | New_Occurrence_Of (Etype (Result), Loc))); | |
2259 | end if; | |
879ac954 | 2260 | |
82e5c243 AC |
2261 | Proc_Spec := |
2262 | Make_Procedure_Specification (Loc, | |
2263 | Defining_Unit_Name => Proc_Id, | |
2264 | Parameter_Specifications => Params); | |
879ac954 | 2265 | |
82e5c243 | 2266 | Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec); |
879ac954 | 2267 | |
82e5c243 AC |
2268 | -- Insert _Postconditions before the first source declaration of the |
2269 | -- body. This ensures that the body will not cause any premature | |
2270 | -- freezing, as it may mention types: | |
879ac954 | 2271 | |
82e5c243 AC |
2272 | -- procedure Proc (Obj : Array_Typ) is |
2273 | -- procedure _postconditions is | |
2274 | -- begin | |
2275 | -- ... Obj ... | |
2276 | -- end _postconditions; | |
879ac954 | 2277 | |
82e5c243 AC |
2278 | -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); |
2279 | -- begin | |
879ac954 | 2280 | |
82e5c243 AC |
2281 | -- In the example above, Obj is of type T but the incorrect placement |
2282 | -- of _Postconditions will cause a crash in gigi due to an out-of- | |
2283 | -- order reference. The body of _Postconditions must be placed after | |
2284 | -- the declaration of Temp to preserve correct visibility. | |
879ac954 | 2285 | |
82e5c243 AC |
2286 | Insert_Before_First_Source_Declaration (Proc_Decl); |
2287 | Analyze (Proc_Decl); | |
879ac954 | 2288 | |
82e5c243 AC |
2289 | -- Set an explicit End_Label to override the sloc of the implicit |
2290 | -- RETURN statement, and prevent it from inheriting the sloc of one | |
2291 | -- the postconditions: this would cause confusing debug info to be | |
2292 | -- produced, interfering with coverage-analysis tools. | |
2293 | ||
2294 | Proc_Bod := | |
2295 | Make_Subprogram_Body (Loc, | |
2296 | Specification => | |
2297 | Copy_Subprogram_Spec (Proc_Spec), | |
2298 | Declarations => Empty_List, | |
2299 | Handled_Statement_Sequence => | |
2300 | Make_Handled_Sequence_Of_Statements (Loc, | |
2301 | Statements => Stmts, | |
2302 | End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); | |
2303 | ||
2304 | Insert_After_And_Analyze (Proc_Decl, Proc_Bod); | |
2305 | end Build_Postconditions_Procedure; | |
2306 | ||
2307 | ---------------------------- | |
2308 | -- Process_Contract_Cases -- | |
2309 | ---------------------------- | |
2310 | ||
2311 | procedure Process_Contract_Cases (Stmts : in out List_Id) is | |
2312 | procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); | |
2313 | -- Process pragma Contract_Cases for subprogram Subp_Id | |
2314 | ||
2315 | -------------------------------- | |
2316 | -- Process_Contract_Cases_For -- | |
2317 | -------------------------------- | |
2318 | ||
2319 | procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is | |
2320 | Items : constant Node_Id := Contract (Subp_Id); | |
2321 | Prag : Node_Id; | |
2322 | ||
2323 | begin | |
2324 | if Present (Items) then | |
2325 | Prag := Contract_Test_Cases (Items); | |
2326 | while Present (Prag) loop | |
2327 | if Pragma_Name (Prag) = Name_Contract_Cases then | |
2328 | Expand_Pragma_Contract_Cases | |
2329 | (CCs => Prag, | |
2330 | Subp_Id => Subp_Id, | |
2331 | Decls => Declarations (Body_Decl), | |
2332 | Stmts => Stmts); | |
2333 | end if; | |
879ac954 | 2334 | |
82e5c243 AC |
2335 | Prag := Next_Pragma (Prag); |
2336 | end loop; | |
2337 | end if; | |
2338 | end Process_Contract_Cases_For; | |
879ac954 | 2339 | |
82e5c243 | 2340 | -- Start of processing for Process_Contract_Cases |
879ac954 | 2341 | |
82e5c243 AC |
2342 | begin |
2343 | Process_Contract_Cases_For (Body_Id); | |
879ac954 | 2344 | |
82e5c243 AC |
2345 | if Present (Spec_Id) then |
2346 | Process_Contract_Cases_For (Spec_Id); | |
2347 | end if; | |
2348 | end Process_Contract_Cases; | |
879ac954 | 2349 | |
82e5c243 AC |
2350 | ---------------------------- |
2351 | -- Process_Postconditions -- | |
2352 | ---------------------------- | |
879ac954 | 2353 | |
82e5c243 AC |
2354 | procedure Process_Postconditions (Stmts : in out List_Id) is |
2355 | procedure Process_Body_Postconditions (Post_Nam : Name_Id); | |
2356 | -- Collect all [refined] postconditions of a specific kind denoted | |
2357 | -- by Post_Nam that belong to the body, and generate pragma Check | |
2358 | -- equivalents in list Stmts. | |
879ac954 | 2359 | |
82e5c243 AC |
2360 | procedure Process_Spec_Postconditions; |
2361 | -- Collect all [inherited] postconditions of the spec, and generate | |
2362 | -- pragma Check equivalents in list Stmts. | |
2363 | ||
2364 | --------------------------------- | |
2365 | -- Process_Body_Postconditions -- | |
2366 | --------------------------------- | |
2367 | ||
2368 | procedure Process_Body_Postconditions (Post_Nam : Name_Id) is | |
2369 | Items : constant Node_Id := Contract (Body_Id); | |
2370 | Unit_Decl : constant Node_Id := Parent (Body_Decl); | |
879ac954 AC |
2371 | Decl : Node_Id; |
2372 | Prag : Node_Id; | |
879ac954 AC |
2373 | |
2374 | begin | |
2375 | -- Process the contract | |
2376 | ||
2377 | if Present (Items) then | |
2378 | Prag := Pre_Post_Conditions (Items); | |
2379 | while Present (Prag) loop | |
82e5c243 AC |
2380 | if Pragma_Name (Prag) = Post_Nam then |
2381 | Append_Enabled_Item | |
2382 | (Item => Build_Pragma_Check_Equivalent (Prag), | |
2383 | List => Stmts); | |
879ac954 AC |
2384 | end if; |
2385 | ||
2386 | Prag := Next_Pragma (Prag); | |
2387 | end loop; | |
2388 | end if; | |
2389 | ||
82e5c243 AC |
2390 | -- The subprogram body being processed is actually the proper body |
2391 | -- of a stub with a corresponding spec. The subprogram stub may | |
2392 | -- carry a postcondition pragma, in which case it must be taken | |
2393 | -- into account. The pragma appears after the stub. | |
879ac954 | 2394 | |
82e5c243 AC |
2395 | if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then |
2396 | Decl := Next (Corresponding_Stub (Unit_Decl)); | |
879ac954 AC |
2397 | while Present (Decl) loop |
2398 | ||
2399 | -- Note that non-matching pragmas are skipped | |
2400 | ||
2401 | if Nkind (Decl) = N_Pragma then | |
82e5c243 AC |
2402 | if Pragma_Name (Decl) = Post_Nam then |
2403 | Append_Enabled_Item | |
2404 | (Item => Build_Pragma_Check_Equivalent (Decl), | |
2405 | List => Stmts); | |
879ac954 AC |
2406 | end if; |
2407 | ||
2408 | -- Skip internally generated code | |
2409 | ||
2410 | elsif not Comes_From_Source (Decl) then | |
2411 | null; | |
2412 | ||
82e5c243 AC |
2413 | -- Postcondition pragmas are usually grouped together. There |
2414 | -- is no need to inspect the whole declarative list. | |
879ac954 AC |
2415 | |
2416 | else | |
2417 | exit; | |
2418 | end if; | |
2419 | ||
2420 | Next (Decl); | |
2421 | end loop; | |
2422 | end if; | |
82e5c243 | 2423 | end Process_Body_Postconditions; |
879ac954 | 2424 | |
82e5c243 AC |
2425 | --------------------------------- |
2426 | -- Process_Spec_Postconditions -- | |
2427 | --------------------------------- | |
879ac954 | 2428 | |
82e5c243 AC |
2429 | procedure Process_Spec_Postconditions is |
2430 | Subps : constant Subprogram_List := | |
2431 | Inherited_Subprograms (Spec_Id); | |
2432 | Items : Node_Id; | |
2433 | Prag : Node_Id; | |
2434 | Subp_Id : Entity_Id; | |
879ac954 | 2435 | |
82e5c243 AC |
2436 | begin |
2437 | -- Process the contract | |
a6363ed3 | 2438 | |
82e5c243 | 2439 | Items := Contract (Spec_Id); |
a6363ed3 | 2440 | |
82e5c243 AC |
2441 | if Present (Items) then |
2442 | Prag := Pre_Post_Conditions (Items); | |
2443 | while Present (Prag) loop | |
2444 | if Pragma_Name (Prag) = Name_Postcondition then | |
2445 | Append_Enabled_Item | |
2446 | (Item => Build_Pragma_Check_Equivalent (Prag), | |
2447 | List => Stmts); | |
2448 | end if; | |
a6363ed3 | 2449 | |
82e5c243 AC |
2450 | Prag := Next_Pragma (Prag); |
2451 | end loop; | |
2452 | end if; | |
a6363ed3 | 2453 | |
82e5c243 AC |
2454 | -- Process the contracts of all inherited subprograms, looking for |
2455 | -- class-wide postconditions. | |
07820c51 | 2456 | |
82e5c243 AC |
2457 | for Index in Subps'Range loop |
2458 | Subp_Id := Subps (Index); | |
2459 | Items := Contract (Subp_Id); | |
a6363ed3 | 2460 | |
82e5c243 AC |
2461 | if Present (Items) then |
2462 | Prag := Pre_Post_Conditions (Items); | |
2463 | while Present (Prag) loop | |
2464 | if Pragma_Name (Prag) = Name_Postcondition | |
2465 | and then Class_Present (Prag) | |
2466 | then | |
2467 | Append_Enabled_Item | |
2468 | (Item => | |
2469 | Build_Pragma_Check_Equivalent | |
2470 | (Prag => Prag, | |
2471 | Subp_Id => Spec_Id, | |
2472 | Inher_Id => Subp_Id), | |
2473 | List => Stmts); | |
2474 | end if; | |
a6363ed3 | 2475 | |
82e5c243 AC |
2476 | Prag := Next_Pragma (Prag); |
2477 | end loop; | |
a6363ed3 | 2478 | end if; |
879ac954 | 2479 | end loop; |
82e5c243 | 2480 | end Process_Spec_Postconditions; |
879ac954 | 2481 | |
82e5c243 | 2482 | -- Start of processing for Process_Postconditions |
879ac954 | 2483 | |
82e5c243 AC |
2484 | begin |
2485 | -- The processing of postconditions is done in reverse order (body | |
2486 | -- first) to ensure the following arrangement: | |
879ac954 | 2487 | |
82e5c243 AC |
2488 | -- <refined postconditions from body> |
2489 | -- <postconditions from body> | |
2490 | -- <postconditions from spec> | |
2491 | -- <inherited postconditions> | |
2492 | ||
2493 | Process_Body_Postconditions (Name_Refined_Post); | |
2494 | Process_Body_Postconditions (Name_Postcondition); | |
879ac954 AC |
2495 | |
2496 | if Present (Spec_Id) then | |
82e5c243 | 2497 | Process_Spec_Postconditions; |
879ac954 | 2498 | end if; |
82e5c243 | 2499 | end Process_Postconditions; |
879ac954 | 2500 | |
82e5c243 AC |
2501 | --------------------------- |
2502 | -- Process_Preconditions -- | |
2503 | --------------------------- | |
879ac954 | 2504 | |
82e5c243 AC |
2505 | procedure Process_Preconditions is |
2506 | Class_Pre : Node_Id := Empty; | |
2507 | -- The sole [inherited] class-wide precondition pragma that applies | |
2508 | -- to the subprogram. | |
879ac954 | 2509 | |
82e5c243 AC |
2510 | Insert_Node : Node_Id := Empty; |
2511 | -- The insertion node after which all pragma Check equivalents are | |
2512 | -- inserted. | |
879ac954 | 2513 | |
82e5c243 AC |
2514 | function Is_Prologue_Renaming (Decl : Node_Id) return Boolean; |
2515 | -- Determine whether arbitrary declaration Decl denotes a renaming of | |
2516 | -- a discriminant or protection field _object. | |
879ac954 | 2517 | |
82e5c243 AC |
2518 | procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); |
2519 | -- Merge two class-wide preconditions by "or else"-ing them. The | |
2520 | -- changes are accumulated in parameter Into. Update the error | |
2521 | -- message of Into. | |
879ac954 | 2522 | |
82e5c243 AC |
2523 | procedure Prepend_To_Decls (Item : Node_Id); |
2524 | -- Prepend a single item to the declarations of the subprogram body | |
879ac954 | 2525 | |
82e5c243 AC |
2526 | procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); |
2527 | -- Save a class-wide precondition into Class_Pre, or prepend a normal | |
2528 | -- precondition to the declarations of the body and analyze it. | |
879ac954 | 2529 | |
82e5c243 AC |
2530 | procedure Process_Inherited_Preconditions; |
2531 | -- Collect all inherited class-wide preconditions and merge them into | |
2532 | -- one big precondition to be evaluated as pragma Check. | |
879ac954 | 2533 | |
82e5c243 AC |
2534 | procedure Process_Preconditions_For (Subp_Id : Entity_Id); |
2535 | -- Collect all preconditions of subprogram Subp_Id and prepend their | |
2536 | -- pragma Check equivalents to the declarations of the body. | |
879ac954 | 2537 | |
82e5c243 AC |
2538 | -------------------------- |
2539 | -- Is_Prologue_Renaming -- | |
2540 | -------------------------- | |
879ac954 | 2541 | |
82e5c243 AC |
2542 | function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is |
2543 | Nam : Node_Id; | |
2544 | Obj : Entity_Id; | |
2545 | Pref : Node_Id; | |
2546 | Sel : Node_Id; | |
879ac954 | 2547 | |
82e5c243 AC |
2548 | begin |
2549 | if Nkind (Decl) = N_Object_Renaming_Declaration then | |
2550 | Obj := Defining_Entity (Decl); | |
2551 | Nam := Name (Decl); | |
879ac954 | 2552 | |
82e5c243 AC |
2553 | if Nkind (Nam) = N_Selected_Component then |
2554 | Pref := Prefix (Nam); | |
2555 | Sel := Selector_Name (Nam); | |
879ac954 | 2556 | |
82e5c243 AC |
2557 | -- A discriminant renaming appears as |
2558 | -- Discr : constant ... := Prefix.Discr; | |
879ac954 | 2559 | |
82e5c243 AC |
2560 | if Ekind (Obj) = E_Constant |
2561 | and then Is_Entity_Name (Sel) | |
2562 | and then Present (Entity (Sel)) | |
2563 | and then Ekind (Entity (Sel)) = E_Discriminant | |
2564 | then | |
2565 | return True; | |
879ac954 | 2566 | |
82e5c243 AC |
2567 | -- A protection field renaming appears as |
2568 | -- Prot : ... := _object._object; | |
879ac954 | 2569 | |
82e5c243 AC |
2570 | -- A renamed private component is just a component of |
2571 | -- _object, with an arbitrary name. | |
879ac954 | 2572 | |
82e5c243 AC |
2573 | elsif Ekind (Obj) = E_Variable |
2574 | and then Nkind (Pref) = N_Identifier | |
2575 | and then Chars (Pref) = Name_uObject | |
2576 | and then Nkind (Sel) = N_Identifier | |
2577 | then | |
2578 | return True; | |
2579 | end if; | |
2580 | end if; | |
2581 | end if; | |
879ac954 | 2582 | |
82e5c243 AC |
2583 | return False; |
2584 | end Is_Prologue_Renaming; | |
879ac954 | 2585 | |
82e5c243 AC |
2586 | ------------------------- |
2587 | -- Merge_Preconditions -- | |
2588 | ------------------------- | |
879ac954 | 2589 | |
82e5c243 AC |
2590 | procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is |
2591 | function Expression_Arg (Prag : Node_Id) return Node_Id; | |
2592 | -- Return the boolean expression argument of a precondition while | |
2593 | -- updating its parentheses count for the subsequent merge. | |
879ac954 | 2594 | |
82e5c243 AC |
2595 | function Message_Arg (Prag : Node_Id) return Node_Id; |
2596 | -- Return the message argument of a precondition | |
879ac954 | 2597 | |
82e5c243 AC |
2598 | -------------------- |
2599 | -- Expression_Arg -- | |
2600 | -------------------- | |
879ac954 | 2601 | |
82e5c243 AC |
2602 | function Expression_Arg (Prag : Node_Id) return Node_Id is |
2603 | Args : constant List_Id := Pragma_Argument_Associations (Prag); | |
2604 | Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); | |
879ac954 | 2605 | |
82e5c243 AC |
2606 | begin |
2607 | if Paren_Count (Arg) = 0 then | |
2608 | Set_Paren_Count (Arg, 1); | |
2609 | end if; | |
879ac954 | 2610 | |
82e5c243 AC |
2611 | return Arg; |
2612 | end Expression_Arg; | |
879ac954 | 2613 | |
82e5c243 AC |
2614 | ----------------- |
2615 | -- Message_Arg -- | |
2616 | ----------------- | |
879ac954 | 2617 | |
82e5c243 AC |
2618 | function Message_Arg (Prag : Node_Id) return Node_Id is |
2619 | Args : constant List_Id := Pragma_Argument_Associations (Prag); | |
2620 | begin | |
2621 | return Get_Pragma_Arg (Last (Args)); | |
2622 | end Message_Arg; | |
879ac954 | 2623 | |
82e5c243 | 2624 | -- Local variables |
879ac954 | 2625 | |
82e5c243 AC |
2626 | From_Expr : constant Node_Id := Expression_Arg (From); |
2627 | From_Msg : constant Node_Id := Message_Arg (From); | |
2628 | Into_Expr : constant Node_Id := Expression_Arg (Into); | |
2629 | Into_Msg : constant Node_Id := Message_Arg (Into); | |
2630 | Loc : constant Source_Ptr := Sloc (Into); | |
879ac954 | 2631 | |
82e5c243 | 2632 | -- Start of processing for Merge_Preconditions |
879ac954 | 2633 | |
82e5c243 AC |
2634 | begin |
2635 | -- Merge the two preconditions by "or else"-ing them | |
879ac954 | 2636 | |
82e5c243 AC |
2637 | Rewrite (Into_Expr, |
2638 | Make_Or_Else (Loc, | |
2639 | Right_Opnd => Relocate_Node (Into_Expr), | |
2640 | Left_Opnd => From_Expr)); | |
879ac954 | 2641 | |
82e5c243 AC |
2642 | -- Merge the two error messages to produce a single message of the |
2643 | -- form: | |
879ac954 | 2644 | |
82e5c243 AC |
2645 | -- failed precondition from ... |
2646 | -- also failed inherited precondition from ... | |
879ac954 | 2647 | |
82e5c243 AC |
2648 | if not Exception_Locations_Suppressed then |
2649 | Start_String (Strval (Into_Msg)); | |
2650 | Store_String_Char (ASCII.LF); | |
2651 | Store_String_Chars (" also "); | |
2652 | Store_String_Chars (Strval (From_Msg)); | |
879ac954 | 2653 | |
82e5c243 AC |
2654 | Set_Strval (Into_Msg, End_String); |
2655 | end if; | |
2656 | end Merge_Preconditions; | |
879ac954 | 2657 | |
82e5c243 AC |
2658 | ---------------------- |
2659 | -- Prepend_To_Decls -- | |
2660 | ---------------------- | |
879ac954 | 2661 | |
82e5c243 AC |
2662 | procedure Prepend_To_Decls (Item : Node_Id) is |
2663 | Decls : List_Id := Declarations (Body_Decl); | |
879ac954 | 2664 | |
82e5c243 AC |
2665 | begin |
2666 | -- Ensure that the body has a declarative list | |
879ac954 | 2667 | |
82e5c243 AC |
2668 | if No (Decls) then |
2669 | Decls := New_List; | |
2670 | Set_Declarations (Body_Decl, Decls); | |
879ac954 AC |
2671 | end if; |
2672 | ||
82e5c243 AC |
2673 | Prepend_To (Decls, Item); |
2674 | end Prepend_To_Decls; | |
879ac954 | 2675 | |
82e5c243 AC |
2676 | ------------------------------ |
2677 | -- Prepend_To_Decls_Or_Save -- | |
2678 | ------------------------------ | |
879ac954 | 2679 | |
82e5c243 AC |
2680 | procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is |
2681 | Check_Prag : Node_Id; | |
879ac954 | 2682 | |
82e5c243 AC |
2683 | begin |
2684 | Check_Prag := Build_Pragma_Check_Equivalent (Prag); | |
879ac954 | 2685 | |
82e5c243 AC |
2686 | -- Save the sole class-wide precondition (if any) for the next |
2687 | -- step, where it will be merged with inherited preconditions. | |
879ac954 | 2688 | |
82e5c243 AC |
2689 | if Class_Present (Prag) then |
2690 | pragma Assert (No (Class_Pre)); | |
2691 | Class_Pre := Check_Prag; | |
879ac954 | 2692 | |
82e5c243 AC |
2693 | -- Accumulate the corresponding Check pragmas at the top of the |
2694 | -- declarations. Prepending the items ensures that they will be | |
2695 | -- evaluated in their original order. | |
879ac954 | 2696 | |
82e5c243 AC |
2697 | else |
2698 | if Present (Insert_Node) then | |
2699 | Insert_After (Insert_Node, Check_Prag); | |
2700 | else | |
2701 | Prepend_To_Decls (Check_Prag); | |
2702 | end if; | |
879ac954 | 2703 | |
82e5c243 | 2704 | Analyze (Check_Prag); |
879ac954 | 2705 | end if; |
82e5c243 | 2706 | end Prepend_To_Decls_Or_Save; |
879ac954 | 2707 | |
82e5c243 AC |
2708 | ------------------------------------- |
2709 | -- Process_Inherited_Preconditions -- | |
2710 | ------------------------------------- | |
879ac954 | 2711 | |
82e5c243 AC |
2712 | procedure Process_Inherited_Preconditions is |
2713 | Subps : constant Subprogram_List := | |
2714 | Inherited_Subprograms (Spec_Id); | |
2715 | Check_Prag : Node_Id; | |
2716 | Items : Node_Id; | |
2717 | Prag : Node_Id; | |
2718 | Subp_Id : Entity_Id; | |
879ac954 | 2719 | |
82e5c243 AC |
2720 | begin |
2721 | -- Process the contracts of all inherited subprograms, looking for | |
2722 | -- class-wide preconditions. | |
879ac954 | 2723 | |
82e5c243 AC |
2724 | for Index in Subps'Range loop |
2725 | Subp_Id := Subps (Index); | |
2726 | Items := Contract (Subp_Id); | |
879ac954 | 2727 | |
82e5c243 AC |
2728 | if Present (Items) then |
2729 | Prag := Pre_Post_Conditions (Items); | |
2730 | while Present (Prag) loop | |
2731 | if Pragma_Name (Prag) = Name_Precondition | |
2732 | and then Class_Present (Prag) | |
2733 | then | |
2734 | Check_Prag := | |
2735 | Build_Pragma_Check_Equivalent | |
2736 | (Prag => Prag, | |
2737 | Subp_Id => Spec_Id, | |
2738 | Inher_Id => Subp_Id); | |
879ac954 | 2739 | |
82e5c243 AC |
2740 | -- The spec of an inherited subprogram already yielded |
2741 | -- a class-wide precondition. Merge the existing | |
2742 | -- precondition with the current one using "or else". | |
879ac954 | 2743 | |
82e5c243 AC |
2744 | if Present (Class_Pre) then |
2745 | Merge_Preconditions (Check_Prag, Class_Pre); | |
2746 | else | |
2747 | Class_Pre := Check_Prag; | |
2748 | end if; | |
2749 | end if; | |
879ac954 | 2750 | |
82e5c243 AC |
2751 | Prag := Next_Pragma (Prag); |
2752 | end loop; | |
2753 | end if; | |
2754 | end loop; | |
879ac954 | 2755 | |
82e5c243 | 2756 | -- Add the merged class-wide preconditions |
5f325af2 | 2757 | |
82e5c243 AC |
2758 | if Present (Class_Pre) then |
2759 | Prepend_To_Decls (Class_Pre); | |
2760 | Analyze (Class_Pre); | |
2761 | end if; | |
2762 | end Process_Inherited_Preconditions; | |
5f325af2 | 2763 | |
82e5c243 AC |
2764 | ------------------------------- |
2765 | -- Process_Preconditions_For -- | |
2766 | ------------------------------- | |
5f325af2 | 2767 | |
82e5c243 AC |
2768 | procedure Process_Preconditions_For (Subp_Id : Entity_Id) is |
2769 | Items : constant Node_Id := Contract (Subp_Id); | |
2770 | Decl : Node_Id; | |
2771 | Prag : Node_Id; | |
2772 | Subp_Decl : Node_Id; | |
5f325af2 | 2773 | |
82e5c243 AC |
2774 | begin |
2775 | -- Process the contract | |
5f325af2 | 2776 | |
82e5c243 AC |
2777 | if Present (Items) then |
2778 | Prag := Pre_Post_Conditions (Items); | |
2779 | while Present (Prag) loop | |
2780 | if Pragma_Name (Prag) = Name_Precondition then | |
2781 | Prepend_To_Decls_Or_Save (Prag); | |
2782 | end if; | |
5f325af2 | 2783 | |
82e5c243 AC |
2784 | Prag := Next_Pragma (Prag); |
2785 | end loop; | |
2786 | end if; | |
5f325af2 | 2787 | |
82e5c243 AC |
2788 | -- The subprogram declaration being processed is actually a body |
2789 | -- stub. The stub may carry a precondition pragma, in which case | |
2790 | -- it must be taken into account. The pragma appears after the | |
2791 | -- stub. | |
5f325af2 | 2792 | |
82e5c243 | 2793 | Subp_Decl := Unit_Declaration_Node (Subp_Id); |
5f325af2 | 2794 | |
82e5c243 | 2795 | if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then |
5f325af2 | 2796 | |
82e5c243 | 2797 | -- Inspect the declarations following the body stub |
5f325af2 | 2798 | |
82e5c243 AC |
2799 | Decl := Next (Subp_Decl); |
2800 | while Present (Decl) loop | |
5f325af2 | 2801 | |
82e5c243 | 2802 | -- Note that non-matching pragmas are skipped |
5f325af2 | 2803 | |
82e5c243 AC |
2804 | if Nkind (Decl) = N_Pragma then |
2805 | if Pragma_Name (Decl) = Name_Precondition then | |
2806 | Prepend_To_Decls_Or_Save (Decl); | |
2807 | end if; | |
5f325af2 | 2808 | |
82e5c243 | 2809 | -- Skip internally generated code |
5f325af2 | 2810 | |
82e5c243 AC |
2811 | elsif not Comes_From_Source (Decl) then |
2812 | null; | |
5f325af2 | 2813 | |
82e5c243 AC |
2814 | -- Preconditions are usually grouped together. There is no |
2815 | -- need to inspect the whole declarative list. | |
5f325af2 | 2816 | |
82e5c243 AC |
2817 | else |
2818 | exit; | |
2819 | end if; | |
5f325af2 | 2820 | |
82e5c243 AC |
2821 | Next (Decl); |
2822 | end loop; | |
2823 | end if; | |
2824 | end Process_Preconditions_For; | |
5f325af2 | 2825 | |
82e5c243 | 2826 | -- Local variables |
5f325af2 | 2827 | |
82e5c243 AC |
2828 | Decls : constant List_Id := Declarations (Body_Decl); |
2829 | Decl : Node_Id; | |
5f325af2 | 2830 | |
82e5c243 | 2831 | -- Start of processing for Process_Preconditions |
5f325af2 | 2832 | |
82e5c243 AC |
2833 | begin |
2834 | -- Find the proper insertion point for all pragma Check equivalents | |
5f325af2 | 2835 | |
82e5c243 AC |
2836 | if Present (Decls) then |
2837 | Decl := First (Decls); | |
2838 | while Present (Decl) loop | |
5f325af2 | 2839 | |
82e5c243 AC |
2840 | -- First source declaration terminates the search, because all |
2841 | -- preconditions must be evaluated prior to it, by definition. | |
5f325af2 | 2842 | |
82e5c243 AC |
2843 | if Comes_From_Source (Decl) then |
2844 | exit; | |
5f325af2 | 2845 | |
82e5c243 AC |
2846 | -- Certain internally generated object renamings such as those |
2847 | -- for discriminants and protection fields must be elaborated | |
2848 | -- before the preconditions are evaluated, as their expressions | |
2849 | -- may mention the discriminants. The renamings include those | |
2850 | -- for private components so we need to find the last such. | |
5f325af2 | 2851 | |
82e5c243 AC |
2852 | elsif Is_Prologue_Renaming (Decl) then |
2853 | while Present (Next (Decl)) | |
2854 | and then Is_Prologue_Renaming (Next (Decl)) | |
2855 | loop | |
2856 | Next (Decl); | |
2857 | end loop; | |
5f325af2 | 2858 | |
82e5c243 | 2859 | Insert_Node := Decl; |
5f325af2 | 2860 | |
82e5c243 AC |
2861 | -- Otherwise the declaration does not come from source. This |
2862 | -- also terminates the search, because internal code may raise | |
2863 | -- exceptions which should not preempt the preconditions. | |
5f325af2 | 2864 | |
82e5c243 AC |
2865 | else |
2866 | exit; | |
2867 | end if; | |
5f325af2 | 2868 | |
82e5c243 AC |
2869 | Next (Decl); |
2870 | end loop; | |
2871 | end if; | |
5f325af2 | 2872 | |
82e5c243 AC |
2873 | -- The processing of preconditions is done in reverse order (body |
2874 | -- first), because each pragma Check equivalent is inserted at the | |
2875 | -- top of the declarations. This ensures that the final order is | |
2876 | -- consistent with following diagram: | |
5f325af2 | 2877 | |
82e5c243 AC |
2878 | -- <inherited preconditions> |
2879 | -- <preconditions from spec> | |
2880 | -- <preconditions from body> | |
5f325af2 | 2881 | |
82e5c243 | 2882 | Process_Preconditions_For (Body_Id); |
5f325af2 | 2883 | |
82e5c243 AC |
2884 | if Present (Spec_Id) then |
2885 | Process_Preconditions_For (Spec_Id); | |
2886 | Process_Inherited_Preconditions; | |
2887 | end if; | |
2888 | end Process_Preconditions; | |
5f325af2 | 2889 | |
82e5c243 | 2890 | -- Local variables |
5f325af2 | 2891 | |
82e5c243 AC |
2892 | Restore_Scope : Boolean := False; |
2893 | Result : Entity_Id; | |
2894 | Stmts : List_Id := No_List; | |
2895 | Subp_Id : Entity_Id; | |
5f325af2 | 2896 | |
82e5c243 | 2897 | -- Start of processing for Expand_Subprogram_Contract |
5f325af2 | 2898 | |
82e5c243 AC |
2899 | begin |
2900 | -- Obtain the entity of the initial declaration | |
5f325af2 | 2901 | |
82e5c243 AC |
2902 | if Present (Spec_Id) then |
2903 | Subp_Id := Spec_Id; | |
2904 | else | |
2905 | Subp_Id := Body_Id; | |
2906 | end if; | |
5f325af2 | 2907 | |
82e5c243 | 2908 | -- Do not perform expansion activity when it is not needed |
5f325af2 | 2909 | |
82e5c243 AC |
2910 | if not Expander_Active then |
2911 | return; | |
5f325af2 | 2912 | |
82e5c243 | 2913 | -- ASIS requires an unaltered tree |
5f325af2 | 2914 | |
82e5c243 AC |
2915 | elsif ASIS_Mode then |
2916 | return; | |
5f325af2 | 2917 | |
82e5c243 | 2918 | -- GNATprove does not need the executable semantics of a contract |
5f325af2 | 2919 | |
82e5c243 AC |
2920 | elsif GNATprove_Mode then |
2921 | return; | |
5f325af2 | 2922 | |
82e5c243 AC |
2923 | -- The contract of a generic subprogram or one declared in a generic |
2924 | -- context is not expanded, as the corresponding instance will provide | |
2925 | -- the executable semantics of the contract. | |
5f325af2 | 2926 | |
82e5c243 AC |
2927 | elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then |
2928 | return; | |
5f325af2 | 2929 | |
82e5c243 AC |
2930 | -- All subprograms carry a contract, but for some it is not significant |
2931 | -- and should not be processed. This is a small optimization. | |
5f325af2 | 2932 | |
82e5c243 AC |
2933 | elsif not Has_Significant_Contract (Subp_Id) then |
2934 | return; | |
5f325af2 | 2935 | |
82e5c243 AC |
2936 | -- The contract of an ignored Ghost subprogram does not need expansion, |
2937 | -- because the subprogram and all calls to it will be removed. | |
5f325af2 | 2938 | |
82e5c243 AC |
2939 | elsif Is_Ignored_Ghost_Entity (Subp_Id) then |
2940 | return; | |
2941 | end if; | |
5f325af2 | 2942 | |
82e5c243 AC |
2943 | -- Do not re-expand the same contract. This scenario occurs when a |
2944 | -- construct is rewritten into something else during its analysis | |
2945 | -- (expression functions for instance). | |
5f325af2 | 2946 | |
82e5c243 AC |
2947 | if Has_Expanded_Contract (Subp_Id) then |
2948 | return; | |
5f325af2 | 2949 | |
82e5c243 | 2950 | -- Otherwise mark the subprogram |
5f325af2 | 2951 | |
82e5c243 AC |
2952 | else |
2953 | Set_Has_Expanded_Contract (Subp_Id); | |
2954 | end if; | |
5f325af2 | 2955 | |
82e5c243 AC |
2956 | -- Ensure that the formal parameters are visible when expanding all |
2957 | -- contract items. | |
5f325af2 | 2958 | |
82e5c243 AC |
2959 | if not In_Open_Scopes (Subp_Id) then |
2960 | Restore_Scope := True; | |
2961 | Push_Scope (Subp_Id); | |
5f325af2 | 2962 | |
82e5c243 AC |
2963 | if Is_Generic_Subprogram (Subp_Id) then |
2964 | Install_Generic_Formals (Subp_Id); | |
2965 | else | |
2966 | Install_Formals (Subp_Id); | |
2967 | end if; | |
2968 | end if; | |
5f325af2 | 2969 | |
82e5c243 AC |
2970 | -- The expansion of a subprogram contract involves the creation of Check |
2971 | -- pragmas to verify the contract assertions of the spec and body in a | |
2972 | -- particular order. The order is as follows: | |
5f325af2 | 2973 | |
82e5c243 AC |
2974 | -- function Example (...) return ... is |
2975 | -- procedure _Postconditions (...) is | |
2976 | -- begin | |
2977 | -- <refined postconditions from body> | |
2978 | -- <postconditions from body> | |
2979 | -- <postconditions from spec> | |
2980 | -- <inherited postconditions> | |
2981 | -- <contract case consequences> | |
2982 | -- <invariant check of function result> | |
2983 | -- <invariant and predicate checks of parameters> | |
2984 | -- end _Postconditions; | |
5f325af2 | 2985 | |
82e5c243 AC |
2986 | -- <inherited preconditions> |
2987 | -- <preconditions from spec> | |
2988 | -- <preconditions from body> | |
2989 | -- <contract case conditions> | |
5f325af2 | 2990 | |
82e5c243 AC |
2991 | -- <source declarations> |
2992 | -- begin | |
2993 | -- <source statements> | |
5f325af2 | 2994 | |
82e5c243 AC |
2995 | -- _Preconditions (Result); |
2996 | -- return Result; | |
2997 | -- end Example; | |
5f325af2 | 2998 | |
82e5c243 AC |
2999 | -- Routine _Postconditions holds all contract assertions that must be |
3000 | -- verified on exit from the related subprogram. | |
5f325af2 | 3001 | |
82e5c243 AC |
3002 | -- Step 1: Handle all preconditions. This action must come before the |
3003 | -- processing of pragma Contract_Cases because the pragma prepends items | |
3004 | -- to the body declarations. | |
5f325af2 | 3005 | |
82e5c243 AC |
3006 | Process_Preconditions; |
3007 | ||
3008 | -- Step 2: Handle all postconditions. This action must come before the | |
3009 | -- processing of pragma Contract_Cases because the pragma appends items | |
3010 | -- to list Stmts. | |
5f325af2 | 3011 | |
82e5c243 | 3012 | Process_Postconditions (Stmts); |
5f325af2 | 3013 | |
82e5c243 AC |
3014 | -- Step 3: Handle pragma Contract_Cases. This action must come before |
3015 | -- the processing of invariants and predicates because those append | |
3016 | -- items to list Stmts. | |
5f325af2 | 3017 | |
82e5c243 | 3018 | Process_Contract_Cases (Stmts); |
5f325af2 | 3019 | |
82e5c243 AC |
3020 | -- Step 4: Apply invariant and predicate checks on a function result and |
3021 | -- all formals. The resulting checks are accumulated in list Stmts. | |
5f325af2 | 3022 | |
82e5c243 | 3023 | Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); |
5f325af2 | 3024 | |
82e5c243 | 3025 | -- Step 5: Construct procedure _Postconditions |
5f325af2 | 3026 | |
82e5c243 | 3027 | Build_Postconditions_Procedure (Subp_Id, Stmts, Result); |
5f325af2 | 3028 | |
82e5c243 AC |
3029 | if Restore_Scope then |
3030 | End_Scope; | |
3031 | end if; | |
3032 | end Expand_Subprogram_Contract; | |
5f325af2 | 3033 | |
82e5c243 AC |
3034 | --------------------------------- |
3035 | -- Inherit_Subprogram_Contract -- | |
3036 | --------------------------------- | |
5f325af2 | 3037 | |
82e5c243 AC |
3038 | procedure Inherit_Subprogram_Contract |
3039 | (Subp : Entity_Id; | |
3040 | From_Subp : Entity_Id) | |
3041 | is | |
3042 | procedure Inherit_Pragma (Prag_Id : Pragma_Id); | |
3043 | -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to | |
3044 | -- Subp's contract. | |
5f325af2 | 3045 | |
82e5c243 AC |
3046 | -------------------- |
3047 | -- Inherit_Pragma -- | |
3048 | -------------------- | |
5f325af2 | 3049 | |
82e5c243 AC |
3050 | procedure Inherit_Pragma (Prag_Id : Pragma_Id) is |
3051 | Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); | |
3052 | New_Prag : Node_Id; | |
5f325af2 | 3053 | |
82e5c243 AC |
3054 | begin |
3055 | -- A pragma cannot be part of more than one First_Pragma/Next_Pragma | |
3056 | -- chains, therefore the node must be replicated. The new pragma is | |
3057 | -- flagged as inherited for distinction purposes. | |
5f325af2 | 3058 | |
82e5c243 AC |
3059 | if Present (Prag) then |
3060 | New_Prag := New_Copy_Tree (Prag); | |
3061 | Set_Is_Inherited_Pragma (New_Prag); | |
5f325af2 | 3062 | |
82e5c243 | 3063 | Add_Contract_Item (New_Prag, Subp); |
5f325af2 | 3064 | end if; |
82e5c243 | 3065 | end Inherit_Pragma; |
5f325af2 | 3066 | |
82e5c243 | 3067 | -- Start of processing for Inherit_Subprogram_Contract |
5f325af2 | 3068 | |
82e5c243 AC |
3069 | begin |
3070 | -- Inheritance is carried out only when both entities are subprograms | |
3071 | -- with contracts. | |
5f325af2 | 3072 | |
82e5c243 AC |
3073 | if Is_Subprogram_Or_Generic_Subprogram (Subp) |
3074 | and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) | |
3075 | and then Present (Contract (From_Subp)) | |
3076 | then | |
3077 | Inherit_Pragma (Pragma_Extensions_Visible); | |
3078 | end if; | |
3079 | end Inherit_Subprogram_Contract; | |
5f325af2 | 3080 | |
82e5c243 AC |
3081 | ------------------------------------- |
3082 | -- Instantiate_Subprogram_Contract -- | |
3083 | ------------------------------------- | |
5f325af2 | 3084 | |
82e5c243 AC |
3085 | procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is |
3086 | procedure Instantiate_Pragmas (First_Prag : Node_Id); | |
3087 | -- Instantiate all contract-related source pragmas found in the list, | |
3088 | -- starting with pragma First_Prag. Each instantiated pragma is added | |
3089 | -- to list L. | |
5f325af2 | 3090 | |
82e5c243 AC |
3091 | ------------------------- |
3092 | -- Instantiate_Pragmas -- | |
3093 | ------------------------- | |
5f325af2 | 3094 | |
82e5c243 AC |
3095 | procedure Instantiate_Pragmas (First_Prag : Node_Id) is |
3096 | Inst_Prag : Node_Id; | |
3097 | Prag : Node_Id; | |
5f325af2 | 3098 | |
82e5c243 AC |
3099 | begin |
3100 | Prag := First_Prag; | |
3101 | while Present (Prag) loop | |
3102 | if Is_Generic_Contract_Pragma (Prag) then | |
3103 | Inst_Prag := | |
3104 | Copy_Generic_Node (Prag, Empty, Instantiating => True); | |
5f325af2 | 3105 | |
82e5c243 AC |
3106 | Set_Analyzed (Inst_Prag, False); |
3107 | Append_To (L, Inst_Prag); | |
3108 | end if; | |
5f325af2 | 3109 | |
82e5c243 AC |
3110 | Prag := Next_Pragma (Prag); |
3111 | end loop; | |
3112 | end Instantiate_Pragmas; | |
5f325af2 | 3113 | |
82e5c243 | 3114 | -- Local variables |
5f325af2 | 3115 | |
82e5c243 | 3116 | Items : constant Node_Id := Contract (Defining_Entity (Templ)); |
5f325af2 | 3117 | |
82e5c243 | 3118 | -- Start of processing for Instantiate_Subprogram_Contract |
5f325af2 | 3119 | |
82e5c243 AC |
3120 | begin |
3121 | if Present (Items) then | |
3122 | Instantiate_Pragmas (Pre_Post_Conditions (Items)); | |
3123 | Instantiate_Pragmas (Contract_Test_Cases (Items)); | |
3124 | Instantiate_Pragmas (Classifications (Items)); | |
3125 | end if; | |
3126 | end Instantiate_Subprogram_Contract; | |
5f325af2 | 3127 | |
82e5c243 AC |
3128 | ---------------------------------------- |
3129 | -- Save_Global_References_In_Contract -- | |
3130 | ---------------------------------------- | |
5f325af2 | 3131 | |
82e5c243 AC |
3132 | procedure Save_Global_References_In_Contract |
3133 | (Templ : Node_Id; | |
3134 | Gen_Id : Entity_Id) | |
3135 | is | |
3136 | procedure Save_Global_References_In_List (First_Prag : Node_Id); | |
3137 | -- Save all global references in contract-related source pragmas found | |
3138 | -- in the list, starting with pragma First_Prag. | |
5f325af2 | 3139 | |
82e5c243 AC |
3140 | ------------------------------------ |
3141 | -- Save_Global_References_In_List -- | |
3142 | ------------------------------------ | |
5f325af2 | 3143 | |
82e5c243 AC |
3144 | procedure Save_Global_References_In_List (First_Prag : Node_Id) is |
3145 | Prag : Node_Id; | |
5f325af2 | 3146 | |
5f325af2 | 3147 | begin |
82e5c243 AC |
3148 | Prag := First_Prag; |
3149 | while Present (Prag) loop | |
3150 | if Is_Generic_Contract_Pragma (Prag) then | |
3151 | Save_Global_References (Prag); | |
3152 | end if; | |
3153 | ||
3154 | Prag := Next_Pragma (Prag); | |
3155 | end loop; | |
3156 | end Save_Global_References_In_List; | |
5f325af2 AC |
3157 | |
3158 | -- Local variables | |
3159 | ||
82e5c243 | 3160 | Items : constant Node_Id := Contract (Defining_Entity (Templ)); |
5f325af2 | 3161 | |
82e5c243 | 3162 | -- Start of processing for Save_Global_References_In_Contract |
5f325af2 AC |
3163 | |
3164 | begin | |
82e5c243 AC |
3165 | -- The entity of the analyzed generic copy must be on the scope stack |
3166 | -- to ensure proper detection of global references. | |
3167 | ||
3168 | Push_Scope (Gen_Id); | |
3169 | ||
3170 | if Permits_Aspect_Specifications (Templ) | |
3171 | and then Has_Aspects (Templ) | |
3172 | then | |
3173 | Save_Global_References_In_Aspects (Templ); | |
3174 | end if; | |
3175 | ||
3176 | if Present (Items) then | |
3177 | Save_Global_References_In_List (Pre_Post_Conditions (Items)); | |
3178 | Save_Global_References_In_List (Contract_Test_Cases (Items)); | |
3179 | Save_Global_References_In_List (Classifications (Items)); | |
3180 | end if; | |
3181 | ||
3182 | Pop_Scope; | |
3183 | end Save_Global_References_In_Contract; | |
5f325af2 | 3184 | |
879ac954 | 3185 | end Contracts; |