1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- C O N T R A C T S --
9 -- Copyright (C) 2015-2018, 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 Debug
; use Debug
;
29 with Einfo
; use Einfo
;
30 with Elists
; use Elists
;
31 with Errout
; use Errout
;
32 with Exp_Prag
; use Exp_Prag
;
33 with Exp_Tss
; use Exp_Tss
;
34 with Exp_Util
; use Exp_Util
;
35 with Namet
; use Namet
;
36 with Nlists
; use Nlists
;
37 with Nmake
; use Nmake
;
40 with Sem_Aux
; use Sem_Aux
;
41 with Sem_Ch6
; use Sem_Ch6
;
42 with Sem_Ch8
; use Sem_Ch8
;
43 with Sem_Ch12
; use Sem_Ch12
;
44 with Sem_Ch13
; use Sem_Ch13
;
45 with Sem_Disp
; use Sem_Disp
;
46 with Sem_Prag
; use Sem_Prag
;
47 with Sem_Util
; use Sem_Util
;
48 with Sinfo
; use Sinfo
;
49 with Snames
; use Snames
;
50 with Stringt
; use Stringt
;
51 with SCIL_LL
; use SCIL_LL
;
52 with Tbuild
; use Tbuild
;
54 package body Contracts
is
56 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
);
57 -- Analyze all delayed pragmas chained on the contract of package
58 -- instantiation Inst_Id as if they appear at the end of a declarative
59 -- region. The pragmas in question are:
63 procedure Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
);
64 -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
65 -- contract-only subprogram body of eligible subprograms found in L, adds
66 -- them to their corresponding list of declarations, and analyzes them.
68 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
);
69 -- Expand the contracts of a subprogram body and its correspoding spec (if
70 -- any). This routine processes all [refined] pre- and postconditions as
71 -- well as Contract_Cases, invariants and predicates. Body_Id denotes the
72 -- entity of the subprogram body.
74 -----------------------
75 -- Add_Contract_Item --
76 -----------------------
78 procedure Add_Contract_Item
(Prag
: Node_Id
; Id
: Entity_Id
) is
79 Items
: Node_Id
:= Contract
(Id
);
81 procedure Add_Classification
;
82 -- Prepend Prag to the list of classifications
84 procedure Add_Contract_Test_Case
;
85 -- Prepend Prag to the list of contract and test cases
87 procedure Add_Pre_Post_Condition
;
88 -- Prepend Prag to the list of pre- and postconditions
90 ------------------------
91 -- Add_Classification --
92 ------------------------
94 procedure Add_Classification
is
96 Set_Next_Pragma
(Prag
, Classifications
(Items
));
97 Set_Classifications
(Items
, Prag
);
98 end Add_Classification
;
100 ----------------------------
101 -- Add_Contract_Test_Case --
102 ----------------------------
104 procedure Add_Contract_Test_Case
is
106 Set_Next_Pragma
(Prag
, Contract_Test_Cases
(Items
));
107 Set_Contract_Test_Cases
(Items
, Prag
);
108 end Add_Contract_Test_Case
;
110 ----------------------------
111 -- Add_Pre_Post_Condition --
112 ----------------------------
114 procedure Add_Pre_Post_Condition
is
116 Set_Next_Pragma
(Prag
, Pre_Post_Conditions
(Items
));
117 Set_Pre_Post_Conditions
(Items
, Prag
);
118 end Add_Pre_Post_Condition
;
122 -- A contract must contain only pragmas
124 pragma Assert
(Nkind
(Prag
) = N_Pragma
);
125 Prag_Nam
: constant Name_Id
:= Pragma_Name
(Prag
);
127 -- Start of processing for Add_Contract_Item
130 -- Create a new contract when adding the first item
133 Items
:= Make_Contract
(Sloc
(Id
));
134 Set_Contract
(Id
, Items
);
137 -- Constants, the applicable pragmas are:
140 if Ekind
(Id
) = E_Constant
then
141 if Prag_Nam
= Name_Part_Of
then
144 -- The pragma is not a proper contract item
150 -- Entry bodies, the applicable pragmas are:
155 elsif Is_Entry_Body
(Id
) then
156 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
159 elsif Prag_Nam
= Name_Refined_Post
then
160 Add_Pre_Post_Condition
;
162 -- The pragma is not a proper contract item
168 -- Entry or subprogram declarations, the applicable pragmas are:
172 -- Extensions_Visible
180 elsif Is_Entry_Declaration
(Id
)
181 or else Ekind_In
(Id
, E_Function
,
186 if Nam_In
(Prag_Nam
, Name_Attach_Handler
, Name_Interrupt_Handler
)
187 and then Ekind_In
(Id
, E_Generic_Procedure
, E_Procedure
)
191 elsif Nam_In
(Prag_Nam
, Name_Depends
,
192 Name_Extensions_Visible
,
197 elsif Prag_Nam
= Name_Volatile_Function
198 and then Ekind_In
(Id
, E_Function
, E_Generic_Function
)
202 elsif Nam_In
(Prag_Nam
, Name_Contract_Cases
, Name_Test_Case
) then
203 Add_Contract_Test_Case
;
205 elsif Nam_In
(Prag_Nam
, Name_Postcondition
, Name_Precondition
) then
206 Add_Pre_Post_Condition
;
208 -- The pragma is not a proper contract item
214 -- Packages or instantiations, the applicable pragmas are:
218 -- Part_Of (instantiation only)
220 elsif Ekind_In
(Id
, E_Generic_Package
, E_Package
) then
221 if Nam_In
(Prag_Nam
, Name_Abstract_State
,
222 Name_Initial_Condition
,
227 -- Indicator Part_Of must be associated with a package instantiation
229 elsif Prag_Nam
= Name_Part_Of
and then Is_Generic_Instance
(Id
) then
232 -- The pragma is not a proper contract item
238 -- Package bodies, the applicable pragmas are:
241 elsif Ekind
(Id
) = E_Package_Body
then
242 if Prag_Nam
= Name_Refined_State
then
245 -- The pragma is not a proper contract item
251 -- Protected units, the applicable pragmas are:
254 elsif Ekind
(Id
) = E_Protected_Type
then
255 if Prag_Nam
= Name_Part_Of
then
258 -- The pragma is not a proper contract item
264 -- Subprogram bodies, the applicable pragmas are:
271 elsif Ekind
(Id
) = E_Subprogram_Body
then
272 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
275 elsif Nam_In
(Prag_Nam
, Name_Postcondition
,
279 Add_Pre_Post_Condition
;
281 -- The pragma is not a proper contract item
287 -- Task bodies, the applicable pragmas are:
291 elsif Ekind
(Id
) = E_Task_Body
then
292 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
295 -- The pragma is not a proper contract item
301 -- Task units, the applicable pragmas are:
306 elsif Ekind
(Id
) = E_Task_Type
then
307 if Nam_In
(Prag_Nam
, Name_Depends
, Name_Global
, Name_Part_Of
) then
310 -- The pragma is not a proper contract item
316 -- Variables, the applicable pragmas are:
319 -- Constant_After_Elaboration
326 elsif Ekind
(Id
) = E_Variable
then
327 if Nam_In
(Prag_Nam
, Name_Async_Readers
,
329 Name_Constant_After_Elaboration
,
331 Name_Effective_Reads
,
332 Name_Effective_Writes
,
338 -- The pragma is not a proper contract item
344 end Add_Contract_Item
;
346 -----------------------
347 -- Analyze_Contracts --
348 -----------------------
350 procedure Analyze_Contracts
(L
: List_Id
) is
354 if CodePeer_Mode
and then Debug_Flag_Dot_KK
then
355 Build_And_Analyze_Contract_Only_Subprograms
(L
);
359 while Present
(Decl
) loop
361 -- Entry or subprogram declarations
363 if Nkind_In
(Decl
, N_Abstract_Subprogram_Declaration
,
365 N_Generic_Subprogram_Declaration
,
366 N_Subprogram_Declaration
)
369 Subp_Id
: constant Entity_Id
:= Defining_Entity
(Decl
);
372 Analyze_Entry_Or_Subprogram_Contract
(Subp_Id
);
374 -- If analysis of a class-wide pre/postcondition indicates
375 -- that a class-wide clone is needed, analyze its declaration
376 -- now. Its body is created when the body of the original
377 -- operation is analyzed (and rewritten).
379 if Is_Subprogram
(Subp_Id
)
380 and then Present
(Class_Wide_Clone
(Subp_Id
))
382 Analyze
(Unit_Declaration_Node
(Class_Wide_Clone
(Subp_Id
)));
386 -- Entry or subprogram bodies
388 elsif Nkind_In
(Decl
, N_Entry_Body
, N_Subprogram_Body
) then
389 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
393 elsif Nkind
(Decl
) = N_Object_Declaration
then
394 Analyze_Object_Contract
(Defining_Entity
(Decl
));
396 -- Package instantiation
398 elsif Nkind
(Decl
) = N_Package_Instantiation
then
399 Analyze_Package_Instantiation_Contract
(Defining_Entity
(Decl
));
403 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
404 N_Single_Protected_Declaration
)
406 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
408 -- Subprogram body stubs
410 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
411 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
415 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
416 N_Task_Type_Declaration
)
418 Analyze_Task_Contract
(Defining_Entity
(Decl
));
420 -- For type declarations, we need to do the preanalysis of Iterable
421 -- aspect specifications.
423 -- Other type aspects need to be resolved here???
425 elsif Nkind
(Decl
) = N_Private_Type_Declaration
426 and then Present
(Aspect_Specifications
(Decl
))
429 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
430 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
434 Validate_Iterable_Aspect
(E
, It
);
441 end Analyze_Contracts
;
443 -----------------------------------------------
444 -- Analyze_Entry_Or_Subprogram_Body_Contract --
445 -----------------------------------------------
447 -- WARNING: This routine manages SPARK regions. Return statements must be
448 -- replaced by gotos which jump to the end of the routine and restore the
451 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
452 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
453 Items
: constant Node_Id
:= Contract
(Body_Id
);
454 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
456 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
457 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
458 -- Save the SPARK_Mode-related data to restore on exit
461 -- When a subprogram body declaration is illegal, its defining entity is
462 -- left unanalyzed. There is nothing left to do in this case because the
463 -- body lacks a contract, or even a proper Ekind.
465 if Ekind
(Body_Id
) = E_Void
then
468 -- Do not analyze a contract multiple times
470 elsif Present
(Items
) then
471 if Analyzed
(Items
) then
474 Set_Analyzed
(Items
);
478 -- Due to the timing of contract analysis, delayed pragmas may be
479 -- subject to the wrong SPARK_Mode, usually that of the enclosing
480 -- context. To remedy this, restore the original SPARK_Mode of the
481 -- related subprogram body.
483 Set_SPARK_Mode
(Body_Id
);
485 -- Ensure that the contract cases or postconditions mention 'Result or
486 -- define a post-state.
488 Check_Result_And_Post_State
(Body_Id
);
490 -- A stand-alone nonvolatile function body cannot have an effectively
491 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
492 -- check is relevant only when SPARK_Mode is on, as it is not a standard
493 -- legality rule. The check is performed here because Volatile_Function
494 -- is processed after the analysis of the related subprogram body. The
495 -- check only applies to source subprograms and not to generated TSS
499 and then Ekind_In
(Body_Id
, E_Function
, E_Generic_Function
)
500 and then Comes_From_Source
(Spec_Id
)
501 and then not Is_Volatile_Function
(Body_Id
)
503 Check_Nonvolatile_Function_Profile
(Body_Id
);
506 -- Restore the SPARK_Mode of the enclosing context after all delayed
507 -- pragmas have been analyzed.
509 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
511 -- Capture all global references in a generic subprogram body now that
512 -- the contract has been analyzed.
514 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
515 Save_Global_References_In_Contract
516 (Templ
=> Original_Node
(Body_Decl
),
520 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
521 -- invariants and predicates associated with body and its spec. Do not
522 -- expand the contract of subprogram body stubs.
524 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
525 Expand_Subprogram_Contract
(Body_Id
);
527 end Analyze_Entry_Or_Subprogram_Body_Contract
;
529 ------------------------------------------
530 -- Analyze_Entry_Or_Subprogram_Contract --
531 ------------------------------------------
533 -- WARNING: This routine manages SPARK regions. Return statements must be
534 -- replaced by gotos which jump to the end of the routine and restore the
537 procedure Analyze_Entry_Or_Subprogram_Contract
538 (Subp_Id
: Entity_Id
;
539 Freeze_Id
: Entity_Id
:= Empty
)
541 Items
: constant Node_Id
:= Contract
(Subp_Id
);
542 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
544 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
545 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
546 -- Save the SPARK_Mode-related data to restore on exit
548 Skip_Assert_Exprs
: constant Boolean :=
549 Ekind_In
(Subp_Id
, E_Entry
, E_Entry_Family
)
550 and then not ASIS_Mode
551 and then not GNATprove_Mode
;
553 Depends
: Node_Id
:= Empty
;
554 Global
: Node_Id
:= Empty
;
559 -- Do not analyze a contract multiple times
561 if Present
(Items
) then
562 if Analyzed
(Items
) then
565 Set_Analyzed
(Items
);
569 -- Due to the timing of contract analysis, delayed pragmas may be
570 -- subject to the wrong SPARK_Mode, usually that of the enclosing
571 -- context. To remedy this, restore the original SPARK_Mode of the
572 -- related subprogram body.
574 Set_SPARK_Mode
(Subp_Id
);
576 -- All subprograms carry a contract, but for some it is not significant
577 -- and should not be processed.
579 if not Has_Significant_Contract
(Subp_Id
) then
582 elsif Present
(Items
) then
584 -- Do not analyze the pre/postconditions of an entry declaration
585 -- unless annotating the original tree for ASIS or GNATprove. The
586 -- real analysis occurs when the pre/postconditons are relocated to
587 -- the contract wrapper procedure (see Build_Contract_Wrapper).
589 if Skip_Assert_Exprs
then
592 -- Otherwise analyze the pre/postconditions
595 Prag
:= Pre_Post_Conditions
(Items
);
596 while Present
(Prag
) loop
597 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
598 Prag
:= Next_Pragma
(Prag
);
602 -- Analyze contract-cases and test-cases
604 Prag
:= Contract_Test_Cases
(Items
);
605 while Present
(Prag
) loop
606 Prag_Nam
:= Pragma_Name
(Prag
);
608 if Prag_Nam
= Name_Contract_Cases
then
610 -- Do not analyze the contract cases of an entry declaration
611 -- unless annotating the original tree for ASIS or GNATprove.
612 -- The real analysis occurs when the contract cases are moved
613 -- to the contract wrapper procedure (Build_Contract_Wrapper).
615 if Skip_Assert_Exprs
then
618 -- Otherwise analyze the contract cases
621 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
624 pragma Assert
(Prag_Nam
= Name_Test_Case
);
625 Analyze_Test_Case_In_Decl_Part
(Prag
);
628 Prag
:= Next_Pragma
(Prag
);
631 -- Analyze classification pragmas
633 Prag
:= Classifications
(Items
);
634 while Present
(Prag
) loop
635 Prag_Nam
:= Pragma_Name
(Prag
);
637 if Prag_Nam
= Name_Depends
then
640 elsif Prag_Nam
= Name_Global
then
644 Prag
:= Next_Pragma
(Prag
);
647 -- Analyze Global first, as Depends may mention items classified in
648 -- the global categorization.
650 if Present
(Global
) then
651 Analyze_Global_In_Decl_Part
(Global
);
654 -- Depends must be analyzed after Global in order to see the modes of
657 if Present
(Depends
) then
658 Analyze_Depends_In_Decl_Part
(Depends
);
661 -- Ensure that the contract cases or postconditions mention 'Result
662 -- or define a post-state.
664 Check_Result_And_Post_State
(Subp_Id
);
667 -- A nonvolatile function cannot have an effectively volatile formal
668 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
669 -- only when SPARK_Mode is on, as it is not a standard legality rule.
670 -- The check is performed here because pragma Volatile_Function is
671 -- processed after the analysis of the related subprogram declaration.
674 and then Ekind_In
(Subp_Id
, E_Function
, E_Generic_Function
)
675 and then Comes_From_Source
(Subp_Id
)
676 and then not Is_Volatile_Function
(Subp_Id
)
678 Check_Nonvolatile_Function_Profile
(Subp_Id
);
681 -- Restore the SPARK_Mode of the enclosing context after all delayed
682 -- pragmas have been analyzed.
684 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
686 -- Capture all global references in a generic subprogram now that the
687 -- contract has been analyzed.
689 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
690 Save_Global_References_In_Contract
691 (Templ
=> Original_Node
(Subp_Decl
),
694 end Analyze_Entry_Or_Subprogram_Contract
;
696 -----------------------------
697 -- Analyze_Object_Contract --
698 -----------------------------
700 -- WARNING: This routine manages SPARK regions. Return statements must be
701 -- replaced by gotos which jump to the end of the routine and restore the
704 procedure Analyze_Object_Contract
706 Freeze_Id
: Entity_Id
:= Empty
)
708 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
710 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
711 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
712 -- Save the SPARK_Mode-related data to restore on exit
714 AR_Val
: Boolean := False;
715 AW_Val
: Boolean := False;
716 ER_Val
: Boolean := False;
717 EW_Val
: Boolean := False;
721 Seen
: Boolean := False;
724 -- The loop parameter in an element iterator over a formal container
725 -- is declared with an object declaration, but no contracts apply.
727 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
731 -- Do not analyze a contract multiple times
733 Items
:= Contract
(Obj_Id
);
735 if Present
(Items
) then
736 if Analyzed
(Items
) then
739 Set_Analyzed
(Items
);
743 -- The anonymous object created for a single concurrent type inherits
744 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
745 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
746 -- of the enclosing context. To remedy this, restore the original mode
747 -- of the related anonymous object.
749 if Is_Single_Concurrent_Object
(Obj_Id
)
750 and then Present
(SPARK_Pragma
(Obj_Id
))
752 Set_SPARK_Mode
(Obj_Id
);
755 -- Constant-related checks
757 if Ekind
(Obj_Id
) = E_Constant
then
759 -- Analyze indicator Part_Of
761 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
763 -- Check whether the lack of indicator Part_Of agrees with the
764 -- placement of the constant with respect to the state space.
767 Check_Missing_Part_Of
(Obj_Id
);
770 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
771 -- This check is relevant only when SPARK_Mode is on, as it is not
772 -- a standard Ada legality rule. Internally-generated constants that
773 -- map generic formals to actuals in instantiations are allowed to
777 and then Comes_From_Source
(Obj_Id
)
778 and then Is_Effectively_Volatile
(Obj_Id
)
779 and then No
(Corresponding_Generic_Association
(Parent
(Obj_Id
)))
781 Error_Msg_N
("constant cannot be volatile", Obj_Id
);
784 -- Variable-related checks
786 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
788 -- Analyze all external properties
790 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Readers
);
792 if Present
(Prag
) then
793 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
797 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Writers
);
799 if Present
(Prag
) then
800 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
804 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Reads
);
806 if Present
(Prag
) then
807 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
811 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Writes
);
813 if Present
(Prag
) then
814 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
818 -- Verify the mutual interaction of the various external properties
821 Check_External_Properties
(Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
824 -- The anonymous object created for a single concurrent type carries
825 -- pragmas Depends and Globat of the type.
827 if Is_Single_Concurrent_Object
(Obj_Id
) then
829 -- Analyze Global first, as Depends may mention items classified
830 -- in the global categorization.
832 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
834 if Present
(Prag
) then
835 Analyze_Global_In_Decl_Part
(Prag
);
838 -- Depends must be analyzed after Global in order to see the modes
839 -- of all global items.
841 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
843 if Present
(Prag
) then
844 Analyze_Depends_In_Decl_Part
(Prag
);
848 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
850 -- Analyze indicator Part_Of
852 if Present
(Prag
) then
853 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
855 -- The variable is a constituent of a single protected/task type
856 -- and behaves as a component of the type. Verify that references
857 -- to the variable occur within the definition or body of the type
860 if Present
(Encapsulating_State
(Obj_Id
))
861 and then Is_Single_Concurrent_Object
862 (Encapsulating_State
(Obj_Id
))
863 and then Present
(Part_Of_References
(Obj_Id
))
865 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
866 while Present
(Ref_Elmt
) loop
867 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
868 Next_Elmt
(Ref_Elmt
);
872 -- Otherwise check whether the lack of indicator Part_Of agrees with
873 -- the placement of the variable with respect to the state space.
876 Check_Missing_Part_Of
(Obj_Id
);
879 -- The following checks are relevant only when SPARK_Mode is on, as
880 -- they are not standard Ada legality rules. Internally generated
881 -- temporaries are ignored.
883 if SPARK_Mode
= On
and then Comes_From_Source
(Obj_Id
) then
884 if Is_Effectively_Volatile
(Obj_Id
) then
886 -- The declaration of an effectively volatile object must
887 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
889 if not Is_Library_Level_Entity
(Obj_Id
) then
891 ("volatile variable & must be declared at library level "
892 & "(SPARK RM 7.1.3(3))", Obj_Id
);
894 -- An object of a discriminated type cannot be effectively
895 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
897 elsif Has_Discriminants
(Obj_Typ
)
898 and then not Is_Protected_Type
(Obj_Typ
)
901 ("discriminated object & cannot be volatile", Obj_Id
);
904 -- The object is not effectively volatile
907 -- A non-effectively volatile object cannot have effectively
908 -- volatile components (SPARK RM 7.1.3(6)).
910 if not Is_Effectively_Volatile
(Obj_Id
)
911 and then Has_Volatile_Component
(Obj_Typ
)
914 ("non-volatile object & cannot have volatile components",
923 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
925 -- A Ghost object cannot be of a type that yields a synchronized
926 -- object (SPARK RM 6.9(19)).
928 if Yields_Synchronized_Object
(Obj_Typ
) then
929 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
931 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
932 -- SPARK RM 6.9(19)).
934 elsif Is_Effectively_Volatile
(Obj_Id
) then
935 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
937 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
938 -- One exception to this is the object that represents the dispatch
939 -- table of a Ghost tagged type, as the symbol needs to be exported.
941 elsif Is_Exported
(Obj_Id
) then
942 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
944 elsif Is_Imported
(Obj_Id
) then
945 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
949 -- Restore the SPARK_Mode of the enclosing context after all delayed
950 -- pragmas have been analyzed.
952 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
953 end Analyze_Object_Contract
;
955 -----------------------------------
956 -- Analyze_Package_Body_Contract --
957 -----------------------------------
959 -- WARNING: This routine manages SPARK regions. Return statements must be
960 -- replaced by gotos which jump to the end of the routine and restore the
963 procedure Analyze_Package_Body_Contract
964 (Body_Id
: Entity_Id
;
965 Freeze_Id
: Entity_Id
:= Empty
)
967 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
968 Items
: constant Node_Id
:= Contract
(Body_Id
);
969 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
971 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
972 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
973 -- Save the SPARK_Mode-related data to restore on exit
978 -- Do not analyze a contract multiple times
980 if Present
(Items
) then
981 if Analyzed
(Items
) then
984 Set_Analyzed
(Items
);
988 -- Due to the timing of contract analysis, delayed pragmas may be
989 -- subject to the wrong SPARK_Mode, usually that of the enclosing
990 -- context. To remedy this, restore the original SPARK_Mode of the
991 -- related package body.
993 Set_SPARK_Mode
(Body_Id
);
995 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
997 -- The analysis of pragma Refined_State detects whether the spec has
998 -- abstract states available for refinement.
1000 if Present
(Ref_State
) then
1001 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
1004 -- Restore the SPARK_Mode of the enclosing context after all delayed
1005 -- pragmas have been analyzed.
1007 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1009 -- Capture all global references in a generic package body now that the
1010 -- contract has been analyzed.
1012 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1013 Save_Global_References_In_Contract
1014 (Templ
=> Original_Node
(Body_Decl
),
1017 end Analyze_Package_Body_Contract
;
1019 ------------------------------
1020 -- Analyze_Package_Contract --
1021 ------------------------------
1023 -- WARNING: This routine manages SPARK regions. Return statements must be
1024 -- replaced by gotos which jump to the end of the routine and restore the
1027 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1028 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1029 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1031 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1032 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1033 -- Save the SPARK_Mode-related data to restore on exit
1035 Init
: Node_Id
:= Empty
;
1036 Init_Cond
: Node_Id
:= Empty
;
1041 -- Do not analyze a contract multiple times
1043 if Present
(Items
) then
1044 if Analyzed
(Items
) then
1047 Set_Analyzed
(Items
);
1051 -- Due to the timing of contract analysis, delayed pragmas may be
1052 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1053 -- context. To remedy this, restore the original SPARK_Mode of the
1056 Set_SPARK_Mode
(Pack_Id
);
1058 if Present
(Items
) then
1060 -- Locate and store pragmas Initial_Condition and Initializes, since
1061 -- their order of analysis matters.
1063 Prag
:= Classifications
(Items
);
1064 while Present
(Prag
) loop
1065 Prag_Nam
:= Pragma_Name
(Prag
);
1067 if Prag_Nam
= Name_Initial_Condition
then
1070 elsif Prag_Nam
= Name_Initializes
then
1074 Prag
:= Next_Pragma
(Prag
);
1077 -- Analyze the initialization-related pragmas. Initializes must come
1078 -- before Initial_Condition due to item dependencies.
1080 if Present
(Init
) then
1081 Analyze_Initializes_In_Decl_Part
(Init
);
1084 if Present
(Init_Cond
) then
1085 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1089 -- Restore the SPARK_Mode of the enclosing context after all delayed
1090 -- pragmas have been analyzed.
1092 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1094 -- Capture all global references in a generic package now that the
1095 -- contract has been analyzed.
1097 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1098 Save_Global_References_In_Contract
1099 (Templ
=> Original_Node
(Pack_Decl
),
1102 end Analyze_Package_Contract
;
1104 --------------------------------------------
1105 -- Analyze_Package_Instantiation_Contract --
1106 --------------------------------------------
1108 -- WARNING: This routine manages SPARK regions. Return statements must be
1109 -- replaced by gotos which jump to the end of the routine and restore the
1112 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
) is
1113 Inst_Spec
: constant Node_Id
:=
1114 Instance_Spec
(Unit_Declaration_Node
(Inst_Id
));
1116 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1117 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1118 -- Save the SPARK_Mode-related data to restore on exit
1120 Pack_Id
: Entity_Id
;
1124 -- Nothing to do when the package instantiation is erroneous or left
1125 -- partially decorated.
1127 if No
(Inst_Spec
) then
1131 Pack_Id
:= Defining_Entity
(Inst_Spec
);
1132 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1134 -- Due to the timing of contract analysis, delayed pragmas may be
1135 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1136 -- context. To remedy this, restore the original SPARK_Mode of the
1139 Set_SPARK_Mode
(Pack_Id
);
1141 -- Check whether the lack of indicator Part_Of agrees with the placement
1142 -- of the package instantiation with respect to the state space. Nested
1143 -- package instantiations do not need to be checked because they inherit
1144 -- Part_Of indicator of the outermost package instantiation (see routine
1145 -- Propagate_Part_Of in Sem_Prag).
1150 elsif No
(Prag
) then
1151 Check_Missing_Part_Of
(Pack_Id
);
1154 -- Restore the SPARK_Mode of the enclosing context after all delayed
1155 -- pragmas have been analyzed.
1157 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1158 end Analyze_Package_Instantiation_Contract
;
1160 --------------------------------
1161 -- Analyze_Protected_Contract --
1162 --------------------------------
1164 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1165 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1168 -- Do not analyze a contract multiple times
1170 if Present
(Items
) then
1171 if Analyzed
(Items
) then
1174 Set_Analyzed
(Items
);
1177 end Analyze_Protected_Contract
;
1179 -------------------------------------------
1180 -- Analyze_Subprogram_Body_Stub_Contract --
1181 -------------------------------------------
1183 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1184 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1185 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1188 -- A subprogram body stub may act as its own spec or as the completion
1189 -- of a previous declaration. Depending on the context, the contract of
1190 -- the stub may contain two sets of pragmas.
1192 -- The stub is a completion, the applicable pragmas are:
1196 if Present
(Spec_Id
) then
1197 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1199 -- The stub acts as its own spec, the applicable pragmas are:
1208 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1210 end Analyze_Subprogram_Body_Stub_Contract
;
1212 ---------------------------
1213 -- Analyze_Task_Contract --
1214 ---------------------------
1216 -- WARNING: This routine manages SPARK regions. Return statements must be
1217 -- replaced by gotos which jump to the end of the routine and restore the
1220 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1221 Items
: constant Node_Id
:= Contract
(Task_Id
);
1223 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1224 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1225 -- Save the SPARK_Mode-related data to restore on exit
1230 -- Do not analyze a contract multiple times
1232 if Present
(Items
) then
1233 if Analyzed
(Items
) then
1236 Set_Analyzed
(Items
);
1240 -- Due to the timing of contract analysis, delayed pragmas may be
1241 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1242 -- context. To remedy this, restore the original SPARK_Mode of the
1243 -- related task unit.
1245 Set_SPARK_Mode
(Task_Id
);
1247 -- Analyze Global first, as Depends may mention items classified in the
1248 -- global categorization.
1250 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1252 if Present
(Prag
) then
1253 Analyze_Global_In_Decl_Part
(Prag
);
1256 -- Depends must be analyzed after Global in order to see the modes of
1257 -- all global items.
1259 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1261 if Present
(Prag
) then
1262 Analyze_Depends_In_Decl_Part
(Prag
);
1265 -- Restore the SPARK_Mode of the enclosing context after all delayed
1266 -- pragmas have been analyzed.
1268 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1269 end Analyze_Task_Contract
;
1271 -------------------------------------------------
1272 -- Build_And_Analyze_Contract_Only_Subprograms --
1273 -------------------------------------------------
1275 procedure Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
) is
1276 procedure Analyze_Contract_Only_Subprograms
;
1277 -- Analyze the contract-only subprograms of L
1279 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
);
1280 -- Append the contract-only bodies of Subp_List to its declarations list
1282 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
;
1283 -- If E is an entity for a non-imported subprogram specification with
1284 -- pre/postconditions and we are compiling with CodePeer mode, then
1285 -- this procedure will create a wrapper to help Gnat2scil process its
1286 -- contracts. Return Empty if the wrapper cannot be built.
1288 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
;
1289 -- Build the contract-only subprograms of all eligible subprograms found
1292 function Has_Private_Declarations
(N
: Node_Id
) return Boolean;
1293 -- Return True for package specs, task definitions, and protected type
1294 -- definitions whose list of private declarations is not empty.
1296 ---------------------------------------
1297 -- Analyze_Contract_Only_Subprograms --
1298 ---------------------------------------
1300 procedure Analyze_Contract_Only_Subprograms
is
1301 procedure Analyze_Contract_Only_Bodies
;
1302 -- Analyze all the contract-only bodies of L
1304 ----------------------------------
1305 -- Analyze_Contract_Only_Bodies --
1306 ----------------------------------
1308 procedure Analyze_Contract_Only_Bodies
is
1313 while Present
(Decl
) loop
1314 if Nkind
(Decl
) = N_Subprogram_Body
1315 and then Is_Contract_Only_Body
1316 (Defining_Unit_Name
(Specification
(Decl
)))
1323 end Analyze_Contract_Only_Bodies
;
1325 -- Start of processing for Analyze_Contract_Only_Subprograms
1328 if Ekind
(Current_Scope
) /= E_Package
then
1329 Analyze_Contract_Only_Bodies
;
1333 Pkg_Spec
: constant Node_Id
:=
1334 Package_Specification
(Current_Scope
);
1337 if not Has_Private_Declarations
(Pkg_Spec
) then
1338 Analyze_Contract_Only_Bodies
;
1340 -- For packages with private declarations, the contract-only
1341 -- bodies of subprograms defined in the visible part of the
1342 -- package are added to its private declarations (to ensure
1343 -- that they do not cause premature freezing of types and also
1344 -- that they are analyzed with proper visibility). Hence they
1345 -- will be analyzed later.
1347 elsif Visible_Declarations
(Pkg_Spec
) = L
then
1350 elsif Private_Declarations
(Pkg_Spec
) = L
then
1351 Analyze_Contract_Only_Bodies
;
1355 end Analyze_Contract_Only_Subprograms
;
1357 --------------------------------------
1358 -- Append_Contract_Only_Subprograms --
1359 --------------------------------------
1361 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
) is
1363 if No
(Subp_List
) then
1367 if Ekind
(Current_Scope
) /= E_Package
then
1368 Append_List
(Subp_List
, To
=> L
);
1372 Pkg_Spec
: constant Node_Id
:=
1373 Package_Specification
(Current_Scope
);
1376 if not Has_Private_Declarations
(Pkg_Spec
) then
1377 Append_List
(Subp_List
, To
=> L
);
1379 -- If the package has private declarations then append them to
1380 -- its private declarations; they will be analyzed when the
1381 -- contracts of its private declarations are analyzed.
1386 To
=> Private_Declarations
(Pkg_Spec
));
1390 end Append_Contract_Only_Subprograms
;
1392 ------------------------------------
1393 -- Build_Contract_Only_Subprogram --
1394 ------------------------------------
1396 -- This procedure takes care of building a wrapper to generate better
1397 -- analysis results in the case of a call to a subprogram whose body
1398 -- is unavailable to CodePeer but whose specification includes Pre/Post
1399 -- conditions. The body might be unavailable for any of a number or
1400 -- reasons (it is imported, the .adb file is simply missing, or the
1401 -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
1402 -- pragma). The built subprogram has the following contents:
1403 -- * check preconditions
1404 -- * call the subprogram
1405 -- * check postconditions
1407 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
is
1408 Loc
: constant Source_Ptr
:= Sloc
(E
);
1410 Missing_Body_Name
: constant Name_Id
:=
1411 New_External_Name
(Chars
(E
), "__missing_body");
1413 function Build_Missing_Body_Decls
return List_Id
;
1414 -- Build the declaration of the missing body subprogram and its
1415 -- corresponding pragma Import.
1417 function Build_Missing_Body_Subprogram_Call
return Node_Id
;
1418 -- Build the call to the missing body subprogram
1420 function Skip_Contract_Only_Subprogram
(E
: Entity_Id
) return Boolean;
1421 -- Return True for cases where the wrapper is not needed or we cannot
1424 ------------------------------
1425 -- Build_Missing_Body_Decls --
1426 ------------------------------
1428 function Build_Missing_Body_Decls
return List_Id
is
1429 Spec
: constant Node_Id
:= Declaration_Node
(E
);
1435 Make_Subprogram_Declaration
(Loc
, Copy_Subprogram_Spec
(Spec
));
1436 Set_Chars
(Defining_Entity
(Decl
), Missing_Body_Name
);
1440 Chars
=> Name_Import
,
1441 Pragma_Argument_Associations
=> New_List
(
1442 Make_Pragma_Argument_Association
(Loc
,
1443 Expression
=> Make_Identifier
(Loc
, Name_Ada
)),
1445 Make_Pragma_Argument_Association
(Loc
,
1446 Expression
=> Make_Identifier
(Loc
, Missing_Body_Name
))));
1448 return New_List
(Decl
, Prag
);
1449 end Build_Missing_Body_Decls
;
1451 ----------------------------------------
1452 -- Build_Missing_Body_Subprogram_Call --
1453 ----------------------------------------
1455 function Build_Missing_Body_Subprogram_Call
return Node_Id
is
1462 -- Build parameter list that we need
1464 Forml
:= First_Formal
(E
);
1465 while Present
(Forml
) loop
1466 Append_To
(Parms
, Make_Identifier
(Loc
, Chars
(Forml
)));
1467 Next_Formal
(Forml
);
1470 -- Build the call to the missing body subprogram
1472 if Ekind_In
(E
, E_Function
, E_Generic_Function
) then
1474 Make_Simple_Return_Statement
(Loc
,
1476 Make_Function_Call
(Loc
,
1478 Make_Identifier
(Loc
, Missing_Body_Name
),
1479 Parameter_Associations
=> Parms
));
1483 Make_Procedure_Call_Statement
(Loc
,
1485 Make_Identifier
(Loc
, Missing_Body_Name
),
1486 Parameter_Associations
=> Parms
);
1488 end Build_Missing_Body_Subprogram_Call
;
1490 -----------------------------------
1491 -- Skip_Contract_Only_Subprogram --
1492 -----------------------------------
1494 function Skip_Contract_Only_Subprogram
1495 (E
: Entity_Id
) return Boolean
1497 function Depends_On_Enclosing_Private_Type
return Boolean;
1498 -- Return True if some formal of E (or its return type) are
1499 -- private types defined in an enclosing package.
1501 function Some_Enclosing_Package_Has_Private_Decls
return Boolean;
1502 -- Return True if some enclosing package of the current scope has
1503 -- private declarations.
1505 ---------------------------------------
1506 -- Depends_On_Enclosing_Private_Type --
1507 ---------------------------------------
1509 function Depends_On_Enclosing_Private_Type
return Boolean is
1510 function Defined_In_Enclosing_Package
1511 (Typ
: Entity_Id
) return Boolean;
1512 -- Return True if Typ is an entity defined in an enclosing
1513 -- package of the current scope.
1515 ----------------------------------
1516 -- Defined_In_Enclosing_Package --
1517 ----------------------------------
1519 function Defined_In_Enclosing_Package
1520 (Typ
: Entity_Id
) return Boolean
1522 Scop
: Entity_Id
:= Scope
(Current_Scope
);
1525 while Scop
/= Scope
(Typ
)
1526 and then not Is_Compilation_Unit
(Scop
)
1528 Scop
:= Scope
(Scop
);
1531 return Scop
= Scope
(Typ
);
1532 end Defined_In_Enclosing_Package
;
1536 Param_E
: Entity_Id
;
1539 -- Start of processing for Depends_On_Enclosing_Private_Type
1542 Param_E
:= First_Entity
(E
);
1543 while Present
(Param_E
) loop
1544 Typ
:= Etype
(Param_E
);
1546 if Is_Private_Type
(Typ
)
1547 and then Defined_In_Enclosing_Package
(Typ
)
1552 Next_Entity
(Param_E
);
1556 Ekind
(E
) = E_Function
1557 and then Is_Private_Type
(Etype
(E
))
1558 and then Defined_In_Enclosing_Package
(Etype
(E
));
1559 end Depends_On_Enclosing_Private_Type
;
1561 ----------------------------------------------
1562 -- Some_Enclosing_Package_Has_Private_Decls --
1563 ----------------------------------------------
1565 function Some_Enclosing_Package_Has_Private_Decls
return Boolean is
1566 Scop
: Entity_Id
:= Current_Scope
;
1567 Pkg_Spec
: Node_Id
:= Package_Specification
(Scop
);
1571 if Ekind
(Scop
) = E_Package
1572 and then Has_Private_Declarations
1573 (Package_Specification
(Scop
))
1575 Pkg_Spec
:= Package_Specification
(Scop
);
1578 exit when Is_Compilation_Unit
(Scop
);
1579 Scop
:= Scope
(Scop
);
1582 return Pkg_Spec
/= Package_Specification
(Current_Scope
);
1583 end Some_Enclosing_Package_Has_Private_Decls
;
1585 -- Start of processing for Skip_Contract_Only_Subprogram
1588 if not CodePeer_Mode
1589 or else Inside_A_Generic
1590 or else not Is_Subprogram
(E
)
1591 or else Is_Abstract_Subprogram
(E
)
1592 or else Is_Imported
(E
)
1593 or else No
(Contract
(E
))
1594 or else No
(Pre_Post_Conditions
(Contract
(E
)))
1595 or else Is_Contract_Only_Body
(E
)
1596 or else Convention
(E
) = Convention_Protected
1600 -- We do not support building the contract-only subprogram if E
1601 -- is a subprogram declared in a nested package that has some
1602 -- formal or return type depending on a private type defined in
1603 -- an enclosing package.
1605 elsif Ekind
(Current_Scope
) = E_Package
1606 and then Some_Enclosing_Package_Has_Private_Decls
1607 and then Depends_On_Enclosing_Private_Type
1609 if Debug_Flag_Dot_KK
then
1611 Saved_Mode
: constant Warning_Mode_Type
:= Warning_Mode
;
1614 -- Warnings are disabled by default under CodePeer_Mode
1615 -- (see switch-c). Enable them temporarily.
1617 Warning_Mode
:= Normal
;
1619 ("cannot generate contract-only subprogram?", E
);
1620 Warning_Mode
:= Saved_Mode
;
1628 end Skip_Contract_Only_Subprogram
;
1630 -- Start of processing for Build_Contract_Only_Subprogram
1633 -- Test cases where the wrapper is not needed and cases where we
1636 if Skip_Contract_Only_Subprogram
(E
) then
1640 -- Note on calls to Copy_Separate_Tree. The trees we are copying
1641 -- here are fully analyzed, but we definitely want fully syntactic
1642 -- unanalyzed trees in the body we construct, so that the analysis
1643 -- generates the right visibility, and that is exactly what the
1644 -- calls to Copy_Separate_Tree give us.
1647 Name
: constant Name_Id
:=
1648 New_External_Name
(Chars
(E
), "__contract_only");
1654 Make_Subprogram_Body
(Loc
,
1656 Copy_Subprogram_Spec
(Declaration_Node
(E
)),
1658 Build_Missing_Body_Decls
,
1659 Handled_Statement_Sequence
=>
1660 Make_Handled_Sequence_Of_Statements
(Loc
,
1661 Statements
=> New_List
(
1662 Build_Missing_Body_Subprogram_Call
),
1663 End_Label
=> Make_Identifier
(Loc
, Name
)));
1665 Id
:= Defining_Unit_Name
(Specification
(Bod
));
1667 -- Copy only the pre/postconditions of the original contract
1668 -- since it is what we need, but also because pragmas stored in
1669 -- the other fields have N_Pragmas with N_Aspect_Specifications
1670 -- that reference their associated pragma (thus causing an endless
1671 -- loop when trying to copy the subtree).
1674 New_Contract
: constant Node_Id
:= Make_Contract
(Sloc
(E
));
1677 Set_Pre_Post_Conditions
(New_Contract
,
1678 Copy_Separate_Tree
(Pre_Post_Conditions
(Contract
(E
))));
1679 Set_Contract
(Id
, New_Contract
);
1682 -- Fix the name of this new subprogram and link the original
1683 -- subprogram with its Contract_Only_Body subprogram.
1685 Set_Chars
(Id
, Name
);
1686 Set_Is_Contract_Only_Body
(Id
);
1687 Set_Contract_Only_Body
(E
, Id
);
1691 end Build_Contract_Only_Subprogram
;
1693 -------------------------------------
1694 -- Build_Contract_Only_Subprograms --
1695 -------------------------------------
1697 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
is
1700 Result
: List_Id
:= No_List
;
1701 Subp_Id
: Entity_Id
;
1705 while Present
(Decl
) loop
1706 if Nkind
(Decl
) = N_Subprogram_Declaration
then
1707 Subp_Id
:= Defining_Unit_Name
(Specification
(Decl
));
1708 New_Subp
:= Build_Contract_Only_Subprogram
(Subp_Id
);
1710 if Present
(New_Subp
) then
1715 Append_To
(Result
, New_Subp
);
1723 end Build_Contract_Only_Subprograms
;
1725 ------------------------------
1726 -- Has_Private_Declarations --
1727 ------------------------------
1729 function Has_Private_Declarations
(N
: Node_Id
) return Boolean is
1731 if not Nkind_In
(N
, N_Package_Specification
,
1732 N_Protected_Definition
,
1738 Present
(Private_Declarations
(N
))
1739 and then Is_Non_Empty_List
(Private_Declarations
(N
));
1741 end Has_Private_Declarations
;
1745 Subp_List
: List_Id
;
1747 -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
1750 Subp_List
:= Build_Contract_Only_Subprograms
(L
);
1751 Append_Contract_Only_Subprograms
(Subp_List
);
1752 Analyze_Contract_Only_Subprograms
;
1753 end Build_And_Analyze_Contract_Only_Subprograms
;
1755 -----------------------------
1756 -- Create_Generic_Contract --
1757 -----------------------------
1759 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
1760 Templ
: constant Node_Id
:= Original_Node
(Unit
);
1761 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
1763 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
1764 -- Add a single contract-related source pragma Prag to the contract of
1765 -- generic template Templ_Id.
1767 ---------------------------------
1768 -- Add_Generic_Contract_Pragma --
1769 ---------------------------------
1771 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
1772 Prag_Templ
: Node_Id
;
1775 -- Mark the pragma to prevent the premature capture of global
1776 -- references when capturing global references of the context
1777 -- (see Save_References_In_Pragma).
1779 Set_Is_Generic_Contract_Pragma
(Prag
);
1781 -- Pragmas that apply to a generic subprogram declaration are not
1782 -- part of the semantic structure of the generic template:
1785 -- procedure Example (Formal : Integer);
1786 -- pragma Precondition (Formal > 0);
1788 -- Create a generic template for such pragmas and link the template
1789 -- of the pragma with the generic template.
1791 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1793 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
1794 Prag_Templ
:= Original_Node
(Prag
);
1796 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
1797 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
1799 -- Otherwise link the pragma with the generic template
1802 Add_Contract_Item
(Prag
, Templ_Id
);
1804 end Add_Generic_Contract_Pragma
;
1808 Context
: constant Node_Id
:= Parent
(Unit
);
1809 Decl
: Node_Id
:= Empty
;
1811 -- Start of processing for Create_Generic_Contract
1814 -- A generic package declaration carries contract-related source pragmas
1815 -- in its visible declarations.
1817 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
1818 Set_Ekind
(Templ_Id
, E_Generic_Package
);
1820 if Present
(Visible_Declarations
(Specification
(Templ
))) then
1821 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
1824 -- A generic package body carries contract-related source pragmas in its
1827 elsif Nkind
(Templ
) = N_Package_Body
then
1828 Set_Ekind
(Templ_Id
, E_Package_Body
);
1830 if Present
(Declarations
(Templ
)) then
1831 Decl
:= First
(Declarations
(Templ
));
1834 -- Generic subprogram declaration
1836 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1837 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
1838 Set_Ekind
(Templ_Id
, E_Generic_Function
);
1840 Set_Ekind
(Templ_Id
, E_Generic_Procedure
);
1843 -- When the generic subprogram acts as a compilation unit, inspect
1844 -- the Pragmas_After list for contract-related source pragmas.
1846 if Nkind
(Context
) = N_Compilation_Unit
then
1847 if Present
(Aux_Decls_Node
(Context
))
1848 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
1850 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
1853 -- Otherwise inspect the successive declarations for contract-related
1857 Decl
:= Next
(Unit
);
1860 -- A generic subprogram body carries contract-related source pragmas in
1861 -- its declarations.
1863 elsif Nkind
(Templ
) = N_Subprogram_Body
then
1864 Set_Ekind
(Templ_Id
, E_Subprogram_Body
);
1866 if Present
(Declarations
(Templ
)) then
1867 Decl
:= First
(Declarations
(Templ
));
1871 -- Inspect the relevant declarations looking for contract-related source
1872 -- pragmas and add them to the contract of the generic unit.
1874 while Present
(Decl
) loop
1875 if Comes_From_Source
(Decl
) then
1876 if Nkind
(Decl
) = N_Pragma
then
1878 -- The source pragma is a contract annotation
1880 if Is_Contract_Annotation
(Decl
) then
1881 Add_Generic_Contract_Pragma
(Decl
);
1884 -- The region where a contract-related source pragma may appear
1885 -- ends with the first source non-pragma declaration or statement.
1894 end Create_Generic_Contract
;
1896 --------------------------------
1897 -- Expand_Subprogram_Contract --
1898 --------------------------------
1900 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
1901 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1902 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1904 procedure Add_Invariant_And_Predicate_Checks
1905 (Subp_Id
: Entity_Id
;
1906 Stmts
: in out List_Id
;
1907 Result
: out Node_Id
);
1908 -- Process the result of function Subp_Id (if applicable) and all its
1909 -- formals. Add invariant and predicate checks where applicable. The
1910 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1911 -- function, Result contains the entity of parameter _Result, to be
1912 -- used in the creation of procedure _Postconditions.
1914 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
1915 -- Append a node to a list. If there is no list, create a new one. When
1916 -- the item denotes a pragma, it is added to the list only when it is
1919 procedure Build_Postconditions_Procedure
1920 (Subp_Id
: Entity_Id
;
1922 Result
: Entity_Id
);
1923 -- Create the body of procedure _Postconditions which handles various
1924 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1925 -- of statements to be checked on exit. Parameter Result is the entity
1926 -- of parameter _Result when Subp_Id denotes a function.
1928 procedure Process_Contract_Cases
(Stmts
: in out List_Id
);
1929 -- Process pragma Contract_Cases. This routine prepends items to the
1930 -- body declarations and appends items to list Stmts.
1932 procedure Process_Postconditions
(Stmts
: in out List_Id
);
1933 -- Collect all [inherited] spec and body postconditions and accumulate
1934 -- their pragma Check equivalents in list Stmts.
1936 procedure Process_Preconditions
;
1937 -- Collect all [inherited] spec and body preconditions and prepend their
1938 -- pragma Check equivalents to the declarations of the body.
1940 ----------------------------------------
1941 -- Add_Invariant_And_Predicate_Checks --
1942 ----------------------------------------
1944 procedure Add_Invariant_And_Predicate_Checks
1945 (Subp_Id
: Entity_Id
;
1946 Stmts
: in out List_Id
;
1947 Result
: out Node_Id
)
1949 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
1950 -- Id denotes the return value of a function or a formal parameter.
1951 -- Add an invariant check if the type of Id is access to a type with
1952 -- invariants. The routine appends the generated code to Stmts.
1954 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
1955 -- Determine whether type Typ can benefit from invariant checks. To
1956 -- qualify, the type must have a non-null invariant procedure and
1957 -- subprogram Subp_Id must appear visible from the point of view of
1960 ---------------------------------
1961 -- Add_Invariant_Access_Checks --
1962 ---------------------------------
1964 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
1965 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
1972 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
1973 Typ
:= Designated_Type
(Typ
);
1975 if Invariant_Checks_OK
(Typ
) then
1977 Make_Explicit_Dereference
(Loc
,
1978 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
1979 Set_Etype
(Ref
, Typ
);
1982 -- if <Id> /= null then
1983 -- <invariant_call (<Ref>)>
1988 Make_If_Statement
(Loc
,
1991 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
1992 Right_Opnd
=> Make_Null
(Loc
)),
1993 Then_Statements
=> New_List
(
1994 Make_Invariant_Call
(Ref
))),
1998 end Add_Invariant_Access_Checks
;
2000 -------------------------
2001 -- Invariant_Checks_OK --
2002 -------------------------
2004 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
2005 function Has_Public_Visibility_Of_Subprogram
return Boolean;
2006 -- Determine whether type Typ has public visibility of subprogram
2009 -----------------------------------------
2010 -- Has_Public_Visibility_Of_Subprogram --
2011 -----------------------------------------
2013 function Has_Public_Visibility_Of_Subprogram
return Boolean is
2014 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2017 -- An Initialization procedure must be considered visible even
2018 -- though it is internally generated.
2020 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2023 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2026 -- Internally generated code is never publicly visible except
2027 -- for a subprogram that is the implementation of an expression
2028 -- function. In that case the visibility is determined by the
2031 elsif not Comes_From_Source
(Subp_Decl
)
2033 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2035 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2039 -- Determine whether the subprogram is declared in the visible
2040 -- declarations of the package containing the type, or in the
2041 -- visible declaration of a child unit of that package.
2045 Decls
: constant List_Id
:=
2046 List_Containing
(Subp_Decl
);
2047 Subp_Scope
: constant Entity_Id
:=
2048 Scope
(Defining_Entity
(Subp_Decl
));
2049 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2053 Decls
= Visible_Declarations
2054 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2057 (Ekind
(Subp_Scope
) = E_Package
2058 and then Typ_Scope
/= Subp_Scope
2059 and then Is_Child_Unit
(Subp_Scope
)
2061 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2063 Decls
= Visible_Declarations
2065 (Unit_Declaration_Node
(Subp_Scope
))));
2068 end Has_Public_Visibility_Of_Subprogram
;
2070 -- Start of processing for Invariant_Checks_OK
2074 Has_Invariants
(Typ
)
2075 and then Present
(Invariant_Procedure
(Typ
))
2076 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2077 and then Has_Public_Visibility_Of_Subprogram
;
2078 end Invariant_Checks_OK
;
2082 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2083 -- Source location of subprogram body contract
2088 -- Start of processing for Add_Invariant_And_Predicate_Checks
2093 -- Process the result of a function
2095 if Ekind
(Subp_Id
) = E_Function
then
2096 Typ
:= Etype
(Subp_Id
);
2098 -- Generate _Result which is used in procedure _Postconditions to
2099 -- verify the return value.
2101 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2102 Set_Etype
(Result
, Typ
);
2104 -- Add an invariant check when the return type has invariants and
2105 -- the related function is visible to the outside.
2107 if Invariant_Checks_OK
(Typ
) then
2110 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2114 -- Add an invariant check when the return type is an access to a
2115 -- type with invariants.
2117 Add_Invariant_Access_Checks
(Result
);
2120 -- Add invariant and predicates for all formals that qualify
2122 Formal
:= First_Formal
(Subp_Id
);
2123 while Present
(Formal
) loop
2124 Typ
:= Etype
(Formal
);
2126 if Ekind
(Formal
) /= E_In_Parameter
2127 or else Is_Access_Type
(Typ
)
2129 if Invariant_Checks_OK
(Typ
) then
2132 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2136 Add_Invariant_Access_Checks
(Formal
);
2138 -- Note: we used to add predicate checks for OUT and IN OUT
2139 -- formals here, but that was misguided, since such checks are
2140 -- performed on the caller side, based on the predicate of the
2141 -- actual, rather than the predicate of the formal.
2145 Next_Formal
(Formal
);
2147 end Add_Invariant_And_Predicate_Checks
;
2149 -------------------------
2150 -- Append_Enabled_Item --
2151 -------------------------
2153 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2155 -- Do not chain ignored or disabled pragmas
2157 if Nkind
(Item
) = N_Pragma
2158 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2162 -- Otherwise, add the item
2169 -- If the pragma is a conjunct in a composite postcondition, it
2170 -- has been processed in reverse order. In the postcondition body
2171 -- it must appear before the others.
2173 if Nkind
(Item
) = N_Pragma
2174 and then From_Aspect_Specification
(Item
)
2175 and then Split_PPC
(Item
)
2177 Prepend
(Item
, List
);
2179 Append
(Item
, List
);
2182 end Append_Enabled_Item
;
2184 ------------------------------------
2185 -- Build_Postconditions_Procedure --
2186 ------------------------------------
2188 procedure Build_Postconditions_Procedure
2189 (Subp_Id
: Entity_Id
;
2193 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
);
2194 -- Insert node Stmt before the first source declaration of the
2195 -- related subprogram's body. If no such declaration exists, Stmt
2196 -- becomes the last declaration.
2198 --------------------------------------------
2199 -- Insert_Before_First_Source_Declaration --
2200 --------------------------------------------
2202 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
) is
2203 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2207 -- Inspect the declarations of the related subprogram body looking
2208 -- for the first source declaration.
2210 if Present
(Decls
) then
2211 Decl
:= First
(Decls
);
2212 while Present
(Decl
) loop
2213 if Comes_From_Source
(Decl
) then
2214 Insert_Before
(Decl
, Stmt
);
2221 -- If we get there, then the subprogram body lacks any source
2222 -- declarations. The body of _Postconditions now acts as the
2223 -- last declaration.
2225 Append
(Stmt
, Decls
);
2227 -- Ensure that the body has a declaration list
2230 Set_Declarations
(Body_Decl
, New_List
(Stmt
));
2232 end Insert_Before_First_Source_Declaration
;
2236 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2237 Params
: List_Id
:= No_List
;
2239 Proc_Decl
: Node_Id
;
2240 Proc_Id
: Entity_Id
;
2241 Proc_Spec
: Node_Id
;
2243 -- Start of processing for Build_Postconditions_Procedure
2246 -- Nothing to do if there are no actions to check on exit
2252 Proc_Id
:= Make_Defining_Identifier
(Loc
, Name_uPostconditions
);
2253 Set_Debug_Info_Needed
(Proc_Id
);
2254 Set_Postconditions_Proc
(Subp_Id
, Proc_Id
);
2256 -- Force the front-end inlining of _Postconditions when generating C
2257 -- code, since its body may have references to itypes defined in the
2258 -- enclosing subprogram, which would cause problems for unnesting
2259 -- routines in the absence of inlining.
2261 if Modify_Tree_For_C
then
2262 Set_Has_Pragma_Inline
(Proc_Id
);
2263 Set_Has_Pragma_Inline_Always
(Proc_Id
);
2264 Set_Is_Inlined
(Proc_Id
);
2267 -- The related subprogram is a function: create the specification of
2268 -- parameter _Result.
2270 if Present
(Result
) then
2271 Params
:= New_List
(
2272 Make_Parameter_Specification
(Loc
,
2273 Defining_Identifier
=> Result
,
2275 New_Occurrence_Of
(Etype
(Result
), Loc
)));
2279 Make_Procedure_Specification
(Loc
,
2280 Defining_Unit_Name
=> Proc_Id
,
2281 Parameter_Specifications
=> Params
);
2283 Proc_Decl
:= Make_Subprogram_Declaration
(Loc
, Proc_Spec
);
2285 -- Insert _Postconditions before the first source declaration of the
2286 -- body. This ensures that the body will not cause any premature
2287 -- freezing, as it may mention types:
2289 -- procedure Proc (Obj : Array_Typ) is
2290 -- procedure _postconditions is
2293 -- end _postconditions;
2295 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
2298 -- In the example above, Obj is of type T but the incorrect placement
2299 -- of _Postconditions will cause a crash in gigi due to an out-of-
2300 -- order reference. The body of _Postconditions must be placed after
2301 -- the declaration of Temp to preserve correct visibility.
2303 Insert_Before_First_Source_Declaration
(Proc_Decl
);
2304 Analyze
(Proc_Decl
);
2306 -- Set an explicit End_Label to override the sloc of the implicit
2307 -- RETURN statement, and prevent it from inheriting the sloc of one
2308 -- the postconditions: this would cause confusing debug info to be
2309 -- produced, interfering with coverage-analysis tools.
2312 Make_Subprogram_Body
(Loc
,
2314 Copy_Subprogram_Spec
(Proc_Spec
),
2315 Declarations
=> Empty_List
,
2316 Handled_Statement_Sequence
=>
2317 Make_Handled_Sequence_Of_Statements
(Loc
,
2318 Statements
=> Stmts
,
2319 End_Label
=> Make_Identifier
(Loc
, Chars
(Proc_Id
))));
2321 Insert_After_And_Analyze
(Proc_Decl
, Proc_Bod
);
2322 end Build_Postconditions_Procedure
;
2324 ----------------------------
2325 -- Process_Contract_Cases --
2326 ----------------------------
2328 procedure Process_Contract_Cases
(Stmts
: in out List_Id
) is
2329 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2330 -- Process pragma Contract_Cases for subprogram Subp_Id
2332 --------------------------------
2333 -- Process_Contract_Cases_For --
2334 --------------------------------
2336 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2337 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2341 if Present
(Items
) then
2342 Prag
:= Contract_Test_Cases
(Items
);
2343 while Present
(Prag
) loop
2344 if Pragma_Name
(Prag
) = Name_Contract_Cases
2345 and then Is_Checked
(Prag
)
2347 Expand_Pragma_Contract_Cases
2350 Decls
=> Declarations
(Body_Decl
),
2354 Prag
:= Next_Pragma
(Prag
);
2357 end Process_Contract_Cases_For
;
2359 pragma Unmodified
(Stmts
);
2360 -- Stmts is passed as IN OUT to signal that the list can be updated,
2361 -- even if the corresponding integer value representing the list does
2364 -- Start of processing for Process_Contract_Cases
2367 Process_Contract_Cases_For
(Body_Id
);
2369 if Present
(Spec_Id
) then
2370 Process_Contract_Cases_For
(Spec_Id
);
2372 end Process_Contract_Cases
;
2374 ----------------------------
2375 -- Process_Postconditions --
2376 ----------------------------
2378 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2379 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2380 -- Collect all [refined] postconditions of a specific kind denoted
2381 -- by Post_Nam that belong to the body, and generate pragma Check
2382 -- equivalents in list Stmts.
2384 procedure Process_Spec_Postconditions
;
2385 -- Collect all [inherited] postconditions of the spec, and generate
2386 -- pragma Check equivalents in list Stmts.
2388 ---------------------------------
2389 -- Process_Body_Postconditions --
2390 ---------------------------------
2392 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2393 Items
: constant Node_Id
:= Contract
(Body_Id
);
2394 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2399 -- Process the contract
2401 if Present
(Items
) then
2402 Prag
:= Pre_Post_Conditions
(Items
);
2403 while Present
(Prag
) loop
2404 if Pragma_Name
(Prag
) = Post_Nam
2405 and then Is_Checked
(Prag
)
2408 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2412 Prag
:= Next_Pragma
(Prag
);
2416 -- The subprogram body being processed is actually the proper body
2417 -- of a stub with a corresponding spec. The subprogram stub may
2418 -- carry a postcondition pragma, in which case it must be taken
2419 -- into account. The pragma appears after the stub.
2421 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2422 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2423 while Present
(Decl
) loop
2425 -- Note that non-matching pragmas are skipped
2427 if Nkind
(Decl
) = N_Pragma
then
2428 if Pragma_Name
(Decl
) = Post_Nam
2429 and then Is_Checked
(Decl
)
2432 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2436 -- Skip internally generated code
2438 elsif not Comes_From_Source
(Decl
) then
2441 -- Postcondition pragmas are usually grouped together. There
2442 -- is no need to inspect the whole declarative list.
2451 end Process_Body_Postconditions
;
2453 ---------------------------------
2454 -- Process_Spec_Postconditions --
2455 ---------------------------------
2457 procedure Process_Spec_Postconditions
is
2458 Subps
: constant Subprogram_List
:=
2459 Inherited_Subprograms
(Spec_Id
);
2463 Subp_Id
: Entity_Id
;
2466 -- Process the contract
2468 Items
:= Contract
(Spec_Id
);
2470 if Present
(Items
) then
2471 Prag
:= Pre_Post_Conditions
(Items
);
2472 while Present
(Prag
) loop
2473 if Pragma_Name
(Prag
) = Name_Postcondition
2474 and then Is_Checked
(Prag
)
2477 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2481 Prag
:= Next_Pragma
(Prag
);
2485 -- Process the contracts of all inherited subprograms, looking for
2486 -- class-wide postconditions.
2488 for Index
in Subps
'Range loop
2489 Subp_Id
:= Subps
(Index
);
2490 Items
:= Contract
(Subp_Id
);
2492 if Present
(Items
) then
2493 Prag
:= Pre_Post_Conditions
(Items
);
2494 while Present
(Prag
) loop
2495 if Pragma_Name
(Prag
) = Name_Postcondition
2496 and then Class_Present
(Prag
)
2499 Build_Pragma_Check_Equivalent
2502 Inher_Id
=> Subp_Id
);
2504 -- The pragma Check equivalent of the class-wide
2505 -- postcondition is still created even though the
2506 -- pragma may be ignored because the equivalent
2507 -- performs semantic checks.
2509 if Is_Checked
(Prag
) then
2510 Append_Enabled_Item
(Item
, Stmts
);
2514 Prag
:= Next_Pragma
(Prag
);
2518 end Process_Spec_Postconditions
;
2520 pragma Unmodified
(Stmts
);
2521 -- Stmts is passed as IN OUT to signal that the list can be updated,
2522 -- even if the corresponding integer value representing the list does
2525 -- Start of processing for Process_Postconditions
2528 -- The processing of postconditions is done in reverse order (body
2529 -- first) to ensure the following arrangement:
2531 -- <refined postconditions from body>
2532 -- <postconditions from body>
2533 -- <postconditions from spec>
2534 -- <inherited postconditions>
2536 Process_Body_Postconditions
(Name_Refined_Post
);
2537 Process_Body_Postconditions
(Name_Postcondition
);
2539 if Present
(Spec_Id
) then
2540 Process_Spec_Postconditions
;
2542 end Process_Postconditions
;
2544 ---------------------------
2545 -- Process_Preconditions --
2546 ---------------------------
2548 procedure Process_Preconditions
is
2549 Class_Pre
: Node_Id
:= Empty
;
2550 -- The sole [inherited] class-wide precondition pragma that applies
2551 -- to the subprogram.
2553 Insert_Node
: Node_Id
:= Empty
;
2554 -- The insertion node after which all pragma Check equivalents are
2557 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean;
2558 -- Determine whether arbitrary declaration Decl denotes a renaming of
2559 -- a discriminant or protection field _object.
2561 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
);
2562 -- Merge two class-wide preconditions by "or else"-ing them. The
2563 -- changes are accumulated in parameter Into. Update the error
2566 procedure Prepend_To_Decls
(Item
: Node_Id
);
2567 -- Prepend a single item to the declarations of the subprogram body
2569 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
);
2570 -- Save a class-wide precondition into Class_Pre, or prepend a normal
2571 -- precondition to the declarations of the body and analyze it.
2573 procedure Process_Inherited_Preconditions
;
2574 -- Collect all inherited class-wide preconditions and merge them into
2575 -- one big precondition to be evaluated as pragma Check.
2577 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
2578 -- Collect all preconditions of subprogram Subp_Id and prepend their
2579 -- pragma Check equivalents to the declarations of the body.
2581 --------------------------
2582 -- Is_Prologue_Renaming --
2583 --------------------------
2585 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
2592 if Nkind
(Decl
) = N_Object_Renaming_Declaration
then
2593 Obj
:= Defining_Entity
(Decl
);
2596 if Nkind
(Nam
) = N_Selected_Component
then
2597 Pref
:= Prefix
(Nam
);
2598 Sel
:= Selector_Name
(Nam
);
2600 -- A discriminant renaming appears as
2601 -- Discr : constant ... := Prefix.Discr;
2603 if Ekind
(Obj
) = E_Constant
2604 and then Is_Entity_Name
(Sel
)
2605 and then Present
(Entity
(Sel
))
2606 and then Ekind
(Entity
(Sel
)) = E_Discriminant
2610 -- A protection field renaming appears as
2611 -- Prot : ... := _object._object;
2613 -- A renamed private component is just a component of
2614 -- _object, with an arbitrary name.
2616 elsif Ekind
(Obj
) = E_Variable
2617 and then Nkind
(Pref
) = N_Identifier
2618 and then Chars
(Pref
) = Name_uObject
2619 and then Nkind
(Sel
) = N_Identifier
2627 end Is_Prologue_Renaming
;
2629 -------------------------
2630 -- Merge_Preconditions --
2631 -------------------------
2633 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
) is
2634 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
;
2635 -- Return the boolean expression argument of a precondition while
2636 -- updating its parentheses count for the subsequent merge.
2638 function Message_Arg
(Prag
: Node_Id
) return Node_Id
;
2639 -- Return the message argument of a precondition
2641 --------------------
2642 -- Expression_Arg --
2643 --------------------
2645 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
is
2646 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2647 Arg
: constant Node_Id
:= Get_Pragma_Arg
(Next
(First
(Args
)));
2650 if Paren_Count
(Arg
) = 0 then
2651 Set_Paren_Count
(Arg
, 1);
2661 function Message_Arg
(Prag
: Node_Id
) return Node_Id
is
2662 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2664 return Get_Pragma_Arg
(Last
(Args
));
2669 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
2670 From_Msg
: constant Node_Id
:= Message_Arg
(From
);
2671 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
2672 Into_Msg
: constant Node_Id
:= Message_Arg
(Into
);
2673 Loc
: constant Source_Ptr
:= Sloc
(Into
);
2675 -- Start of processing for Merge_Preconditions
2678 -- Merge the two preconditions by "or else"-ing them
2682 Right_Opnd
=> Relocate_Node
(Into_Expr
),
2683 Left_Opnd
=> From_Expr
));
2685 -- Merge the two error messages to produce a single message of the
2688 -- failed precondition from ...
2689 -- also failed inherited precondition from ...
2691 if not Exception_Locations_Suppressed
then
2692 Start_String
(Strval
(Into_Msg
));
2693 Store_String_Char
(ASCII
.LF
);
2694 Store_String_Chars
(" also ");
2695 Store_String_Chars
(Strval
(From_Msg
));
2697 Set_Strval
(Into_Msg
, End_String
);
2699 end Merge_Preconditions
;
2701 ----------------------
2702 -- Prepend_To_Decls --
2703 ----------------------
2705 procedure Prepend_To_Decls
(Item
: Node_Id
) is
2709 Decls
:= Declarations
(Body_Decl
);
2711 -- Ensure that the body has a declarative list
2715 Set_Declarations
(Body_Decl
, Decls
);
2718 Prepend_To
(Decls
, Item
);
2719 end Prepend_To_Decls
;
2721 ------------------------------
2722 -- Prepend_To_Decls_Or_Save --
2723 ------------------------------
2725 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
) is
2726 Check_Prag
: Node_Id
;
2729 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
2731 -- Save the sole class-wide precondition (if any) for the next
2732 -- step, where it will be merged with inherited preconditions.
2734 if Class_Present
(Prag
) then
2735 pragma Assert
(No
(Class_Pre
));
2736 Class_Pre
:= Check_Prag
;
2738 -- Accumulate the corresponding Check pragmas at the top of the
2739 -- declarations. Prepending the items ensures that they will be
2740 -- evaluated in their original order.
2743 if Present
(Insert_Node
) then
2744 Insert_After
(Insert_Node
, Check_Prag
);
2746 Prepend_To_Decls
(Check_Prag
);
2749 Analyze
(Check_Prag
);
2751 end Prepend_To_Decls_Or_Save
;
2753 -------------------------------------
2754 -- Process_Inherited_Preconditions --
2755 -------------------------------------
2757 procedure Process_Inherited_Preconditions
is
2758 Subps
: constant Subprogram_List
:=
2759 Inherited_Subprograms
(Spec_Id
);
2764 Subp_Id
: Entity_Id
;
2767 -- Process the contracts of all inherited subprograms, looking for
2768 -- class-wide preconditions.
2770 for Index
in Subps
'Range loop
2771 Subp_Id
:= Subps
(Index
);
2772 Items
:= Contract
(Subp_Id
);
2774 if Present
(Items
) then
2775 Prag
:= Pre_Post_Conditions
(Items
);
2776 while Present
(Prag
) loop
2777 if Pragma_Name
(Prag
) = Name_Precondition
2778 and then Class_Present
(Prag
)
2781 Build_Pragma_Check_Equivalent
2784 Inher_Id
=> Subp_Id
);
2786 -- The pragma Check equivalent of the class-wide
2787 -- precondition is still created even though the
2788 -- pragma may be ignored because the equivalent
2789 -- performs semantic checks.
2791 if Is_Checked
(Prag
) then
2793 -- The spec of an inherited subprogram already
2794 -- yielded a class-wide precondition. Merge the
2795 -- existing precondition with the current one
2798 if Present
(Class_Pre
) then
2799 Merge_Preconditions
(Item
, Class_Pre
);
2806 Prag
:= Next_Pragma
(Prag
);
2811 -- Add the merged class-wide preconditions
2813 if Present
(Class_Pre
) then
2814 Prepend_To_Decls
(Class_Pre
);
2815 Analyze
(Class_Pre
);
2817 end Process_Inherited_Preconditions
;
2819 -------------------------------
2820 -- Process_Preconditions_For --
2821 -------------------------------
2823 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
2824 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2828 Subp_Decl
: Node_Id
;
2831 -- Process the contract
2833 if Present
(Items
) then
2834 Prag
:= Pre_Post_Conditions
(Items
);
2835 while Present
(Prag
) loop
2836 if Pragma_Name
(Prag
) = Name_Precondition
2837 and then Is_Checked
(Prag
)
2839 Prepend_To_Decls_Or_Save
(Prag
);
2842 Prag
:= Next_Pragma
(Prag
);
2846 -- The subprogram declaration being processed is actually a body
2847 -- stub. The stub may carry a precondition pragma, in which case
2848 -- it must be taken into account. The pragma appears after the
2851 Subp_Decl
:= Unit_Declaration_Node
(Subp_Id
);
2853 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
2855 -- Inspect the declarations following the body stub
2857 Decl
:= Next
(Subp_Decl
);
2858 while Present
(Decl
) loop
2860 -- Note that non-matching pragmas are skipped
2862 if Nkind
(Decl
) = N_Pragma
then
2863 if Pragma_Name
(Decl
) = Name_Precondition
2864 and then Is_Checked
(Decl
)
2866 Prepend_To_Decls_Or_Save
(Decl
);
2869 -- Skip internally generated code
2871 elsif not Comes_From_Source
(Decl
) then
2874 -- Preconditions are usually grouped together. There is no
2875 -- need to inspect the whole declarative list.
2884 end Process_Preconditions_For
;
2888 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2891 -- Start of processing for Process_Preconditions
2894 -- Find the proper insertion point for all pragma Check equivalents
2896 if Present
(Decls
) then
2897 Decl
:= First
(Decls
);
2898 while Present
(Decl
) loop
2900 -- First source declaration terminates the search, because all
2901 -- preconditions must be evaluated prior to it, by definition.
2903 if Comes_From_Source
(Decl
) then
2906 -- Certain internally generated object renamings such as those
2907 -- for discriminants and protection fields must be elaborated
2908 -- before the preconditions are evaluated, as their expressions
2909 -- may mention the discriminants. The renamings include those
2910 -- for private components so we need to find the last such.
2912 elsif Is_Prologue_Renaming
(Decl
) then
2913 while Present
(Next
(Decl
))
2914 and then Is_Prologue_Renaming
(Next
(Decl
))
2919 Insert_Node
:= Decl
;
2921 -- Otherwise the declaration does not come from source. This
2922 -- also terminates the search, because internal code may raise
2923 -- exceptions which should not preempt the preconditions.
2933 -- The processing of preconditions is done in reverse order (body
2934 -- first), because each pragma Check equivalent is inserted at the
2935 -- top of the declarations. This ensures that the final order is
2936 -- consistent with following diagram:
2938 -- <inherited preconditions>
2939 -- <preconditions from spec>
2940 -- <preconditions from body>
2942 Process_Preconditions_For
(Body_Id
);
2944 if Present
(Spec_Id
) then
2945 Process_Preconditions_For
(Spec_Id
);
2946 Process_Inherited_Preconditions
;
2948 end Process_Preconditions
;
2952 Restore_Scope
: Boolean := False;
2954 Stmts
: List_Id
:= No_List
;
2955 Subp_Id
: Entity_Id
;
2957 -- Start of processing for Expand_Subprogram_Contract
2960 -- Obtain the entity of the initial declaration
2962 if Present
(Spec_Id
) then
2968 -- Do not perform expansion activity when it is not needed
2970 if not Expander_Active
then
2973 -- ASIS requires an unaltered tree
2975 elsif ASIS_Mode
then
2978 -- GNATprove does not need the executable semantics of a contract
2980 elsif GNATprove_Mode
then
2983 -- The contract of a generic subprogram or one declared in a generic
2984 -- context is not expanded, as the corresponding instance will provide
2985 -- the executable semantics of the contract.
2987 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
2990 -- All subprograms carry a contract, but for some it is not significant
2991 -- and should not be processed. This is a small optimization.
2993 elsif not Has_Significant_Contract
(Subp_Id
) then
2996 -- The contract of an ignored Ghost subprogram does not need expansion,
2997 -- because the subprogram and all calls to it will be removed.
2999 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
3002 -- Do not re-expand the same contract. This scenario occurs when a
3003 -- construct is rewritten into something else during its analysis
3004 -- (expression functions for instance).
3006 elsif Has_Expanded_Contract
(Subp_Id
) then
3010 -- Prevent multiple expansion attempts of the same contract
3012 Set_Has_Expanded_Contract
(Subp_Id
);
3014 -- Ensure that the formal parameters are visible when expanding all
3017 if not In_Open_Scopes
(Subp_Id
) then
3018 Restore_Scope
:= True;
3019 Push_Scope
(Subp_Id
);
3021 if Is_Generic_Subprogram
(Subp_Id
) then
3022 Install_Generic_Formals
(Subp_Id
);
3024 Install_Formals
(Subp_Id
);
3028 -- The expansion of a subprogram contract involves the creation of Check
3029 -- pragmas to verify the contract assertions of the spec and body in a
3030 -- particular order. The order is as follows:
3032 -- function Example (...) return ... is
3033 -- procedure _Postconditions (...) is
3035 -- <refined postconditions from body>
3036 -- <postconditions from body>
3037 -- <postconditions from spec>
3038 -- <inherited postconditions>
3039 -- <contract case consequences>
3040 -- <invariant check of function result>
3041 -- <invariant and predicate checks of parameters>
3042 -- end _Postconditions;
3044 -- <inherited preconditions>
3045 -- <preconditions from spec>
3046 -- <preconditions from body>
3047 -- <contract case conditions>
3049 -- <source declarations>
3051 -- <source statements>
3053 -- _Preconditions (Result);
3057 -- Routine _Postconditions holds all contract assertions that must be
3058 -- verified on exit from the related subprogram.
3060 -- Step 1: Handle all preconditions. This action must come before the
3061 -- processing of pragma Contract_Cases because the pragma prepends items
3062 -- to the body declarations.
3064 Process_Preconditions
;
3066 -- Step 2: Handle all postconditions. This action must come before the
3067 -- processing of pragma Contract_Cases because the pragma appends items
3070 Process_Postconditions
(Stmts
);
3072 -- Step 3: Handle pragma Contract_Cases. This action must come before
3073 -- the processing of invariants and predicates because those append
3074 -- items to list Stmts.
3076 Process_Contract_Cases
(Stmts
);
3078 -- Step 4: Apply invariant and predicate checks on a function result and
3079 -- all formals. The resulting checks are accumulated in list Stmts.
3081 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3083 -- Step 5: Construct procedure _Postconditions
3085 Build_Postconditions_Procedure
(Subp_Id
, Stmts
, Result
);
3087 if Restore_Scope
then
3090 end Expand_Subprogram_Contract
;
3092 -------------------------------
3093 -- Freeze_Previous_Contracts --
3094 -------------------------------
3096 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3097 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3098 pragma Inline
(Causes_Contract_Freezing
);
3099 -- Determine whether arbitrary node N causes contract freezing
3101 procedure Freeze_Contracts
;
3102 pragma Inline
(Freeze_Contracts
);
3103 -- Freeze the contracts of all eligible constructs which precede body
3106 procedure Freeze_Enclosing_Package_Body
;
3107 pragma Inline
(Freeze_Enclosing_Package_Body
);
3108 -- Freeze the contract of the nearest package body (if any) which
3109 -- encloses body Body_Decl.
3111 ------------------------------
3112 -- Causes_Contract_Freezing --
3113 ------------------------------
3115 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3117 return Nkind_In
(N
, N_Entry_Body
,
3121 N_Subprogram_Body_Stub
,
3123 end Causes_Contract_Freezing
;
3125 ----------------------
3126 -- Freeze_Contracts --
3127 ----------------------
3129 procedure Freeze_Contracts
is
3130 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3134 -- Nothing to do when the body which causes freezing does not appear
3135 -- in a declarative list because there cannot possibly be constructs
3138 if not Is_List_Member
(Body_Decl
) then
3142 -- Inspect the declarations preceding the body, and freeze individual
3143 -- contracts of eligible constructs.
3145 Decl
:= Prev
(Body_Decl
);
3146 while Present
(Decl
) loop
3148 -- Stop the traversal when a preceding construct that causes
3149 -- freezing is encountered as there is no point in refreezing
3150 -- the already frozen constructs.
3152 if Causes_Contract_Freezing
(Decl
) then
3155 -- Entry or subprogram declarations
3157 elsif Nkind_In
(Decl
, N_Abstract_Subprogram_Declaration
,
3158 N_Entry_Declaration
,
3159 N_Generic_Subprogram_Declaration
,
3160 N_Subprogram_Declaration
)
3162 Analyze_Entry_Or_Subprogram_Contract
3163 (Subp_Id
=> Defining_Entity
(Decl
),
3164 Freeze_Id
=> Body_Id
);
3168 elsif Nkind
(Decl
) = N_Object_Declaration
then
3169 Analyze_Object_Contract
3170 (Obj_Id
=> Defining_Entity
(Decl
),
3171 Freeze_Id
=> Body_Id
);
3175 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
3176 N_Single_Protected_Declaration
)
3178 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3180 -- Subprogram body stubs
3182 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3183 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3187 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
3188 N_Task_Type_Declaration
)
3190 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3195 end Freeze_Contracts
;
3197 -----------------------------------
3198 -- Freeze_Enclosing_Package_Body --
3199 -----------------------------------
3201 procedure Freeze_Enclosing_Package_Body
is
3202 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3206 -- Climb the parent chain looking for an enclosing package body. Do
3207 -- not use the scope stack, because a body utilizes the entity of its
3208 -- corresponding spec.
3210 Par
:= Parent
(Body_Decl
);
3211 while Present
(Par
) loop
3212 if Nkind
(Par
) = N_Package_Body
then
3213 Analyze_Package_Body_Contract
3214 (Body_Id
=> Defining_Entity
(Par
),
3215 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3219 -- Do not look for an enclosing package body when the construct
3220 -- which causes freezing is a body generated for an expression
3221 -- function and it appears within a package spec. This ensures
3222 -- that the traversal will not reach too far up the parent chain
3223 -- and attempt to freeze a package body which must not be frozen.
3225 -- package body Enclosing_Body
3226 -- with Refined_State => (State => Var)
3228 -- package Nested is
3229 -- type Some_Type is ...;
3230 -- function Cause_Freezing return ...;
3232 -- function Cause_Freezing is (...);
3235 -- Var : Nested.Some_Type;
3237 elsif Nkind
(Par
) = N_Package_Declaration
3238 and then Nkind
(Orig_Decl
) = N_Expression_Function
3242 -- Prevent the search from going too far
3244 elsif Is_Body_Or_Package_Declaration
(Par
) then
3248 Par
:= Parent
(Par
);
3250 end Freeze_Enclosing_Package_Body
;
3254 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3256 -- Start of processing for Freeze_Previous_Contracts
3259 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3261 -- A body that is in the process of being inlined appears from source,
3262 -- but carries name _parent. Such a body does not cause freezing of
3265 if Chars
(Body_Id
) = Name_uParent
then
3269 Freeze_Enclosing_Package_Body
;
3271 end Freeze_Previous_Contracts
;
3273 ---------------------------------
3274 -- Inherit_Subprogram_Contract --
3275 ---------------------------------
3277 procedure Inherit_Subprogram_Contract
3279 From_Subp
: Entity_Id
)
3281 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3282 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3285 --------------------
3286 -- Inherit_Pragma --
3287 --------------------
3289 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3290 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3294 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3295 -- chains, therefore the node must be replicated. The new pragma is
3296 -- flagged as inherited for distinction purposes.
3298 if Present
(Prag
) then
3299 New_Prag
:= New_Copy_Tree
(Prag
);
3300 Set_Is_Inherited_Pragma
(New_Prag
);
3302 Add_Contract_Item
(New_Prag
, Subp
);
3306 -- Start of processing for Inherit_Subprogram_Contract
3309 -- Inheritance is carried out only when both entities are subprograms
3312 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3313 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3314 and then Present
(Contract
(From_Subp
))
3316 Inherit_Pragma
(Pragma_Extensions_Visible
);
3318 end Inherit_Subprogram_Contract
;
3320 -------------------------------------
3321 -- Instantiate_Subprogram_Contract --
3322 -------------------------------------
3324 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3325 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3326 -- Instantiate all contract-related source pragmas found in the list,
3327 -- starting with pragma First_Prag. Each instantiated pragma is added
3330 -------------------------
3331 -- Instantiate_Pragmas --
3332 -------------------------
3334 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3335 Inst_Prag
: Node_Id
;
3340 while Present
(Prag
) loop
3341 if Is_Generic_Contract_Pragma
(Prag
) then
3343 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3345 Set_Analyzed
(Inst_Prag
, False);
3346 Append_To
(L
, Inst_Prag
);
3349 Prag
:= Next_Pragma
(Prag
);
3351 end Instantiate_Pragmas
;
3355 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3357 -- Start of processing for Instantiate_Subprogram_Contract
3360 if Present
(Items
) then
3361 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3362 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3363 Instantiate_Pragmas
(Classifications
(Items
));
3365 end Instantiate_Subprogram_Contract
;
3367 ----------------------------------------
3368 -- Save_Global_References_In_Contract --
3369 ----------------------------------------
3371 procedure Save_Global_References_In_Contract
3375 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
3376 -- Save all global references in contract-related source pragmas found
3377 -- in the list, starting with pragma First_Prag.
3379 ------------------------------------
3380 -- Save_Global_References_In_List --
3381 ------------------------------------
3383 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
3388 while Present
(Prag
) loop
3389 if Is_Generic_Contract_Pragma
(Prag
) then
3390 Save_Global_References
(Prag
);
3393 Prag
:= Next_Pragma
(Prag
);
3395 end Save_Global_References_In_List
;
3399 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3401 -- Start of processing for Save_Global_References_In_Contract
3404 -- The entity of the analyzed generic copy must be on the scope stack
3405 -- to ensure proper detection of global references.
3407 Push_Scope
(Gen_Id
);
3409 if Permits_Aspect_Specifications
(Templ
)
3410 and then Has_Aspects
(Templ
)
3412 Save_Global_References_In_Aspects
(Templ
);
3415 if Present
(Items
) then
3416 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
3417 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
3418 Save_Global_References_In_List
(Classifications
(Items
));
3422 end Save_Global_References_In_Contract
;