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 Always_Terminates, Contract_Cases, Exceptional_Cases,
113 -- Subprogram_Variant, invariants and predicates. Body_Id denotes the
114 -- entity of the subprogram body.
116 procedure Preanalyze_Condition
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:
233 -- Extensions_Visible
239 -- Subprogram_Variant
243 elsif Is_Entry_Declaration
(Id
)
244 or else Ekind
(Id
) in E_Function
246 | E_Generic_Procedure
249 if Prag_Nam
in Name_Attach_Handler | Name_Interrupt_Handler
250 and then Ekind
(Id
) in E_Generic_Procedure | E_Procedure
254 elsif Prag_Nam
in Name_Depends
255 | Name_Extensions_Visible
261 elsif Prag_Nam
= Name_Volatile_Function
262 and then Ekind
(Id
) in E_Function | E_Generic_Function
266 elsif Prag_Nam
in Name_Always_Terminates
267 | Name_Contract_Cases
268 | Name_Exceptional_Cases
269 | Name_Subprogram_Variant
272 Add_Contract_Test_Case
;
274 elsif Prag_Nam
in Name_Postcondition | Name_Precondition
then
275 Add_Pre_Post_Condition
;
277 -- The pragma is not a proper contract item
280 raise Contract_Error
;
283 -- Packages or instantiations, the applicable pragmas are:
287 -- Part_Of (instantiation only)
289 elsif Is_Package_Or_Generic_Package
(Id
) then
290 if Prag_Nam
in Name_Abstract_State
291 | Name_Initial_Condition
296 -- Indicator Part_Of must be associated with a package instantiation
298 elsif Prag_Nam
= Name_Part_Of
and then Is_Generic_Instance
(Id
) then
301 elsif Prag_Nam
= Name_Always_Terminates
then
302 Add_Contract_Test_Case
;
304 -- The pragma is not a proper contract item
307 raise Contract_Error
;
310 -- Package bodies, the applicable pragmas are:
313 elsif Ekind
(Id
) = E_Package_Body
then
314 if Prag_Nam
= Name_Refined_State
then
317 -- The pragma is not a proper contract item
320 raise Contract_Error
;
323 -- The four volatility refinement pragmas are ok for all types.
324 -- Part_Of is ok for task types and protected types.
325 -- Depends and Global are ok for task types.
327 -- Precondition and Postcondition are added separately; they are allowed
328 -- for access-to-subprogram types.
330 elsif Is_Type
(Id
) then
332 Is_OK_Classification
: constant Boolean :=
333 Prag_Nam
in Name_Async_Readers
335 | Name_Effective_Reads
336 | Name_Effective_Writes
338 or else (Ekind
(Id
) = E_Task_Type
339 and Prag_Nam
in Name_Part_Of
342 or else (Ekind
(Id
) = E_Protected_Type
343 and Prag_Nam
= Name_Part_Of
);
346 if Is_OK_Classification
then
349 elsif Ekind
(Id
) = E_Subprogram_Type
350 and then Prag_Nam
in Name_Precondition
353 Add_Pre_Post_Condition
;
356 -- The pragma is not a proper contract item
358 raise Contract_Error
;
362 -- Subprogram bodies, the applicable pragmas are:
369 elsif Ekind
(Id
) = E_Subprogram_Body
then
370 if Prag_Nam
in Name_Refined_Depends | Name_Refined_Global
then
373 elsif Prag_Nam
in Name_Postcondition
377 Add_Pre_Post_Condition
;
379 -- The pragma is not a proper contract item
382 raise Contract_Error
;
385 -- Task bodies, the applicable pragmas are:
389 elsif Ekind
(Id
) = E_Task_Body
then
390 if Prag_Nam
in Name_Refined_Depends | Name_Refined_Global
then
393 -- The pragma is not a proper contract item
396 raise Contract_Error
;
399 -- Task units, the applicable pragmas are:
404 -- Variables, the applicable pragmas are:
407 -- Constant_After_Elaboration
415 elsif Ekind
(Id
) = E_Variable
then
416 if Prag_Nam
in Name_Async_Readers
418 | Name_Constant_After_Elaboration
420 | Name_Effective_Reads
421 | Name_Effective_Writes
428 -- The pragma is not a proper contract item
431 raise Contract_Error
;
435 raise Contract_Error
;
437 end Add_Contract_Item
;
439 -----------------------
440 -- Analyze_Contracts --
441 -----------------------
443 procedure Analyze_Contracts
(L
: List_Id
) is
448 while Present
(Decl
) loop
450 -- Entry or subprogram declarations
452 if Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
453 | N_Entry_Declaration
454 | N_Generic_Subprogram_Declaration
455 | N_Subprogram_Declaration
457 Analyze_Entry_Or_Subprogram_Contract
(Defining_Entity
(Decl
));
459 -- Entry or subprogram bodies
461 elsif Nkind
(Decl
) in N_Entry_Body | N_Subprogram_Body
then
462 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
466 elsif Nkind
(Decl
) = N_Object_Declaration
then
467 Analyze_Object_Contract
(Defining_Entity
(Decl
));
469 -- Package instantiation
471 elsif Nkind
(Decl
) = N_Package_Instantiation
then
472 Analyze_Package_Instantiation_Contract
(Defining_Entity
(Decl
));
476 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
477 | N_Single_Protected_Declaration
479 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
481 -- Subprogram body stubs
483 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
484 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
488 elsif Nkind
(Decl
) in N_Single_Task_Declaration
489 | N_Task_Type_Declaration
491 Analyze_Task_Contract
(Defining_Entity
(Decl
));
493 -- For type declarations, we need to do the preanalysis of Iterable
494 -- and the 3 Xxx_Literal aspect specifications.
496 -- Other type aspects need to be resolved here???
498 elsif Nkind
(Decl
) = N_Private_Type_Declaration
499 and then Present
(Aspect_Specifications
(Decl
))
502 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
503 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
504 I_Lit
: constant Node_Id
:=
505 Find_Aspect
(E
, Aspect_Integer_Literal
);
506 R_Lit
: constant Node_Id
:=
507 Find_Aspect
(E
, Aspect_Real_Literal
);
508 S_Lit
: constant Node_Id
:=
509 Find_Aspect
(E
, Aspect_String_Literal
);
513 Validate_Iterable_Aspect
(E
, It
);
516 if Present
(I_Lit
) then
517 Validate_Literal_Aspect
(E
, I_Lit
);
519 if Present
(R_Lit
) then
520 Validate_Literal_Aspect
(E
, R_Lit
);
522 if Present
(S_Lit
) then
523 Validate_Literal_Aspect
(E
, S_Lit
);
528 if Nkind
(Decl
) in N_Full_Type_Declaration
529 | N_Private_Type_Declaration
530 | N_Task_Type_Declaration
531 | N_Protected_Type_Declaration
532 | N_Formal_Type_Declaration
534 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
539 end Analyze_Contracts
;
541 -------------------------------------
542 -- Analyze_Pragmas_In_Declarations --
543 -------------------------------------
545 procedure Analyze_Pragmas_In_Declarations
(Body_Id
: Entity_Id
) is
549 -- Move through the body's declarations analyzing all pragmas which
550 -- appear at the top of the declarations.
552 Curr_Decl
:= First
(Declarations
(Unit_Declaration_Node
(Body_Id
)));
553 while Present
(Curr_Decl
) loop
555 if Nkind
(Curr_Decl
) = N_Pragma
then
557 if Pragma_Significant_To_Subprograms
558 (Get_Pragma_Id
(Curr_Decl
))
563 -- Skip the renamings of discriminants and protection fields
565 elsif Is_Prologue_Renaming
(Curr_Decl
) then
568 -- We have reached something which is not a pragma so we can be sure
569 -- there are no more contracts or pragmas which need to be taken into
578 end Analyze_Pragmas_In_Declarations
;
580 -----------------------------------------------
581 -- Analyze_Entry_Or_Subprogram_Body_Contract --
582 -----------------------------------------------
584 -- WARNING: This routine manages SPARK regions. Return statements must be
585 -- replaced by gotos which jump to the end of the routine and restore the
588 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
589 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
590 Items
: constant Node_Id
:= Contract
(Body_Id
);
591 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
594 -- When a subprogram body declaration is illegal, its defining entity is
595 -- left unanalyzed. There is nothing left to do in this case because the
596 -- body lacks a contract, or even a proper Ekind.
598 if Ekind
(Body_Id
) = E_Void
then
601 -- Do not analyze a contract multiple times
603 elsif Present
(Items
) then
604 if Analyzed
(Items
) then
607 Set_Analyzed
(Items
);
610 -- When this is a subprogram body not coming from source, for example an
611 -- expression function, it does not cause freezing of previous contracts
612 -- (see Analyze_Subprogram_Body_Helper), in particular not of those on
613 -- its spec if it exists. In this case make sure they have been properly
614 -- analyzed before being expanded below, as we may be invoked during the
615 -- freezing of the subprogram in the middle of its enclosing declarative
616 -- part because the declarative part contains e.g. the declaration of a
617 -- variable initialized by means of a call to the subprogram.
619 elsif Nkind
(Body_Decl
) = N_Subprogram_Body
620 and then not Comes_From_Source
(Original_Node
(Body_Decl
))
621 and then Present
(Corresponding_Spec
(Body_Decl
))
622 and then Present
(Contract
(Corresponding_Spec
(Body_Decl
)))
624 Analyze_Entry_Or_Subprogram_Contract
(Corresponding_Spec
(Body_Decl
));
627 -- Ensure that the contract cases or postconditions mention 'Result or
628 -- define a post-state.
630 Check_Result_And_Post_State
(Body_Id
);
632 -- Capture all global references in a generic subprogram body now that
633 -- the contract has been analyzed.
635 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
636 Save_Global_References_In_Contract
637 (Templ
=> Original_Node
(Body_Decl
),
641 -- Deal with preconditions, [refined] postconditions, Always_Terminates,
642 -- Contract_Cases, Exceptional_Cases, Subprogram_Variant, invariants and
643 -- predicates associated with body and its spec. Do not expand the
644 -- contract of subprogram body stubs.
646 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
647 Expand_Subprogram_Contract
(Body_Id
);
649 end Analyze_Entry_Or_Subprogram_Body_Contract
;
651 ------------------------------------------
652 -- Analyze_Entry_Or_Subprogram_Contract --
653 ------------------------------------------
655 -- WARNING: This routine manages SPARK regions. Return statements must be
656 -- replaced by gotos which jump to the end of the routine and restore the
659 procedure Analyze_Entry_Or_Subprogram_Contract
660 (Subp_Id
: Entity_Id
;
661 Freeze_Id
: Entity_Id
:= Empty
)
663 Items
: constant Node_Id
:= Contract
(Subp_Id
);
664 Subp_Decl
: constant Node_Id
:=
665 (if Ekind
(Subp_Id
) = E_Subprogram_Type
666 then Associated_Node_For_Itype
(Subp_Id
)
667 else Unit_Declaration_Node
(Subp_Id
));
669 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
670 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
671 -- Save the SPARK_Mode-related data to restore on exit
673 Skip_Assert_Exprs
: constant Boolean :=
674 Is_Entry
(Subp_Id
) and then not GNATprove_Mode
;
676 Depends
: Node_Id
:= Empty
;
677 Global
: Node_Id
:= Empty
;
682 -- Do not analyze a contract multiple times
684 if Present
(Items
) then
685 if Analyzed
(Items
) then
688 Set_Analyzed
(Items
);
692 -- Due to the timing of contract analysis, delayed pragmas may be
693 -- subject to the wrong SPARK_Mode, usually that of the enclosing
694 -- context. To remedy this, restore the original SPARK_Mode of the
695 -- related subprogram body.
697 Set_SPARK_Mode
(Subp_Id
);
699 -- All subprograms carry a contract, but for some it is not significant
700 -- and should not be processed.
702 if not Has_Significant_Contract
(Subp_Id
) then
705 elsif Present
(Items
) then
707 -- Do not analyze the pre/postconditions of an entry declaration
708 -- unless annotating the original tree for GNATprove. The
709 -- real analysis occurs when the pre/postconditons are relocated to
710 -- the contract wrapper procedure (see Build_Contract_Wrapper).
712 if Skip_Assert_Exprs
then
715 -- Otherwise analyze the pre/postconditions.
716 -- If these come from an aspect specification, their expressions
717 -- might include references to types that are not frozen yet, in the
718 -- case where the body is a rewritten expression function that is a
719 -- completion, so freeze all types within before constructing the
724 Bod
: Node_Id
:= Empty
;
725 Freeze_Types
: Boolean := False;
728 if Present
(Freeze_Id
) then
729 Bod
:= Unit_Declaration_Node
(Freeze_Id
);
731 if Nkind
(Bod
) = N_Subprogram_Body
732 and then Was_Expression_Function
(Bod
)
733 and then Ekind
(Subp_Id
) = E_Function
734 and then Chars
(Subp_Id
) = Chars
(Freeze_Id
)
735 and then Subp_Id
/= Freeze_Id
737 Freeze_Types
:= True;
741 Prag
:= Pre_Post_Conditions
(Items
);
742 while Present
(Prag
) loop
744 and then Present
(Corresponding_Aspect
(Prag
))
748 Typ
=> Standard_Boolean
,
751 (First
(Pragma_Argument_Associations
(Prag
))),
755 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
756 Prag
:= Next_Pragma
(Prag
);
761 -- Analyze contract-cases, subprogram-variant and test-cases
763 Prag
:= Contract_Test_Cases
(Items
);
764 while Present
(Prag
) loop
765 Prag_Nam
:= Pragma_Name
(Prag
);
767 if Prag_Nam
= Name_Always_Terminates
then
768 Analyze_Always_Terminates_In_Decl_Part
(Prag
);
770 elsif Prag_Nam
= Name_Contract_Cases
then
772 -- Do not analyze the contract cases of an entry declaration
773 -- unless annotating the original tree for GNATprove.
774 -- The real analysis occurs when the contract cases are moved
775 -- to the contract wrapper procedure (Build_Contract_Wrapper).
777 if Skip_Assert_Exprs
then
780 -- Otherwise analyze the contract cases
783 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
786 elsif Prag_Nam
= Name_Exceptional_Cases
then
787 Analyze_Exceptional_Cases_In_Decl_Part
(Prag
);
789 elsif Prag_Nam
= Name_Subprogram_Variant
then
790 Analyze_Subprogram_Variant_In_Decl_Part
(Prag
);
793 pragma Assert
(Prag_Nam
= Name_Test_Case
);
794 Analyze_Test_Case_In_Decl_Part
(Prag
);
797 Prag
:= Next_Pragma
(Prag
);
800 -- Analyze classification pragmas
802 Prag
:= Classifications
(Items
);
803 while Present
(Prag
) loop
804 Prag_Nam
:= Pragma_Name
(Prag
);
806 if Prag_Nam
= Name_Depends
then
809 elsif Prag_Nam
= Name_Global
then
813 Prag
:= Next_Pragma
(Prag
);
816 -- Analyze Global first, as Depends may mention items classified in
817 -- the global categorization.
819 if Present
(Global
) then
820 Analyze_Global_In_Decl_Part
(Global
);
823 -- Depends must be analyzed after Global in order to see the modes of
826 if Present
(Depends
) then
827 Analyze_Depends_In_Decl_Part
(Depends
);
830 -- Ensure that the contract cases or postconditions mention 'Result
831 -- or define a post-state.
833 Check_Result_And_Post_State
(Subp_Id
);
836 -- Restore the SPARK_Mode of the enclosing context after all delayed
837 -- pragmas have been analyzed.
839 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
841 -- Capture all global references in a generic subprogram now that the
842 -- contract has been analyzed.
844 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
845 Save_Global_References_In_Contract
846 (Templ
=> Original_Node
(Subp_Decl
),
849 end Analyze_Entry_Or_Subprogram_Contract
;
851 ----------------------------------------------
852 -- Check_Type_Or_Object_External_Properties --
853 ----------------------------------------------
855 procedure Check_Type_Or_Object_External_Properties
856 (Type_Or_Obj_Id
: Entity_Id
)
858 Is_Type_Id
: constant Boolean := Is_Type
(Type_Or_Obj_Id
);
862 AR_Val
: Boolean := False;
863 AW_Val
: Boolean := False;
864 ER_Val
: Boolean := False;
865 EW_Val
: Boolean := False;
867 Seen
: Boolean := False;
870 -- Start of processing for Check_Type_Or_Object_External_Properties
873 -- Analyze all external properties
876 -- If the parent type of a derived type is volatile
877 -- then the derived type inherits volatility-related flags.
879 if Is_Derived_Type
(Type_Or_Obj_Id
) then
881 Parent_Type
: constant Entity_Id
:=
882 Etype
(Base_Type
(Type_Or_Obj_Id
));
884 if Is_Effectively_Volatile
(Parent_Type
) then
885 AR_Val
:= Async_Readers_Enabled
(Parent_Type
);
886 AW_Val
:= Async_Writers_Enabled
(Parent_Type
);
887 ER_Val
:= Effective_Reads_Enabled
(Parent_Type
);
888 EW_Val
:= Effective_Writes_Enabled
(Parent_Type
);
894 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Readers
);
896 if Present
(Prag
) then
898 Saved_AR_Val
: constant Boolean := AR_Val
;
900 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
902 if Saved_AR_Val
and not AR_Val
then
904 ("illegal non-confirming Async_Readers specification",
910 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Writers
);
912 if Present
(Prag
) then
914 Saved_AW_Val
: constant Boolean := AW_Val
;
916 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
918 if Saved_AW_Val
and not AW_Val
then
920 ("illegal non-confirming Async_Writers specification",
926 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Reads
);
928 if Present
(Prag
) then
930 Saved_ER_Val
: constant Boolean := ER_Val
;
932 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
934 if Saved_ER_Val
and not ER_Val
then
936 ("illegal non-confirming Effective_Reads specification",
942 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Writes
);
944 if Present
(Prag
) then
946 Saved_EW_Val
: constant Boolean := EW_Val
;
948 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
950 if Saved_EW_Val
and not EW_Val
then
952 ("illegal non-confirming Effective_Writes specification",
958 -- Verify the mutual interaction of the various external properties.
959 -- For types and variables for which No_Caching is enabled, it has been
960 -- checked already that only False values for other external properties
964 and then not No_Caching_Enabled
(Type_Or_Obj_Id
)
966 Check_External_Properties
967 (Type_Or_Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
970 -- Analyze the non-external volatility property No_Caching
972 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_No_Caching
);
974 if Present
(Prag
) then
975 Analyze_External_Property_In_Decl_Part
(Prag
, NC_Val
);
977 end Check_Type_Or_Object_External_Properties
;
979 -----------------------------
980 -- Analyze_Object_Contract --
981 -----------------------------
983 -- WARNING: This routine manages SPARK regions. Return statements must be
984 -- replaced by gotos which jump to the end of the routine and restore the
987 procedure Analyze_Object_Contract
989 Freeze_Id
: Entity_Id
:= Empty
)
991 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
993 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
994 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
995 -- Save the SPARK_Mode-related data to restore on exit
1002 -- The loop parameter in an element iterator over a formal container
1003 -- is declared with an object declaration, but no contracts apply.
1005 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
1009 -- Do not analyze a contract multiple times
1011 Items
:= Contract
(Obj_Id
);
1013 if Present
(Items
) then
1014 if Analyzed
(Items
) then
1017 Set_Analyzed
(Items
);
1021 -- The anonymous object created for a single concurrent type inherits
1022 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
1023 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
1024 -- of the enclosing context. To remedy this, restore the original mode
1025 -- of the related anonymous object.
1027 if Is_Single_Concurrent_Object
(Obj_Id
)
1028 and then Present
(SPARK_Pragma
(Obj_Id
))
1030 Set_SPARK_Mode
(Obj_Id
);
1033 -- Checks related to external properties, same for constants and
1036 Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id
=> Obj_Id
);
1038 -- Constant-related checks
1040 if Ekind
(Obj_Id
) = E_Constant
then
1042 -- Analyze indicator Part_Of
1044 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1046 -- Check whether the lack of indicator Part_Of agrees with the
1047 -- placement of the constant with respect to the state space.
1050 Check_Missing_Part_Of
(Obj_Id
);
1053 -- Variable-related checks
1055 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
1057 -- The anonymous object created for a single task type carries
1058 -- pragmas Depends and Global of the type.
1060 if Is_Single_Task_Object
(Obj_Id
) then
1062 -- Analyze Global first, as Depends may mention items classified
1063 -- in the global categorization.
1065 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
1067 if Present
(Prag
) then
1068 Analyze_Global_In_Decl_Part
(Prag
);
1071 -- Depends must be analyzed after Global in order to see the modes
1072 -- of all global items.
1074 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
1076 if Present
(Prag
) then
1077 Analyze_Depends_In_Decl_Part
(Prag
);
1081 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1083 -- Analyze indicator Part_Of
1085 if Present
(Prag
) then
1086 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
1088 -- The variable is a constituent of a single protected/task type
1089 -- and behaves as a component of the type. Verify that references
1090 -- to the variable occur within the definition or body of the type
1093 if Present
(Encapsulating_State
(Obj_Id
))
1094 and then Is_Single_Concurrent_Object
1095 (Encapsulating_State
(Obj_Id
))
1096 and then Present
(Part_Of_References
(Obj_Id
))
1098 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
1099 while Present
(Ref_Elmt
) loop
1100 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
1101 Next_Elmt
(Ref_Elmt
);
1105 -- Otherwise check whether the lack of indicator Part_Of agrees with
1106 -- the placement of the variable with respect to the state space.
1109 Check_Missing_Part_Of
(Obj_Id
);
1115 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
1117 -- A Ghost object cannot be of a type that yields a synchronized
1118 -- object (SPARK RM 6.9(19)).
1120 if Yields_Synchronized_Object
(Obj_Typ
) then
1121 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
1123 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
1124 -- One exception to this is the object that represents the dispatch
1125 -- table of a Ghost tagged type, as the symbol needs to be exported.
1127 elsif Is_Exported
(Obj_Id
) then
1128 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
1130 elsif Is_Imported
(Obj_Id
) then
1131 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
1135 -- Restore the SPARK_Mode of the enclosing context after all delayed
1136 -- pragmas have been analyzed.
1138 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1139 end Analyze_Object_Contract
;
1141 -----------------------------------
1142 -- Analyze_Package_Body_Contract --
1143 -----------------------------------
1145 -- WARNING: This routine manages SPARK regions. Return statements must be
1146 -- replaced by gotos which jump to the end of the routine and restore the
1149 procedure Analyze_Package_Body_Contract
1150 (Body_Id
: Entity_Id
;
1151 Freeze_Id
: Entity_Id
:= Empty
)
1153 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1154 Items
: constant Node_Id
:= Contract
(Body_Id
);
1155 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
1157 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1158 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1159 -- Save the SPARK_Mode-related data to restore on exit
1161 Ref_State
: Node_Id
;
1164 -- Do not analyze a contract multiple times
1166 if Present
(Items
) then
1167 if Analyzed
(Items
) then
1170 Set_Analyzed
(Items
);
1174 -- Due to the timing of contract analysis, delayed pragmas may be
1175 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1176 -- context. To remedy this, restore the original SPARK_Mode of the
1177 -- related package body.
1179 Set_SPARK_Mode
(Body_Id
);
1181 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
1183 -- The analysis of pragma Refined_State detects whether the spec has
1184 -- abstract states available for refinement.
1186 if Present
(Ref_State
) then
1187 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
1190 -- Restore the SPARK_Mode of the enclosing context after all delayed
1191 -- pragmas have been analyzed.
1193 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1195 -- Capture all global references in a generic package body now that the
1196 -- contract has been analyzed.
1198 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1199 Save_Global_References_In_Contract
1200 (Templ
=> Original_Node
(Body_Decl
),
1203 end Analyze_Package_Body_Contract
;
1205 ------------------------------
1206 -- Analyze_Package_Contract --
1207 ------------------------------
1209 -- WARNING: This routine manages SPARK regions. Return statements must be
1210 -- replaced by gotos which jump to the end of the routine and restore the
1213 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1214 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1215 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1217 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1218 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1219 -- Save the SPARK_Mode-related data to restore on exit
1221 Init
: Node_Id
:= Empty
;
1222 Init_Cond
: Node_Id
:= Empty
;
1227 -- Do not analyze a contract multiple times
1229 if Present
(Items
) then
1230 if Analyzed
(Items
) then
1233 -- Do not analyze the contract of the internal package
1234 -- created to check conformance of an actual package.
1235 -- Such an internal package is removed from the tree after
1236 -- legality checks are completed, and it does not contain
1237 -- the declarations of all local entities of the generic.
1239 elsif Is_Internal
(Pack_Id
)
1240 and then Is_Generic_Instance
(Pack_Id
)
1245 Set_Analyzed
(Items
);
1249 -- Due to the timing of contract analysis, delayed pragmas may be
1250 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1251 -- context. To remedy this, restore the original SPARK_Mode of the
1254 Set_SPARK_Mode
(Pack_Id
);
1256 if Present
(Items
) then
1258 -- Locate and store pragmas Initial_Condition and Initializes, since
1259 -- their order of analysis matters.
1261 Prag
:= Classifications
(Items
);
1262 while Present
(Prag
) loop
1263 Prag_Nam
:= Pragma_Name
(Prag
);
1265 if Prag_Nam
= Name_Initial_Condition
then
1268 elsif Prag_Nam
= Name_Initializes
then
1272 Prag
:= Next_Pragma
(Prag
);
1275 -- Analyze the initialization-related pragmas. Initializes must come
1276 -- before Initial_Condition due to item dependencies.
1278 if Present
(Init
) then
1279 Analyze_Initializes_In_Decl_Part
(Init
);
1282 if Present
(Init_Cond
) then
1283 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1287 -- Restore the SPARK_Mode of the enclosing context after all delayed
1288 -- pragmas have been analyzed.
1290 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1292 -- Capture all global references in a generic package now that the
1293 -- contract has been analyzed.
1295 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1296 Save_Global_References_In_Contract
1297 (Templ
=> Original_Node
(Pack_Decl
),
1300 end Analyze_Package_Contract
;
1302 --------------------------------------------
1303 -- Analyze_Package_Instantiation_Contract --
1304 --------------------------------------------
1306 -- WARNING: This routine manages SPARK regions. Return statements must be
1307 -- replaced by gotos which jump to the end of the routine and restore the
1310 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
) is
1311 Inst_Spec
: constant Node_Id
:=
1312 Instance_Spec
(Unit_Declaration_Node
(Inst_Id
));
1314 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1315 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1316 -- Save the SPARK_Mode-related data to restore on exit
1318 Pack_Id
: Entity_Id
;
1322 -- Nothing to do when the package instantiation is erroneous or left
1323 -- partially decorated.
1325 if No
(Inst_Spec
) then
1329 Pack_Id
:= Defining_Entity
(Inst_Spec
);
1330 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1332 -- Due to the timing of contract analysis, delayed pragmas may be
1333 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1334 -- context. To remedy this, restore the original SPARK_Mode of the
1337 Set_SPARK_Mode
(Pack_Id
);
1339 -- Check whether the lack of indicator Part_Of agrees with the placement
1340 -- of the package instantiation with respect to the state space. Nested
1341 -- package instantiations do not need to be checked because they inherit
1342 -- Part_Of indicator of the outermost package instantiation (see routine
1343 -- Propagate_Part_Of in Sem_Prag).
1348 elsif No
(Prag
) then
1349 Check_Missing_Part_Of
(Pack_Id
);
1352 -- Restore the SPARK_Mode of the enclosing context after all delayed
1353 -- pragmas have been analyzed.
1355 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1356 end Analyze_Package_Instantiation_Contract
;
1358 --------------------------------
1359 -- Analyze_Protected_Contract --
1360 --------------------------------
1362 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1363 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1366 -- Do not analyze a contract multiple times
1368 if Present
(Items
) then
1369 if Analyzed
(Items
) then
1372 Set_Analyzed
(Items
);
1375 end Analyze_Protected_Contract
;
1377 -------------------------------------------
1378 -- Analyze_Subprogram_Body_Stub_Contract --
1379 -------------------------------------------
1381 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1382 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1383 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1386 -- A subprogram body stub may act as its own spec or as the completion
1387 -- of a previous declaration. Depending on the context, the contract of
1388 -- the stub may contain two sets of pragmas.
1390 -- The stub is a completion, the applicable pragmas are:
1394 if Present
(Spec_Id
) then
1395 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1397 -- The stub acts as its own spec, the applicable pragmas are:
1398 -- Always_Terminates
1401 -- Exceptional_Cases
1405 -- Subprogram_Variant
1409 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1411 end Analyze_Subprogram_Body_Stub_Contract
;
1413 ---------------------------
1414 -- Analyze_Task_Contract --
1415 ---------------------------
1417 -- WARNING: This routine manages SPARK regions. Return statements must be
1418 -- replaced by gotos which jump to the end of the routine and restore the
1421 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1422 Items
: constant Node_Id
:= Contract
(Task_Id
);
1424 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1425 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1426 -- Save the SPARK_Mode-related data to restore on exit
1431 -- Do not analyze a contract multiple times
1433 if Present
(Items
) then
1434 if Analyzed
(Items
) then
1437 Set_Analyzed
(Items
);
1441 -- Due to the timing of contract analysis, delayed pragmas may be
1442 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1443 -- context. To remedy this, restore the original SPARK_Mode of the
1444 -- related task unit.
1446 Set_SPARK_Mode
(Task_Id
);
1448 -- Analyze Global first, as Depends may mention items classified in the
1449 -- global categorization.
1451 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1453 if Present
(Prag
) then
1454 Analyze_Global_In_Decl_Part
(Prag
);
1457 -- Depends must be analyzed after Global in order to see the modes of
1458 -- all global items.
1460 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1462 if Present
(Prag
) then
1463 Analyze_Depends_In_Decl_Part
(Prag
);
1466 -- Restore the SPARK_Mode of the enclosing context after all delayed
1467 -- pragmas have been analyzed.
1469 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1470 end Analyze_Task_Contract
;
1472 ---------------------------
1473 -- Analyze_Type_Contract --
1474 ---------------------------
1476 procedure Analyze_Type_Contract
(Type_Id
: Entity_Id
) is
1478 Check_Type_Or_Object_External_Properties
1479 (Type_Or_Obj_Id
=> Type_Id
);
1481 -- Analyze Pre/Post on access-to-subprogram type
1483 if Ekind
(Type_Id
) in Access_Subprogram_Kind
then
1484 Analyze_Entry_Or_Subprogram_Contract
1485 (Directly_Designated_Type
(Type_Id
));
1487 end Analyze_Type_Contract
;
1489 ---------------------------------------
1490 -- Build_Subprogram_Contract_Wrapper --
1491 ---------------------------------------
1493 procedure Build_Subprogram_Contract_Wrapper
1494 (Body_Id
: Entity_Id
;
1499 Body_Decl
: constant Entity_Id
:= Unit_Declaration_Node
(Body_Id
);
1500 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
1501 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1502 Subp_Id
: Entity_Id
;
1503 Ret_Type
: Entity_Id
;
1505 Wrapper_Id
: Entity_Id
;
1506 Wrapper_Body
: Node_Id
;
1507 Wrapper_Spec
: Node_Id
;
1510 -- When there are no postcondition statements we do not need to
1511 -- generate a wrapper.
1517 -- Obtain the related subprogram id from the body id.
1519 if Present
(Spec_Id
) then
1524 Ret_Type
:= Etype
(Subp_Id
);
1526 -- Generate the contracts wrapper by moving the original declarations
1527 -- and statements within a local subprogram, calling it and possibly
1528 -- preserving the result for the purpose of evaluating postconditions,
1529 -- contracts, type invariants, etc.
1531 -- In the case of a function, generate:
1533 -- function Original_Func (X : in out Integer) return Typ is
1534 -- <prologue renamings>
1537 -- function _Wrapped_Statements return Typ is
1538 -- <original declarations>
1540 -- <original statements>
1545 -- Result_Obj : constant Typ := _Wrapped_Statements
1547 -- <postconditions statements>
1551 -- Or else, in the case of a procedure, generate:
1553 -- procedure Original_Proc (X : in out Integer) is
1554 -- <prologue renamings>
1557 -- procedure _Wrapped_Statements is
1558 -- <original declarations>
1560 -- <original statements>
1564 -- _Wrapped_Statements;
1565 -- <postconditions statements>
1568 -- Create Identifier
1570 Wrapper_Id
:= Make_Defining_Identifier
(Loc
, Name_uWrapped_Statements
);
1571 Set_Debug_Info_Needed
(Wrapper_Id
);
1572 Set_Wrapped_Statements
(Subp_Id
, Wrapper_Id
);
1574 Set_Has_Pragma_Inline
(Wrapper_Id
, Has_Pragma_Inline
(Subp_Id
));
1575 Set_Has_Pragma_Inline_Always
1576 (Wrapper_Id
, Has_Pragma_Inline_Always
(Subp_Id
));
1578 -- Create specification and declaration for the wrapper
1580 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1582 Make_Procedure_Specification
(Loc
,
1583 Defining_Unit_Name
=> Wrapper_Id
);
1586 Make_Function_Specification
(Loc
,
1587 Defining_Unit_Name
=> Wrapper_Id
,
1588 Result_Definition
=> New_Occurrence_Of
(Ret_Type
, Loc
));
1591 -- Create the wrapper body using Body_Id's statements and declarations
1594 Make_Subprogram_Body
(Loc
,
1595 Specification
=> Wrapper_Spec
,
1596 Declarations
=> Declarations
(Body_Decl
),
1597 Handled_Statement_Sequence
=>
1598 Relocate_Node
(Handled_Statement_Sequence
(Body_Decl
)));
1600 Append_To
(Decls
, Wrapper_Body
);
1601 Set_Declarations
(Body_Decl
, Decls
);
1602 Set_Handled_Statement_Sequence
(Body_Decl
,
1603 Make_Handled_Sequence_Of_Statements
(Loc
,
1604 End_Label
=> Make_Identifier
(Loc
, Chars
(Wrapper_Id
))));
1606 -- Prepend a call to the wrapper when the subprogram is a procedure
1608 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1610 Make_Procedure_Call_Statement
(Loc
,
1611 Name
=> New_Occurrence_Of
(Wrapper_Id
, Loc
)));
1613 (Handled_Statement_Sequence
(Body_Decl
), Stmts
);
1615 -- Generate the post-execution statements and the extended return
1616 -- when the subprogram being wrapped is a function.
1619 Set_Statements
(Handled_Statement_Sequence
(Body_Decl
), New_List
(
1620 Make_Extended_Return_Statement
(Loc
,
1621 Return_Object_Declarations
=> New_List
(
1622 Make_Object_Declaration
(Loc
,
1623 Defining_Identifier
=> Result
,
1624 Constant_Present
=> True,
1625 Object_Definition
=>
1626 New_Occurrence_Of
(Ret_Type
, Loc
),
1628 Make_Function_Call
(Loc
,
1630 New_Occurrence_Of
(Wrapper_Id
, Loc
)))),
1631 Handled_Statement_Sequence
=>
1632 Make_Handled_Sequence_Of_Statements
(Loc
,
1633 Statements
=> Stmts
))));
1635 end Build_Subprogram_Contract_Wrapper
;
1637 ----------------------------------
1638 -- Build_Entry_Contract_Wrapper --
1639 ----------------------------------
1641 procedure Build_Entry_Contract_Wrapper
(E
: Entity_Id
; Decl
: Node_Id
) is
1642 Conc_Typ
: constant Entity_Id
:= Scope
(E
);
1643 Loc
: constant Source_Ptr
:= Sloc
(E
);
1645 procedure Add_Discriminant_Renamings
1646 (Obj_Id
: Entity_Id
;
1648 -- Add renaming declarations for all discriminants of concurrent type
1649 -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
1650 -- represents the concurrent object.
1652 procedure Add_Matching_Formals
1654 Actuals
: in out List_Id
);
1655 -- Add formal parameters that match those of entry E to list Formals.
1656 -- The routine also adds matching actuals for the new formals to list
1659 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
);
1660 -- Relocate pragma Prag to list To. The routine creates a new list if
1661 -- To does not exist.
1663 --------------------------------
1664 -- Add_Discriminant_Renamings --
1665 --------------------------------
1667 procedure Add_Discriminant_Renamings
1668 (Obj_Id
: Entity_Id
;
1672 Renaming_Decl
: Node_Id
;
1675 -- Inspect the discriminants of the concurrent type and generate a
1676 -- renaming for each one.
1678 if Has_Discriminants
(Conc_Typ
) then
1679 Discr
:= First_Discriminant
(Conc_Typ
);
1680 while Present
(Discr
) loop
1682 Make_Object_Renaming_Declaration
(Loc
,
1683 Defining_Identifier
=>
1684 Make_Defining_Identifier
(Loc
, Chars
(Discr
)),
1686 New_Occurrence_Of
(Etype
(Discr
), Loc
),
1688 Make_Selected_Component
(Loc
,
1689 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
1691 Make_Identifier
(Loc
, Chars
(Discr
))));
1693 Prepend_To
(Decls
, Renaming_Decl
);
1695 Next_Discriminant
(Discr
);
1698 end Add_Discriminant_Renamings
;
1700 --------------------------
1701 -- Add_Matching_Formals --
1702 --------------------------
1704 procedure Add_Matching_Formals
1706 Actuals
: in out List_Id
)
1709 New_Formal
: Entity_Id
;
1712 -- Inspect the formal parameters of the entry and generate a new
1713 -- matching formal with the same name for the wrapper. A reference
1714 -- to the new formal becomes an actual in the entry call.
1716 Formal
:= First_Formal
(E
);
1717 while Present
(Formal
) loop
1718 New_Formal
:= Make_Defining_Identifier
(Loc
, Chars
(Formal
));
1720 Make_Parameter_Specification
(Loc
,
1721 Defining_Identifier
=> New_Formal
,
1722 In_Present
=> In_Present
(Parent
(Formal
)),
1723 Out_Present
=> Out_Present
(Parent
(Formal
)),
1725 New_Occurrence_Of
(Etype
(Formal
), Loc
)));
1727 if No
(Actuals
) then
1728 Actuals
:= New_List
;
1731 Append_To
(Actuals
, New_Occurrence_Of
(New_Formal
, Loc
));
1732 Next_Formal
(Formal
);
1734 end Add_Matching_Formals
;
1736 ---------------------
1737 -- Transfer_Pragma --
1738 ---------------------
1740 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
) is
1748 New_Prag
:= Relocate_Node
(Prag
);
1750 Set_Analyzed
(New_Prag
, False);
1751 Append
(New_Prag
, To
);
1752 end Transfer_Pragma
;
1756 Items
: constant Node_Id
:= Contract
(E
);
1757 Actuals
: List_Id
:= No_List
;
1760 Decls
: List_Id
:= No_List
;
1762 Has_Pragma
: Boolean := False;
1763 Index_Id
: Entity_Id
;
1766 Wrapper_Id
: Entity_Id
;
1768 -- Start of processing for Build_Entry_Contract_Wrapper
1771 -- This routine generates a specialized wrapper for a protected or task
1772 -- entry [family] which implements precondition/postcondition semantics.
1773 -- Preconditions and case guards of contract cases are checked before
1774 -- the protected action or rendezvous takes place.
1776 -- procedure Wrapper
1777 -- (Obj_Id : Conc_Typ; -- concurrent object
1778 -- [Index : Index_Typ;] -- index of entry family
1779 -- [Formal_1 : ...; -- parameters of original entry
1782 -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
1783 -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
1785 -- <contracts pragmas>
1786 -- <case guard checks>
1789 -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
1792 -- Create the wrapper only when the entry has at least one executable
1793 -- contract item such as contract cases, precondition or postcondition.
1795 if Present
(Items
) then
1797 -- Inspect the list of pre/postconditions and transfer all available
1798 -- pragmas to the declarative list of the wrapper.
1800 Prag
:= Pre_Post_Conditions
(Items
);
1801 while Present
(Prag
) loop
1802 if Pragma_Name_Unmapped
(Prag
) in Name_Postcondition
1804 and then Is_Checked
(Prag
)
1807 Transfer_Pragma
(Prag
, To
=> Decls
);
1810 Prag
:= Next_Pragma
(Prag
);
1813 -- Inspect the list of test/contract cases and transfer only contract
1814 -- cases pragmas to the declarative part of the wrapper.
1816 Prag
:= Contract_Test_Cases
(Items
);
1817 while Present
(Prag
) loop
1818 if Pragma_Name
(Prag
) = Name_Contract_Cases
1819 and then Is_Checked
(Prag
)
1822 Transfer_Pragma
(Prag
, To
=> Decls
);
1825 Prag
:= Next_Pragma
(Prag
);
1829 -- The entry lacks executable contract items and a wrapper is not needed
1831 if not Has_Pragma
then
1835 -- Create the profile of the wrapper. The first formal parameter is the
1836 -- concurrent object.
1839 Make_Defining_Identifier
(Loc
,
1840 Chars
=> New_External_Name
(Chars
(Conc_Typ
), 'A'));
1842 Formals
:= New_List
(
1843 Make_Parameter_Specification
(Loc
,
1844 Defining_Identifier
=> Obj_Id
,
1845 Out_Present
=> True,
1847 Parameter_Type
=> New_Occurrence_Of
(Conc_Typ
, Loc
)));
1849 -- Construct the call to the original entry. The call will be gradually
1850 -- augmented with an optional entry index and extra parameters.
1853 Make_Selected_Component
(Loc
,
1854 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
1855 Selector_Name
=> New_Occurrence_Of
(E
, Loc
));
1857 -- When creating a wrapper for an entry family, the second formal is the
1860 if Ekind
(E
) = E_Entry_Family
then
1861 Index_Id
:= Make_Defining_Identifier
(Loc
, Name_I
);
1864 Make_Parameter_Specification
(Loc
,
1865 Defining_Identifier
=> Index_Id
,
1867 New_Occurrence_Of
(Entry_Index_Type
(E
), Loc
)));
1869 -- The call to the original entry becomes an indexed component to
1870 -- accommodate the entry index.
1873 Make_Indexed_Component
(Loc
,
1875 Expressions
=> New_List
(New_Occurrence_Of
(Index_Id
, Loc
)));
1878 -- Add formal parameters to match those of the entry and build actuals
1879 -- for the entry call.
1881 Add_Matching_Formals
(Formals
, Actuals
);
1884 Make_Procedure_Call_Statement
(Loc
,
1886 Parameter_Associations
=> Actuals
);
1888 -- Add renaming declarations for the discriminants of the enclosing type
1889 -- as the various contract items may reference them.
1891 Add_Discriminant_Renamings
(Obj_Id
, Decls
);
1894 Make_Defining_Identifier
(Loc
, New_External_Name
(Chars
(E
), 'E'));
1895 Set_Contract_Wrapper
(E
, Wrapper_Id
);
1896 Set_Is_Entry_Wrapper
(Wrapper_Id
);
1898 -- The wrapper body is analyzed when the enclosing type is frozen
1900 Append_Freeze_Action
(Defining_Entity
(Decl
),
1901 Make_Subprogram_Body
(Loc
,
1903 Make_Procedure_Specification
(Loc
,
1904 Defining_Unit_Name
=> Wrapper_Id
,
1905 Parameter_Specifications
=> Formals
),
1906 Declarations
=> Decls
,
1907 Handled_Statement_Sequence
=>
1908 Make_Handled_Sequence_Of_Statements
(Loc
,
1909 Statements
=> New_List
(Call
))));
1910 end Build_Entry_Contract_Wrapper
;
1912 ---------------------------
1913 -- Check_Class_Condition --
1914 ---------------------------
1916 procedure Check_Class_Condition
1919 Par_Subp
: Entity_Id
;
1920 Is_Precondition
: Boolean)
1922 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
1923 -- Check reference to formal of inherited operation or to primitive
1924 -- operation of root type.
1930 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
1935 if Nkind
(N
) = N_Identifier
1936 and then Present
(Entity
(N
))
1938 (Is_Formal
(Entity
(N
)) or else Is_Subprogram
(Entity
(N
)))
1940 (Nkind
(Parent
(N
)) /= N_Attribute_Reference
1941 or else Attribute_Name
(Parent
(N
)) /= Name_Class
)
1943 -- These checks do not apply to dispatching calls within the
1944 -- condition, but only to calls whose static tag is that of
1947 if Is_Subprogram
(Entity
(N
))
1948 and then Nkind
(Parent
(N
)) = N_Function_Call
1949 and then Present
(Controlling_Argument
(Parent
(N
)))
1954 -- Determine whether entity has a renaming
1956 Orig_E
:= Entity
(N
);
1957 New_E
:= Get_Mapped_Entity
(Orig_E
);
1959 if Present
(New_E
) then
1961 -- AI12-0166: A precondition for a protected operation
1962 -- cannot include an internal call to a protected function
1963 -- of the type. In the case of an inherited condition for an
1964 -- overriding operation, both the operation and the function
1965 -- are given by primitive wrappers.
1968 and then Ekind
(New_E
) = E_Function
1969 and then Is_Primitive_Wrapper
(New_E
)
1970 and then Is_Primitive_Wrapper
(Subp
)
1971 and then Scope
(Subp
) = Scope
(New_E
)
1973 Error_Msg_Node_2
:= Wrapped_Entity
(Subp
);
1975 ("internal call to& cannot appear in inherited "
1976 & "precondition of protected operation&",
1977 Subp
, Wrapped_Entity
(New_E
));
1981 -- Check that there are no calls left to abstract operations if
1982 -- the current subprogram is not abstract.
1985 and then Nkind
(Parent
(N
)) = N_Function_Call
1986 and then N
= Name
(Parent
(N
))
1988 if not Is_Abstract_Subprogram
(Subp
)
1989 and then Is_Abstract_Subprogram
(New_E
)
1991 Error_Msg_Sloc
:= Sloc
(Current_Scope
);
1992 Error_Msg_Node_2
:= Subp
;
1994 if Comes_From_Source
(Subp
) then
1996 ("cannot call abstract subprogram & in inherited "
1997 & "condition for&#", Subp
, New_E
);
2000 ("cannot call abstract subprogram & in inherited "
2001 & "condition for inherited&#", Subp
, New_E
);
2004 -- In SPARK mode, report error on inherited condition for an
2005 -- inherited operation if it contains a call to an overriding
2006 -- operation, because this implies that the pre/postconditions
2007 -- of the inherited operation have changed silently.
2009 elsif SPARK_Mode
= On
2010 and then Warn_On_Suspicious_Contract
2011 and then Present
(Alias
(Subp
))
2012 and then Present
(New_E
)
2013 and then Comes_From_Source
(New_E
)
2016 ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
2018 Error_Msg_Sloc
:= Sloc
(New_E
);
2019 Error_Msg_Node_2
:= Subp
;
2021 ("\overriding of&# forces overriding of&",
2022 Parent
(Subp
), New_E
);
2030 procedure Check_Condition_Entities
is
2031 new Traverse_Proc
(Check_Entity
);
2033 -- Start of processing for Check_Class_Condition
2036 -- No check required if the subprograms match
2038 if Par_Subp
= Subp
then
2042 Update_Primitives_Mapping
(Par_Subp
, Subp
);
2043 Map_Formals
(Par_Subp
, Subp
);
2044 Check_Condition_Entities
(Cond
);
2045 end Check_Class_Condition
;
2047 -----------------------------
2048 -- Create_Generic_Contract --
2049 -----------------------------
2051 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
2052 Templ
: constant Node_Id
:= Original_Node
(Unit
);
2053 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
2055 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
2056 -- Add a single contract-related source pragma Prag to the contract of
2057 -- generic template Templ_Id.
2059 ---------------------------------
2060 -- Add_Generic_Contract_Pragma --
2061 ---------------------------------
2063 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
2064 Prag_Templ
: Node_Id
;
2067 -- Mark the pragma to prevent the premature capture of global
2068 -- references when capturing global references of the context
2069 -- (see Save_References_In_Pragma).
2071 Set_Is_Generic_Contract_Pragma
(Prag
);
2073 -- Pragmas that apply to a generic subprogram declaration are not
2074 -- part of the semantic structure of the generic template:
2077 -- procedure Example (Formal : Integer);
2078 -- pragma Precondition (Formal > 0);
2080 -- Create a generic template for such pragmas and link the template
2081 -- of the pragma with the generic template.
2083 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2085 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
2086 Prag_Templ
:= Original_Node
(Prag
);
2088 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
2089 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
2091 -- Otherwise link the pragma with the generic template
2094 Add_Contract_Item
(Prag
, Templ_Id
);
2098 -- We do not stop the compilation at this point in the case of an
2099 -- invalid pragma because it will be properly diagnosed afterward.
2101 when Contract_Error
=> null;
2102 end Add_Generic_Contract_Pragma
;
2106 Context
: constant Node_Id
:= Parent
(Unit
);
2107 Decl
: Node_Id
:= Empty
;
2109 -- Start of processing for Create_Generic_Contract
2112 -- A generic package declaration carries contract-related source pragmas
2113 -- in its visible declarations.
2115 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
2116 Mutate_Ekind
(Templ_Id
, E_Generic_Package
);
2118 if Present
(Visible_Declarations
(Specification
(Templ
))) then
2119 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
2122 -- A generic package body carries contract-related source pragmas in its
2125 elsif Nkind
(Templ
) = N_Package_Body
then
2126 Mutate_Ekind
(Templ_Id
, E_Package_Body
);
2128 if Present
(Declarations
(Templ
)) then
2129 Decl
:= First
(Declarations
(Templ
));
2132 -- Generic subprogram declaration
2134 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2135 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
2136 Mutate_Ekind
(Templ_Id
, E_Generic_Function
);
2138 Mutate_Ekind
(Templ_Id
, E_Generic_Procedure
);
2141 -- When the generic subprogram acts as a compilation unit, inspect
2142 -- the Pragmas_After list for contract-related source pragmas.
2144 if Nkind
(Context
) = N_Compilation_Unit
then
2145 if Present
(Aux_Decls_Node
(Context
))
2146 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
2148 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
2151 -- Otherwise inspect the successive declarations for contract-related
2155 Decl
:= Next
(Unit
);
2158 -- A generic subprogram body carries contract-related source pragmas in
2159 -- its declarations.
2161 elsif Nkind
(Templ
) = N_Subprogram_Body
then
2162 Mutate_Ekind
(Templ_Id
, E_Subprogram_Body
);
2164 if Present
(Declarations
(Templ
)) then
2165 Decl
:= First
(Declarations
(Templ
));
2169 -- Inspect the relevant declarations looking for contract-related source
2170 -- pragmas and add them to the contract of the generic unit.
2172 while Present
(Decl
) loop
2173 if Comes_From_Source
(Decl
) then
2174 if Nkind
(Decl
) = N_Pragma
then
2176 -- The source pragma is a contract annotation
2178 if Is_Contract_Annotation
(Decl
) then
2179 Add_Generic_Contract_Pragma
(Decl
);
2182 -- The region where a contract-related source pragma may appear
2183 -- ends with the first source non-pragma declaration or statement.
2192 end Create_Generic_Contract
;
2194 --------------------------------
2195 -- Expand_Subprogram_Contract --
2196 --------------------------------
2198 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
2199 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
2200 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
2202 procedure Add_Invariant_And_Predicate_Checks
2203 (Subp_Id
: Entity_Id
;
2204 Stmts
: in out List_Id
;
2205 Result
: out Node_Id
);
2206 -- Process the result of function Subp_Id (if applicable) and all its
2207 -- formals. Add invariant and predicate checks where applicable. The
2208 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
2209 -- function, Result contains the entity of parameter _Result, to be
2210 -- used in the creation of procedure _Postconditions.
2212 procedure Add_Stable_Property_Contracts
2213 (Subp_Id
: Entity_Id
; Class_Present
: Boolean);
2214 -- Augment postcondition contracts to reflect Stable_Property aspect
2215 -- (if Class_Present = False) or Stable_Property'Class aspect (if
2216 -- Class_Present = True).
2218 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
2219 -- Append a node to a list. If there is no list, create a new one. When
2220 -- the item denotes a pragma, it is added to the list only when it is
2223 procedure Process_Contract_Cases
2224 (Stmts
: in out List_Id
;
2226 -- Process pragma Contract_Cases. This routine prepends items to the
2227 -- body declarations and appends items to list Stmts.
2229 procedure Process_Postconditions
(Stmts
: in out List_Id
);
2230 -- Collect all [inherited] spec and body postconditions and accumulate
2231 -- their pragma Check equivalents in list Stmts.
2233 procedure Process_Preconditions
(Decls
: in out List_Id
);
2234 -- Collect all [inherited] spec and body preconditions and prepend their
2235 -- pragma Check equivalents to the declarations of the body.
2237 ----------------------------------------
2238 -- Add_Invariant_And_Predicate_Checks --
2239 ----------------------------------------
2241 procedure Add_Invariant_And_Predicate_Checks
2242 (Subp_Id
: Entity_Id
;
2243 Stmts
: in out List_Id
;
2244 Result
: out Node_Id
)
2246 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
2247 -- Id denotes the return value of a function or a formal parameter.
2248 -- Add an invariant check if the type of Id is access to a type with
2249 -- invariants. The routine appends the generated code to Stmts.
2251 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
2252 -- Determine whether type Typ can benefit from invariant checks. To
2253 -- qualify, the type must have a non-null invariant procedure and
2254 -- subprogram Subp_Id must appear visible from the point of view of
2257 ---------------------------------
2258 -- Add_Invariant_Access_Checks --
2259 ---------------------------------
2261 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
2262 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2269 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
2270 Typ
:= Designated_Type
(Typ
);
2272 if Invariant_Checks_OK
(Typ
) then
2274 Make_Explicit_Dereference
(Loc
,
2275 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
2276 Set_Etype
(Ref
, Typ
);
2279 -- if <Id> /= null then
2280 -- <invariant_call (<Ref>)>
2285 Make_If_Statement
(Loc
,
2288 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
2289 Right_Opnd
=> Make_Null
(Loc
)),
2290 Then_Statements
=> New_List
(
2291 Make_Invariant_Call
(Ref
))),
2295 end Add_Invariant_Access_Checks
;
2297 -------------------------
2298 -- Invariant_Checks_OK --
2299 -------------------------
2301 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
2302 function Has_Public_Visibility_Of_Subprogram
return Boolean;
2303 -- Determine whether type Typ has public visibility of subprogram
2306 -----------------------------------------
2307 -- Has_Public_Visibility_Of_Subprogram --
2308 -----------------------------------------
2310 function Has_Public_Visibility_Of_Subprogram
return Boolean is
2311 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2314 -- An Initialization procedure must be considered visible even
2315 -- though it is internally generated.
2317 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2320 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2323 -- Internally generated code is never publicly visible except
2324 -- for a subprogram that is the implementation of an expression
2325 -- function. In that case the visibility is determined by the
2328 elsif not Comes_From_Source
(Subp_Decl
)
2330 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2332 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2336 -- Determine whether the subprogram is declared in the visible
2337 -- declarations of the package containing the type, or in the
2338 -- visible declaration of a child unit of that package.
2340 elsif Is_List_Member
(Subp_Decl
) then
2342 Decls
: constant List_Id
:=
2343 List_Containing
(Subp_Decl
);
2344 Subp_Scope
: constant Entity_Id
:=
2345 Scope
(Defining_Entity
(Subp_Decl
));
2346 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2350 Decls
= Visible_Declarations
2351 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2354 (Ekind
(Subp_Scope
) = E_Package
2355 and then Typ_Scope
/= Subp_Scope
2356 and then Is_Child_Unit
(Subp_Scope
)
2358 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2360 Decls
= Visible_Declarations
2362 (Unit_Declaration_Node
(Subp_Scope
))));
2365 -- Determine whether the subprogram is a child subprogram of
2366 -- of the package containing the type.
2370 (Nkind
(Parent
(Subp_Decl
)) = N_Compilation_Unit
);
2373 Subp_Scope
: constant Entity_Id
:=
2374 Scope
(Defining_Entity
(Subp_Decl
));
2375 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2379 Ekind
(Subp_Scope
) = E_Package
2381 (Typ_Scope
= Subp_Scope
2383 (Is_Child_Unit
(Subp_Scope
)
2384 and then Is_Ancestor_Package
2385 (Typ_Scope
, Subp_Scope
)));
2388 end Has_Public_Visibility_Of_Subprogram
;
2390 -- Start of processing for Invariant_Checks_OK
2394 Has_Invariants
(Typ
)
2395 and then Present
(Invariant_Procedure
(Typ
))
2396 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2397 and then Has_Public_Visibility_Of_Subprogram
;
2398 end Invariant_Checks_OK
;
2402 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2403 -- Source location of subprogram body contract
2408 -- Start of processing for Add_Invariant_And_Predicate_Checks
2413 -- Process the result of a function
2415 if Ekind
(Subp_Id
) = E_Function
then
2416 Typ
:= Etype
(Subp_Id
);
2418 -- Generate _Result which is used in procedure _Postconditions to
2419 -- verify the return value.
2421 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2422 Set_Etype
(Result
, Typ
);
2424 -- Add an invariant check when the return type has invariants and
2425 -- the related function is visible to the outside.
2427 if Invariant_Checks_OK
(Typ
) then
2430 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2434 -- Add an invariant check when the return type is an access to a
2435 -- type with invariants.
2437 Add_Invariant_Access_Checks
(Result
);
2440 -- Add invariant checks for all formals that qualify (see AI05-0289
2443 Formal
:= First_Formal
(Subp_Id
);
2444 while Present
(Formal
) loop
2445 Typ
:= Etype
(Formal
);
2447 if Ekind
(Formal
) /= E_In_Parameter
2448 or else Ekind
(Subp_Id
) = E_Procedure
2449 or else Is_Access_Type
(Typ
)
2451 if Invariant_Checks_OK
(Typ
) then
2454 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2458 Add_Invariant_Access_Checks
(Formal
);
2460 -- Note: we used to add predicate checks for OUT and IN OUT
2461 -- formals here, but that was misguided, since such checks are
2462 -- performed on the caller side, based on the predicate of the
2463 -- actual, rather than the predicate of the formal.
2467 Next_Formal
(Formal
);
2469 end Add_Invariant_And_Predicate_Checks
;
2471 -----------------------------------
2472 -- Add_Stable_Property_Contracts --
2473 -----------------------------------
2475 procedure Add_Stable_Property_Contracts
2476 (Subp_Id
: Entity_Id
; Class_Present
: Boolean)
2478 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
2480 procedure Insert_Stable_Property_Check
2481 (Formal
: Entity_Id
; Property_Function
: Entity_Id
);
2482 -- Build the pragma for one check and insert it in the tree.
2484 function Make_Stable_Property_Condition
2485 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
;
2486 -- Builds tree for "Func (Formal) = Func (Formal)'Old" expression.
2488 function Stable_Properties
2489 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2490 return Subprogram_List
;
2491 -- If no aspect specified, then returns length-zero result.
2492 -- Negated indicates that reserved word NOT was specified.
2494 ----------------------------------
2495 -- Insert_Stable_Property_Check --
2496 ----------------------------------
2498 procedure Insert_Stable_Property_Check
2499 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) is
2501 Args
: constant List_Id
:=
2503 (Make_Pragma_Argument_Association
2506 Make_Stable_Property_Condition
2508 Property_Function
=> Property_Function
)),
2509 Make_Pragma_Argument_Association
2515 "failed stable property check at "
2516 & Build_Location_String
(Loc
)
2518 & To_String
(Fully_Qualified_Name_String
2519 (Formal
, Append_NUL
=> False))
2520 & " and property function "
2521 & To_String
(Fully_Qualified_Name_String
2522 (Property_Function
, Append_NUL
=> False))
2525 Prag
: constant Node_Id
:=
2527 Pragma_Identifier
=>
2528 Make_Identifier
(Loc
, Name_Postcondition
),
2529 Pragma_Argument_Associations
=> Args
,
2530 Class_Present
=> Class_Present
);
2532 Subp_Decl
: constant Node_Id
:= Enclosing_Declaration
(Subp_Id
);
2533 pragma Assert
(Is_Declaration
(Subp_Decl
));
2535 Insert_After_And_Analyze
(Subp_Decl
, Prag
);
2536 end Insert_Stable_Property_Check
;
2538 ------------------------------------
2539 -- Make_Stable_Property_Condition --
2540 ------------------------------------
2542 function Make_Stable_Property_Condition
2543 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
2545 function Call_Property_Function
return Node_Id
is
2549 New_Occurrence_Of
(Property_Function
, Loc
),
2550 Parameter_Associations
=>
2551 New_List
(New_Occurrence_Of
(Formal
, Loc
))));
2555 Call_Property_Function
,
2556 Make_Attribute_Reference
2558 Prefix
=> Call_Property_Function
,
2559 Attribute_Name
=> Name_Old
));
2560 end Make_Stable_Property_Condition
;
2562 -----------------------
2563 -- Stable_Properties --
2564 -----------------------
2566 function Stable_Properties
2567 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2568 return Subprogram_List
2570 Aspect_Spec
: Node_Id
:=
2571 Find_Value_Of_Aspect
2572 (Aspect_Bearer
, Aspect_Stable_Properties
,
2573 Class_Present
=> Class_Present
);
2575 -- ??? For a derived type, we wish Find_Value_Of_Aspect
2576 -- somehow knew that this aspect is not inherited.
2577 -- But it doesn't, so we cope with that here.
2579 -- There are probably issues here with inheritance from
2580 -- interface types, where just looking for the one parent type
2581 -- isn't enough. But this is far from the only work needed for
2582 -- Stable_Properties'Class for interface types.
2584 if Is_Derived_Type
(Aspect_Bearer
) then
2586 Parent_Type
: constant Entity_Id
:=
2587 Etype
(Base_Type
(Aspect_Bearer
));
2590 Find_Value_Of_Aspect
2591 (Parent_Type
, Aspect_Stable_Properties
,
2592 Class_Present
=> Class_Present
)
2594 -- prevent inheritance
2595 Aspect_Spec
:= Empty
;
2600 if No
(Aspect_Spec
) then
2601 Negated
:= Aspect_Bearer
= Subp_Id
;
2602 -- This is a little bit subtle.
2603 -- We need to assign True in the Subp_Id case in order to
2604 -- distinguish between no aspect spec at all vs. an
2605 -- explicitly specified "with S_P => []" empty list.
2606 -- In both cases Stable_Properties will return a length-0
2607 -- array, but the two cases are not equivalent.
2608 -- Very roughly speaking the lack of an S_P aspect spec for
2609 -- a subprogram would be equivalent to something like
2610 -- "with S_P => [not]", where we apply the "not" modifier to
2611 -- an empty set of subprograms, if such a construct existed.
2612 -- We could just assign True here, but it seems untidy to
2613 -- return True in the case of an aspect spec for a type
2614 -- (since negation is only allowed for subp S_P aspects).
2616 return (1 .. 0 => <>);
2618 return Parse_Aspect_Stable_Properties
2619 (Aspect_Spec
, Negated
=> Negated
);
2621 end Stable_Properties
;
2623 Formal
: Entity_Id
:= First_Formal
(Subp_Id
);
2624 Type_Of_Formal
: Entity_Id
;
2626 Subp_Properties_Negated
: Boolean;
2627 Subp_Properties
: constant Subprogram_List
:=
2628 Stable_Properties
(Subp_Id
, Subp_Properties_Negated
);
2630 -- start of processing for Add_Stable_Property_Contracts
2633 if not (Is_Primitive
(Subp_Id
) and then Comes_From_Source
(Subp_Id
))
2638 while Present
(Formal
) loop
2639 Type_Of_Formal
:= Base_Type
(Etype
(Formal
));
2641 if not Subp_Properties_Negated
then
2643 for SPF_Id
of Subp_Properties
loop
2644 if Type_Of_Formal
= Base_Type
(Etype
(First_Formal
(SPF_Id
)))
2645 and then Scope
(Type_Of_Formal
) = Scope
(Subp_Id
)
2647 -- ??? Need to filter out checks for SPFs that are
2648 -- mentioned explicitly in the postcondition of
2651 Insert_Stable_Property_Check
2652 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2656 elsif Scope
(Type_Of_Formal
) = Scope
(Subp_Id
) then
2658 Ignored
: Boolean range False .. False;
2660 Typ_Property_Funcs
: constant Subprogram_List
:=
2661 Stable_Properties
(Type_Of_Formal
, Negated
=> Ignored
);
2663 function Excluded_By_Aspect_Spec_Of_Subp
2664 (SPF_Id
: Entity_Id
) return Boolean;
2665 -- Examine Subp_Properties to determine whether SPF should
2668 -------------------------------------
2669 -- Excluded_By_Aspect_Spec_Of_Subp --
2670 -------------------------------------
2672 function Excluded_By_Aspect_Spec_Of_Subp
2673 (SPF_Id
: Entity_Id
) return Boolean is
2675 pragma Assert
(Subp_Properties_Negated
);
2676 -- Look through renames for equality test here ???
2677 return (for some F
of Subp_Properties
=> F
= SPF_Id
);
2678 end Excluded_By_Aspect_Spec_Of_Subp
;
2680 -- Look through renames for equality test here ???
2681 Subp_Is_Stable_Property_Function
: constant Boolean :=
2682 (for some F
of Typ_Property_Funcs
=> F
= Subp_Id
);
2684 if not Subp_Is_Stable_Property_Function
then
2685 for SPF_Id
of Typ_Property_Funcs
loop
2686 if not Excluded_By_Aspect_Spec_Of_Subp
(SPF_Id
) then
2687 -- ??? Need to filter out checks for SPFs that are
2688 -- mentioned explicitly in the postcondition of
2690 Insert_Stable_Property_Check
2691 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2697 Next_Formal
(Formal
);
2699 end Add_Stable_Property_Contracts
;
2701 -------------------------
2702 -- Append_Enabled_Item --
2703 -------------------------
2705 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2707 -- Do not chain ignored or disabled pragmas
2709 if Nkind
(Item
) = N_Pragma
2710 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2714 -- Otherwise, add the item
2721 -- If the pragma is a conjunct in a composite postcondition, it
2722 -- has been processed in reverse order. In the postcondition body
2723 -- it must appear before the others.
2725 if Nkind
(Item
) = N_Pragma
2726 and then From_Aspect_Specification
(Item
)
2727 and then Split_PPC
(Item
)
2729 Prepend
(Item
, List
);
2731 Append
(Item
, List
);
2734 end Append_Enabled_Item
;
2736 ----------------------------
2737 -- Process_Contract_Cases --
2738 ----------------------------
2740 procedure Process_Contract_Cases
2741 (Stmts
: in out List_Id
;
2744 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2745 -- Process pragma Contract_Cases for subprogram Subp_Id
2747 --------------------------------
2748 -- Process_Contract_Cases_For --
2749 --------------------------------
2751 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2752 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2756 if Present
(Items
) then
2757 Prag
:= Contract_Test_Cases
(Items
);
2758 while Present
(Prag
) loop
2759 if Is_Checked
(Prag
) then
2760 if Pragma_Name
(Prag
) = Name_Always_Terminates
then
2761 Expand_Pragma_Always_Terminates
(Prag
);
2763 elsif Pragma_Name
(Prag
) = Name_Contract_Cases
then
2764 Expand_Pragma_Contract_Cases
2770 elsif Pragma_Name
(Prag
) = Name_Exceptional_Cases
then
2771 Expand_Pragma_Exceptional_Cases
(Prag
);
2773 elsif Pragma_Name
(Prag
) = Name_Subprogram_Variant
then
2774 Expand_Pragma_Subprogram_Variant
2777 Body_Decls
=> Decls
);
2781 Prag
:= Next_Pragma
(Prag
);
2784 end Process_Contract_Cases_For
;
2786 -- Start of processing for Process_Contract_Cases
2789 Process_Contract_Cases_For
(Body_Id
);
2791 if Present
(Spec_Id
) then
2792 Process_Contract_Cases_For
(Spec_Id
);
2794 end Process_Contract_Cases
;
2796 ----------------------------
2797 -- Process_Postconditions --
2798 ----------------------------
2800 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2801 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2802 -- Collect all [refined] postconditions of a specific kind denoted
2803 -- by Post_Nam that belong to the body, and generate pragma Check
2804 -- equivalents in list Stmts.
2806 procedure Process_Spec_Postconditions
;
2807 -- Collect all [inherited] postconditions of the spec, and generate
2808 -- pragma Check equivalents in list Stmts.
2810 ---------------------------------
2811 -- Process_Body_Postconditions --
2812 ---------------------------------
2814 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2815 Items
: constant Node_Id
:= Contract
(Body_Id
);
2816 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2821 -- Process the contract
2823 if Present
(Items
) then
2824 Prag
:= Pre_Post_Conditions
(Items
);
2825 while Present
(Prag
) loop
2826 if Pragma_Name
(Prag
) = Post_Nam
2827 and then Is_Checked
(Prag
)
2830 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2834 Prag
:= Next_Pragma
(Prag
);
2838 -- The subprogram body being processed is actually the proper body
2839 -- of a stub with a corresponding spec. The subprogram stub may
2840 -- carry a postcondition pragma, in which case it must be taken
2841 -- into account. The pragma appears after the stub.
2843 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2844 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2845 while Present
(Decl
) loop
2847 -- Note that non-matching pragmas are skipped
2849 if Nkind
(Decl
) = N_Pragma
then
2850 if Pragma_Name
(Decl
) = Post_Nam
2851 and then Is_Checked
(Decl
)
2854 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2858 -- Skip internally generated code
2860 elsif not Comes_From_Source
(Decl
) then
2863 -- Postcondition pragmas are usually grouped together. There
2864 -- is no need to inspect the whole declarative list.
2873 end Process_Body_Postconditions
;
2875 ---------------------------------
2876 -- Process_Spec_Postconditions --
2877 ---------------------------------
2879 procedure Process_Spec_Postconditions
is
2880 Subps
: constant Subprogram_List
:=
2881 Inherited_Subprograms
(Spec_Id
);
2882 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
2884 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean;
2885 -- Return True if the contract of subprogram Subp_Id has been
2892 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean is
2894 for Index
in Seen
'Range loop
2895 if Seen
(Index
) = Subp_Id
then
2908 Subp_Id
: Entity_Id
;
2910 -- Start of processing for Process_Spec_Postconditions
2913 -- Process the contract
2915 Items
:= Contract
(Spec_Id
);
2917 if Present
(Items
) then
2918 Prag
:= Pre_Post_Conditions
(Items
);
2919 while Present
(Prag
) loop
2920 if Pragma_Name
(Prag
) = Name_Postcondition
2921 and then Is_Checked
(Prag
)
2924 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2928 Prag
:= Next_Pragma
(Prag
);
2932 -- Process the contracts of all inherited subprograms, looking for
2933 -- class-wide postconditions.
2935 for Index
in Subps
'Range loop
2936 Subp_Id
:= Subps
(Index
);
2938 if Present
(Alias
(Subp_Id
)) then
2939 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
2942 -- Wrappers of class-wide pre/postconditions reference the
2943 -- parent primitive that has the inherited contract.
2945 if Is_Wrapper
(Subp_Id
)
2946 and then Present
(LSP_Subprogram
(Subp_Id
))
2948 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
2951 Items
:= Contract
(Subp_Id
);
2953 if not Seen_Subp
(Subp_Id
) and then Present
(Items
) then
2954 Seen
(Index
) := Subp_Id
;
2956 Prag
:= Pre_Post_Conditions
(Items
);
2957 while Present
(Prag
) loop
2958 if Pragma_Name
(Prag
) = Name_Postcondition
2959 and then Class_Present
(Prag
)
2962 Build_Pragma_Check_Equivalent
2965 Inher_Id
=> Subp_Id
);
2967 -- The pragma Check equivalent of the class-wide
2968 -- postcondition is still created even though the
2969 -- pragma may be ignored because the equivalent
2970 -- performs semantic checks.
2972 if Is_Checked
(Prag
) then
2973 Append_Enabled_Item
(Item
, Stmts
);
2977 Prag
:= Next_Pragma
(Prag
);
2981 end Process_Spec_Postconditions
;
2983 pragma Unmodified
(Stmts
);
2984 -- Stmts is passed as IN OUT to signal that the list can be updated,
2985 -- even if the corresponding integer value representing the list does
2988 -- Start of processing for Process_Postconditions
2991 -- The processing of postconditions is done in reverse order (body
2992 -- first) to ensure the following arrangement:
2994 -- <refined postconditions from body>
2995 -- <postconditions from body>
2996 -- <postconditions from spec>
2997 -- <inherited postconditions>
2999 Process_Body_Postconditions
(Name_Refined_Post
);
3000 Process_Body_Postconditions
(Name_Postcondition
);
3002 if Present
(Spec_Id
) then
3003 Process_Spec_Postconditions
;
3005 end Process_Postconditions
;
3007 ---------------------------
3008 -- Process_Preconditions --
3009 ---------------------------
3011 procedure Process_Preconditions
(Decls
: in out List_Id
) is
3012 Insert_Node
: Node_Id
:= Empty
;
3013 -- The insertion node after which all pragma Check equivalents are
3016 procedure Prepend_To_Decls
(Item
: Node_Id
);
3017 -- Prepend a single item to the declarations of the subprogram body
3019 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
);
3020 -- Prepend a normal precondition to the declarations of the body and
3023 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
3024 -- Collect all preconditions of subprogram Subp_Id and prepend their
3025 -- pragma Check equivalents to the declarations of the body.
3027 ----------------------
3028 -- Prepend_To_Decls --
3029 ----------------------
3031 procedure Prepend_To_Decls
(Item
: Node_Id
) is
3033 -- Ensure that the body has a declarative list
3037 Set_Declarations
(Body_Decl
, Decls
);
3040 Prepend_To
(Decls
, Item
);
3041 end Prepend_To_Decls
;
3043 -----------------------------
3044 -- Prepend_Pragma_To_Decls --
3045 -----------------------------
3047 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
) is
3048 Check_Prag
: Node_Id
;
3051 -- Skip the sole class-wide precondition (if any) since it is
3052 -- processed by Merge_Class_Conditions.
3054 if Class_Present
(Prag
) then
3057 -- Accumulate the corresponding Check pragmas at the top of the
3058 -- declarations. Prepending the items ensures that they will be
3059 -- evaluated in their original order.
3062 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
3063 Prepend_To_Decls
(Check_Prag
);
3066 end Prepend_Pragma_To_Decls
;
3068 -------------------------------
3069 -- Process_Preconditions_For --
3070 -------------------------------
3072 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
3073 Items
: constant Node_Id
:= Contract
(Subp_Id
);
3074 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
3080 -- Process the contract. If the body is an expression function
3081 -- that is a completion, freeze types within, because this may
3082 -- not have been done yet, when the subprogram declaration and
3083 -- its completion by an expression function appear in distinct
3084 -- declarative lists of the same unit (visible and private).
3087 Was_Expression_Function
(Body_Decl
)
3088 and then Sloc
(Body_Id
) /= Sloc
(Subp_Id
)
3089 and then In_Same_Source_Unit
(Body_Id
, Subp_Id
)
3090 and then not In_Same_List
(Body_Decl
, Subp_Decl
);
3092 if Present
(Items
) then
3093 Prag
:= Pre_Post_Conditions
(Items
);
3094 while Present
(Prag
) loop
3095 if Pragma_Name
(Prag
) = Name_Precondition
3096 and then Is_Checked
(Prag
)
3099 and then Present
(Corresponding_Aspect
(Prag
))
3103 Typ
=> Standard_Boolean
,
3106 (First
(Pragma_Argument_Associations
(Prag
))),
3110 Prepend_Pragma_To_Decls
(Prag
);
3113 Prag
:= Next_Pragma
(Prag
);
3117 -- The subprogram declaration being processed is actually a body
3118 -- stub. The stub may carry a precondition pragma, in which case
3119 -- it must be taken into account. The pragma appears after the
3122 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
3124 -- Inspect the declarations following the body stub
3126 Decl
:= Next
(Subp_Decl
);
3127 while Present
(Decl
) loop
3129 -- Note that non-matching pragmas are skipped
3131 if Nkind
(Decl
) = N_Pragma
then
3132 if Pragma_Name
(Decl
) = Name_Precondition
3133 and then Is_Checked
(Decl
)
3135 Prepend_Pragma_To_Decls
(Decl
);
3138 -- Skip internally generated code
3140 elsif not Comes_From_Source
(Decl
) then
3143 -- Preconditions are usually grouped together. There is no
3144 -- need to inspect the whole declarative list.
3153 end Process_Preconditions_For
;
3157 Body_Decls
: constant List_Id
:= Declarations
(Body_Decl
);
3159 Next_Decl
: Node_Id
;
3161 -- Start of processing for Process_Preconditions
3164 -- Find the proper insertion point for all pragma Check equivalents
3166 if Present
(Body_Decls
) then
3167 Decl
:= First
(Body_Decls
);
3168 while Present
(Decl
) loop
3170 -- First source declaration terminates the search, because all
3171 -- preconditions must be evaluated prior to it, by definition.
3173 if Comes_From_Source
(Decl
) then
3176 -- Certain internally generated object renamings such as those
3177 -- for discriminants and protection fields must be elaborated
3178 -- before the preconditions are evaluated, as their expressions
3179 -- may mention the discriminants. The renamings include those
3180 -- for private components so we need to find the last such.
3182 elsif Is_Prologue_Renaming
(Decl
) then
3183 while Present
(Next
(Decl
))
3184 and then Is_Prologue_Renaming
(Next
(Decl
))
3189 Insert_Node
:= Decl
;
3191 -- Otherwise the declaration does not come from source. This
3192 -- also terminates the search, because internal code may raise
3193 -- exceptions which should not preempt the preconditions.
3202 -- The processing of preconditions is done in reverse order (body
3203 -- first), because each pragma Check equivalent is inserted at the
3204 -- top of the declarations. This ensures that the final order is
3205 -- consistent with following diagram:
3207 -- <inherited preconditions>
3208 -- <preconditions from spec>
3209 -- <preconditions from body>
3211 Process_Preconditions_For
(Body_Id
);
3213 -- Move the generated entry-call prologue renamings into the
3214 -- outer declarations for use in the preconditions.
3216 Decl
:= First
(Body_Decls
);
3217 while Present
(Decl
) and then Present
(Insert_Node
) loop
3218 Next_Decl
:= Next
(Decl
);
3220 Prepend_To_Decls
(Decl
);
3222 exit when Decl
= Insert_Node
;
3227 if Present
(Spec_Id
) then
3228 Process_Preconditions_For
(Spec_Id
);
3230 end Process_Preconditions
;
3234 Restore_Scope
: Boolean := False;
3236 Stmts
: List_Id
:= No_List
;
3237 Decls
: List_Id
:= New_List
;
3238 Subp_Id
: Entity_Id
;
3240 -- Start of processing for Expand_Subprogram_Contract
3243 -- Obtain the entity of the initial declaration
3245 if Present
(Spec_Id
) then
3251 -- Do not perform expansion activity when it is not needed
3253 if not Expander_Active
then
3256 -- GNATprove does not need the executable semantics of a contract
3258 elsif GNATprove_Mode
then
3261 -- The contract of a generic subprogram or one declared in a generic
3262 -- context is not expanded, as the corresponding instance will provide
3263 -- the executable semantics of the contract.
3265 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
3268 -- All subprograms carry a contract, but for some it is not significant
3269 -- and should not be processed. This is a small optimization.
3271 elsif not Has_Significant_Contract
(Subp_Id
) then
3274 -- The contract of an ignored Ghost subprogram does not need expansion,
3275 -- because the subprogram and all calls to it will be removed.
3277 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
3280 -- No action needed for helpers and indirect-call wrapper built to
3281 -- support class-wide preconditions.
3283 elsif Present
(Class_Preconditions_Subprogram
(Subp_Id
)) then
3286 -- Do not re-expand the same contract. This scenario occurs when a
3287 -- construct is rewritten into something else during its analysis
3288 -- (expression functions for instance).
3290 elsif Has_Expanded_Contract
(Subp_Id
) then
3294 -- Prevent multiple expansion attempts of the same contract
3296 Set_Has_Expanded_Contract
(Subp_Id
);
3298 -- Ensure that the formal parameters are visible when expanding all
3301 if not In_Open_Scopes
(Subp_Id
) then
3302 Restore_Scope
:= True;
3303 Push_Scope
(Subp_Id
);
3305 if Is_Generic_Subprogram
(Subp_Id
) then
3306 Install_Generic_Formals
(Subp_Id
);
3308 Install_Formals
(Subp_Id
);
3312 -- The expansion of a subprogram contract involves the creation of Check
3313 -- pragmas to verify the contract assertions of the spec and body in a
3314 -- particular order. The order is as follows:
3316 -- function Original_Code (...) return ... is
3317 -- <prologue renamings>
3318 -- <inherited preconditions>
3319 -- <preconditions from spec>
3320 -- <preconditions from body>
3321 -- <contract case conditions>
3323 -- function _Wrapped_Statements (...) return ... is
3324 -- <source declarations>
3326 -- <source statements>
3327 -- end _Wrapped_Statements;
3330 -- return Result : constant ... := _Wrapped_Statements do
3331 -- <refined postconditions from body>
3332 -- <postconditions from body>
3333 -- <postconditions from spec>
3334 -- <inherited postconditions>
3335 -- <contract case consequences>
3336 -- <invariant check of function result>
3337 -- <invariant and predicate checks of parameters
3339 -- end Original_Code;
3341 -- Step 1: augment contracts list with postconditions associated with
3342 -- Stable_Properties and Stable_Properties'Class aspects. This must
3343 -- precede Process_Postconditions.
3345 for Class_Present
in Boolean loop
3346 Add_Stable_Property_Contracts
3347 (Subp_Id
, Class_Present
=> Class_Present
);
3350 -- Step 2: Handle all preconditions. This action must come before the
3351 -- processing of pragma Contract_Cases because the pragma prepends items
3352 -- to the body declarations.
3354 Process_Preconditions
(Decls
);
3356 -- Step 3: Handle all postconditions. This action must come before the
3357 -- processing of pragma Contract_Cases because the pragma appends items
3360 Process_Postconditions
(Stmts
);
3362 -- Step 4: Handle pragma Contract_Cases. This action must come before
3363 -- the processing of invariants and predicates because those append
3364 -- items to list Stmts.
3366 Process_Contract_Cases
(Stmts
, Decls
);
3368 -- Step 5: Apply invariant and predicate checks on a function result and
3369 -- all formals. The resulting checks are accumulated in list Stmts.
3371 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3373 -- Step 6: Construct subprogram _wrapped_statements
3375 -- When no statements are present we still need to insert contract
3376 -- related declarations.
3379 Prepend_List_To
(Declarations
(Body_Decl
), Decls
);
3381 -- Otherwise, we need a wrapper
3384 Build_Subprogram_Contract_Wrapper
(Body_Id
, Stmts
, Decls
, Result
);
3387 if Restore_Scope
then
3390 end Expand_Subprogram_Contract
;
3392 -------------------------------
3393 -- Freeze_Previous_Contracts --
3394 -------------------------------
3396 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3397 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3398 pragma Inline
(Causes_Contract_Freezing
);
3399 -- Determine whether arbitrary node N causes contract freezing. This is
3400 -- used as an assertion for the current body declaration that caused
3401 -- contract freezing, and as a condition to detect body declaration that
3402 -- already caused contract freezing before.
3404 procedure Freeze_Contracts
;
3405 pragma Inline
(Freeze_Contracts
);
3406 -- Freeze the contracts of all eligible constructs which precede body
3409 procedure Freeze_Enclosing_Package_Body
;
3410 pragma Inline
(Freeze_Enclosing_Package_Body
);
3411 -- Freeze the contract of the nearest package body (if any) which
3412 -- encloses body Body_Decl.
3414 ------------------------------
3415 -- Causes_Contract_Freezing --
3416 ------------------------------
3418 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3420 -- The following condition matches guards for calls to
3421 -- Freeze_Previous_Contracts from routines that analyze various body
3422 -- declarations. In particular, it detects expression functions, as
3423 -- described in the call from Analyze_Subprogram_Body_Helper.
3426 Comes_From_Source
(Original_Node
(N
))
3429 N_Entry_Body | N_Package_Body | N_Protected_Body |
3430 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body
;
3431 end Causes_Contract_Freezing
;
3433 ----------------------
3434 -- Freeze_Contracts --
3435 ----------------------
3437 procedure Freeze_Contracts
is
3438 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3442 -- Nothing to do when the body which causes freezing does not appear
3443 -- in a declarative list because there cannot possibly be constructs
3446 if not Is_List_Member
(Body_Decl
) then
3450 -- Inspect the declarations preceding the body, and freeze individual
3451 -- contracts of eligible constructs.
3453 Decl
:= Prev
(Body_Decl
);
3454 while Present
(Decl
) loop
3456 -- Stop the traversal when a preceding construct that causes
3457 -- freezing is encountered as there is no point in refreezing
3458 -- the already frozen constructs.
3460 if Causes_Contract_Freezing
(Decl
) then
3463 -- Entry or subprogram declarations
3465 elsif Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
3466 | N_Entry_Declaration
3467 | N_Generic_Subprogram_Declaration
3468 | N_Subprogram_Declaration
3470 Analyze_Entry_Or_Subprogram_Contract
3471 (Subp_Id
=> Defining_Entity
(Decl
),
3472 Freeze_Id
=> Body_Id
);
3476 elsif Nkind
(Decl
) = N_Object_Declaration
then
3477 Analyze_Object_Contract
3478 (Obj_Id
=> Defining_Entity
(Decl
),
3479 Freeze_Id
=> Body_Id
);
3483 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
3484 | N_Single_Protected_Declaration
3486 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3488 -- Subprogram body stubs
3490 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3491 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3495 elsif Nkind
(Decl
) in N_Single_Task_Declaration
3496 | N_Task_Type_Declaration
3498 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3501 if Nkind
(Decl
) in N_Full_Type_Declaration
3502 | N_Private_Type_Declaration
3503 | N_Task_Type_Declaration
3504 | N_Protected_Type_Declaration
3505 | N_Formal_Type_Declaration
3507 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
3512 end Freeze_Contracts
;
3514 -----------------------------------
3515 -- Freeze_Enclosing_Package_Body --
3516 -----------------------------------
3518 procedure Freeze_Enclosing_Package_Body
is
3519 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3523 -- Climb the parent chain looking for an enclosing package body. Do
3524 -- not use the scope stack, because a body utilizes the entity of its
3525 -- corresponding spec.
3527 Par
:= Parent
(Body_Decl
);
3528 while Present
(Par
) loop
3529 if Nkind
(Par
) = N_Package_Body
then
3530 Analyze_Package_Body_Contract
3531 (Body_Id
=> Defining_Entity
(Par
),
3532 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3536 -- Do not look for an enclosing package body when the construct
3537 -- which causes freezing is a body generated for an expression
3538 -- function and it appears within a package spec. This ensures
3539 -- that the traversal will not reach too far up the parent chain
3540 -- and attempt to freeze a package body which must not be frozen.
3542 -- package body Enclosing_Body
3543 -- with Refined_State => (State => Var)
3545 -- package Nested is
3546 -- type Some_Type is ...;
3547 -- function Cause_Freezing return ...;
3549 -- function Cause_Freezing is (...);
3552 -- Var : Nested.Some_Type;
3554 elsif Nkind
(Par
) = N_Package_Declaration
3555 and then Nkind
(Orig_Decl
) = N_Expression_Function
3559 -- Prevent the search from going too far
3561 elsif Is_Body_Or_Package_Declaration
(Par
) then
3565 Par
:= Parent
(Par
);
3567 end Freeze_Enclosing_Package_Body
;
3571 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3573 -- Start of processing for Freeze_Previous_Contracts
3576 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3578 -- A body that is in the process of being inlined appears from source,
3579 -- but carries name _parent. Such a body does not cause freezing of
3582 if Chars
(Body_Id
) = Name_uParent
then
3586 Freeze_Enclosing_Package_Body
;
3588 end Freeze_Previous_Contracts
;
3590 ---------------------------------
3591 -- Inherit_Subprogram_Contract --
3592 ---------------------------------
3594 procedure Inherit_Subprogram_Contract
3596 From_Subp
: Entity_Id
)
3598 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3599 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3602 --------------------
3603 -- Inherit_Pragma --
3604 --------------------
3606 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3607 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3611 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3612 -- chains, therefore the node must be replicated. The new pragma is
3613 -- flagged as inherited for distinction purposes.
3615 if Present
(Prag
) then
3616 New_Prag
:= New_Copy_Tree
(Prag
);
3617 Set_Is_Inherited_Pragma
(New_Prag
);
3619 Add_Contract_Item
(New_Prag
, Subp
);
3623 -- Start of processing for Inherit_Subprogram_Contract
3626 -- Inheritance is carried out only when both entities are subprograms
3629 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3630 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3631 and then Present
(Contract
(From_Subp
))
3633 Inherit_Pragma
(Pragma_Extensions_Visible
);
3634 Inherit_Pragma
(Pragma_Side_Effects
);
3636 end Inherit_Subprogram_Contract
;
3638 -------------------------------------
3639 -- Instantiate_Subprogram_Contract --
3640 -------------------------------------
3642 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3643 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3644 -- Instantiate all contract-related source pragmas found in the list,
3645 -- starting with pragma First_Prag. Each instantiated pragma is added
3648 -------------------------
3649 -- Instantiate_Pragmas --
3650 -------------------------
3652 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3653 Inst_Prag
: Node_Id
;
3658 while Present
(Prag
) loop
3659 if Is_Generic_Contract_Pragma
(Prag
) then
3661 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3663 Set_Analyzed
(Inst_Prag
, False);
3664 Append_To
(L
, Inst_Prag
);
3667 Prag
:= Next_Pragma
(Prag
);
3669 end Instantiate_Pragmas
;
3673 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3675 -- Start of processing for Instantiate_Subprogram_Contract
3678 if Present
(Items
) then
3679 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3680 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3681 Instantiate_Pragmas
(Classifications
(Items
));
3683 end Instantiate_Subprogram_Contract
;
3685 --------------------------
3686 -- Is_Prologue_Renaming --
3687 --------------------------
3689 -- This should be turned into a flag and set during the expansion of
3690 -- task and protected types when the renamings get generated ???
3692 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
3699 if Nkind
(Decl
) = N_Object_Renaming_Declaration
3700 and then not Comes_From_Source
(Decl
)
3702 Obj
:= Defining_Entity
(Decl
);
3705 if Nkind
(Nam
) = N_Selected_Component
then
3706 -- Analyze the renaming declaration so we can further examine it
3708 if not Analyzed
(Decl
) then
3712 Pref
:= Prefix
(Nam
);
3713 Sel
:= Selector_Name
(Nam
);
3715 -- A discriminant renaming appears as
3716 -- Discr : constant ... := Prefix.Discr;
3718 if Ekind
(Obj
) = E_Constant
3719 and then Is_Entity_Name
(Sel
)
3720 and then Present
(Entity
(Sel
))
3721 and then Ekind
(Entity
(Sel
)) = E_Discriminant
3725 -- A protection field renaming appears as
3726 -- Prot : ... := _object._object;
3728 -- A renamed private component is just a component of
3729 -- _object, with an arbitrary name.
3731 elsif Ekind
(Obj
) in E_Variable | E_Constant
3732 and then Nkind
(Pref
) = N_Identifier
3733 and then Chars
(Pref
) = Name_uObject
3734 and then Nkind
(Sel
) = N_Identifier
3742 end Is_Prologue_Renaming
;
3744 -----------------------------------
3745 -- Make_Class_Precondition_Subps --
3746 -----------------------------------
3748 procedure Make_Class_Precondition_Subps
3749 (Subp_Id
: Entity_Id
;
3750 Late_Overriding
: Boolean := False)
3752 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
3753 Tagged_Type
: constant Entity_Id
:= Find_Dispatching_Type
(Subp_Id
);
3755 procedure Add_Indirect_Call_Wrapper
;
3756 -- Build the indirect-call wrapper and append it to the freezing actions
3759 procedure Add_Call_Helper
3760 (Helper_Id
: Entity_Id
;
3761 Is_Dynamic
: Boolean);
3762 -- Factorizes code for building a call helper with the given identifier
3763 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
3764 -- controls building the static or dynamic version of the helper.
3766 function Build_Unique_Name
(Suffix
: String) return Name_Id
;
3767 -- Build an unique new name adding suffix to Subp_Id name (plus its
3768 -- homonym number for values bigger than 1).
3770 -------------------------------
3771 -- Add_Indirect_Call_Wrapper --
3772 -------------------------------
3774 procedure Add_Indirect_Call_Wrapper
is
3776 function Build_ICW_Body
return Node_Id
;
3777 -- Build the body of the indirect call wrapper
3779 function Build_ICW_Decl
return Node_Id
;
3780 -- Build the declaration of the indirect call wrapper
3782 --------------------
3783 -- Build_ICW_Body --
3784 --------------------
3786 function Build_ICW_Body
return Node_Id
is
3787 ICW_Id
: constant Entity_Id
:= Indirect_Call_Wrapper
(Subp_Id
);
3788 Spec
: constant Node_Id
:= Parent
(ICW_Id
);
3789 Body_Spec
: Node_Id
;
3794 Body_Spec
:= Copy_Subprogram_Spec
(Spec
);
3796 -- Build call to wrapped subprogram
3799 Actuals
: constant List_Id
:= Empty_List
;
3800 Formal_Spec
: Entity_Id
:=
3801 First
(Parameter_Specifications
(Spec
));
3803 -- Build parameter association & call
3805 while Present
(Formal_Spec
) loop
3808 (Defining_Identifier
(Formal_Spec
), Loc
));
3812 if Ekind
(ICW_Id
) = E_Procedure
then
3814 Make_Procedure_Call_Statement
(Loc
,
3815 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3816 Parameter_Associations
=> Actuals
);
3819 Make_Simple_Return_Statement
(Loc
,
3821 Make_Function_Call
(Loc
,
3822 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3823 Parameter_Associations
=> Actuals
));
3828 Make_Subprogram_Body
(Loc
,
3829 Specification
=> Body_Spec
,
3830 Declarations
=> New_List
,
3831 Handled_Statement_Sequence
=>
3832 Make_Handled_Sequence_Of_Statements
(Loc
,
3833 Statements
=> New_List
(Call
)));
3835 -- The new operation is internal and overriding indicators do not
3838 Set_Must_Override
(Body_Spec
, False);
3843 --------------------
3844 -- Build_ICW_Decl --
3845 --------------------
3847 function Build_ICW_Decl
return Node_Id
is
3848 ICW_Id
: constant Entity_Id
:=
3849 Make_Defining_Identifier
(Loc
,
3850 Build_Unique_Name
(Suffix
=> "ICW"));
3855 Spec
:= Copy_Subprogram_Spec
(Parent
(Subp_Id
));
3856 Set_Must_Override
(Spec
, False);
3857 Set_Must_Not_Override
(Spec
, False);
3858 Set_Defining_Unit_Name
(Spec
, ICW_Id
);
3859 Mutate_Ekind
(ICW_Id
, Ekind
(Subp_Id
));
3860 Set_Is_Public
(ICW_Id
);
3862 -- The indirect call wrapper is commonly used for indirect calls
3863 -- but inlined for direct calls performed from the DTW.
3865 Set_Is_Inlined
(ICW_Id
);
3867 if Nkind
(Spec
) = N_Procedure_Specification
then
3868 Set_Null_Present
(Spec
, False);
3871 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
3873 -- Link original subprogram to indirect wrapper and vice versa
3875 Set_Indirect_Call_Wrapper
(Subp_Id
, ICW_Id
);
3876 Set_Class_Preconditions_Subprogram
(ICW_Id
, Subp_Id
);
3878 -- Inherit debug info flag to allow debugging the wrapper
3880 if Needs_Debug_Info
(Subp_Id
) then
3881 Set_Debug_Info_Needed
(ICW_Id
);
3892 -- Start of processing for Add_Indirect_Call_Wrapper
3895 pragma Assert
(No
(Indirect_Call_Wrapper
(Subp_Id
)));
3897 ICW_Decl
:= Build_ICW_Decl
;
3899 Append_Freeze_Action
(Tagged_Type
, ICW_Decl
);
3902 ICW_Body
:= Build_ICW_Body
;
3903 Append_Freeze_Action
(Tagged_Type
, ICW_Body
);
3905 -- We cannot defer the analysis of this ICW wrapper when it is
3906 -- built as a consequence of building its partner DTW wrapper
3907 -- at the freezing point of the tagged type.
3909 if Is_Dispatch_Table_Wrapper
(Subp_Id
) then
3912 end Add_Indirect_Call_Wrapper
;
3914 ---------------------
3915 -- Add_Call_Helper --
3916 ---------------------
3918 procedure Add_Call_Helper
3919 (Helper_Id
: Entity_Id
;
3920 Is_Dynamic
: Boolean)
3922 function Build_Call_Helper_Body
return Node_Id
;
3923 -- Build the body of a call helper
3925 function Build_Call_Helper_Decl
return Node_Id
;
3926 -- Build the declaration of a call helper
3928 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
;
3929 -- Build the specification of the helper
3931 ----------------------------
3932 -- Build_Call_Helper_Body --
3933 ----------------------------
3935 function Build_Call_Helper_Body
return Node_Id
is
3937 function Copy_And_Update_References
3938 (Expr
: Node_Id
) return Node_Id
;
3939 -- Copy Expr updating references to formals of Helper_Id; update
3940 -- also references to loop identifiers of quantified expressions.
3942 --------------------------------
3943 -- Copy_And_Update_References --
3944 --------------------------------
3946 function Copy_And_Update_References
3947 (Expr
: Node_Id
) return Node_Id
3949 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
3951 procedure Map_Quantified_Expression_Loop_Identifiers
;
3952 -- Traverse Expr and append to Assoc_List the mapping of loop
3953 -- identifers of quantified expressions with its new copy.
3955 ------------------------------------------------
3956 -- Map_Quantified_Expression_Loop_Identifiers --
3957 ------------------------------------------------
3959 procedure Map_Quantified_Expression_Loop_Identifiers
is
3960 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
;
3961 -- Append to Assoc_List the mapping of loop identifers of
3962 -- quantified expressions with its new copy.
3964 --------------------
3965 -- Map_Loop_Param --
3966 --------------------
3968 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
3971 if Nkind
(N
) = N_Loop_Parameter_Specification
3972 and then Nkind
(Parent
(N
)) = N_Quantified_Expression
3975 Def_Id
: constant Entity_Id
:=
3976 Defining_Identifier
(N
);
3978 Append_Elmt
(Def_Id
, Assoc_List
);
3979 Append_Elmt
(New_Copy
(Def_Id
), Assoc_List
);
3986 procedure Map_Quantified_Expressions
is
3987 new Traverse_Proc
(Map_Loop_Param
);
3990 Map_Quantified_Expressions
(Expr
);
3991 end Map_Quantified_Expression_Loop_Identifiers
;
3995 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp_Id
);
3996 Helper_Formal_Id
: Entity_Id
:= First_Formal
(Helper_Id
);
3998 -- Start of processing for Copy_And_Update_References
4001 while Present
(Subp_Formal_Id
) loop
4002 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4003 Append_Elmt
(Helper_Formal_Id
, Assoc_List
);
4005 Next_Formal
(Subp_Formal_Id
);
4006 Next_Formal
(Helper_Formal_Id
);
4009 Map_Quantified_Expression_Loop_Identifiers
;
4011 return New_Copy_Tree
(Expr
, Map
=> Assoc_List
);
4012 end Copy_And_Update_References
;
4016 Helper_Decl
: constant Node_Id
:= Parent
(Parent
(Helper_Id
));
4017 Body_Id
: Entity_Id
;
4018 Body_Spec
: Node_Id
;
4019 Body_Stmts
: Node_Id
;
4020 Helper_Body
: Node_Id
;
4021 Return_Expr
: Node_Id
;
4023 -- Start of processing for Build_Call_Helper_Body
4026 pragma Assert
(Analyzed
(Unit_Declaration_Node
(Helper_Id
)));
4027 pragma Assert
(No
(Corresponding_Body
(Helper_Decl
)));
4029 Body_Id
:= Make_Defining_Identifier
(Loc
, Chars
(Helper_Id
));
4030 Body_Spec
:= Build_Call_Helper_Spec
(Body_Id
);
4032 Set_Corresponding_Body
(Helper_Decl
, Body_Id
);
4033 Set_Must_Override
(Body_Spec
, False);
4035 if Present
(Class_Preconditions
(Subp_Id
))
4036 -- Evaluate the expression if we are building a dynamic helper
4037 -- or we are building a static helper for a non-abstract tagged
4038 -- type; for abstract tagged types the helper just returns True
4039 -- since it is called by the indirect call wrapper (ICW).
4043 not Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)))
4046 Copy_And_Update_References
(Class_Preconditions
(Subp_Id
));
4048 -- When the subprogram is compiled with assertions disabled the
4049 -- helper just returns True; done to avoid reporting errors at
4050 -- link time since a unit may be compiled with assertions disabled
4051 -- and another (which depends on it) compiled with assertions
4055 pragma Assert
(Present
(Ignored_Class_Preconditions
(Subp_Id
))
4056 or else Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)));
4057 Return_Expr
:= New_Occurrence_Of
(Standard_True
, Loc
);
4061 Make_Handled_Sequence_Of_Statements
(Loc
,
4062 Statements
=> New_List
(
4063 Make_Simple_Return_Statement
(Loc
, Return_Expr
)));
4066 Make_Subprogram_Body
(Loc
,
4067 Specification
=> Body_Spec
,
4068 Declarations
=> New_List
,
4069 Handled_Statement_Sequence
=> Body_Stmts
);
4072 end Build_Call_Helper_Body
;
4074 ----------------------------
4075 -- Build_Call_Helper_Decl --
4076 ----------------------------
4078 function Build_Call_Helper_Decl
return Node_Id
is
4083 Spec
:= Build_Call_Helper_Spec
(Helper_Id
);
4084 Set_Must_Override
(Spec
, False);
4085 Set_Must_Not_Override
(Spec
, False);
4086 Set_Is_Inlined
(Helper_Id
);
4087 Set_Is_Public
(Helper_Id
);
4089 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
4091 -- Inherit debug info flag from Subp_Id to Helper_Id to allow
4092 -- debugging of the helper subprogram.
4094 if Needs_Debug_Info
(Subp_Id
) then
4095 Set_Debug_Info_Needed
(Helper_Id
);
4099 end Build_Call_Helper_Decl
;
4101 ----------------------------
4102 -- Build_Call_Helper_Spec --
4103 ----------------------------
4105 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
4107 Spec
: constant Node_Id
:= Parent
(Subp_Id
);
4108 Def_Id
: constant Node_Id
:= Defining_Unit_Name
(Spec
);
4110 Func_Formals
: constant List_Id
:= New_List
;
4111 P_Spec
: constant List_Id
:= Parameter_Specifications
(Spec
);
4112 Par_Formal
: Node_Id
;
4114 Param_Type
: Node_Id
;
4117 -- Create a list of formal parameters with the same types as the
4118 -- original subprogram but changing the controlling formal.
4120 Param
:= First
(P_Spec
);
4121 Formal
:= First_Formal
(Def_Id
);
4122 while Present
(Formal
) loop
4123 Par_Formal
:= Parent
(Formal
);
4125 if Is_Dynamic
and then Is_Controlling_Formal
(Formal
) then
4126 if Nkind
(Parameter_Type
(Par_Formal
))
4127 = N_Access_Definition
4130 Copy_Separate_Tree
(Parameter_Type
(Par_Formal
));
4131 Rewrite
(Subtype_Mark
(Param_Type
),
4132 Make_Attribute_Reference
(Loc
,
4133 Prefix
=> Relocate_Node
(Subtype_Mark
(Param_Type
)),
4134 Attribute_Name
=> Name_Class
));
4138 Make_Attribute_Reference
(Loc
,
4139 Prefix
=> New_Occurrence_Of
(Etype
(Formal
), Loc
),
4140 Attribute_Name
=> Name_Class
);
4143 Param_Type
:= New_Occurrence_Of
(Etype
(Formal
), Loc
);
4146 Append_To
(Func_Formals
,
4147 Make_Parameter_Specification
(Loc
,
4148 Defining_Identifier
=>
4149 Make_Defining_Identifier
(Loc
, Chars
(Formal
)),
4150 In_Present
=> In_Present
(Par_Formal
),
4151 Out_Present
=> Out_Present
(Par_Formal
),
4152 Null_Exclusion_Present
=> Null_Exclusion_Present
4154 Parameter_Type
=> Param_Type
));
4157 Next_Formal
(Formal
);
4161 Make_Function_Specification
(Loc
,
4162 Defining_Unit_Name
=> Spec_Id
,
4163 Parameter_Specifications
=> Func_Formals
,
4164 Result_Definition
=>
4165 New_Occurrence_Of
(Standard_Boolean
, Loc
));
4166 end Build_Call_Helper_Spec
;
4170 Helper_Body
: Node_Id
;
4171 Helper_Decl
: Node_Id
;
4173 -- Start of processing for Add_Call_Helper
4176 Helper_Decl
:= Build_Call_Helper_Decl
;
4177 Mutate_Ekind
(Helper_Id
, Ekind
(Subp_Id
));
4179 -- Add the helper to the freezing actions of the tagged type
4181 Append_Freeze_Action
(Tagged_Type
, Helper_Decl
);
4182 Analyze
(Helper_Decl
);
4184 Helper_Body
:= Build_Call_Helper_Body
;
4185 Append_Freeze_Action
(Tagged_Type
, Helper_Body
);
4187 -- If this helper is built as part of building the DTW at the
4188 -- freezing point of its tagged type then we cannot defer
4191 if Late_Overriding
then
4192 pragma Assert
(Is_Dispatch_Table_Wrapper
(Subp_Id
));
4193 Analyze
(Helper_Body
);
4195 end Add_Call_Helper
;
4197 -----------------------
4198 -- Build_Unique_Name --
4199 -----------------------
4201 function Build_Unique_Name
(Suffix
: String) return Name_Id
is
4203 -- Append the homonym number. Strip the leading space character in
4204 -- the image of natural numbers. Also do not add the homonym value
4207 if Has_Homonym
(Subp_Id
) and then Homonym_Number
(Subp_Id
) > 1 then
4209 S
: constant String := Homonym_Number
(Subp_Id
)'Img;
4212 return New_External_Name
(Chars
(Subp_Id
),
4213 Suffix
=> Suffix
& "_" & S
(2 .. S
'Last));
4217 return New_External_Name
(Chars
(Subp_Id
), Suffix
);
4218 end Build_Unique_Name
;
4222 Helper_Id
: Entity_Id
;
4224 -- Start of processing for Make_Class_Precondition_Subps
4227 if Present
(Class_Preconditions
(Subp_Id
))
4228 or Present
(Ignored_Class_Preconditions
(Subp_Id
))
4231 (Comes_From_Source
(Subp_Id
)
4232 or else Is_Dispatch_Table_Wrapper
(Subp_Id
));
4234 if No
(Dynamic_Call_Helper
(Subp_Id
)) then
4236 -- Build and add to the freezing actions of Tagged_Type its
4237 -- dynamic-call helper.
4240 Make_Defining_Identifier
(Loc
,
4241 Build_Unique_Name
(Suffix
=> "DP"));
4242 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> True);
4244 -- Link original subprogram to helper and vice versa
4246 Set_Dynamic_Call_Helper
(Subp_Id
, Helper_Id
);
4247 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4250 if not Is_Abstract_Subprogram
(Subp_Id
)
4251 and then No
(Static_Call_Helper
(Subp_Id
))
4253 -- Build and add to the freezing actions of Tagged_Type its
4254 -- static-call helper.
4257 Make_Defining_Identifier
(Loc
,
4258 Build_Unique_Name
(Suffix
=> "SP"));
4260 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> False);
4262 -- Link original subprogram to helper and vice versa
4264 Set_Static_Call_Helper
(Subp_Id
, Helper_Id
);
4265 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4267 -- Build and add to the freezing actions of Tagged_Type the
4268 -- indirect-call wrapper.
4270 Add_Indirect_Call_Wrapper
;
4273 end Make_Class_Precondition_Subps
;
4275 ----------------------------------------------
4276 -- Process_Class_Conditions_At_Freeze_Point --
4277 ----------------------------------------------
4279 procedure Process_Class_Conditions_At_Freeze_Point
(Typ
: Entity_Id
) is
4281 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
);
4282 -- Check class-wide pre/postconditions of Spec_Id
4284 function Has_Class_Postconditions_Subprogram
4285 (Spec_Id
: Entity_Id
) return Boolean;
4286 -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
4288 function Has_Class_Preconditions_Subprogram
4289 (Spec_Id
: Entity_Id
) return Boolean;
4290 -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
4292 ----------------------------
4293 -- Check_Class_Conditions --
4294 ----------------------------
4296 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
) is
4297 Par_Subp
: Entity_Id
;
4300 for Kind
in Condition_Kind
loop
4301 Par_Subp
:= Nearest_Class_Condition_Subprogram
(Kind
, Spec_Id
);
4303 if Present
(Par_Subp
) then
4304 Check_Class_Condition
4305 (Cond
=> Class_Condition
(Kind
, Par_Subp
),
4307 Par_Subp
=> Par_Subp
,
4308 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4309 | Class_Precondition
);
4312 end Check_Class_Conditions
;
4314 -----------------------------------------
4315 -- Has_Class_Postconditions_Subprogram --
4316 -----------------------------------------
4318 function Has_Class_Postconditions_Subprogram
4319 (Spec_Id
: Entity_Id
) return Boolean is
4322 Present
(Nearest_Class_Condition_Subprogram
4323 (Spec_Id
=> Spec_Id
,
4324 Kind
=> Class_Postcondition
))
4326 Present
(Nearest_Class_Condition_Subprogram
4327 (Spec_Id
=> Spec_Id
,
4328 Kind
=> Ignored_Class_Postcondition
));
4329 end Has_Class_Postconditions_Subprogram
;
4331 ----------------------------------------
4332 -- Has_Class_Preconditions_Subprogram --
4333 ----------------------------------------
4335 function Has_Class_Preconditions_Subprogram
4336 (Spec_Id
: Entity_Id
) return Boolean is
4339 Present
(Nearest_Class_Condition_Subprogram
4340 (Spec_Id
=> Spec_Id
,
4341 Kind
=> Class_Precondition
))
4343 Present
(Nearest_Class_Condition_Subprogram
4344 (Spec_Id
=> Spec_Id
,
4345 Kind
=> Ignored_Class_Precondition
));
4346 end Has_Class_Preconditions_Subprogram
;
4350 Prim_Elmt
: Elmt_Id
:= First_Elmt
(Primitive_Operations
(Typ
));
4353 -- Start of processing for Process_Class_Conditions_At_Freeze_Point
4356 while Present
(Prim_Elmt
) loop
4357 Prim
:= Node
(Prim_Elmt
);
4359 if Has_Class_Preconditions_Subprogram
(Prim
)
4360 or else Has_Class_Postconditions_Subprogram
(Prim
)
4362 if Comes_From_Source
(Prim
) then
4363 if Has_Significant_Contract
(Prim
) then
4364 Merge_Class_Conditions
(Prim
);
4367 -- Handle wrapper of protected operation
4369 elsif Is_Primitive_Wrapper
(Prim
) then
4370 Merge_Class_Conditions
(Prim
);
4372 -- Check inherited class-wide conditions, excluding internal
4373 -- entities built for mapping of interface primitives.
4375 elsif Is_Derived_Type
(Typ
)
4376 and then Present
(Alias
(Prim
))
4377 and then No
(Interface_Alias
(Prim
))
4379 Check_Class_Conditions
(Prim
);
4383 Next_Elmt
(Prim_Elmt
);
4385 end Process_Class_Conditions_At_Freeze_Point
;
4387 ----------------------------
4388 -- Merge_Class_Conditions --
4389 ----------------------------
4391 procedure Merge_Class_Conditions
(Spec_Id
: Entity_Id
) is
4393 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
);
4394 -- Collect all inherited class-wide conditions of Spec_Id and merge
4395 -- them into one big condition.
4397 ----------------------------------
4398 -- Process_Inherited_Conditions --
4399 ----------------------------------
4401 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
) is
4402 Tag_Typ
: constant Entity_Id
:= Find_Dispatching_Type
(Spec_Id
);
4403 Subps
: constant Subprogram_List
:= Inherited_Subprograms
(Spec_Id
);
4404 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
4406 function Inherit_Condition
4407 (Par_Subp
: Entity_Id
;
4408 Subp
: Entity_Id
) return Node_Id
;
4409 -- Inherit the class-wide condition from Par_Subp to Subp and adjust
4410 -- all the references to formals in the inherited condition.
4412 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
);
4413 -- Merge two class-wide preconditions or postconditions (the former
4414 -- are merged using "or else", and the latter are merged using "and-
4415 -- then"). The changes are accumulated in parameter Into.
4417 function Seen_Subp
(Id
: Entity_Id
) return Boolean;
4418 -- Return True if the contract of subprogram Id has been processed
4420 -----------------------
4421 -- Inherit_Condition --
4422 -----------------------
4424 function Inherit_Condition
4425 (Par_Subp
: Entity_Id
;
4426 Subp
: Entity_Id
) return Node_Id
4428 function Check_Condition
(Expr
: Node_Id
) return Boolean;
4429 -- Used in assertion to check that Expr has no reference to the
4430 -- formals of Par_Subp.
4432 ---------------------
4433 -- Check_Condition --
4434 ---------------------
4436 function Check_Condition
(Expr
: Node_Id
) return Boolean is
4437 Par_Formal_Id
: Entity_Id
;
4439 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
4440 -- Check occurrence of Par_Formal_Id
4446 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
4448 if Nkind
(N
) = N_Identifier
4449 and then Present
(Entity
(N
))
4450 and then Entity
(N
) = Par_Formal_Id
4458 function Check_Expression
is new Traverse_Func
(Check_Entity
);
4460 -- Start of processing for Check_Condition
4463 Par_Formal_Id
:= First_Formal
(Par_Subp
);
4465 while Present
(Par_Formal_Id
) loop
4466 if Check_Expression
(Expr
) = Abandon
then
4470 Next_Formal
(Par_Formal_Id
);
4474 end Check_Condition
;
4478 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4479 Par_Formal_Id
: Entity_Id
:= First_Formal
(Par_Subp
);
4480 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp
);
4481 New_Condition
: Node_Id
;
4484 while Present
(Par_Formal_Id
) loop
4485 Append_Elmt
(Par_Formal_Id
, Assoc_List
);
4486 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4488 Next_Formal
(Par_Formal_Id
);
4489 Next_Formal
(Subp_Formal_Id
);
4492 -- Check that Parent field of all the nodes have their correct
4493 -- decoration; required because otherwise mapped nodes with
4494 -- wrong Parent field are left unmodified in the copied tree
4495 -- and cause reporting wrong errors at later stages.
4498 (Check_Parents
(Class_Condition
(Kind
, Par_Subp
), Assoc_List
));
4502 (Source
=> Class_Condition
(Kind
, Par_Subp
),
4505 -- Ensure that the inherited condition has no reference to the
4506 -- formals of the parent subprogram.
4508 pragma Assert
(Check_Condition
(New_Condition
));
4510 return New_Condition
;
4511 end Inherit_Condition
;
4513 ----------------------
4514 -- Merge_Conditions --
4515 ----------------------
4517 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
) is
4518 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
;
4519 -- Return the boolean expression argument of a condition while
4520 -- updating its parentheses count for the subsequent merge.
4522 --------------------
4523 -- Expression_Arg --
4524 --------------------
4526 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
is
4528 if Paren_Count
(Expr
) = 0 then
4529 Set_Paren_Count
(Expr
, 1);
4537 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
4538 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
4539 Loc
: constant Source_Ptr
:= Sloc
(Into
);
4541 -- Start of processing for Merge_Conditions
4546 -- Merge the two preconditions by "or else"-ing them
4548 when Ignored_Class_Precondition
4549 | Class_Precondition
4553 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4554 Left_Opnd
=> From_Expr
));
4556 -- Merge the two postconditions by "and then"-ing them
4558 when Ignored_Class_Postcondition
4559 | Class_Postcondition
4563 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4564 Left_Opnd
=> From_Expr
));
4566 end Merge_Conditions
;
4572 function Seen_Subp
(Id
: Entity_Id
) return Boolean is
4574 for Index
in Seen
'Range loop
4575 if Seen
(Index
) = Id
then
4585 Class_Cond
: Node_Id
;
4587 Subp_Id
: Entity_Id
;
4588 Par_Prim
: Entity_Id
:= Empty
;
4589 Par_Iface_Prims
: Elist_Id
:= No_Elist
;
4591 -- Start of processing for Process_Inherited_Conditions
4594 Class_Cond
:= Class_Condition
(Kind
, Spec_Id
);
4596 -- Process parent primitives looking for nearest ancestor with
4597 -- class-wide conditions.
4599 for Index
in Subps
'Range loop
4600 Subp_Id
:= Subps
(Index
);
4603 and then Is_Ancestor
(Find_Dispatching_Type
(Subp_Id
), Tag_Typ
)
4605 if Present
(Alias
(Subp_Id
)) then
4606 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4609 -- Wrappers of class-wide pre/postconditions reference the
4610 -- parent primitive that has the inherited contract and help
4611 -- us to climb fast.
4613 if Is_Wrapper
(Subp_Id
)
4614 and then Present
(LSP_Subprogram
(Subp_Id
))
4616 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
4619 if not Seen_Subp
(Subp_Id
)
4620 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4622 Seen
(Index
) := Subp_Id
;
4623 Par_Prim
:= Subp_Id
;
4624 Par_Iface_Prims
:= Covered_Interface_Primitives
(Par_Prim
);
4626 Cond
:= Inherit_Condition
4628 Par_Subp
=> Subp_Id
);
4630 if Present
(Class_Cond
) then
4631 Merge_Conditions
(Cond
, Class_Cond
);
4636 Check_Class_Condition
4637 (Cond
=> Class_Cond
,
4639 Par_Subp
=> Subp_Id
,
4640 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4641 | Class_Precondition
);
4642 Build_Class_Wide_Expression
4643 (Pragma_Or_Expr
=> Class_Cond
,
4645 Par_Subp
=> Subp_Id
,
4646 Adjust_Sloc
=> False);
4648 -- We are done as soon as we process the nearest ancestor
4655 -- Process the contract of interface primitives not covered by
4656 -- the nearest ancestor.
4658 for Index
in Subps
'Range loop
4659 Subp_Id
:= Subps
(Index
);
4661 if Is_Interface
(Find_Dispatching_Type
(Subp_Id
)) then
4662 if Present
(Alias
(Subp_Id
)) then
4663 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4666 if not Seen_Subp
(Subp_Id
)
4667 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4668 and then not Contains
(Par_Iface_Prims
, Subp_Id
)
4670 Seen
(Index
) := Subp_Id
;
4672 Cond
:= Inherit_Condition
4674 Par_Subp
=> Subp_Id
);
4676 Check_Class_Condition
4679 Par_Subp
=> Subp_Id
,
4680 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4681 | Class_Precondition
);
4682 Build_Class_Wide_Expression
4683 (Pragma_Or_Expr
=> Cond
,
4685 Par_Subp
=> Subp_Id
,
4686 Adjust_Sloc
=> False);
4688 if Present
(Class_Cond
) then
4689 Merge_Conditions
(Cond
, Class_Cond
);
4697 Set_Class_Condition
(Kind
, Spec_Id
, Class_Cond
);
4698 end Process_Inherited_Conditions
;
4704 -- Start of processing for Merge_Class_Conditions
4707 for Kind
in Condition_Kind
loop
4708 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4710 -- If this subprogram has class-wide conditions then preanalyze
4711 -- them before processing inherited conditions since conditions
4712 -- are checked and merged from right to left.
4714 if Present
(Cond
) then
4715 Preanalyze_Condition
(Spec_Id
, Cond
);
4718 Process_Inherited_Conditions
(Kind
);
4720 -- Preanalyze merged inherited conditions
4722 if Cond
/= Class_Condition
(Kind
, Spec_Id
) then
4723 Preanalyze_Condition
(Spec_Id
,
4724 Class_Condition
(Kind
, Spec_Id
));
4727 end Merge_Class_Conditions
;
4729 ---------------------------------
4730 -- Preanalyze_Class_Conditions --
4731 ---------------------------------
4733 procedure Preanalyze_Class_Conditions
(Spec_Id
: Entity_Id
) is
4737 for Kind
in Condition_Kind
loop
4738 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4740 if Present
(Cond
) then
4741 Preanalyze_Condition
(Spec_Id
, Cond
);
4744 end Preanalyze_Class_Conditions
;
4746 --------------------------
4747 -- Preanalyze_Condition --
4748 --------------------------
4750 procedure Preanalyze_Condition
4754 procedure Clear_Unset_References
;
4755 -- Clear unset references on formals of Subp since preanalysis
4756 -- occurs in a place unrelated to the actual code.
4758 procedure Remove_Controlling_Arguments
;
4759 -- Traverse Expr and clear the Controlling_Argument of calls to
4760 -- nonabstract functions.
4762 procedure Restore_Original_Selected_Component
;
4763 -- Traverse Expr searching for dispatching calls to functions whose
4764 -- original node was a selected component, and replace them with
4765 -- their original node.
4767 ----------------------------
4768 -- Clear_Unset_References --
4769 ----------------------------
4771 procedure Clear_Unset_References
is
4772 F
: Entity_Id
:= First_Formal
(Subp
);
4775 while Present
(F
) loop
4776 Set_Unset_Reference
(F
, Empty
);
4779 end Clear_Unset_References
;
4781 ----------------------------------
4782 -- Remove_Controlling_Arguments --
4783 ----------------------------------
4785 procedure Remove_Controlling_Arguments
is
4786 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
;
4787 -- Reset the Controlling_Argument of calls to nonabstract
4790 ---------------------
4791 -- Remove_Ctrl_Arg --
4792 ---------------------
4794 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
is
4796 if Nkind
(N
) = N_Function_Call
4797 and then Present
(Controlling_Argument
(N
))
4798 and then not Is_Abstract_Subprogram
(Entity
(Name
(N
)))
4800 Set_Controlling_Argument
(N
, Empty
);
4804 end Remove_Ctrl_Arg
;
4806 procedure Remove_Ctrl_Args
is new Traverse_Proc
(Remove_Ctrl_Arg
);
4808 Remove_Ctrl_Args
(Expr
);
4809 end Remove_Controlling_Arguments
;
4811 -----------------------------------------
4812 -- Restore_Original_Selected_Component --
4813 -----------------------------------------
4815 procedure Restore_Original_Selected_Component
is
4816 Restored_Nodes_List
: Elist_Id
:= No_Elist
;
4818 procedure Fix_Parents
(N
: Node_Id
);
4819 -- Traverse the subtree of N fixing the Parent field of all the
4822 function Restore_Node
(N
: Node_Id
) return Traverse_Result
;
4823 -- Process dispatching calls to functions whose original node was
4824 -- a selected component, and replace them with their original
4825 -- node. Restored nodes are stored in the Restored_Nodes_List
4826 -- to fix the parent fields of their subtrees in a separate
4833 procedure Fix_Parents
(N
: Node_Id
) is
4836 (Parent_Node
: Node_Id
;
4837 Node
: Node_Id
) return Traverse_Result
;
4838 -- Process a single node
4845 (Parent_Node
: Node_Id
;
4846 Node
: Node_Id
) return Traverse_Result
4848 Par
: constant Node_Id
:= Parent
(Node
);
4851 if Par
/= Parent_Node
then
4852 if Is_List_Member
(Node
) then
4853 Set_List_Parent
(List_Containing
(Node
), Parent_Node
);
4855 Set_Parent
(Node
, Parent_Node
);
4862 procedure Fix_Parents
is
4863 new Traverse_Proc_With_Parent
(Fix_Parent
);
4873 function Restore_Node
(N
: Node_Id
) return Traverse_Result
is
4875 if Nkind
(N
) = N_Function_Call
4876 and then Nkind
(Original_Node
(N
)) = N_Selected_Component
4877 and then Is_Dispatching_Operation
(Entity
(Name
(N
)))
4879 Rewrite
(N
, Original_Node
(N
));
4880 Set_Original_Node
(N
, N
);
4882 -- Save the restored node in the Restored_Nodes_List to fix
4883 -- the parent fields of their subtrees in a separate tree
4886 Append_New_Elmt
(N
, Restored_Nodes_List
);
4892 procedure Restore_Nodes
is new Traverse_Proc
(Restore_Node
);
4894 -- Start of processing for Restore_Original_Selected_Component
4897 Restore_Nodes
(Expr
);
4899 -- After restoring the original node we must fix the decoration
4900 -- of the Parent attribute to ensure tree consistency; required
4901 -- because when the class-wide condition is inherited, calls to
4902 -- New_Copy_Tree will perform copies of this subtree, and formal
4903 -- occurrences with wrong Parent field cannot be mapped to the
4906 if Present
(Restored_Nodes_List
) then
4908 Elmt
: Elmt_Id
:= First_Elmt
(Restored_Nodes_List
);
4911 while Present
(Elmt
) loop
4912 Fix_Parents
(Node
(Elmt
));
4917 end Restore_Original_Selected_Component
;
4919 -- Start of processing for Preanalyze_Condition
4922 pragma Assert
(Present
(Expr
));
4923 pragma Assert
(Inside_Class_Condition_Preanalysis
= False);
4926 Install_Formals
(Subp
);
4927 Inside_Class_Condition_Preanalysis
:= True;
4929 Preanalyze_Spec_Expression
(Expr
, Standard_Boolean
);
4931 Inside_Class_Condition_Preanalysis
:= False;
4934 -- If this preanalyzed condition has occurrences of dispatching calls
4935 -- using the Object.Operation notation, during preanalysis such calls
4936 -- are rewritten as dispatching function calls; if at later stages
4937 -- this condition is inherited we must have restored the original
4938 -- selected-component node to ensure that the preanalysis of the
4939 -- inherited condition rewrites these dispatching calls in the
4940 -- correct context to avoid reporting spurious errors.
4942 Restore_Original_Selected_Component
;
4944 -- Traverse Expr and clear the Controlling_Argument of calls to
4945 -- nonabstract functions. Required since the preanalyzed condition
4946 -- is not yet installed on its definite context and will be cloned
4947 -- and extended in derivations with additional conditions.
4949 Remove_Controlling_Arguments
;
4951 -- Clear also attribute Unset_Reference; again because preanalysis
4952 -- occurs in a place unrelated to the actual code.
4954 Clear_Unset_References
;
4955 end Preanalyze_Condition
;
4957 ----------------------------------------
4958 -- Save_Global_References_In_Contract --
4959 ----------------------------------------
4961 procedure Save_Global_References_In_Contract
4965 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
4966 -- Save all global references in contract-related source pragmas found
4967 -- in the list, starting with pragma First_Prag.
4969 ------------------------------------
4970 -- Save_Global_References_In_List --
4971 ------------------------------------
4973 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
4974 Prag
: Node_Id
:= First_Prag
;
4977 while Present
(Prag
) loop
4978 if Is_Generic_Contract_Pragma
(Prag
) then
4979 Save_Global_References
(Prag
);
4982 Prag
:= Next_Pragma
(Prag
);
4984 end Save_Global_References_In_List
;
4988 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
4990 -- Start of processing for Save_Global_References_In_Contract
4993 -- The entity of the analyzed generic copy must be on the scope stack
4994 -- to ensure proper detection of global references.
4996 Push_Scope
(Gen_Id
);
4998 if Permits_Aspect_Specifications
(Templ
)
4999 and then Has_Aspects
(Templ
)
5001 Save_Global_References_In_Aspects
(Templ
);
5004 if Present
(Items
) then
5005 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
5006 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
5007 Save_Global_References_In_List
(Classifications
(Items
));
5011 end Save_Global_References_In_Contract
;
5013 -------------------------
5014 -- Set_Class_Condition --
5015 -------------------------
5017 procedure Set_Class_Condition
5018 (Kind
: Condition_Kind
;
5024 when Class_Postcondition
=>
5025 Set_Class_Postconditions
(Subp
, Cond
);
5027 when Class_Precondition
=>
5028 Set_Class_Preconditions
(Subp
, Cond
);
5030 when Ignored_Class_Postcondition
=>
5031 Set_Ignored_Class_Postconditions
(Subp
, Cond
);
5033 when Ignored_Class_Precondition
=>
5034 Set_Ignored_Class_Preconditions
(Subp
, Cond
);
5036 end Set_Class_Condition
;