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
);
593 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
594 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
595 -- Save the SPARK_Mode-related data to restore on exit
598 -- When a subprogram body declaration is illegal, its defining entity is
599 -- left unanalyzed. There is nothing left to do in this case because the
600 -- body lacks a contract, or even a proper Ekind.
602 if Ekind
(Body_Id
) = E_Void
then
605 -- Do not analyze a contract multiple times
607 elsif Present
(Items
) then
608 if Analyzed
(Items
) then
611 Set_Analyzed
(Items
);
614 -- When this is a subprogram body not coming from source, for example an
615 -- expression function, it does not cause freezing of previous contracts
616 -- (see Analyze_Subprogram_Body_Helper), in particular not of those on
617 -- its spec if it exists. In this case make sure they have been properly
618 -- analyzed before being expanded below, as we may be invoked during the
619 -- freezing of the subprogram in the middle of its enclosing declarative
620 -- part because the declarative part contains e.g. the declaration of a
621 -- variable initialized by means of a call to the subprogram.
623 elsif Nkind
(Body_Decl
) = N_Subprogram_Body
624 and then not Comes_From_Source
(Original_Node
(Body_Decl
))
625 and then Present
(Corresponding_Spec
(Body_Decl
))
626 and then Present
(Contract
(Corresponding_Spec
(Body_Decl
)))
628 Analyze_Entry_Or_Subprogram_Contract
(Corresponding_Spec
(Body_Decl
));
631 -- Due to the timing of contract analysis, delayed pragmas may be
632 -- subject to the wrong SPARK_Mode, usually that of the enclosing
633 -- context. To remedy this, restore the original SPARK_Mode of the
634 -- related subprogram body.
636 Set_SPARK_Mode
(Body_Id
);
638 -- Ensure that the contract cases or postconditions mention 'Result or
639 -- define a post-state.
641 Check_Result_And_Post_State
(Body_Id
);
643 -- A stand-alone nonvolatile function body cannot have an effectively
644 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
645 -- check is relevant only when SPARK_Mode is on, as it is not a standard
646 -- legality rule. The check is performed here because Volatile_Function
647 -- is processed after the analysis of the related subprogram body. The
648 -- check only applies to source subprograms and not to generated TSS
652 and then Ekind
(Body_Id
) in E_Function | E_Generic_Function
653 and then Comes_From_Source
(Spec_Id
)
654 and then not Is_Volatile_Function
(Body_Id
)
656 Check_Nonvolatile_Function_Profile
(Body_Id
);
659 -- Restore the SPARK_Mode of the enclosing context after all delayed
660 -- pragmas have been analyzed.
662 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
664 -- Capture all global references in a generic subprogram body now that
665 -- the contract has been analyzed.
667 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
668 Save_Global_References_In_Contract
669 (Templ
=> Original_Node
(Body_Decl
),
673 -- Deal with preconditions, [refined] postconditions, Always_Terminates,
674 -- Contract_Cases, Exceptional_Cases, Subprogram_Variant, invariants and
675 -- predicates associated with body and its spec. Do not expand the
676 -- contract of subprogram body stubs.
678 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
679 Expand_Subprogram_Contract
(Body_Id
);
681 end Analyze_Entry_Or_Subprogram_Body_Contract
;
683 ------------------------------------------
684 -- Analyze_Entry_Or_Subprogram_Contract --
685 ------------------------------------------
687 -- WARNING: This routine manages SPARK regions. Return statements must be
688 -- replaced by gotos which jump to the end of the routine and restore the
691 procedure Analyze_Entry_Or_Subprogram_Contract
692 (Subp_Id
: Entity_Id
;
693 Freeze_Id
: Entity_Id
:= Empty
)
695 Items
: constant Node_Id
:= Contract
(Subp_Id
);
696 Subp_Decl
: constant Node_Id
:=
697 (if Ekind
(Subp_Id
) = E_Subprogram_Type
698 then Associated_Node_For_Itype
(Subp_Id
)
699 else Unit_Declaration_Node
(Subp_Id
));
701 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
702 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
703 -- Save the SPARK_Mode-related data to restore on exit
705 Skip_Assert_Exprs
: constant Boolean :=
706 Is_Entry
(Subp_Id
) and then not GNATprove_Mode
;
708 Depends
: Node_Id
:= Empty
;
709 Global
: Node_Id
:= Empty
;
714 -- Do not analyze a contract multiple times
716 if Present
(Items
) then
717 if Analyzed
(Items
) then
720 Set_Analyzed
(Items
);
724 -- Due to the timing of contract analysis, delayed pragmas may be
725 -- subject to the wrong SPARK_Mode, usually that of the enclosing
726 -- context. To remedy this, restore the original SPARK_Mode of the
727 -- related subprogram body.
729 Set_SPARK_Mode
(Subp_Id
);
731 -- All subprograms carry a contract, but for some it is not significant
732 -- and should not be processed.
734 if not Has_Significant_Contract
(Subp_Id
) then
737 elsif Present
(Items
) then
739 -- Do not analyze the pre/postconditions of an entry declaration
740 -- unless annotating the original tree for GNATprove. The
741 -- real analysis occurs when the pre/postconditons are relocated to
742 -- the contract wrapper procedure (see Build_Contract_Wrapper).
744 if Skip_Assert_Exprs
then
747 -- Otherwise analyze the pre/postconditions.
748 -- If these come from an aspect specification, their expressions
749 -- might include references to types that are not frozen yet, in the
750 -- case where the body is a rewritten expression function that is a
751 -- completion, so freeze all types within before constructing the
756 Bod
: Node_Id
:= Empty
;
757 Freeze_Types
: Boolean := False;
760 if Present
(Freeze_Id
) then
761 Bod
:= Unit_Declaration_Node
(Freeze_Id
);
763 if Nkind
(Bod
) = N_Subprogram_Body
764 and then Was_Expression_Function
(Bod
)
765 and then Ekind
(Subp_Id
) = E_Function
766 and then Chars
(Subp_Id
) = Chars
(Freeze_Id
)
767 and then Subp_Id
/= Freeze_Id
769 Freeze_Types
:= True;
773 Prag
:= Pre_Post_Conditions
(Items
);
774 while Present
(Prag
) loop
776 and then Present
(Corresponding_Aspect
(Prag
))
780 Typ
=> Standard_Boolean
,
783 (First
(Pragma_Argument_Associations
(Prag
))),
787 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
788 Prag
:= Next_Pragma
(Prag
);
793 -- Analyze contract-cases, subprogram-variant and test-cases
795 Prag
:= Contract_Test_Cases
(Items
);
796 while Present
(Prag
) loop
797 Prag_Nam
:= Pragma_Name
(Prag
);
799 if Prag_Nam
= Name_Always_Terminates
then
800 Analyze_Always_Terminates_In_Decl_Part
(Prag
);
802 elsif Prag_Nam
= Name_Contract_Cases
then
804 -- Do not analyze the contract cases of an entry declaration
805 -- unless annotating the original tree for GNATprove.
806 -- The real analysis occurs when the contract cases are moved
807 -- to the contract wrapper procedure (Build_Contract_Wrapper).
809 if Skip_Assert_Exprs
then
812 -- Otherwise analyze the contract cases
815 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
818 elsif Prag_Nam
= Name_Exceptional_Cases
then
819 Analyze_Exceptional_Cases_In_Decl_Part
(Prag
);
821 elsif Prag_Nam
= Name_Subprogram_Variant
then
822 Analyze_Subprogram_Variant_In_Decl_Part
(Prag
);
825 pragma Assert
(Prag_Nam
= Name_Test_Case
);
826 Analyze_Test_Case_In_Decl_Part
(Prag
);
829 Prag
:= Next_Pragma
(Prag
);
832 -- Analyze classification pragmas
834 Prag
:= Classifications
(Items
);
835 while Present
(Prag
) loop
836 Prag_Nam
:= Pragma_Name
(Prag
);
838 if Prag_Nam
= Name_Depends
then
841 elsif Prag_Nam
= Name_Global
then
845 Prag
:= Next_Pragma
(Prag
);
848 -- Analyze Global first, as Depends may mention items classified in
849 -- the global categorization.
851 if Present
(Global
) then
852 Analyze_Global_In_Decl_Part
(Global
);
855 -- Depends must be analyzed after Global in order to see the modes of
858 if Present
(Depends
) then
859 Analyze_Depends_In_Decl_Part
(Depends
);
862 -- Ensure that the contract cases or postconditions mention 'Result
863 -- or define a post-state.
865 Check_Result_And_Post_State
(Subp_Id
);
868 -- A nonvolatile function cannot have an effectively volatile formal
869 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
870 -- only when SPARK_Mode is on, as it is not a standard legality rule.
871 -- The check is performed here because pragma Volatile_Function is
872 -- processed after the analysis of the related subprogram declaration.
875 and then Ekind
(Subp_Id
) in E_Function | E_Generic_Function
876 and then Comes_From_Source
(Subp_Id
)
877 and then not Is_Volatile_Function
(Subp_Id
)
879 Check_Nonvolatile_Function_Profile
(Subp_Id
);
882 -- Restore the SPARK_Mode of the enclosing context after all delayed
883 -- pragmas have been analyzed.
885 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
887 -- Capture all global references in a generic subprogram now that the
888 -- contract has been analyzed.
890 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
891 Save_Global_References_In_Contract
892 (Templ
=> Original_Node
(Subp_Decl
),
895 end Analyze_Entry_Or_Subprogram_Contract
;
897 ----------------------------------------------
898 -- Check_Type_Or_Object_External_Properties --
899 ----------------------------------------------
901 procedure Check_Type_Or_Object_External_Properties
902 (Type_Or_Obj_Id
: Entity_Id
)
904 Is_Type_Id
: constant Boolean := Is_Type
(Type_Or_Obj_Id
);
905 Decl_Kind
: constant String :=
906 (if Is_Type_Id
then "type" else "object");
910 AR_Val
: Boolean := False;
911 AW_Val
: Boolean := False;
912 ER_Val
: Boolean := False;
913 EW_Val
: Boolean := False;
915 Seen
: Boolean := False;
919 -- Start of processing for Check_Type_Or_Object_External_Properties
922 -- Analyze all external properties
925 Obj_Typ
:= Type_Or_Obj_Id
;
927 -- If the parent type of a derived type is volatile
928 -- then the derived type inherits volatility-related flags.
930 if Is_Derived_Type
(Type_Or_Obj_Id
) then
932 Parent_Type
: constant Entity_Id
:=
933 Etype
(Base_Type
(Type_Or_Obj_Id
));
935 if Is_Effectively_Volatile
(Parent_Type
) then
936 AR_Val
:= Async_Readers_Enabled
(Parent_Type
);
937 AW_Val
:= Async_Writers_Enabled
(Parent_Type
);
938 ER_Val
:= Effective_Reads_Enabled
(Parent_Type
);
939 EW_Val
:= Effective_Writes_Enabled
(Parent_Type
);
944 Obj_Typ
:= Etype
(Type_Or_Obj_Id
);
947 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Readers
);
949 if Present
(Prag
) then
951 Saved_AR_Val
: constant Boolean := AR_Val
;
953 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
955 if Saved_AR_Val
and not AR_Val
then
957 ("illegal non-confirming Async_Readers specification",
963 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Writers
);
965 if Present
(Prag
) then
967 Saved_AW_Val
: constant Boolean := AW_Val
;
969 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
971 if Saved_AW_Val
and not AW_Val
then
973 ("illegal non-confirming Async_Writers specification",
979 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Reads
);
981 if Present
(Prag
) then
983 Saved_ER_Val
: constant Boolean := ER_Val
;
985 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
987 if Saved_ER_Val
and not ER_Val
then
989 ("illegal non-confirming Effective_Reads specification",
995 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Writes
);
997 if Present
(Prag
) then
999 Saved_EW_Val
: constant Boolean := EW_Val
;
1001 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
1003 if Saved_EW_Val
and not EW_Val
then
1005 ("illegal non-confirming Effective_Writes specification",
1011 -- Verify the mutual interaction of the various external properties.
1012 -- For types and variables for which No_Caching is enabled, it has been
1013 -- checked already that only False values for other external properties
1017 and then not No_Caching_Enabled
(Type_Or_Obj_Id
)
1019 Check_External_Properties
1020 (Type_Or_Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
1023 -- Analyze the non-external volatility property No_Caching
1025 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_No_Caching
);
1027 if Present
(Prag
) then
1028 Analyze_External_Property_In_Decl_Part
(Prag
, NC_Val
);
1031 -- The following checks are relevant only when SPARK_Mode is on, as
1032 -- they are not standard Ada legality rules. Internally generated
1033 -- temporaries are ignored, as well as return objects.
1036 and then Comes_From_Source
(Type_Or_Obj_Id
)
1037 and then not Is_Return_Object
(Type_Or_Obj_Id
)
1039 if Is_Effectively_Volatile
(Type_Or_Obj_Id
) then
1041 -- The declaration of an effectively volatile object or type must
1042 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
1044 if not Is_Library_Level_Entity
(Type_Or_Obj_Id
) then
1045 Error_Msg_Code
:= GEC_Volatile_At_Library_Level
;
1047 ("effectively volatile "
1049 & " & must be declared at library level '[[]']",
1052 -- An object of a discriminated type cannot be effectively
1053 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
1055 elsif Has_Discriminants
(Obj_Typ
)
1056 and then not Is_Protected_Type
(Obj_Typ
)
1059 ("discriminated " & Decl_Kind
& " & cannot be volatile",
1063 -- An object decl shall be compatible with respect to volatility
1064 -- with its type (SPARK RM 7.1.3(2)).
1066 if not Is_Type_Id
then
1067 if Is_Effectively_Volatile
(Obj_Typ
) then
1068 Check_Volatility_Compatibility
1069 (Type_Or_Obj_Id
, Obj_Typ
,
1070 "volatile object", "its type",
1071 Srcpos_Bearer
=> Type_Or_Obj_Id
);
1074 -- A component of a composite type (in this case, the composite
1075 -- type is an array type) shall be compatible with respect to
1076 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1078 elsif Is_Array_Type
(Obj_Typ
) then
1079 Check_Volatility_Compatibility
1080 (Component_Type
(Obj_Typ
), Obj_Typ
,
1081 "component type", "its enclosing array type",
1082 Srcpos_Bearer
=> Obj_Typ
);
1084 -- A component of a composite type (in this case, the composite
1085 -- type is a record type) shall be compatible with respect to
1086 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1088 elsif Is_Record_Type
(Obj_Typ
) then
1090 Comp
: Entity_Id
:= First_Component
(Obj_Typ
);
1092 while Present
(Comp
) loop
1093 Check_Volatility_Compatibility
1094 (Etype
(Comp
), Obj_Typ
,
1095 "record component " & Get_Name_String
(Chars
(Comp
)),
1096 "its enclosing record type",
1097 Srcpos_Bearer
=> Comp
);
1098 Next_Component
(Comp
);
1103 -- The type or object is not effectively volatile
1106 -- A non-effectively volatile type cannot have effectively
1107 -- volatile components (SPARK RM 7.1.3(6)).
1110 and then not Is_Effectively_Volatile
(Type_Or_Obj_Id
)
1111 and then Has_Effectively_Volatile_Component
(Type_Or_Obj_Id
)
1114 ("non-volatile type & cannot have effectively volatile"
1120 end Check_Type_Or_Object_External_Properties
;
1122 -----------------------------
1123 -- Analyze_Object_Contract --
1124 -----------------------------
1126 -- WARNING: This routine manages SPARK regions. Return statements must be
1127 -- replaced by gotos which jump to the end of the routine and restore the
1130 procedure Analyze_Object_Contract
1131 (Obj_Id
: Entity_Id
;
1132 Freeze_Id
: Entity_Id
:= Empty
)
1134 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
1136 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1137 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1138 -- Save the SPARK_Mode-related data to restore on exit
1145 -- The loop parameter in an element iterator over a formal container
1146 -- is declared with an object declaration, but no contracts apply.
1148 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
1152 -- Do not analyze a contract multiple times
1154 Items
:= Contract
(Obj_Id
);
1156 if Present
(Items
) then
1157 if Analyzed
(Items
) then
1160 Set_Analyzed
(Items
);
1164 -- The anonymous object created for a single concurrent type inherits
1165 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
1166 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
1167 -- of the enclosing context. To remedy this, restore the original mode
1168 -- of the related anonymous object.
1170 if Is_Single_Concurrent_Object
(Obj_Id
)
1171 and then Present
(SPARK_Pragma
(Obj_Id
))
1173 Set_SPARK_Mode
(Obj_Id
);
1176 -- Checks related to external properties, same for constants and
1179 Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id
=> Obj_Id
);
1181 -- Constant-related checks
1183 if Ekind
(Obj_Id
) = E_Constant
then
1185 -- Analyze indicator Part_Of
1187 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1189 -- Check whether the lack of indicator Part_Of agrees with the
1190 -- placement of the constant with respect to the state space.
1193 Check_Missing_Part_Of
(Obj_Id
);
1196 -- Variable-related checks
1198 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
1200 -- The anonymous object created for a single task type carries
1201 -- pragmas Depends and Global of the type.
1203 if Is_Single_Task_Object
(Obj_Id
) then
1205 -- Analyze Global first, as Depends may mention items classified
1206 -- in the global categorization.
1208 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
1210 if Present
(Prag
) then
1211 Analyze_Global_In_Decl_Part
(Prag
);
1214 -- Depends must be analyzed after Global in order to see the modes
1215 -- of all global items.
1217 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
1219 if Present
(Prag
) then
1220 Analyze_Depends_In_Decl_Part
(Prag
);
1224 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1226 -- Analyze indicator Part_Of
1228 if Present
(Prag
) then
1229 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
1231 -- The variable is a constituent of a single protected/task type
1232 -- and behaves as a component of the type. Verify that references
1233 -- to the variable occur within the definition or body of the type
1236 if Present
(Encapsulating_State
(Obj_Id
))
1237 and then Is_Single_Concurrent_Object
1238 (Encapsulating_State
(Obj_Id
))
1239 and then Present
(Part_Of_References
(Obj_Id
))
1241 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
1242 while Present
(Ref_Elmt
) loop
1243 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
1244 Next_Elmt
(Ref_Elmt
);
1248 -- Otherwise check whether the lack of indicator Part_Of agrees with
1249 -- the placement of the variable with respect to the state space.
1252 Check_Missing_Part_Of
(Obj_Id
);
1258 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
1260 -- A Ghost object cannot be of a type that yields a synchronized
1261 -- object (SPARK RM 6.9(19)).
1263 if Yields_Synchronized_Object
(Obj_Typ
) then
1264 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
1266 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
1267 -- SPARK RM 6.9(19)).
1269 elsif SPARK_Mode
= On
and then Is_Effectively_Volatile
(Obj_Id
) then
1270 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
1272 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
1273 -- One exception to this is the object that represents the dispatch
1274 -- table of a Ghost tagged type, as the symbol needs to be exported.
1276 elsif Is_Exported
(Obj_Id
) then
1277 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
1279 elsif Is_Imported
(Obj_Id
) then
1280 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
1284 -- Restore the SPARK_Mode of the enclosing context after all delayed
1285 -- pragmas have been analyzed.
1287 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1288 end Analyze_Object_Contract
;
1290 -----------------------------------
1291 -- Analyze_Package_Body_Contract --
1292 -----------------------------------
1294 -- WARNING: This routine manages SPARK regions. Return statements must be
1295 -- replaced by gotos which jump to the end of the routine and restore the
1298 procedure Analyze_Package_Body_Contract
1299 (Body_Id
: Entity_Id
;
1300 Freeze_Id
: Entity_Id
:= Empty
)
1302 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1303 Items
: constant Node_Id
:= Contract
(Body_Id
);
1304 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
1306 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1307 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1308 -- Save the SPARK_Mode-related data to restore on exit
1310 Ref_State
: Node_Id
;
1313 -- Do not analyze a contract multiple times
1315 if Present
(Items
) then
1316 if Analyzed
(Items
) then
1319 Set_Analyzed
(Items
);
1323 -- Due to the timing of contract analysis, delayed pragmas may be
1324 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1325 -- context. To remedy this, restore the original SPARK_Mode of the
1326 -- related package body.
1328 Set_SPARK_Mode
(Body_Id
);
1330 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
1332 -- The analysis of pragma Refined_State detects whether the spec has
1333 -- abstract states available for refinement.
1335 if Present
(Ref_State
) then
1336 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
1339 -- Restore the SPARK_Mode of the enclosing context after all delayed
1340 -- pragmas have been analyzed.
1342 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1344 -- Capture all global references in a generic package body now that the
1345 -- contract has been analyzed.
1347 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1348 Save_Global_References_In_Contract
1349 (Templ
=> Original_Node
(Body_Decl
),
1352 end Analyze_Package_Body_Contract
;
1354 ------------------------------
1355 -- Analyze_Package_Contract --
1356 ------------------------------
1358 -- WARNING: This routine manages SPARK regions. Return statements must be
1359 -- replaced by gotos which jump to the end of the routine and restore the
1362 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1363 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1364 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1366 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1367 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1368 -- Save the SPARK_Mode-related data to restore on exit
1370 Init
: Node_Id
:= Empty
;
1371 Init_Cond
: Node_Id
:= Empty
;
1376 -- Do not analyze a contract multiple times
1378 if Present
(Items
) then
1379 if Analyzed
(Items
) then
1382 -- Do not analyze the contract of the internal package
1383 -- created to check conformance of an actual package.
1384 -- Such an internal package is removed from the tree after
1385 -- legality checks are completed, and it does not contain
1386 -- the declarations of all local entities of the generic.
1388 elsif Is_Internal
(Pack_Id
)
1389 and then Is_Generic_Instance
(Pack_Id
)
1394 Set_Analyzed
(Items
);
1398 -- Due to the timing of contract analysis, delayed pragmas may be
1399 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1400 -- context. To remedy this, restore the original SPARK_Mode of the
1403 Set_SPARK_Mode
(Pack_Id
);
1405 if Present
(Items
) then
1407 -- Locate and store pragmas Initial_Condition and Initializes, since
1408 -- their order of analysis matters.
1410 Prag
:= Classifications
(Items
);
1411 while Present
(Prag
) loop
1412 Prag_Nam
:= Pragma_Name
(Prag
);
1414 if Prag_Nam
= Name_Initial_Condition
then
1417 elsif Prag_Nam
= Name_Initializes
then
1421 Prag
:= Next_Pragma
(Prag
);
1424 -- Analyze the initialization-related pragmas. Initializes must come
1425 -- before Initial_Condition due to item dependencies.
1427 if Present
(Init
) then
1428 Analyze_Initializes_In_Decl_Part
(Init
);
1431 if Present
(Init_Cond
) then
1432 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1436 -- Restore the SPARK_Mode of the enclosing context after all delayed
1437 -- pragmas have been analyzed.
1439 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1441 -- Capture all global references in a generic package now that the
1442 -- contract has been analyzed.
1444 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1445 Save_Global_References_In_Contract
1446 (Templ
=> Original_Node
(Pack_Decl
),
1449 end Analyze_Package_Contract
;
1451 --------------------------------------------
1452 -- Analyze_Package_Instantiation_Contract --
1453 --------------------------------------------
1455 -- WARNING: This routine manages SPARK regions. Return statements must be
1456 -- replaced by gotos which jump to the end of the routine and restore the
1459 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
) is
1460 Inst_Spec
: constant Node_Id
:=
1461 Instance_Spec
(Unit_Declaration_Node
(Inst_Id
));
1463 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1464 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1465 -- Save the SPARK_Mode-related data to restore on exit
1467 Pack_Id
: Entity_Id
;
1471 -- Nothing to do when the package instantiation is erroneous or left
1472 -- partially decorated.
1474 if No
(Inst_Spec
) then
1478 Pack_Id
:= Defining_Entity
(Inst_Spec
);
1479 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1481 -- Due to the timing of contract analysis, delayed pragmas may be
1482 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1483 -- context. To remedy this, restore the original SPARK_Mode of the
1486 Set_SPARK_Mode
(Pack_Id
);
1488 -- Check whether the lack of indicator Part_Of agrees with the placement
1489 -- of the package instantiation with respect to the state space. Nested
1490 -- package instantiations do not need to be checked because they inherit
1491 -- Part_Of indicator of the outermost package instantiation (see routine
1492 -- Propagate_Part_Of in Sem_Prag).
1497 elsif No
(Prag
) then
1498 Check_Missing_Part_Of
(Pack_Id
);
1501 -- Restore the SPARK_Mode of the enclosing context after all delayed
1502 -- pragmas have been analyzed.
1504 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1505 end Analyze_Package_Instantiation_Contract
;
1507 --------------------------------
1508 -- Analyze_Protected_Contract --
1509 --------------------------------
1511 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1512 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1515 -- Do not analyze a contract multiple times
1517 if Present
(Items
) then
1518 if Analyzed
(Items
) then
1521 Set_Analyzed
(Items
);
1524 end Analyze_Protected_Contract
;
1526 -------------------------------------------
1527 -- Analyze_Subprogram_Body_Stub_Contract --
1528 -------------------------------------------
1530 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1531 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1532 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1535 -- A subprogram body stub may act as its own spec or as the completion
1536 -- of a previous declaration. Depending on the context, the contract of
1537 -- the stub may contain two sets of pragmas.
1539 -- The stub is a completion, the applicable pragmas are:
1543 if Present
(Spec_Id
) then
1544 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1546 -- The stub acts as its own spec, the applicable pragmas are:
1547 -- Always_Terminates
1550 -- Exceptional_Cases
1554 -- Subprogram_Variant
1558 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1560 end Analyze_Subprogram_Body_Stub_Contract
;
1562 ---------------------------
1563 -- Analyze_Task_Contract --
1564 ---------------------------
1566 -- WARNING: This routine manages SPARK regions. Return statements must be
1567 -- replaced by gotos which jump to the end of the routine and restore the
1570 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1571 Items
: constant Node_Id
:= Contract
(Task_Id
);
1573 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1574 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1575 -- Save the SPARK_Mode-related data to restore on exit
1580 -- Do not analyze a contract multiple times
1582 if Present
(Items
) then
1583 if Analyzed
(Items
) then
1586 Set_Analyzed
(Items
);
1590 -- Due to the timing of contract analysis, delayed pragmas may be
1591 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1592 -- context. To remedy this, restore the original SPARK_Mode of the
1593 -- related task unit.
1595 Set_SPARK_Mode
(Task_Id
);
1597 -- Analyze Global first, as Depends may mention items classified in the
1598 -- global categorization.
1600 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1602 if Present
(Prag
) then
1603 Analyze_Global_In_Decl_Part
(Prag
);
1606 -- Depends must be analyzed after Global in order to see the modes of
1607 -- all global items.
1609 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1611 if Present
(Prag
) then
1612 Analyze_Depends_In_Decl_Part
(Prag
);
1615 -- Restore the SPARK_Mode of the enclosing context after all delayed
1616 -- pragmas have been analyzed.
1618 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1619 end Analyze_Task_Contract
;
1621 ---------------------------
1622 -- Analyze_Type_Contract --
1623 ---------------------------
1625 procedure Analyze_Type_Contract
(Type_Id
: Entity_Id
) is
1627 Check_Type_Or_Object_External_Properties
1628 (Type_Or_Obj_Id
=> Type_Id
);
1630 -- Analyze Pre/Post on access-to-subprogram type
1632 if Ekind
(Type_Id
) in Access_Subprogram_Kind
then
1633 Analyze_Entry_Or_Subprogram_Contract
1634 (Directly_Designated_Type
(Type_Id
));
1636 end Analyze_Type_Contract
;
1638 ---------------------------------------
1639 -- Build_Subprogram_Contract_Wrapper --
1640 ---------------------------------------
1642 procedure Build_Subprogram_Contract_Wrapper
1643 (Body_Id
: Entity_Id
;
1648 Body_Decl
: constant Entity_Id
:= Unit_Declaration_Node
(Body_Id
);
1649 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
1650 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1651 Subp_Id
: Entity_Id
;
1652 Ret_Type
: Entity_Id
;
1654 Wrapper_Id
: Entity_Id
;
1655 Wrapper_Body
: Node_Id
;
1656 Wrapper_Spec
: Node_Id
;
1659 -- When there are no postcondition statements we do not need to
1660 -- generate a wrapper.
1666 -- Obtain the related subprogram id from the body id.
1668 if Present
(Spec_Id
) then
1673 Ret_Type
:= Etype
(Subp_Id
);
1675 -- Generate the contracts wrapper by moving the original declarations
1676 -- and statements within a local subprogram, calling it and possibly
1677 -- preserving the result for the purpose of evaluating postconditions,
1678 -- contracts, type invariants, etc.
1680 -- In the case of a function, generate:
1682 -- function Original_Func (X : in out Integer) return Typ is
1683 -- <prologue renamings>
1686 -- function _Wrapped_Statements return Typ is
1687 -- <original declarations>
1689 -- <original statements>
1694 -- Result_Obj : constant Typ := _Wrapped_Statements
1696 -- <postconditions statements>
1700 -- Or else, in the case of a procedure, generate:
1702 -- procedure Original_Proc (X : in out Integer) is
1703 -- <prologue renamings>
1706 -- procedure _Wrapped_Statements is
1707 -- <original declarations>
1709 -- <original statements>
1713 -- _Wrapped_Statements;
1714 -- <postconditions statements>
1717 -- Create Identifier
1719 Wrapper_Id
:= Make_Defining_Identifier
(Loc
, Name_uWrapped_Statements
);
1720 Set_Debug_Info_Needed
(Wrapper_Id
);
1721 Set_Wrapped_Statements
(Subp_Id
, Wrapper_Id
);
1723 Set_Has_Pragma_Inline
(Wrapper_Id
, Has_Pragma_Inline
(Subp_Id
));
1724 Set_Has_Pragma_Inline_Always
1725 (Wrapper_Id
, Has_Pragma_Inline_Always
(Subp_Id
));
1727 -- Create specification and declaration for the wrapper
1729 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1731 Make_Procedure_Specification
(Loc
,
1732 Defining_Unit_Name
=> Wrapper_Id
);
1735 Make_Function_Specification
(Loc
,
1736 Defining_Unit_Name
=> Wrapper_Id
,
1737 Result_Definition
=> New_Occurrence_Of
(Ret_Type
, Loc
));
1740 -- Create the wrapper body using Body_Id's statements and declarations
1743 Make_Subprogram_Body
(Loc
,
1744 Specification
=> Wrapper_Spec
,
1745 Declarations
=> Declarations
(Body_Decl
),
1746 Handled_Statement_Sequence
=>
1747 Relocate_Node
(Handled_Statement_Sequence
(Body_Decl
)));
1749 Append_To
(Decls
, Wrapper_Body
);
1750 Set_Declarations
(Body_Decl
, Decls
);
1751 Set_Handled_Statement_Sequence
(Body_Decl
,
1752 Make_Handled_Sequence_Of_Statements
(Loc
,
1753 End_Label
=> Make_Identifier
(Loc
, Chars
(Wrapper_Id
))));
1755 -- Prepend a call to the wrapper when the subprogram is a procedure
1757 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1759 Make_Procedure_Call_Statement
(Loc
,
1760 Name
=> New_Occurrence_Of
(Wrapper_Id
, Loc
)));
1762 (Handled_Statement_Sequence
(Body_Decl
), Stmts
);
1764 -- Generate the post-execution statements and the extended return
1765 -- when the subprogram being wrapped is a function.
1768 Set_Statements
(Handled_Statement_Sequence
(Body_Decl
), New_List
(
1769 Make_Extended_Return_Statement
(Loc
,
1770 Return_Object_Declarations
=> New_List
(
1771 Make_Object_Declaration
(Loc
,
1772 Defining_Identifier
=> Result
,
1773 Constant_Present
=> True,
1774 Object_Definition
=>
1775 New_Occurrence_Of
(Ret_Type
, Loc
),
1777 Make_Function_Call
(Loc
,
1779 New_Occurrence_Of
(Wrapper_Id
, Loc
)))),
1780 Handled_Statement_Sequence
=>
1781 Make_Handled_Sequence_Of_Statements
(Loc
,
1782 Statements
=> Stmts
))));
1784 end Build_Subprogram_Contract_Wrapper
;
1786 ----------------------------------
1787 -- Build_Entry_Contract_Wrapper --
1788 ----------------------------------
1790 procedure Build_Entry_Contract_Wrapper
(E
: Entity_Id
; Decl
: Node_Id
) is
1791 Conc_Typ
: constant Entity_Id
:= Scope
(E
);
1792 Loc
: constant Source_Ptr
:= Sloc
(E
);
1794 procedure Add_Discriminant_Renamings
1795 (Obj_Id
: Entity_Id
;
1797 -- Add renaming declarations for all discriminants of concurrent type
1798 -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
1799 -- represents the concurrent object.
1801 procedure Add_Matching_Formals
1803 Actuals
: in out List_Id
);
1804 -- Add formal parameters that match those of entry E to list Formals.
1805 -- The routine also adds matching actuals for the new formals to list
1808 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
);
1809 -- Relocate pragma Prag to list To. The routine creates a new list if
1810 -- To does not exist.
1812 --------------------------------
1813 -- Add_Discriminant_Renamings --
1814 --------------------------------
1816 procedure Add_Discriminant_Renamings
1817 (Obj_Id
: Entity_Id
;
1821 Renaming_Decl
: Node_Id
;
1824 -- Inspect the discriminants of the concurrent type and generate a
1825 -- renaming for each one.
1827 if Has_Discriminants
(Conc_Typ
) then
1828 Discr
:= First_Discriminant
(Conc_Typ
);
1829 while Present
(Discr
) loop
1831 Make_Object_Renaming_Declaration
(Loc
,
1832 Defining_Identifier
=>
1833 Make_Defining_Identifier
(Loc
, Chars
(Discr
)),
1835 New_Occurrence_Of
(Etype
(Discr
), Loc
),
1837 Make_Selected_Component
(Loc
,
1838 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
1840 Make_Identifier
(Loc
, Chars
(Discr
))));
1842 Prepend_To
(Decls
, Renaming_Decl
);
1844 Next_Discriminant
(Discr
);
1847 end Add_Discriminant_Renamings
;
1849 --------------------------
1850 -- Add_Matching_Formals --
1851 --------------------------
1853 procedure Add_Matching_Formals
1855 Actuals
: in out List_Id
)
1858 New_Formal
: Entity_Id
;
1861 -- Inspect the formal parameters of the entry and generate a new
1862 -- matching formal with the same name for the wrapper. A reference
1863 -- to the new formal becomes an actual in the entry call.
1865 Formal
:= First_Formal
(E
);
1866 while Present
(Formal
) loop
1867 New_Formal
:= Make_Defining_Identifier
(Loc
, Chars
(Formal
));
1869 Make_Parameter_Specification
(Loc
,
1870 Defining_Identifier
=> New_Formal
,
1871 In_Present
=> In_Present
(Parent
(Formal
)),
1872 Out_Present
=> Out_Present
(Parent
(Formal
)),
1874 New_Occurrence_Of
(Etype
(Formal
), Loc
)));
1876 if No
(Actuals
) then
1877 Actuals
:= New_List
;
1880 Append_To
(Actuals
, New_Occurrence_Of
(New_Formal
, Loc
));
1881 Next_Formal
(Formal
);
1883 end Add_Matching_Formals
;
1885 ---------------------
1886 -- Transfer_Pragma --
1887 ---------------------
1889 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
) is
1897 New_Prag
:= Relocate_Node
(Prag
);
1899 Set_Analyzed
(New_Prag
, False);
1900 Append
(New_Prag
, To
);
1901 end Transfer_Pragma
;
1905 Items
: constant Node_Id
:= Contract
(E
);
1906 Actuals
: List_Id
:= No_List
;
1909 Decls
: List_Id
:= No_List
;
1911 Has_Pragma
: Boolean := False;
1912 Index_Id
: Entity_Id
;
1915 Wrapper_Id
: Entity_Id
;
1917 -- Start of processing for Build_Entry_Contract_Wrapper
1920 -- This routine generates a specialized wrapper for a protected or task
1921 -- entry [family] which implements precondition/postcondition semantics.
1922 -- Preconditions and case guards of contract cases are checked before
1923 -- the protected action or rendezvous takes place.
1925 -- procedure Wrapper
1926 -- (Obj_Id : Conc_Typ; -- concurrent object
1927 -- [Index : Index_Typ;] -- index of entry family
1928 -- [Formal_1 : ...; -- parameters of original entry
1931 -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
1932 -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
1934 -- <contracts pragmas>
1935 -- <case guard checks>
1938 -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
1941 -- Create the wrapper only when the entry has at least one executable
1942 -- contract item such as contract cases, precondition or postcondition.
1944 if Present
(Items
) then
1946 -- Inspect the list of pre/postconditions and transfer all available
1947 -- pragmas to the declarative list of the wrapper.
1949 Prag
:= Pre_Post_Conditions
(Items
);
1950 while Present
(Prag
) loop
1951 if Pragma_Name_Unmapped
(Prag
) in Name_Postcondition
1953 and then Is_Checked
(Prag
)
1956 Transfer_Pragma
(Prag
, To
=> Decls
);
1959 Prag
:= Next_Pragma
(Prag
);
1962 -- Inspect the list of test/contract cases and transfer only contract
1963 -- cases pragmas to the declarative part of the wrapper.
1965 Prag
:= Contract_Test_Cases
(Items
);
1966 while Present
(Prag
) loop
1967 if Pragma_Name
(Prag
) = Name_Contract_Cases
1968 and then Is_Checked
(Prag
)
1971 Transfer_Pragma
(Prag
, To
=> Decls
);
1974 Prag
:= Next_Pragma
(Prag
);
1978 -- The entry lacks executable contract items and a wrapper is not needed
1980 if not Has_Pragma
then
1984 -- Create the profile of the wrapper. The first formal parameter is the
1985 -- concurrent object.
1988 Make_Defining_Identifier
(Loc
,
1989 Chars
=> New_External_Name
(Chars
(Conc_Typ
), 'A'));
1991 Formals
:= New_List
(
1992 Make_Parameter_Specification
(Loc
,
1993 Defining_Identifier
=> Obj_Id
,
1994 Out_Present
=> True,
1996 Parameter_Type
=> New_Occurrence_Of
(Conc_Typ
, Loc
)));
1998 -- Construct the call to the original entry. The call will be gradually
1999 -- augmented with an optional entry index and extra parameters.
2002 Make_Selected_Component
(Loc
,
2003 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
2004 Selector_Name
=> New_Occurrence_Of
(E
, Loc
));
2006 -- When creating a wrapper for an entry family, the second formal is the
2009 if Ekind
(E
) = E_Entry_Family
then
2010 Index_Id
:= Make_Defining_Identifier
(Loc
, Name_I
);
2013 Make_Parameter_Specification
(Loc
,
2014 Defining_Identifier
=> Index_Id
,
2016 New_Occurrence_Of
(Entry_Index_Type
(E
), Loc
)));
2018 -- The call to the original entry becomes an indexed component to
2019 -- accommodate the entry index.
2022 Make_Indexed_Component
(Loc
,
2024 Expressions
=> New_List
(New_Occurrence_Of
(Index_Id
, Loc
)));
2027 -- Add formal parameters to match those of the entry and build actuals
2028 -- for the entry call.
2030 Add_Matching_Formals
(Formals
, Actuals
);
2033 Make_Procedure_Call_Statement
(Loc
,
2035 Parameter_Associations
=> Actuals
);
2037 -- Add renaming declarations for the discriminants of the enclosing type
2038 -- as the various contract items may reference them.
2040 Add_Discriminant_Renamings
(Obj_Id
, Decls
);
2043 Make_Defining_Identifier
(Loc
, New_External_Name
(Chars
(E
), 'E'));
2044 Set_Contract_Wrapper
(E
, Wrapper_Id
);
2045 Set_Is_Entry_Wrapper
(Wrapper_Id
);
2047 -- The wrapper body is analyzed when the enclosing type is frozen
2049 Append_Freeze_Action
(Defining_Entity
(Decl
),
2050 Make_Subprogram_Body
(Loc
,
2052 Make_Procedure_Specification
(Loc
,
2053 Defining_Unit_Name
=> Wrapper_Id
,
2054 Parameter_Specifications
=> Formals
),
2055 Declarations
=> Decls
,
2056 Handled_Statement_Sequence
=>
2057 Make_Handled_Sequence_Of_Statements
(Loc
,
2058 Statements
=> New_List
(Call
))));
2059 end Build_Entry_Contract_Wrapper
;
2061 ---------------------------
2062 -- Check_Class_Condition --
2063 ---------------------------
2065 procedure Check_Class_Condition
2068 Par_Subp
: Entity_Id
;
2069 Is_Precondition
: Boolean)
2071 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
2072 -- Check reference to formal of inherited operation or to primitive
2073 -- operation of root type.
2079 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
2084 if Nkind
(N
) = N_Identifier
2085 and then Present
(Entity
(N
))
2087 (Is_Formal
(Entity
(N
)) or else Is_Subprogram
(Entity
(N
)))
2089 (Nkind
(Parent
(N
)) /= N_Attribute_Reference
2090 or else Attribute_Name
(Parent
(N
)) /= Name_Class
)
2092 -- These checks do not apply to dispatching calls within the
2093 -- condition, but only to calls whose static tag is that of
2096 if Is_Subprogram
(Entity
(N
))
2097 and then Nkind
(Parent
(N
)) = N_Function_Call
2098 and then Present
(Controlling_Argument
(Parent
(N
)))
2103 -- Determine whether entity has a renaming
2105 Orig_E
:= Entity
(N
);
2106 New_E
:= Get_Mapped_Entity
(Orig_E
);
2108 if Present
(New_E
) then
2110 -- AI12-0166: A precondition for a protected operation
2111 -- cannot include an internal call to a protected function
2112 -- of the type. In the case of an inherited condition for an
2113 -- overriding operation, both the operation and the function
2114 -- are given by primitive wrappers.
2117 and then Ekind
(New_E
) = E_Function
2118 and then Is_Primitive_Wrapper
(New_E
)
2119 and then Is_Primitive_Wrapper
(Subp
)
2120 and then Scope
(Subp
) = Scope
(New_E
)
2122 Error_Msg_Node_2
:= Wrapped_Entity
(Subp
);
2124 ("internal call to& cannot appear in inherited "
2125 & "precondition of protected operation&",
2126 Subp
, Wrapped_Entity
(New_E
));
2130 -- Check that there are no calls left to abstract operations if
2131 -- the current subprogram is not abstract.
2134 and then Nkind
(Parent
(N
)) = N_Function_Call
2135 and then N
= Name
(Parent
(N
))
2137 if not Is_Abstract_Subprogram
(Subp
)
2138 and then Is_Abstract_Subprogram
(New_E
)
2140 Error_Msg_Sloc
:= Sloc
(Current_Scope
);
2141 Error_Msg_Node_2
:= Subp
;
2143 if Comes_From_Source
(Subp
) then
2145 ("cannot call abstract subprogram & in inherited "
2146 & "condition for&#", Subp
, New_E
);
2149 ("cannot call abstract subprogram & in inherited "
2150 & "condition for inherited&#", Subp
, New_E
);
2153 -- In SPARK mode, report error on inherited condition for an
2154 -- inherited operation if it contains a call to an overriding
2155 -- operation, because this implies that the pre/postconditions
2156 -- of the inherited operation have changed silently.
2158 elsif SPARK_Mode
= On
2159 and then Warn_On_Suspicious_Contract
2160 and then Present
(Alias
(Subp
))
2161 and then Present
(New_E
)
2162 and then Comes_From_Source
(New_E
)
2165 ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
2167 Error_Msg_Sloc
:= Sloc
(New_E
);
2168 Error_Msg_Node_2
:= Subp
;
2170 ("\overriding of&# forces overriding of&",
2171 Parent
(Subp
), New_E
);
2179 procedure Check_Condition_Entities
is
2180 new Traverse_Proc
(Check_Entity
);
2182 -- Start of processing for Check_Class_Condition
2185 -- No check required if the subprograms match
2187 if Par_Subp
= Subp
then
2191 Update_Primitives_Mapping
(Par_Subp
, Subp
);
2192 Map_Formals
(Par_Subp
, Subp
);
2193 Check_Condition_Entities
(Cond
);
2194 end Check_Class_Condition
;
2196 -----------------------------
2197 -- Create_Generic_Contract --
2198 -----------------------------
2200 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
2201 Templ
: constant Node_Id
:= Original_Node
(Unit
);
2202 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
2204 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
2205 -- Add a single contract-related source pragma Prag to the contract of
2206 -- generic template Templ_Id.
2208 ---------------------------------
2209 -- Add_Generic_Contract_Pragma --
2210 ---------------------------------
2212 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
2213 Prag_Templ
: Node_Id
;
2216 -- Mark the pragma to prevent the premature capture of global
2217 -- references when capturing global references of the context
2218 -- (see Save_References_In_Pragma).
2220 Set_Is_Generic_Contract_Pragma
(Prag
);
2222 -- Pragmas that apply to a generic subprogram declaration are not
2223 -- part of the semantic structure of the generic template:
2226 -- procedure Example (Formal : Integer);
2227 -- pragma Precondition (Formal > 0);
2229 -- Create a generic template for such pragmas and link the template
2230 -- of the pragma with the generic template.
2232 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2234 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
2235 Prag_Templ
:= Original_Node
(Prag
);
2237 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
2238 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
2240 -- Otherwise link the pragma with the generic template
2243 Add_Contract_Item
(Prag
, Templ_Id
);
2247 -- We do not stop the compilation at this point in the case of an
2248 -- invalid pragma because it will be properly diagnosed afterward.
2250 when Contract_Error
=> null;
2251 end Add_Generic_Contract_Pragma
;
2255 Context
: constant Node_Id
:= Parent
(Unit
);
2256 Decl
: Node_Id
:= Empty
;
2258 -- Start of processing for Create_Generic_Contract
2261 -- A generic package declaration carries contract-related source pragmas
2262 -- in its visible declarations.
2264 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
2265 Mutate_Ekind
(Templ_Id
, E_Generic_Package
);
2267 if Present
(Visible_Declarations
(Specification
(Templ
))) then
2268 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
2271 -- A generic package body carries contract-related source pragmas in its
2274 elsif Nkind
(Templ
) = N_Package_Body
then
2275 Mutate_Ekind
(Templ_Id
, E_Package_Body
);
2277 if Present
(Declarations
(Templ
)) then
2278 Decl
:= First
(Declarations
(Templ
));
2281 -- Generic subprogram declaration
2283 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2284 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
2285 Mutate_Ekind
(Templ_Id
, E_Generic_Function
);
2287 Mutate_Ekind
(Templ_Id
, E_Generic_Procedure
);
2290 -- When the generic subprogram acts as a compilation unit, inspect
2291 -- the Pragmas_After list for contract-related source pragmas.
2293 if Nkind
(Context
) = N_Compilation_Unit
then
2294 if Present
(Aux_Decls_Node
(Context
))
2295 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
2297 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
2300 -- Otherwise inspect the successive declarations for contract-related
2304 Decl
:= Next
(Unit
);
2307 -- A generic subprogram body carries contract-related source pragmas in
2308 -- its declarations.
2310 elsif Nkind
(Templ
) = N_Subprogram_Body
then
2311 Mutate_Ekind
(Templ_Id
, E_Subprogram_Body
);
2313 if Present
(Declarations
(Templ
)) then
2314 Decl
:= First
(Declarations
(Templ
));
2318 -- Inspect the relevant declarations looking for contract-related source
2319 -- pragmas and add them to the contract of the generic unit.
2321 while Present
(Decl
) loop
2322 if Comes_From_Source
(Decl
) then
2323 if Nkind
(Decl
) = N_Pragma
then
2325 -- The source pragma is a contract annotation
2327 if Is_Contract_Annotation
(Decl
) then
2328 Add_Generic_Contract_Pragma
(Decl
);
2331 -- The region where a contract-related source pragma may appear
2332 -- ends with the first source non-pragma declaration or statement.
2341 end Create_Generic_Contract
;
2343 --------------------------------
2344 -- Expand_Subprogram_Contract --
2345 --------------------------------
2347 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
2348 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
2349 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
2351 procedure Add_Invariant_And_Predicate_Checks
2352 (Subp_Id
: Entity_Id
;
2353 Stmts
: in out List_Id
;
2354 Result
: out Node_Id
);
2355 -- Process the result of function Subp_Id (if applicable) and all its
2356 -- formals. Add invariant and predicate checks where applicable. The
2357 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
2358 -- function, Result contains the entity of parameter _Result, to be
2359 -- used in the creation of procedure _Postconditions.
2361 procedure Add_Stable_Property_Contracts
2362 (Subp_Id
: Entity_Id
; Class_Present
: Boolean);
2363 -- Augment postcondition contracts to reflect Stable_Property aspect
2364 -- (if Class_Present = False) or Stable_Property'Class aspect (if
2365 -- Class_Present = True).
2367 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
2368 -- Append a node to a list. If there is no list, create a new one. When
2369 -- the item denotes a pragma, it is added to the list only when it is
2372 procedure Process_Contract_Cases
2373 (Stmts
: in out List_Id
;
2375 -- Process pragma Contract_Cases. This routine prepends items to the
2376 -- body declarations and appends items to list Stmts.
2378 procedure Process_Postconditions
(Stmts
: in out List_Id
);
2379 -- Collect all [inherited] spec and body postconditions and accumulate
2380 -- their pragma Check equivalents in list Stmts.
2382 procedure Process_Preconditions
(Decls
: in out List_Id
);
2383 -- Collect all [inherited] spec and body preconditions and prepend their
2384 -- pragma Check equivalents to the declarations of the body.
2386 ----------------------------------------
2387 -- Add_Invariant_And_Predicate_Checks --
2388 ----------------------------------------
2390 procedure Add_Invariant_And_Predicate_Checks
2391 (Subp_Id
: Entity_Id
;
2392 Stmts
: in out List_Id
;
2393 Result
: out Node_Id
)
2395 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
2396 -- Id denotes the return value of a function or a formal parameter.
2397 -- Add an invariant check if the type of Id is access to a type with
2398 -- invariants. The routine appends the generated code to Stmts.
2400 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
2401 -- Determine whether type Typ can benefit from invariant checks. To
2402 -- qualify, the type must have a non-null invariant procedure and
2403 -- subprogram Subp_Id must appear visible from the point of view of
2406 ---------------------------------
2407 -- Add_Invariant_Access_Checks --
2408 ---------------------------------
2410 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
2411 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2418 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
2419 Typ
:= Designated_Type
(Typ
);
2421 if Invariant_Checks_OK
(Typ
) then
2423 Make_Explicit_Dereference
(Loc
,
2424 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
2425 Set_Etype
(Ref
, Typ
);
2428 -- if <Id> /= null then
2429 -- <invariant_call (<Ref>)>
2434 Make_If_Statement
(Loc
,
2437 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
2438 Right_Opnd
=> Make_Null
(Loc
)),
2439 Then_Statements
=> New_List
(
2440 Make_Invariant_Call
(Ref
))),
2444 end Add_Invariant_Access_Checks
;
2446 -------------------------
2447 -- Invariant_Checks_OK --
2448 -------------------------
2450 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
2451 function Has_Public_Visibility_Of_Subprogram
return Boolean;
2452 -- Determine whether type Typ has public visibility of subprogram
2455 -----------------------------------------
2456 -- Has_Public_Visibility_Of_Subprogram --
2457 -----------------------------------------
2459 function Has_Public_Visibility_Of_Subprogram
return Boolean is
2460 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2463 -- An Initialization procedure must be considered visible even
2464 -- though it is internally generated.
2466 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2469 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2472 -- Internally generated code is never publicly visible except
2473 -- for a subprogram that is the implementation of an expression
2474 -- function. In that case the visibility is determined by the
2477 elsif not Comes_From_Source
(Subp_Decl
)
2479 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2481 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2485 -- Determine whether the subprogram is declared in the visible
2486 -- declarations of the package containing the type, or in the
2487 -- visible declaration of a child unit of that package.
2489 elsif Is_List_Member
(Subp_Decl
) then
2491 Decls
: constant List_Id
:=
2492 List_Containing
(Subp_Decl
);
2493 Subp_Scope
: constant Entity_Id
:=
2494 Scope
(Defining_Entity
(Subp_Decl
));
2495 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2499 Decls
= Visible_Declarations
2500 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2503 (Ekind
(Subp_Scope
) = E_Package
2504 and then Typ_Scope
/= Subp_Scope
2505 and then Is_Child_Unit
(Subp_Scope
)
2507 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2509 Decls
= Visible_Declarations
2511 (Unit_Declaration_Node
(Subp_Scope
))));
2514 -- Determine whether the subprogram is a child subprogram of
2515 -- of the package containing the type.
2519 (Nkind
(Parent
(Subp_Decl
)) = N_Compilation_Unit
);
2522 Subp_Scope
: constant Entity_Id
:=
2523 Scope
(Defining_Entity
(Subp_Decl
));
2524 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2528 Ekind
(Subp_Scope
) = E_Package
2530 (Typ_Scope
= Subp_Scope
2532 (Is_Child_Unit
(Subp_Scope
)
2533 and then Is_Ancestor_Package
2534 (Typ_Scope
, Subp_Scope
)));
2537 end Has_Public_Visibility_Of_Subprogram
;
2539 -- Start of processing for Invariant_Checks_OK
2543 Has_Invariants
(Typ
)
2544 and then Present
(Invariant_Procedure
(Typ
))
2545 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2546 and then Has_Public_Visibility_Of_Subprogram
;
2547 end Invariant_Checks_OK
;
2551 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2552 -- Source location of subprogram body contract
2557 -- Start of processing for Add_Invariant_And_Predicate_Checks
2562 -- Process the result of a function
2564 if Ekind
(Subp_Id
) = E_Function
then
2565 Typ
:= Etype
(Subp_Id
);
2567 -- Generate _Result which is used in procedure _Postconditions to
2568 -- verify the return value.
2570 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2571 Set_Etype
(Result
, Typ
);
2573 -- Add an invariant check when the return type has invariants and
2574 -- the related function is visible to the outside.
2576 if Invariant_Checks_OK
(Typ
) then
2579 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2583 -- Add an invariant check when the return type is an access to a
2584 -- type with invariants.
2586 Add_Invariant_Access_Checks
(Result
);
2589 -- Add invariant checks for all formals that qualify (see AI05-0289
2592 Formal
:= First_Formal
(Subp_Id
);
2593 while Present
(Formal
) loop
2594 Typ
:= Etype
(Formal
);
2596 if Ekind
(Formal
) /= E_In_Parameter
2597 or else Ekind
(Subp_Id
) = E_Procedure
2598 or else Is_Access_Type
(Typ
)
2600 if Invariant_Checks_OK
(Typ
) then
2603 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2607 Add_Invariant_Access_Checks
(Formal
);
2609 -- Note: we used to add predicate checks for OUT and IN OUT
2610 -- formals here, but that was misguided, since such checks are
2611 -- performed on the caller side, based on the predicate of the
2612 -- actual, rather than the predicate of the formal.
2616 Next_Formal
(Formal
);
2618 end Add_Invariant_And_Predicate_Checks
;
2620 -----------------------------------
2621 -- Add_Stable_Property_Contracts --
2622 -----------------------------------
2624 procedure Add_Stable_Property_Contracts
2625 (Subp_Id
: Entity_Id
; Class_Present
: Boolean)
2627 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
2629 procedure Insert_Stable_Property_Check
2630 (Formal
: Entity_Id
; Property_Function
: Entity_Id
);
2631 -- Build the pragma for one check and insert it in the tree.
2633 function Make_Stable_Property_Condition
2634 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
;
2635 -- Builds tree for "Func (Formal) = Func (Formal)'Old" expression.
2637 function Stable_Properties
2638 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2639 return Subprogram_List
;
2640 -- If no aspect specified, then returns length-zero result.
2641 -- Negated indicates that reserved word NOT was specified.
2643 ----------------------------------
2644 -- Insert_Stable_Property_Check --
2645 ----------------------------------
2647 procedure Insert_Stable_Property_Check
2648 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) is
2650 Args
: constant List_Id
:=
2652 (Make_Pragma_Argument_Association
2655 Make_Stable_Property_Condition
2657 Property_Function
=> Property_Function
)),
2658 Make_Pragma_Argument_Association
2664 "failed stable property check at "
2665 & Build_Location_String
(Loc
)
2667 & To_String
(Fully_Qualified_Name_String
2668 (Formal
, Append_NUL
=> False))
2669 & " and property function "
2670 & To_String
(Fully_Qualified_Name_String
2671 (Property_Function
, Append_NUL
=> False))
2674 Prag
: constant Node_Id
:=
2676 Pragma_Identifier
=>
2677 Make_Identifier
(Loc
, Name_Postcondition
),
2678 Pragma_Argument_Associations
=> Args
,
2679 Class_Present
=> Class_Present
);
2681 Subp_Decl
: Node_Id
:= Subp_Id
;
2683 -- Enclosing_Declaration may return, for example,
2684 -- a N_Procedure_Specification node. Cope with this.
2686 Subp_Decl
:= Enclosing_Declaration
(Subp_Decl
);
2687 exit when Is_Declaration
(Subp_Decl
);
2688 Subp_Decl
:= Parent
(Subp_Decl
);
2689 pragma Assert
(Present
(Subp_Decl
));
2692 Insert_After_And_Analyze
(Subp_Decl
, Prag
);
2693 end Insert_Stable_Property_Check
;
2695 ------------------------------------
2696 -- Make_Stable_Property_Condition --
2697 ------------------------------------
2699 function Make_Stable_Property_Condition
2700 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
2702 function Call_Property_Function
return Node_Id
is
2706 New_Occurrence_Of
(Property_Function
, Loc
),
2707 Parameter_Associations
=>
2708 New_List
(New_Occurrence_Of
(Formal
, Loc
))));
2712 Call_Property_Function
,
2713 Make_Attribute_Reference
2715 Prefix
=> Call_Property_Function
,
2716 Attribute_Name
=> Name_Old
));
2717 end Make_Stable_Property_Condition
;
2719 -----------------------
2720 -- Stable_Properties --
2721 -----------------------
2723 function Stable_Properties
2724 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2725 return Subprogram_List
2727 Aspect_Spec
: Node_Id
:=
2728 Find_Value_Of_Aspect
2729 (Aspect_Bearer
, Aspect_Stable_Properties
,
2730 Class_Present
=> Class_Present
);
2732 -- ??? For a derived type, we wish Find_Value_Of_Aspect
2733 -- somehow knew that this aspect is not inherited.
2734 -- But it doesn't, so we cope with that here.
2736 -- There are probably issues here with inheritance from
2737 -- interface types, where just looking for the one parent type
2738 -- isn't enough. But this is far from the only work needed for
2739 -- Stable_Properties'Class for interface types.
2741 if Is_Derived_Type
(Aspect_Bearer
) then
2743 Parent_Type
: constant Entity_Id
:=
2744 Etype
(Base_Type
(Aspect_Bearer
));
2747 Find_Value_Of_Aspect
2748 (Parent_Type
, Aspect_Stable_Properties
,
2749 Class_Present
=> Class_Present
)
2751 -- prevent inheritance
2752 Aspect_Spec
:= Empty
;
2757 if No
(Aspect_Spec
) then
2758 Negated
:= Aspect_Bearer
= Subp_Id
;
2759 -- This is a little bit subtle.
2760 -- We need to assign True in the Subp_Id case in order to
2761 -- distinguish between no aspect spec at all vs. an
2762 -- explicitly specified "with S_P => []" empty list.
2763 -- In both cases Stable_Properties will return a length-0
2764 -- array, but the two cases are not equivalent.
2765 -- Very roughly speaking the lack of an S_P aspect spec for
2766 -- a subprogram would be equivalent to something like
2767 -- "with S_P => [not]", where we apply the "not" modifier to
2768 -- an empty set of subprograms, if such a construct existed.
2769 -- We could just assign True here, but it seems untidy to
2770 -- return True in the case of an aspect spec for a type
2771 -- (since negation is only allowed for subp S_P aspects).
2773 return (1 .. 0 => <>);
2775 return Parse_Aspect_Stable_Properties
2776 (Aspect_Spec
, Negated
=> Negated
);
2778 end Stable_Properties
;
2780 Formal
: Entity_Id
:= First_Formal
(Subp_Id
);
2781 Type_Of_Formal
: Entity_Id
;
2783 Subp_Properties_Negated
: Boolean;
2784 Subp_Properties
: constant Subprogram_List
:=
2785 Stable_Properties
(Subp_Id
, Subp_Properties_Negated
);
2787 -- start of processing for Add_Stable_Property_Contracts
2790 if not (Is_Primitive
(Subp_Id
) and then Comes_From_Source
(Subp_Id
))
2795 while Present
(Formal
) loop
2796 Type_Of_Formal
:= Base_Type
(Etype
(Formal
));
2798 if not Subp_Properties_Negated
then
2800 for SPF_Id
of Subp_Properties
loop
2801 if Type_Of_Formal
= Base_Type
(Etype
(First_Formal
(SPF_Id
)))
2802 and then Scope
(Type_Of_Formal
) = Scope
(Subp_Id
)
2804 -- ??? Need to filter out checks for SPFs that are
2805 -- mentioned explicitly in the postcondition of
2808 Insert_Stable_Property_Check
2809 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2813 elsif Scope
(Type_Of_Formal
) = Scope
(Subp_Id
) then
2815 Ignored
: Boolean range False .. False;
2817 Typ_Property_Funcs
: constant Subprogram_List
:=
2818 Stable_Properties
(Type_Of_Formal
, Negated
=> Ignored
);
2820 function Excluded_By_Aspect_Spec_Of_Subp
2821 (SPF_Id
: Entity_Id
) return Boolean;
2822 -- Examine Subp_Properties to determine whether SPF should
2825 -------------------------------------
2826 -- Excluded_By_Aspect_Spec_Of_Subp --
2827 -------------------------------------
2829 function Excluded_By_Aspect_Spec_Of_Subp
2830 (SPF_Id
: Entity_Id
) return Boolean is
2832 pragma Assert
(Subp_Properties_Negated
);
2833 -- Look through renames for equality test here ???
2834 return (for some F
of Subp_Properties
=> F
= SPF_Id
);
2835 end Excluded_By_Aspect_Spec_Of_Subp
;
2837 -- Look through renames for equality test here ???
2838 Subp_Is_Stable_Property_Function
: constant Boolean :=
2839 (for some F
of Typ_Property_Funcs
=> F
= Subp_Id
);
2841 if not Subp_Is_Stable_Property_Function
then
2842 for SPF_Id
of Typ_Property_Funcs
loop
2843 if not Excluded_By_Aspect_Spec_Of_Subp
(SPF_Id
) then
2844 -- ??? Need to filter out checks for SPFs that are
2845 -- mentioned explicitly in the postcondition of
2847 Insert_Stable_Property_Check
2848 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2854 Next_Formal
(Formal
);
2856 end Add_Stable_Property_Contracts
;
2858 -------------------------
2859 -- Append_Enabled_Item --
2860 -------------------------
2862 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2864 -- Do not chain ignored or disabled pragmas
2866 if Nkind
(Item
) = N_Pragma
2867 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2871 -- Otherwise, add the item
2878 -- If the pragma is a conjunct in a composite postcondition, it
2879 -- has been processed in reverse order. In the postcondition body
2880 -- it must appear before the others.
2882 if Nkind
(Item
) = N_Pragma
2883 and then From_Aspect_Specification
(Item
)
2884 and then Split_PPC
(Item
)
2886 Prepend
(Item
, List
);
2888 Append
(Item
, List
);
2891 end Append_Enabled_Item
;
2893 ----------------------------
2894 -- Process_Contract_Cases --
2895 ----------------------------
2897 procedure Process_Contract_Cases
2898 (Stmts
: in out List_Id
;
2901 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2902 -- Process pragma Contract_Cases for subprogram Subp_Id
2904 --------------------------------
2905 -- Process_Contract_Cases_For --
2906 --------------------------------
2908 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2909 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2913 if Present
(Items
) then
2914 Prag
:= Contract_Test_Cases
(Items
);
2915 while Present
(Prag
) loop
2916 if Is_Checked
(Prag
) then
2917 if Pragma_Name
(Prag
) = Name_Always_Terminates
then
2918 Expand_Pragma_Always_Terminates
(Prag
);
2920 elsif Pragma_Name
(Prag
) = Name_Contract_Cases
then
2921 Expand_Pragma_Contract_Cases
2927 elsif Pragma_Name
(Prag
) = Name_Exceptional_Cases
then
2928 Expand_Pragma_Exceptional_Cases
(Prag
);
2930 elsif Pragma_Name
(Prag
) = Name_Subprogram_Variant
then
2931 Expand_Pragma_Subprogram_Variant
2934 Body_Decls
=> Decls
);
2938 Prag
:= Next_Pragma
(Prag
);
2941 end Process_Contract_Cases_For
;
2943 -- Start of processing for Process_Contract_Cases
2946 Process_Contract_Cases_For
(Body_Id
);
2948 if Present
(Spec_Id
) then
2949 Process_Contract_Cases_For
(Spec_Id
);
2951 end Process_Contract_Cases
;
2953 ----------------------------
2954 -- Process_Postconditions --
2955 ----------------------------
2957 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2958 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2959 -- Collect all [refined] postconditions of a specific kind denoted
2960 -- by Post_Nam that belong to the body, and generate pragma Check
2961 -- equivalents in list Stmts.
2963 procedure Process_Spec_Postconditions
;
2964 -- Collect all [inherited] postconditions of the spec, and generate
2965 -- pragma Check equivalents in list Stmts.
2967 ---------------------------------
2968 -- Process_Body_Postconditions --
2969 ---------------------------------
2971 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2972 Items
: constant Node_Id
:= Contract
(Body_Id
);
2973 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2978 -- Process the contract
2980 if Present
(Items
) then
2981 Prag
:= Pre_Post_Conditions
(Items
);
2982 while Present
(Prag
) loop
2983 if Pragma_Name
(Prag
) = Post_Nam
2984 and then Is_Checked
(Prag
)
2987 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2991 Prag
:= Next_Pragma
(Prag
);
2995 -- The subprogram body being processed is actually the proper body
2996 -- of a stub with a corresponding spec. The subprogram stub may
2997 -- carry a postcondition pragma, in which case it must be taken
2998 -- into account. The pragma appears after the stub.
3000 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
3001 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
3002 while Present
(Decl
) loop
3004 -- Note that non-matching pragmas are skipped
3006 if Nkind
(Decl
) = N_Pragma
then
3007 if Pragma_Name
(Decl
) = Post_Nam
3008 and then Is_Checked
(Decl
)
3011 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
3015 -- Skip internally generated code
3017 elsif not Comes_From_Source
(Decl
) then
3020 -- Postcondition pragmas are usually grouped together. There
3021 -- is no need to inspect the whole declarative list.
3030 end Process_Body_Postconditions
;
3032 ---------------------------------
3033 -- Process_Spec_Postconditions --
3034 ---------------------------------
3036 procedure Process_Spec_Postconditions
is
3037 Subps
: constant Subprogram_List
:=
3038 Inherited_Subprograms
(Spec_Id
);
3039 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
3041 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean;
3042 -- Return True if the contract of subprogram Subp_Id has been
3049 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean is
3051 for Index
in Seen
'Range loop
3052 if Seen
(Index
) = Subp_Id
then
3065 Subp_Id
: Entity_Id
;
3067 -- Start of processing for Process_Spec_Postconditions
3070 -- Process the contract
3072 Items
:= Contract
(Spec_Id
);
3074 if Present
(Items
) then
3075 Prag
:= Pre_Post_Conditions
(Items
);
3076 while Present
(Prag
) loop
3077 if Pragma_Name
(Prag
) = Name_Postcondition
3078 and then Is_Checked
(Prag
)
3081 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
3085 Prag
:= Next_Pragma
(Prag
);
3089 -- Process the contracts of all inherited subprograms, looking for
3090 -- class-wide postconditions.
3092 for Index
in Subps
'Range loop
3093 Subp_Id
:= Subps
(Index
);
3095 if Present
(Alias
(Subp_Id
)) then
3096 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
3099 -- Wrappers of class-wide pre/postconditions reference the
3100 -- parent primitive that has the inherited contract.
3102 if Is_Wrapper
(Subp_Id
)
3103 and then Present
(LSP_Subprogram
(Subp_Id
))
3105 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
3108 Items
:= Contract
(Subp_Id
);
3110 if not Seen_Subp
(Subp_Id
) and then Present
(Items
) then
3111 Seen
(Index
) := Subp_Id
;
3113 Prag
:= Pre_Post_Conditions
(Items
);
3114 while Present
(Prag
) loop
3115 if Pragma_Name
(Prag
) = Name_Postcondition
3116 and then Class_Present
(Prag
)
3119 Build_Pragma_Check_Equivalent
3122 Inher_Id
=> Subp_Id
);
3124 -- The pragma Check equivalent of the class-wide
3125 -- postcondition is still created even though the
3126 -- pragma may be ignored because the equivalent
3127 -- performs semantic checks.
3129 if Is_Checked
(Prag
) then
3130 Append_Enabled_Item
(Item
, Stmts
);
3134 Prag
:= Next_Pragma
(Prag
);
3138 end Process_Spec_Postconditions
;
3140 pragma Unmodified
(Stmts
);
3141 -- Stmts is passed as IN OUT to signal that the list can be updated,
3142 -- even if the corresponding integer value representing the list does
3145 -- Start of processing for Process_Postconditions
3148 -- The processing of postconditions is done in reverse order (body
3149 -- first) to ensure the following arrangement:
3151 -- <refined postconditions from body>
3152 -- <postconditions from body>
3153 -- <postconditions from spec>
3154 -- <inherited postconditions>
3156 Process_Body_Postconditions
(Name_Refined_Post
);
3157 Process_Body_Postconditions
(Name_Postcondition
);
3159 if Present
(Spec_Id
) then
3160 Process_Spec_Postconditions
;
3162 end Process_Postconditions
;
3164 ---------------------------
3165 -- Process_Preconditions --
3166 ---------------------------
3168 procedure Process_Preconditions
(Decls
: in out List_Id
) is
3169 Insert_Node
: Node_Id
:= Empty
;
3170 -- The insertion node after which all pragma Check equivalents are
3173 procedure Prepend_To_Decls
(Item
: Node_Id
);
3174 -- Prepend a single item to the declarations of the subprogram body
3176 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
);
3177 -- Prepend a normal precondition to the declarations of the body and
3180 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
3181 -- Collect all preconditions of subprogram Subp_Id and prepend their
3182 -- pragma Check equivalents to the declarations of the body.
3184 ----------------------
3185 -- Prepend_To_Decls --
3186 ----------------------
3188 procedure Prepend_To_Decls
(Item
: Node_Id
) is
3190 -- Ensure that the body has a declarative list
3194 Set_Declarations
(Body_Decl
, Decls
);
3197 Prepend_To
(Decls
, Item
);
3198 end Prepend_To_Decls
;
3200 -----------------------------
3201 -- Prepend_Pragma_To_Decls --
3202 -----------------------------
3204 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
) is
3205 Check_Prag
: Node_Id
;
3208 -- Skip the sole class-wide precondition (if any) since it is
3209 -- processed by Merge_Class_Conditions.
3211 if Class_Present
(Prag
) then
3214 -- Accumulate the corresponding Check pragmas at the top of the
3215 -- declarations. Prepending the items ensures that they will be
3216 -- evaluated in their original order.
3219 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
3220 Prepend_To_Decls
(Check_Prag
);
3223 end Prepend_Pragma_To_Decls
;
3225 -------------------------------
3226 -- Process_Preconditions_For --
3227 -------------------------------
3229 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
3230 Items
: constant Node_Id
:= Contract
(Subp_Id
);
3231 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
3237 -- Process the contract. If the body is an expression function
3238 -- that is a completion, freeze types within, because this may
3239 -- not have been done yet, when the subprogram declaration and
3240 -- its completion by an expression function appear in distinct
3241 -- declarative lists of the same unit (visible and private).
3244 Was_Expression_Function
(Body_Decl
)
3245 and then Sloc
(Body_Id
) /= Sloc
(Subp_Id
)
3246 and then In_Same_Source_Unit
(Body_Id
, Subp_Id
)
3247 and then not In_Same_List
(Body_Decl
, Subp_Decl
);
3249 if Present
(Items
) then
3250 Prag
:= Pre_Post_Conditions
(Items
);
3251 while Present
(Prag
) loop
3252 if Pragma_Name
(Prag
) = Name_Precondition
3253 and then Is_Checked
(Prag
)
3256 and then Present
(Corresponding_Aspect
(Prag
))
3260 Typ
=> Standard_Boolean
,
3263 (First
(Pragma_Argument_Associations
(Prag
))),
3267 Prepend_Pragma_To_Decls
(Prag
);
3270 Prag
:= Next_Pragma
(Prag
);
3274 -- The subprogram declaration being processed is actually a body
3275 -- stub. The stub may carry a precondition pragma, in which case
3276 -- it must be taken into account. The pragma appears after the
3279 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
3281 -- Inspect the declarations following the body stub
3283 Decl
:= Next
(Subp_Decl
);
3284 while Present
(Decl
) loop
3286 -- Note that non-matching pragmas are skipped
3288 if Nkind
(Decl
) = N_Pragma
then
3289 if Pragma_Name
(Decl
) = Name_Precondition
3290 and then Is_Checked
(Decl
)
3292 Prepend_Pragma_To_Decls
(Decl
);
3295 -- Skip internally generated code
3297 elsif not Comes_From_Source
(Decl
) then
3300 -- Preconditions are usually grouped together. There is no
3301 -- need to inspect the whole declarative list.
3310 end Process_Preconditions_For
;
3314 Body_Decls
: constant List_Id
:= Declarations
(Body_Decl
);
3316 Next_Decl
: Node_Id
;
3318 -- Start of processing for Process_Preconditions
3321 -- Find the proper insertion point for all pragma Check equivalents
3323 if Present
(Body_Decls
) then
3324 Decl
:= First
(Body_Decls
);
3325 while Present
(Decl
) loop
3327 -- First source declaration terminates the search, because all
3328 -- preconditions must be evaluated prior to it, by definition.
3330 if Comes_From_Source
(Decl
) then
3333 -- Certain internally generated object renamings such as those
3334 -- for discriminants and protection fields must be elaborated
3335 -- before the preconditions are evaluated, as their expressions
3336 -- may mention the discriminants. The renamings include those
3337 -- for private components so we need to find the last such.
3339 elsif Is_Prologue_Renaming
(Decl
) then
3340 while Present
(Next
(Decl
))
3341 and then Is_Prologue_Renaming
(Next
(Decl
))
3346 Insert_Node
:= Decl
;
3348 -- Otherwise the declaration does not come from source. This
3349 -- also terminates the search, because internal code may raise
3350 -- exceptions which should not preempt the preconditions.
3359 -- The processing of preconditions is done in reverse order (body
3360 -- first), because each pragma Check equivalent is inserted at the
3361 -- top of the declarations. This ensures that the final order is
3362 -- consistent with following diagram:
3364 -- <inherited preconditions>
3365 -- <preconditions from spec>
3366 -- <preconditions from body>
3368 Process_Preconditions_For
(Body_Id
);
3370 -- Move the generated entry-call prologue renamings into the
3371 -- outer declarations for use in the preconditions.
3373 Decl
:= First
(Body_Decls
);
3374 while Present
(Decl
) and then Present
(Insert_Node
) loop
3375 Next_Decl
:= Next
(Decl
);
3377 Prepend_To_Decls
(Decl
);
3379 exit when Decl
= Insert_Node
;
3384 if Present
(Spec_Id
) then
3385 Process_Preconditions_For
(Spec_Id
);
3387 end Process_Preconditions
;
3391 Restore_Scope
: Boolean := False;
3393 Stmts
: List_Id
:= No_List
;
3394 Decls
: List_Id
:= New_List
;
3395 Subp_Id
: Entity_Id
;
3397 -- Start of processing for Expand_Subprogram_Contract
3400 -- Obtain the entity of the initial declaration
3402 if Present
(Spec_Id
) then
3408 -- Do not perform expansion activity when it is not needed
3410 if not Expander_Active
then
3413 -- GNATprove does not need the executable semantics of a contract
3415 elsif GNATprove_Mode
then
3418 -- The contract of a generic subprogram or one declared in a generic
3419 -- context is not expanded, as the corresponding instance will provide
3420 -- the executable semantics of the contract.
3422 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
3425 -- All subprograms carry a contract, but for some it is not significant
3426 -- and should not be processed. This is a small optimization.
3428 elsif not Has_Significant_Contract
(Subp_Id
) then
3431 -- The contract of an ignored Ghost subprogram does not need expansion,
3432 -- because the subprogram and all calls to it will be removed.
3434 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
3437 -- No action needed for helpers and indirect-call wrapper built to
3438 -- support class-wide preconditions.
3440 elsif Present
(Class_Preconditions_Subprogram
(Subp_Id
)) then
3443 -- Do not re-expand the same contract. This scenario occurs when a
3444 -- construct is rewritten into something else during its analysis
3445 -- (expression functions for instance).
3447 elsif Has_Expanded_Contract
(Subp_Id
) then
3451 -- Prevent multiple expansion attempts of the same contract
3453 Set_Has_Expanded_Contract
(Subp_Id
);
3455 -- Ensure that the formal parameters are visible when expanding all
3458 if not In_Open_Scopes
(Subp_Id
) then
3459 Restore_Scope
:= True;
3460 Push_Scope
(Subp_Id
);
3462 if Is_Generic_Subprogram
(Subp_Id
) then
3463 Install_Generic_Formals
(Subp_Id
);
3465 Install_Formals
(Subp_Id
);
3469 -- The expansion of a subprogram contract involves the creation of Check
3470 -- pragmas to verify the contract assertions of the spec and body in a
3471 -- particular order. The order is as follows:
3473 -- function Original_Code (...) return ... is
3474 -- <prologue renamings>
3475 -- <inherited preconditions>
3476 -- <preconditions from spec>
3477 -- <preconditions from body>
3478 -- <contract case conditions>
3480 -- function _Wrapped_Statements (...) return ... is
3481 -- <source declarations>
3483 -- <source statements>
3484 -- end _Wrapped_Statements;
3487 -- return Result : constant ... := _Wrapped_Statements do
3488 -- <refined postconditions from body>
3489 -- <postconditions from body>
3490 -- <postconditions from spec>
3491 -- <inherited postconditions>
3492 -- <contract case consequences>
3493 -- <invariant check of function result>
3494 -- <invariant and predicate checks of parameters
3496 -- end Original_Code;
3498 -- Step 1: augment contracts list with postconditions associated with
3499 -- Stable_Properties and Stable_Properties'Class aspects. This must
3500 -- precede Process_Postconditions.
3502 for Class_Present
in Boolean loop
3503 Add_Stable_Property_Contracts
3504 (Subp_Id
, Class_Present
=> Class_Present
);
3507 -- Step 2: Handle all preconditions. This action must come before the
3508 -- processing of pragma Contract_Cases because the pragma prepends items
3509 -- to the body declarations.
3511 Process_Preconditions
(Decls
);
3513 -- Step 3: Handle all postconditions. This action must come before the
3514 -- processing of pragma Contract_Cases because the pragma appends items
3517 Process_Postconditions
(Stmts
);
3519 -- Step 4: Handle pragma Contract_Cases. This action must come before
3520 -- the processing of invariants and predicates because those append
3521 -- items to list Stmts.
3523 Process_Contract_Cases
(Stmts
, Decls
);
3525 -- Step 5: Apply invariant and predicate checks on a function result and
3526 -- all formals. The resulting checks are accumulated in list Stmts.
3528 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3530 -- Step 6: Construct subprogram _wrapped_statements
3532 -- When no statements are present we still need to insert contract
3533 -- related declarations.
3536 Prepend_List_To
(Declarations
(Body_Decl
), Decls
);
3538 -- Otherwise, we need a wrapper
3541 Build_Subprogram_Contract_Wrapper
(Body_Id
, Stmts
, Decls
, Result
);
3544 if Restore_Scope
then
3547 end Expand_Subprogram_Contract
;
3549 -------------------------------
3550 -- Freeze_Previous_Contracts --
3551 -------------------------------
3553 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3554 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3555 pragma Inline
(Causes_Contract_Freezing
);
3556 -- Determine whether arbitrary node N causes contract freezing. This is
3557 -- used as an assertion for the current body declaration that caused
3558 -- contract freezing, and as a condition to detect body declaration that
3559 -- already caused contract freezing before.
3561 procedure Freeze_Contracts
;
3562 pragma Inline
(Freeze_Contracts
);
3563 -- Freeze the contracts of all eligible constructs which precede body
3566 procedure Freeze_Enclosing_Package_Body
;
3567 pragma Inline
(Freeze_Enclosing_Package_Body
);
3568 -- Freeze the contract of the nearest package body (if any) which
3569 -- encloses body Body_Decl.
3571 ------------------------------
3572 -- Causes_Contract_Freezing --
3573 ------------------------------
3575 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3577 -- The following condition matches guards for calls to
3578 -- Freeze_Previous_Contracts from routines that analyze various body
3579 -- declarations. In particular, it detects expression functions, as
3580 -- described in the call from Analyze_Subprogram_Body_Helper.
3583 Comes_From_Source
(Original_Node
(N
))
3586 N_Entry_Body | N_Package_Body | N_Protected_Body |
3587 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body
;
3588 end Causes_Contract_Freezing
;
3590 ----------------------
3591 -- Freeze_Contracts --
3592 ----------------------
3594 procedure Freeze_Contracts
is
3595 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3599 -- Nothing to do when the body which causes freezing does not appear
3600 -- in a declarative list because there cannot possibly be constructs
3603 if not Is_List_Member
(Body_Decl
) then
3607 -- Inspect the declarations preceding the body, and freeze individual
3608 -- contracts of eligible constructs.
3610 Decl
:= Prev
(Body_Decl
);
3611 while Present
(Decl
) loop
3613 -- Stop the traversal when a preceding construct that causes
3614 -- freezing is encountered as there is no point in refreezing
3615 -- the already frozen constructs.
3617 if Causes_Contract_Freezing
(Decl
) then
3620 -- Entry or subprogram declarations
3622 elsif Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
3623 | N_Entry_Declaration
3624 | N_Generic_Subprogram_Declaration
3625 | N_Subprogram_Declaration
3627 Analyze_Entry_Or_Subprogram_Contract
3628 (Subp_Id
=> Defining_Entity
(Decl
),
3629 Freeze_Id
=> Body_Id
);
3633 elsif Nkind
(Decl
) = N_Object_Declaration
then
3634 Analyze_Object_Contract
3635 (Obj_Id
=> Defining_Entity
(Decl
),
3636 Freeze_Id
=> Body_Id
);
3640 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
3641 | N_Single_Protected_Declaration
3643 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3645 -- Subprogram body stubs
3647 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3648 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3652 elsif Nkind
(Decl
) in N_Single_Task_Declaration
3653 | N_Task_Type_Declaration
3655 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3658 if Nkind
(Decl
) in N_Full_Type_Declaration
3659 | N_Private_Type_Declaration
3660 | N_Task_Type_Declaration
3661 | N_Protected_Type_Declaration
3662 | N_Formal_Type_Declaration
3664 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
3669 end Freeze_Contracts
;
3671 -----------------------------------
3672 -- Freeze_Enclosing_Package_Body --
3673 -----------------------------------
3675 procedure Freeze_Enclosing_Package_Body
is
3676 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3680 -- Climb the parent chain looking for an enclosing package body. Do
3681 -- not use the scope stack, because a body utilizes the entity of its
3682 -- corresponding spec.
3684 Par
:= Parent
(Body_Decl
);
3685 while Present
(Par
) loop
3686 if Nkind
(Par
) = N_Package_Body
then
3687 Analyze_Package_Body_Contract
3688 (Body_Id
=> Defining_Entity
(Par
),
3689 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3693 -- Do not look for an enclosing package body when the construct
3694 -- which causes freezing is a body generated for an expression
3695 -- function and it appears within a package spec. This ensures
3696 -- that the traversal will not reach too far up the parent chain
3697 -- and attempt to freeze a package body which must not be frozen.
3699 -- package body Enclosing_Body
3700 -- with Refined_State => (State => Var)
3702 -- package Nested is
3703 -- type Some_Type is ...;
3704 -- function Cause_Freezing return ...;
3706 -- function Cause_Freezing is (...);
3709 -- Var : Nested.Some_Type;
3711 elsif Nkind
(Par
) = N_Package_Declaration
3712 and then Nkind
(Orig_Decl
) = N_Expression_Function
3716 -- Prevent the search from going too far
3718 elsif Is_Body_Or_Package_Declaration
(Par
) then
3722 Par
:= Parent
(Par
);
3724 end Freeze_Enclosing_Package_Body
;
3728 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3730 -- Start of processing for Freeze_Previous_Contracts
3733 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3735 -- A body that is in the process of being inlined appears from source,
3736 -- but carries name _parent. Such a body does not cause freezing of
3739 if Chars
(Body_Id
) = Name_uParent
then
3743 Freeze_Enclosing_Package_Body
;
3745 end Freeze_Previous_Contracts
;
3747 ---------------------------------
3748 -- Inherit_Subprogram_Contract --
3749 ---------------------------------
3751 procedure Inherit_Subprogram_Contract
3753 From_Subp
: Entity_Id
)
3755 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3756 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3759 --------------------
3760 -- Inherit_Pragma --
3761 --------------------
3763 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3764 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3768 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3769 -- chains, therefore the node must be replicated. The new pragma is
3770 -- flagged as inherited for distinction purposes.
3772 if Present
(Prag
) then
3773 New_Prag
:= New_Copy_Tree
(Prag
);
3774 Set_Is_Inherited_Pragma
(New_Prag
);
3776 Add_Contract_Item
(New_Prag
, Subp
);
3780 -- Start of processing for Inherit_Subprogram_Contract
3783 -- Inheritance is carried out only when both entities are subprograms
3786 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3787 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3788 and then Present
(Contract
(From_Subp
))
3790 Inherit_Pragma
(Pragma_Extensions_Visible
);
3791 Inherit_Pragma
(Pragma_Side_Effects
);
3793 end Inherit_Subprogram_Contract
;
3795 -------------------------------------
3796 -- Instantiate_Subprogram_Contract --
3797 -------------------------------------
3799 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3800 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3801 -- Instantiate all contract-related source pragmas found in the list,
3802 -- starting with pragma First_Prag. Each instantiated pragma is added
3805 -------------------------
3806 -- Instantiate_Pragmas --
3807 -------------------------
3809 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3810 Inst_Prag
: Node_Id
;
3815 while Present
(Prag
) loop
3816 if Is_Generic_Contract_Pragma
(Prag
) then
3818 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3820 Set_Analyzed
(Inst_Prag
, False);
3821 Append_To
(L
, Inst_Prag
);
3824 Prag
:= Next_Pragma
(Prag
);
3826 end Instantiate_Pragmas
;
3830 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3832 -- Start of processing for Instantiate_Subprogram_Contract
3835 if Present
(Items
) then
3836 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3837 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3838 Instantiate_Pragmas
(Classifications
(Items
));
3840 end Instantiate_Subprogram_Contract
;
3842 --------------------------
3843 -- Is_Prologue_Renaming --
3844 --------------------------
3846 -- This should be turned into a flag and set during the expansion of
3847 -- task and protected types when the renamings get generated ???
3849 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
3856 if Nkind
(Decl
) = N_Object_Renaming_Declaration
3857 and then not Comes_From_Source
(Decl
)
3859 Obj
:= Defining_Entity
(Decl
);
3862 if Nkind
(Nam
) = N_Selected_Component
then
3863 -- Analyze the renaming declaration so we can further examine it
3865 if not Analyzed
(Decl
) then
3869 Pref
:= Prefix
(Nam
);
3870 Sel
:= Selector_Name
(Nam
);
3872 -- A discriminant renaming appears as
3873 -- Discr : constant ... := Prefix.Discr;
3875 if Ekind
(Obj
) = E_Constant
3876 and then Is_Entity_Name
(Sel
)
3877 and then Present
(Entity
(Sel
))
3878 and then Ekind
(Entity
(Sel
)) = E_Discriminant
3882 -- A protection field renaming appears as
3883 -- Prot : ... := _object._object;
3885 -- A renamed private component is just a component of
3886 -- _object, with an arbitrary name.
3888 elsif Ekind
(Obj
) in E_Variable | E_Constant
3889 and then Nkind
(Pref
) = N_Identifier
3890 and then Chars
(Pref
) = Name_uObject
3891 and then Nkind
(Sel
) = N_Identifier
3899 end Is_Prologue_Renaming
;
3901 -----------------------------------
3902 -- Make_Class_Precondition_Subps --
3903 -----------------------------------
3905 procedure Make_Class_Precondition_Subps
3906 (Subp_Id
: Entity_Id
;
3907 Late_Overriding
: Boolean := False)
3909 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
3910 Tagged_Type
: constant Entity_Id
:= Find_Dispatching_Type
(Subp_Id
);
3912 procedure Add_Indirect_Call_Wrapper
;
3913 -- Build the indirect-call wrapper and append it to the freezing actions
3916 procedure Add_Call_Helper
3917 (Helper_Id
: Entity_Id
;
3918 Is_Dynamic
: Boolean);
3919 -- Factorizes code for building a call helper with the given identifier
3920 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
3921 -- controls building the static or dynamic version of the helper.
3923 function Build_Unique_Name
(Suffix
: String) return Name_Id
;
3924 -- Build an unique new name adding suffix to Subp_Id name (plus its
3925 -- homonym number for values bigger than 1).
3927 -------------------------------
3928 -- Add_Indirect_Call_Wrapper --
3929 -------------------------------
3931 procedure Add_Indirect_Call_Wrapper
is
3933 function Build_ICW_Body
return Node_Id
;
3934 -- Build the body of the indirect call wrapper
3936 function Build_ICW_Decl
return Node_Id
;
3937 -- Build the declaration of the indirect call wrapper
3939 --------------------
3940 -- Build_ICW_Body --
3941 --------------------
3943 function Build_ICW_Body
return Node_Id
is
3944 ICW_Id
: constant Entity_Id
:= Indirect_Call_Wrapper
(Subp_Id
);
3945 Spec
: constant Node_Id
:= Parent
(ICW_Id
);
3946 Body_Spec
: Node_Id
;
3951 Body_Spec
:= Copy_Subprogram_Spec
(Spec
);
3953 -- Build call to wrapped subprogram
3956 Actuals
: constant List_Id
:= Empty_List
;
3957 Formal_Spec
: Entity_Id
:=
3958 First
(Parameter_Specifications
(Spec
));
3960 -- Build parameter association & call
3962 while Present
(Formal_Spec
) loop
3965 (Defining_Identifier
(Formal_Spec
), Loc
));
3969 if Ekind
(ICW_Id
) = E_Procedure
then
3971 Make_Procedure_Call_Statement
(Loc
,
3972 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3973 Parameter_Associations
=> Actuals
);
3976 Make_Simple_Return_Statement
(Loc
,
3978 Make_Function_Call
(Loc
,
3979 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3980 Parameter_Associations
=> Actuals
));
3985 Make_Subprogram_Body
(Loc
,
3986 Specification
=> Body_Spec
,
3987 Declarations
=> New_List
,
3988 Handled_Statement_Sequence
=>
3989 Make_Handled_Sequence_Of_Statements
(Loc
,
3990 Statements
=> New_List
(Call
)));
3992 -- The new operation is internal and overriding indicators do not
3995 Set_Must_Override
(Body_Spec
, False);
4000 --------------------
4001 -- Build_ICW_Decl --
4002 --------------------
4004 function Build_ICW_Decl
return Node_Id
is
4005 ICW_Id
: constant Entity_Id
:=
4006 Make_Defining_Identifier
(Loc
,
4007 Build_Unique_Name
(Suffix
=> "ICW"));
4012 Spec
:= Copy_Subprogram_Spec
(Parent
(Subp_Id
));
4013 Set_Must_Override
(Spec
, False);
4014 Set_Must_Not_Override
(Spec
, False);
4015 Set_Defining_Unit_Name
(Spec
, ICW_Id
);
4016 Mutate_Ekind
(ICW_Id
, Ekind
(Subp_Id
));
4017 Set_Is_Public
(ICW_Id
);
4019 -- The indirect call wrapper is commonly used for indirect calls
4020 -- but inlined for direct calls performed from the DTW.
4022 Set_Is_Inlined
(ICW_Id
);
4024 if Nkind
(Spec
) = N_Procedure_Specification
then
4025 Set_Null_Present
(Spec
, False);
4028 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
4030 -- Link original subprogram to indirect wrapper and vice versa
4032 Set_Indirect_Call_Wrapper
(Subp_Id
, ICW_Id
);
4033 Set_Class_Preconditions_Subprogram
(ICW_Id
, Subp_Id
);
4035 -- Inherit debug info flag to allow debugging the wrapper
4037 if Needs_Debug_Info
(Subp_Id
) then
4038 Set_Debug_Info_Needed
(ICW_Id
);
4049 -- Start of processing for Add_Indirect_Call_Wrapper
4052 pragma Assert
(No
(Indirect_Call_Wrapper
(Subp_Id
)));
4054 ICW_Decl
:= Build_ICW_Decl
;
4056 Append_Freeze_Action
(Tagged_Type
, ICW_Decl
);
4059 ICW_Body
:= Build_ICW_Body
;
4060 Append_Freeze_Action
(Tagged_Type
, ICW_Body
);
4062 -- We cannot defer the analysis of this ICW wrapper when it is
4063 -- built as a consequence of building its partner DTW wrapper
4064 -- at the freezing point of the tagged type.
4066 if Is_Dispatch_Table_Wrapper
(Subp_Id
) then
4069 end Add_Indirect_Call_Wrapper
;
4071 ---------------------
4072 -- Add_Call_Helper --
4073 ---------------------
4075 procedure Add_Call_Helper
4076 (Helper_Id
: Entity_Id
;
4077 Is_Dynamic
: Boolean)
4079 function Build_Call_Helper_Body
return Node_Id
;
4080 -- Build the body of a call helper
4082 function Build_Call_Helper_Decl
return Node_Id
;
4083 -- Build the declaration of a call helper
4085 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
;
4086 -- Build the specification of the helper
4088 ----------------------------
4089 -- Build_Call_Helper_Body --
4090 ----------------------------
4092 function Build_Call_Helper_Body
return Node_Id
is
4094 function Copy_And_Update_References
4095 (Expr
: Node_Id
) return Node_Id
;
4096 -- Copy Expr updating references to formals of Helper_Id; update
4097 -- also references to loop identifiers of quantified expressions.
4099 --------------------------------
4100 -- Copy_And_Update_References --
4101 --------------------------------
4103 function Copy_And_Update_References
4104 (Expr
: Node_Id
) return Node_Id
4106 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4108 procedure Map_Quantified_Expression_Loop_Identifiers
;
4109 -- Traverse Expr and append to Assoc_List the mapping of loop
4110 -- identifers of quantified expressions with its new copy.
4112 ------------------------------------------------
4113 -- Map_Quantified_Expression_Loop_Identifiers --
4114 ------------------------------------------------
4116 procedure Map_Quantified_Expression_Loop_Identifiers
is
4117 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
;
4118 -- Append to Assoc_List the mapping of loop identifers of
4119 -- quantified expressions with its new copy.
4121 --------------------
4122 -- Map_Loop_Param --
4123 --------------------
4125 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
4128 if Nkind
(N
) = N_Loop_Parameter_Specification
4129 and then Nkind
(Parent
(N
)) = N_Quantified_Expression
4132 Def_Id
: constant Entity_Id
:=
4133 Defining_Identifier
(N
);
4135 Append_Elmt
(Def_Id
, Assoc_List
);
4136 Append_Elmt
(New_Copy
(Def_Id
), Assoc_List
);
4143 procedure Map_Quantified_Expressions
is
4144 new Traverse_Proc
(Map_Loop_Param
);
4147 Map_Quantified_Expressions
(Expr
);
4148 end Map_Quantified_Expression_Loop_Identifiers
;
4152 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp_Id
);
4153 Helper_Formal_Id
: Entity_Id
:= First_Formal
(Helper_Id
);
4155 -- Start of processing for Copy_And_Update_References
4158 while Present
(Subp_Formal_Id
) loop
4159 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4160 Append_Elmt
(Helper_Formal_Id
, Assoc_List
);
4162 Next_Formal
(Subp_Formal_Id
);
4163 Next_Formal
(Helper_Formal_Id
);
4166 Map_Quantified_Expression_Loop_Identifiers
;
4168 return New_Copy_Tree
(Expr
, Map
=> Assoc_List
);
4169 end Copy_And_Update_References
;
4173 Helper_Decl
: constant Node_Id
:= Parent
(Parent
(Helper_Id
));
4174 Body_Id
: Entity_Id
;
4175 Body_Spec
: Node_Id
;
4176 Body_Stmts
: Node_Id
;
4177 Helper_Body
: Node_Id
;
4178 Return_Expr
: Node_Id
;
4180 -- Start of processing for Build_Call_Helper_Body
4183 pragma Assert
(Analyzed
(Unit_Declaration_Node
(Helper_Id
)));
4184 pragma Assert
(No
(Corresponding_Body
(Helper_Decl
)));
4186 Body_Id
:= Make_Defining_Identifier
(Loc
, Chars
(Helper_Id
));
4187 Body_Spec
:= Build_Call_Helper_Spec
(Body_Id
);
4189 Set_Corresponding_Body
(Helper_Decl
, Body_Id
);
4190 Set_Must_Override
(Body_Spec
, False);
4192 if Present
(Class_Preconditions
(Subp_Id
))
4193 -- Evaluate the expression if we are building a dynamic helper
4194 -- or we are building a static helper for a non-abstract tagged
4195 -- type; for abstract tagged types the helper just returns True
4196 -- since it is called by the indirect call wrapper (ICW).
4200 not Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)))
4203 Copy_And_Update_References
(Class_Preconditions
(Subp_Id
));
4205 -- When the subprogram is compiled with assertions disabled the
4206 -- helper just returns True; done to avoid reporting errors at
4207 -- link time since a unit may be compiled with assertions disabled
4208 -- and another (which depends on it) compiled with assertions
4212 pragma Assert
(Present
(Ignored_Class_Preconditions
(Subp_Id
))
4213 or else Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)));
4214 Return_Expr
:= New_Occurrence_Of
(Standard_True
, Loc
);
4218 Make_Handled_Sequence_Of_Statements
(Loc
,
4219 Statements
=> New_List
(
4220 Make_Simple_Return_Statement
(Loc
, Return_Expr
)));
4223 Make_Subprogram_Body
(Loc
,
4224 Specification
=> Body_Spec
,
4225 Declarations
=> New_List
,
4226 Handled_Statement_Sequence
=> Body_Stmts
);
4229 end Build_Call_Helper_Body
;
4231 ----------------------------
4232 -- Build_Call_Helper_Decl --
4233 ----------------------------
4235 function Build_Call_Helper_Decl
return Node_Id
is
4240 Spec
:= Build_Call_Helper_Spec
(Helper_Id
);
4241 Set_Must_Override
(Spec
, False);
4242 Set_Must_Not_Override
(Spec
, False);
4243 Set_Is_Inlined
(Helper_Id
);
4244 Set_Is_Public
(Helper_Id
);
4246 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
4248 -- Inherit debug info flag from Subp_Id to Helper_Id to allow
4249 -- debugging of the helper subprogram.
4251 if Needs_Debug_Info
(Subp_Id
) then
4252 Set_Debug_Info_Needed
(Helper_Id
);
4256 end Build_Call_Helper_Decl
;
4258 ----------------------------
4259 -- Build_Call_Helper_Spec --
4260 ----------------------------
4262 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
4264 Spec
: constant Node_Id
:= Parent
(Subp_Id
);
4265 Def_Id
: constant Node_Id
:= Defining_Unit_Name
(Spec
);
4267 Func_Formals
: constant List_Id
:= New_List
;
4268 P_Spec
: constant List_Id
:= Parameter_Specifications
(Spec
);
4269 Par_Formal
: Node_Id
;
4271 Param_Type
: Node_Id
;
4274 -- Create a list of formal parameters with the same types as the
4275 -- original subprogram but changing the controlling formal.
4277 Param
:= First
(P_Spec
);
4278 Formal
:= First_Formal
(Def_Id
);
4279 while Present
(Formal
) loop
4280 Par_Formal
:= Parent
(Formal
);
4282 if Is_Dynamic
and then Is_Controlling_Formal
(Formal
) then
4283 if Nkind
(Parameter_Type
(Par_Formal
))
4284 = N_Access_Definition
4287 Copy_Separate_Tree
(Parameter_Type
(Par_Formal
));
4288 Rewrite
(Subtype_Mark
(Param_Type
),
4289 Make_Attribute_Reference
(Loc
,
4290 Prefix
=> Relocate_Node
(Subtype_Mark
(Param_Type
)),
4291 Attribute_Name
=> Name_Class
));
4295 Make_Attribute_Reference
(Loc
,
4296 Prefix
=> New_Occurrence_Of
(Etype
(Formal
), Loc
),
4297 Attribute_Name
=> Name_Class
);
4300 Param_Type
:= New_Occurrence_Of
(Etype
(Formal
), Loc
);
4303 Append_To
(Func_Formals
,
4304 Make_Parameter_Specification
(Loc
,
4305 Defining_Identifier
=>
4306 Make_Defining_Identifier
(Loc
, Chars
(Formal
)),
4307 In_Present
=> In_Present
(Par_Formal
),
4308 Out_Present
=> Out_Present
(Par_Formal
),
4309 Null_Exclusion_Present
=> Null_Exclusion_Present
4311 Parameter_Type
=> Param_Type
));
4314 Next_Formal
(Formal
);
4318 Make_Function_Specification
(Loc
,
4319 Defining_Unit_Name
=> Spec_Id
,
4320 Parameter_Specifications
=> Func_Formals
,
4321 Result_Definition
=>
4322 New_Occurrence_Of
(Standard_Boolean
, Loc
));
4323 end Build_Call_Helper_Spec
;
4327 Helper_Body
: Node_Id
;
4328 Helper_Decl
: Node_Id
;
4330 -- Start of processing for Add_Call_Helper
4333 Helper_Decl
:= Build_Call_Helper_Decl
;
4334 Mutate_Ekind
(Helper_Id
, Ekind
(Subp_Id
));
4336 -- Add the helper to the freezing actions of the tagged type
4338 Append_Freeze_Action
(Tagged_Type
, Helper_Decl
);
4339 Analyze
(Helper_Decl
);
4341 Helper_Body
:= Build_Call_Helper_Body
;
4342 Append_Freeze_Action
(Tagged_Type
, Helper_Body
);
4344 -- If this helper is built as part of building the DTW at the
4345 -- freezing point of its tagged type then we cannot defer
4348 if Late_Overriding
then
4349 pragma Assert
(Is_Dispatch_Table_Wrapper
(Subp_Id
));
4350 Analyze
(Helper_Body
);
4352 end Add_Call_Helper
;
4354 -----------------------
4355 -- Build_Unique_Name --
4356 -----------------------
4358 function Build_Unique_Name
(Suffix
: String) return Name_Id
is
4360 -- Append the homonym number. Strip the leading space character in
4361 -- the image of natural numbers. Also do not add the homonym value
4364 if Has_Homonym
(Subp_Id
) and then Homonym_Number
(Subp_Id
) > 1 then
4366 S
: constant String := Homonym_Number
(Subp_Id
)'Img;
4369 return New_External_Name
(Chars
(Subp_Id
),
4370 Suffix
=> Suffix
& "_" & S
(2 .. S
'Last));
4374 return New_External_Name
(Chars
(Subp_Id
), Suffix
);
4375 end Build_Unique_Name
;
4379 Helper_Id
: Entity_Id
;
4381 -- Start of processing for Make_Class_Precondition_Subps
4384 if Present
(Class_Preconditions
(Subp_Id
))
4385 or Present
(Ignored_Class_Preconditions
(Subp_Id
))
4388 (Comes_From_Source
(Subp_Id
)
4389 or else Is_Dispatch_Table_Wrapper
(Subp_Id
));
4391 if No
(Dynamic_Call_Helper
(Subp_Id
)) then
4393 -- Build and add to the freezing actions of Tagged_Type its
4394 -- dynamic-call helper.
4397 Make_Defining_Identifier
(Loc
,
4398 Build_Unique_Name
(Suffix
=> "DP"));
4399 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> True);
4401 -- Link original subprogram to helper and vice versa
4403 Set_Dynamic_Call_Helper
(Subp_Id
, Helper_Id
);
4404 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4407 if not Is_Abstract_Subprogram
(Subp_Id
)
4408 and then No
(Static_Call_Helper
(Subp_Id
))
4410 -- Build and add to the freezing actions of Tagged_Type its
4411 -- static-call helper.
4414 Make_Defining_Identifier
(Loc
,
4415 Build_Unique_Name
(Suffix
=> "SP"));
4417 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> False);
4419 -- Link original subprogram to helper and vice versa
4421 Set_Static_Call_Helper
(Subp_Id
, Helper_Id
);
4422 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4424 -- Build and add to the freezing actions of Tagged_Type the
4425 -- indirect-call wrapper.
4427 Add_Indirect_Call_Wrapper
;
4430 end Make_Class_Precondition_Subps
;
4432 ----------------------------------------------
4433 -- Process_Class_Conditions_At_Freeze_Point --
4434 ----------------------------------------------
4436 procedure Process_Class_Conditions_At_Freeze_Point
(Typ
: Entity_Id
) is
4438 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
);
4439 -- Check class-wide pre/postconditions of Spec_Id
4441 function Has_Class_Postconditions_Subprogram
4442 (Spec_Id
: Entity_Id
) return Boolean;
4443 -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
4445 function Has_Class_Preconditions_Subprogram
4446 (Spec_Id
: Entity_Id
) return Boolean;
4447 -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
4449 ----------------------------
4450 -- Check_Class_Conditions --
4451 ----------------------------
4453 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
) is
4454 Par_Subp
: Entity_Id
;
4457 for Kind
in Condition_Kind
loop
4458 Par_Subp
:= Nearest_Class_Condition_Subprogram
(Kind
, Spec_Id
);
4460 if Present
(Par_Subp
) then
4461 Check_Class_Condition
4462 (Cond
=> Class_Condition
(Kind
, Par_Subp
),
4464 Par_Subp
=> Par_Subp
,
4465 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4466 | Class_Precondition
);
4469 end Check_Class_Conditions
;
4471 -----------------------------------------
4472 -- Has_Class_Postconditions_Subprogram --
4473 -----------------------------------------
4475 function Has_Class_Postconditions_Subprogram
4476 (Spec_Id
: Entity_Id
) return Boolean is
4479 Present
(Nearest_Class_Condition_Subprogram
4480 (Spec_Id
=> Spec_Id
,
4481 Kind
=> Class_Postcondition
))
4483 Present
(Nearest_Class_Condition_Subprogram
4484 (Spec_Id
=> Spec_Id
,
4485 Kind
=> Ignored_Class_Postcondition
));
4486 end Has_Class_Postconditions_Subprogram
;
4488 ----------------------------------------
4489 -- Has_Class_Preconditions_Subprogram --
4490 ----------------------------------------
4492 function Has_Class_Preconditions_Subprogram
4493 (Spec_Id
: Entity_Id
) return Boolean is
4496 Present
(Nearest_Class_Condition_Subprogram
4497 (Spec_Id
=> Spec_Id
,
4498 Kind
=> Class_Precondition
))
4500 Present
(Nearest_Class_Condition_Subprogram
4501 (Spec_Id
=> Spec_Id
,
4502 Kind
=> Ignored_Class_Precondition
));
4503 end Has_Class_Preconditions_Subprogram
;
4507 Prim_Elmt
: Elmt_Id
:= First_Elmt
(Primitive_Operations
(Typ
));
4510 -- Start of processing for Process_Class_Conditions_At_Freeze_Point
4513 while Present
(Prim_Elmt
) loop
4514 Prim
:= Node
(Prim_Elmt
);
4516 if Has_Class_Preconditions_Subprogram
(Prim
)
4517 or else Has_Class_Postconditions_Subprogram
(Prim
)
4519 if Comes_From_Source
(Prim
) then
4520 if Has_Significant_Contract
(Prim
) then
4521 Merge_Class_Conditions
(Prim
);
4524 -- Handle wrapper of protected operation
4526 elsif Is_Primitive_Wrapper
(Prim
) then
4527 Merge_Class_Conditions
(Prim
);
4529 -- Check inherited class-wide conditions, excluding internal
4530 -- entities built for mapping of interface primitives.
4532 elsif Is_Derived_Type
(Typ
)
4533 and then Present
(Alias
(Prim
))
4534 and then No
(Interface_Alias
(Prim
))
4536 Check_Class_Conditions
(Prim
);
4540 Next_Elmt
(Prim_Elmt
);
4542 end Process_Class_Conditions_At_Freeze_Point
;
4544 ----------------------------
4545 -- Merge_Class_Conditions --
4546 ----------------------------
4548 procedure Merge_Class_Conditions
(Spec_Id
: Entity_Id
) is
4550 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
);
4551 -- Collect all inherited class-wide conditions of Spec_Id and merge
4552 -- them into one big condition.
4554 ----------------------------------
4555 -- Process_Inherited_Conditions --
4556 ----------------------------------
4558 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
) is
4559 Tag_Typ
: constant Entity_Id
:= Find_Dispatching_Type
(Spec_Id
);
4560 Subps
: constant Subprogram_List
:= Inherited_Subprograms
(Spec_Id
);
4561 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
4563 function Inherit_Condition
4564 (Par_Subp
: Entity_Id
;
4565 Subp
: Entity_Id
) return Node_Id
;
4566 -- Inherit the class-wide condition from Par_Subp to Subp and adjust
4567 -- all the references to formals in the inherited condition.
4569 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
);
4570 -- Merge two class-wide preconditions or postconditions (the former
4571 -- are merged using "or else", and the latter are merged using "and-
4572 -- then"). The changes are accumulated in parameter Into.
4574 function Seen_Subp
(Id
: Entity_Id
) return Boolean;
4575 -- Return True if the contract of subprogram Id has been processed
4577 -----------------------
4578 -- Inherit_Condition --
4579 -----------------------
4581 function Inherit_Condition
4582 (Par_Subp
: Entity_Id
;
4583 Subp
: Entity_Id
) return Node_Id
4585 function Check_Condition
(Expr
: Node_Id
) return Boolean;
4586 -- Used in assertion to check that Expr has no reference to the
4587 -- formals of Par_Subp.
4589 ---------------------
4590 -- Check_Condition --
4591 ---------------------
4593 function Check_Condition
(Expr
: Node_Id
) return Boolean is
4594 Par_Formal_Id
: Entity_Id
;
4596 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
4597 -- Check occurrence of Par_Formal_Id
4603 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
4605 if Nkind
(N
) = N_Identifier
4606 and then Present
(Entity
(N
))
4607 and then Entity
(N
) = Par_Formal_Id
4615 function Check_Expression
is new Traverse_Func
(Check_Entity
);
4617 -- Start of processing for Check_Condition
4620 Par_Formal_Id
:= First_Formal
(Par_Subp
);
4622 while Present
(Par_Formal_Id
) loop
4623 if Check_Expression
(Expr
) = Abandon
then
4627 Next_Formal
(Par_Formal_Id
);
4631 end Check_Condition
;
4635 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4636 Par_Formal_Id
: Entity_Id
:= First_Formal
(Par_Subp
);
4637 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp
);
4638 New_Condition
: Node_Id
;
4641 while Present
(Par_Formal_Id
) loop
4642 Append_Elmt
(Par_Formal_Id
, Assoc_List
);
4643 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4645 Next_Formal
(Par_Formal_Id
);
4646 Next_Formal
(Subp_Formal_Id
);
4649 -- Check that Parent field of all the nodes have their correct
4650 -- decoration; required because otherwise mapped nodes with
4651 -- wrong Parent field are left unmodified in the copied tree
4652 -- and cause reporting wrong errors at later stages.
4655 (Check_Parents
(Class_Condition
(Kind
, Par_Subp
), Assoc_List
));
4659 (Source
=> Class_Condition
(Kind
, Par_Subp
),
4662 -- Ensure that the inherited condition has no reference to the
4663 -- formals of the parent subprogram.
4665 pragma Assert
(Check_Condition
(New_Condition
));
4667 return New_Condition
;
4668 end Inherit_Condition
;
4670 ----------------------
4671 -- Merge_Conditions --
4672 ----------------------
4674 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
) is
4675 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
;
4676 -- Return the boolean expression argument of a condition while
4677 -- updating its parentheses count for the subsequent merge.
4679 --------------------
4680 -- Expression_Arg --
4681 --------------------
4683 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
is
4685 if Paren_Count
(Expr
) = 0 then
4686 Set_Paren_Count
(Expr
, 1);
4694 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
4695 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
4696 Loc
: constant Source_Ptr
:= Sloc
(Into
);
4698 -- Start of processing for Merge_Conditions
4703 -- Merge the two preconditions by "or else"-ing them
4705 when Ignored_Class_Precondition
4706 | Class_Precondition
4710 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4711 Left_Opnd
=> From_Expr
));
4713 -- Merge the two postconditions by "and then"-ing them
4715 when Ignored_Class_Postcondition
4716 | Class_Postcondition
4720 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4721 Left_Opnd
=> From_Expr
));
4723 end Merge_Conditions
;
4729 function Seen_Subp
(Id
: Entity_Id
) return Boolean is
4731 for Index
in Seen
'Range loop
4732 if Seen
(Index
) = Id
then
4742 Class_Cond
: Node_Id
;
4744 Subp_Id
: Entity_Id
;
4745 Par_Prim
: Entity_Id
:= Empty
;
4746 Par_Iface_Prims
: Elist_Id
:= No_Elist
;
4748 -- Start of processing for Process_Inherited_Conditions
4751 Class_Cond
:= Class_Condition
(Kind
, Spec_Id
);
4753 -- Process parent primitives looking for nearest ancestor with
4754 -- class-wide conditions.
4756 for Index
in Subps
'Range loop
4757 Subp_Id
:= Subps
(Index
);
4760 and then Is_Ancestor
(Find_Dispatching_Type
(Subp_Id
), Tag_Typ
)
4762 if Present
(Alias
(Subp_Id
)) then
4763 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4766 -- Wrappers of class-wide pre/postconditions reference the
4767 -- parent primitive that has the inherited contract and help
4768 -- us to climb fast.
4770 if Is_Wrapper
(Subp_Id
)
4771 and then Present
(LSP_Subprogram
(Subp_Id
))
4773 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
4776 if not Seen_Subp
(Subp_Id
)
4777 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4779 Seen
(Index
) := Subp_Id
;
4780 Par_Prim
:= Subp_Id
;
4781 Par_Iface_Prims
:= Covered_Interface_Primitives
(Par_Prim
);
4783 Cond
:= Inherit_Condition
4785 Par_Subp
=> Subp_Id
);
4787 if Present
(Class_Cond
) then
4788 Merge_Conditions
(Cond
, Class_Cond
);
4793 Check_Class_Condition
4794 (Cond
=> Class_Cond
,
4796 Par_Subp
=> Subp_Id
,
4797 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4798 | Class_Precondition
);
4799 Build_Class_Wide_Expression
4800 (Pragma_Or_Expr
=> Class_Cond
,
4802 Par_Subp
=> Subp_Id
,
4803 Adjust_Sloc
=> False);
4805 -- We are done as soon as we process the nearest ancestor
4812 -- Process the contract of interface primitives not covered by
4813 -- the nearest ancestor.
4815 for Index
in Subps
'Range loop
4816 Subp_Id
:= Subps
(Index
);
4818 if Is_Interface
(Find_Dispatching_Type
(Subp_Id
)) then
4819 if Present
(Alias
(Subp_Id
)) then
4820 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4823 if not Seen_Subp
(Subp_Id
)
4824 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4825 and then not Contains
(Par_Iface_Prims
, Subp_Id
)
4827 Seen
(Index
) := Subp_Id
;
4829 Cond
:= Inherit_Condition
4831 Par_Subp
=> Subp_Id
);
4833 Check_Class_Condition
4836 Par_Subp
=> Subp_Id
,
4837 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4838 | Class_Precondition
);
4839 Build_Class_Wide_Expression
4840 (Pragma_Or_Expr
=> Cond
,
4842 Par_Subp
=> Subp_Id
,
4843 Adjust_Sloc
=> False);
4845 if Present
(Class_Cond
) then
4846 Merge_Conditions
(Cond
, Class_Cond
);
4854 Set_Class_Condition
(Kind
, Spec_Id
, Class_Cond
);
4855 end Process_Inherited_Conditions
;
4861 -- Start of processing for Merge_Class_Conditions
4864 for Kind
in Condition_Kind
loop
4865 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4867 -- If this subprogram has class-wide conditions then preanalyze
4868 -- them before processing inherited conditions since conditions
4869 -- are checked and merged from right to left.
4871 if Present
(Cond
) then
4872 Preanalyze_Condition
(Spec_Id
, Cond
);
4875 Process_Inherited_Conditions
(Kind
);
4877 -- Preanalyze merged inherited conditions
4879 if Cond
/= Class_Condition
(Kind
, Spec_Id
) then
4880 Preanalyze_Condition
(Spec_Id
,
4881 Class_Condition
(Kind
, Spec_Id
));
4884 end Merge_Class_Conditions
;
4886 ---------------------------------
4887 -- Preanalyze_Class_Conditions --
4888 ---------------------------------
4890 procedure Preanalyze_Class_Conditions
(Spec_Id
: Entity_Id
) is
4894 for Kind
in Condition_Kind
loop
4895 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4897 if Present
(Cond
) then
4898 Preanalyze_Condition
(Spec_Id
, Cond
);
4901 end Preanalyze_Class_Conditions
;
4903 --------------------------
4904 -- Preanalyze_Condition --
4905 --------------------------
4907 procedure Preanalyze_Condition
4911 procedure Clear_Unset_References
;
4912 -- Clear unset references on formals of Subp since preanalysis
4913 -- occurs in a place unrelated to the actual code.
4915 procedure Remove_Controlling_Arguments
;
4916 -- Traverse Expr and clear the Controlling_Argument of calls to
4917 -- nonabstract functions.
4919 procedure Restore_Original_Selected_Component
;
4920 -- Traverse Expr searching for dispatching calls to functions whose
4921 -- original node was a selected component, and replace them with
4922 -- their original node.
4924 ----------------------------
4925 -- Clear_Unset_References --
4926 ----------------------------
4928 procedure Clear_Unset_References
is
4929 F
: Entity_Id
:= First_Formal
(Subp
);
4932 while Present
(F
) loop
4933 Set_Unset_Reference
(F
, Empty
);
4936 end Clear_Unset_References
;
4938 ----------------------------------
4939 -- Remove_Controlling_Arguments --
4940 ----------------------------------
4942 procedure Remove_Controlling_Arguments
is
4943 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
;
4944 -- Reset the Controlling_Argument of calls to nonabstract
4947 ---------------------
4948 -- Remove_Ctrl_Arg --
4949 ---------------------
4951 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
is
4953 if Nkind
(N
) = N_Function_Call
4954 and then Present
(Controlling_Argument
(N
))
4955 and then not Is_Abstract_Subprogram
(Entity
(Name
(N
)))
4957 Set_Controlling_Argument
(N
, Empty
);
4961 end Remove_Ctrl_Arg
;
4963 procedure Remove_Ctrl_Args
is new Traverse_Proc
(Remove_Ctrl_Arg
);
4965 Remove_Ctrl_Args
(Expr
);
4966 end Remove_Controlling_Arguments
;
4968 -----------------------------------------
4969 -- Restore_Original_Selected_Component --
4970 -----------------------------------------
4972 procedure Restore_Original_Selected_Component
is
4973 Restored_Nodes_List
: Elist_Id
:= No_Elist
;
4975 procedure Fix_Parents
(N
: Node_Id
);
4976 -- Traverse the subtree of N fixing the Parent field of all the
4979 function Restore_Node
(N
: Node_Id
) return Traverse_Result
;
4980 -- Process dispatching calls to functions whose original node was
4981 -- a selected component, and replace them with their original
4982 -- node. Restored nodes are stored in the Restored_Nodes_List
4983 -- to fix the parent fields of their subtrees in a separate
4990 procedure Fix_Parents
(N
: Node_Id
) is
4993 (Parent_Node
: Node_Id
;
4994 Node
: Node_Id
) return Traverse_Result
;
4995 -- Process a single node
5002 (Parent_Node
: Node_Id
;
5003 Node
: Node_Id
) return Traverse_Result
5005 Par
: constant Node_Id
:= Parent
(Node
);
5008 if Par
/= Parent_Node
then
5009 if Is_List_Member
(Node
) then
5010 Set_List_Parent
(List_Containing
(Node
), Parent_Node
);
5012 Set_Parent
(Node
, Parent_Node
);
5019 procedure Fix_Parents
is
5020 new Traverse_Proc_With_Parent
(Fix_Parent
);
5030 function Restore_Node
(N
: Node_Id
) return Traverse_Result
is
5032 if Nkind
(N
) = N_Function_Call
5033 and then Nkind
(Original_Node
(N
)) = N_Selected_Component
5034 and then Is_Dispatching_Operation
(Entity
(Name
(N
)))
5036 Rewrite
(N
, Original_Node
(N
));
5037 Set_Original_Node
(N
, N
);
5039 -- Save the restored node in the Restored_Nodes_List to fix
5040 -- the parent fields of their subtrees in a separate tree
5043 Append_New_Elmt
(N
, Restored_Nodes_List
);
5049 procedure Restore_Nodes
is new Traverse_Proc
(Restore_Node
);
5051 -- Start of processing for Restore_Original_Selected_Component
5054 Restore_Nodes
(Expr
);
5056 -- After restoring the original node we must fix the decoration
5057 -- of the Parent attribute to ensure tree consistency; required
5058 -- because when the class-wide condition is inherited, calls to
5059 -- New_Copy_Tree will perform copies of this subtree, and formal
5060 -- occurrences with wrong Parent field cannot be mapped to the
5063 if Present
(Restored_Nodes_List
) then
5065 Elmt
: Elmt_Id
:= First_Elmt
(Restored_Nodes_List
);
5068 while Present
(Elmt
) loop
5069 Fix_Parents
(Node
(Elmt
));
5074 end Restore_Original_Selected_Component
;
5076 -- Start of processing for Preanalyze_Condition
5079 pragma Assert
(Present
(Expr
));
5080 pragma Assert
(Inside_Class_Condition_Preanalysis
= False);
5083 Install_Formals
(Subp
);
5084 Inside_Class_Condition_Preanalysis
:= True;
5086 Preanalyze_Spec_Expression
(Expr
, Standard_Boolean
);
5088 Inside_Class_Condition_Preanalysis
:= False;
5091 -- If this preanalyzed condition has occurrences of dispatching calls
5092 -- using the Object.Operation notation, during preanalysis such calls
5093 -- are rewritten as dispatching function calls; if at later stages
5094 -- this condition is inherited we must have restored the original
5095 -- selected-component node to ensure that the preanalysis of the
5096 -- inherited condition rewrites these dispatching calls in the
5097 -- correct context to avoid reporting spurious errors.
5099 Restore_Original_Selected_Component
;
5101 -- Traverse Expr and clear the Controlling_Argument of calls to
5102 -- nonabstract functions. Required since the preanalyzed condition
5103 -- is not yet installed on its definite context and will be cloned
5104 -- and extended in derivations with additional conditions.
5106 Remove_Controlling_Arguments
;
5108 -- Clear also attribute Unset_Reference; again because preanalysis
5109 -- occurs in a place unrelated to the actual code.
5111 Clear_Unset_References
;
5112 end Preanalyze_Condition
;
5114 ----------------------------------------
5115 -- Save_Global_References_In_Contract --
5116 ----------------------------------------
5118 procedure Save_Global_References_In_Contract
5122 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
5123 -- Save all global references in contract-related source pragmas found
5124 -- in the list, starting with pragma First_Prag.
5126 ------------------------------------
5127 -- Save_Global_References_In_List --
5128 ------------------------------------
5130 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
5131 Prag
: Node_Id
:= First_Prag
;
5134 while Present
(Prag
) loop
5135 if Is_Generic_Contract_Pragma
(Prag
) then
5136 Save_Global_References
(Prag
);
5139 Prag
:= Next_Pragma
(Prag
);
5141 end Save_Global_References_In_List
;
5145 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
5147 -- Start of processing for Save_Global_References_In_Contract
5150 -- The entity of the analyzed generic copy must be on the scope stack
5151 -- to ensure proper detection of global references.
5153 Push_Scope
(Gen_Id
);
5155 if Permits_Aspect_Specifications
(Templ
)
5156 and then Has_Aspects
(Templ
)
5158 Save_Global_References_In_Aspects
(Templ
);
5161 if Present
(Items
) then
5162 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
5163 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
5164 Save_Global_References_In_List
(Classifications
(Items
));
5168 end Save_Global_References_In_Contract
;
5170 -------------------------
5171 -- Set_Class_Condition --
5172 -------------------------
5174 procedure Set_Class_Condition
5175 (Kind
: Condition_Kind
;
5181 when Class_Postcondition
=>
5182 Set_Class_Postconditions
(Subp
, Cond
);
5184 when Class_Precondition
=>
5185 Set_Class_Preconditions
(Subp
, Cond
);
5187 when Ignored_Class_Postcondition
=>
5188 Set_Ignored_Class_Postconditions
(Subp
, Cond
);
5190 when Ignored_Class_Precondition
=>
5191 Set_Ignored_Class_Preconditions
(Subp
, Cond
);
5193 end Set_Class_Condition
;