1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- C O N T R A C T S --
9 -- Copyright (C) 2015-2023, Free Software Foundation, Inc. --
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. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
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;
38 with Namet; use Namet;
39 with Nlists; use Nlists;
40 with Nmake; use Nmake;
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:
77 procedure Build_Subprogram_Contract_Wrapper
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
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 Contract_Cases, Exceptional_Cases, Subprogram_Variant,
113 -- invariants and predicates. Body_Id denotes the entity of the
116 procedure Preanalyze_Condition
119 -- Preanalyze the class-wide condition Expr of Subp
121 procedure Set_Class_Condition
122 (Kind : Condition_Kind;
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
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
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
169 Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
170 Set_Pre_Post_Conditions (Items, Prag);
171 end Add_Pre_Post_Condition;
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
183 -- Create a new contract when adding the first item
186 Items := Make_Contract (Sloc (Id));
187 Set_Contract (Id, Items);
190 -- Constants, the applicable pragmas are:
193 if Ekind (Id) = E_Constant then
194 if Prag_Nam in Name_Async_Readers
196 | Name_Effective_Reads
197 | Name_Effective_Writes
203 -- The pragma is not a proper contract item
206 raise Contract_Error;
209 -- Entry bodies, the applicable pragmas are:
214 elsif Is_Entry_Body (Id) then
215 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then
218 elsif Prag_Nam = Name_Refined_Post then
219 Add_Pre_Post_Condition;
221 -- The pragma is not a proper contract item
224 raise Contract_Error;
227 -- Entry or subprogram declarations, the applicable pragmas are:
232 -- Extensions_Visible
237 -- Subprogram_Variant
241 elsif Is_Entry_Declaration (Id)
242 or else Ekind (Id) in E_Function
244 | E_Generic_Procedure
247 if Prag_Nam in Name_Attach_Handler | Name_Interrupt_Handler
248 and then Ekind (Id) in E_Generic_Procedure | E_Procedure
252 elsif Prag_Nam in Name_Depends
253 | Name_Extensions_Visible
258 elsif Prag_Nam = Name_Volatile_Function
259 and then Ekind (Id) in E_Function | E_Generic_Function
263 elsif Prag_Nam in Name_Contract_Cases
264 | Name_Exceptional_Cases
265 | Name_Subprogram_Variant
268 Add_Contract_Test_Case;
270 elsif Prag_Nam in Name_Postcondition | Name_Precondition then
271 Add_Pre_Post_Condition;
273 -- The pragma is not a proper contract item
276 raise Contract_Error;
279 -- Packages or instantiations, the applicable pragmas are:
283 -- Part_Of (instantiation only)
285 elsif Is_Package_Or_Generic_Package (Id) then
286 if Prag_Nam in Name_Abstract_State
287 | Name_Initial_Condition
292 -- Indicator Part_Of must be associated with a package instantiation
294 elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
297 -- The pragma is not a proper contract item
300 raise Contract_Error;
303 -- Package bodies, the applicable pragmas are:
306 elsif Ekind (Id) = E_Package_Body then
307 if Prag_Nam = Name_Refined_State then
310 -- The pragma is not a proper contract item
313 raise Contract_Error;
316 -- The four volatility refinement pragmas are ok for all types.
317 -- Part_Of is ok for task types and protected types.
318 -- Depends and Global are ok for task types.
320 -- Precondition and Postcondition are added separately; they are allowed
321 -- for access-to-subprogram types.
323 elsif Is_Type (Id) then
325 Is_OK_Classification : constant Boolean :=
326 Prag_Nam in Name_Async_Readers
328 | Name_Effective_Reads
329 | Name_Effective_Writes
331 or else (Ekind (Id) = E_Task_Type
332 and Prag_Nam in Name_Part_Of
335 or else (Ekind (Id) = E_Protected_Type
336 and Prag_Nam = Name_Part_Of);
339 if Is_OK_Classification then
342 elsif Ekind (Id) = E_Subprogram_Type
343 and then Prag_Nam in Name_Precondition
346 Add_Pre_Post_Condition;
349 -- The pragma is not a proper contract item
351 raise Contract_Error;
355 -- Subprogram bodies, the applicable pragmas are:
362 elsif Ekind (Id) = E_Subprogram_Body then
363 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then
366 elsif Prag_Nam in Name_Postcondition
370 Add_Pre_Post_Condition;
372 -- The pragma is not a proper contract item
375 raise Contract_Error;
378 -- Task bodies, the applicable pragmas are:
382 elsif Ekind (Id) = E_Task_Body then
383 if Prag_Nam in Name_Refined_Depends | Name_Refined_Global then
386 -- The pragma is not a proper contract item
389 raise Contract_Error;
392 -- Task units, the applicable pragmas are:
397 -- Variables, the applicable pragmas are:
400 -- Constant_After_Elaboration
408 elsif Ekind (Id) = E_Variable then
409 if Prag_Nam in Name_Async_Readers
411 | Name_Constant_After_Elaboration
413 | Name_Effective_Reads
414 | Name_Effective_Writes
421 -- The pragma is not a proper contract item
424 raise Contract_Error;
428 raise Contract_Error;
430 end Add_Contract_Item;
432 -----------------------
433 -- Analyze_Contracts --
434 -----------------------
436 procedure Analyze_Contracts (L : List_Id) is
441 while Present (Decl) loop
443 -- Entry or subprogram declarations
445 if Nkind (Decl) in N_Abstract_Subprogram_Declaration
446 | N_Entry_Declaration
447 | N_Generic_Subprogram_Declaration
448 | N_Subprogram_Declaration
450 Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
452 -- Entry or subprogram bodies
454 elsif Nkind (Decl) in N_Entry_Body | N_Subprogram_Body then
455 Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl));
459 elsif Nkind (Decl) = N_Object_Declaration then
460 Analyze_Object_Contract (Defining_Entity (Decl));
462 -- Package instantiation
464 elsif Nkind (Decl) = N_Package_Instantiation then
465 Analyze_Package_Instantiation_Contract (Defining_Entity (Decl));
469 elsif Nkind (Decl) in N_Protected_Type_Declaration
470 | N_Single_Protected_Declaration
472 Analyze_Protected_Contract (Defining_Entity (Decl));
474 -- Subprogram body stubs
476 elsif Nkind (Decl) = N_Subprogram_Body_Stub then
477 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
481 elsif Nkind (Decl) in N_Single_Task_Declaration
482 | N_Task_Type_Declaration
484 Analyze_Task_Contract (Defining_Entity (Decl));
486 -- For type declarations, we need to do the preanalysis of Iterable
487 -- and the 3 Xxx_Literal aspect specifications.
489 -- Other type aspects need to be resolved here???
491 elsif Nkind (Decl) = N_Private_Type_Declaration
492 and then Present (Aspect_Specifications (Decl))
495 E : constant Entity_Id := Defining_Identifier (Decl);
496 It : constant Node_Id := Find_Aspect (E, Aspect_Iterable);
497 I_Lit : constant Node_Id :=
498 Find_Aspect (E, Aspect_Integer_Literal);
499 R_Lit : constant Node_Id :=
500 Find_Aspect (E, Aspect_Real_Literal);
501 S_Lit : constant Node_Id :=
502 Find_Aspect (E, Aspect_String_Literal);
506 Validate_Iterable_Aspect (E, It);
509 if Present (I_Lit) then
510 Validate_Literal_Aspect (E, I_Lit);
512 if Present (R_Lit) then
513 Validate_Literal_Aspect (E, R_Lit);
515 if Present (S_Lit) then
516 Validate_Literal_Aspect (E, S_Lit);
521 if Nkind (Decl) in N_Full_Type_Declaration
522 | N_Private_Type_Declaration
523 | N_Task_Type_Declaration
524 | N_Protected_Type_Declaration
525 | N_Formal_Type_Declaration
527 Analyze_Type_Contract (Defining_Identifier (Decl));
532 end Analyze_Contracts;
534 -------------------------------------
535 -- Analyze_Pragmas_In_Declarations --
536 -------------------------------------
538 procedure Analyze_Pragmas_In_Declarations (Body_Id : Entity_Id) is
542 -- Move through the body's declarations analyzing all pragmas which
543 -- appear at the top of the declarations.
545 Curr_Decl := First (Declarations (Unit_Declaration_Node (Body_Id)));
546 while Present (Curr_Decl) loop
548 if Nkind (Curr_Decl) = N_Pragma then
550 if Pragma_Significant_To_Subprograms
551 (Get_Pragma_Id (Curr_Decl))
556 -- Skip the renamings of discriminants and protection fields
558 elsif Is_Prologue_Renaming (Curr_Decl) then
561 -- We have reached something which is not a pragma so we can be sure
562 -- there are no more contracts or pragmas which need to be taken into
571 end Analyze_Pragmas_In_Declarations;
573 -----------------------------------------------
574 -- Analyze_Entry_Or_Subprogram_Body_Contract --
575 -----------------------------------------------
577 -- WARNING: This routine manages SPARK regions. Return statements must be
578 -- replaced by gotos which jump to the end of the routine and restore the
581 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
582 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
583 Items : constant Node_Id := Contract (Body_Id);
584 Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
586 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
587 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
588 -- Save the SPARK_Mode-related data to restore on exit
591 -- When a subprogram body declaration is illegal, its defining entity is
592 -- left unanalyzed. There is nothing left to do in this case because the
593 -- body lacks a contract, or even a proper Ekind.
595 if Ekind (Body_Id) = E_Void then
598 -- Do not analyze a contract multiple times
600 elsif Present (Items) then
601 if Analyzed (Items) then
604 Set_Analyzed (Items);
607 -- When this is a subprogram body not coming from source, for example an
608 -- expression function, it does not cause freezing of previous contracts
609 -- (see Analyze_Subprogram_Body_Helper), in particular not of those on
610 -- its spec if it exists. In this case make sure they have been properly
611 -- analyzed before being expanded below, as we may be invoked during the
612 -- freezing of the subprogram in the middle of its enclosing declarative
613 -- part because the declarative part contains e.g. the declaration of a
614 -- variable initialized by means of a call to the subprogram.
616 elsif Nkind (Body_Decl) = N_Subprogram_Body
617 and then not Comes_From_Source (Original_Node (Body_Decl))
618 and then Present (Corresponding_Spec (Body_Decl))
619 and then Present (Contract (Corresponding_Spec (Body_Decl)))
621 Analyze_Entry_Or_Subprogram_Contract (Corresponding_Spec (Body_Decl));
624 -- Due to the timing of contract analysis, delayed pragmas may be
625 -- subject to the wrong SPARK_Mode, usually that of the enclosing
626 -- context. To remedy this, restore the original SPARK_Mode of the
627 -- related subprogram body.
629 Set_SPARK_Mode (Body_Id);
631 -- Ensure that the contract cases or postconditions mention 'Result or
632 -- define a post-state.
634 Check_Result_And_Post_State (Body_Id);
636 -- A stand-alone nonvolatile function body cannot have an effectively
637 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
638 -- check is relevant only when SPARK_Mode is on, as it is not a standard
639 -- legality rule. The check is performed here because Volatile_Function
640 -- is processed after the analysis of the related subprogram body. The
641 -- check only applies to source subprograms and not to generated TSS
645 and then Ekind (Body_Id) in E_Function | E_Generic_Function
646 and then Comes_From_Source (Spec_Id)
647 and then not Is_Volatile_Function (Body_Id)
649 Check_Nonvolatile_Function_Profile (Body_Id);
652 -- Restore the SPARK_Mode of the enclosing context after all delayed
653 -- pragmas have been analyzed.
655 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
657 -- Capture all global references in a generic subprogram body now that
658 -- the contract has been analyzed.
660 if Is_Generic_Declaration_Or_Body (Body_Decl) then
661 Save_Global_References_In_Contract
662 (Templ => Original_Node (Body_Decl),
666 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
667 -- Exceptional_Cases, Subprogram_Variant, invariants and predicates
668 -- associated with body and its spec. Do not expand the contract of
669 -- subprogram body stubs.
671 if Nkind (Body_Decl) = N_Subprogram_Body then
672 Expand_Subprogram_Contract (Body_Id);
674 end Analyze_Entry_Or_Subprogram_Body_Contract;
676 ------------------------------------------
677 -- Analyze_Entry_Or_Subprogram_Contract --
678 ------------------------------------------
680 -- WARNING: This routine manages SPARK regions. Return statements must be
681 -- replaced by gotos which jump to the end of the routine and restore the
684 procedure Analyze_Entry_Or_Subprogram_Contract
685 (Subp_Id : Entity_Id;
686 Freeze_Id : Entity_Id := Empty)
688 Items : constant Node_Id := Contract (Subp_Id);
689 Subp_Decl : constant Node_Id :=
690 (if Ekind (Subp_Id) = E_Subprogram_Type
691 then Associated_Node_For_Itype (Subp_Id)
692 else Unit_Declaration_Node (Subp_Id));
694 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
695 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
696 -- Save the SPARK_Mode-related data to restore on exit
698 Skip_Assert_Exprs : constant Boolean :=
699 Is_Entry (Subp_Id) and then not GNATprove_Mode;
701 Depends : Node_Id := Empty;
702 Global : Node_Id := Empty;
707 -- Do not analyze a contract multiple times
709 if Present (Items) then
710 if Analyzed (Items) then
713 Set_Analyzed (Items);
717 -- Due to the timing of contract analysis, delayed pragmas may be
718 -- subject to the wrong SPARK_Mode, usually that of the enclosing
719 -- context. To remedy this, restore the original SPARK_Mode of the
720 -- related subprogram body.
722 Set_SPARK_Mode (Subp_Id);
724 -- All subprograms carry a contract, but for some it is not significant
725 -- and should not be processed.
727 if not Has_Significant_Contract (Subp_Id) then
730 elsif Present (Items) then
732 -- Do not analyze the pre/postconditions of an entry declaration
733 -- unless annotating the original tree for GNATprove. The
734 -- real analysis occurs when the pre/postconditons are relocated to
735 -- the contract wrapper procedure (see Build_Contract_Wrapper).
737 if Skip_Assert_Exprs then
740 -- Otherwise analyze the pre/postconditions.
741 -- If these come from an aspect specification, their expressions
742 -- might include references to types that are not frozen yet, in the
743 -- case where the body is a rewritten expression function that is a
744 -- completion, so freeze all types within before constructing the
749 Bod : Node_Id := Empty;
750 Freeze_Types : Boolean := False;
753 if Present (Freeze_Id) then
754 Bod := Unit_Declaration_Node (Freeze_Id);
756 if Nkind (Bod) = N_Subprogram_Body
757 and then Was_Expression_Function (Bod)
758 and then Ekind (Subp_Id) = E_Function
759 and then Chars (Subp_Id) = Chars (Freeze_Id)
760 and then Subp_Id /= Freeze_Id
762 Freeze_Types := True;
766 Prag := Pre_Post_Conditions (Items);
767 while Present (Prag) loop
769 and then Present (Corresponding_Aspect (Prag))
773 Typ => Standard_Boolean,
776 (First (Pragma_Argument_Associations (Prag))),
780 Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
781 Prag := Next_Pragma (Prag);
786 -- Analyze contract-cases, subprogram-variant and test-cases
788 Prag := Contract_Test_Cases (Items);
789 while Present (Prag) loop
790 Prag_Nam := Pragma_Name (Prag);
792 if Prag_Nam = Name_Contract_Cases then
794 -- Do not analyze the contract cases of an entry declaration
795 -- unless annotating the original tree for GNATprove.
796 -- The real analysis occurs when the contract cases are moved
797 -- to the contract wrapper procedure (Build_Contract_Wrapper).
799 if Skip_Assert_Exprs then
802 -- Otherwise analyze the contract cases
805 Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
808 elsif Prag_Nam = Name_Exceptional_Cases then
809 Analyze_Exceptional_Cases_In_Decl_Part (Prag);
811 elsif Prag_Nam = Name_Subprogram_Variant then
812 Analyze_Subprogram_Variant_In_Decl_Part (Prag);
815 pragma Assert (Prag_Nam = Name_Test_Case);
816 Analyze_Test_Case_In_Decl_Part (Prag);
819 Prag := Next_Pragma (Prag);
822 -- Analyze classification pragmas
824 Prag := Classifications (Items);
825 while Present (Prag) loop
826 Prag_Nam := Pragma_Name (Prag);
828 if Prag_Nam = Name_Depends then
831 elsif Prag_Nam = Name_Global then
835 Prag := Next_Pragma (Prag);
838 -- Analyze Global first, as Depends may mention items classified in
839 -- the global categorization.
841 if Present (Global) then
842 Analyze_Global_In_Decl_Part (Global);
845 -- Depends must be analyzed after Global in order to see the modes of
848 if Present (Depends) then
849 Analyze_Depends_In_Decl_Part (Depends);
852 -- Ensure that the contract cases or postconditions mention 'Result
853 -- or define a post-state.
855 Check_Result_And_Post_State (Subp_Id);
858 -- A nonvolatile function cannot have an effectively volatile formal
859 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
860 -- only when SPARK_Mode is on, as it is not a standard legality rule.
861 -- The check is performed here because pragma Volatile_Function is
862 -- processed after the analysis of the related subprogram declaration.
865 and then Ekind (Subp_Id) in E_Function | E_Generic_Function
866 and then Comes_From_Source (Subp_Id)
867 and then not Is_Volatile_Function (Subp_Id)
869 Check_Nonvolatile_Function_Profile (Subp_Id);
872 -- Restore the SPARK_Mode of the enclosing context after all delayed
873 -- pragmas have been analyzed.
875 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
877 -- Capture all global references in a generic subprogram now that the
878 -- contract has been analyzed.
880 if Is_Generic_Declaration_Or_Body (Subp_Decl) then
881 Save_Global_References_In_Contract
882 (Templ => Original_Node (Subp_Decl),
885 end Analyze_Entry_Or_Subprogram_Contract;
887 ----------------------------------------------
888 -- Check_Type_Or_Object_External_Properties --
889 ----------------------------------------------
891 procedure Check_Type_Or_Object_External_Properties
892 (Type_Or_Obj_Id : Entity_Id)
894 Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id);
895 Decl_Kind : constant String :=
896 (if Is_Type_Id then "type" else "object");
900 AR_Val : Boolean := False;
901 AW_Val : Boolean := False;
902 ER_Val : Boolean := False;
903 EW_Val : Boolean := False;
905 Seen : Boolean := False;
909 -- Start of processing for Check_Type_Or_Object_External_Properties
912 -- Analyze all external properties
915 Obj_Typ := Type_Or_Obj_Id;
917 -- If the parent type of a derived type is volatile
918 -- then the derived type inherits volatility-related flags.
920 if Is_Derived_Type (Type_Or_Obj_Id) then
922 Parent_Type : constant Entity_Id :=
923 Etype (Base_Type (Type_Or_Obj_Id));
925 if Is_Effectively_Volatile (Parent_Type) then
926 AR_Val := Async_Readers_Enabled (Parent_Type);
927 AW_Val := Async_Writers_Enabled (Parent_Type);
928 ER_Val := Effective_Reads_Enabled (Parent_Type);
929 EW_Val := Effective_Writes_Enabled (Parent_Type);
934 Obj_Typ := Etype (Type_Or_Obj_Id);
937 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers);
939 if Present (Prag) then
941 Saved_AR_Val : constant Boolean := AR_Val;
943 Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
945 if Saved_AR_Val and not AR_Val then
947 ("illegal non-confirming Async_Readers specification",
953 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Writers);
955 if Present (Prag) then
957 Saved_AW_Val : constant Boolean := AW_Val;
959 Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
961 if Saved_AW_Val and not AW_Val then
963 ("illegal non-confirming Async_Writers specification",
969 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Reads);
971 if Present (Prag) then
973 Saved_ER_Val : constant Boolean := ER_Val;
975 Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
977 if Saved_ER_Val and not ER_Val then
979 ("illegal non-confirming Effective_Reads specification",
985 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Writes);
987 if Present (Prag) then
989 Saved_EW_Val : constant Boolean := EW_Val;
991 Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
993 if Saved_EW_Val and not EW_Val then
995 ("illegal non-confirming Effective_Writes specification",
1001 -- Verify the mutual interaction of the various external properties.
1002 -- For types and variables for which No_Caching is enabled, it has been
1003 -- checked already that only False values for other external properties
1007 and then not No_Caching_Enabled (Type_Or_Obj_Id)
1009 Check_External_Properties
1010 (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
1013 -- Analyze the non-external volatility property No_Caching
1015 Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching);
1017 if Present (Prag) then
1018 Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
1021 -- The following checks are relevant only when SPARK_Mode is on, as
1022 -- they are not standard Ada legality rules. Internally generated
1023 -- temporaries are ignored, as well as return objects.
1026 and then Comes_From_Source (Type_Or_Obj_Id)
1027 and then not Is_Return_Object (Type_Or_Obj_Id)
1029 if Is_Effectively_Volatile (Type_Or_Obj_Id) then
1031 -- The declaration of an effectively volatile object or type must
1032 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
1034 if not Is_Library_Level_Entity (Type_Or_Obj_Id) then
1036 ("effectively volatile "
1038 & " & must be declared at library level "
1039 & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id);
1041 -- An object of a discriminated type cannot be effectively
1042 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
1044 elsif Has_Discriminants (Obj_Typ)
1045 and then not Is_Protected_Type (Obj_Typ)
1048 ("discriminated " & Decl_Kind & " & cannot be volatile",
1052 -- An object decl shall be compatible with respect to volatility
1053 -- with its type (SPARK RM 7.1.3(2)).
1055 if not Is_Type_Id then
1056 if Is_Effectively_Volatile (Obj_Typ) then
1057 Check_Volatility_Compatibility
1058 (Type_Or_Obj_Id, Obj_Typ,
1059 "volatile object", "its type",
1060 Srcpos_Bearer => Type_Or_Obj_Id);
1063 -- A component of a composite type (in this case, the composite
1064 -- type is an array type) shall be compatible with respect to
1065 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1067 elsif Is_Array_Type (Obj_Typ) then
1068 Check_Volatility_Compatibility
1069 (Component_Type (Obj_Typ), Obj_Typ,
1070 "component type", "its enclosing array type",
1071 Srcpos_Bearer => Obj_Typ);
1073 -- A component of a composite type (in this case, the composite
1074 -- type is a record type) shall be compatible with respect to
1075 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1077 elsif Is_Record_Type (Obj_Typ) then
1079 Comp : Entity_Id := First_Component (Obj_Typ);
1081 while Present (Comp) loop
1082 Check_Volatility_Compatibility
1083 (Etype (Comp), Obj_Typ,
1084 "record component " & Get_Name_String (Chars (Comp)),
1085 "its enclosing record type",
1086 Srcpos_Bearer => Comp);
1087 Next_Component (Comp);
1092 -- The type or object is not effectively volatile
1095 -- A non-effectively volatile type cannot have effectively
1096 -- volatile components (SPARK RM 7.1.3(6)).
1099 and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
1100 and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id)
1103 ("non-volatile type & cannot have effectively volatile"
1109 end Check_Type_Or_Object_External_Properties;
1111 -----------------------------
1112 -- Analyze_Object_Contract --
1113 -----------------------------
1115 -- WARNING: This routine manages SPARK regions. Return statements must be
1116 -- replaced by gotos which jump to the end of the routine and restore the
1119 procedure Analyze_Object_Contract
1120 (Obj_Id : Entity_Id;
1121 Freeze_Id : Entity_Id := Empty)
1123 Obj_Typ : constant Entity_Id := Etype (Obj_Id);
1125 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1126 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1127 -- Save the SPARK_Mode-related data to restore on exit
1134 -- The loop parameter in an element iterator over a formal container
1135 -- is declared with an object declaration, but no contracts apply.
1137 if Ekind (Obj_Id) = E_Loop_Parameter then
1141 -- Do not analyze a contract multiple times
1143 Items := Contract (Obj_Id);
1145 if Present (Items) then
1146 if Analyzed (Items) then
1149 Set_Analyzed (Items);
1153 -- The anonymous object created for a single concurrent type inherits
1154 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
1155 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
1156 -- of the enclosing context. To remedy this, restore the original mode
1157 -- of the related anonymous object.
1159 if Is_Single_Concurrent_Object (Obj_Id)
1160 and then Present (SPARK_Pragma (Obj_Id))
1162 Set_SPARK_Mode (Obj_Id);
1165 -- Checks related to external properties, same for constants and
1168 Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id);
1170 -- Constant-related checks
1172 if Ekind (Obj_Id) = E_Constant then
1174 -- Analyze indicator Part_Of
1176 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
1178 -- Check whether the lack of indicator Part_Of agrees with the
1179 -- placement of the constant with respect to the state space.
1182 Check_Missing_Part_Of (Obj_Id);
1185 -- Variable-related checks
1187 else pragma Assert (Ekind (Obj_Id) = E_Variable);
1189 -- The anonymous object created for a single task type carries
1190 -- pragmas Depends and Global of the type.
1192 if Is_Single_Task_Object (Obj_Id) then
1194 -- Analyze Global first, as Depends may mention items classified
1195 -- in the global categorization.
1197 Prag := Get_Pragma (Obj_Id, Pragma_Global);
1199 if Present (Prag) then
1200 Analyze_Global_In_Decl_Part (Prag);
1203 -- Depends must be analyzed after Global in order to see the modes
1204 -- of all global items.
1206 Prag := Get_Pragma (Obj_Id, Pragma_Depends);
1208 if Present (Prag) then
1209 Analyze_Depends_In_Decl_Part (Prag);
1213 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
1215 -- Analyze indicator Part_Of
1217 if Present (Prag) then
1218 Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id);
1220 -- The variable is a constituent of a single protected/task type
1221 -- and behaves as a component of the type. Verify that references
1222 -- to the variable occur within the definition or body of the type
1225 if Present (Encapsulating_State (Obj_Id))
1226 and then Is_Single_Concurrent_Object
1227 (Encapsulating_State (Obj_Id))
1228 and then Present (Part_Of_References (Obj_Id))
1230 Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id));
1231 while Present (Ref_Elmt) loop
1232 Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt));
1233 Next_Elmt (Ref_Elmt);
1237 -- Otherwise check whether the lack of indicator Part_Of agrees with
1238 -- the placement of the variable with respect to the state space.
1241 Check_Missing_Part_Of (Obj_Id);
1247 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
1249 -- A Ghost object cannot be of a type that yields a synchronized
1250 -- object (SPARK RM 6.9(19)).
1252 if Yields_Synchronized_Object (Obj_Typ) then
1253 Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
1255 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
1256 -- SPARK RM 6.9(19)).
1258 elsif SPARK_Mode = On and then Is_Effectively_Volatile (Obj_Id) then
1259 Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
1261 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
1262 -- One exception to this is the object that represents the dispatch
1263 -- table of a Ghost tagged type, as the symbol needs to be exported.
1265 elsif Is_Exported (Obj_Id) then
1266 Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
1268 elsif Is_Imported (Obj_Id) then
1269 Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
1273 -- Restore the SPARK_Mode of the enclosing context after all delayed
1274 -- pragmas have been analyzed.
1276 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1277 end Analyze_Object_Contract;
1279 -----------------------------------
1280 -- Analyze_Package_Body_Contract --
1281 -----------------------------------
1283 -- WARNING: This routine manages SPARK regions. Return statements must be
1284 -- replaced by gotos which jump to the end of the routine and restore the
1287 procedure Analyze_Package_Body_Contract
1288 (Body_Id : Entity_Id;
1289 Freeze_Id : Entity_Id := Empty)
1291 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
1292 Items : constant Node_Id := Contract (Body_Id);
1293 Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
1295 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1296 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1297 -- Save the SPARK_Mode-related data to restore on exit
1299 Ref_State : Node_Id;
1302 -- Do not analyze a contract multiple times
1304 if Present (Items) then
1305 if Analyzed (Items) then
1308 Set_Analyzed (Items);
1312 -- Due to the timing of contract analysis, delayed pragmas may be
1313 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1314 -- context. To remedy this, restore the original SPARK_Mode of the
1315 -- related package body.
1317 Set_SPARK_Mode (Body_Id);
1319 Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
1321 -- The analysis of pragma Refined_State detects whether the spec has
1322 -- abstract states available for refinement.
1324 if Present (Ref_State) then
1325 Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id);
1328 -- Restore the SPARK_Mode of the enclosing context after all delayed
1329 -- pragmas have been analyzed.
1331 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1333 -- Capture all global references in a generic package body now that the
1334 -- contract has been analyzed.
1336 if Is_Generic_Declaration_Or_Body (Body_Decl) then
1337 Save_Global_References_In_Contract
1338 (Templ => Original_Node (Body_Decl),
1341 end Analyze_Package_Body_Contract;
1343 ------------------------------
1344 -- Analyze_Package_Contract --
1345 ------------------------------
1347 -- WARNING: This routine manages SPARK regions. Return statements must be
1348 -- replaced by gotos which jump to the end of the routine and restore the
1351 procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
1352 Items : constant Node_Id := Contract (Pack_Id);
1353 Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
1355 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1356 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1357 -- Save the SPARK_Mode-related data to restore on exit
1359 Init : Node_Id := Empty;
1360 Init_Cond : Node_Id := Empty;
1365 -- Do not analyze a contract multiple times
1367 if Present (Items) then
1368 if Analyzed (Items) then
1371 -- Do not analyze the contract of the internal package
1372 -- created to check conformance of an actual package.
1373 -- Such an internal package is removed from the tree after
1374 -- legality checks are completed, and it does not contain
1375 -- the declarations of all local entities of the generic.
1377 elsif Is_Internal (Pack_Id)
1378 and then Is_Generic_Instance (Pack_Id)
1383 Set_Analyzed (Items);
1387 -- Due to the timing of contract analysis, delayed pragmas may be
1388 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1389 -- context. To remedy this, restore the original SPARK_Mode of the
1392 Set_SPARK_Mode (Pack_Id);
1394 if Present (Items) then
1396 -- Locate and store pragmas Initial_Condition and Initializes, since
1397 -- their order of analysis matters.
1399 Prag := Classifications (Items);
1400 while Present (Prag) loop
1401 Prag_Nam := Pragma_Name (Prag);
1403 if Prag_Nam = Name_Initial_Condition then
1406 elsif Prag_Nam = Name_Initializes then
1410 Prag := Next_Pragma (Prag);
1413 -- Analyze the initialization-related pragmas. Initializes must come
1414 -- before Initial_Condition due to item dependencies.
1416 if Present (Init) then
1417 Analyze_Initializes_In_Decl_Part (Init);
1420 if Present (Init_Cond) then
1421 Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
1425 -- Restore the SPARK_Mode of the enclosing context after all delayed
1426 -- pragmas have been analyzed.
1428 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1430 -- Capture all global references in a generic package now that the
1431 -- contract has been analyzed.
1433 if Is_Generic_Declaration_Or_Body (Pack_Decl) then
1434 Save_Global_References_In_Contract
1435 (Templ => Original_Node (Pack_Decl),
1438 end Analyze_Package_Contract;
1440 --------------------------------------------
1441 -- Analyze_Package_Instantiation_Contract --
1442 --------------------------------------------
1444 -- WARNING: This routine manages SPARK regions. Return statements must be
1445 -- replaced by gotos which jump to the end of the routine and restore the
1448 procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is
1449 Inst_Spec : constant Node_Id :=
1450 Instance_Spec (Unit_Declaration_Node (Inst_Id));
1452 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1453 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1454 -- Save the SPARK_Mode-related data to restore on exit
1456 Pack_Id : Entity_Id;
1460 -- Nothing to do when the package instantiation is erroneous or left
1461 -- partially decorated.
1463 if No (Inst_Spec) then
1467 Pack_Id := Defining_Entity (Inst_Spec);
1468 Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
1470 -- Due to the timing of contract analysis, delayed pragmas may be
1471 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1472 -- context. To remedy this, restore the original SPARK_Mode of the
1475 Set_SPARK_Mode (Pack_Id);
1477 -- Check whether the lack of indicator Part_Of agrees with the placement
1478 -- of the package instantiation with respect to the state space. Nested
1479 -- package instantiations do not need to be checked because they inherit
1480 -- Part_Of indicator of the outermost package instantiation (see routine
1481 -- Propagate_Part_Of in Sem_Prag).
1486 elsif No (Prag) then
1487 Check_Missing_Part_Of (Pack_Id);
1490 -- Restore the SPARK_Mode of the enclosing context after all delayed
1491 -- pragmas have been analyzed.
1493 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1494 end Analyze_Package_Instantiation_Contract;
1496 --------------------------------
1497 -- Analyze_Protected_Contract --
1498 --------------------------------
1500 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
1501 Items : constant Node_Id := Contract (Prot_Id);
1504 -- Do not analyze a contract multiple times
1506 if Present (Items) then
1507 if Analyzed (Items) then
1510 Set_Analyzed (Items);
1513 end Analyze_Protected_Contract;
1515 -------------------------------------------
1516 -- Analyze_Subprogram_Body_Stub_Contract --
1517 -------------------------------------------
1519 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
1520 Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
1521 Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
1524 -- A subprogram body stub may act as its own spec or as the completion
1525 -- of a previous declaration. Depending on the context, the contract of
1526 -- the stub may contain two sets of pragmas.
1528 -- The stub is a completion, the applicable pragmas are:
1532 if Present (Spec_Id) then
1533 Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
1535 -- The stub acts as its own spec, the applicable pragmas are:
1538 -- Exceptional_Cases
1542 -- Subprogram_Variant
1546 Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
1548 end Analyze_Subprogram_Body_Stub_Contract;
1550 ---------------------------
1551 -- Analyze_Task_Contract --
1552 ---------------------------
1554 -- WARNING: This routine manages SPARK regions. Return statements must be
1555 -- replaced by gotos which jump to the end of the routine and restore the
1558 procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
1559 Items : constant Node_Id := Contract (Task_Id);
1561 Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
1562 Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
1563 -- Save the SPARK_Mode-related data to restore on exit
1568 -- Do not analyze a contract multiple times
1570 if Present (Items) then
1571 if Analyzed (Items) then
1574 Set_Analyzed (Items);
1578 -- Due to the timing of contract analysis, delayed pragmas may be
1579 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1580 -- context. To remedy this, restore the original SPARK_Mode of the
1581 -- related task unit.
1583 Set_SPARK_Mode (Task_Id);
1585 -- Analyze Global first, as Depends may mention items classified in the
1586 -- global categorization.
1588 Prag := Get_Pragma (Task_Id, Pragma_Global);
1590 if Present (Prag) then
1591 Analyze_Global_In_Decl_Part (Prag);
1594 -- Depends must be analyzed after Global in order to see the modes of
1595 -- all global items.
1597 Prag := Get_Pragma (Task_Id, Pragma_Depends);
1599 if Present (Prag) then
1600 Analyze_Depends_In_Decl_Part (Prag);
1603 -- Restore the SPARK_Mode of the enclosing context after all delayed
1604 -- pragmas have been analyzed.
1606 Restore_SPARK_Mode (Saved_SM, Saved_SMP);
1607 end Analyze_Task_Contract;
1609 ---------------------------
1610 -- Analyze_Type_Contract --
1611 ---------------------------
1613 procedure Analyze_Type_Contract (Type_Id : Entity_Id) is
1615 Check_Type_Or_Object_External_Properties
1616 (Type_Or_Obj_Id => Type_Id);
1618 -- Analyze Pre/Post on access-to-subprogram type
1620 if Ekind (Type_Id) in Access_Subprogram_Kind then
1621 Analyze_Entry_Or_Subprogram_Contract
1622 (Directly_Designated_Type (Type_Id));
1624 end Analyze_Type_Contract;
1626 ---------------------------------------
1627 -- Build_Subprogram_Contract_Wrapper --
1628 ---------------------------------------
1630 procedure Build_Subprogram_Contract_Wrapper
1631 (Body_Id : Entity_Id;
1636 Body_Decl : constant Entity_Id := Unit_Declaration_Node (Body_Id);
1637 Loc : constant Source_Ptr := Sloc (Body_Decl);
1638 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
1639 Subp_Id : Entity_Id;
1640 Ret_Type : Entity_Id;
1642 Wrapper_Id : Entity_Id;
1643 Wrapper_Body : Node_Id;
1644 Wrapper_Spec : Node_Id;
1647 -- When there are no postcondition statements we do not need to
1648 -- generate a wrapper.
1654 -- Obtain the related subprogram id from the body id.
1656 if Present (Spec_Id) then
1661 Ret_Type := Etype (Subp_Id);
1663 -- Generate the contracts wrapper by moving the original declarations
1664 -- and statements within a local subprogram, calling it and possibly
1665 -- preserving the result for the purpose of evaluating postconditions,
1666 -- contracts, type invariants, etc.
1668 -- In the case of a function, generate:
1670 -- function Original_Func (X : in out Integer) return Typ is
1671 -- <prologue renamings>
1674 -- function _Wrapped_Statements return Typ is
1675 -- <original declarations>
1677 -- <original statements>
1682 -- Result_Obj : constant Typ := _Wrapped_Statements
1684 -- <postconditions statements>
1688 -- Or else, in the case of a procedure, generate:
1690 -- procedure Original_Proc (X : in out Integer) is
1691 -- <prologue renamings>
1694 -- procedure _Wrapped_Statements is
1695 -- <original declarations>
1697 -- <original statements>
1701 -- _Wrapped_Statements;
1702 -- <postconditions statements>
1705 -- Create Identifier
1707 Wrapper_Id := Make_Defining_Identifier (Loc, Name_uWrapped_Statements);
1708 Set_Debug_Info_Needed (Wrapper_Id);
1709 Set_Wrapped_Statements (Subp_Id, Wrapper_Id);
1711 Set_Has_Pragma_Inline (Wrapper_Id, Has_Pragma_Inline (Subp_Id));
1712 Set_Has_Pragma_Inline_Always
1713 (Wrapper_Id, Has_Pragma_Inline_Always (Subp_Id));
1715 -- Create specification and declaration for the wrapper
1717 if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
1719 Make_Procedure_Specification (Loc,
1720 Defining_Unit_Name => Wrapper_Id);
1723 Make_Function_Specification (Loc,
1724 Defining_Unit_Name => Wrapper_Id,
1725 Result_Definition => New_Occurrence_Of (Ret_Type, Loc));
1728 -- Create the wrapper body using Body_Id's statements and declarations
1731 Make_Subprogram_Body (Loc,
1732 Specification => Wrapper_Spec,
1733 Declarations => Declarations (Body_Decl),
1734 Handled_Statement_Sequence =>
1735 Relocate_Node (Handled_Statement_Sequence (Body_Decl)));
1737 Append_To (Decls, Wrapper_Body);
1738 Set_Declarations (Body_Decl, Decls);
1739 Set_Handled_Statement_Sequence (Body_Decl,
1740 Make_Handled_Sequence_Of_Statements (Loc,
1741 End_Label => Make_Identifier (Loc, Chars (Wrapper_Id))));
1743 -- Prepend a call to the wrapper when the subprogram is a procedure
1745 if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
1747 Make_Procedure_Call_Statement (Loc,
1748 Name => New_Occurrence_Of (Wrapper_Id, Loc)));
1750 (Handled_Statement_Sequence (Body_Decl), Stmts);
1752 -- Generate the post-execution statements and the extended return
1753 -- when the subprogram being wrapped is a function.
1756 Set_Statements (Handled_Statement_Sequence (Body_Decl), New_List (
1757 Make_Extended_Return_Statement (Loc,
1758 Return_Object_Declarations => New_List (
1759 Make_Object_Declaration (Loc,
1760 Defining_Identifier => Result,
1761 Constant_Present => True,
1762 Object_Definition =>
1763 New_Occurrence_Of (Ret_Type, Loc),
1765 Make_Function_Call (Loc,
1767 New_Occurrence_Of (Wrapper_Id, Loc)))),
1768 Handled_Statement_Sequence =>
1769 Make_Handled_Sequence_Of_Statements (Loc,
1770 Statements => Stmts))));
1772 end Build_Subprogram_Contract_Wrapper;
1774 ----------------------------------
1775 -- Build_Entry_Contract_Wrapper --
1776 ----------------------------------
1778 procedure Build_Entry_Contract_Wrapper (E : Entity_Id; Decl : Node_Id) is
1779 Conc_Typ : constant Entity_Id := Scope (E);
1780 Loc : constant Source_Ptr := Sloc (E);
1782 procedure Add_Discriminant_Renamings
1783 (Obj_Id : Entity_Id;
1785 -- Add renaming declarations for all discriminants of concurrent type
1786 -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
1787 -- represents the concurrent object.
1789 procedure Add_Matching_Formals
1791 Actuals : in out List_Id);
1792 -- Add formal parameters that match those of entry E to list Formals.
1793 -- The routine also adds matching actuals for the new formals to list
1796 procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id);
1797 -- Relocate pragma Prag to list To. The routine creates a new list if
1798 -- To does not exist.
1800 --------------------------------
1801 -- Add_Discriminant_Renamings --
1802 --------------------------------
1804 procedure Add_Discriminant_Renamings
1805 (Obj_Id : Entity_Id;
1809 Renaming_Decl : Node_Id;
1812 -- Inspect the discriminants of the concurrent type and generate a
1813 -- renaming for each one.
1815 if Has_Discriminants (Conc_Typ) then
1816 Discr := First_Discriminant (Conc_Typ);
1817 while Present (Discr) loop
1819 Make_Object_Renaming_Declaration (Loc,
1820 Defining_Identifier =>
1821 Make_Defining_Identifier (Loc, Chars (Discr)),
1823 New_Occurrence_Of (Etype (Discr), Loc),
1825 Make_Selected_Component (Loc,
1826 Prefix => New_Occurrence_Of (Obj_Id, Loc),
1828 Make_Identifier (Loc, Chars (Discr))));
1830 Prepend_To (Decls, Renaming_Decl);
1832 Next_Discriminant (Discr);
1835 end Add_Discriminant_Renamings;
1837 --------------------------
1838 -- Add_Matching_Formals --
1839 --------------------------
1841 procedure Add_Matching_Formals
1843 Actuals : in out List_Id)
1846 New_Formal : Entity_Id;
1849 -- Inspect the formal parameters of the entry and generate a new
1850 -- matching formal with the same name for the wrapper. A reference
1851 -- to the new formal becomes an actual in the entry call.
1853 Formal := First_Formal (E);
1854 while Present (Formal) loop
1855 New_Formal := Make_Defining_Identifier (Loc, Chars (Formal));
1857 Make_Parameter_Specification (Loc,
1858 Defining_Identifier => New_Formal,
1859 In_Present => In_Present (Parent (Formal)),
1860 Out_Present => Out_Present (Parent (Formal)),
1862 New_Occurrence_Of (Etype (Formal), Loc)));
1864 if No (Actuals) then
1865 Actuals := New_List;
1868 Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
1869 Next_Formal (Formal);
1871 end Add_Matching_Formals;
1873 ---------------------
1874 -- Transfer_Pragma --
1875 ---------------------
1877 procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id) is
1885 New_Prag := Relocate_Node (Prag);
1887 Set_Analyzed (New_Prag, False);
1888 Append (New_Prag, To);
1889 end Transfer_Pragma;
1893 Items : constant Node_Id := Contract (E);
1894 Actuals : List_Id := No_List;
1897 Decls : List_Id := No_List;
1899 Has_Pragma : Boolean := False;
1900 Index_Id : Entity_Id;
1903 Wrapper_Id : Entity_Id;
1905 -- Start of processing for Build_Entry_Contract_Wrapper
1908 -- This routine generates a specialized wrapper for a protected or task
1909 -- entry [family] which implements precondition/postcondition semantics.
1910 -- Preconditions and case guards of contract cases are checked before
1911 -- the protected action or rendezvous takes place.
1913 -- procedure Wrapper
1914 -- (Obj_Id : Conc_Typ; -- concurrent object
1915 -- [Index : Index_Typ;] -- index of entry family
1916 -- [Formal_1 : ...; -- parameters of original entry
1919 -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
1920 -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
1922 -- <contracts pragmas>
1923 -- <case guard checks>
1926 -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
1929 -- Create the wrapper only when the entry has at least one executable
1930 -- contract item such as contract cases, precondition or postcondition.
1932 if Present (Items) then
1934 -- Inspect the list of pre/postconditions and transfer all available
1935 -- pragmas to the declarative list of the wrapper.
1937 Prag := Pre_Post_Conditions (Items);
1938 while Present (Prag) loop
1939 if Pragma_Name_Unmapped (Prag) in Name_Postcondition
1941 and then Is_Checked (Prag)
1944 Transfer_Pragma (Prag, To => Decls);
1947 Prag := Next_Pragma (Prag);
1950 -- Inspect the list of test/contract cases and transfer only contract
1951 -- cases pragmas to the declarative part of the wrapper.
1953 Prag := Contract_Test_Cases (Items);
1954 while Present (Prag) loop
1955 if Pragma_Name (Prag) = Name_Contract_Cases
1956 and then Is_Checked (Prag)
1959 Transfer_Pragma (Prag, To => Decls);
1962 Prag := Next_Pragma (Prag);
1966 -- The entry lacks executable contract items and a wrapper is not needed
1968 if not Has_Pragma then
1972 -- Create the profile of the wrapper. The first formal parameter is the
1973 -- concurrent object.
1976 Make_Defining_Identifier (Loc,
1977 Chars => New_External_Name (Chars (Conc_Typ), 'A'));
1979 Formals := New_List (
1980 Make_Parameter_Specification (Loc,
1981 Defining_Identifier => Obj_Id,
1982 Out_Present => True,
1984 Parameter_Type => New_Occurrence_Of (Conc_Typ, Loc)));
1986 -- Construct the call to the original entry. The call will be gradually
1987 -- augmented with an optional entry index and extra parameters.
1990 Make_Selected_Component (Loc,
1991 Prefix => New_Occurrence_Of (Obj_Id, Loc),
1992 Selector_Name => New_Occurrence_Of (E, Loc));
1994 -- When creating a wrapper for an entry family, the second formal is the
1997 if Ekind (E) = E_Entry_Family then
1998 Index_Id := Make_Defining_Identifier (Loc, Name_I);
2001 Make_Parameter_Specification (Loc,
2002 Defining_Identifier => Index_Id,
2004 New_Occurrence_Of (Entry_Index_Type (E), Loc)));
2006 -- The call to the original entry becomes an indexed component to
2007 -- accommodate the entry index.
2010 Make_Indexed_Component (Loc,
2012 Expressions => New_List (New_Occurrence_Of (Index_Id, Loc)));
2015 -- Add formal parameters to match those of the entry and build actuals
2016 -- for the entry call.
2018 Add_Matching_Formals (Formals, Actuals);
2021 Make_Procedure_Call_Statement (Loc,
2023 Parameter_Associations => Actuals);
2025 -- Add renaming declarations for the discriminants of the enclosing type
2026 -- as the various contract items may reference them.
2028 Add_Discriminant_Renamings (Obj_Id, Decls);
2031 Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
2032 Set_Contract_Wrapper (E, Wrapper_Id);
2033 Set_Is_Entry_Wrapper (Wrapper_Id);
2035 -- The wrapper body is analyzed when the enclosing type is frozen
2037 Append_Freeze_Action (Defining_Entity (Decl),
2038 Make_Subprogram_Body (Loc,
2040 Make_Procedure_Specification (Loc,
2041 Defining_Unit_Name => Wrapper_Id,
2042 Parameter_Specifications => Formals),
2043 Declarations => Decls,
2044 Handled_Statement_Sequence =>
2045 Make_Handled_Sequence_Of_Statements (Loc,
2046 Statements => New_List (Call))));
2047 end Build_Entry_Contract_Wrapper;
2049 ---------------------------
2050 -- Check_Class_Condition --
2051 ---------------------------
2053 procedure Check_Class_Condition
2056 Par_Subp : Entity_Id;
2057 Is_Precondition : Boolean)
2059 function Check_Entity (N : Node_Id) return Traverse_Result;
2060 -- Check reference to formal of inherited operation or to primitive
2061 -- operation of root type.
2067 function Check_Entity (N : Node_Id) return Traverse_Result is
2072 if Nkind (N) = N_Identifier
2073 and then Present (Entity (N))
2075 (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
2077 (Nkind (Parent (N)) /= N_Attribute_Reference
2078 or else Attribute_Name (Parent (N)) /= Name_Class)
2080 -- These checks do not apply to dispatching calls within the
2081 -- condition, but only to calls whose static tag is that of
2084 if Is_Subprogram (Entity (N))
2085 and then Nkind (Parent (N)) = N_Function_Call
2086 and then Present (Controlling_Argument (Parent (N)))
2091 -- Determine whether entity has a renaming
2093 Orig_E := Entity (N);
2094 New_E := Get_Mapped_Entity (Orig_E);
2096 if Present (New_E) then
2098 -- AI12-0166: A precondition for a protected operation
2099 -- cannot include an internal call to a protected function
2100 -- of the type. In the case of an inherited condition for an
2101 -- overriding operation, both the operation and the function
2102 -- are given by primitive wrappers.
2105 and then Ekind (New_E) = E_Function
2106 and then Is_Primitive_Wrapper (New_E)
2107 and then Is_Primitive_Wrapper (Subp)
2108 and then Scope (Subp) = Scope (New_E)
2110 Error_Msg_Node_2 := Wrapped_Entity (Subp);
2112 ("internal call to& cannot appear in inherited "
2113 & "precondition of protected operation&",
2114 Subp, Wrapped_Entity (New_E));
2118 -- Check that there are no calls left to abstract operations if
2119 -- the current subprogram is not abstract.
2122 and then Nkind (Parent (N)) = N_Function_Call
2123 and then N = Name (Parent (N))
2125 if not Is_Abstract_Subprogram (Subp)
2126 and then Is_Abstract_Subprogram (New_E)
2128 Error_Msg_Sloc := Sloc (Current_Scope);
2129 Error_Msg_Node_2 := Subp;
2131 if Comes_From_Source (Subp) then
2133 ("cannot call abstract subprogram & in inherited "
2134 & "condition for&#", Subp, New_E);
2137 ("cannot call abstract subprogram & in inherited "
2138 & "condition for inherited&#", Subp, New_E);
2141 -- In SPARK mode, report error on inherited condition for an
2142 -- inherited operation if it contains a call to an overriding
2143 -- operation, because this implies that the pre/postconditions
2144 -- of the inherited operation have changed silently.
2146 elsif SPARK_Mode = On
2147 and then Warn_On_Suspicious_Contract
2148 and then Present (Alias (Subp))
2149 and then Present (New_E)
2150 and then Comes_From_Source (New_E)
2153 ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
2155 Error_Msg_Sloc := Sloc (New_E);
2156 Error_Msg_Node_2 := Subp;
2158 ("\overriding of&# forces overriding of&",
2159 Parent (Subp), New_E);
2167 procedure Check_Condition_Entities is
2168 new Traverse_Proc (Check_Entity);
2170 -- Start of processing for Check_Class_Condition
2173 -- No check required if the subprograms match
2175 if Par_Subp = Subp then
2179 Update_Primitives_Mapping (Par_Subp, Subp);
2180 Map_Formals (Par_Subp, Subp);
2181 Check_Condition_Entities (Cond);
2182 end Check_Class_Condition;
2184 -----------------------------
2185 -- Create_Generic_Contract --
2186 -----------------------------
2188 procedure Create_Generic_Contract (Unit : Node_Id) is
2189 Templ : constant Node_Id := Original_Node (Unit);
2190 Templ_Id : constant Entity_Id := Defining_Entity (Templ);
2192 procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
2193 -- Add a single contract-related source pragma Prag to the contract of
2194 -- generic template Templ_Id.
2196 ---------------------------------
2197 -- Add_Generic_Contract_Pragma --
2198 ---------------------------------
2200 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
2201 Prag_Templ : Node_Id;
2204 -- Mark the pragma to prevent the premature capture of global
2205 -- references when capturing global references of the context
2206 -- (see Save_References_In_Pragma).
2208 Set_Is_Generic_Contract_Pragma (Prag);
2210 -- Pragmas that apply to a generic subprogram declaration are not
2211 -- part of the semantic structure of the generic template:
2214 -- procedure Example (Formal : Integer);
2215 -- pragma Precondition (Formal > 0);
2217 -- Create a generic template for such pragmas and link the template
2218 -- of the pragma with the generic template.
2220 if Nkind (Templ) = N_Generic_Subprogram_Declaration then
2222 (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
2223 Prag_Templ := Original_Node (Prag);
2225 Set_Is_Generic_Contract_Pragma (Prag_Templ);
2226 Add_Contract_Item (Prag_Templ, Templ_Id);
2228 -- Otherwise link the pragma with the generic template
2231 Add_Contract_Item (Prag, Templ_Id);
2235 -- We do not stop the compilation at this point in the case of an
2236 -- invalid pragma because it will be properly diagnosed afterward.
2238 when Contract_Error => null;
2239 end Add_Generic_Contract_Pragma;
2243 Context : constant Node_Id := Parent (Unit);
2244 Decl : Node_Id := Empty;
2246 -- Start of processing for Create_Generic_Contract
2249 -- A generic package declaration carries contract-related source pragmas
2250 -- in its visible declarations.
2252 if Nkind (Templ) = N_Generic_Package_Declaration then
2253 Mutate_Ekind (Templ_Id, E_Generic_Package);
2255 if Present (Visible_Declarations (Specification (Templ))) then
2256 Decl := First (Visible_Declarations (Specification (Templ)));
2259 -- A generic package body carries contract-related source pragmas in its
2262 elsif Nkind (Templ) = N_Package_Body then
2263 Mutate_Ekind (Templ_Id, E_Package_Body);
2265 if Present (Declarations (Templ)) then
2266 Decl := First (Declarations (Templ));
2269 -- Generic subprogram declaration
2271 elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
2272 if Nkind (Specification (Templ)) = N_Function_Specification then
2273 Mutate_Ekind (Templ_Id, E_Generic_Function);
2275 Mutate_Ekind (Templ_Id, E_Generic_Procedure);
2278 -- When the generic subprogram acts as a compilation unit, inspect
2279 -- the Pragmas_After list for contract-related source pragmas.
2281 if Nkind (Context) = N_Compilation_Unit then
2282 if Present (Aux_Decls_Node (Context))
2283 and then Present (Pragmas_After (Aux_Decls_Node (Context)))
2285 Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
2288 -- Otherwise inspect the successive declarations for contract-related
2292 Decl := Next (Unit);
2295 -- A generic subprogram body carries contract-related source pragmas in
2296 -- its declarations.
2298 elsif Nkind (Templ) = N_Subprogram_Body then
2299 Mutate_Ekind (Templ_Id, E_Subprogram_Body);
2301 if Present (Declarations (Templ)) then
2302 Decl := First (Declarations (Templ));
2306 -- Inspect the relevant declarations looking for contract-related source
2307 -- pragmas and add them to the contract of the generic unit.
2309 while Present (Decl) loop
2310 if Comes_From_Source (Decl) then
2311 if Nkind (Decl) = N_Pragma then
2313 -- The source pragma is a contract annotation
2315 if Is_Contract_Annotation (Decl) then
2316 Add_Generic_Contract_Pragma (Decl);
2319 -- The region where a contract-related source pragma may appear
2320 -- ends with the first source non-pragma declaration or statement.
2329 end Create_Generic_Contract;
2331 --------------------------------
2332 -- Expand_Subprogram_Contract --
2333 --------------------------------
2335 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is
2336 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
2337 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
2339 procedure Add_Invariant_And_Predicate_Checks
2340 (Subp_Id : Entity_Id;
2341 Stmts : in out List_Id;
2342 Result : out Node_Id);
2343 -- Process the result of function Subp_Id (if applicable) and all its
2344 -- formals. Add invariant and predicate checks where applicable. The
2345 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
2346 -- function, Result contains the entity of parameter _Result, to be
2347 -- used in the creation of procedure _Postconditions.
2349 procedure Add_Stable_Property_Contracts
2350 (Subp_Id : Entity_Id; Class_Present : Boolean);
2351 -- Augment postcondition contracts to reflect Stable_Property aspect
2352 -- (if Class_Present = False) or Stable_Property'Class aspect (if
2353 -- Class_Present = True).
2355 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
2356 -- Append a node to a list. If there is no list, create a new one. When
2357 -- the item denotes a pragma, it is added to the list only when it is
2360 procedure Process_Contract_Cases
2361 (Stmts : in out List_Id;
2363 -- Process pragma Contract_Cases. This routine prepends items to the
2364 -- body declarations and appends items to list Stmts.
2366 procedure Process_Postconditions (Stmts : in out List_Id);
2367 -- Collect all [inherited] spec and body postconditions and accumulate
2368 -- their pragma Check equivalents in list Stmts.
2370 procedure Process_Preconditions (Decls : in out List_Id);
2371 -- Collect all [inherited] spec and body preconditions and prepend their
2372 -- pragma Check equivalents to the declarations of the body.
2374 ----------------------------------------
2375 -- Add_Invariant_And_Predicate_Checks --
2376 ----------------------------------------
2378 procedure Add_Invariant_And_Predicate_Checks
2379 (Subp_Id : Entity_Id;
2380 Stmts : in out List_Id;
2381 Result : out Node_Id)
2383 procedure Add_Invariant_Access_Checks (Id : Entity_Id);
2384 -- Id denotes the return value of a function or a formal parameter.
2385 -- Add an invariant check if the type of Id is access to a type with
2386 -- invariants. The routine appends the generated code to Stmts.
2388 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
2389 -- Determine whether type Typ can benefit from invariant checks. To
2390 -- qualify, the type must have a non-null invariant procedure and
2391 -- subprogram Subp_Id must appear visible from the point of view of
2394 ---------------------------------
2395 -- Add_Invariant_Access_Checks --
2396 ---------------------------------
2398 procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
2399 Loc : constant Source_Ptr := Sloc (Body_Decl);
2406 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
2407 Typ := Designated_Type (Typ);
2409 if Invariant_Checks_OK (Typ) then
2411 Make_Explicit_Dereference (Loc,
2412 Prefix => New_Occurrence_Of (Id, Loc));
2413 Set_Etype (Ref, Typ);
2416 -- if <Id> /= null then
2417 -- <invariant_call (<Ref>)>
2422 Make_If_Statement (Loc,
2425 Left_Opnd => New_Occurrence_Of (Id, Loc),
2426 Right_Opnd => Make_Null (Loc)),
2427 Then_Statements => New_List (
2428 Make_Invariant_Call (Ref))),
2432 end Add_Invariant_Access_Checks;
2434 -------------------------
2435 -- Invariant_Checks_OK --
2436 -------------------------
2438 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
2439 function Has_Public_Visibility_Of_Subprogram return Boolean;
2440 -- Determine whether type Typ has public visibility of subprogram
2443 -----------------------------------------
2444 -- Has_Public_Visibility_Of_Subprogram --
2445 -----------------------------------------
2447 function Has_Public_Visibility_Of_Subprogram return Boolean is
2448 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
2451 -- An Initialization procedure must be considered visible even
2452 -- though it is internally generated.
2454 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
2457 elsif Ekind (Scope (Typ)) /= E_Package then
2460 -- Internally generated code is never publicly visible except
2461 -- for a subprogram that is the implementation of an expression
2462 -- function. In that case the visibility is determined by the
2465 elsif not Comes_From_Source (Subp_Decl)
2467 (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
2469 Comes_From_Source (Defining_Entity (Subp_Decl)))
2473 -- Determine whether the subprogram is declared in the visible
2474 -- declarations of the package containing the type, or in the
2475 -- visible declaration of a child unit of that package.
2479 Decls : constant List_Id :=
2480 List_Containing (Subp_Decl);
2481 Subp_Scope : constant Entity_Id :=
2482 Scope (Defining_Entity (Subp_Decl));
2483 Typ_Scope : constant Entity_Id := Scope (Typ);
2487 Decls = Visible_Declarations
2488 (Specification (Unit_Declaration_Node (Typ_Scope)))
2491 (Ekind (Subp_Scope) = E_Package
2492 and then Typ_Scope /= Subp_Scope
2493 and then Is_Child_Unit (Subp_Scope)
2495 Is_Ancestor_Package (Typ_Scope, Subp_Scope)
2497 Decls = Visible_Declarations
2499 (Unit_Declaration_Node (Subp_Scope))));
2502 end Has_Public_Visibility_Of_Subprogram;
2504 -- Start of processing for Invariant_Checks_OK
2508 Has_Invariants (Typ)
2509 and then Present (Invariant_Procedure (Typ))
2510 and then not Has_Null_Body (Invariant_Procedure (Typ))
2511 and then Has_Public_Visibility_Of_Subprogram;
2512 end Invariant_Checks_OK;
2516 Loc : constant Source_Ptr := Sloc (Body_Decl);
2517 -- Source location of subprogram body contract
2522 -- Start of processing for Add_Invariant_And_Predicate_Checks
2527 -- Process the result of a function
2529 if Ekind (Subp_Id) = E_Function then
2530 Typ := Etype (Subp_Id);
2532 -- Generate _Result which is used in procedure _Postconditions to
2533 -- verify the return value.
2535 Result := Make_Defining_Identifier (Loc, Name_uResult);
2536 Set_Etype (Result, Typ);
2538 -- Add an invariant check when the return type has invariants and
2539 -- the related function is visible to the outside.
2541 if Invariant_Checks_OK (Typ) then
2544 Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
2548 -- Add an invariant check when the return type is an access to a
2549 -- type with invariants.
2551 Add_Invariant_Access_Checks (Result);
2554 -- Add invariant checks for all formals that qualify (see AI05-0289
2557 Formal := First_Formal (Subp_Id);
2558 while Present (Formal) loop
2559 Typ := Etype (Formal);
2561 if Ekind (Formal) /= E_In_Parameter
2562 or else Ekind (Subp_Id) = E_Procedure
2563 or else Is_Access_Type (Typ)
2565 if Invariant_Checks_OK (Typ) then
2568 Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
2572 Add_Invariant_Access_Checks (Formal);
2574 -- Note: we used to add predicate checks for OUT and IN OUT
2575 -- formals here, but that was misguided, since such checks are
2576 -- performed on the caller side, based on the predicate of the
2577 -- actual, rather than the predicate of the formal.
2581 Next_Formal (Formal);
2583 end Add_Invariant_And_Predicate_Checks;
2585 -----------------------------------
2586 -- Add_Stable_Property_Contracts --
2587 -----------------------------------
2589 procedure Add_Stable_Property_Contracts
2590 (Subp_Id : Entity_Id; Class_Present : Boolean)
2592 Loc : constant Source_Ptr := Sloc (Subp_Id);
2594 procedure Insert_Stable_Property_Check
2595 (Formal : Entity_Id; Property_Function : Entity_Id);
2596 -- Build the pragma for one check and insert it in the tree.
2598 function Make_Stable_Property_Condition
2599 (Formal : Entity_Id; Property_Function : Entity_Id) return Node_Id;
2600 -- Builds tree for "Func (Formal) = Func (Formal)'Old" expression.
2602 function Stable_Properties
2603 (Aspect_Bearer : Entity_Id; Negated : out Boolean)
2604 return Subprogram_List;
2605 -- If no aspect specified, then returns length-zero result.
2606 -- Negated indicates that reserved word NOT was specified.
2608 ----------------------------------
2609 -- Insert_Stable_Property_Check --
2610 ----------------------------------
2612 procedure Insert_Stable_Property_Check
2613 (Formal : Entity_Id; Property_Function : Entity_Id) is
2615 Args : constant List_Id :=
2617 (Make_Pragma_Argument_Association
2620 Make_Stable_Property_Condition
2622 Property_Function => Property_Function)),
2623 Make_Pragma_Argument_Association
2629 "failed stable property check at "
2630 & Build_Location_String (Loc)
2632 & To_String (Fully_Qualified_Name_String
2633 (Formal, Append_NUL => False))
2634 & " and property function "
2635 & To_String (Fully_Qualified_Name_String
2636 (Property_Function, Append_NUL => False))
2639 Prag : constant Node_Id :=
2641 Pragma_Identifier =>
2642 Make_Identifier (Loc, Name_Postcondition),
2643 Pragma_Argument_Associations => Args,
2644 Class_Present => Class_Present);
2646 Subp_Decl : Node_Id := Subp_Id;
2648 -- Enclosing_Declaration may return, for example,
2649 -- a N_Procedure_Specification node. Cope with this.
2651 Subp_Decl := Enclosing_Declaration (Subp_Decl);
2652 exit when Is_Declaration (Subp_Decl);
2653 Subp_Decl := Parent (Subp_Decl);
2654 pragma Assert (Present (Subp_Decl));
2657 Insert_After_And_Analyze (Subp_Decl, Prag);
2658 end Insert_Stable_Property_Check;
2660 ------------------------------------
2661 -- Make_Stable_Property_Condition --
2662 ------------------------------------
2664 function Make_Stable_Property_Condition
2665 (Formal : Entity_Id; Property_Function : Entity_Id) return Node_Id
2667 function Call_Property_Function return Node_Id is
2671 New_Occurrence_Of (Property_Function, Loc),
2672 Parameter_Associations =>
2673 New_List (New_Occurrence_Of (Formal, Loc))));
2677 Call_Property_Function,
2678 Make_Attribute_Reference
2680 Prefix => Call_Property_Function,
2681 Attribute_Name => Name_Old));
2682 end Make_Stable_Property_Condition;
2684 -----------------------
2685 -- Stable_Properties --
2686 -----------------------
2688 function Stable_Properties
2689 (Aspect_Bearer : Entity_Id; Negated : out Boolean)
2690 return Subprogram_List
2692 Aspect_Spec : Node_Id :=
2693 Find_Value_Of_Aspect
2694 (Aspect_Bearer, Aspect_Stable_Properties,
2695 Class_Present => Class_Present);
2697 -- ??? For a derived type, we wish Find_Value_Of_Aspect
2698 -- somehow knew that this aspect is not inherited.
2699 -- But it doesn't, so we cope with that here.
2701 -- There are probably issues here with inheritance from
2702 -- interface types, where just looking for the one parent type
2703 -- isn't enough. But this is far from the only work needed for
2704 -- Stable_Properties'Class for interface types.
2706 if Is_Derived_Type (Aspect_Bearer) then
2708 Parent_Type : constant Entity_Id :=
2709 Etype (Base_Type (Aspect_Bearer));
2712 Find_Value_Of_Aspect
2713 (Parent_Type, Aspect_Stable_Properties,
2714 Class_Present => Class_Present)
2716 -- prevent inheritance
2717 Aspect_Spec := Empty;
2722 if No (Aspect_Spec) then
2723 Negated := Aspect_Bearer = Subp_Id;
2724 -- This is a little bit subtle.
2725 -- We need to assign True in the Subp_Id case in order to
2726 -- distinguish between no aspect spec at all vs. an
2727 -- explicitly specified "with S_P => []" empty list.
2728 -- In both cases Stable_Properties will return a length-0
2729 -- array, but the two cases are not equivalent.
2730 -- Very roughly speaking the lack of an S_P aspect spec for
2731 -- a subprogram would be equivalent to something like
2732 -- "with S_P => [not]", where we apply the "not" modifier to
2733 -- an empty set of subprograms, if such a construct existed.
2734 -- We could just assign True here, but it seems untidy to
2735 -- return True in the case of an aspect spec for a type
2736 -- (since negation is only allowed for subp S_P aspects).
2738 return (1 .. 0 => <>);
2740 return Parse_Aspect_Stable_Properties
2741 (Aspect_Spec, Negated => Negated);
2743 end Stable_Properties;
2745 Formal : Entity_Id := First_Formal (Subp_Id);
2746 Type_Of_Formal : Entity_Id;
2748 Subp_Properties_Negated : Boolean;
2749 Subp_Properties : constant Subprogram_List :=
2750 Stable_Properties (Subp_Id, Subp_Properties_Negated);
2752 -- start of processing for Add_Stable_Property_Contracts
2755 if not (Is_Primitive (Subp_Id) and then Comes_From_Source (Subp_Id))
2760 while Present (Formal) loop
2761 Type_Of_Formal := Base_Type (Etype (Formal));
2763 if not Subp_Properties_Negated then
2765 for SPF_Id of Subp_Properties loop
2766 if Type_Of_Formal = Base_Type (Etype (First_Formal (SPF_Id)))
2767 and then Scope (Type_Of_Formal) = Scope (Subp_Id)
2769 -- ??? Need to filter out checks for SPFs that are
2770 -- mentioned explicitly in the postcondition of
2773 Insert_Stable_Property_Check
2774 (Formal => Formal, Property_Function => SPF_Id);
2778 elsif Scope (Type_Of_Formal) = Scope (Subp_Id) then
2780 Ignored : Boolean range False .. False;
2782 Typ_Property_Funcs : constant Subprogram_List :=
2783 Stable_Properties (Type_Of_Formal, Negated => Ignored);
2785 function Excluded_By_Aspect_Spec_Of_Subp
2786 (SPF_Id : Entity_Id) return Boolean;
2787 -- Examine Subp_Properties to determine whether SPF should
2790 -------------------------------------
2791 -- Excluded_By_Aspect_Spec_Of_Subp --
2792 -------------------------------------
2794 function Excluded_By_Aspect_Spec_Of_Subp
2795 (SPF_Id : Entity_Id) return Boolean is
2797 pragma Assert (Subp_Properties_Negated);
2798 -- Look through renames for equality test here ???
2799 return (for some F of Subp_Properties => F = SPF_Id);
2800 end Excluded_By_Aspect_Spec_Of_Subp;
2802 -- Look through renames for equality test here ???
2803 Subp_Is_Stable_Property_Function : constant Boolean :=
2804 (for some F of Typ_Property_Funcs => F = Subp_Id);
2806 if not Subp_Is_Stable_Property_Function then
2807 for SPF_Id of Typ_Property_Funcs loop
2808 if not Excluded_By_Aspect_Spec_Of_Subp (SPF_Id) then
2809 -- ??? Need to filter out checks for SPFs that are
2810 -- mentioned explicitly in the postcondition of
2812 Insert_Stable_Property_Check
2813 (Formal => Formal, Property_Function => SPF_Id);
2819 Next_Formal (Formal);
2821 end Add_Stable_Property_Contracts;
2823 -------------------------
2824 -- Append_Enabled_Item --
2825 -------------------------
2827 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
2829 -- Do not chain ignored or disabled pragmas
2831 if Nkind (Item) = N_Pragma
2832 and then (Is_Ignored (Item) or else Is_Disabled (Item))
2836 -- Otherwise, add the item
2843 -- If the pragma is a conjunct in a composite postcondition, it
2844 -- has been processed in reverse order. In the postcondition body
2845 -- it must appear before the others.
2847 if Nkind (Item) = N_Pragma
2848 and then From_Aspect_Specification (Item)
2849 and then Split_PPC (Item)
2851 Prepend (Item, List);
2853 Append (Item, List);
2856 end Append_Enabled_Item;
2858 ----------------------------
2859 -- Process_Contract_Cases --
2860 ----------------------------
2862 procedure Process_Contract_Cases
2863 (Stmts : in out List_Id;
2866 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
2867 -- Process pragma Contract_Cases for subprogram Subp_Id
2869 --------------------------------
2870 -- Process_Contract_Cases_For --
2871 --------------------------------
2873 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
2874 Items : constant Node_Id := Contract (Subp_Id);
2878 if Present (Items) then
2879 Prag := Contract_Test_Cases (Items);
2880 while Present (Prag) loop
2881 if Is_Checked (Prag) then
2882 if Pragma_Name (Prag) = Name_Contract_Cases then
2883 Expand_Pragma_Contract_Cases
2889 elsif Pragma_Name (Prag) = Name_Exceptional_Cases then
2890 Expand_Pragma_Exceptional_Cases (Prag);
2892 elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
2893 Expand_Pragma_Subprogram_Variant
2896 Body_Decls => Decls);
2900 Prag := Next_Pragma (Prag);
2903 end Process_Contract_Cases_For;
2905 -- Start of processing for Process_Contract_Cases
2908 Process_Contract_Cases_For (Body_Id);
2910 if Present (Spec_Id) then
2911 Process_Contract_Cases_For (Spec_Id);
2913 end Process_Contract_Cases;
2915 ----------------------------
2916 -- Process_Postconditions --
2917 ----------------------------
2919 procedure Process_Postconditions (Stmts : in out List_Id) is
2920 procedure Process_Body_Postconditions (Post_Nam : Name_Id);
2921 -- Collect all [refined] postconditions of a specific kind denoted
2922 -- by Post_Nam that belong to the body, and generate pragma Check
2923 -- equivalents in list Stmts.
2925 procedure Process_Spec_Postconditions;
2926 -- Collect all [inherited] postconditions of the spec, and generate
2927 -- pragma Check equivalents in list Stmts.
2929 ---------------------------------
2930 -- Process_Body_Postconditions --
2931 ---------------------------------
2933 procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
2934 Items : constant Node_Id := Contract (Body_Id);
2935 Unit_Decl : constant Node_Id := Parent (Body_Decl);
2940 -- Process the contract
2942 if Present (Items) then
2943 Prag := Pre_Post_Conditions (Items);
2944 while Present (Prag) loop
2945 if Pragma_Name (Prag) = Post_Nam
2946 and then Is_Checked (Prag)
2949 (Item => Build_Pragma_Check_Equivalent (Prag),
2953 Prag := Next_Pragma (Prag);
2957 -- The subprogram body being processed is actually the proper body
2958 -- of a stub with a corresponding spec. The subprogram stub may
2959 -- carry a postcondition pragma, in which case it must be taken
2960 -- into account. The pragma appears after the stub.
2962 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
2963 Decl := Next (Corresponding_Stub (Unit_Decl));
2964 while Present (Decl) loop
2966 -- Note that non-matching pragmas are skipped
2968 if Nkind (Decl) = N_Pragma then
2969 if Pragma_Name (Decl) = Post_Nam
2970 and then Is_Checked (Decl)
2973 (Item => Build_Pragma_Check_Equivalent (Decl),
2977 -- Skip internally generated code
2979 elsif not Comes_From_Source (Decl) then
2982 -- Postcondition pragmas are usually grouped together. There
2983 -- is no need to inspect the whole declarative list.
2992 end Process_Body_Postconditions;
2994 ---------------------------------
2995 -- Process_Spec_Postconditions --
2996 ---------------------------------
2998 procedure Process_Spec_Postconditions is
2999 Subps : constant Subprogram_List :=
3000 Inherited_Subprograms (Spec_Id);
3001 Seen : Subprogram_List (Subps'Range) := (others => Empty);
3003 function Seen_Subp (Subp_Id : Entity_Id) return Boolean;
3004 -- Return True if the contract of subprogram Subp_Id has been
3011 function Seen_Subp (Subp_Id : Entity_Id) return Boolean is
3013 for Index in Seen'Range loop
3014 if Seen (Index) = Subp_Id then
3027 Subp_Id : Entity_Id;
3029 -- Start of processing for Process_Spec_Postconditions
3032 -- Process the contract
3034 Items := Contract (Spec_Id);
3036 if Present (Items) then
3037 Prag := Pre_Post_Conditions (Items);
3038 while Present (Prag) loop
3039 if Pragma_Name (Prag) = Name_Postcondition
3040 and then Is_Checked (Prag)
3043 (Item => Build_Pragma_Check_Equivalent (Prag),
3047 Prag := Next_Pragma (Prag);
3051 -- Process the contracts of all inherited subprograms, looking for
3052 -- class-wide postconditions.
3054 for Index in Subps'Range loop
3055 Subp_Id := Subps (Index);
3057 if Present (Alias (Subp_Id)) then
3058 Subp_Id := Ultimate_Alias (Subp_Id);
3061 -- Wrappers of class-wide pre/postconditions reference the
3062 -- parent primitive that has the inherited contract.
3064 if Is_Wrapper (Subp_Id)
3065 and then Present (LSP_Subprogram (Subp_Id))
3067 Subp_Id := LSP_Subprogram (Subp_Id);
3070 Items := Contract (Subp_Id);
3072 if not Seen_Subp (Subp_Id) and then Present (Items) then
3073 Seen (Index) := Subp_Id;
3075 Prag := Pre_Post_Conditions (Items);
3076 while Present (Prag) loop
3077 if Pragma_Name (Prag) = Name_Postcondition
3078 and then Class_Present (Prag)
3081 Build_Pragma_Check_Equivalent
3084 Inher_Id => Subp_Id);
3086 -- The pragma Check equivalent of the class-wide
3087 -- postcondition is still created even though the
3088 -- pragma may be ignored because the equivalent
3089 -- performs semantic checks.
3091 if Is_Checked (Prag) then
3092 Append_Enabled_Item (Item, Stmts);
3096 Prag := Next_Pragma (Prag);
3100 end Process_Spec_Postconditions;
3102 pragma Unmodified (Stmts);
3103 -- Stmts is passed as IN OUT to signal that the list can be updated,
3104 -- even if the corresponding integer value representing the list does
3107 -- Start of processing for Process_Postconditions
3110 -- The processing of postconditions is done in reverse order (body
3111 -- first) to ensure the following arrangement:
3113 -- <refined postconditions from body>
3114 -- <postconditions from body>
3115 -- <postconditions from spec>
3116 -- <inherited postconditions>
3118 Process_Body_Postconditions (Name_Refined_Post);
3119 Process_Body_Postconditions (Name_Postcondition);
3121 if Present (Spec_Id) then
3122 Process_Spec_Postconditions;
3124 end Process_Postconditions;
3126 ---------------------------
3127 -- Process_Preconditions --
3128 ---------------------------
3130 procedure Process_Preconditions (Decls : in out List_Id) is
3131 Insert_Node : Node_Id := Empty;
3132 -- The insertion node after which all pragma Check equivalents are
3135 procedure Prepend_To_Decls (Item : Node_Id);
3136 -- Prepend a single item to the declarations of the subprogram body
3138 procedure Prepend_Pragma_To_Decls (Prag : Node_Id);
3139 -- Prepend a normal precondition to the declarations of the body and
3142 procedure Process_Preconditions_For (Subp_Id : Entity_Id);
3143 -- Collect all preconditions of subprogram Subp_Id and prepend their
3144 -- pragma Check equivalents to the declarations of the body.
3146 ----------------------
3147 -- Prepend_To_Decls --
3148 ----------------------
3150 procedure Prepend_To_Decls (Item : Node_Id) is
3152 -- Ensure that the body has a declarative list
3156 Set_Declarations (Body_Decl, Decls);
3159 Prepend_To (Decls, Item);
3160 end Prepend_To_Decls;
3162 -----------------------------
3163 -- Prepend_Pragma_To_Decls --
3164 -----------------------------
3166 procedure Prepend_Pragma_To_Decls (Prag : Node_Id) is
3167 Check_Prag : Node_Id;
3170 -- Skip the sole class-wide precondition (if any) since it is
3171 -- processed by Merge_Class_Conditions.
3173 if Class_Present (Prag) then
3176 -- Accumulate the corresponding Check pragmas at the top of the
3177 -- declarations. Prepending the items ensures that they will be
3178 -- evaluated in their original order.
3181 Check_Prag := Build_Pragma_Check_Equivalent (Prag);
3182 Prepend_To_Decls (Check_Prag);
3185 end Prepend_Pragma_To_Decls;
3187 -------------------------------
3188 -- Process_Preconditions_For --
3189 -------------------------------
3191 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
3192 Items : constant Node_Id := Contract (Subp_Id);
3193 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
3199 -- Process the contract. If the body is an expression function
3200 -- that is a completion, freeze types within, because this may
3201 -- not have been done yet, when the subprogram declaration and
3202 -- its completion by an expression function appear in distinct
3203 -- declarative lists of the same unit (visible and private).
3206 Was_Expression_Function (Body_Decl)
3207 and then Sloc (Body_Id) /= Sloc (Subp_Id)
3208 and then In_Same_Source_Unit (Body_Id, Subp_Id)
3209 and then not In_Same_List (Body_Decl, Subp_Decl);
3211 if Present (Items) then
3212 Prag := Pre_Post_Conditions (Items);
3213 while Present (Prag) loop
3214 if Pragma_Name (Prag) = Name_Precondition
3215 and then Is_Checked (Prag)
3218 and then Present (Corresponding_Aspect (Prag))
3222 Typ => Standard_Boolean,
3225 (First (Pragma_Argument_Associations (Prag))),
3229 Prepend_Pragma_To_Decls (Prag);
3232 Prag := Next_Pragma (Prag);
3236 -- The subprogram declaration being processed is actually a body
3237 -- stub. The stub may carry a precondition pragma, in which case
3238 -- it must be taken into account. The pragma appears after the
3241 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
3243 -- Inspect the declarations following the body stub
3245 Decl := Next (Subp_Decl);
3246 while Present (Decl) loop
3248 -- Note that non-matching pragmas are skipped
3250 if Nkind (Decl) = N_Pragma then
3251 if Pragma_Name (Decl) = Name_Precondition
3252 and then Is_Checked (Decl)
3254 Prepend_Pragma_To_Decls (Decl);
3257 -- Skip internally generated code
3259 elsif not Comes_From_Source (Decl) then
3262 -- Preconditions are usually grouped together. There is no
3263 -- need to inspect the whole declarative list.
3272 end Process_Preconditions_For;
3276 Body_Decls : constant List_Id := Declarations (Body_Decl);
3278 Next_Decl : Node_Id;
3280 -- Start of processing for Process_Preconditions
3283 -- Find the proper insertion point for all pragma Check equivalents
3285 if Present (Body_Decls) then
3286 Decl := First (Body_Decls);
3287 while Present (Decl) loop
3289 -- First source declaration terminates the search, because all
3290 -- preconditions must be evaluated prior to it, by definition.
3292 if Comes_From_Source (Decl) then
3295 -- Certain internally generated object renamings such as those
3296 -- for discriminants and protection fields must be elaborated
3297 -- before the preconditions are evaluated, as their expressions
3298 -- may mention the discriminants. The renamings include those
3299 -- for private components so we need to find the last such.
3301 elsif Is_Prologue_Renaming (Decl) then
3302 while Present (Next (Decl))
3303 and then Is_Prologue_Renaming (Next (Decl))
3308 Insert_Node := Decl;
3310 -- Otherwise the declaration does not come from source. This
3311 -- also terminates the search, because internal code may raise
3312 -- exceptions which should not preempt the preconditions.
3321 -- The processing of preconditions is done in reverse order (body
3322 -- first), because each pragma Check equivalent is inserted at the
3323 -- top of the declarations. This ensures that the final order is
3324 -- consistent with following diagram:
3326 -- <inherited preconditions>
3327 -- <preconditions from spec>
3328 -- <preconditions from body>
3330 Process_Preconditions_For (Body_Id);
3332 -- Move the generated entry-call prologue renamings into the
3333 -- outer declarations for use in the preconditions.
3335 Decl := First (Body_Decls);
3336 while Present (Decl) and then Present (Insert_Node) loop
3337 Next_Decl := Next (Decl);
3339 Prepend_To_Decls (Decl);
3341 exit when Decl = Insert_Node;
3346 if Present (Spec_Id) then
3347 Process_Preconditions_For (Spec_Id);
3349 end Process_Preconditions;
3353 Restore_Scope : Boolean := False;
3355 Stmts : List_Id := No_List;
3356 Decls : List_Id := New_List;
3357 Subp_Id : Entity_Id;
3359 -- Start of processing for Expand_Subprogram_Contract
3362 -- Obtain the entity of the initial declaration
3364 if Present (Spec_Id) then
3370 -- Do not perform expansion activity when it is not needed
3372 if not Expander_Active then
3375 -- GNATprove does not need the executable semantics of a contract
3377 elsif GNATprove_Mode then
3380 -- The contract of a generic subprogram or one declared in a generic
3381 -- context is not expanded, as the corresponding instance will provide
3382 -- the executable semantics of the contract.
3384 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
3387 -- All subprograms carry a contract, but for some it is not significant
3388 -- and should not be processed. This is a small optimization.
3390 elsif not Has_Significant_Contract (Subp_Id) then
3393 -- The contract of an ignored Ghost subprogram does not need expansion,
3394 -- because the subprogram and all calls to it will be removed.
3396 elsif Is_Ignored_Ghost_Entity (Subp_Id) then
3399 -- No action needed for helpers and indirect-call wrapper built to
3400 -- support class-wide preconditions.
3402 elsif Present (Class_Preconditions_Subprogram (Subp_Id)) then
3405 -- Do not re-expand the same contract. This scenario occurs when a
3406 -- construct is rewritten into something else during its analysis
3407 -- (expression functions for instance).
3409 elsif Has_Expanded_Contract (Subp_Id) then
3413 -- Prevent multiple expansion attempts of the same contract
3415 Set_Has_Expanded_Contract (Subp_Id);
3417 -- Ensure that the formal parameters are visible when expanding all
3420 if not In_Open_Scopes (Subp_Id) then
3421 Restore_Scope := True;
3422 Push_Scope (Subp_Id);
3424 if Is_Generic_Subprogram (Subp_Id) then
3425 Install_Generic_Formals (Subp_Id);
3427 Install_Formals (Subp_Id);
3431 -- The expansion of a subprogram contract involves the creation of Check
3432 -- pragmas to verify the contract assertions of the spec and body in a
3433 -- particular order. The order is as follows:
3435 -- function Original_Code (...) return ... is
3436 -- <prologue renamings>
3437 -- <inherited preconditions>
3438 -- <preconditions from spec>
3439 -- <preconditions from body>
3440 -- <contract case conditions>
3442 -- function _Wrapped_Statements (...) return ... is
3443 -- <source declarations>
3445 -- <source statements>
3446 -- end _Wrapped_Statements;
3449 -- return Result : constant ... := _Wrapped_Statements do
3450 -- <refined postconditions from body>
3451 -- <postconditions from body>
3452 -- <postconditions from spec>
3453 -- <inherited postconditions>
3454 -- <contract case consequences>
3455 -- <invariant check of function result>
3456 -- <invariant and predicate checks of parameters
3458 -- end Original_Code;
3460 -- Step 1: augment contracts list with postconditions associated with
3461 -- Stable_Properties and Stable_Properties'Class aspects. This must
3462 -- precede Process_Postconditions.
3464 for Class_Present in Boolean loop
3465 Add_Stable_Property_Contracts
3466 (Subp_Id, Class_Present => Class_Present);
3469 -- Step 2: Handle all preconditions. This action must come before the
3470 -- processing of pragma Contract_Cases because the pragma prepends items
3471 -- to the body declarations.
3473 Process_Preconditions (Decls);
3475 -- Step 3: Handle all postconditions. This action must come before the
3476 -- processing of pragma Contract_Cases because the pragma appends items
3479 Process_Postconditions (Stmts);
3481 -- Step 4: Handle pragma Contract_Cases. This action must come before
3482 -- the processing of invariants and predicates because those append
3483 -- items to list Stmts.
3485 Process_Contract_Cases (Stmts, Decls);
3487 -- Step 5: Apply invariant and predicate checks on a function result and
3488 -- all formals. The resulting checks are accumulated in list Stmts.
3490 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
3492 -- Step 6: Construct subprogram _wrapped_statements
3494 -- When no statements are present we still need to insert contract
3495 -- related declarations.
3498 Prepend_List_To (Declarations (Body_Decl), Decls);
3500 -- Otherwise, we need a wrapper
3503 Build_Subprogram_Contract_Wrapper (Body_Id, Stmts, Decls, Result);
3506 if Restore_Scope then
3509 end Expand_Subprogram_Contract;
3511 -------------------------------
3512 -- Freeze_Previous_Contracts --
3513 -------------------------------
3515 procedure Freeze_Previous_Contracts (Body_Decl : Node_Id) is
3516 function Causes_Contract_Freezing (N : Node_Id) return Boolean;
3517 pragma Inline (Causes_Contract_Freezing);
3518 -- Determine whether arbitrary node N causes contract freezing. This is
3519 -- used as an assertion for the current body declaration that caused
3520 -- contract freezing, and as a condition to detect body declaration that
3521 -- already caused contract freezing before.
3523 procedure Freeze_Contracts;
3524 pragma Inline (Freeze_Contracts);
3525 -- Freeze the contracts of all eligible constructs which precede body
3528 procedure Freeze_Enclosing_Package_Body;
3529 pragma Inline (Freeze_Enclosing_Package_Body);
3530 -- Freeze the contract of the nearest package body (if any) which
3531 -- encloses body Body_Decl.
3533 ------------------------------
3534 -- Causes_Contract_Freezing --
3535 ------------------------------
3537 function Causes_Contract_Freezing (N : Node_Id) return Boolean is
3539 -- The following condition matches guards for calls to
3540 -- Freeze_Previous_Contracts from routines that analyze various body
3541 -- declarations. In particular, it detects expression functions, as
3542 -- described in the call from Analyze_Subprogram_Body_Helper.
3545 Comes_From_Source (Original_Node (N))
3548 N_Entry_Body | N_Package_Body | N_Protected_Body |
3549 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body;
3550 end Causes_Contract_Freezing;
3552 ----------------------
3553 -- Freeze_Contracts --
3554 ----------------------
3556 procedure Freeze_Contracts is
3557 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
3561 -- Nothing to do when the body which causes freezing does not appear
3562 -- in a declarative list because there cannot possibly be constructs
3565 if not Is_List_Member (Body_Decl) then
3569 -- Inspect the declarations preceding the body, and freeze individual
3570 -- contracts of eligible constructs.
3572 Decl := Prev (Body_Decl);
3573 while Present (Decl) loop
3575 -- Stop the traversal when a preceding construct that causes
3576 -- freezing is encountered as there is no point in refreezing
3577 -- the already frozen constructs.
3579 if Causes_Contract_Freezing (Decl) then
3582 -- Entry or subprogram declarations
3584 elsif Nkind (Decl) in N_Abstract_Subprogram_Declaration
3585 | N_Entry_Declaration
3586 | N_Generic_Subprogram_Declaration
3587 | N_Subprogram_Declaration
3589 Analyze_Entry_Or_Subprogram_Contract
3590 (Subp_Id => Defining_Entity (Decl),
3591 Freeze_Id => Body_Id);
3595 elsif Nkind (Decl) = N_Object_Declaration then
3596 Analyze_Object_Contract
3597 (Obj_Id => Defining_Entity (Decl),
3598 Freeze_Id => Body_Id);
3602 elsif Nkind (Decl) in N_Protected_Type_Declaration
3603 | N_Single_Protected_Declaration
3605 Analyze_Protected_Contract (Defining_Entity (Decl));
3607 -- Subprogram body stubs
3609 elsif Nkind (Decl) = N_Subprogram_Body_Stub then
3610 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
3614 elsif Nkind (Decl) in N_Single_Task_Declaration
3615 | N_Task_Type_Declaration
3617 Analyze_Task_Contract (Defining_Entity (Decl));
3620 if Nkind (Decl) in N_Full_Type_Declaration
3621 | N_Private_Type_Declaration
3622 | N_Task_Type_Declaration
3623 | N_Protected_Type_Declaration
3624 | N_Formal_Type_Declaration
3626 Analyze_Type_Contract (Defining_Identifier (Decl));
3631 end Freeze_Contracts;
3633 -----------------------------------
3634 -- Freeze_Enclosing_Package_Body --
3635 -----------------------------------
3637 procedure Freeze_Enclosing_Package_Body is
3638 Orig_Decl : constant Node_Id := Original_Node (Body_Decl);
3642 -- Climb the parent chain looking for an enclosing package body. Do
3643 -- not use the scope stack, because a body utilizes the entity of its
3644 -- corresponding spec.
3646 Par := Parent (Body_Decl);
3647 while Present (Par) loop
3648 if Nkind (Par) = N_Package_Body then
3649 Analyze_Package_Body_Contract
3650 (Body_Id => Defining_Entity (Par),
3651 Freeze_Id => Defining_Entity (Body_Decl));
3655 -- Do not look for an enclosing package body when the construct
3656 -- which causes freezing is a body generated for an expression
3657 -- function and it appears within a package spec. This ensures
3658 -- that the traversal will not reach too far up the parent chain
3659 -- and attempt to freeze a package body which must not be frozen.
3661 -- package body Enclosing_Body
3662 -- with Refined_State => (State => Var)
3664 -- package Nested is
3665 -- type Some_Type is ...;
3666 -- function Cause_Freezing return ...;
3668 -- function Cause_Freezing is (...);
3671 -- Var : Nested.Some_Type;
3673 elsif Nkind (Par) = N_Package_Declaration
3674 and then Nkind (Orig_Decl) = N_Expression_Function
3678 -- Prevent the search from going too far
3680 elsif Is_Body_Or_Package_Declaration (Par) then
3684 Par := Parent (Par);
3686 end Freeze_Enclosing_Package_Body;
3690 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
3692 -- Start of processing for Freeze_Previous_Contracts
3695 pragma Assert (Causes_Contract_Freezing (Body_Decl));
3697 -- A body that is in the process of being inlined appears from source,
3698 -- but carries name _parent. Such a body does not cause freezing of
3701 if Chars (Body_Id) = Name_uParent then
3705 Freeze_Enclosing_Package_Body;
3707 end Freeze_Previous_Contracts;
3709 ---------------------------------
3710 -- Inherit_Subprogram_Contract --
3711 ---------------------------------
3713 procedure Inherit_Subprogram_Contract
3715 From_Subp : Entity_Id)
3717 procedure Inherit_Pragma (Prag_Id : Pragma_Id);
3718 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3721 --------------------
3722 -- Inherit_Pragma --
3723 --------------------
3725 procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
3726 Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
3730 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3731 -- chains, therefore the node must be replicated. The new pragma is
3732 -- flagged as inherited for distinction purposes.
3734 if Present (Prag) then
3735 New_Prag := New_Copy_Tree (Prag);
3736 Set_Is_Inherited_Pragma (New_Prag);
3738 Add_Contract_Item (New_Prag, Subp);
3742 -- Start of processing for Inherit_Subprogram_Contract
3745 -- Inheritance is carried out only when both entities are subprograms
3748 if Is_Subprogram_Or_Generic_Subprogram (Subp)
3749 and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
3750 and then Present (Contract (From_Subp))
3752 Inherit_Pragma (Pragma_Extensions_Visible);
3754 end Inherit_Subprogram_Contract;
3756 -------------------------------------
3757 -- Instantiate_Subprogram_Contract --
3758 -------------------------------------
3760 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
3761 procedure Instantiate_Pragmas (First_Prag : Node_Id);
3762 -- Instantiate all contract-related source pragmas found in the list,
3763 -- starting with pragma First_Prag. Each instantiated pragma is added
3766 -------------------------
3767 -- Instantiate_Pragmas --
3768 -------------------------
3770 procedure Instantiate_Pragmas (First_Prag : Node_Id) is
3771 Inst_Prag : Node_Id;
3776 while Present (Prag) loop
3777 if Is_Generic_Contract_Pragma (Prag) then
3779 Copy_Generic_Node (Prag, Empty, Instantiating => True);
3781 Set_Analyzed (Inst_Prag, False);
3782 Append_To (L, Inst_Prag);
3785 Prag := Next_Pragma (Prag);
3787 end Instantiate_Pragmas;
3791 Items : constant Node_Id := Contract (Defining_Entity (Templ));
3793 -- Start of processing for Instantiate_Subprogram_Contract
3796 if Present (Items) then
3797 Instantiate_Pragmas (Pre_Post_Conditions (Items));
3798 Instantiate_Pragmas (Contract_Test_Cases (Items));
3799 Instantiate_Pragmas (Classifications (Items));
3801 end Instantiate_Subprogram_Contract;
3803 --------------------------
3804 -- Is_Prologue_Renaming --
3805 --------------------------
3807 -- This should be turned into a flag and set during the expansion of
3808 -- task and protected types when the renamings get generated ???
3810 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
3817 if Nkind (Decl) = N_Object_Renaming_Declaration
3818 and then not Comes_From_Source (Decl)
3820 Obj := Defining_Entity (Decl);
3823 if Nkind (Nam) = N_Selected_Component then
3824 -- Analyze the renaming declaration so we can further examine it
3826 if not Analyzed (Decl) then
3830 Pref := Prefix (Nam);
3831 Sel := Selector_Name (Nam);
3833 -- A discriminant renaming appears as
3834 -- Discr : constant ... := Prefix.Discr;
3836 if Ekind (Obj) = E_Constant
3837 and then Is_Entity_Name (Sel)
3838 and then Present (Entity (Sel))
3839 and then Ekind (Entity (Sel)) = E_Discriminant
3843 -- A protection field renaming appears as
3844 -- Prot : ... := _object._object;
3846 -- A renamed private component is just a component of
3847 -- _object, with an arbitrary name.
3849 elsif Ekind (Obj) in E_Variable | E_Constant
3850 and then Nkind (Pref) = N_Identifier
3851 and then Chars (Pref) = Name_uObject
3852 and then Nkind (Sel) = N_Identifier
3860 end Is_Prologue_Renaming;
3862 -----------------------------------
3863 -- Make_Class_Precondition_Subps --
3864 -----------------------------------
3866 procedure Make_Class_Precondition_Subps
3867 (Subp_Id : Entity_Id;
3868 Late_Overriding : Boolean := False)
3870 Loc : constant Source_Ptr := Sloc (Subp_Id);
3871 Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
3873 procedure Add_Indirect_Call_Wrapper;
3874 -- Build the indirect-call wrapper and append it to the freezing actions
3877 procedure Add_Call_Helper
3878 (Helper_Id : Entity_Id;
3879 Is_Dynamic : Boolean);
3880 -- Factorizes code for building a call helper with the given identifier
3881 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
3882 -- controls building the static or dynamic version of the helper.
3884 function Build_Unique_Name (Suffix : String) return Name_Id;
3885 -- Build an unique new name adding suffix to Subp_Id name (plus its
3886 -- homonym number for values bigger than 1).
3888 -------------------------------
3889 -- Add_Indirect_Call_Wrapper --
3890 -------------------------------
3892 procedure Add_Indirect_Call_Wrapper is
3894 function Build_ICW_Body return Node_Id;
3895 -- Build the body of the indirect call wrapper
3897 function Build_ICW_Decl return Node_Id;
3898 -- Build the declaration of the indirect call wrapper
3900 --------------------
3901 -- Build_ICW_Body --
3902 --------------------
3904 function Build_ICW_Body return Node_Id is
3905 ICW_Id : constant Entity_Id := Indirect_Call_Wrapper (Subp_Id);
3906 Spec : constant Node_Id := Parent (ICW_Id);
3907 Body_Spec : Node_Id;
3912 Body_Spec := Copy_Subprogram_Spec (Spec);
3914 -- Build call to wrapped subprogram
3917 Actuals : constant List_Id := Empty_List;
3918 Formal_Spec : Entity_Id :=
3919 First (Parameter_Specifications (Spec));
3921 -- Build parameter association & call
3923 while Present (Formal_Spec) loop
3926 (Defining_Identifier (Formal_Spec), Loc));
3930 if Ekind (ICW_Id) = E_Procedure then
3932 Make_Procedure_Call_Statement (Loc,
3933 Name => New_Occurrence_Of (Subp_Id, Loc),
3934 Parameter_Associations => Actuals);
3937 Make_Simple_Return_Statement (Loc,
3939 Make_Function_Call (Loc,
3940 Name => New_Occurrence_Of (Subp_Id, Loc),
3941 Parameter_Associations => Actuals));
3946 Make_Subprogram_Body (Loc,
3947 Specification => Body_Spec,
3948 Declarations => New_List,
3949 Handled_Statement_Sequence =>
3950 Make_Handled_Sequence_Of_Statements (Loc,
3951 Statements => New_List (Call)));
3953 -- The new operation is internal and overriding indicators do not
3956 Set_Must_Override (Body_Spec, False);
3961 --------------------
3962 -- Build_ICW_Decl --
3963 --------------------
3965 function Build_ICW_Decl return Node_Id is
3966 ICW_Id : constant Entity_Id :=
3967 Make_Defining_Identifier (Loc,
3968 Build_Unique_Name (Suffix => "ICW"));
3973 Spec := Copy_Subprogram_Spec (Parent (Subp_Id));
3974 Set_Must_Override (Spec, False);
3975 Set_Must_Not_Override (Spec, False);
3976 Set_Defining_Unit_Name (Spec, ICW_Id);
3977 Mutate_Ekind (ICW_Id, Ekind (Subp_Id));
3978 Set_Is_Public (ICW_Id);
3980 -- The indirect call wrapper is commonly used for indirect calls
3981 -- but inlined for direct calls performed from the DTW.
3983 Set_Is_Inlined (ICW_Id);
3985 if Nkind (Spec) = N_Procedure_Specification then
3986 Set_Null_Present (Spec, False);
3989 Decl := Make_Subprogram_Declaration (Loc, Spec);
3991 -- Link original subprogram to indirect wrapper and vice versa
3993 Set_Indirect_Call_Wrapper (Subp_Id, ICW_Id);
3994 Set_Class_Preconditions_Subprogram (ICW_Id, Subp_Id);
3996 -- Inherit debug info flag to allow debugging the wrapper
3998 if Needs_Debug_Info (Subp_Id) then
3999 Set_Debug_Info_Needed (ICW_Id);
4010 -- Start of processing for Add_Indirect_Call_Wrapper
4013 pragma Assert (No (Indirect_Call_Wrapper (Subp_Id)));
4015 ICW_Decl := Build_ICW_Decl;
4017 Append_Freeze_Action (Tagged_Type, ICW_Decl);
4020 ICW_Body := Build_ICW_Body;
4021 Append_Freeze_Action (Tagged_Type, ICW_Body);
4023 -- We cannot defer the analysis of this ICW wrapper when it is
4024 -- built as a consequence of building its partner DTW wrapper
4025 -- at the freezing point of the tagged type.
4027 if Is_Dispatch_Table_Wrapper (Subp_Id) then
4030 end Add_Indirect_Call_Wrapper;
4032 ---------------------
4033 -- Add_Call_Helper --
4034 ---------------------
4036 procedure Add_Call_Helper
4037 (Helper_Id : Entity_Id;
4038 Is_Dynamic : Boolean)
4040 function Build_Call_Helper_Body return Node_Id;
4041 -- Build the body of a call helper
4043 function Build_Call_Helper_Decl return Node_Id;
4044 -- Build the declaration of a call helper
4046 function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id;
4047 -- Build the specification of the helper
4049 ----------------------------
4050 -- Build_Call_Helper_Body --
4051 ----------------------------
4053 function Build_Call_Helper_Body return Node_Id is
4055 function Copy_And_Update_References
4056 (Expr : Node_Id) return Node_Id;
4057 -- Copy Expr updating references to formals of Helper_Id; update
4058 -- also references to loop identifiers of quantified expressions.
4060 --------------------------------
4061 -- Copy_And_Update_References --
4062 --------------------------------
4064 function Copy_And_Update_References
4065 (Expr : Node_Id) return Node_Id
4067 Assoc_List : constant Elist_Id := New_Elmt_List;
4069 procedure Map_Quantified_Expression_Loop_Identifiers;
4070 -- Traverse Expr and append to Assoc_List the mapping of loop
4071 -- identifers of quantified expressions with its new copy.
4073 ------------------------------------------------
4074 -- Map_Quantified_Expression_Loop_Identifiers --
4075 ------------------------------------------------
4077 procedure Map_Quantified_Expression_Loop_Identifiers is
4078 function Map_Loop_Param (N : Node_Id) return Traverse_Result;
4079 -- Append to Assoc_List the mapping of loop identifers of
4080 -- quantified expressions with its new copy.
4082 --------------------
4083 -- Map_Loop_Param --
4084 --------------------
4086 function Map_Loop_Param (N : Node_Id) return Traverse_Result
4089 if Nkind (N) = N_Loop_Parameter_Specification
4090 and then Nkind (Parent (N)) = N_Quantified_Expression
4093 Def_Id : constant Entity_Id :=
4094 Defining_Identifier (N);
4096 Append_Elmt (Def_Id, Assoc_List);
4097 Append_Elmt (New_Copy (Def_Id), Assoc_List);
4104 procedure Map_Quantified_Expressions is
4105 new Traverse_Proc (Map_Loop_Param);
4108 Map_Quantified_Expressions (Expr);
4109 end Map_Quantified_Expression_Loop_Identifiers;
4113 Subp_Formal_Id : Entity_Id := First_Formal (Subp_Id);
4114 Helper_Formal_Id : Entity_Id := First_Formal (Helper_Id);
4116 -- Start of processing for Copy_And_Update_References
4119 while Present (Subp_Formal_Id) loop
4120 Append_Elmt (Subp_Formal_Id, Assoc_List);
4121 Append_Elmt (Helper_Formal_Id, Assoc_List);
4123 Next_Formal (Subp_Formal_Id);
4124 Next_Formal (Helper_Formal_Id);
4127 Map_Quantified_Expression_Loop_Identifiers;
4129 return New_Copy_Tree (Expr, Map => Assoc_List);
4130 end Copy_And_Update_References;
4134 Helper_Decl : constant Node_Id := Parent (Parent (Helper_Id));
4135 Body_Id : Entity_Id;
4136 Body_Spec : Node_Id;
4137 Body_Stmts : Node_Id;
4138 Helper_Body : Node_Id;
4139 Return_Expr : Node_Id;
4141 -- Start of processing for Build_Call_Helper_Body
4144 pragma Assert (Analyzed (Unit_Declaration_Node (Helper_Id)));
4145 pragma Assert (No (Corresponding_Body (Helper_Decl)));
4147 Body_Id := Make_Defining_Identifier (Loc, Chars (Helper_Id));
4148 Body_Spec := Build_Call_Helper_Spec (Body_Id);
4150 Set_Corresponding_Body (Helper_Decl, Body_Id);
4151 Set_Must_Override (Body_Spec, False);
4153 if Present (Class_Preconditions (Subp_Id))
4154 -- Evaluate the expression if we are building a dynamic helper
4155 -- or we are building a static helper for a non-abstract tagged
4156 -- type; for abstract tagged types the helper just returns True
4157 -- since it is called by the indirect call wrapper (ICW).
4161 not Is_Abstract_Type (Find_Dispatching_Type (Subp_Id)))
4164 Copy_And_Update_References (Class_Preconditions (Subp_Id));
4166 -- When the subprogram is compiled with assertions disabled the
4167 -- helper just returns True; done to avoid reporting errors at
4168 -- link time since a unit may be compiled with assertions disabled
4169 -- and another (which depends on it) compiled with assertions
4173 pragma Assert (Present (Ignored_Class_Preconditions (Subp_Id))
4174 or else Is_Abstract_Type (Find_Dispatching_Type (Subp_Id)));
4175 Return_Expr := New_Occurrence_Of (Standard_True, Loc);
4179 Make_Handled_Sequence_Of_Statements (Loc,
4180 Statements => New_List (
4181 Make_Simple_Return_Statement (Loc, Return_Expr)));
4184 Make_Subprogram_Body (Loc,
4185 Specification => Body_Spec,
4186 Declarations => New_List,
4187 Handled_Statement_Sequence => Body_Stmts);
4190 end Build_Call_Helper_Body;
4192 ----------------------------
4193 -- Build_Call_Helper_Decl --
4194 ----------------------------
4196 function Build_Call_Helper_Decl return Node_Id is
4201 Spec := Build_Call_Helper_Spec (Helper_Id);
4202 Set_Must_Override (Spec, False);
4203 Set_Must_Not_Override (Spec, False);
4204 Set_Is_Inlined (Helper_Id);
4205 Set_Is_Public (Helper_Id);
4207 Decl := Make_Subprogram_Declaration (Loc, Spec);
4209 -- Inherit debug info flag from Subp_Id to Helper_Id to allow
4210 -- debugging of the helper subprogram.
4212 if Needs_Debug_Info (Subp_Id) then
4213 Set_Debug_Info_Needed (Helper_Id);
4217 end Build_Call_Helper_Decl;
4219 ----------------------------
4220 -- Build_Call_Helper_Spec --
4221 ----------------------------
4223 function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id
4225 Spec : constant Node_Id := Parent (Subp_Id);
4226 Def_Id : constant Node_Id := Defining_Unit_Name (Spec);
4228 Func_Formals : constant List_Id := New_List;
4229 P_Spec : constant List_Id := Parameter_Specifications (Spec);
4230 Par_Formal : Node_Id;
4232 Param_Type : Node_Id;
4235 -- Create a list of formal parameters with the same types as the
4236 -- original subprogram but changing the controlling formal.
4238 Param := First (P_Spec);
4239 Formal := First_Formal (Def_Id);
4240 while Present (Formal) loop
4241 Par_Formal := Parent (Formal);
4243 if Is_Dynamic and then Is_Controlling_Formal (Formal) then
4244 if Nkind (Parameter_Type (Par_Formal))
4245 = N_Access_Definition
4248 Copy_Separate_Tree (Parameter_Type (Par_Formal));
4249 Rewrite (Subtype_Mark (Param_Type),
4250 Make_Attribute_Reference (Loc,
4251 Prefix => Relocate_Node (Subtype_Mark (Param_Type)),
4252 Attribute_Name => Name_Class));
4256 Make_Attribute_Reference (Loc,
4257 Prefix => New_Occurrence_Of (Etype (Formal), Loc),
4258 Attribute_Name => Name_Class);
4261 Param_Type := New_Occurrence_Of (Etype (Formal), Loc);
4264 Append_To (Func_Formals,
4265 Make_Parameter_Specification (Loc,
4266 Defining_Identifier =>
4267 Make_Defining_Identifier (Loc, Chars (Formal)),
4268 In_Present => In_Present (Par_Formal),
4269 Out_Present => Out_Present (Par_Formal),
4270 Null_Exclusion_Present => Null_Exclusion_Present
4272 Parameter_Type => Param_Type));
4275 Next_Formal (Formal);
4279 Make_Function_Specification (Loc,
4280 Defining_Unit_Name => Spec_Id,
4281 Parameter_Specifications => Func_Formals,
4282 Result_Definition =>
4283 New_Occurrence_Of (Standard_Boolean, Loc));
4284 end Build_Call_Helper_Spec;
4288 Helper_Body : Node_Id;
4289 Helper_Decl : Node_Id;
4291 -- Start of processing for Add_Call_Helper
4294 Helper_Decl := Build_Call_Helper_Decl;
4295 Mutate_Ekind (Helper_Id, Ekind (Subp_Id));
4297 -- Add the helper to the freezing actions of the tagged type
4299 Append_Freeze_Action (Tagged_Type, Helper_Decl);
4300 Analyze (Helper_Decl);
4302 Helper_Body := Build_Call_Helper_Body;
4303 Append_Freeze_Action (Tagged_Type, Helper_Body);
4305 -- If this helper is built as part of building the DTW at the
4306 -- freezing point of its tagged type then we cannot defer
4309 if Late_Overriding then
4310 pragma Assert (Is_Dispatch_Table_Wrapper (Subp_Id));
4311 Analyze (Helper_Body);
4313 end Add_Call_Helper;
4315 -----------------------
4316 -- Build_Unique_Name --
4317 -----------------------
4319 function Build_Unique_Name (Suffix : String) return Name_Id is
4321 -- Append the homonym number. Strip the leading space character in
4322 -- the image of natural numbers. Also do not add the homonym value
4325 if Has_Homonym (Subp_Id) and then Homonym_Number (Subp_Id) > 1 then
4327 S : constant String := Homonym_Number (Subp_Id)'Img;
4330 return New_External_Name (Chars (Subp_Id),
4331 Suffix => Suffix & "_" & S (2 .. S'Last));
4335 return New_External_Name (Chars (Subp_Id), Suffix);
4336 end Build_Unique_Name;
4340 Helper_Id : Entity_Id;
4342 -- Start of processing for Make_Class_Precondition_Subps
4345 if Present (Class_Preconditions (Subp_Id))
4346 or Present (Ignored_Class_Preconditions (Subp_Id))
4349 (Comes_From_Source (Subp_Id)
4350 or else Is_Dispatch_Table_Wrapper (Subp_Id));
4352 if No (Dynamic_Call_Helper (Subp_Id)) then
4354 -- Build and add to the freezing actions of Tagged_Type its
4355 -- dynamic-call helper.
4358 Make_Defining_Identifier (Loc,
4359 Build_Unique_Name (Suffix => "DP"));
4360 Add_Call_Helper (Helper_Id, Is_Dynamic => True);
4362 -- Link original subprogram to helper and vice versa
4364 Set_Dynamic_Call_Helper (Subp_Id, Helper_Id);
4365 Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
4368 if not Is_Abstract_Subprogram (Subp_Id)
4369 and then No (Static_Call_Helper (Subp_Id))
4371 -- Build and add to the freezing actions of Tagged_Type its
4372 -- static-call helper.
4375 Make_Defining_Identifier (Loc,
4376 Build_Unique_Name (Suffix => "SP"));
4378 Add_Call_Helper (Helper_Id, Is_Dynamic => False);
4380 -- Link original subprogram to helper and vice versa
4382 Set_Static_Call_Helper (Subp_Id, Helper_Id);
4383 Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
4385 -- Build and add to the freezing actions of Tagged_Type the
4386 -- indirect-call wrapper.
4388 Add_Indirect_Call_Wrapper;
4391 end Make_Class_Precondition_Subps;
4393 ----------------------------------------------
4394 -- Process_Class_Conditions_At_Freeze_Point --
4395 ----------------------------------------------
4397 procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id) is
4399 procedure Check_Class_Conditions (Spec_Id : Entity_Id);
4400 -- Check class-wide pre/postconditions of Spec_Id
4402 function Has_Class_Postconditions_Subprogram
4403 (Spec_Id : Entity_Id) return Boolean;
4404 -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
4406 function Has_Class_Preconditions_Subprogram
4407 (Spec_Id : Entity_Id) return Boolean;
4408 -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
4410 ----------------------------
4411 -- Check_Class_Conditions --
4412 ----------------------------
4414 procedure Check_Class_Conditions (Spec_Id : Entity_Id) is
4415 Par_Subp : Entity_Id;
4418 for Kind in Condition_Kind loop
4419 Par_Subp := Nearest_Class_Condition_Subprogram (Kind, Spec_Id);
4421 if Present (Par_Subp) then
4422 Check_Class_Condition
4423 (Cond => Class_Condition (Kind, Par_Subp),
4425 Par_Subp => Par_Subp,
4426 Is_Precondition => Kind in Ignored_Class_Precondition
4427 | Class_Precondition);
4430 end Check_Class_Conditions;
4432 -----------------------------------------
4433 -- Has_Class_Postconditions_Subprogram --
4434 -----------------------------------------
4436 function Has_Class_Postconditions_Subprogram
4437 (Spec_Id : Entity_Id) return Boolean is
4440 Present (Nearest_Class_Condition_Subprogram
4441 (Spec_Id => Spec_Id,
4442 Kind => Class_Postcondition))
4444 Present (Nearest_Class_Condition_Subprogram
4445 (Spec_Id => Spec_Id,
4446 Kind => Ignored_Class_Postcondition));
4447 end Has_Class_Postconditions_Subprogram;
4449 ----------------------------------------
4450 -- Has_Class_Preconditions_Subprogram --
4451 ----------------------------------------
4453 function Has_Class_Preconditions_Subprogram
4454 (Spec_Id : Entity_Id) return Boolean is
4457 Present (Nearest_Class_Condition_Subprogram
4458 (Spec_Id => Spec_Id,
4459 Kind => Class_Precondition))
4461 Present (Nearest_Class_Condition_Subprogram
4462 (Spec_Id => Spec_Id,
4463 Kind => Ignored_Class_Precondition));
4464 end Has_Class_Preconditions_Subprogram;
4468 Prim_Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ));
4471 -- Start of processing for Process_Class_Conditions_At_Freeze_Point
4474 while Present (Prim_Elmt) loop
4475 Prim := Node (Prim_Elmt);
4477 if Has_Class_Preconditions_Subprogram (Prim)
4478 or else Has_Class_Postconditions_Subprogram (Prim)
4480 if Comes_From_Source (Prim) then
4481 if Has_Significant_Contract (Prim) then
4482 Merge_Class_Conditions (Prim);
4485 -- Handle wrapper of protected operation
4487 elsif Is_Primitive_Wrapper (Prim) then
4488 Merge_Class_Conditions (Prim);
4490 -- Check inherited class-wide conditions, excluding internal
4491 -- entities built for mapping of interface primitives.
4493 elsif Is_Derived_Type (Typ)
4494 and then Present (Alias (Prim))
4495 and then No (Interface_Alias (Prim))
4497 Check_Class_Conditions (Prim);
4501 Next_Elmt (Prim_Elmt);
4503 end Process_Class_Conditions_At_Freeze_Point;
4505 ----------------------------
4506 -- Merge_Class_Conditions --
4507 ----------------------------
4509 procedure Merge_Class_Conditions (Spec_Id : Entity_Id) is
4511 procedure Process_Inherited_Conditions (Kind : Condition_Kind);
4512 -- Collect all inherited class-wide conditions of Spec_Id and merge
4513 -- them into one big condition.
4515 ----------------------------------
4516 -- Process_Inherited_Conditions --
4517 ----------------------------------
4519 procedure Process_Inherited_Conditions (Kind : Condition_Kind) is
4520 Tag_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id);
4521 Subps : constant Subprogram_List := Inherited_Subprograms (Spec_Id);
4522 Seen : Subprogram_List (Subps'Range) := (others => Empty);
4524 function Inherit_Condition
4525 (Par_Subp : Entity_Id;
4526 Subp : Entity_Id) return Node_Id;
4527 -- Inherit the class-wide condition from Par_Subp to Subp and adjust
4528 -- all the references to formals in the inherited condition.
4530 procedure Merge_Conditions (From : Node_Id; Into : Node_Id);
4531 -- Merge two class-wide preconditions or postconditions (the former
4532 -- are merged using "or else", and the latter are merged using "and-
4533 -- then"). The changes are accumulated in parameter Into.
4535 function Seen_Subp (Id : Entity_Id) return Boolean;
4536 -- Return True if the contract of subprogram Id has been processed
4538 -----------------------
4539 -- Inherit_Condition --
4540 -----------------------
4542 function Inherit_Condition
4543 (Par_Subp : Entity_Id;
4544 Subp : Entity_Id) return Node_Id
4546 function Check_Condition (Expr : Node_Id) return Boolean;
4547 -- Used in assertion to check that Expr has no reference to the
4548 -- formals of Par_Subp.
4550 ---------------------
4551 -- Check_Condition --
4552 ---------------------
4554 function Check_Condition (Expr : Node_Id) return Boolean is
4555 Par_Formal_Id : Entity_Id;
4557 function Check_Entity (N : Node_Id) return Traverse_Result;
4558 -- Check occurrence of Par_Formal_Id
4564 function Check_Entity (N : Node_Id) return Traverse_Result is
4566 if Nkind (N) = N_Identifier
4567 and then Present (Entity (N))
4568 and then Entity (N) = Par_Formal_Id
4576 function Check_Expression is new Traverse_Func (Check_Entity);
4578 -- Start of processing for Check_Condition
4581 Par_Formal_Id := First_Formal (Par_Subp);
4583 while Present (Par_Formal_Id) loop
4584 if Check_Expression (Expr) = Abandon then
4588 Next_Formal (Par_Formal_Id);
4592 end Check_Condition;
4596 Assoc_List : constant Elist_Id := New_Elmt_List;
4597 Par_Formal_Id : Entity_Id := First_Formal (Par_Subp);
4598 Subp_Formal_Id : Entity_Id := First_Formal (Subp);
4599 New_Condition : Node_Id;
4602 while Present (Par_Formal_Id) loop
4603 Append_Elmt (Par_Formal_Id, Assoc_List);
4604 Append_Elmt (Subp_Formal_Id, Assoc_List);
4606 Next_Formal (Par_Formal_Id);
4607 Next_Formal (Subp_Formal_Id);
4610 -- Check that Parent field of all the nodes have their correct
4611 -- decoration; required because otherwise mapped nodes with
4612 -- wrong Parent field are left unmodified in the copied tree
4613 -- and cause reporting wrong errors at later stages.
4616 (Check_Parents (Class_Condition (Kind, Par_Subp), Assoc_List));
4620 (Source => Class_Condition (Kind, Par_Subp),
4623 -- Ensure that the inherited condition has no reference to the
4624 -- formals of the parent subprogram.
4626 pragma Assert (Check_Condition (New_Condition));
4628 return New_Condition;
4629 end Inherit_Condition;
4631 ----------------------
4632 -- Merge_Conditions --
4633 ----------------------
4635 procedure Merge_Conditions (From : Node_Id; Into : Node_Id) is
4636 function Expression_Arg (Expr : Node_Id) return Node_Id;
4637 -- Return the boolean expression argument of a condition while
4638 -- updating its parentheses count for the subsequent merge.
4640 --------------------
4641 -- Expression_Arg --
4642 --------------------
4644 function Expression_Arg (Expr : Node_Id) return Node_Id is
4646 if Paren_Count (Expr) = 0 then
4647 Set_Paren_Count (Expr, 1);
4655 From_Expr : constant Node_Id := Expression_Arg (From);
4656 Into_Expr : constant Node_Id := Expression_Arg (Into);
4657 Loc : constant Source_Ptr := Sloc (Into);
4659 -- Start of processing for Merge_Conditions
4664 -- Merge the two preconditions by "or else"-ing them
4666 when Ignored_Class_Precondition
4667 | Class_Precondition
4671 Right_Opnd => Relocate_Node (Into_Expr),
4672 Left_Opnd => From_Expr));
4674 -- Merge the two postconditions by "and then"-ing them
4676 when Ignored_Class_Postcondition
4677 | Class_Postcondition
4681 Right_Opnd => Relocate_Node (Into_Expr),
4682 Left_Opnd => From_Expr));
4684 end Merge_Conditions;
4690 function Seen_Subp (Id : Entity_Id) return Boolean is
4692 for Index in Seen'Range loop
4693 if Seen (Index) = Id then
4703 Class_Cond : Node_Id;
4705 Subp_Id : Entity_Id;
4706 Par_Prim : Entity_Id := Empty;
4707 Par_Iface_Prims : Elist_Id := No_Elist;
4709 -- Start of processing for Process_Inherited_Conditions
4712 Class_Cond := Class_Condition (Kind, Spec_Id);
4714 -- Process parent primitives looking for nearest ancestor with
4715 -- class-wide conditions.
4717 for Index in Subps'Range loop
4718 Subp_Id := Subps (Index);
4721 and then Is_Ancestor (Find_Dispatching_Type (Subp_Id), Tag_Typ)
4723 if Present (Alias (Subp_Id)) then
4724 Subp_Id := Ultimate_Alias (Subp_Id);
4727 -- Wrappers of class-wide pre/postconditions reference the
4728 -- parent primitive that has the inherited contract and help
4729 -- us to climb fast.
4731 if Is_Wrapper (Subp_Id)
4732 and then Present (LSP_Subprogram (Subp_Id))
4734 Subp_Id := LSP_Subprogram (Subp_Id);
4737 if not Seen_Subp (Subp_Id)
4738 and then Present (Class_Condition (Kind, Subp_Id))
4740 Seen (Index) := Subp_Id;
4741 Par_Prim := Subp_Id;
4742 Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim);
4744 Cond := Inherit_Condition
4746 Par_Subp => Subp_Id);
4748 if Present (Class_Cond) then
4749 Merge_Conditions (Cond, Class_Cond);
4754 Check_Class_Condition
4755 (Cond => Class_Cond,
4757 Par_Subp => Subp_Id,
4758 Is_Precondition => Kind in Ignored_Class_Precondition
4759 | Class_Precondition);
4760 Build_Class_Wide_Expression
4761 (Pragma_Or_Expr => Class_Cond,
4763 Par_Subp => Subp_Id,
4764 Adjust_Sloc => False);
4766 -- We are done as soon as we process the nearest ancestor
4773 -- Process the contract of interface primitives not covered by
4774 -- the nearest ancestor.
4776 for Index in Subps'Range loop
4777 Subp_Id := Subps (Index);
4779 if Is_Interface (Find_Dispatching_Type (Subp_Id)) then
4780 if Present (Alias (Subp_Id)) then
4781 Subp_Id := Ultimate_Alias (Subp_Id);
4784 if not Seen_Subp (Subp_Id)
4785 and then Present (Class_Condition (Kind, Subp_Id))
4786 and then not Contains (Par_Iface_Prims, Subp_Id)
4788 Seen (Index) := Subp_Id;
4790 Cond := Inherit_Condition
4792 Par_Subp => Subp_Id);
4794 Check_Class_Condition
4797 Par_Subp => Subp_Id,
4798 Is_Precondition => Kind in Ignored_Class_Precondition
4799 | Class_Precondition);
4800 Build_Class_Wide_Expression
4801 (Pragma_Or_Expr => Cond,
4803 Par_Subp => Subp_Id,
4804 Adjust_Sloc => False);
4806 if Present (Class_Cond) then
4807 Merge_Conditions (Cond, Class_Cond);
4815 Set_Class_Condition (Kind, Spec_Id, Class_Cond);
4816 end Process_Inherited_Conditions;
4822 -- Start of processing for Merge_Class_Conditions
4825 for Kind in Condition_Kind loop
4826 Cond := Class_Condition (Kind, Spec_Id);
4828 -- If this subprogram has class-wide conditions then preanalyze
4829 -- them before processing inherited conditions since conditions
4830 -- are checked and merged from right to left.
4832 if Present (Cond) then
4833 Preanalyze_Condition (Spec_Id, Cond);
4836 Process_Inherited_Conditions (Kind);
4838 -- Preanalyze merged inherited conditions
4840 if Cond /= Class_Condition (Kind, Spec_Id) then
4841 Preanalyze_Condition (Spec_Id,
4842 Class_Condition (Kind, Spec_Id));
4845 end Merge_Class_Conditions;
4847 ---------------------------------
4848 -- Preanalyze_Class_Conditions --
4849 ---------------------------------
4851 procedure Preanalyze_Class_Conditions (Spec_Id : Entity_Id) is
4855 for Kind in Condition_Kind loop
4856 Cond := Class_Condition (Kind, Spec_Id);
4858 if Present (Cond) then
4859 Preanalyze_Condition (Spec_Id, Cond);
4862 end Preanalyze_Class_Conditions;
4864 --------------------------
4865 -- Preanalyze_Condition --
4866 --------------------------
4868 procedure Preanalyze_Condition
4872 procedure Clear_Unset_References;
4873 -- Clear unset references on formals of Subp since preanalysis
4874 -- occurs in a place unrelated to the actual code.
4876 procedure Remove_Controlling_Arguments;
4877 -- Traverse Expr and clear the Controlling_Argument of calls to
4878 -- nonabstract functions.
4880 procedure Restore_Original_Selected_Component;
4881 -- Traverse Expr searching for dispatching calls to functions whose
4882 -- original node was a selected component, and replace them with
4883 -- their original node.
4885 ----------------------------
4886 -- Clear_Unset_References --
4887 ----------------------------
4889 procedure Clear_Unset_References is
4890 F : Entity_Id := First_Formal (Subp);
4893 while Present (F) loop
4894 Set_Unset_Reference (F, Empty);
4897 end Clear_Unset_References;
4899 ----------------------------------
4900 -- Remove_Controlling_Arguments --
4901 ----------------------------------
4903 procedure Remove_Controlling_Arguments is
4904 function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result;
4905 -- Reset the Controlling_Argument of calls to nonabstract
4908 ---------------------
4909 -- Remove_Ctrl_Arg --
4910 ---------------------
4912 function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result is
4914 if Nkind (N) = N_Function_Call
4915 and then Present (Controlling_Argument (N))
4916 and then not Is_Abstract_Subprogram (Entity (Name (N)))
4918 Set_Controlling_Argument (N, Empty);
4922 end Remove_Ctrl_Arg;
4924 procedure Remove_Ctrl_Args is new Traverse_Proc (Remove_Ctrl_Arg);
4926 Remove_Ctrl_Args (Expr);
4927 end Remove_Controlling_Arguments;
4929 -----------------------------------------
4930 -- Restore_Original_Selected_Component --
4931 -----------------------------------------
4933 procedure Restore_Original_Selected_Component is
4934 Restored_Nodes_List : Elist_Id := No_Elist;
4936 procedure Fix_Parents (N : Node_Id);
4937 -- Traverse the subtree of N fixing the Parent field of all the
4940 function Restore_Node (N : Node_Id) return Traverse_Result;
4941 -- Process dispatching calls to functions whose original node was
4942 -- a selected component, and replace them with their original
4943 -- node. Restored nodes are stored in the Restored_Nodes_List
4944 -- to fix the parent fields of their subtrees in a separate
4951 procedure Fix_Parents (N : Node_Id) is
4954 (Parent_Node : Node_Id;
4955 Node : Node_Id) return Traverse_Result;
4956 -- Process a single node
4963 (Parent_Node : Node_Id;
4964 Node : Node_Id) return Traverse_Result
4966 Par : constant Node_Id := Parent (Node);
4969 if Par /= Parent_Node then
4970 if Is_List_Member (Node) then
4971 Set_List_Parent (List_Containing (Node), Parent_Node);
4973 Set_Parent (Node, Parent_Node);
4980 procedure Fix_Parents is
4981 new Traverse_Proc_With_Parent (Fix_Parent);
4991 function Restore_Node (N : Node_Id) return Traverse_Result is
4993 if Nkind (N) = N_Function_Call
4994 and then Nkind (Original_Node (N)) = N_Selected_Component
4995 and then Is_Dispatching_Operation (Entity (Name (N)))
4997 Rewrite (N, Original_Node (N));
4998 Set_Original_Node (N, N);
5000 -- Save the restored node in the Restored_Nodes_List to fix
5001 -- the parent fields of their subtrees in a separate tree
5004 Append_New_Elmt (N, Restored_Nodes_List);
5010 procedure Restore_Nodes is new Traverse_Proc (Restore_Node);
5012 -- Start of processing for Restore_Original_Selected_Component
5015 Restore_Nodes (Expr);
5017 -- After restoring the original node we must fix the decoration
5018 -- of the Parent attribute to ensure tree consistency; required
5019 -- because when the class-wide condition is inherited, calls to
5020 -- New_Copy_Tree will perform copies of this subtree, and formal
5021 -- occurrences with wrong Parent field cannot be mapped to the
5024 if Present (Restored_Nodes_List) then
5026 Elmt : Elmt_Id := First_Elmt (Restored_Nodes_List);
5029 while Present (Elmt) loop
5030 Fix_Parents (Node (Elmt));
5035 end Restore_Original_Selected_Component;
5037 -- Start of processing for Preanalyze_Condition
5040 pragma Assert (Present (Expr));
5041 pragma Assert (Inside_Class_Condition_Preanalysis = False);
5044 Install_Formals (Subp);
5045 Inside_Class_Condition_Preanalysis := True;
5047 Preanalyze_Spec_Expression (Expr, Standard_Boolean);
5049 Inside_Class_Condition_Preanalysis := False;
5052 -- If this preanalyzed condition has occurrences of dispatching calls
5053 -- using the Object.Operation notation, during preanalysis such calls
5054 -- are rewritten as dispatching function calls; if at later stages
5055 -- this condition is inherited we must have restored the original
5056 -- selected-component node to ensure that the preanalysis of the
5057 -- inherited condition rewrites these dispatching calls in the
5058 -- correct context to avoid reporting spurious errors.
5060 Restore_Original_Selected_Component;
5062 -- Traverse Expr and clear the Controlling_Argument of calls to
5063 -- nonabstract functions. Required since the preanalyzed condition
5064 -- is not yet installed on its definite context and will be cloned
5065 -- and extended in derivations with additional conditions.
5067 Remove_Controlling_Arguments;
5069 -- Clear also attribute Unset_Reference; again because preanalysis
5070 -- occurs in a place unrelated to the actual code.
5072 Clear_Unset_References;
5073 end Preanalyze_Condition;
5075 ----------------------------------------
5076 -- Save_Global_References_In_Contract --
5077 ----------------------------------------
5079 procedure Save_Global_References_In_Contract
5083 procedure Save_Global_References_In_List (First_Prag : Node_Id);
5084 -- Save all global references in contract-related source pragmas found
5085 -- in the list, starting with pragma First_Prag.
5087 ------------------------------------
5088 -- Save_Global_References_In_List --
5089 ------------------------------------
5091 procedure Save_Global_References_In_List (First_Prag : Node_Id) is
5092 Prag : Node_Id := First_Prag;
5095 while Present (Prag) loop
5096 if Is_Generic_Contract_Pragma (Prag) then
5097 Save_Global_References (Prag);
5100 Prag := Next_Pragma (Prag);
5102 end Save_Global_References_In_List;
5106 Items : constant Node_Id := Contract (Defining_Entity (Templ));
5108 -- Start of processing for Save_Global_References_In_Contract
5111 -- The entity of the analyzed generic copy must be on the scope stack
5112 -- to ensure proper detection of global references.
5114 Push_Scope (Gen_Id);
5116 if Permits_Aspect_Specifications (Templ)
5117 and then Has_Aspects (Templ)
5119 Save_Global_References_In_Aspects (Templ);
5122 if Present (Items) then
5123 Save_Global_References_In_List (Pre_Post_Conditions (Items));
5124 Save_Global_References_In_List (Contract_Test_Cases (Items));
5125 Save_Global_References_In_List (Classifications (Items));
5129 end Save_Global_References_In_Contract;
5131 -------------------------
5132 -- Set_Class_Condition --
5133 -------------------------
5135 procedure Set_Class_Condition
5136 (Kind : Condition_Kind;
5142 when Class_Postcondition =>
5143 Set_Class_Postconditions (Subp, Cond);
5145 when Class_Precondition =>
5146 Set_Class_Preconditions (Subp, Cond);
5148 when Ignored_Class_Postcondition =>
5149 Set_Ignored_Class_Postconditions (Subp, Cond);
5151 when Ignored_Class_Precondition =>
5152 Set_Ignored_Class_Preconditions (Subp, Cond);
5154 end Set_Class_Condition;