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 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
);
66 -- Analyze all delayed pragmas chained on the contract of package
67 -- instantiation Inst_Id as if they appear at the end of a declarative
68 -- region. The pragmas in question are:
72 procedure Build_Subprogram_Contract_Wrapper
77 -- Generate a wrapper for a given subprogram body when the expansion of
78 -- postconditions require it by moving its declarations and statements
79 -- into a locally declared subprogram _Wrapped_Statements.
81 -- Postcondition and precondition checks then get inserted in place of
82 -- the original statements and declarations along with a call to
83 -- _Wrapped_Statements.
85 procedure Check_Class_Condition
89 Is_Precondition
: Boolean);
90 -- Perform checking of class-wide pre/postcondition Cond inherited by Subp
91 -- from Par_Subp. Is_Precondition enables check specific for preconditions.
92 -- In SPARK_Mode, an inherited operation that is not overridden but has
93 -- inherited modified conditions pre/postconditions is illegal.
95 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean;
96 -- Determine whether arbitrary declaration Decl denotes a renaming of
97 -- a discriminant or protection field _object.
99 procedure Check_Type_Or_Object_External_Properties
100 (Type_Or_Obj_Id
: Entity_Id
);
101 -- Perform checking of external properties pragmas that is common to both
102 -- type declarations and object declarations.
104 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
);
105 -- Expand the contracts of a subprogram body and its correspoding spec (if
106 -- any). This routine processes all [refined] pre- and postconditions as
107 -- well as Contract_Cases, Subprogram_Variant, invariants and predicates.
108 -- Body_Id denotes the entity of the subprogram body.
110 procedure Preanalyze_Condition
113 -- Preanalyze the class-wide condition Expr of Subp
115 procedure Set_Class_Condition
116 (Kind
: Condition_Kind
;
119 -- Set the class-wide Kind condition of Subp
121 -----------------------
122 -- Add_Contract_Item --
123 -----------------------
125 procedure Add_Contract_Item
(Prag
: Node_Id
; Id
: Entity_Id
) is
126 Items
: Node_Id
:= Contract
(Id
);
128 procedure Add_Classification
;
129 -- Prepend Prag to the list of classifications
131 procedure Add_Contract_Test_Case
;
132 -- Prepend Prag to the list of contract and test cases
134 procedure Add_Pre_Post_Condition
;
135 -- Prepend Prag to the list of pre- and postconditions
137 ------------------------
138 -- Add_Classification --
139 ------------------------
141 procedure Add_Classification
is
143 Set_Next_Pragma
(Prag
, Classifications
(Items
));
144 Set_Classifications
(Items
, Prag
);
145 end Add_Classification
;
147 ----------------------------
148 -- Add_Contract_Test_Case --
149 ----------------------------
151 procedure Add_Contract_Test_Case
is
153 Set_Next_Pragma
(Prag
, Contract_Test_Cases
(Items
));
154 Set_Contract_Test_Cases
(Items
, Prag
);
155 end Add_Contract_Test_Case
;
157 ----------------------------
158 -- Add_Pre_Post_Condition --
159 ----------------------------
161 procedure Add_Pre_Post_Condition
is
163 Set_Next_Pragma
(Prag
, Pre_Post_Conditions
(Items
));
164 Set_Pre_Post_Conditions
(Items
, Prag
);
165 end Add_Pre_Post_Condition
;
169 -- A contract must contain only pragmas
171 pragma Assert
(Nkind
(Prag
) = N_Pragma
);
172 Prag_Nam
: constant Name_Id
:= Pragma_Name
(Prag
);
174 -- Start of processing for Add_Contract_Item
177 -- Create a new contract when adding the first item
180 Items
:= Make_Contract
(Sloc
(Id
));
181 Set_Contract
(Id
, Items
);
184 -- Constants, the applicable pragmas are:
187 if Ekind
(Id
) = E_Constant
then
188 if Prag_Nam
in Name_Async_Readers
190 | Name_Effective_Reads
191 | Name_Effective_Writes
197 -- The pragma is not a proper contract item
203 -- Entry bodies, the applicable pragmas are:
208 elsif Is_Entry_Body
(Id
) then
209 if Prag_Nam
in Name_Refined_Depends | Name_Refined_Global
then
212 elsif Prag_Nam
= Name_Refined_Post
then
213 Add_Pre_Post_Condition
;
215 -- The pragma is not a proper contract item
221 -- Entry or subprogram declarations, the applicable pragmas are:
225 -- Extensions_Visible
233 elsif Is_Entry_Declaration
(Id
)
234 or else Ekind
(Id
) in E_Function
236 | E_Generic_Procedure
239 if Prag_Nam
in Name_Attach_Handler | Name_Interrupt_Handler
240 and then Ekind
(Id
) in E_Generic_Procedure | E_Procedure
244 elsif Prag_Nam
in Name_Depends
245 | Name_Extensions_Visible
250 elsif Prag_Nam
= Name_Volatile_Function
251 and then Ekind
(Id
) in E_Function | E_Generic_Function
255 elsif Prag_Nam
in Name_Contract_Cases
256 | Name_Subprogram_Variant
259 Add_Contract_Test_Case
;
261 elsif Prag_Nam
in Name_Postcondition | Name_Precondition
then
262 Add_Pre_Post_Condition
;
264 -- The pragma is not a proper contract item
270 -- Packages or instantiations, the applicable pragmas are:
274 -- Part_Of (instantiation only)
276 elsif Is_Package_Or_Generic_Package
(Id
) then
277 if Prag_Nam
in Name_Abstract_State
278 | Name_Initial_Condition
283 -- Indicator Part_Of must be associated with a package instantiation
285 elsif Prag_Nam
= Name_Part_Of
and then Is_Generic_Instance
(Id
) then
288 -- The pragma is not a proper contract item
294 -- Package bodies, the applicable pragmas are:
297 elsif Ekind
(Id
) = E_Package_Body
then
298 if Prag_Nam
= Name_Refined_State
then
301 -- The pragma is not a proper contract item
307 -- The four volatility refinement pragmas are ok for all types.
308 -- Part_Of is ok for task types and protected types.
309 -- Depends and Global are ok for task types.
311 elsif Is_Type
(Id
) then
313 Is_OK
: constant Boolean :=
314 Prag_Nam
in Name_Async_Readers
316 | Name_Effective_Reads
317 | Name_Effective_Writes
319 or else (Ekind
(Id
) = E_Task_Type
320 and Prag_Nam
in Name_Part_Of
323 or else (Ekind
(Id
) = E_Protected_Type
324 and Prag_Nam
= Name_Part_Of
);
330 -- The pragma is not a proper contract item
336 -- Subprogram bodies, the applicable pragmas are:
343 elsif Ekind
(Id
) = E_Subprogram_Body
then
344 if Prag_Nam
in Name_Refined_Depends | Name_Refined_Global
then
347 elsif Prag_Nam
in Name_Postcondition
351 Add_Pre_Post_Condition
;
353 -- The pragma is not a proper contract item
359 -- Task bodies, the applicable pragmas are:
363 elsif Ekind
(Id
) = E_Task_Body
then
364 if Prag_Nam
in Name_Refined_Depends | Name_Refined_Global
then
367 -- The pragma is not a proper contract item
373 -- Task units, the applicable pragmas are:
378 -- Variables, the applicable pragmas are:
381 -- Constant_After_Elaboration
389 elsif Ekind
(Id
) = E_Variable
then
390 if Prag_Nam
in Name_Async_Readers
392 | Name_Constant_After_Elaboration
394 | Name_Effective_Reads
395 | Name_Effective_Writes
402 -- The pragma is not a proper contract item
411 end Add_Contract_Item
;
413 -----------------------
414 -- Analyze_Contracts --
415 -----------------------
417 procedure Analyze_Contracts
(L
: List_Id
) is
422 while Present
(Decl
) loop
424 -- Entry or subprogram declarations
426 if Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
427 | N_Entry_Declaration
428 | N_Generic_Subprogram_Declaration
429 | N_Subprogram_Declaration
431 Analyze_Entry_Or_Subprogram_Contract
(Defining_Entity
(Decl
));
433 -- Entry or subprogram bodies
435 elsif Nkind
(Decl
) in N_Entry_Body | N_Subprogram_Body
then
436 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
440 elsif Nkind
(Decl
) = N_Object_Declaration
then
441 Analyze_Object_Contract
(Defining_Entity
(Decl
));
443 -- Package instantiation
445 elsif Nkind
(Decl
) = N_Package_Instantiation
then
446 Analyze_Package_Instantiation_Contract
(Defining_Entity
(Decl
));
450 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
451 | N_Single_Protected_Declaration
453 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
455 -- Subprogram body stubs
457 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
458 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
462 elsif Nkind
(Decl
) in N_Single_Task_Declaration
463 | N_Task_Type_Declaration
465 Analyze_Task_Contract
(Defining_Entity
(Decl
));
467 -- For type declarations, we need to do the preanalysis of Iterable
468 -- and the 3 Xxx_Literal aspect specifications.
470 -- Other type aspects need to be resolved here???
472 elsif Nkind
(Decl
) = N_Private_Type_Declaration
473 and then Present
(Aspect_Specifications
(Decl
))
476 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
477 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
478 I_Lit
: constant Node_Id
:=
479 Find_Aspect
(E
, Aspect_Integer_Literal
);
480 R_Lit
: constant Node_Id
:=
481 Find_Aspect
(E
, Aspect_Real_Literal
);
482 S_Lit
: constant Node_Id
:=
483 Find_Aspect
(E
, Aspect_String_Literal
);
487 Validate_Iterable_Aspect
(E
, It
);
490 if Present
(I_Lit
) then
491 Validate_Literal_Aspect
(E
, I_Lit
);
493 if Present
(R_Lit
) then
494 Validate_Literal_Aspect
(E
, R_Lit
);
496 if Present
(S_Lit
) then
497 Validate_Literal_Aspect
(E
, S_Lit
);
502 if Nkind
(Decl
) in N_Full_Type_Declaration
503 | N_Private_Type_Declaration
504 | N_Task_Type_Declaration
505 | N_Protected_Type_Declaration
506 | N_Formal_Type_Declaration
508 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
513 end Analyze_Contracts
;
515 -------------------------------------
516 -- Analyze_Pragmas_In_Declarations --
517 -------------------------------------
519 procedure Analyze_Pragmas_In_Declarations
(Body_Id
: Entity_Id
) is
523 -- Move through the body's declarations analyzing all pragmas which
524 -- appear at the top of the declarations.
526 Curr_Decl
:= First
(Declarations
(Unit_Declaration_Node
(Body_Id
)));
527 while Present
(Curr_Decl
) loop
529 if Nkind
(Curr_Decl
) = N_Pragma
then
531 if Pragma_Significant_To_Subprograms
532 (Get_Pragma_Id
(Curr_Decl
))
537 -- Skip the renamings of discriminants and protection fields
539 elsif Is_Prologue_Renaming
(Curr_Decl
) then
542 -- We have reached something which is not a pragma so we can be sure
543 -- there are no more contracts or pragmas which need to be taken into
552 end Analyze_Pragmas_In_Declarations
;
554 -----------------------------------------------
555 -- Analyze_Entry_Or_Subprogram_Body_Contract --
556 -----------------------------------------------
558 -- WARNING: This routine manages SPARK regions. Return statements must be
559 -- replaced by gotos which jump to the end of the routine and restore the
562 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
563 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
564 Items
: constant Node_Id
:= Contract
(Body_Id
);
565 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
567 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
568 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
569 -- Save the SPARK_Mode-related data to restore on exit
572 -- When a subprogram body declaration is illegal, its defining entity is
573 -- left unanalyzed. There is nothing left to do in this case because the
574 -- body lacks a contract, or even a proper Ekind.
576 if Ekind
(Body_Id
) = E_Void
then
579 -- Do not analyze a contract multiple times
581 elsif Present
(Items
) then
582 if Analyzed
(Items
) then
585 Set_Analyzed
(Items
);
589 -- Due to the timing of contract analysis, delayed pragmas may be
590 -- subject to the wrong SPARK_Mode, usually that of the enclosing
591 -- context. To remedy this, restore the original SPARK_Mode of the
592 -- related subprogram body.
594 Set_SPARK_Mode
(Body_Id
);
596 -- Ensure that the contract cases or postconditions mention 'Result or
597 -- define a post-state.
599 Check_Result_And_Post_State
(Body_Id
);
601 -- A stand-alone nonvolatile function body cannot have an effectively
602 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
603 -- check is relevant only when SPARK_Mode is on, as it is not a standard
604 -- legality rule. The check is performed here because Volatile_Function
605 -- is processed after the analysis of the related subprogram body. The
606 -- check only applies to source subprograms and not to generated TSS
610 and then Ekind
(Body_Id
) in E_Function | E_Generic_Function
611 and then Comes_From_Source
(Spec_Id
)
612 and then not Is_Volatile_Function
(Body_Id
)
614 Check_Nonvolatile_Function_Profile
(Body_Id
);
617 -- Restore the SPARK_Mode of the enclosing context after all delayed
618 -- pragmas have been analyzed.
620 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
622 -- Capture all global references in a generic subprogram body now that
623 -- the contract has been analyzed.
625 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
626 Save_Global_References_In_Contract
627 (Templ
=> Original_Node
(Body_Decl
),
631 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
632 -- Subprogram_Variant, invariants and predicates associated with body
633 -- and its spec. Do not expand the contract of subprogram body stubs.
635 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
636 Expand_Subprogram_Contract
(Body_Id
);
638 end Analyze_Entry_Or_Subprogram_Body_Contract
;
640 ------------------------------------------
641 -- Analyze_Entry_Or_Subprogram_Contract --
642 ------------------------------------------
644 -- WARNING: This routine manages SPARK regions. Return statements must be
645 -- replaced by gotos which jump to the end of the routine and restore the
648 procedure Analyze_Entry_Or_Subprogram_Contract
649 (Subp_Id
: Entity_Id
;
650 Freeze_Id
: Entity_Id
:= Empty
)
652 Items
: constant Node_Id
:= Contract
(Subp_Id
);
653 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
655 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
656 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
657 -- Save the SPARK_Mode-related data to restore on exit
659 Skip_Assert_Exprs
: constant Boolean :=
660 Is_Entry
(Subp_Id
) and then not GNATprove_Mode
;
662 Depends
: Node_Id
:= Empty
;
663 Global
: Node_Id
:= Empty
;
668 -- Do not analyze a contract multiple times
670 if Present
(Items
) then
671 if Analyzed
(Items
) then
674 Set_Analyzed
(Items
);
678 -- Due to the timing of contract analysis, delayed pragmas may be
679 -- subject to the wrong SPARK_Mode, usually that of the enclosing
680 -- context. To remedy this, restore the original SPARK_Mode of the
681 -- related subprogram body.
683 Set_SPARK_Mode
(Subp_Id
);
685 -- All subprograms carry a contract, but for some it is not significant
686 -- and should not be processed.
688 if not Has_Significant_Contract
(Subp_Id
) then
691 elsif Present
(Items
) then
693 -- Do not analyze the pre/postconditions of an entry declaration
694 -- unless annotating the original tree for GNATprove. The
695 -- real analysis occurs when the pre/postconditons are relocated to
696 -- the contract wrapper procedure (see Build_Contract_Wrapper).
698 if Skip_Assert_Exprs
then
701 -- Otherwise analyze the pre/postconditions.
702 -- If these come from an aspect specification, their expressions
703 -- might include references to types that are not frozen yet, in the
704 -- case where the body is a rewritten expression function that is a
705 -- completion, so freeze all types within before constructing the
710 Bod
: Node_Id
:= Empty
;
711 Freeze_Types
: Boolean := False;
714 if Present
(Freeze_Id
) then
715 Bod
:= Unit_Declaration_Node
(Freeze_Id
);
717 if Nkind
(Bod
) = N_Subprogram_Body
718 and then Was_Expression_Function
(Bod
)
719 and then Ekind
(Subp_Id
) = E_Function
720 and then Chars
(Subp_Id
) = Chars
(Freeze_Id
)
721 and then Subp_Id
/= Freeze_Id
723 Freeze_Types
:= True;
727 Prag
:= Pre_Post_Conditions
(Items
);
728 while Present
(Prag
) loop
730 and then Present
(Corresponding_Aspect
(Prag
))
734 Typ
=> Standard_Boolean
,
737 (First
(Pragma_Argument_Associations
(Prag
))),
741 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
742 Prag
:= Next_Pragma
(Prag
);
747 -- Analyze contract-cases, subprogram-variant and test-cases
749 Prag
:= Contract_Test_Cases
(Items
);
750 while Present
(Prag
) loop
751 Prag_Nam
:= Pragma_Name
(Prag
);
753 if Prag_Nam
= Name_Contract_Cases
then
755 -- Do not analyze the contract cases of an entry declaration
756 -- unless annotating the original tree for GNATprove.
757 -- The real analysis occurs when the contract cases are moved
758 -- to the contract wrapper procedure (Build_Contract_Wrapper).
760 if Skip_Assert_Exprs
then
763 -- Otherwise analyze the contract cases
766 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
769 elsif Prag_Nam
= Name_Subprogram_Variant
then
770 Analyze_Subprogram_Variant_In_Decl_Part
(Prag
);
773 pragma Assert
(Prag_Nam
= Name_Test_Case
);
774 Analyze_Test_Case_In_Decl_Part
(Prag
);
777 Prag
:= Next_Pragma
(Prag
);
780 -- Analyze classification pragmas
782 Prag
:= Classifications
(Items
);
783 while Present
(Prag
) loop
784 Prag_Nam
:= Pragma_Name
(Prag
);
786 if Prag_Nam
= Name_Depends
then
789 elsif Prag_Nam
= Name_Global
then
793 Prag
:= Next_Pragma
(Prag
);
796 -- Analyze Global first, as Depends may mention items classified in
797 -- the global categorization.
799 if Present
(Global
) then
800 Analyze_Global_In_Decl_Part
(Global
);
803 -- Depends must be analyzed after Global in order to see the modes of
806 if Present
(Depends
) then
807 Analyze_Depends_In_Decl_Part
(Depends
);
810 -- Ensure that the contract cases or postconditions mention 'Result
811 -- or define a post-state.
813 Check_Result_And_Post_State
(Subp_Id
);
816 -- A nonvolatile function cannot have an effectively volatile formal
817 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
818 -- only when SPARK_Mode is on, as it is not a standard legality rule.
819 -- The check is performed here because pragma Volatile_Function is
820 -- processed after the analysis of the related subprogram declaration.
823 and then Ekind
(Subp_Id
) in E_Function | E_Generic_Function
824 and then Comes_From_Source
(Subp_Id
)
825 and then not Is_Volatile_Function
(Subp_Id
)
827 Check_Nonvolatile_Function_Profile
(Subp_Id
);
830 -- Restore the SPARK_Mode of the enclosing context after all delayed
831 -- pragmas have been analyzed.
833 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
835 -- Capture all global references in a generic subprogram now that the
836 -- contract has been analyzed.
838 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
839 Save_Global_References_In_Contract
840 (Templ
=> Original_Node
(Subp_Decl
),
843 end Analyze_Entry_Or_Subprogram_Contract
;
845 ----------------------------------------------
846 -- Check_Type_Or_Object_External_Properties --
847 ----------------------------------------------
849 procedure Check_Type_Or_Object_External_Properties
850 (Type_Or_Obj_Id
: Entity_Id
)
852 Is_Type_Id
: constant Boolean := Is_Type
(Type_Or_Obj_Id
);
853 Decl_Kind
: constant String :=
854 (if Is_Type_Id
then "type" else "object");
858 AR_Val
: Boolean := False;
859 AW_Val
: Boolean := False;
860 ER_Val
: Boolean := False;
861 EW_Val
: Boolean := False;
863 Seen
: Boolean := False;
867 -- Start of processing for Check_Type_Or_Object_External_Properties
870 -- Analyze all external properties
873 Obj_Typ
:= Type_Or_Obj_Id
;
875 -- If the parent type of a derived type is volatile
876 -- then the derived type inherits volatility-related flags.
878 if Is_Derived_Type
(Type_Or_Obj_Id
) then
880 Parent_Type
: constant Entity_Id
:=
881 Etype
(Base_Type
(Type_Or_Obj_Id
));
883 if Is_Effectively_Volatile
(Parent_Type
) then
884 AR_Val
:= Async_Readers_Enabled
(Parent_Type
);
885 AW_Val
:= Async_Writers_Enabled
(Parent_Type
);
886 ER_Val
:= Effective_Reads_Enabled
(Parent_Type
);
887 EW_Val
:= Effective_Writes_Enabled
(Parent_Type
);
892 Obj_Typ
:= Etype
(Type_Or_Obj_Id
);
895 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Readers
);
897 if Present
(Prag
) then
899 Saved_AR_Val
: constant Boolean := AR_Val
;
901 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
903 if Saved_AR_Val
and not AR_Val
then
905 ("illegal non-confirming Async_Readers specification",
911 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Async_Writers
);
913 if Present
(Prag
) then
915 Saved_AW_Val
: constant Boolean := AW_Val
;
917 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
919 if Saved_AW_Val
and not AW_Val
then
921 ("illegal non-confirming Async_Writers specification",
927 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Reads
);
929 if Present
(Prag
) then
931 Saved_ER_Val
: constant Boolean := ER_Val
;
933 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
935 if Saved_ER_Val
and not ER_Val
then
937 ("illegal non-confirming Effective_Reads specification",
943 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_Effective_Writes
);
945 if Present
(Prag
) then
947 Saved_EW_Val
: constant Boolean := EW_Val
;
949 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
951 if Saved_EW_Val
and not EW_Val
then
953 ("illegal non-confirming Effective_Writes specification",
959 -- Verify the mutual interaction of the various external properties.
960 -- For types and variables for which No_Caching is enabled, it has been
961 -- checked already that only False values for other external properties
965 and then not No_Caching_Enabled
(Type_Or_Obj_Id
)
967 Check_External_Properties
968 (Type_Or_Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
971 -- Analyze the non-external volatility property No_Caching
973 Prag
:= Get_Pragma
(Type_Or_Obj_Id
, Pragma_No_Caching
);
975 if Present
(Prag
) then
976 Analyze_External_Property_In_Decl_Part
(Prag
, NC_Val
);
979 -- The following checks are relevant only when SPARK_Mode is on, as
980 -- they are not standard Ada legality rules. Internally generated
981 -- temporaries are ignored, as well as return objects.
984 and then Comes_From_Source
(Type_Or_Obj_Id
)
985 and then not Is_Return_Object
(Type_Or_Obj_Id
)
987 if Is_Effectively_Volatile
(Type_Or_Obj_Id
) then
989 -- The declaration of an effectively volatile object or type must
990 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
992 if not Is_Library_Level_Entity
(Type_Or_Obj_Id
) then
994 ("effectively volatile "
996 & " & must be declared at library level "
997 & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id
);
999 -- An object of a discriminated type cannot be effectively
1000 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
1002 elsif Has_Discriminants
(Obj_Typ
)
1003 and then not Is_Protected_Type
(Obj_Typ
)
1006 ("discriminated " & Decl_Kind
& " & cannot be volatile",
1010 -- An object decl shall be compatible with respect to volatility
1011 -- with its type (SPARK RM 7.1.3(2)).
1013 if not Is_Type_Id
then
1014 if Is_Effectively_Volatile
(Obj_Typ
) then
1015 Check_Volatility_Compatibility
1016 (Type_Or_Obj_Id
, Obj_Typ
,
1017 "volatile object", "its type",
1018 Srcpos_Bearer
=> Type_Or_Obj_Id
);
1021 -- A component of a composite type (in this case, the composite
1022 -- type is an array type) shall be compatible with respect to
1023 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1025 elsif Is_Array_Type
(Obj_Typ
) then
1026 Check_Volatility_Compatibility
1027 (Component_Type
(Obj_Typ
), Obj_Typ
,
1028 "component type", "its enclosing array type",
1029 Srcpos_Bearer
=> Obj_Typ
);
1031 -- A component of a composite type (in this case, the composite
1032 -- type is a record type) shall be compatible with respect to
1033 -- volatility with the composite type (SPARK RM 7.1.3(6)).
1035 elsif Is_Record_Type
(Obj_Typ
) then
1037 Comp
: Entity_Id
:= First_Component
(Obj_Typ
);
1039 while Present
(Comp
) loop
1040 Check_Volatility_Compatibility
1041 (Etype
(Comp
), Obj_Typ
,
1042 "record component " & Get_Name_String
(Chars
(Comp
)),
1043 "its enclosing record type",
1044 Srcpos_Bearer
=> Comp
);
1045 Next_Component
(Comp
);
1050 -- The type or object is not effectively volatile
1053 -- A non-effectively volatile type cannot have effectively
1054 -- volatile components (SPARK RM 7.1.3(6)).
1057 and then not Is_Effectively_Volatile
(Type_Or_Obj_Id
)
1058 and then Has_Effectively_Volatile_Component
(Type_Or_Obj_Id
)
1061 ("non-volatile type & cannot have effectively volatile"
1067 end Check_Type_Or_Object_External_Properties
;
1069 -----------------------------
1070 -- Analyze_Object_Contract --
1071 -----------------------------
1073 -- WARNING: This routine manages SPARK regions. Return statements must be
1074 -- replaced by gotos which jump to the end of the routine and restore the
1077 procedure Analyze_Object_Contract
1078 (Obj_Id
: Entity_Id
;
1079 Freeze_Id
: Entity_Id
:= Empty
)
1081 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
1083 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1084 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1085 -- Save the SPARK_Mode-related data to restore on exit
1092 -- The loop parameter in an element iterator over a formal container
1093 -- is declared with an object declaration, but no contracts apply.
1095 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
1099 -- Do not analyze a contract multiple times
1101 Items
:= Contract
(Obj_Id
);
1103 if Present
(Items
) then
1104 if Analyzed
(Items
) then
1107 Set_Analyzed
(Items
);
1111 -- The anonymous object created for a single concurrent type inherits
1112 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
1113 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
1114 -- of the enclosing context. To remedy this, restore the original mode
1115 -- of the related anonymous object.
1117 if Is_Single_Concurrent_Object
(Obj_Id
)
1118 and then Present
(SPARK_Pragma
(Obj_Id
))
1120 Set_SPARK_Mode
(Obj_Id
);
1123 -- Checks related to external properties, same for constants and
1126 Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id
=> Obj_Id
);
1128 -- Constant-related checks
1130 if Ekind
(Obj_Id
) = E_Constant
then
1132 -- Analyze indicator Part_Of
1134 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1136 -- Check whether the lack of indicator Part_Of agrees with the
1137 -- placement of the constant with respect to the state space.
1140 Check_Missing_Part_Of
(Obj_Id
);
1143 -- Variable-related checks
1145 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
1147 -- The anonymous object created for a single task type carries
1148 -- pragmas Depends and Global of the type.
1150 if Is_Single_Task_Object
(Obj_Id
) then
1152 -- Analyze Global first, as Depends may mention items classified
1153 -- in the global categorization.
1155 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
1157 if Present
(Prag
) then
1158 Analyze_Global_In_Decl_Part
(Prag
);
1161 -- Depends must be analyzed after Global in order to see the modes
1162 -- of all global items.
1164 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
1166 if Present
(Prag
) then
1167 Analyze_Depends_In_Decl_Part
(Prag
);
1171 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
1173 -- Analyze indicator Part_Of
1175 if Present
(Prag
) then
1176 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
1178 -- The variable is a constituent of a single protected/task type
1179 -- and behaves as a component of the type. Verify that references
1180 -- to the variable occur within the definition or body of the type
1183 if Present
(Encapsulating_State
(Obj_Id
))
1184 and then Is_Single_Concurrent_Object
1185 (Encapsulating_State
(Obj_Id
))
1186 and then Present
(Part_Of_References
(Obj_Id
))
1188 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
1189 while Present
(Ref_Elmt
) loop
1190 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
1191 Next_Elmt
(Ref_Elmt
);
1195 -- Otherwise check whether the lack of indicator Part_Of agrees with
1196 -- the placement of the variable with respect to the state space.
1199 Check_Missing_Part_Of
(Obj_Id
);
1205 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
1207 -- A Ghost object cannot be of a type that yields a synchronized
1208 -- object (SPARK RM 6.9(19)).
1210 if Yields_Synchronized_Object
(Obj_Typ
) then
1211 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
1213 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
1214 -- SPARK RM 6.9(19)).
1216 elsif SPARK_Mode
= On
and then Is_Effectively_Volatile
(Obj_Id
) then
1217 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
1219 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
1220 -- One exception to this is the object that represents the dispatch
1221 -- table of a Ghost tagged type, as the symbol needs to be exported.
1223 elsif Is_Exported
(Obj_Id
) then
1224 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
1226 elsif Is_Imported
(Obj_Id
) then
1227 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
1231 -- Restore the SPARK_Mode of the enclosing context after all delayed
1232 -- pragmas have been analyzed.
1234 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1235 end Analyze_Object_Contract
;
1237 -----------------------------------
1238 -- Analyze_Package_Body_Contract --
1239 -----------------------------------
1241 -- WARNING: This routine manages SPARK regions. Return statements must be
1242 -- replaced by gotos which jump to the end of the routine and restore the
1245 procedure Analyze_Package_Body_Contract
1246 (Body_Id
: Entity_Id
;
1247 Freeze_Id
: Entity_Id
:= Empty
)
1249 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1250 Items
: constant Node_Id
:= Contract
(Body_Id
);
1251 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
1253 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1254 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1255 -- Save the SPARK_Mode-related data to restore on exit
1257 Ref_State
: Node_Id
;
1260 -- Do not analyze a contract multiple times
1262 if Present
(Items
) then
1263 if Analyzed
(Items
) then
1266 Set_Analyzed
(Items
);
1270 -- Due to the timing of contract analysis, delayed pragmas may be
1271 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1272 -- context. To remedy this, restore the original SPARK_Mode of the
1273 -- related package body.
1275 Set_SPARK_Mode
(Body_Id
);
1277 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
1279 -- The analysis of pragma Refined_State detects whether the spec has
1280 -- abstract states available for refinement.
1282 if Present
(Ref_State
) then
1283 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
1286 -- Restore the SPARK_Mode of the enclosing context after all delayed
1287 -- pragmas have been analyzed.
1289 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1291 -- Capture all global references in a generic package body now that the
1292 -- contract has been analyzed.
1294 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1295 Save_Global_References_In_Contract
1296 (Templ
=> Original_Node
(Body_Decl
),
1299 end Analyze_Package_Body_Contract
;
1301 ------------------------------
1302 -- Analyze_Package_Contract --
1303 ------------------------------
1305 -- WARNING: This routine manages SPARK regions. Return statements must be
1306 -- replaced by gotos which jump to the end of the routine and restore the
1309 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1310 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1311 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1313 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1314 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1315 -- Save the SPARK_Mode-related data to restore on exit
1317 Init
: Node_Id
:= Empty
;
1318 Init_Cond
: Node_Id
:= Empty
;
1323 -- Do not analyze a contract multiple times
1325 if Present
(Items
) then
1326 if Analyzed
(Items
) then
1329 -- Do not analyze the contract of the internal package
1330 -- created to check conformance of an actual package.
1331 -- Such an internal package is removed from the tree after
1332 -- legality checks are completed, and it does not contain
1333 -- the declarations of all local entities of the generic.
1335 elsif Is_Internal
(Pack_Id
)
1336 and then Is_Generic_Instance
(Pack_Id
)
1341 Set_Analyzed
(Items
);
1345 -- Due to the timing of contract analysis, delayed pragmas may be
1346 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1347 -- context. To remedy this, restore the original SPARK_Mode of the
1350 Set_SPARK_Mode
(Pack_Id
);
1352 if Present
(Items
) then
1354 -- Locate and store pragmas Initial_Condition and Initializes, since
1355 -- their order of analysis matters.
1357 Prag
:= Classifications
(Items
);
1358 while Present
(Prag
) loop
1359 Prag_Nam
:= Pragma_Name
(Prag
);
1361 if Prag_Nam
= Name_Initial_Condition
then
1364 elsif Prag_Nam
= Name_Initializes
then
1368 Prag
:= Next_Pragma
(Prag
);
1371 -- Analyze the initialization-related pragmas. Initializes must come
1372 -- before Initial_Condition due to item dependencies.
1374 if Present
(Init
) then
1375 Analyze_Initializes_In_Decl_Part
(Init
);
1378 if Present
(Init_Cond
) then
1379 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1383 -- Restore the SPARK_Mode of the enclosing context after all delayed
1384 -- pragmas have been analyzed.
1386 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1388 -- Capture all global references in a generic package now that the
1389 -- contract has been analyzed.
1391 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1392 Save_Global_References_In_Contract
1393 (Templ
=> Original_Node
(Pack_Decl
),
1396 end Analyze_Package_Contract
;
1398 --------------------------------------------
1399 -- Analyze_Package_Instantiation_Contract --
1400 --------------------------------------------
1402 -- WARNING: This routine manages SPARK regions. Return statements must be
1403 -- replaced by gotos which jump to the end of the routine and restore the
1406 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
) is
1407 Inst_Spec
: constant Node_Id
:=
1408 Instance_Spec
(Unit_Declaration_Node
(Inst_Id
));
1410 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1411 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1412 -- Save the SPARK_Mode-related data to restore on exit
1414 Pack_Id
: Entity_Id
;
1418 -- Nothing to do when the package instantiation is erroneous or left
1419 -- partially decorated.
1421 if No
(Inst_Spec
) then
1425 Pack_Id
:= Defining_Entity
(Inst_Spec
);
1426 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1428 -- Due to the timing of contract analysis, delayed pragmas may be
1429 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1430 -- context. To remedy this, restore the original SPARK_Mode of the
1433 Set_SPARK_Mode
(Pack_Id
);
1435 -- Check whether the lack of indicator Part_Of agrees with the placement
1436 -- of the package instantiation with respect to the state space. Nested
1437 -- package instantiations do not need to be checked because they inherit
1438 -- Part_Of indicator of the outermost package instantiation (see routine
1439 -- Propagate_Part_Of in Sem_Prag).
1444 elsif No
(Prag
) then
1445 Check_Missing_Part_Of
(Pack_Id
);
1448 -- Restore the SPARK_Mode of the enclosing context after all delayed
1449 -- pragmas have been analyzed.
1451 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1452 end Analyze_Package_Instantiation_Contract
;
1454 --------------------------------
1455 -- Analyze_Protected_Contract --
1456 --------------------------------
1458 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1459 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1462 -- Do not analyze a contract multiple times
1464 if Present
(Items
) then
1465 if Analyzed
(Items
) then
1468 Set_Analyzed
(Items
);
1471 end Analyze_Protected_Contract
;
1473 -------------------------------------------
1474 -- Analyze_Subprogram_Body_Stub_Contract --
1475 -------------------------------------------
1477 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1478 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1479 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1482 -- A subprogram body stub may act as its own spec or as the completion
1483 -- of a previous declaration. Depending on the context, the contract of
1484 -- the stub may contain two sets of pragmas.
1486 -- The stub is a completion, the applicable pragmas are:
1490 if Present
(Spec_Id
) then
1491 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1493 -- The stub acts as its own spec, the applicable pragmas are:
1499 -- Subprogram_Variant
1503 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1505 end Analyze_Subprogram_Body_Stub_Contract
;
1507 ---------------------------
1508 -- Analyze_Task_Contract --
1509 ---------------------------
1511 -- WARNING: This routine manages SPARK regions. Return statements must be
1512 -- replaced by gotos which jump to the end of the routine and restore the
1515 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1516 Items
: constant Node_Id
:= Contract
(Task_Id
);
1518 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1519 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1520 -- Save the SPARK_Mode-related data to restore on exit
1525 -- Do not analyze a contract multiple times
1527 if Present
(Items
) then
1528 if Analyzed
(Items
) then
1531 Set_Analyzed
(Items
);
1535 -- Due to the timing of contract analysis, delayed pragmas may be
1536 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1537 -- context. To remedy this, restore the original SPARK_Mode of the
1538 -- related task unit.
1540 Set_SPARK_Mode
(Task_Id
);
1542 -- Analyze Global first, as Depends may mention items classified in the
1543 -- global categorization.
1545 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1547 if Present
(Prag
) then
1548 Analyze_Global_In_Decl_Part
(Prag
);
1551 -- Depends must be analyzed after Global in order to see the modes of
1552 -- all global items.
1554 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1556 if Present
(Prag
) then
1557 Analyze_Depends_In_Decl_Part
(Prag
);
1560 -- Restore the SPARK_Mode of the enclosing context after all delayed
1561 -- pragmas have been analyzed.
1563 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1564 end Analyze_Task_Contract
;
1566 ---------------------------
1567 -- Analyze_Type_Contract --
1568 ---------------------------
1570 procedure Analyze_Type_Contract
(Type_Id
: Entity_Id
) is
1572 Check_Type_Or_Object_External_Properties
1573 (Type_Or_Obj_Id
=> Type_Id
);
1574 end Analyze_Type_Contract
;
1576 ---------------------------------------
1577 -- Build_Subprogram_Contract_Wrapper --
1578 ---------------------------------------
1580 procedure Build_Subprogram_Contract_Wrapper
1581 (Body_Id
: Entity_Id
;
1586 Body_Decl
: constant Entity_Id
:= Unit_Declaration_Node
(Body_Id
);
1587 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
1588 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1589 Subp_Id
: Entity_Id
;
1590 Ret_Type
: Entity_Id
;
1592 Wrapper_Id
: Entity_Id
;
1593 Wrapper_Body
: Node_Id
;
1594 Wrapper_Spec
: Node_Id
;
1597 -- When there are no postcondition statements we do not need to
1598 -- generate a wrapper.
1604 -- Obtain the related subprogram id from the body id.
1606 if Present
(Spec_Id
) then
1611 Ret_Type
:= Etype
(Subp_Id
);
1613 -- Generate the contracts wrapper by moving the original declarations
1614 -- and statements within a local subprogram, calling it and possibly
1615 -- preserving the result for the purpose of evaluating postconditions,
1616 -- contracts, type invariants, etc.
1618 -- In the case of a function, generate:
1620 -- function Original_Func (X : in out Integer) return Typ is
1621 -- <prologue renamings>
1624 -- function _Wrapped_Statements return Typ is
1625 -- <original declarations>
1627 -- <original statements>
1632 -- Result_Obj : constant Typ := _Wrapped_Statements
1634 -- <postconditions statments>
1638 -- Or else, in the case of a procedure, generate:
1640 -- procedure Original_Proc (X : in out Integer) is
1641 -- <prologue renamings>
1644 -- procedure _Wrapped_Statements is
1645 -- <original declarations>
1647 -- <original statements>
1651 -- _Wrapped_Statements;
1652 -- <postconditions statments>
1655 -- Create Identifier
1657 Wrapper_Id
:= Make_Defining_Identifier
(Loc
, Name_uWrapped_Statements
);
1658 Set_Debug_Info_Needed
(Wrapper_Id
);
1659 Set_Wrapped_Statements
(Subp_Id
, Wrapper_Id
);
1661 Set_Has_Pragma_Inline
(Wrapper_Id
, Has_Pragma_Inline
(Subp_Id
));
1662 Set_Has_Pragma_Inline_Always
1663 (Wrapper_Id
, Has_Pragma_Inline_Always
(Subp_Id
));
1665 -- Create specification and declaration for the wrapper
1667 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1669 Make_Procedure_Specification
(Loc
,
1670 Defining_Unit_Name
=> Wrapper_Id
);
1673 Make_Function_Specification
(Loc
,
1674 Defining_Unit_Name
=> Wrapper_Id
,
1675 Result_Definition
=> New_Occurrence_Of
(Ret_Type
, Loc
));
1678 -- Create the wrapper body using Body_Id's statements and declarations
1681 Make_Subprogram_Body
(Loc
,
1682 Specification
=> Wrapper_Spec
,
1683 Declarations
=> Declarations
(Body_Decl
),
1684 Handled_Statement_Sequence
=>
1685 Relocate_Node
(Handled_Statement_Sequence
(Body_Decl
)));
1687 Append_To
(Decls
, Wrapper_Body
);
1688 Set_Declarations
(Body_Decl
, Decls
);
1689 Set_Handled_Statement_Sequence
(Body_Decl
,
1690 Make_Handled_Sequence_Of_Statements
(Loc
,
1691 End_Label
=> Make_Identifier
(Loc
, Chars
(Wrapper_Id
))));
1693 -- Prepend a call to the wrapper when the subprogram is a procedure
1695 if No
(Ret_Type
) or else Ret_Type
= Standard_Void_Type
then
1697 Make_Procedure_Call_Statement
(Loc
,
1698 Name
=> New_Occurrence_Of
(Wrapper_Id
, Loc
)));
1700 (Handled_Statement_Sequence
(Body_Decl
), Stmts
);
1702 -- Generate the post-execution statements and the extended return
1703 -- when the subprogram being wrapped is a function.
1706 Set_Statements
(Handled_Statement_Sequence
(Body_Decl
), New_List
(
1707 Make_Extended_Return_Statement
(Loc
,
1708 Return_Object_Declarations
=> New_List
(
1709 Make_Object_Declaration
(Loc
,
1710 Defining_Identifier
=> Result
,
1711 Constant_Present
=> True,
1712 Object_Definition
=>
1713 New_Occurrence_Of
(Ret_Type
, Loc
),
1715 Make_Function_Call
(Loc
,
1717 New_Occurrence_Of
(Wrapper_Id
, Loc
)))),
1718 Handled_Statement_Sequence
=>
1719 Make_Handled_Sequence_Of_Statements
(Loc
,
1720 Statements
=> Stmts
))));
1722 end Build_Subprogram_Contract_Wrapper
;
1724 ----------------------------------
1725 -- Build_Entry_Contract_Wrapper --
1726 ----------------------------------
1728 procedure Build_Entry_Contract_Wrapper
(E
: Entity_Id
; Decl
: Node_Id
) is
1729 Conc_Typ
: constant Entity_Id
:= Scope
(E
);
1730 Loc
: constant Source_Ptr
:= Sloc
(E
);
1732 procedure Add_Discriminant_Renamings
1733 (Obj_Id
: Entity_Id
;
1735 -- Add renaming declarations for all discriminants of concurrent type
1736 -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
1737 -- represents the concurrent object.
1739 procedure Add_Matching_Formals
1741 Actuals
: in out List_Id
);
1742 -- Add formal parameters that match those of entry E to list Formals.
1743 -- The routine also adds matching actuals for the new formals to list
1746 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
);
1747 -- Relocate pragma Prag to list To. The routine creates a new list if
1748 -- To does not exist.
1750 --------------------------------
1751 -- Add_Discriminant_Renamings --
1752 --------------------------------
1754 procedure Add_Discriminant_Renamings
1755 (Obj_Id
: Entity_Id
;
1759 Renaming_Decl
: Node_Id
;
1762 -- Inspect the discriminants of the concurrent type and generate a
1763 -- renaming for each one.
1765 if Has_Discriminants
(Conc_Typ
) then
1766 Discr
:= First_Discriminant
(Conc_Typ
);
1767 while Present
(Discr
) loop
1769 Make_Object_Renaming_Declaration
(Loc
,
1770 Defining_Identifier
=>
1771 Make_Defining_Identifier
(Loc
, Chars
(Discr
)),
1773 New_Occurrence_Of
(Etype
(Discr
), Loc
),
1775 Make_Selected_Component
(Loc
,
1776 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
1778 Make_Identifier
(Loc
, Chars
(Discr
))));
1780 Prepend_To
(Decls
, Renaming_Decl
);
1782 Next_Discriminant
(Discr
);
1785 end Add_Discriminant_Renamings
;
1787 --------------------------
1788 -- Add_Matching_Formals --
1789 --------------------------
1791 procedure Add_Matching_Formals
1793 Actuals
: in out List_Id
)
1796 New_Formal
: Entity_Id
;
1799 -- Inspect the formal parameters of the entry and generate a new
1800 -- matching formal with the same name for the wrapper. A reference
1801 -- to the new formal becomes an actual in the entry call.
1803 Formal
:= First_Formal
(E
);
1804 while Present
(Formal
) loop
1805 New_Formal
:= Make_Defining_Identifier
(Loc
, Chars
(Formal
));
1807 Make_Parameter_Specification
(Loc
,
1808 Defining_Identifier
=> New_Formal
,
1809 In_Present
=> In_Present
(Parent
(Formal
)),
1810 Out_Present
=> Out_Present
(Parent
(Formal
)),
1812 New_Occurrence_Of
(Etype
(Formal
), Loc
)));
1814 if No
(Actuals
) then
1815 Actuals
:= New_List
;
1818 Append_To
(Actuals
, New_Occurrence_Of
(New_Formal
, Loc
));
1819 Next_Formal
(Formal
);
1821 end Add_Matching_Formals
;
1823 ---------------------
1824 -- Transfer_Pragma --
1825 ---------------------
1827 procedure Transfer_Pragma
(Prag
: Node_Id
; To
: in out List_Id
) is
1835 New_Prag
:= Relocate_Node
(Prag
);
1837 Set_Analyzed
(New_Prag
, False);
1838 Append
(New_Prag
, To
);
1839 end Transfer_Pragma
;
1843 Items
: constant Node_Id
:= Contract
(E
);
1844 Actuals
: List_Id
:= No_List
;
1847 Decls
: List_Id
:= No_List
;
1849 Has_Pragma
: Boolean := False;
1850 Index_Id
: Entity_Id
;
1853 Wrapper_Id
: Entity_Id
;
1855 -- Start of processing for Build_Entry_Contract_Wrapper
1858 -- This routine generates a specialized wrapper for a protected or task
1859 -- entry [family] which implements precondition/postcondition semantics.
1860 -- Preconditions and case guards of contract cases are checked before
1861 -- the protected action or rendezvous takes place.
1863 -- procedure Wrapper
1864 -- (Obj_Id : Conc_Typ; -- concurrent object
1865 -- [Index : Index_Typ;] -- index of entry family
1866 -- [Formal_1 : ...; -- parameters of original entry
1869 -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
1870 -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
1872 -- <contracts pragmas>
1873 -- <case guard checks>
1876 -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
1879 -- Create the wrapper only when the entry has at least one executable
1880 -- contract item such as contract cases, precondition or postcondition.
1882 if Present
(Items
) then
1884 -- Inspect the list of pre/postconditions and transfer all available
1885 -- pragmas to the declarative list of the wrapper.
1887 Prag
:= Pre_Post_Conditions
(Items
);
1888 while Present
(Prag
) loop
1889 if Pragma_Name_Unmapped
(Prag
) in Name_Postcondition
1891 and then Is_Checked
(Prag
)
1894 Transfer_Pragma
(Prag
, To
=> Decls
);
1897 Prag
:= Next_Pragma
(Prag
);
1900 -- Inspect the list of test/contract cases and transfer only contract
1901 -- cases pragmas to the declarative part of the wrapper.
1903 Prag
:= Contract_Test_Cases
(Items
);
1904 while Present
(Prag
) loop
1905 if Pragma_Name
(Prag
) = Name_Contract_Cases
1906 and then Is_Checked
(Prag
)
1909 Transfer_Pragma
(Prag
, To
=> Decls
);
1912 Prag
:= Next_Pragma
(Prag
);
1916 -- The entry lacks executable contract items and a wrapper is not needed
1918 if not Has_Pragma
then
1922 -- Create the profile of the wrapper. The first formal parameter is the
1923 -- concurrent object.
1926 Make_Defining_Identifier
(Loc
,
1927 Chars
=> New_External_Name
(Chars
(Conc_Typ
), 'A'));
1929 Formals
:= New_List
(
1930 Make_Parameter_Specification
(Loc
,
1931 Defining_Identifier
=> Obj_Id
,
1932 Out_Present
=> True,
1934 Parameter_Type
=> New_Occurrence_Of
(Conc_Typ
, Loc
)));
1936 -- Construct the call to the original entry. The call will be gradually
1937 -- augmented with an optional entry index and extra parameters.
1940 Make_Selected_Component
(Loc
,
1941 Prefix
=> New_Occurrence_Of
(Obj_Id
, Loc
),
1942 Selector_Name
=> New_Occurrence_Of
(E
, Loc
));
1944 -- When creating a wrapper for an entry family, the second formal is the
1947 if Ekind
(E
) = E_Entry_Family
then
1948 Index_Id
:= Make_Defining_Identifier
(Loc
, Name_I
);
1951 Make_Parameter_Specification
(Loc
,
1952 Defining_Identifier
=> Index_Id
,
1954 New_Occurrence_Of
(Entry_Index_Type
(E
), Loc
)));
1956 -- The call to the original entry becomes an indexed component to
1957 -- accommodate the entry index.
1960 Make_Indexed_Component
(Loc
,
1962 Expressions
=> New_List
(New_Occurrence_Of
(Index_Id
, Loc
)));
1965 -- Add formal parameters to match those of the entry and build actuals
1966 -- for the entry call.
1968 Add_Matching_Formals
(Formals
, Actuals
);
1971 Make_Procedure_Call_Statement
(Loc
,
1973 Parameter_Associations
=> Actuals
);
1975 -- Add renaming declarations for the discriminants of the enclosing type
1976 -- as the various contract items may reference them.
1978 Add_Discriminant_Renamings
(Obj_Id
, Decls
);
1981 Make_Defining_Identifier
(Loc
, New_External_Name
(Chars
(E
), 'E'));
1982 Set_Contract_Wrapper
(E
, Wrapper_Id
);
1983 Set_Is_Entry_Wrapper
(Wrapper_Id
);
1985 -- The wrapper body is analyzed when the enclosing type is frozen
1987 Append_Freeze_Action
(Defining_Entity
(Decl
),
1988 Make_Subprogram_Body
(Loc
,
1990 Make_Procedure_Specification
(Loc
,
1991 Defining_Unit_Name
=> Wrapper_Id
,
1992 Parameter_Specifications
=> Formals
),
1993 Declarations
=> Decls
,
1994 Handled_Statement_Sequence
=>
1995 Make_Handled_Sequence_Of_Statements
(Loc
,
1996 Statements
=> New_List
(Call
))));
1997 end Build_Entry_Contract_Wrapper
;
1999 ---------------------------
2000 -- Check_Class_Condition --
2001 ---------------------------
2003 procedure Check_Class_Condition
2006 Par_Subp
: Entity_Id
;
2007 Is_Precondition
: Boolean)
2009 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
2010 -- Check reference to formal of inherited operation or to primitive
2011 -- operation of root type.
2017 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
2022 if Nkind
(N
) = N_Identifier
2023 and then Present
(Entity
(N
))
2025 (Is_Formal
(Entity
(N
)) or else Is_Subprogram
(Entity
(N
)))
2027 (Nkind
(Parent
(N
)) /= N_Attribute_Reference
2028 or else Attribute_Name
(Parent
(N
)) /= Name_Class
)
2030 -- These checks do not apply to dispatching calls within the
2031 -- condition, but only to calls whose static tag is that of
2034 if Is_Subprogram
(Entity
(N
))
2035 and then Nkind
(Parent
(N
)) = N_Function_Call
2036 and then Present
(Controlling_Argument
(Parent
(N
)))
2041 -- Determine whether entity has a renaming
2043 Orig_E
:= Entity
(N
);
2044 New_E
:= Get_Mapped_Entity
(Orig_E
);
2046 if Present
(New_E
) then
2048 -- AI12-0166: A precondition for a protected operation
2049 -- cannot include an internal call to a protected function
2050 -- of the type. In the case of an inherited condition for an
2051 -- overriding operation, both the operation and the function
2052 -- are given by primitive wrappers.
2055 and then Ekind
(New_E
) = E_Function
2056 and then Is_Primitive_Wrapper
(New_E
)
2057 and then Is_Primitive_Wrapper
(Subp
)
2058 and then Scope
(Subp
) = Scope
(New_E
)
2060 Error_Msg_Node_2
:= Wrapped_Entity
(Subp
);
2062 ("internal call to& cannot appear in inherited "
2063 & "precondition of protected operation&",
2064 Subp
, Wrapped_Entity
(New_E
));
2068 -- Check that there are no calls left to abstract operations if
2069 -- the current subprogram is not abstract.
2072 and then Nkind
(Parent
(N
)) = N_Function_Call
2073 and then N
= Name
(Parent
(N
))
2075 if not Is_Abstract_Subprogram
(Subp
)
2076 and then Is_Abstract_Subprogram
(New_E
)
2078 Error_Msg_Sloc
:= Sloc
(Current_Scope
);
2079 Error_Msg_Node_2
:= Subp
;
2081 if Comes_From_Source
(Subp
) then
2083 ("cannot call abstract subprogram & in inherited "
2084 & "condition for&#", Subp
, New_E
);
2087 ("cannot call abstract subprogram & in inherited "
2088 & "condition for inherited&#", Subp
, New_E
);
2091 -- In SPARK mode, report error on inherited condition for an
2092 -- inherited operation if it contains a call to an overriding
2093 -- operation, because this implies that the pre/postconditions
2094 -- of the inherited operation have changed silently.
2096 elsif SPARK_Mode
= On
2097 and then Warn_On_Suspicious_Contract
2098 and then Present
(Alias
(Subp
))
2099 and then Present
(New_E
)
2100 and then Comes_From_Source
(New_E
)
2103 ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
2105 Error_Msg_Sloc
:= Sloc
(New_E
);
2106 Error_Msg_Node_2
:= Subp
;
2108 ("\overriding of&# forces overriding of&",
2109 Parent
(Subp
), New_E
);
2117 procedure Check_Condition_Entities
is
2118 new Traverse_Proc
(Check_Entity
);
2120 -- Start of processing for Check_Class_Condition
2123 -- No check required if the subprograms match
2125 if Par_Subp
= Subp
then
2129 Update_Primitives_Mapping
(Par_Subp
, Subp
);
2130 Map_Formals
(Par_Subp
, Subp
);
2131 Check_Condition_Entities
(Cond
);
2132 end Check_Class_Condition
;
2134 -----------------------------
2135 -- Create_Generic_Contract --
2136 -----------------------------
2138 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
2139 Templ
: constant Node_Id
:= Original_Node
(Unit
);
2140 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
2142 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
2143 -- Add a single contract-related source pragma Prag to the contract of
2144 -- generic template Templ_Id.
2146 ---------------------------------
2147 -- Add_Generic_Contract_Pragma --
2148 ---------------------------------
2150 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
2151 Prag_Templ
: Node_Id
;
2154 -- Mark the pragma to prevent the premature capture of global
2155 -- references when capturing global references of the context
2156 -- (see Save_References_In_Pragma).
2158 Set_Is_Generic_Contract_Pragma
(Prag
);
2160 -- Pragmas that apply to a generic subprogram declaration are not
2161 -- part of the semantic structure of the generic template:
2164 -- procedure Example (Formal : Integer);
2165 -- pragma Precondition (Formal > 0);
2167 -- Create a generic template for such pragmas and link the template
2168 -- of the pragma with the generic template.
2170 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2172 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
2173 Prag_Templ
:= Original_Node
(Prag
);
2175 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
2176 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
2178 -- Otherwise link the pragma with the generic template
2181 Add_Contract_Item
(Prag
, Templ_Id
);
2183 end Add_Generic_Contract_Pragma
;
2187 Context
: constant Node_Id
:= Parent
(Unit
);
2188 Decl
: Node_Id
:= Empty
;
2190 -- Start of processing for Create_Generic_Contract
2193 -- A generic package declaration carries contract-related source pragmas
2194 -- in its visible declarations.
2196 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
2197 Mutate_Ekind
(Templ_Id
, E_Generic_Package
);
2199 if Present
(Visible_Declarations
(Specification
(Templ
))) then
2200 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
2203 -- A generic package body carries contract-related source pragmas in its
2206 elsif Nkind
(Templ
) = N_Package_Body
then
2207 Mutate_Ekind
(Templ_Id
, E_Package_Body
);
2209 if Present
(Declarations
(Templ
)) then
2210 Decl
:= First
(Declarations
(Templ
));
2213 -- Generic subprogram declaration
2215 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
2216 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
2217 Mutate_Ekind
(Templ_Id
, E_Generic_Function
);
2219 Mutate_Ekind
(Templ_Id
, E_Generic_Procedure
);
2222 -- When the generic subprogram acts as a compilation unit, inspect
2223 -- the Pragmas_After list for contract-related source pragmas.
2225 if Nkind
(Context
) = N_Compilation_Unit
then
2226 if Present
(Aux_Decls_Node
(Context
))
2227 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
2229 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
2232 -- Otherwise inspect the successive declarations for contract-related
2236 Decl
:= Next
(Unit
);
2239 -- A generic subprogram body carries contract-related source pragmas in
2240 -- its declarations.
2242 elsif Nkind
(Templ
) = N_Subprogram_Body
then
2243 Mutate_Ekind
(Templ_Id
, E_Subprogram_Body
);
2245 if Present
(Declarations
(Templ
)) then
2246 Decl
:= First
(Declarations
(Templ
));
2250 -- Inspect the relevant declarations looking for contract-related source
2251 -- pragmas and add them to the contract of the generic unit.
2253 while Present
(Decl
) loop
2254 if Comes_From_Source
(Decl
) then
2255 if Nkind
(Decl
) = N_Pragma
then
2257 -- The source pragma is a contract annotation
2259 if Is_Contract_Annotation
(Decl
) then
2260 Add_Generic_Contract_Pragma
(Decl
);
2263 -- The region where a contract-related source pragma may appear
2264 -- ends with the first source non-pragma declaration or statement.
2273 end Create_Generic_Contract
;
2275 --------------------------------
2276 -- Expand_Subprogram_Contract --
2277 --------------------------------
2279 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
2280 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
2281 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
2283 procedure Add_Invariant_And_Predicate_Checks
2284 (Subp_Id
: Entity_Id
;
2285 Stmts
: in out List_Id
;
2286 Result
: out Node_Id
);
2287 -- Process the result of function Subp_Id (if applicable) and all its
2288 -- formals. Add invariant and predicate checks where applicable. The
2289 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
2290 -- function, Result contains the entity of parameter _Result, to be
2291 -- used in the creation of procedure _Postconditions.
2293 procedure Add_Stable_Property_Contracts
2294 (Subp_Id
: Entity_Id
; Class_Present
: Boolean);
2295 -- Augment postcondition contracts to reflect Stable_Property aspect
2296 -- (if Class_Present = False) or Stable_Property'Class aspect (if
2297 -- Class_Present = True).
2299 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
2300 -- Append a node to a list. If there is no list, create a new one. When
2301 -- the item denotes a pragma, it is added to the list only when it is
2304 procedure Process_Contract_Cases
2305 (Stmts
: in out List_Id
;
2307 -- Process pragma Contract_Cases. This routine prepends items to the
2308 -- body declarations and appends items to list Stmts.
2310 procedure Process_Postconditions
(Stmts
: in out List_Id
);
2311 -- Collect all [inherited] spec and body postconditions and accumulate
2312 -- their pragma Check equivalents in list Stmts.
2314 procedure Process_Preconditions
(Decls
: in out List_Id
);
2315 -- Collect all [inherited] spec and body preconditions and prepend their
2316 -- pragma Check equivalents to the declarations of the body.
2318 ----------------------------------------
2319 -- Add_Invariant_And_Predicate_Checks --
2320 ----------------------------------------
2322 procedure Add_Invariant_And_Predicate_Checks
2323 (Subp_Id
: Entity_Id
;
2324 Stmts
: in out List_Id
;
2325 Result
: out Node_Id
)
2327 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
2328 -- Id denotes the return value of a function or a formal parameter.
2329 -- Add an invariant check if the type of Id is access to a type with
2330 -- invariants. The routine appends the generated code to Stmts.
2332 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
2333 -- Determine whether type Typ can benefit from invariant checks. To
2334 -- qualify, the type must have a non-null invariant procedure and
2335 -- subprogram Subp_Id must appear visible from the point of view of
2338 ---------------------------------
2339 -- Add_Invariant_Access_Checks --
2340 ---------------------------------
2342 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
2343 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2350 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
2351 Typ
:= Designated_Type
(Typ
);
2353 if Invariant_Checks_OK
(Typ
) then
2355 Make_Explicit_Dereference
(Loc
,
2356 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
2357 Set_Etype
(Ref
, Typ
);
2360 -- if <Id> /= null then
2361 -- <invariant_call (<Ref>)>
2366 Make_If_Statement
(Loc
,
2369 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
2370 Right_Opnd
=> Make_Null
(Loc
)),
2371 Then_Statements
=> New_List
(
2372 Make_Invariant_Call
(Ref
))),
2376 end Add_Invariant_Access_Checks
;
2378 -------------------------
2379 -- Invariant_Checks_OK --
2380 -------------------------
2382 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
2383 function Has_Public_Visibility_Of_Subprogram
return Boolean;
2384 -- Determine whether type Typ has public visibility of subprogram
2387 -----------------------------------------
2388 -- Has_Public_Visibility_Of_Subprogram --
2389 -----------------------------------------
2391 function Has_Public_Visibility_Of_Subprogram
return Boolean is
2392 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2395 -- An Initialization procedure must be considered visible even
2396 -- though it is internally generated.
2398 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2401 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2404 -- Internally generated code is never publicly visible except
2405 -- for a subprogram that is the implementation of an expression
2406 -- function. In that case the visibility is determined by the
2409 elsif not Comes_From_Source
(Subp_Decl
)
2411 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2413 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2417 -- Determine whether the subprogram is declared in the visible
2418 -- declarations of the package containing the type, or in the
2419 -- visible declaration of a child unit of that package.
2423 Decls
: constant List_Id
:=
2424 List_Containing
(Subp_Decl
);
2425 Subp_Scope
: constant Entity_Id
:=
2426 Scope
(Defining_Entity
(Subp_Decl
));
2427 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2431 Decls
= Visible_Declarations
2432 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2435 (Ekind
(Subp_Scope
) = E_Package
2436 and then Typ_Scope
/= Subp_Scope
2437 and then Is_Child_Unit
(Subp_Scope
)
2439 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2441 Decls
= Visible_Declarations
2443 (Unit_Declaration_Node
(Subp_Scope
))));
2446 end Has_Public_Visibility_Of_Subprogram
;
2448 -- Start of processing for Invariant_Checks_OK
2452 Has_Invariants
(Typ
)
2453 and then Present
(Invariant_Procedure
(Typ
))
2454 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2455 and then Has_Public_Visibility_Of_Subprogram
;
2456 end Invariant_Checks_OK
;
2460 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2461 -- Source location of subprogram body contract
2466 -- Start of processing for Add_Invariant_And_Predicate_Checks
2471 -- Process the result of a function
2473 if Ekind
(Subp_Id
) = E_Function
then
2474 Typ
:= Etype
(Subp_Id
);
2476 -- Generate _Result which is used in procedure _Postconditions to
2477 -- verify the return value.
2479 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2480 Set_Etype
(Result
, Typ
);
2482 -- Add an invariant check when the return type has invariants and
2483 -- the related function is visible to the outside.
2485 if Invariant_Checks_OK
(Typ
) then
2488 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2492 -- Add an invariant check when the return type is an access to a
2493 -- type with invariants.
2495 Add_Invariant_Access_Checks
(Result
);
2498 -- Add invariant checks for all formals that qualify (see AI05-0289
2501 Formal
:= First_Formal
(Subp_Id
);
2502 while Present
(Formal
) loop
2503 Typ
:= Etype
(Formal
);
2505 if Ekind
(Formal
) /= E_In_Parameter
2506 or else Ekind
(Subp_Id
) = E_Procedure
2507 or else Is_Access_Type
(Typ
)
2509 if Invariant_Checks_OK
(Typ
) then
2512 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2516 Add_Invariant_Access_Checks
(Formal
);
2518 -- Note: we used to add predicate checks for OUT and IN OUT
2519 -- formals here, but that was misguided, since such checks are
2520 -- performed on the caller side, based on the predicate of the
2521 -- actual, rather than the predicate of the formal.
2525 Next_Formal
(Formal
);
2527 end Add_Invariant_And_Predicate_Checks
;
2529 -----------------------------------
2530 -- Add_Stable_Property_Contracts --
2531 -----------------------------------
2533 procedure Add_Stable_Property_Contracts
2534 (Subp_Id
: Entity_Id
; Class_Present
: Boolean)
2536 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
2538 procedure Insert_Stable_Property_Check
2539 (Formal
: Entity_Id
; Property_Function
: Entity_Id
);
2540 -- Build the pragma for one check and insert it in the tree.
2542 function Make_Stable_Property_Condition
2543 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
;
2544 -- Builds tree for "Func (Formal) = Func (Formal)'Old" expression.
2546 function Stable_Properties
2547 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2548 return Subprogram_List
;
2549 -- If no aspect specified, then returns length-zero result.
2550 -- Negated indicates that reserved word NOT was specified.
2552 ----------------------------------
2553 -- Insert_Stable_Property_Check --
2554 ----------------------------------
2556 procedure Insert_Stable_Property_Check
2557 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) is
2559 Args
: constant List_Id
:=
2561 (Make_Pragma_Argument_Association
2564 Make_Stable_Property_Condition
2566 Property_Function
=> Property_Function
)),
2567 Make_Pragma_Argument_Association
2573 "failed stable property check at "
2574 & Build_Location_String
(Loc
)
2576 & To_String
(Fully_Qualified_Name_String
2577 (Formal
, Append_NUL
=> False))
2578 & " and property function "
2579 & To_String
(Fully_Qualified_Name_String
2580 (Property_Function
, Append_NUL
=> False))
2583 Prag
: constant Node_Id
:=
2585 Pragma_Identifier
=>
2586 Make_Identifier
(Loc
, Name_Postcondition
),
2587 Pragma_Argument_Associations
=> Args
,
2588 Class_Present
=> Class_Present
);
2590 Subp_Decl
: Node_Id
:= Subp_Id
;
2592 -- Enclosing_Declaration may return, for example,
2593 -- a N_Procedure_Specification node. Cope with this.
2595 Subp_Decl
:= Enclosing_Declaration
(Subp_Decl
);
2596 exit when Is_Declaration
(Subp_Decl
);
2597 Subp_Decl
:= Parent
(Subp_Decl
);
2598 pragma Assert
(Present
(Subp_Decl
));
2601 Insert_After_And_Analyze
(Subp_Decl
, Prag
);
2602 end Insert_Stable_Property_Check
;
2604 ------------------------------------
2605 -- Make_Stable_Property_Condition --
2606 ------------------------------------
2608 function Make_Stable_Property_Condition
2609 (Formal
: Entity_Id
; Property_Function
: Entity_Id
) return Node_Id
2611 function Call_Property_Function
return Node_Id
is
2615 New_Occurrence_Of
(Property_Function
, Loc
),
2616 Parameter_Associations
=>
2617 New_List
(New_Occurrence_Of
(Formal
, Loc
))));
2621 Call_Property_Function
,
2622 Make_Attribute_Reference
2624 Prefix
=> Call_Property_Function
,
2625 Attribute_Name
=> Name_Old
));
2626 end Make_Stable_Property_Condition
;
2628 -----------------------
2629 -- Stable_Properties --
2630 -----------------------
2632 function Stable_Properties
2633 (Aspect_Bearer
: Entity_Id
; Negated
: out Boolean)
2634 return Subprogram_List
2636 Aspect_Spec
: Node_Id
:=
2637 Find_Value_Of_Aspect
2638 (Aspect_Bearer
, Aspect_Stable_Properties
,
2639 Class_Present
=> Class_Present
);
2641 -- ??? For a derived type, we wish Find_Value_Of_Aspect
2642 -- somehow knew that this aspect is not inherited.
2643 -- But it doesn't, so we cope with that here.
2645 -- There are probably issues here with inheritance from
2646 -- interface types, where just looking for the one parent type
2647 -- isn't enough. But this is far from the only work needed for
2648 -- Stable_Properties'Class for interface types.
2650 if Is_Derived_Type
(Aspect_Bearer
) then
2652 Parent_Type
: constant Entity_Id
:=
2653 Etype
(Base_Type
(Aspect_Bearer
));
2656 Find_Value_Of_Aspect
2657 (Parent_Type
, Aspect_Stable_Properties
,
2658 Class_Present
=> Class_Present
)
2660 -- prevent inheritance
2661 Aspect_Spec
:= Empty
;
2666 if No
(Aspect_Spec
) then
2667 Negated
:= Aspect_Bearer
= Subp_Id
;
2668 -- This is a little bit subtle.
2669 -- We need to assign True in the Subp_Id case in order to
2670 -- distinguish between no aspect spec at all vs. an
2671 -- explicitly specified "with S_P => []" empty list.
2672 -- In both cases Stable_Properties will return a length-0
2673 -- array, but the two cases are not equivalent.
2674 -- Very roughly speaking the lack of an S_P aspect spec for
2675 -- a subprogram would be equivalent to something like
2676 -- "with S_P => [not]", where we apply the "not" modifier to
2677 -- an empty set of subprograms, if such a construct existed.
2678 -- We could just assign True here, but it seems untidy to
2679 -- return True in the case of an aspect spec for a type
2680 -- (since negation is only allowed for subp S_P aspects).
2682 return (1 .. 0 => <>);
2684 return Parse_Aspect_Stable_Properties
2685 (Aspect_Spec
, Negated
=> Negated
);
2687 end Stable_Properties
;
2689 Formal
: Entity_Id
:= First_Formal
(Subp_Id
);
2690 Type_Of_Formal
: Entity_Id
;
2692 Subp_Properties_Negated
: Boolean;
2693 Subp_Properties
: constant Subprogram_List
:=
2694 Stable_Properties
(Subp_Id
, Subp_Properties_Negated
);
2696 -- start of processing for Add_Stable_Property_Contracts
2699 if not (Is_Primitive
(Subp_Id
) and then Comes_From_Source
(Subp_Id
))
2704 while Present
(Formal
) loop
2705 Type_Of_Formal
:= Base_Type
(Etype
(Formal
));
2707 if not Subp_Properties_Negated
then
2709 for SPF_Id
of Subp_Properties
loop
2710 if Type_Of_Formal
= Base_Type
(Etype
(First_Formal
(SPF_Id
)))
2711 and then Scope
(Type_Of_Formal
) = Scope
(Subp_Id
)
2713 -- ??? Need to filter out checks for SPFs that are
2714 -- mentioned explicitly in the postcondition of
2717 Insert_Stable_Property_Check
2718 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2722 elsif Scope
(Type_Of_Formal
) = Scope
(Subp_Id
) then
2724 Ignored
: Boolean range False .. False;
2726 Typ_Property_Funcs
: constant Subprogram_List
:=
2727 Stable_Properties
(Type_Of_Formal
, Negated
=> Ignored
);
2729 function Excluded_By_Aspect_Spec_Of_Subp
2730 (SPF_Id
: Entity_Id
) return Boolean;
2731 -- Examine Subp_Properties to determine whether SPF should
2734 -------------------------------------
2735 -- Excluded_By_Aspect_Spec_Of_Subp --
2736 -------------------------------------
2738 function Excluded_By_Aspect_Spec_Of_Subp
2739 (SPF_Id
: Entity_Id
) return Boolean is
2741 pragma Assert
(Subp_Properties_Negated
);
2742 -- Look through renames for equality test here ???
2743 return (for some F
of Subp_Properties
=> F
= SPF_Id
);
2744 end Excluded_By_Aspect_Spec_Of_Subp
;
2746 -- Look through renames for equality test here ???
2747 Subp_Is_Stable_Property_Function
: constant Boolean :=
2748 (for some F
of Typ_Property_Funcs
=> F
= Subp_Id
);
2750 if not Subp_Is_Stable_Property_Function
then
2751 for SPF_Id
of Typ_Property_Funcs
loop
2752 if not Excluded_By_Aspect_Spec_Of_Subp
(SPF_Id
) then
2753 -- ??? Need to filter out checks for SPFs that are
2754 -- mentioned explicitly in the postcondition of
2756 Insert_Stable_Property_Check
2757 (Formal
=> Formal
, Property_Function
=> SPF_Id
);
2763 Next_Formal
(Formal
);
2765 end Add_Stable_Property_Contracts
;
2767 -------------------------
2768 -- Append_Enabled_Item --
2769 -------------------------
2771 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2773 -- Do not chain ignored or disabled pragmas
2775 if Nkind
(Item
) = N_Pragma
2776 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2780 -- Otherwise, add the item
2787 -- If the pragma is a conjunct in a composite postcondition, it
2788 -- has been processed in reverse order. In the postcondition body
2789 -- it must appear before the others.
2791 if Nkind
(Item
) = N_Pragma
2792 and then From_Aspect_Specification
(Item
)
2793 and then Split_PPC
(Item
)
2795 Prepend
(Item
, List
);
2797 Append
(Item
, List
);
2800 end Append_Enabled_Item
;
2802 ----------------------------
2803 -- Process_Contract_Cases --
2804 ----------------------------
2806 procedure Process_Contract_Cases
2807 (Stmts
: in out List_Id
;
2810 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2811 -- Process pragma Contract_Cases for subprogram Subp_Id
2813 --------------------------------
2814 -- Process_Contract_Cases_For --
2815 --------------------------------
2817 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2818 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2822 if Present
(Items
) then
2823 Prag
:= Contract_Test_Cases
(Items
);
2824 while Present
(Prag
) loop
2825 if Is_Checked
(Prag
) then
2826 if Pragma_Name
(Prag
) = Name_Contract_Cases
then
2827 Expand_Pragma_Contract_Cases
2833 elsif Pragma_Name
(Prag
) = Name_Subprogram_Variant
then
2834 Expand_Pragma_Subprogram_Variant
2837 Body_Decls
=> Decls
);
2841 Prag
:= Next_Pragma
(Prag
);
2844 end Process_Contract_Cases_For
;
2846 -- Start of processing for Process_Contract_Cases
2849 Process_Contract_Cases_For
(Body_Id
);
2851 if Present
(Spec_Id
) then
2852 Process_Contract_Cases_For
(Spec_Id
);
2854 end Process_Contract_Cases
;
2856 ----------------------------
2857 -- Process_Postconditions --
2858 ----------------------------
2860 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2861 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2862 -- Collect all [refined] postconditions of a specific kind denoted
2863 -- by Post_Nam that belong to the body, and generate pragma Check
2864 -- equivalents in list Stmts.
2866 procedure Process_Spec_Postconditions
;
2867 -- Collect all [inherited] postconditions of the spec, and generate
2868 -- pragma Check equivalents in list Stmts.
2870 ---------------------------------
2871 -- Process_Body_Postconditions --
2872 ---------------------------------
2874 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2875 Items
: constant Node_Id
:= Contract
(Body_Id
);
2876 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2881 -- Process the contract
2883 if Present
(Items
) then
2884 Prag
:= Pre_Post_Conditions
(Items
);
2885 while Present
(Prag
) loop
2886 if Pragma_Name
(Prag
) = Post_Nam
2887 and then Is_Checked
(Prag
)
2890 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2894 Prag
:= Next_Pragma
(Prag
);
2898 -- The subprogram body being processed is actually the proper body
2899 -- of a stub with a corresponding spec. The subprogram stub may
2900 -- carry a postcondition pragma, in which case it must be taken
2901 -- into account. The pragma appears after the stub.
2903 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2904 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2905 while Present
(Decl
) loop
2907 -- Note that non-matching pragmas are skipped
2909 if Nkind
(Decl
) = N_Pragma
then
2910 if Pragma_Name
(Decl
) = Post_Nam
2911 and then Is_Checked
(Decl
)
2914 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2918 -- Skip internally generated code
2920 elsif not Comes_From_Source
(Decl
) then
2923 -- Postcondition pragmas are usually grouped together. There
2924 -- is no need to inspect the whole declarative list.
2933 end Process_Body_Postconditions
;
2935 ---------------------------------
2936 -- Process_Spec_Postconditions --
2937 ---------------------------------
2939 procedure Process_Spec_Postconditions
is
2940 Subps
: constant Subprogram_List
:=
2941 Inherited_Subprograms
(Spec_Id
);
2942 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
2944 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean;
2945 -- Return True if the contract of subprogram Subp_Id has been
2952 function Seen_Subp
(Subp_Id
: Entity_Id
) return Boolean is
2954 for Index
in Seen
'Range loop
2955 if Seen
(Index
) = Subp_Id
then
2968 Subp_Id
: Entity_Id
;
2970 -- Start of processing for Process_Spec_Postconditions
2973 -- Process the contract
2975 Items
:= Contract
(Spec_Id
);
2977 if Present
(Items
) then
2978 Prag
:= Pre_Post_Conditions
(Items
);
2979 while Present
(Prag
) loop
2980 if Pragma_Name
(Prag
) = Name_Postcondition
2981 and then Is_Checked
(Prag
)
2984 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2988 Prag
:= Next_Pragma
(Prag
);
2992 -- Process the contracts of all inherited subprograms, looking for
2993 -- class-wide postconditions.
2995 for Index
in Subps
'Range loop
2996 Subp_Id
:= Subps
(Index
);
2998 if Present
(Alias
(Subp_Id
)) then
2999 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
3002 -- Wrappers of class-wide pre/postconditions reference the
3003 -- parent primitive that has the inherited contract.
3005 if Is_Wrapper
(Subp_Id
)
3006 and then Present
(LSP_Subprogram
(Subp_Id
))
3008 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
3011 Items
:= Contract
(Subp_Id
);
3013 if not Seen_Subp
(Subp_Id
) and then Present
(Items
) then
3014 Seen
(Index
) := Subp_Id
;
3016 Prag
:= Pre_Post_Conditions
(Items
);
3017 while Present
(Prag
) loop
3018 if Pragma_Name
(Prag
) = Name_Postcondition
3019 and then Class_Present
(Prag
)
3022 Build_Pragma_Check_Equivalent
3025 Inher_Id
=> Subp_Id
);
3027 -- The pragma Check equivalent of the class-wide
3028 -- postcondition is still created even though the
3029 -- pragma may be ignored because the equivalent
3030 -- performs semantic checks.
3032 if Is_Checked
(Prag
) then
3033 Append_Enabled_Item
(Item
, Stmts
);
3037 Prag
:= Next_Pragma
(Prag
);
3041 end Process_Spec_Postconditions
;
3043 pragma Unmodified
(Stmts
);
3044 -- Stmts is passed as IN OUT to signal that the list can be updated,
3045 -- even if the corresponding integer value representing the list does
3048 -- Start of processing for Process_Postconditions
3051 -- The processing of postconditions is done in reverse order (body
3052 -- first) to ensure the following arrangement:
3054 -- <refined postconditions from body>
3055 -- <postconditions from body>
3056 -- <postconditions from spec>
3057 -- <inherited postconditions>
3059 Process_Body_Postconditions
(Name_Refined_Post
);
3060 Process_Body_Postconditions
(Name_Postcondition
);
3062 if Present
(Spec_Id
) then
3063 Process_Spec_Postconditions
;
3065 end Process_Postconditions
;
3067 ---------------------------
3068 -- Process_Preconditions --
3069 ---------------------------
3071 procedure Process_Preconditions
(Decls
: in out List_Id
) is
3072 Insert_Node
: Node_Id
:= Empty
;
3073 -- The insertion node after which all pragma Check equivalents are
3076 procedure Prepend_To_Decls
(Item
: Node_Id
);
3077 -- Prepend a single item to the declarations of the subprogram body
3079 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
);
3080 -- Prepend a normal precondition to the declarations of the body and
3083 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
3084 -- Collect all preconditions of subprogram Subp_Id and prepend their
3085 -- pragma Check equivalents to the declarations of the body.
3087 ----------------------
3088 -- Prepend_To_Decls --
3089 ----------------------
3091 procedure Prepend_To_Decls
(Item
: Node_Id
) is
3093 -- Ensure that the body has a declarative list
3097 Set_Declarations
(Body_Decl
, Decls
);
3100 Prepend_To
(Decls
, Item
);
3101 end Prepend_To_Decls
;
3103 -----------------------------
3104 -- Prepend_Pragma_To_Decls --
3105 -----------------------------
3107 procedure Prepend_Pragma_To_Decls
(Prag
: Node_Id
) is
3108 Check_Prag
: Node_Id
;
3111 -- Skip the sole class-wide precondition (if any) since it is
3112 -- processed by Merge_Class_Conditions.
3114 if Class_Present
(Prag
) then
3117 -- Accumulate the corresponding Check pragmas at the top of the
3118 -- declarations. Prepending the items ensures that they will be
3119 -- evaluated in their original order.
3122 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
3123 Prepend_To_Decls
(Check_Prag
);
3126 end Prepend_Pragma_To_Decls
;
3128 -------------------------------
3129 -- Process_Preconditions_For --
3130 -------------------------------
3132 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
3133 Items
: constant Node_Id
:= Contract
(Subp_Id
);
3134 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
3140 -- Process the contract. If the body is an expression function
3141 -- that is a completion, freeze types within, because this may
3142 -- not have been done yet, when the subprogram declaration and
3143 -- its completion by an expression function appear in distinct
3144 -- declarative lists of the same unit (visible and private).
3147 Was_Expression_Function
(Body_Decl
)
3148 and then Sloc
(Body_Id
) /= Sloc
(Subp_Id
)
3149 and then In_Same_Source_Unit
(Body_Id
, Subp_Id
)
3150 and then not In_Same_List
(Body_Decl
, Subp_Decl
);
3152 if Present
(Items
) then
3153 Prag
:= Pre_Post_Conditions
(Items
);
3154 while Present
(Prag
) loop
3155 if Pragma_Name
(Prag
) = Name_Precondition
3156 and then Is_Checked
(Prag
)
3159 and then Present
(Corresponding_Aspect
(Prag
))
3163 Typ
=> Standard_Boolean
,
3166 (First
(Pragma_Argument_Associations
(Prag
))),
3170 Prepend_Pragma_To_Decls
(Prag
);
3173 Prag
:= Next_Pragma
(Prag
);
3177 -- The subprogram declaration being processed is actually a body
3178 -- stub. The stub may carry a precondition pragma, in which case
3179 -- it must be taken into account. The pragma appears after the
3182 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
3184 -- Inspect the declarations following the body stub
3186 Decl
:= Next
(Subp_Decl
);
3187 while Present
(Decl
) loop
3189 -- Note that non-matching pragmas are skipped
3191 if Nkind
(Decl
) = N_Pragma
then
3192 if Pragma_Name
(Decl
) = Name_Precondition
3193 and then Is_Checked
(Decl
)
3195 Prepend_Pragma_To_Decls
(Decl
);
3198 -- Skip internally generated code
3200 elsif not Comes_From_Source
(Decl
) then
3203 -- Preconditions are usually grouped together. There is no
3204 -- need to inspect the whole declarative list.
3213 end Process_Preconditions_For
;
3217 Body_Decls
: constant List_Id
:= Declarations
(Body_Decl
);
3219 Next_Decl
: Node_Id
;
3221 -- Start of processing for Process_Preconditions
3224 -- Find the proper insertion point for all pragma Check equivalents
3226 if Present
(Body_Decls
) then
3227 Decl
:= First
(Body_Decls
);
3228 while Present
(Decl
) loop
3230 -- First source declaration terminates the search, because all
3231 -- preconditions must be evaluated prior to it, by definition.
3233 if Comes_From_Source
(Decl
) then
3236 -- Certain internally generated object renamings such as those
3237 -- for discriminants and protection fields must be elaborated
3238 -- before the preconditions are evaluated, as their expressions
3239 -- may mention the discriminants. The renamings include those
3240 -- for private components so we need to find the last such.
3242 elsif Is_Prologue_Renaming
(Decl
) then
3243 while Present
(Next
(Decl
))
3244 and then Is_Prologue_Renaming
(Next
(Decl
))
3249 Insert_Node
:= Decl
;
3251 -- Otherwise the declaration does not come from source. This
3252 -- also terminates the search, because internal code may raise
3253 -- exceptions which should not preempt the preconditions.
3262 -- The processing of preconditions is done in reverse order (body
3263 -- first), because each pragma Check equivalent is inserted at the
3264 -- top of the declarations. This ensures that the final order is
3265 -- consistent with following diagram:
3267 -- <inherited preconditions>
3268 -- <preconditions from spec>
3269 -- <preconditions from body>
3271 Process_Preconditions_For
(Body_Id
);
3273 -- Move the generated entry-call prologue renamings into the
3274 -- outer declarations for use in the preconditions.
3276 Decl
:= First
(Body_Decls
);
3277 while Present
(Decl
) and then Present
(Insert_Node
) loop
3278 Next_Decl
:= Next
(Decl
);
3280 Prepend_To_Decls
(Decl
);
3282 exit when Decl
= Insert_Node
;
3287 if Present
(Spec_Id
) then
3288 Process_Preconditions_For
(Spec_Id
);
3290 end Process_Preconditions
;
3294 Restore_Scope
: Boolean := False;
3296 Stmts
: List_Id
:= No_List
;
3297 Decls
: List_Id
:= New_List
;
3298 Subp_Id
: Entity_Id
;
3300 -- Start of processing for Expand_Subprogram_Contract
3303 -- Obtain the entity of the initial declaration
3305 if Present
(Spec_Id
) then
3311 -- Do not perform expansion activity when it is not needed
3313 if not Expander_Active
then
3316 -- GNATprove does not need the executable semantics of a contract
3318 elsif GNATprove_Mode
then
3321 -- The contract of a generic subprogram or one declared in a generic
3322 -- context is not expanded, as the corresponding instance will provide
3323 -- the executable semantics of the contract.
3325 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
3328 -- All subprograms carry a contract, but for some it is not significant
3329 -- and should not be processed. This is a small optimization.
3331 elsif not Has_Significant_Contract
(Subp_Id
) then
3334 -- The contract of an ignored Ghost subprogram does not need expansion,
3335 -- because the subprogram and all calls to it will be removed.
3337 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
3340 -- No action needed for helpers and indirect-call wrapper built to
3341 -- support class-wide preconditions.
3343 elsif Present
(Class_Preconditions_Subprogram
(Subp_Id
)) then
3346 -- Do not re-expand the same contract. This scenario occurs when a
3347 -- construct is rewritten into something else during its analysis
3348 -- (expression functions for instance).
3350 elsif Has_Expanded_Contract
(Subp_Id
) then
3354 -- Prevent multiple expansion attempts of the same contract
3356 Set_Has_Expanded_Contract
(Subp_Id
);
3358 -- Ensure that the formal parameters are visible when expanding all
3361 if not In_Open_Scopes
(Subp_Id
) then
3362 Restore_Scope
:= True;
3363 Push_Scope
(Subp_Id
);
3365 if Is_Generic_Subprogram
(Subp_Id
) then
3366 Install_Generic_Formals
(Subp_Id
);
3368 Install_Formals
(Subp_Id
);
3372 -- The expansion of a subprogram contract involves the creation of Check
3373 -- pragmas to verify the contract assertions of the spec and body in a
3374 -- particular order. The order is as follows:
3376 -- function Original_Code (...) return ... is
3377 -- <prologue renamings>
3378 -- <inherited preconditions>
3379 -- <preconditions from spec>
3380 -- <preconditions from body>
3381 -- <contract case conditions>
3383 -- function _Wrapped_Statements (...) return ... is
3384 -- <source declarations>
3386 -- <source statements>
3387 -- end _Wrapped_Statements;
3390 -- return Result : constant ... := _Wrapped_Statements do
3391 -- <refined postconditions from body>
3392 -- <postconditions from body>
3393 -- <postconditions from spec>
3394 -- <inherited postconditions>
3395 -- <contract case consequences>
3396 -- <invariant check of function result>
3397 -- <invariant and predicate checks of parameters
3399 -- end Original_Code;
3401 -- Step 1: augment contracts list with postconditions associated with
3402 -- Stable_Properties and Stable_Properties'Class aspects. This must
3403 -- precede Process_Postconditions.
3405 for Class_Present
in Boolean loop
3406 Add_Stable_Property_Contracts
3407 (Subp_Id
, Class_Present
=> Class_Present
);
3410 -- Step 2: Handle all preconditions. This action must come before the
3411 -- processing of pragma Contract_Cases because the pragma prepends items
3412 -- to the body declarations.
3414 Process_Preconditions
(Decls
);
3416 -- Step 3: Handle all postconditions. This action must come before the
3417 -- processing of pragma Contract_Cases because the pragma appends items
3420 Process_Postconditions
(Stmts
);
3422 -- Step 4: Handle pragma Contract_Cases. This action must come before
3423 -- the processing of invariants and predicates because those append
3424 -- items to list Stmts.
3426 Process_Contract_Cases
(Stmts
, Decls
);
3428 -- Step 5: Apply invariant and predicate checks on a function result and
3429 -- all formals. The resulting checks are accumulated in list Stmts.
3431 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3433 -- Step 6: Construct subprogram _wrapped_statements
3435 -- When no statements are present we still need to insert contract
3436 -- related declarations.
3439 Prepend_List_To
(Declarations
(Body_Decl
), Decls
);
3441 -- Otherwise, we need a wrapper
3444 Build_Subprogram_Contract_Wrapper
(Body_Id
, Stmts
, Decls
, Result
);
3447 if Restore_Scope
then
3450 end Expand_Subprogram_Contract
;
3452 -------------------------------
3453 -- Freeze_Previous_Contracts --
3454 -------------------------------
3456 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3457 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3458 pragma Inline
(Causes_Contract_Freezing
);
3459 -- Determine whether arbitrary node N causes contract freezing. This is
3460 -- used as an assertion for the current body declaration that caused
3461 -- contract freezing, and as a condition to detect body declaration that
3462 -- already caused contract freezing before.
3464 procedure Freeze_Contracts
;
3465 pragma Inline
(Freeze_Contracts
);
3466 -- Freeze the contracts of all eligible constructs which precede body
3469 procedure Freeze_Enclosing_Package_Body
;
3470 pragma Inline
(Freeze_Enclosing_Package_Body
);
3471 -- Freeze the contract of the nearest package body (if any) which
3472 -- encloses body Body_Decl.
3474 ------------------------------
3475 -- Causes_Contract_Freezing --
3476 ------------------------------
3478 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3480 -- The following condition matches guards for calls to
3481 -- Freeze_Previous_Contracts from routines that analyze various body
3482 -- declarations. In particular, it detects expression functions, as
3483 -- described in the call from Analyze_Subprogram_Body_Helper.
3486 Comes_From_Source
(Original_Node
(N
))
3489 N_Entry_Body | N_Package_Body | N_Protected_Body |
3490 N_Subprogram_Body | N_Subprogram_Body_Stub | N_Task_Body
;
3491 end Causes_Contract_Freezing
;
3493 ----------------------
3494 -- Freeze_Contracts --
3495 ----------------------
3497 procedure Freeze_Contracts
is
3498 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3502 -- Nothing to do when the body which causes freezing does not appear
3503 -- in a declarative list because there cannot possibly be constructs
3506 if not Is_List_Member
(Body_Decl
) then
3510 -- Inspect the declarations preceding the body, and freeze individual
3511 -- contracts of eligible constructs.
3513 Decl
:= Prev
(Body_Decl
);
3514 while Present
(Decl
) loop
3516 -- Stop the traversal when a preceding construct that causes
3517 -- freezing is encountered as there is no point in refreezing
3518 -- the already frozen constructs.
3520 if Causes_Contract_Freezing
(Decl
) then
3523 -- Entry or subprogram declarations
3525 elsif Nkind
(Decl
) in N_Abstract_Subprogram_Declaration
3526 | N_Entry_Declaration
3527 | N_Generic_Subprogram_Declaration
3528 | N_Subprogram_Declaration
3530 Analyze_Entry_Or_Subprogram_Contract
3531 (Subp_Id
=> Defining_Entity
(Decl
),
3532 Freeze_Id
=> Body_Id
);
3536 elsif Nkind
(Decl
) = N_Object_Declaration
then
3537 Analyze_Object_Contract
3538 (Obj_Id
=> Defining_Entity
(Decl
),
3539 Freeze_Id
=> Body_Id
);
3543 elsif Nkind
(Decl
) in N_Protected_Type_Declaration
3544 | N_Single_Protected_Declaration
3546 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3548 -- Subprogram body stubs
3550 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3551 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3555 elsif Nkind
(Decl
) in N_Single_Task_Declaration
3556 | N_Task_Type_Declaration
3558 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3561 if Nkind
(Decl
) in N_Full_Type_Declaration
3562 | N_Private_Type_Declaration
3563 | N_Task_Type_Declaration
3564 | N_Protected_Type_Declaration
3565 | N_Formal_Type_Declaration
3567 Analyze_Type_Contract
(Defining_Identifier
(Decl
));
3572 end Freeze_Contracts
;
3574 -----------------------------------
3575 -- Freeze_Enclosing_Package_Body --
3576 -----------------------------------
3578 procedure Freeze_Enclosing_Package_Body
is
3579 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3583 -- Climb the parent chain looking for an enclosing package body. Do
3584 -- not use the scope stack, because a body utilizes the entity of its
3585 -- corresponding spec.
3587 Par
:= Parent
(Body_Decl
);
3588 while Present
(Par
) loop
3589 if Nkind
(Par
) = N_Package_Body
then
3590 Analyze_Package_Body_Contract
3591 (Body_Id
=> Defining_Entity
(Par
),
3592 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3596 -- Do not look for an enclosing package body when the construct
3597 -- which causes freezing is a body generated for an expression
3598 -- function and it appears within a package spec. This ensures
3599 -- that the traversal will not reach too far up the parent chain
3600 -- and attempt to freeze a package body which must not be frozen.
3602 -- package body Enclosing_Body
3603 -- with Refined_State => (State => Var)
3605 -- package Nested is
3606 -- type Some_Type is ...;
3607 -- function Cause_Freezing return ...;
3609 -- function Cause_Freezing is (...);
3612 -- Var : Nested.Some_Type;
3614 elsif Nkind
(Par
) = N_Package_Declaration
3615 and then Nkind
(Orig_Decl
) = N_Expression_Function
3619 -- Prevent the search from going too far
3621 elsif Is_Body_Or_Package_Declaration
(Par
) then
3625 Par
:= Parent
(Par
);
3627 end Freeze_Enclosing_Package_Body
;
3631 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3633 -- Start of processing for Freeze_Previous_Contracts
3636 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3638 -- A body that is in the process of being inlined appears from source,
3639 -- but carries name _parent. Such a body does not cause freezing of
3642 if Chars
(Body_Id
) = Name_uParent
then
3646 Freeze_Enclosing_Package_Body
;
3648 end Freeze_Previous_Contracts
;
3650 ---------------------------------
3651 -- Inherit_Subprogram_Contract --
3652 ---------------------------------
3654 procedure Inherit_Subprogram_Contract
3656 From_Subp
: Entity_Id
)
3658 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3659 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3662 --------------------
3663 -- Inherit_Pragma --
3664 --------------------
3666 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3667 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3671 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3672 -- chains, therefore the node must be replicated. The new pragma is
3673 -- flagged as inherited for distinction purposes.
3675 if Present
(Prag
) then
3676 New_Prag
:= New_Copy_Tree
(Prag
);
3677 Set_Is_Inherited_Pragma
(New_Prag
);
3679 Add_Contract_Item
(New_Prag
, Subp
);
3683 -- Start of processing for Inherit_Subprogram_Contract
3686 -- Inheritance is carried out only when both entities are subprograms
3689 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3690 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3691 and then Present
(Contract
(From_Subp
))
3693 Inherit_Pragma
(Pragma_Extensions_Visible
);
3695 end Inherit_Subprogram_Contract
;
3697 -------------------------------------
3698 -- Instantiate_Subprogram_Contract --
3699 -------------------------------------
3701 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3702 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3703 -- Instantiate all contract-related source pragmas found in the list,
3704 -- starting with pragma First_Prag. Each instantiated pragma is added
3707 -------------------------
3708 -- Instantiate_Pragmas --
3709 -------------------------
3711 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3712 Inst_Prag
: Node_Id
;
3717 while Present
(Prag
) loop
3718 if Is_Generic_Contract_Pragma
(Prag
) then
3720 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3722 Set_Analyzed
(Inst_Prag
, False);
3723 Append_To
(L
, Inst_Prag
);
3726 Prag
:= Next_Pragma
(Prag
);
3728 end Instantiate_Pragmas
;
3732 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3734 -- Start of processing for Instantiate_Subprogram_Contract
3737 if Present
(Items
) then
3738 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3739 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3740 Instantiate_Pragmas
(Classifications
(Items
));
3742 end Instantiate_Subprogram_Contract
;
3744 --------------------------
3745 -- Is_Prologue_Renaming --
3746 --------------------------
3748 -- This should be turned into a flag and set during the expansion of
3749 -- task and protected types when the renamings get generated ???
3751 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
3758 if Nkind
(Decl
) = N_Object_Renaming_Declaration
3759 and then not Comes_From_Source
(Decl
)
3761 Obj
:= Defining_Entity
(Decl
);
3764 if Nkind
(Nam
) = N_Selected_Component
then
3765 -- Analyze the renaming declaration so we can further examine it
3767 if not Analyzed
(Decl
) then
3771 Pref
:= Prefix
(Nam
);
3772 Sel
:= Selector_Name
(Nam
);
3774 -- A discriminant renaming appears as
3775 -- Discr : constant ... := Prefix.Discr;
3777 if Ekind
(Obj
) = E_Constant
3778 and then Is_Entity_Name
(Sel
)
3779 and then Present
(Entity
(Sel
))
3780 and then Ekind
(Entity
(Sel
)) = E_Discriminant
3784 -- A protection field renaming appears as
3785 -- Prot : ... := _object._object;
3787 -- A renamed private component is just a component of
3788 -- _object, with an arbitrary name.
3790 elsif Ekind
(Obj
) in E_Variable | E_Constant
3791 and then Nkind
(Pref
) = N_Identifier
3792 and then Chars
(Pref
) = Name_uObject
3793 and then Nkind
(Sel
) = N_Identifier
3801 end Is_Prologue_Renaming
;
3803 -----------------------------------
3804 -- Make_Class_Precondition_Subps --
3805 -----------------------------------
3807 procedure Make_Class_Precondition_Subps
3808 (Subp_Id
: Entity_Id
;
3809 Late_Overriding
: Boolean := False)
3811 Loc
: constant Source_Ptr
:= Sloc
(Subp_Id
);
3812 Tagged_Type
: constant Entity_Id
:= Find_Dispatching_Type
(Subp_Id
);
3814 procedure Add_Indirect_Call_Wrapper
;
3815 -- Build the indirect-call wrapper and append it to the freezing actions
3818 procedure Add_Call_Helper
3819 (Helper_Id
: Entity_Id
;
3820 Is_Dynamic
: Boolean);
3821 -- Factorizes code for building a call helper with the given identifier
3822 -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
3823 -- controls building the static or dynamic version of the helper.
3825 function Build_Unique_Name
(Suffix
: String) return Name_Id
;
3826 -- Build an unique new name adding suffix to Subp_Id name (plus its
3827 -- homonym number for values bigger than 1).
3829 -------------------------------
3830 -- Add_Indirect_Call_Wrapper --
3831 -------------------------------
3833 procedure Add_Indirect_Call_Wrapper
is
3835 function Build_ICW_Body
return Node_Id
;
3836 -- Build the body of the indirect call wrapper
3838 function Build_ICW_Decl
return Node_Id
;
3839 -- Build the declaration of the indirect call wrapper
3841 --------------------
3842 -- Build_ICW_Body --
3843 --------------------
3845 function Build_ICW_Body
return Node_Id
is
3846 ICW_Id
: constant Entity_Id
:= Indirect_Call_Wrapper
(Subp_Id
);
3847 Spec
: constant Node_Id
:= Parent
(ICW_Id
);
3848 Body_Spec
: Node_Id
;
3853 Body_Spec
:= Copy_Subprogram_Spec
(Spec
);
3855 -- Build call to wrapped subprogram
3858 Actuals
: constant List_Id
:= Empty_List
;
3859 Formal_Spec
: Entity_Id
:=
3860 First
(Parameter_Specifications
(Spec
));
3862 -- Build parameter association & call
3864 while Present
(Formal_Spec
) loop
3867 (Defining_Identifier
(Formal_Spec
), Loc
));
3871 if Ekind
(ICW_Id
) = E_Procedure
then
3873 Make_Procedure_Call_Statement
(Loc
,
3874 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3875 Parameter_Associations
=> Actuals
);
3878 Make_Simple_Return_Statement
(Loc
,
3880 Make_Function_Call
(Loc
,
3881 Name
=> New_Occurrence_Of
(Subp_Id
, Loc
),
3882 Parameter_Associations
=> Actuals
));
3887 Make_Subprogram_Body
(Loc
,
3888 Specification
=> Body_Spec
,
3889 Declarations
=> New_List
,
3890 Handled_Statement_Sequence
=>
3891 Make_Handled_Sequence_Of_Statements
(Loc
,
3892 Statements
=> New_List
(Call
)));
3894 -- The new operation is internal and overriding indicators do not
3897 Set_Must_Override
(Body_Spec
, False);
3902 --------------------
3903 -- Build_ICW_Decl --
3904 --------------------
3906 function Build_ICW_Decl
return Node_Id
is
3907 ICW_Id
: constant Entity_Id
:=
3908 Make_Defining_Identifier
(Loc
,
3909 Build_Unique_Name
(Suffix
=> "ICW"));
3914 Spec
:= Copy_Subprogram_Spec
(Parent
(Subp_Id
));
3915 Set_Must_Override
(Spec
, False);
3916 Set_Must_Not_Override
(Spec
, False);
3917 Set_Defining_Unit_Name
(Spec
, ICW_Id
);
3918 Mutate_Ekind
(ICW_Id
, Ekind
(Subp_Id
));
3919 Set_Is_Public
(ICW_Id
);
3921 -- The indirect call wrapper is commonly used for indirect calls
3922 -- but inlined for direct calls performed from the DTW.
3924 Set_Is_Inlined
(ICW_Id
);
3926 if Nkind
(Spec
) = N_Procedure_Specification
then
3927 Set_Null_Present
(Spec
, False);
3930 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
3932 -- Link original subprogram to indirect wrapper and vice versa
3934 Set_Indirect_Call_Wrapper
(Subp_Id
, ICW_Id
);
3935 Set_Class_Preconditions_Subprogram
(ICW_Id
, Subp_Id
);
3937 -- Inherit debug info flag to allow debugging the wrapper
3939 if Needs_Debug_Info
(Subp_Id
) then
3940 Set_Debug_Info_Needed
(ICW_Id
);
3951 -- Start of processing for Add_Indirect_Call_Wrapper
3954 pragma Assert
(No
(Indirect_Call_Wrapper
(Subp_Id
)));
3956 ICW_Decl
:= Build_ICW_Decl
;
3958 Append_Freeze_Action
(Tagged_Type
, ICW_Decl
);
3961 ICW_Body
:= Build_ICW_Body
;
3962 Append_Freeze_Action
(Tagged_Type
, ICW_Body
);
3964 -- We cannot defer the analysis of this ICW wrapper when it is
3965 -- built as a consequence of building its partner DTW wrapper
3966 -- at the freezing point of the tagged type.
3968 if Is_Dispatch_Table_Wrapper
(Subp_Id
) then
3971 end Add_Indirect_Call_Wrapper
;
3973 ---------------------
3974 -- Add_Call_Helper --
3975 ---------------------
3977 procedure Add_Call_Helper
3978 (Helper_Id
: Entity_Id
;
3979 Is_Dynamic
: Boolean)
3981 function Build_Call_Helper_Body
return Node_Id
;
3982 -- Build the body of a call helper
3984 function Build_Call_Helper_Decl
return Node_Id
;
3985 -- Build the declaration of a call helper
3987 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
;
3988 -- Build the specification of the helper
3990 ----------------------------
3991 -- Build_Call_Helper_Body --
3992 ----------------------------
3994 function Build_Call_Helper_Body
return Node_Id
is
3996 function Copy_And_Update_References
3997 (Expr
: Node_Id
) return Node_Id
;
3998 -- Copy Expr updating references to formals of Helper_Id; update
3999 -- also references to loop identifiers of quantified expressions.
4001 --------------------------------
4002 -- Copy_And_Update_References --
4003 --------------------------------
4005 function Copy_And_Update_References
4006 (Expr
: Node_Id
) return Node_Id
4008 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4010 procedure Map_Quantified_Expression_Loop_Identifiers
;
4011 -- Traverse Expr and append to Assoc_List the mapping of loop
4012 -- identifers of quantified expressions with its new copy.
4014 ------------------------------------------------
4015 -- Map_Quantified_Expression_Loop_Identifiers --
4016 ------------------------------------------------
4018 procedure Map_Quantified_Expression_Loop_Identifiers
is
4019 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
;
4020 -- Append to Assoc_List the mapping of loop identifers of
4021 -- quantified expressions with its new copy.
4023 --------------------
4024 -- Map_Loop_Param --
4025 --------------------
4027 function Map_Loop_Param
(N
: Node_Id
) return Traverse_Result
4030 if Nkind
(N
) = N_Loop_Parameter_Specification
4031 and then Nkind
(Parent
(N
)) = N_Quantified_Expression
4034 Def_Id
: constant Entity_Id
:=
4035 Defining_Identifier
(N
);
4037 Append_Elmt
(Def_Id
, Assoc_List
);
4038 Append_Elmt
(New_Copy
(Def_Id
), Assoc_List
);
4045 procedure Map_Quantified_Expressions
is
4046 new Traverse_Proc
(Map_Loop_Param
);
4049 Map_Quantified_Expressions
(Expr
);
4050 end Map_Quantified_Expression_Loop_Identifiers
;
4054 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp_Id
);
4055 Helper_Formal_Id
: Entity_Id
:= First_Formal
(Helper_Id
);
4057 -- Start of processing for Copy_And_Update_References
4060 while Present
(Subp_Formal_Id
) loop
4061 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4062 Append_Elmt
(Helper_Formal_Id
, Assoc_List
);
4064 Next_Formal
(Subp_Formal_Id
);
4065 Next_Formal
(Helper_Formal_Id
);
4068 Map_Quantified_Expression_Loop_Identifiers
;
4070 return New_Copy_Tree
(Expr
, Map
=> Assoc_List
);
4071 end Copy_And_Update_References
;
4075 Helper_Decl
: constant Node_Id
:= Parent
(Parent
(Helper_Id
));
4076 Body_Id
: Entity_Id
;
4077 Body_Spec
: Node_Id
;
4078 Body_Stmts
: Node_Id
;
4079 Helper_Body
: Node_Id
;
4080 Return_Expr
: Node_Id
;
4082 -- Start of processing for Build_Call_Helper_Body
4085 pragma Assert
(Analyzed
(Unit_Declaration_Node
(Helper_Id
)));
4086 pragma Assert
(No
(Corresponding_Body
(Helper_Decl
)));
4088 Body_Id
:= Make_Defining_Identifier
(Loc
, Chars
(Helper_Id
));
4089 Body_Spec
:= Build_Call_Helper_Spec
(Body_Id
);
4091 Set_Corresponding_Body
(Helper_Decl
, Body_Id
);
4092 Set_Must_Override
(Body_Spec
, False);
4094 if Present
(Class_Preconditions
(Subp_Id
))
4095 -- Evaluate the expression if we are building a dynamic helper
4096 -- or we are building a static helper for a non-abstract tagged
4097 -- type; for abstract tagged types the helper just returns True
4098 -- since it is called by the indirect call wrapper (ICW).
4102 not Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)))
4105 Copy_And_Update_References
(Class_Preconditions
(Subp_Id
));
4107 -- When the subprogram is compiled with assertions disabled the
4108 -- helper just returns True; done to avoid reporting errors at
4109 -- link time since a unit may be compiled with assertions disabled
4110 -- and another (which depends on it) compiled with assertions
4114 pragma Assert
(Present
(Ignored_Class_Preconditions
(Subp_Id
))
4115 or else Is_Abstract_Type
(Find_Dispatching_Type
(Subp_Id
)));
4116 Return_Expr
:= New_Occurrence_Of
(Standard_True
, Loc
);
4120 Make_Handled_Sequence_Of_Statements
(Loc
,
4121 Statements
=> New_List
(
4122 Make_Simple_Return_Statement
(Loc
, Return_Expr
)));
4125 Make_Subprogram_Body
(Loc
,
4126 Specification
=> Body_Spec
,
4127 Declarations
=> New_List
,
4128 Handled_Statement_Sequence
=> Body_Stmts
);
4131 end Build_Call_Helper_Body
;
4133 ----------------------------
4134 -- Build_Call_Helper_Decl --
4135 ----------------------------
4137 function Build_Call_Helper_Decl
return Node_Id
is
4142 Spec
:= Build_Call_Helper_Spec
(Helper_Id
);
4143 Set_Must_Override
(Spec
, False);
4144 Set_Must_Not_Override
(Spec
, False);
4145 Set_Is_Inlined
(Helper_Id
);
4146 Set_Is_Public
(Helper_Id
);
4148 Decl
:= Make_Subprogram_Declaration
(Loc
, Spec
);
4150 -- Inherit debug info flag from Subp_Id to Helper_Id to allow
4151 -- debugging of the helper subprogram.
4153 if Needs_Debug_Info
(Subp_Id
) then
4154 Set_Debug_Info_Needed
(Helper_Id
);
4158 end Build_Call_Helper_Decl
;
4160 ----------------------------
4161 -- Build_Call_Helper_Spec --
4162 ----------------------------
4164 function Build_Call_Helper_Spec
(Spec_Id
: Entity_Id
) return Node_Id
4166 Spec
: constant Node_Id
:= Parent
(Subp_Id
);
4167 Def_Id
: constant Node_Id
:= Defining_Unit_Name
(Spec
);
4169 Func_Formals
: constant List_Id
:= New_List
;
4170 P_Spec
: constant List_Id
:= Parameter_Specifications
(Spec
);
4171 Par_Formal
: Node_Id
;
4173 Param_Type
: Node_Id
;
4176 -- Create a list of formal parameters with the same types as the
4177 -- original subprogram but changing the controlling formal.
4179 Param
:= First
(P_Spec
);
4180 Formal
:= First_Formal
(Def_Id
);
4181 while Present
(Formal
) loop
4182 Par_Formal
:= Parent
(Formal
);
4184 if Is_Dynamic
and then Is_Controlling_Formal
(Formal
) then
4185 if Nkind
(Parameter_Type
(Par_Formal
))
4186 = N_Access_Definition
4189 Copy_Separate_Tree
(Parameter_Type
(Par_Formal
));
4190 Rewrite
(Subtype_Mark
(Param_Type
),
4191 Make_Attribute_Reference
(Loc
,
4192 Prefix
=> Relocate_Node
(Subtype_Mark
(Param_Type
)),
4193 Attribute_Name
=> Name_Class
));
4197 Make_Attribute_Reference
(Loc
,
4198 Prefix
=> New_Occurrence_Of
(Etype
(Formal
), Loc
),
4199 Attribute_Name
=> Name_Class
);
4202 Param_Type
:= New_Occurrence_Of
(Etype
(Formal
), Loc
);
4205 Append_To
(Func_Formals
,
4206 Make_Parameter_Specification
(Loc
,
4207 Defining_Identifier
=>
4208 Make_Defining_Identifier
(Loc
, Chars
(Formal
)),
4209 In_Present
=> In_Present
(Par_Formal
),
4210 Out_Present
=> Out_Present
(Par_Formal
),
4211 Null_Exclusion_Present
=> Null_Exclusion_Present
4213 Parameter_Type
=> Param_Type
));
4216 Next_Formal
(Formal
);
4220 Make_Function_Specification
(Loc
,
4221 Defining_Unit_Name
=> Spec_Id
,
4222 Parameter_Specifications
=> Func_Formals
,
4223 Result_Definition
=>
4224 New_Occurrence_Of
(Standard_Boolean
, Loc
));
4225 end Build_Call_Helper_Spec
;
4229 Helper_Body
: Node_Id
;
4230 Helper_Decl
: Node_Id
;
4232 -- Start of processing for Add_Call_Helper
4235 Helper_Decl
:= Build_Call_Helper_Decl
;
4236 Mutate_Ekind
(Helper_Id
, Ekind
(Subp_Id
));
4238 -- Add the helper to the freezing actions of the tagged type
4240 Append_Freeze_Action
(Tagged_Type
, Helper_Decl
);
4241 Analyze
(Helper_Decl
);
4243 Helper_Body
:= Build_Call_Helper_Body
;
4244 Append_Freeze_Action
(Tagged_Type
, Helper_Body
);
4246 -- If this helper is built as part of building the DTW at the
4247 -- freezing point of its tagged type then we cannot defer
4250 if Late_Overriding
then
4251 pragma Assert
(Is_Dispatch_Table_Wrapper
(Subp_Id
));
4252 Analyze
(Helper_Body
);
4254 end Add_Call_Helper
;
4256 -----------------------
4257 -- Build_Unique_Name --
4258 -----------------------
4260 function Build_Unique_Name
(Suffix
: String) return Name_Id
is
4262 -- Append the homonym number. Strip the leading space character in
4263 -- the image of natural numbers. Also do not add the homonym value
4266 if Has_Homonym
(Subp_Id
) and then Homonym_Number
(Subp_Id
) > 1 then
4268 S
: constant String := Homonym_Number
(Subp_Id
)'Img;
4271 return New_External_Name
(Chars
(Subp_Id
),
4272 Suffix
=> Suffix
& "_" & S
(2 .. S
'Last));
4276 return New_External_Name
(Chars
(Subp_Id
), Suffix
);
4277 end Build_Unique_Name
;
4281 Helper_Id
: Entity_Id
;
4283 -- Start of processing for Make_Class_Precondition_Subps
4286 if Present
(Class_Preconditions
(Subp_Id
))
4287 or Present
(Ignored_Class_Preconditions
(Subp_Id
))
4290 (Comes_From_Source
(Subp_Id
)
4291 or else Is_Dispatch_Table_Wrapper
(Subp_Id
));
4293 if No
(Dynamic_Call_Helper
(Subp_Id
)) then
4295 -- Build and add to the freezing actions of Tagged_Type its
4296 -- dynamic-call helper.
4299 Make_Defining_Identifier
(Loc
,
4300 Build_Unique_Name
(Suffix
=> "DP"));
4301 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> True);
4303 -- Link original subprogram to helper and vice versa
4305 Set_Dynamic_Call_Helper
(Subp_Id
, Helper_Id
);
4306 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4309 if not Is_Abstract_Subprogram
(Subp_Id
)
4310 and then No
(Static_Call_Helper
(Subp_Id
))
4312 -- Build and add to the freezing actions of Tagged_Type its
4313 -- static-call helper.
4316 Make_Defining_Identifier
(Loc
,
4317 Build_Unique_Name
(Suffix
=> "SP"));
4319 Add_Call_Helper
(Helper_Id
, Is_Dynamic
=> False);
4321 -- Link original subprogram to helper and vice versa
4323 Set_Static_Call_Helper
(Subp_Id
, Helper_Id
);
4324 Set_Class_Preconditions_Subprogram
(Helper_Id
, Subp_Id
);
4326 -- Build and add to the freezing actions of Tagged_Type the
4327 -- indirect-call wrapper.
4329 Add_Indirect_Call_Wrapper
;
4332 end Make_Class_Precondition_Subps
;
4334 ----------------------------------------------
4335 -- Process_Class_Conditions_At_Freeze_Point --
4336 ----------------------------------------------
4338 procedure Process_Class_Conditions_At_Freeze_Point
(Typ
: Entity_Id
) is
4340 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
);
4341 -- Check class-wide pre/postconditions of Spec_Id
4343 function Has_Class_Postconditions_Subprogram
4344 (Spec_Id
: Entity_Id
) return Boolean;
4345 -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
4347 function Has_Class_Preconditions_Subprogram
4348 (Spec_Id
: Entity_Id
) return Boolean;
4349 -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
4351 ----------------------------
4352 -- Check_Class_Conditions --
4353 ----------------------------
4355 procedure Check_Class_Conditions
(Spec_Id
: Entity_Id
) is
4356 Par_Subp
: Entity_Id
;
4359 for Kind
in Condition_Kind
loop
4360 Par_Subp
:= Nearest_Class_Condition_Subprogram
(Kind
, Spec_Id
);
4362 if Present
(Par_Subp
) then
4363 Check_Class_Condition
4364 (Cond
=> Class_Condition
(Kind
, Par_Subp
),
4366 Par_Subp
=> Par_Subp
,
4367 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4368 | Class_Precondition
);
4371 end Check_Class_Conditions
;
4373 -----------------------------------------
4374 -- Has_Class_Postconditions_Subprogram --
4375 -----------------------------------------
4377 function Has_Class_Postconditions_Subprogram
4378 (Spec_Id
: Entity_Id
) return Boolean is
4381 Present
(Nearest_Class_Condition_Subprogram
4382 (Spec_Id
=> Spec_Id
,
4383 Kind
=> Class_Postcondition
))
4385 Present
(Nearest_Class_Condition_Subprogram
4386 (Spec_Id
=> Spec_Id
,
4387 Kind
=> Ignored_Class_Postcondition
));
4388 end Has_Class_Postconditions_Subprogram
;
4390 ----------------------------------------
4391 -- Has_Class_Preconditions_Subprogram --
4392 ----------------------------------------
4394 function Has_Class_Preconditions_Subprogram
4395 (Spec_Id
: Entity_Id
) return Boolean is
4398 Present
(Nearest_Class_Condition_Subprogram
4399 (Spec_Id
=> Spec_Id
,
4400 Kind
=> Class_Precondition
))
4402 Present
(Nearest_Class_Condition_Subprogram
4403 (Spec_Id
=> Spec_Id
,
4404 Kind
=> Ignored_Class_Precondition
));
4405 end Has_Class_Preconditions_Subprogram
;
4409 Prim_Elmt
: Elmt_Id
:= First_Elmt
(Primitive_Operations
(Typ
));
4412 -- Start of processing for Process_Class_Conditions_At_Freeze_Point
4415 while Present
(Prim_Elmt
) loop
4416 Prim
:= Node
(Prim_Elmt
);
4418 if Has_Class_Preconditions_Subprogram
(Prim
)
4419 or else Has_Class_Postconditions_Subprogram
(Prim
)
4421 if Comes_From_Source
(Prim
) then
4422 if Has_Significant_Contract
(Prim
) then
4423 Merge_Class_Conditions
(Prim
);
4426 -- Handle wrapper of protected operation
4428 elsif Is_Primitive_Wrapper
(Prim
) then
4429 Merge_Class_Conditions
(Prim
);
4431 -- Check inherited class-wide conditions, excluding internal
4432 -- entities built for mapping of interface primitives.
4434 elsif Is_Derived_Type
(Typ
)
4435 and then Present
(Alias
(Prim
))
4436 and then No
(Interface_Alias
(Prim
))
4438 Check_Class_Conditions
(Prim
);
4442 Next_Elmt
(Prim_Elmt
);
4444 end Process_Class_Conditions_At_Freeze_Point
;
4446 ----------------------------
4447 -- Merge_Class_Conditions --
4448 ----------------------------
4450 procedure Merge_Class_Conditions
(Spec_Id
: Entity_Id
) is
4452 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
);
4453 -- Collect all inherited class-wide conditions of Spec_Id and merge
4454 -- them into one big condition.
4456 ----------------------------------
4457 -- Process_Inherited_Conditions --
4458 ----------------------------------
4460 procedure Process_Inherited_Conditions
(Kind
: Condition_Kind
) is
4461 Tag_Typ
: constant Entity_Id
:= Find_Dispatching_Type
(Spec_Id
);
4462 Subps
: constant Subprogram_List
:= Inherited_Subprograms
(Spec_Id
);
4463 Seen
: Subprogram_List
(Subps
'Range) := (others => Empty
);
4465 function Inherit_Condition
4466 (Par_Subp
: Entity_Id
;
4467 Subp
: Entity_Id
) return Node_Id
;
4468 -- Inherit the class-wide condition from Par_Subp to Subp and adjust
4469 -- all the references to formals in the inherited condition.
4471 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
);
4472 -- Merge two class-wide preconditions or postconditions (the former
4473 -- are merged using "or else", and the latter are merged using "and-
4474 -- then"). The changes are accumulated in parameter Into.
4476 function Seen_Subp
(Id
: Entity_Id
) return Boolean;
4477 -- Return True if the contract of subprogram Id has been processed
4479 -----------------------
4480 -- Inherit_Condition --
4481 -----------------------
4483 function Inherit_Condition
4484 (Par_Subp
: Entity_Id
;
4485 Subp
: Entity_Id
) return Node_Id
4487 function Check_Condition
(Expr
: Node_Id
) return Boolean;
4488 -- Used in assertion to check that Expr has no reference to the
4489 -- formals of Par_Subp.
4491 ---------------------
4492 -- Check_Condition --
4493 ---------------------
4495 function Check_Condition
(Expr
: Node_Id
) return Boolean is
4496 Par_Formal_Id
: Entity_Id
;
4498 function Check_Entity
(N
: Node_Id
) return Traverse_Result
;
4499 -- Check occurrence of Par_Formal_Id
4505 function Check_Entity
(N
: Node_Id
) return Traverse_Result
is
4507 if Nkind
(N
) = N_Identifier
4508 and then Present
(Entity
(N
))
4509 and then Entity
(N
) = Par_Formal_Id
4517 function Check_Expression
is new Traverse_Func
(Check_Entity
);
4519 -- Start of processing for Check_Condition
4522 Par_Formal_Id
:= First_Formal
(Par_Subp
);
4524 while Present
(Par_Formal_Id
) loop
4525 if Check_Expression
(Expr
) = Abandon
then
4529 Next_Formal
(Par_Formal_Id
);
4533 end Check_Condition
;
4537 Assoc_List
: constant Elist_Id
:= New_Elmt_List
;
4538 Par_Formal_Id
: Entity_Id
:= First_Formal
(Par_Subp
);
4539 Subp_Formal_Id
: Entity_Id
:= First_Formal
(Subp
);
4540 New_Condition
: Node_Id
;
4543 while Present
(Par_Formal_Id
) loop
4544 Append_Elmt
(Par_Formal_Id
, Assoc_List
);
4545 Append_Elmt
(Subp_Formal_Id
, Assoc_List
);
4547 Next_Formal
(Par_Formal_Id
);
4548 Next_Formal
(Subp_Formal_Id
);
4551 -- Check that Parent field of all the nodes have their correct
4552 -- decoration; required because otherwise mapped nodes with
4553 -- wrong Parent field are left unmodified in the copied tree
4554 -- and cause reporting wrong errors at later stages.
4557 (Check_Parents
(Class_Condition
(Kind
, Par_Subp
), Assoc_List
));
4561 (Source
=> Class_Condition
(Kind
, Par_Subp
),
4564 -- Ensure that the inherited condition has no reference to the
4565 -- formals of the parent subprogram.
4567 pragma Assert
(Check_Condition
(New_Condition
));
4569 return New_Condition
;
4570 end Inherit_Condition
;
4572 ----------------------
4573 -- Merge_Conditions --
4574 ----------------------
4576 procedure Merge_Conditions
(From
: Node_Id
; Into
: Node_Id
) is
4577 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
;
4578 -- Return the boolean expression argument of a condition while
4579 -- updating its parentheses count for the subsequent merge.
4581 --------------------
4582 -- Expression_Arg --
4583 --------------------
4585 function Expression_Arg
(Expr
: Node_Id
) return Node_Id
is
4587 if Paren_Count
(Expr
) = 0 then
4588 Set_Paren_Count
(Expr
, 1);
4596 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
4597 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
4598 Loc
: constant Source_Ptr
:= Sloc
(Into
);
4600 -- Start of processing for Merge_Conditions
4605 -- Merge the two preconditions by "or else"-ing them
4607 when Ignored_Class_Precondition
4608 | Class_Precondition
4612 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4613 Left_Opnd
=> From_Expr
));
4615 -- Merge the two postconditions by "and then"-ing them
4617 when Ignored_Class_Postcondition
4618 | Class_Postcondition
4622 Right_Opnd
=> Relocate_Node
(Into_Expr
),
4623 Left_Opnd
=> From_Expr
));
4625 end Merge_Conditions
;
4631 function Seen_Subp
(Id
: Entity_Id
) return Boolean is
4633 for Index
in Seen
'Range loop
4634 if Seen
(Index
) = Id
then
4644 Class_Cond
: Node_Id
;
4646 Subp_Id
: Entity_Id
;
4647 Par_Prim
: Entity_Id
:= Empty
;
4648 Par_Iface_Prims
: Elist_Id
:= No_Elist
;
4650 -- Start of processing for Process_Inherited_Conditions
4653 Class_Cond
:= Class_Condition
(Kind
, Spec_Id
);
4655 -- Process parent primitives looking for nearest ancestor with
4656 -- class-wide conditions.
4658 for Index
in Subps
'Range loop
4659 Subp_Id
:= Subps
(Index
);
4662 and then Is_Ancestor
(Find_Dispatching_Type
(Subp_Id
), Tag_Typ
)
4664 if Present
(Alias
(Subp_Id
)) then
4665 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4668 -- Wrappers of class-wide pre/postconditions reference the
4669 -- parent primitive that has the inherited contract and help
4670 -- us to climb fast.
4672 if Is_Wrapper
(Subp_Id
)
4673 and then Present
(LSP_Subprogram
(Subp_Id
))
4675 Subp_Id
:= LSP_Subprogram
(Subp_Id
);
4678 if not Seen_Subp
(Subp_Id
)
4679 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4681 Seen
(Index
) := Subp_Id
;
4682 Par_Prim
:= Subp_Id
;
4683 Par_Iface_Prims
:= Covered_Interface_Primitives
(Par_Prim
);
4685 Cond
:= Inherit_Condition
4687 Par_Subp
=> Subp_Id
);
4689 if Present
(Class_Cond
) then
4690 Merge_Conditions
(Cond
, Class_Cond
);
4695 Check_Class_Condition
4696 (Cond
=> Class_Cond
,
4698 Par_Subp
=> Subp_Id
,
4699 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4700 | Class_Precondition
);
4701 Build_Class_Wide_Expression
4702 (Pragma_Or_Expr
=> Class_Cond
,
4704 Par_Subp
=> Subp_Id
,
4705 Adjust_Sloc
=> False);
4707 -- We are done as soon as we process the nearest ancestor
4714 -- Process the contract of interface primitives not covered by
4715 -- the nearest ancestor.
4717 for Index
in Subps
'Range loop
4718 Subp_Id
:= Subps
(Index
);
4720 if Is_Interface
(Find_Dispatching_Type
(Subp_Id
)) then
4721 if Present
(Alias
(Subp_Id
)) then
4722 Subp_Id
:= Ultimate_Alias
(Subp_Id
);
4725 if not Seen_Subp
(Subp_Id
)
4726 and then Present
(Class_Condition
(Kind
, Subp_Id
))
4727 and then not Contains
(Par_Iface_Prims
, Subp_Id
)
4729 Seen
(Index
) := Subp_Id
;
4731 Cond
:= Inherit_Condition
4733 Par_Subp
=> Subp_Id
);
4735 Check_Class_Condition
4738 Par_Subp
=> Subp_Id
,
4739 Is_Precondition
=> Kind
in Ignored_Class_Precondition
4740 | Class_Precondition
);
4741 Build_Class_Wide_Expression
4742 (Pragma_Or_Expr
=> Cond
,
4744 Par_Subp
=> Subp_Id
,
4745 Adjust_Sloc
=> False);
4747 if Present
(Class_Cond
) then
4748 Merge_Conditions
(Cond
, Class_Cond
);
4756 Set_Class_Condition
(Kind
, Spec_Id
, Class_Cond
);
4757 end Process_Inherited_Conditions
;
4763 -- Start of processing for Merge_Class_Conditions
4766 for Kind
in Condition_Kind
loop
4767 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4769 -- If this subprogram has class-wide conditions then preanalyze
4770 -- them before processing inherited conditions since conditions
4771 -- are checked and merged from right to left.
4773 if Present
(Cond
) then
4774 Preanalyze_Condition
(Spec_Id
, Cond
);
4777 Process_Inherited_Conditions
(Kind
);
4779 -- Preanalyze merged inherited conditions
4781 if Cond
/= Class_Condition
(Kind
, Spec_Id
) then
4782 Preanalyze_Condition
(Spec_Id
,
4783 Class_Condition
(Kind
, Spec_Id
));
4786 end Merge_Class_Conditions
;
4788 ---------------------------------
4789 -- Preanalyze_Class_Conditions --
4790 ---------------------------------
4792 procedure Preanalyze_Class_Conditions
(Spec_Id
: Entity_Id
) is
4796 for Kind
in Condition_Kind
loop
4797 Cond
:= Class_Condition
(Kind
, Spec_Id
);
4799 if Present
(Cond
) then
4800 Preanalyze_Condition
(Spec_Id
, Cond
);
4803 end Preanalyze_Class_Conditions
;
4805 --------------------------
4806 -- Preanalyze_Condition --
4807 --------------------------
4809 procedure Preanalyze_Condition
4813 procedure Clear_Unset_References
;
4814 -- Clear unset references on formals of Subp since preanalysis
4815 -- occurs in a place unrelated to the actual code.
4817 procedure Remove_Controlling_Arguments
;
4818 -- Traverse Expr and clear the Controlling_Argument of calls to
4819 -- nonabstract functions.
4821 procedure Remove_Formals
(Id
: Entity_Id
);
4822 -- Remove formals from homonym chains and make them not visible
4824 procedure Restore_Original_Selected_Component
;
4825 -- Traverse Expr searching for dispatching calls to functions whose
4826 -- original node was a selected component, and replace them with
4827 -- their original node.
4829 ----------------------------
4830 -- Clear_Unset_References --
4831 ----------------------------
4833 procedure Clear_Unset_References
is
4834 F
: Entity_Id
:= First_Formal
(Subp
);
4837 while Present
(F
) loop
4838 Set_Unset_Reference
(F
, Empty
);
4841 end Clear_Unset_References
;
4843 ----------------------------------
4844 -- Remove_Controlling_Arguments --
4845 ----------------------------------
4847 procedure Remove_Controlling_Arguments
is
4848 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
;
4849 -- Reset the Controlling_Argument of calls to nonabstract
4852 ---------------------
4853 -- Remove_Ctrl_Arg --
4854 ---------------------
4856 function Remove_Ctrl_Arg
(N
: Node_Id
) return Traverse_Result
is
4858 if Nkind
(N
) = N_Function_Call
4859 and then Present
(Controlling_Argument
(N
))
4860 and then not Is_Abstract_Subprogram
(Entity
(Name
(N
)))
4862 Set_Controlling_Argument
(N
, Empty
);
4866 end Remove_Ctrl_Arg
;
4868 procedure Remove_Ctrl_Args
is new Traverse_Proc
(Remove_Ctrl_Arg
);
4870 Remove_Ctrl_Args
(Expr
);
4871 end Remove_Controlling_Arguments
;
4873 --------------------
4874 -- Remove_Formals --
4875 --------------------
4877 procedure Remove_Formals
(Id
: Entity_Id
) is
4878 F
: Entity_Id
:= First_Formal
(Id
);
4881 while Present
(F
) loop
4882 Set_Is_Immediately_Visible
(F
, False);
4888 -----------------------------------------
4889 -- Restore_Original_Selected_Component --
4890 -----------------------------------------
4892 procedure Restore_Original_Selected_Component
is
4893 Restored_Nodes_List
: Elist_Id
:= No_Elist
;
4895 procedure Fix_Parents
(N
: Node_Id
);
4896 -- Traverse the subtree of N fixing the Parent field of all the
4899 function Restore_Node
(N
: Node_Id
) return Traverse_Result
;
4900 -- Process dispatching calls to functions whose original node was
4901 -- a selected component, and replace them with their original
4902 -- node. Restored nodes are stored in the Restored_Nodes_List
4903 -- to fix the parent fields of their subtrees in a separate
4910 procedure Fix_Parents
(N
: Node_Id
) is
4913 (Parent_Node
: Node_Id
;
4914 Node
: Node_Id
) return Traverse_Result
;
4915 -- Process a single node
4922 (Parent_Node
: Node_Id
;
4923 Node
: Node_Id
) return Traverse_Result
4925 Par
: constant Node_Id
:= Parent
(Node
);
4928 if Par
/= Parent_Node
then
4929 pragma Assert
(not Is_List_Member
(Node
));
4930 Set_Parent
(Node
, Parent_Node
);
4936 procedure Fix_Parents
is
4937 new Traverse_Proc_With_Parent
(Fix_Parent
);
4947 function Restore_Node
(N
: Node_Id
) return Traverse_Result
is
4949 if Nkind
(N
) = N_Function_Call
4950 and then Nkind
(Original_Node
(N
)) = N_Selected_Component
4951 and then Is_Dispatching_Operation
(Entity
(Name
(N
)))
4953 Rewrite
(N
, Original_Node
(N
));
4954 Set_Original_Node
(N
, N
);
4956 -- Save the restored node in the Restored_Nodes_List to fix
4957 -- the parent fields of their subtrees in a separate tree
4960 Append_New_Elmt
(N
, Restored_Nodes_List
);
4966 procedure Restore_Nodes
is new Traverse_Proc
(Restore_Node
);
4968 -- Start of processing for Restore_Original_Selected_Component
4971 Restore_Nodes
(Expr
);
4973 -- After restoring the original node we must fix the decoration
4974 -- of the Parent attribute to ensure tree consistency; required
4975 -- because when the class-wide condition is inherited, calls to
4976 -- New_Copy_Tree will perform copies of this subtree, and formal
4977 -- occurrences with wrong Parent field cannot be mapped to the
4980 if Present
(Restored_Nodes_List
) then
4982 Elmt
: Elmt_Id
:= First_Elmt
(Restored_Nodes_List
);
4985 while Present
(Elmt
) loop
4986 Fix_Parents
(Node
(Elmt
));
4991 end Restore_Original_Selected_Component
;
4993 -- Start of processing for Preanalyze_Condition
4996 pragma Assert
(Present
(Expr
));
4997 pragma Assert
(Inside_Class_Condition_Preanalysis
= False);
5000 Install_Formals
(Subp
);
5001 Inside_Class_Condition_Preanalysis
:= True;
5003 Preanalyze_Spec_Expression
(Expr
, Standard_Boolean
);
5005 Inside_Class_Condition_Preanalysis
:= False;
5006 Remove_Formals
(Subp
);
5009 -- If this preanalyzed condition has occurrences of dispatching calls
5010 -- using the Object.Operation notation, during preanalysis such calls
5011 -- are rewritten as dispatching function calls; if at later stages
5012 -- this condition is inherited we must have restored the original
5013 -- selected-component node to ensure that the preanalysis of the
5014 -- inherited condition rewrites these dispatching calls in the
5015 -- correct context to avoid reporting spurious errors.
5017 Restore_Original_Selected_Component
;
5019 -- Traverse Expr and clear the Controlling_Argument of calls to
5020 -- nonabstract functions. Required since the preanalyzed condition
5021 -- is not yet installed on its definite context and will be cloned
5022 -- and extended in derivations with additional conditions.
5024 Remove_Controlling_Arguments
;
5026 -- Clear also attribute Unset_Reference; again because preanalysis
5027 -- occurs in a place unrelated to the actual code.
5029 Clear_Unset_References
;
5030 end Preanalyze_Condition
;
5032 ----------------------------------------
5033 -- Save_Global_References_In_Contract --
5034 ----------------------------------------
5036 procedure Save_Global_References_In_Contract
5040 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
5041 -- Save all global references in contract-related source pragmas found
5042 -- in the list, starting with pragma First_Prag.
5044 ------------------------------------
5045 -- Save_Global_References_In_List --
5046 ------------------------------------
5048 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
5049 Prag
: Node_Id
:= First_Prag
;
5052 while Present
(Prag
) loop
5053 if Is_Generic_Contract_Pragma
(Prag
) then
5054 Save_Global_References
(Prag
);
5057 Prag
:= Next_Pragma
(Prag
);
5059 end Save_Global_References_In_List
;
5063 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
5065 -- Start of processing for Save_Global_References_In_Contract
5068 -- The entity of the analyzed generic copy must be on the scope stack
5069 -- to ensure proper detection of global references.
5071 Push_Scope
(Gen_Id
);
5073 if Permits_Aspect_Specifications
(Templ
)
5074 and then Has_Aspects
(Templ
)
5076 Save_Global_References_In_Aspects
(Templ
);
5079 if Present
(Items
) then
5080 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
5081 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
5082 Save_Global_References_In_List
(Classifications
(Items
));
5086 end Save_Global_References_In_Contract
;
5088 -------------------------
5089 -- Set_Class_Condition --
5090 -------------------------
5092 procedure Set_Class_Condition
5093 (Kind
: Condition_Kind
;
5099 when Class_Postcondition
=>
5100 Set_Class_Postconditions
(Subp
, Cond
);
5102 when Class_Precondition
=>
5103 Set_Class_Preconditions
(Subp
, Cond
);
5105 when Ignored_Class_Postcondition
=>
5106 Set_Ignored_Class_Postconditions
(Subp
, Cond
);
5108 when Ignored_Class_Precondition
=>
5109 Set_Ignored_Class_Preconditions
(Subp
, Cond
);
5111 end Set_Class_Condition
;