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
: Node_Id
:= Subp_Id
;
2534 -- Enclosing_Declaration may return, for example,
2535 -- a N_Procedure_Specification node. Cope with this.
2537 Subp_Decl
:= Enclosing_Declaration
(Subp_Decl
);
2538 exit when Is_Declaration
(Subp_Decl
);
2539 Subp_Decl
:= Parent
(Subp_Decl
);
2540 pragma Assert
(Present
(Subp_Decl
));
2543 Insert_After_And_Analyze
(Subp_Decl
, Prag
);
2544 end Insert_Stable_Property_Check
;
2546 ------------------------------------
2547 -- Make_Stable_Property_Condition --
2548 ------------------------------------
2550 function Make_Stable_Property_Condition
2551 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
2553 function Call_Property_Function
return Node_Id
is
2557 New_Occurrence_Of
(Property_Function
, Loc
),
2558 Parameter_Associations
=>
2559 New_List
(New_Occurrence_Of
(Formal
, Loc
))));
2563 Call_Property_Function
,
2564 Make_Attribute_Reference
2566 Prefix
=> Call_Property_Function
,
2567 Attribute_Name
=> Name_Old
));
2568 end Make_Stable_Property_Condition
;
2570 -----------------------
2571 -- Stable_Properties --
2572 -----------------------
2574 function Stable_Properties
2575 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2576 return Subprogram_List
2578 Aspect_Spec
: Node_Id
:=
2579 Find_Value_Of_Aspect
2580 (Aspect_Bearer
, Aspect_Stable_Properties
,
2581 Class_Present
=> Class_Present
);
2583 -- ??? For a derived type, we wish Find_Value_Of_Aspect
2584 -- somehow knew that this aspect is not inherited.
2585 -- But it doesn't, so we cope with that here.
2587 -- There are probably issues here with inheritance from
2588 -- interface types, where just looking for the one parent type
2589 -- isn't enough. But this is far from the only work needed for
2590 -- Stable_Properties'Class for interface types.
2592 if Is_Derived_Type
(Aspect_Bearer
) then
2594 Parent_Type
: constant Entity_Id
:=
2595 Etype
(Base_Type
(Aspect_Bearer
));
2598 Find_Value_Of_Aspect
2599 (Parent_Type
, Aspect_Stable_Properties
,
2600 Class_Present
=> Class_Present
)
2602 -- prevent inheritance
2603 Aspect_Spec
:= Empty
;
2608 if No
(Aspect_Spec
) then
2609 Negated
:= Aspect_Bearer
= Subp_Id
;
2610 -- This is a little bit subtle.
2611 -- We need to assign True in the Subp_Id case in order to
2612 -- distinguish between no aspect spec at all vs. an
2613 -- explicitly specified "with S_P => []" empty list.
2614 -- In both cases Stable_Properties will return a length-0
2615 -- array, but the two cases are not equivalent.
2616 -- Very roughly speaking the lack of an S_P aspect spec for
2617 -- a subprogram would be equivalent to something like
2618 -- "with S_P => [not]", where we apply the "not" modifier to
2619 -- an empty set of subprograms, if such a construct existed.
2620 -- We could just assign True here, but it seems untidy to
2621 -- return True in the case of an aspect spec for a type
2622 -- (since negation is only allowed for subp S_P aspects).
2624 return (1 .. 0 => <>);
2626 return Parse_Aspect_Stable_Properties
2627 (Aspect_Spec
, Negated
=> Negated
);
2629 end Stable_Properties
;
2631 Formal
: Entity_Id
:= First_Formal
(Subp_Id
);
2632 Type_Of_Formal
: Entity_Id
;
2634 Subp_Properties_Negated
: Boolean;
2635 Subp_Properties
: constant Subprogram_List
:=
2636 Stable_Properties
(Subp_Id
, Subp_Properties_Negated
);
2638 -- start of processing for Add_Stable_Property_Contracts
2641 if not (Is_Primitive
(Subp_Id
) and then Comes_From_Source
(Subp_Id
))
2646 while Present
(Formal
) loop
2647 Type_Of_Formal
:= Base_Type
(Etype
(Formal
));
2649 if not Subp_Properties_Negated
then
2651 for SPF_Id
of Subp_Properties
loop
2652 if Type_Of_Formal
= Base_Type
(Etype
(First_Formal
(SPF_Id
)))
2653 and then Scope
(Type_Of_Formal
) = Scope
(Subp_Id
)
2655 -- ??? Need to filter out checks for SPFs that are
2656 -- mentioned explicitly in the postcondition of
2659 Insert_Stable_Property_Check
2660 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2664 elsif Scope
(Type_Of_Formal
) = Scope
(Subp_Id
) then
2666 Ignored
: Boolean range False .. False;
2668 Typ_Property_Funcs
: constant Subprogram_List
:=
2669 Stable_Properties
(Type_Of_Formal
, Negated
=> Ignored
);
2671 function Excluded_By_Aspect_Spec_Of_Subp
2672 (SPF_Id
: Entity_Id
) return Boolean;
2673 -- Examine Subp_Properties to determine whether SPF should
2676 -------------------------------------
2677 -- Excluded_By_Aspect_Spec_Of_Subp --
2678 -------------------------------------
2680 function Excluded_By_Aspect_Spec_Of_Subp
2681 (SPF_Id
: Entity_Id
) return Boolean is
2683 pragma Assert
(Subp_Properties_Negated
);
2684 -- Look through renames for equality test here ???
2685 return (for some F
of Subp_Properties
=> F
= SPF_Id
);
2686 end Excluded_By_Aspect_Spec_Of_Subp
;
2688 -- Look through renames for equality test here ???
2689 Subp_Is_Stable_Property_Function
: constant Boolean :=
2690 (for some F
of Typ_Property_Funcs
=> F
= Subp_Id
);
2692 if not Subp_Is_Stable_Property_Function
then
2693 for SPF_Id
of Typ_Property_Funcs
loop
2694 if not Excluded_By_Aspect_Spec_Of_Subp
(SPF_Id
) then
2695 -- ??? Need to filter out checks for SPFs that are
2696 -- mentioned explicitly in the postcondition of
2698 Insert_Stable_Property_Check
2699 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2705 Next_Formal
(Formal
);
2707 end Add_Stable_Property_Contracts
;
2709 -------------------------
2710 -- Append_Enabled_Item --
2711 -------------------------
2713 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2715 -- Do not chain ignored or disabled pragmas
2717 if Nkind
(Item
) = N_Pragma
2718 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2722 -- Otherwise, add the item
2729 -- If the pragma is a conjunct in a composite postcondition, it
2730 -- has been processed in reverse order. In the postcondition body
2731 -- it must appear before the others.
2733 if Nkind
(Item
) = N_Pragma
2734 and then From_Aspect_Specification
(Item
)
2735 and then Split_PPC
(Item
)
2737 Prepend
(Item
, List
);
2739 Append
(Item
, List
);
2742 end Append_Enabled_Item
;
2744 ----------------------------
2745 -- Process_Contract_Cases --
2746 ----------------------------
2748 procedure Process_Contract_Cases
2749 (Stmts
: in out List_Id
;
2752 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2753 -- Process pragma Contract_Cases for subprogram Subp_Id
2755 --------------------------------
2756 -- Process_Contract_Cases_For --
2757 --------------------------------
2759 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2760 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2764 if Present
(Items
) then
2765 Prag
:= Contract_Test_Cases
(Items
);
2766 while Present
(Prag
) loop
2767 if Is_Checked
(Prag
) then
2768 if Pragma_Name
(Prag
) = Name_Always_Terminates
then
2769 Expand_Pragma_Always_Terminates
(Prag
);
2771 elsif Pragma_Name
(Prag
) = Name_Contract_Cases
then
2772 Expand_Pragma_Contract_Cases
2778 elsif Pragma_Name
(Prag
) = Name_Exceptional_Cases
then
2779 Expand_Pragma_Exceptional_Cases
(Prag
);
2781 elsif Pragma_Name
(Prag
) = Name_Subprogram_Variant
then
2782 Expand_Pragma_Subprogram_Variant
2785 Body_Decls
=> Decls
);
2789 Prag
:= Next_Pragma
(Prag
);
2792 end Process_Contract_Cases_For
;
2794 -- Start of processing for Process_Contract_Cases
2797 Process_Contract_Cases_For
(Body_Id
);
2799 if Present
(Spec_Id
) then
2800 Process_Contract_Cases_For
(Spec_Id
);
2802 end Process_Contract_Cases
;
2804 ----------------------------
2805 -- Process_Postconditions --
2806 ----------------------------
2808 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2809 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2810 -- Collect all [refined] postconditions of a specific kind denoted
2811 -- by Post_Nam that belong to the body, and generate pragma Check
2812 -- equivalents in list Stmts.
2814 procedure Process_Spec_Postconditions
;
2815 -- Collect all [inherited] postconditions of the spec, and generate
2816 -- pragma Check equivalents in list Stmts.
2818 ---------------------------------
2819 -- Process_Body_Postconditions --
2820 ---------------------------------
2822 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2823 Items
: constant Node_Id
:= Contract
(Body_Id
);
2824 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2829 -- Process the contract
2831 if Present
(Items
) then
2832 Prag
:= Pre_Post_Conditions
(Items
);
2833 while Present
(Prag
) loop
2834 if Pragma_Name
(Prag
) = Post_Nam
2835 and then Is_Checked
(Prag
)
2838 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2842 Prag
:= Next_Pragma
(Prag
);
2846 -- The subprogram body being processed is actually the proper body
2847 -- of a stub with a corresponding spec. The subprogram stub may
2848 -- carry a postcondition pragma, in which case it must be taken
2849 -- into account. The pragma appears after the stub.
2851 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2852 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2853 while Present
(Decl
) loop
2855 -- Note that non-matching pragmas are skipped
2857 if Nkind
(Decl
) = N_Pragma
then
2858 if Pragma_Name
(Decl
) = Post_Nam
2859 and then Is_Checked
(Decl
)
2862 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2866 -- Skip internally generated code
2868 elsif not Comes_From_Source
(Decl
) then
2871 -- Postcondition pragmas are usually grouped together. There
2872 -- is no need to inspect the whole declarative list.
2881 end Process_Body_Postconditions
;
2883 ---------------------------------
2884 -- Process_Spec_Postconditions --
2885 ---------------------------------
2887 procedure Process_Spec_Postconditions
is
2888 Subps
: constant Subprogram_List
:=
2889 Inherited_Subprograms
(Spec_Id
);
2890 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
2892 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean;
2893 -- Return True if the contract of subprogram Subp_Id has been
2900 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean is
2902 for Index
in Seen
'Range loop
2903 if Seen
(Index
) = Subp_Id
then
2916 Subp_Id
: Entity_Id
;
2918 -- Start of processing for Process_Spec_Postconditions
2921 -- Process the contract
2923 Items
:= Contract
(Spec_Id
);
2925 if Present
(Items
) then
2926 Prag
:= Pre_Post_Conditions
(Items
);
2927 while Present
(Prag
) loop
2928 if Pragma_Name
(Prag
) = Name_Postcondition
2929 and then Is_Checked
(Prag
)
2932 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2936 Prag
:= Next_Pragma
(Prag
);
2940 -- Process the contracts of all inherited subprograms, looking for
2941 -- class-wide postconditions.
2943 for Index
in Subps
'Range loop
2944 Subp_Id
:= Subps
(Index
);
2946 if Present
(Alias
(Subp_Id
)) then
2947 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
2950 -- Wrappers of class-wide pre/postconditions reference the
2951 -- parent primitive that has the inherited contract.
2953 if Is_Wrapper
(Subp_Id
)
2954 and then Present
(LSP_Subprogram
(Subp_Id
))
2956 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
2959 Items
:= Contract
(Subp_Id
);
2961 if not Seen_Subp
(Subp_Id
) and then Present
(Items
) then
2962 Seen
(Index
) := Subp_Id
;
2964 Prag
:= Pre_Post_Conditions
(Items
);
2965 while Present
(Prag
) loop
2966 if Pragma_Name
(Prag
) = Name_Postcondition
2967 and then Class_Present
(Prag
)
2970 Build_Pragma_Check_Equivalent
2973 Inher_Id
=> Subp_Id
);
2975 -- The pragma Check equivalent of the class-wide
2976 -- postcondition is still created even though the
2977 -- pragma may be ignored because the equivalent
2978 -- performs semantic checks.
2980 if Is_Checked
(Prag
) then
2981 Append_Enabled_Item
(Item
, Stmts
);
2985 Prag
:= Next_Pragma
(Prag
);
2989 end Process_Spec_Postconditions
;
2991 pragma Unmodified
(Stmts
);
2992 -- Stmts is passed as IN OUT to signal that the list can be updated,
2993 -- even if the corresponding integer value representing the list does
2996 -- Start of processing for Process_Postconditions
2999 -- The processing of postconditions is done in reverse order (body
3000 -- first) to ensure the following arrangement:
3002 -- <refined postconditions from body>
3003 -- <postconditions from body>
3004 -- <postconditions from spec>
3005 -- <inherited postconditions>
3007 Process_Body_Postconditions
(Name_Refined_Post
);
3008 Process_Body_Postconditions
(Name_Postcondition
);
3010 if Present
(Spec_Id
) then
3011 Process_Spec_Postconditions
;
3013 end Process_Postconditions
;
3015 ---------------------------
3016 -- Process_Preconditions --
3017 ---------------------------
3019 procedure Process_Preconditions
(Decls
: in out List_Id
) is
3020 Insert_Node
: Node_Id
:= Empty
;
3021 -- The insertion node after which all pragma Check equivalents are
3024 procedure Prepend_To_Decls
(Item
: Node_Id
);
3025 -- Prepend a single item to the declarations of the subprogram body
3027 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
);
3028 -- Prepend a normal precondition to the declarations of the body and
3031 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
3032 -- Collect all preconditions of subprogram Subp_Id and prepend their
3033 -- pragma Check equivalents to the declarations of the body.
3035 ----------------------
3036 -- Prepend_To_Decls --
3037 ----------------------
3039 procedure Prepend_To_Decls
(Item
: Node_Id
) is
3041 -- Ensure that the body has a declarative list
3045 Set_Declarations
(Body_Decl
, Decls
);
3048 Prepend_To
(Decls
, Item
);
3049 end Prepend_To_Decls
;
3051 -----------------------------
3052 -- Prepend_Pragma_To_Decls --
3053 -----------------------------
3055 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
) is
3056 Check_Prag
: Node_Id
;
3059 -- Skip the sole class-wide precondition (if any) since it is
3060 -- processed by Merge_Class_Conditions.
3062 if Class_Present
(Prag
) then
3065 -- Accumulate the corresponding Check pragmas at the top of the
3066 -- declarations. Prepending the items ensures that they will be
3067 -- evaluated in their original order.
3070 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
3071 Prepend_To_Decls
(Check_Prag
);
3074 end Prepend_Pragma_To_Decls
;
3076 -------------------------------
3077 -- Process_Preconditions_For --
3078 -------------------------------
3080 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
3081 Items
: constant Node_Id
:= Contract
(Subp_Id
);
3082 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
3088 -- Process the contract. If the body is an expression function
3089 -- that is a completion, freeze types within, because this may
3090 -- not have been done yet, when the subprogram declaration and
3091 -- its completion by an expression function appear in distinct
3092 -- declarative lists of the same unit (visible and private).
3095 Was_Expression_Function
(Body_Decl
)
3096 and then Sloc
(Body_Id
) /= Sloc
(Subp_Id
)
3097 and then In_Same_Source_Unit
(Body_Id
, Subp_Id
)
3098 and then not In_Same_List
(Body_Decl
, Subp_Decl
);
3100 if Present
(Items
) then
3101 Prag
:= Pre_Post_Conditions
(Items
);
3102 while Present
(Prag
) loop
3103 if Pragma_Name
(Prag
) = Name_Precondition
3104 and then Is_Checked
(Prag
)
3107 and then Present
(Corresponding_Aspect
(Prag
))
3111 Typ
=> Standard_Boolean
,
3114 (First
(Pragma_Argument_Associations
(Prag
))),
3118 Prepend_Pragma_To_Decls
(Prag
);
3121 Prag
:= Next_Pragma
(Prag
);
3125 -- The subprogram declaration being processed is actually a body
3126 -- stub. The stub may carry a precondition pragma, in which case
3127 -- it must be taken into account. The pragma appears after the
3130 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
3132 -- Inspect the declarations following the body stub
3134 Decl
:= Next
(Subp_Decl
);
3135 while Present
(Decl
) loop
3137 -- Note that non-matching pragmas are skipped
3139 if Nkind
(Decl
) = N_Pragma
then
3140 if Pragma_Name
(Decl
) = Name_Precondition
3141 and then Is_Checked
(Decl
)
3143 Prepend_Pragma_To_Decls
(Decl
);
3146 -- Skip internally generated code
3148 elsif not Comes_From_Source
(Decl
) then
3151 -- Preconditions are usually grouped together. There is no
3152 -- need to inspect the whole declarative list.
3161 end Process_Preconditions_For
;
3165 Body_Decls
: constant List_Id
:= Declarations
(Body_Decl
);
3167 Next_Decl
: Node_Id
;
3169 -- Start of processing for Process_Preconditions
3172 -- Find the proper insertion point for all pragma Check equivalents
3174 if Present
(Body_Decls
) then
3175 Decl
:= First
(Body_Decls
);
3176 while Present
(Decl
) loop
3178 -- First source declaration terminates the search, because all
3179 -- preconditions must be evaluated prior to it, by definition.
3181 if Comes_From_Source
(Decl
) then
3184 -- Certain internally generated object renamings such as those
3185 -- for discriminants and protection fields must be elaborated
3186 -- before the preconditions are evaluated, as their expressions
3187 -- may mention the discriminants. The renamings include those
3188 -- for private components so we need to find the last such.
3190 elsif Is_Prologue_Renaming
(Decl
) then
3191 while Present
(Next
(Decl
))
3192 and then Is_Prologue_Renaming
(Next
(Decl
))
3197 Insert_Node
:= Decl
;
3199 -- Otherwise the declaration does not come from source. This
3200 -- also terminates the search, because internal code may raise
3201 -- exceptions which should not preempt the preconditions.
3210 -- The processing of preconditions is done in reverse order (body
3211 -- first), because each pragma Check equivalent is inserted at the
3212 -- top of the declarations. This ensures that the final order is
3213 -- consistent with following diagram:
3215 -- <inherited preconditions>
3216 -- <preconditions from spec>
3217 -- <preconditions from body>
3219 Process_Preconditions_For
(Body_Id
);
3221 -- Move the generated entry-call prologue renamings into the
3222 -- outer declarations for use in the preconditions.
3224 Decl
:= First
(Body_Decls
);
3225 while Present
(Decl
) and then Present
(Insert_Node
) loop
3226 Next_Decl
:= Next
(Decl
);
3228 Prepend_To_Decls
(Decl
);
3230 exit when Decl
= Insert_Node
;
3235 if Present
(Spec_Id
) then
3236 Process_Preconditions_For
(Spec_Id
);
3238 end Process_Preconditions
;
3242 Restore_Scope
: Boolean := False;
3244 Stmts
: List_Id
:= No_List
;
3245 Decls
: List_Id
:= New_List
;
3246 Subp_Id
: Entity_Id
;
3248 -- Start of processing for Expand_Subprogram_Contract
3251 -- Obtain the entity of the initial declaration
3253 if Present
(Spec_Id
) then
3259 -- Do not perform expansion activity when it is not needed
3261 if not Expander_Active
then
3264 -- GNATprove does not need the executable semantics of a contract
3266 elsif GNATprove_Mode
then
3269 -- The contract of a generic subprogram or one declared in a generic
3270 -- context is not expanded, as the corresponding instance will provide
3271 -- the executable semantics of the contract.
3273 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
3276 -- All subprograms carry a contract, but for some it is not significant
3277 -- and should not be processed. This is a small optimization.
3279 elsif not Has_Significant_Contract
(Subp_Id
) then
3282 -- The contract of an ignored Ghost subprogram does not need expansion,
3283 -- because the subprogram and all calls to it will be removed.
3285 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
3288 -- No action needed for helpers and indirect-call wrapper built to
3289 -- support class-wide preconditions.
3291 elsif Present
(Class_Preconditions_Subprogram
(Subp_Id
)) then
3294 -- Do not re-expand the same contract. This scenario occurs when a
3295 -- construct is rewritten into something else during its analysis
3296 -- (expression functions for instance).
3298 elsif Has_Expanded_Contract
(Subp_Id
) then
3302 -- Prevent multiple expansion attempts of the same contract
3304 Set_Has_Expanded_Contract
(Subp_Id
);
3306 -- Ensure that the formal parameters are visible when expanding all
3309 if not In_Open_Scopes
(Subp_Id
) then
3310 Restore_Scope
:= True;
3311 Push_Scope
(Subp_Id
);
3313 if Is_Generic_Subprogram
(Subp_Id
) then
3314 Install_Generic_Formals
(Subp_Id
);
3316 Install_Formals
(Subp_Id
);
3320 -- The expansion of a subprogram contract involves the creation of Check
3321 -- pragmas to verify the contract assertions of the spec and body in a
3322 -- particular order. The order is as follows:
3324 -- function Original_Code (...) return ... is
3325 -- <prologue renamings>
3326 -- <inherited preconditions>
3327 -- <preconditions from spec>
3328 -- <preconditions from body>
3329 -- <contract case conditions>
3331 -- function _Wrapped_Statements (...) return ... is
3332 -- <source declarations>
3334 -- <source statements>
3335 -- end _Wrapped_Statements;
3338 -- return Result : constant ... := _Wrapped_Statements do
3339 -- <refined postconditions from body>
3340 -- <postconditions from body>
3341 -- <postconditions from spec>
3342 -- <inherited postconditions>
3343 -- <contract case consequences>
3344 -- <invariant check of function result>
3345 -- <invariant and predicate checks of parameters
3347 -- end Original_Code;
3349 -- Step 1: augment contracts list with postconditions associated with
3350 -- Stable_Properties and Stable_Properties'Class aspects. This must
3351 -- precede Process_Postconditions.
3353 for Class_Present
in Boolean loop
3354 Add_Stable_Property_Contracts
3355 (Subp_Id
, Class_Present
=> Class_Present
);
3358 -- Step 2: Handle all preconditions. This action must come before the
3359 -- processing of pragma Contract_Cases because the pragma prepends items
3360 -- to the body declarations.
3362 Process_Preconditions
(Decls
);
3364 -- Step 3: Handle all postconditions. This action must come before the
3365 -- processing of pragma Contract_Cases because the pragma appends items
3368 Process_Postconditions
(Stmts
);
3370 -- Step 4: Handle pragma Contract_Cases. This action must come before
3371 -- the processing of invariants and predicates because those append
3372 -- items to list Stmts.
3374 Process_Contract_Cases
(Stmts
, Decls
);
3376 -- Step 5: Apply invariant and predicate checks on a function result and
3377 -- all formals. The resulting checks are accumulated in list Stmts.
3379 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3381 -- Step 6: Construct subprogram _wrapped_statements
3383 -- When no statements are present we still need to insert contract
3384 -- related declarations.
3387 Prepend_List_To
(Declarations
(Body_Decl
), Decls
);
3389 -- Otherwise, we need a wrapper
3392 Build_Subprogram_Contract_Wrapper
(Body_Id
, Stmts
, Decls
, Result
);
3395 if Restore_Scope
then
3398 end Expand_Subprogram_Contract
;
3400 -------------------------------
3401 -- Freeze_Previous_Contracts --
3402 -------------------------------
3404 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3405 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3406 pragma Inline
(Causes_Contract_Freezing
);
3407 -- Determine whether arbitrary node N causes contract freezing. This is
3408 -- used as an assertion for the current body declaration that caused
3409 -- contract freezing, and as a condition to detect body declaration that
3410 -- already caused contract freezing before.
3412 procedure Freeze_Contracts
;
3413 pragma Inline
(Freeze_Contracts
);
3414 -- Freeze the contracts of all eligible constructs which precede body
3417 procedure Freeze_Enclosing_Package_Body
;
3418 pragma Inline
(Freeze_Enclosing_Package_Body
);
3419 -- Freeze the contract of the nearest package body (if any) which
3420 -- encloses body Body_Decl.
3422 ------------------------------
3423 -- Causes_Contract_Freezing --
3424 ------------------------------
3426 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3428 -- The following condition matches guards for calls to
3429 -- Freeze_Previous_Contracts from routines that analyze various body
3430 -- declarations. In particular, it detects expression functions, as
3431 -- described in the call from Analyze_Subprogram_Body_Helper.
3434 Comes_From_Source
(Original_Node
(N
))
3437 N_Entry_Body | N_Package_Body | N_Protected_Body |
3438 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body
;
3439 end Causes_Contract_Freezing
;
3441 ----------------------
3442 -- Freeze_Contracts --
3443 ----------------------
3445 procedure Freeze_Contracts
is
3446 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3450 -- Nothing to do when the body which causes freezing does not appear
3451 -- in a declarative list because there cannot possibly be constructs
3454 if not Is_List_Member
(Body_Decl
) then
3458 -- Inspect the declarations preceding the body, and freeze individual
3459 -- contracts of eligible constructs.
3461 Decl
:= Prev
(Body_Decl
);
3462 while Present
(Decl
) loop
3464 -- Stop the traversal when a preceding construct that causes
3465 -- freezing is encountered as there is no point in refreezing
3466 -- the already frozen constructs.
3468 if Causes_Contract_Freezing
(Decl
) then
3471 -- Entry or subprogram declarations
3473 elsif Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
3474 | N_Entry_Declaration
3475 | N_Generic_Subprogram_Declaration
3476 | N_Subprogram_Declaration
3478 Analyze_Entry_Or_Subprogram_Contract
3479 (Subp_Id
=> Defining_Entity
(Decl
),
3480 Freeze_Id
=> Body_Id
);
3484 elsif Nkind
(Decl
) = N_Object_Declaration
then
3485 Analyze_Object_Contract
3486 (Obj_Id
=> Defining_Entity
(Decl
),
3487 Freeze_Id
=> Body_Id
);
3491 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
3492 | N_Single_Protected_Declaration
3494 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3496 -- Subprogram body stubs
3498 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3499 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3503 elsif Nkind
(Decl
) in N_Single_Task_Declaration
3504 | N_Task_Type_Declaration
3506 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3509 if Nkind
(Decl
) in N_Full_Type_Declaration
3510 | N_Private_Type_Declaration
3511 | N_Task_Type_Declaration
3512 | N_Protected_Type_Declaration
3513 | N_Formal_Type_Declaration
3515 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
3520 end Freeze_Contracts
;
3522 -----------------------------------
3523 -- Freeze_Enclosing_Package_Body --
3524 -----------------------------------
3526 procedure Freeze_Enclosing_Package_Body
is
3527 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3531 -- Climb the parent chain looking for an enclosing package body. Do
3532 -- not use the scope stack, because a body utilizes the entity of its
3533 -- corresponding spec.
3535 Par
:= Parent
(Body_Decl
);
3536 while Present
(Par
) loop
3537 if Nkind
(Par
) = N_Package_Body
then
3538 Analyze_Package_Body_Contract
3539 (Body_Id
=> Defining_Entity
(Par
),
3540 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3544 -- Do not look for an enclosing package body when the construct
3545 -- which causes freezing is a body generated for an expression
3546 -- function and it appears within a package spec. This ensures
3547 -- that the traversal will not reach too far up the parent chain
3548 -- and attempt to freeze a package body which must not be frozen.
3550 -- package body Enclosing_Body
3551 -- with Refined_State => (State => Var)
3553 -- package Nested is
3554 -- type Some_Type is ...;
3555 -- function Cause_Freezing return ...;
3557 -- function Cause_Freezing is (...);
3560 -- Var : Nested.Some_Type;
3562 elsif Nkind
(Par
) = N_Package_Declaration
3563 and then Nkind
(Orig_Decl
) = N_Expression_Function
3567 -- Prevent the search from going too far
3569 elsif Is_Body_Or_Package_Declaration
(Par
) then
3573 Par
:= Parent
(Par
);
3575 end Freeze_Enclosing_Package_Body
;
3579 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3581 -- Start of processing for Freeze_Previous_Contracts
3584 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3586 -- A body that is in the process of being inlined appears from source,
3587 -- but carries name _parent. Such a body does not cause freezing of
3590 if Chars
(Body_Id
) = Name_uParent
then
3594 Freeze_Enclosing_Package_Body
;
3596 end Freeze_Previous_Contracts
;
3598 ---------------------------------
3599 -- Inherit_Subprogram_Contract --
3600 ---------------------------------
3602 procedure Inherit_Subprogram_Contract
3604 From_Subp
: Entity_Id
)
3606 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3607 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3610 --------------------
3611 -- Inherit_Pragma --
3612 --------------------
3614 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3615 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3619 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3620 -- chains, therefore the node must be replicated. The new pragma is
3621 -- flagged as inherited for distinction purposes.
3623 if Present
(Prag
) then
3624 New_Prag
:= New_Copy_Tree
(Prag
);
3625 Set_Is_Inherited_Pragma
(New_Prag
);
3627 Add_Contract_Item
(New_Prag
, Subp
);
3631 -- Start of processing for Inherit_Subprogram_Contract
3634 -- Inheritance is carried out only when both entities are subprograms
3637 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3638 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3639 and then Present
(Contract
(From_Subp
))
3641 Inherit_Pragma
(Pragma_Extensions_Visible
);
3642 Inherit_Pragma
(Pragma_Side_Effects
);
3644 end Inherit_Subprogram_Contract
;
3646 -------------------------------------
3647 -- Instantiate_Subprogram_Contract --
3648 -------------------------------------
3650 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3651 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3652 -- Instantiate all contract-related source pragmas found in the list,
3653 -- starting with pragma First_Prag. Each instantiated pragma is added
3656 -------------------------
3657 -- Instantiate_Pragmas --
3658 -------------------------
3660 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3661 Inst_Prag
: Node_Id
;
3666 while Present
(Prag
) loop
3667 if Is_Generic_Contract_Pragma
(Prag
) then
3669 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3671 Set_Analyzed
(Inst_Prag
, False);
3672 Append_To
(L
, Inst_Prag
);
3675 Prag
:= Next_Pragma
(Prag
);
3677 end Instantiate_Pragmas
;
3681 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3683 -- Start of processing for Instantiate_Subprogram_Contract
3686 if Present
(Items
) then
3687 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3688 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3689 Instantiate_Pragmas
(Classifications
(Items
));
3691 end Instantiate_Subprogram_Contract
;
3693 --------------------------
3694 -- Is_Prologue_Renaming --
3695 --------------------------
3697 -- This should be turned into a flag and set during the expansion of
3698 -- task and protected types when the renamings get generated ???
3700 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
3707 if Nkind
(Decl
) = N_Object_Renaming_Declaration
3708 and then not Comes_From_Source
(Decl
)
3710 Obj
:= Defining_Entity
(Decl
);
3713 if Nkind
(Nam
) = N_Selected_Component
then
3714 -- Analyze the renaming declaration so we can further examine it
3716 if not Analyzed
(Decl
) then
3720 Pref
:= Prefix
(Nam
);
3721 Sel
:= Selector_Name
(Nam
);
3723 -- A discriminant renaming appears as
3724 -- Discr : constant ... := Prefix.Discr;
3726 if Ekind
(Obj
) = E_Constant
3727 and then Is_Entity_Name
(Sel
)
3728 and then Present
(Entity
(Sel
))
3729 and then Ekind
(Entity
(Sel
)) = E_Discriminant
3733 -- A protection field renaming appears as
3734 -- Prot : ... := _object._object;
3736 -- A renamed private component is just a component of
3737 -- _object, with an arbitrary name.
3739 elsif Ekind
(Obj
) in E_Variable | E_Constant
3740 and then Nkind
(Pref
) = N_Identifier
3741 and then Chars
(Pref
) = Name_uObject
3742 and then Nkind
(Sel
) = N_Identifier
3750 end Is_Prologue_Renaming
;
3752 -----------------------------------
3753 -- Make_Class_Precondition_Subps --
3754 -----------------------------------
3756 procedure Make_Class_Precondition_Subps
3757 (Subp_Id
: Entity_Id
;
3758 Late_Overriding
: Boolean := False)
3760 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
3761 Tagged_Type
: constant Entity_Id
:= Find_Dispatching_Type
(Subp_Id
);
3763 procedure Add_Indirect_Call_Wrapper
;
3764 -- Build the indirect-call wrapper and append it to the freezing actions
3767 procedure Add_Call_Helper
3768 (Helper_Id
: Entity_Id
;
3769 Is_Dynamic
: Boolean);
3770 -- Factorizes code for building a call helper with the given identifier
3771 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
3772 -- controls building the static or dynamic version of the helper.
3774 function Build_Unique_Name
(Suffix
: String) return Name_Id
;
3775 -- Build an unique new name adding suffix to Subp_Id name (plus its
3776 -- homonym number for values bigger than 1).
3778 -------------------------------
3779 -- Add_Indirect_Call_Wrapper --
3780 -------------------------------
3782 procedure Add_Indirect_Call_Wrapper
is
3784 function Build_ICW_Body
return Node_Id
;
3785 -- Build the body of the indirect call wrapper
3787 function Build_ICW_Decl
return Node_Id
;
3788 -- Build the declaration of the indirect call wrapper
3790 --------------------
3791 -- Build_ICW_Body --
3792 --------------------
3794 function Build_ICW_Body
return Node_Id
is
3795 ICW_Id
: constant Entity_Id
:= Indirect_Call_Wrapper
(Subp_Id
);
3796 Spec
: constant Node_Id
:= Parent
(ICW_Id
);
3797 Body_Spec
: Node_Id
;
3802 Body_Spec
:= Copy_Subprogram_Spec
(Spec
);
3804 -- Build call to wrapped subprogram
3807 Actuals
: constant List_Id
:= Empty_List
;
3808 Formal_Spec
: Entity_Id
:=
3809 First
(Parameter_Specifications
(Spec
));
3811 -- Build parameter association & call
3813 while Present
(Formal_Spec
) loop
3816 (Defining_Identifier
(Formal_Spec
), Loc
));
3820 if Ekind
(ICW_Id
) = E_Procedure
then
3822 Make_Procedure_Call_Statement
(Loc
,
3823 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3824 Parameter_Associations
=> Actuals
);
3827 Make_Simple_Return_Statement
(Loc
,
3829 Make_Function_Call
(Loc
,
3830 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3831 Parameter_Associations
=> Actuals
));
3836 Make_Subprogram_Body
(Loc
,
3837 Specification
=> Body_Spec
,
3838 Declarations
=> New_List
,
3839 Handled_Statement_Sequence
=>
3840 Make_Handled_Sequence_Of_Statements
(Loc
,
3841 Statements
=> New_List
(Call
)));
3843 -- The new operation is internal and overriding indicators do not
3846 Set_Must_Override
(Body_Spec
, False);
3851 --------------------
3852 -- Build_ICW_Decl --
3853 --------------------
3855 function Build_ICW_Decl
return Node_Id
is
3856 ICW_Id
: constant Entity_Id
:=
3857 Make_Defining_Identifier
(Loc
,
3858 Build_Unique_Name
(Suffix
=> "ICW"));
3863 Spec
:= Copy_Subprogram_Spec
(Parent
(Subp_Id
));
3864 Set_Must_Override
(Spec
, False);
3865 Set_Must_Not_Override
(Spec
, False);
3866 Set_Defining_Unit_Name
(Spec
, ICW_Id
);
3867 Mutate_Ekind
(ICW_Id
, Ekind
(Subp_Id
));
3868 Set_Is_Public
(ICW_Id
);
3870 -- The indirect call wrapper is commonly used for indirect calls
3871 -- but inlined for direct calls performed from the DTW.
3873 Set_Is_Inlined
(ICW_Id
);
3875 if Nkind
(Spec
) = N_Procedure_Specification
then
3876 Set_Null_Present
(Spec
, False);
3879 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
3881 -- Link original subprogram to indirect wrapper and vice versa
3883 Set_Indirect_Call_Wrapper
(Subp_Id
, ICW_Id
);
3884 Set_Class_Preconditions_Subprogram
(ICW_Id
, Subp_Id
);
3886 -- Inherit debug info flag to allow debugging the wrapper
3888 if Needs_Debug_Info
(Subp_Id
) then
3889 Set_Debug_Info_Needed
(ICW_Id
);
3900 -- Start of processing for Add_Indirect_Call_Wrapper
3903 pragma Assert
(No
(Indirect_Call_Wrapper
(Subp_Id
)));
3905 ICW_Decl
:= Build_ICW_Decl
;
3907 Append_Freeze_Action
(Tagged_Type
, ICW_Decl
);
3910 ICW_Body
:= Build_ICW_Body
;
3911 Append_Freeze_Action
(Tagged_Type
, ICW_Body
);
3913 -- We cannot defer the analysis of this ICW wrapper when it is
3914 -- built as a consequence of building its partner DTW wrapper
3915 -- at the freezing point of the tagged type.
3917 if Is_Dispatch_Table_Wrapper
(Subp_Id
) then
3920 end Add_Indirect_Call_Wrapper
;
3922 ---------------------
3923 -- Add_Call_Helper --
3924 ---------------------
3926 procedure Add_Call_Helper
3927 (Helper_Id
: Entity_Id
;
3928 Is_Dynamic
: Boolean)
3930 function Build_Call_Helper_Body
return Node_Id
;
3931 -- Build the body of a call helper
3933 function Build_Call_Helper_Decl
return Node_Id
;
3934 -- Build the declaration of a call helper
3936 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
;
3937 -- Build the specification of the helper
3939 ----------------------------
3940 -- Build_Call_Helper_Body --
3941 ----------------------------
3943 function Build_Call_Helper_Body
return Node_Id
is
3945 function Copy_And_Update_References
3946 (Expr
: Node_Id
) return Node_Id
;
3947 -- Copy Expr updating references to formals of Helper_Id; update
3948 -- also references to loop identifiers of quantified expressions.
3950 --------------------------------
3951 -- Copy_And_Update_References --
3952 --------------------------------
3954 function Copy_And_Update_References
3955 (Expr
: Node_Id
) return Node_Id
3957 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
3959 procedure Map_Quantified_Expression_Loop_Identifiers
;
3960 -- Traverse Expr and append to Assoc_List the mapping of loop
3961 -- identifers of quantified expressions with its new copy.
3963 ------------------------------------------------
3964 -- Map_Quantified_Expression_Loop_Identifiers --
3965 ------------------------------------------------
3967 procedure Map_Quantified_Expression_Loop_Identifiers
is
3968 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
;
3969 -- Append to Assoc_List the mapping of loop identifers of
3970 -- quantified expressions with its new copy.
3972 --------------------
3973 -- Map_Loop_Param --
3974 --------------------
3976 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
3979 if Nkind
(N
) = N_Loop_Parameter_Specification
3980 and then Nkind
(Parent
(N
)) = N_Quantified_Expression
3983 Def_Id
: constant Entity_Id
:=
3984 Defining_Identifier
(N
);
3986 Append_Elmt
(Def_Id
, Assoc_List
);
3987 Append_Elmt
(New_Copy
(Def_Id
), Assoc_List
);
3994 procedure Map_Quantified_Expressions
is
3995 new Traverse_Proc
(Map_Loop_Param
);
3998 Map_Quantified_Expressions
(Expr
);
3999 end Map_Quantified_Expression_Loop_Identifiers
;
4003 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp_Id
);
4004 Helper_Formal_Id
: Entity_Id
:= First_Formal
(Helper_Id
);
4006 -- Start of processing for Copy_And_Update_References
4009 while Present
(Subp_Formal_Id
) loop
4010 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4011 Append_Elmt
(Helper_Formal_Id
, Assoc_List
);
4013 Next_Formal
(Subp_Formal_Id
);
4014 Next_Formal
(Helper_Formal_Id
);
4017 Map_Quantified_Expression_Loop_Identifiers
;
4019 return New_Copy_Tree
(Expr
, Map
=> Assoc_List
);
4020 end Copy_And_Update_References
;
4024 Helper_Decl
: constant Node_Id
:= Parent
(Parent
(Helper_Id
));
4025 Body_Id
: Entity_Id
;
4026 Body_Spec
: Node_Id
;
4027 Body_Stmts
: Node_Id
;
4028 Helper_Body
: Node_Id
;
4029 Return_Expr
: Node_Id
;
4031 -- Start of processing for Build_Call_Helper_Body
4034 pragma Assert
(Analyzed
(Unit_Declaration_Node
(Helper_Id
)));
4035 pragma Assert
(No
(Corresponding_Body
(Helper_Decl
)));
4037 Body_Id
:= Make_Defining_Identifier
(Loc
, Chars
(Helper_Id
));
4038 Body_Spec
:= Build_Call_Helper_Spec
(Body_Id
);
4040 Set_Corresponding_Body
(Helper_Decl
, Body_Id
);
4041 Set_Must_Override
(Body_Spec
, False);
4043 if Present
(Class_Preconditions
(Subp_Id
))
4044 -- Evaluate the expression if we are building a dynamic helper
4045 -- or we are building a static helper for a non-abstract tagged
4046 -- type; for abstract tagged types the helper just returns True
4047 -- since it is called by the indirect call wrapper (ICW).
4051 not Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)))
4054 Copy_And_Update_References
(Class_Preconditions
(Subp_Id
));
4056 -- When the subprogram is compiled with assertions disabled the
4057 -- helper just returns True; done to avoid reporting errors at
4058 -- link time since a unit may be compiled with assertions disabled
4059 -- and another (which depends on it) compiled with assertions
4063 pragma Assert
(Present
(Ignored_Class_Preconditions
(Subp_Id
))
4064 or else Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)));
4065 Return_Expr
:= New_Occurrence_Of
(Standard_True
, Loc
);
4069 Make_Handled_Sequence_Of_Statements
(Loc
,
4070 Statements
=> New_List
(
4071 Make_Simple_Return_Statement
(Loc
, Return_Expr
)));
4074 Make_Subprogram_Body
(Loc
,
4075 Specification
=> Body_Spec
,
4076 Declarations
=> New_List
,
4077 Handled_Statement_Sequence
=> Body_Stmts
);
4080 end Build_Call_Helper_Body
;
4082 ----------------------------
4083 -- Build_Call_Helper_Decl --
4084 ----------------------------
4086 function Build_Call_Helper_Decl
return Node_Id
is
4091 Spec
:= Build_Call_Helper_Spec
(Helper_Id
);
4092 Set_Must_Override
(Spec
, False);
4093 Set_Must_Not_Override
(Spec
, False);
4094 Set_Is_Inlined
(Helper_Id
);
4095 Set_Is_Public
(Helper_Id
);
4097 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
4099 -- Inherit debug info flag from Subp_Id to Helper_Id to allow
4100 -- debugging of the helper subprogram.
4102 if Needs_Debug_Info
(Subp_Id
) then
4103 Set_Debug_Info_Needed
(Helper_Id
);
4107 end Build_Call_Helper_Decl
;
4109 ----------------------------
4110 -- Build_Call_Helper_Spec --
4111 ----------------------------
4113 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
4115 Spec
: constant Node_Id
:= Parent
(Subp_Id
);
4116 Def_Id
: constant Node_Id
:= Defining_Unit_Name
(Spec
);
4118 Func_Formals
: constant List_Id
:= New_List
;
4119 P_Spec
: constant List_Id
:= Parameter_Specifications
(Spec
);
4120 Par_Formal
: Node_Id
;
4122 Param_Type
: Node_Id
;
4125 -- Create a list of formal parameters with the same types as the
4126 -- original subprogram but changing the controlling formal.
4128 Param
:= First
(P_Spec
);
4129 Formal
:= First_Formal
(Def_Id
);
4130 while Present
(Formal
) loop
4131 Par_Formal
:= Parent
(Formal
);
4133 if Is_Dynamic
and then Is_Controlling_Formal
(Formal
) then
4134 if Nkind
(Parameter_Type
(Par_Formal
))
4135 = N_Access_Definition
4138 Copy_Separate_Tree
(Parameter_Type
(Par_Formal
));
4139 Rewrite
(Subtype_Mark
(Param_Type
),
4140 Make_Attribute_Reference
(Loc
,
4141 Prefix
=> Relocate_Node
(Subtype_Mark
(Param_Type
)),
4142 Attribute_Name
=> Name_Class
));
4146 Make_Attribute_Reference
(Loc
,
4147 Prefix
=> New_Occurrence_Of
(Etype
(Formal
), Loc
),
4148 Attribute_Name
=> Name_Class
);
4151 Param_Type
:= New_Occurrence_Of
(Etype
(Formal
), Loc
);
4154 Append_To
(Func_Formals
,
4155 Make_Parameter_Specification
(Loc
,
4156 Defining_Identifier
=>
4157 Make_Defining_Identifier
(Loc
, Chars
(Formal
)),
4158 In_Present
=> In_Present
(Par_Formal
),
4159 Out_Present
=> Out_Present
(Par_Formal
),
4160 Null_Exclusion_Present
=> Null_Exclusion_Present
4162 Parameter_Type
=> Param_Type
));
4165 Next_Formal
(Formal
);
4169 Make_Function_Specification
(Loc
,
4170 Defining_Unit_Name
=> Spec_Id
,
4171 Parameter_Specifications
=> Func_Formals
,
4172 Result_Definition
=>
4173 New_Occurrence_Of
(Standard_Boolean
, Loc
));
4174 end Build_Call_Helper_Spec
;
4178 Helper_Body
: Node_Id
;
4179 Helper_Decl
: Node_Id
;
4181 -- Start of processing for Add_Call_Helper
4184 Helper_Decl
:= Build_Call_Helper_Decl
;
4185 Mutate_Ekind
(Helper_Id
, Ekind
(Subp_Id
));
4187 -- Add the helper to the freezing actions of the tagged type
4189 Append_Freeze_Action
(Tagged_Type
, Helper_Decl
);
4190 Analyze
(Helper_Decl
);
4192 Helper_Body
:= Build_Call_Helper_Body
;
4193 Append_Freeze_Action
(Tagged_Type
, Helper_Body
);
4195 -- If this helper is built as part of building the DTW at the
4196 -- freezing point of its tagged type then we cannot defer
4199 if Late_Overriding
then
4200 pragma Assert
(Is_Dispatch_Table_Wrapper
(Subp_Id
));
4201 Analyze
(Helper_Body
);
4203 end Add_Call_Helper
;
4205 -----------------------
4206 -- Build_Unique_Name --
4207 -----------------------
4209 function Build_Unique_Name
(Suffix
: String) return Name_Id
is
4211 -- Append the homonym number. Strip the leading space character in
4212 -- the image of natural numbers. Also do not add the homonym value
4215 if Has_Homonym
(Subp_Id
) and then Homonym_Number
(Subp_Id
) > 1 then
4217 S
: constant String := Homonym_Number
(Subp_Id
)'Img;
4220 return New_External_Name
(Chars
(Subp_Id
),
4221 Suffix
=> Suffix
& "_" & S
(2 .. S
'Last));
4225 return New_External_Name
(Chars
(Subp_Id
), Suffix
);
4226 end Build_Unique_Name
;
4230 Helper_Id
: Entity_Id
;
4232 -- Start of processing for Make_Class_Precondition_Subps
4235 if Present
(Class_Preconditions
(Subp_Id
))
4236 or Present
(Ignored_Class_Preconditions
(Subp_Id
))
4239 (Comes_From_Source
(Subp_Id
)
4240 or else Is_Dispatch_Table_Wrapper
(Subp_Id
));
4242 if No
(Dynamic_Call_Helper
(Subp_Id
)) then
4244 -- Build and add to the freezing actions of Tagged_Type its
4245 -- dynamic-call helper.
4248 Make_Defining_Identifier
(Loc
,
4249 Build_Unique_Name
(Suffix
=> "DP"));
4250 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> True);
4252 -- Link original subprogram to helper and vice versa
4254 Set_Dynamic_Call_Helper
(Subp_Id
, Helper_Id
);
4255 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4258 if not Is_Abstract_Subprogram
(Subp_Id
)
4259 and then No
(Static_Call_Helper
(Subp_Id
))
4261 -- Build and add to the freezing actions of Tagged_Type its
4262 -- static-call helper.
4265 Make_Defining_Identifier
(Loc
,
4266 Build_Unique_Name
(Suffix
=> "SP"));
4268 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> False);
4270 -- Link original subprogram to helper and vice versa
4272 Set_Static_Call_Helper
(Subp_Id
, Helper_Id
);
4273 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4275 -- Build and add to the freezing actions of Tagged_Type the
4276 -- indirect-call wrapper.
4278 Add_Indirect_Call_Wrapper
;
4281 end Make_Class_Precondition_Subps
;
4283 ----------------------------------------------
4284 -- Process_Class_Conditions_At_Freeze_Point --
4285 ----------------------------------------------
4287 procedure Process_Class_Conditions_At_Freeze_Point
(Typ
: Entity_Id
) is
4289 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
);
4290 -- Check class-wide pre/postconditions of Spec_Id
4292 function Has_Class_Postconditions_Subprogram
4293 (Spec_Id
: Entity_Id
) return Boolean;
4294 -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
4296 function Has_Class_Preconditions_Subprogram
4297 (Spec_Id
: Entity_Id
) return Boolean;
4298 -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
4300 ----------------------------
4301 -- Check_Class_Conditions --
4302 ----------------------------
4304 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
) is
4305 Par_Subp
: Entity_Id
;
4308 for Kind
in Condition_Kind
loop
4309 Par_Subp
:= Nearest_Class_Condition_Subprogram
(Kind
, Spec_Id
);
4311 if Present
(Par_Subp
) then
4312 Check_Class_Condition
4313 (Cond
=> Class_Condition
(Kind
, Par_Subp
),
4315 Par_Subp
=> Par_Subp
,
4316 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4317 | Class_Precondition
);
4320 end Check_Class_Conditions
;
4322 -----------------------------------------
4323 -- Has_Class_Postconditions_Subprogram --
4324 -----------------------------------------
4326 function Has_Class_Postconditions_Subprogram
4327 (Spec_Id
: Entity_Id
) return Boolean is
4330 Present
(Nearest_Class_Condition_Subprogram
4331 (Spec_Id
=> Spec_Id
,
4332 Kind
=> Class_Postcondition
))
4334 Present
(Nearest_Class_Condition_Subprogram
4335 (Spec_Id
=> Spec_Id
,
4336 Kind
=> Ignored_Class_Postcondition
));
4337 end Has_Class_Postconditions_Subprogram
;
4339 ----------------------------------------
4340 -- Has_Class_Preconditions_Subprogram --
4341 ----------------------------------------
4343 function Has_Class_Preconditions_Subprogram
4344 (Spec_Id
: Entity_Id
) return Boolean is
4347 Present
(Nearest_Class_Condition_Subprogram
4348 (Spec_Id
=> Spec_Id
,
4349 Kind
=> Class_Precondition
))
4351 Present
(Nearest_Class_Condition_Subprogram
4352 (Spec_Id
=> Spec_Id
,
4353 Kind
=> Ignored_Class_Precondition
));
4354 end Has_Class_Preconditions_Subprogram
;
4358 Prim_Elmt
: Elmt_Id
:= First_Elmt
(Primitive_Operations
(Typ
));
4361 -- Start of processing for Process_Class_Conditions_At_Freeze_Point
4364 while Present
(Prim_Elmt
) loop
4365 Prim
:= Node
(Prim_Elmt
);
4367 if Has_Class_Preconditions_Subprogram
(Prim
)
4368 or else Has_Class_Postconditions_Subprogram
(Prim
)
4370 if Comes_From_Source
(Prim
) then
4371 if Has_Significant_Contract
(Prim
) then
4372 Merge_Class_Conditions
(Prim
);
4375 -- Handle wrapper of protected operation
4377 elsif Is_Primitive_Wrapper
(Prim
) then
4378 Merge_Class_Conditions
(Prim
);
4380 -- Check inherited class-wide conditions, excluding internal
4381 -- entities built for mapping of interface primitives.
4383 elsif Is_Derived_Type
(Typ
)
4384 and then Present
(Alias
(Prim
))
4385 and then No
(Interface_Alias
(Prim
))
4387 Check_Class_Conditions
(Prim
);
4391 Next_Elmt
(Prim_Elmt
);
4393 end Process_Class_Conditions_At_Freeze_Point
;
4395 ----------------------------
4396 -- Merge_Class_Conditions --
4397 ----------------------------
4399 procedure Merge_Class_Conditions
(Spec_Id
: Entity_Id
) is
4401 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
);
4402 -- Collect all inherited class-wide conditions of Spec_Id and merge
4403 -- them into one big condition.
4405 ----------------------------------
4406 -- Process_Inherited_Conditions --
4407 ----------------------------------
4409 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
) is
4410 Tag_Typ
: constant Entity_Id
:= Find_Dispatching_Type
(Spec_Id
);
4411 Subps
: constant Subprogram_List
:= Inherited_Subprograms
(Spec_Id
);
4412 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
4414 function Inherit_Condition
4415 (Par_Subp
: Entity_Id
;
4416 Subp
: Entity_Id
) return Node_Id
;
4417 -- Inherit the class-wide condition from Par_Subp to Subp and adjust
4418 -- all the references to formals in the inherited condition.
4420 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
);
4421 -- Merge two class-wide preconditions or postconditions (the former
4422 -- are merged using "or else", and the latter are merged using "and-
4423 -- then"). The changes are accumulated in parameter Into.
4425 function Seen_Subp
(Id
: Entity_Id
) return Boolean;
4426 -- Return True if the contract of subprogram Id has been processed
4428 -----------------------
4429 -- Inherit_Condition --
4430 -----------------------
4432 function Inherit_Condition
4433 (Par_Subp
: Entity_Id
;
4434 Subp
: Entity_Id
) return Node_Id
4436 function Check_Condition
(Expr
: Node_Id
) return Boolean;
4437 -- Used in assertion to check that Expr has no reference to the
4438 -- formals of Par_Subp.
4440 ---------------------
4441 -- Check_Condition --
4442 ---------------------
4444 function Check_Condition
(Expr
: Node_Id
) return Boolean is
4445 Par_Formal_Id
: Entity_Id
;
4447 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
4448 -- Check occurrence of Par_Formal_Id
4454 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
4456 if Nkind
(N
) = N_Identifier
4457 and then Present
(Entity
(N
))
4458 and then Entity
(N
) = Par_Formal_Id
4466 function Check_Expression
is new Traverse_Func
(Check_Entity
);
4468 -- Start of processing for Check_Condition
4471 Par_Formal_Id
:= First_Formal
(Par_Subp
);
4473 while Present
(Par_Formal_Id
) loop
4474 if Check_Expression
(Expr
) = Abandon
then
4478 Next_Formal
(Par_Formal_Id
);
4482 end Check_Condition
;
4486 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4487 Par_Formal_Id
: Entity_Id
:= First_Formal
(Par_Subp
);
4488 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp
);
4489 New_Condition
: Node_Id
;
4492 while Present
(Par_Formal_Id
) loop
4493 Append_Elmt
(Par_Formal_Id
, Assoc_List
);
4494 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4496 Next_Formal
(Par_Formal_Id
);
4497 Next_Formal
(Subp_Formal_Id
);
4500 -- Check that Parent field of all the nodes have their correct
4501 -- decoration; required because otherwise mapped nodes with
4502 -- wrong Parent field are left unmodified in the copied tree
4503 -- and cause reporting wrong errors at later stages.
4506 (Check_Parents
(Class_Condition
(Kind
, Par_Subp
), Assoc_List
));
4510 (Source
=> Class_Condition
(Kind
, Par_Subp
),
4513 -- Ensure that the inherited condition has no reference to the
4514 -- formals of the parent subprogram.
4516 pragma Assert
(Check_Condition
(New_Condition
));
4518 return New_Condition
;
4519 end Inherit_Condition
;
4521 ----------------------
4522 -- Merge_Conditions --
4523 ----------------------
4525 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
) is
4526 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
;
4527 -- Return the boolean expression argument of a condition while
4528 -- updating its parentheses count for the subsequent merge.
4530 --------------------
4531 -- Expression_Arg --
4532 --------------------
4534 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
is
4536 if Paren_Count
(Expr
) = 0 then
4537 Set_Paren_Count
(Expr
, 1);
4545 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
4546 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
4547 Loc
: constant Source_Ptr
:= Sloc
(Into
);
4549 -- Start of processing for Merge_Conditions
4554 -- Merge the two preconditions by "or else"-ing them
4556 when Ignored_Class_Precondition
4557 | Class_Precondition
4561 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4562 Left_Opnd
=> From_Expr
));
4564 -- Merge the two postconditions by "and then"-ing them
4566 when Ignored_Class_Postcondition
4567 | Class_Postcondition
4571 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4572 Left_Opnd
=> From_Expr
));
4574 end Merge_Conditions
;
4580 function Seen_Subp
(Id
: Entity_Id
) return Boolean is
4582 for Index
in Seen
'Range loop
4583 if Seen
(Index
) = Id
then
4593 Class_Cond
: Node_Id
;
4595 Subp_Id
: Entity_Id
;
4596 Par_Prim
: Entity_Id
:= Empty
;
4597 Par_Iface_Prims
: Elist_Id
:= No_Elist
;
4599 -- Start of processing for Process_Inherited_Conditions
4602 Class_Cond
:= Class_Condition
(Kind
, Spec_Id
);
4604 -- Process parent primitives looking for nearest ancestor with
4605 -- class-wide conditions.
4607 for Index
in Subps
'Range loop
4608 Subp_Id
:= Subps
(Index
);
4611 and then Is_Ancestor
(Find_Dispatching_Type
(Subp_Id
), Tag_Typ
)
4613 if Present
(Alias
(Subp_Id
)) then
4614 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4617 -- Wrappers of class-wide pre/postconditions reference the
4618 -- parent primitive that has the inherited contract and help
4619 -- us to climb fast.
4621 if Is_Wrapper
(Subp_Id
)
4622 and then Present
(LSP_Subprogram
(Subp_Id
))
4624 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
4627 if not Seen_Subp
(Subp_Id
)
4628 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4630 Seen
(Index
) := Subp_Id
;
4631 Par_Prim
:= Subp_Id
;
4632 Par_Iface_Prims
:= Covered_Interface_Primitives
(Par_Prim
);
4634 Cond
:= Inherit_Condition
4636 Par_Subp
=> Subp_Id
);
4638 if Present
(Class_Cond
) then
4639 Merge_Conditions
(Cond
, Class_Cond
);
4644 Check_Class_Condition
4645 (Cond
=> Class_Cond
,
4647 Par_Subp
=> Subp_Id
,
4648 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4649 | Class_Precondition
);
4650 Build_Class_Wide_Expression
4651 (Pragma_Or_Expr
=> Class_Cond
,
4653 Par_Subp
=> Subp_Id
,
4654 Adjust_Sloc
=> False);
4656 -- We are done as soon as we process the nearest ancestor
4663 -- Process the contract of interface primitives not covered by
4664 -- the nearest ancestor.
4666 for Index
in Subps
'Range loop
4667 Subp_Id
:= Subps
(Index
);
4669 if Is_Interface
(Find_Dispatching_Type
(Subp_Id
)) then
4670 if Present
(Alias
(Subp_Id
)) then
4671 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4674 if not Seen_Subp
(Subp_Id
)
4675 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4676 and then not Contains
(Par_Iface_Prims
, Subp_Id
)
4678 Seen
(Index
) := Subp_Id
;
4680 Cond
:= Inherit_Condition
4682 Par_Subp
=> Subp_Id
);
4684 Check_Class_Condition
4687 Par_Subp
=> Subp_Id
,
4688 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4689 | Class_Precondition
);
4690 Build_Class_Wide_Expression
4691 (Pragma_Or_Expr
=> Cond
,
4693 Par_Subp
=> Subp_Id
,
4694 Adjust_Sloc
=> False);
4696 if Present
(Class_Cond
) then
4697 Merge_Conditions
(Cond
, Class_Cond
);
4705 Set_Class_Condition
(Kind
, Spec_Id
, Class_Cond
);
4706 end Process_Inherited_Conditions
;
4712 -- Start of processing for Merge_Class_Conditions
4715 for Kind
in Condition_Kind
loop
4716 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4718 -- If this subprogram has class-wide conditions then preanalyze
4719 -- them before processing inherited conditions since conditions
4720 -- are checked and merged from right to left.
4722 if Present
(Cond
) then
4723 Preanalyze_Condition
(Spec_Id
, Cond
);
4726 Process_Inherited_Conditions
(Kind
);
4728 -- Preanalyze merged inherited conditions
4730 if Cond
/= Class_Condition
(Kind
, Spec_Id
) then
4731 Preanalyze_Condition
(Spec_Id
,
4732 Class_Condition
(Kind
, Spec_Id
));
4735 end Merge_Class_Conditions
;
4737 ---------------------------------
4738 -- Preanalyze_Class_Conditions --
4739 ---------------------------------
4741 procedure Preanalyze_Class_Conditions
(Spec_Id
: Entity_Id
) is
4745 for Kind
in Condition_Kind
loop
4746 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4748 if Present
(Cond
) then
4749 Preanalyze_Condition
(Spec_Id
, Cond
);
4752 end Preanalyze_Class_Conditions
;
4754 --------------------------
4755 -- Preanalyze_Condition --
4756 --------------------------
4758 procedure Preanalyze_Condition
4762 procedure Clear_Unset_References
;
4763 -- Clear unset references on formals of Subp since preanalysis
4764 -- occurs in a place unrelated to the actual code.
4766 procedure Remove_Controlling_Arguments
;
4767 -- Traverse Expr and clear the Controlling_Argument of calls to
4768 -- nonabstract functions.
4770 procedure Restore_Original_Selected_Component
;
4771 -- Traverse Expr searching for dispatching calls to functions whose
4772 -- original node was a selected component, and replace them with
4773 -- their original node.
4775 ----------------------------
4776 -- Clear_Unset_References --
4777 ----------------------------
4779 procedure Clear_Unset_References
is
4780 F
: Entity_Id
:= First_Formal
(Subp
);
4783 while Present
(F
) loop
4784 Set_Unset_Reference
(F
, Empty
);
4787 end Clear_Unset_References
;
4789 ----------------------------------
4790 -- Remove_Controlling_Arguments --
4791 ----------------------------------
4793 procedure Remove_Controlling_Arguments
is
4794 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
;
4795 -- Reset the Controlling_Argument of calls to nonabstract
4798 ---------------------
4799 -- Remove_Ctrl_Arg --
4800 ---------------------
4802 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
is
4804 if Nkind
(N
) = N_Function_Call
4805 and then Present
(Controlling_Argument
(N
))
4806 and then not Is_Abstract_Subprogram
(Entity
(Name
(N
)))
4808 Set_Controlling_Argument
(N
, Empty
);
4812 end Remove_Ctrl_Arg
;
4814 procedure Remove_Ctrl_Args
is new Traverse_Proc
(Remove_Ctrl_Arg
);
4816 Remove_Ctrl_Args
(Expr
);
4817 end Remove_Controlling_Arguments
;
4819 -----------------------------------------
4820 -- Restore_Original_Selected_Component --
4821 -----------------------------------------
4823 procedure Restore_Original_Selected_Component
is
4824 Restored_Nodes_List
: Elist_Id
:= No_Elist
;
4826 procedure Fix_Parents
(N
: Node_Id
);
4827 -- Traverse the subtree of N fixing the Parent field of all the
4830 function Restore_Node
(N
: Node_Id
) return Traverse_Result
;
4831 -- Process dispatching calls to functions whose original node was
4832 -- a selected component, and replace them with their original
4833 -- node. Restored nodes are stored in the Restored_Nodes_List
4834 -- to fix the parent fields of their subtrees in a separate
4841 procedure Fix_Parents
(N
: Node_Id
) is
4844 (Parent_Node
: Node_Id
;
4845 Node
: Node_Id
) return Traverse_Result
;
4846 -- Process a single node
4853 (Parent_Node
: Node_Id
;
4854 Node
: Node_Id
) return Traverse_Result
4856 Par
: constant Node_Id
:= Parent
(Node
);
4859 if Par
/= Parent_Node
then
4860 if Is_List_Member
(Node
) then
4861 Set_List_Parent
(List_Containing
(Node
), Parent_Node
);
4863 Set_Parent
(Node
, Parent_Node
);
4870 procedure Fix_Parents
is
4871 new Traverse_Proc_With_Parent
(Fix_Parent
);
4881 function Restore_Node
(N
: Node_Id
) return Traverse_Result
is
4883 if Nkind
(N
) = N_Function_Call
4884 and then Nkind
(Original_Node
(N
)) = N_Selected_Component
4885 and then Is_Dispatching_Operation
(Entity
(Name
(N
)))
4887 Rewrite
(N
, Original_Node
(N
));
4888 Set_Original_Node
(N
, N
);
4890 -- Save the restored node in the Restored_Nodes_List to fix
4891 -- the parent fields of their subtrees in a separate tree
4894 Append_New_Elmt
(N
, Restored_Nodes_List
);
4900 procedure Restore_Nodes
is new Traverse_Proc
(Restore_Node
);
4902 -- Start of processing for Restore_Original_Selected_Component
4905 Restore_Nodes
(Expr
);
4907 -- After restoring the original node we must fix the decoration
4908 -- of the Parent attribute to ensure tree consistency; required
4909 -- because when the class-wide condition is inherited, calls to
4910 -- New_Copy_Tree will perform copies of this subtree, and formal
4911 -- occurrences with wrong Parent field cannot be mapped to the
4914 if Present
(Restored_Nodes_List
) then
4916 Elmt
: Elmt_Id
:= First_Elmt
(Restored_Nodes_List
);
4919 while Present
(Elmt
) loop
4920 Fix_Parents
(Node
(Elmt
));
4925 end Restore_Original_Selected_Component
;
4927 -- Start of processing for Preanalyze_Condition
4930 pragma Assert
(Present
(Expr
));
4931 pragma Assert
(Inside_Class_Condition_Preanalysis
= False);
4934 Install_Formals
(Subp
);
4935 Inside_Class_Condition_Preanalysis
:= True;
4937 Preanalyze_Spec_Expression
(Expr
, Standard_Boolean
);
4939 Inside_Class_Condition_Preanalysis
:= False;
4942 -- If this preanalyzed condition has occurrences of dispatching calls
4943 -- using the Object.Operation notation, during preanalysis such calls
4944 -- are rewritten as dispatching function calls; if at later stages
4945 -- this condition is inherited we must have restored the original
4946 -- selected-component node to ensure that the preanalysis of the
4947 -- inherited condition rewrites these dispatching calls in the
4948 -- correct context to avoid reporting spurious errors.
4950 Restore_Original_Selected_Component
;
4952 -- Traverse Expr and clear the Controlling_Argument of calls to
4953 -- nonabstract functions. Required since the preanalyzed condition
4954 -- is not yet installed on its definite context and will be cloned
4955 -- and extended in derivations with additional conditions.
4957 Remove_Controlling_Arguments
;
4959 -- Clear also attribute Unset_Reference; again because preanalysis
4960 -- occurs in a place unrelated to the actual code.
4962 Clear_Unset_References
;
4963 end Preanalyze_Condition
;
4965 ----------------------------------------
4966 -- Save_Global_References_In_Contract --
4967 ----------------------------------------
4969 procedure Save_Global_References_In_Contract
4973 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
4974 -- Save all global references in contract-related source pragmas found
4975 -- in the list, starting with pragma First_Prag.
4977 ------------------------------------
4978 -- Save_Global_References_In_List --
4979 ------------------------------------
4981 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
4982 Prag
: Node_Id
:= First_Prag
;
4985 while Present
(Prag
) loop
4986 if Is_Generic_Contract_Pragma
(Prag
) then
4987 Save_Global_References
(Prag
);
4990 Prag
:= Next_Pragma
(Prag
);
4992 end Save_Global_References_In_List
;
4996 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
4998 -- Start of processing for Save_Global_References_In_Contract
5001 -- The entity of the analyzed generic copy must be on the scope stack
5002 -- to ensure proper detection of global references.
5004 Push_Scope
(Gen_Id
);
5006 if Permits_Aspect_Specifications
(Templ
)
5007 and then Has_Aspects
(Templ
)
5009 Save_Global_References_In_Aspects
(Templ
);
5012 if Present
(Items
) then
5013 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
5014 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
5015 Save_Global_References_In_List
(Classifications
(Items
));
5019 end Save_Global_References_In_Contract
;
5021 -------------------------
5022 -- Set_Class_Condition --
5023 -------------------------
5025 procedure Set_Class_Condition
5026 (Kind
: Condition_Kind
;
5032 when Class_Postcondition
=>
5033 Set_Class_Postconditions
(Subp
, Cond
);
5035 when Class_Precondition
=>
5036 Set_Class_Preconditions
(Subp
, Cond
);
5038 when Ignored_Class_Postcondition
=>
5039 Set_Ignored_Class_Postconditions
(Subp
, Cond
);
5041 when Ignored_Class_Precondition
=>
5042 Set_Ignored_Class_Preconditions
(Subp
, Cond
);
5044 end Set_Class_Condition
;