]>
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 | -- -- | |
9 | -- Copyright (C) 2015, Free Software Foundation, Inc. -- | |
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; | |
28 | with Einfo; use Einfo; | |
29 | with Elists; use Elists; | |
30 | with Errout; use Errout; | |
31 | with Exp_Prag; use Exp_Prag; | |
32 | with Exp_Tss; use Exp_Tss; | |
33 | with Exp_Util; use Exp_Util; | |
34 | with Namet; use Namet; | |
35 | with Nlists; use Nlists; | |
36 | with Nmake; use Nmake; | |
37 | with Opt; use Opt; | |
38 | with Sem; use Sem; | |
39 | with Sem_Aux; use Sem_Aux; | |
40 | with Sem_Ch6; use Sem_Ch6; | |
41 | with Sem_Ch8; use Sem_Ch8; | |
42 | with Sem_Ch12; use Sem_Ch12; | |
43 | with Sem_Disp; use Sem_Disp; | |
44 | with Sem_Prag; use Sem_Prag; | |
45 | with Sem_Util; use Sem_Util; | |
46 | with Sinfo; use Sinfo; | |
47 | with Snames; use Snames; | |
48 | with Stringt; use Stringt; | |
49 | with Tbuild; use Tbuild; | |
50 | ||
51 | package body Contracts is | |
52 | ||
53 | procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); | |
54 | -- Expand the contracts of a subprogram body and its correspoding spec (if | |
55 | -- any). This routine processes all [refined] pre- and postconditions as | |
56 | -- well as Contract_Cases, invariants and predicates. Body_Id denotes the | |
57 | -- entity of the subprogram body. | |
58 | ||
59 | ----------------------- | |
60 | -- Add_Contract_Item -- | |
61 | ----------------------- | |
62 | ||
63 | procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is | |
64 | Items : Node_Id := Contract (Id); | |
65 | ||
66 | procedure Add_Classification; | |
67 | -- Prepend Prag to the list of classifications | |
68 | ||
69 | procedure Add_Contract_Test_Case; | |
70 | -- Prepend Prag to the list of contract and test cases | |
71 | ||
72 | procedure Add_Pre_Post_Condition; | |
73 | -- Prepend Prag to the list of pre- and postconditions | |
74 | ||
75 | ------------------------ | |
76 | -- Add_Classification -- | |
77 | ------------------------ | |
78 | ||
79 | procedure Add_Classification is | |
80 | begin | |
81 | Set_Next_Pragma (Prag, Classifications (Items)); | |
82 | Set_Classifications (Items, Prag); | |
83 | end Add_Classification; | |
84 | ||
85 | ---------------------------- | |
86 | -- Add_Contract_Test_Case -- | |
87 | ---------------------------- | |
88 | ||
89 | procedure Add_Contract_Test_Case is | |
90 | begin | |
91 | Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); | |
92 | Set_Contract_Test_Cases (Items, Prag); | |
93 | end Add_Contract_Test_Case; | |
94 | ||
95 | ---------------------------- | |
96 | -- Add_Pre_Post_Condition -- | |
97 | ---------------------------- | |
98 | ||
99 | procedure Add_Pre_Post_Condition is | |
100 | begin | |
101 | Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); | |
102 | Set_Pre_Post_Conditions (Items, Prag); | |
103 | end Add_Pre_Post_Condition; | |
104 | ||
105 | -- Local variables | |
106 | ||
107 | Prag_Nam : Name_Id; | |
108 | ||
109 | -- Start of processing for Add_Contract_Item | |
110 | ||
111 | begin | |
112 | -- A contract must contain only pragmas | |
113 | ||
114 | pragma Assert (Nkind (Prag) = N_Pragma); | |
115 | Prag_Nam := Pragma_Name (Prag); | |
116 | ||
117 | -- Create a new contract when adding the first item | |
118 | ||
119 | if No (Items) then | |
120 | Items := Make_Contract (Sloc (Id)); | |
121 | Set_Contract (Id, Items); | |
122 | end if; | |
123 | ||
124 | -- Contract items related to constants. Applicable pragmas are: | |
125 | -- Part_Of | |
126 | ||
127 | if Ekind (Id) = E_Constant then | |
128 | if Prag_Nam = Name_Part_Of then | |
129 | Add_Classification; | |
130 | ||
131 | -- The pragma is not a proper contract item | |
132 | ||
133 | else | |
134 | raise Program_Error; | |
135 | end if; | |
136 | ||
137 | -- Contract items related to [generic] packages or instantiations. The | |
138 | -- applicable pragmas are: | |
139 | -- Abstract_States | |
140 | -- Initial_Condition | |
141 | -- Initializes | |
142 | -- Part_Of (instantiation only) | |
143 | ||
144 | elsif Ekind_In (Id, E_Generic_Package, E_Package) then | |
145 | if Nam_In (Prag_Nam, Name_Abstract_State, | |
146 | Name_Initial_Condition, | |
147 | Name_Initializes) | |
148 | then | |
149 | Add_Classification; | |
150 | ||
151 | -- Indicator Part_Of must be associated with a package instantiation | |
152 | ||
153 | elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then | |
154 | Add_Classification; | |
155 | ||
156 | -- The pragma is not a proper contract item | |
157 | ||
158 | else | |
159 | raise Program_Error; | |
160 | end if; | |
161 | ||
162 | -- Contract items related to package bodies. The applicable pragmas are: | |
163 | -- Refined_States | |
164 | ||
165 | elsif Ekind (Id) = E_Package_Body then | |
166 | if Prag_Nam = Name_Refined_State then | |
167 | Add_Classification; | |
168 | ||
169 | -- The pragma is not a proper contract item | |
170 | ||
171 | else | |
172 | raise Program_Error; | |
173 | end if; | |
174 | ||
175 | -- Contract items related to subprogram or entry declarations. The | |
176 | -- applicable pragmas are: | |
177 | -- Contract_Cases | |
178 | -- Depends | |
179 | -- Extensions_Visible | |
180 | -- Global | |
181 | -- Postcondition | |
182 | -- Precondition | |
183 | -- Test_Case | |
184 | -- Volatile_Function | |
185 | ||
186 | elsif Ekind_In (Id, E_Entry, E_Entry_Family) | |
187 | or else Is_Generic_Subprogram (Id) | |
188 | or else Is_Subprogram (Id) | |
189 | then | |
190 | if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then | |
191 | Add_Pre_Post_Condition; | |
192 | ||
193 | elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then | |
194 | Add_Contract_Test_Case; | |
195 | ||
196 | elsif Nam_In (Prag_Nam, Name_Depends, | |
197 | Name_Extensions_Visible, | |
198 | Name_Global) | |
199 | then | |
200 | Add_Classification; | |
201 | ||
202 | elsif Prag_Nam = Name_Volatile_Function | |
203 | and then Ekind_In (Id, E_Function, E_Generic_Function) | |
204 | then | |
205 | Add_Classification; | |
206 | ||
207 | -- The pragma is not a proper contract item | |
208 | ||
209 | else | |
210 | raise Program_Error; | |
211 | end if; | |
212 | ||
213 | -- Contract items related to subprogram bodies. Applicable pragmas are: | |
214 | -- Postcondition | |
215 | -- Precondition | |
216 | -- Refined_Depends | |
217 | -- Refined_Global | |
218 | -- Refined_Post | |
219 | ||
220 | elsif Ekind (Id) = E_Subprogram_Body then | |
221 | if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then | |
222 | Add_Classification; | |
223 | ||
224 | elsif Nam_In (Prag_Nam, Name_Postcondition, | |
225 | Name_Precondition, | |
226 | Name_Refined_Post) | |
227 | then | |
228 | Add_Pre_Post_Condition; | |
229 | ||
230 | -- The pragma is not a proper contract item | |
231 | ||
232 | else | |
233 | raise Program_Error; | |
234 | end if; | |
235 | ||
236 | -- Contract items related to variables. Applicable pragmas are: | |
237 | -- Async_Readers | |
238 | -- Async_Writers | |
239 | -- Constant_After_Elaboration | |
240 | -- Effective_Reads | |
241 | -- Effective_Writes | |
242 | -- Part_Of | |
243 | ||
244 | elsif Ekind (Id) = E_Variable then | |
245 | if Nam_In (Prag_Nam, Name_Async_Readers, | |
246 | Name_Async_Writers, | |
247 | Name_Constant_After_Elaboration, | |
248 | Name_Effective_Reads, | |
249 | Name_Effective_Writes, | |
250 | Name_Part_Of) | |
251 | then | |
252 | Add_Classification; | |
253 | ||
254 | -- The pragma is not a proper contract item | |
255 | ||
256 | else | |
257 | raise Program_Error; | |
258 | end if; | |
259 | end if; | |
260 | end Add_Contract_Item; | |
261 | ||
262 | --------------------------------------------- | |
263 | -- Analyze_Enclosing_Package_Body_Contract -- | |
264 | --------------------------------------------- | |
265 | ||
266 | procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id) is | |
267 | Par : Node_Id; | |
268 | ||
269 | begin | |
270 | -- Climb the parent chain looking for an enclosing body. Do not use the | |
e96b7045 | 271 | -- scope stack, as a body uses the entity of its corresponding spec. |
879ac954 AC |
272 | |
273 | Par := Parent (Body_Decl); | |
274 | while Present (Par) loop | |
275 | if Nkind (Par) = N_Package_Body then | |
276 | Analyze_Package_Body_Contract | |
277 | (Body_Id => Defining_Entity (Par), | |
278 | Freeze_Id => Defining_Entity (Body_Decl)); | |
279 | ||
280 | return; | |
281 | end if; | |
282 | ||
283 | Par := Parent (Par); | |
284 | end loop; | |
285 | end Analyze_Enclosing_Package_Body_Contract; | |
286 | ||
287 | ----------------------------- | |
288 | -- Analyze_Object_Contract -- | |
289 | ----------------------------- | |
290 | ||
291 | procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is | |
292 | Obj_Typ : constant Entity_Id := Etype (Obj_Id); | |
293 | AR_Val : Boolean := False; | |
294 | AW_Val : Boolean := False; | |
295 | ER_Val : Boolean := False; | |
296 | EW_Val : Boolean := False; | |
297 | Items : Node_Id; | |
298 | Prag : Node_Id; | |
299 | Seen : Boolean := False; | |
300 | ||
301 | begin | |
302 | -- The loop parameter in an element iterator over a formal container | |
e96b7045 | 303 | -- is declared with an object declaration, but no contracts apply. |
879ac954 AC |
304 | |
305 | if Ekind (Obj_Id) = E_Loop_Parameter then | |
306 | return; | |
307 | end if; | |
308 | ||
e96b7045 | 309 | -- Do not analyze a contract multiple times |
879ac954 AC |
310 | |
311 | Items := Contract (Obj_Id); | |
312 | ||
313 | if Present (Items) then | |
314 | if Analyzed (Items) then | |
315 | return; | |
316 | else | |
317 | Set_Analyzed (Items); | |
318 | end if; | |
319 | end if; | |
320 | ||
e96b7045 | 321 | -- Constant-related checks |
879ac954 AC |
322 | |
323 | if Ekind (Obj_Id) = E_Constant then | |
324 | ||
325 | -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)). | |
e96b7045 AC |
326 | -- This check is relevant only when SPARK_Mode is on, as it is not |
327 | -- a standard Ada legality rule. Internally-generated constants that | |
879ac954 AC |
328 | -- map generic formals to actuals in instantiations are allowed to |
329 | -- be volatile. | |
330 | ||
331 | if SPARK_Mode = On | |
332 | and then Comes_From_Source (Obj_Id) | |
333 | and then Is_Effectively_Volatile (Obj_Id) | |
334 | and then No (Corresponding_Generic_Association (Parent (Obj_Id))) | |
335 | then | |
336 | Error_Msg_N ("constant cannot be volatile", Obj_Id); | |
337 | end if; | |
338 | ||
e96b7045 | 339 | -- Variable-related checks |
879ac954 AC |
340 | |
341 | else pragma Assert (Ekind (Obj_Id) = E_Variable); | |
342 | ||
e96b7045 | 343 | -- The following checks are relevant only when SPARK_Mode is on, as |
879ac954 AC |
344 | -- they are not standard Ada legality rules. Internally generated |
345 | -- temporaries are ignored. | |
346 | ||
347 | if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then | |
348 | if Is_Effectively_Volatile (Obj_Id) then | |
349 | ||
350 | -- The declaration of an effectively volatile object must | |
351 | -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). | |
352 | ||
353 | if not Is_Library_Level_Entity (Obj_Id) then | |
354 | Error_Msg_N | |
355 | ("volatile variable & must be declared at library level", | |
356 | Obj_Id); | |
357 | ||
358 | -- An object of a discriminated type cannot be effectively | |
359 | -- volatile except for protected objects (SPARK RM 7.1.3(5)). | |
360 | ||
361 | elsif Has_Discriminants (Obj_Typ) | |
362 | and then not Is_Protected_Type (Obj_Typ) | |
363 | then | |
364 | Error_Msg_N | |
365 | ("discriminated object & cannot be volatile", Obj_Id); | |
366 | ||
367 | -- An object of a tagged type cannot be effectively volatile | |
368 | -- (SPARK RM C.6(5)). | |
369 | ||
370 | elsif Is_Tagged_Type (Obj_Typ) then | |
371 | Error_Msg_N ("tagged object & cannot be volatile", Obj_Id); | |
372 | end if; | |
373 | ||
374 | -- The object is not effectively volatile | |
375 | ||
376 | else | |
377 | -- A non-effectively volatile object cannot have effectively | |
378 | -- volatile components (SPARK RM 7.1.3(6)). | |
379 | ||
380 | if not Is_Effectively_Volatile (Obj_Id) | |
381 | and then Has_Volatile_Component (Obj_Typ) | |
382 | then | |
383 | Error_Msg_N | |
384 | ("non-volatile object & cannot have volatile components", | |
385 | Obj_Id); | |
386 | end if; | |
387 | end if; | |
388 | end if; | |
389 | ||
390 | if Is_Ghost_Entity (Obj_Id) then | |
391 | ||
392 | -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8)) | |
393 | ||
394 | if Is_Effectively_Volatile (Obj_Id) then | |
395 | Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id); | |
396 | ||
397 | -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)) | |
398 | ||
399 | elsif Is_Imported (Obj_Id) then | |
400 | Error_Msg_N ("ghost object & cannot be imported", Obj_Id); | |
401 | ||
402 | elsif Is_Exported (Obj_Id) then | |
403 | Error_Msg_N ("ghost object & cannot be exported", Obj_Id); | |
404 | end if; | |
405 | end if; | |
406 | ||
407 | -- Analyze all external properties | |
408 | ||
409 | Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); | |
410 | ||
411 | if Present (Prag) then | |
412 | Analyze_External_Property_In_Decl_Part (Prag, AR_Val); | |
413 | Seen := True; | |
414 | end if; | |
415 | ||
416 | Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); | |
417 | ||
418 | if Present (Prag) then | |
419 | Analyze_External_Property_In_Decl_Part (Prag, AW_Val); | |
420 | Seen := True; | |
421 | end if; | |
422 | ||
423 | Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); | |
424 | ||
425 | if Present (Prag) then | |
426 | Analyze_External_Property_In_Decl_Part (Prag, ER_Val); | |
427 | Seen := True; | |
428 | end if; | |
429 | ||
430 | Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); | |
431 | ||
432 | if Present (Prag) then | |
433 | Analyze_External_Property_In_Decl_Part (Prag, EW_Val); | |
434 | Seen := True; | |
435 | end if; | |
436 | ||
437 | -- Verify the mutual interaction of the various external properties | |
438 | ||
439 | if Seen then | |
440 | Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); | |
441 | end if; | |
442 | end if; | |
443 | ||
444 | -- Check whether the lack of indicator Part_Of agrees with the placement | |
445 | -- of the object with respect to the state space. | |
446 | ||
447 | Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); | |
448 | ||
449 | if No (Prag) then | |
450 | Check_Missing_Part_Of (Obj_Id); | |
451 | end if; | |
452 | ||
453 | -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One | |
454 | -- exception to this is the object that represents the dispatch table of | |
e96b7045 | 455 | -- a Ghost tagged type, as the symbol needs to be exported. |
879ac954 AC |
456 | |
457 | if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then | |
458 | if Is_Exported (Obj_Id) then | |
459 | Error_Msg_N ("ghost object & cannot be exported", Obj_Id); | |
460 | ||
461 | elsif Is_Imported (Obj_Id) then | |
462 | Error_Msg_N ("ghost object & cannot be imported", Obj_Id); | |
463 | end if; | |
464 | end if; | |
465 | end Analyze_Object_Contract; | |
466 | ||
467 | ----------------------------------- | |
468 | -- Analyze_Package_Body_Contract -- | |
469 | ----------------------------------- | |
470 | ||
471 | procedure Analyze_Package_Body_Contract | |
472 | (Body_Id : Entity_Id; | |
473 | Freeze_Id : Entity_Id := Empty) | |
474 | is | |
475 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
476 | Items : constant Node_Id := Contract (Body_Id); | |
477 | Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); | |
478 | Mode : SPARK_Mode_Type; | |
479 | Ref_State : Node_Id; | |
480 | ||
481 | begin | |
e96b7045 | 482 | -- Do not analyze a contract multiple times |
879ac954 AC |
483 | |
484 | if Present (Items) then | |
485 | if Analyzed (Items) then | |
486 | return; | |
487 | else | |
488 | Set_Analyzed (Items); | |
489 | end if; | |
490 | end if; | |
491 | ||
492 | -- Due to the timing of contract analysis, delayed pragmas may be | |
493 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
494 | -- context. To remedy this, restore the original SPARK_Mode of the | |
495 | -- related package body. | |
496 | ||
497 | Save_SPARK_Mode_And_Set (Body_Id, Mode); | |
498 | ||
499 | Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State); | |
500 | ||
501 | -- The analysis of pragma Refined_State detects whether the spec has | |
502 | -- abstract states available for refinement. | |
503 | ||
504 | if Present (Ref_State) then | |
505 | Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id); | |
506 | ||
507 | -- State refinement is required when the package declaration defines at | |
508 | -- least one abstract state. Null states are not considered. Refinement | |
e96b7045 | 509 | -- is not enforced when SPARK checks are turned off. |
879ac954 AC |
510 | |
511 | elsif SPARK_Mode /= Off | |
512 | and then Requires_State_Refinement (Spec_Id, Body_Id) | |
513 | then | |
514 | Error_Msg_N ("package & requires state refinement", Spec_Id); | |
515 | end if; | |
516 | ||
517 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
518 | -- pragmas have been analyzed. | |
519 | ||
520 | Restore_SPARK_Mode (Mode); | |
521 | ||
522 | -- Capture all global references in a generic package body now that the | |
523 | -- contract has been analyzed. | |
524 | ||
525 | if Is_Generic_Declaration_Or_Body (Body_Decl) then | |
526 | Save_Global_References_In_Contract | |
527 | (Templ => Original_Node (Body_Decl), | |
528 | Gen_Id => Spec_Id); | |
529 | end if; | |
530 | end Analyze_Package_Body_Contract; | |
531 | ||
532 | ------------------------------ | |
533 | -- Analyze_Package_Contract -- | |
534 | ------------------------------ | |
535 | ||
536 | procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is | |
537 | Items : constant Node_Id := Contract (Pack_Id); | |
538 | Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id); | |
539 | Init : Node_Id := Empty; | |
540 | Init_Cond : Node_Id := Empty; | |
541 | Mode : SPARK_Mode_Type; | |
542 | Prag : Node_Id; | |
543 | Prag_Nam : Name_Id; | |
544 | ||
545 | begin | |
e96b7045 | 546 | -- Do not analyze a contract multiple times |
879ac954 AC |
547 | |
548 | if Present (Items) then | |
549 | if Analyzed (Items) then | |
550 | return; | |
551 | else | |
552 | Set_Analyzed (Items); | |
553 | end if; | |
554 | end if; | |
555 | ||
556 | -- Due to the timing of contract analysis, delayed pragmas may be | |
557 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
558 | -- context. To remedy this, restore the original SPARK_Mode of the | |
559 | -- related package. | |
560 | ||
561 | Save_SPARK_Mode_And_Set (Pack_Id, Mode); | |
562 | ||
563 | if Present (Items) then | |
564 | ||
e96b7045 | 565 | -- Locate and store pragmas Initial_Condition and Initializes, since |
879ac954 AC |
566 | -- their order of analysis matters. |
567 | ||
568 | Prag := Classifications (Items); | |
569 | while Present (Prag) loop | |
570 | Prag_Nam := Pragma_Name (Prag); | |
571 | ||
572 | if Prag_Nam = Name_Initial_Condition then | |
573 | Init_Cond := Prag; | |
574 | ||
575 | elsif Prag_Nam = Name_Initializes then | |
576 | Init := Prag; | |
577 | end if; | |
578 | ||
579 | Prag := Next_Pragma (Prag); | |
580 | end loop; | |
581 | ||
e96b7045 | 582 | -- Analyze the initialization-related pragmas. Initializes must come |
879ac954 AC |
583 | -- before Initial_Condition due to item dependencies. |
584 | ||
585 | if Present (Init) then | |
586 | Analyze_Initializes_In_Decl_Part (Init); | |
587 | end if; | |
588 | ||
589 | if Present (Init_Cond) then | |
590 | Analyze_Initial_Condition_In_Decl_Part (Init_Cond); | |
591 | end if; | |
592 | end if; | |
593 | ||
594 | -- Check whether the lack of indicator Part_Of agrees with the placement | |
595 | -- of the package instantiation with respect to the state space. | |
596 | ||
597 | if Is_Generic_Instance (Pack_Id) then | |
598 | Prag := Get_Pragma (Pack_Id, Pragma_Part_Of); | |
599 | ||
600 | if No (Prag) then | |
601 | Check_Missing_Part_Of (Pack_Id); | |
602 | end if; | |
603 | end if; | |
604 | ||
605 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
606 | -- pragmas have been analyzed. | |
607 | ||
608 | Restore_SPARK_Mode (Mode); | |
609 | ||
610 | -- Capture all global references in a generic package now that the | |
611 | -- contract has been analyzed. | |
612 | ||
613 | if Is_Generic_Declaration_Or_Body (Pack_Decl) then | |
614 | Save_Global_References_In_Contract | |
615 | (Templ => Original_Node (Pack_Decl), | |
616 | Gen_Id => Pack_Id); | |
617 | end if; | |
618 | end Analyze_Package_Contract; | |
619 | ||
620 | -------------------------------------- | |
621 | -- Analyze_Subprogram_Body_Contract -- | |
622 | -------------------------------------- | |
623 | ||
624 | procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is | |
2ba4f1fb AC |
625 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); |
626 | Items : constant Node_Id := Contract (Body_Id); | |
627 | Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); | |
628 | Mode : SPARK_Mode_Type; | |
879ac954 AC |
629 | |
630 | begin | |
631 | -- When a subprogram body declaration is illegal, its defining entity is | |
632 | -- left unanalyzed. There is nothing left to do in this case because the | |
633 | -- body lacks a contract, or even a proper Ekind. | |
634 | ||
635 | if Ekind (Body_Id) = E_Void then | |
636 | return; | |
637 | ||
e96b7045 | 638 | -- Do not analyze a contract multiple times |
879ac954 AC |
639 | |
640 | elsif Present (Items) then | |
641 | if Analyzed (Items) then | |
642 | return; | |
643 | else | |
644 | Set_Analyzed (Items); | |
645 | end if; | |
646 | end if; | |
647 | ||
648 | -- Due to the timing of contract analysis, delayed pragmas may be | |
649 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
650 | -- context. To remedy this, restore the original SPARK_Mode of the | |
651 | -- related subprogram body. | |
652 | ||
653 | Save_SPARK_Mode_And_Set (Body_Id, Mode); | |
654 | ||
879ac954 AC |
655 | -- Ensure that the contract cases or postconditions mention 'Result or |
656 | -- define a post-state. | |
657 | ||
658 | Check_Result_And_Post_State (Body_Id); | |
659 | ||
e96b7045 | 660 | -- A stand-alone nonvolatile function body cannot have an effectively |
879ac954 | 661 | -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This |
e96b7045 | 662 | -- check is relevant only when SPARK_Mode is on, as it is not a standard |
879ac954 AC |
663 | -- legality rule. The check is performed here because Volatile_Function |
664 | -- is processed after the analysis of the related subprogram body. | |
665 | ||
666 | if SPARK_Mode = On | |
667 | and then Ekind_In (Body_Id, E_Function, E_Generic_Function) | |
668 | and then not Is_Volatile_Function (Body_Id) | |
669 | then | |
670 | Check_Nonvolatile_Function_Profile (Body_Id); | |
671 | end if; | |
672 | ||
673 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
674 | -- pragmas have been analyzed. | |
675 | ||
676 | Restore_SPARK_Mode (Mode); | |
677 | ||
678 | -- Capture all global references in a generic subprogram body now that | |
679 | -- the contract has been analyzed. | |
680 | ||
681 | if Is_Generic_Declaration_Or_Body (Body_Decl) then | |
682 | Save_Global_References_In_Contract | |
683 | (Templ => Original_Node (Body_Decl), | |
684 | Gen_Id => Spec_Id); | |
685 | end if; | |
686 | ||
687 | -- Deal with preconditions, [refined] postconditions, Contract_Cases, | |
688 | -- invariants and predicates associated with body and its spec. Do not | |
689 | -- expand the contract of subprogram body stubs. | |
690 | ||
691 | if Nkind (Body_Decl) = N_Subprogram_Body then | |
692 | Expand_Subprogram_Contract (Body_Id); | |
693 | end if; | |
694 | end Analyze_Subprogram_Body_Contract; | |
695 | ||
696 | --------------------------------- | |
697 | -- Analyze_Subprogram_Contract -- | |
698 | --------------------------------- | |
699 | ||
700 | procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is | |
701 | Items : constant Node_Id := Contract (Subp_Id); | |
702 | Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); | |
703 | Depends : Node_Id := Empty; | |
704 | Global : Node_Id := Empty; | |
705 | Mode : SPARK_Mode_Type; | |
706 | Prag : Node_Id; | |
707 | Prag_Nam : Name_Id; | |
708 | ||
709 | begin | |
e96b7045 | 710 | -- Do not analyze a contract multiple times |
879ac954 AC |
711 | |
712 | if Present (Items) then | |
713 | if Analyzed (Items) then | |
714 | return; | |
715 | else | |
716 | Set_Analyzed (Items); | |
717 | end if; | |
718 | end if; | |
719 | ||
720 | -- Due to the timing of contract analysis, delayed pragmas may be | |
721 | -- subject to the wrong SPARK_Mode, usually that of the enclosing | |
722 | -- context. To remedy this, restore the original SPARK_Mode of the | |
723 | -- related subprogram body. | |
724 | ||
725 | Save_SPARK_Mode_And_Set (Subp_Id, Mode); | |
726 | ||
727 | -- All subprograms carry a contract, but for some it is not significant | |
728 | -- and should not be processed. | |
729 | ||
730 | if not Has_Significant_Contract (Subp_Id) then | |
731 | null; | |
732 | ||
733 | elsif Present (Items) then | |
734 | ||
735 | -- Analyze pre- and postconditions | |
736 | ||
737 | Prag := Pre_Post_Conditions (Items); | |
738 | while Present (Prag) loop | |
739 | Analyze_Pre_Post_Condition_In_Decl_Part (Prag); | |
740 | Prag := Next_Pragma (Prag); | |
741 | end loop; | |
742 | ||
743 | -- Analyze contract-cases and test-cases | |
744 | ||
745 | Prag := Contract_Test_Cases (Items); | |
746 | while Present (Prag) loop | |
747 | Prag_Nam := Pragma_Name (Prag); | |
748 | ||
749 | if Prag_Nam = Name_Contract_Cases then | |
750 | Analyze_Contract_Cases_In_Decl_Part (Prag); | |
751 | else | |
752 | pragma Assert (Prag_Nam = Name_Test_Case); | |
753 | Analyze_Test_Case_In_Decl_Part (Prag); | |
754 | end if; | |
755 | ||
756 | Prag := Next_Pragma (Prag); | |
757 | end loop; | |
758 | ||
759 | -- Analyze classification pragmas | |
760 | ||
761 | Prag := Classifications (Items); | |
762 | while Present (Prag) loop | |
763 | Prag_Nam := Pragma_Name (Prag); | |
764 | ||
765 | if Prag_Nam = Name_Depends then | |
766 | Depends := Prag; | |
767 | ||
768 | elsif Prag_Nam = Name_Global then | |
769 | Global := Prag; | |
770 | end if; | |
771 | ||
772 | Prag := Next_Pragma (Prag); | |
773 | end loop; | |
774 | ||
e96b7045 | 775 | -- Analyze Global first, as Depends may mention items classified in |
879ac954 AC |
776 | -- the global categorization. |
777 | ||
778 | if Present (Global) then | |
779 | Analyze_Global_In_Decl_Part (Global); | |
780 | end if; | |
781 | ||
782 | -- Depends must be analyzed after Global in order to see the modes of | |
783 | -- all global items. | |
784 | ||
785 | if Present (Depends) then | |
786 | Analyze_Depends_In_Decl_Part (Depends); | |
787 | end if; | |
788 | ||
789 | -- Ensure that the contract cases or postconditions mention 'Result | |
790 | -- or define a post-state. | |
791 | ||
792 | Check_Result_And_Post_State (Subp_Id); | |
793 | end if; | |
794 | ||
e96b7045 | 795 | -- A nonvolatile function cannot have an effectively volatile formal |
879ac954 | 796 | -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant |
e96b7045 AC |
797 | -- only when SPARK_Mode is on, as it is not a standard legality rule. |
798 | -- The check is performed here because pragma Volatile_Function is | |
799 | -- processed after the analysis of the related subprogram declaration. | |
879ac954 AC |
800 | |
801 | if SPARK_Mode = On | |
802 | and then Ekind_In (Subp_Id, E_Function, E_Generic_Function) | |
803 | and then not Is_Volatile_Function (Subp_Id) | |
804 | then | |
805 | Check_Nonvolatile_Function_Profile (Subp_Id); | |
806 | end if; | |
807 | ||
808 | -- Restore the SPARK_Mode of the enclosing context after all delayed | |
809 | -- pragmas have been analyzed. | |
810 | ||
811 | Restore_SPARK_Mode (Mode); | |
812 | ||
813 | -- Capture all global references in a generic subprogram now that the | |
814 | -- contract has been analyzed. | |
815 | ||
816 | if Is_Generic_Declaration_Or_Body (Subp_Decl) then | |
817 | Save_Global_References_In_Contract | |
818 | (Templ => Original_Node (Subp_Decl), | |
819 | Gen_Id => Subp_Id); | |
820 | end if; | |
821 | end Analyze_Subprogram_Contract; | |
822 | ||
823 | ------------------------------------------- | |
824 | -- Analyze_Subprogram_Body_Stub_Contract -- | |
825 | ------------------------------------------- | |
826 | ||
827 | procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is | |
828 | Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); | |
829 | Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); | |
830 | ||
831 | begin | |
832 | -- A subprogram body stub may act as its own spec or as the completion | |
833 | -- of a previous declaration. Depending on the context, the contract of | |
834 | -- the stub may contain two sets of pragmas. | |
835 | ||
836 | -- The stub is a completion, the applicable pragmas are: | |
837 | -- Refined_Depends | |
838 | -- Refined_Global | |
839 | ||
840 | if Present (Spec_Id) then | |
841 | Analyze_Subprogram_Body_Contract (Stub_Id); | |
842 | ||
843 | -- The stub acts as its own spec, the applicable pragmas are: | |
844 | -- Contract_Cases | |
845 | -- Depends | |
846 | -- Global | |
847 | -- Postcondition | |
848 | -- Precondition | |
849 | -- Test_Case | |
850 | ||
851 | else | |
852 | Analyze_Subprogram_Contract (Stub_Id); | |
853 | end if; | |
854 | end Analyze_Subprogram_Body_Stub_Contract; | |
855 | ||
856 | ----------------------------- | |
857 | -- Create_Generic_Contract -- | |
858 | ----------------------------- | |
859 | ||
860 | procedure Create_Generic_Contract (Unit : Node_Id) is | |
861 | Templ : constant Node_Id := Original_Node (Unit); | |
862 | Templ_Id : constant Entity_Id := Defining_Entity (Templ); | |
863 | ||
864 | procedure Add_Generic_Contract_Pragma (Prag : Node_Id); | |
865 | -- Add a single contract-related source pragma Prag to the contract of | |
866 | -- generic template Templ_Id. | |
867 | ||
868 | --------------------------------- | |
869 | -- Add_Generic_Contract_Pragma -- | |
870 | --------------------------------- | |
871 | ||
872 | procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is | |
873 | Prag_Templ : Node_Id; | |
874 | ||
875 | begin | |
876 | -- Mark the pragma to prevent the premature capture of global | |
877 | -- references when capturing global references of the context | |
878 | -- (see Save_References_In_Pragma). | |
879 | ||
880 | Set_Is_Generic_Contract_Pragma (Prag); | |
881 | ||
882 | -- Pragmas that apply to a generic subprogram declaration are not | |
883 | -- part of the semantic structure of the generic template: | |
884 | ||
885 | -- generic | |
886 | -- procedure Example (Formal : Integer); | |
887 | -- pragma Precondition (Formal > 0); | |
888 | ||
889 | -- Create a generic template for such pragmas and link the template | |
890 | -- of the pragma with the generic template. | |
891 | ||
892 | if Nkind (Templ) = N_Generic_Subprogram_Declaration then | |
893 | Rewrite | |
894 | (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); | |
895 | Prag_Templ := Original_Node (Prag); | |
896 | ||
897 | Set_Is_Generic_Contract_Pragma (Prag_Templ); | |
898 | Add_Contract_Item (Prag_Templ, Templ_Id); | |
899 | ||
900 | -- Otherwise link the pragma with the generic template | |
901 | ||
902 | else | |
903 | Add_Contract_Item (Prag, Templ_Id); | |
904 | end if; | |
905 | end Add_Generic_Contract_Pragma; | |
906 | ||
907 | -- Local variables | |
908 | ||
909 | Context : constant Node_Id := Parent (Unit); | |
910 | Decl : Node_Id := Empty; | |
911 | ||
912 | -- Start of processing for Create_Generic_Contract | |
913 | ||
914 | begin | |
915 | -- A generic package declaration carries contract-related source pragmas | |
916 | -- in its visible declarations. | |
917 | ||
918 | if Nkind (Templ) = N_Generic_Package_Declaration then | |
919 | Set_Ekind (Templ_Id, E_Generic_Package); | |
920 | ||
921 | if Present (Visible_Declarations (Specification (Templ))) then | |
922 | Decl := First (Visible_Declarations (Specification (Templ))); | |
923 | end if; | |
924 | ||
925 | -- A generic package body carries contract-related source pragmas in its | |
926 | -- declarations. | |
927 | ||
928 | elsif Nkind (Templ) = N_Package_Body then | |
929 | Set_Ekind (Templ_Id, E_Package_Body); | |
930 | ||
931 | if Present (Declarations (Templ)) then | |
932 | Decl := First (Declarations (Templ)); | |
933 | end if; | |
934 | ||
935 | -- Generic subprogram declaration | |
936 | ||
937 | elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then | |
938 | if Nkind (Specification (Templ)) = N_Function_Specification then | |
939 | Set_Ekind (Templ_Id, E_Generic_Function); | |
940 | else | |
941 | Set_Ekind (Templ_Id, E_Generic_Procedure); | |
942 | end if; | |
943 | ||
944 | -- When the generic subprogram acts as a compilation unit, inspect | |
945 | -- the Pragmas_After list for contract-related source pragmas. | |
946 | ||
947 | if Nkind (Context) = N_Compilation_Unit then | |
948 | if Present (Aux_Decls_Node (Context)) | |
949 | and then Present (Pragmas_After (Aux_Decls_Node (Context))) | |
950 | then | |
951 | Decl := First (Pragmas_After (Aux_Decls_Node (Context))); | |
952 | end if; | |
953 | ||
954 | -- Otherwise inspect the successive declarations for contract-related | |
955 | -- source pragmas. | |
956 | ||
957 | else | |
958 | Decl := Next (Unit); | |
959 | end if; | |
960 | ||
961 | -- A generic subprogram body carries contract-related source pragmas in | |
962 | -- its declarations. | |
963 | ||
964 | elsif Nkind (Templ) = N_Subprogram_Body then | |
965 | Set_Ekind (Templ_Id, E_Subprogram_Body); | |
966 | ||
967 | if Present (Declarations (Templ)) then | |
968 | Decl := First (Declarations (Templ)); | |
969 | end if; | |
970 | end if; | |
971 | ||
972 | -- Inspect the relevant declarations looking for contract-related source | |
973 | -- pragmas and add them to the contract of the generic unit. | |
974 | ||
975 | while Present (Decl) loop | |
976 | if Comes_From_Source (Decl) then | |
977 | if Nkind (Decl) = N_Pragma then | |
978 | ||
979 | -- The source pragma is a contract annotation | |
980 | ||
981 | if Is_Contract_Annotation (Decl) then | |
982 | Add_Generic_Contract_Pragma (Decl); | |
983 | end if; | |
984 | ||
985 | -- The region where a contract-related source pragma may appear | |
986 | -- ends with the first source non-pragma declaration or statement. | |
987 | ||
988 | else | |
989 | exit; | |
990 | end if; | |
991 | end if; | |
992 | ||
993 | Next (Decl); | |
994 | end loop; | |
995 | end Create_Generic_Contract; | |
996 | ||
997 | -------------------------------- | |
998 | -- Expand_Subprogram_Contract -- | |
999 | -------------------------------- | |
1000 | ||
1001 | procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is | |
1002 | Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); | |
1003 | Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); | |
1004 | ||
1005 | procedure Add_Invariant_And_Predicate_Checks | |
1006 | (Subp_Id : Entity_Id; | |
1007 | Stmts : in out List_Id; | |
1008 | Result : out Node_Id); | |
1009 | -- Process the result of function Subp_Id (if applicable) and all its | |
1010 | -- formals. Add invariant and predicate checks where applicable. The | |
1011 | -- routine appends all the checks to list Stmts. If Subp_Id denotes a | |
1012 | -- function, Result contains the entity of parameter _Result, to be | |
1013 | -- used in the creation of procedure _Postconditions. | |
1014 | ||
1015 | procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); | |
1016 | -- Append a node to a list. If there is no list, create a new one. When | |
1017 | -- the item denotes a pragma, it is added to the list only when it is | |
1018 | -- enabled. | |
1019 | ||
1020 | procedure Build_Postconditions_Procedure | |
1021 | (Subp_Id : Entity_Id; | |
1022 | Stmts : List_Id; | |
1023 | Result : Entity_Id); | |
1024 | -- Create the body of procedure _Postconditions which handles various | |
1025 | -- assertion actions on exit from subprogram Subp_Id. Stmts is the list | |
1026 | -- of statements to be checked on exit. Parameter Result is the entity | |
1027 | -- of parameter _Result when Subp_Id denotes a function. | |
1028 | ||
1029 | function Build_Pragma_Check_Equivalent | |
1030 | (Prag : Node_Id; | |
1031 | Subp_Id : Entity_Id := Empty; | |
1032 | Inher_Id : Entity_Id := Empty) return Node_Id; | |
1033 | -- Transform a [refined] pre- or postcondition denoted by Prag into an | |
1034 | -- equivalent pragma Check. When the pre- or postcondition is inherited, | |
1035 | -- the routine corrects the references of all formals of Inher_Id to | |
1036 | -- point to the formals of Subp_Id. | |
1037 | ||
1038 | procedure Process_Contract_Cases (Stmts : in out List_Id); | |
1039 | -- Process pragma Contract_Cases. This routine prepends items to the | |
1040 | -- body declarations and appends items to list Stmts. | |
1041 | ||
1042 | procedure Process_Postconditions (Stmts : in out List_Id); | |
1043 | -- Collect all [inherited] spec and body postconditions and accumulate | |
1044 | -- their pragma Check equivalents in list Stmts. | |
1045 | ||
1046 | procedure Process_Preconditions; | |
1047 | -- Collect all [inherited] spec and body preconditions and prepend their | |
1048 | -- pragma Check equivalents to the declarations of the body. | |
1049 | ||
1050 | ---------------------------------------- | |
1051 | -- Add_Invariant_And_Predicate_Checks -- | |
1052 | ---------------------------------------- | |
1053 | ||
1054 | procedure Add_Invariant_And_Predicate_Checks | |
1055 | (Subp_Id : Entity_Id; | |
1056 | Stmts : in out List_Id; | |
1057 | Result : out Node_Id) | |
1058 | is | |
1059 | procedure Add_Invariant_Access_Checks (Id : Entity_Id); | |
1060 | -- Id denotes the return value of a function or a formal parameter. | |
1061 | -- Add an invariant check if the type of Id is access to a type with | |
1062 | -- invariants. The routine appends the generated code to Stmts. | |
1063 | ||
1064 | function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; | |
1065 | -- Determine whether type Typ can benefit from invariant checks. To | |
1066 | -- qualify, the type must have a non-null invariant procedure and | |
1067 | -- subprogram Subp_Id must appear visible from the point of view of | |
1068 | -- the type. | |
1069 | ||
1070 | --------------------------------- | |
1071 | -- Add_Invariant_Access_Checks -- | |
1072 | --------------------------------- | |
1073 | ||
1074 | procedure Add_Invariant_Access_Checks (Id : Entity_Id) is | |
1075 | Loc : constant Source_Ptr := Sloc (Body_Decl); | |
1076 | Ref : Node_Id; | |
1077 | Typ : Entity_Id; | |
1078 | ||
1079 | begin | |
1080 | Typ := Etype (Id); | |
1081 | ||
1082 | if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then | |
1083 | Typ := Designated_Type (Typ); | |
1084 | ||
1085 | if Invariant_Checks_OK (Typ) then | |
1086 | Ref := | |
1087 | Make_Explicit_Dereference (Loc, | |
1088 | Prefix => New_Occurrence_Of (Id, Loc)); | |
1089 | Set_Etype (Ref, Typ); | |
1090 | ||
1091 | -- Generate: | |
1092 | -- if <Id> /= null then | |
1093 | -- <invariant_call (<Ref>)> | |
1094 | -- end if; | |
1095 | ||
1096 | Append_Enabled_Item | |
1097 | (Item => | |
1098 | Make_If_Statement (Loc, | |
1099 | Condition => | |
1100 | Make_Op_Ne (Loc, | |
1101 | Left_Opnd => New_Occurrence_Of (Id, Loc), | |
1102 | Right_Opnd => Make_Null (Loc)), | |
1103 | Then_Statements => New_List ( | |
1104 | Make_Invariant_Call (Ref))), | |
1105 | List => Stmts); | |
1106 | end if; | |
1107 | end if; | |
1108 | end Add_Invariant_Access_Checks; | |
1109 | ||
1110 | ------------------------- | |
1111 | -- Invariant_Checks_OK -- | |
1112 | ------------------------- | |
1113 | ||
1114 | function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is | |
1115 | function Has_Null_Body (Proc_Id : Entity_Id) return Boolean; | |
1116 | -- Determine whether the body of procedure Proc_Id contains a sole | |
1117 | -- null statement, possibly followed by an optional return. | |
1118 | ||
1119 | function Has_Public_Visibility_Of_Subprogram return Boolean; | |
1120 | -- Determine whether type Typ has public visibility of subprogram | |
1121 | -- Subp_Id. | |
1122 | ||
1123 | ------------------- | |
1124 | -- Has_Null_Body -- | |
1125 | ------------------- | |
1126 | ||
1127 | function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is | |
1128 | Body_Id : Entity_Id; | |
1129 | Decl : Node_Id; | |
1130 | Spec : Node_Id; | |
1131 | Stmt1 : Node_Id; | |
1132 | Stmt2 : Node_Id; | |
1133 | ||
1134 | begin | |
1135 | Spec := Parent (Proc_Id); | |
1136 | Decl := Parent (Spec); | |
1137 | ||
1138 | -- Retrieve the entity of the invariant procedure body | |
1139 | ||
1140 | if Nkind (Spec) = N_Procedure_Specification | |
1141 | and then Nkind (Decl) = N_Subprogram_Declaration | |
1142 | then | |
1143 | Body_Id := Corresponding_Body (Decl); | |
1144 | ||
1145 | -- The body acts as a spec | |
1146 | ||
1147 | else | |
1148 | Body_Id := Proc_Id; | |
1149 | end if; | |
1150 | ||
1151 | -- The body will be generated later | |
1152 | ||
1153 | if No (Body_Id) then | |
1154 | return False; | |
1155 | end if; | |
1156 | ||
1157 | Spec := Parent (Body_Id); | |
1158 | Decl := Parent (Spec); | |
1159 | ||
1160 | pragma Assert | |
1161 | (Nkind (Spec) = N_Procedure_Specification | |
1162 | and then Nkind (Decl) = N_Subprogram_Body); | |
1163 | ||
1164 | Stmt1 := First (Statements (Handled_Statement_Sequence (Decl))); | |
1165 | ||
1166 | -- Look for a null statement followed by an optional return | |
1167 | -- statement. | |
1168 | ||
1169 | if Nkind (Stmt1) = N_Null_Statement then | |
1170 | Stmt2 := Next (Stmt1); | |
1171 | ||
1172 | if Present (Stmt2) then | |
1173 | return Nkind (Stmt2) = N_Simple_Return_Statement; | |
1174 | else | |
1175 | return True; | |
1176 | end if; | |
1177 | end if; | |
1178 | ||
1179 | return False; | |
1180 | end Has_Null_Body; | |
1181 | ||
1182 | ----------------------------------------- | |
1183 | -- Has_Public_Visibility_Of_Subprogram -- | |
1184 | ----------------------------------------- | |
1185 | ||
1186 | function Has_Public_Visibility_Of_Subprogram return Boolean is | |
1187 | Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); | |
1188 | ||
1189 | begin | |
1190 | -- An Initialization procedure must be considered visible even | |
1191 | -- though it is internally generated. | |
1192 | ||
1193 | if Is_Init_Proc (Defining_Entity (Subp_Decl)) then | |
1194 | return True; | |
1195 | ||
1196 | elsif Ekind (Scope (Typ)) /= E_Package then | |
1197 | return False; | |
1198 | ||
1199 | -- Internally generated code is never publicly visible except | |
1200 | -- for a subprogram that is the implementation of an expression | |
1201 | -- function. In that case the visibility is determined by the | |
1202 | -- last check. | |
1203 | ||
1204 | elsif not Comes_From_Source (Subp_Decl) | |
1205 | and then | |
1206 | (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function | |
1207 | or else not | |
1208 | Comes_From_Source (Defining_Entity (Subp_Decl))) | |
1209 | then | |
1210 | return False; | |
1211 | ||
1212 | -- Determine whether the subprogram is declared in the visible | |
1213 | -- declarations of the package containing the type. | |
1214 | ||
1215 | else | |
1216 | return List_Containing (Subp_Decl) = | |
1217 | Visible_Declarations | |
1218 | (Specification (Unit_Declaration_Node (Scope (Typ)))); | |
1219 | end if; | |
1220 | end Has_Public_Visibility_Of_Subprogram; | |
1221 | ||
1222 | -- Start of processing for Invariant_Checks_OK | |
1223 | ||
1224 | begin | |
1225 | return | |
1226 | Has_Invariants (Typ) | |
1227 | and then Present (Invariant_Procedure (Typ)) | |
1228 | and then not Has_Null_Body (Invariant_Procedure (Typ)) | |
1229 | and then Has_Public_Visibility_Of_Subprogram; | |
1230 | end Invariant_Checks_OK; | |
1231 | ||
1232 | -- Local variables | |
1233 | ||
1234 | Loc : constant Source_Ptr := Sloc (Body_Decl); | |
1235 | -- Source location of subprogram body contract | |
1236 | ||
1237 | Formal : Entity_Id; | |
1238 | Typ : Entity_Id; | |
1239 | ||
1240 | -- Start of processing for Add_Invariant_And_Predicate_Checks | |
1241 | ||
1242 | begin | |
1243 | Result := Empty; | |
1244 | ||
1245 | -- Process the result of a function | |
1246 | ||
1247 | if Ekind (Subp_Id) = E_Function then | |
1248 | Typ := Etype (Subp_Id); | |
1249 | ||
1250 | -- Generate _Result which is used in procedure _Postconditions to | |
1251 | -- verify the return value. | |
1252 | ||
1253 | Result := Make_Defining_Identifier (Loc, Name_uResult); | |
1254 | Set_Etype (Result, Typ); | |
1255 | ||
1256 | -- Add an invariant check when the return type has invariants and | |
1257 | -- the related function is visible to the outside. | |
1258 | ||
1259 | if Invariant_Checks_OK (Typ) then | |
1260 | Append_Enabled_Item | |
1261 | (Item => | |
1262 | Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), | |
1263 | List => Stmts); | |
1264 | end if; | |
1265 | ||
1266 | -- Add an invariant check when the return type is an access to a | |
1267 | -- type with invariants. | |
1268 | ||
1269 | Add_Invariant_Access_Checks (Result); | |
1270 | end if; | |
1271 | ||
1272 | -- Add invariant and predicates for all formals that qualify | |
1273 | ||
1274 | Formal := First_Formal (Subp_Id); | |
1275 | while Present (Formal) loop | |
1276 | Typ := Etype (Formal); | |
1277 | ||
1278 | if Ekind (Formal) /= E_In_Parameter | |
1279 | or else Is_Access_Type (Typ) | |
1280 | then | |
1281 | if Invariant_Checks_OK (Typ) then | |
1282 | Append_Enabled_Item | |
1283 | (Item => | |
1284 | Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), | |
1285 | List => Stmts); | |
1286 | end if; | |
1287 | ||
1288 | Add_Invariant_Access_Checks (Formal); | |
1289 | ||
1290 | -- Note: we used to add predicate checks for OUT and IN OUT | |
1291 | -- formals here, but that was misguided, since such checks are | |
1292 | -- performed on the caller side, based on the predicate of the | |
1293 | -- actual, rather than the predicate of the formal. | |
1294 | ||
1295 | end if; | |
1296 | ||
1297 | Next_Formal (Formal); | |
1298 | end loop; | |
1299 | end Add_Invariant_And_Predicate_Checks; | |
1300 | ||
1301 | ------------------------- | |
1302 | -- Append_Enabled_Item -- | |
1303 | ------------------------- | |
1304 | ||
1305 | procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is | |
1306 | begin | |
1307 | -- Do not chain ignored or disabled pragmas | |
1308 | ||
1309 | if Nkind (Item) = N_Pragma | |
1310 | and then (Is_Ignored (Item) or else Is_Disabled (Item)) | |
1311 | then | |
1312 | null; | |
1313 | ||
1314 | -- Otherwise, add the item | |
1315 | ||
1316 | else | |
1317 | if No (List) then | |
1318 | List := New_List; | |
1319 | end if; | |
1320 | ||
1321 | -- If the pragma is a conjunct in a composite postcondition, it | |
1322 | -- has been processed in reverse order. In the postcondition body | |
e96b7045 | 1323 | -- it must appear before the others. |
879ac954 AC |
1324 | |
1325 | if Nkind (Item) = N_Pragma | |
1326 | and then From_Aspect_Specification (Item) | |
1327 | and then Split_PPC (Item) | |
1328 | then | |
1329 | Prepend (Item, List); | |
1330 | else | |
1331 | Append (Item, List); | |
1332 | end if; | |
1333 | end if; | |
1334 | end Append_Enabled_Item; | |
1335 | ||
1336 | ------------------------------------ | |
1337 | -- Build_Postconditions_Procedure -- | |
1338 | ------------------------------------ | |
1339 | ||
1340 | procedure Build_Postconditions_Procedure | |
1341 | (Subp_Id : Entity_Id; | |
1342 | Stmts : List_Id; | |
1343 | Result : Entity_Id) | |
1344 | is | |
1345 | procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id); | |
1346 | -- Insert node Stmt before the first source declaration of the | |
1347 | -- related subprogram's body. If no such declaration exists, Stmt | |
1348 | -- becomes the last declaration. | |
1349 | ||
1350 | -------------------------------------------- | |
1351 | -- Insert_Before_First_Source_Declaration -- | |
1352 | -------------------------------------------- | |
1353 | ||
1354 | procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is | |
1355 | Decls : constant List_Id := Declarations (Body_Decl); | |
1356 | Decl : Node_Id; | |
1357 | ||
1358 | begin | |
1359 | -- Inspect the declarations of the related subprogram body looking | |
1360 | -- for the first source declaration. | |
1361 | ||
1362 | if Present (Decls) then | |
1363 | Decl := First (Decls); | |
1364 | while Present (Decl) loop | |
1365 | if Comes_From_Source (Decl) then | |
1366 | Insert_Before (Decl, Stmt); | |
1367 | return; | |
1368 | end if; | |
1369 | ||
1370 | Next (Decl); | |
1371 | end loop; | |
1372 | ||
1373 | -- If we get there, then the subprogram body lacks any source | |
1374 | -- declarations. The body of _Postconditions now acts as the | |
1375 | -- last declaration. | |
1376 | ||
1377 | Append (Stmt, Decls); | |
1378 | ||
1379 | -- Ensure that the body has a declaration list | |
1380 | ||
1381 | else | |
1382 | Set_Declarations (Body_Decl, New_List (Stmt)); | |
1383 | end if; | |
1384 | end Insert_Before_First_Source_Declaration; | |
1385 | ||
1386 | -- Local variables | |
1387 | ||
1388 | Loc : constant Source_Ptr := Sloc (Body_Decl); | |
1389 | Params : List_Id := No_List; | |
1390 | Proc_Bod : Node_Id; | |
1391 | Proc_Id : Entity_Id; | |
1392 | ||
1393 | -- Start of processing for Build_Postconditions_Procedure | |
1394 | ||
1395 | begin | |
1396 | -- Nothing to do if there are no actions to check on exit | |
1397 | ||
1398 | if No (Stmts) then | |
1399 | return; | |
1400 | end if; | |
1401 | ||
1402 | Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); | |
1403 | Set_Debug_Info_Needed (Proc_Id); | |
1404 | Set_Postconditions_Proc (Subp_Id, Proc_Id); | |
1405 | ||
e96b7045 | 1406 | -- The related subprogram is a function: create the specification of |
879ac954 AC |
1407 | -- parameter _Result. |
1408 | ||
1409 | if Present (Result) then | |
1410 | Params := New_List ( | |
1411 | Make_Parameter_Specification (Loc, | |
1412 | Defining_Identifier => Result, | |
1413 | Parameter_Type => | |
1414 | New_Occurrence_Of (Etype (Result), Loc))); | |
1415 | end if; | |
1416 | ||
1417 | -- Insert _Postconditions before the first source declaration of the | |
1418 | -- body. This ensures that the body will not cause any premature | |
e96b7045 | 1419 | -- freezing, as it may mention types: |
879ac954 AC |
1420 | |
1421 | -- procedure Proc (Obj : Array_Typ) is | |
1422 | -- procedure _postconditions is | |
1423 | -- begin | |
1424 | -- ... Obj ... | |
1425 | -- end _postconditions; | |
1426 | ||
1427 | -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); | |
1428 | -- begin | |
1429 | ||
1430 | -- In the example above, Obj is of type T but the incorrect placement | |
e96b7045 | 1431 | -- of _Postconditions will cause a crash in gigi due to an out-of- |
879ac954 AC |
1432 | -- order reference. The body of _Postconditions must be placed after |
1433 | -- the declaration of Temp to preserve correct visibility. | |
1434 | ||
e96b7045 | 1435 | -- Set an explicit End_Label to override the sloc of the implicit |
879ac954 | 1436 | -- RETURN statement, and prevent it from inheriting the sloc of one |
e96b7045 AC |
1437 | -- the postconditions: this would cause confusing debug info to be |
1438 | -- produced, interfering with coverage-analysis tools. | |
879ac954 AC |
1439 | |
1440 | Proc_Bod := | |
1441 | Make_Subprogram_Body (Loc, | |
1442 | Specification => | |
1443 | Make_Procedure_Specification (Loc, | |
1444 | Defining_Unit_Name => Proc_Id, | |
1445 | Parameter_Specifications => Params), | |
1446 | ||
1447 | Declarations => Empty_List, | |
1448 | Handled_Statement_Sequence => | |
1449 | Make_Handled_Sequence_Of_Statements (Loc, | |
1450 | Statements => Stmts, | |
1451 | End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); | |
1452 | ||
1453 | Insert_Before_First_Source_Declaration (Proc_Bod); | |
1454 | Analyze (Proc_Bod); | |
1455 | end Build_Postconditions_Procedure; | |
1456 | ||
1457 | ----------------------------------- | |
1458 | -- Build_Pragma_Check_Equivalent -- | |
1459 | ----------------------------------- | |
1460 | ||
1461 | function Build_Pragma_Check_Equivalent | |
1462 | (Prag : Node_Id; | |
1463 | Subp_Id : Entity_Id := Empty; | |
1464 | Inher_Id : Entity_Id := Empty) return Node_Id | |
1465 | is | |
1466 | function Suppress_Reference (N : Node_Id) return Traverse_Result; | |
1467 | -- Detect whether node N references a formal parameter subject to | |
1468 | -- pragma Unreferenced. If this is the case, set Comes_From_Source | |
1469 | -- to False to suppress the generation of a reference when analyzing | |
1470 | -- N later on. | |
1471 | ||
1472 | ------------------------ | |
1473 | -- Suppress_Reference -- | |
1474 | ------------------------ | |
1475 | ||
1476 | function Suppress_Reference (N : Node_Id) return Traverse_Result is | |
1477 | Formal : Entity_Id; | |
1478 | ||
1479 | begin | |
1480 | if Is_Entity_Name (N) and then Present (Entity (N)) then | |
1481 | Formal := Entity (N); | |
1482 | ||
1483 | -- The formal parameter is subject to pragma Unreferenced. | |
1484 | -- Prevent the generation of a reference by resetting the | |
1485 | -- Comes_From_Source flag. | |
1486 | ||
1487 | if Is_Formal (Formal) | |
1488 | and then Has_Pragma_Unreferenced (Formal) | |
1489 | then | |
1490 | Set_Comes_From_Source (N, False); | |
1491 | end if; | |
1492 | end if; | |
1493 | ||
1494 | return OK; | |
1495 | end Suppress_Reference; | |
1496 | ||
1497 | procedure Suppress_References is | |
1498 | new Traverse_Proc (Suppress_Reference); | |
1499 | ||
1500 | -- Local variables | |
1501 | ||
1502 | Loc : constant Source_Ptr := Sloc (Prag); | |
1503 | Prag_Nam : constant Name_Id := Pragma_Name (Prag); | |
1504 | Check_Prag : Node_Id; | |
1505 | Formals_Map : Elist_Id; | |
1506 | Inher_Formal : Entity_Id; | |
1507 | Msg_Arg : Node_Id; | |
1508 | Nam : Name_Id; | |
1509 | Subp_Formal : Entity_Id; | |
1510 | ||
1511 | -- Start of processing for Build_Pragma_Check_Equivalent | |
1512 | ||
1513 | begin | |
1514 | Formals_Map := No_Elist; | |
1515 | ||
1516 | -- When the pre- or postcondition is inherited, map the formals of | |
1517 | -- the inherited subprogram to those of the current subprogram. | |
1518 | ||
1519 | if Present (Inher_Id) then | |
1520 | pragma Assert (Present (Subp_Id)); | |
1521 | ||
1522 | Formals_Map := New_Elmt_List; | |
1523 | ||
1524 | -- Create a relation <inherited formal> => <subprogram formal> | |
1525 | ||
1526 | Inher_Formal := First_Formal (Inher_Id); | |
1527 | Subp_Formal := First_Formal (Subp_Id); | |
1528 | while Present (Inher_Formal) and then Present (Subp_Formal) loop | |
1529 | Append_Elmt (Inher_Formal, Formals_Map); | |
1530 | Append_Elmt (Subp_Formal, Formals_Map); | |
1531 | ||
1532 | Next_Formal (Inher_Formal); | |
1533 | Next_Formal (Subp_Formal); | |
1534 | end loop; | |
1535 | end if; | |
1536 | ||
1537 | -- Copy the original pragma while performing substitutions (if | |
1538 | -- applicable). | |
1539 | ||
1540 | Check_Prag := | |
1541 | New_Copy_Tree | |
1542 | (Source => Prag, | |
1543 | Map => Formals_Map, | |
1544 | New_Scope => Current_Scope); | |
1545 | ||
1546 | -- Mark the pragma as being internally generated and reset the | |
1547 | -- Analyzed flag. | |
1548 | ||
1549 | Set_Analyzed (Check_Prag, False); | |
1550 | Set_Comes_From_Source (Check_Prag, False); | |
1551 | ||
1552 | -- The tree of the original pragma may contain references to the | |
1553 | -- formal parameters of the related subprogram. At the same time | |
1554 | -- the corresponding body may mark the formals as unreferenced: | |
1555 | ||
1556 | -- procedure Proc (Formal : ...) | |
1557 | -- with Pre => Formal ...; | |
1558 | ||
1559 | -- procedure Proc (Formal : ...) is | |
1560 | -- pragma Unreferenced (Formal); | |
1561 | -- ... | |
1562 | ||
1563 | -- This creates problems because all pragma Check equivalents are | |
1564 | -- analyzed at the end of the body declarations. Since all source | |
1565 | -- references have already been accounted for, reset any references | |
1566 | -- to such formals in the generated pragma Check equivalent. | |
1567 | ||
1568 | Suppress_References (Check_Prag); | |
1569 | ||
1570 | if Present (Corresponding_Aspect (Prag)) then | |
1571 | Nam := Chars (Identifier (Corresponding_Aspect (Prag))); | |
1572 | else | |
1573 | Nam := Prag_Nam; | |
1574 | end if; | |
1575 | ||
1576 | -- Convert the copy into pragma Check by correcting the name and | |
1577 | -- adding a check_kind argument. | |
1578 | ||
1579 | Set_Pragma_Identifier | |
1580 | (Check_Prag, Make_Identifier (Loc, Name_Check)); | |
1581 | ||
1582 | Prepend_To (Pragma_Argument_Associations (Check_Prag), | |
1583 | Make_Pragma_Argument_Association (Loc, | |
1584 | Expression => Make_Identifier (Loc, Nam))); | |
1585 | ||
1586 | -- Update the error message when the pragma is inherited | |
1587 | ||
1588 | if Present (Inher_Id) then | |
1589 | Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag)); | |
1590 | ||
1591 | if Chars (Msg_Arg) = Name_Message then | |
1592 | String_To_Name_Buffer (Strval (Expression (Msg_Arg))); | |
1593 | ||
1594 | -- Insert "inherited" to improve the error message | |
1595 | ||
1596 | if Name_Buffer (1 .. 8) = "failed p" then | |
1597 | Insert_Str_In_Name_Buffer ("inherited ", 8); | |
1598 | Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer); | |
1599 | end if; | |
1600 | end if; | |
1601 | end if; | |
1602 | ||
1603 | return Check_Prag; | |
1604 | end Build_Pragma_Check_Equivalent; | |
1605 | ||
1606 | ---------------------------- | |
1607 | -- Process_Contract_Cases -- | |
1608 | ---------------------------- | |
1609 | ||
1610 | procedure Process_Contract_Cases (Stmts : in out List_Id) is | |
1611 | procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); | |
1612 | -- Process pragma Contract_Cases for subprogram Subp_Id | |
1613 | ||
1614 | -------------------------------- | |
1615 | -- Process_Contract_Cases_For -- | |
1616 | -------------------------------- | |
1617 | ||
1618 | procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is | |
1619 | Items : constant Node_Id := Contract (Subp_Id); | |
1620 | Prag : Node_Id; | |
1621 | ||
1622 | begin | |
1623 | if Present (Items) then | |
1624 | Prag := Contract_Test_Cases (Items); | |
1625 | while Present (Prag) loop | |
1626 | if Pragma_Name (Prag) = Name_Contract_Cases then | |
1627 | Expand_Pragma_Contract_Cases | |
1628 | (CCs => Prag, | |
1629 | Subp_Id => Subp_Id, | |
1630 | Decls => Declarations (Body_Decl), | |
1631 | Stmts => Stmts); | |
1632 | end if; | |
1633 | ||
1634 | Prag := Next_Pragma (Prag); | |
1635 | end loop; | |
1636 | end if; | |
1637 | end Process_Contract_Cases_For; | |
1638 | ||
1639 | -- Start of processing for Process_Contract_Cases | |
1640 | ||
1641 | begin | |
1642 | Process_Contract_Cases_For (Body_Id); | |
1643 | ||
1644 | if Present (Spec_Id) then | |
1645 | Process_Contract_Cases_For (Spec_Id); | |
1646 | end if; | |
1647 | end Process_Contract_Cases; | |
1648 | ||
1649 | ---------------------------- | |
1650 | -- Process_Postconditions -- | |
1651 | ---------------------------- | |
1652 | ||
1653 | procedure Process_Postconditions (Stmts : in out List_Id) is | |
1654 | procedure Process_Body_Postconditions (Post_Nam : Name_Id); | |
1655 | -- Collect all [refined] postconditions of a specific kind denoted | |
e96b7045 | 1656 | -- by Post_Nam that belong to the body, and generate pragma Check |
879ac954 AC |
1657 | -- equivalents in list Stmts. |
1658 | ||
1659 | procedure Process_Spec_Postconditions; | |
e96b7045 | 1660 | -- Collect all [inherited] postconditions of the spec, and generate |
879ac954 AC |
1661 | -- pragma Check equivalents in list Stmts. |
1662 | ||
1663 | --------------------------------- | |
1664 | -- Process_Body_Postconditions -- | |
1665 | --------------------------------- | |
1666 | ||
1667 | procedure Process_Body_Postconditions (Post_Nam : Name_Id) is | |
1668 | Items : constant Node_Id := Contract (Body_Id); | |
1669 | Unit_Decl : constant Node_Id := Parent (Body_Decl); | |
1670 | Decl : Node_Id; | |
1671 | Prag : Node_Id; | |
1672 | ||
1673 | begin | |
1674 | -- Process the contract | |
1675 | ||
1676 | if Present (Items) then | |
1677 | Prag := Pre_Post_Conditions (Items); | |
1678 | while Present (Prag) loop | |
1679 | if Pragma_Name (Prag) = Post_Nam then | |
1680 | Append_Enabled_Item | |
1681 | (Item => Build_Pragma_Check_Equivalent (Prag), | |
1682 | List => Stmts); | |
1683 | end if; | |
1684 | ||
1685 | Prag := Next_Pragma (Prag); | |
1686 | end loop; | |
1687 | end if; | |
1688 | ||
1689 | -- The subprogram body being processed is actually the proper body | |
1690 | -- of a stub with a corresponding spec. The subprogram stub may | |
e96b7045 | 1691 | -- carry a postcondition pragma, in which case it must be taken |
879ac954 AC |
1692 | -- into account. The pragma appears after the stub. |
1693 | ||
1694 | if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then | |
1695 | Decl := Next (Corresponding_Stub (Unit_Decl)); | |
1696 | while Present (Decl) loop | |
1697 | ||
1698 | -- Note that non-matching pragmas are skipped | |
1699 | ||
1700 | if Nkind (Decl) = N_Pragma then | |
1701 | if Pragma_Name (Decl) = Post_Nam then | |
1702 | Append_Enabled_Item | |
1703 | (Item => Build_Pragma_Check_Equivalent (Decl), | |
1704 | List => Stmts); | |
1705 | end if; | |
1706 | ||
1707 | -- Skip internally generated code | |
1708 | ||
1709 | elsif not Comes_From_Source (Decl) then | |
1710 | null; | |
1711 | ||
1712 | -- Postcondition pragmas are usually grouped together. There | |
1713 | -- is no need to inspect the whole declarative list. | |
1714 | ||
1715 | else | |
1716 | exit; | |
1717 | end if; | |
1718 | ||
1719 | Next (Decl); | |
1720 | end loop; | |
1721 | end if; | |
1722 | end Process_Body_Postconditions; | |
1723 | ||
1724 | --------------------------------- | |
1725 | -- Process_Spec_Postconditions -- | |
1726 | --------------------------------- | |
1727 | ||
1728 | procedure Process_Spec_Postconditions is | |
1729 | Subps : constant Subprogram_List := | |
1730 | Inherited_Subprograms (Spec_Id); | |
1731 | Items : Node_Id; | |
1732 | Prag : Node_Id; | |
1733 | Subp_Id : Entity_Id; | |
1734 | ||
1735 | begin | |
1736 | -- Process the contract | |
1737 | ||
1738 | Items := Contract (Spec_Id); | |
1739 | ||
1740 | if Present (Items) then | |
1741 | Prag := Pre_Post_Conditions (Items); | |
1742 | while Present (Prag) loop | |
1743 | if Pragma_Name (Prag) = Name_Postcondition then | |
1744 | Append_Enabled_Item | |
1745 | (Item => Build_Pragma_Check_Equivalent (Prag), | |
1746 | List => Stmts); | |
1747 | end if; | |
1748 | ||
1749 | Prag := Next_Pragma (Prag); | |
1750 | end loop; | |
1751 | end if; | |
1752 | ||
1753 | -- Process the contracts of all inherited subprograms, looking for | |
1754 | -- class-wide postconditions. | |
1755 | ||
1756 | for Index in Subps'Range loop | |
1757 | Subp_Id := Subps (Index); | |
1758 | Items := Contract (Subp_Id); | |
1759 | ||
1760 | if Present (Items) then | |
1761 | Prag := Pre_Post_Conditions (Items); | |
1762 | while Present (Prag) loop | |
1763 | if Pragma_Name (Prag) = Name_Postcondition | |
1764 | and then Class_Present (Prag) | |
1765 | then | |
1766 | Append_Enabled_Item | |
1767 | (Item => | |
1768 | Build_Pragma_Check_Equivalent | |
1769 | (Prag => Prag, | |
1770 | Subp_Id => Spec_Id, | |
1771 | Inher_Id => Subp_Id), | |
1772 | List => Stmts); | |
1773 | end if; | |
1774 | ||
1775 | Prag := Next_Pragma (Prag); | |
1776 | end loop; | |
1777 | end if; | |
1778 | end loop; | |
1779 | end Process_Spec_Postconditions; | |
1780 | ||
1781 | -- Start of processing for Process_Postconditions | |
1782 | ||
1783 | begin | |
1784 | -- The processing of postconditions is done in reverse order (body | |
1785 | -- first) to ensure the following arrangement: | |
1786 | ||
1787 | -- <refined postconditions from body> | |
1788 | -- <postconditions from body> | |
1789 | -- <postconditions from spec> | |
1790 | -- <inherited postconditions> | |
1791 | ||
1792 | Process_Body_Postconditions (Name_Refined_Post); | |
1793 | Process_Body_Postconditions (Name_Postcondition); | |
1794 | ||
1795 | if Present (Spec_Id) then | |
1796 | Process_Spec_Postconditions; | |
1797 | end if; | |
1798 | end Process_Postconditions; | |
1799 | ||
1800 | --------------------------- | |
1801 | -- Process_Preconditions -- | |
1802 | --------------------------- | |
1803 | ||
1804 | procedure Process_Preconditions is | |
1805 | Class_Pre : Node_Id := Empty; | |
1806 | -- The sole [inherited] class-wide precondition pragma that applies | |
1807 | -- to the subprogram. | |
1808 | ||
1809 | Insert_Node : Node_Id := Empty; | |
1810 | -- The insertion node after which all pragma Check equivalents are | |
1811 | -- inserted. | |
1812 | ||
1813 | procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); | |
1814 | -- Merge two class-wide preconditions by "or else"-ing them. The | |
1815 | -- changes are accumulated in parameter Into. Update the error | |
1816 | -- message of Into. | |
1817 | ||
1818 | procedure Prepend_To_Decls (Item : Node_Id); | |
1819 | -- Prepend a single item to the declarations of the subprogram body | |
1820 | ||
1821 | procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); | |
e96b7045 AC |
1822 | -- Save a class-wide precondition into Class_Pre, or prepend a normal |
1823 | -- precondition to the declarations of the body and analyze it. | |
879ac954 AC |
1824 | |
1825 | procedure Process_Inherited_Preconditions; | |
1826 | -- Collect all inherited class-wide preconditions and merge them into | |
1827 | -- one big precondition to be evaluated as pragma Check. | |
1828 | ||
1829 | procedure Process_Preconditions_For (Subp_Id : Entity_Id); | |
1830 | -- Collect all preconditions of subprogram Subp_Id and prepend their | |
1831 | -- pragma Check equivalents to the declarations of the body. | |
1832 | ||
1833 | ------------------------- | |
1834 | -- Merge_Preconditions -- | |
1835 | ------------------------- | |
1836 | ||
1837 | procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is | |
1838 | function Expression_Arg (Prag : Node_Id) return Node_Id; | |
1839 | -- Return the boolean expression argument of a precondition while | |
e96b7045 | 1840 | -- updating its parentheses count for the subsequent merge. |
879ac954 AC |
1841 | |
1842 | function Message_Arg (Prag : Node_Id) return Node_Id; | |
1843 | -- Return the message argument of a precondition | |
1844 | ||
1845 | -------------------- | |
1846 | -- Expression_Arg -- | |
1847 | -------------------- | |
1848 | ||
1849 | function Expression_Arg (Prag : Node_Id) return Node_Id is | |
1850 | Args : constant List_Id := Pragma_Argument_Associations (Prag); | |
1851 | Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); | |
1852 | ||
1853 | begin | |
1854 | if Paren_Count (Arg) = 0 then | |
1855 | Set_Paren_Count (Arg, 1); | |
1856 | end if; | |
1857 | ||
1858 | return Arg; | |
1859 | end Expression_Arg; | |
1860 | ||
1861 | ----------------- | |
1862 | -- Message_Arg -- | |
1863 | ----------------- | |
1864 | ||
1865 | function Message_Arg (Prag : Node_Id) return Node_Id is | |
1866 | Args : constant List_Id := Pragma_Argument_Associations (Prag); | |
1867 | begin | |
1868 | return Get_Pragma_Arg (Last (Args)); | |
1869 | end Message_Arg; | |
1870 | ||
1871 | -- Local variables | |
1872 | ||
1873 | From_Expr : constant Node_Id := Expression_Arg (From); | |
1874 | From_Msg : constant Node_Id := Message_Arg (From); | |
1875 | Into_Expr : constant Node_Id := Expression_Arg (Into); | |
1876 | Into_Msg : constant Node_Id := Message_Arg (Into); | |
1877 | Loc : constant Source_Ptr := Sloc (Into); | |
1878 | ||
1879 | -- Start of processing for Merge_Preconditions | |
1880 | ||
1881 | begin | |
1882 | -- Merge the two preconditions by "or else"-ing them | |
1883 | ||
1884 | Rewrite (Into_Expr, | |
1885 | Make_Or_Else (Loc, | |
1886 | Right_Opnd => Relocate_Node (Into_Expr), | |
1887 | Left_Opnd => From_Expr)); | |
1888 | ||
1889 | -- Merge the two error messages to produce a single message of the | |
1890 | -- form: | |
1891 | ||
1892 | -- failed precondition from ... | |
1893 | -- also failed inherited precondition from ... | |
1894 | ||
1895 | if not Exception_Locations_Suppressed then | |
1896 | Start_String (Strval (Into_Msg)); | |
1897 | Store_String_Char (ASCII.LF); | |
1898 | Store_String_Chars (" also "); | |
1899 | Store_String_Chars (Strval (From_Msg)); | |
1900 | ||
1901 | Set_Strval (Into_Msg, End_String); | |
1902 | end if; | |
1903 | end Merge_Preconditions; | |
1904 | ||
1905 | ---------------------- | |
1906 | -- Prepend_To_Decls -- | |
1907 | ---------------------- | |
1908 | ||
1909 | procedure Prepend_To_Decls (Item : Node_Id) is | |
1910 | Decls : List_Id := Declarations (Body_Decl); | |
1911 | ||
1912 | begin | |
1913 | -- Ensure that the body has a declarative list | |
1914 | ||
1915 | if No (Decls) then | |
1916 | Decls := New_List; | |
1917 | Set_Declarations (Body_Decl, Decls); | |
1918 | end if; | |
1919 | ||
1920 | Prepend_To (Decls, Item); | |
1921 | end Prepend_To_Decls; | |
1922 | ||
1923 | ------------------------------ | |
1924 | -- Prepend_To_Decls_Or_Save -- | |
1925 | ------------------------------ | |
1926 | ||
1927 | procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is | |
1928 | Check_Prag : Node_Id; | |
1929 | ||
1930 | begin | |
1931 | Check_Prag := Build_Pragma_Check_Equivalent (Prag); | |
1932 | ||
1933 | -- Save the sole class-wide precondition (if any) for the next | |
e96b7045 | 1934 | -- step, where it will be merged with inherited preconditions. |
879ac954 AC |
1935 | |
1936 | if Class_Present (Prag) then | |
1937 | pragma Assert (No (Class_Pre)); | |
1938 | Class_Pre := Check_Prag; | |
1939 | ||
1940 | -- Accumulate the corresponding Check pragmas at the top of the | |
1941 | -- declarations. Prepending the items ensures that they will be | |
1942 | -- evaluated in their original order. | |
1943 | ||
1944 | else | |
1945 | if Present (Insert_Node) then | |
1946 | Insert_After (Insert_Node, Check_Prag); | |
1947 | else | |
1948 | Prepend_To_Decls (Check_Prag); | |
1949 | end if; | |
1950 | ||
1951 | Analyze (Check_Prag); | |
1952 | end if; | |
1953 | end Prepend_To_Decls_Or_Save; | |
1954 | ||
1955 | ------------------------------------- | |
1956 | -- Process_Inherited_Preconditions -- | |
1957 | ------------------------------------- | |
1958 | ||
1959 | procedure Process_Inherited_Preconditions is | |
1960 | Subps : constant Subprogram_List := | |
1961 | Inherited_Subprograms (Spec_Id); | |
1962 | Check_Prag : Node_Id; | |
1963 | Items : Node_Id; | |
1964 | Prag : Node_Id; | |
1965 | Subp_Id : Entity_Id; | |
1966 | ||
1967 | begin | |
1968 | -- Process the contracts of all inherited subprograms, looking for | |
1969 | -- class-wide preconditions. | |
1970 | ||
1971 | for Index in Subps'Range loop | |
1972 | Subp_Id := Subps (Index); | |
1973 | Items := Contract (Subp_Id); | |
1974 | ||
1975 | if Present (Items) then | |
1976 | Prag := Pre_Post_Conditions (Items); | |
1977 | while Present (Prag) loop | |
1978 | if Pragma_Name (Prag) = Name_Precondition | |
1979 | and then Class_Present (Prag) | |
1980 | then | |
1981 | Check_Prag := | |
1982 | Build_Pragma_Check_Equivalent | |
1983 | (Prag => Prag, | |
1984 | Subp_Id => Spec_Id, | |
1985 | Inher_Id => Subp_Id); | |
1986 | ||
e96b7045 | 1987 | -- The spec of an inherited subprogram already yielded |
879ac954 AC |
1988 | -- a class-wide precondition. Merge the existing |
1989 | -- precondition with the current one using "or else". | |
1990 | ||
1991 | if Present (Class_Pre) then | |
1992 | Merge_Preconditions (Check_Prag, Class_Pre); | |
1993 | else | |
1994 | Class_Pre := Check_Prag; | |
1995 | end if; | |
1996 | end if; | |
1997 | ||
1998 | Prag := Next_Pragma (Prag); | |
1999 | end loop; | |
2000 | end if; | |
2001 | end loop; | |
2002 | ||
2003 | -- Add the merged class-wide preconditions | |
2004 | ||
2005 | if Present (Class_Pre) then | |
2006 | Prepend_To_Decls (Class_Pre); | |
2007 | Analyze (Class_Pre); | |
2008 | end if; | |
2009 | end Process_Inherited_Preconditions; | |
2010 | ||
2011 | ------------------------------- | |
2012 | -- Process_Preconditions_For -- | |
2013 | ------------------------------- | |
2014 | ||
2015 | procedure Process_Preconditions_For (Subp_Id : Entity_Id) is | |
2016 | Items : constant Node_Id := Contract (Subp_Id); | |
2017 | Decl : Node_Id; | |
2018 | Prag : Node_Id; | |
2019 | Subp_Decl : Node_Id; | |
2020 | ||
2021 | begin | |
2022 | -- Process the contract | |
2023 | ||
2024 | if Present (Items) then | |
2025 | Prag := Pre_Post_Conditions (Items); | |
2026 | while Present (Prag) loop | |
2027 | if Pragma_Name (Prag) = Name_Precondition then | |
2028 | Prepend_To_Decls_Or_Save (Prag); | |
2029 | end if; | |
2030 | ||
2031 | Prag := Next_Pragma (Prag); | |
2032 | end loop; | |
2033 | end if; | |
2034 | ||
2035 | -- The subprogram declaration being processed is actually a body | |
e96b7045 AC |
2036 | -- stub. The stub may carry a precondition pragma, in which case |
2037 | -- it must be taken into account. The pragma appears after the | |
2038 | -- stub. | |
879ac954 AC |
2039 | |
2040 | Subp_Decl := Unit_Declaration_Node (Subp_Id); | |
2041 | ||
2042 | if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then | |
2043 | ||
2044 | -- Inspect the declarations following the body stub | |
2045 | ||
2046 | Decl := Next (Subp_Decl); | |
2047 | while Present (Decl) loop | |
2048 | ||
2049 | -- Note that non-matching pragmas are skipped | |
2050 | ||
2051 | if Nkind (Decl) = N_Pragma then | |
2052 | if Pragma_Name (Decl) = Name_Precondition then | |
2053 | Prepend_To_Decls_Or_Save (Decl); | |
2054 | end if; | |
2055 | ||
2056 | -- Skip internally generated code | |
2057 | ||
2058 | elsif not Comes_From_Source (Decl) then | |
2059 | null; | |
2060 | ||
2061 | -- Preconditions are usually grouped together. There is no | |
2062 | -- need to inspect the whole declarative list. | |
2063 | ||
2064 | else | |
2065 | exit; | |
2066 | end if; | |
2067 | ||
2068 | Next (Decl); | |
2069 | end loop; | |
2070 | end if; | |
2071 | end Process_Preconditions_For; | |
2072 | ||
2073 | -- Local variables | |
2074 | ||
2075 | Decls : constant List_Id := Declarations (Body_Decl); | |
2076 | Decl : Node_Id; | |
2077 | ||
2078 | -- Start of processing for Process_Preconditions | |
2079 | ||
2080 | begin | |
e96b7045 | 2081 | -- Find the last internally generated declaration, starting from the |
879ac954 AC |
2082 | -- top of the body declarations. This ensures that discriminals and |
2083 | -- subtypes are properly visible to the pragma Check equivalents. | |
2084 | ||
2085 | if Present (Decls) then | |
2086 | Decl := First (Decls); | |
2087 | while Present (Decl) loop | |
2088 | exit when Comes_From_Source (Decl); | |
2089 | Insert_Node := Decl; | |
2090 | Next (Decl); | |
2091 | end loop; | |
2092 | end if; | |
2093 | ||
2094 | -- The processing of preconditions is done in reverse order (body | |
e96b7045 | 2095 | -- first), because each pragma Check equivalent is inserted at the |
879ac954 AC |
2096 | -- top of the declarations. This ensures that the final order is |
2097 | -- consistent with following diagram: | |
2098 | ||
2099 | -- <inherited preconditions> | |
2100 | -- <preconditions from spec> | |
2101 | -- <preconditions from body> | |
2102 | ||
2103 | Process_Preconditions_For (Body_Id); | |
2104 | ||
2105 | if Present (Spec_Id) then | |
2106 | Process_Preconditions_For (Spec_Id); | |
2107 | Process_Inherited_Preconditions; | |
2108 | end if; | |
2109 | end Process_Preconditions; | |
2110 | ||
2111 | -- Local variables | |
2112 | ||
2113 | Restore_Scope : Boolean := False; | |
2114 | Result : Entity_Id; | |
2115 | Stmts : List_Id := No_List; | |
2116 | Subp_Id : Entity_Id; | |
2117 | ||
2118 | -- Start of processing for Expand_Subprogram_Contract | |
2119 | ||
2120 | begin | |
2121 | -- Obtain the entity of the initial declaration | |
2122 | ||
2123 | if Present (Spec_Id) then | |
2124 | Subp_Id := Spec_Id; | |
2125 | else | |
2126 | Subp_Id := Body_Id; | |
2127 | end if; | |
2128 | ||
2129 | -- Do not perform expansion activity when it is not needed | |
2130 | ||
2131 | if not Expander_Active then | |
2132 | return; | |
2133 | ||
2134 | -- ASIS requires an unaltered tree | |
2135 | ||
2136 | elsif ASIS_Mode then | |
2137 | return; | |
2138 | ||
2139 | -- GNATprove does not need the executable semantics of a contract | |
2140 | ||
2141 | elsif GNATprove_Mode then | |
2142 | return; | |
2143 | ||
2144 | -- The contract of a generic subprogram or one declared in a generic | |
e96b7045 | 2145 | -- context is not expanded, as the corresponding instance will provide |
879ac954 AC |
2146 | -- the executable semantics of the contract. |
2147 | ||
2148 | elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then | |
2149 | return; | |
2150 | ||
2151 | -- All subprograms carry a contract, but for some it is not significant | |
2152 | -- and should not be processed. This is a small optimization. | |
2153 | ||
2154 | elsif not Has_Significant_Contract (Subp_Id) then | |
2155 | return; | |
2156 | ||
e96b7045 | 2157 | -- The contract of an ignored Ghost subprogram does not need expansion, |
879ac954 AC |
2158 | -- because the subprogram and all calls to it will be removed. |
2159 | ||
2160 | elsif Is_Ignored_Ghost_Entity (Subp_Id) then | |
2161 | return; | |
2162 | end if; | |
2163 | ||
2164 | -- Do not re-expand the same contract. This scenario occurs when a | |
2165 | -- construct is rewritten into something else during its analysis | |
2166 | -- (expression functions for instance). | |
2167 | ||
2168 | if Has_Expanded_Contract (Subp_Id) then | |
2169 | return; | |
2170 | ||
2171 | -- Otherwise mark the subprogram | |
2172 | ||
2173 | else | |
2174 | Set_Has_Expanded_Contract (Subp_Id); | |
2175 | end if; | |
2176 | ||
2177 | -- Ensure that the formal parameters are visible when expanding all | |
2178 | -- contract items. | |
2179 | ||
2180 | if not In_Open_Scopes (Subp_Id) then | |
2181 | Restore_Scope := True; | |
2182 | Push_Scope (Subp_Id); | |
2183 | ||
2184 | if Is_Generic_Subprogram (Subp_Id) then | |
2185 | Install_Generic_Formals (Subp_Id); | |
2186 | else | |
2187 | Install_Formals (Subp_Id); | |
2188 | end if; | |
2189 | end if; | |
2190 | ||
2191 | -- The expansion of a subprogram contract involves the creation of Check | |
2192 | -- pragmas to verify the contract assertions of the spec and body in a | |
2193 | -- particular order. The order is as follows: | |
2194 | ||
2195 | -- function Example (...) return ... is | |
2196 | -- procedure _Postconditions (...) is | |
2197 | -- begin | |
2198 | -- <refined postconditions from body> | |
2199 | -- <postconditions from body> | |
2200 | -- <postconditions from spec> | |
2201 | -- <inherited postconditions> | |
2202 | -- <contract case consequences> | |
2203 | -- <invariant check of function result> | |
2204 | -- <invariant and predicate checks of parameters> | |
2205 | -- end _Postconditions; | |
2206 | ||
2207 | -- <inherited preconditions> | |
2208 | -- <preconditions from spec> | |
2209 | -- <preconditions from body> | |
2210 | -- <contract case conditions> | |
2211 | ||
2212 | -- <source declarations> | |
2213 | -- begin | |
2214 | -- <source statements> | |
2215 | ||
2216 | -- _Preconditions (Result); | |
2217 | -- return Result; | |
2218 | -- end Example; | |
2219 | ||
2220 | -- Routine _Postconditions holds all contract assertions that must be | |
2221 | -- verified on exit from the related subprogram. | |
2222 | ||
2223 | -- Step 1: Handle all preconditions. This action must come before the | |
2224 | -- processing of pragma Contract_Cases because the pragma prepends items | |
2225 | -- to the body declarations. | |
2226 | ||
2227 | Process_Preconditions; | |
2228 | ||
2229 | -- Step 2: Handle all postconditions. This action must come before the | |
2230 | -- processing of pragma Contract_Cases because the pragma appends items | |
2231 | -- to list Stmts. | |
2232 | ||
2233 | Process_Postconditions (Stmts); | |
2234 | ||
2235 | -- Step 3: Handle pragma Contract_Cases. This action must come before | |
2236 | -- the processing of invariants and predicates because those append | |
e96b7045 | 2237 | -- items to list Stmts. |
879ac954 AC |
2238 | |
2239 | Process_Contract_Cases (Stmts); | |
2240 | ||
2241 | -- Step 4: Apply invariant and predicate checks on a function result and | |
2242 | -- all formals. The resulting checks are accumulated in list Stmts. | |
2243 | ||
2244 | Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); | |
2245 | ||
2246 | -- Step 5: Construct procedure _Postconditions | |
2247 | ||
2248 | Build_Postconditions_Procedure (Subp_Id, Stmts, Result); | |
2249 | ||
2250 | if Restore_Scope then | |
2251 | End_Scope; | |
2252 | end if; | |
2253 | end Expand_Subprogram_Contract; | |
2254 | ||
2255 | --------------------------------- | |
2256 | -- Inherit_Subprogram_Contract -- | |
2257 | --------------------------------- | |
2258 | ||
2259 | procedure Inherit_Subprogram_Contract | |
2260 | (Subp : Entity_Id; | |
2261 | From_Subp : Entity_Id) | |
2262 | is | |
2263 | procedure Inherit_Pragma (Prag_Id : Pragma_Id); | |
2264 | -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to | |
2265 | -- Subp's contract. | |
2266 | ||
2267 | -------------------- | |
2268 | -- Inherit_Pragma -- | |
2269 | -------------------- | |
2270 | ||
2271 | procedure Inherit_Pragma (Prag_Id : Pragma_Id) is | |
2272 | Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id); | |
2273 | New_Prag : Node_Id; | |
2274 | ||
2275 | begin | |
2276 | -- A pragma cannot be part of more than one First_Pragma/Next_Pragma | |
2277 | -- chains, therefore the node must be replicated. The new pragma is | |
e96b7045 | 2278 | -- flagged as inherited for distinction purposes. |
879ac954 AC |
2279 | |
2280 | if Present (Prag) then | |
2281 | New_Prag := New_Copy_Tree (Prag); | |
2ba4f1fb | 2282 | Set_Is_Inherited_Pragma (New_Prag); |
879ac954 AC |
2283 | |
2284 | Add_Contract_Item (New_Prag, Subp); | |
2285 | end if; | |
2286 | end Inherit_Pragma; | |
2287 | ||
2288 | -- Start of processing for Inherit_Subprogram_Contract | |
2289 | ||
2290 | begin | |
2291 | -- Inheritance is carried out only when both entities are subprograms | |
2292 | -- with contracts. | |
2293 | ||
2294 | if Is_Subprogram_Or_Generic_Subprogram (Subp) | |
2295 | and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) | |
2296 | and then Present (Contract (From_Subp)) | |
2297 | then | |
2298 | Inherit_Pragma (Pragma_Extensions_Visible); | |
2299 | end if; | |
2300 | end Inherit_Subprogram_Contract; | |
2301 | ||
2302 | ------------------------------------- | |
2303 | -- Instantiate_Subprogram_Contract -- | |
2304 | ------------------------------------- | |
2305 | ||
2306 | procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is | |
2307 | procedure Instantiate_Pragmas (First_Prag : Node_Id); | |
e96b7045 | 2308 | -- Instantiate all contract-related source pragmas found in the list, |
879ac954 AC |
2309 | -- starting with pragma First_Prag. Each instantiated pragma is added |
2310 | -- to list L. | |
2311 | ||
2312 | ------------------------- | |
2313 | -- Instantiate_Pragmas -- | |
2314 | ------------------------- | |
2315 | ||
2316 | procedure Instantiate_Pragmas (First_Prag : Node_Id) is | |
2317 | Inst_Prag : Node_Id; | |
2318 | Prag : Node_Id; | |
2319 | ||
2320 | begin | |
2321 | Prag := First_Prag; | |
2322 | while Present (Prag) loop | |
2323 | if Is_Generic_Contract_Pragma (Prag) then | |
2324 | Inst_Prag := | |
2325 | Copy_Generic_Node (Prag, Empty, Instantiating => True); | |
2326 | ||
2327 | Set_Analyzed (Inst_Prag, False); | |
2328 | Append_To (L, Inst_Prag); | |
2329 | end if; | |
2330 | ||
2331 | Prag := Next_Pragma (Prag); | |
2332 | end loop; | |
2333 | end Instantiate_Pragmas; | |
2334 | ||
2335 | -- Local variables | |
2336 | ||
2337 | Items : constant Node_Id := Contract (Defining_Entity (Templ)); | |
2338 | ||
2339 | -- Start of processing for Instantiate_Subprogram_Contract | |
2340 | ||
2341 | begin | |
2342 | if Present (Items) then | |
2343 | Instantiate_Pragmas (Pre_Post_Conditions (Items)); | |
2344 | Instantiate_Pragmas (Contract_Test_Cases (Items)); | |
2345 | Instantiate_Pragmas (Classifications (Items)); | |
2346 | end if; | |
2347 | end Instantiate_Subprogram_Contract; | |
2348 | ||
2349 | ---------------------------------------- | |
2350 | -- Save_Global_References_In_Contract -- | |
2351 | ---------------------------------------- | |
2352 | ||
2353 | procedure Save_Global_References_In_Contract | |
2354 | (Templ : Node_Id; | |
2355 | Gen_Id : Entity_Id) | |
2356 | is | |
2357 | procedure Save_Global_References_In_List (First_Prag : Node_Id); | |
2358 | -- Save all global references in contract-related source pragmas found | |
e96b7045 | 2359 | -- in the list, starting with pragma First_Prag. |
879ac954 AC |
2360 | |
2361 | ------------------------------------ | |
2362 | -- Save_Global_References_In_List -- | |
2363 | ------------------------------------ | |
2364 | ||
2365 | procedure Save_Global_References_In_List (First_Prag : Node_Id) is | |
2366 | Prag : Node_Id; | |
2367 | ||
2368 | begin | |
2369 | Prag := First_Prag; | |
2370 | while Present (Prag) loop | |
2371 | if Is_Generic_Contract_Pragma (Prag) then | |
2372 | Save_Global_References (Prag); | |
2373 | end if; | |
2374 | ||
2375 | Prag := Next_Pragma (Prag); | |
2376 | end loop; | |
2377 | end Save_Global_References_In_List; | |
2378 | ||
2379 | -- Local variables | |
2380 | ||
2381 | Items : constant Node_Id := Contract (Defining_Entity (Templ)); | |
2382 | ||
2383 | -- Start of processing for Save_Global_References_In_Contract | |
2384 | ||
2385 | begin | |
2386 | -- The entity of the analyzed generic copy must be on the scope stack | |
2387 | -- to ensure proper detection of global references. | |
2388 | ||
2389 | Push_Scope (Gen_Id); | |
2390 | ||
2391 | if Permits_Aspect_Specifications (Templ) | |
2392 | and then Has_Aspects (Templ) | |
2393 | then | |
2394 | Save_Global_References_In_Aspects (Templ); | |
2395 | end if; | |
2396 | ||
2397 | if Present (Items) then | |
2398 | Save_Global_References_In_List (Pre_Post_Conditions (Items)); | |
2399 | Save_Global_References_In_List (Contract_Test_Cases (Items)); | |
2400 | Save_Global_References_In_List (Classifications (Items)); | |
2401 | end if; | |
2402 | ||
2403 | Pop_Scope; | |
2404 | end Save_Global_References_In_Contract; | |
2405 | ||
2406 | end Contracts; |