hppa: Fix LO_SUM DLTIND14R address support in PRINT_OPERAND_ADDRESS
[official-gcc.git] / gcc / ada / contracts.adb
blob551e9f3c32ce0358fb8882e45b22a3d309982f3b
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-2024, 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 ------------------------------------------------------------------------------
26 with Aspects; use Aspects;
27 with Atree; use Atree;
28 with Einfo; use Einfo;
29 with Einfo.Entities; use Einfo.Entities;
30 with Einfo.Utils; use Einfo.Utils;
31 with Elists; use Elists;
32 with Errout; use Errout;
33 with Exp_Prag; use Exp_Prag;
34 with Exp_Tss; use Exp_Tss;
35 with Exp_Util; use Exp_Util;
36 with Freeze; use Freeze;
37 with Lib; use Lib;
38 with Namet; use Namet;
39 with Nlists; use Nlists;
40 with Nmake; use Nmake;
41 with Opt; use Opt;
42 with Sem; use Sem;
43 with Sem_Aux; use Sem_Aux;
44 with Sem_Ch3; use Sem_Ch3;
45 with Sem_Ch6; use Sem_Ch6;
46 with Sem_Ch8; use Sem_Ch8;
47 with Sem_Ch12; use Sem_Ch12;
48 with Sem_Ch13; use Sem_Ch13;
49 with Sem_Disp; use Sem_Disp;
50 with Sem_Prag; use Sem_Prag;
51 with Sem_Type; use Sem_Type;
52 with Sem_Util; use Sem_Util;
53 with Sinfo; use Sinfo;
54 with Sinfo.Nodes; use Sinfo.Nodes;
55 with Sinfo.Utils; use Sinfo.Utils;
56 with Sinput; use Sinput;
57 with Snames; use Snames;
58 with Stand; use Stand;
59 with Stringt; use Stringt;
60 with Tbuild; use Tbuild;
61 with Warnsw; use Warnsw;
63 package body Contracts is
65 Contract_Error : exception;
66 -- This exception is raised by Add_Contract_Item when it is invoked on an
67 -- invalid pragma. Note that clients of the package must filter them out
68 -- before invoking Add_Contract_Item, so it should not escape the package.
70 procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id);
71 -- Analyze all delayed pragmas chained on the contract of package
72 -- instantiation Inst_Id as if they appear at the end of a declarative
73 -- region. The pragmas in question are:
75 -- Part_Of
77 procedure Build_Subprogram_Contract_Wrapper
78 (Body_Id : Entity_Id;
79 Stmts : List_Id;
80 Decls : List_Id;
81 Result : Entity_Id);
82 -- Generate a wrapper for a given subprogram body when the expansion of
83 -- postconditions require it by moving its declarations and statements
84 -- into a locally declared subprogram _Wrapped_Statements.
86 -- Postcondition and precondition checks then get inserted in place of
87 -- the original statements and declarations along with a call to
88 -- _Wrapped_Statements.
90 procedure Check_Class_Condition
91 (Cond : Node_Id;
92 Subp : Entity_Id;
93 Par_Subp : Entity_Id;
94 Is_Precondition : Boolean);
95 -- Perform checking of class-wide pre/postcondition Cond inherited by Subp
96 -- from Par_Subp. Is_Precondition enables check specific for preconditions.
97 -- In SPARK_Mode, an inherited operation that is not overridden but has
98 -- inherited modified conditions pre/postconditions is illegal.
100 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
101 -- Determine whether arbitrary declaration Decl denotes a renaming of
102 -- a discriminant or protection field _object.
104 procedure Check_Type_Or_Object_External_Properties
105 (Type_Or_Obj_Id : Entity_Id);
106 -- Perform checking of external properties pragmas that is common to both
107 -- type declarations and object declarations.
109 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
110 -- Expand the contracts of a subprogram body and its correspoding spec (if
111 -- any). This routine processes all [refined] pre- and postconditions as
112 -- well as Always_Terminates, Contract_Cases, Exceptional_Cases,
113 -- Subprogram_Variant, invariants and predicates. Body_Id denotes the
114 -- entity of the subprogram body.
116 procedure Preanalyze_Condition
117 (Subp : Entity_Id;
118 Expr : Node_Id);
119 -- Preanalyze the class-wide condition Expr of Subp
121 procedure Set_Class_Condition
122 (Kind : Condition_Kind;
123 Subp : Entity_Id;
124 Cond : Node_Id);
125 -- Set the class-wide Kind condition of Subp
127 -----------------------
128 -- Add_Contract_Item --
129 -----------------------
131 procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
132 Items : Node_Id := Contract (Id);
134 procedure Add_Classification;
135 -- Prepend Prag to the list of classifications
137 procedure Add_Contract_Test_Case;
138 -- Prepend Prag to the list of contract and test cases
140 procedure Add_Pre_Post_Condition;
141 -- Prepend Prag to the list of pre- and postconditions
143 ------------------------
144 -- Add_Classification --
145 ------------------------
147 procedure Add_Classification is
148 begin
149 Set_Next_Pragma (Prag, Classifications (Items));
150 Set_Classifications (Items, Prag);
151 end Add_Classification;
153 ----------------------------
154 -- Add_Contract_Test_Case --
155 ----------------------------
157 procedure Add_Contract_Test_Case is
158 begin
159 Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
160 Set_Contract_Test_Cases (Items, Prag);
161 end Add_Contract_Test_Case;
163 ----------------------------
164 -- Add_Pre_Post_Condition --
165 ----------------------------
167 procedure Add_Pre_Post_Condition is
168 begin
169 Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
170 Set_Pre_Post_Conditions (Items, Prag);
171 end Add_Pre_Post_Condition;
173 -- Local variables
175 -- A contract must contain only pragmas
177 pragma Assert (Nkind (Prag) = N_Pragma);
178 Prag_Nam : constant Name_Id := Pragma_Name (Prag);
180 -- Start of processing for Add_Contract_Item
182 begin
183 -- Create a new contract when adding the first item
185 if No (Items) then
186 Items := Make_Contract (Sloc (Id));
187 Set_Contract (Id, Items);
188 end if;
190 -- Constants, the applicable pragmas are:
191 -- Part_Of
193 if Ekind (Id) = E_Constant then
194 if Prag_Nam in Name_Async_Readers
195 | Name_Async_Writers
196 | Name_Effective_Reads
197 | Name_Effective_Writes
198 | Name_No_Caching
199 | Name_Part_Of
200 then
201 Add_Classification;
203 -- The pragma is not a proper contract item
205 else
206 raise Contract_Error;
207 end if;
209 -- Entry bodies, the applicable pragmas are:
210 -- Refined_Depends
211 -- Refined_Global
212 -- Refined_Post
214 elsif Is_Entry_Body (Id) then
215 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then
216 Add_Classification;
218 elsif Prag_Nam = Name_Refined_Post then
219 Add_Pre_Post_Condition;
221 -- The pragma is not a proper contract item
223 else
224 raise Contract_Error;
225 end if;
227 -- Entry or subprogram declarations, the applicable pragmas are:
228 -- Always_Terminates
229 -- Attach_Handler
230 -- Contract_Cases
231 -- Depends
232 -- Exceptional_Cases
233 -- Extensions_Visible
234 -- Global
235 -- Interrupt_Handler
236 -- Postcondition
237 -- Precondition
238 -- Side_Effects
239 -- Subprogram_Variant
240 -- Test_Case
241 -- Volatile_Function
243 elsif Is_Entry_Declaration (Id)
244 or else Ekind (Id) in E_Function
245 | E_Generic_Function
246 | E_Generic_Procedure
247 | E_Procedure
248 then
249 if Prag_Nam in Name_Attach_Handler | Name_Interrupt_Handler
250 and then Ekind (Id) in E_Generic_Procedure | E_Procedure
251 then
252 Add_Classification;
254 elsif Prag_Nam in Name_Depends
255 | Name_Extensions_Visible
256 | Name_Global
257 | Name_Side_Effects
258 then
259 Add_Classification;
261 elsif Prag_Nam = Name_Volatile_Function
262 and then Ekind (Id) in E_Function | E_Generic_Function
263 then
264 Add_Classification;
266 elsif Prag_Nam in Name_Always_Terminates
267 | Name_Contract_Cases
268 | Name_Exceptional_Cases
269 | Name_Subprogram_Variant
270 | Name_Test_Case
271 then
272 Add_Contract_Test_Case;
274 elsif Prag_Nam in Name_Postcondition | Name_Precondition then
275 Add_Pre_Post_Condition;
277 -- The pragma is not a proper contract item
279 else
280 raise Contract_Error;
281 end if;
283 -- Packages or instantiations, the applicable pragmas are:
284 -- Abstract_States
285 -- Initial_Condition
286 -- Initializes
287 -- Part_Of (instantiation only)
289 elsif Is_Package_Or_Generic_Package (Id) then
290 if Prag_Nam in Name_Abstract_State
291 | Name_Initial_Condition
292 | Name_Initializes
293 then
294 Add_Classification;
296 -- Indicator Part_Of must be associated with a package instantiation
298 elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
299 Add_Classification;
301 elsif Prag_Nam = Name_Always_Terminates then
302 Add_Contract_Test_Case;
304 -- The pragma is not a proper contract item
306 else
307 raise Contract_Error;
308 end if;
310 -- Package bodies, the applicable pragmas are:
311 -- Refined_States
313 elsif Ekind (Id) = E_Package_Body then
314 if Prag_Nam = Name_Refined_State then
315 Add_Classification;
317 -- The pragma is not a proper contract item
319 else
320 raise Contract_Error;
321 end if;
323 -- The four volatility refinement pragmas are ok for all types.
324 -- Part_Of is ok for task types and protected types.
325 -- Depends and Global are ok for task types.
327 -- Precondition and Postcondition are added separately; they are allowed
328 -- for access-to-subprogram types.
330 elsif Is_Type (Id) then
331 declare
332 Is_OK_Classification : constant Boolean :=
333 Prag_Nam in Name_Async_Readers
334 | Name_Async_Writers
335 | Name_Effective_Reads
336 | Name_Effective_Writes
337 | Name_No_Caching
338 or else (Ekind (Id) = E_Task_Type
339 and Prag_Nam in Name_Part_Of
340 | Name_Depends
341 | Name_Global)
342 or else (Ekind (Id) = E_Protected_Type
343 and Prag_Nam = Name_Part_Of);
345 begin
346 if Is_OK_Classification then
347 Add_Classification;
349 elsif Ekind (Id) = E_Subprogram_Type
350 and then Prag_Nam in Name_Precondition
351 | Name_Postcondition
352 then
353 Add_Pre_Post_Condition;
354 else
356 -- The pragma is not a proper contract item
358 raise Contract_Error;
359 end if;
360 end;
362 -- Subprogram bodies, the applicable pragmas are:
363 -- Postcondition
364 -- Precondition
365 -- Refined_Depends
366 -- Refined_Global
367 -- Refined_Post
369 elsif Ekind (Id) = E_Subprogram_Body then
370 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then
371 Add_Classification;
373 elsif Prag_Nam in Name_Postcondition
374 | Name_Precondition
375 | Name_Refined_Post
376 then
377 Add_Pre_Post_Condition;
379 -- The pragma is not a proper contract item
381 else
382 raise Contract_Error;
383 end if;
385 -- Task bodies, the applicable pragmas are:
386 -- Refined_Depends
387 -- Refined_Global
389 elsif Ekind (Id) = E_Task_Body then
390 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then
391 Add_Classification;
393 -- The pragma is not a proper contract item
395 else
396 raise Contract_Error;
397 end if;
399 -- Task units, the applicable pragmas are:
400 -- Depends
401 -- Global
402 -- Part_Of
404 -- Variables, the applicable pragmas are:
405 -- Async_Readers
406 -- Async_Writers
407 -- Constant_After_Elaboration
408 -- Depends
409 -- Effective_Reads
410 -- Effective_Writes
411 -- Global
412 -- No_Caching
413 -- Part_Of
415 elsif Ekind (Id) = E_Variable then
416 if Prag_Nam in Name_Async_Readers
417 | Name_Async_Writers
418 | Name_Constant_After_Elaboration
419 | Name_Depends
420 | Name_Effective_Reads
421 | Name_Effective_Writes
422 | Name_Global
423 | Name_No_Caching
424 | Name_Part_Of
425 then
426 Add_Classification;
428 -- The pragma is not a proper contract item
430 else
431 raise Contract_Error;
432 end if;
434 else
435 raise Contract_Error;
436 end if;
437 end Add_Contract_Item;
439 -----------------------
440 -- Analyze_Contracts --
441 -----------------------
443 procedure Analyze_Contracts (L : List_Id) is
444 Decl : Node_Id;
446 begin
447 Decl := First (L);
448 while Present (Decl) loop
450 -- Entry or subprogram declarations
452 if Nkind (Decl) in N_Abstract_Subprogram_Declaration
453 | N_Entry_Declaration
454 | N_Generic_Subprogram_Declaration
455 | N_Subprogram_Declaration
456 then
457 Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
459 -- Entry or subprogram bodies
461 elsif Nkind (Decl) in N_Entry_Body | N_Subprogram_Body then
462 Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl));
464 -- Objects
466 elsif Nkind (Decl) = N_Object_Declaration then
467 Analyze_Object_Contract (Defining_Entity (Decl));
469 -- Package instantiation
471 elsif Nkind (Decl) = N_Package_Instantiation then
472 Analyze_Package_Instantiation_Contract (Defining_Entity (Decl));
474 -- Protected units
476 elsif Nkind (Decl) in N_Protected_Type_Declaration
477 | N_Single_Protected_Declaration
478 then
479 Analyze_Protected_Contract (Defining_Entity (Decl));
481 -- Subprogram body stubs
483 elsif Nkind (Decl) = N_Subprogram_Body_Stub then
484 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
486 -- Task units
488 elsif Nkind (Decl) in N_Single_Task_Declaration
489 | N_Task_Type_Declaration
490 then
491 Analyze_Task_Contract (Defining_Entity (Decl));
493 -- For type declarations, we need to do the preanalysis of Iterable
494 -- and the 3 Xxx_Literal aspect specifications.
496 -- Other type aspects need to be resolved here???
498 elsif Nkind (Decl) = N_Private_Type_Declaration
499 and then Present (Aspect_Specifications (Decl))
500 then
501 declare
502 E : constant Entity_Id := Defining_Identifier (Decl);
503 It : constant Node_Id := Find_Aspect (E, Aspect_Iterable);
504 I_Lit : constant Node_Id :=
505 Find_Aspect (E, Aspect_Integer_Literal);
506 R_Lit : constant Node_Id :=
507 Find_Aspect (E, Aspect_Real_Literal);
508 S_Lit : constant Node_Id :=
509 Find_Aspect (E, Aspect_String_Literal);
511 begin
512 if Present (It) then
513 Validate_Iterable_Aspect (E, It);
514 end if;
516 if Present (I_Lit) then
517 Validate_Literal_Aspect (E, I_Lit);
518 end if;
519 if Present (R_Lit) then
520 Validate_Literal_Aspect (E, R_Lit);
521 end if;
522 if Present (S_Lit) then
523 Validate_Literal_Aspect (E, S_Lit);
524 end if;
525 end;
526 end if;
528 if Nkind (Decl) in N_Full_Type_Declaration
529 | N_Private_Type_Declaration
530 | N_Task_Type_Declaration
531 | N_Protected_Type_Declaration
532 | N_Formal_Type_Declaration
533 then
534 Analyze_Type_Contract (Defining_Identifier (Decl));
535 end if;
537 Next (Decl);
538 end loop;
539 end Analyze_Contracts;
541 -------------------------------------
542 -- Analyze_Pragmas_In_Declarations --
543 -------------------------------------
545 procedure Analyze_Pragmas_In_Declarations (Body_Id : Entity_Id) is
546 Curr_Decl : Node_Id;
548 begin
549 -- Move through the body's declarations analyzing all pragmas which
550 -- appear at the top of the declarations.
552 Curr_Decl := First (Declarations (Unit_Declaration_Node (Body_Id)));
553 while Present (Curr_Decl) loop
555 if Nkind (Curr_Decl) = N_Pragma then
557 if Pragma_Significant_To_Subprograms
558 (Get_Pragma_Id (Curr_Decl))
559 then
560 Analyze (Curr_Decl);
561 end if;
563 -- Skip the renamings of discriminants and protection fields
565 elsif Is_Prologue_Renaming (Curr_Decl) then
566 null;
568 -- We have reached something which is not a pragma so we can be sure
569 -- there are no more contracts or pragmas which need to be taken into
570 -- account.
572 else
573 exit;
574 end if;
576 Next (Curr_Decl);
577 end loop;
578 end Analyze_Pragmas_In_Declarations;
580 -----------------------------------------------
581 -- Analyze_Entry_Or_Subprogram_Body_Contract --
582 -----------------------------------------------
584 -- WARNING: This routine manages SPARK regions. Return statements must be
585 -- replaced by gotos which jump to the end of the routine and restore the
586 -- SPARK mode.
588 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
589 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
590 Items : constant Node_Id := Contract (Body_Id);
591 Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
593 begin
594 -- When a subprogram body declaration is illegal, its defining entity is
595 -- left unanalyzed. There is nothing left to do in this case because the
596 -- body lacks a contract, or even a proper Ekind.
598 if Ekind (Body_Id) = E_Void then
599 return;
601 -- Do not analyze a contract multiple times
603 elsif Present (Items) then
604 if Analyzed (Items) then
605 return;
606 else
607 Set_Analyzed (Items);
608 end if;
610 -- When this is a subprogram body not coming from source, for example an
611 -- expression function, it does not cause freezing of previous contracts
612 -- (see Analyze_Subprogram_Body_Helper), in particular not of those on
613 -- its spec if it exists. In this case make sure they have been properly
614 -- analyzed before being expanded below, as we may be invoked during the
615 -- freezing of the subprogram in the middle of its enclosing declarative
616 -- part because the declarative part contains e.g. the declaration of a
617 -- variable initialized by means of a call to the subprogram.
619 elsif Nkind (Body_Decl) = N_Subprogram_Body
620 and then not Comes_From_Source (Original_Node (Body_Decl))
621 and then Present (Corresponding_Spec (Body_Decl))
622 and then Present (Contract (Corresponding_Spec (Body_Decl)))
623 then
624 Analyze_Entry_Or_Subprogram_Contract (Corresponding_Spec (Body_Decl));
625 end if;
627 -- Ensure that the contract cases or postconditions mention 'Result or
628 -- define a post-state.
630 Check_Result_And_Post_State (Body_Id);
632 -- Capture all global references in a generic subprogram body now that
633 -- the contract has been analyzed.
635 if Is_Generic_Declaration_Or_Body (Body_Decl) then
636 Save_Global_References_In_Contract
637 (Templ => Original_Node (Body_Decl),
638 Gen_Id => Spec_Id);
639 end if;
641 -- Deal with preconditions, [refined] postconditions, Always_Terminates,
642 -- Contract_Cases, Exceptional_Cases, Subprogram_Variant, invariants and
643 -- predicates associated with body and its spec. Do not expand the
644 -- contract of subprogram body stubs.
646 if Nkind (Body_Decl) = N_Subprogram_Body then
647 Expand_Subprogram_Contract (Body_Id);
648 end if;
649 end Analyze_Entry_Or_Subprogram_Body_Contract;
651 ------------------------------------------
652 -- Analyze_Entry_Or_Subprogram_Contract --
653 ------------------------------------------
655 -- WARNING: This routine manages SPARK regions. Return statements must be
656 -- replaced by gotos which jump to the end of the routine and restore the
657 -- SPARK mode.
659 procedure Analyze_Entry_Or_Subprogram_Contract
660 (Subp_Id : Entity_Id;
661 Freeze_Id : Entity_Id := Empty)
663 Items : constant Node_Id := Contract (Subp_Id);
664 Subp_Decl : constant Node_Id :=
665 (if Ekind (Subp_Id) = E_Subprogram_Type
666 then Associated_Node_For_Itype (Subp_Id)
667 else Unit_Declaration_Node (Subp_Id));
669 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
670 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
671 -- Save the SPARK_Mode-related data to restore on exit
673 Skip_Assert_Exprs : constant Boolean :=
674 Is_Entry (Subp_Id) and then not GNATprove_Mode;
676 Depends : Node_Id := Empty;
677 Global : Node_Id := Empty;
678 Prag : Node_Id;
679 Prag_Nam : Name_Id;
681 begin
682 -- Do not analyze a contract multiple times
684 if Present (Items) then
685 if Analyzed (Items) then
686 return;
687 else
688 Set_Analyzed (Items);
689 end if;
690 end if;
692 -- Due to the timing of contract analysis, delayed pragmas may be
693 -- subject to the wrong SPARK_Mode, usually that of the enclosing
694 -- context. To remedy this, restore the original SPARK_Mode of the
695 -- related subprogram body.
697 Set_SPARK_Mode (Subp_Id);
699 -- All subprograms carry a contract, but for some it is not significant
700 -- and should not be processed.
702 if not Has_Significant_Contract (Subp_Id) then
703 null;
705 elsif Present (Items) then
707 -- Do not analyze the pre/postconditions of an entry declaration
708 -- unless annotating the original tree for GNATprove. The
709 -- real analysis occurs when the pre/postconditons are relocated to
710 -- the contract wrapper procedure (see Build_Contract_Wrapper).
712 if Skip_Assert_Exprs then
713 null;
715 -- Otherwise analyze the pre/postconditions.
716 -- If these come from an aspect specification, their expressions
717 -- might include references to types that are not frozen yet, in the
718 -- case where the body is a rewritten expression function that is a
719 -- completion, so freeze all types within before constructing the
720 -- contract code.
722 else
723 declare
724 Bod : Node_Id := Empty;
725 Freeze_Types : Boolean := False;
727 begin
728 if Present (Freeze_Id) then
729 Bod := Unit_Declaration_Node (Freeze_Id);
731 if Nkind (Bod) = N_Subprogram_Body
732 and then Was_Expression_Function (Bod)
733 and then Ekind (Subp_Id) = E_Function
734 and then Chars (Subp_Id) = Chars (Freeze_Id)
735 and then Subp_Id /= Freeze_Id
736 then
737 Freeze_Types := True;
738 end if;
739 end if;
741 Prag := Pre_Post_Conditions (Items);
742 while Present (Prag) loop
743 if Freeze_Types
744 and then Present (Corresponding_Aspect (Prag))
745 then
746 Freeze_Expr_Types
747 (Def_Id => Subp_Id,
748 Typ => Standard_Boolean,
749 Expr =>
750 Expression
751 (First (Pragma_Argument_Associations (Prag))),
752 N => Bod);
753 end if;
755 Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
756 Prag := Next_Pragma (Prag);
757 end loop;
758 end;
759 end if;
761 -- Analyze contract-cases, subprogram-variant and test-cases
763 Prag := Contract_Test_Cases (Items);
764 while Present (Prag) loop
765 Prag_Nam := Pragma_Name (Prag);
767 if Prag_Nam = Name_Always_Terminates then
768 Analyze_Always_Terminates_In_Decl_Part (Prag);
770 elsif Prag_Nam = Name_Contract_Cases then
772 -- Do not analyze the contract cases of an entry declaration
773 -- unless annotating the original tree for GNATprove.
774 -- The real analysis occurs when the contract cases are moved
775 -- to the contract wrapper procedure (Build_Contract_Wrapper).
777 if Skip_Assert_Exprs then
778 null;
780 -- Otherwise analyze the contract cases
782 else
783 Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
784 end if;
786 elsif Prag_Nam = Name_Exceptional_Cases then
787 Analyze_Exceptional_Cases_In_Decl_Part (Prag);
789 elsif Prag_Nam = Name_Subprogram_Variant then
790 Analyze_Subprogram_Variant_In_Decl_Part (Prag);
792 else
793 pragma Assert (Prag_Nam = Name_Test_Case);
794 Analyze_Test_Case_In_Decl_Part (Prag);
795 end if;
797 Prag := Next_Pragma (Prag);
798 end loop;
800 -- Analyze classification pragmas
802 Prag := Classifications (Items);
803 while Present (Prag) loop
804 Prag_Nam := Pragma_Name (Prag);
806 if Prag_Nam = Name_Depends then
807 Depends := Prag;
809 elsif Prag_Nam = Name_Global then
810 Global := Prag;
811 end if;
813 Prag := Next_Pragma (Prag);
814 end loop;
816 -- Analyze Global first, as Depends may mention items classified in
817 -- the global categorization.
819 if Present (Global) then
820 Analyze_Global_In_Decl_Part (Global);
821 end if;
823 -- Depends must be analyzed after Global in order to see the modes of
824 -- all global items.
826 if Present (Depends) then
827 Analyze_Depends_In_Decl_Part (Depends);
828 end if;
830 -- Ensure that the contract cases or postconditions mention 'Result
831 -- or define a post-state.
833 Check_Result_And_Post_State (Subp_Id);
834 end if;
836 -- Restore the SPARK_Mode of the enclosing context after all delayed
837 -- pragmas have been analyzed.
839 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
841 -- Capture all global references in a generic subprogram now that the
842 -- contract has been analyzed.
844 if Is_Generic_Declaration_Or_Body (Subp_Decl) then
845 Save_Global_References_In_Contract
846 (Templ => Original_Node (Subp_Decl),
847 Gen_Id => Subp_Id);
848 end if;
849 end Analyze_Entry_Or_Subprogram_Contract;
851 ----------------------------------------------
852 -- Check_Type_Or_Object_External_Properties --
853 ----------------------------------------------
855 procedure Check_Type_Or_Object_External_Properties
856 (Type_Or_Obj_Id : Entity_Id)
858 Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id);
860 -- Local variables
862 AR_Val : Boolean := False;
863 AW_Val : Boolean := False;
864 ER_Val : Boolean := False;
865 EW_Val : Boolean := False;
866 NC_Val : Boolean;
867 Seen : Boolean := False;
868 Prag : Node_Id;
870 -- Start of processing for Check_Type_Or_Object_External_Properties
872 begin
873 -- Analyze all external properties
875 if Is_Type_Id then
876 -- If the parent type of a derived type is volatile
877 -- then the derived type inherits volatility-related flags.
879 if Is_Derived_Type (Type_Or_Obj_Id) then
880 declare
881 Parent_Type : constant Entity_Id :=
882 Etype (Base_Type (Type_Or_Obj_Id));
883 begin
884 if Is_Effectively_Volatile (Parent_Type) then
885 AR_Val := Async_Readers_Enabled (Parent_Type);
886 AW_Val := Async_Writers_Enabled (Parent_Type);
887 ER_Val := Effective_Reads_Enabled (Parent_Type);
888 EW_Val := Effective_Writes_Enabled (Parent_Type);
889 end if;
890 end;
891 end if;
892 end if;
894 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers);
896 if Present (Prag) then
897 declare
898 Saved_AR_Val : constant Boolean := AR_Val;
899 begin
900 Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
901 Seen := True;
902 if Saved_AR_Val and not AR_Val then
903 Error_Msg_N
904 ("illegal non-confirming Async_Readers specification",
905 Prag);
906 end if;
907 end;
908 end if;
910 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Writers);
912 if Present (Prag) then
913 declare
914 Saved_AW_Val : constant Boolean := AW_Val;
915 begin
916 Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
917 Seen := True;
918 if Saved_AW_Val and not AW_Val then
919 Error_Msg_N
920 ("illegal non-confirming Async_Writers specification",
921 Prag);
922 end if;
923 end;
924 end if;
926 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Reads);
928 if Present (Prag) then
929 declare
930 Saved_ER_Val : constant Boolean := ER_Val;
931 begin
932 Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
933 Seen := True;
934 if Saved_ER_Val and not ER_Val then
935 Error_Msg_N
936 ("illegal non-confirming Effective_Reads specification",
937 Prag);
938 end if;
939 end;
940 end if;
942 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Writes);
944 if Present (Prag) then
945 declare
946 Saved_EW_Val : constant Boolean := EW_Val;
947 begin
948 Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
949 Seen := True;
950 if Saved_EW_Val and not EW_Val then
951 Error_Msg_N
952 ("illegal non-confirming Effective_Writes specification",
953 Prag);
954 end if;
955 end;
956 end if;
958 -- Verify the mutual interaction of the various external properties.
959 -- For types and variables for which No_Caching is enabled, it has been
960 -- checked already that only False values for other external properties
961 -- are allowed.
963 if Seen
964 and then not No_Caching_Enabled (Type_Or_Obj_Id)
965 then
966 Check_External_Properties
967 (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
968 end if;
970 -- Analyze the non-external volatility property No_Caching
972 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching);
974 if Present (Prag) then
975 Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
976 end if;
977 end Check_Type_Or_Object_External_Properties;
979 -----------------------------
980 -- Analyze_Object_Contract --
981 -----------------------------
983 -- WARNING: This routine manages SPARK regions. Return statements must be
984 -- replaced by gotos which jump to the end of the routine and restore the
985 -- SPARK mode.
987 procedure Analyze_Object_Contract
988 (Obj_Id : Entity_Id;
989 Freeze_Id : Entity_Id := Empty)
991 Obj_Typ : constant Entity_Id := Etype (Obj_Id);
993 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
994 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
995 -- Save the SPARK_Mode-related data to restore on exit
997 Items : Node_Id;
998 Prag : Node_Id;
999 Ref_Elmt : Elmt_Id;
1001 begin
1002 -- The loop parameter in an element iterator over a formal container
1003 -- is declared with an object declaration, but no contracts apply.
1005 if Ekind (Obj_Id) = E_Loop_Parameter then
1006 return;
1007 end if;
1009 -- Do not analyze a contract multiple times
1011 Items := Contract (Obj_Id);
1013 if Present (Items) then
1014 if Analyzed (Items) then
1015 return;
1016 else
1017 Set_Analyzed (Items);
1018 end if;
1019 end if;
1021 -- The anonymous object created for a single concurrent type inherits
1022 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
1023 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
1024 -- of the enclosing context. To remedy this, restore the original mode
1025 -- of the related anonymous object.
1027 if Is_Single_Concurrent_Object (Obj_Id)
1028 and then Present (SPARK_Pragma (Obj_Id))
1029 then
1030 Set_SPARK_Mode (Obj_Id);
1031 end if;
1033 -- Checks related to external properties, same for constants and
1034 -- variables.
1036 Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id);
1038 -- Constant-related checks
1040 if Ekind (Obj_Id) = E_Constant then
1042 -- Analyze indicator Part_Of
1044 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
1046 -- Check whether the lack of indicator Part_Of agrees with the
1047 -- placement of the constant with respect to the state space.
1049 if No (Prag) then
1050 Check_Missing_Part_Of (Obj_Id);
1051 end if;
1053 -- Variable-related checks
1055 else pragma Assert (Ekind (Obj_Id) = E_Variable);
1057 -- The anonymous object created for a single task type carries
1058 -- pragmas Depends and Global of the type.
1060 if Is_Single_Task_Object (Obj_Id) then
1062 -- Analyze Global first, as Depends may mention items classified
1063 -- in the global categorization.
1065 Prag := Get_Pragma (Obj_Id, Pragma_Global);
1067 if Present (Prag) then
1068 Analyze_Global_In_Decl_Part (Prag);
1069 end if;
1071 -- Depends must be analyzed after Global in order to see the modes
1072 -- of all global items.
1074 Prag := Get_Pragma (Obj_Id, Pragma_Depends);
1076 if Present (Prag) then
1077 Analyze_Depends_In_Decl_Part (Prag);
1078 end if;
1079 end if;
1081 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
1083 -- Analyze indicator Part_Of
1085 if Present (Prag) then
1086 Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id);
1088 -- The variable is a constituent of a single protected/task type
1089 -- and behaves as a component of the type. Verify that references
1090 -- to the variable occur within the definition or body of the type
1091 -- (SPARK RM 9.3).
1093 if Present (Encapsulating_State (Obj_Id))
1094 and then Is_Single_Concurrent_Object
1095 (Encapsulating_State (Obj_Id))
1096 and then Present (Part_Of_References (Obj_Id))
1097 then
1098 Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id));
1099 while Present (Ref_Elmt) loop
1100 Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt));
1101 Next_Elmt (Ref_Elmt);
1102 end loop;
1103 end if;
1105 -- Otherwise check whether the lack of indicator Part_Of agrees with
1106 -- the placement of the variable with respect to the state space.
1108 else
1109 Check_Missing_Part_Of (Obj_Id);
1110 end if;
1111 end if;
1113 -- Common checks
1115 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
1117 -- A Ghost object cannot be of a type that yields a synchronized
1118 -- object (SPARK RM 6.9(19)).
1120 if Yields_Synchronized_Object (Obj_Typ) then
1121 Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
1123 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
1124 -- One exception to this is the object that represents the dispatch
1125 -- table of a Ghost tagged type, as the symbol needs to be exported.
1127 elsif Is_Exported (Obj_Id) then
1128 Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
1130 elsif Is_Imported (Obj_Id) then
1131 Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
1132 end if;
1133 end if;
1135 -- Restore the SPARK_Mode of the enclosing context after all delayed
1136 -- pragmas have been analyzed.
1138 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1139 end Analyze_Object_Contract;
1141 -----------------------------------
1142 -- Analyze_Package_Body_Contract --
1143 -----------------------------------
1145 -- WARNING: This routine manages SPARK regions. Return statements must be
1146 -- replaced by gotos which jump to the end of the routine and restore the
1147 -- SPARK mode.
1149 procedure Analyze_Package_Body_Contract
1150 (Body_Id : Entity_Id;
1151 Freeze_Id : Entity_Id := Empty)
1153 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
1154 Items : constant Node_Id := Contract (Body_Id);
1155 Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
1157 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1158 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1159 -- Save the SPARK_Mode-related data to restore on exit
1161 Ref_State : Node_Id;
1163 begin
1164 -- Do not analyze a contract multiple times
1166 if Present (Items) then
1167 if Analyzed (Items) then
1168 return;
1169 else
1170 Set_Analyzed (Items);
1171 end if;
1172 end if;
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 package body.
1179 Set_SPARK_Mode (Body_Id);
1181 Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
1183 -- The analysis of pragma Refined_State detects whether the spec has
1184 -- abstract states available for refinement.
1186 if Present (Ref_State) then
1187 Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id);
1188 end if;
1190 -- Restore the SPARK_Mode of the enclosing context after all delayed
1191 -- pragmas have been analyzed.
1193 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1195 -- Capture all global references in a generic package body now that the
1196 -- contract has been analyzed.
1198 if Is_Generic_Declaration_Or_Body (Body_Decl) then
1199 Save_Global_References_In_Contract
1200 (Templ => Original_Node (Body_Decl),
1201 Gen_Id => Spec_Id);
1202 end if;
1203 end Analyze_Package_Body_Contract;
1205 ------------------------------
1206 -- Analyze_Package_Contract --
1207 ------------------------------
1209 -- WARNING: This routine manages SPARK regions. Return statements must be
1210 -- replaced by gotos which jump to the end of the routine and restore the
1211 -- SPARK mode.
1213 procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
1214 Items : constant Node_Id := Contract (Pack_Id);
1215 Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
1217 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1218 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1219 -- Save the SPARK_Mode-related data to restore on exit
1221 Init : Node_Id := Empty;
1222 Init_Cond : Node_Id := Empty;
1223 Prag : Node_Id;
1224 Prag_Nam : Name_Id;
1226 begin
1227 -- Do not analyze a contract multiple times
1229 if Present (Items) then
1230 if Analyzed (Items) then
1231 return;
1233 -- Do not analyze the contract of the internal package
1234 -- created to check conformance of an actual package.
1235 -- Such an internal package is removed from the tree after
1236 -- legality checks are completed, and it does not contain
1237 -- the declarations of all local entities of the generic.
1239 elsif Is_Internal (Pack_Id)
1240 and then Is_Generic_Instance (Pack_Id)
1241 then
1242 return;
1244 else
1245 Set_Analyzed (Items);
1246 end if;
1247 end if;
1249 -- Due to the timing of contract analysis, delayed pragmas may be
1250 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1251 -- context. To remedy this, restore the original SPARK_Mode of the
1252 -- related package.
1254 Set_SPARK_Mode (Pack_Id);
1256 if Present (Items) then
1258 -- Locate and store pragmas Initial_Condition and Initializes, since
1259 -- their order of analysis matters.
1261 Prag := Classifications (Items);
1262 while Present (Prag) loop
1263 Prag_Nam := Pragma_Name (Prag);
1265 if Prag_Nam = Name_Initial_Condition then
1266 Init_Cond := Prag;
1268 elsif Prag_Nam = Name_Initializes then
1269 Init := Prag;
1270 end if;
1272 Prag := Next_Pragma (Prag);
1273 end loop;
1275 -- Analyze the initialization-related pragmas. Initializes must come
1276 -- before Initial_Condition due to item dependencies.
1278 if Present (Init) then
1279 Analyze_Initializes_In_Decl_Part (Init);
1280 end if;
1282 if Present (Init_Cond) then
1283 Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
1284 end if;
1285 end if;
1287 -- Restore the SPARK_Mode of the enclosing context after all delayed
1288 -- pragmas have been analyzed.
1290 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1292 -- Capture all global references in a generic package now that the
1293 -- contract has been analyzed.
1295 if Is_Generic_Declaration_Or_Body (Pack_Decl) then
1296 Save_Global_References_In_Contract
1297 (Templ => Original_Node (Pack_Decl),
1298 Gen_Id => Pack_Id);
1299 end if;
1300 end Analyze_Package_Contract;
1302 --------------------------------------------
1303 -- Analyze_Package_Instantiation_Contract --
1304 --------------------------------------------
1306 -- WARNING: This routine manages SPARK regions. Return statements must be
1307 -- replaced by gotos which jump to the end of the routine and restore the
1308 -- SPARK mode.
1310 procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is
1311 Inst_Spec : constant Node_Id :=
1312 Instance_Spec (Unit_Declaration_Node (Inst_Id));
1314 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1315 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1316 -- Save the SPARK_Mode-related data to restore on exit
1318 Pack_Id : Entity_Id;
1319 Prag : Node_Id;
1321 begin
1322 -- Nothing to do when the package instantiation is erroneous or left
1323 -- partially decorated.
1325 if No (Inst_Spec) then
1326 return;
1327 end if;
1329 Pack_Id := Defining_Entity (Inst_Spec);
1330 Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
1332 -- Due to the timing of contract analysis, delayed pragmas may be
1333 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1334 -- context. To remedy this, restore the original SPARK_Mode of the
1335 -- related package.
1337 Set_SPARK_Mode (Pack_Id);
1339 -- Check whether the lack of indicator Part_Of agrees with the placement
1340 -- of the package instantiation with respect to the state space. Nested
1341 -- package instantiations do not need to be checked because they inherit
1342 -- Part_Of indicator of the outermost package instantiation (see routine
1343 -- Propagate_Part_Of in Sem_Prag).
1345 if In_Instance then
1346 null;
1348 elsif No (Prag) then
1349 Check_Missing_Part_Of (Pack_Id);
1350 end if;
1352 -- Restore the SPARK_Mode of the enclosing context after all delayed
1353 -- pragmas have been analyzed.
1355 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1356 end Analyze_Package_Instantiation_Contract;
1358 --------------------------------
1359 -- Analyze_Protected_Contract --
1360 --------------------------------
1362 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
1363 Items : constant Node_Id := Contract (Prot_Id);
1365 begin
1366 -- Do not analyze a contract multiple times
1368 if Present (Items) then
1369 if Analyzed (Items) then
1370 return;
1371 else
1372 Set_Analyzed (Items);
1373 end if;
1374 end if;
1375 end Analyze_Protected_Contract;
1377 -------------------------------------------
1378 -- Analyze_Subprogram_Body_Stub_Contract --
1379 -------------------------------------------
1381 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
1382 Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
1383 Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
1385 begin
1386 -- A subprogram body stub may act as its own spec or as the completion
1387 -- of a previous declaration. Depending on the context, the contract of
1388 -- the stub may contain two sets of pragmas.
1390 -- The stub is a completion, the applicable pragmas are:
1391 -- Refined_Depends
1392 -- Refined_Global
1394 if Present (Spec_Id) then
1395 Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
1397 -- The stub acts as its own spec, the applicable pragmas are:
1398 -- Always_Terminates
1399 -- Contract_Cases
1400 -- Depends
1401 -- Exceptional_Cases
1402 -- Global
1403 -- Postcondition
1404 -- Precondition
1405 -- Subprogram_Variant
1406 -- Test_Case
1408 else
1409 Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
1410 end if;
1411 end Analyze_Subprogram_Body_Stub_Contract;
1413 ---------------------------
1414 -- Analyze_Task_Contract --
1415 ---------------------------
1417 -- WARNING: This routine manages SPARK regions. Return statements must be
1418 -- replaced by gotos which jump to the end of the routine and restore the
1419 -- SPARK mode.
1421 procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
1422 Items : constant Node_Id := Contract (Task_Id);
1424 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1425 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1426 -- Save the SPARK_Mode-related data to restore on exit
1428 Prag : Node_Id;
1430 begin
1431 -- Do not analyze a contract multiple times
1433 if Present (Items) then
1434 if Analyzed (Items) then
1435 return;
1436 else
1437 Set_Analyzed (Items);
1438 end if;
1439 end if;
1441 -- Due to the timing of contract analysis, delayed pragmas may be
1442 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1443 -- context. To remedy this, restore the original SPARK_Mode of the
1444 -- related task unit.
1446 Set_SPARK_Mode (Task_Id);
1448 -- Analyze Global first, as Depends may mention items classified in the
1449 -- global categorization.
1451 Prag := Get_Pragma (Task_Id, Pragma_Global);
1453 if Present (Prag) then
1454 Analyze_Global_In_Decl_Part (Prag);
1455 end if;
1457 -- Depends must be analyzed after Global in order to see the modes of
1458 -- all global items.
1460 Prag := Get_Pragma (Task_Id, Pragma_Depends);
1462 if Present (Prag) then
1463 Analyze_Depends_In_Decl_Part (Prag);
1464 end if;
1466 -- Restore the SPARK_Mode of the enclosing context after all delayed
1467 -- pragmas have been analyzed.
1469 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1470 end Analyze_Task_Contract;
1472 ---------------------------
1473 -- Analyze_Type_Contract --
1474 ---------------------------
1476 procedure Analyze_Type_Contract (Type_Id : Entity_Id) is
1477 begin
1478 Check_Type_Or_Object_External_Properties
1479 (Type_Or_Obj_Id => Type_Id);
1481 -- Analyze Pre/Post on access-to-subprogram type
1483 if Ekind (Type_Id) in Access_Subprogram_Kind then
1484 Analyze_Entry_Or_Subprogram_Contract
1485 (Directly_Designated_Type (Type_Id));
1486 end if;
1487 end Analyze_Type_Contract;
1489 ---------------------------------------
1490 -- Build_Subprogram_Contract_Wrapper --
1491 ---------------------------------------
1493 procedure Build_Subprogram_Contract_Wrapper
1494 (Body_Id : Entity_Id;
1495 Stmts : List_Id;
1496 Decls : List_Id;
1497 Result : Entity_Id)
1499 Body_Decl : constant Entity_Id := Unit_Declaration_Node (Body_Id);
1500 Loc : constant Source_Ptr := Sloc (Body_Decl);
1501 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
1502 Subp_Id : Entity_Id;
1503 Ret_Type : Entity_Id;
1505 Wrapper_Id : Entity_Id;
1506 Wrapper_Body : Node_Id;
1507 Wrapper_Spec : Node_Id;
1509 begin
1510 -- When there are no postcondition statements we do not need to
1511 -- generate a wrapper.
1513 if No (Stmts) then
1514 return;
1515 end if;
1517 -- Obtain the related subprogram id from the body id.
1519 if Present (Spec_Id) then
1520 Subp_Id := Spec_Id;
1521 else
1522 Subp_Id := Body_Id;
1523 end if;
1524 Ret_Type := Etype (Subp_Id);
1526 -- Generate the contracts wrapper by moving the original declarations
1527 -- and statements within a local subprogram, calling it and possibly
1528 -- preserving the result for the purpose of evaluating postconditions,
1529 -- contracts, type invariants, etc.
1531 -- In the case of a function, generate:
1533 -- function Original_Func (X : in out Integer) return Typ is
1534 -- <prologue renamings>
1535 -- <preconditions>
1537 -- function _Wrapped_Statements return Typ is
1538 -- <original declarations>
1539 -- begin
1540 -- <original statements>
1541 -- end;
1543 -- begin
1544 -- return
1545 -- Result_Obj : constant Typ := _Wrapped_Statements
1546 -- do
1547 -- <postconditions statements>
1548 -- end return;
1549 -- end;
1551 -- Or else, in the case of a procedure, generate:
1553 -- procedure Original_Proc (X : in out Integer) is
1554 -- <prologue renamings>
1555 -- <preconditions>
1557 -- procedure _Wrapped_Statements is
1558 -- <original declarations>
1559 -- begin
1560 -- <original statements>
1561 -- end;
1563 -- begin
1564 -- _Wrapped_Statements;
1565 -- <postconditions statements>
1566 -- end;
1568 -- Create Identifier
1570 Wrapper_Id := Make_Defining_Identifier (Loc, Name_uWrapped_Statements);
1571 Set_Debug_Info_Needed (Wrapper_Id);
1572 Set_Wrapped_Statements (Subp_Id, Wrapper_Id);
1574 Set_Has_Pragma_Inline (Wrapper_Id, Has_Pragma_Inline (Subp_Id));
1575 Set_Has_Pragma_Inline_Always
1576 (Wrapper_Id, Has_Pragma_Inline_Always (Subp_Id));
1578 -- Create specification and declaration for the wrapper
1580 if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
1581 Wrapper_Spec :=
1582 Make_Procedure_Specification (Loc,
1583 Defining_Unit_Name => Wrapper_Id);
1584 else
1585 Wrapper_Spec :=
1586 Make_Function_Specification (Loc,
1587 Defining_Unit_Name => Wrapper_Id,
1588 Result_Definition => New_Occurrence_Of (Ret_Type, Loc));
1589 end if;
1591 -- Create the wrapper body using Body_Id's statements and declarations
1593 Wrapper_Body :=
1594 Make_Subprogram_Body (Loc,
1595 Specification => Wrapper_Spec,
1596 Declarations => Declarations (Body_Decl),
1597 Handled_Statement_Sequence =>
1598 Relocate_Node (Handled_Statement_Sequence (Body_Decl)));
1600 Append_To (Decls, Wrapper_Body);
1601 Set_Declarations (Body_Decl, Decls);
1602 Set_Handled_Statement_Sequence (Body_Decl,
1603 Make_Handled_Sequence_Of_Statements (Loc,
1604 End_Label => Make_Identifier (Loc, Chars (Wrapper_Id))));
1606 -- Prepend a call to the wrapper when the subprogram is a procedure
1608 if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
1609 Prepend_To (Stmts,
1610 Make_Procedure_Call_Statement (Loc,
1611 Name => New_Occurrence_Of (Wrapper_Id, Loc)));
1612 Set_Statements
1613 (Handled_Statement_Sequence (Body_Decl), Stmts);
1615 -- Generate the post-execution statements and the extended return
1616 -- when the subprogram being wrapped is a function.
1618 else
1619 Set_Statements (Handled_Statement_Sequence (Body_Decl), New_List (
1620 Make_Extended_Return_Statement (Loc,
1621 Return_Object_Declarations => New_List (
1622 Make_Object_Declaration (Loc,
1623 Defining_Identifier => Result,
1624 Constant_Present => True,
1625 Object_Definition =>
1626 New_Occurrence_Of (Ret_Type, Loc),
1627 Expression =>
1628 Make_Function_Call (Loc,
1629 Name =>
1630 New_Occurrence_Of (Wrapper_Id, Loc)))),
1631 Handled_Statement_Sequence =>
1632 Make_Handled_Sequence_Of_Statements (Loc,
1633 Statements => Stmts))));
1634 end if;
1635 end Build_Subprogram_Contract_Wrapper;
1637 ----------------------------------
1638 -- Build_Entry_Contract_Wrapper --
1639 ----------------------------------
1641 procedure Build_Entry_Contract_Wrapper (E : Entity_Id; Decl : Node_Id) is
1642 Conc_Typ : constant Entity_Id := Scope (E);
1643 Loc : constant Source_Ptr := Sloc (E);
1645 procedure Add_Discriminant_Renamings
1646 (Obj_Id : Entity_Id;
1647 Decls : List_Id);
1648 -- Add renaming declarations for all discriminants of concurrent type
1649 -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
1650 -- represents the concurrent object.
1652 procedure Add_Matching_Formals
1653 (Formals : List_Id;
1654 Actuals : in out List_Id);
1655 -- Add formal parameters that match those of entry E to list Formals.
1656 -- The routine also adds matching actuals for the new formals to list
1657 -- Actuals.
1659 procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id);
1660 -- Relocate pragma Prag to list To. The routine creates a new list if
1661 -- To does not exist.
1663 --------------------------------
1664 -- Add_Discriminant_Renamings --
1665 --------------------------------
1667 procedure Add_Discriminant_Renamings
1668 (Obj_Id : Entity_Id;
1669 Decls : List_Id)
1671 Discr : Entity_Id;
1672 Renaming_Decl : Node_Id;
1674 begin
1675 -- Inspect the discriminants of the concurrent type and generate a
1676 -- renaming for each one.
1678 if Has_Discriminants (Conc_Typ) then
1679 Discr := First_Discriminant (Conc_Typ);
1680 while Present (Discr) loop
1681 Renaming_Decl :=
1682 Make_Object_Renaming_Declaration (Loc,
1683 Defining_Identifier =>
1684 Make_Defining_Identifier (Loc, Chars (Discr)),
1685 Subtype_Mark =>
1686 New_Occurrence_Of (Etype (Discr), Loc),
1687 Name =>
1688 Make_Selected_Component (Loc,
1689 Prefix => New_Occurrence_Of (Obj_Id, Loc),
1690 Selector_Name =>
1691 Make_Identifier (Loc, Chars (Discr))));
1693 Prepend_To (Decls, Renaming_Decl);
1695 Next_Discriminant (Discr);
1696 end loop;
1697 end if;
1698 end Add_Discriminant_Renamings;
1700 --------------------------
1701 -- Add_Matching_Formals --
1702 --------------------------
1704 procedure Add_Matching_Formals
1705 (Formals : List_Id;
1706 Actuals : in out List_Id)
1708 Formal : Entity_Id;
1709 New_Formal : Entity_Id;
1711 begin
1712 -- Inspect the formal parameters of the entry and generate a new
1713 -- matching formal with the same name for the wrapper. A reference
1714 -- to the new formal becomes an actual in the entry call.
1716 Formal := First_Formal (E);
1717 while Present (Formal) loop
1718 New_Formal := Make_Defining_Identifier (Loc, Chars (Formal));
1719 Append_To (Formals,
1720 Make_Parameter_Specification (Loc,
1721 Defining_Identifier => New_Formal,
1722 In_Present => In_Present (Parent (Formal)),
1723 Out_Present => Out_Present (Parent (Formal)),
1724 Parameter_Type =>
1725 New_Occurrence_Of (Etype (Formal), Loc)));
1727 if No (Actuals) then
1728 Actuals := New_List;
1729 end if;
1731 Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
1732 Next_Formal (Formal);
1733 end loop;
1734 end Add_Matching_Formals;
1736 ---------------------
1737 -- Transfer_Pragma --
1738 ---------------------
1740 procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id) is
1741 New_Prag : Node_Id;
1743 begin
1744 if No (To) then
1745 To := New_List;
1746 end if;
1748 New_Prag := Relocate_Node (Prag);
1750 Set_Analyzed (New_Prag, False);
1751 Append (New_Prag, To);
1752 end Transfer_Pragma;
1754 -- Local variables
1756 Items : constant Node_Id := Contract (E);
1757 Actuals : List_Id := No_List;
1758 Call : Node_Id;
1759 Call_Nam : Node_Id;
1760 Decls : List_Id := No_List;
1761 Formals : List_Id;
1762 Has_Pragma : Boolean := False;
1763 Index_Id : Entity_Id;
1764 Obj_Id : Entity_Id;
1765 Prag : Node_Id;
1766 Wrapper_Id : Entity_Id;
1768 -- Start of processing for Build_Entry_Contract_Wrapper
1770 begin
1771 -- This routine generates a specialized wrapper for a protected or task
1772 -- entry [family] which implements precondition/postcondition semantics.
1773 -- Preconditions and case guards of contract cases are checked before
1774 -- the protected action or rendezvous takes place.
1776 -- procedure Wrapper
1777 -- (Obj_Id : Conc_Typ; -- concurrent object
1778 -- [Index : Index_Typ;] -- index of entry family
1779 -- [Formal_1 : ...; -- parameters of original entry
1780 -- Formal_N : ...])
1781 -- is
1782 -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
1783 -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
1785 -- <contracts pragmas>
1786 -- <case guard checks>
1788 -- begin
1789 -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
1790 -- end Wrapper;
1792 -- Create the wrapper only when the entry has at least one executable
1793 -- contract item such as contract cases, precondition or postcondition.
1795 if Present (Items) then
1797 -- Inspect the list of pre/postconditions and transfer all available
1798 -- pragmas to the declarative list of the wrapper.
1800 Prag := Pre_Post_Conditions (Items);
1801 while Present (Prag) loop
1802 if Pragma_Name_Unmapped (Prag) in Name_Postcondition
1803 | Name_Precondition
1804 and then Is_Checked (Prag)
1805 then
1806 Has_Pragma := True;
1807 Transfer_Pragma (Prag, To => Decls);
1808 end if;
1810 Prag := Next_Pragma (Prag);
1811 end loop;
1813 -- Inspect the list of test/contract cases and transfer only contract
1814 -- cases pragmas to the declarative part of the wrapper.
1816 Prag := Contract_Test_Cases (Items);
1817 while Present (Prag) loop
1818 if Pragma_Name (Prag) = Name_Contract_Cases
1819 and then Is_Checked (Prag)
1820 then
1821 Has_Pragma := True;
1822 Transfer_Pragma (Prag, To => Decls);
1823 end if;
1825 Prag := Next_Pragma (Prag);
1826 end loop;
1827 end if;
1829 -- The entry lacks executable contract items and a wrapper is not needed
1831 if not Has_Pragma then
1832 return;
1833 end if;
1835 -- Create the profile of the wrapper. The first formal parameter is the
1836 -- concurrent object.
1838 Obj_Id :=
1839 Make_Defining_Identifier (Loc,
1840 Chars => New_External_Name (Chars (Conc_Typ), 'A'));
1842 Formals := New_List (
1843 Make_Parameter_Specification (Loc,
1844 Defining_Identifier => Obj_Id,
1845 Out_Present => True,
1846 In_Present => True,
1847 Parameter_Type => New_Occurrence_Of (Conc_Typ, Loc)));
1849 -- Construct the call to the original entry. The call will be gradually
1850 -- augmented with an optional entry index and extra parameters.
1852 Call_Nam :=
1853 Make_Selected_Component (Loc,
1854 Prefix => New_Occurrence_Of (Obj_Id, Loc),
1855 Selector_Name => New_Occurrence_Of (E, Loc));
1857 -- When creating a wrapper for an entry family, the second formal is the
1858 -- entry index.
1860 if Ekind (E) = E_Entry_Family then
1861 Index_Id := Make_Defining_Identifier (Loc, Name_I);
1863 Append_To (Formals,
1864 Make_Parameter_Specification (Loc,
1865 Defining_Identifier => Index_Id,
1866 Parameter_Type =>
1867 New_Occurrence_Of (Entry_Index_Type (E), Loc)));
1869 -- The call to the original entry becomes an indexed component to
1870 -- accommodate the entry index.
1872 Call_Nam :=
1873 Make_Indexed_Component (Loc,
1874 Prefix => Call_Nam,
1875 Expressions => New_List (New_Occurrence_Of (Index_Id, Loc)));
1876 end if;
1878 -- Add formal parameters to match those of the entry and build actuals
1879 -- for the entry call.
1881 Add_Matching_Formals (Formals, Actuals);
1883 Call :=
1884 Make_Procedure_Call_Statement (Loc,
1885 Name => Call_Nam,
1886 Parameter_Associations => Actuals);
1888 -- Add renaming declarations for the discriminants of the enclosing type
1889 -- as the various contract items may reference them.
1891 Add_Discriminant_Renamings (Obj_Id, Decls);
1893 Wrapper_Id :=
1894 Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
1895 Set_Contract_Wrapper (E, Wrapper_Id);
1896 Set_Is_Entry_Wrapper (Wrapper_Id);
1898 -- The wrapper body is analyzed when the enclosing type is frozen
1900 Append_Freeze_Action (Defining_Entity (Decl),
1901 Make_Subprogram_Body (Loc,
1902 Specification =>
1903 Make_Procedure_Specification (Loc,
1904 Defining_Unit_Name => Wrapper_Id,
1905 Parameter_Specifications => Formals),
1906 Declarations => Decls,
1907 Handled_Statement_Sequence =>
1908 Make_Handled_Sequence_Of_Statements (Loc,
1909 Statements => New_List (Call))));
1910 end Build_Entry_Contract_Wrapper;
1912 ---------------------------
1913 -- Check_Class_Condition --
1914 ---------------------------
1916 procedure Check_Class_Condition
1917 (Cond : Node_Id;
1918 Subp : Entity_Id;
1919 Par_Subp : Entity_Id;
1920 Is_Precondition : Boolean)
1922 function Check_Entity (N : Node_Id) return Traverse_Result;
1923 -- Check reference to formal of inherited operation or to primitive
1924 -- operation of root type.
1926 ------------------
1927 -- Check_Entity --
1928 ------------------
1930 function Check_Entity (N : Node_Id) return Traverse_Result is
1931 New_E : Entity_Id;
1932 Orig_E : Entity_Id;
1934 begin
1935 if Nkind (N) = N_Identifier
1936 and then Present (Entity (N))
1937 and then
1938 (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
1939 and then
1940 (Nkind (Parent (N)) /= N_Attribute_Reference
1941 or else Attribute_Name (Parent (N)) /= Name_Class)
1942 then
1943 -- These checks do not apply to dispatching calls within the
1944 -- condition, but only to calls whose static tag is that of
1945 -- the parent type.
1947 if Is_Subprogram (Entity (N))
1948 and then Nkind (Parent (N)) = N_Function_Call
1949 and then Present (Controlling_Argument (Parent (N)))
1950 then
1951 return OK;
1952 end if;
1954 -- Determine whether entity has a renaming
1956 Orig_E := Entity (N);
1957 New_E := Get_Mapped_Entity (Orig_E);
1959 if Present (New_E) then
1961 -- AI12-0166: A precondition for a protected operation
1962 -- cannot include an internal call to a protected function
1963 -- of the type. In the case of an inherited condition for an
1964 -- overriding operation, both the operation and the function
1965 -- are given by primitive wrappers.
1967 if Is_Precondition
1968 and then Ekind (New_E) = E_Function
1969 and then Is_Primitive_Wrapper (New_E)
1970 and then Is_Primitive_Wrapper (Subp)
1971 and then Scope (Subp) = Scope (New_E)
1972 then
1973 Error_Msg_Node_2 := Wrapped_Entity (Subp);
1974 Error_Msg_NE
1975 ("internal call to& cannot appear in inherited "
1976 & "precondition of protected operation&",
1977 Subp, Wrapped_Entity (New_E));
1978 end if;
1979 end if;
1981 -- Check that there are no calls left to abstract operations if
1982 -- the current subprogram is not abstract.
1984 if Present (New_E)
1985 and then Nkind (Parent (N)) = N_Function_Call
1986 and then N = Name (Parent (N))
1987 then
1988 if not Is_Abstract_Subprogram (Subp)
1989 and then Is_Abstract_Subprogram (New_E)
1990 then
1991 Error_Msg_Sloc := Sloc (Current_Scope);
1992 Error_Msg_Node_2 := Subp;
1994 if Comes_From_Source (Subp) then
1995 Error_Msg_NE
1996 ("cannot call abstract subprogram & in inherited "
1997 & "condition for&#", Subp, New_E);
1998 else
1999 Error_Msg_NE
2000 ("cannot call abstract subprogram & in inherited "
2001 & "condition for inherited&#", Subp, New_E);
2002 end if;
2004 -- In SPARK mode, report error on inherited condition for an
2005 -- inherited operation if it contains a call to an overriding
2006 -- operation, because this implies that the pre/postconditions
2007 -- of the inherited operation have changed silently.
2009 elsif SPARK_Mode = On
2010 and then Warn_On_Suspicious_Contract
2011 and then Present (Alias (Subp))
2012 and then Present (New_E)
2013 and then Comes_From_Source (New_E)
2014 then
2015 Error_Msg_N
2016 ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
2017 Parent (Subp));
2018 Error_Msg_Sloc := Sloc (New_E);
2019 Error_Msg_Node_2 := Subp;
2020 Error_Msg_NE
2021 ("\overriding of&# forces overriding of&",
2022 Parent (Subp), New_E);
2023 end if;
2024 end if;
2025 end if;
2027 return OK;
2028 end Check_Entity;
2030 procedure Check_Condition_Entities is
2031 new Traverse_Proc (Check_Entity);
2033 -- Start of processing for Check_Class_Condition
2035 begin
2036 -- No check required if the subprograms match
2038 if Par_Subp = Subp then
2039 return;
2040 end if;
2042 Update_Primitives_Mapping (Par_Subp, Subp);
2043 Map_Formals (Par_Subp, Subp);
2044 Check_Condition_Entities (Cond);
2045 end Check_Class_Condition;
2047 -----------------------------
2048 -- Create_Generic_Contract --
2049 -----------------------------
2051 procedure Create_Generic_Contract (Unit : Node_Id) is
2052 Templ : constant Node_Id := Original_Node (Unit);
2053 Templ_Id : constant Entity_Id := Defining_Entity (Templ);
2055 procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
2056 -- Add a single contract-related source pragma Prag to the contract of
2057 -- generic template Templ_Id.
2059 ---------------------------------
2060 -- Add_Generic_Contract_Pragma --
2061 ---------------------------------
2063 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
2064 Prag_Templ : Node_Id;
2066 begin
2067 -- Mark the pragma to prevent the premature capture of global
2068 -- references when capturing global references of the context
2069 -- (see Save_References_In_Pragma).
2071 Set_Is_Generic_Contract_Pragma (Prag);
2073 -- Pragmas that apply to a generic subprogram declaration are not
2074 -- part of the semantic structure of the generic template:
2076 -- generic
2077 -- procedure Example (Formal : Integer);
2078 -- pragma Precondition (Formal > 0);
2080 -- Create a generic template for such pragmas and link the template
2081 -- of the pragma with the generic template.
2083 if Nkind (Templ) = N_Generic_Subprogram_Declaration then
2084 Rewrite
2085 (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
2086 Prag_Templ := Original_Node (Prag);
2088 Set_Is_Generic_Contract_Pragma (Prag_Templ);
2089 Add_Contract_Item (Prag_Templ, Templ_Id);
2091 -- Otherwise link the pragma with the generic template
2093 else
2094 Add_Contract_Item (Prag, Templ_Id);
2095 end if;
2097 exception
2098 -- We do not stop the compilation at this point in the case of an
2099 -- invalid pragma because it will be properly diagnosed afterward.
2101 when Contract_Error => null;
2102 end Add_Generic_Contract_Pragma;
2104 -- Local variables
2106 Context : constant Node_Id := Parent (Unit);
2107 Decl : Node_Id := Empty;
2109 -- Start of processing for Create_Generic_Contract
2111 begin
2112 -- A generic package declaration carries contract-related source pragmas
2113 -- in its visible declarations.
2115 if Nkind (Templ) = N_Generic_Package_Declaration then
2116 Mutate_Ekind (Templ_Id, E_Generic_Package);
2118 if Present (Visible_Declarations (Specification (Templ))) then
2119 Decl := First (Visible_Declarations (Specification (Templ)));
2120 end if;
2122 -- A generic package body carries contract-related source pragmas in its
2123 -- declarations.
2125 elsif Nkind (Templ) = N_Package_Body then
2126 Mutate_Ekind (Templ_Id, E_Package_Body);
2128 if Present (Declarations (Templ)) then
2129 Decl := First (Declarations (Templ));
2130 end if;
2132 -- Generic subprogram declaration
2134 elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
2135 if Nkind (Specification (Templ)) = N_Function_Specification then
2136 Mutate_Ekind (Templ_Id, E_Generic_Function);
2137 else
2138 Mutate_Ekind (Templ_Id, E_Generic_Procedure);
2139 end if;
2141 -- When the generic subprogram acts as a compilation unit, inspect
2142 -- the Pragmas_After list for contract-related source pragmas.
2144 if Nkind (Context) = N_Compilation_Unit then
2145 if Present (Aux_Decls_Node (Context))
2146 and then Present (Pragmas_After (Aux_Decls_Node (Context)))
2147 then
2148 Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
2149 end if;
2151 -- Otherwise inspect the successive declarations for contract-related
2152 -- source pragmas.
2154 else
2155 Decl := Next (Unit);
2156 end if;
2158 -- A generic subprogram body carries contract-related source pragmas in
2159 -- its declarations.
2161 elsif Nkind (Templ) = N_Subprogram_Body then
2162 Mutate_Ekind (Templ_Id, E_Subprogram_Body);
2164 if Present (Declarations (Templ)) then
2165 Decl := First (Declarations (Templ));
2166 end if;
2167 end if;
2169 -- Inspect the relevant declarations looking for contract-related source
2170 -- pragmas and add them to the contract of the generic unit.
2172 while Present (Decl) loop
2173 if Comes_From_Source (Decl) then
2174 if Nkind (Decl) = N_Pragma then
2176 -- The source pragma is a contract annotation
2178 if Is_Contract_Annotation (Decl) then
2179 Add_Generic_Contract_Pragma (Decl);
2180 end if;
2182 -- The region where a contract-related source pragma may appear
2183 -- ends with the first source non-pragma declaration or statement.
2185 else
2186 exit;
2187 end if;
2188 end if;
2190 Next (Decl);
2191 end loop;
2192 end Create_Generic_Contract;
2194 --------------------------------
2195 -- Expand_Subprogram_Contract --
2196 --------------------------------
2198 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is
2199 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
2200 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
2202 procedure Add_Invariant_And_Predicate_Checks
2203 (Subp_Id : Entity_Id;
2204 Stmts : in out List_Id;
2205 Result : out Node_Id);
2206 -- Process the result of function Subp_Id (if applicable) and all its
2207 -- formals. Add invariant and predicate checks where applicable. The
2208 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
2209 -- function, Result contains the entity of parameter _Result, to be
2210 -- used in the creation of procedure _Postconditions.
2212 procedure Add_Stable_Property_Contracts
2213 (Subp_Id : Entity_Id; Class_Present : Boolean);
2214 -- Augment postcondition contracts to reflect Stable_Property aspect
2215 -- (if Class_Present = False) or Stable_Property'Class aspect (if
2216 -- Class_Present = True).
2218 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
2219 -- Append a node to a list. If there is no list, create a new one. When
2220 -- the item denotes a pragma, it is added to the list only when it is
2221 -- enabled.
2223 procedure Process_Contract_Cases
2224 (Stmts : in out List_Id;
2225 Decls : List_Id);
2226 -- Process pragma Contract_Cases. This routine prepends items to the
2227 -- body declarations and appends items to list Stmts.
2229 procedure Process_Postconditions (Stmts : in out List_Id);
2230 -- Collect all [inherited] spec and body postconditions and accumulate
2231 -- their pragma Check equivalents in list Stmts.
2233 procedure Process_Preconditions (Decls : in out List_Id);
2234 -- Collect all [inherited] spec and body preconditions and prepend their
2235 -- pragma Check equivalents to the declarations of the body.
2237 ----------------------------------------
2238 -- Add_Invariant_And_Predicate_Checks --
2239 ----------------------------------------
2241 procedure Add_Invariant_And_Predicate_Checks
2242 (Subp_Id : Entity_Id;
2243 Stmts : in out List_Id;
2244 Result : out Node_Id)
2246 procedure Add_Invariant_Access_Checks (Id : Entity_Id);
2247 -- Id denotes the return value of a function or a formal parameter.
2248 -- Add an invariant check if the type of Id is access to a type with
2249 -- invariants. The routine appends the generated code to Stmts.
2251 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
2252 -- Determine whether type Typ can benefit from invariant checks. To
2253 -- qualify, the type must have a non-null invariant procedure and
2254 -- subprogram Subp_Id must appear visible from the point of view of
2255 -- the type.
2257 ---------------------------------
2258 -- Add_Invariant_Access_Checks --
2259 ---------------------------------
2261 procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
2262 Loc : constant Source_Ptr := Sloc (Body_Decl);
2263 Ref : Node_Id;
2264 Typ : Entity_Id;
2266 begin
2267 Typ := Etype (Id);
2269 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
2270 Typ := Designated_Type (Typ);
2272 if Invariant_Checks_OK (Typ) then
2273 Ref :=
2274 Make_Explicit_Dereference (Loc,
2275 Prefix => New_Occurrence_Of (Id, Loc));
2276 Set_Etype (Ref, Typ);
2278 -- Generate:
2279 -- if <Id> /= null then
2280 -- <invariant_call (<Ref>)>
2281 -- end if;
2283 Append_Enabled_Item
2284 (Item =>
2285 Make_If_Statement (Loc,
2286 Condition =>
2287 Make_Op_Ne (Loc,
2288 Left_Opnd => New_Occurrence_Of (Id, Loc),
2289 Right_Opnd => Make_Null (Loc)),
2290 Then_Statements => New_List (
2291 Make_Invariant_Call (Ref))),
2292 List => Stmts);
2293 end if;
2294 end if;
2295 end Add_Invariant_Access_Checks;
2297 -------------------------
2298 -- Invariant_Checks_OK --
2299 -------------------------
2301 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
2302 function Has_Public_Visibility_Of_Subprogram return Boolean;
2303 -- Determine whether type Typ has public visibility of subprogram
2304 -- Subp_Id.
2306 -----------------------------------------
2307 -- Has_Public_Visibility_Of_Subprogram --
2308 -----------------------------------------
2310 function Has_Public_Visibility_Of_Subprogram return Boolean is
2311 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
2313 begin
2314 -- An Initialization procedure must be considered visible even
2315 -- though it is internally generated.
2317 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
2318 return True;
2320 elsif Ekind (Scope (Typ)) /= E_Package then
2321 return False;
2323 -- Internally generated code is never publicly visible except
2324 -- for a subprogram that is the implementation of an expression
2325 -- function. In that case the visibility is determined by the
2326 -- last check.
2328 elsif not Comes_From_Source (Subp_Decl)
2329 and then
2330 (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
2331 or else not
2332 Comes_From_Source (Defining_Entity (Subp_Decl)))
2333 then
2334 return False;
2336 -- Determine whether the subprogram is declared in the visible
2337 -- declarations of the package containing the type, or in the
2338 -- visible declaration of a child unit of that package.
2340 elsif Is_List_Member (Subp_Decl) then
2341 declare
2342 Decls : constant List_Id :=
2343 List_Containing (Subp_Decl);
2344 Subp_Scope : constant Entity_Id :=
2345 Scope (Defining_Entity (Subp_Decl));
2346 Typ_Scope : constant Entity_Id := Scope (Typ);
2348 begin
2349 return
2350 Decls = Visible_Declarations
2351 (Specification (Unit_Declaration_Node (Typ_Scope)))
2353 or else
2354 (Ekind (Subp_Scope) = E_Package
2355 and then Typ_Scope /= Subp_Scope
2356 and then Is_Child_Unit (Subp_Scope)
2357 and then
2358 Is_Ancestor_Package (Typ_Scope, Subp_Scope)
2359 and then
2360 Decls = Visible_Declarations
2361 (Specification
2362 (Unit_Declaration_Node (Subp_Scope))));
2363 end;
2365 -- Determine whether the subprogram is a child subprogram of
2366 -- of the package containing the type.
2368 else
2369 pragma Assert
2370 (Nkind (Parent (Subp_Decl)) = N_Compilation_Unit);
2372 declare
2373 Subp_Scope : constant Entity_Id :=
2374 Scope (Defining_Entity (Subp_Decl));
2375 Typ_Scope : constant Entity_Id := Scope (Typ);
2377 begin
2378 return
2379 Ekind (Subp_Scope) = E_Package
2380 and then
2381 (Typ_Scope = Subp_Scope
2382 or else
2383 (Is_Child_Unit (Subp_Scope)
2384 and then Is_Ancestor_Package
2385 (Typ_Scope, Subp_Scope)));
2386 end;
2387 end if;
2388 end Has_Public_Visibility_Of_Subprogram;
2390 -- Start of processing for Invariant_Checks_OK
2392 begin
2393 return
2394 Has_Invariants (Typ)
2395 and then Present (Invariant_Procedure (Typ))
2396 and then not Has_Null_Body (Invariant_Procedure (Typ))
2397 and then Has_Public_Visibility_Of_Subprogram;
2398 end Invariant_Checks_OK;
2400 -- Local variables
2402 Loc : constant Source_Ptr := Sloc (Body_Decl);
2403 -- Source location of subprogram body contract
2405 Formal : Entity_Id;
2406 Typ : Entity_Id;
2408 -- Start of processing for Add_Invariant_And_Predicate_Checks
2410 begin
2411 Result := Empty;
2413 -- Process the result of a function
2415 if Ekind (Subp_Id) = E_Function then
2416 Typ := Etype (Subp_Id);
2418 -- Generate _Result which is used in procedure _Postconditions to
2419 -- verify the return value.
2421 Result := Make_Defining_Identifier (Loc, Name_uResult);
2422 Set_Etype (Result, Typ);
2424 -- Add an invariant check when the return type has invariants and
2425 -- the related function is visible to the outside.
2427 if Invariant_Checks_OK (Typ) then
2428 Append_Enabled_Item
2429 (Item =>
2430 Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
2431 List => Stmts);
2432 end if;
2434 -- Add an invariant check when the return type is an access to a
2435 -- type with invariants.
2437 Add_Invariant_Access_Checks (Result);
2438 end if;
2440 -- Add invariant checks for all formals that qualify (see AI05-0289
2441 -- and AI12-0044).
2443 Formal := First_Formal (Subp_Id);
2444 while Present (Formal) loop
2445 Typ := Etype (Formal);
2447 if Ekind (Formal) /= E_In_Parameter
2448 or else Ekind (Subp_Id) = E_Procedure
2449 or else Is_Access_Type (Typ)
2450 then
2451 if Invariant_Checks_OK (Typ) then
2452 Append_Enabled_Item
2453 (Item =>
2454 Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
2455 List => Stmts);
2456 end if;
2458 Add_Invariant_Access_Checks (Formal);
2460 -- Note: we used to add predicate checks for OUT and IN OUT
2461 -- formals here, but that was misguided, since such checks are
2462 -- performed on the caller side, based on the predicate of the
2463 -- actual, rather than the predicate of the formal.
2465 end if;
2467 Next_Formal (Formal);
2468 end loop;
2469 end Add_Invariant_And_Predicate_Checks;
2471 -----------------------------------
2472 -- Add_Stable_Property_Contracts --
2473 -----------------------------------
2475 procedure Add_Stable_Property_Contracts
2476 (Subp_Id : Entity_Id; Class_Present : Boolean)
2478 Loc : constant Source_Ptr := Sloc (Subp_Id);
2480 procedure Insert_Stable_Property_Check
2481 (Formal : Entity_Id; Property_Function : Entity_Id);
2482 -- Build the pragma for one check and insert it in the tree.
2484 function Make_Stable_Property_Condition
2485 (Formal : Entity_Id; Property_Function : Entity_Id) return Node_Id;
2486 -- Builds tree for "Func (Formal) = Func (Formal)'Old" expression.
2488 function Stable_Properties
2489 (Aspect_Bearer : Entity_Id; Negated : out Boolean)
2490 return Subprogram_List;
2491 -- If no aspect specified, then returns length-zero result.
2492 -- Negated indicates that reserved word NOT was specified.
2494 ----------------------------------
2495 -- Insert_Stable_Property_Check --
2496 ----------------------------------
2498 procedure Insert_Stable_Property_Check
2499 (Formal : Entity_Id; Property_Function : Entity_Id) is
2501 Args : constant List_Id :=
2502 New_List
2503 (Make_Pragma_Argument_Association
2504 (Sloc => Loc,
2505 Expression =>
2506 Make_Stable_Property_Condition
2507 (Formal => Formal,
2508 Property_Function => Property_Function)),
2509 Make_Pragma_Argument_Association
2510 (Sloc => Loc,
2511 Expression =>
2512 Make_String_Literal
2513 (Sloc => Loc,
2514 Strval =>
2515 "failed stable property check at "
2516 & Build_Location_String (Loc)
2517 & " for parameter "
2518 & To_String (Fully_Qualified_Name_String
2519 (Formal, Append_NUL => False))
2520 & " and property function "
2521 & To_String (Fully_Qualified_Name_String
2522 (Property_Function, Append_NUL => False))
2523 )));
2525 Prag : constant Node_Id :=
2526 Make_Pragma (Loc,
2527 Pragma_Identifier =>
2528 Make_Identifier (Loc, Name_Postcondition),
2529 Pragma_Argument_Associations => Args,
2530 Class_Present => Class_Present);
2532 Subp_Decl : constant Node_Id := Enclosing_Declaration (Subp_Id);
2533 pragma Assert (Is_Declaration (Subp_Decl));
2534 begin
2535 Insert_After_And_Analyze (Subp_Decl, Prag);
2536 end Insert_Stable_Property_Check;
2538 ------------------------------------
2539 -- Make_Stable_Property_Condition --
2540 ------------------------------------
2542 function Make_Stable_Property_Condition
2543 (Formal : Entity_Id; Property_Function : Entity_Id) return Node_Id
2545 function Call_Property_Function return Node_Id is
2546 (Make_Function_Call
2547 (Loc,
2548 Name =>
2549 New_Occurrence_Of (Property_Function, Loc),
2550 Parameter_Associations =>
2551 New_List (New_Occurrence_Of (Formal, Loc))));
2552 begin
2553 return Make_Op_Eq
2554 (Loc,
2555 Call_Property_Function,
2556 Make_Attribute_Reference
2557 (Loc,
2558 Prefix => Call_Property_Function,
2559 Attribute_Name => Name_Old));
2560 end Make_Stable_Property_Condition;
2562 -----------------------
2563 -- Stable_Properties --
2564 -----------------------
2566 function Stable_Properties
2567 (Aspect_Bearer : Entity_Id; Negated : out Boolean)
2568 return Subprogram_List
2570 Aspect_Spec : Node_Id :=
2571 Find_Value_Of_Aspect
2572 (Aspect_Bearer, Aspect_Stable_Properties,
2573 Class_Present => Class_Present);
2574 begin
2575 -- ??? For a derived type, we wish Find_Value_Of_Aspect
2576 -- somehow knew that this aspect is not inherited.
2577 -- But it doesn't, so we cope with that here.
2579 -- There are probably issues here with inheritance from
2580 -- interface types, where just looking for the one parent type
2581 -- isn't enough. But this is far from the only work needed for
2582 -- Stable_Properties'Class for interface types.
2584 if Is_Derived_Type (Aspect_Bearer) then
2585 declare
2586 Parent_Type : constant Entity_Id :=
2587 Etype (Base_Type (Aspect_Bearer));
2588 begin
2589 if Aspect_Spec =
2590 Find_Value_Of_Aspect
2591 (Parent_Type, Aspect_Stable_Properties,
2592 Class_Present => Class_Present)
2593 then
2594 -- prevent inheritance
2595 Aspect_Spec := Empty;
2596 end if;
2597 end;
2598 end if;
2600 if No (Aspect_Spec) then
2601 Negated := Aspect_Bearer = Subp_Id;
2602 -- This is a little bit subtle.
2603 -- We need to assign True in the Subp_Id case in order to
2604 -- distinguish between no aspect spec at all vs. an
2605 -- explicitly specified "with S_P => []" empty list.
2606 -- In both cases Stable_Properties will return a length-0
2607 -- array, but the two cases are not equivalent.
2608 -- Very roughly speaking the lack of an S_P aspect spec for
2609 -- a subprogram would be equivalent to something like
2610 -- "with S_P => [not]", where we apply the "not" modifier to
2611 -- an empty set of subprograms, if such a construct existed.
2612 -- We could just assign True here, but it seems untidy to
2613 -- return True in the case of an aspect spec for a type
2614 -- (since negation is only allowed for subp S_P aspects).
2616 return (1 .. 0 => <>);
2617 else
2618 return Parse_Aspect_Stable_Properties
2619 (Aspect_Spec, Negated => Negated);
2620 end if;
2621 end Stable_Properties;
2623 Formal : Entity_Id := First_Formal (Subp_Id);
2624 Type_Of_Formal : Entity_Id;
2626 Subp_Properties_Negated : Boolean;
2627 Subp_Properties : constant Subprogram_List :=
2628 Stable_Properties (Subp_Id, Subp_Properties_Negated);
2630 -- start of processing for Add_Stable_Property_Contracts
2632 begin
2633 if not (Is_Primitive (Subp_Id) and then Comes_From_Source (Subp_Id))
2634 then
2635 return;
2636 end if;
2638 while Present (Formal) loop
2639 Type_Of_Formal := Base_Type (Etype (Formal));
2641 if not Subp_Properties_Negated then
2643 for SPF_Id of Subp_Properties loop
2644 if Type_Of_Formal = Base_Type (Etype (First_Formal (SPF_Id)))
2645 and then Scope (Type_Of_Formal) = Scope (Subp_Id)
2646 then
2647 -- ??? Need to filter out checks for SPFs that are
2648 -- mentioned explicitly in the postcondition of
2649 -- Subp_Id.
2651 Insert_Stable_Property_Check
2652 (Formal => Formal, Property_Function => SPF_Id);
2653 end if;
2654 end loop;
2656 elsif Scope (Type_Of_Formal) = Scope (Subp_Id) then
2657 declare
2658 Ignored : Boolean range False .. False;
2660 Typ_Property_Funcs : constant Subprogram_List :=
2661 Stable_Properties (Type_Of_Formal, Negated => Ignored);
2663 function Excluded_By_Aspect_Spec_Of_Subp
2664 (SPF_Id : Entity_Id) return Boolean;
2665 -- Examine Subp_Properties to determine whether SPF should
2666 -- be excluded.
2668 -------------------------------------
2669 -- Excluded_By_Aspect_Spec_Of_Subp --
2670 -------------------------------------
2672 function Excluded_By_Aspect_Spec_Of_Subp
2673 (SPF_Id : Entity_Id) return Boolean is
2674 begin
2675 pragma Assert (Subp_Properties_Negated);
2676 -- Look through renames for equality test here ???
2677 return (for some F of Subp_Properties => F = SPF_Id);
2678 end Excluded_By_Aspect_Spec_Of_Subp;
2680 -- Look through renames for equality test here ???
2681 Subp_Is_Stable_Property_Function : constant Boolean :=
2682 (for some F of Typ_Property_Funcs => F = Subp_Id);
2683 begin
2684 if not Subp_Is_Stable_Property_Function then
2685 for SPF_Id of Typ_Property_Funcs loop
2686 if not Excluded_By_Aspect_Spec_Of_Subp (SPF_Id) then
2687 -- ??? Need to filter out checks for SPFs that are
2688 -- mentioned explicitly in the postcondition of
2689 -- Subp_Id.
2690 Insert_Stable_Property_Check
2691 (Formal => Formal, Property_Function => SPF_Id);
2692 end if;
2693 end loop;
2694 end if;
2695 end;
2696 end if;
2697 Next_Formal (Formal);
2698 end loop;
2699 end Add_Stable_Property_Contracts;
2701 -------------------------
2702 -- Append_Enabled_Item --
2703 -------------------------
2705 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
2706 begin
2707 -- Do not chain ignored or disabled pragmas
2709 if Nkind (Item) = N_Pragma
2710 and then (Is_Ignored (Item) or else Is_Disabled (Item))
2711 then
2712 null;
2714 -- Otherwise, add the item
2716 else
2717 if No (List) then
2718 List := New_List;
2719 end if;
2721 -- If the pragma is a conjunct in a composite postcondition, it
2722 -- has been processed in reverse order. In the postcondition body
2723 -- it must appear before the others.
2725 if Nkind (Item) = N_Pragma
2726 and then From_Aspect_Specification (Item)
2727 and then Split_PPC (Item)
2728 then
2729 Prepend (Item, List);
2730 else
2731 Append (Item, List);
2732 end if;
2733 end if;
2734 end Append_Enabled_Item;
2736 ----------------------------
2737 -- Process_Contract_Cases --
2738 ----------------------------
2740 procedure Process_Contract_Cases
2741 (Stmts : in out List_Id;
2742 Decls : List_Id)
2744 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
2745 -- Process pragma Contract_Cases for subprogram Subp_Id
2747 --------------------------------
2748 -- Process_Contract_Cases_For --
2749 --------------------------------
2751 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
2752 Items : constant Node_Id := Contract (Subp_Id);
2753 Prag : Node_Id;
2755 begin
2756 if Present (Items) then
2757 Prag := Contract_Test_Cases (Items);
2758 while Present (Prag) loop
2759 if Is_Checked (Prag) then
2760 if Pragma_Name (Prag) = Name_Always_Terminates then
2761 Expand_Pragma_Always_Terminates (Prag);
2763 elsif Pragma_Name (Prag) = Name_Contract_Cases then
2764 Expand_Pragma_Contract_Cases
2765 (CCs => Prag,
2766 Subp_Id => Subp_Id,
2767 Decls => Decls,
2768 Stmts => Stmts);
2770 elsif Pragma_Name (Prag) = Name_Exceptional_Cases then
2771 Expand_Pragma_Exceptional_Cases (Prag);
2773 elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
2774 Expand_Pragma_Subprogram_Variant
2775 (Prag => Prag,
2776 Subp_Id => Subp_Id,
2777 Body_Decls => Decls);
2778 end if;
2779 end if;
2781 Prag := Next_Pragma (Prag);
2782 end loop;
2783 end if;
2784 end Process_Contract_Cases_For;
2786 -- Start of processing for Process_Contract_Cases
2788 begin
2789 Process_Contract_Cases_For (Body_Id);
2791 if Present (Spec_Id) then
2792 Process_Contract_Cases_For (Spec_Id);
2793 end if;
2794 end Process_Contract_Cases;
2796 ----------------------------
2797 -- Process_Postconditions --
2798 ----------------------------
2800 procedure Process_Postconditions (Stmts : in out List_Id) is
2801 procedure Process_Body_Postconditions (Post_Nam : Name_Id);
2802 -- Collect all [refined] postconditions of a specific kind denoted
2803 -- by Post_Nam that belong to the body, and generate pragma Check
2804 -- equivalents in list Stmts.
2806 procedure Process_Spec_Postconditions;
2807 -- Collect all [inherited] postconditions of the spec, and generate
2808 -- pragma Check equivalents in list Stmts.
2810 ---------------------------------
2811 -- Process_Body_Postconditions --
2812 ---------------------------------
2814 procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
2815 Items : constant Node_Id := Contract (Body_Id);
2816 Unit_Decl : constant Node_Id := Parent (Body_Decl);
2817 Decl : Node_Id;
2818 Prag : Node_Id;
2820 begin
2821 -- Process the contract
2823 if Present (Items) then
2824 Prag := Pre_Post_Conditions (Items);
2825 while Present (Prag) loop
2826 if Pragma_Name (Prag) = Post_Nam
2827 and then Is_Checked (Prag)
2828 then
2829 Append_Enabled_Item
2830 (Item => Build_Pragma_Check_Equivalent (Prag),
2831 List => Stmts);
2832 end if;
2834 Prag := Next_Pragma (Prag);
2835 end loop;
2836 end if;
2838 -- The subprogram body being processed is actually the proper body
2839 -- of a stub with a corresponding spec. The subprogram stub may
2840 -- carry a postcondition pragma, in which case it must be taken
2841 -- into account. The pragma appears after the stub.
2843 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
2844 Decl := Next (Corresponding_Stub (Unit_Decl));
2845 while Present (Decl) loop
2847 -- Note that non-matching pragmas are skipped
2849 if Nkind (Decl) = N_Pragma then
2850 if Pragma_Name (Decl) = Post_Nam
2851 and then Is_Checked (Decl)
2852 then
2853 Append_Enabled_Item
2854 (Item => Build_Pragma_Check_Equivalent (Decl),
2855 List => Stmts);
2856 end if;
2858 -- Skip internally generated code
2860 elsif not Comes_From_Source (Decl) then
2861 null;
2863 -- Postcondition pragmas are usually grouped together. There
2864 -- is no need to inspect the whole declarative list.
2866 else
2867 exit;
2868 end if;
2870 Next (Decl);
2871 end loop;
2872 end if;
2873 end Process_Body_Postconditions;
2875 ---------------------------------
2876 -- Process_Spec_Postconditions --
2877 ---------------------------------
2879 procedure Process_Spec_Postconditions is
2880 Subps : constant Subprogram_List :=
2881 Inherited_Subprograms (Spec_Id);
2882 Seen : Subprogram_List (Subps'Range) := (others => Empty);
2884 function Seen_Subp (Subp_Id : Entity_Id) return Boolean;
2885 -- Return True if the contract of subprogram Subp_Id has been
2886 -- processed.
2888 ---------------
2889 -- Seen_Subp --
2890 ---------------
2892 function Seen_Subp (Subp_Id : Entity_Id) return Boolean is
2893 begin
2894 for Index in Seen'Range loop
2895 if Seen (Index) = Subp_Id then
2896 return True;
2897 end if;
2898 end loop;
2900 return False;
2901 end Seen_Subp;
2903 -- Local variables
2905 Item : Node_Id;
2906 Items : Node_Id;
2907 Prag : Node_Id;
2908 Subp_Id : Entity_Id;
2910 -- Start of processing for Process_Spec_Postconditions
2912 begin
2913 -- Process the contract
2915 Items := Contract (Spec_Id);
2917 if Present (Items) then
2918 Prag := Pre_Post_Conditions (Items);
2919 while Present (Prag) loop
2920 if Pragma_Name (Prag) = Name_Postcondition
2921 and then Is_Checked (Prag)
2922 then
2923 Append_Enabled_Item
2924 (Item => Build_Pragma_Check_Equivalent (Prag),
2925 List => Stmts);
2926 end if;
2928 Prag := Next_Pragma (Prag);
2929 end loop;
2930 end if;
2932 -- Process the contracts of all inherited subprograms, looking for
2933 -- class-wide postconditions.
2935 for Index in Subps'Range loop
2936 Subp_Id := Subps (Index);
2938 if Present (Alias (Subp_Id)) then
2939 Subp_Id := Ultimate_Alias (Subp_Id);
2940 end if;
2942 -- Wrappers of class-wide pre/postconditions reference the
2943 -- parent primitive that has the inherited contract.
2945 if Is_Wrapper (Subp_Id)
2946 and then Present (LSP_Subprogram (Subp_Id))
2947 then
2948 Subp_Id := LSP_Subprogram (Subp_Id);
2949 end if;
2951 Items := Contract (Subp_Id);
2953 if not Seen_Subp (Subp_Id) and then Present (Items) then
2954 Seen (Index) := Subp_Id;
2956 Prag := Pre_Post_Conditions (Items);
2957 while Present (Prag) loop
2958 if Pragma_Name (Prag) = Name_Postcondition
2959 and then Class_Present (Prag)
2960 then
2961 Item :=
2962 Build_Pragma_Check_Equivalent
2963 (Prag => Prag,
2964 Subp_Id => Spec_Id,
2965 Inher_Id => Subp_Id);
2967 -- The pragma Check equivalent of the class-wide
2968 -- postcondition is still created even though the
2969 -- pragma may be ignored because the equivalent
2970 -- performs semantic checks.
2972 if Is_Checked (Prag) then
2973 Append_Enabled_Item (Item, Stmts);
2974 end if;
2975 end if;
2977 Prag := Next_Pragma (Prag);
2978 end loop;
2979 end if;
2980 end loop;
2981 end Process_Spec_Postconditions;
2983 pragma Unmodified (Stmts);
2984 -- Stmts is passed as IN OUT to signal that the list can be updated,
2985 -- even if the corresponding integer value representing the list does
2986 -- not change.
2988 -- Start of processing for Process_Postconditions
2990 begin
2991 -- The processing of postconditions is done in reverse order (body
2992 -- first) to ensure the following arrangement:
2994 -- <refined postconditions from body>
2995 -- <postconditions from body>
2996 -- <postconditions from spec>
2997 -- <inherited postconditions>
2999 Process_Body_Postconditions (Name_Refined_Post);
3000 Process_Body_Postconditions (Name_Postcondition);
3002 if Present (Spec_Id) then
3003 Process_Spec_Postconditions;
3004 end if;
3005 end Process_Postconditions;
3007 ---------------------------
3008 -- Process_Preconditions --
3009 ---------------------------
3011 procedure Process_Preconditions (Decls : in out List_Id) is
3012 Insert_Node : Node_Id := Empty;
3013 -- The insertion node after which all pragma Check equivalents are
3014 -- inserted.
3016 procedure Prepend_To_Decls (Item : Node_Id);
3017 -- Prepend a single item to the declarations of the subprogram body
3019 procedure Prepend_Pragma_To_Decls (Prag : Node_Id);
3020 -- Prepend a normal precondition to the declarations of the body and
3021 -- analyze it.
3023 procedure Process_Preconditions_For (Subp_Id : Entity_Id);
3024 -- Collect all preconditions of subprogram Subp_Id and prepend their
3025 -- pragma Check equivalents to the declarations of the body.
3027 ----------------------
3028 -- Prepend_To_Decls --
3029 ----------------------
3031 procedure Prepend_To_Decls (Item : Node_Id) is
3032 begin
3033 -- Ensure that the body has a declarative list
3035 if No (Decls) then
3036 Decls := New_List;
3037 Set_Declarations (Body_Decl, Decls);
3038 end if;
3040 Prepend_To (Decls, Item);
3041 end Prepend_To_Decls;
3043 -----------------------------
3044 -- Prepend_Pragma_To_Decls --
3045 -----------------------------
3047 procedure Prepend_Pragma_To_Decls (Prag : Node_Id) is
3048 Check_Prag : Node_Id;
3050 begin
3051 -- Skip the sole class-wide precondition (if any) since it is
3052 -- processed by Merge_Class_Conditions.
3054 if Class_Present (Prag) then
3055 null;
3057 -- Accumulate the corresponding Check pragmas at the top of the
3058 -- declarations. Prepending the items ensures that they will be
3059 -- evaluated in their original order.
3061 else
3062 Check_Prag := Build_Pragma_Check_Equivalent (Prag);
3063 Prepend_To_Decls (Check_Prag);
3065 end if;
3066 end Prepend_Pragma_To_Decls;
3068 -------------------------------
3069 -- Process_Preconditions_For --
3070 -------------------------------
3072 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
3073 Items : constant Node_Id := Contract (Subp_Id);
3074 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
3075 Decl : Node_Id;
3076 Freeze_T : Boolean;
3077 Prag : Node_Id;
3079 begin
3080 -- Process the contract. If the body is an expression function
3081 -- that is a completion, freeze types within, because this may
3082 -- not have been done yet, when the subprogram declaration and
3083 -- its completion by an expression function appear in distinct
3084 -- declarative lists of the same unit (visible and private).
3086 Freeze_T :=
3087 Was_Expression_Function (Body_Decl)
3088 and then Sloc (Body_Id) /= Sloc (Subp_Id)
3089 and then In_Same_Source_Unit (Body_Id, Subp_Id)
3090 and then not In_Same_List (Body_Decl, Subp_Decl);
3092 if Present (Items) then
3093 Prag := Pre_Post_Conditions (Items);
3094 while Present (Prag) loop
3095 if Pragma_Name (Prag) = Name_Precondition
3096 and then Is_Checked (Prag)
3097 then
3098 if Freeze_T
3099 and then Present (Corresponding_Aspect (Prag))
3100 then
3101 Freeze_Expr_Types
3102 (Def_Id => Subp_Id,
3103 Typ => Standard_Boolean,
3104 Expr =>
3105 Expression
3106 (First (Pragma_Argument_Associations (Prag))),
3107 N => Body_Decl);
3108 end if;
3110 Prepend_Pragma_To_Decls (Prag);
3111 end if;
3113 Prag := Next_Pragma (Prag);
3114 end loop;
3115 end if;
3117 -- The subprogram declaration being processed is actually a body
3118 -- stub. The stub may carry a precondition pragma, in which case
3119 -- it must be taken into account. The pragma appears after the
3120 -- stub.
3122 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
3124 -- Inspect the declarations following the body stub
3126 Decl := Next (Subp_Decl);
3127 while Present (Decl) loop
3129 -- Note that non-matching pragmas are skipped
3131 if Nkind (Decl) = N_Pragma then
3132 if Pragma_Name (Decl) = Name_Precondition
3133 and then Is_Checked (Decl)
3134 then
3135 Prepend_Pragma_To_Decls (Decl);
3136 end if;
3138 -- Skip internally generated code
3140 elsif not Comes_From_Source (Decl) then
3141 null;
3143 -- Preconditions are usually grouped together. There is no
3144 -- need to inspect the whole declarative list.
3146 else
3147 exit;
3148 end if;
3150 Next (Decl);
3151 end loop;
3152 end if;
3153 end Process_Preconditions_For;
3155 -- Local variables
3157 Body_Decls : constant List_Id := Declarations (Body_Decl);
3158 Decl : Node_Id;
3159 Next_Decl : Node_Id;
3161 -- Start of processing for Process_Preconditions
3163 begin
3164 -- Find the proper insertion point for all pragma Check equivalents
3166 if Present (Body_Decls) then
3167 Decl := First (Body_Decls);
3168 while Present (Decl) loop
3170 -- First source declaration terminates the search, because all
3171 -- preconditions must be evaluated prior to it, by definition.
3173 if Comes_From_Source (Decl) then
3174 exit;
3176 -- Certain internally generated object renamings such as those
3177 -- for discriminants and protection fields must be elaborated
3178 -- before the preconditions are evaluated, as their expressions
3179 -- may mention the discriminants. The renamings include those
3180 -- for private components so we need to find the last such.
3182 elsif Is_Prologue_Renaming (Decl) then
3183 while Present (Next (Decl))
3184 and then Is_Prologue_Renaming (Next (Decl))
3185 loop
3186 Next (Decl);
3187 end loop;
3189 Insert_Node := Decl;
3191 -- Otherwise the declaration does not come from source. This
3192 -- also terminates the search, because internal code may raise
3193 -- exceptions which should not preempt the preconditions.
3195 else
3196 exit;
3197 end if;
3199 Next (Decl);
3200 end loop;
3202 -- The processing of preconditions is done in reverse order (body
3203 -- first), because each pragma Check equivalent is inserted at the
3204 -- top of the declarations. This ensures that the final order is
3205 -- consistent with following diagram:
3207 -- <inherited preconditions>
3208 -- <preconditions from spec>
3209 -- <preconditions from body>
3211 Process_Preconditions_For (Body_Id);
3213 -- Move the generated entry-call prologue renamings into the
3214 -- outer declarations for use in the preconditions.
3216 Decl := First (Body_Decls);
3217 while Present (Decl) and then Present (Insert_Node) loop
3218 Next_Decl := Next (Decl);
3219 Remove (Decl);
3220 Prepend_To_Decls (Decl);
3222 exit when Decl = Insert_Node;
3223 Decl := Next_Decl;
3224 end loop;
3225 end if;
3227 if Present (Spec_Id) then
3228 Process_Preconditions_For (Spec_Id);
3229 end if;
3230 end Process_Preconditions;
3232 -- Local variables
3234 Restore_Scope : Boolean := False;
3235 Result : Entity_Id;
3236 Stmts : List_Id := No_List;
3237 Decls : List_Id := New_List;
3238 Subp_Id : Entity_Id;
3240 -- Start of processing for Expand_Subprogram_Contract
3242 begin
3243 -- Obtain the entity of the initial declaration
3245 if Present (Spec_Id) then
3246 Subp_Id := Spec_Id;
3247 else
3248 Subp_Id := Body_Id;
3249 end if;
3251 -- Do not perform expansion activity when it is not needed
3253 if not Expander_Active then
3254 return;
3256 -- GNATprove does not need the executable semantics of a contract
3258 elsif GNATprove_Mode then
3259 return;
3261 -- The contract of a generic subprogram or one declared in a generic
3262 -- context is not expanded, as the corresponding instance will provide
3263 -- the executable semantics of the contract.
3265 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
3266 return;
3268 -- All subprograms carry a contract, but for some it is not significant
3269 -- and should not be processed. This is a small optimization.
3271 elsif not Has_Significant_Contract (Subp_Id) then
3272 return;
3274 -- The contract of an ignored Ghost subprogram does not need expansion,
3275 -- because the subprogram and all calls to it will be removed.
3277 elsif Is_Ignored_Ghost_Entity (Subp_Id) then
3278 return;
3280 -- No action needed for helpers and indirect-call wrapper built to
3281 -- support class-wide preconditions.
3283 elsif Present (Class_Preconditions_Subprogram (Subp_Id)) then
3284 return;
3286 -- Do not re-expand the same contract. This scenario occurs when a
3287 -- construct is rewritten into something else during its analysis
3288 -- (expression functions for instance).
3290 elsif Has_Expanded_Contract (Subp_Id) then
3291 return;
3292 end if;
3294 -- Prevent multiple expansion attempts of the same contract
3296 Set_Has_Expanded_Contract (Subp_Id);
3298 -- Ensure that the formal parameters are visible when expanding all
3299 -- contract items.
3301 if not In_Open_Scopes (Subp_Id) then
3302 Restore_Scope := True;
3303 Push_Scope (Subp_Id);
3305 if Is_Generic_Subprogram (Subp_Id) then
3306 Install_Generic_Formals (Subp_Id);
3307 else
3308 Install_Formals (Subp_Id);
3309 end if;
3310 end if;
3312 -- The expansion of a subprogram contract involves the creation of Check
3313 -- pragmas to verify the contract assertions of the spec and body in a
3314 -- particular order. The order is as follows:
3316 -- function Original_Code (...) return ... is
3317 -- <prologue renamings>
3318 -- <inherited preconditions>
3319 -- <preconditions from spec>
3320 -- <preconditions from body>
3321 -- <contract case conditions>
3323 -- function _Wrapped_Statements (...) return ... is
3324 -- <source declarations>
3325 -- begin
3326 -- <source statements>
3327 -- end _Wrapped_Statements;
3329 -- begin
3330 -- return Result : constant ... := _Wrapped_Statements do
3331 -- <refined postconditions from body>
3332 -- <postconditions from body>
3333 -- <postconditions from spec>
3334 -- <inherited postconditions>
3335 -- <contract case consequences>
3336 -- <invariant check of function result>
3337 -- <invariant and predicate checks of parameters
3338 -- end return;
3339 -- end Original_Code;
3341 -- Step 1: augment contracts list with postconditions associated with
3342 -- Stable_Properties and Stable_Properties'Class aspects. This must
3343 -- precede Process_Postconditions.
3345 for Class_Present in Boolean loop
3346 Add_Stable_Property_Contracts
3347 (Subp_Id, Class_Present => Class_Present);
3348 end loop;
3350 -- Step 2: Handle all preconditions. This action must come before the
3351 -- processing of pragma Contract_Cases because the pragma prepends items
3352 -- to the body declarations.
3354 Process_Preconditions (Decls);
3356 -- Step 3: Handle all postconditions. This action must come before the
3357 -- processing of pragma Contract_Cases because the pragma appends items
3358 -- to list Stmts.
3360 Process_Postconditions (Stmts);
3362 -- Step 4: Handle pragma Contract_Cases. This action must come before
3363 -- the processing of invariants and predicates because those append
3364 -- items to list Stmts.
3366 Process_Contract_Cases (Stmts, Decls);
3368 -- Step 5: Apply invariant and predicate checks on a function result and
3369 -- all formals. The resulting checks are accumulated in list Stmts.
3371 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
3373 -- Step 6: Construct subprogram _wrapped_statements
3375 -- When no statements are present we still need to insert contract
3376 -- related declarations.
3378 if No (Stmts) then
3379 Prepend_List_To (Declarations (Body_Decl), Decls);
3381 -- Otherwise, we need a wrapper
3383 else
3384 Build_Subprogram_Contract_Wrapper (Body_Id, Stmts, Decls, Result);
3385 end if;
3387 if Restore_Scope then
3388 End_Scope;
3389 end if;
3390 end Expand_Subprogram_Contract;
3392 -------------------------------
3393 -- Freeze_Previous_Contracts --
3394 -------------------------------
3396 procedure Freeze_Previous_Contracts (Body_Decl : Node_Id) is
3397 function Causes_Contract_Freezing (N : Node_Id) return Boolean;
3398 pragma Inline (Causes_Contract_Freezing);
3399 -- Determine whether arbitrary node N causes contract freezing. This is
3400 -- used as an assertion for the current body declaration that caused
3401 -- contract freezing, and as a condition to detect body declaration that
3402 -- already caused contract freezing before.
3404 procedure Freeze_Contracts;
3405 pragma Inline (Freeze_Contracts);
3406 -- Freeze the contracts of all eligible constructs which precede body
3407 -- Body_Decl.
3409 procedure Freeze_Enclosing_Package_Body;
3410 pragma Inline (Freeze_Enclosing_Package_Body);
3411 -- Freeze the contract of the nearest package body (if any) which
3412 -- encloses body Body_Decl.
3414 ------------------------------
3415 -- Causes_Contract_Freezing --
3416 ------------------------------
3418 function Causes_Contract_Freezing (N : Node_Id) return Boolean is
3419 begin
3420 -- The following condition matches guards for calls to
3421 -- Freeze_Previous_Contracts from routines that analyze various body
3422 -- declarations. In particular, it detects expression functions, as
3423 -- described in the call from Analyze_Subprogram_Body_Helper.
3425 return
3426 Comes_From_Source (Original_Node (N))
3427 and then
3428 Nkind (N) in
3429 N_Entry_Body | N_Package_Body | N_Protected_Body |
3430 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body;
3431 end Causes_Contract_Freezing;
3433 ----------------------
3434 -- Freeze_Contracts --
3435 ----------------------
3437 procedure Freeze_Contracts is
3438 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
3439 Decl : Node_Id;
3441 begin
3442 -- Nothing to do when the body which causes freezing does not appear
3443 -- in a declarative list because there cannot possibly be constructs
3444 -- with contracts.
3446 if not Is_List_Member (Body_Decl) then
3447 return;
3448 end if;
3450 -- Inspect the declarations preceding the body, and freeze individual
3451 -- contracts of eligible constructs.
3453 Decl := Prev (Body_Decl);
3454 while Present (Decl) loop
3456 -- Stop the traversal when a preceding construct that causes
3457 -- freezing is encountered as there is no point in refreezing
3458 -- the already frozen constructs.
3460 if Causes_Contract_Freezing (Decl) then
3461 exit;
3463 -- Entry or subprogram declarations
3465 elsif Nkind (Decl) in N_Abstract_Subprogram_Declaration
3466 | N_Entry_Declaration
3467 | N_Generic_Subprogram_Declaration
3468 | N_Subprogram_Declaration
3469 then
3470 Analyze_Entry_Or_Subprogram_Contract
3471 (Subp_Id => Defining_Entity (Decl),
3472 Freeze_Id => Body_Id);
3474 -- Objects
3476 elsif Nkind (Decl) = N_Object_Declaration then
3477 Analyze_Object_Contract
3478 (Obj_Id => Defining_Entity (Decl),
3479 Freeze_Id => Body_Id);
3481 -- Protected units
3483 elsif Nkind (Decl) in N_Protected_Type_Declaration
3484 | N_Single_Protected_Declaration
3485 then
3486 Analyze_Protected_Contract (Defining_Entity (Decl));
3488 -- Subprogram body stubs
3490 elsif Nkind (Decl) = N_Subprogram_Body_Stub then
3491 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
3493 -- Task units
3495 elsif Nkind (Decl) in N_Single_Task_Declaration
3496 | N_Task_Type_Declaration
3497 then
3498 Analyze_Task_Contract (Defining_Entity (Decl));
3499 end if;
3501 if Nkind (Decl) in N_Full_Type_Declaration
3502 | N_Private_Type_Declaration
3503 | N_Task_Type_Declaration
3504 | N_Protected_Type_Declaration
3505 | N_Formal_Type_Declaration
3506 then
3507 Analyze_Type_Contract (Defining_Identifier (Decl));
3508 end if;
3510 Prev (Decl);
3511 end loop;
3512 end Freeze_Contracts;
3514 -----------------------------------
3515 -- Freeze_Enclosing_Package_Body --
3516 -----------------------------------
3518 procedure Freeze_Enclosing_Package_Body is
3519 Orig_Decl : constant Node_Id := Original_Node (Body_Decl);
3520 Par : Node_Id;
3522 begin
3523 -- Climb the parent chain looking for an enclosing package body. Do
3524 -- not use the scope stack, because a body utilizes the entity of its
3525 -- corresponding spec.
3527 Par := Parent (Body_Decl);
3528 while Present (Par) loop
3529 if Nkind (Par) = N_Package_Body then
3530 Analyze_Package_Body_Contract
3531 (Body_Id => Defining_Entity (Par),
3532 Freeze_Id => Defining_Entity (Body_Decl));
3534 exit;
3536 -- Do not look for an enclosing package body when the construct
3537 -- which causes freezing is a body generated for an expression
3538 -- function and it appears within a package spec. This ensures
3539 -- that the traversal will not reach too far up the parent chain
3540 -- and attempt to freeze a package body which must not be frozen.
3542 -- package body Enclosing_Body
3543 -- with Refined_State => (State => Var)
3544 -- is
3545 -- package Nested is
3546 -- type Some_Type is ...;
3547 -- function Cause_Freezing return ...;
3548 -- private
3549 -- function Cause_Freezing is (...);
3550 -- end Nested;
3552 -- Var : Nested.Some_Type;
3554 elsif Nkind (Par) = N_Package_Declaration
3555 and then Nkind (Orig_Decl) = N_Expression_Function
3556 then
3557 exit;
3559 -- Prevent the search from going too far
3561 elsif Is_Body_Or_Package_Declaration (Par) then
3562 exit;
3563 end if;
3565 Par := Parent (Par);
3566 end loop;
3567 end Freeze_Enclosing_Package_Body;
3569 -- Local variables
3571 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
3573 -- Start of processing for Freeze_Previous_Contracts
3575 begin
3576 pragma Assert (Causes_Contract_Freezing (Body_Decl));
3578 -- A body that is in the process of being inlined appears from source,
3579 -- but carries name _parent. Such a body does not cause freezing of
3580 -- contracts.
3582 if Chars (Body_Id) = Name_uParent then
3583 return;
3584 end if;
3586 Freeze_Enclosing_Package_Body;
3587 Freeze_Contracts;
3588 end Freeze_Previous_Contracts;
3590 ---------------------------------
3591 -- Inherit_Subprogram_Contract --
3592 ---------------------------------
3594 procedure Inherit_Subprogram_Contract
3595 (Subp : Entity_Id;
3596 From_Subp : Entity_Id)
3598 procedure Inherit_Pragma (Prag_Id : Pragma_Id);
3599 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3600 -- Subp's contract.
3602 --------------------
3603 -- Inherit_Pragma --
3604 --------------------
3606 procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
3607 Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
3608 New_Prag : Node_Id;
3610 begin
3611 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3612 -- chains, therefore the node must be replicated. The new pragma is
3613 -- flagged as inherited for distinction purposes.
3615 if Present (Prag) then
3616 New_Prag := New_Copy_Tree (Prag);
3617 Set_Is_Inherited_Pragma (New_Prag);
3619 Add_Contract_Item (New_Prag, Subp);
3620 end if;
3621 end Inherit_Pragma;
3623 -- Start of processing for Inherit_Subprogram_Contract
3625 begin
3626 -- Inheritance is carried out only when both entities are subprograms
3627 -- with contracts.
3629 if Is_Subprogram_Or_Generic_Subprogram (Subp)
3630 and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
3631 and then Present (Contract (From_Subp))
3632 then
3633 Inherit_Pragma (Pragma_Extensions_Visible);
3634 Inherit_Pragma (Pragma_Side_Effects);
3635 end if;
3636 end Inherit_Subprogram_Contract;
3638 -------------------------------------
3639 -- Instantiate_Subprogram_Contract --
3640 -------------------------------------
3642 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
3643 procedure Instantiate_Pragmas (First_Prag : Node_Id);
3644 -- Instantiate all contract-related source pragmas found in the list,
3645 -- starting with pragma First_Prag. Each instantiated pragma is added
3646 -- to list L.
3648 -------------------------
3649 -- Instantiate_Pragmas --
3650 -------------------------
3652 procedure Instantiate_Pragmas (First_Prag : Node_Id) is
3653 Inst_Prag : Node_Id;
3654 Prag : Node_Id;
3656 begin
3657 Prag := First_Prag;
3658 while Present (Prag) loop
3659 if Is_Generic_Contract_Pragma (Prag) then
3660 Inst_Prag :=
3661 Copy_Generic_Node (Prag, Empty, Instantiating => True);
3663 Set_Analyzed (Inst_Prag, False);
3664 Append_To (L, Inst_Prag);
3665 end if;
3667 Prag := Next_Pragma (Prag);
3668 end loop;
3669 end Instantiate_Pragmas;
3671 -- Local variables
3673 Items : constant Node_Id := Contract (Defining_Entity (Templ));
3675 -- Start of processing for Instantiate_Subprogram_Contract
3677 begin
3678 if Present (Items) then
3679 Instantiate_Pragmas (Pre_Post_Conditions (Items));
3680 Instantiate_Pragmas (Contract_Test_Cases (Items));
3681 Instantiate_Pragmas (Classifications (Items));
3682 end if;
3683 end Instantiate_Subprogram_Contract;
3685 --------------------------
3686 -- Is_Prologue_Renaming --
3687 --------------------------
3689 -- This should be turned into a flag and set during the expansion of
3690 -- task and protected types when the renamings get generated ???
3692 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
3693 Nam : Node_Id;
3694 Obj : Entity_Id;
3695 Pref : Node_Id;
3696 Sel : Node_Id;
3698 begin
3699 if Nkind (Decl) = N_Object_Renaming_Declaration
3700 and then not Comes_From_Source (Decl)
3701 then
3702 Obj := Defining_Entity (Decl);
3703 Nam := Name (Decl);
3705 if Nkind (Nam) = N_Selected_Component then
3706 -- Analyze the renaming declaration so we can further examine it
3708 if not Analyzed (Decl) then
3709 Analyze (Decl);
3710 end if;
3712 Pref := Prefix (Nam);
3713 Sel := Selector_Name (Nam);
3715 -- A discriminant renaming appears as
3716 -- Discr : constant ... := Prefix.Discr;
3718 if Ekind (Obj) = E_Constant
3719 and then Is_Entity_Name (Sel)
3720 and then Present (Entity (Sel))
3721 and then Ekind (Entity (Sel)) = E_Discriminant
3722 then
3723 return True;
3725 -- A protection field renaming appears as
3726 -- Prot : ... := _object._object;
3728 -- A renamed private component is just a component of
3729 -- _object, with an arbitrary name.
3731 elsif Ekind (Obj) in E_Variable | E_Constant
3732 and then Nkind (Pref) = N_Identifier
3733 and then Chars (Pref) = Name_uObject
3734 and then Nkind (Sel) = N_Identifier
3735 then
3736 return True;
3737 end if;
3738 end if;
3739 end if;
3741 return False;
3742 end Is_Prologue_Renaming;
3744 -----------------------------------
3745 -- Make_Class_Precondition_Subps --
3746 -----------------------------------
3748 procedure Make_Class_Precondition_Subps
3749 (Subp_Id : Entity_Id;
3750 Late_Overriding : Boolean := False)
3752 Loc : constant Source_Ptr := Sloc (Subp_Id);
3753 Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
3755 procedure Add_Indirect_Call_Wrapper;
3756 -- Build the indirect-call wrapper and append it to the freezing actions
3757 -- of Tagged_Type.
3759 procedure Add_Call_Helper
3760 (Helper_Id : Entity_Id;
3761 Is_Dynamic : Boolean);
3762 -- Factorizes code for building a call helper with the given identifier
3763 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
3764 -- controls building the static or dynamic version of the helper.
3766 function Build_Unique_Name (Suffix : String) return Name_Id;
3767 -- Build an unique new name adding suffix to Subp_Id name (plus its
3768 -- homonym number for values bigger than 1).
3770 -------------------------------
3771 -- Add_Indirect_Call_Wrapper --
3772 -------------------------------
3774 procedure Add_Indirect_Call_Wrapper is
3776 function Build_ICW_Body return Node_Id;
3777 -- Build the body of the indirect call wrapper
3779 function Build_ICW_Decl return Node_Id;
3780 -- Build the declaration of the indirect call wrapper
3782 --------------------
3783 -- Build_ICW_Body --
3784 --------------------
3786 function Build_ICW_Body return Node_Id is
3787 ICW_Id : constant Entity_Id := Indirect_Call_Wrapper (Subp_Id);
3788 Spec : constant Node_Id := Parent (ICW_Id);
3789 Body_Spec : Node_Id;
3790 Call : Node_Id;
3791 ICW_Body : Node_Id;
3793 begin
3794 Body_Spec := Copy_Subprogram_Spec (Spec);
3796 -- Build call to wrapped subprogram
3798 declare
3799 Actuals : constant List_Id := Empty_List;
3800 Formal_Spec : Entity_Id :=
3801 First (Parameter_Specifications (Spec));
3802 begin
3803 -- Build parameter association & call
3805 while Present (Formal_Spec) loop
3806 Append_To (Actuals,
3807 New_Occurrence_Of
3808 (Defining_Identifier (Formal_Spec), Loc));
3809 Next (Formal_Spec);
3810 end loop;
3812 if Ekind (ICW_Id) = E_Procedure then
3813 Call :=
3814 Make_Procedure_Call_Statement (Loc,
3815 Name => New_Occurrence_Of (Subp_Id, Loc),
3816 Parameter_Associations => Actuals);
3817 else
3818 Call :=
3819 Make_Simple_Return_Statement (Loc,
3820 Expression =>
3821 Make_Function_Call (Loc,
3822 Name => New_Occurrence_Of (Subp_Id, Loc),
3823 Parameter_Associations => Actuals));
3824 end if;
3825 end;
3827 ICW_Body :=
3828 Make_Subprogram_Body (Loc,
3829 Specification => Body_Spec,
3830 Declarations => New_List,
3831 Handled_Statement_Sequence =>
3832 Make_Handled_Sequence_Of_Statements (Loc,
3833 Statements => New_List (Call)));
3835 -- The new operation is internal and overriding indicators do not
3836 -- apply.
3838 Set_Must_Override (Body_Spec, False);
3840 return ICW_Body;
3841 end Build_ICW_Body;
3843 --------------------
3844 -- Build_ICW_Decl --
3845 --------------------
3847 function Build_ICW_Decl return Node_Id is
3848 ICW_Id : constant Entity_Id :=
3849 Make_Defining_Identifier (Loc,
3850 Build_Unique_Name (Suffix => "ICW"));
3851 Decl : Node_Id;
3852 Spec : Node_Id;
3854 begin
3855 Spec := Copy_Subprogram_Spec (Parent (Subp_Id));
3856 Set_Must_Override (Spec, False);
3857 Set_Must_Not_Override (Spec, False);
3858 Set_Defining_Unit_Name (Spec, ICW_Id);
3859 Mutate_Ekind (ICW_Id, Ekind (Subp_Id));
3860 Set_Is_Public (ICW_Id);
3862 -- The indirect call wrapper is commonly used for indirect calls
3863 -- but inlined for direct calls performed from the DTW.
3865 Set_Is_Inlined (ICW_Id);
3867 if Nkind (Spec) = N_Procedure_Specification then
3868 Set_Null_Present (Spec, False);
3869 end if;
3871 Decl := Make_Subprogram_Declaration (Loc, Spec);
3873 -- Link original subprogram to indirect wrapper and vice versa
3875 Set_Indirect_Call_Wrapper (Subp_Id, ICW_Id);
3876 Set_Class_Preconditions_Subprogram (ICW_Id, Subp_Id);
3878 -- Inherit debug info flag to allow debugging the wrapper
3880 if Needs_Debug_Info (Subp_Id) then
3881 Set_Debug_Info_Needed (ICW_Id);
3882 end if;
3884 return Decl;
3885 end Build_ICW_Decl;
3887 -- Local Variables
3889 ICW_Body : Node_Id;
3890 ICW_Decl : Node_Id;
3892 -- Start of processing for Add_Indirect_Call_Wrapper
3894 begin
3895 pragma Assert (No (Indirect_Call_Wrapper (Subp_Id)));
3897 ICW_Decl := Build_ICW_Decl;
3899 Append_Freeze_Action (Tagged_Type, ICW_Decl);
3900 Analyze (ICW_Decl);
3902 ICW_Body := Build_ICW_Body;
3903 Append_Freeze_Action (Tagged_Type, ICW_Body);
3905 -- We cannot defer the analysis of this ICW wrapper when it is
3906 -- built as a consequence of building its partner DTW wrapper
3907 -- at the freezing point of the tagged type.
3909 if Is_Dispatch_Table_Wrapper (Subp_Id) then
3910 Analyze (ICW_Body);
3911 end if;
3912 end Add_Indirect_Call_Wrapper;
3914 ---------------------
3915 -- Add_Call_Helper --
3916 ---------------------
3918 procedure Add_Call_Helper
3919 (Helper_Id : Entity_Id;
3920 Is_Dynamic : Boolean)
3922 function Build_Call_Helper_Body return Node_Id;
3923 -- Build the body of a call helper
3925 function Build_Call_Helper_Decl return Node_Id;
3926 -- Build the declaration of a call helper
3928 function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id;
3929 -- Build the specification of the helper
3931 ----------------------------
3932 -- Build_Call_Helper_Body --
3933 ----------------------------
3935 function Build_Call_Helper_Body return Node_Id is
3937 function Copy_And_Update_References
3938 (Expr : Node_Id) return Node_Id;
3939 -- Copy Expr updating references to formals of Helper_Id; update
3940 -- also references to loop identifiers of quantified expressions.
3942 --------------------------------
3943 -- Copy_And_Update_References --
3944 --------------------------------
3946 function Copy_And_Update_References
3947 (Expr : Node_Id) return Node_Id
3949 Assoc_List : constant Elist_Id := New_Elmt_List;
3951 procedure Map_Quantified_Expression_Loop_Identifiers;
3952 -- Traverse Expr and append to Assoc_List the mapping of loop
3953 -- identifers of quantified expressions with its new copy.
3955 ------------------------------------------------
3956 -- Map_Quantified_Expression_Loop_Identifiers --
3957 ------------------------------------------------
3959 procedure Map_Quantified_Expression_Loop_Identifiers is
3960 function Map_Loop_Param (N : Node_Id) return Traverse_Result;
3961 -- Append to Assoc_List the mapping of loop identifers of
3962 -- quantified expressions with its new copy.
3964 --------------------
3965 -- Map_Loop_Param --
3966 --------------------
3968 function Map_Loop_Param (N : Node_Id) return Traverse_Result
3970 begin
3971 if Nkind (N) = N_Loop_Parameter_Specification
3972 and then Nkind (Parent (N)) = N_Quantified_Expression
3973 then
3974 declare
3975 Def_Id : constant Entity_Id :=
3976 Defining_Identifier (N);
3977 begin
3978 Append_Elmt (Def_Id, Assoc_List);
3979 Append_Elmt (New_Copy (Def_Id), Assoc_List);
3980 end;
3981 end if;
3983 return OK;
3984 end Map_Loop_Param;
3986 procedure Map_Quantified_Expressions is
3987 new Traverse_Proc (Map_Loop_Param);
3989 begin
3990 Map_Quantified_Expressions (Expr);
3991 end Map_Quantified_Expression_Loop_Identifiers;
3993 -- Local variables
3995 Subp_Formal_Id : Entity_Id := First_Formal (Subp_Id);
3996 Helper_Formal_Id : Entity_Id := First_Formal (Helper_Id);
3998 -- Start of processing for Copy_And_Update_References
4000 begin
4001 while Present (Subp_Formal_Id) loop
4002 Append_Elmt (Subp_Formal_Id, Assoc_List);
4003 Append_Elmt (Helper_Formal_Id, Assoc_List);
4005 Next_Formal (Subp_Formal_Id);
4006 Next_Formal (Helper_Formal_Id);
4007 end loop;
4009 Map_Quantified_Expression_Loop_Identifiers;
4011 return New_Copy_Tree (Expr, Map => Assoc_List);
4012 end Copy_And_Update_References;
4014 -- Local variables
4016 Helper_Decl : constant Node_Id := Parent (Parent (Helper_Id));
4017 Body_Id : Entity_Id;
4018 Body_Spec : Node_Id;
4019 Body_Stmts : Node_Id;
4020 Helper_Body : Node_Id;
4021 Return_Expr : Node_Id;
4023 -- Start of processing for Build_Call_Helper_Body
4025 begin
4026 pragma Assert (Analyzed (Unit_Declaration_Node (Helper_Id)));
4027 pragma Assert (No (Corresponding_Body (Helper_Decl)));
4029 Body_Id := Make_Defining_Identifier (Loc, Chars (Helper_Id));
4030 Body_Spec := Build_Call_Helper_Spec (Body_Id);
4032 Set_Corresponding_Body (Helper_Decl, Body_Id);
4033 Set_Must_Override (Body_Spec, False);
4035 if Present (Class_Preconditions (Subp_Id))
4036 -- Evaluate the expression if we are building a dynamic helper
4037 -- or we are building a static helper for a non-abstract tagged
4038 -- type; for abstract tagged types the helper just returns True
4039 -- since it is called by the indirect call wrapper (ICW).
4040 and then
4041 (Is_Dynamic
4042 or else
4043 not Is_Abstract_Type (Find_Dispatching_Type (Subp_Id)))
4044 then
4045 Return_Expr :=
4046 Copy_And_Update_References (Class_Preconditions (Subp_Id));
4048 -- When the subprogram is compiled with assertions disabled the
4049 -- helper just returns True; done to avoid reporting errors at
4050 -- link time since a unit may be compiled with assertions disabled
4051 -- and another (which depends on it) compiled with assertions
4052 -- enabled.
4054 else
4055 pragma Assert (Present (Ignored_Class_Preconditions (Subp_Id))
4056 or else Is_Abstract_Type (Find_Dispatching_Type (Subp_Id)));
4057 Return_Expr := New_Occurrence_Of (Standard_True, Loc);
4058 end if;
4060 Body_Stmts :=
4061 Make_Handled_Sequence_Of_Statements (Loc,
4062 Statements => New_List (
4063 Make_Simple_Return_Statement (Loc, Return_Expr)));
4065 Helper_Body :=
4066 Make_Subprogram_Body (Loc,
4067 Specification => Body_Spec,
4068 Declarations => New_List,
4069 Handled_Statement_Sequence => Body_Stmts);
4071 return Helper_Body;
4072 end Build_Call_Helper_Body;
4074 ----------------------------
4075 -- Build_Call_Helper_Decl --
4076 ----------------------------
4078 function Build_Call_Helper_Decl return Node_Id is
4079 Decl : Node_Id;
4080 Spec : Node_Id;
4082 begin
4083 Spec := Build_Call_Helper_Spec (Helper_Id);
4084 Set_Must_Override (Spec, False);
4085 Set_Must_Not_Override (Spec, False);
4086 Set_Is_Inlined (Helper_Id);
4087 Set_Is_Public (Helper_Id);
4089 Decl := Make_Subprogram_Declaration (Loc, Spec);
4091 -- Inherit debug info flag from Subp_Id to Helper_Id to allow
4092 -- debugging of the helper subprogram.
4094 if Needs_Debug_Info (Subp_Id) then
4095 Set_Debug_Info_Needed (Helper_Id);
4096 end if;
4098 return Decl;
4099 end Build_Call_Helper_Decl;
4101 ----------------------------
4102 -- Build_Call_Helper_Spec --
4103 ----------------------------
4105 function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id
4107 Spec : constant Node_Id := Parent (Subp_Id);
4108 Def_Id : constant Node_Id := Defining_Unit_Name (Spec);
4109 Formal : Entity_Id;
4110 Func_Formals : constant List_Id := New_List;
4111 P_Spec : constant List_Id := Parameter_Specifications (Spec);
4112 Par_Formal : Node_Id;
4113 Param : Node_Id;
4114 Param_Type : Node_Id;
4116 begin
4117 -- Create a list of formal parameters with the same types as the
4118 -- original subprogram but changing the controlling formal.
4120 Param := First (P_Spec);
4121 Formal := First_Formal (Def_Id);
4122 while Present (Formal) loop
4123 Par_Formal := Parent (Formal);
4125 if Is_Dynamic and then Is_Controlling_Formal (Formal) then
4126 if Nkind (Parameter_Type (Par_Formal))
4127 = N_Access_Definition
4128 then
4129 Param_Type :=
4130 Copy_Separate_Tree (Parameter_Type (Par_Formal));
4131 Rewrite (Subtype_Mark (Param_Type),
4132 Make_Attribute_Reference (Loc,
4133 Prefix => Relocate_Node (Subtype_Mark (Param_Type)),
4134 Attribute_Name => Name_Class));
4136 else
4137 Param_Type :=
4138 Make_Attribute_Reference (Loc,
4139 Prefix => New_Occurrence_Of (Etype (Formal), Loc),
4140 Attribute_Name => Name_Class);
4141 end if;
4142 else
4143 Param_Type := New_Occurrence_Of (Etype (Formal), Loc);
4144 end if;
4146 Append_To (Func_Formals,
4147 Make_Parameter_Specification (Loc,
4148 Defining_Identifier =>
4149 Make_Defining_Identifier (Loc, Chars (Formal)),
4150 In_Present => In_Present (Par_Formal),
4151 Out_Present => Out_Present (Par_Formal),
4152 Null_Exclusion_Present => Null_Exclusion_Present
4153 (Par_Formal),
4154 Parameter_Type => Param_Type));
4156 Next (Param);
4157 Next_Formal (Formal);
4158 end loop;
4160 return
4161 Make_Function_Specification (Loc,
4162 Defining_Unit_Name => Spec_Id,
4163 Parameter_Specifications => Func_Formals,
4164 Result_Definition =>
4165 New_Occurrence_Of (Standard_Boolean, Loc));
4166 end Build_Call_Helper_Spec;
4168 -- Local variables
4170 Helper_Body : Node_Id;
4171 Helper_Decl : Node_Id;
4173 -- Start of processing for Add_Call_Helper
4175 begin
4176 Helper_Decl := Build_Call_Helper_Decl;
4177 Mutate_Ekind (Helper_Id, Ekind (Subp_Id));
4179 -- Add the helper to the freezing actions of the tagged type
4181 Append_Freeze_Action (Tagged_Type, Helper_Decl);
4182 Analyze (Helper_Decl);
4184 Helper_Body := Build_Call_Helper_Body;
4185 Append_Freeze_Action (Tagged_Type, Helper_Body);
4187 -- If this helper is built as part of building the DTW at the
4188 -- freezing point of its tagged type then we cannot defer
4189 -- its analysis.
4191 if Late_Overriding then
4192 pragma Assert (Is_Dispatch_Table_Wrapper (Subp_Id));
4193 Analyze (Helper_Body);
4194 end if;
4195 end Add_Call_Helper;
4197 -----------------------
4198 -- Build_Unique_Name --
4199 -----------------------
4201 function Build_Unique_Name (Suffix : String) return Name_Id is
4202 begin
4203 -- Append the homonym number. Strip the leading space character in
4204 -- the image of natural numbers. Also do not add the homonym value
4205 -- of 1.
4207 if Has_Homonym (Subp_Id) and then Homonym_Number (Subp_Id) > 1 then
4208 declare
4209 S : constant String := Homonym_Number (Subp_Id)'Img;
4211 begin
4212 return New_External_Name (Chars (Subp_Id),
4213 Suffix => Suffix & "_" & S (2 .. S'Last));
4214 end;
4215 end if;
4217 return New_External_Name (Chars (Subp_Id), Suffix);
4218 end Build_Unique_Name;
4220 -- Local variables
4222 Helper_Id : Entity_Id;
4224 -- Start of processing for Make_Class_Precondition_Subps
4226 begin
4227 if Present (Class_Preconditions (Subp_Id))
4228 or Present (Ignored_Class_Preconditions (Subp_Id))
4229 then
4230 pragma Assert
4231 (Comes_From_Source (Subp_Id)
4232 or else Is_Dispatch_Table_Wrapper (Subp_Id));
4234 if No (Dynamic_Call_Helper (Subp_Id)) then
4236 -- Build and add to the freezing actions of Tagged_Type its
4237 -- dynamic-call helper.
4239 Helper_Id :=
4240 Make_Defining_Identifier (Loc,
4241 Build_Unique_Name (Suffix => "DP"));
4242 Add_Call_Helper (Helper_Id, Is_Dynamic => True);
4244 -- Link original subprogram to helper and vice versa
4246 Set_Dynamic_Call_Helper (Subp_Id, Helper_Id);
4247 Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
4248 end if;
4250 if not Is_Abstract_Subprogram (Subp_Id)
4251 and then No (Static_Call_Helper (Subp_Id))
4252 then
4253 -- Build and add to the freezing actions of Tagged_Type its
4254 -- static-call helper.
4256 Helper_Id :=
4257 Make_Defining_Identifier (Loc,
4258 Build_Unique_Name (Suffix => "SP"));
4260 Add_Call_Helper (Helper_Id, Is_Dynamic => False);
4262 -- Link original subprogram to helper and vice versa
4264 Set_Static_Call_Helper (Subp_Id, Helper_Id);
4265 Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
4267 -- Build and add to the freezing actions of Tagged_Type the
4268 -- indirect-call wrapper.
4270 Add_Indirect_Call_Wrapper;
4271 end if;
4272 end if;
4273 end Make_Class_Precondition_Subps;
4275 ----------------------------------------------
4276 -- Process_Class_Conditions_At_Freeze_Point --
4277 ----------------------------------------------
4279 procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id) is
4281 procedure Check_Class_Conditions (Spec_Id : Entity_Id);
4282 -- Check class-wide pre/postconditions of Spec_Id
4284 function Has_Class_Postconditions_Subprogram
4285 (Spec_Id : Entity_Id) return Boolean;
4286 -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
4288 function Has_Class_Preconditions_Subprogram
4289 (Spec_Id : Entity_Id) return Boolean;
4290 -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
4292 ----------------------------
4293 -- Check_Class_Conditions --
4294 ----------------------------
4296 procedure Check_Class_Conditions (Spec_Id : Entity_Id) is
4297 Par_Subp : Entity_Id;
4299 begin
4300 for Kind in Condition_Kind loop
4301 Par_Subp := Nearest_Class_Condition_Subprogram (Kind, Spec_Id);
4303 if Present (Par_Subp) then
4304 Check_Class_Condition
4305 (Cond => Class_Condition (Kind, Par_Subp),
4306 Subp => Spec_Id,
4307 Par_Subp => Par_Subp,
4308 Is_Precondition => Kind in Ignored_Class_Precondition
4309 | Class_Precondition);
4310 end if;
4311 end loop;
4312 end Check_Class_Conditions;
4314 -----------------------------------------
4315 -- Has_Class_Postconditions_Subprogram --
4316 -----------------------------------------
4318 function Has_Class_Postconditions_Subprogram
4319 (Spec_Id : Entity_Id) return Boolean is
4320 begin
4321 return
4322 Present (Nearest_Class_Condition_Subprogram
4323 (Spec_Id => Spec_Id,
4324 Kind => Class_Postcondition))
4325 or else
4326 Present (Nearest_Class_Condition_Subprogram
4327 (Spec_Id => Spec_Id,
4328 Kind => Ignored_Class_Postcondition));
4329 end Has_Class_Postconditions_Subprogram;
4331 ----------------------------------------
4332 -- Has_Class_Preconditions_Subprogram --
4333 ----------------------------------------
4335 function Has_Class_Preconditions_Subprogram
4336 (Spec_Id : Entity_Id) return Boolean is
4337 begin
4338 return
4339 Present (Nearest_Class_Condition_Subprogram
4340 (Spec_Id => Spec_Id,
4341 Kind => Class_Precondition))
4342 or else
4343 Present (Nearest_Class_Condition_Subprogram
4344 (Spec_Id => Spec_Id,
4345 Kind => Ignored_Class_Precondition));
4346 end Has_Class_Preconditions_Subprogram;
4348 -- Local variables
4350 Prim_Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ));
4351 Prim : Entity_Id;
4353 -- Start of processing for Process_Class_Conditions_At_Freeze_Point
4355 begin
4356 while Present (Prim_Elmt) loop
4357 Prim := Node (Prim_Elmt);
4359 if Has_Class_Preconditions_Subprogram (Prim)
4360 or else Has_Class_Postconditions_Subprogram (Prim)
4361 then
4362 if Comes_From_Source (Prim) then
4363 if Has_Significant_Contract (Prim) then
4364 Merge_Class_Conditions (Prim);
4365 end if;
4367 -- Handle wrapper of protected operation
4369 elsif Is_Primitive_Wrapper (Prim) then
4370 Merge_Class_Conditions (Prim);
4372 -- Check inherited class-wide conditions, excluding internal
4373 -- entities built for mapping of interface primitives.
4375 elsif Is_Derived_Type (Typ)
4376 and then Present (Alias (Prim))
4377 and then No (Interface_Alias (Prim))
4378 then
4379 Check_Class_Conditions (Prim);
4380 end if;
4381 end if;
4383 Next_Elmt (Prim_Elmt);
4384 end loop;
4385 end Process_Class_Conditions_At_Freeze_Point;
4387 ----------------------------
4388 -- Merge_Class_Conditions --
4389 ----------------------------
4391 procedure Merge_Class_Conditions (Spec_Id : Entity_Id) is
4393 procedure Process_Inherited_Conditions (Kind : Condition_Kind);
4394 -- Collect all inherited class-wide conditions of Spec_Id and merge
4395 -- them into one big condition.
4397 ----------------------------------
4398 -- Process_Inherited_Conditions --
4399 ----------------------------------
4401 procedure Process_Inherited_Conditions (Kind : Condition_Kind) is
4402 Tag_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id);
4403 Subps : constant Subprogram_List := Inherited_Subprograms (Spec_Id);
4404 Seen : Subprogram_List (Subps'Range) := (others => Empty);
4406 function Inherit_Condition
4407 (Par_Subp : Entity_Id;
4408 Subp : Entity_Id) return Node_Id;
4409 -- Inherit the class-wide condition from Par_Subp to Subp and adjust
4410 -- all the references to formals in the inherited condition.
4412 procedure Merge_Conditions (From : Node_Id; Into : Node_Id);
4413 -- Merge two class-wide preconditions or postconditions (the former
4414 -- are merged using "or else", and the latter are merged using "and-
4415 -- then"). The changes are accumulated in parameter Into.
4417 function Seen_Subp (Id : Entity_Id) return Boolean;
4418 -- Return True if the contract of subprogram Id has been processed
4420 -----------------------
4421 -- Inherit_Condition --
4422 -----------------------
4424 function Inherit_Condition
4425 (Par_Subp : Entity_Id;
4426 Subp : Entity_Id) return Node_Id
4428 function Check_Condition (Expr : Node_Id) return Boolean;
4429 -- Used in assertion to check that Expr has no reference to the
4430 -- formals of Par_Subp.
4432 ---------------------
4433 -- Check_Condition --
4434 ---------------------
4436 function Check_Condition (Expr : Node_Id) return Boolean is
4437 Par_Formal_Id : Entity_Id;
4439 function Check_Entity (N : Node_Id) return Traverse_Result;
4440 -- Check occurrence of Par_Formal_Id
4442 ------------------
4443 -- Check_Entity --
4444 ------------------
4446 function Check_Entity (N : Node_Id) return Traverse_Result is
4447 begin
4448 if Nkind (N) = N_Identifier
4449 and then Present (Entity (N))
4450 and then Entity (N) = Par_Formal_Id
4451 then
4452 return Abandon;
4453 end if;
4455 return OK;
4456 end Check_Entity;
4458 function Check_Expression is new Traverse_Func (Check_Entity);
4460 -- Start of processing for Check_Condition
4462 begin
4463 Par_Formal_Id := First_Formal (Par_Subp);
4465 while Present (Par_Formal_Id) loop
4466 if Check_Expression (Expr) = Abandon then
4467 return False;
4468 end if;
4470 Next_Formal (Par_Formal_Id);
4471 end loop;
4473 return True;
4474 end Check_Condition;
4476 -- Local variables
4478 Assoc_List : constant Elist_Id := New_Elmt_List;
4479 Par_Formal_Id : Entity_Id := First_Formal (Par_Subp);
4480 Subp_Formal_Id : Entity_Id := First_Formal (Subp);
4481 New_Condition : Node_Id;
4483 begin
4484 while Present (Par_Formal_Id) loop
4485 Append_Elmt (Par_Formal_Id, Assoc_List);
4486 Append_Elmt (Subp_Formal_Id, Assoc_List);
4488 Next_Formal (Par_Formal_Id);
4489 Next_Formal (Subp_Formal_Id);
4490 end loop;
4492 -- Check that Parent field of all the nodes have their correct
4493 -- decoration; required because otherwise mapped nodes with
4494 -- wrong Parent field are left unmodified in the copied tree
4495 -- and cause reporting wrong errors at later stages.
4497 pragma Assert
4498 (Check_Parents (Class_Condition (Kind, Par_Subp), Assoc_List));
4500 New_Condition :=
4501 New_Copy_Tree
4502 (Source => Class_Condition (Kind, Par_Subp),
4503 Map => Assoc_List);
4505 -- Ensure that the inherited condition has no reference to the
4506 -- formals of the parent subprogram.
4508 pragma Assert (Check_Condition (New_Condition));
4510 return New_Condition;
4511 end Inherit_Condition;
4513 ----------------------
4514 -- Merge_Conditions --
4515 ----------------------
4517 procedure Merge_Conditions (From : Node_Id; Into : Node_Id) is
4518 function Expression_Arg (Expr : Node_Id) return Node_Id;
4519 -- Return the boolean expression argument of a condition while
4520 -- updating its parentheses count for the subsequent merge.
4522 --------------------
4523 -- Expression_Arg --
4524 --------------------
4526 function Expression_Arg (Expr : Node_Id) return Node_Id is
4527 begin
4528 if Paren_Count (Expr) = 0 then
4529 Set_Paren_Count (Expr, 1);
4530 end if;
4532 return Expr;
4533 end Expression_Arg;
4535 -- Local variables
4537 From_Expr : constant Node_Id := Expression_Arg (From);
4538 Into_Expr : constant Node_Id := Expression_Arg (Into);
4539 Loc : constant Source_Ptr := Sloc (Into);
4541 -- Start of processing for Merge_Conditions
4543 begin
4544 case Kind is
4546 -- Merge the two preconditions by "or else"-ing them
4548 when Ignored_Class_Precondition
4549 | Class_Precondition
4551 Rewrite (Into_Expr,
4552 Make_Or_Else (Loc,
4553 Right_Opnd => Relocate_Node (Into_Expr),
4554 Left_Opnd => From_Expr));
4556 -- Merge the two postconditions by "and then"-ing them
4558 when Ignored_Class_Postcondition
4559 | Class_Postcondition
4561 Rewrite (Into_Expr,
4562 Make_And_Then (Loc,
4563 Right_Opnd => Relocate_Node (Into_Expr),
4564 Left_Opnd => From_Expr));
4565 end case;
4566 end Merge_Conditions;
4568 ---------------
4569 -- Seen_Subp --
4570 ---------------
4572 function Seen_Subp (Id : Entity_Id) return Boolean is
4573 begin
4574 for Index in Seen'Range loop
4575 if Seen (Index) = Id then
4576 return True;
4577 end if;
4578 end loop;
4580 return False;
4581 end Seen_Subp;
4583 -- Local variables
4585 Class_Cond : Node_Id;
4586 Cond : Node_Id;
4587 Subp_Id : Entity_Id;
4588 Par_Prim : Entity_Id := Empty;
4589 Par_Iface_Prims : Elist_Id := No_Elist;
4591 -- Start of processing for Process_Inherited_Conditions
4593 begin
4594 Class_Cond := Class_Condition (Kind, Spec_Id);
4596 -- Process parent primitives looking for nearest ancestor with
4597 -- class-wide conditions.
4599 for Index in Subps'Range loop
4600 Subp_Id := Subps (Index);
4602 if No (Par_Prim)
4603 and then Is_Ancestor (Find_Dispatching_Type (Subp_Id), Tag_Typ)
4604 then
4605 if Present (Alias (Subp_Id)) then
4606 Subp_Id := Ultimate_Alias (Subp_Id);
4607 end if;
4609 -- Wrappers of class-wide pre/postconditions reference the
4610 -- parent primitive that has the inherited contract and help
4611 -- us to climb fast.
4613 if Is_Wrapper (Subp_Id)
4614 and then Present (LSP_Subprogram (Subp_Id))
4615 then
4616 Subp_Id := LSP_Subprogram (Subp_Id);
4617 end if;
4619 if not Seen_Subp (Subp_Id)
4620 and then Present (Class_Condition (Kind, Subp_Id))
4621 then
4622 Seen (Index) := Subp_Id;
4623 Par_Prim := Subp_Id;
4624 Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim);
4626 Cond := Inherit_Condition
4627 (Subp => Spec_Id,
4628 Par_Subp => Subp_Id);
4630 if Present (Class_Cond) then
4631 Merge_Conditions (Cond, Class_Cond);
4632 else
4633 Class_Cond := Cond;
4634 end if;
4636 Check_Class_Condition
4637 (Cond => Class_Cond,
4638 Subp => Spec_Id,
4639 Par_Subp => Subp_Id,
4640 Is_Precondition => Kind in Ignored_Class_Precondition
4641 | Class_Precondition);
4642 Build_Class_Wide_Expression
4643 (Pragma_Or_Expr => Class_Cond,
4644 Subp => Spec_Id,
4645 Par_Subp => Subp_Id,
4646 Adjust_Sloc => False);
4648 -- We are done as soon as we process the nearest ancestor
4650 exit;
4651 end if;
4652 end if;
4653 end loop;
4655 -- Process the contract of interface primitives not covered by
4656 -- the nearest ancestor.
4658 for Index in Subps'Range loop
4659 Subp_Id := Subps (Index);
4661 if Is_Interface (Find_Dispatching_Type (Subp_Id)) then
4662 if Present (Alias (Subp_Id)) then
4663 Subp_Id := Ultimate_Alias (Subp_Id);
4664 end if;
4666 if not Seen_Subp (Subp_Id)
4667 and then Present (Class_Condition (Kind, Subp_Id))
4668 and then not Contains (Par_Iface_Prims, Subp_Id)
4669 then
4670 Seen (Index) := Subp_Id;
4672 Cond := Inherit_Condition
4673 (Subp => Spec_Id,
4674 Par_Subp => Subp_Id);
4676 Check_Class_Condition
4677 (Cond => Cond,
4678 Subp => Spec_Id,
4679 Par_Subp => Subp_Id,
4680 Is_Precondition => Kind in Ignored_Class_Precondition
4681 | Class_Precondition);
4682 Build_Class_Wide_Expression
4683 (Pragma_Or_Expr => Cond,
4684 Subp => Spec_Id,
4685 Par_Subp => Subp_Id,
4686 Adjust_Sloc => False);
4688 if Present (Class_Cond) then
4689 Merge_Conditions (Cond, Class_Cond);
4690 else
4691 Class_Cond := Cond;
4692 end if;
4693 end if;
4694 end if;
4695 end loop;
4697 Set_Class_Condition (Kind, Spec_Id, Class_Cond);
4698 end Process_Inherited_Conditions;
4700 -- Local variables
4702 Cond : Node_Id;
4704 -- Start of processing for Merge_Class_Conditions
4706 begin
4707 for Kind in Condition_Kind loop
4708 Cond := Class_Condition (Kind, Spec_Id);
4710 -- If this subprogram has class-wide conditions then preanalyze
4711 -- them before processing inherited conditions since conditions
4712 -- are checked and merged from right to left.
4714 if Present (Cond) then
4715 Preanalyze_Condition (Spec_Id, Cond);
4716 end if;
4718 Process_Inherited_Conditions (Kind);
4720 -- Preanalyze merged inherited conditions
4722 if Cond /= Class_Condition (Kind, Spec_Id) then
4723 Preanalyze_Condition (Spec_Id,
4724 Class_Condition (Kind, Spec_Id));
4725 end if;
4726 end loop;
4727 end Merge_Class_Conditions;
4729 ---------------------------------
4730 -- Preanalyze_Class_Conditions --
4731 ---------------------------------
4733 procedure Preanalyze_Class_Conditions (Spec_Id : Entity_Id) is
4734 Cond : Node_Id;
4736 begin
4737 for Kind in Condition_Kind loop
4738 Cond := Class_Condition (Kind, Spec_Id);
4740 if Present (Cond) then
4741 Preanalyze_Condition (Spec_Id, Cond);
4742 end if;
4743 end loop;
4744 end Preanalyze_Class_Conditions;
4746 --------------------------
4747 -- Preanalyze_Condition --
4748 --------------------------
4750 procedure Preanalyze_Condition
4751 (Subp : Entity_Id;
4752 Expr : Node_Id)
4754 procedure Clear_Unset_References;
4755 -- Clear unset references on formals of Subp since preanalysis
4756 -- occurs in a place unrelated to the actual code.
4758 procedure Remove_Controlling_Arguments;
4759 -- Traverse Expr and clear the Controlling_Argument of calls to
4760 -- nonabstract functions.
4762 procedure Restore_Original_Selected_Component;
4763 -- Traverse Expr searching for dispatching calls to functions whose
4764 -- original node was a selected component, and replace them with
4765 -- their original node.
4767 ----------------------------
4768 -- Clear_Unset_References --
4769 ----------------------------
4771 procedure Clear_Unset_References is
4772 F : Entity_Id := First_Formal (Subp);
4774 begin
4775 while Present (F) loop
4776 Set_Unset_Reference (F, Empty);
4777 Next_Formal (F);
4778 end loop;
4779 end Clear_Unset_References;
4781 ----------------------------------
4782 -- Remove_Controlling_Arguments --
4783 ----------------------------------
4785 procedure Remove_Controlling_Arguments is
4786 function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result;
4787 -- Reset the Controlling_Argument of calls to nonabstract
4788 -- function calls.
4790 ---------------------
4791 -- Remove_Ctrl_Arg --
4792 ---------------------
4794 function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result is
4795 begin
4796 if Nkind (N) = N_Function_Call
4797 and then Present (Controlling_Argument (N))
4798 and then not Is_Abstract_Subprogram (Entity (Name (N)))
4799 then
4800 Set_Controlling_Argument (N, Empty);
4801 end if;
4803 return OK;
4804 end Remove_Ctrl_Arg;
4806 procedure Remove_Ctrl_Args is new Traverse_Proc (Remove_Ctrl_Arg);
4807 begin
4808 Remove_Ctrl_Args (Expr);
4809 end Remove_Controlling_Arguments;
4811 -----------------------------------------
4812 -- Restore_Original_Selected_Component --
4813 -----------------------------------------
4815 procedure Restore_Original_Selected_Component is
4816 Restored_Nodes_List : Elist_Id := No_Elist;
4818 procedure Fix_Parents (N : Node_Id);
4819 -- Traverse the subtree of N fixing the Parent field of all the
4820 -- nodes.
4822 function Restore_Node (N : Node_Id) return Traverse_Result;
4823 -- Process dispatching calls to functions whose original node was
4824 -- a selected component, and replace them with their original
4825 -- node. Restored nodes are stored in the Restored_Nodes_List
4826 -- to fix the parent fields of their subtrees in a separate
4827 -- tree traversal.
4829 -----------------
4830 -- Fix_Parents --
4831 -----------------
4833 procedure Fix_Parents (N : Node_Id) is
4835 function Fix_Parent
4836 (Parent_Node : Node_Id;
4837 Node : Node_Id) return Traverse_Result;
4838 -- Process a single node
4840 ----------------
4841 -- Fix_Parent --
4842 ----------------
4844 function Fix_Parent
4845 (Parent_Node : Node_Id;
4846 Node : Node_Id) return Traverse_Result
4848 Par : constant Node_Id := Parent (Node);
4850 begin
4851 if Par /= Parent_Node then
4852 if Is_List_Member (Node) then
4853 Set_List_Parent (List_Containing (Node), Parent_Node);
4854 else
4855 Set_Parent (Node, Parent_Node);
4856 end if;
4857 end if;
4859 return OK;
4860 end Fix_Parent;
4862 procedure Fix_Parents is
4863 new Traverse_Proc_With_Parent (Fix_Parent);
4865 begin
4866 Fix_Parents (N);
4867 end Fix_Parents;
4869 ------------------
4870 -- Restore_Node --
4871 ------------------
4873 function Restore_Node (N : Node_Id) return Traverse_Result is
4874 begin
4875 if Nkind (N) = N_Function_Call
4876 and then Nkind (Original_Node (N)) = N_Selected_Component
4877 and then Is_Dispatching_Operation (Entity (Name (N)))
4878 then
4879 Rewrite (N, Original_Node (N));
4880 Set_Original_Node (N, N);
4882 -- Save the restored node in the Restored_Nodes_List to fix
4883 -- the parent fields of their subtrees in a separate tree
4884 -- traversal.
4886 Append_New_Elmt (N, Restored_Nodes_List);
4887 end if;
4889 return OK;
4890 end Restore_Node;
4892 procedure Restore_Nodes is new Traverse_Proc (Restore_Node);
4894 -- Start of processing for Restore_Original_Selected_Component
4896 begin
4897 Restore_Nodes (Expr);
4899 -- After restoring the original node we must fix the decoration
4900 -- of the Parent attribute to ensure tree consistency; required
4901 -- because when the class-wide condition is inherited, calls to
4902 -- New_Copy_Tree will perform copies of this subtree, and formal
4903 -- occurrences with wrong Parent field cannot be mapped to the
4904 -- new formals.
4906 if Present (Restored_Nodes_List) then
4907 declare
4908 Elmt : Elmt_Id := First_Elmt (Restored_Nodes_List);
4910 begin
4911 while Present (Elmt) loop
4912 Fix_Parents (Node (Elmt));
4913 Next_Elmt (Elmt);
4914 end loop;
4915 end;
4916 end if;
4917 end Restore_Original_Selected_Component;
4919 -- Start of processing for Preanalyze_Condition
4921 begin
4922 pragma Assert (Present (Expr));
4923 pragma Assert (Inside_Class_Condition_Preanalysis = False);
4925 Push_Scope (Subp);
4926 Install_Formals (Subp);
4927 Inside_Class_Condition_Preanalysis := True;
4929 Preanalyze_Spec_Expression (Expr, Standard_Boolean);
4931 Inside_Class_Condition_Preanalysis := False;
4932 End_Scope;
4934 -- If this preanalyzed condition has occurrences of dispatching calls
4935 -- using the Object.Operation notation, during preanalysis such calls
4936 -- are rewritten as dispatching function calls; if at later stages
4937 -- this condition is inherited we must have restored the original
4938 -- selected-component node to ensure that the preanalysis of the
4939 -- inherited condition rewrites these dispatching calls in the
4940 -- correct context to avoid reporting spurious errors.
4942 Restore_Original_Selected_Component;
4944 -- Traverse Expr and clear the Controlling_Argument of calls to
4945 -- nonabstract functions. Required since the preanalyzed condition
4946 -- is not yet installed on its definite context and will be cloned
4947 -- and extended in derivations with additional conditions.
4949 Remove_Controlling_Arguments;
4951 -- Clear also attribute Unset_Reference; again because preanalysis
4952 -- occurs in a place unrelated to the actual code.
4954 Clear_Unset_References;
4955 end Preanalyze_Condition;
4957 ----------------------------------------
4958 -- Save_Global_References_In_Contract --
4959 ----------------------------------------
4961 procedure Save_Global_References_In_Contract
4962 (Templ : Node_Id;
4963 Gen_Id : Entity_Id)
4965 procedure Save_Global_References_In_List (First_Prag : Node_Id);
4966 -- Save all global references in contract-related source pragmas found
4967 -- in the list, starting with pragma First_Prag.
4969 ------------------------------------
4970 -- Save_Global_References_In_List --
4971 ------------------------------------
4973 procedure Save_Global_References_In_List (First_Prag : Node_Id) is
4974 Prag : Node_Id := First_Prag;
4976 begin
4977 while Present (Prag) loop
4978 if Is_Generic_Contract_Pragma (Prag) then
4979 Save_Global_References (Prag);
4980 end if;
4982 Prag := Next_Pragma (Prag);
4983 end loop;
4984 end Save_Global_References_In_List;
4986 -- Local variables
4988 Items : constant Node_Id := Contract (Defining_Entity (Templ));
4990 -- Start of processing for Save_Global_References_In_Contract
4992 begin
4993 -- The entity of the analyzed generic copy must be on the scope stack
4994 -- to ensure proper detection of global references.
4996 Push_Scope (Gen_Id);
4998 if Permits_Aspect_Specifications (Templ)
4999 and then Has_Aspects (Templ)
5000 then
5001 Save_Global_References_In_Aspects (Templ);
5002 end if;
5004 if Present (Items) then
5005 Save_Global_References_In_List (Pre_Post_Conditions (Items));
5006 Save_Global_References_In_List (Contract_Test_Cases (Items));
5007 Save_Global_References_In_List (Classifications (Items));
5008 end if;
5010 Pop_Scope;
5011 end Save_Global_References_In_Contract;
5013 -------------------------
5014 -- Set_Class_Condition --
5015 -------------------------
5017 procedure Set_Class_Condition
5018 (Kind : Condition_Kind;
5019 Subp : Entity_Id;
5020 Cond : Node_Id)
5022 begin
5023 case Kind is
5024 when Class_Postcondition =>
5025 Set_Class_Postconditions (Subp, Cond);
5027 when Class_Precondition =>
5028 Set_Class_Preconditions (Subp, Cond);
5030 when Ignored_Class_Postcondition =>
5031 Set_Ignored_Class_Postconditions (Subp, Cond);
5033 when Ignored_Class_Precondition =>
5034 Set_Ignored_Class_Preconditions (Subp, Cond);
5035 end case;
5036 end Set_Class_Condition;
5038 end Contracts;