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