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 Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
);
57 -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
58 -- contract-only subprogram body of eligible subprograms found in L, adds
59 -- them to their corresponding list of declarations, and analyzes them.
61 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
);
62 -- Expand the contracts of a subprogram body and its correspoding spec (if
63 -- any). This routine processes all [refined] pre- and postconditions as
64 -- well as Contract_Cases, invariants and predicates. Body_Id denotes the
65 -- entity of the subprogram body.
67 -----------------------
68 -- Add_Contract_Item --
69 -----------------------
71 procedure Add_Contract_Item
(Prag
: Node_Id
; Id
: Entity_Id
) is
72 Items
: Node_Id
:= Contract
(Id
);
74 procedure Add_Classification
;
75 -- Prepend Prag to the list of classifications
77 procedure Add_Contract_Test_Case
;
78 -- Prepend Prag to the list of contract and test cases
80 procedure Add_Pre_Post_Condition
;
81 -- Prepend Prag to the list of pre- and postconditions
83 ------------------------
84 -- Add_Classification --
85 ------------------------
87 procedure Add_Classification
is
89 Set_Next_Pragma
(Prag
, Classifications
(Items
));
90 Set_Classifications
(Items
, Prag
);
91 end Add_Classification
;
93 ----------------------------
94 -- Add_Contract_Test_Case --
95 ----------------------------
97 procedure Add_Contract_Test_Case
is
99 Set_Next_Pragma
(Prag
, Contract_Test_Cases
(Items
));
100 Set_Contract_Test_Cases
(Items
, Prag
);
101 end Add_Contract_Test_Case
;
103 ----------------------------
104 -- Add_Pre_Post_Condition --
105 ----------------------------
107 procedure Add_Pre_Post_Condition
is
109 Set_Next_Pragma
(Prag
, Pre_Post_Conditions
(Items
));
110 Set_Pre_Post_Conditions
(Items
, Prag
);
111 end Add_Pre_Post_Condition
;
115 -- A contract must contain only pragmas
117 pragma Assert
(Nkind
(Prag
) = N_Pragma
);
118 Prag_Nam
: constant Name_Id
:= Pragma_Name
(Prag
);
120 -- Start of processing for Add_Contract_Item
123 -- Create a new contract when adding the first item
126 Items
:= Make_Contract
(Sloc
(Id
));
127 Set_Contract
(Id
, Items
);
130 -- Constants, the applicable pragmas are:
133 if Ekind
(Id
) = E_Constant
then
134 if Prag_Nam
= Name_Part_Of
then
137 -- The pragma is not a proper contract item
143 -- Entry bodies, the applicable pragmas are:
148 elsif Is_Entry_Body
(Id
) then
149 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
152 elsif Prag_Nam
= Name_Refined_Post
then
153 Add_Pre_Post_Condition
;
155 -- The pragma is not a proper contract item
161 -- Entry or subprogram declarations, the applicable pragmas are:
165 -- Extensions_Visible
173 elsif Is_Entry_Declaration
(Id
)
174 or else Ekind_In
(Id
, E_Function
,
179 if Nam_In
(Prag_Nam
, Name_Attach_Handler
, Name_Interrupt_Handler
)
180 and then Ekind_In
(Id
, E_Generic_Procedure
, E_Procedure
)
184 elsif Nam_In
(Prag_Nam
, Name_Depends
,
185 Name_Extensions_Visible
,
190 elsif Prag_Nam
= Name_Volatile_Function
191 and then Ekind_In
(Id
, E_Function
, E_Generic_Function
)
195 elsif Nam_In
(Prag_Nam
, Name_Contract_Cases
, Name_Test_Case
) then
196 Add_Contract_Test_Case
;
198 elsif Nam_In
(Prag_Nam
, Name_Postcondition
, Name_Precondition
) then
199 Add_Pre_Post_Condition
;
201 -- The pragma is not a proper contract item
207 -- Packages or instantiations, the applicable pragmas are:
211 -- Part_Of (instantiation only)
213 elsif Ekind_In
(Id
, E_Generic_Package
, E_Package
) then
214 if Nam_In
(Prag_Nam
, Name_Abstract_State
,
215 Name_Initial_Condition
,
220 -- Indicator Part_Of must be associated with a package instantiation
222 elsif Prag_Nam
= Name_Part_Of
and then Is_Generic_Instance
(Id
) then
225 -- The pragma is not a proper contract item
231 -- Package bodies, the applicable pragmas are:
234 elsif Ekind
(Id
) = E_Package_Body
then
235 if Prag_Nam
= Name_Refined_State
then
238 -- The pragma is not a proper contract item
244 -- Protected units, the applicable pragmas are:
247 elsif Ekind
(Id
) = E_Protected_Type
then
248 if Prag_Nam
= Name_Part_Of
then
251 -- The pragma is not a proper contract item
257 -- Subprogram bodies, the applicable pragmas are:
264 elsif Ekind
(Id
) = E_Subprogram_Body
then
265 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
268 elsif Nam_In
(Prag_Nam
, Name_Postcondition
,
272 Add_Pre_Post_Condition
;
274 -- The pragma is not a proper contract item
280 -- Task bodies, the applicable pragmas are:
284 elsif Ekind
(Id
) = E_Task_Body
then
285 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
288 -- The pragma is not a proper contract item
294 -- Task units, the applicable pragmas are:
299 elsif Ekind
(Id
) = E_Task_Type
then
300 if Nam_In
(Prag_Nam
, Name_Depends
, Name_Global
, Name_Part_Of
) then
303 -- The pragma is not a proper contract item
309 -- Variables, the applicable pragmas are:
312 -- Constant_After_Elaboration
319 elsif Ekind
(Id
) = E_Variable
then
320 if Nam_In
(Prag_Nam
, Name_Async_Readers
,
322 Name_Constant_After_Elaboration
,
324 Name_Effective_Reads
,
325 Name_Effective_Writes
,
331 -- The pragma is not a proper contract item
337 end Add_Contract_Item
;
339 -----------------------
340 -- Analyze_Contracts --
341 -----------------------
343 procedure Analyze_Contracts
(L
: List_Id
) is
347 if CodePeer_Mode
and then Debug_Flag_Dot_KK
then
348 Build_And_Analyze_Contract_Only_Subprograms
(L
);
352 while Present
(Decl
) loop
354 -- Entry or subprogram declarations
356 if Nkind_In
(Decl
, N_Abstract_Subprogram_Declaration
,
358 N_Generic_Subprogram_Declaration
,
359 N_Subprogram_Declaration
)
362 Subp_Id
: constant Entity_Id
:= Defining_Entity
(Decl
);
365 Analyze_Entry_Or_Subprogram_Contract
(Subp_Id
);
367 -- If analysis of a class-wide pre/postcondition indicates
368 -- that a class-wide clone is needed, analyze its declaration
369 -- now. Its body is created when the body of the original
370 -- operation is analyzed (and rewritten).
372 if Is_Subprogram
(Subp_Id
)
373 and then Present
(Class_Wide_Clone
(Subp_Id
))
375 Analyze
(Unit_Declaration_Node
(Class_Wide_Clone
(Subp_Id
)));
379 -- Entry or subprogram bodies
381 elsif Nkind_In
(Decl
, N_Entry_Body
, N_Subprogram_Body
) then
382 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
386 elsif Nkind
(Decl
) = N_Object_Declaration
then
387 Analyze_Object_Contract
(Defining_Entity
(Decl
));
391 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
392 N_Single_Protected_Declaration
)
394 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
396 -- Subprogram body stubs
398 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
399 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
403 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
404 N_Task_Type_Declaration
)
406 Analyze_Task_Contract
(Defining_Entity
(Decl
));
408 -- For type declarations, we need to do the preanalysis of Iterable
409 -- aspect specifications.
411 -- Other type aspects need to be resolved here???
413 elsif Nkind
(Decl
) = N_Private_Type_Declaration
414 and then Present
(Aspect_Specifications
(Decl
))
417 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
418 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
422 Validate_Iterable_Aspect
(E
, It
);
429 end Analyze_Contracts
;
431 -----------------------------------------------
432 -- Analyze_Entry_Or_Subprogram_Body_Contract --
433 -----------------------------------------------
435 -- WARNING: This routine manages SPARK regions. Return statements must be
436 -- replaced by gotos which jump to the end of the routine and restore the
439 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
440 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
441 Items
: constant Node_Id
:= Contract
(Body_Id
);
442 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
444 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
445 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
446 -- Save the SPARK_Mode-related data to restore on exit
449 -- When a subprogram body declaration is illegal, its defining entity is
450 -- left unanalyzed. There is nothing left to do in this case because the
451 -- body lacks a contract, or even a proper Ekind.
453 if Ekind
(Body_Id
) = E_Void
then
456 -- Do not analyze a contract multiple times
458 elsif Present
(Items
) then
459 if Analyzed
(Items
) then
462 Set_Analyzed
(Items
);
466 -- Due to the timing of contract analysis, delayed pragmas may be
467 -- subject to the wrong SPARK_Mode, usually that of the enclosing
468 -- context. To remedy this, restore the original SPARK_Mode of the
469 -- related subprogram body.
471 Set_SPARK_Mode
(Body_Id
);
473 -- Ensure that the contract cases or postconditions mention 'Result or
474 -- define a post-state.
476 Check_Result_And_Post_State
(Body_Id
);
478 -- A stand-alone nonvolatile function body cannot have an effectively
479 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
480 -- check is relevant only when SPARK_Mode is on, as it is not a standard
481 -- legality rule. The check is performed here because Volatile_Function
482 -- is processed after the analysis of the related subprogram body. The
483 -- check only applies to source subprograms and not to generated TSS
487 and then Ekind_In
(Body_Id
, E_Function
, E_Generic_Function
)
488 and then Comes_From_Source
(Spec_Id
)
489 and then not Is_Volatile_Function
(Body_Id
)
491 Check_Nonvolatile_Function_Profile
(Body_Id
);
494 -- Restore the SPARK_Mode of the enclosing context after all delayed
495 -- pragmas have been analyzed.
497 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
499 -- Capture all global references in a generic subprogram body now that
500 -- the contract has been analyzed.
502 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
503 Save_Global_References_In_Contract
504 (Templ
=> Original_Node
(Body_Decl
),
508 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
509 -- invariants and predicates associated with body and its spec. Do not
510 -- expand the contract of subprogram body stubs.
512 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
513 Expand_Subprogram_Contract
(Body_Id
);
515 end Analyze_Entry_Or_Subprogram_Body_Contract
;
517 ------------------------------------------
518 -- Analyze_Entry_Or_Subprogram_Contract --
519 ------------------------------------------
521 -- WARNING: This routine manages SPARK regions. Return statements must be
522 -- replaced by gotos which jump to the end of the routine and restore the
525 procedure Analyze_Entry_Or_Subprogram_Contract
526 (Subp_Id
: Entity_Id
;
527 Freeze_Id
: Entity_Id
:= Empty
)
529 Items
: constant Node_Id
:= Contract
(Subp_Id
);
530 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
532 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
533 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
534 -- Save the SPARK_Mode-related data to restore on exit
536 Skip_Assert_Exprs
: constant Boolean :=
537 Ekind_In
(Subp_Id
, E_Entry
, E_Entry_Family
)
538 and then not ASIS_Mode
539 and then not GNATprove_Mode
;
541 Depends
: Node_Id
:= Empty
;
542 Global
: Node_Id
:= Empty
;
547 -- Do not analyze a contract multiple times
549 if Present
(Items
) then
550 if Analyzed
(Items
) then
553 Set_Analyzed
(Items
);
557 -- Due to the timing of contract analysis, delayed pragmas may be
558 -- subject to the wrong SPARK_Mode, usually that of the enclosing
559 -- context. To remedy this, restore the original SPARK_Mode of the
560 -- related subprogram body.
562 Set_SPARK_Mode
(Subp_Id
);
564 -- All subprograms carry a contract, but for some it is not significant
565 -- and should not be processed.
567 if not Has_Significant_Contract
(Subp_Id
) then
570 elsif Present
(Items
) then
572 -- Do not analyze the pre/postconditions of an entry declaration
573 -- unless annotating the original tree for ASIS or GNATprove. The
574 -- real analysis occurs when the pre/postconditons are relocated to
575 -- the contract wrapper procedure (see Build_Contract_Wrapper).
577 if Skip_Assert_Exprs
then
580 -- Otherwise analyze the pre/postconditions
583 Prag
:= Pre_Post_Conditions
(Items
);
584 while Present
(Prag
) loop
585 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
586 Prag
:= Next_Pragma
(Prag
);
590 -- Analyze contract-cases and test-cases
592 Prag
:= Contract_Test_Cases
(Items
);
593 while Present
(Prag
) loop
594 Prag_Nam
:= Pragma_Name
(Prag
);
596 if Prag_Nam
= Name_Contract_Cases
then
598 -- Do not analyze the contract cases of an entry declaration
599 -- unless annotating the original tree for ASIS or GNATprove.
600 -- The real analysis occurs when the contract cases are moved
601 -- to the contract wrapper procedure (Build_Contract_Wrapper).
603 if Skip_Assert_Exprs
then
606 -- Otherwise analyze the contract cases
609 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
612 pragma Assert
(Prag_Nam
= Name_Test_Case
);
613 Analyze_Test_Case_In_Decl_Part
(Prag
);
616 Prag
:= Next_Pragma
(Prag
);
619 -- Analyze classification pragmas
621 Prag
:= Classifications
(Items
);
622 while Present
(Prag
) loop
623 Prag_Nam
:= Pragma_Name
(Prag
);
625 if Prag_Nam
= Name_Depends
then
628 elsif Prag_Nam
= Name_Global
then
632 Prag
:= Next_Pragma
(Prag
);
635 -- Analyze Global first, as Depends may mention items classified in
636 -- the global categorization.
638 if Present
(Global
) then
639 Analyze_Global_In_Decl_Part
(Global
);
642 -- Depends must be analyzed after Global in order to see the modes of
645 if Present
(Depends
) then
646 Analyze_Depends_In_Decl_Part
(Depends
);
649 -- Ensure that the contract cases or postconditions mention 'Result
650 -- or define a post-state.
652 Check_Result_And_Post_State
(Subp_Id
);
655 -- A nonvolatile function cannot have an effectively volatile formal
656 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
657 -- only when SPARK_Mode is on, as it is not a standard legality rule.
658 -- The check is performed here because pragma Volatile_Function is
659 -- processed after the analysis of the related subprogram declaration.
662 and then Ekind_In
(Subp_Id
, E_Function
, E_Generic_Function
)
663 and then Comes_From_Source
(Subp_Id
)
664 and then not Is_Volatile_Function
(Subp_Id
)
666 Check_Nonvolatile_Function_Profile
(Subp_Id
);
669 -- Restore the SPARK_Mode of the enclosing context after all delayed
670 -- pragmas have been analyzed.
672 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
674 -- Capture all global references in a generic subprogram now that the
675 -- contract has been analyzed.
677 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
678 Save_Global_References_In_Contract
679 (Templ
=> Original_Node
(Subp_Decl
),
682 end Analyze_Entry_Or_Subprogram_Contract
;
684 -----------------------------
685 -- Analyze_Object_Contract --
686 -----------------------------
688 -- WARNING: This routine manages SPARK regions. Return statements must be
689 -- replaced by gotos which jump to the end of the routine and restore the
692 procedure Analyze_Object_Contract
694 Freeze_Id
: Entity_Id
:= Empty
)
696 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
698 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
699 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
700 -- Save the SPARK_Mode-related data to restore on exit
702 AR_Val
: Boolean := False;
703 AW_Val
: Boolean := False;
704 ER_Val
: Boolean := False;
705 EW_Val
: Boolean := False;
709 Seen
: Boolean := False;
712 -- The loop parameter in an element iterator over a formal container
713 -- is declared with an object declaration, but no contracts apply.
715 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
719 -- Do not analyze a contract multiple times
721 Items
:= Contract
(Obj_Id
);
723 if Present
(Items
) then
724 if Analyzed
(Items
) then
727 Set_Analyzed
(Items
);
731 -- The anonymous object created for a single concurrent type inherits
732 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
733 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
734 -- of the enclosing context. To remedy this, restore the original mode
735 -- of the related anonymous object.
737 if Is_Single_Concurrent_Object
(Obj_Id
)
738 and then Present
(SPARK_Pragma
(Obj_Id
))
740 Set_SPARK_Mode
(Obj_Id
);
743 -- Constant-related checks
745 if Ekind
(Obj_Id
) = E_Constant
then
747 -- Analyze indicator Part_Of
749 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
751 -- Check whether the lack of indicator Part_Of agrees with the
752 -- placement of the constant with respect to the state space.
755 Check_Missing_Part_Of
(Obj_Id
);
758 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
759 -- This check is relevant only when SPARK_Mode is on, as it is not
760 -- a standard Ada legality rule. Internally-generated constants that
761 -- map generic formals to actuals in instantiations are allowed to
765 and then Comes_From_Source
(Obj_Id
)
766 and then Is_Effectively_Volatile
(Obj_Id
)
767 and then No
(Corresponding_Generic_Association
(Parent
(Obj_Id
)))
769 Error_Msg_N
("constant cannot be volatile", Obj_Id
);
772 -- Variable-related checks
774 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
776 -- Analyze all external properties
778 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Readers
);
780 if Present
(Prag
) then
781 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
785 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Writers
);
787 if Present
(Prag
) then
788 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
792 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Reads
);
794 if Present
(Prag
) then
795 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
799 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Writes
);
801 if Present
(Prag
) then
802 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
806 -- Verify the mutual interaction of the various external properties
809 Check_External_Properties
(Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
812 -- The anonymous object created for a single concurrent type carries
813 -- pragmas Depends and Globat of the type.
815 if Is_Single_Concurrent_Object
(Obj_Id
) then
817 -- Analyze Global first, as Depends may mention items classified
818 -- in the global categorization.
820 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
822 if Present
(Prag
) then
823 Analyze_Global_In_Decl_Part
(Prag
);
826 -- Depends must be analyzed after Global in order to see the modes
827 -- of all global items.
829 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
831 if Present
(Prag
) then
832 Analyze_Depends_In_Decl_Part
(Prag
);
836 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
838 -- Analyze indicator Part_Of
840 if Present
(Prag
) then
841 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
843 -- The variable is a constituent of a single protected/task type
844 -- and behaves as a component of the type. Verify that references
845 -- to the variable occur within the definition or body of the type
848 if Present
(Encapsulating_State
(Obj_Id
))
849 and then Is_Single_Concurrent_Object
850 (Encapsulating_State
(Obj_Id
))
851 and then Present
(Part_Of_References
(Obj_Id
))
853 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
854 while Present
(Ref_Elmt
) loop
855 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
856 Next_Elmt
(Ref_Elmt
);
860 -- Otherwise check whether the lack of indicator Part_Of agrees with
861 -- the placement of the variable with respect to the state space.
864 Check_Missing_Part_Of
(Obj_Id
);
867 -- The following checks are relevant only when SPARK_Mode is on, as
868 -- they are not standard Ada legality rules. Internally generated
869 -- temporaries are ignored.
871 if SPARK_Mode
= On
and then Comes_From_Source
(Obj_Id
) then
872 if Is_Effectively_Volatile
(Obj_Id
) then
874 -- The declaration of an effectively volatile object must
875 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
877 if not Is_Library_Level_Entity
(Obj_Id
) then
879 ("volatile variable & must be declared at library level",
882 -- An object of a discriminated type cannot be effectively
883 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
885 elsif Has_Discriminants
(Obj_Typ
)
886 and then not Is_Protected_Type
(Obj_Typ
)
889 ("discriminated object & cannot be volatile", Obj_Id
);
892 -- The object is not effectively volatile
895 -- A non-effectively volatile object cannot have effectively
896 -- volatile components (SPARK RM 7.1.3(6)).
898 if not Is_Effectively_Volatile
(Obj_Id
)
899 and then Has_Volatile_Component
(Obj_Typ
)
902 ("non-volatile object & cannot have volatile components",
911 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
913 -- A Ghost object cannot be of a type that yields a synchronized
914 -- object (SPARK RM 6.9(19)).
916 if Yields_Synchronized_Object
(Obj_Typ
) then
917 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
919 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
920 -- SPARK RM 6.9(19)).
922 elsif Is_Effectively_Volatile
(Obj_Id
) then
923 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
925 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
926 -- One exception to this is the object that represents the dispatch
927 -- table of a Ghost tagged type, as the symbol needs to be exported.
929 elsif Is_Exported
(Obj_Id
) then
930 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
932 elsif Is_Imported
(Obj_Id
) then
933 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
937 -- Restore the SPARK_Mode of the enclosing context after all delayed
938 -- pragmas have been analyzed.
940 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
941 end Analyze_Object_Contract
;
943 -----------------------------------
944 -- Analyze_Package_Body_Contract --
945 -----------------------------------
947 -- WARNING: This routine manages SPARK regions. Return statements must be
948 -- replaced by gotos which jump to the end of the routine and restore the
951 procedure Analyze_Package_Body_Contract
952 (Body_Id
: Entity_Id
;
953 Freeze_Id
: Entity_Id
:= Empty
)
955 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
956 Items
: constant Node_Id
:= Contract
(Body_Id
);
957 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
959 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
960 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
961 -- Save the SPARK_Mode-related data to restore on exit
966 -- Do not analyze a contract multiple times
968 if Present
(Items
) then
969 if Analyzed
(Items
) then
972 Set_Analyzed
(Items
);
976 -- Due to the timing of contract analysis, delayed pragmas may be
977 -- subject to the wrong SPARK_Mode, usually that of the enclosing
978 -- context. To remedy this, restore the original SPARK_Mode of the
979 -- related package body.
981 Set_SPARK_Mode
(Body_Id
);
983 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
985 -- The analysis of pragma Refined_State detects whether the spec has
986 -- abstract states available for refinement.
988 if Present
(Ref_State
) then
989 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
992 -- Restore the SPARK_Mode of the enclosing context after all delayed
993 -- pragmas have been analyzed.
995 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
997 -- Capture all global references in a generic package body now that the
998 -- contract has been analyzed.
1000 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1001 Save_Global_References_In_Contract
1002 (Templ
=> Original_Node
(Body_Decl
),
1005 end Analyze_Package_Body_Contract
;
1007 ------------------------------
1008 -- Analyze_Package_Contract --
1009 ------------------------------
1011 -- WARNING: This routine manages SPARK regions. Return statements must be
1012 -- replaced by gotos which jump to the end of the routine and restore the
1015 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1016 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1017 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1019 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1020 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1021 -- Save the SPARK_Mode-related data to restore on exit
1023 Init
: Node_Id
:= Empty
;
1024 Init_Cond
: Node_Id
:= Empty
;
1029 -- Do not analyze a contract multiple times
1031 if Present
(Items
) then
1032 if Analyzed
(Items
) then
1035 Set_Analyzed
(Items
);
1039 -- Due to the timing of contract analysis, delayed pragmas may be
1040 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1041 -- context. To remedy this, restore the original SPARK_Mode of the
1044 Set_SPARK_Mode
(Pack_Id
);
1046 if Present
(Items
) then
1048 -- Locate and store pragmas Initial_Condition and Initializes, since
1049 -- their order of analysis matters.
1051 Prag
:= Classifications
(Items
);
1052 while Present
(Prag
) loop
1053 Prag_Nam
:= Pragma_Name
(Prag
);
1055 if Prag_Nam
= Name_Initial_Condition
then
1058 elsif Prag_Nam
= Name_Initializes
then
1062 Prag
:= Next_Pragma
(Prag
);
1065 -- Analyze the initialization-related pragmas. Initializes must come
1066 -- before Initial_Condition due to item dependencies.
1068 if Present
(Init
) then
1069 Analyze_Initializes_In_Decl_Part
(Init
);
1072 if Present
(Init_Cond
) then
1073 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1077 -- Check whether the lack of indicator Part_Of agrees with the placement
1078 -- of the package instantiation with respect to the state space.
1080 if Is_Generic_Instance
(Pack_Id
) then
1081 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1084 Check_Missing_Part_Of
(Pack_Id
);
1088 -- Restore the SPARK_Mode of the enclosing context after all delayed
1089 -- pragmas have been analyzed.
1091 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1093 -- Capture all global references in a generic package now that the
1094 -- contract has been analyzed.
1096 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1097 Save_Global_References_In_Contract
1098 (Templ
=> Original_Node
(Pack_Decl
),
1101 end Analyze_Package_Contract
;
1103 --------------------------------
1104 -- Analyze_Protected_Contract --
1105 --------------------------------
1107 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1108 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1111 -- Do not analyze a contract multiple times
1113 if Present
(Items
) then
1114 if Analyzed
(Items
) then
1117 Set_Analyzed
(Items
);
1120 end Analyze_Protected_Contract
;
1122 -------------------------------------------
1123 -- Analyze_Subprogram_Body_Stub_Contract --
1124 -------------------------------------------
1126 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1127 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1128 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1131 -- A subprogram body stub may act as its own spec or as the completion
1132 -- of a previous declaration. Depending on the context, the contract of
1133 -- the stub may contain two sets of pragmas.
1135 -- The stub is a completion, the applicable pragmas are:
1139 if Present
(Spec_Id
) then
1140 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1142 -- The stub acts as its own spec, the applicable pragmas are:
1151 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1153 end Analyze_Subprogram_Body_Stub_Contract
;
1155 ---------------------------
1156 -- Analyze_Task_Contract --
1157 ---------------------------
1159 -- WARNING: This routine manages SPARK regions. Return statements must be
1160 -- replaced by gotos which jump to the end of the routine and restore the
1163 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1164 Items
: constant Node_Id
:= Contract
(Task_Id
);
1166 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1167 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1168 -- Save the SPARK_Mode-related data to restore on exit
1173 -- Do not analyze a contract multiple times
1175 if Present
(Items
) then
1176 if Analyzed
(Items
) then
1179 Set_Analyzed
(Items
);
1183 -- Due to the timing of contract analysis, delayed pragmas may be
1184 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1185 -- context. To remedy this, restore the original SPARK_Mode of the
1186 -- related task unit.
1188 Set_SPARK_Mode
(Task_Id
);
1190 -- Analyze Global first, as Depends may mention items classified in the
1191 -- global categorization.
1193 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1195 if Present
(Prag
) then
1196 Analyze_Global_In_Decl_Part
(Prag
);
1199 -- Depends must be analyzed after Global in order to see the modes of
1200 -- all global items.
1202 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1204 if Present
(Prag
) then
1205 Analyze_Depends_In_Decl_Part
(Prag
);
1208 -- Restore the SPARK_Mode of the enclosing context after all delayed
1209 -- pragmas have been analyzed.
1211 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1212 end Analyze_Task_Contract
;
1214 -------------------------------------------------
1215 -- Build_And_Analyze_Contract_Only_Subprograms --
1216 -------------------------------------------------
1218 procedure Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
) is
1219 procedure Analyze_Contract_Only_Subprograms
;
1220 -- Analyze the contract-only subprograms of L
1222 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
);
1223 -- Append the contract-only bodies of Subp_List to its declarations list
1225 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
;
1226 -- If E is an entity for a non-imported subprogram specification with
1227 -- pre/postconditions and we are compiling with CodePeer mode, then
1228 -- this procedure will create a wrapper to help Gnat2scil process its
1229 -- contracts. Return Empty if the wrapper cannot be built.
1231 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
;
1232 -- Build the contract-only subprograms of all eligible subprograms found
1235 function Has_Private_Declarations
(N
: Node_Id
) return Boolean;
1236 -- Return True for package specs, task definitions, and protected type
1237 -- definitions whose list of private declarations is not empty.
1239 ---------------------------------------
1240 -- Analyze_Contract_Only_Subprograms --
1241 ---------------------------------------
1243 procedure Analyze_Contract_Only_Subprograms
is
1244 procedure Analyze_Contract_Only_Bodies
;
1245 -- Analyze all the contract-only bodies of L
1247 ----------------------------------
1248 -- Analyze_Contract_Only_Bodies --
1249 ----------------------------------
1251 procedure Analyze_Contract_Only_Bodies
is
1256 while Present
(Decl
) loop
1257 if Nkind
(Decl
) = N_Subprogram_Body
1258 and then Is_Contract_Only_Body
1259 (Defining_Unit_Name
(Specification
(Decl
)))
1266 end Analyze_Contract_Only_Bodies
;
1268 -- Start of processing for Analyze_Contract_Only_Subprograms
1271 if Ekind
(Current_Scope
) /= E_Package
then
1272 Analyze_Contract_Only_Bodies
;
1276 Pkg_Spec
: constant Node_Id
:=
1277 Package_Specification
(Current_Scope
);
1280 if not Has_Private_Declarations
(Pkg_Spec
) then
1281 Analyze_Contract_Only_Bodies
;
1283 -- For packages with private declarations, the contract-only
1284 -- bodies of subprograms defined in the visible part of the
1285 -- package are added to its private declarations (to ensure
1286 -- that they do not cause premature freezing of types and also
1287 -- that they are analyzed with proper visibility). Hence they
1288 -- will be analyzed later.
1290 elsif Visible_Declarations
(Pkg_Spec
) = L
then
1293 elsif Private_Declarations
(Pkg_Spec
) = L
then
1294 Analyze_Contract_Only_Bodies
;
1298 end Analyze_Contract_Only_Subprograms
;
1300 --------------------------------------
1301 -- Append_Contract_Only_Subprograms --
1302 --------------------------------------
1304 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
) is
1306 if No
(Subp_List
) then
1310 if Ekind
(Current_Scope
) /= E_Package
then
1311 Append_List
(Subp_List
, To
=> L
);
1315 Pkg_Spec
: constant Node_Id
:=
1316 Package_Specification
(Current_Scope
);
1319 if not Has_Private_Declarations
(Pkg_Spec
) then
1320 Append_List
(Subp_List
, To
=> L
);
1322 -- If the package has private declarations then append them to
1323 -- its private declarations; they will be analyzed when the
1324 -- contracts of its private declarations are analyzed.
1329 To
=> Private_Declarations
(Pkg_Spec
));
1333 end Append_Contract_Only_Subprograms
;
1335 ------------------------------------
1336 -- Build_Contract_Only_Subprogram --
1337 ------------------------------------
1339 -- This procedure takes care of building a wrapper to generate better
1340 -- analysis results in the case of a call to a subprogram whose body
1341 -- is unavailable to CodePeer but whose specification includes Pre/Post
1342 -- conditions. The body might be unavailable for any of a number or
1343 -- reasons (it is imported, the .adb file is simply missing, or the
1344 -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
1345 -- pragma). The built subprogram has the following contents:
1346 -- * check preconditions
1347 -- * call the subprogram
1348 -- * check postconditions
1350 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
is
1351 Loc
: constant Source_Ptr
:= Sloc
(E
);
1353 Missing_Body_Name
: constant Name_Id
:=
1354 New_External_Name
(Chars
(E
), "__missing_body");
1356 function Build_Missing_Body_Decls
return List_Id
;
1357 -- Build the declaration of the missing body subprogram and its
1358 -- corresponding pragma Import.
1360 function Build_Missing_Body_Subprogram_Call
return Node_Id
;
1361 -- Build the call to the missing body subprogram
1363 function Skip_Contract_Only_Subprogram
(E
: Entity_Id
) return Boolean;
1364 -- Return True for cases where the wrapper is not needed or we cannot
1367 ------------------------------
1368 -- Build_Missing_Body_Decls --
1369 ------------------------------
1371 function Build_Missing_Body_Decls
return List_Id
is
1372 Spec
: constant Node_Id
:= Declaration_Node
(E
);
1378 Make_Subprogram_Declaration
(Loc
, Copy_Subprogram_Spec
(Spec
));
1379 Set_Chars
(Defining_Entity
(Decl
), Missing_Body_Name
);
1383 Chars
=> Name_Import
,
1384 Pragma_Argument_Associations
=> New_List
(
1385 Make_Pragma_Argument_Association
(Loc
,
1386 Expression
=> Make_Identifier
(Loc
, Name_Ada
)),
1388 Make_Pragma_Argument_Association
(Loc
,
1389 Expression
=> Make_Identifier
(Loc
, Missing_Body_Name
))));
1391 return New_List
(Decl
, Prag
);
1392 end Build_Missing_Body_Decls
;
1394 ----------------------------------------
1395 -- Build_Missing_Body_Subprogram_Call --
1396 ----------------------------------------
1398 function Build_Missing_Body_Subprogram_Call
return Node_Id
is
1405 -- Build parameter list that we need
1407 Forml
:= First_Formal
(E
);
1408 while Present
(Forml
) loop
1409 Append_To
(Parms
, Make_Identifier
(Loc
, Chars
(Forml
)));
1410 Next_Formal
(Forml
);
1413 -- Build the call to the missing body subprogram
1415 if Ekind_In
(E
, E_Function
, E_Generic_Function
) then
1417 Make_Simple_Return_Statement
(Loc
,
1419 Make_Function_Call
(Loc
,
1421 Make_Identifier
(Loc
, Missing_Body_Name
),
1422 Parameter_Associations
=> Parms
));
1426 Make_Procedure_Call_Statement
(Loc
,
1428 Make_Identifier
(Loc
, Missing_Body_Name
),
1429 Parameter_Associations
=> Parms
);
1431 end Build_Missing_Body_Subprogram_Call
;
1433 -----------------------------------
1434 -- Skip_Contract_Only_Subprogram --
1435 -----------------------------------
1437 function Skip_Contract_Only_Subprogram
1438 (E
: Entity_Id
) return Boolean
1440 function Depends_On_Enclosing_Private_Type
return Boolean;
1441 -- Return True if some formal of E (or its return type) are
1442 -- private types defined in an enclosing package.
1444 function Some_Enclosing_Package_Has_Private_Decls
return Boolean;
1445 -- Return True if some enclosing package of the current scope has
1446 -- private declarations.
1448 ---------------------------------------
1449 -- Depends_On_Enclosing_Private_Type --
1450 ---------------------------------------
1452 function Depends_On_Enclosing_Private_Type
return Boolean is
1453 function Defined_In_Enclosing_Package
1454 (Typ
: Entity_Id
) return Boolean;
1455 -- Return True if Typ is an entity defined in an enclosing
1456 -- package of the current scope.
1458 ----------------------------------
1459 -- Defined_In_Enclosing_Package --
1460 ----------------------------------
1462 function Defined_In_Enclosing_Package
1463 (Typ
: Entity_Id
) return Boolean
1465 Scop
: Entity_Id
:= Scope
(Current_Scope
);
1468 while Scop
/= Scope
(Typ
)
1469 and then not Is_Compilation_Unit
(Scop
)
1471 Scop
:= Scope
(Scop
);
1474 return Scop
= Scope
(Typ
);
1475 end Defined_In_Enclosing_Package
;
1479 Param_E
: Entity_Id
;
1482 -- Start of processing for Depends_On_Enclosing_Private_Type
1485 Param_E
:= First_Entity
(E
);
1486 while Present
(Param_E
) loop
1487 Typ
:= Etype
(Param_E
);
1489 if Is_Private_Type
(Typ
)
1490 and then Defined_In_Enclosing_Package
(Typ
)
1495 Next_Entity
(Param_E
);
1499 Ekind
(E
) = E_Function
1500 and then Is_Private_Type
(Etype
(E
))
1501 and then Defined_In_Enclosing_Package
(Etype
(E
));
1502 end Depends_On_Enclosing_Private_Type
;
1504 ----------------------------------------------
1505 -- Some_Enclosing_Package_Has_Private_Decls --
1506 ----------------------------------------------
1508 function Some_Enclosing_Package_Has_Private_Decls
return Boolean is
1509 Scop
: Entity_Id
:= Current_Scope
;
1510 Pkg_Spec
: Node_Id
:= Package_Specification
(Scop
);
1514 if Ekind
(Scop
) = E_Package
1515 and then Has_Private_Declarations
1516 (Package_Specification
(Scop
))
1518 Pkg_Spec
:= Package_Specification
(Scop
);
1521 exit when Is_Compilation_Unit
(Scop
);
1522 Scop
:= Scope
(Scop
);
1525 return Pkg_Spec
/= Package_Specification
(Current_Scope
);
1526 end Some_Enclosing_Package_Has_Private_Decls
;
1528 -- Start of processing for Skip_Contract_Only_Subprogram
1531 if not CodePeer_Mode
1532 or else Inside_A_Generic
1533 or else not Is_Subprogram
(E
)
1534 or else Is_Abstract_Subprogram
(E
)
1535 or else Is_Imported
(E
)
1536 or else No
(Contract
(E
))
1537 or else No
(Pre_Post_Conditions
(Contract
(E
)))
1538 or else Is_Contract_Only_Body
(E
)
1539 or else Convention
(E
) = Convention_Protected
1543 -- We do not support building the contract-only subprogram if E
1544 -- is a subprogram declared in a nested package that has some
1545 -- formal or return type depending on a private type defined in
1546 -- an enclosing package.
1548 elsif Ekind
(Current_Scope
) = E_Package
1549 and then Some_Enclosing_Package_Has_Private_Decls
1550 and then Depends_On_Enclosing_Private_Type
1552 if Debug_Flag_Dot_KK
then
1554 Saved_Mode
: constant Warning_Mode_Type
:= Warning_Mode
;
1557 -- Warnings are disabled by default under CodePeer_Mode
1558 -- (see switch-c). Enable them temporarily.
1560 Warning_Mode
:= Normal
;
1562 ("cannot generate contract-only subprogram?", E
);
1563 Warning_Mode
:= Saved_Mode
;
1571 end Skip_Contract_Only_Subprogram
;
1573 -- Start of processing for Build_Contract_Only_Subprogram
1576 -- Test cases where the wrapper is not needed and cases where we
1579 if Skip_Contract_Only_Subprogram
(E
) then
1583 -- Note on calls to Copy_Separate_Tree. The trees we are copying
1584 -- here are fully analyzed, but we definitely want fully syntactic
1585 -- unanalyzed trees in the body we construct, so that the analysis
1586 -- generates the right visibility, and that is exactly what the
1587 -- calls to Copy_Separate_Tree give us.
1590 Name
: constant Name_Id
:=
1591 New_External_Name
(Chars
(E
), "__contract_only");
1597 Make_Subprogram_Body
(Loc
,
1599 Copy_Subprogram_Spec
(Declaration_Node
(E
)),
1601 Build_Missing_Body_Decls
,
1602 Handled_Statement_Sequence
=>
1603 Make_Handled_Sequence_Of_Statements
(Loc
,
1604 Statements
=> New_List
(
1605 Build_Missing_Body_Subprogram_Call
),
1606 End_Label
=> Make_Identifier
(Loc
, Name
)));
1608 Id
:= Defining_Unit_Name
(Specification
(Bod
));
1610 -- Copy only the pre/postconditions of the original contract
1611 -- since it is what we need, but also because pragmas stored in
1612 -- the other fields have N_Pragmas with N_Aspect_Specifications
1613 -- that reference their associated pragma (thus causing an endless
1614 -- loop when trying to copy the subtree).
1617 New_Contract
: constant Node_Id
:= Make_Contract
(Sloc
(E
));
1620 Set_Pre_Post_Conditions
(New_Contract
,
1621 Copy_Separate_Tree
(Pre_Post_Conditions
(Contract
(E
))));
1622 Set_Contract
(Id
, New_Contract
);
1625 -- Fix the name of this new subprogram and link the original
1626 -- subprogram with its Contract_Only_Body subprogram.
1628 Set_Chars
(Id
, Name
);
1629 Set_Is_Contract_Only_Body
(Id
);
1630 Set_Contract_Only_Body
(E
, Id
);
1634 end Build_Contract_Only_Subprogram
;
1636 -------------------------------------
1637 -- Build_Contract_Only_Subprograms --
1638 -------------------------------------
1640 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
is
1643 Result
: List_Id
:= No_List
;
1644 Subp_Id
: Entity_Id
;
1648 while Present
(Decl
) loop
1649 if Nkind
(Decl
) = N_Subprogram_Declaration
then
1650 Subp_Id
:= Defining_Unit_Name
(Specification
(Decl
));
1651 New_Subp
:= Build_Contract_Only_Subprogram
(Subp_Id
);
1653 if Present
(New_Subp
) then
1658 Append_To
(Result
, New_Subp
);
1666 end Build_Contract_Only_Subprograms
;
1668 ------------------------------
1669 -- Has_Private_Declarations --
1670 ------------------------------
1672 function Has_Private_Declarations
(N
: Node_Id
) return Boolean is
1674 if not Nkind_In
(N
, N_Package_Specification
,
1675 N_Protected_Definition
,
1681 Present
(Private_Declarations
(N
))
1682 and then Is_Non_Empty_List
(Private_Declarations
(N
));
1684 end Has_Private_Declarations
;
1688 Subp_List
: List_Id
;
1690 -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
1693 Subp_List
:= Build_Contract_Only_Subprograms
(L
);
1694 Append_Contract_Only_Subprograms
(Subp_List
);
1695 Analyze_Contract_Only_Subprograms
;
1696 end Build_And_Analyze_Contract_Only_Subprograms
;
1698 -----------------------------
1699 -- Create_Generic_Contract --
1700 -----------------------------
1702 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
1703 Templ
: constant Node_Id
:= Original_Node
(Unit
);
1704 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
1706 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
1707 -- Add a single contract-related source pragma Prag to the contract of
1708 -- generic template Templ_Id.
1710 ---------------------------------
1711 -- Add_Generic_Contract_Pragma --
1712 ---------------------------------
1714 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
1715 Prag_Templ
: Node_Id
;
1718 -- Mark the pragma to prevent the premature capture of global
1719 -- references when capturing global references of the context
1720 -- (see Save_References_In_Pragma).
1722 Set_Is_Generic_Contract_Pragma
(Prag
);
1724 -- Pragmas that apply to a generic subprogram declaration are not
1725 -- part of the semantic structure of the generic template:
1728 -- procedure Example (Formal : Integer);
1729 -- pragma Precondition (Formal > 0);
1731 -- Create a generic template for such pragmas and link the template
1732 -- of the pragma with the generic template.
1734 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1736 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
1737 Prag_Templ
:= Original_Node
(Prag
);
1739 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
1740 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
1742 -- Otherwise link the pragma with the generic template
1745 Add_Contract_Item
(Prag
, Templ_Id
);
1747 end Add_Generic_Contract_Pragma
;
1751 Context
: constant Node_Id
:= Parent
(Unit
);
1752 Decl
: Node_Id
:= Empty
;
1754 -- Start of processing for Create_Generic_Contract
1757 -- A generic package declaration carries contract-related source pragmas
1758 -- in its visible declarations.
1760 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
1761 Set_Ekind
(Templ_Id
, E_Generic_Package
);
1763 if Present
(Visible_Declarations
(Specification
(Templ
))) then
1764 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
1767 -- A generic package body carries contract-related source pragmas in its
1770 elsif Nkind
(Templ
) = N_Package_Body
then
1771 Set_Ekind
(Templ_Id
, E_Package_Body
);
1773 if Present
(Declarations
(Templ
)) then
1774 Decl
:= First
(Declarations
(Templ
));
1777 -- Generic subprogram declaration
1779 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1780 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
1781 Set_Ekind
(Templ_Id
, E_Generic_Function
);
1783 Set_Ekind
(Templ_Id
, E_Generic_Procedure
);
1786 -- When the generic subprogram acts as a compilation unit, inspect
1787 -- the Pragmas_After list for contract-related source pragmas.
1789 if Nkind
(Context
) = N_Compilation_Unit
then
1790 if Present
(Aux_Decls_Node
(Context
))
1791 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
1793 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
1796 -- Otherwise inspect the successive declarations for contract-related
1800 Decl
:= Next
(Unit
);
1803 -- A generic subprogram body carries contract-related source pragmas in
1804 -- its declarations.
1806 elsif Nkind
(Templ
) = N_Subprogram_Body
then
1807 Set_Ekind
(Templ_Id
, E_Subprogram_Body
);
1809 if Present
(Declarations
(Templ
)) then
1810 Decl
:= First
(Declarations
(Templ
));
1814 -- Inspect the relevant declarations looking for contract-related source
1815 -- pragmas and add them to the contract of the generic unit.
1817 while Present
(Decl
) loop
1818 if Comes_From_Source
(Decl
) then
1819 if Nkind
(Decl
) = N_Pragma
then
1821 -- The source pragma is a contract annotation
1823 if Is_Contract_Annotation
(Decl
) then
1824 Add_Generic_Contract_Pragma
(Decl
);
1827 -- The region where a contract-related source pragma may appear
1828 -- ends with the first source non-pragma declaration or statement.
1837 end Create_Generic_Contract
;
1839 --------------------------------
1840 -- Expand_Subprogram_Contract --
1841 --------------------------------
1843 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
1844 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1845 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1847 procedure Add_Invariant_And_Predicate_Checks
1848 (Subp_Id
: Entity_Id
;
1849 Stmts
: in out List_Id
;
1850 Result
: out Node_Id
);
1851 -- Process the result of function Subp_Id (if applicable) and all its
1852 -- formals. Add invariant and predicate checks where applicable. The
1853 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1854 -- function, Result contains the entity of parameter _Result, to be
1855 -- used in the creation of procedure _Postconditions.
1857 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
1858 -- Append a node to a list. If there is no list, create a new one. When
1859 -- the item denotes a pragma, it is added to the list only when it is
1862 procedure Build_Postconditions_Procedure
1863 (Subp_Id
: Entity_Id
;
1865 Result
: Entity_Id
);
1866 -- Create the body of procedure _Postconditions which handles various
1867 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1868 -- of statements to be checked on exit. Parameter Result is the entity
1869 -- of parameter _Result when Subp_Id denotes a function.
1871 procedure Process_Contract_Cases
(Stmts
: in out List_Id
);
1872 -- Process pragma Contract_Cases. This routine prepends items to the
1873 -- body declarations and appends items to list Stmts.
1875 procedure Process_Postconditions
(Stmts
: in out List_Id
);
1876 -- Collect all [inherited] spec and body postconditions and accumulate
1877 -- their pragma Check equivalents in list Stmts.
1879 procedure Process_Preconditions
;
1880 -- Collect all [inherited] spec and body preconditions and prepend their
1881 -- pragma Check equivalents to the declarations of the body.
1883 ----------------------------------------
1884 -- Add_Invariant_And_Predicate_Checks --
1885 ----------------------------------------
1887 procedure Add_Invariant_And_Predicate_Checks
1888 (Subp_Id
: Entity_Id
;
1889 Stmts
: in out List_Id
;
1890 Result
: out Node_Id
)
1892 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
1893 -- Id denotes the return value of a function or a formal parameter.
1894 -- Add an invariant check if the type of Id is access to a type with
1895 -- invariants. The routine appends the generated code to Stmts.
1897 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
1898 -- Determine whether type Typ can benefit from invariant checks. To
1899 -- qualify, the type must have a non-null invariant procedure and
1900 -- subprogram Subp_Id must appear visible from the point of view of
1903 ---------------------------------
1904 -- Add_Invariant_Access_Checks --
1905 ---------------------------------
1907 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
1908 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
1915 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
1916 Typ
:= Designated_Type
(Typ
);
1918 if Invariant_Checks_OK
(Typ
) then
1920 Make_Explicit_Dereference
(Loc
,
1921 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
1922 Set_Etype
(Ref
, Typ
);
1925 -- if <Id> /= null then
1926 -- <invariant_call (<Ref>)>
1931 Make_If_Statement
(Loc
,
1934 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
1935 Right_Opnd
=> Make_Null
(Loc
)),
1936 Then_Statements
=> New_List
(
1937 Make_Invariant_Call
(Ref
))),
1941 end Add_Invariant_Access_Checks
;
1943 -------------------------
1944 -- Invariant_Checks_OK --
1945 -------------------------
1947 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
1948 function Has_Public_Visibility_Of_Subprogram
return Boolean;
1949 -- Determine whether type Typ has public visibility of subprogram
1952 -----------------------------------------
1953 -- Has_Public_Visibility_Of_Subprogram --
1954 -----------------------------------------
1956 function Has_Public_Visibility_Of_Subprogram
return Boolean is
1957 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
1960 -- An Initialization procedure must be considered visible even
1961 -- though it is internally generated.
1963 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
1966 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
1969 -- Internally generated code is never publicly visible except
1970 -- for a subprogram that is the implementation of an expression
1971 -- function. In that case the visibility is determined by the
1974 elsif not Comes_From_Source
(Subp_Decl
)
1976 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
1978 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
1982 -- Determine whether the subprogram is declared in the visible
1983 -- declarations of the package containing the type, or in the
1984 -- visible declaration of a child unit of that package.
1988 Decls
: constant List_Id
:=
1989 List_Containing
(Subp_Decl
);
1990 Subp_Scope
: constant Entity_Id
:=
1991 Scope
(Defining_Entity
(Subp_Decl
));
1992 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
1996 Decls
= Visible_Declarations
1997 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2000 (Ekind
(Subp_Scope
) = E_Package
2001 and then Typ_Scope
/= Subp_Scope
2002 and then Is_Child_Unit
(Subp_Scope
)
2004 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2006 Decls
= Visible_Declarations
2008 (Unit_Declaration_Node
(Subp_Scope
))));
2011 end Has_Public_Visibility_Of_Subprogram
;
2013 -- Start of processing for Invariant_Checks_OK
2017 Has_Invariants
(Typ
)
2018 and then Present
(Invariant_Procedure
(Typ
))
2019 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2020 and then Has_Public_Visibility_Of_Subprogram
;
2021 end Invariant_Checks_OK
;
2025 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2026 -- Source location of subprogram body contract
2031 -- Start of processing for Add_Invariant_And_Predicate_Checks
2036 -- Process the result of a function
2038 if Ekind
(Subp_Id
) = E_Function
then
2039 Typ
:= Etype
(Subp_Id
);
2041 -- Generate _Result which is used in procedure _Postconditions to
2042 -- verify the return value.
2044 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2045 Set_Etype
(Result
, Typ
);
2047 -- Add an invariant check when the return type has invariants and
2048 -- the related function is visible to the outside.
2050 if Invariant_Checks_OK
(Typ
) then
2053 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2057 -- Add an invariant check when the return type is an access to a
2058 -- type with invariants.
2060 Add_Invariant_Access_Checks
(Result
);
2063 -- Add invariant and predicates for all formals that qualify
2065 Formal
:= First_Formal
(Subp_Id
);
2066 while Present
(Formal
) loop
2067 Typ
:= Etype
(Formal
);
2069 if Ekind
(Formal
) /= E_In_Parameter
2070 or else Is_Access_Type
(Typ
)
2072 if Invariant_Checks_OK
(Typ
) then
2075 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2079 Add_Invariant_Access_Checks
(Formal
);
2081 -- Note: we used to add predicate checks for OUT and IN OUT
2082 -- formals here, but that was misguided, since such checks are
2083 -- performed on the caller side, based on the predicate of the
2084 -- actual, rather than the predicate of the formal.
2088 Next_Formal
(Formal
);
2090 end Add_Invariant_And_Predicate_Checks
;
2092 -------------------------
2093 -- Append_Enabled_Item --
2094 -------------------------
2096 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2098 -- Do not chain ignored or disabled pragmas
2100 if Nkind
(Item
) = N_Pragma
2101 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2105 -- Otherwise, add the item
2112 -- If the pragma is a conjunct in a composite postcondition, it
2113 -- has been processed in reverse order. In the postcondition body
2114 -- it must appear before the others.
2116 if Nkind
(Item
) = N_Pragma
2117 and then From_Aspect_Specification
(Item
)
2118 and then Split_PPC
(Item
)
2120 Prepend
(Item
, List
);
2122 Append
(Item
, List
);
2125 end Append_Enabled_Item
;
2127 ------------------------------------
2128 -- Build_Postconditions_Procedure --
2129 ------------------------------------
2131 procedure Build_Postconditions_Procedure
2132 (Subp_Id
: Entity_Id
;
2136 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
);
2137 -- Insert node Stmt before the first source declaration of the
2138 -- related subprogram's body. If no such declaration exists, Stmt
2139 -- becomes the last declaration.
2141 --------------------------------------------
2142 -- Insert_Before_First_Source_Declaration --
2143 --------------------------------------------
2145 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
) is
2146 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2150 -- Inspect the declarations of the related subprogram body looking
2151 -- for the first source declaration.
2153 if Present
(Decls
) then
2154 Decl
:= First
(Decls
);
2155 while Present
(Decl
) loop
2156 if Comes_From_Source
(Decl
) then
2157 Insert_Before
(Decl
, Stmt
);
2164 -- If we get there, then the subprogram body lacks any source
2165 -- declarations. The body of _Postconditions now acts as the
2166 -- last declaration.
2168 Append
(Stmt
, Decls
);
2170 -- Ensure that the body has a declaration list
2173 Set_Declarations
(Body_Decl
, New_List
(Stmt
));
2175 end Insert_Before_First_Source_Declaration
;
2179 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2180 Params
: List_Id
:= No_List
;
2182 Proc_Decl
: Node_Id
;
2183 Proc_Id
: Entity_Id
;
2184 Proc_Spec
: Node_Id
;
2186 -- Start of processing for Build_Postconditions_Procedure
2189 -- Nothing to do if there are no actions to check on exit
2195 Proc_Id
:= Make_Defining_Identifier
(Loc
, Name_uPostconditions
);
2196 Set_Debug_Info_Needed
(Proc_Id
);
2197 Set_Postconditions_Proc
(Subp_Id
, Proc_Id
);
2199 -- Force the front-end inlining of _Postconditions when generating C
2200 -- code, since its body may have references to itypes defined in the
2201 -- enclosing subprogram, which would cause problems for unnesting
2202 -- routines in the absence of inlining.
2204 if Modify_Tree_For_C
then
2205 Set_Has_Pragma_Inline
(Proc_Id
);
2206 Set_Has_Pragma_Inline_Always
(Proc_Id
);
2207 Set_Is_Inlined
(Proc_Id
);
2210 -- The related subprogram is a function: create the specification of
2211 -- parameter _Result.
2213 if Present
(Result
) then
2214 Params
:= New_List
(
2215 Make_Parameter_Specification
(Loc
,
2216 Defining_Identifier
=> Result
,
2218 New_Occurrence_Of
(Etype
(Result
), Loc
)));
2222 Make_Procedure_Specification
(Loc
,
2223 Defining_Unit_Name
=> Proc_Id
,
2224 Parameter_Specifications
=> Params
);
2226 Proc_Decl
:= Make_Subprogram_Declaration
(Loc
, Proc_Spec
);
2228 -- Insert _Postconditions before the first source declaration of the
2229 -- body. This ensures that the body will not cause any premature
2230 -- freezing, as it may mention types:
2232 -- procedure Proc (Obj : Array_Typ) is
2233 -- procedure _postconditions is
2236 -- end _postconditions;
2238 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
2241 -- In the example above, Obj is of type T but the incorrect placement
2242 -- of _Postconditions will cause a crash in gigi due to an out-of-
2243 -- order reference. The body of _Postconditions must be placed after
2244 -- the declaration of Temp to preserve correct visibility.
2246 Insert_Before_First_Source_Declaration
(Proc_Decl
);
2247 Analyze
(Proc_Decl
);
2249 -- Set an explicit End_Label to override the sloc of the implicit
2250 -- RETURN statement, and prevent it from inheriting the sloc of one
2251 -- the postconditions: this would cause confusing debug info to be
2252 -- produced, interfering with coverage-analysis tools.
2255 Make_Subprogram_Body
(Loc
,
2257 Copy_Subprogram_Spec
(Proc_Spec
),
2258 Declarations
=> Empty_List
,
2259 Handled_Statement_Sequence
=>
2260 Make_Handled_Sequence_Of_Statements
(Loc
,
2261 Statements
=> Stmts
,
2262 End_Label
=> Make_Identifier
(Loc
, Chars
(Proc_Id
))));
2264 Insert_After_And_Analyze
(Proc_Decl
, Proc_Bod
);
2265 end Build_Postconditions_Procedure
;
2267 ----------------------------
2268 -- Process_Contract_Cases --
2269 ----------------------------
2271 procedure Process_Contract_Cases
(Stmts
: in out List_Id
) is
2272 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2273 -- Process pragma Contract_Cases for subprogram Subp_Id
2275 --------------------------------
2276 -- Process_Contract_Cases_For --
2277 --------------------------------
2279 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2280 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2284 if Present
(Items
) then
2285 Prag
:= Contract_Test_Cases
(Items
);
2286 while Present
(Prag
) loop
2287 if Pragma_Name
(Prag
) = Name_Contract_Cases
2288 and then Is_Checked
(Prag
)
2290 Expand_Pragma_Contract_Cases
2293 Decls
=> Declarations
(Body_Decl
),
2297 Prag
:= Next_Pragma
(Prag
);
2300 end Process_Contract_Cases_For
;
2302 pragma Unmodified
(Stmts
);
2303 -- Stmts is passed as IN OUT to signal that the list can be updated,
2304 -- even if the corresponding integer value representing the list does
2307 -- Start of processing for Process_Contract_Cases
2310 Process_Contract_Cases_For
(Body_Id
);
2312 if Present
(Spec_Id
) then
2313 Process_Contract_Cases_For
(Spec_Id
);
2315 end Process_Contract_Cases
;
2317 ----------------------------
2318 -- Process_Postconditions --
2319 ----------------------------
2321 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2322 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2323 -- Collect all [refined] postconditions of a specific kind denoted
2324 -- by Post_Nam that belong to the body, and generate pragma Check
2325 -- equivalents in list Stmts.
2327 procedure Process_Spec_Postconditions
;
2328 -- Collect all [inherited] postconditions of the spec, and generate
2329 -- pragma Check equivalents in list Stmts.
2331 ---------------------------------
2332 -- Process_Body_Postconditions --
2333 ---------------------------------
2335 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2336 Items
: constant Node_Id
:= Contract
(Body_Id
);
2337 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2342 -- Process the contract
2344 if Present
(Items
) then
2345 Prag
:= Pre_Post_Conditions
(Items
);
2346 while Present
(Prag
) loop
2347 if Pragma_Name
(Prag
) = Post_Nam
2348 and then Is_Checked
(Prag
)
2351 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2355 Prag
:= Next_Pragma
(Prag
);
2359 -- The subprogram body being processed is actually the proper body
2360 -- of a stub with a corresponding spec. The subprogram stub may
2361 -- carry a postcondition pragma, in which case it must be taken
2362 -- into account. The pragma appears after the stub.
2364 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2365 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2366 while Present
(Decl
) loop
2368 -- Note that non-matching pragmas are skipped
2370 if Nkind
(Decl
) = N_Pragma
then
2371 if Pragma_Name
(Decl
) = Post_Nam
2372 and then Is_Checked
(Decl
)
2375 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2379 -- Skip internally generated code
2381 elsif not Comes_From_Source
(Decl
) then
2384 -- Postcondition pragmas are usually grouped together. There
2385 -- is no need to inspect the whole declarative list.
2394 end Process_Body_Postconditions
;
2396 ---------------------------------
2397 -- Process_Spec_Postconditions --
2398 ---------------------------------
2400 procedure Process_Spec_Postconditions
is
2401 Subps
: constant Subprogram_List
:=
2402 Inherited_Subprograms
(Spec_Id
);
2406 Subp_Id
: Entity_Id
;
2409 -- Process the contract
2411 Items
:= Contract
(Spec_Id
);
2413 if Present
(Items
) then
2414 Prag
:= Pre_Post_Conditions
(Items
);
2415 while Present
(Prag
) loop
2416 if Pragma_Name
(Prag
) = Name_Postcondition
2417 and then Is_Checked
(Prag
)
2420 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2424 Prag
:= Next_Pragma
(Prag
);
2428 -- Process the contracts of all inherited subprograms, looking for
2429 -- class-wide postconditions.
2431 for Index
in Subps
'Range loop
2432 Subp_Id
:= Subps
(Index
);
2433 Items
:= Contract
(Subp_Id
);
2435 if Present
(Items
) then
2436 Prag
:= Pre_Post_Conditions
(Items
);
2437 while Present
(Prag
) loop
2438 if Pragma_Name
(Prag
) = Name_Postcondition
2439 and then Class_Present
(Prag
)
2442 Build_Pragma_Check_Equivalent
2445 Inher_Id
=> Subp_Id
);
2447 -- The pragma Check equivalent of the class-wide
2448 -- postcondition is still created even though the
2449 -- pragma may be ignored because the equivalent
2450 -- performs semantic checks.
2452 if Is_Checked
(Prag
) then
2453 Append_Enabled_Item
(Item
, Stmts
);
2457 Prag
:= Next_Pragma
(Prag
);
2461 end Process_Spec_Postconditions
;
2463 pragma Unmodified
(Stmts
);
2464 -- Stmts is passed as IN OUT to signal that the list can be updated,
2465 -- even if the corresponding integer value representing the list does
2468 -- Start of processing for Process_Postconditions
2471 -- The processing of postconditions is done in reverse order (body
2472 -- first) to ensure the following arrangement:
2474 -- <refined postconditions from body>
2475 -- <postconditions from body>
2476 -- <postconditions from spec>
2477 -- <inherited postconditions>
2479 Process_Body_Postconditions
(Name_Refined_Post
);
2480 Process_Body_Postconditions
(Name_Postcondition
);
2482 if Present
(Spec_Id
) then
2483 Process_Spec_Postconditions
;
2485 end Process_Postconditions
;
2487 ---------------------------
2488 -- Process_Preconditions --
2489 ---------------------------
2491 procedure Process_Preconditions
is
2492 Class_Pre
: Node_Id
:= Empty
;
2493 -- The sole [inherited] class-wide precondition pragma that applies
2494 -- to the subprogram.
2496 Insert_Node
: Node_Id
:= Empty
;
2497 -- The insertion node after which all pragma Check equivalents are
2500 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean;
2501 -- Determine whether arbitrary declaration Decl denotes a renaming of
2502 -- a discriminant or protection field _object.
2504 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
);
2505 -- Merge two class-wide preconditions by "or else"-ing them. The
2506 -- changes are accumulated in parameter Into. Update the error
2509 procedure Prepend_To_Decls
(Item
: Node_Id
);
2510 -- Prepend a single item to the declarations of the subprogram body
2512 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
);
2513 -- Save a class-wide precondition into Class_Pre, or prepend a normal
2514 -- precondition to the declarations of the body and analyze it.
2516 procedure Process_Inherited_Preconditions
;
2517 -- Collect all inherited class-wide preconditions and merge them into
2518 -- one big precondition to be evaluated as pragma Check.
2520 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
2521 -- Collect all preconditions of subprogram Subp_Id and prepend their
2522 -- pragma Check equivalents to the declarations of the body.
2524 --------------------------
2525 -- Is_Prologue_Renaming --
2526 --------------------------
2528 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
2535 if Nkind
(Decl
) = N_Object_Renaming_Declaration
then
2536 Obj
:= Defining_Entity
(Decl
);
2539 if Nkind
(Nam
) = N_Selected_Component
then
2540 Pref
:= Prefix
(Nam
);
2541 Sel
:= Selector_Name
(Nam
);
2543 -- A discriminant renaming appears as
2544 -- Discr : constant ... := Prefix.Discr;
2546 if Ekind
(Obj
) = E_Constant
2547 and then Is_Entity_Name
(Sel
)
2548 and then Present
(Entity
(Sel
))
2549 and then Ekind
(Entity
(Sel
)) = E_Discriminant
2553 -- A protection field renaming appears as
2554 -- Prot : ... := _object._object;
2556 -- A renamed private component is just a component of
2557 -- _object, with an arbitrary name.
2559 elsif Ekind
(Obj
) = E_Variable
2560 and then Nkind
(Pref
) = N_Identifier
2561 and then Chars
(Pref
) = Name_uObject
2562 and then Nkind
(Sel
) = N_Identifier
2570 end Is_Prologue_Renaming
;
2572 -------------------------
2573 -- Merge_Preconditions --
2574 -------------------------
2576 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
) is
2577 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
;
2578 -- Return the boolean expression argument of a precondition while
2579 -- updating its parentheses count for the subsequent merge.
2581 function Message_Arg
(Prag
: Node_Id
) return Node_Id
;
2582 -- Return the message argument of a precondition
2584 --------------------
2585 -- Expression_Arg --
2586 --------------------
2588 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
is
2589 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2590 Arg
: constant Node_Id
:= Get_Pragma_Arg
(Next
(First
(Args
)));
2593 if Paren_Count
(Arg
) = 0 then
2594 Set_Paren_Count
(Arg
, 1);
2604 function Message_Arg
(Prag
: Node_Id
) return Node_Id
is
2605 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2607 return Get_Pragma_Arg
(Last
(Args
));
2612 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
2613 From_Msg
: constant Node_Id
:= Message_Arg
(From
);
2614 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
2615 Into_Msg
: constant Node_Id
:= Message_Arg
(Into
);
2616 Loc
: constant Source_Ptr
:= Sloc
(Into
);
2618 -- Start of processing for Merge_Preconditions
2621 -- Merge the two preconditions by "or else"-ing them
2625 Right_Opnd
=> Relocate_Node
(Into_Expr
),
2626 Left_Opnd
=> From_Expr
));
2628 -- Merge the two error messages to produce a single message of the
2631 -- failed precondition from ...
2632 -- also failed inherited precondition from ...
2634 if not Exception_Locations_Suppressed
then
2635 Start_String
(Strval
(Into_Msg
));
2636 Store_String_Char
(ASCII
.LF
);
2637 Store_String_Chars
(" also ");
2638 Store_String_Chars
(Strval
(From_Msg
));
2640 Set_Strval
(Into_Msg
, End_String
);
2642 end Merge_Preconditions
;
2644 ----------------------
2645 -- Prepend_To_Decls --
2646 ----------------------
2648 procedure Prepend_To_Decls
(Item
: Node_Id
) is
2652 Decls
:= Declarations
(Body_Decl
);
2654 -- Ensure that the body has a declarative list
2658 Set_Declarations
(Body_Decl
, Decls
);
2661 Prepend_To
(Decls
, Item
);
2662 end Prepend_To_Decls
;
2664 ------------------------------
2665 -- Prepend_To_Decls_Or_Save --
2666 ------------------------------
2668 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
) is
2669 Check_Prag
: Node_Id
;
2672 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
2674 -- Save the sole class-wide precondition (if any) for the next
2675 -- step, where it will be merged with inherited preconditions.
2677 if Class_Present
(Prag
) then
2678 pragma Assert
(No
(Class_Pre
));
2679 Class_Pre
:= Check_Prag
;
2681 -- Accumulate the corresponding Check pragmas at the top of the
2682 -- declarations. Prepending the items ensures that they will be
2683 -- evaluated in their original order.
2686 if Present
(Insert_Node
) then
2687 Insert_After
(Insert_Node
, Check_Prag
);
2689 Prepend_To_Decls
(Check_Prag
);
2692 Analyze
(Check_Prag
);
2694 end Prepend_To_Decls_Or_Save
;
2696 -------------------------------------
2697 -- Process_Inherited_Preconditions --
2698 -------------------------------------
2700 procedure Process_Inherited_Preconditions
is
2701 Subps
: constant Subprogram_List
:=
2702 Inherited_Subprograms
(Spec_Id
);
2707 Subp_Id
: Entity_Id
;
2710 -- Process the contracts of all inherited subprograms, looking for
2711 -- class-wide preconditions.
2713 for Index
in Subps
'Range loop
2714 Subp_Id
:= Subps
(Index
);
2715 Items
:= Contract
(Subp_Id
);
2717 if Present
(Items
) then
2718 Prag
:= Pre_Post_Conditions
(Items
);
2719 while Present
(Prag
) loop
2720 if Pragma_Name
(Prag
) = Name_Precondition
2721 and then Class_Present
(Prag
)
2724 Build_Pragma_Check_Equivalent
2727 Inher_Id
=> Subp_Id
);
2729 -- The pragma Check equivalent of the class-wide
2730 -- precondition is still created even though the
2731 -- pragma may be ignored because the equivalent
2732 -- performs semantic checks.
2734 if Is_Checked
(Prag
) then
2736 -- The spec of an inherited subprogram already
2737 -- yielded a class-wide precondition. Merge the
2738 -- existing precondition with the current one
2741 if Present
(Class_Pre
) then
2742 Merge_Preconditions
(Item
, Class_Pre
);
2749 Prag
:= Next_Pragma
(Prag
);
2754 -- Add the merged class-wide preconditions
2756 if Present
(Class_Pre
) then
2757 Prepend_To_Decls
(Class_Pre
);
2758 Analyze
(Class_Pre
);
2760 end Process_Inherited_Preconditions
;
2762 -------------------------------
2763 -- Process_Preconditions_For --
2764 -------------------------------
2766 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
2767 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2771 Subp_Decl
: Node_Id
;
2774 -- Process the contract
2776 if Present
(Items
) then
2777 Prag
:= Pre_Post_Conditions
(Items
);
2778 while Present
(Prag
) loop
2779 if Pragma_Name
(Prag
) = Name_Precondition
2780 and then Is_Checked
(Prag
)
2782 Prepend_To_Decls_Or_Save
(Prag
);
2785 Prag
:= Next_Pragma
(Prag
);
2789 -- The subprogram declaration being processed is actually a body
2790 -- stub. The stub may carry a precondition pragma, in which case
2791 -- it must be taken into account. The pragma appears after the
2794 Subp_Decl
:= Unit_Declaration_Node
(Subp_Id
);
2796 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
2798 -- Inspect the declarations following the body stub
2800 Decl
:= Next
(Subp_Decl
);
2801 while Present
(Decl
) loop
2803 -- Note that non-matching pragmas are skipped
2805 if Nkind
(Decl
) = N_Pragma
then
2806 if Pragma_Name
(Decl
) = Name_Precondition
2807 and then Is_Checked
(Decl
)
2809 Prepend_To_Decls_Or_Save
(Decl
);
2812 -- Skip internally generated code
2814 elsif not Comes_From_Source
(Decl
) then
2817 -- Preconditions are usually grouped together. There is no
2818 -- need to inspect the whole declarative list.
2827 end Process_Preconditions_For
;
2831 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2834 -- Start of processing for Process_Preconditions
2837 -- Find the proper insertion point for all pragma Check equivalents
2839 if Present
(Decls
) then
2840 Decl
:= First
(Decls
);
2841 while Present
(Decl
) loop
2843 -- First source declaration terminates the search, because all
2844 -- preconditions must be evaluated prior to it, by definition.
2846 if Comes_From_Source
(Decl
) then
2849 -- Certain internally generated object renamings such as those
2850 -- for discriminants and protection fields must be elaborated
2851 -- before the preconditions are evaluated, as their expressions
2852 -- may mention the discriminants. The renamings include those
2853 -- for private components so we need to find the last such.
2855 elsif Is_Prologue_Renaming
(Decl
) then
2856 while Present
(Next
(Decl
))
2857 and then Is_Prologue_Renaming
(Next
(Decl
))
2862 Insert_Node
:= Decl
;
2864 -- Otherwise the declaration does not come from source. This
2865 -- also terminates the search, because internal code may raise
2866 -- exceptions which should not preempt the preconditions.
2876 -- The processing of preconditions is done in reverse order (body
2877 -- first), because each pragma Check equivalent is inserted at the
2878 -- top of the declarations. This ensures that the final order is
2879 -- consistent with following diagram:
2881 -- <inherited preconditions>
2882 -- <preconditions from spec>
2883 -- <preconditions from body>
2885 Process_Preconditions_For
(Body_Id
);
2887 if Present
(Spec_Id
) then
2888 Process_Preconditions_For
(Spec_Id
);
2889 Process_Inherited_Preconditions
;
2891 end Process_Preconditions
;
2895 Restore_Scope
: Boolean := False;
2897 Stmts
: List_Id
:= No_List
;
2898 Subp_Id
: Entity_Id
;
2900 -- Start of processing for Expand_Subprogram_Contract
2903 -- Obtain the entity of the initial declaration
2905 if Present
(Spec_Id
) then
2911 -- Do not perform expansion activity when it is not needed
2913 if not Expander_Active
then
2916 -- ASIS requires an unaltered tree
2918 elsif ASIS_Mode
then
2921 -- GNATprove does not need the executable semantics of a contract
2923 elsif GNATprove_Mode
then
2926 -- The contract of a generic subprogram or one declared in a generic
2927 -- context is not expanded, as the corresponding instance will provide
2928 -- the executable semantics of the contract.
2930 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
2933 -- All subprograms carry a contract, but for some it is not significant
2934 -- and should not be processed. This is a small optimization.
2936 elsif not Has_Significant_Contract
(Subp_Id
) then
2939 -- The contract of an ignored Ghost subprogram does not need expansion,
2940 -- because the subprogram and all calls to it will be removed.
2942 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
2945 -- Do not re-expand the same contract. This scenario occurs when a
2946 -- construct is rewritten into something else during its analysis
2947 -- (expression functions for instance).
2949 elsif Has_Expanded_Contract
(Subp_Id
) then
2953 -- Prevent multiple expansion attempts of the same contract
2955 Set_Has_Expanded_Contract
(Subp_Id
);
2957 -- Ensure that the formal parameters are visible when expanding all
2960 if not In_Open_Scopes
(Subp_Id
) then
2961 Restore_Scope
:= True;
2962 Push_Scope
(Subp_Id
);
2964 if Is_Generic_Subprogram
(Subp_Id
) then
2965 Install_Generic_Formals
(Subp_Id
);
2967 Install_Formals
(Subp_Id
);
2971 -- The expansion of a subprogram contract involves the creation of Check
2972 -- pragmas to verify the contract assertions of the spec and body in a
2973 -- particular order. The order is as follows:
2975 -- function Example (...) return ... is
2976 -- procedure _Postconditions (...) is
2978 -- <refined postconditions from body>
2979 -- <postconditions from body>
2980 -- <postconditions from spec>
2981 -- <inherited postconditions>
2982 -- <contract case consequences>
2983 -- <invariant check of function result>
2984 -- <invariant and predicate checks of parameters>
2985 -- end _Postconditions;
2987 -- <inherited preconditions>
2988 -- <preconditions from spec>
2989 -- <preconditions from body>
2990 -- <contract case conditions>
2992 -- <source declarations>
2994 -- <source statements>
2996 -- _Preconditions (Result);
3000 -- Routine _Postconditions holds all contract assertions that must be
3001 -- verified on exit from the related subprogram.
3003 -- Step 1: Handle all preconditions. This action must come before the
3004 -- processing of pragma Contract_Cases because the pragma prepends items
3005 -- to the body declarations.
3007 Process_Preconditions
;
3009 -- Step 2: Handle all postconditions. This action must come before the
3010 -- processing of pragma Contract_Cases because the pragma appends items
3013 Process_Postconditions
(Stmts
);
3015 -- Step 3: Handle pragma Contract_Cases. This action must come before
3016 -- the processing of invariants and predicates because those append
3017 -- items to list Stmts.
3019 Process_Contract_Cases
(Stmts
);
3021 -- Step 4: Apply invariant and predicate checks on a function result and
3022 -- all formals. The resulting checks are accumulated in list Stmts.
3024 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3026 -- Step 5: Construct procedure _Postconditions
3028 Build_Postconditions_Procedure
(Subp_Id
, Stmts
, Result
);
3030 if Restore_Scope
then
3033 end Expand_Subprogram_Contract
;
3035 -------------------------------
3036 -- Freeze_Previous_Contracts --
3037 -------------------------------
3039 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3040 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3041 pragma Inline
(Causes_Contract_Freezing
);
3042 -- Determine whether arbitrary node N causes contract freezing
3044 procedure Freeze_Contracts
;
3045 pragma Inline
(Freeze_Contracts
);
3046 -- Freeze the contracts of all eligible constructs which precede body
3049 procedure Freeze_Enclosing_Package_Body
;
3050 pragma Inline
(Freeze_Enclosing_Package_Body
);
3051 -- Freeze the contract of the nearest package body (if any) which
3052 -- encloses body Body_Decl.
3054 ------------------------------
3055 -- Causes_Contract_Freezing --
3056 ------------------------------
3058 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3060 return Nkind_In
(N
, N_Entry_Body
,
3064 N_Subprogram_Body_Stub
,
3066 end Causes_Contract_Freezing
;
3068 ----------------------
3069 -- Freeze_Contracts --
3070 ----------------------
3072 procedure Freeze_Contracts
is
3073 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3077 -- Nothing to do when the body which causes freezing does not appear
3078 -- in a declarative list because there cannot possibly be constructs
3081 if not Is_List_Member
(Body_Decl
) then
3085 -- Inspect the declarations preceding the body, and freeze individual
3086 -- contracts of eligible constructs.
3088 Decl
:= Prev
(Body_Decl
);
3089 while Present
(Decl
) loop
3091 -- Stop the traversal when a preceding construct that causes
3092 -- freezing is encountered as there is no point in refreezing
3093 -- the already frozen constructs.
3095 if Causes_Contract_Freezing
(Decl
) then
3098 -- Entry or subprogram declarations
3100 elsif Nkind_In
(Decl
, N_Abstract_Subprogram_Declaration
,
3101 N_Entry_Declaration
,
3102 N_Generic_Subprogram_Declaration
,
3103 N_Subprogram_Declaration
)
3105 Analyze_Entry_Or_Subprogram_Contract
3106 (Subp_Id
=> Defining_Entity
(Decl
),
3107 Freeze_Id
=> Body_Id
);
3111 elsif Nkind
(Decl
) = N_Object_Declaration
then
3112 Analyze_Object_Contract
3113 (Obj_Id
=> Defining_Entity
(Decl
),
3114 Freeze_Id
=> Body_Id
);
3118 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
3119 N_Single_Protected_Declaration
)
3121 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3123 -- Subprogram body stubs
3125 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3126 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3130 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
3131 N_Task_Type_Declaration
)
3133 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3138 end Freeze_Contracts
;
3140 -----------------------------------
3141 -- Freeze_Enclosing_Package_Body --
3142 -----------------------------------
3144 procedure Freeze_Enclosing_Package_Body
is
3145 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3149 -- Climb the parent chain looking for an enclosing package body. Do
3150 -- not use the scope stack, because a body utilizes the entity of its
3151 -- corresponding spec.
3153 Par
:= Parent
(Body_Decl
);
3154 while Present
(Par
) loop
3155 if Nkind
(Par
) = N_Package_Body
then
3156 Analyze_Package_Body_Contract
3157 (Body_Id
=> Defining_Entity
(Par
),
3158 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3162 -- Do not look for an enclosing package body when the construct
3163 -- which causes freezing is a body generated for an expression
3164 -- function and it appears within a package spec. This ensures
3165 -- that the traversal will not reach too far up the parent chain
3166 -- and attempt to freeze a package body which must not be frozen.
3168 -- package body Enclosing_Body
3169 -- with Refined_State => (State => Var)
3171 -- package Nested is
3172 -- type Some_Type is ...;
3173 -- function Cause_Freezing return ...;
3175 -- function Cause_Freezing is (...);
3178 -- Var : Nested.Some_Type;
3180 elsif Nkind
(Par
) = N_Package_Declaration
3181 and then Nkind
(Orig_Decl
) = N_Expression_Function
3185 -- Prevent the search from going too far
3187 elsif Is_Body_Or_Package_Declaration
(Par
) then
3191 Par
:= Parent
(Par
);
3193 end Freeze_Enclosing_Package_Body
;
3197 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3199 -- Start of processing for Freeze_Previous_Contracts
3202 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3204 -- A body that is in the process of being inlined appears from source,
3205 -- but carries name _parent. Such a body does not cause freezing of
3208 if Chars
(Body_Id
) = Name_uParent
then
3212 Freeze_Enclosing_Package_Body
;
3214 end Freeze_Previous_Contracts
;
3216 ---------------------------------
3217 -- Inherit_Subprogram_Contract --
3218 ---------------------------------
3220 procedure Inherit_Subprogram_Contract
3222 From_Subp
: Entity_Id
)
3224 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3225 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3228 --------------------
3229 -- Inherit_Pragma --
3230 --------------------
3232 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3233 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3237 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3238 -- chains, therefore the node must be replicated. The new pragma is
3239 -- flagged as inherited for distinction purposes.
3241 if Present
(Prag
) then
3242 New_Prag
:= New_Copy_Tree
(Prag
);
3243 Set_Is_Inherited_Pragma
(New_Prag
);
3245 Add_Contract_Item
(New_Prag
, Subp
);
3249 -- Start of processing for Inherit_Subprogram_Contract
3252 -- Inheritance is carried out only when both entities are subprograms
3255 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3256 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3257 and then Present
(Contract
(From_Subp
))
3259 Inherit_Pragma
(Pragma_Extensions_Visible
);
3261 end Inherit_Subprogram_Contract
;
3263 -------------------------------------
3264 -- Instantiate_Subprogram_Contract --
3265 -------------------------------------
3267 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3268 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3269 -- Instantiate all contract-related source pragmas found in the list,
3270 -- starting with pragma First_Prag. Each instantiated pragma is added
3273 -------------------------
3274 -- Instantiate_Pragmas --
3275 -------------------------
3277 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3278 Inst_Prag
: Node_Id
;
3283 while Present
(Prag
) loop
3284 if Is_Generic_Contract_Pragma
(Prag
) then
3286 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3288 Set_Analyzed
(Inst_Prag
, False);
3289 Append_To
(L
, Inst_Prag
);
3292 Prag
:= Next_Pragma
(Prag
);
3294 end Instantiate_Pragmas
;
3298 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3300 -- Start of processing for Instantiate_Subprogram_Contract
3303 if Present
(Items
) then
3304 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3305 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3306 Instantiate_Pragmas
(Classifications
(Items
));
3308 end Instantiate_Subprogram_Contract
;
3310 ----------------------------------------
3311 -- Save_Global_References_In_Contract --
3312 ----------------------------------------
3314 procedure Save_Global_References_In_Contract
3318 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
3319 -- Save all global references in contract-related source pragmas found
3320 -- in the list, starting with pragma First_Prag.
3322 ------------------------------------
3323 -- Save_Global_References_In_List --
3324 ------------------------------------
3326 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
3331 while Present
(Prag
) loop
3332 if Is_Generic_Contract_Pragma
(Prag
) then
3333 Save_Global_References
(Prag
);
3336 Prag
:= Next_Pragma
(Prag
);
3338 end Save_Global_References_In_List
;
3342 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3344 -- Start of processing for Save_Global_References_In_Contract
3347 -- The entity of the analyzed generic copy must be on the scope stack
3348 -- to ensure proper detection of global references.
3350 Push_Scope
(Gen_Id
);
3352 if Permits_Aspect_Specifications
(Templ
)
3353 and then Has_Aspects
(Templ
)
3355 Save_Global_References_In_Aspects
(Templ
);
3358 if Present
(Items
) then
3359 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
3360 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
3361 Save_Global_References_In_List
(Classifications
(Items
));
3365 end Save_Global_References_In_Contract
;