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 Freeze
; use Freeze
;
37 with Namet
; use Namet
;
38 with Nlists
; use Nlists
;
39 with Nmake
; use Nmake
;
42 with Sem_Aux
; use Sem_Aux
;
43 with Sem_Ch6
; use Sem_Ch6
;
44 with Sem_Ch8
; use Sem_Ch8
;
45 with Sem_Ch12
; use Sem_Ch12
;
46 with Sem_Ch13
; use Sem_Ch13
;
47 with Sem_Disp
; use Sem_Disp
;
48 with Sem_Prag
; use Sem_Prag
;
49 with Sem_Util
; use Sem_Util
;
50 with Sinfo
; use Sinfo
;
51 with Snames
; use Snames
;
52 with Stand
; use Stand
;
53 with Stringt
; use Stringt
;
54 with SCIL_LL
; use SCIL_LL
;
55 with Tbuild
; use Tbuild
;
57 package body Contracts
is
59 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
);
60 -- Analyze all delayed pragmas chained on the contract of package
61 -- instantiation Inst_Id as if they appear at the end of a declarative
62 -- region. The pragmas in question are:
66 procedure Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
);
67 -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
68 -- contract-only subprogram body of eligible subprograms found in L, adds
69 -- them to their corresponding list of declarations, and analyzes them.
71 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
);
72 -- Expand the contracts of a subprogram body and its correspoding spec (if
73 -- any). This routine processes all [refined] pre- and postconditions as
74 -- well as Contract_Cases, invariants and predicates. Body_Id denotes the
75 -- entity of the subprogram body.
77 -----------------------
78 -- Add_Contract_Item --
79 -----------------------
81 procedure Add_Contract_Item
(Prag
: Node_Id
; Id
: Entity_Id
) is
82 Items
: Node_Id
:= Contract
(Id
);
84 procedure Add_Classification
;
85 -- Prepend Prag to the list of classifications
87 procedure Add_Contract_Test_Case
;
88 -- Prepend Prag to the list of contract and test cases
90 procedure Add_Pre_Post_Condition
;
91 -- Prepend Prag to the list of pre- and postconditions
93 ------------------------
94 -- Add_Classification --
95 ------------------------
97 procedure Add_Classification
is
99 Set_Next_Pragma
(Prag
, Classifications
(Items
));
100 Set_Classifications
(Items
, Prag
);
101 end Add_Classification
;
103 ----------------------------
104 -- Add_Contract_Test_Case --
105 ----------------------------
107 procedure Add_Contract_Test_Case
is
109 Set_Next_Pragma
(Prag
, Contract_Test_Cases
(Items
));
110 Set_Contract_Test_Cases
(Items
, Prag
);
111 end Add_Contract_Test_Case
;
113 ----------------------------
114 -- Add_Pre_Post_Condition --
115 ----------------------------
117 procedure Add_Pre_Post_Condition
is
119 Set_Next_Pragma
(Prag
, Pre_Post_Conditions
(Items
));
120 Set_Pre_Post_Conditions
(Items
, Prag
);
121 end Add_Pre_Post_Condition
;
125 -- A contract must contain only pragmas
127 pragma Assert
(Nkind
(Prag
) = N_Pragma
);
128 Prag_Nam
: constant Name_Id
:= Pragma_Name
(Prag
);
130 -- Start of processing for Add_Contract_Item
133 -- Create a new contract when adding the first item
136 Items
:= Make_Contract
(Sloc
(Id
));
137 Set_Contract
(Id
, Items
);
140 -- Constants, the applicable pragmas are:
143 if Ekind
(Id
) = E_Constant
then
144 if Prag_Nam
= Name_Part_Of
then
147 -- The pragma is not a proper contract item
153 -- Entry bodies, the applicable pragmas are:
158 elsif Is_Entry_Body
(Id
) then
159 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
162 elsif Prag_Nam
= Name_Refined_Post
then
163 Add_Pre_Post_Condition
;
165 -- The pragma is not a proper contract item
171 -- Entry or subprogram declarations, the applicable pragmas are:
175 -- Extensions_Visible
183 elsif Is_Entry_Declaration
(Id
)
184 or else Ekind_In
(Id
, E_Function
,
189 if Nam_In
(Prag_Nam
, Name_Attach_Handler
, Name_Interrupt_Handler
)
190 and then Ekind_In
(Id
, E_Generic_Procedure
, E_Procedure
)
194 elsif Nam_In
(Prag_Nam
, Name_Depends
,
195 Name_Extensions_Visible
,
200 elsif Prag_Nam
= Name_Volatile_Function
201 and then Ekind_In
(Id
, E_Function
, E_Generic_Function
)
205 elsif Nam_In
(Prag_Nam
, Name_Contract_Cases
, Name_Test_Case
) then
206 Add_Contract_Test_Case
;
208 elsif Nam_In
(Prag_Nam
, Name_Postcondition
, Name_Precondition
) then
209 Add_Pre_Post_Condition
;
211 -- The pragma is not a proper contract item
217 -- Packages or instantiations, the applicable pragmas are:
221 -- Part_Of (instantiation only)
223 elsif Ekind_In
(Id
, E_Generic_Package
, E_Package
) then
224 if Nam_In
(Prag_Nam
, Name_Abstract_State
,
225 Name_Initial_Condition
,
230 -- Indicator Part_Of must be associated with a package instantiation
232 elsif Prag_Nam
= Name_Part_Of
and then Is_Generic_Instance
(Id
) then
235 -- The pragma is not a proper contract item
241 -- Package bodies, the applicable pragmas are:
244 elsif Ekind
(Id
) = E_Package_Body
then
245 if Prag_Nam
= Name_Refined_State
then
248 -- The pragma is not a proper contract item
254 -- Protected units, the applicable pragmas are:
257 elsif Ekind
(Id
) = E_Protected_Type
then
258 if Prag_Nam
= Name_Part_Of
then
261 -- The pragma is not a proper contract item
267 -- Subprogram bodies, the applicable pragmas are:
274 elsif Ekind
(Id
) = E_Subprogram_Body
then
275 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
278 elsif Nam_In
(Prag_Nam
, Name_Postcondition
,
282 Add_Pre_Post_Condition
;
284 -- The pragma is not a proper contract item
290 -- Task bodies, the applicable pragmas are:
294 elsif Ekind
(Id
) = E_Task_Body
then
295 if Nam_In
(Prag_Nam
, Name_Refined_Depends
, Name_Refined_Global
) then
298 -- The pragma is not a proper contract item
304 -- Task units, the applicable pragmas are:
309 elsif Ekind
(Id
) = E_Task_Type
then
310 if Nam_In
(Prag_Nam
, Name_Depends
, Name_Global
, Name_Part_Of
) then
313 -- The pragma is not a proper contract item
319 -- Variables, the applicable pragmas are:
322 -- Constant_After_Elaboration
329 elsif Ekind
(Id
) = E_Variable
then
330 if Nam_In
(Prag_Nam
, Name_Async_Readers
,
332 Name_Constant_After_Elaboration
,
334 Name_Effective_Reads
,
335 Name_Effective_Writes
,
341 -- The pragma is not a proper contract item
347 end Add_Contract_Item
;
349 -----------------------
350 -- Analyze_Contracts --
351 -----------------------
353 procedure Analyze_Contracts
(L
: List_Id
) is
357 if CodePeer_Mode
and then Debug_Flag_Dot_KK
then
358 Build_And_Analyze_Contract_Only_Subprograms
(L
);
362 while Present
(Decl
) loop
364 -- Entry or subprogram declarations
366 if Nkind_In
(Decl
, N_Abstract_Subprogram_Declaration
,
368 N_Generic_Subprogram_Declaration
,
369 N_Subprogram_Declaration
)
372 Subp_Id
: constant Entity_Id
:= Defining_Entity
(Decl
);
375 Analyze_Entry_Or_Subprogram_Contract
(Subp_Id
);
377 -- If analysis of a class-wide pre/postcondition indicates
378 -- that a class-wide clone is needed, analyze its declaration
379 -- now. Its body is created when the body of the original
380 -- operation is analyzed (and rewritten).
382 if Is_Subprogram
(Subp_Id
)
383 and then Present
(Class_Wide_Clone
(Subp_Id
))
385 Analyze
(Unit_Declaration_Node
(Class_Wide_Clone
(Subp_Id
)));
389 -- Entry or subprogram bodies
391 elsif Nkind_In
(Decl
, N_Entry_Body
, N_Subprogram_Body
) then
392 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
396 elsif Nkind
(Decl
) = N_Object_Declaration
then
397 Analyze_Object_Contract
(Defining_Entity
(Decl
));
399 -- Package instantiation
401 elsif Nkind
(Decl
) = N_Package_Instantiation
then
402 Analyze_Package_Instantiation_Contract
(Defining_Entity
(Decl
));
406 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
407 N_Single_Protected_Declaration
)
409 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
411 -- Subprogram body stubs
413 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
414 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
418 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
419 N_Task_Type_Declaration
)
421 Analyze_Task_Contract
(Defining_Entity
(Decl
));
423 -- For type declarations, we need to do the preanalysis of Iterable
424 -- aspect specifications.
426 -- Other type aspects need to be resolved here???
428 elsif Nkind
(Decl
) = N_Private_Type_Declaration
429 and then Present
(Aspect_Specifications
(Decl
))
432 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
433 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
437 Validate_Iterable_Aspect
(E
, It
);
444 end Analyze_Contracts
;
446 -----------------------------------------------
447 -- Analyze_Entry_Or_Subprogram_Body_Contract --
448 -----------------------------------------------
450 -- WARNING: This routine manages SPARK regions. Return statements must be
451 -- replaced by gotos which jump to the end of the routine and restore the
454 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
455 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
456 Items
: constant Node_Id
:= Contract
(Body_Id
);
457 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
459 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
460 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
461 -- Save the SPARK_Mode-related data to restore on exit
464 -- When a subprogram body declaration is illegal, its defining entity is
465 -- left unanalyzed. There is nothing left to do in this case because the
466 -- body lacks a contract, or even a proper Ekind.
468 if Ekind
(Body_Id
) = E_Void
then
471 -- Do not analyze a contract multiple times
473 elsif Present
(Items
) then
474 if Analyzed
(Items
) then
477 Set_Analyzed
(Items
);
481 -- Due to the timing of contract analysis, delayed pragmas may be
482 -- subject to the wrong SPARK_Mode, usually that of the enclosing
483 -- context. To remedy this, restore the original SPARK_Mode of the
484 -- related subprogram body.
486 Set_SPARK_Mode
(Body_Id
);
488 -- Ensure that the contract cases or postconditions mention 'Result or
489 -- define a post-state.
491 Check_Result_And_Post_State
(Body_Id
);
493 -- A stand-alone nonvolatile function body cannot have an effectively
494 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
495 -- check is relevant only when SPARK_Mode is on, as it is not a standard
496 -- legality rule. The check is performed here because Volatile_Function
497 -- is processed after the analysis of the related subprogram body. The
498 -- check only applies to source subprograms and not to generated TSS
502 and then Ekind_In
(Body_Id
, E_Function
, E_Generic_Function
)
503 and then Comes_From_Source
(Spec_Id
)
504 and then not Is_Volatile_Function
(Body_Id
)
506 Check_Nonvolatile_Function_Profile
(Body_Id
);
509 -- Restore the SPARK_Mode of the enclosing context after all delayed
510 -- pragmas have been analyzed.
512 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
514 -- Capture all global references in a generic subprogram body now that
515 -- the contract has been analyzed.
517 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
518 Save_Global_References_In_Contract
519 (Templ
=> Original_Node
(Body_Decl
),
523 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
524 -- invariants and predicates associated with body and its spec. Do not
525 -- expand the contract of subprogram body stubs.
527 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
528 Expand_Subprogram_Contract
(Body_Id
);
530 end Analyze_Entry_Or_Subprogram_Body_Contract
;
532 ------------------------------------------
533 -- Analyze_Entry_Or_Subprogram_Contract --
534 ------------------------------------------
536 -- WARNING: This routine manages SPARK regions. Return statements must be
537 -- replaced by gotos which jump to the end of the routine and restore the
540 procedure Analyze_Entry_Or_Subprogram_Contract
541 (Subp_Id
: Entity_Id
;
542 Freeze_Id
: Entity_Id
:= Empty
)
544 Items
: constant Node_Id
:= Contract
(Subp_Id
);
545 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
547 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
548 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
549 -- Save the SPARK_Mode-related data to restore on exit
551 Skip_Assert_Exprs
: constant Boolean :=
552 Ekind_In
(Subp_Id
, E_Entry
, E_Entry_Family
)
553 and then not ASIS_Mode
554 and then not GNATprove_Mode
;
556 Depends
: Node_Id
:= Empty
;
557 Global
: Node_Id
:= Empty
;
562 -- Do not analyze a contract multiple times
564 if Present
(Items
) then
565 if Analyzed
(Items
) then
568 Set_Analyzed
(Items
);
572 -- Due to the timing of contract analysis, delayed pragmas may be
573 -- subject to the wrong SPARK_Mode, usually that of the enclosing
574 -- context. To remedy this, restore the original SPARK_Mode of the
575 -- related subprogram body.
577 Set_SPARK_Mode
(Subp_Id
);
579 -- All subprograms carry a contract, but for some it is not significant
580 -- and should not be processed.
582 if not Has_Significant_Contract
(Subp_Id
) then
585 elsif Present
(Items
) then
587 -- Do not analyze the pre/postconditions of an entry declaration
588 -- unless annotating the original tree for ASIS or GNATprove. The
589 -- real analysis occurs when the pre/postconditons are relocated to
590 -- the contract wrapper procedure (see Build_Contract_Wrapper).
592 if Skip_Assert_Exprs
then
595 -- Otherwise analyze the pre/postconditions.
596 -- If these come from an aspect specification, their expressions
597 -- might include references to types that are not frozen yet, in the
598 -- case where the body is a rewritten expression function that is a
599 -- completion, so freeze all types within before constructing the
605 Freeze_Types
: Boolean := False;
608 if Present
(Freeze_Id
) then
609 Bod
:= Unit_Declaration_Node
(Freeze_Id
);
611 if Nkind
(Bod
) = N_Subprogram_Body
612 and then Was_Expression_Function
(Bod
)
613 and then Ekind
(Subp_Id
) = E_Function
614 and then Chars
(Subp_Id
) = Chars
(Freeze_Id
)
615 and then Subp_Id
/= Freeze_Id
617 Freeze_Types
:= True;
621 Prag
:= Pre_Post_Conditions
(Items
);
622 while Present
(Prag
) loop
624 and then Present
(Corresponding_Aspect
(Prag
))
628 Typ
=> Standard_Boolean
,
629 Expr
=> Expression
(Corresponding_Aspect
(Prag
)),
633 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
634 Prag
:= Next_Pragma
(Prag
);
639 -- Analyze contract-cases and test-cases
641 Prag
:= Contract_Test_Cases
(Items
);
642 while Present
(Prag
) loop
643 Prag_Nam
:= Pragma_Name
(Prag
);
645 if Prag_Nam
= Name_Contract_Cases
then
647 -- Do not analyze the contract cases of an entry declaration
648 -- unless annotating the original tree for ASIS or GNATprove.
649 -- The real analysis occurs when the contract cases are moved
650 -- to the contract wrapper procedure (Build_Contract_Wrapper).
652 if Skip_Assert_Exprs
then
655 -- Otherwise analyze the contract cases
658 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
661 pragma Assert
(Prag_Nam
= Name_Test_Case
);
662 Analyze_Test_Case_In_Decl_Part
(Prag
);
665 Prag
:= Next_Pragma
(Prag
);
668 -- Analyze classification pragmas
670 Prag
:= Classifications
(Items
);
671 while Present
(Prag
) loop
672 Prag_Nam
:= Pragma_Name
(Prag
);
674 if Prag_Nam
= Name_Depends
then
677 elsif Prag_Nam
= Name_Global
then
681 Prag
:= Next_Pragma
(Prag
);
684 -- Analyze Global first, as Depends may mention items classified in
685 -- the global categorization.
687 if Present
(Global
) then
688 Analyze_Global_In_Decl_Part
(Global
);
691 -- Depends must be analyzed after Global in order to see the modes of
694 if Present
(Depends
) then
695 Analyze_Depends_In_Decl_Part
(Depends
);
698 -- Ensure that the contract cases or postconditions mention 'Result
699 -- or define a post-state.
701 Check_Result_And_Post_State
(Subp_Id
);
704 -- A nonvolatile function cannot have an effectively volatile formal
705 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
706 -- only when SPARK_Mode is on, as it is not a standard legality rule.
707 -- The check is performed here because pragma Volatile_Function is
708 -- processed after the analysis of the related subprogram declaration.
711 and then Ekind_In
(Subp_Id
, E_Function
, E_Generic_Function
)
712 and then Comes_From_Source
(Subp_Id
)
713 and then not Is_Volatile_Function
(Subp_Id
)
715 Check_Nonvolatile_Function_Profile
(Subp_Id
);
718 -- Restore the SPARK_Mode of the enclosing context after all delayed
719 -- pragmas have been analyzed.
721 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
723 -- Capture all global references in a generic subprogram now that the
724 -- contract has been analyzed.
726 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
727 Save_Global_References_In_Contract
728 (Templ
=> Original_Node
(Subp_Decl
),
731 end Analyze_Entry_Or_Subprogram_Contract
;
733 -----------------------------
734 -- Analyze_Object_Contract --
735 -----------------------------
737 -- WARNING: This routine manages SPARK regions. Return statements must be
738 -- replaced by gotos which jump to the end of the routine and restore the
741 procedure Analyze_Object_Contract
743 Freeze_Id
: Entity_Id
:= Empty
)
745 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
747 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
748 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
749 -- Save the SPARK_Mode-related data to restore on exit
751 AR_Val
: Boolean := False;
752 AW_Val
: Boolean := False;
753 ER_Val
: Boolean := False;
754 EW_Val
: Boolean := False;
758 Seen
: Boolean := False;
761 -- The loop parameter in an element iterator over a formal container
762 -- is declared with an object declaration, but no contracts apply.
764 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
768 -- Do not analyze a contract multiple times
770 Items
:= Contract
(Obj_Id
);
772 if Present
(Items
) then
773 if Analyzed
(Items
) then
776 Set_Analyzed
(Items
);
780 -- The anonymous object created for a single concurrent type inherits
781 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
782 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
783 -- of the enclosing context. To remedy this, restore the original mode
784 -- of the related anonymous object.
786 if Is_Single_Concurrent_Object
(Obj_Id
)
787 and then Present
(SPARK_Pragma
(Obj_Id
))
789 Set_SPARK_Mode
(Obj_Id
);
792 -- Constant-related checks
794 if Ekind
(Obj_Id
) = E_Constant
then
796 -- Analyze indicator Part_Of
798 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
800 -- Check whether the lack of indicator Part_Of agrees with the
801 -- placement of the constant with respect to the state space.
804 Check_Missing_Part_Of
(Obj_Id
);
807 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
808 -- This check is relevant only when SPARK_Mode is on, as it is not
809 -- a standard Ada legality rule. Internally-generated constants that
810 -- map generic formals to actuals in instantiations are allowed to
814 and then Comes_From_Source
(Obj_Id
)
815 and then Is_Effectively_Volatile
(Obj_Id
)
816 and then No
(Corresponding_Generic_Association
(Parent
(Obj_Id
)))
818 Error_Msg_N
("constant cannot be volatile", Obj_Id
);
821 -- Variable-related checks
823 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
825 -- Analyze all external properties
827 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Readers
);
829 if Present
(Prag
) then
830 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
834 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Writers
);
836 if Present
(Prag
) then
837 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
841 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Reads
);
843 if Present
(Prag
) then
844 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
848 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Writes
);
850 if Present
(Prag
) then
851 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
855 -- Verify the mutual interaction of the various external properties
858 Check_External_Properties
(Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
861 -- The anonymous object created for a single concurrent type carries
862 -- pragmas Depends and Globat of the type.
864 if Is_Single_Concurrent_Object
(Obj_Id
) then
866 -- Analyze Global first, as Depends may mention items classified
867 -- in the global categorization.
869 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
871 if Present
(Prag
) then
872 Analyze_Global_In_Decl_Part
(Prag
);
875 -- Depends must be analyzed after Global in order to see the modes
876 -- of all global items.
878 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
880 if Present
(Prag
) then
881 Analyze_Depends_In_Decl_Part
(Prag
);
885 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
887 -- Analyze indicator Part_Of
889 if Present
(Prag
) then
890 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
892 -- The variable is a constituent of a single protected/task type
893 -- and behaves as a component of the type. Verify that references
894 -- to the variable occur within the definition or body of the type
897 if Present
(Encapsulating_State
(Obj_Id
))
898 and then Is_Single_Concurrent_Object
899 (Encapsulating_State
(Obj_Id
))
900 and then Present
(Part_Of_References
(Obj_Id
))
902 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
903 while Present
(Ref_Elmt
) loop
904 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
905 Next_Elmt
(Ref_Elmt
);
909 -- Otherwise check whether the lack of indicator Part_Of agrees with
910 -- the placement of the variable with respect to the state space.
913 Check_Missing_Part_Of
(Obj_Id
);
916 -- The following checks are relevant only when SPARK_Mode is on, as
917 -- they are not standard Ada legality rules. Internally generated
918 -- temporaries are ignored.
920 if SPARK_Mode
= On
and then Comes_From_Source
(Obj_Id
) then
921 if Is_Effectively_Volatile
(Obj_Id
) then
923 -- The declaration of an effectively volatile object must
924 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
926 if not Is_Library_Level_Entity
(Obj_Id
) then
928 ("volatile variable & must be declared at library level "
929 & "(SPARK RM 7.1.3(3))", Obj_Id
);
931 -- An object of a discriminated type cannot be effectively
932 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
934 elsif Has_Discriminants
(Obj_Typ
)
935 and then not Is_Protected_Type
(Obj_Typ
)
938 ("discriminated object & cannot be volatile", Obj_Id
);
941 -- The object is not effectively volatile
944 -- A non-effectively volatile object cannot have effectively
945 -- volatile components (SPARK RM 7.1.3(6)).
947 if not Is_Effectively_Volatile
(Obj_Id
)
948 and then Has_Volatile_Component
(Obj_Typ
)
951 ("non-volatile object & cannot have volatile components",
960 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
962 -- A Ghost object cannot be of a type that yields a synchronized
963 -- object (SPARK RM 6.9(19)).
965 if Yields_Synchronized_Object
(Obj_Typ
) then
966 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
968 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
969 -- SPARK RM 6.9(19)).
971 elsif Is_Effectively_Volatile
(Obj_Id
) then
972 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
974 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
975 -- One exception to this is the object that represents the dispatch
976 -- table of a Ghost tagged type, as the symbol needs to be exported.
978 elsif Is_Exported
(Obj_Id
) then
979 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
981 elsif Is_Imported
(Obj_Id
) then
982 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
986 -- Restore the SPARK_Mode of the enclosing context after all delayed
987 -- pragmas have been analyzed.
989 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
990 end Analyze_Object_Contract
;
992 -----------------------------------
993 -- Analyze_Package_Body_Contract --
994 -----------------------------------
996 -- WARNING: This routine manages SPARK regions. Return statements must be
997 -- replaced by gotos which jump to the end of the routine and restore the
1000 procedure Analyze_Package_Body_Contract
1001 (Body_Id
: Entity_Id
;
1002 Freeze_Id
: Entity_Id
:= Empty
)
1004 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1005 Items
: constant Node_Id
:= Contract
(Body_Id
);
1006 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
1008 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1009 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1010 -- Save the SPARK_Mode-related data to restore on exit
1012 Ref_State
: Node_Id
;
1015 -- Do not analyze a contract multiple times
1017 if Present
(Items
) then
1018 if Analyzed
(Items
) then
1021 Set_Analyzed
(Items
);
1025 -- Due to the timing of contract analysis, delayed pragmas may be
1026 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1027 -- context. To remedy this, restore the original SPARK_Mode of the
1028 -- related package body.
1030 Set_SPARK_Mode
(Body_Id
);
1032 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
1034 -- The analysis of pragma Refined_State detects whether the spec has
1035 -- abstract states available for refinement.
1037 if Present
(Ref_State
) then
1038 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
1041 -- Restore the SPARK_Mode of the enclosing context after all delayed
1042 -- pragmas have been analyzed.
1044 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1046 -- Capture all global references in a generic package body now that the
1047 -- contract has been analyzed.
1049 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1050 Save_Global_References_In_Contract
1051 (Templ
=> Original_Node
(Body_Decl
),
1054 end Analyze_Package_Body_Contract
;
1056 ------------------------------
1057 -- Analyze_Package_Contract --
1058 ------------------------------
1060 -- WARNING: This routine manages SPARK regions. Return statements must be
1061 -- replaced by gotos which jump to the end of the routine and restore the
1064 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1065 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1066 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1068 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1069 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1070 -- Save the SPARK_Mode-related data to restore on exit
1072 Init
: Node_Id
:= Empty
;
1073 Init_Cond
: Node_Id
:= Empty
;
1078 -- Do not analyze a contract multiple times
1080 if Present
(Items
) then
1081 if Analyzed
(Items
) then
1084 Set_Analyzed
(Items
);
1088 -- Due to the timing of contract analysis, delayed pragmas may be
1089 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1090 -- context. To remedy this, restore the original SPARK_Mode of the
1093 Set_SPARK_Mode
(Pack_Id
);
1095 if Present
(Items
) then
1097 -- Locate and store pragmas Initial_Condition and Initializes, since
1098 -- their order of analysis matters.
1100 Prag
:= Classifications
(Items
);
1101 while Present
(Prag
) loop
1102 Prag_Nam
:= Pragma_Name
(Prag
);
1104 if Prag_Nam
= Name_Initial_Condition
then
1107 elsif Prag_Nam
= Name_Initializes
then
1111 Prag
:= Next_Pragma
(Prag
);
1114 -- Analyze the initialization-related pragmas. Initializes must come
1115 -- before Initial_Condition due to item dependencies.
1117 if Present
(Init
) then
1118 Analyze_Initializes_In_Decl_Part
(Init
);
1121 if Present
(Init_Cond
) then
1122 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1126 -- Restore the SPARK_Mode of the enclosing context after all delayed
1127 -- pragmas have been analyzed.
1129 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1131 -- Capture all global references in a generic package now that the
1132 -- contract has been analyzed.
1134 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1135 Save_Global_References_In_Contract
1136 (Templ
=> Original_Node
(Pack_Decl
),
1139 end Analyze_Package_Contract
;
1141 --------------------------------------------
1142 -- Analyze_Package_Instantiation_Contract --
1143 --------------------------------------------
1145 -- WARNING: This routine manages SPARK regions. Return statements must be
1146 -- replaced by gotos which jump to the end of the routine and restore the
1149 procedure Analyze_Package_Instantiation_Contract
(Inst_Id
: Entity_Id
) is
1150 Inst_Spec
: constant Node_Id
:=
1151 Instance_Spec
(Unit_Declaration_Node
(Inst_Id
));
1153 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1154 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1155 -- Save the SPARK_Mode-related data to restore on exit
1157 Pack_Id
: Entity_Id
;
1161 -- Nothing to do when the package instantiation is erroneous or left
1162 -- partially decorated.
1164 if No
(Inst_Spec
) then
1168 Pack_Id
:= Defining_Entity
(Inst_Spec
);
1169 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1171 -- Due to the timing of contract analysis, delayed pragmas may be
1172 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1173 -- context. To remedy this, restore the original SPARK_Mode of the
1176 Set_SPARK_Mode
(Pack_Id
);
1178 -- Check whether the lack of indicator Part_Of agrees with the placement
1179 -- of the package instantiation with respect to the state space. Nested
1180 -- package instantiations do not need to be checked because they inherit
1181 -- Part_Of indicator of the outermost package instantiation (see routine
1182 -- Propagate_Part_Of in Sem_Prag).
1187 elsif No
(Prag
) then
1188 Check_Missing_Part_Of
(Pack_Id
);
1191 -- Restore the SPARK_Mode of the enclosing context after all delayed
1192 -- pragmas have been analyzed.
1194 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1195 end Analyze_Package_Instantiation_Contract
;
1197 --------------------------------
1198 -- Analyze_Protected_Contract --
1199 --------------------------------
1201 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1202 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1205 -- Do not analyze a contract multiple times
1207 if Present
(Items
) then
1208 if Analyzed
(Items
) then
1211 Set_Analyzed
(Items
);
1214 end Analyze_Protected_Contract
;
1216 -------------------------------------------
1217 -- Analyze_Subprogram_Body_Stub_Contract --
1218 -------------------------------------------
1220 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1221 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1222 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1225 -- A subprogram body stub may act as its own spec or as the completion
1226 -- of a previous declaration. Depending on the context, the contract of
1227 -- the stub may contain two sets of pragmas.
1229 -- The stub is a completion, the applicable pragmas are:
1233 if Present
(Spec_Id
) then
1234 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1236 -- The stub acts as its own spec, the applicable pragmas are:
1245 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1247 end Analyze_Subprogram_Body_Stub_Contract
;
1249 ---------------------------
1250 -- Analyze_Task_Contract --
1251 ---------------------------
1253 -- WARNING: This routine manages SPARK regions. Return statements must be
1254 -- replaced by gotos which jump to the end of the routine and restore the
1257 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1258 Items
: constant Node_Id
:= Contract
(Task_Id
);
1260 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1261 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1262 -- Save the SPARK_Mode-related data to restore on exit
1267 -- Do not analyze a contract multiple times
1269 if Present
(Items
) then
1270 if Analyzed
(Items
) then
1273 Set_Analyzed
(Items
);
1277 -- Due to the timing of contract analysis, delayed pragmas may be
1278 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1279 -- context. To remedy this, restore the original SPARK_Mode of the
1280 -- related task unit.
1282 Set_SPARK_Mode
(Task_Id
);
1284 -- Analyze Global first, as Depends may mention items classified in the
1285 -- global categorization.
1287 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1289 if Present
(Prag
) then
1290 Analyze_Global_In_Decl_Part
(Prag
);
1293 -- Depends must be analyzed after Global in order to see the modes of
1294 -- all global items.
1296 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1298 if Present
(Prag
) then
1299 Analyze_Depends_In_Decl_Part
(Prag
);
1302 -- Restore the SPARK_Mode of the enclosing context after all delayed
1303 -- pragmas have been analyzed.
1305 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1306 end Analyze_Task_Contract
;
1308 -------------------------------------------------
1309 -- Build_And_Analyze_Contract_Only_Subprograms --
1310 -------------------------------------------------
1312 procedure Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
) is
1313 procedure Analyze_Contract_Only_Subprograms
;
1314 -- Analyze the contract-only subprograms of L
1316 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
);
1317 -- Append the contract-only bodies of Subp_List to its declarations list
1319 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
;
1320 -- If E is an entity for a non-imported subprogram specification with
1321 -- pre/postconditions and we are compiling with CodePeer mode, then
1322 -- this procedure will create a wrapper to help Gnat2scil process its
1323 -- contracts. Return Empty if the wrapper cannot be built.
1325 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
;
1326 -- Build the contract-only subprograms of all eligible subprograms found
1329 function Has_Private_Declarations
(N
: Node_Id
) return Boolean;
1330 -- Return True for package specs, task definitions, and protected type
1331 -- definitions whose list of private declarations is not empty.
1333 ---------------------------------------
1334 -- Analyze_Contract_Only_Subprograms --
1335 ---------------------------------------
1337 procedure Analyze_Contract_Only_Subprograms
is
1338 procedure Analyze_Contract_Only_Bodies
;
1339 -- Analyze all the contract-only bodies of L
1341 ----------------------------------
1342 -- Analyze_Contract_Only_Bodies --
1343 ----------------------------------
1345 procedure Analyze_Contract_Only_Bodies
is
1350 while Present
(Decl
) loop
1351 if Nkind
(Decl
) = N_Subprogram_Body
1352 and then Is_Contract_Only_Body
1353 (Defining_Unit_Name
(Specification
(Decl
)))
1360 end Analyze_Contract_Only_Bodies
;
1362 -- Start of processing for Analyze_Contract_Only_Subprograms
1365 if Ekind
(Current_Scope
) /= E_Package
then
1366 Analyze_Contract_Only_Bodies
;
1370 Pkg_Spec
: constant Node_Id
:=
1371 Package_Specification
(Current_Scope
);
1374 if not Has_Private_Declarations
(Pkg_Spec
) then
1375 Analyze_Contract_Only_Bodies
;
1377 -- For packages with private declarations, the contract-only
1378 -- bodies of subprograms defined in the visible part of the
1379 -- package are added to its private declarations (to ensure
1380 -- that they do not cause premature freezing of types and also
1381 -- that they are analyzed with proper visibility). Hence they
1382 -- will be analyzed later.
1384 elsif Visible_Declarations
(Pkg_Spec
) = L
then
1387 elsif Private_Declarations
(Pkg_Spec
) = L
then
1388 Analyze_Contract_Only_Bodies
;
1392 end Analyze_Contract_Only_Subprograms
;
1394 --------------------------------------
1395 -- Append_Contract_Only_Subprograms --
1396 --------------------------------------
1398 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
) is
1400 if No
(Subp_List
) then
1404 if Ekind
(Current_Scope
) /= E_Package
then
1405 Append_List
(Subp_List
, To
=> L
);
1409 Pkg_Spec
: constant Node_Id
:=
1410 Package_Specification
(Current_Scope
);
1413 if not Has_Private_Declarations
(Pkg_Spec
) then
1414 Append_List
(Subp_List
, To
=> L
);
1416 -- If the package has private declarations then append them to
1417 -- its private declarations; they will be analyzed when the
1418 -- contracts of its private declarations are analyzed.
1423 To
=> Private_Declarations
(Pkg_Spec
));
1427 end Append_Contract_Only_Subprograms
;
1429 ------------------------------------
1430 -- Build_Contract_Only_Subprogram --
1431 ------------------------------------
1433 -- This procedure takes care of building a wrapper to generate better
1434 -- analysis results in the case of a call to a subprogram whose body
1435 -- is unavailable to CodePeer but whose specification includes Pre/Post
1436 -- conditions. The body might be unavailable for any of a number or
1437 -- reasons (it is imported, the .adb file is simply missing, or the
1438 -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
1439 -- pragma). The built subprogram has the following contents:
1440 -- * check preconditions
1441 -- * call the subprogram
1442 -- * check postconditions
1444 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
is
1445 Loc
: constant Source_Ptr
:= Sloc
(E
);
1447 Missing_Body_Name
: constant Name_Id
:=
1448 New_External_Name
(Chars
(E
), "__missing_body");
1450 function Build_Missing_Body_Decls
return List_Id
;
1451 -- Build the declaration of the missing body subprogram and its
1452 -- corresponding pragma Import.
1454 function Build_Missing_Body_Subprogram_Call
return Node_Id
;
1455 -- Build the call to the missing body subprogram
1457 function Skip_Contract_Only_Subprogram
(E
: Entity_Id
) return Boolean;
1458 -- Return True for cases where the wrapper is not needed or we cannot
1461 ------------------------------
1462 -- Build_Missing_Body_Decls --
1463 ------------------------------
1465 function Build_Missing_Body_Decls
return List_Id
is
1466 Spec
: constant Node_Id
:= Declaration_Node
(E
);
1472 Make_Subprogram_Declaration
(Loc
, Copy_Subprogram_Spec
(Spec
));
1473 Set_Chars
(Defining_Entity
(Decl
), Missing_Body_Name
);
1477 Chars
=> Name_Import
,
1478 Pragma_Argument_Associations
=> New_List
(
1479 Make_Pragma_Argument_Association
(Loc
,
1480 Expression
=> Make_Identifier
(Loc
, Name_Ada
)),
1482 Make_Pragma_Argument_Association
(Loc
,
1483 Expression
=> Make_Identifier
(Loc
, Missing_Body_Name
))));
1485 return New_List
(Decl
, Prag
);
1486 end Build_Missing_Body_Decls
;
1488 ----------------------------------------
1489 -- Build_Missing_Body_Subprogram_Call --
1490 ----------------------------------------
1492 function Build_Missing_Body_Subprogram_Call
return Node_Id
is
1499 -- Build parameter list that we need
1501 Forml
:= First_Formal
(E
);
1502 while Present
(Forml
) loop
1503 Append_To
(Parms
, Make_Identifier
(Loc
, Chars
(Forml
)));
1504 Next_Formal
(Forml
);
1507 -- Build the call to the missing body subprogram
1509 if Ekind_In
(E
, E_Function
, E_Generic_Function
) then
1511 Make_Simple_Return_Statement
(Loc
,
1513 Make_Function_Call
(Loc
,
1515 Make_Identifier
(Loc
, Missing_Body_Name
),
1516 Parameter_Associations
=> Parms
));
1520 Make_Procedure_Call_Statement
(Loc
,
1522 Make_Identifier
(Loc
, Missing_Body_Name
),
1523 Parameter_Associations
=> Parms
);
1525 end Build_Missing_Body_Subprogram_Call
;
1527 -----------------------------------
1528 -- Skip_Contract_Only_Subprogram --
1529 -----------------------------------
1531 function Skip_Contract_Only_Subprogram
1532 (E
: Entity_Id
) return Boolean
1534 function Depends_On_Enclosing_Private_Type
return Boolean;
1535 -- Return True if some formal of E (or its return type) are
1536 -- private types defined in an enclosing package.
1538 function Some_Enclosing_Package_Has_Private_Decls
return Boolean;
1539 -- Return True if some enclosing package of the current scope has
1540 -- private declarations.
1542 ---------------------------------------
1543 -- Depends_On_Enclosing_Private_Type --
1544 ---------------------------------------
1546 function Depends_On_Enclosing_Private_Type
return Boolean is
1547 function Defined_In_Enclosing_Package
1548 (Typ
: Entity_Id
) return Boolean;
1549 -- Return True if Typ is an entity defined in an enclosing
1550 -- package of the current scope.
1552 ----------------------------------
1553 -- Defined_In_Enclosing_Package --
1554 ----------------------------------
1556 function Defined_In_Enclosing_Package
1557 (Typ
: Entity_Id
) return Boolean
1559 Scop
: Entity_Id
:= Scope
(Current_Scope
);
1562 while Scop
/= Scope
(Typ
)
1563 and then not Is_Compilation_Unit
(Scop
)
1565 Scop
:= Scope
(Scop
);
1568 return Scop
= Scope
(Typ
);
1569 end Defined_In_Enclosing_Package
;
1573 Param_E
: Entity_Id
;
1576 -- Start of processing for Depends_On_Enclosing_Private_Type
1579 Param_E
:= First_Entity
(E
);
1580 while Present
(Param_E
) loop
1581 Typ
:= Etype
(Param_E
);
1583 if Is_Private_Type
(Typ
)
1584 and then Defined_In_Enclosing_Package
(Typ
)
1589 Next_Entity
(Param_E
);
1593 Ekind
(E
) = E_Function
1594 and then Is_Private_Type
(Etype
(E
))
1595 and then Defined_In_Enclosing_Package
(Etype
(E
));
1596 end Depends_On_Enclosing_Private_Type
;
1598 ----------------------------------------------
1599 -- Some_Enclosing_Package_Has_Private_Decls --
1600 ----------------------------------------------
1602 function Some_Enclosing_Package_Has_Private_Decls
return Boolean is
1603 Scop
: Entity_Id
:= Current_Scope
;
1604 Pkg_Spec
: Node_Id
:= Package_Specification
(Scop
);
1608 if Ekind
(Scop
) = E_Package
1609 and then Has_Private_Declarations
1610 (Package_Specification
(Scop
))
1612 Pkg_Spec
:= Package_Specification
(Scop
);
1615 exit when Is_Compilation_Unit
(Scop
);
1616 Scop
:= Scope
(Scop
);
1619 return Pkg_Spec
/= Package_Specification
(Current_Scope
);
1620 end Some_Enclosing_Package_Has_Private_Decls
;
1622 -- Start of processing for Skip_Contract_Only_Subprogram
1625 if not CodePeer_Mode
1626 or else Inside_A_Generic
1627 or else not Is_Subprogram
(E
)
1628 or else Is_Abstract_Subprogram
(E
)
1629 or else Is_Imported
(E
)
1630 or else No
(Contract
(E
))
1631 or else No
(Pre_Post_Conditions
(Contract
(E
)))
1632 or else Is_Contract_Only_Body
(E
)
1633 or else Convention
(E
) = Convention_Protected
1637 -- We do not support building the contract-only subprogram if E
1638 -- is a subprogram declared in a nested package that has some
1639 -- formal or return type depending on a private type defined in
1640 -- an enclosing package.
1642 elsif Ekind
(Current_Scope
) = E_Package
1643 and then Some_Enclosing_Package_Has_Private_Decls
1644 and then Depends_On_Enclosing_Private_Type
1646 if Debug_Flag_Dot_KK
then
1648 Saved_Mode
: constant Warning_Mode_Type
:= Warning_Mode
;
1651 -- Warnings are disabled by default under CodePeer_Mode
1652 -- (see switch-c). Enable them temporarily.
1654 Warning_Mode
:= Normal
;
1656 ("cannot generate contract-only subprogram?", E
);
1657 Warning_Mode
:= Saved_Mode
;
1665 end Skip_Contract_Only_Subprogram
;
1667 -- Start of processing for Build_Contract_Only_Subprogram
1670 -- Test cases where the wrapper is not needed and cases where we
1673 if Skip_Contract_Only_Subprogram
(E
) then
1677 -- Note on calls to Copy_Separate_Tree. The trees we are copying
1678 -- here are fully analyzed, but we definitely want fully syntactic
1679 -- unanalyzed trees in the body we construct, so that the analysis
1680 -- generates the right visibility, and that is exactly what the
1681 -- calls to Copy_Separate_Tree give us.
1684 Name
: constant Name_Id
:=
1685 New_External_Name
(Chars
(E
), "__contract_only");
1691 Make_Subprogram_Body
(Loc
,
1693 Copy_Subprogram_Spec
(Declaration_Node
(E
)),
1695 Build_Missing_Body_Decls
,
1696 Handled_Statement_Sequence
=>
1697 Make_Handled_Sequence_Of_Statements
(Loc
,
1698 Statements
=> New_List
(
1699 Build_Missing_Body_Subprogram_Call
),
1700 End_Label
=> Make_Identifier
(Loc
, Name
)));
1702 Id
:= Defining_Unit_Name
(Specification
(Bod
));
1704 -- Copy only the pre/postconditions of the original contract
1705 -- since it is what we need, but also because pragmas stored in
1706 -- the other fields have N_Pragmas with N_Aspect_Specifications
1707 -- that reference their associated pragma (thus causing an endless
1708 -- loop when trying to copy the subtree).
1711 New_Contract
: constant Node_Id
:= Make_Contract
(Sloc
(E
));
1714 Set_Pre_Post_Conditions
(New_Contract
,
1715 Copy_Separate_Tree
(Pre_Post_Conditions
(Contract
(E
))));
1716 Set_Contract
(Id
, New_Contract
);
1719 -- Fix the name of this new subprogram and link the original
1720 -- subprogram with its Contract_Only_Body subprogram.
1722 Set_Chars
(Id
, Name
);
1723 Set_Is_Contract_Only_Body
(Id
);
1724 Set_Contract_Only_Body
(E
, Id
);
1728 end Build_Contract_Only_Subprogram
;
1730 -------------------------------------
1731 -- Build_Contract_Only_Subprograms --
1732 -------------------------------------
1734 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
is
1737 Result
: List_Id
:= No_List
;
1738 Subp_Id
: Entity_Id
;
1742 while Present
(Decl
) loop
1743 if Nkind
(Decl
) = N_Subprogram_Declaration
then
1744 Subp_Id
:= Defining_Unit_Name
(Specification
(Decl
));
1745 New_Subp
:= Build_Contract_Only_Subprogram
(Subp_Id
);
1747 if Present
(New_Subp
) then
1752 Append_To
(Result
, New_Subp
);
1760 end Build_Contract_Only_Subprograms
;
1762 ------------------------------
1763 -- Has_Private_Declarations --
1764 ------------------------------
1766 function Has_Private_Declarations
(N
: Node_Id
) return Boolean is
1768 if not Nkind_In
(N
, N_Package_Specification
,
1769 N_Protected_Definition
,
1775 Present
(Private_Declarations
(N
))
1776 and then Is_Non_Empty_List
(Private_Declarations
(N
));
1778 end Has_Private_Declarations
;
1782 Subp_List
: List_Id
;
1784 -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
1787 Subp_List
:= Build_Contract_Only_Subprograms
(L
);
1788 Append_Contract_Only_Subprograms
(Subp_List
);
1789 Analyze_Contract_Only_Subprograms
;
1790 end Build_And_Analyze_Contract_Only_Subprograms
;
1792 -----------------------------
1793 -- Create_Generic_Contract --
1794 -----------------------------
1796 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
1797 Templ
: constant Node_Id
:= Original_Node
(Unit
);
1798 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
1800 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
1801 -- Add a single contract-related source pragma Prag to the contract of
1802 -- generic template Templ_Id.
1804 ---------------------------------
1805 -- Add_Generic_Contract_Pragma --
1806 ---------------------------------
1808 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
1809 Prag_Templ
: Node_Id
;
1812 -- Mark the pragma to prevent the premature capture of global
1813 -- references when capturing global references of the context
1814 -- (see Save_References_In_Pragma).
1816 Set_Is_Generic_Contract_Pragma
(Prag
);
1818 -- Pragmas that apply to a generic subprogram declaration are not
1819 -- part of the semantic structure of the generic template:
1822 -- procedure Example (Formal : Integer);
1823 -- pragma Precondition (Formal > 0);
1825 -- Create a generic template for such pragmas and link the template
1826 -- of the pragma with the generic template.
1828 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1830 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
1831 Prag_Templ
:= Original_Node
(Prag
);
1833 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
1834 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
1836 -- Otherwise link the pragma with the generic template
1839 Add_Contract_Item
(Prag
, Templ_Id
);
1841 end Add_Generic_Contract_Pragma
;
1845 Context
: constant Node_Id
:= Parent
(Unit
);
1846 Decl
: Node_Id
:= Empty
;
1848 -- Start of processing for Create_Generic_Contract
1851 -- A generic package declaration carries contract-related source pragmas
1852 -- in its visible declarations.
1854 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
1855 Set_Ekind
(Templ_Id
, E_Generic_Package
);
1857 if Present
(Visible_Declarations
(Specification
(Templ
))) then
1858 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
1861 -- A generic package body carries contract-related source pragmas in its
1864 elsif Nkind
(Templ
) = N_Package_Body
then
1865 Set_Ekind
(Templ_Id
, E_Package_Body
);
1867 if Present
(Declarations
(Templ
)) then
1868 Decl
:= First
(Declarations
(Templ
));
1871 -- Generic subprogram declaration
1873 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1874 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
1875 Set_Ekind
(Templ_Id
, E_Generic_Function
);
1877 Set_Ekind
(Templ_Id
, E_Generic_Procedure
);
1880 -- When the generic subprogram acts as a compilation unit, inspect
1881 -- the Pragmas_After list for contract-related source pragmas.
1883 if Nkind
(Context
) = N_Compilation_Unit
then
1884 if Present
(Aux_Decls_Node
(Context
))
1885 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
1887 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
1890 -- Otherwise inspect the successive declarations for contract-related
1894 Decl
:= Next
(Unit
);
1897 -- A generic subprogram body carries contract-related source pragmas in
1898 -- its declarations.
1900 elsif Nkind
(Templ
) = N_Subprogram_Body
then
1901 Set_Ekind
(Templ_Id
, E_Subprogram_Body
);
1903 if Present
(Declarations
(Templ
)) then
1904 Decl
:= First
(Declarations
(Templ
));
1908 -- Inspect the relevant declarations looking for contract-related source
1909 -- pragmas and add them to the contract of the generic unit.
1911 while Present
(Decl
) loop
1912 if Comes_From_Source
(Decl
) then
1913 if Nkind
(Decl
) = N_Pragma
then
1915 -- The source pragma is a contract annotation
1917 if Is_Contract_Annotation
(Decl
) then
1918 Add_Generic_Contract_Pragma
(Decl
);
1921 -- The region where a contract-related source pragma may appear
1922 -- ends with the first source non-pragma declaration or statement.
1931 end Create_Generic_Contract
;
1933 --------------------------------
1934 -- Expand_Subprogram_Contract --
1935 --------------------------------
1937 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
1938 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1939 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1941 procedure Add_Invariant_And_Predicate_Checks
1942 (Subp_Id
: Entity_Id
;
1943 Stmts
: in out List_Id
;
1944 Result
: out Node_Id
);
1945 -- Process the result of function Subp_Id (if applicable) and all its
1946 -- formals. Add invariant and predicate checks where applicable. The
1947 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1948 -- function, Result contains the entity of parameter _Result, to be
1949 -- used in the creation of procedure _Postconditions.
1951 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
1952 -- Append a node to a list. If there is no list, create a new one. When
1953 -- the item denotes a pragma, it is added to the list only when it is
1956 procedure Build_Postconditions_Procedure
1957 (Subp_Id
: Entity_Id
;
1959 Result
: Entity_Id
);
1960 -- Create the body of procedure _Postconditions which handles various
1961 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1962 -- of statements to be checked on exit. Parameter Result is the entity
1963 -- of parameter _Result when Subp_Id denotes a function.
1965 procedure Process_Contract_Cases
(Stmts
: in out List_Id
);
1966 -- Process pragma Contract_Cases. This routine prepends items to the
1967 -- body declarations and appends items to list Stmts.
1969 procedure Process_Postconditions
(Stmts
: in out List_Id
);
1970 -- Collect all [inherited] spec and body postconditions and accumulate
1971 -- their pragma Check equivalents in list Stmts.
1973 procedure Process_Preconditions
;
1974 -- Collect all [inherited] spec and body preconditions and prepend their
1975 -- pragma Check equivalents to the declarations of the body.
1977 ----------------------------------------
1978 -- Add_Invariant_And_Predicate_Checks --
1979 ----------------------------------------
1981 procedure Add_Invariant_And_Predicate_Checks
1982 (Subp_Id
: Entity_Id
;
1983 Stmts
: in out List_Id
;
1984 Result
: out Node_Id
)
1986 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
1987 -- Id denotes the return value of a function or a formal parameter.
1988 -- Add an invariant check if the type of Id is access to a type with
1989 -- invariants. The routine appends the generated code to Stmts.
1991 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
1992 -- Determine whether type Typ can benefit from invariant checks. To
1993 -- qualify, the type must have a non-null invariant procedure and
1994 -- subprogram Subp_Id must appear visible from the point of view of
1997 ---------------------------------
1998 -- Add_Invariant_Access_Checks --
1999 ---------------------------------
2001 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
2002 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2009 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
2010 Typ
:= Designated_Type
(Typ
);
2012 if Invariant_Checks_OK
(Typ
) then
2014 Make_Explicit_Dereference
(Loc
,
2015 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
2016 Set_Etype
(Ref
, Typ
);
2019 -- if <Id> /= null then
2020 -- <invariant_call (<Ref>)>
2025 Make_If_Statement
(Loc
,
2028 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
2029 Right_Opnd
=> Make_Null
(Loc
)),
2030 Then_Statements
=> New_List
(
2031 Make_Invariant_Call
(Ref
))),
2035 end Add_Invariant_Access_Checks
;
2037 -------------------------
2038 -- Invariant_Checks_OK --
2039 -------------------------
2041 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
2042 function Has_Public_Visibility_Of_Subprogram
return Boolean;
2043 -- Determine whether type Typ has public visibility of subprogram
2046 -----------------------------------------
2047 -- Has_Public_Visibility_Of_Subprogram --
2048 -----------------------------------------
2050 function Has_Public_Visibility_Of_Subprogram
return Boolean is
2051 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2054 -- An Initialization procedure must be considered visible even
2055 -- though it is internally generated.
2057 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2060 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2063 -- Internally generated code is never publicly visible except
2064 -- for a subprogram that is the implementation of an expression
2065 -- function. In that case the visibility is determined by the
2068 elsif not Comes_From_Source
(Subp_Decl
)
2070 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2072 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2076 -- Determine whether the subprogram is declared in the visible
2077 -- declarations of the package containing the type, or in the
2078 -- visible declaration of a child unit of that package.
2082 Decls
: constant List_Id
:=
2083 List_Containing
(Subp_Decl
);
2084 Subp_Scope
: constant Entity_Id
:=
2085 Scope
(Defining_Entity
(Subp_Decl
));
2086 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2090 Decls
= Visible_Declarations
2091 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2094 (Ekind
(Subp_Scope
) = E_Package
2095 and then Typ_Scope
/= Subp_Scope
2096 and then Is_Child_Unit
(Subp_Scope
)
2098 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2100 Decls
= Visible_Declarations
2102 (Unit_Declaration_Node
(Subp_Scope
))));
2105 end Has_Public_Visibility_Of_Subprogram
;
2107 -- Start of processing for Invariant_Checks_OK
2111 Has_Invariants
(Typ
)
2112 and then Present
(Invariant_Procedure
(Typ
))
2113 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2114 and then Has_Public_Visibility_Of_Subprogram
;
2115 end Invariant_Checks_OK
;
2119 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2120 -- Source location of subprogram body contract
2125 -- Start of processing for Add_Invariant_And_Predicate_Checks
2130 -- Process the result of a function
2132 if Ekind
(Subp_Id
) = E_Function
then
2133 Typ
:= Etype
(Subp_Id
);
2135 -- Generate _Result which is used in procedure _Postconditions to
2136 -- verify the return value.
2138 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2139 Set_Etype
(Result
, Typ
);
2141 -- Add an invariant check when the return type has invariants and
2142 -- the related function is visible to the outside.
2144 if Invariant_Checks_OK
(Typ
) then
2147 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2151 -- Add an invariant check when the return type is an access to a
2152 -- type with invariants.
2154 Add_Invariant_Access_Checks
(Result
);
2157 -- Add invariant and predicates for all formals that qualify
2159 Formal
:= First_Formal
(Subp_Id
);
2160 while Present
(Formal
) loop
2161 Typ
:= Etype
(Formal
);
2163 if Ekind
(Formal
) /= E_In_Parameter
2164 or else Is_Access_Type
(Typ
)
2166 if Invariant_Checks_OK
(Typ
) then
2169 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2173 Add_Invariant_Access_Checks
(Formal
);
2175 -- Note: we used to add predicate checks for OUT and IN OUT
2176 -- formals here, but that was misguided, since such checks are
2177 -- performed on the caller side, based on the predicate of the
2178 -- actual, rather than the predicate of the formal.
2182 Next_Formal
(Formal
);
2184 end Add_Invariant_And_Predicate_Checks
;
2186 -------------------------
2187 -- Append_Enabled_Item --
2188 -------------------------
2190 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2192 -- Do not chain ignored or disabled pragmas
2194 if Nkind
(Item
) = N_Pragma
2195 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2199 -- Otherwise, add the item
2206 -- If the pragma is a conjunct in a composite postcondition, it
2207 -- has been processed in reverse order. In the postcondition body
2208 -- it must appear before the others.
2210 if Nkind
(Item
) = N_Pragma
2211 and then From_Aspect_Specification
(Item
)
2212 and then Split_PPC
(Item
)
2214 Prepend
(Item
, List
);
2216 Append
(Item
, List
);
2219 end Append_Enabled_Item
;
2221 ------------------------------------
2222 -- Build_Postconditions_Procedure --
2223 ------------------------------------
2225 procedure Build_Postconditions_Procedure
2226 (Subp_Id
: Entity_Id
;
2230 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
);
2231 -- Insert node Stmt before the first source declaration of the
2232 -- related subprogram's body. If no such declaration exists, Stmt
2233 -- becomes the last declaration.
2235 --------------------------------------------
2236 -- Insert_Before_First_Source_Declaration --
2237 --------------------------------------------
2239 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
) is
2240 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2244 -- Inspect the declarations of the related subprogram body looking
2245 -- for the first source declaration.
2247 if Present
(Decls
) then
2248 Decl
:= First
(Decls
);
2249 while Present
(Decl
) loop
2250 if Comes_From_Source
(Decl
) then
2251 Insert_Before
(Decl
, Stmt
);
2258 -- If we get there, then the subprogram body lacks any source
2259 -- declarations. The body of _Postconditions now acts as the
2260 -- last declaration.
2262 Append
(Stmt
, Decls
);
2264 -- Ensure that the body has a declaration list
2267 Set_Declarations
(Body_Decl
, New_List
(Stmt
));
2269 end Insert_Before_First_Source_Declaration
;
2273 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2274 Params
: List_Id
:= No_List
;
2276 Proc_Decl
: Node_Id
;
2277 Proc_Id
: Entity_Id
;
2278 Proc_Spec
: Node_Id
;
2280 -- Start of processing for Build_Postconditions_Procedure
2283 -- Nothing to do if there are no actions to check on exit
2289 Proc_Id
:= Make_Defining_Identifier
(Loc
, Name_uPostconditions
);
2290 Set_Debug_Info_Needed
(Proc_Id
);
2291 Set_Postconditions_Proc
(Subp_Id
, Proc_Id
);
2293 -- Force the front-end inlining of _Postconditions when generating C
2294 -- code, since its body may have references to itypes defined in the
2295 -- enclosing subprogram, which would cause problems for unnesting
2296 -- routines in the absence of inlining.
2298 if Modify_Tree_For_C
then
2299 Set_Has_Pragma_Inline
(Proc_Id
);
2300 Set_Has_Pragma_Inline_Always
(Proc_Id
);
2301 Set_Is_Inlined
(Proc_Id
);
2304 -- The related subprogram is a function: create the specification of
2305 -- parameter _Result.
2307 if Present
(Result
) then
2308 Params
:= New_List
(
2309 Make_Parameter_Specification
(Loc
,
2310 Defining_Identifier
=> Result
,
2312 New_Occurrence_Of
(Etype
(Result
), Loc
)));
2316 Make_Procedure_Specification
(Loc
,
2317 Defining_Unit_Name
=> Proc_Id
,
2318 Parameter_Specifications
=> Params
);
2320 Proc_Decl
:= Make_Subprogram_Declaration
(Loc
, Proc_Spec
);
2322 -- Insert _Postconditions before the first source declaration of the
2323 -- body. This ensures that the body will not cause any premature
2324 -- freezing, as it may mention types:
2326 -- procedure Proc (Obj : Array_Typ) is
2327 -- procedure _postconditions is
2330 -- end _postconditions;
2332 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
2335 -- In the example above, Obj is of type T but the incorrect placement
2336 -- of _Postconditions will cause a crash in gigi due to an out-of-
2337 -- order reference. The body of _Postconditions must be placed after
2338 -- the declaration of Temp to preserve correct visibility.
2340 Insert_Before_First_Source_Declaration
(Proc_Decl
);
2341 Analyze
(Proc_Decl
);
2343 -- Set an explicit End_Label to override the sloc of the implicit
2344 -- RETURN statement, and prevent it from inheriting the sloc of one
2345 -- the postconditions: this would cause confusing debug info to be
2346 -- produced, interfering with coverage-analysis tools.
2349 Make_Subprogram_Body
(Loc
,
2351 Copy_Subprogram_Spec
(Proc_Spec
),
2352 Declarations
=> Empty_List
,
2353 Handled_Statement_Sequence
=>
2354 Make_Handled_Sequence_Of_Statements
(Loc
,
2355 Statements
=> Stmts
,
2356 End_Label
=> Make_Identifier
(Loc
, Chars
(Proc_Id
))));
2358 Insert_After_And_Analyze
(Proc_Decl
, Proc_Bod
);
2359 end Build_Postconditions_Procedure
;
2361 ----------------------------
2362 -- Process_Contract_Cases --
2363 ----------------------------
2365 procedure Process_Contract_Cases
(Stmts
: in out List_Id
) is
2366 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2367 -- Process pragma Contract_Cases for subprogram Subp_Id
2369 --------------------------------
2370 -- Process_Contract_Cases_For --
2371 --------------------------------
2373 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2374 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2378 if Present
(Items
) then
2379 Prag
:= Contract_Test_Cases
(Items
);
2380 while Present
(Prag
) loop
2381 if Pragma_Name
(Prag
) = Name_Contract_Cases
2382 and then Is_Checked
(Prag
)
2384 Expand_Pragma_Contract_Cases
2387 Decls
=> Declarations
(Body_Decl
),
2391 Prag
:= Next_Pragma
(Prag
);
2394 end Process_Contract_Cases_For
;
2396 pragma Unmodified
(Stmts
);
2397 -- Stmts is passed as IN OUT to signal that the list can be updated,
2398 -- even if the corresponding integer value representing the list does
2401 -- Start of processing for Process_Contract_Cases
2404 Process_Contract_Cases_For
(Body_Id
);
2406 if Present
(Spec_Id
) then
2407 Process_Contract_Cases_For
(Spec_Id
);
2409 end Process_Contract_Cases
;
2411 ----------------------------
2412 -- Process_Postconditions --
2413 ----------------------------
2415 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2416 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2417 -- Collect all [refined] postconditions of a specific kind denoted
2418 -- by Post_Nam that belong to the body, and generate pragma Check
2419 -- equivalents in list Stmts.
2421 procedure Process_Spec_Postconditions
;
2422 -- Collect all [inherited] postconditions of the spec, and generate
2423 -- pragma Check equivalents in list Stmts.
2425 ---------------------------------
2426 -- Process_Body_Postconditions --
2427 ---------------------------------
2429 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2430 Items
: constant Node_Id
:= Contract
(Body_Id
);
2431 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2436 -- Process the contract
2438 if Present
(Items
) then
2439 Prag
:= Pre_Post_Conditions
(Items
);
2440 while Present
(Prag
) loop
2441 if Pragma_Name
(Prag
) = Post_Nam
2442 and then Is_Checked
(Prag
)
2445 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2449 Prag
:= Next_Pragma
(Prag
);
2453 -- The subprogram body being processed is actually the proper body
2454 -- of a stub with a corresponding spec. The subprogram stub may
2455 -- carry a postcondition pragma, in which case it must be taken
2456 -- into account. The pragma appears after the stub.
2458 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2459 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2460 while Present
(Decl
) loop
2462 -- Note that non-matching pragmas are skipped
2464 if Nkind
(Decl
) = N_Pragma
then
2465 if Pragma_Name
(Decl
) = Post_Nam
2466 and then Is_Checked
(Decl
)
2469 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2473 -- Skip internally generated code
2475 elsif not Comes_From_Source
(Decl
) then
2478 -- Postcondition pragmas are usually grouped together. There
2479 -- is no need to inspect the whole declarative list.
2488 end Process_Body_Postconditions
;
2490 ---------------------------------
2491 -- Process_Spec_Postconditions --
2492 ---------------------------------
2494 procedure Process_Spec_Postconditions
is
2495 Subps
: constant Subprogram_List
:=
2496 Inherited_Subprograms
(Spec_Id
);
2500 Subp_Id
: Entity_Id
;
2503 -- Process the contract
2505 Items
:= Contract
(Spec_Id
);
2507 if Present
(Items
) then
2508 Prag
:= Pre_Post_Conditions
(Items
);
2509 while Present
(Prag
) loop
2510 if Pragma_Name
(Prag
) = Name_Postcondition
2511 and then Is_Checked
(Prag
)
2514 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2518 Prag
:= Next_Pragma
(Prag
);
2522 -- Process the contracts of all inherited subprograms, looking for
2523 -- class-wide postconditions.
2525 for Index
in Subps
'Range loop
2526 Subp_Id
:= Subps
(Index
);
2527 Items
:= Contract
(Subp_Id
);
2529 if Present
(Items
) then
2530 Prag
:= Pre_Post_Conditions
(Items
);
2531 while Present
(Prag
) loop
2532 if Pragma_Name
(Prag
) = Name_Postcondition
2533 and then Class_Present
(Prag
)
2536 Build_Pragma_Check_Equivalent
2539 Inher_Id
=> Subp_Id
);
2541 -- The pragma Check equivalent of the class-wide
2542 -- postcondition is still created even though the
2543 -- pragma may be ignored because the equivalent
2544 -- performs semantic checks.
2546 if Is_Checked
(Prag
) then
2547 Append_Enabled_Item
(Item
, Stmts
);
2551 Prag
:= Next_Pragma
(Prag
);
2555 end Process_Spec_Postconditions
;
2557 pragma Unmodified
(Stmts
);
2558 -- Stmts is passed as IN OUT to signal that the list can be updated,
2559 -- even if the corresponding integer value representing the list does
2562 -- Start of processing for Process_Postconditions
2565 -- The processing of postconditions is done in reverse order (body
2566 -- first) to ensure the following arrangement:
2568 -- <refined postconditions from body>
2569 -- <postconditions from body>
2570 -- <postconditions from spec>
2571 -- <inherited postconditions>
2573 Process_Body_Postconditions
(Name_Refined_Post
);
2574 Process_Body_Postconditions
(Name_Postcondition
);
2576 if Present
(Spec_Id
) then
2577 Process_Spec_Postconditions
;
2579 end Process_Postconditions
;
2581 ---------------------------
2582 -- Process_Preconditions --
2583 ---------------------------
2585 procedure Process_Preconditions
is
2586 Class_Pre
: Node_Id
:= Empty
;
2587 -- The sole [inherited] class-wide precondition pragma that applies
2588 -- to the subprogram.
2590 Insert_Node
: Node_Id
:= Empty
;
2591 -- The insertion node after which all pragma Check equivalents are
2594 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean;
2595 -- Determine whether arbitrary declaration Decl denotes a renaming of
2596 -- a discriminant or protection field _object.
2598 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
);
2599 -- Merge two class-wide preconditions by "or else"-ing them. The
2600 -- changes are accumulated in parameter Into. Update the error
2603 procedure Prepend_To_Decls
(Item
: Node_Id
);
2604 -- Prepend a single item to the declarations of the subprogram body
2606 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
);
2607 -- Save a class-wide precondition into Class_Pre, or prepend a normal
2608 -- precondition to the declarations of the body and analyze it.
2610 procedure Process_Inherited_Preconditions
;
2611 -- Collect all inherited class-wide preconditions and merge them into
2612 -- one big precondition to be evaluated as pragma Check.
2614 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
2615 -- Collect all preconditions of subprogram Subp_Id and prepend their
2616 -- pragma Check equivalents to the declarations of the body.
2618 --------------------------
2619 -- Is_Prologue_Renaming --
2620 --------------------------
2622 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
2629 if Nkind
(Decl
) = N_Object_Renaming_Declaration
then
2630 Obj
:= Defining_Entity
(Decl
);
2633 if Nkind
(Nam
) = N_Selected_Component
then
2634 Pref
:= Prefix
(Nam
);
2635 Sel
:= Selector_Name
(Nam
);
2637 -- A discriminant renaming appears as
2638 -- Discr : constant ... := Prefix.Discr;
2640 if Ekind
(Obj
) = E_Constant
2641 and then Is_Entity_Name
(Sel
)
2642 and then Present
(Entity
(Sel
))
2643 and then Ekind
(Entity
(Sel
)) = E_Discriminant
2647 -- A protection field renaming appears as
2648 -- Prot : ... := _object._object;
2650 -- A renamed private component is just a component of
2651 -- _object, with an arbitrary name.
2653 elsif Ekind
(Obj
) = E_Variable
2654 and then Nkind
(Pref
) = N_Identifier
2655 and then Chars
(Pref
) = Name_uObject
2656 and then Nkind
(Sel
) = N_Identifier
2664 end Is_Prologue_Renaming
;
2666 -------------------------
2667 -- Merge_Preconditions --
2668 -------------------------
2670 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
) is
2671 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
;
2672 -- Return the boolean expression argument of a precondition while
2673 -- updating its parentheses count for the subsequent merge.
2675 function Message_Arg
(Prag
: Node_Id
) return Node_Id
;
2676 -- Return the message argument of a precondition
2678 --------------------
2679 -- Expression_Arg --
2680 --------------------
2682 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
is
2683 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2684 Arg
: constant Node_Id
:= Get_Pragma_Arg
(Next
(First
(Args
)));
2687 if Paren_Count
(Arg
) = 0 then
2688 Set_Paren_Count
(Arg
, 1);
2698 function Message_Arg
(Prag
: Node_Id
) return Node_Id
is
2699 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2701 return Get_Pragma_Arg
(Last
(Args
));
2706 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
2707 From_Msg
: constant Node_Id
:= Message_Arg
(From
);
2708 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
2709 Into_Msg
: constant Node_Id
:= Message_Arg
(Into
);
2710 Loc
: constant Source_Ptr
:= Sloc
(Into
);
2712 -- Start of processing for Merge_Preconditions
2715 -- Merge the two preconditions by "or else"-ing them
2719 Right_Opnd
=> Relocate_Node
(Into_Expr
),
2720 Left_Opnd
=> From_Expr
));
2722 -- Merge the two error messages to produce a single message of the
2725 -- failed precondition from ...
2726 -- also failed inherited precondition from ...
2728 if not Exception_Locations_Suppressed
then
2729 Start_String
(Strval
(Into_Msg
));
2730 Store_String_Char
(ASCII
.LF
);
2731 Store_String_Chars
(" also ");
2732 Store_String_Chars
(Strval
(From_Msg
));
2734 Set_Strval
(Into_Msg
, End_String
);
2736 end Merge_Preconditions
;
2738 ----------------------
2739 -- Prepend_To_Decls --
2740 ----------------------
2742 procedure Prepend_To_Decls
(Item
: Node_Id
) is
2746 Decls
:= Declarations
(Body_Decl
);
2748 -- Ensure that the body has a declarative list
2752 Set_Declarations
(Body_Decl
, Decls
);
2755 Prepend_To
(Decls
, Item
);
2756 end Prepend_To_Decls
;
2758 ------------------------------
2759 -- Prepend_To_Decls_Or_Save --
2760 ------------------------------
2762 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
) is
2763 Check_Prag
: Node_Id
;
2766 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
2768 -- Save the sole class-wide precondition (if any) for the next
2769 -- step, where it will be merged with inherited preconditions.
2771 if Class_Present
(Prag
) then
2772 pragma Assert
(No
(Class_Pre
));
2773 Class_Pre
:= Check_Prag
;
2775 -- Accumulate the corresponding Check pragmas at the top of the
2776 -- declarations. Prepending the items ensures that they will be
2777 -- evaluated in their original order.
2780 if Present
(Insert_Node
) then
2781 Insert_After
(Insert_Node
, Check_Prag
);
2783 Prepend_To_Decls
(Check_Prag
);
2786 Analyze
(Check_Prag
);
2788 end Prepend_To_Decls_Or_Save
;
2790 -------------------------------------
2791 -- Process_Inherited_Preconditions --
2792 -------------------------------------
2794 procedure Process_Inherited_Preconditions
is
2795 Subps
: constant Subprogram_List
:=
2796 Inherited_Subprograms
(Spec_Id
);
2801 Subp_Id
: Entity_Id
;
2804 -- Process the contracts of all inherited subprograms, looking for
2805 -- class-wide preconditions.
2807 for Index
in Subps
'Range loop
2808 Subp_Id
:= Subps
(Index
);
2809 Items
:= Contract
(Subp_Id
);
2811 if Present
(Items
) then
2812 Prag
:= Pre_Post_Conditions
(Items
);
2813 while Present
(Prag
) loop
2814 if Pragma_Name
(Prag
) = Name_Precondition
2815 and then Class_Present
(Prag
)
2818 Build_Pragma_Check_Equivalent
2821 Inher_Id
=> Subp_Id
);
2823 -- The pragma Check equivalent of the class-wide
2824 -- precondition is still created even though the
2825 -- pragma may be ignored because the equivalent
2826 -- performs semantic checks.
2828 if Is_Checked
(Prag
) then
2830 -- The spec of an inherited subprogram already
2831 -- yielded a class-wide precondition. Merge the
2832 -- existing precondition with the current one
2835 if Present
(Class_Pre
) then
2836 Merge_Preconditions
(Item
, Class_Pre
);
2843 Prag
:= Next_Pragma
(Prag
);
2848 -- Add the merged class-wide preconditions
2850 if Present
(Class_Pre
) then
2851 Prepend_To_Decls
(Class_Pre
);
2852 Analyze
(Class_Pre
);
2854 end Process_Inherited_Preconditions
;
2856 -------------------------------
2857 -- Process_Preconditions_For --
2858 -------------------------------
2860 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
2861 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2862 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2868 -- Process the contract. If the body is an expression function
2869 -- that is a completion, freeze types within, because this may
2870 -- not have been done yet, when the subprogram declaration and
2871 -- its completion by an expression function appear in distinct
2872 -- declarative lists of the same unit (visible and private).
2875 Was_Expression_Function
(Body_Decl
)
2876 and then Sloc
(Body_Id
) /= Sloc
(Subp_Id
)
2877 and then In_Same_Source_Unit
(Body_Id
, Subp_Id
)
2878 and then List_Containing
(Body_Decl
) /=
2879 List_Containing
(Subp_Decl
)
2880 and then not In_Instance
;
2882 if Present
(Items
) then
2883 Prag
:= Pre_Post_Conditions
(Items
);
2884 while Present
(Prag
) loop
2885 if Pragma_Name
(Prag
) = Name_Precondition
2886 and then Is_Checked
(Prag
)
2889 and then Present
(Corresponding_Aspect
(Prag
))
2893 Typ
=> Standard_Boolean
,
2894 Expr
=> Expression
(Corresponding_Aspect
(Prag
)),
2898 Prepend_To_Decls_Or_Save
(Prag
);
2901 Prag
:= Next_Pragma
(Prag
);
2905 -- The subprogram declaration being processed is actually a body
2906 -- stub. The stub may carry a precondition pragma, in which case
2907 -- it must be taken into account. The pragma appears after the
2910 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
2912 -- Inspect the declarations following the body stub
2914 Decl
:= Next
(Subp_Decl
);
2915 while Present
(Decl
) loop
2917 -- Note that non-matching pragmas are skipped
2919 if Nkind
(Decl
) = N_Pragma
then
2920 if Pragma_Name
(Decl
) = Name_Precondition
2921 and then Is_Checked
(Decl
)
2923 Prepend_To_Decls_Or_Save
(Decl
);
2926 -- Skip internally generated code
2928 elsif not Comes_From_Source
(Decl
) then
2931 -- Preconditions are usually grouped together. There is no
2932 -- need to inspect the whole declarative list.
2941 end Process_Preconditions_For
;
2945 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2948 -- Start of processing for Process_Preconditions
2951 -- Find the proper insertion point for all pragma Check equivalents
2953 if Present
(Decls
) then
2954 Decl
:= First
(Decls
);
2955 while Present
(Decl
) loop
2957 -- First source declaration terminates the search, because all
2958 -- preconditions must be evaluated prior to it, by definition.
2960 if Comes_From_Source
(Decl
) then
2963 -- Certain internally generated object renamings such as those
2964 -- for discriminants and protection fields must be elaborated
2965 -- before the preconditions are evaluated, as their expressions
2966 -- may mention the discriminants. The renamings include those
2967 -- for private components so we need to find the last such.
2969 elsif Is_Prologue_Renaming
(Decl
) then
2970 while Present
(Next
(Decl
))
2971 and then Is_Prologue_Renaming
(Next
(Decl
))
2976 Insert_Node
:= Decl
;
2978 -- Otherwise the declaration does not come from source. This
2979 -- also terminates the search, because internal code may raise
2980 -- exceptions which should not preempt the preconditions.
2990 -- The processing of preconditions is done in reverse order (body
2991 -- first), because each pragma Check equivalent is inserted at the
2992 -- top of the declarations. This ensures that the final order is
2993 -- consistent with following diagram:
2995 -- <inherited preconditions>
2996 -- <preconditions from spec>
2997 -- <preconditions from body>
2999 Process_Preconditions_For
(Body_Id
);
3001 if Present
(Spec_Id
) then
3002 Process_Preconditions_For
(Spec_Id
);
3003 Process_Inherited_Preconditions
;
3005 end Process_Preconditions
;
3009 Restore_Scope
: Boolean := False;
3011 Stmts
: List_Id
:= No_List
;
3012 Subp_Id
: Entity_Id
;
3014 -- Start of processing for Expand_Subprogram_Contract
3017 -- Obtain the entity of the initial declaration
3019 if Present
(Spec_Id
) then
3025 -- Do not perform expansion activity when it is not needed
3027 if not Expander_Active
then
3030 -- ASIS requires an unaltered tree
3032 elsif ASIS_Mode
then
3035 -- GNATprove does not need the executable semantics of a contract
3037 elsif GNATprove_Mode
then
3040 -- The contract of a generic subprogram or one declared in a generic
3041 -- context is not expanded, as the corresponding instance will provide
3042 -- the executable semantics of the contract.
3044 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
3047 -- All subprograms carry a contract, but for some it is not significant
3048 -- and should not be processed. This is a small optimization.
3050 elsif not Has_Significant_Contract
(Subp_Id
) then
3053 -- The contract of an ignored Ghost subprogram does not need expansion,
3054 -- because the subprogram and all calls to it will be removed.
3056 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
3059 -- Do not re-expand the same contract. This scenario occurs when a
3060 -- construct is rewritten into something else during its analysis
3061 -- (expression functions for instance).
3063 elsif Has_Expanded_Contract
(Subp_Id
) then
3067 -- Prevent multiple expansion attempts of the same contract
3069 Set_Has_Expanded_Contract
(Subp_Id
);
3071 -- Ensure that the formal parameters are visible when expanding all
3074 if not In_Open_Scopes
(Subp_Id
) then
3075 Restore_Scope
:= True;
3076 Push_Scope
(Subp_Id
);
3078 if Is_Generic_Subprogram
(Subp_Id
) then
3079 Install_Generic_Formals
(Subp_Id
);
3081 Install_Formals
(Subp_Id
);
3085 -- The expansion of a subprogram contract involves the creation of Check
3086 -- pragmas to verify the contract assertions of the spec and body in a
3087 -- particular order. The order is as follows:
3089 -- function Example (...) return ... is
3090 -- procedure _Postconditions (...) is
3092 -- <refined postconditions from body>
3093 -- <postconditions from body>
3094 -- <postconditions from spec>
3095 -- <inherited postconditions>
3096 -- <contract case consequences>
3097 -- <invariant check of function result>
3098 -- <invariant and predicate checks of parameters>
3099 -- end _Postconditions;
3101 -- <inherited preconditions>
3102 -- <preconditions from spec>
3103 -- <preconditions from body>
3104 -- <contract case conditions>
3106 -- <source declarations>
3108 -- <source statements>
3110 -- _Preconditions (Result);
3114 -- Routine _Postconditions holds all contract assertions that must be
3115 -- verified on exit from the related subprogram.
3117 -- Step 1: Handle all preconditions. This action must come before the
3118 -- processing of pragma Contract_Cases because the pragma prepends items
3119 -- to the body declarations.
3121 Process_Preconditions
;
3123 -- Step 2: Handle all postconditions. This action must come before the
3124 -- processing of pragma Contract_Cases because the pragma appends items
3127 Process_Postconditions
(Stmts
);
3129 -- Step 3: Handle pragma Contract_Cases. This action must come before
3130 -- the processing of invariants and predicates because those append
3131 -- items to list Stmts.
3133 Process_Contract_Cases
(Stmts
);
3135 -- Step 4: Apply invariant and predicate checks on a function result and
3136 -- all formals. The resulting checks are accumulated in list Stmts.
3138 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3140 -- Step 5: Construct procedure _Postconditions
3142 Build_Postconditions_Procedure
(Subp_Id
, Stmts
, Result
);
3144 if Restore_Scope
then
3147 end Expand_Subprogram_Contract
;
3149 -------------------------------
3150 -- Freeze_Previous_Contracts --
3151 -------------------------------
3153 procedure Freeze_Previous_Contracts
(Body_Decl
: Node_Id
) is
3154 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean;
3155 pragma Inline
(Causes_Contract_Freezing
);
3156 -- Determine whether arbitrary node N causes contract freezing
3158 procedure Freeze_Contracts
;
3159 pragma Inline
(Freeze_Contracts
);
3160 -- Freeze the contracts of all eligible constructs which precede body
3163 procedure Freeze_Enclosing_Package_Body
;
3164 pragma Inline
(Freeze_Enclosing_Package_Body
);
3165 -- Freeze the contract of the nearest package body (if any) which
3166 -- encloses body Body_Decl.
3168 ------------------------------
3169 -- Causes_Contract_Freezing --
3170 ------------------------------
3172 function Causes_Contract_Freezing
(N
: Node_Id
) return Boolean is
3174 return Nkind_In
(N
, N_Entry_Body
,
3178 N_Subprogram_Body_Stub
,
3180 end Causes_Contract_Freezing
;
3182 ----------------------
3183 -- Freeze_Contracts --
3184 ----------------------
3186 procedure Freeze_Contracts
is
3187 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3191 -- Nothing to do when the body which causes freezing does not appear
3192 -- in a declarative list because there cannot possibly be constructs
3195 if not Is_List_Member
(Body_Decl
) then
3199 -- Inspect the declarations preceding the body, and freeze individual
3200 -- contracts of eligible constructs.
3202 Decl
:= Prev
(Body_Decl
);
3203 while Present
(Decl
) loop
3205 -- Stop the traversal when a preceding construct that causes
3206 -- freezing is encountered as there is no point in refreezing
3207 -- the already frozen constructs.
3209 if Causes_Contract_Freezing
(Decl
) then
3212 -- Entry or subprogram declarations
3214 elsif Nkind_In
(Decl
, N_Abstract_Subprogram_Declaration
,
3215 N_Entry_Declaration
,
3216 N_Generic_Subprogram_Declaration
,
3217 N_Subprogram_Declaration
)
3219 Analyze_Entry_Or_Subprogram_Contract
3220 (Subp_Id
=> Defining_Entity
(Decl
),
3221 Freeze_Id
=> Body_Id
);
3225 elsif Nkind
(Decl
) = N_Object_Declaration
then
3226 Analyze_Object_Contract
3227 (Obj_Id
=> Defining_Entity
(Decl
),
3228 Freeze_Id
=> Body_Id
);
3232 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
3233 N_Single_Protected_Declaration
)
3235 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
3237 -- Subprogram body stubs
3239 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
3240 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
3244 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
3245 N_Task_Type_Declaration
)
3247 Analyze_Task_Contract
(Defining_Entity
(Decl
));
3252 end Freeze_Contracts
;
3254 -----------------------------------
3255 -- Freeze_Enclosing_Package_Body --
3256 -----------------------------------
3258 procedure Freeze_Enclosing_Package_Body
is
3259 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
3263 -- Climb the parent chain looking for an enclosing package body. Do
3264 -- not use the scope stack, because a body utilizes the entity of its
3265 -- corresponding spec.
3267 Par
:= Parent
(Body_Decl
);
3268 while Present
(Par
) loop
3269 if Nkind
(Par
) = N_Package_Body
then
3270 Analyze_Package_Body_Contract
3271 (Body_Id
=> Defining_Entity
(Par
),
3272 Freeze_Id
=> Defining_Entity
(Body_Decl
));
3276 -- Do not look for an enclosing package body when the construct
3277 -- which causes freezing is a body generated for an expression
3278 -- function and it appears within a package spec. This ensures
3279 -- that the traversal will not reach too far up the parent chain
3280 -- and attempt to freeze a package body which must not be frozen.
3282 -- package body Enclosing_Body
3283 -- with Refined_State => (State => Var)
3285 -- package Nested is
3286 -- type Some_Type is ...;
3287 -- function Cause_Freezing return ...;
3289 -- function Cause_Freezing is (...);
3292 -- Var : Nested.Some_Type;
3294 elsif Nkind
(Par
) = N_Package_Declaration
3295 and then Nkind
(Orig_Decl
) = N_Expression_Function
3299 -- Prevent the search from going too far
3301 elsif Is_Body_Or_Package_Declaration
(Par
) then
3305 Par
:= Parent
(Par
);
3307 end Freeze_Enclosing_Package_Body
;
3311 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
3313 -- Start of processing for Freeze_Previous_Contracts
3316 pragma Assert
(Causes_Contract_Freezing
(Body_Decl
));
3318 -- A body that is in the process of being inlined appears from source,
3319 -- but carries name _parent. Such a body does not cause freezing of
3322 if Chars
(Body_Id
) = Name_uParent
then
3326 Freeze_Enclosing_Package_Body
;
3328 end Freeze_Previous_Contracts
;
3330 ---------------------------------
3331 -- Inherit_Subprogram_Contract --
3332 ---------------------------------
3334 procedure Inherit_Subprogram_Contract
3336 From_Subp
: Entity_Id
)
3338 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3339 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3342 --------------------
3343 -- Inherit_Pragma --
3344 --------------------
3346 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3347 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3351 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3352 -- chains, therefore the node must be replicated. The new pragma is
3353 -- flagged as inherited for distinction purposes.
3355 if Present
(Prag
) then
3356 New_Prag
:= New_Copy_Tree
(Prag
);
3357 Set_Is_Inherited_Pragma
(New_Prag
);
3359 Add_Contract_Item
(New_Prag
, Subp
);
3363 -- Start of processing for Inherit_Subprogram_Contract
3366 -- Inheritance is carried out only when both entities are subprograms
3369 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3370 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3371 and then Present
(Contract
(From_Subp
))
3373 Inherit_Pragma
(Pragma_Extensions_Visible
);
3375 end Inherit_Subprogram_Contract
;
3377 -------------------------------------
3378 -- Instantiate_Subprogram_Contract --
3379 -------------------------------------
3381 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3382 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3383 -- Instantiate all contract-related source pragmas found in the list,
3384 -- starting with pragma First_Prag. Each instantiated pragma is added
3387 -------------------------
3388 -- Instantiate_Pragmas --
3389 -------------------------
3391 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3392 Inst_Prag
: Node_Id
;
3397 while Present
(Prag
) loop
3398 if Is_Generic_Contract_Pragma
(Prag
) then
3400 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3402 Set_Analyzed
(Inst_Prag
, False);
3403 Append_To
(L
, Inst_Prag
);
3406 Prag
:= Next_Pragma
(Prag
);
3408 end Instantiate_Pragmas
;
3412 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3414 -- Start of processing for Instantiate_Subprogram_Contract
3417 if Present
(Items
) then
3418 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3419 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3420 Instantiate_Pragmas
(Classifications
(Items
));
3422 end Instantiate_Subprogram_Contract
;
3424 ----------------------------------------
3425 -- Save_Global_References_In_Contract --
3426 ----------------------------------------
3428 procedure Save_Global_References_In_Contract
3432 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
3433 -- Save all global references in contract-related source pragmas found
3434 -- in the list, starting with pragma First_Prag.
3436 ------------------------------------
3437 -- Save_Global_References_In_List --
3438 ------------------------------------
3440 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
3445 while Present
(Prag
) loop
3446 if Is_Generic_Contract_Pragma
(Prag
) then
3447 Save_Global_References
(Prag
);
3450 Prag
:= Next_Pragma
(Prag
);
3452 end Save_Global_References_In_List
;
3456 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3458 -- Start of processing for Save_Global_References_In_Contract
3461 -- The entity of the analyzed generic copy must be on the scope stack
3462 -- to ensure proper detection of global references.
3464 Push_Scope
(Gen_Id
);
3466 if Permits_Aspect_Specifications
(Templ
)
3467 and then Has_Aspects
(Templ
)
3469 Save_Global_References_In_Aspects
(Templ
);
3472 if Present
(Items
) then
3473 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
3474 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
3475 Save_Global_References_In_List
(Classifications
(Items
));
3479 end Save_Global_References_In_Contract
;