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
238 -- Subprogram_Variant
242 elsif Is_Entry_Declaration
(Id
)
243 or else Ekind
(Id
) in E_Function
245 | E_Generic_Procedure
248 if Prag_Nam
in Name_Attach_Handler | Name_Interrupt_Handler
249 and then Ekind
(Id
) in E_Generic_Procedure | E_Procedure
253 elsif Prag_Nam
in Name_Depends
254 | Name_Extensions_Visible
259 elsif Prag_Nam
= Name_Volatile_Function
260 and then Ekind
(Id
) in E_Function | E_Generic_Function
264 elsif Prag_Nam
in Name_Always_Terminates
265 | Name_Contract_Cases
266 | Name_Exceptional_Cases
267 | Name_Subprogram_Variant
270 Add_Contract_Test_Case
;
272 elsif Prag_Nam
in Name_Postcondition | Name_Precondition
then
273 Add_Pre_Post_Condition
;
275 -- The pragma is not a proper contract item
278 raise Contract_Error
;
281 -- Packages or instantiations, the applicable pragmas are:
285 -- Part_Of (instantiation only)
287 elsif Is_Package_Or_Generic_Package
(Id
) then
288 if Prag_Nam
in Name_Abstract_State
289 | Name_Initial_Condition
294 -- Indicator Part_Of must be associated with a package instantiation
296 elsif Prag_Nam
= Name_Part_Of
and then Is_Generic_Instance
(Id
) then
299 elsif Prag_Nam
= Name_Always_Terminates
then
300 Add_Contract_Test_Case
;
302 -- The pragma is not a proper contract item
305 raise Contract_Error
;
308 -- Package bodies, the applicable pragmas are:
311 elsif Ekind
(Id
) = E_Package_Body
then
312 if Prag_Nam
= Name_Refined_State
then
315 -- The pragma is not a proper contract item
318 raise Contract_Error
;
321 -- The four volatility refinement pragmas are ok for all types.
322 -- Part_Of is ok for task types and protected types.
323 -- Depends and Global are ok for task types.
325 -- Precondition and Postcondition are added separately; they are allowed
326 -- for access-to-subprogram types.
328 elsif Is_Type
(Id
) then
330 Is_OK_Classification
: constant Boolean :=
331 Prag_Nam
in Name_Async_Readers
333 | Name_Effective_Reads
334 | Name_Effective_Writes
336 or else (Ekind
(Id
) = E_Task_Type
337 and Prag_Nam
in Name_Part_Of
340 or else (Ekind
(Id
) = E_Protected_Type
341 and Prag_Nam
= Name_Part_Of
);
344 if Is_OK_Classification
then
347 elsif Ekind
(Id
) = E_Subprogram_Type
348 and then Prag_Nam
in Name_Precondition
351 Add_Pre_Post_Condition
;
354 -- The pragma is not a proper contract item
356 raise Contract_Error
;
360 -- Subprogram bodies, the applicable pragmas are:
367 elsif Ekind
(Id
) = E_Subprogram_Body
then
368 if Prag_Nam
in Name_Refined_Depends | Name_Refined_Global
then
371 elsif Prag_Nam
in Name_Postcondition
375 Add_Pre_Post_Condition
;
377 -- The pragma is not a proper contract item
380 raise Contract_Error
;
383 -- Task bodies, the applicable pragmas are:
387 elsif Ekind
(Id
) = E_Task_Body
then
388 if Prag_Nam
in Name_Refined_Depends | Name_Refined_Global
then
391 -- The pragma is not a proper contract item
394 raise Contract_Error
;
397 -- Task units, the applicable pragmas are:
402 -- Variables, the applicable pragmas are:
405 -- Constant_After_Elaboration
413 elsif Ekind
(Id
) = E_Variable
then
414 if Prag_Nam
in Name_Async_Readers
416 | Name_Constant_After_Elaboration
418 | Name_Effective_Reads
419 | Name_Effective_Writes
426 -- The pragma is not a proper contract item
429 raise Contract_Error
;
433 raise Contract_Error
;
435 end Add_Contract_Item
;
437 -----------------------
438 -- Analyze_Contracts --
439 -----------------------
441 procedure Analyze_Contracts
(L
: List_Id
) is
446 while Present
(Decl
) loop
448 -- Entry or subprogram declarations
450 if Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
451 | N_Entry_Declaration
452 | N_Generic_Subprogram_Declaration
453 | N_Subprogram_Declaration
455 Analyze_Entry_Or_Subprogram_Contract
(Defining_Entity
(Decl
));
457 -- Entry or subprogram bodies
459 elsif Nkind
(Decl
) in N_Entry_Body | N_Subprogram_Body
then
460 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
464 elsif Nkind
(Decl
) = N_Object_Declaration
then
465 Analyze_Object_Contract
(Defining_Entity
(Decl
));
467 -- Package instantiation
469 elsif Nkind
(Decl
) = N_Package_Instantiation
then
470 Analyze_Package_Instantiation_Contract
(Defining_Entity
(Decl
));
474 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
475 | N_Single_Protected_Declaration
477 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
479 -- Subprogram body stubs
481 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
482 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
486 elsif Nkind
(Decl
) in N_Single_Task_Declaration
487 | N_Task_Type_Declaration
489 Analyze_Task_Contract
(Defining_Entity
(Decl
));
491 -- For type declarations, we need to do the preanalysis of Iterable
492 -- and the 3 Xxx_Literal aspect specifications.
494 -- Other type aspects need to be resolved here???
496 elsif Nkind
(Decl
) = N_Private_Type_Declaration
497 and then Present
(Aspect_Specifications
(Decl
))
500 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
501 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
502 I_Lit
: constant Node_Id
:=
503 Find_Aspect
(E
, Aspect_Integer_Literal
);
504 R_Lit
: constant Node_Id
:=
505 Find_Aspect
(E
, Aspect_Real_Literal
);
506 S_Lit
: constant Node_Id
:=
507 Find_Aspect
(E
, Aspect_String_Literal
);
511 Validate_Iterable_Aspect
(E
, It
);
514 if Present
(I_Lit
) then
515 Validate_Literal_Aspect
(E
, I_Lit
);
517 if Present
(R_Lit
) then
518 Validate_Literal_Aspect
(E
, R_Lit
);
520 if Present
(S_Lit
) then
521 Validate_Literal_Aspect
(E
, S_Lit
);
526 if Nkind
(Decl
) in N_Full_Type_Declaration
527 | N_Private_Type_Declaration
528 | N_Task_Type_Declaration
529 | N_Protected_Type_Declaration
530 | N_Formal_Type_Declaration
532 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
537 end Analyze_Contracts
;
539 -------------------------------------
540 -- Analyze_Pragmas_In_Declarations --
541 -------------------------------------
543 procedure Analyze_Pragmas_In_Declarations
(Body_Id
: Entity_Id
) is
547 -- Move through the body's declarations analyzing all pragmas which
548 -- appear at the top of the declarations.
550 Curr_Decl
:= First
(Declarations
(Unit_Declaration_Node
(Body_Id
)));
551 while Present
(Curr_Decl
) loop
553 if Nkind
(Curr_Decl
) = N_Pragma
then
555 if Pragma_Significant_To_Subprograms
556 (Get_Pragma_Id
(Curr_Decl
))
561 -- Skip the renamings of discriminants and protection fields
563 elsif Is_Prologue_Renaming
(Curr_Decl
) then
566 -- We have reached something which is not a pragma so we can be sure
567 -- there are no more contracts or pragmas which need to be taken into
576 end Analyze_Pragmas_In_Declarations
;
578 -----------------------------------------------
579 -- Analyze_Entry_Or_Subprogram_Body_Contract --
580 -----------------------------------------------
582 -- WARNING: This routine manages SPARK regions. Return statements must be
583 -- replaced by gotos which jump to the end of the routine and restore the
586 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
587 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
588 Items
: constant Node_Id
:= Contract
(Body_Id
);
589 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
591 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
592 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
593 -- Save the SPARK_Mode-related data to restore on exit
596 -- When a subprogram body declaration is illegal, its defining entity is
597 -- left unanalyzed. There is nothing left to do in this case because the
598 -- body lacks a contract, or even a proper Ekind.
600 if Ekind
(Body_Id
) = E_Void
then
603 -- Do not analyze a contract multiple times
605 elsif Present
(Items
) then
606 if Analyzed
(Items
) then
609 Set_Analyzed
(Items
);
612 -- When this is a subprogram body not coming from source, for example an
613 -- expression function, it does not cause freezing of previous contracts
614 -- (see Analyze_Subprogram_Body_Helper), in particular not of those on
615 -- its spec if it exists. In this case make sure they have been properly
616 -- analyzed before being expanded below, as we may be invoked during the
617 -- freezing of the subprogram in the middle of its enclosing declarative
618 -- part because the declarative part contains e.g. the declaration of a
619 -- variable initialized by means of a call to the subprogram.
621 elsif Nkind
(Body_Decl
) = N_Subprogram_Body
622 and then not Comes_From_Source
(Original_Node
(Body_Decl
))
623 and then Present
(Corresponding_Spec
(Body_Decl
))
624 and then Present
(Contract
(Corresponding_Spec
(Body_Decl
)))
626 Analyze_Entry_Or_Subprogram_Contract
(Corresponding_Spec
(Body_Decl
));
629 -- Due to the timing of contract analysis, delayed pragmas may be
630 -- subject to the wrong SPARK_Mode, usually that of the enclosing
631 -- context. To remedy this, restore the original SPARK_Mode of the
632 -- related subprogram body.
634 Set_SPARK_Mode
(Body_Id
);
636 -- Ensure that the contract cases or postconditions mention 'Result or
637 -- define a post-state.
639 Check_Result_And_Post_State
(Body_Id
);
641 -- A stand-alone nonvolatile function body cannot have an effectively
642 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
643 -- check is relevant only when SPARK_Mode is on, as it is not a standard
644 -- legality rule. The check is performed here because Volatile_Function
645 -- is processed after the analysis of the related subprogram body. The
646 -- check only applies to source subprograms and not to generated TSS
650 and then Ekind
(Body_Id
) in E_Function | E_Generic_Function
651 and then Comes_From_Source
(Spec_Id
)
652 and then not Is_Volatile_Function
(Body_Id
)
654 Check_Nonvolatile_Function_Profile
(Body_Id
);
657 -- Restore the SPARK_Mode of the enclosing context after all delayed
658 -- pragmas have been analyzed.
660 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
662 -- Capture all global references in a generic subprogram body now that
663 -- the contract has been analyzed.
665 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
666 Save_Global_References_In_Contract
667 (Templ
=> Original_Node
(Body_Decl
),
671 -- Deal with preconditions, [refined] postconditions, Always_Terminates,
672 -- Contract_Cases, Exceptional_Cases, Subprogram_Variant, invariants and
673 -- predicates associated with body and its spec. Do not expand the
674 -- contract of subprogram body stubs.
676 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
677 Expand_Subprogram_Contract
(Body_Id
);
679 end Analyze_Entry_Or_Subprogram_Body_Contract
;
681 ------------------------------------------
682 -- Analyze_Entry_Or_Subprogram_Contract --
683 ------------------------------------------
685 -- WARNING: This routine manages SPARK regions. Return statements must be
686 -- replaced by gotos which jump to the end of the routine and restore the
689 procedure Analyze_Entry_Or_Subprogram_Contract
690 (Subp_Id
: Entity_Id
;
691 Freeze_Id
: Entity_Id
:= Empty
)
693 Items
: constant Node_Id
:= Contract
(Subp_Id
);
694 Subp_Decl
: constant Node_Id
:=
695 (if Ekind
(Subp_Id
) = E_Subprogram_Type
696 then Associated_Node_For_Itype
(Subp_Id
)
697 else Unit_Declaration_Node
(Subp_Id
));
699 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
700 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
701 -- Save the SPARK_Mode-related data to restore on exit
703 Skip_Assert_Exprs
: constant Boolean :=
704 Is_Entry
(Subp_Id
) and then not GNATprove_Mode
;
706 Depends
: Node_Id
:= Empty
;
707 Global
: Node_Id
:= Empty
;
712 -- Do not analyze a contract multiple times
714 if Present
(Items
) then
715 if Analyzed
(Items
) then
718 Set_Analyzed
(Items
);
722 -- Due to the timing of contract analysis, delayed pragmas may be
723 -- subject to the wrong SPARK_Mode, usually that of the enclosing
724 -- context. To remedy this, restore the original SPARK_Mode of the
725 -- related subprogram body.
727 Set_SPARK_Mode
(Subp_Id
);
729 -- All subprograms carry a contract, but for some it is not significant
730 -- and should not be processed.
732 if not Has_Significant_Contract
(Subp_Id
) then
735 elsif Present
(Items
) then
737 -- Do not analyze the pre/postconditions of an entry declaration
738 -- unless annotating the original tree for GNATprove. The
739 -- real analysis occurs when the pre/postconditons are relocated to
740 -- the contract wrapper procedure (see Build_Contract_Wrapper).
742 if Skip_Assert_Exprs
then
745 -- Otherwise analyze the pre/postconditions.
746 -- If these come from an aspect specification, their expressions
747 -- might include references to types that are not frozen yet, in the
748 -- case where the body is a rewritten expression function that is a
749 -- completion, so freeze all types within before constructing the
754 Bod
: Node_Id
:= Empty
;
755 Freeze_Types
: Boolean := False;
758 if Present
(Freeze_Id
) then
759 Bod
:= Unit_Declaration_Node
(Freeze_Id
);
761 if Nkind
(Bod
) = N_Subprogram_Body
762 and then Was_Expression_Function
(Bod
)
763 and then Ekind
(Subp_Id
) = E_Function
764 and then Chars
(Subp_Id
) = Chars
(Freeze_Id
)
765 and then Subp_Id
/= Freeze_Id
767 Freeze_Types
:= True;
771 Prag
:= Pre_Post_Conditions
(Items
);
772 while Present
(Prag
) loop
774 and then Present
(Corresponding_Aspect
(Prag
))
778 Typ
=> Standard_Boolean
,
781 (First
(Pragma_Argument_Associations
(Prag
))),
785 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
786 Prag
:= Next_Pragma
(Prag
);
791 -- Analyze contract-cases, subprogram-variant and test-cases
793 Prag
:= Contract_Test_Cases
(Items
);
794 while Present
(Prag
) loop
795 Prag_Nam
:= Pragma_Name
(Prag
);
797 if Prag_Nam
= Name_Always_Terminates
then
798 Analyze_Always_Terminates_In_Decl_Part
(Prag
);
800 elsif Prag_Nam
= Name_Contract_Cases
then
802 -- Do not analyze the contract cases of an entry declaration
803 -- unless annotating the original tree for GNATprove.
804 -- The real analysis occurs when the contract cases are moved
805 -- to the contract wrapper procedure (Build_Contract_Wrapper).
807 if Skip_Assert_Exprs
then
810 -- Otherwise analyze the contract cases
813 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
816 elsif Prag_Nam
= Name_Exceptional_Cases
then
817 Analyze_Exceptional_Cases_In_Decl_Part
(Prag
);
819 elsif Prag_Nam
= Name_Subprogram_Variant
then
820 Analyze_Subprogram_Variant_In_Decl_Part
(Prag
);
823 pragma Assert
(Prag_Nam
= Name_Test_Case
);
824 Analyze_Test_Case_In_Decl_Part
(Prag
);
827 Prag
:= Next_Pragma
(Prag
);
830 -- Analyze classification pragmas
832 Prag
:= Classifications
(Items
);
833 while Present
(Prag
) loop
834 Prag_Nam
:= Pragma_Name
(Prag
);
836 if Prag_Nam
= Name_Depends
then
839 elsif Prag_Nam
= Name_Global
then
843 Prag
:= Next_Pragma
(Prag
);
846 -- Analyze Global first, as Depends may mention items classified in
847 -- the global categorization.
849 if Present
(Global
) then
850 Analyze_Global_In_Decl_Part
(Global
);
853 -- Depends must be analyzed after Global in order to see the modes of
856 if Present
(Depends
) then
857 Analyze_Depends_In_Decl_Part
(Depends
);
860 -- Ensure that the contract cases or postconditions mention 'Result
861 -- or define a post-state.
863 Check_Result_And_Post_State
(Subp_Id
);
866 -- A nonvolatile function cannot have an effectively volatile formal
867 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
868 -- only when SPARK_Mode is on, as it is not a standard legality rule.
869 -- The check is performed here because pragma Volatile_Function is
870 -- processed after the analysis of the related subprogram declaration.
873 and then Ekind
(Subp_Id
) in E_Function | E_Generic_Function
874 and then Comes_From_Source
(Subp_Id
)
875 and then not Is_Volatile_Function
(Subp_Id
)
877 Check_Nonvolatile_Function_Profile
(Subp_Id
);
880 -- Restore the SPARK_Mode of the enclosing context after all delayed
881 -- pragmas have been analyzed.
883 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
885 -- Capture all global references in a generic subprogram now that the
886 -- contract has been analyzed.
888 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
889 Save_Global_References_In_Contract
890 (Templ
=> Original_Node
(Subp_Decl
),
893 end Analyze_Entry_Or_Subprogram_Contract
;
895 ----------------------------------------------
896 -- Check_Type_Or_Object_External_Properties --
897 ----------------------------------------------
899 procedure Check_Type_Or_Object_External_Properties
900 (Type_Or_Obj_Id
: Entity_Id
)
902 Is_Type_Id
: constant Boolean := Is_Type
(Type_Or_Obj_Id
);
903 Decl_Kind
: constant String :=
904 (if Is_Type_Id
then "type" else "object");
908 AR_Val
: Boolean := False;
909 AW_Val
: Boolean := False;
910 ER_Val
: Boolean := False;
911 EW_Val
: Boolean := False;
913 Seen
: Boolean := False;
917 -- Start of processing for Check_Type_Or_Object_External_Properties
920 -- Analyze all external properties
923 Obj_Typ
:= Type_Or_Obj_Id
;
925 -- If the parent type of a derived type is volatile
926 -- then the derived type inherits volatility-related flags.
928 if Is_Derived_Type
(Type_Or_Obj_Id
) then
930 Parent_Type
: constant Entity_Id
:=
931 Etype
(Base_Type
(Type_Or_Obj_Id
));
933 if Is_Effectively_Volatile
(Parent_Type
) then
934 AR_Val
:= Async_Readers_Enabled
(Parent_Type
);
935 AW_Val
:= Async_Writers_Enabled
(Parent_Type
);
936 ER_Val
:= Effective_Reads_Enabled
(Parent_Type
);
937 EW_Val
:= Effective_Writes_Enabled
(Parent_Type
);
942 Obj_Typ
:= Etype
(Type_Or_Obj_Id
);
945 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Readers
);
947 if Present
(Prag
) then
949 Saved_AR_Val
: constant Boolean := AR_Val
;
951 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
953 if Saved_AR_Val
and not AR_Val
then
955 ("illegal non-confirming Async_Readers specification",
961 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Writers
);
963 if Present
(Prag
) then
965 Saved_AW_Val
: constant Boolean := AW_Val
;
967 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
969 if Saved_AW_Val
and not AW_Val
then
971 ("illegal non-confirming Async_Writers specification",
977 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Reads
);
979 if Present
(Prag
) then
981 Saved_ER_Val
: constant Boolean := ER_Val
;
983 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
985 if Saved_ER_Val
and not ER_Val
then
987 ("illegal non-confirming Effective_Reads specification",
993 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Writes
);
995 if Present
(Prag
) then
997 Saved_EW_Val
: constant Boolean := EW_Val
;
999 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
1001 if Saved_EW_Val
and not EW_Val
then
1003 ("illegal non-confirming Effective_Writes specification",
1009 -- Verify the mutual interaction of the various external properties.
1010 -- For types and variables for which No_Caching is enabled, it has been
1011 -- checked already that only False values for other external properties
1015 and then not No_Caching_Enabled
(Type_Or_Obj_Id
)
1017 Check_External_Properties
1018 (Type_Or_Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
1021 -- Analyze the non-external volatility property No_Caching
1023 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_No_Caching
);
1025 if Present
(Prag
) then
1026 Analyze_External_Property_In_Decl_Part
(Prag
, NC_Val
);
1029 -- The following checks are relevant only when SPARK_Mode is on, as
1030 -- they are not standard Ada legality rules. Internally generated
1031 -- temporaries are ignored, as well as return objects.
1034 and then Comes_From_Source
(Type_Or_Obj_Id
)
1035 and then not Is_Return_Object
(Type_Or_Obj_Id
)
1037 if Is_Effectively_Volatile
(Type_Or_Obj_Id
) then
1039 -- The declaration of an effectively volatile object or type must
1040 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
1042 if not Is_Library_Level_Entity
(Type_Or_Obj_Id
) then
1043 Error_Msg_Code
:= GEC_Volatile_At_Library_Level
;
1045 ("effectively volatile "
1047 & " & must be declared at library level '[[]']",
1050 -- An object of a discriminated type cannot be effectively
1051 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
1053 elsif Has_Discriminants
(Obj_Typ
)
1054 and then not Is_Protected_Type
(Obj_Typ
)
1057 ("discriminated " & Decl_Kind
& " & cannot be volatile",
1061 -- An object decl shall be compatible with respect to volatility
1062 -- with its type (SPARK RM 7.1.3(2)).
1064 if not Is_Type_Id
then
1065 if Is_Effectively_Volatile
(Obj_Typ
) then
1066 Check_Volatility_Compatibility
1067 (Type_Or_Obj_Id
, Obj_Typ
,
1068 "volatile object", "its type",
1069 Srcpos_Bearer
=> Type_Or_Obj_Id
);
1072 -- A component of a composite type (in this case, the composite
1073 -- type is an array type) shall be compatible with respect to
1074 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1076 elsif Is_Array_Type
(Obj_Typ
) then
1077 Check_Volatility_Compatibility
1078 (Component_Type
(Obj_Typ
), Obj_Typ
,
1079 "component type", "its enclosing array type",
1080 Srcpos_Bearer
=> Obj_Typ
);
1082 -- A component of a composite type (in this case, the composite
1083 -- type is a record type) shall be compatible with respect to
1084 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1086 elsif Is_Record_Type
(Obj_Typ
) then
1088 Comp
: Entity_Id
:= First_Component
(Obj_Typ
);
1090 while Present
(Comp
) loop
1091 Check_Volatility_Compatibility
1092 (Etype
(Comp
), Obj_Typ
,
1093 "record component " & Get_Name_String
(Chars
(Comp
)),
1094 "its enclosing record type",
1095 Srcpos_Bearer
=> Comp
);
1096 Next_Component
(Comp
);
1101 -- The type or object is not effectively volatile
1104 -- A non-effectively volatile type cannot have effectively
1105 -- volatile components (SPARK RM 7.1.3(6)).
1108 and then not Is_Effectively_Volatile
(Type_Or_Obj_Id
)
1109 and then Has_Effectively_Volatile_Component
(Type_Or_Obj_Id
)
1112 ("non-volatile type & cannot have effectively volatile"
1118 end Check_Type_Or_Object_External_Properties
;
1120 -----------------------------
1121 -- Analyze_Object_Contract --
1122 -----------------------------
1124 -- WARNING: This routine manages SPARK regions. Return statements must be
1125 -- replaced by gotos which jump to the end of the routine and restore the
1128 procedure Analyze_Object_Contract
1129 (Obj_Id
: Entity_Id
;
1130 Freeze_Id
: Entity_Id
:= Empty
)
1132 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
1134 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1135 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1136 -- Save the SPARK_Mode-related data to restore on exit
1143 -- The loop parameter in an element iterator over a formal container
1144 -- is declared with an object declaration, but no contracts apply.
1146 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
1150 -- Do not analyze a contract multiple times
1152 Items
:= Contract
(Obj_Id
);
1154 if Present
(Items
) then
1155 if Analyzed
(Items
) then
1158 Set_Analyzed
(Items
);
1162 -- The anonymous object created for a single concurrent type inherits
1163 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
1164 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
1165 -- of the enclosing context. To remedy this, restore the original mode
1166 -- of the related anonymous object.
1168 if Is_Single_Concurrent_Object
(Obj_Id
)
1169 and then Present
(SPARK_Pragma
(Obj_Id
))
1171 Set_SPARK_Mode
(Obj_Id
);
1174 -- Checks related to external properties, same for constants and
1177 Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id
=> Obj_Id
);
1179 -- Constant-related checks
1181 if Ekind
(Obj_Id
) = E_Constant
then
1183 -- Analyze indicator Part_Of
1185 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1187 -- Check whether the lack of indicator Part_Of agrees with the
1188 -- placement of the constant with respect to the state space.
1191 Check_Missing_Part_Of
(Obj_Id
);
1194 -- Variable-related checks
1196 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
1198 -- The anonymous object created for a single task type carries
1199 -- pragmas Depends and Global of the type.
1201 if Is_Single_Task_Object
(Obj_Id
) then
1203 -- Analyze Global first, as Depends may mention items classified
1204 -- in the global categorization.
1206 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
1208 if Present
(Prag
) then
1209 Analyze_Global_In_Decl_Part
(Prag
);
1212 -- Depends must be analyzed after Global in order to see the modes
1213 -- of all global items.
1215 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
1217 if Present
(Prag
) then
1218 Analyze_Depends_In_Decl_Part
(Prag
);
1222 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1224 -- Analyze indicator Part_Of
1226 if Present
(Prag
) then
1227 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
1229 -- The variable is a constituent of a single protected/task type
1230 -- and behaves as a component of the type. Verify that references
1231 -- to the variable occur within the definition or body of the type
1234 if Present
(Encapsulating_State
(Obj_Id
))
1235 and then Is_Single_Concurrent_Object
1236 (Encapsulating_State
(Obj_Id
))
1237 and then Present
(Part_Of_References
(Obj_Id
))
1239 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
1240 while Present
(Ref_Elmt
) loop
1241 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
1242 Next_Elmt
(Ref_Elmt
);
1246 -- Otherwise check whether the lack of indicator Part_Of agrees with
1247 -- the placement of the variable with respect to the state space.
1250 Check_Missing_Part_Of
(Obj_Id
);
1256 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
1258 -- A Ghost object cannot be of a type that yields a synchronized
1259 -- object (SPARK RM 6.9(19)).
1261 if Yields_Synchronized_Object
(Obj_Typ
) then
1262 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
1264 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
1265 -- SPARK RM 6.9(19)).
1267 elsif SPARK_Mode
= On
and then Is_Effectively_Volatile
(Obj_Id
) then
1268 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
1270 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
1271 -- One exception to this is the object that represents the dispatch
1272 -- table of a Ghost tagged type, as the symbol needs to be exported.
1274 elsif Is_Exported
(Obj_Id
) then
1275 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
1277 elsif Is_Imported
(Obj_Id
) then
1278 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
1282 -- Restore the SPARK_Mode of the enclosing context after all delayed
1283 -- pragmas have been analyzed.
1285 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1286 end Analyze_Object_Contract
;
1288 -----------------------------------
1289 -- Analyze_Package_Body_Contract --
1290 -----------------------------------
1292 -- WARNING: This routine manages SPARK regions. Return statements must be
1293 -- replaced by gotos which jump to the end of the routine and restore the
1296 procedure Analyze_Package_Body_Contract
1297 (Body_Id
: Entity_Id
;
1298 Freeze_Id
: Entity_Id
:= Empty
)
1300 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1301 Items
: constant Node_Id
:= Contract
(Body_Id
);
1302 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
1304 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1305 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1306 -- Save the SPARK_Mode-related data to restore on exit
1308 Ref_State
: Node_Id
;
1311 -- Do not analyze a contract multiple times
1313 if Present
(Items
) then
1314 if Analyzed
(Items
) then
1317 Set_Analyzed
(Items
);
1321 -- Due to the timing of contract analysis, delayed pragmas may be
1322 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1323 -- context. To remedy this, restore the original SPARK_Mode of the
1324 -- related package body.
1326 Set_SPARK_Mode
(Body_Id
);
1328 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
1330 -- The analysis of pragma Refined_State detects whether the spec has
1331 -- abstract states available for refinement.
1333 if Present
(Ref_State
) then
1334 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
1337 -- Restore the SPARK_Mode of the enclosing context after all delayed
1338 -- pragmas have been analyzed.
1340 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1342 -- Capture all global references in a generic package body now that the
1343 -- contract has been analyzed.
1345 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1346 Save_Global_References_In_Contract
1347 (Templ
=> Original_Node
(Body_Decl
),
1350 end Analyze_Package_Body_Contract
;
1352 ------------------------------
1353 -- Analyze_Package_Contract --
1354 ------------------------------
1356 -- WARNING: This routine manages SPARK regions. Return statements must be
1357 -- replaced by gotos which jump to the end of the routine and restore the
1360 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1361 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1362 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1364 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1365 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1366 -- Save the SPARK_Mode-related data to restore on exit
1368 Init
: Node_Id
:= Empty
;
1369 Init_Cond
: Node_Id
:= Empty
;
1374 -- Do not analyze a contract multiple times
1376 if Present
(Items
) then
1377 if Analyzed
(Items
) then
1380 -- Do not analyze the contract of the internal package
1381 -- created to check conformance of an actual package.
1382 -- Such an internal package is removed from the tree after
1383 -- legality checks are completed, and it does not contain
1384 -- the declarations of all local entities of the generic.
1386 elsif Is_Internal
(Pack_Id
)
1387 and then Is_Generic_Instance
(Pack_Id
)
1392 Set_Analyzed
(Items
);
1396 -- Due to the timing of contract analysis, delayed pragmas may be
1397 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1398 -- context. To remedy this, restore the original SPARK_Mode of the
1401 Set_SPARK_Mode
(Pack_Id
);
1403 if Present
(Items
) then
1405 -- Locate and store pragmas Initial_Condition and Initializes, since
1406 -- their order of analysis matters.
1408 Prag
:= Classifications
(Items
);
1409 while Present
(Prag
) loop
1410 Prag_Nam
:= Pragma_Name
(Prag
);
1412 if Prag_Nam
= Name_Initial_Condition
then
1415 elsif Prag_Nam
= Name_Initializes
then
1419 Prag
:= Next_Pragma
(Prag
);
1422 -- Analyze the initialization-related pragmas. Initializes must come
1423 -- before Initial_Condition due to item dependencies.
1425 if Present
(Init
) then
1426 Analyze_Initializes_In_Decl_Part
(Init
);
1429 if Present
(Init_Cond
) then
1430 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1434 -- Restore the SPARK_Mode of the enclosing context after all delayed
1435 -- pragmas have been analyzed.
1437 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1439 -- Capture all global references in a generic package now that the
1440 -- contract has been analyzed.
1442 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1443 Save_Global_References_In_Contract
1444 (Templ
=> Original_Node
(Pack_Decl
),
1447 end Analyze_Package_Contract
;
1449 --------------------------------------------
1450 -- Analyze_Package_Instantiation_Contract --
1451 --------------------------------------------
1453 -- WARNING: This routine manages SPARK regions. Return statements must be
1454 -- replaced by gotos which jump to the end of the routine and restore the
1457 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
) is
1458 Inst_Spec
: constant Node_Id
:=
1459 Instance_Spec
(Unit_Declaration_Node
(Inst_Id
));
1461 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1462 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1463 -- Save the SPARK_Mode-related data to restore on exit
1465 Pack_Id
: Entity_Id
;
1469 -- Nothing to do when the package instantiation is erroneous or left
1470 -- partially decorated.
1472 if No
(Inst_Spec
) then
1476 Pack_Id
:= Defining_Entity
(Inst_Spec
);
1477 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1479 -- Due to the timing of contract analysis, delayed pragmas may be
1480 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1481 -- context. To remedy this, restore the original SPARK_Mode of the
1484 Set_SPARK_Mode
(Pack_Id
);
1486 -- Check whether the lack of indicator Part_Of agrees with the placement
1487 -- of the package instantiation with respect to the state space. Nested
1488 -- package instantiations do not need to be checked because they inherit
1489 -- Part_Of indicator of the outermost package instantiation (see routine
1490 -- Propagate_Part_Of in Sem_Prag).
1495 elsif No
(Prag
) then
1496 Check_Missing_Part_Of
(Pack_Id
);
1499 -- Restore the SPARK_Mode of the enclosing context after all delayed
1500 -- pragmas have been analyzed.
1502 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1503 end Analyze_Package_Instantiation_Contract
;
1505 --------------------------------
1506 -- Analyze_Protected_Contract --
1507 --------------------------------
1509 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1510 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1513 -- Do not analyze a contract multiple times
1515 if Present
(Items
) then
1516 if Analyzed
(Items
) then
1519 Set_Analyzed
(Items
);
1522 end Analyze_Protected_Contract
;
1524 -------------------------------------------
1525 -- Analyze_Subprogram_Body_Stub_Contract --
1526 -------------------------------------------
1528 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1529 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1530 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1533 -- A subprogram body stub may act as its own spec or as the completion
1534 -- of a previous declaration. Depending on the context, the contract of
1535 -- the stub may contain two sets of pragmas.
1537 -- The stub is a completion, the applicable pragmas are:
1541 if Present
(Spec_Id
) then
1542 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1544 -- The stub acts as its own spec, the applicable pragmas are:
1545 -- Always_Terminates
1548 -- Exceptional_Cases
1552 -- Subprogram_Variant
1556 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1558 end Analyze_Subprogram_Body_Stub_Contract
;
1560 ---------------------------
1561 -- Analyze_Task_Contract --
1562 ---------------------------
1564 -- WARNING: This routine manages SPARK regions. Return statements must be
1565 -- replaced by gotos which jump to the end of the routine and restore the
1568 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1569 Items
: constant Node_Id
:= Contract
(Task_Id
);
1571 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1572 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1573 -- Save the SPARK_Mode-related data to restore on exit
1578 -- Do not analyze a contract multiple times
1580 if Present
(Items
) then
1581 if Analyzed
(Items
) then
1584 Set_Analyzed
(Items
);
1588 -- Due to the timing of contract analysis, delayed pragmas may be
1589 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1590 -- context. To remedy this, restore the original SPARK_Mode of the
1591 -- related task unit.
1593 Set_SPARK_Mode
(Task_Id
);
1595 -- Analyze Global first, as Depends may mention items classified in the
1596 -- global categorization.
1598 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1600 if Present
(Prag
) then
1601 Analyze_Global_In_Decl_Part
(Prag
);
1604 -- Depends must be analyzed after Global in order to see the modes of
1605 -- all global items.
1607 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1609 if Present
(Prag
) then
1610 Analyze_Depends_In_Decl_Part
(Prag
);
1613 -- Restore the SPARK_Mode of the enclosing context after all delayed
1614 -- pragmas have been analyzed.
1616 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1617 end Analyze_Task_Contract
;
1619 ---------------------------
1620 -- Analyze_Type_Contract --
1621 ---------------------------
1623 procedure Analyze_Type_Contract
(Type_Id
: Entity_Id
) is
1625 Check_Type_Or_Object_External_Properties
1626 (Type_Or_Obj_Id
=> Type_Id
);
1628 -- Analyze Pre/Post on access-to-subprogram type
1630 if Ekind
(Type_Id
) in Access_Subprogram_Kind
then
1631 Analyze_Entry_Or_Subprogram_Contract
1632 (Directly_Designated_Type
(Type_Id
));
1634 end Analyze_Type_Contract
;
1636 ---------------------------------------
1637 -- Build_Subprogram_Contract_Wrapper --
1638 ---------------------------------------
1640 procedure Build_Subprogram_Contract_Wrapper
1641 (Body_Id
: Entity_Id
;
1646 Body_Decl
: constant Entity_Id
:= Unit_Declaration_Node
(Body_Id
);
1647 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
1648 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1649 Subp_Id
: Entity_Id
;
1650 Ret_Type
: Entity_Id
;
1652 Wrapper_Id
: Entity_Id
;
1653 Wrapper_Body
: Node_Id
;
1654 Wrapper_Spec
: Node_Id
;
1657 -- When there are no postcondition statements we do not need to
1658 -- generate a wrapper.
1664 -- Obtain the related subprogram id from the body id.
1666 if Present
(Spec_Id
) then
1671 Ret_Type
:= Etype
(Subp_Id
);
1673 -- Generate the contracts wrapper by moving the original declarations
1674 -- and statements within a local subprogram, calling it and possibly
1675 -- preserving the result for the purpose of evaluating postconditions,
1676 -- contracts, type invariants, etc.
1678 -- In the case of a function, generate:
1680 -- function Original_Func (X : in out Integer) return Typ is
1681 -- <prologue renamings>
1684 -- function _Wrapped_Statements return Typ is
1685 -- <original declarations>
1687 -- <original statements>
1692 -- Result_Obj : constant Typ := _Wrapped_Statements
1694 -- <postconditions statements>
1698 -- Or else, in the case of a procedure, generate:
1700 -- procedure Original_Proc (X : in out Integer) is
1701 -- <prologue renamings>
1704 -- procedure _Wrapped_Statements is
1705 -- <original declarations>
1707 -- <original statements>
1711 -- _Wrapped_Statements;
1712 -- <postconditions statements>
1715 -- Create Identifier
1717 Wrapper_Id
:= Make_Defining_Identifier
(Loc
, Name_uWrapped_Statements
);
1718 Set_Debug_Info_Needed
(Wrapper_Id
);
1719 Set_Wrapped_Statements
(Subp_Id
, Wrapper_Id
);
1721 Set_Has_Pragma_Inline
(Wrapper_Id
, Has_Pragma_Inline
(Subp_Id
));
1722 Set_Has_Pragma_Inline_Always
1723 (Wrapper_Id
, Has_Pragma_Inline_Always
(Subp_Id
));
1725 -- Create specification and declaration for the wrapper
1727 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1729 Make_Procedure_Specification
(Loc
,
1730 Defining_Unit_Name
=> Wrapper_Id
);
1733 Make_Function_Specification
(Loc
,
1734 Defining_Unit_Name
=> Wrapper_Id
,
1735 Result_Definition
=> New_Occurrence_Of
(Ret_Type
, Loc
));
1738 -- Create the wrapper body using Body_Id's statements and declarations
1741 Make_Subprogram_Body
(Loc
,
1742 Specification
=> Wrapper_Spec
,
1743 Declarations
=> Declarations
(Body_Decl
),
1744 Handled_Statement_Sequence
=>
1745 Relocate_Node
(Handled_Statement_Sequence
(Body_Decl
)));
1747 Append_To
(Decls
, Wrapper_Body
);
1748 Set_Declarations
(Body_Decl
, Decls
);
1749 Set_Handled_Statement_Sequence
(Body_Decl
,
1750 Make_Handled_Sequence_Of_Statements
(Loc
,
1751 End_Label
=> Make_Identifier
(Loc
, Chars
(Wrapper_Id
))));
1753 -- Prepend a call to the wrapper when the subprogram is a procedure
1755 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1757 Make_Procedure_Call_Statement
(Loc
,
1758 Name
=> New_Occurrence_Of
(Wrapper_Id
, Loc
)));
1760 (Handled_Statement_Sequence
(Body_Decl
), Stmts
);
1762 -- Generate the post-execution statements and the extended return
1763 -- when the subprogram being wrapped is a function.
1766 Set_Statements
(Handled_Statement_Sequence
(Body_Decl
), New_List
(
1767 Make_Extended_Return_Statement
(Loc
,
1768 Return_Object_Declarations
=> New_List
(
1769 Make_Object_Declaration
(Loc
,
1770 Defining_Identifier
=> Result
,
1771 Constant_Present
=> True,
1772 Object_Definition
=>
1773 New_Occurrence_Of
(Ret_Type
, Loc
),
1775 Make_Function_Call
(Loc
,
1777 New_Occurrence_Of
(Wrapper_Id
, Loc
)))),
1778 Handled_Statement_Sequence
=>
1779 Make_Handled_Sequence_Of_Statements
(Loc
,
1780 Statements
=> Stmts
))));
1782 end Build_Subprogram_Contract_Wrapper
;
1784 ----------------------------------
1785 -- Build_Entry_Contract_Wrapper --
1786 ----------------------------------
1788 procedure Build_Entry_Contract_Wrapper
(E
: Entity_Id
; Decl
: Node_Id
) is
1789 Conc_Typ
: constant Entity_Id
:= Scope
(E
);
1790 Loc
: constant Source_Ptr
:= Sloc
(E
);
1792 procedure Add_Discriminant_Renamings
1793 (Obj_Id
: Entity_Id
;
1795 -- Add renaming declarations for all discriminants of concurrent type
1796 -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
1797 -- represents the concurrent object.
1799 procedure Add_Matching_Formals
1801 Actuals
: in out List_Id
);
1802 -- Add formal parameters that match those of entry E to list Formals.
1803 -- The routine also adds matching actuals for the new formals to list
1806 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
);
1807 -- Relocate pragma Prag to list To. The routine creates a new list if
1808 -- To does not exist.
1810 --------------------------------
1811 -- Add_Discriminant_Renamings --
1812 --------------------------------
1814 procedure Add_Discriminant_Renamings
1815 (Obj_Id
: Entity_Id
;
1819 Renaming_Decl
: Node_Id
;
1822 -- Inspect the discriminants of the concurrent type and generate a
1823 -- renaming for each one.
1825 if Has_Discriminants
(Conc_Typ
) then
1826 Discr
:= First_Discriminant
(Conc_Typ
);
1827 while Present
(Discr
) loop
1829 Make_Object_Renaming_Declaration
(Loc
,
1830 Defining_Identifier
=>
1831 Make_Defining_Identifier
(Loc
, Chars
(Discr
)),
1833 New_Occurrence_Of
(Etype
(Discr
), Loc
),
1835 Make_Selected_Component
(Loc
,
1836 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
1838 Make_Identifier
(Loc
, Chars
(Discr
))));
1840 Prepend_To
(Decls
, Renaming_Decl
);
1842 Next_Discriminant
(Discr
);
1845 end Add_Discriminant_Renamings
;
1847 --------------------------
1848 -- Add_Matching_Formals --
1849 --------------------------
1851 procedure Add_Matching_Formals
1853 Actuals
: in out List_Id
)
1856 New_Formal
: Entity_Id
;
1859 -- Inspect the formal parameters of the entry and generate a new
1860 -- matching formal with the same name for the wrapper. A reference
1861 -- to the new formal becomes an actual in the entry call.
1863 Formal
:= First_Formal
(E
);
1864 while Present
(Formal
) loop
1865 New_Formal
:= Make_Defining_Identifier
(Loc
, Chars
(Formal
));
1867 Make_Parameter_Specification
(Loc
,
1868 Defining_Identifier
=> New_Formal
,
1869 In_Present
=> In_Present
(Parent
(Formal
)),
1870 Out_Present
=> Out_Present
(Parent
(Formal
)),
1872 New_Occurrence_Of
(Etype
(Formal
), Loc
)));
1874 if No
(Actuals
) then
1875 Actuals
:= New_List
;
1878 Append_To
(Actuals
, New_Occurrence_Of
(New_Formal
, Loc
));
1879 Next_Formal
(Formal
);
1881 end Add_Matching_Formals
;
1883 ---------------------
1884 -- Transfer_Pragma --
1885 ---------------------
1887 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
) is
1895 New_Prag
:= Relocate_Node
(Prag
);
1897 Set_Analyzed
(New_Prag
, False);
1898 Append
(New_Prag
, To
);
1899 end Transfer_Pragma
;
1903 Items
: constant Node_Id
:= Contract
(E
);
1904 Actuals
: List_Id
:= No_List
;
1907 Decls
: List_Id
:= No_List
;
1909 Has_Pragma
: Boolean := False;
1910 Index_Id
: Entity_Id
;
1913 Wrapper_Id
: Entity_Id
;
1915 -- Start of processing for Build_Entry_Contract_Wrapper
1918 -- This routine generates a specialized wrapper for a protected or task
1919 -- entry [family] which implements precondition/postcondition semantics.
1920 -- Preconditions and case guards of contract cases are checked before
1921 -- the protected action or rendezvous takes place.
1923 -- procedure Wrapper
1924 -- (Obj_Id : Conc_Typ; -- concurrent object
1925 -- [Index : Index_Typ;] -- index of entry family
1926 -- [Formal_1 : ...; -- parameters of original entry
1929 -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
1930 -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
1932 -- <contracts pragmas>
1933 -- <case guard checks>
1936 -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
1939 -- Create the wrapper only when the entry has at least one executable
1940 -- contract item such as contract cases, precondition or postcondition.
1942 if Present
(Items
) then
1944 -- Inspect the list of pre/postconditions and transfer all available
1945 -- pragmas to the declarative list of the wrapper.
1947 Prag
:= Pre_Post_Conditions
(Items
);
1948 while Present
(Prag
) loop
1949 if Pragma_Name_Unmapped
(Prag
) in Name_Postcondition
1951 and then Is_Checked
(Prag
)
1954 Transfer_Pragma
(Prag
, To
=> Decls
);
1957 Prag
:= Next_Pragma
(Prag
);
1960 -- Inspect the list of test/contract cases and transfer only contract
1961 -- cases pragmas to the declarative part of the wrapper.
1963 Prag
:= Contract_Test_Cases
(Items
);
1964 while Present
(Prag
) loop
1965 if Pragma_Name
(Prag
) = Name_Contract_Cases
1966 and then Is_Checked
(Prag
)
1969 Transfer_Pragma
(Prag
, To
=> Decls
);
1972 Prag
:= Next_Pragma
(Prag
);
1976 -- The entry lacks executable contract items and a wrapper is not needed
1978 if not Has_Pragma
then
1982 -- Create the profile of the wrapper. The first formal parameter is the
1983 -- concurrent object.
1986 Make_Defining_Identifier
(Loc
,
1987 Chars
=> New_External_Name
(Chars
(Conc_Typ
), 'A'));
1989 Formals
:= New_List
(
1990 Make_Parameter_Specification
(Loc
,
1991 Defining_Identifier
=> Obj_Id
,
1992 Out_Present
=> True,
1994 Parameter_Type
=> New_Occurrence_Of
(Conc_Typ
, Loc
)));
1996 -- Construct the call to the original entry. The call will be gradually
1997 -- augmented with an optional entry index and extra parameters.
2000 Make_Selected_Component
(Loc
,
2001 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
2002 Selector_Name
=> New_Occurrence_Of
(E
, Loc
));
2004 -- When creating a wrapper for an entry family, the second formal is the
2007 if Ekind
(E
) = E_Entry_Family
then
2008 Index_Id
:= Make_Defining_Identifier
(Loc
, Name_I
);
2011 Make_Parameter_Specification
(Loc
,
2012 Defining_Identifier
=> Index_Id
,
2014 New_Occurrence_Of
(Entry_Index_Type
(E
), Loc
)));
2016 -- The call to the original entry becomes an indexed component to
2017 -- accommodate the entry index.
2020 Make_Indexed_Component
(Loc
,
2022 Expressions
=> New_List
(New_Occurrence_Of
(Index_Id
, Loc
)));
2025 -- Add formal parameters to match those of the entry and build actuals
2026 -- for the entry call.
2028 Add_Matching_Formals
(Formals
, Actuals
);
2031 Make_Procedure_Call_Statement
(Loc
,
2033 Parameter_Associations
=> Actuals
);
2035 -- Add renaming declarations for the discriminants of the enclosing type
2036 -- as the various contract items may reference them.
2038 Add_Discriminant_Renamings
(Obj_Id
, Decls
);
2041 Make_Defining_Identifier
(Loc
, New_External_Name
(Chars
(E
), 'E'));
2042 Set_Contract_Wrapper
(E
, Wrapper_Id
);
2043 Set_Is_Entry_Wrapper
(Wrapper_Id
);
2045 -- The wrapper body is analyzed when the enclosing type is frozen
2047 Append_Freeze_Action
(Defining_Entity
(Decl
),
2048 Make_Subprogram_Body
(Loc
,
2050 Make_Procedure_Specification
(Loc
,
2051 Defining_Unit_Name
=> Wrapper_Id
,
2052 Parameter_Specifications
=> Formals
),
2053 Declarations
=> Decls
,
2054 Handled_Statement_Sequence
=>
2055 Make_Handled_Sequence_Of_Statements
(Loc
,
2056 Statements
=> New_List
(Call
))));
2057 end Build_Entry_Contract_Wrapper
;
2059 ---------------------------
2060 -- Check_Class_Condition --
2061 ---------------------------
2063 procedure Check_Class_Condition
2066 Par_Subp
: Entity_Id
;
2067 Is_Precondition
: Boolean)
2069 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
2070 -- Check reference to formal of inherited operation or to primitive
2071 -- operation of root type.
2077 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
2082 if Nkind
(N
) = N_Identifier
2083 and then Present
(Entity
(N
))
2085 (Is_Formal
(Entity
(N
)) or else Is_Subprogram
(Entity
(N
)))
2087 (Nkind
(Parent
(N
)) /= N_Attribute_Reference
2088 or else Attribute_Name
(Parent
(N
)) /= Name_Class
)
2090 -- These checks do not apply to dispatching calls within the
2091 -- condition, but only to calls whose static tag is that of
2094 if Is_Subprogram
(Entity
(N
))
2095 and then Nkind
(Parent
(N
)) = N_Function_Call
2096 and then Present
(Controlling_Argument
(Parent
(N
)))
2101 -- Determine whether entity has a renaming
2103 Orig_E
:= Entity
(N
);
2104 New_E
:= Get_Mapped_Entity
(Orig_E
);
2106 if Present
(New_E
) then
2108 -- AI12-0166: A precondition for a protected operation
2109 -- cannot include an internal call to a protected function
2110 -- of the type. In the case of an inherited condition for an
2111 -- overriding operation, both the operation and the function
2112 -- are given by primitive wrappers.
2115 and then Ekind
(New_E
) = E_Function
2116 and then Is_Primitive_Wrapper
(New_E
)
2117 and then Is_Primitive_Wrapper
(Subp
)
2118 and then Scope
(Subp
) = Scope
(New_E
)
2120 Error_Msg_Node_2
:= Wrapped_Entity
(Subp
);
2122 ("internal call to& cannot appear in inherited "
2123 & "precondition of protected operation&",
2124 Subp
, Wrapped_Entity
(New_E
));
2128 -- Check that there are no calls left to abstract operations if
2129 -- the current subprogram is not abstract.
2132 and then Nkind
(Parent
(N
)) = N_Function_Call
2133 and then N
= Name
(Parent
(N
))
2135 if not Is_Abstract_Subprogram
(Subp
)
2136 and then Is_Abstract_Subprogram
(New_E
)
2138 Error_Msg_Sloc
:= Sloc
(Current_Scope
);
2139 Error_Msg_Node_2
:= Subp
;
2141 if Comes_From_Source
(Subp
) then
2143 ("cannot call abstract subprogram & in inherited "
2144 & "condition for&#", Subp
, New_E
);
2147 ("cannot call abstract subprogram & in inherited "
2148 & "condition for inherited&#", Subp
, New_E
);
2151 -- In SPARK mode, report error on inherited condition for an
2152 -- inherited operation if it contains a call to an overriding
2153 -- operation, because this implies that the pre/postconditions
2154 -- of the inherited operation have changed silently.
2156 elsif SPARK_Mode
= On
2157 and then Warn_On_Suspicious_Contract
2158 and then Present
(Alias
(Subp
))
2159 and then Present
(New_E
)
2160 and then Comes_From_Source
(New_E
)
2163 ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
2165 Error_Msg_Sloc
:= Sloc
(New_E
);
2166 Error_Msg_Node_2
:= Subp
;
2168 ("\overriding of&# forces overriding of&",
2169 Parent
(Subp
), New_E
);
2177 procedure Check_Condition_Entities
is
2178 new Traverse_Proc
(Check_Entity
);
2180 -- Start of processing for Check_Class_Condition
2183 -- No check required if the subprograms match
2185 if Par_Subp
= Subp
then
2189 Update_Primitives_Mapping
(Par_Subp
, Subp
);
2190 Map_Formals
(Par_Subp
, Subp
);
2191 Check_Condition_Entities
(Cond
);
2192 end Check_Class_Condition
;
2194 -----------------------------
2195 -- Create_Generic_Contract --
2196 -----------------------------
2198 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
2199 Templ
: constant Node_Id
:= Original_Node
(Unit
);
2200 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
2202 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
2203 -- Add a single contract-related source pragma Prag to the contract of
2204 -- generic template Templ_Id.
2206 ---------------------------------
2207 -- Add_Generic_Contract_Pragma --
2208 ---------------------------------
2210 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
2211 Prag_Templ
: Node_Id
;
2214 -- Mark the pragma to prevent the premature capture of global
2215 -- references when capturing global references of the context
2216 -- (see Save_References_In_Pragma).
2218 Set_Is_Generic_Contract_Pragma
(Prag
);
2220 -- Pragmas that apply to a generic subprogram declaration are not
2221 -- part of the semantic structure of the generic template:
2224 -- procedure Example (Formal : Integer);
2225 -- pragma Precondition (Formal > 0);
2227 -- Create a generic template for such pragmas and link the template
2228 -- of the pragma with the generic template.
2230 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2232 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
2233 Prag_Templ
:= Original_Node
(Prag
);
2235 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
2236 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
2238 -- Otherwise link the pragma with the generic template
2241 Add_Contract_Item
(Prag
, Templ_Id
);
2245 -- We do not stop the compilation at this point in the case of an
2246 -- invalid pragma because it will be properly diagnosed afterward.
2248 when Contract_Error
=> null;
2249 end Add_Generic_Contract_Pragma
;
2253 Context
: constant Node_Id
:= Parent
(Unit
);
2254 Decl
: Node_Id
:= Empty
;
2256 -- Start of processing for Create_Generic_Contract
2259 -- A generic package declaration carries contract-related source pragmas
2260 -- in its visible declarations.
2262 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
2263 Mutate_Ekind
(Templ_Id
, E_Generic_Package
);
2265 if Present
(Visible_Declarations
(Specification
(Templ
))) then
2266 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
2269 -- A generic package body carries contract-related source pragmas in its
2272 elsif Nkind
(Templ
) = N_Package_Body
then
2273 Mutate_Ekind
(Templ_Id
, E_Package_Body
);
2275 if Present
(Declarations
(Templ
)) then
2276 Decl
:= First
(Declarations
(Templ
));
2279 -- Generic subprogram declaration
2281 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2282 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
2283 Mutate_Ekind
(Templ_Id
, E_Generic_Function
);
2285 Mutate_Ekind
(Templ_Id
, E_Generic_Procedure
);
2288 -- When the generic subprogram acts as a compilation unit, inspect
2289 -- the Pragmas_After list for contract-related source pragmas.
2291 if Nkind
(Context
) = N_Compilation_Unit
then
2292 if Present
(Aux_Decls_Node
(Context
))
2293 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
2295 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
2298 -- Otherwise inspect the successive declarations for contract-related
2302 Decl
:= Next
(Unit
);
2305 -- A generic subprogram body carries contract-related source pragmas in
2306 -- its declarations.
2308 elsif Nkind
(Templ
) = N_Subprogram_Body
then
2309 Mutate_Ekind
(Templ_Id
, E_Subprogram_Body
);
2311 if Present
(Declarations
(Templ
)) then
2312 Decl
:= First
(Declarations
(Templ
));
2316 -- Inspect the relevant declarations looking for contract-related source
2317 -- pragmas and add them to the contract of the generic unit.
2319 while Present
(Decl
) loop
2320 if Comes_From_Source
(Decl
) then
2321 if Nkind
(Decl
) = N_Pragma
then
2323 -- The source pragma is a contract annotation
2325 if Is_Contract_Annotation
(Decl
) then
2326 Add_Generic_Contract_Pragma
(Decl
);
2329 -- The region where a contract-related source pragma may appear
2330 -- ends with the first source non-pragma declaration or statement.
2339 end Create_Generic_Contract
;
2341 --------------------------------
2342 -- Expand_Subprogram_Contract --
2343 --------------------------------
2345 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
2346 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
2347 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
2349 procedure Add_Invariant_And_Predicate_Checks
2350 (Subp_Id
: Entity_Id
;
2351 Stmts
: in out List_Id
;
2352 Result
: out Node_Id
);
2353 -- Process the result of function Subp_Id (if applicable) and all its
2354 -- formals. Add invariant and predicate checks where applicable. The
2355 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
2356 -- function, Result contains the entity of parameter _Result, to be
2357 -- used in the creation of procedure _Postconditions.
2359 procedure Add_Stable_Property_Contracts
2360 (Subp_Id
: Entity_Id
; Class_Present
: Boolean);
2361 -- Augment postcondition contracts to reflect Stable_Property aspect
2362 -- (if Class_Present = False) or Stable_Property'Class aspect (if
2363 -- Class_Present = True).
2365 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
2366 -- Append a node to a list. If there is no list, create a new one. When
2367 -- the item denotes a pragma, it is added to the list only when it is
2370 procedure Process_Contract_Cases
2371 (Stmts
: in out List_Id
;
2373 -- Process pragma Contract_Cases. This routine prepends items to the
2374 -- body declarations and appends items to list Stmts.
2376 procedure Process_Postconditions
(Stmts
: in out List_Id
);
2377 -- Collect all [inherited] spec and body postconditions and accumulate
2378 -- their pragma Check equivalents in list Stmts.
2380 procedure Process_Preconditions
(Decls
: in out List_Id
);
2381 -- Collect all [inherited] spec and body preconditions and prepend their
2382 -- pragma Check equivalents to the declarations of the body.
2384 ----------------------------------------
2385 -- Add_Invariant_And_Predicate_Checks --
2386 ----------------------------------------
2388 procedure Add_Invariant_And_Predicate_Checks
2389 (Subp_Id
: Entity_Id
;
2390 Stmts
: in out List_Id
;
2391 Result
: out Node_Id
)
2393 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
2394 -- Id denotes the return value of a function or a formal parameter.
2395 -- Add an invariant check if the type of Id is access to a type with
2396 -- invariants. The routine appends the generated code to Stmts.
2398 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
2399 -- Determine whether type Typ can benefit from invariant checks. To
2400 -- qualify, the type must have a non-null invariant procedure and
2401 -- subprogram Subp_Id must appear visible from the point of view of
2404 ---------------------------------
2405 -- Add_Invariant_Access_Checks --
2406 ---------------------------------
2408 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
2409 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2416 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
2417 Typ
:= Designated_Type
(Typ
);
2419 if Invariant_Checks_OK
(Typ
) then
2421 Make_Explicit_Dereference
(Loc
,
2422 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
2423 Set_Etype
(Ref
, Typ
);
2426 -- if <Id> /= null then
2427 -- <invariant_call (<Ref>)>
2432 Make_If_Statement
(Loc
,
2435 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
2436 Right_Opnd
=> Make_Null
(Loc
)),
2437 Then_Statements
=> New_List
(
2438 Make_Invariant_Call
(Ref
))),
2442 end Add_Invariant_Access_Checks
;
2444 -------------------------
2445 -- Invariant_Checks_OK --
2446 -------------------------
2448 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
2449 function Has_Public_Visibility_Of_Subprogram
return Boolean;
2450 -- Determine whether type Typ has public visibility of subprogram
2453 -----------------------------------------
2454 -- Has_Public_Visibility_Of_Subprogram --
2455 -----------------------------------------
2457 function Has_Public_Visibility_Of_Subprogram
return Boolean is
2458 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2461 -- An Initialization procedure must be considered visible even
2462 -- though it is internally generated.
2464 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2467 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2470 -- Internally generated code is never publicly visible except
2471 -- for a subprogram that is the implementation of an expression
2472 -- function. In that case the visibility is determined by the
2475 elsif not Comes_From_Source
(Subp_Decl
)
2477 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2479 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2483 -- Determine whether the subprogram is declared in the visible
2484 -- declarations of the package containing the type, or in the
2485 -- visible declaration of a child unit of that package.
2489 Decls
: constant List_Id
:=
2490 List_Containing
(Subp_Decl
);
2491 Subp_Scope
: constant Entity_Id
:=
2492 Scope
(Defining_Entity
(Subp_Decl
));
2493 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2497 Decls
= Visible_Declarations
2498 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2501 (Ekind
(Subp_Scope
) = E_Package
2502 and then Typ_Scope
/= Subp_Scope
2503 and then Is_Child_Unit
(Subp_Scope
)
2505 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2507 Decls
= Visible_Declarations
2509 (Unit_Declaration_Node
(Subp_Scope
))));
2512 end Has_Public_Visibility_Of_Subprogram
;
2514 -- Start of processing for Invariant_Checks_OK
2518 Has_Invariants
(Typ
)
2519 and then Present
(Invariant_Procedure
(Typ
))
2520 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2521 and then Has_Public_Visibility_Of_Subprogram
;
2522 end Invariant_Checks_OK
;
2526 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2527 -- Source location of subprogram body contract
2532 -- Start of processing for Add_Invariant_And_Predicate_Checks
2537 -- Process the result of a function
2539 if Ekind
(Subp_Id
) = E_Function
then
2540 Typ
:= Etype
(Subp_Id
);
2542 -- Generate _Result which is used in procedure _Postconditions to
2543 -- verify the return value.
2545 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2546 Set_Etype
(Result
, Typ
);
2548 -- Add an invariant check when the return type has invariants and
2549 -- the related function is visible to the outside.
2551 if Invariant_Checks_OK
(Typ
) then
2554 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2558 -- Add an invariant check when the return type is an access to a
2559 -- type with invariants.
2561 Add_Invariant_Access_Checks
(Result
);
2564 -- Add invariant checks for all formals that qualify (see AI05-0289
2567 Formal
:= First_Formal
(Subp_Id
);
2568 while Present
(Formal
) loop
2569 Typ
:= Etype
(Formal
);
2571 if Ekind
(Formal
) /= E_In_Parameter
2572 or else Ekind
(Subp_Id
) = E_Procedure
2573 or else Is_Access_Type
(Typ
)
2575 if Invariant_Checks_OK
(Typ
) then
2578 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2582 Add_Invariant_Access_Checks
(Formal
);
2584 -- Note: we used to add predicate checks for OUT and IN OUT
2585 -- formals here, but that was misguided, since such checks are
2586 -- performed on the caller side, based on the predicate of the
2587 -- actual, rather than the predicate of the formal.
2591 Next_Formal
(Formal
);
2593 end Add_Invariant_And_Predicate_Checks
;
2595 -----------------------------------
2596 -- Add_Stable_Property_Contracts --
2597 -----------------------------------
2599 procedure Add_Stable_Property_Contracts
2600 (Subp_Id
: Entity_Id
; Class_Present
: Boolean)
2602 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
2604 procedure Insert_Stable_Property_Check
2605 (Formal
: Entity_Id
; Property_Function
: Entity_Id
);
2606 -- Build the pragma for one check and insert it in the tree.
2608 function Make_Stable_Property_Condition
2609 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
;
2610 -- Builds tree for "Func (Formal) = Func (Formal)'Old" expression.
2612 function Stable_Properties
2613 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2614 return Subprogram_List
;
2615 -- If no aspect specified, then returns length-zero result.
2616 -- Negated indicates that reserved word NOT was specified.
2618 ----------------------------------
2619 -- Insert_Stable_Property_Check --
2620 ----------------------------------
2622 procedure Insert_Stable_Property_Check
2623 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) is
2625 Args
: constant List_Id
:=
2627 (Make_Pragma_Argument_Association
2630 Make_Stable_Property_Condition
2632 Property_Function
=> Property_Function
)),
2633 Make_Pragma_Argument_Association
2639 "failed stable property check at "
2640 & Build_Location_String
(Loc
)
2642 & To_String
(Fully_Qualified_Name_String
2643 (Formal
, Append_NUL
=> False))
2644 & " and property function "
2645 & To_String
(Fully_Qualified_Name_String
2646 (Property_Function
, Append_NUL
=> False))
2649 Prag
: constant Node_Id
:=
2651 Pragma_Identifier
=>
2652 Make_Identifier
(Loc
, Name_Postcondition
),
2653 Pragma_Argument_Associations
=> Args
,
2654 Class_Present
=> Class_Present
);
2656 Subp_Decl
: Node_Id
:= Subp_Id
;
2658 -- Enclosing_Declaration may return, for example,
2659 -- a N_Procedure_Specification node. Cope with this.
2661 Subp_Decl
:= Enclosing_Declaration
(Subp_Decl
);
2662 exit when Is_Declaration
(Subp_Decl
);
2663 Subp_Decl
:= Parent
(Subp_Decl
);
2664 pragma Assert
(Present
(Subp_Decl
));
2667 Insert_After_And_Analyze
(Subp_Decl
, Prag
);
2668 end Insert_Stable_Property_Check
;
2670 ------------------------------------
2671 -- Make_Stable_Property_Condition --
2672 ------------------------------------
2674 function Make_Stable_Property_Condition
2675 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
2677 function Call_Property_Function
return Node_Id
is
2681 New_Occurrence_Of
(Property_Function
, Loc
),
2682 Parameter_Associations
=>
2683 New_List
(New_Occurrence_Of
(Formal
, Loc
))));
2687 Call_Property_Function
,
2688 Make_Attribute_Reference
2690 Prefix
=> Call_Property_Function
,
2691 Attribute_Name
=> Name_Old
));
2692 end Make_Stable_Property_Condition
;
2694 -----------------------
2695 -- Stable_Properties --
2696 -----------------------
2698 function Stable_Properties
2699 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2700 return Subprogram_List
2702 Aspect_Spec
: Node_Id
:=
2703 Find_Value_Of_Aspect
2704 (Aspect_Bearer
, Aspect_Stable_Properties
,
2705 Class_Present
=> Class_Present
);
2707 -- ??? For a derived type, we wish Find_Value_Of_Aspect
2708 -- somehow knew that this aspect is not inherited.
2709 -- But it doesn't, so we cope with that here.
2711 -- There are probably issues here with inheritance from
2712 -- interface types, where just looking for the one parent type
2713 -- isn't enough. But this is far from the only work needed for
2714 -- Stable_Properties'Class for interface types.
2716 if Is_Derived_Type
(Aspect_Bearer
) then
2718 Parent_Type
: constant Entity_Id
:=
2719 Etype
(Base_Type
(Aspect_Bearer
));
2722 Find_Value_Of_Aspect
2723 (Parent_Type
, Aspect_Stable_Properties
,
2724 Class_Present
=> Class_Present
)
2726 -- prevent inheritance
2727 Aspect_Spec
:= Empty
;
2732 if No
(Aspect_Spec
) then
2733 Negated
:= Aspect_Bearer
= Subp_Id
;
2734 -- This is a little bit subtle.
2735 -- We need to assign True in the Subp_Id case in order to
2736 -- distinguish between no aspect spec at all vs. an
2737 -- explicitly specified "with S_P => []" empty list.
2738 -- In both cases Stable_Properties will return a length-0
2739 -- array, but the two cases are not equivalent.
2740 -- Very roughly speaking the lack of an S_P aspect spec for
2741 -- a subprogram would be equivalent to something like
2742 -- "with S_P => [not]", where we apply the "not" modifier to
2743 -- an empty set of subprograms, if such a construct existed.
2744 -- We could just assign True here, but it seems untidy to
2745 -- return True in the case of an aspect spec for a type
2746 -- (since negation is only allowed for subp S_P aspects).
2748 return (1 .. 0 => <>);
2750 return Parse_Aspect_Stable_Properties
2751 (Aspect_Spec
, Negated
=> Negated
);
2753 end Stable_Properties
;
2755 Formal
: Entity_Id
:= First_Formal
(Subp_Id
);
2756 Type_Of_Formal
: Entity_Id
;
2758 Subp_Properties_Negated
: Boolean;
2759 Subp_Properties
: constant Subprogram_List
:=
2760 Stable_Properties
(Subp_Id
, Subp_Properties_Negated
);
2762 -- start of processing for Add_Stable_Property_Contracts
2765 if not (Is_Primitive
(Subp_Id
) and then Comes_From_Source
(Subp_Id
))
2770 while Present
(Formal
) loop
2771 Type_Of_Formal
:= Base_Type
(Etype
(Formal
));
2773 if not Subp_Properties_Negated
then
2775 for SPF_Id
of Subp_Properties
loop
2776 if Type_Of_Formal
= Base_Type
(Etype
(First_Formal
(SPF_Id
)))
2777 and then Scope
(Type_Of_Formal
) = Scope
(Subp_Id
)
2779 -- ??? Need to filter out checks for SPFs that are
2780 -- mentioned explicitly in the postcondition of
2783 Insert_Stable_Property_Check
2784 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2788 elsif Scope
(Type_Of_Formal
) = Scope
(Subp_Id
) then
2790 Ignored
: Boolean range False .. False;
2792 Typ_Property_Funcs
: constant Subprogram_List
:=
2793 Stable_Properties
(Type_Of_Formal
, Negated
=> Ignored
);
2795 function Excluded_By_Aspect_Spec_Of_Subp
2796 (SPF_Id
: Entity_Id
) return Boolean;
2797 -- Examine Subp_Properties to determine whether SPF should
2800 -------------------------------------
2801 -- Excluded_By_Aspect_Spec_Of_Subp --
2802 -------------------------------------
2804 function Excluded_By_Aspect_Spec_Of_Subp
2805 (SPF_Id
: Entity_Id
) return Boolean is
2807 pragma Assert
(Subp_Properties_Negated
);
2808 -- Look through renames for equality test here ???
2809 return (for some F
of Subp_Properties
=> F
= SPF_Id
);
2810 end Excluded_By_Aspect_Spec_Of_Subp
;
2812 -- Look through renames for equality test here ???
2813 Subp_Is_Stable_Property_Function
: constant Boolean :=
2814 (for some F
of Typ_Property_Funcs
=> F
= Subp_Id
);
2816 if not Subp_Is_Stable_Property_Function
then
2817 for SPF_Id
of Typ_Property_Funcs
loop
2818 if not Excluded_By_Aspect_Spec_Of_Subp
(SPF_Id
) then
2819 -- ??? Need to filter out checks for SPFs that are
2820 -- mentioned explicitly in the postcondition of
2822 Insert_Stable_Property_Check
2823 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2829 Next_Formal
(Formal
);
2831 end Add_Stable_Property_Contracts
;
2833 -------------------------
2834 -- Append_Enabled_Item --
2835 -------------------------
2837 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2839 -- Do not chain ignored or disabled pragmas
2841 if Nkind
(Item
) = N_Pragma
2842 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2846 -- Otherwise, add the item
2853 -- If the pragma is a conjunct in a composite postcondition, it
2854 -- has been processed in reverse order. In the postcondition body
2855 -- it must appear before the others.
2857 if Nkind
(Item
) = N_Pragma
2858 and then From_Aspect_Specification
(Item
)
2859 and then Split_PPC
(Item
)
2861 Prepend
(Item
, List
);
2863 Append
(Item
, List
);
2866 end Append_Enabled_Item
;
2868 ----------------------------
2869 -- Process_Contract_Cases --
2870 ----------------------------
2872 procedure Process_Contract_Cases
2873 (Stmts
: in out List_Id
;
2876 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2877 -- Process pragma Contract_Cases for subprogram Subp_Id
2879 --------------------------------
2880 -- Process_Contract_Cases_For --
2881 --------------------------------
2883 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2884 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2888 if Present
(Items
) then
2889 Prag
:= Contract_Test_Cases
(Items
);
2890 while Present
(Prag
) loop
2891 if Is_Checked
(Prag
) then
2892 if Pragma_Name
(Prag
) = Name_Always_Terminates
then
2893 Expand_Pragma_Always_Terminates
(Prag
);
2895 elsif Pragma_Name
(Prag
) = Name_Contract_Cases
then
2896 Expand_Pragma_Contract_Cases
2902 elsif Pragma_Name
(Prag
) = Name_Exceptional_Cases
then
2903 Expand_Pragma_Exceptional_Cases
(Prag
);
2905 elsif Pragma_Name
(Prag
) = Name_Subprogram_Variant
then
2906 Expand_Pragma_Subprogram_Variant
2909 Body_Decls
=> Decls
);
2913 Prag
:= Next_Pragma
(Prag
);
2916 end Process_Contract_Cases_For
;
2918 -- Start of processing for Process_Contract_Cases
2921 Process_Contract_Cases_For
(Body_Id
);
2923 if Present
(Spec_Id
) then
2924 Process_Contract_Cases_For
(Spec_Id
);
2926 end Process_Contract_Cases
;
2928 ----------------------------
2929 -- Process_Postconditions --
2930 ----------------------------
2932 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2933 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2934 -- Collect all [refined] postconditions of a specific kind denoted
2935 -- by Post_Nam that belong to the body, and generate pragma Check
2936 -- equivalents in list Stmts.
2938 procedure Process_Spec_Postconditions
;
2939 -- Collect all [inherited] postconditions of the spec, and generate
2940 -- pragma Check equivalents in list Stmts.
2942 ---------------------------------
2943 -- Process_Body_Postconditions --
2944 ---------------------------------
2946 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2947 Items
: constant Node_Id
:= Contract
(Body_Id
);
2948 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2953 -- Process the contract
2955 if Present
(Items
) then
2956 Prag
:= Pre_Post_Conditions
(Items
);
2957 while Present
(Prag
) loop
2958 if Pragma_Name
(Prag
) = Post_Nam
2959 and then Is_Checked
(Prag
)
2962 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2966 Prag
:= Next_Pragma
(Prag
);
2970 -- The subprogram body being processed is actually the proper body
2971 -- of a stub with a corresponding spec. The subprogram stub may
2972 -- carry a postcondition pragma, in which case it must be taken
2973 -- into account. The pragma appears after the stub.
2975 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2976 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2977 while Present
(Decl
) loop
2979 -- Note that non-matching pragmas are skipped
2981 if Nkind
(Decl
) = N_Pragma
then
2982 if Pragma_Name
(Decl
) = Post_Nam
2983 and then Is_Checked
(Decl
)
2986 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2990 -- Skip internally generated code
2992 elsif not Comes_From_Source
(Decl
) then
2995 -- Postcondition pragmas are usually grouped together. There
2996 -- is no need to inspect the whole declarative list.
3005 end Process_Body_Postconditions
;
3007 ---------------------------------
3008 -- Process_Spec_Postconditions --
3009 ---------------------------------
3011 procedure Process_Spec_Postconditions
is
3012 Subps
: constant Subprogram_List
:=
3013 Inherited_Subprograms
(Spec_Id
);
3014 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
3016 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean;
3017 -- Return True if the contract of subprogram Subp_Id has been
3024 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean is
3026 for Index
in Seen
'Range loop
3027 if Seen
(Index
) = Subp_Id
then
3040 Subp_Id
: Entity_Id
;
3042 -- Start of processing for Process_Spec_Postconditions
3045 -- Process the contract
3047 Items
:= Contract
(Spec_Id
);
3049 if Present
(Items
) then
3050 Prag
:= Pre_Post_Conditions
(Items
);
3051 while Present
(Prag
) loop
3052 if Pragma_Name
(Prag
) = Name_Postcondition
3053 and then Is_Checked
(Prag
)
3056 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
3060 Prag
:= Next_Pragma
(Prag
);
3064 -- Process the contracts of all inherited subprograms, looking for
3065 -- class-wide postconditions.
3067 for Index
in Subps
'Range loop
3068 Subp_Id
:= Subps
(Index
);
3070 if Present
(Alias
(Subp_Id
)) then
3071 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
3074 -- Wrappers of class-wide pre/postconditions reference the
3075 -- parent primitive that has the inherited contract.
3077 if Is_Wrapper
(Subp_Id
)
3078 and then Present
(LSP_Subprogram
(Subp_Id
))
3080 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
3083 Items
:= Contract
(Subp_Id
);
3085 if not Seen_Subp
(Subp_Id
) and then Present
(Items
) then
3086 Seen
(Index
) := Subp_Id
;
3088 Prag
:= Pre_Post_Conditions
(Items
);
3089 while Present
(Prag
) loop
3090 if Pragma_Name
(Prag
) = Name_Postcondition
3091 and then Class_Present
(Prag
)
3094 Build_Pragma_Check_Equivalent
3097 Inher_Id
=> Subp_Id
);
3099 -- The pragma Check equivalent of the class-wide
3100 -- postcondition is still created even though the
3101 -- pragma may be ignored because the equivalent
3102 -- performs semantic checks.
3104 if Is_Checked
(Prag
) then
3105 Append_Enabled_Item
(Item
, Stmts
);
3109 Prag
:= Next_Pragma
(Prag
);
3113 end Process_Spec_Postconditions
;
3115 pragma Unmodified
(Stmts
);
3116 -- Stmts is passed as IN OUT to signal that the list can be updated,
3117 -- even if the corresponding integer value representing the list does
3120 -- Start of processing for Process_Postconditions
3123 -- The processing of postconditions is done in reverse order (body
3124 -- first) to ensure the following arrangement:
3126 -- <refined postconditions from body>
3127 -- <postconditions from body>
3128 -- <postconditions from spec>
3129 -- <inherited postconditions>
3131 Process_Body_Postconditions
(Name_Refined_Post
);
3132 Process_Body_Postconditions
(Name_Postcondition
);
3134 if Present
(Spec_Id
) then
3135 Process_Spec_Postconditions
;
3137 end Process_Postconditions
;
3139 ---------------------------
3140 -- Process_Preconditions --
3141 ---------------------------
3143 procedure Process_Preconditions
(Decls
: in out List_Id
) is
3144 Insert_Node
: Node_Id
:= Empty
;
3145 -- The insertion node after which all pragma Check equivalents are
3148 procedure Prepend_To_Decls
(Item
: Node_Id
);
3149 -- Prepend a single item to the declarations of the subprogram body
3151 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
);
3152 -- Prepend a normal precondition to the declarations of the body and
3155 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
3156 -- Collect all preconditions of subprogram Subp_Id and prepend their
3157 -- pragma Check equivalents to the declarations of the body.
3159 ----------------------
3160 -- Prepend_To_Decls --
3161 ----------------------
3163 procedure Prepend_To_Decls
(Item
: Node_Id
) is
3165 -- Ensure that the body has a declarative list
3169 Set_Declarations
(Body_Decl
, Decls
);
3172 Prepend_To
(Decls
, Item
);
3173 end Prepend_To_Decls
;
3175 -----------------------------
3176 -- Prepend_Pragma_To_Decls --
3177 -----------------------------
3179 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
) is
3180 Check_Prag
: Node_Id
;
3183 -- Skip the sole class-wide precondition (if any) since it is
3184 -- processed by Merge_Class_Conditions.
3186 if Class_Present
(Prag
) then
3189 -- Accumulate the corresponding Check pragmas at the top of the
3190 -- declarations. Prepending the items ensures that they will be
3191 -- evaluated in their original order.
3194 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
3195 Prepend_To_Decls
(Check_Prag
);
3198 end Prepend_Pragma_To_Decls
;
3200 -------------------------------
3201 -- Process_Preconditions_For --
3202 -------------------------------
3204 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
3205 Items
: constant Node_Id
:= Contract
(Subp_Id
);
3206 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
3212 -- Process the contract. If the body is an expression function
3213 -- that is a completion, freeze types within, because this may
3214 -- not have been done yet, when the subprogram declaration and
3215 -- its completion by an expression function appear in distinct
3216 -- declarative lists of the same unit (visible and private).
3219 Was_Expression_Function
(Body_Decl
)
3220 and then Sloc
(Body_Id
) /= Sloc
(Subp_Id
)
3221 and then In_Same_Source_Unit
(Body_Id
, Subp_Id
)
3222 and then not In_Same_List
(Body_Decl
, Subp_Decl
);
3224 if Present
(Items
) then
3225 Prag
:= Pre_Post_Conditions
(Items
);
3226 while Present
(Prag
) loop
3227 if Pragma_Name
(Prag
) = Name_Precondition
3228 and then Is_Checked
(Prag
)
3231 and then Present
(Corresponding_Aspect
(Prag
))
3235 Typ
=> Standard_Boolean
,
3238 (First
(Pragma_Argument_Associations
(Prag
))),
3242 Prepend_Pragma_To_Decls
(Prag
);
3245 Prag
:= Next_Pragma
(Prag
);
3249 -- The subprogram declaration being processed is actually a body
3250 -- stub. The stub may carry a precondition pragma, in which case
3251 -- it must be taken into account. The pragma appears after the
3254 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
3256 -- Inspect the declarations following the body stub
3258 Decl
:= Next
(Subp_Decl
);
3259 while Present
(Decl
) loop
3261 -- Note that non-matching pragmas are skipped
3263 if Nkind
(Decl
) = N_Pragma
then
3264 if Pragma_Name
(Decl
) = Name_Precondition
3265 and then Is_Checked
(Decl
)
3267 Prepend_Pragma_To_Decls
(Decl
);
3270 -- Skip internally generated code
3272 elsif not Comes_From_Source
(Decl
) then
3275 -- Preconditions are usually grouped together. There is no
3276 -- need to inspect the whole declarative list.
3285 end Process_Preconditions_For
;
3289 Body_Decls
: constant List_Id
:= Declarations
(Body_Decl
);
3291 Next_Decl
: Node_Id
;
3293 -- Start of processing for Process_Preconditions
3296 -- Find the proper insertion point for all pragma Check equivalents
3298 if Present
(Body_Decls
) then
3299 Decl
:= First
(Body_Decls
);
3300 while Present
(Decl
) loop
3302 -- First source declaration terminates the search, because all
3303 -- preconditions must be evaluated prior to it, by definition.
3305 if Comes_From_Source
(Decl
) then
3308 -- Certain internally generated object renamings such as those
3309 -- for discriminants and protection fields must be elaborated
3310 -- before the preconditions are evaluated, as their expressions
3311 -- may mention the discriminants. The renamings include those
3312 -- for private components so we need to find the last such.
3314 elsif Is_Prologue_Renaming
(Decl
) then
3315 while Present
(Next
(Decl
))
3316 and then Is_Prologue_Renaming
(Next
(Decl
))
3321 Insert_Node
:= Decl
;
3323 -- Otherwise the declaration does not come from source. This
3324 -- also terminates the search, because internal code may raise
3325 -- exceptions which should not preempt the preconditions.
3334 -- The processing of preconditions is done in reverse order (body
3335 -- first), because each pragma Check equivalent is inserted at the
3336 -- top of the declarations. This ensures that the final order is
3337 -- consistent with following diagram:
3339 -- <inherited preconditions>
3340 -- <preconditions from spec>
3341 -- <preconditions from body>
3343 Process_Preconditions_For
(Body_Id
);
3345 -- Move the generated entry-call prologue renamings into the
3346 -- outer declarations for use in the preconditions.
3348 Decl
:= First
(Body_Decls
);
3349 while Present
(Decl
) and then Present
(Insert_Node
) loop
3350 Next_Decl
:= Next
(Decl
);
3352 Prepend_To_Decls
(Decl
);
3354 exit when Decl
= Insert_Node
;
3359 if Present
(Spec_Id
) then
3360 Process_Preconditions_For
(Spec_Id
);
3362 end Process_Preconditions
;
3366 Restore_Scope
: Boolean := False;
3368 Stmts
: List_Id
:= No_List
;
3369 Decls
: List_Id
:= New_List
;
3370 Subp_Id
: Entity_Id
;
3372 -- Start of processing for Expand_Subprogram_Contract
3375 -- Obtain the entity of the initial declaration
3377 if Present
(Spec_Id
) then
3383 -- Do not perform expansion activity when it is not needed
3385 if not Expander_Active
then
3388 -- GNATprove does not need the executable semantics of a contract
3390 elsif GNATprove_Mode
then
3393 -- The contract of a generic subprogram or one declared in a generic
3394 -- context is not expanded, as the corresponding instance will provide
3395 -- the executable semantics of the contract.
3397 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
3400 -- All subprograms carry a contract, but for some it is not significant
3401 -- and should not be processed. This is a small optimization.
3403 elsif not Has_Significant_Contract
(Subp_Id
) then
3406 -- The contract of an ignored Ghost subprogram does not need expansion,
3407 -- because the subprogram and all calls to it will be removed.
3409 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
3412 -- No action needed for helpers and indirect-call wrapper built to
3413 -- support class-wide preconditions.
3415 elsif Present
(Class_Preconditions_Subprogram
(Subp_Id
)) then
3418 -- Do not re-expand the same contract. This scenario occurs when a
3419 -- construct is rewritten into something else during its analysis
3420 -- (expression functions for instance).
3422 elsif Has_Expanded_Contract
(Subp_Id
) then
3426 -- Prevent multiple expansion attempts of the same contract
3428 Set_Has_Expanded_Contract
(Subp_Id
);
3430 -- Ensure that the formal parameters are visible when expanding all
3433 if not In_Open_Scopes
(Subp_Id
) then
3434 Restore_Scope
:= True;
3435 Push_Scope
(Subp_Id
);
3437 if Is_Generic_Subprogram
(Subp_Id
) then
3438 Install_Generic_Formals
(Subp_Id
);
3440 Install_Formals
(Subp_Id
);
3444 -- The expansion of a subprogram contract involves the creation of Check
3445 -- pragmas to verify the contract assertions of the spec and body in a
3446 -- particular order. The order is as follows:
3448 -- function Original_Code (...) return ... is
3449 -- <prologue renamings>
3450 -- <inherited preconditions>
3451 -- <preconditions from spec>
3452 -- <preconditions from body>
3453 -- <contract case conditions>
3455 -- function _Wrapped_Statements (...) return ... is
3456 -- <source declarations>
3458 -- <source statements>
3459 -- end _Wrapped_Statements;
3462 -- return Result : constant ... := _Wrapped_Statements do
3463 -- <refined postconditions from body>
3464 -- <postconditions from body>
3465 -- <postconditions from spec>
3466 -- <inherited postconditions>
3467 -- <contract case consequences>
3468 -- <invariant check of function result>
3469 -- <invariant and predicate checks of parameters
3471 -- end Original_Code;
3473 -- Step 1: augment contracts list with postconditions associated with
3474 -- Stable_Properties and Stable_Properties'Class aspects. This must
3475 -- precede Process_Postconditions.
3477 for Class_Present
in Boolean loop
3478 Add_Stable_Property_Contracts
3479 (Subp_Id
, Class_Present
=> Class_Present
);
3482 -- Step 2: Handle all preconditions. This action must come before the
3483 -- processing of pragma Contract_Cases because the pragma prepends items
3484 -- to the body declarations.
3486 Process_Preconditions
(Decls
);
3488 -- Step 3: Handle all postconditions. This action must come before the
3489 -- processing of pragma Contract_Cases because the pragma appends items
3492 Process_Postconditions
(Stmts
);
3494 -- Step 4: Handle pragma Contract_Cases. This action must come before
3495 -- the processing of invariants and predicates because those append
3496 -- items to list Stmts.
3498 Process_Contract_Cases
(Stmts
, Decls
);
3500 -- Step 5: Apply invariant and predicate checks on a function result and
3501 -- all formals. The resulting checks are accumulated in list Stmts.
3503 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3505 -- Step 6: Construct subprogram _wrapped_statements
3507 -- When no statements are present we still need to insert contract
3508 -- related declarations.
3511 Prepend_List_To
(Declarations
(Body_Decl
), Decls
);
3513 -- Otherwise, we need a wrapper
3516 Build_Subprogram_Contract_Wrapper
(Body_Id
, Stmts
, Decls
, Result
);
3519 if Restore_Scope
then
3522 end Expand_Subprogram_Contract
;
3524 -------------------------------
3525 -- Freeze_Previous_Contracts --
3526 -------------------------------
3528 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3529 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3530 pragma Inline
(Causes_Contract_Freezing
);
3531 -- Determine whether arbitrary node N causes contract freezing. This is
3532 -- used as an assertion for the current body declaration that caused
3533 -- contract freezing, and as a condition to detect body declaration that
3534 -- already caused contract freezing before.
3536 procedure Freeze_Contracts
;
3537 pragma Inline
(Freeze_Contracts
);
3538 -- Freeze the contracts of all eligible constructs which precede body
3541 procedure Freeze_Enclosing_Package_Body
;
3542 pragma Inline
(Freeze_Enclosing_Package_Body
);
3543 -- Freeze the contract of the nearest package body (if any) which
3544 -- encloses body Body_Decl.
3546 ------------------------------
3547 -- Causes_Contract_Freezing --
3548 ------------------------------
3550 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3552 -- The following condition matches guards for calls to
3553 -- Freeze_Previous_Contracts from routines that analyze various body
3554 -- declarations. In particular, it detects expression functions, as
3555 -- described in the call from Analyze_Subprogram_Body_Helper.
3558 Comes_From_Source
(Original_Node
(N
))
3561 N_Entry_Body | N_Package_Body | N_Protected_Body |
3562 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body
;
3563 end Causes_Contract_Freezing
;
3565 ----------------------
3566 -- Freeze_Contracts --
3567 ----------------------
3569 procedure Freeze_Contracts
is
3570 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3574 -- Nothing to do when the body which causes freezing does not appear
3575 -- in a declarative list because there cannot possibly be constructs
3578 if not Is_List_Member
(Body_Decl
) then
3582 -- Inspect the declarations preceding the body, and freeze individual
3583 -- contracts of eligible constructs.
3585 Decl
:= Prev
(Body_Decl
);
3586 while Present
(Decl
) loop
3588 -- Stop the traversal when a preceding construct that causes
3589 -- freezing is encountered as there is no point in refreezing
3590 -- the already frozen constructs.
3592 if Causes_Contract_Freezing
(Decl
) then
3595 -- Entry or subprogram declarations
3597 elsif Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
3598 | N_Entry_Declaration
3599 | N_Generic_Subprogram_Declaration
3600 | N_Subprogram_Declaration
3602 Analyze_Entry_Or_Subprogram_Contract
3603 (Subp_Id
=> Defining_Entity
(Decl
),
3604 Freeze_Id
=> Body_Id
);
3608 elsif Nkind
(Decl
) = N_Object_Declaration
then
3609 Analyze_Object_Contract
3610 (Obj_Id
=> Defining_Entity
(Decl
),
3611 Freeze_Id
=> Body_Id
);
3615 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
3616 | N_Single_Protected_Declaration
3618 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3620 -- Subprogram body stubs
3622 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3623 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3627 elsif Nkind
(Decl
) in N_Single_Task_Declaration
3628 | N_Task_Type_Declaration
3630 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3633 if Nkind
(Decl
) in N_Full_Type_Declaration
3634 | N_Private_Type_Declaration
3635 | N_Task_Type_Declaration
3636 | N_Protected_Type_Declaration
3637 | N_Formal_Type_Declaration
3639 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
3644 end Freeze_Contracts
;
3646 -----------------------------------
3647 -- Freeze_Enclosing_Package_Body --
3648 -----------------------------------
3650 procedure Freeze_Enclosing_Package_Body
is
3651 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3655 -- Climb the parent chain looking for an enclosing package body. Do
3656 -- not use the scope stack, because a body utilizes the entity of its
3657 -- corresponding spec.
3659 Par
:= Parent
(Body_Decl
);
3660 while Present
(Par
) loop
3661 if Nkind
(Par
) = N_Package_Body
then
3662 Analyze_Package_Body_Contract
3663 (Body_Id
=> Defining_Entity
(Par
),
3664 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3668 -- Do not look for an enclosing package body when the construct
3669 -- which causes freezing is a body generated for an expression
3670 -- function and it appears within a package spec. This ensures
3671 -- that the traversal will not reach too far up the parent chain
3672 -- and attempt to freeze a package body which must not be frozen.
3674 -- package body Enclosing_Body
3675 -- with Refined_State => (State => Var)
3677 -- package Nested is
3678 -- type Some_Type is ...;
3679 -- function Cause_Freezing return ...;
3681 -- function Cause_Freezing is (...);
3684 -- Var : Nested.Some_Type;
3686 elsif Nkind
(Par
) = N_Package_Declaration
3687 and then Nkind
(Orig_Decl
) = N_Expression_Function
3691 -- Prevent the search from going too far
3693 elsif Is_Body_Or_Package_Declaration
(Par
) then
3697 Par
:= Parent
(Par
);
3699 end Freeze_Enclosing_Package_Body
;
3703 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3705 -- Start of processing for Freeze_Previous_Contracts
3708 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3710 -- A body that is in the process of being inlined appears from source,
3711 -- but carries name _parent. Such a body does not cause freezing of
3714 if Chars
(Body_Id
) = Name_uParent
then
3718 Freeze_Enclosing_Package_Body
;
3720 end Freeze_Previous_Contracts
;
3722 ---------------------------------
3723 -- Inherit_Subprogram_Contract --
3724 ---------------------------------
3726 procedure Inherit_Subprogram_Contract
3728 From_Subp
: Entity_Id
)
3730 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3731 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3734 --------------------
3735 -- Inherit_Pragma --
3736 --------------------
3738 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3739 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3743 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3744 -- chains, therefore the node must be replicated. The new pragma is
3745 -- flagged as inherited for distinction purposes.
3747 if Present
(Prag
) then
3748 New_Prag
:= New_Copy_Tree
(Prag
);
3749 Set_Is_Inherited_Pragma
(New_Prag
);
3751 Add_Contract_Item
(New_Prag
, Subp
);
3755 -- Start of processing for Inherit_Subprogram_Contract
3758 -- Inheritance is carried out only when both entities are subprograms
3761 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3762 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3763 and then Present
(Contract
(From_Subp
))
3765 Inherit_Pragma
(Pragma_Extensions_Visible
);
3767 end Inherit_Subprogram_Contract
;
3769 -------------------------------------
3770 -- Instantiate_Subprogram_Contract --
3771 -------------------------------------
3773 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3774 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3775 -- Instantiate all contract-related source pragmas found in the list,
3776 -- starting with pragma First_Prag. Each instantiated pragma is added
3779 -------------------------
3780 -- Instantiate_Pragmas --
3781 -------------------------
3783 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3784 Inst_Prag
: Node_Id
;
3789 while Present
(Prag
) loop
3790 if Is_Generic_Contract_Pragma
(Prag
) then
3792 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3794 Set_Analyzed
(Inst_Prag
, False);
3795 Append_To
(L
, Inst_Prag
);
3798 Prag
:= Next_Pragma
(Prag
);
3800 end Instantiate_Pragmas
;
3804 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3806 -- Start of processing for Instantiate_Subprogram_Contract
3809 if Present
(Items
) then
3810 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3811 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3812 Instantiate_Pragmas
(Classifications
(Items
));
3814 end Instantiate_Subprogram_Contract
;
3816 --------------------------
3817 -- Is_Prologue_Renaming --
3818 --------------------------
3820 -- This should be turned into a flag and set during the expansion of
3821 -- task and protected types when the renamings get generated ???
3823 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
3830 if Nkind
(Decl
) = N_Object_Renaming_Declaration
3831 and then not Comes_From_Source
(Decl
)
3833 Obj
:= Defining_Entity
(Decl
);
3836 if Nkind
(Nam
) = N_Selected_Component
then
3837 -- Analyze the renaming declaration so we can further examine it
3839 if not Analyzed
(Decl
) then
3843 Pref
:= Prefix
(Nam
);
3844 Sel
:= Selector_Name
(Nam
);
3846 -- A discriminant renaming appears as
3847 -- Discr : constant ... := Prefix.Discr;
3849 if Ekind
(Obj
) = E_Constant
3850 and then Is_Entity_Name
(Sel
)
3851 and then Present
(Entity
(Sel
))
3852 and then Ekind
(Entity
(Sel
)) = E_Discriminant
3856 -- A protection field renaming appears as
3857 -- Prot : ... := _object._object;
3859 -- A renamed private component is just a component of
3860 -- _object, with an arbitrary name.
3862 elsif Ekind
(Obj
) in E_Variable | E_Constant
3863 and then Nkind
(Pref
) = N_Identifier
3864 and then Chars
(Pref
) = Name_uObject
3865 and then Nkind
(Sel
) = N_Identifier
3873 end Is_Prologue_Renaming
;
3875 -----------------------------------
3876 -- Make_Class_Precondition_Subps --
3877 -----------------------------------
3879 procedure Make_Class_Precondition_Subps
3880 (Subp_Id
: Entity_Id
;
3881 Late_Overriding
: Boolean := False)
3883 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
3884 Tagged_Type
: constant Entity_Id
:= Find_Dispatching_Type
(Subp_Id
);
3886 procedure Add_Indirect_Call_Wrapper
;
3887 -- Build the indirect-call wrapper and append it to the freezing actions
3890 procedure Add_Call_Helper
3891 (Helper_Id
: Entity_Id
;
3892 Is_Dynamic
: Boolean);
3893 -- Factorizes code for building a call helper with the given identifier
3894 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
3895 -- controls building the static or dynamic version of the helper.
3897 function Build_Unique_Name
(Suffix
: String) return Name_Id
;
3898 -- Build an unique new name adding suffix to Subp_Id name (plus its
3899 -- homonym number for values bigger than 1).
3901 -------------------------------
3902 -- Add_Indirect_Call_Wrapper --
3903 -------------------------------
3905 procedure Add_Indirect_Call_Wrapper
is
3907 function Build_ICW_Body
return Node_Id
;
3908 -- Build the body of the indirect call wrapper
3910 function Build_ICW_Decl
return Node_Id
;
3911 -- Build the declaration of the indirect call wrapper
3913 --------------------
3914 -- Build_ICW_Body --
3915 --------------------
3917 function Build_ICW_Body
return Node_Id
is
3918 ICW_Id
: constant Entity_Id
:= Indirect_Call_Wrapper
(Subp_Id
);
3919 Spec
: constant Node_Id
:= Parent
(ICW_Id
);
3920 Body_Spec
: Node_Id
;
3925 Body_Spec
:= Copy_Subprogram_Spec
(Spec
);
3927 -- Build call to wrapped subprogram
3930 Actuals
: constant List_Id
:= Empty_List
;
3931 Formal_Spec
: Entity_Id
:=
3932 First
(Parameter_Specifications
(Spec
));
3934 -- Build parameter association & call
3936 while Present
(Formal_Spec
) loop
3939 (Defining_Identifier
(Formal_Spec
), Loc
));
3943 if Ekind
(ICW_Id
) = E_Procedure
then
3945 Make_Procedure_Call_Statement
(Loc
,
3946 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3947 Parameter_Associations
=> Actuals
);
3950 Make_Simple_Return_Statement
(Loc
,
3952 Make_Function_Call
(Loc
,
3953 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3954 Parameter_Associations
=> Actuals
));
3959 Make_Subprogram_Body
(Loc
,
3960 Specification
=> Body_Spec
,
3961 Declarations
=> New_List
,
3962 Handled_Statement_Sequence
=>
3963 Make_Handled_Sequence_Of_Statements
(Loc
,
3964 Statements
=> New_List
(Call
)));
3966 -- The new operation is internal and overriding indicators do not
3969 Set_Must_Override
(Body_Spec
, False);
3974 --------------------
3975 -- Build_ICW_Decl --
3976 --------------------
3978 function Build_ICW_Decl
return Node_Id
is
3979 ICW_Id
: constant Entity_Id
:=
3980 Make_Defining_Identifier
(Loc
,
3981 Build_Unique_Name
(Suffix
=> "ICW"));
3986 Spec
:= Copy_Subprogram_Spec
(Parent
(Subp_Id
));
3987 Set_Must_Override
(Spec
, False);
3988 Set_Must_Not_Override
(Spec
, False);
3989 Set_Defining_Unit_Name
(Spec
, ICW_Id
);
3990 Mutate_Ekind
(ICW_Id
, Ekind
(Subp_Id
));
3991 Set_Is_Public
(ICW_Id
);
3993 -- The indirect call wrapper is commonly used for indirect calls
3994 -- but inlined for direct calls performed from the DTW.
3996 Set_Is_Inlined
(ICW_Id
);
3998 if Nkind
(Spec
) = N_Procedure_Specification
then
3999 Set_Null_Present
(Spec
, False);
4002 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
4004 -- Link original subprogram to indirect wrapper and vice versa
4006 Set_Indirect_Call_Wrapper
(Subp_Id
, ICW_Id
);
4007 Set_Class_Preconditions_Subprogram
(ICW_Id
, Subp_Id
);
4009 -- Inherit debug info flag to allow debugging the wrapper
4011 if Needs_Debug_Info
(Subp_Id
) then
4012 Set_Debug_Info_Needed
(ICW_Id
);
4023 -- Start of processing for Add_Indirect_Call_Wrapper
4026 pragma Assert
(No
(Indirect_Call_Wrapper
(Subp_Id
)));
4028 ICW_Decl
:= Build_ICW_Decl
;
4030 Append_Freeze_Action
(Tagged_Type
, ICW_Decl
);
4033 ICW_Body
:= Build_ICW_Body
;
4034 Append_Freeze_Action
(Tagged_Type
, ICW_Body
);
4036 -- We cannot defer the analysis of this ICW wrapper when it is
4037 -- built as a consequence of building its partner DTW wrapper
4038 -- at the freezing point of the tagged type.
4040 if Is_Dispatch_Table_Wrapper
(Subp_Id
) then
4043 end Add_Indirect_Call_Wrapper
;
4045 ---------------------
4046 -- Add_Call_Helper --
4047 ---------------------
4049 procedure Add_Call_Helper
4050 (Helper_Id
: Entity_Id
;
4051 Is_Dynamic
: Boolean)
4053 function Build_Call_Helper_Body
return Node_Id
;
4054 -- Build the body of a call helper
4056 function Build_Call_Helper_Decl
return Node_Id
;
4057 -- Build the declaration of a call helper
4059 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
;
4060 -- Build the specification of the helper
4062 ----------------------------
4063 -- Build_Call_Helper_Body --
4064 ----------------------------
4066 function Build_Call_Helper_Body
return Node_Id
is
4068 function Copy_And_Update_References
4069 (Expr
: Node_Id
) return Node_Id
;
4070 -- Copy Expr updating references to formals of Helper_Id; update
4071 -- also references to loop identifiers of quantified expressions.
4073 --------------------------------
4074 -- Copy_And_Update_References --
4075 --------------------------------
4077 function Copy_And_Update_References
4078 (Expr
: Node_Id
) return Node_Id
4080 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4082 procedure Map_Quantified_Expression_Loop_Identifiers
;
4083 -- Traverse Expr and append to Assoc_List the mapping of loop
4084 -- identifers of quantified expressions with its new copy.
4086 ------------------------------------------------
4087 -- Map_Quantified_Expression_Loop_Identifiers --
4088 ------------------------------------------------
4090 procedure Map_Quantified_Expression_Loop_Identifiers
is
4091 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
;
4092 -- Append to Assoc_List the mapping of loop identifers of
4093 -- quantified expressions with its new copy.
4095 --------------------
4096 -- Map_Loop_Param --
4097 --------------------
4099 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
4102 if Nkind
(N
) = N_Loop_Parameter_Specification
4103 and then Nkind
(Parent
(N
)) = N_Quantified_Expression
4106 Def_Id
: constant Entity_Id
:=
4107 Defining_Identifier
(N
);
4109 Append_Elmt
(Def_Id
, Assoc_List
);
4110 Append_Elmt
(New_Copy
(Def_Id
), Assoc_List
);
4117 procedure Map_Quantified_Expressions
is
4118 new Traverse_Proc
(Map_Loop_Param
);
4121 Map_Quantified_Expressions
(Expr
);
4122 end Map_Quantified_Expression_Loop_Identifiers
;
4126 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp_Id
);
4127 Helper_Formal_Id
: Entity_Id
:= First_Formal
(Helper_Id
);
4129 -- Start of processing for Copy_And_Update_References
4132 while Present
(Subp_Formal_Id
) loop
4133 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4134 Append_Elmt
(Helper_Formal_Id
, Assoc_List
);
4136 Next_Formal
(Subp_Formal_Id
);
4137 Next_Formal
(Helper_Formal_Id
);
4140 Map_Quantified_Expression_Loop_Identifiers
;
4142 return New_Copy_Tree
(Expr
, Map
=> Assoc_List
);
4143 end Copy_And_Update_References
;
4147 Helper_Decl
: constant Node_Id
:= Parent
(Parent
(Helper_Id
));
4148 Body_Id
: Entity_Id
;
4149 Body_Spec
: Node_Id
;
4150 Body_Stmts
: Node_Id
;
4151 Helper_Body
: Node_Id
;
4152 Return_Expr
: Node_Id
;
4154 -- Start of processing for Build_Call_Helper_Body
4157 pragma Assert
(Analyzed
(Unit_Declaration_Node
(Helper_Id
)));
4158 pragma Assert
(No
(Corresponding_Body
(Helper_Decl
)));
4160 Body_Id
:= Make_Defining_Identifier
(Loc
, Chars
(Helper_Id
));
4161 Body_Spec
:= Build_Call_Helper_Spec
(Body_Id
);
4163 Set_Corresponding_Body
(Helper_Decl
, Body_Id
);
4164 Set_Must_Override
(Body_Spec
, False);
4166 if Present
(Class_Preconditions
(Subp_Id
))
4167 -- Evaluate the expression if we are building a dynamic helper
4168 -- or we are building a static helper for a non-abstract tagged
4169 -- type; for abstract tagged types the helper just returns True
4170 -- since it is called by the indirect call wrapper (ICW).
4174 not Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)))
4177 Copy_And_Update_References
(Class_Preconditions
(Subp_Id
));
4179 -- When the subprogram is compiled with assertions disabled the
4180 -- helper just returns True; done to avoid reporting errors at
4181 -- link time since a unit may be compiled with assertions disabled
4182 -- and another (which depends on it) compiled with assertions
4186 pragma Assert
(Present
(Ignored_Class_Preconditions
(Subp_Id
))
4187 or else Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)));
4188 Return_Expr
:= New_Occurrence_Of
(Standard_True
, Loc
);
4192 Make_Handled_Sequence_Of_Statements
(Loc
,
4193 Statements
=> New_List
(
4194 Make_Simple_Return_Statement
(Loc
, Return_Expr
)));
4197 Make_Subprogram_Body
(Loc
,
4198 Specification
=> Body_Spec
,
4199 Declarations
=> New_List
,
4200 Handled_Statement_Sequence
=> Body_Stmts
);
4203 end Build_Call_Helper_Body
;
4205 ----------------------------
4206 -- Build_Call_Helper_Decl --
4207 ----------------------------
4209 function Build_Call_Helper_Decl
return Node_Id
is
4214 Spec
:= Build_Call_Helper_Spec
(Helper_Id
);
4215 Set_Must_Override
(Spec
, False);
4216 Set_Must_Not_Override
(Spec
, False);
4217 Set_Is_Inlined
(Helper_Id
);
4218 Set_Is_Public
(Helper_Id
);
4220 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
4222 -- Inherit debug info flag from Subp_Id to Helper_Id to allow
4223 -- debugging of the helper subprogram.
4225 if Needs_Debug_Info
(Subp_Id
) then
4226 Set_Debug_Info_Needed
(Helper_Id
);
4230 end Build_Call_Helper_Decl
;
4232 ----------------------------
4233 -- Build_Call_Helper_Spec --
4234 ----------------------------
4236 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
4238 Spec
: constant Node_Id
:= Parent
(Subp_Id
);
4239 Def_Id
: constant Node_Id
:= Defining_Unit_Name
(Spec
);
4241 Func_Formals
: constant List_Id
:= New_List
;
4242 P_Spec
: constant List_Id
:= Parameter_Specifications
(Spec
);
4243 Par_Formal
: Node_Id
;
4245 Param_Type
: Node_Id
;
4248 -- Create a list of formal parameters with the same types as the
4249 -- original subprogram but changing the controlling formal.
4251 Param
:= First
(P_Spec
);
4252 Formal
:= First_Formal
(Def_Id
);
4253 while Present
(Formal
) loop
4254 Par_Formal
:= Parent
(Formal
);
4256 if Is_Dynamic
and then Is_Controlling_Formal
(Formal
) then
4257 if Nkind
(Parameter_Type
(Par_Formal
))
4258 = N_Access_Definition
4261 Copy_Separate_Tree
(Parameter_Type
(Par_Formal
));
4262 Rewrite
(Subtype_Mark
(Param_Type
),
4263 Make_Attribute_Reference
(Loc
,
4264 Prefix
=> Relocate_Node
(Subtype_Mark
(Param_Type
)),
4265 Attribute_Name
=> Name_Class
));
4269 Make_Attribute_Reference
(Loc
,
4270 Prefix
=> New_Occurrence_Of
(Etype
(Formal
), Loc
),
4271 Attribute_Name
=> Name_Class
);
4274 Param_Type
:= New_Occurrence_Of
(Etype
(Formal
), Loc
);
4277 Append_To
(Func_Formals
,
4278 Make_Parameter_Specification
(Loc
,
4279 Defining_Identifier
=>
4280 Make_Defining_Identifier
(Loc
, Chars
(Formal
)),
4281 In_Present
=> In_Present
(Par_Formal
),
4282 Out_Present
=> Out_Present
(Par_Formal
),
4283 Null_Exclusion_Present
=> Null_Exclusion_Present
4285 Parameter_Type
=> Param_Type
));
4288 Next_Formal
(Formal
);
4292 Make_Function_Specification
(Loc
,
4293 Defining_Unit_Name
=> Spec_Id
,
4294 Parameter_Specifications
=> Func_Formals
,
4295 Result_Definition
=>
4296 New_Occurrence_Of
(Standard_Boolean
, Loc
));
4297 end Build_Call_Helper_Spec
;
4301 Helper_Body
: Node_Id
;
4302 Helper_Decl
: Node_Id
;
4304 -- Start of processing for Add_Call_Helper
4307 Helper_Decl
:= Build_Call_Helper_Decl
;
4308 Mutate_Ekind
(Helper_Id
, Ekind
(Subp_Id
));
4310 -- Add the helper to the freezing actions of the tagged type
4312 Append_Freeze_Action
(Tagged_Type
, Helper_Decl
);
4313 Analyze
(Helper_Decl
);
4315 Helper_Body
:= Build_Call_Helper_Body
;
4316 Append_Freeze_Action
(Tagged_Type
, Helper_Body
);
4318 -- If this helper is built as part of building the DTW at the
4319 -- freezing point of its tagged type then we cannot defer
4322 if Late_Overriding
then
4323 pragma Assert
(Is_Dispatch_Table_Wrapper
(Subp_Id
));
4324 Analyze
(Helper_Body
);
4326 end Add_Call_Helper
;
4328 -----------------------
4329 -- Build_Unique_Name --
4330 -----------------------
4332 function Build_Unique_Name
(Suffix
: String) return Name_Id
is
4334 -- Append the homonym number. Strip the leading space character in
4335 -- the image of natural numbers. Also do not add the homonym value
4338 if Has_Homonym
(Subp_Id
) and then Homonym_Number
(Subp_Id
) > 1 then
4340 S
: constant String := Homonym_Number
(Subp_Id
)'Img;
4343 return New_External_Name
(Chars
(Subp_Id
),
4344 Suffix
=> Suffix
& "_" & S
(2 .. S
'Last));
4348 return New_External_Name
(Chars
(Subp_Id
), Suffix
);
4349 end Build_Unique_Name
;
4353 Helper_Id
: Entity_Id
;
4355 -- Start of processing for Make_Class_Precondition_Subps
4358 if Present
(Class_Preconditions
(Subp_Id
))
4359 or Present
(Ignored_Class_Preconditions
(Subp_Id
))
4362 (Comes_From_Source
(Subp_Id
)
4363 or else Is_Dispatch_Table_Wrapper
(Subp_Id
));
4365 if No
(Dynamic_Call_Helper
(Subp_Id
)) then
4367 -- Build and add to the freezing actions of Tagged_Type its
4368 -- dynamic-call helper.
4371 Make_Defining_Identifier
(Loc
,
4372 Build_Unique_Name
(Suffix
=> "DP"));
4373 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> True);
4375 -- Link original subprogram to helper and vice versa
4377 Set_Dynamic_Call_Helper
(Subp_Id
, Helper_Id
);
4378 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4381 if not Is_Abstract_Subprogram
(Subp_Id
)
4382 and then No
(Static_Call_Helper
(Subp_Id
))
4384 -- Build and add to the freezing actions of Tagged_Type its
4385 -- static-call helper.
4388 Make_Defining_Identifier
(Loc
,
4389 Build_Unique_Name
(Suffix
=> "SP"));
4391 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> False);
4393 -- Link original subprogram to helper and vice versa
4395 Set_Static_Call_Helper
(Subp_Id
, Helper_Id
);
4396 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4398 -- Build and add to the freezing actions of Tagged_Type the
4399 -- indirect-call wrapper.
4401 Add_Indirect_Call_Wrapper
;
4404 end Make_Class_Precondition_Subps
;
4406 ----------------------------------------------
4407 -- Process_Class_Conditions_At_Freeze_Point --
4408 ----------------------------------------------
4410 procedure Process_Class_Conditions_At_Freeze_Point
(Typ
: Entity_Id
) is
4412 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
);
4413 -- Check class-wide pre/postconditions of Spec_Id
4415 function Has_Class_Postconditions_Subprogram
4416 (Spec_Id
: Entity_Id
) return Boolean;
4417 -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
4419 function Has_Class_Preconditions_Subprogram
4420 (Spec_Id
: Entity_Id
) return Boolean;
4421 -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
4423 ----------------------------
4424 -- Check_Class_Conditions --
4425 ----------------------------
4427 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
) is
4428 Par_Subp
: Entity_Id
;
4431 for Kind
in Condition_Kind
loop
4432 Par_Subp
:= Nearest_Class_Condition_Subprogram
(Kind
, Spec_Id
);
4434 if Present
(Par_Subp
) then
4435 Check_Class_Condition
4436 (Cond
=> Class_Condition
(Kind
, Par_Subp
),
4438 Par_Subp
=> Par_Subp
,
4439 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4440 | Class_Precondition
);
4443 end Check_Class_Conditions
;
4445 -----------------------------------------
4446 -- Has_Class_Postconditions_Subprogram --
4447 -----------------------------------------
4449 function Has_Class_Postconditions_Subprogram
4450 (Spec_Id
: Entity_Id
) return Boolean is
4453 Present
(Nearest_Class_Condition_Subprogram
4454 (Spec_Id
=> Spec_Id
,
4455 Kind
=> Class_Postcondition
))
4457 Present
(Nearest_Class_Condition_Subprogram
4458 (Spec_Id
=> Spec_Id
,
4459 Kind
=> Ignored_Class_Postcondition
));
4460 end Has_Class_Postconditions_Subprogram
;
4462 ----------------------------------------
4463 -- Has_Class_Preconditions_Subprogram --
4464 ----------------------------------------
4466 function Has_Class_Preconditions_Subprogram
4467 (Spec_Id
: Entity_Id
) return Boolean is
4470 Present
(Nearest_Class_Condition_Subprogram
4471 (Spec_Id
=> Spec_Id
,
4472 Kind
=> Class_Precondition
))
4474 Present
(Nearest_Class_Condition_Subprogram
4475 (Spec_Id
=> Spec_Id
,
4476 Kind
=> Ignored_Class_Precondition
));
4477 end Has_Class_Preconditions_Subprogram
;
4481 Prim_Elmt
: Elmt_Id
:= First_Elmt
(Primitive_Operations
(Typ
));
4484 -- Start of processing for Process_Class_Conditions_At_Freeze_Point
4487 while Present
(Prim_Elmt
) loop
4488 Prim
:= Node
(Prim_Elmt
);
4490 if Has_Class_Preconditions_Subprogram
(Prim
)
4491 or else Has_Class_Postconditions_Subprogram
(Prim
)
4493 if Comes_From_Source
(Prim
) then
4494 if Has_Significant_Contract
(Prim
) then
4495 Merge_Class_Conditions
(Prim
);
4498 -- Handle wrapper of protected operation
4500 elsif Is_Primitive_Wrapper
(Prim
) then
4501 Merge_Class_Conditions
(Prim
);
4503 -- Check inherited class-wide conditions, excluding internal
4504 -- entities built for mapping of interface primitives.
4506 elsif Is_Derived_Type
(Typ
)
4507 and then Present
(Alias
(Prim
))
4508 and then No
(Interface_Alias
(Prim
))
4510 Check_Class_Conditions
(Prim
);
4514 Next_Elmt
(Prim_Elmt
);
4516 end Process_Class_Conditions_At_Freeze_Point
;
4518 ----------------------------
4519 -- Merge_Class_Conditions --
4520 ----------------------------
4522 procedure Merge_Class_Conditions
(Spec_Id
: Entity_Id
) is
4524 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
);
4525 -- Collect all inherited class-wide conditions of Spec_Id and merge
4526 -- them into one big condition.
4528 ----------------------------------
4529 -- Process_Inherited_Conditions --
4530 ----------------------------------
4532 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
) is
4533 Tag_Typ
: constant Entity_Id
:= Find_Dispatching_Type
(Spec_Id
);
4534 Subps
: constant Subprogram_List
:= Inherited_Subprograms
(Spec_Id
);
4535 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
4537 function Inherit_Condition
4538 (Par_Subp
: Entity_Id
;
4539 Subp
: Entity_Id
) return Node_Id
;
4540 -- Inherit the class-wide condition from Par_Subp to Subp and adjust
4541 -- all the references to formals in the inherited condition.
4543 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
);
4544 -- Merge two class-wide preconditions or postconditions (the former
4545 -- are merged using "or else", and the latter are merged using "and-
4546 -- then"). The changes are accumulated in parameter Into.
4548 function Seen_Subp
(Id
: Entity_Id
) return Boolean;
4549 -- Return True if the contract of subprogram Id has been processed
4551 -----------------------
4552 -- Inherit_Condition --
4553 -----------------------
4555 function Inherit_Condition
4556 (Par_Subp
: Entity_Id
;
4557 Subp
: Entity_Id
) return Node_Id
4559 function Check_Condition
(Expr
: Node_Id
) return Boolean;
4560 -- Used in assertion to check that Expr has no reference to the
4561 -- formals of Par_Subp.
4563 ---------------------
4564 -- Check_Condition --
4565 ---------------------
4567 function Check_Condition
(Expr
: Node_Id
) return Boolean is
4568 Par_Formal_Id
: Entity_Id
;
4570 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
4571 -- Check occurrence of Par_Formal_Id
4577 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
4579 if Nkind
(N
) = N_Identifier
4580 and then Present
(Entity
(N
))
4581 and then Entity
(N
) = Par_Formal_Id
4589 function Check_Expression
is new Traverse_Func
(Check_Entity
);
4591 -- Start of processing for Check_Condition
4594 Par_Formal_Id
:= First_Formal
(Par_Subp
);
4596 while Present
(Par_Formal_Id
) loop
4597 if Check_Expression
(Expr
) = Abandon
then
4601 Next_Formal
(Par_Formal_Id
);
4605 end Check_Condition
;
4609 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4610 Par_Formal_Id
: Entity_Id
:= First_Formal
(Par_Subp
);
4611 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp
);
4612 New_Condition
: Node_Id
;
4615 while Present
(Par_Formal_Id
) loop
4616 Append_Elmt
(Par_Formal_Id
, Assoc_List
);
4617 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4619 Next_Formal
(Par_Formal_Id
);
4620 Next_Formal
(Subp_Formal_Id
);
4623 -- Check that Parent field of all the nodes have their correct
4624 -- decoration; required because otherwise mapped nodes with
4625 -- wrong Parent field are left unmodified in the copied tree
4626 -- and cause reporting wrong errors at later stages.
4629 (Check_Parents
(Class_Condition
(Kind
, Par_Subp
), Assoc_List
));
4633 (Source
=> Class_Condition
(Kind
, Par_Subp
),
4636 -- Ensure that the inherited condition has no reference to the
4637 -- formals of the parent subprogram.
4639 pragma Assert
(Check_Condition
(New_Condition
));
4641 return New_Condition
;
4642 end Inherit_Condition
;
4644 ----------------------
4645 -- Merge_Conditions --
4646 ----------------------
4648 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
) is
4649 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
;
4650 -- Return the boolean expression argument of a condition while
4651 -- updating its parentheses count for the subsequent merge.
4653 --------------------
4654 -- Expression_Arg --
4655 --------------------
4657 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
is
4659 if Paren_Count
(Expr
) = 0 then
4660 Set_Paren_Count
(Expr
, 1);
4668 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
4669 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
4670 Loc
: constant Source_Ptr
:= Sloc
(Into
);
4672 -- Start of processing for Merge_Conditions
4677 -- Merge the two preconditions by "or else"-ing them
4679 when Ignored_Class_Precondition
4680 | Class_Precondition
4684 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4685 Left_Opnd
=> From_Expr
));
4687 -- Merge the two postconditions by "and then"-ing them
4689 when Ignored_Class_Postcondition
4690 | Class_Postcondition
4694 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4695 Left_Opnd
=> From_Expr
));
4697 end Merge_Conditions
;
4703 function Seen_Subp
(Id
: Entity_Id
) return Boolean is
4705 for Index
in Seen
'Range loop
4706 if Seen
(Index
) = Id
then
4716 Class_Cond
: Node_Id
;
4718 Subp_Id
: Entity_Id
;
4719 Par_Prim
: Entity_Id
:= Empty
;
4720 Par_Iface_Prims
: Elist_Id
:= No_Elist
;
4722 -- Start of processing for Process_Inherited_Conditions
4725 Class_Cond
:= Class_Condition
(Kind
, Spec_Id
);
4727 -- Process parent primitives looking for nearest ancestor with
4728 -- class-wide conditions.
4730 for Index
in Subps
'Range loop
4731 Subp_Id
:= Subps
(Index
);
4734 and then Is_Ancestor
(Find_Dispatching_Type
(Subp_Id
), Tag_Typ
)
4736 if Present
(Alias
(Subp_Id
)) then
4737 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4740 -- Wrappers of class-wide pre/postconditions reference the
4741 -- parent primitive that has the inherited contract and help
4742 -- us to climb fast.
4744 if Is_Wrapper
(Subp_Id
)
4745 and then Present
(LSP_Subprogram
(Subp_Id
))
4747 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
4750 if not Seen_Subp
(Subp_Id
)
4751 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4753 Seen
(Index
) := Subp_Id
;
4754 Par_Prim
:= Subp_Id
;
4755 Par_Iface_Prims
:= Covered_Interface_Primitives
(Par_Prim
);
4757 Cond
:= Inherit_Condition
4759 Par_Subp
=> Subp_Id
);
4761 if Present
(Class_Cond
) then
4762 Merge_Conditions
(Cond
, Class_Cond
);
4767 Check_Class_Condition
4768 (Cond
=> Class_Cond
,
4770 Par_Subp
=> Subp_Id
,
4771 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4772 | Class_Precondition
);
4773 Build_Class_Wide_Expression
4774 (Pragma_Or_Expr
=> Class_Cond
,
4776 Par_Subp
=> Subp_Id
,
4777 Adjust_Sloc
=> False);
4779 -- We are done as soon as we process the nearest ancestor
4786 -- Process the contract of interface primitives not covered by
4787 -- the nearest ancestor.
4789 for Index
in Subps
'Range loop
4790 Subp_Id
:= Subps
(Index
);
4792 if Is_Interface
(Find_Dispatching_Type
(Subp_Id
)) then
4793 if Present
(Alias
(Subp_Id
)) then
4794 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4797 if not Seen_Subp
(Subp_Id
)
4798 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4799 and then not Contains
(Par_Iface_Prims
, Subp_Id
)
4801 Seen
(Index
) := Subp_Id
;
4803 Cond
:= Inherit_Condition
4805 Par_Subp
=> Subp_Id
);
4807 Check_Class_Condition
4810 Par_Subp
=> Subp_Id
,
4811 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4812 | Class_Precondition
);
4813 Build_Class_Wide_Expression
4814 (Pragma_Or_Expr
=> Cond
,
4816 Par_Subp
=> Subp_Id
,
4817 Adjust_Sloc
=> False);
4819 if Present
(Class_Cond
) then
4820 Merge_Conditions
(Cond
, Class_Cond
);
4828 Set_Class_Condition
(Kind
, Spec_Id
, Class_Cond
);
4829 end Process_Inherited_Conditions
;
4835 -- Start of processing for Merge_Class_Conditions
4838 for Kind
in Condition_Kind
loop
4839 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4841 -- If this subprogram has class-wide conditions then preanalyze
4842 -- them before processing inherited conditions since conditions
4843 -- are checked and merged from right to left.
4845 if Present
(Cond
) then
4846 Preanalyze_Condition
(Spec_Id
, Cond
);
4849 Process_Inherited_Conditions
(Kind
);
4851 -- Preanalyze merged inherited conditions
4853 if Cond
/= Class_Condition
(Kind
, Spec_Id
) then
4854 Preanalyze_Condition
(Spec_Id
,
4855 Class_Condition
(Kind
, Spec_Id
));
4858 end Merge_Class_Conditions
;
4860 ---------------------------------
4861 -- Preanalyze_Class_Conditions --
4862 ---------------------------------
4864 procedure Preanalyze_Class_Conditions
(Spec_Id
: Entity_Id
) is
4868 for Kind
in Condition_Kind
loop
4869 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4871 if Present
(Cond
) then
4872 Preanalyze_Condition
(Spec_Id
, Cond
);
4875 end Preanalyze_Class_Conditions
;
4877 --------------------------
4878 -- Preanalyze_Condition --
4879 --------------------------
4881 procedure Preanalyze_Condition
4885 procedure Clear_Unset_References
;
4886 -- Clear unset references on formals of Subp since preanalysis
4887 -- occurs in a place unrelated to the actual code.
4889 procedure Remove_Controlling_Arguments
;
4890 -- Traverse Expr and clear the Controlling_Argument of calls to
4891 -- nonabstract functions.
4893 procedure Restore_Original_Selected_Component
;
4894 -- Traverse Expr searching for dispatching calls to functions whose
4895 -- original node was a selected component, and replace them with
4896 -- their original node.
4898 ----------------------------
4899 -- Clear_Unset_References --
4900 ----------------------------
4902 procedure Clear_Unset_References
is
4903 F
: Entity_Id
:= First_Formal
(Subp
);
4906 while Present
(F
) loop
4907 Set_Unset_Reference
(F
, Empty
);
4910 end Clear_Unset_References
;
4912 ----------------------------------
4913 -- Remove_Controlling_Arguments --
4914 ----------------------------------
4916 procedure Remove_Controlling_Arguments
is
4917 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
;
4918 -- Reset the Controlling_Argument of calls to nonabstract
4921 ---------------------
4922 -- Remove_Ctrl_Arg --
4923 ---------------------
4925 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
is
4927 if Nkind
(N
) = N_Function_Call
4928 and then Present
(Controlling_Argument
(N
))
4929 and then not Is_Abstract_Subprogram
(Entity
(Name
(N
)))
4931 Set_Controlling_Argument
(N
, Empty
);
4935 end Remove_Ctrl_Arg
;
4937 procedure Remove_Ctrl_Args
is new Traverse_Proc
(Remove_Ctrl_Arg
);
4939 Remove_Ctrl_Args
(Expr
);
4940 end Remove_Controlling_Arguments
;
4942 -----------------------------------------
4943 -- Restore_Original_Selected_Component --
4944 -----------------------------------------
4946 procedure Restore_Original_Selected_Component
is
4947 Restored_Nodes_List
: Elist_Id
:= No_Elist
;
4949 procedure Fix_Parents
(N
: Node_Id
);
4950 -- Traverse the subtree of N fixing the Parent field of all the
4953 function Restore_Node
(N
: Node_Id
) return Traverse_Result
;
4954 -- Process dispatching calls to functions whose original node was
4955 -- a selected component, and replace them with their original
4956 -- node. Restored nodes are stored in the Restored_Nodes_List
4957 -- to fix the parent fields of their subtrees in a separate
4964 procedure Fix_Parents
(N
: Node_Id
) is
4967 (Parent_Node
: Node_Id
;
4968 Node
: Node_Id
) return Traverse_Result
;
4969 -- Process a single node
4976 (Parent_Node
: Node_Id
;
4977 Node
: Node_Id
) return Traverse_Result
4979 Par
: constant Node_Id
:= Parent
(Node
);
4982 if Par
/= Parent_Node
then
4983 if Is_List_Member
(Node
) then
4984 Set_List_Parent
(List_Containing
(Node
), Parent_Node
);
4986 Set_Parent
(Node
, Parent_Node
);
4993 procedure Fix_Parents
is
4994 new Traverse_Proc_With_Parent
(Fix_Parent
);
5004 function Restore_Node
(N
: Node_Id
) return Traverse_Result
is
5006 if Nkind
(N
) = N_Function_Call
5007 and then Nkind
(Original_Node
(N
)) = N_Selected_Component
5008 and then Is_Dispatching_Operation
(Entity
(Name
(N
)))
5010 Rewrite
(N
, Original_Node
(N
));
5011 Set_Original_Node
(N
, N
);
5013 -- Save the restored node in the Restored_Nodes_List to fix
5014 -- the parent fields of their subtrees in a separate tree
5017 Append_New_Elmt
(N
, Restored_Nodes_List
);
5023 procedure Restore_Nodes
is new Traverse_Proc
(Restore_Node
);
5025 -- Start of processing for Restore_Original_Selected_Component
5028 Restore_Nodes
(Expr
);
5030 -- After restoring the original node we must fix the decoration
5031 -- of the Parent attribute to ensure tree consistency; required
5032 -- because when the class-wide condition is inherited, calls to
5033 -- New_Copy_Tree will perform copies of this subtree, and formal
5034 -- occurrences with wrong Parent field cannot be mapped to the
5037 if Present
(Restored_Nodes_List
) then
5039 Elmt
: Elmt_Id
:= First_Elmt
(Restored_Nodes_List
);
5042 while Present
(Elmt
) loop
5043 Fix_Parents
(Node
(Elmt
));
5048 end Restore_Original_Selected_Component
;
5050 -- Start of processing for Preanalyze_Condition
5053 pragma Assert
(Present
(Expr
));
5054 pragma Assert
(Inside_Class_Condition_Preanalysis
= False);
5057 Install_Formals
(Subp
);
5058 Inside_Class_Condition_Preanalysis
:= True;
5060 Preanalyze_Spec_Expression
(Expr
, Standard_Boolean
);
5062 Inside_Class_Condition_Preanalysis
:= False;
5065 -- If this preanalyzed condition has occurrences of dispatching calls
5066 -- using the Object.Operation notation, during preanalysis such calls
5067 -- are rewritten as dispatching function calls; if at later stages
5068 -- this condition is inherited we must have restored the original
5069 -- selected-component node to ensure that the preanalysis of the
5070 -- inherited condition rewrites these dispatching calls in the
5071 -- correct context to avoid reporting spurious errors.
5073 Restore_Original_Selected_Component
;
5075 -- Traverse Expr and clear the Controlling_Argument of calls to
5076 -- nonabstract functions. Required since the preanalyzed condition
5077 -- is not yet installed on its definite context and will be cloned
5078 -- and extended in derivations with additional conditions.
5080 Remove_Controlling_Arguments
;
5082 -- Clear also attribute Unset_Reference; again because preanalysis
5083 -- occurs in a place unrelated to the actual code.
5085 Clear_Unset_References
;
5086 end Preanalyze_Condition
;
5088 ----------------------------------------
5089 -- Save_Global_References_In_Contract --
5090 ----------------------------------------
5092 procedure Save_Global_References_In_Contract
5096 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
5097 -- Save all global references in contract-related source pragmas found
5098 -- in the list, starting with pragma First_Prag.
5100 ------------------------------------
5101 -- Save_Global_References_In_List --
5102 ------------------------------------
5104 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
5105 Prag
: Node_Id
:= First_Prag
;
5108 while Present
(Prag
) loop
5109 if Is_Generic_Contract_Pragma
(Prag
) then
5110 Save_Global_References
(Prag
);
5113 Prag
:= Next_Pragma
(Prag
);
5115 end Save_Global_References_In_List
;
5119 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
5121 -- Start of processing for Save_Global_References_In_Contract
5124 -- The entity of the analyzed generic copy must be on the scope stack
5125 -- to ensure proper detection of global references.
5127 Push_Scope
(Gen_Id
);
5129 if Permits_Aspect_Specifications
(Templ
)
5130 and then Has_Aspects
(Templ
)
5132 Save_Global_References_In_Aspects
(Templ
);
5135 if Present
(Items
) then
5136 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
5137 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
5138 Save_Global_References_In_List
(Classifications
(Items
));
5142 end Save_Global_References_In_Contract
;
5144 -------------------------
5145 -- Set_Class_Condition --
5146 -------------------------
5148 procedure Set_Class_Condition
5149 (Kind
: Condition_Kind
;
5155 when Class_Postcondition
=>
5156 Set_Class_Postconditions
(Subp
, Cond
);
5158 when Class_Precondition
=>
5159 Set_Class_Preconditions
(Subp
, Cond
);
5161 when Ignored_Class_Postcondition
=>
5162 Set_Ignored_Class_Postconditions
(Subp
, Cond
);
5164 when Ignored_Class_Precondition
=>
5165 Set_Ignored_Class_Preconditions
(Subp
, Cond
);
5167 end Set_Class_Condition
;