1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- C O N T R A C T S --
9 -- Copyright (C) 2015-2017, Free Software Foundation, Inc. --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
26 with Aspects
; use Aspects
;
27 with Atree
; use Atree
;
28 with Debug
; use Debug
;
29 with Einfo
; use Einfo
;
30 with Elists
; use Elists
;
31 with Errout
; use Errout
;
32 with Exp_Prag
; use Exp_Prag
;
33 with Exp_Tss
; use Exp_Tss
;
34 with Exp_Util
; use Exp_Util
;
35 with Namet
; use Namet
;
36 with Nlists
; use Nlists
;
37 with Nmake
; use Nmake
;
40 with Sem_Aux
; use Sem_Aux
;
41 with Sem_Ch6
; use Sem_Ch6
;
42 with Sem_Ch8
; use Sem_Ch8
;
43 with Sem_Ch12
; use Sem_Ch12
;
44 with Sem_Ch13
; use Sem_Ch13
;
45 with Sem_Disp
; use Sem_Disp
;
46 with Sem_Prag
; use Sem_Prag
;
47 with Sem_Util
; use Sem_Util
;
48 with Sinfo
; use Sinfo
;
49 with Snames
; use Snames
;
50 with Stringt
; use Stringt
;
51 with SCIL_LL
; use SCIL_LL
;
52 with Tbuild
; use Tbuild
;
54 package body Contracts
is
56 procedure Analyze_Contracts
59 Freeze_Id
: Entity_Id
);
60 -- Subsidiary to the one parameter version of Analyze_Contracts and routine
61 -- Analyze_Previous_Constracts. Analyze the contracts of all constructs in
62 -- the list L. If Freeze_Nod is set, then the analysis stops when the node
63 -- is reached. Freeze_Id is the entity of some related context which caused
64 -- freezing up to node Freeze_Nod.
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
355 if CodePeer_Mode
and then Debug_Flag_Dot_KK
then
356 Build_And_Analyze_Contract_Only_Subprograms
(L
);
359 Analyze_Contracts
(L
, Freeze_Nod
=> Empty
, Freeze_Id
=> Empty
);
360 end Analyze_Contracts
;
362 procedure Analyze_Contracts
364 Freeze_Nod
: Node_Id
;
365 Freeze_Id
: Entity_Id
)
371 while Present
(Decl
) loop
373 -- The caller requests that the traversal stops at a particular node
374 -- that causes contract "freezing".
376 if Present
(Freeze_Nod
) and then Decl
= Freeze_Nod
then
380 -- Entry or subprogram declarations
382 if Nkind_In
(Decl
, N_Abstract_Subprogram_Declaration
,
384 N_Generic_Subprogram_Declaration
,
385 N_Subprogram_Declaration
)
388 Subp_Id
: constant Entity_Id
:= Defining_Entity
(Decl
);
391 Analyze_Entry_Or_Subprogram_Contract
(Subp_Id
, Freeze_Id
);
393 -- If analysis of a class-wide pre/postcondition indicates
394 -- that a class-wide clone is needed, analyze its declaration
395 -- now. Its body is created when the body of the original
396 -- operation is analyzed (and rewritten).
398 if Is_Subprogram
(Subp_Id
)
399 and then Present
(Class_Wide_Clone
(Subp_Id
))
401 Analyze
(Unit_Declaration_Node
(Class_Wide_Clone
(Subp_Id
)));
405 -- Entry or subprogram bodies
407 elsif Nkind_In
(Decl
, N_Entry_Body
, N_Subprogram_Body
) then
408 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
412 elsif Nkind
(Decl
) = N_Object_Declaration
then
413 Analyze_Object_Contract
414 (Obj_Id
=> Defining_Entity
(Decl
),
415 Freeze_Id
=> Freeze_Id
);
419 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
420 N_Single_Protected_Declaration
)
422 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
424 -- Subprogram body stubs
426 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
427 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
431 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
432 N_Task_Type_Declaration
)
434 Analyze_Task_Contract
(Defining_Entity
(Decl
));
436 -- For type declarations, we need to do the pre-analysis of
437 -- Iterable aspect specifications.
438 -- Other type aspects need to be resolved here???
440 elsif Nkind
(Decl
) = N_Private_Type_Declaration
441 and then Present
(Aspect_Specifications
(Decl
))
444 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
445 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
448 Validate_Iterable_Aspect
(E
, It
);
455 end Analyze_Contracts
;
457 -----------------------------------------------
458 -- Analyze_Entry_Or_Subprogram_Body_Contract --
459 -----------------------------------------------
461 -- WARNING: This routine manages SPARK regions. Return statements must be
462 -- replaced by gotos which jump to the end of the routine and restore the
465 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
466 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
467 Items
: constant Node_Id
:= Contract
(Body_Id
);
468 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
470 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
471 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
472 -- Save the SPARK_Mode-related data to restore on exit
475 -- When a subprogram body declaration is illegal, its defining entity is
476 -- left unanalyzed. There is nothing left to do in this case because the
477 -- body lacks a contract, or even a proper Ekind.
479 if Ekind
(Body_Id
) = E_Void
then
482 -- Do not analyze a contract multiple times
484 elsif Present
(Items
) then
485 if Analyzed
(Items
) then
488 Set_Analyzed
(Items
);
492 -- Due to the timing of contract analysis, delayed pragmas may be
493 -- subject to the wrong SPARK_Mode, usually that of the enclosing
494 -- context. To remedy this, restore the original SPARK_Mode of the
495 -- related subprogram body.
497 Set_SPARK_Mode
(Body_Id
);
499 -- Ensure that the contract cases or postconditions mention 'Result or
500 -- define a post-state.
502 Check_Result_And_Post_State
(Body_Id
);
504 -- A stand-alone nonvolatile function body cannot have an effectively
505 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
506 -- check is relevant only when SPARK_Mode is on, as it is not a standard
507 -- legality rule. The check is performed here because Volatile_Function
508 -- is processed after the analysis of the related subprogram body. The
509 -- check only applies to source subprograms and not to generated TSS
513 and then Ekind_In
(Body_Id
, E_Function
, E_Generic_Function
)
514 and then Comes_From_Source
(Spec_Id
)
515 and then not Is_Volatile_Function
(Body_Id
)
517 Check_Nonvolatile_Function_Profile
(Body_Id
);
520 -- Restore the SPARK_Mode of the enclosing context after all delayed
521 -- pragmas have been analyzed.
523 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
525 -- Capture all global references in a generic subprogram body now that
526 -- the contract has been analyzed.
528 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
529 Save_Global_References_In_Contract
530 (Templ
=> Original_Node
(Body_Decl
),
534 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
535 -- invariants and predicates associated with body and its spec. Do not
536 -- expand the contract of subprogram body stubs.
538 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
539 Expand_Subprogram_Contract
(Body_Id
);
541 end Analyze_Entry_Or_Subprogram_Body_Contract
;
543 ------------------------------------------
544 -- Analyze_Entry_Or_Subprogram_Contract --
545 ------------------------------------------
547 -- WARNING: This routine manages SPARK regions. Return statements must be
548 -- replaced by gotos which jump to the end of the routine and restore the
551 procedure Analyze_Entry_Or_Subprogram_Contract
552 (Subp_Id
: Entity_Id
;
553 Freeze_Id
: Entity_Id
:= Empty
)
555 Items
: constant Node_Id
:= Contract
(Subp_Id
);
556 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
558 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
559 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
560 -- Save the SPARK_Mode-related data to restore on exit
562 Skip_Assert_Exprs
: constant Boolean :=
563 Ekind_In
(Subp_Id
, E_Entry
, E_Entry_Family
)
564 and then not ASIS_Mode
565 and then not GNATprove_Mode
;
567 Depends
: Node_Id
:= Empty
;
568 Global
: Node_Id
:= Empty
;
573 -- Do not analyze a contract multiple times
575 if Present
(Items
) then
576 if Analyzed
(Items
) then
579 Set_Analyzed
(Items
);
583 -- Due to the timing of contract analysis, delayed pragmas may be
584 -- subject to the wrong SPARK_Mode, usually that of the enclosing
585 -- context. To remedy this, restore the original SPARK_Mode of the
586 -- related subprogram body.
588 Set_SPARK_Mode
(Subp_Id
);
590 -- All subprograms carry a contract, but for some it is not significant
591 -- and should not be processed.
593 if not Has_Significant_Contract
(Subp_Id
) then
596 elsif Present
(Items
) then
598 -- Do not analyze the pre/postconditions of an entry declaration
599 -- unless annotating the original tree for ASIS or GNATprove. The
600 -- real analysis occurs when the pre/postconditons are relocated to
601 -- the contract wrapper procedure (see Build_Contract_Wrapper).
603 if Skip_Assert_Exprs
then
606 -- Otherwise analyze the pre/postconditions
609 Prag
:= Pre_Post_Conditions
(Items
);
610 while Present
(Prag
) loop
611 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
612 Prag
:= Next_Pragma
(Prag
);
616 -- Analyze contract-cases and test-cases
618 Prag
:= Contract_Test_Cases
(Items
);
619 while Present
(Prag
) loop
620 Prag_Nam
:= Pragma_Name
(Prag
);
622 if Prag_Nam
= Name_Contract_Cases
then
624 -- Do not analyze the contract cases of an entry declaration
625 -- unless annotating the original tree for ASIS or GNATprove.
626 -- The real analysis occurs when the contract cases are moved
627 -- to the contract wrapper procedure (Build_Contract_Wrapper).
629 if Skip_Assert_Exprs
then
632 -- Otherwise analyze the contract cases
635 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
638 pragma Assert
(Prag_Nam
= Name_Test_Case
);
639 Analyze_Test_Case_In_Decl_Part
(Prag
);
642 Prag
:= Next_Pragma
(Prag
);
645 -- Analyze classification pragmas
647 Prag
:= Classifications
(Items
);
648 while Present
(Prag
) loop
649 Prag_Nam
:= Pragma_Name
(Prag
);
651 if Prag_Nam
= Name_Depends
then
654 elsif Prag_Nam
= Name_Global
then
658 Prag
:= Next_Pragma
(Prag
);
661 -- Analyze Global first, as Depends may mention items classified in
662 -- the global categorization.
664 if Present
(Global
) then
665 Analyze_Global_In_Decl_Part
(Global
);
668 -- Depends must be analyzed after Global in order to see the modes of
671 if Present
(Depends
) then
672 Analyze_Depends_In_Decl_Part
(Depends
);
675 -- Ensure that the contract cases or postconditions mention 'Result
676 -- or define a post-state.
678 Check_Result_And_Post_State
(Subp_Id
);
681 -- A nonvolatile function cannot have an effectively volatile formal
682 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
683 -- only when SPARK_Mode is on, as it is not a standard legality rule.
684 -- The check is performed here because pragma Volatile_Function is
685 -- processed after the analysis of the related subprogram declaration.
688 and then Ekind_In
(Subp_Id
, E_Function
, E_Generic_Function
)
689 and then Comes_From_Source
(Subp_Id
)
690 and then not Is_Volatile_Function
(Subp_Id
)
692 Check_Nonvolatile_Function_Profile
(Subp_Id
);
695 -- Restore the SPARK_Mode of the enclosing context after all delayed
696 -- pragmas have been analyzed.
698 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
700 -- Capture all global references in a generic subprogram now that the
701 -- contract has been analyzed.
703 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
704 Save_Global_References_In_Contract
705 (Templ
=> Original_Node
(Subp_Decl
),
708 end Analyze_Entry_Or_Subprogram_Contract
;
710 -----------------------------
711 -- Analyze_Object_Contract --
712 -----------------------------
714 -- WARNING: This routine manages SPARK regions. Return statements must be
715 -- replaced by gotos which jump to the end of the routine and restore the
718 procedure Analyze_Object_Contract
720 Freeze_Id
: Entity_Id
:= Empty
)
722 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
724 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
725 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
726 -- Save the SPARK_Mode-related data to restore on exit
728 AR_Val
: Boolean := False;
729 AW_Val
: Boolean := False;
730 ER_Val
: Boolean := False;
731 EW_Val
: Boolean := False;
735 Seen
: Boolean := False;
738 -- The loop parameter in an element iterator over a formal container
739 -- is declared with an object declaration, but no contracts apply.
741 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
745 -- Do not analyze a contract multiple times
747 Items
:= Contract
(Obj_Id
);
749 if Present
(Items
) then
750 if Analyzed
(Items
) then
753 Set_Analyzed
(Items
);
757 -- The anonymous object created for a single concurrent type inherits
758 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
759 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
760 -- of the enclosing context. To remedy this, restore the original mode
761 -- of the related anonymous object.
763 if Is_Single_Concurrent_Object
(Obj_Id
)
764 and then Present
(SPARK_Pragma
(Obj_Id
))
766 Set_SPARK_Mode
(Obj_Id
);
769 -- Constant-related checks
771 if Ekind
(Obj_Id
) = E_Constant
then
773 -- Analyze indicator Part_Of
775 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
777 -- Check whether the lack of indicator Part_Of agrees with the
778 -- placement of the constant with respect to the state space.
781 Check_Missing_Part_Of
(Obj_Id
);
784 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
785 -- This check is relevant only when SPARK_Mode is on, as it is not
786 -- a standard Ada legality rule. Internally-generated constants that
787 -- map generic formals to actuals in instantiations are allowed to
791 and then Comes_From_Source
(Obj_Id
)
792 and then Is_Effectively_Volatile
(Obj_Id
)
793 and then No
(Corresponding_Generic_Association
(Parent
(Obj_Id
)))
795 Error_Msg_N
("constant cannot be volatile", Obj_Id
);
798 -- Variable-related checks
800 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
802 -- Analyze all external properties
804 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Readers
);
806 if Present
(Prag
) then
807 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
811 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Writers
);
813 if Present
(Prag
) then
814 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
818 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Reads
);
820 if Present
(Prag
) then
821 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
825 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Writes
);
827 if Present
(Prag
) then
828 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
832 -- Verify the mutual interaction of the various external properties
835 Check_External_Properties
(Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
838 -- The anonymous object created for a single concurrent type carries
839 -- pragmas Depends and Globat of the type.
841 if Is_Single_Concurrent_Object
(Obj_Id
) then
843 -- Analyze Global first, as Depends may mention items classified
844 -- in the global categorization.
846 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
848 if Present
(Prag
) then
849 Analyze_Global_In_Decl_Part
(Prag
);
852 -- Depends must be analyzed after Global in order to see the modes
853 -- of all global items.
855 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
857 if Present
(Prag
) then
858 Analyze_Depends_In_Decl_Part
(Prag
);
862 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
864 -- Analyze indicator Part_Of
866 if Present
(Prag
) then
867 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
869 -- The variable is a constituent of a single protected/task type
870 -- and behaves as a component of the type. Verify that references
871 -- to the variable occur within the definition or body of the type
874 if Present
(Encapsulating_State
(Obj_Id
))
875 and then Is_Single_Concurrent_Object
876 (Encapsulating_State
(Obj_Id
))
877 and then Present
(Part_Of_References
(Obj_Id
))
879 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
880 while Present
(Ref_Elmt
) loop
881 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
882 Next_Elmt
(Ref_Elmt
);
886 -- Otherwise check whether the lack of indicator Part_Of agrees with
887 -- the placement of the variable with respect to the state space.
890 Check_Missing_Part_Of
(Obj_Id
);
893 -- The following checks are relevant only when SPARK_Mode is on, as
894 -- they are not standard Ada legality rules. Internally generated
895 -- temporaries are ignored.
897 if SPARK_Mode
= On
and then Comes_From_Source
(Obj_Id
) then
898 if Is_Effectively_Volatile
(Obj_Id
) then
900 -- The declaration of an effectively volatile object must
901 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
903 if not Is_Library_Level_Entity
(Obj_Id
) then
905 ("volatile variable & must be declared at library level",
908 -- An object of a discriminated type cannot be effectively
909 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
911 elsif Has_Discriminants
(Obj_Typ
)
912 and then not Is_Protected_Type
(Obj_Typ
)
915 ("discriminated object & cannot be volatile", Obj_Id
);
918 -- The object is not effectively volatile
921 -- A non-effectively volatile object cannot have effectively
922 -- volatile components (SPARK RM 7.1.3(6)).
924 if not Is_Effectively_Volatile
(Obj_Id
)
925 and then Has_Volatile_Component
(Obj_Typ
)
928 ("non-volatile object & cannot have volatile components",
937 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
939 -- A Ghost object cannot be of a type that yields a synchronized
940 -- object (SPARK RM 6.9(19)).
942 if Yields_Synchronized_Object
(Obj_Typ
) then
943 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
945 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
946 -- SPARK RM 6.9(19)).
948 elsif Is_Effectively_Volatile
(Obj_Id
) then
949 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
951 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
952 -- One exception to this is the object that represents the dispatch
953 -- table of a Ghost tagged type, as the symbol needs to be exported.
955 elsif Is_Exported
(Obj_Id
) then
956 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
958 elsif Is_Imported
(Obj_Id
) then
959 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
963 -- Restore the SPARK_Mode of the enclosing context after all delayed
964 -- pragmas have been analyzed.
966 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
967 end Analyze_Object_Contract
;
969 -----------------------------------
970 -- Analyze_Package_Body_Contract --
971 -----------------------------------
973 -- WARNING: This routine manages SPARK regions. Return statements must be
974 -- replaced by gotos which jump to the end of the routine and restore the
977 procedure Analyze_Package_Body_Contract
978 (Body_Id
: Entity_Id
;
979 Freeze_Id
: Entity_Id
:= Empty
)
981 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
982 Items
: constant Node_Id
:= Contract
(Body_Id
);
983 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
985 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
986 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
987 -- Save the SPARK_Mode-related data to restore on exit
992 -- Do not analyze a contract multiple times
994 if Present
(Items
) then
995 if Analyzed
(Items
) then
998 Set_Analyzed
(Items
);
1002 -- Due to the timing of contract analysis, delayed pragmas may be
1003 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1004 -- context. To remedy this, restore the original SPARK_Mode of the
1005 -- related package body.
1007 Set_SPARK_Mode
(Body_Id
);
1009 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
1011 -- The analysis of pragma Refined_State detects whether the spec has
1012 -- abstract states available for refinement.
1014 if Present
(Ref_State
) then
1015 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
1018 -- Restore the SPARK_Mode of the enclosing context after all delayed
1019 -- pragmas have been analyzed.
1021 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1023 -- Capture all global references in a generic package body now that the
1024 -- contract has been analyzed.
1026 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
1027 Save_Global_References_In_Contract
1028 (Templ
=> Original_Node
(Body_Decl
),
1031 end Analyze_Package_Body_Contract
;
1033 ------------------------------
1034 -- Analyze_Package_Contract --
1035 ------------------------------
1037 -- WARNING: This routine manages SPARK regions. Return statements must be
1038 -- replaced by gotos which jump to the end of the routine and restore the
1041 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1042 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1043 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1045 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1046 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1047 -- Save the SPARK_Mode-related data to restore on exit
1049 Init
: Node_Id
:= Empty
;
1050 Init_Cond
: Node_Id
:= Empty
;
1055 -- Do not analyze a contract multiple times
1057 if Present
(Items
) then
1058 if Analyzed
(Items
) then
1061 Set_Analyzed
(Items
);
1065 -- Due to the timing of contract analysis, delayed pragmas may be
1066 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1067 -- context. To remedy this, restore the original SPARK_Mode of the
1070 Set_SPARK_Mode
(Pack_Id
);
1072 if Present
(Items
) then
1074 -- Locate and store pragmas Initial_Condition and Initializes, since
1075 -- their order of analysis matters.
1077 Prag
:= Classifications
(Items
);
1078 while Present
(Prag
) loop
1079 Prag_Nam
:= Pragma_Name
(Prag
);
1081 if Prag_Nam
= Name_Initial_Condition
then
1084 elsif Prag_Nam
= Name_Initializes
then
1088 Prag
:= Next_Pragma
(Prag
);
1091 -- Analyze the initialization-related pragmas. Initializes must come
1092 -- before Initial_Condition due to item dependencies.
1094 if Present
(Init
) then
1095 Analyze_Initializes_In_Decl_Part
(Init
);
1098 if Present
(Init_Cond
) then
1099 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1103 -- Check whether the lack of indicator Part_Of agrees with the placement
1104 -- of the package instantiation with respect to the state space.
1106 if Is_Generic_Instance
(Pack_Id
) then
1107 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1110 Check_Missing_Part_Of
(Pack_Id
);
1114 -- Restore the SPARK_Mode of the enclosing context after all delayed
1115 -- pragmas have been analyzed.
1117 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1119 -- Capture all global references in a generic package now that the
1120 -- contract has been analyzed.
1122 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1123 Save_Global_References_In_Contract
1124 (Templ
=> Original_Node
(Pack_Decl
),
1127 end Analyze_Package_Contract
;
1129 --------------------------------
1130 -- Analyze_Previous_Contracts --
1131 --------------------------------
1133 procedure Analyze_Previous_Contracts
(Body_Decl
: Node_Id
) is
1134 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
1135 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
1140 -- A body that is in the process of being inlined appears from source,
1141 -- but carries name _parent. Such a body does not cause "freezing" of
1144 if Chars
(Body_Id
) = Name_uParent
then
1148 -- Climb the parent chain looking for an enclosing package body. Do not
1149 -- use the scope stack, as a body uses the entity of its corresponding
1152 Par
:= Parent
(Body_Decl
);
1153 while Present
(Par
) loop
1154 if Nkind
(Par
) = N_Package_Body
then
1155 Analyze_Package_Body_Contract
1156 (Body_Id
=> Defining_Entity
(Par
),
1157 Freeze_Id
=> Defining_Entity
(Body_Decl
));
1161 -- Do not look for an enclosing package body when the construct which
1162 -- causes freezing is a body generated for an expression function and
1163 -- it appears within a package spec. This ensures that the traversal
1164 -- will not reach too far up the parent chain and attempt to freeze a
1165 -- package body which should not be frozen.
1167 -- package body Enclosing_Body
1168 -- with Refined_State => (State => Var)
1170 -- package Nested is
1171 -- type Some_Type is ...;
1172 -- function Cause_Freezing return ...;
1174 -- function Cause_Freezing is (...);
1177 -- Var : Nested.Some_Type;
1179 elsif Nkind
(Par
) = N_Package_Declaration
1180 and then Nkind
(Orig_Decl
) = N_Expression_Function
1185 Par
:= Parent
(Par
);
1188 -- Analyze the contracts of all eligible construct up to the body which
1189 -- caused the "freezing".
1191 if Is_List_Member
(Body_Decl
) then
1193 (L
=> List_Containing
(Body_Decl
),
1194 Freeze_Nod
=> Body_Decl
,
1195 Freeze_Id
=> Body_Id
);
1197 end Analyze_Previous_Contracts
;
1199 --------------------------------
1200 -- Analyze_Protected_Contract --
1201 --------------------------------
1203 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1204 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1207 -- Do not analyze a contract multiple times
1209 if Present
(Items
) then
1210 if Analyzed
(Items
) then
1213 Set_Analyzed
(Items
);
1216 end Analyze_Protected_Contract
;
1218 -------------------------------------------
1219 -- Analyze_Subprogram_Body_Stub_Contract --
1220 -------------------------------------------
1222 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1223 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1224 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1227 -- A subprogram body stub may act as its own spec or as the completion
1228 -- of a previous declaration. Depending on the context, the contract of
1229 -- the stub may contain two sets of pragmas.
1231 -- The stub is a completion, the applicable pragmas are:
1235 if Present
(Spec_Id
) then
1236 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1238 -- The stub acts as its own spec, the applicable pragmas are:
1247 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1249 end Analyze_Subprogram_Body_Stub_Contract
;
1251 ---------------------------
1252 -- Analyze_Task_Contract --
1253 ---------------------------
1255 -- WARNING: This routine manages SPARK regions. Return statements must be
1256 -- replaced by gotos which jump to the end of the routine and restore the
1259 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1260 Items
: constant Node_Id
:= Contract
(Task_Id
);
1262 Saved_SM
: constant SPARK_Mode_Type
:= SPARK_Mode
;
1263 Saved_SMP
: constant Node_Id
:= SPARK_Mode_Pragma
;
1264 -- Save the SPARK_Mode-related data to restore on exit
1269 -- Do not analyze a contract multiple times
1271 if Present
(Items
) then
1272 if Analyzed
(Items
) then
1275 Set_Analyzed
(Items
);
1279 -- Due to the timing of contract analysis, delayed pragmas may be
1280 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1281 -- context. To remedy this, restore the original SPARK_Mode of the
1282 -- related task unit.
1284 Set_SPARK_Mode
(Task_Id
);
1286 -- Analyze Global first, as Depends may mention items classified in the
1287 -- global categorization.
1289 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1291 if Present
(Prag
) then
1292 Analyze_Global_In_Decl_Part
(Prag
);
1295 -- Depends must be analyzed after Global in order to see the modes of
1296 -- all global items.
1298 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1300 if Present
(Prag
) then
1301 Analyze_Depends_In_Decl_Part
(Prag
);
1304 -- Restore the SPARK_Mode of the enclosing context after all delayed
1305 -- pragmas have been analyzed.
1307 Restore_SPARK_Mode
(Saved_SM
, Saved_SMP
);
1308 end Analyze_Task_Contract
;
1310 -------------------------------------------------
1311 -- Build_And_Analyze_Contract_Only_Subprograms --
1312 -------------------------------------------------
1314 procedure Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
) is
1315 procedure Analyze_Contract_Only_Subprograms
;
1316 -- Analyze the contract-only subprograms of L
1318 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
);
1319 -- Append the contract-only bodies of Subp_List to its declarations list
1321 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
;
1322 -- If E is an entity for a non-imported subprogram specification with
1323 -- pre/postconditions and we are compiling with CodePeer mode, then
1324 -- this procedure will create a wrapper to help Gnat2scil process its
1325 -- contracts. Return Empty if the wrapper cannot be built.
1327 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
;
1328 -- Build the contract-only subprograms of all eligible subprograms found
1331 function Has_Private_Declarations
(N
: Node_Id
) return Boolean;
1332 -- Return True for package specs, task definitions, and protected type
1333 -- definitions whose list of private declarations is not empty.
1335 ---------------------------------------
1336 -- Analyze_Contract_Only_Subprograms --
1337 ---------------------------------------
1339 procedure Analyze_Contract_Only_Subprograms
is
1340 procedure Analyze_Contract_Only_Bodies
;
1341 -- Analyze all the contract-only bodies of L
1343 ----------------------------------
1344 -- Analyze_Contract_Only_Bodies --
1345 ----------------------------------
1347 procedure Analyze_Contract_Only_Bodies
is
1352 while Present
(Decl
) loop
1353 if Nkind
(Decl
) = N_Subprogram_Body
1354 and then Is_Contract_Only_Body
1355 (Defining_Unit_Name
(Specification
(Decl
)))
1362 end Analyze_Contract_Only_Bodies
;
1364 -- Start of processing for Analyze_Contract_Only_Subprograms
1367 if Ekind
(Current_Scope
) /= E_Package
then
1368 Analyze_Contract_Only_Bodies
;
1372 Pkg_Spec
: constant Node_Id
:=
1373 Package_Specification
(Current_Scope
);
1376 if not Has_Private_Declarations
(Pkg_Spec
) then
1377 Analyze_Contract_Only_Bodies
;
1379 -- For packages with private declarations, the contract-only
1380 -- bodies of subprograms defined in the visible part of the
1381 -- package are added to its private declarations (to ensure
1382 -- that they do not cause premature freezing of types and also
1383 -- that they are analyzed with proper visibility). Hence they
1384 -- will be analyzed later.
1386 elsif Visible_Declarations
(Pkg_Spec
) = L
then
1389 elsif Private_Declarations
(Pkg_Spec
) = L
then
1390 Analyze_Contract_Only_Bodies
;
1394 end Analyze_Contract_Only_Subprograms
;
1396 --------------------------------------
1397 -- Append_Contract_Only_Subprograms --
1398 --------------------------------------
1400 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
) is
1402 if No
(Subp_List
) then
1406 if Ekind
(Current_Scope
) /= E_Package
then
1407 Append_List
(Subp_List
, To
=> L
);
1411 Pkg_Spec
: constant Node_Id
:=
1412 Package_Specification
(Current_Scope
);
1415 if not Has_Private_Declarations
(Pkg_Spec
) then
1416 Append_List
(Subp_List
, To
=> L
);
1418 -- If the package has private declarations then append them to
1419 -- its private declarations; they will be analyzed when the
1420 -- contracts of its private declarations are analyzed.
1425 To
=> Private_Declarations
(Pkg_Spec
));
1429 end Append_Contract_Only_Subprograms
;
1431 ------------------------------------
1432 -- Build_Contract_Only_Subprogram --
1433 ------------------------------------
1435 -- This procedure takes care of building a wrapper to generate better
1436 -- analysis results in the case of a call to a subprogram whose body
1437 -- is unavailable to CodePeer but whose specification includes Pre/Post
1438 -- conditions. The body might be unavailable for any of a number or
1439 -- reasons (it is imported, the .adb file is simply missing, or the
1440 -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
1441 -- pragma). The built subprogram has the following contents:
1442 -- * check preconditions
1443 -- * call the subprogram
1444 -- * check postconditions
1446 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
is
1447 Loc
: constant Source_Ptr
:= Sloc
(E
);
1449 Missing_Body_Name
: constant Name_Id
:=
1450 New_External_Name
(Chars
(E
), "__missing_body");
1452 function Build_Missing_Body_Decls
return List_Id
;
1453 -- Build the declaration of the missing body subprogram and its
1454 -- corresponding pragma Import.
1456 function Build_Missing_Body_Subprogram_Call
return Node_Id
;
1457 -- Build the call to the missing body subprogram
1459 function Skip_Contract_Only_Subprogram
(E
: Entity_Id
) return Boolean;
1460 -- Return True for cases where the wrapper is not needed or we cannot
1463 ------------------------------
1464 -- Build_Missing_Body_Decls --
1465 ------------------------------
1467 function Build_Missing_Body_Decls
return List_Id
is
1468 Spec
: constant Node_Id
:= Declaration_Node
(E
);
1474 Make_Subprogram_Declaration
(Loc
, Copy_Subprogram_Spec
(Spec
));
1475 Set_Chars
(Defining_Entity
(Decl
), Missing_Body_Name
);
1479 Chars
=> Name_Import
,
1480 Pragma_Argument_Associations
=> New_List
(
1481 Make_Pragma_Argument_Association
(Loc
,
1482 Expression
=> Make_Identifier
(Loc
, Name_Ada
)),
1484 Make_Pragma_Argument_Association
(Loc
,
1485 Expression
=> Make_Identifier
(Loc
, Missing_Body_Name
))));
1487 return New_List
(Decl
, Prag
);
1488 end Build_Missing_Body_Decls
;
1490 ----------------------------------------
1491 -- Build_Missing_Body_Subprogram_Call --
1492 ----------------------------------------
1494 function Build_Missing_Body_Subprogram_Call
return Node_Id
is
1501 -- Build parameter list that we need
1503 Forml
:= First_Formal
(E
);
1504 while Present
(Forml
) loop
1505 Append_To
(Parms
, Make_Identifier
(Loc
, Chars
(Forml
)));
1506 Next_Formal
(Forml
);
1509 -- Build the call to the missing body subprogram
1511 if Ekind_In
(E
, E_Function
, E_Generic_Function
) then
1513 Make_Simple_Return_Statement
(Loc
,
1515 Make_Function_Call
(Loc
,
1517 Make_Identifier
(Loc
, Missing_Body_Name
),
1518 Parameter_Associations
=> Parms
));
1522 Make_Procedure_Call_Statement
(Loc
,
1524 Make_Identifier
(Loc
, Missing_Body_Name
),
1525 Parameter_Associations
=> Parms
);
1527 end Build_Missing_Body_Subprogram_Call
;
1529 -----------------------------------
1530 -- Skip_Contract_Only_Subprogram --
1531 -----------------------------------
1533 function Skip_Contract_Only_Subprogram
1534 (E
: Entity_Id
) return Boolean
1536 function Depends_On_Enclosing_Private_Type
return Boolean;
1537 -- Return True if some formal of E (or its return type) are
1538 -- private types defined in an enclosing package.
1540 function Some_Enclosing_Package_Has_Private_Decls
return Boolean;
1541 -- Return True if some enclosing package of the current scope has
1542 -- private declarations.
1544 ---------------------------------------
1545 -- Depends_On_Enclosing_Private_Type --
1546 ---------------------------------------
1548 function Depends_On_Enclosing_Private_Type
return Boolean is
1549 function Defined_In_Enclosing_Package
1550 (Typ
: Entity_Id
) return Boolean;
1551 -- Return True if Typ is an entity defined in an enclosing
1552 -- package of the current scope.
1554 ----------------------------------
1555 -- Defined_In_Enclosing_Package --
1556 ----------------------------------
1558 function Defined_In_Enclosing_Package
1559 (Typ
: Entity_Id
) return Boolean
1561 Scop
: Entity_Id
:= Scope
(Current_Scope
);
1564 while Scop
/= Scope
(Typ
)
1565 and then not Is_Compilation_Unit
(Scop
)
1567 Scop
:= Scope
(Scop
);
1570 return Scop
= Scope
(Typ
);
1571 end Defined_In_Enclosing_Package
;
1575 Param_E
: Entity_Id
;
1578 -- Start of processing for Depends_On_Enclosing_Private_Type
1581 Param_E
:= First_Entity
(E
);
1582 while Present
(Param_E
) loop
1583 Typ
:= Etype
(Param_E
);
1585 if Is_Private_Type
(Typ
)
1586 and then Defined_In_Enclosing_Package
(Typ
)
1591 Next_Entity
(Param_E
);
1595 Ekind
(E
) = E_Function
1596 and then Is_Private_Type
(Etype
(E
))
1597 and then Defined_In_Enclosing_Package
(Etype
(E
));
1598 end Depends_On_Enclosing_Private_Type
;
1600 ----------------------------------------------
1601 -- Some_Enclosing_Package_Has_Private_Decls --
1602 ----------------------------------------------
1604 function Some_Enclosing_Package_Has_Private_Decls
return Boolean is
1605 Scop
: Entity_Id
:= Current_Scope
;
1606 Pkg_Spec
: Node_Id
:= Package_Specification
(Scop
);
1610 if Ekind
(Scop
) = E_Package
1611 and then Has_Private_Declarations
1612 (Package_Specification
(Scop
))
1614 Pkg_Spec
:= Package_Specification
(Scop
);
1617 exit when Is_Compilation_Unit
(Scop
);
1618 Scop
:= Scope
(Scop
);
1621 return Pkg_Spec
/= Package_Specification
(Current_Scope
);
1622 end Some_Enclosing_Package_Has_Private_Decls
;
1624 -- Start of processing for Skip_Contract_Only_Subprogram
1627 if not CodePeer_Mode
1628 or else Inside_A_Generic
1629 or else not Is_Subprogram
(E
)
1630 or else Is_Abstract_Subprogram
(E
)
1631 or else Is_Imported
(E
)
1632 or else No
(Contract
(E
))
1633 or else No
(Pre_Post_Conditions
(Contract
(E
)))
1634 or else Is_Contract_Only_Body
(E
)
1635 or else Convention
(E
) = Convention_Protected
1639 -- We do not support building the contract-only subprogram if E
1640 -- is a subprogram declared in a nested package that has some
1641 -- formal or return type depending on a private type defined in
1642 -- an enclosing package.
1644 elsif Ekind
(Current_Scope
) = E_Package
1645 and then Some_Enclosing_Package_Has_Private_Decls
1646 and then Depends_On_Enclosing_Private_Type
1648 if Debug_Flag_Dot_KK
then
1650 Saved_Mode
: constant Warning_Mode_Type
:= Warning_Mode
;
1653 -- Warnings are disabled by default under CodePeer_Mode
1654 -- (see switch-c). Enable them temporarily.
1656 Warning_Mode
:= Normal
;
1658 ("cannot generate contract-only subprogram?", E
);
1659 Warning_Mode
:= Saved_Mode
;
1667 end Skip_Contract_Only_Subprogram
;
1669 -- Start of processing for Build_Contract_Only_Subprogram
1672 -- Test cases where the wrapper is not needed and cases where we
1675 if Skip_Contract_Only_Subprogram
(E
) then
1679 -- Note on calls to Copy_Separate_Tree. The trees we are copying
1680 -- here are fully analyzed, but we definitely want fully syntactic
1681 -- unanalyzed trees in the body we construct, so that the analysis
1682 -- generates the right visibility, and that is exactly what the
1683 -- calls to Copy_Separate_Tree give us.
1686 Name
: constant Name_Id
:=
1687 New_External_Name
(Chars
(E
), "__contract_only");
1693 Make_Subprogram_Body
(Loc
,
1695 Copy_Subprogram_Spec
(Declaration_Node
(E
)),
1697 Build_Missing_Body_Decls
,
1698 Handled_Statement_Sequence
=>
1699 Make_Handled_Sequence_Of_Statements
(Loc
,
1700 Statements
=> New_List
(
1701 Build_Missing_Body_Subprogram_Call
),
1702 End_Label
=> Make_Identifier
(Loc
, Name
)));
1704 Id
:= Defining_Unit_Name
(Specification
(Bod
));
1706 -- Copy only the pre/postconditions of the original contract
1707 -- since it is what we need, but also because pragmas stored in
1708 -- the other fields have N_Pragmas with N_Aspect_Specifications
1709 -- that reference their associated pragma (thus causing an endless
1710 -- loop when trying to copy the subtree).
1713 New_Contract
: constant Node_Id
:= Make_Contract
(Sloc
(E
));
1716 Set_Pre_Post_Conditions
(New_Contract
,
1717 Copy_Separate_Tree
(Pre_Post_Conditions
(Contract
(E
))));
1718 Set_Contract
(Id
, New_Contract
);
1721 -- Fix the name of this new subprogram and link the original
1722 -- subprogram with its Contract_Only_Body subprogram.
1724 Set_Chars
(Id
, Name
);
1725 Set_Is_Contract_Only_Body
(Id
);
1726 Set_Contract_Only_Body
(E
, Id
);
1730 end Build_Contract_Only_Subprogram
;
1732 -------------------------------------
1733 -- Build_Contract_Only_Subprograms --
1734 -------------------------------------
1736 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
is
1739 Result
: List_Id
:= No_List
;
1740 Subp_Id
: Entity_Id
;
1744 while Present
(Decl
) loop
1745 if Nkind
(Decl
) = N_Subprogram_Declaration
then
1746 Subp_Id
:= Defining_Unit_Name
(Specification
(Decl
));
1747 New_Subp
:= Build_Contract_Only_Subprogram
(Subp_Id
);
1749 if Present
(New_Subp
) then
1754 Append_To
(Result
, New_Subp
);
1762 end Build_Contract_Only_Subprograms
;
1764 ------------------------------
1765 -- Has_Private_Declarations --
1766 ------------------------------
1768 function Has_Private_Declarations
(N
: Node_Id
) return Boolean is
1770 if not Nkind_In
(N
, N_Package_Specification
,
1771 N_Protected_Definition
,
1777 Present
(Private_Declarations
(N
))
1778 and then Is_Non_Empty_List
(Private_Declarations
(N
));
1780 end Has_Private_Declarations
;
1784 Subp_List
: List_Id
;
1786 -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
1789 Subp_List
:= Build_Contract_Only_Subprograms
(L
);
1790 Append_Contract_Only_Subprograms
(Subp_List
);
1791 Analyze_Contract_Only_Subprograms
;
1792 end Build_And_Analyze_Contract_Only_Subprograms
;
1794 -----------------------------
1795 -- Create_Generic_Contract --
1796 -----------------------------
1798 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
1799 Templ
: constant Node_Id
:= Original_Node
(Unit
);
1800 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
1802 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
1803 -- Add a single contract-related source pragma Prag to the contract of
1804 -- generic template Templ_Id.
1806 ---------------------------------
1807 -- Add_Generic_Contract_Pragma --
1808 ---------------------------------
1810 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
1811 Prag_Templ
: Node_Id
;
1814 -- Mark the pragma to prevent the premature capture of global
1815 -- references when capturing global references of the context
1816 -- (see Save_References_In_Pragma).
1818 Set_Is_Generic_Contract_Pragma
(Prag
);
1820 -- Pragmas that apply to a generic subprogram declaration are not
1821 -- part of the semantic structure of the generic template:
1824 -- procedure Example (Formal : Integer);
1825 -- pragma Precondition (Formal > 0);
1827 -- Create a generic template for such pragmas and link the template
1828 -- of the pragma with the generic template.
1830 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1832 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
1833 Prag_Templ
:= Original_Node
(Prag
);
1835 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
1836 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
1838 -- Otherwise link the pragma with the generic template
1841 Add_Contract_Item
(Prag
, Templ_Id
);
1843 end Add_Generic_Contract_Pragma
;
1847 Context
: constant Node_Id
:= Parent
(Unit
);
1848 Decl
: Node_Id
:= Empty
;
1850 -- Start of processing for Create_Generic_Contract
1853 -- A generic package declaration carries contract-related source pragmas
1854 -- in its visible declarations.
1856 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
1857 Set_Ekind
(Templ_Id
, E_Generic_Package
);
1859 if Present
(Visible_Declarations
(Specification
(Templ
))) then
1860 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
1863 -- A generic package body carries contract-related source pragmas in its
1866 elsif Nkind
(Templ
) = N_Package_Body
then
1867 Set_Ekind
(Templ_Id
, E_Package_Body
);
1869 if Present
(Declarations
(Templ
)) then
1870 Decl
:= First
(Declarations
(Templ
));
1873 -- Generic subprogram declaration
1875 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1876 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
1877 Set_Ekind
(Templ_Id
, E_Generic_Function
);
1879 Set_Ekind
(Templ_Id
, E_Generic_Procedure
);
1882 -- When the generic subprogram acts as a compilation unit, inspect
1883 -- the Pragmas_After list for contract-related source pragmas.
1885 if Nkind
(Context
) = N_Compilation_Unit
then
1886 if Present
(Aux_Decls_Node
(Context
))
1887 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
1889 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
1892 -- Otherwise inspect the successive declarations for contract-related
1896 Decl
:= Next
(Unit
);
1899 -- A generic subprogram body carries contract-related source pragmas in
1900 -- its declarations.
1902 elsif Nkind
(Templ
) = N_Subprogram_Body
then
1903 Set_Ekind
(Templ_Id
, E_Subprogram_Body
);
1905 if Present
(Declarations
(Templ
)) then
1906 Decl
:= First
(Declarations
(Templ
));
1910 -- Inspect the relevant declarations looking for contract-related source
1911 -- pragmas and add them to the contract of the generic unit.
1913 while Present
(Decl
) loop
1914 if Comes_From_Source
(Decl
) then
1915 if Nkind
(Decl
) = N_Pragma
then
1917 -- The source pragma is a contract annotation
1919 if Is_Contract_Annotation
(Decl
) then
1920 Add_Generic_Contract_Pragma
(Decl
);
1923 -- The region where a contract-related source pragma may appear
1924 -- ends with the first source non-pragma declaration or statement.
1933 end Create_Generic_Contract
;
1935 --------------------------------
1936 -- Expand_Subprogram_Contract --
1937 --------------------------------
1939 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
1940 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1941 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1943 procedure Add_Invariant_And_Predicate_Checks
1944 (Subp_Id
: Entity_Id
;
1945 Stmts
: in out List_Id
;
1946 Result
: out Node_Id
);
1947 -- Process the result of function Subp_Id (if applicable) and all its
1948 -- formals. Add invariant and predicate checks where applicable. The
1949 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1950 -- function, Result contains the entity of parameter _Result, to be
1951 -- used in the creation of procedure _Postconditions.
1953 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
1954 -- Append a node to a list. If there is no list, create a new one. When
1955 -- the item denotes a pragma, it is added to the list only when it is
1958 procedure Build_Postconditions_Procedure
1959 (Subp_Id
: Entity_Id
;
1961 Result
: Entity_Id
);
1962 -- Create the body of procedure _Postconditions which handles various
1963 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1964 -- of statements to be checked on exit. Parameter Result is the entity
1965 -- of parameter _Result when Subp_Id denotes a function.
1967 procedure Process_Contract_Cases
(Stmts
: in out List_Id
);
1968 -- Process pragma Contract_Cases. This routine prepends items to the
1969 -- body declarations and appends items to list Stmts.
1971 procedure Process_Postconditions
(Stmts
: in out List_Id
);
1972 -- Collect all [inherited] spec and body postconditions and accumulate
1973 -- their pragma Check equivalents in list Stmts.
1975 procedure Process_Preconditions
;
1976 -- Collect all [inherited] spec and body preconditions and prepend their
1977 -- pragma Check equivalents to the declarations of the body.
1979 ----------------------------------------
1980 -- Add_Invariant_And_Predicate_Checks --
1981 ----------------------------------------
1983 procedure Add_Invariant_And_Predicate_Checks
1984 (Subp_Id
: Entity_Id
;
1985 Stmts
: in out List_Id
;
1986 Result
: out Node_Id
)
1988 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
1989 -- Id denotes the return value of a function or a formal parameter.
1990 -- Add an invariant check if the type of Id is access to a type with
1991 -- invariants. The routine appends the generated code to Stmts.
1993 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
1994 -- Determine whether type Typ can benefit from invariant checks. To
1995 -- qualify, the type must have a non-null invariant procedure and
1996 -- subprogram Subp_Id must appear visible from the point of view of
1999 ---------------------------------
2000 -- Add_Invariant_Access_Checks --
2001 ---------------------------------
2003 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
2004 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2011 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
2012 Typ
:= Designated_Type
(Typ
);
2014 if Invariant_Checks_OK
(Typ
) then
2016 Make_Explicit_Dereference
(Loc
,
2017 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
2018 Set_Etype
(Ref
, Typ
);
2021 -- if <Id> /= null then
2022 -- <invariant_call (<Ref>)>
2027 Make_If_Statement
(Loc
,
2030 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
2031 Right_Opnd
=> Make_Null
(Loc
)),
2032 Then_Statements
=> New_List
(
2033 Make_Invariant_Call
(Ref
))),
2037 end Add_Invariant_Access_Checks
;
2039 -------------------------
2040 -- Invariant_Checks_OK --
2041 -------------------------
2043 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
2044 function Has_Public_Visibility_Of_Subprogram
return Boolean;
2045 -- Determine whether type Typ has public visibility of subprogram
2048 -----------------------------------------
2049 -- Has_Public_Visibility_Of_Subprogram --
2050 -----------------------------------------
2052 function Has_Public_Visibility_Of_Subprogram
return Boolean is
2053 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2056 -- An Initialization procedure must be considered visible even
2057 -- though it is internally generated.
2059 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2062 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2065 -- Internally generated code is never publicly visible except
2066 -- for a subprogram that is the implementation of an expression
2067 -- function. In that case the visibility is determined by the
2070 elsif not Comes_From_Source
(Subp_Decl
)
2072 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2074 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2078 -- Determine whether the subprogram is declared in the visible
2079 -- declarations of the package containing the type, or in the
2080 -- visible declaration of a child unit of that package.
2084 Decls
: constant List_Id
:=
2085 List_Containing
(Subp_Decl
);
2086 Subp_Scope
: constant Entity_Id
:=
2087 Scope
(Defining_Entity
(Subp_Decl
));
2088 Typ_Scope
: constant Entity_Id
:= Scope
(Typ
);
2092 Decls
= Visible_Declarations
2093 (Specification
(Unit_Declaration_Node
(Typ_Scope
)))
2096 (Ekind
(Subp_Scope
) = E_Package
2097 and then Typ_Scope
/= Subp_Scope
2098 and then Is_Child_Unit
(Subp_Scope
)
2100 Is_Ancestor_Package
(Typ_Scope
, Subp_Scope
)
2102 Decls
= Visible_Declarations
2104 (Unit_Declaration_Node
(Subp_Scope
))));
2107 end Has_Public_Visibility_Of_Subprogram
;
2109 -- Start of processing for Invariant_Checks_OK
2113 Has_Invariants
(Typ
)
2114 and then Present
(Invariant_Procedure
(Typ
))
2115 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2116 and then Has_Public_Visibility_Of_Subprogram
;
2117 end Invariant_Checks_OK
;
2121 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2122 -- Source location of subprogram body contract
2127 -- Start of processing for Add_Invariant_And_Predicate_Checks
2132 -- Process the result of a function
2134 if Ekind
(Subp_Id
) = E_Function
then
2135 Typ
:= Etype
(Subp_Id
);
2137 -- Generate _Result which is used in procedure _Postconditions to
2138 -- verify the return value.
2140 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2141 Set_Etype
(Result
, Typ
);
2143 -- Add an invariant check when the return type has invariants and
2144 -- the related function is visible to the outside.
2146 if Invariant_Checks_OK
(Typ
) then
2149 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2153 -- Add an invariant check when the return type is an access to a
2154 -- type with invariants.
2156 Add_Invariant_Access_Checks
(Result
);
2159 -- Add invariant and predicates for all formals that qualify
2161 Formal
:= First_Formal
(Subp_Id
);
2162 while Present
(Formal
) loop
2163 Typ
:= Etype
(Formal
);
2165 if Ekind
(Formal
) /= E_In_Parameter
2166 or else Is_Access_Type
(Typ
)
2168 if Invariant_Checks_OK
(Typ
) then
2171 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2175 Add_Invariant_Access_Checks
(Formal
);
2177 -- Note: we used to add predicate checks for OUT and IN OUT
2178 -- formals here, but that was misguided, since such checks are
2179 -- performed on the caller side, based on the predicate of the
2180 -- actual, rather than the predicate of the formal.
2184 Next_Formal
(Formal
);
2186 end Add_Invariant_And_Predicate_Checks
;
2188 -------------------------
2189 -- Append_Enabled_Item --
2190 -------------------------
2192 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2194 -- Do not chain ignored or disabled pragmas
2196 if Nkind
(Item
) = N_Pragma
2197 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2201 -- Otherwise, add the item
2208 -- If the pragma is a conjunct in a composite postcondition, it
2209 -- has been processed in reverse order. In the postcondition body
2210 -- it must appear before the others.
2212 if Nkind
(Item
) = N_Pragma
2213 and then From_Aspect_Specification
(Item
)
2214 and then Split_PPC
(Item
)
2216 Prepend
(Item
, List
);
2218 Append
(Item
, List
);
2221 end Append_Enabled_Item
;
2223 ------------------------------------
2224 -- Build_Postconditions_Procedure --
2225 ------------------------------------
2227 procedure Build_Postconditions_Procedure
2228 (Subp_Id
: Entity_Id
;
2232 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
);
2233 -- Insert node Stmt before the first source declaration of the
2234 -- related subprogram's body. If no such declaration exists, Stmt
2235 -- becomes the last declaration.
2237 --------------------------------------------
2238 -- Insert_Before_First_Source_Declaration --
2239 --------------------------------------------
2241 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
) is
2242 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2246 -- Inspect the declarations of the related subprogram body looking
2247 -- for the first source declaration.
2249 if Present
(Decls
) then
2250 Decl
:= First
(Decls
);
2251 while Present
(Decl
) loop
2252 if Comes_From_Source
(Decl
) then
2253 Insert_Before
(Decl
, Stmt
);
2260 -- If we get there, then the subprogram body lacks any source
2261 -- declarations. The body of _Postconditions now acts as the
2262 -- last declaration.
2264 Append
(Stmt
, Decls
);
2266 -- Ensure that the body has a declaration list
2269 Set_Declarations
(Body_Decl
, New_List
(Stmt
));
2271 end Insert_Before_First_Source_Declaration
;
2275 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2276 Params
: List_Id
:= No_List
;
2278 Proc_Decl
: Node_Id
;
2279 Proc_Id
: Entity_Id
;
2280 Proc_Spec
: Node_Id
;
2282 -- Start of processing for Build_Postconditions_Procedure
2285 -- Nothing to do if there are no actions to check on exit
2291 Proc_Id
:= Make_Defining_Identifier
(Loc
, Name_uPostconditions
);
2292 Set_Debug_Info_Needed
(Proc_Id
);
2293 Set_Postconditions_Proc
(Subp_Id
, Proc_Id
);
2295 -- Force the front-end inlining of _Postconditions when generating C
2296 -- code, since its body may have references to itypes defined in the
2297 -- enclosing subprogram, which would cause problems for unnesting
2298 -- routines in the absence of inlining.
2300 if Modify_Tree_For_C
then
2301 Set_Has_Pragma_Inline
(Proc_Id
);
2302 Set_Has_Pragma_Inline_Always
(Proc_Id
);
2303 Set_Is_Inlined
(Proc_Id
);
2306 -- The related subprogram is a function: create the specification of
2307 -- parameter _Result.
2309 if Present
(Result
) then
2310 Params
:= New_List
(
2311 Make_Parameter_Specification
(Loc
,
2312 Defining_Identifier
=> Result
,
2314 New_Occurrence_Of
(Etype
(Result
), Loc
)));
2318 Make_Procedure_Specification
(Loc
,
2319 Defining_Unit_Name
=> Proc_Id
,
2320 Parameter_Specifications
=> Params
);
2322 Proc_Decl
:= Make_Subprogram_Declaration
(Loc
, Proc_Spec
);
2324 -- Insert _Postconditions before the first source declaration of the
2325 -- body. This ensures that the body will not cause any premature
2326 -- freezing, as it may mention types:
2328 -- procedure Proc (Obj : Array_Typ) is
2329 -- procedure _postconditions is
2332 -- end _postconditions;
2334 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
2337 -- In the example above, Obj is of type T but the incorrect placement
2338 -- of _Postconditions will cause a crash in gigi due to an out-of-
2339 -- order reference. The body of _Postconditions must be placed after
2340 -- the declaration of Temp to preserve correct visibility.
2342 Insert_Before_First_Source_Declaration
(Proc_Decl
);
2343 Analyze
(Proc_Decl
);
2345 -- Set an explicit End_Label to override the sloc of the implicit
2346 -- RETURN statement, and prevent it from inheriting the sloc of one
2347 -- the postconditions: this would cause confusing debug info to be
2348 -- produced, interfering with coverage-analysis tools.
2351 Make_Subprogram_Body
(Loc
,
2353 Copy_Subprogram_Spec
(Proc_Spec
),
2354 Declarations
=> Empty_List
,
2355 Handled_Statement_Sequence
=>
2356 Make_Handled_Sequence_Of_Statements
(Loc
,
2357 Statements
=> Stmts
,
2358 End_Label
=> Make_Identifier
(Loc
, Chars
(Proc_Id
))));
2360 Insert_After_And_Analyze
(Proc_Decl
, Proc_Bod
);
2361 end Build_Postconditions_Procedure
;
2363 ----------------------------
2364 -- Process_Contract_Cases --
2365 ----------------------------
2367 procedure Process_Contract_Cases
(Stmts
: in out List_Id
) is
2368 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2369 -- Process pragma Contract_Cases for subprogram Subp_Id
2371 --------------------------------
2372 -- Process_Contract_Cases_For --
2373 --------------------------------
2375 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2376 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2380 if Present
(Items
) then
2381 Prag
:= Contract_Test_Cases
(Items
);
2382 while Present
(Prag
) loop
2383 if Pragma_Name
(Prag
) = Name_Contract_Cases
then
2384 Expand_Pragma_Contract_Cases
2387 Decls
=> Declarations
(Body_Decl
),
2391 Prag
:= Next_Pragma
(Prag
);
2394 end Process_Contract_Cases_For
;
2396 -- Start of processing for Process_Contract_Cases
2399 Process_Contract_Cases_For
(Body_Id
);
2401 if Present
(Spec_Id
) then
2402 Process_Contract_Cases_For
(Spec_Id
);
2404 end Process_Contract_Cases
;
2406 ----------------------------
2407 -- Process_Postconditions --
2408 ----------------------------
2410 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2411 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2412 -- Collect all [refined] postconditions of a specific kind denoted
2413 -- by Post_Nam that belong to the body, and generate pragma Check
2414 -- equivalents in list Stmts.
2416 procedure Process_Spec_Postconditions
;
2417 -- Collect all [inherited] postconditions of the spec, and generate
2418 -- pragma Check equivalents in list Stmts.
2420 ---------------------------------
2421 -- Process_Body_Postconditions --
2422 ---------------------------------
2424 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2425 Items
: constant Node_Id
:= Contract
(Body_Id
);
2426 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2431 -- Process the contract
2433 if Present
(Items
) then
2434 Prag
:= Pre_Post_Conditions
(Items
);
2435 while Present
(Prag
) loop
2436 if Pragma_Name
(Prag
) = Post_Nam
then
2438 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2442 Prag
:= Next_Pragma
(Prag
);
2446 -- The subprogram body being processed is actually the proper body
2447 -- of a stub with a corresponding spec. The subprogram stub may
2448 -- carry a postcondition pragma, in which case it must be taken
2449 -- into account. The pragma appears after the stub.
2451 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2452 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2453 while Present
(Decl
) loop
2455 -- Note that non-matching pragmas are skipped
2457 if Nkind
(Decl
) = N_Pragma
then
2458 if Pragma_Name
(Decl
) = Post_Nam
then
2460 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2464 -- Skip internally generated code
2466 elsif not Comes_From_Source
(Decl
) then
2469 -- Postcondition pragmas are usually grouped together. There
2470 -- is no need to inspect the whole declarative list.
2479 end Process_Body_Postconditions
;
2481 ---------------------------------
2482 -- Process_Spec_Postconditions --
2483 ---------------------------------
2485 procedure Process_Spec_Postconditions
is
2486 Subps
: constant Subprogram_List
:=
2487 Inherited_Subprograms
(Spec_Id
);
2490 Subp_Id
: Entity_Id
;
2493 -- Process the contract
2495 Items
:= Contract
(Spec_Id
);
2497 if Present
(Items
) then
2498 Prag
:= Pre_Post_Conditions
(Items
);
2499 while Present
(Prag
) loop
2500 if Pragma_Name
(Prag
) = Name_Postcondition
then
2502 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2506 Prag
:= Next_Pragma
(Prag
);
2510 -- Process the contracts of all inherited subprograms, looking for
2511 -- class-wide postconditions.
2513 for Index
in Subps
'Range loop
2514 Subp_Id
:= Subps
(Index
);
2515 Items
:= Contract
(Subp_Id
);
2517 if Present
(Items
) then
2518 Prag
:= Pre_Post_Conditions
(Items
);
2519 while Present
(Prag
) loop
2520 if Pragma_Name
(Prag
) = Name_Postcondition
2521 and then Class_Present
(Prag
)
2525 Build_Pragma_Check_Equivalent
2528 Inher_Id
=> Subp_Id
),
2532 Prag
:= Next_Pragma
(Prag
);
2536 end Process_Spec_Postconditions
;
2538 -- Start of processing for Process_Postconditions
2541 -- The processing of postconditions is done in reverse order (body
2542 -- first) to ensure the following arrangement:
2544 -- <refined postconditions from body>
2545 -- <postconditions from body>
2546 -- <postconditions from spec>
2547 -- <inherited postconditions>
2549 Process_Body_Postconditions
(Name_Refined_Post
);
2550 Process_Body_Postconditions
(Name_Postcondition
);
2552 if Present
(Spec_Id
) then
2553 Process_Spec_Postconditions
;
2555 end Process_Postconditions
;
2557 ---------------------------
2558 -- Process_Preconditions --
2559 ---------------------------
2561 procedure Process_Preconditions
is
2562 Class_Pre
: Node_Id
:= Empty
;
2563 -- The sole [inherited] class-wide precondition pragma that applies
2564 -- to the subprogram.
2566 Insert_Node
: Node_Id
:= Empty
;
2567 -- The insertion node after which all pragma Check equivalents are
2570 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean;
2571 -- Determine whether arbitrary declaration Decl denotes a renaming of
2572 -- a discriminant or protection field _object.
2574 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
);
2575 -- Merge two class-wide preconditions by "or else"-ing them. The
2576 -- changes are accumulated in parameter Into. Update the error
2579 procedure Prepend_To_Decls
(Item
: Node_Id
);
2580 -- Prepend a single item to the declarations of the subprogram body
2582 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
);
2583 -- Save a class-wide precondition into Class_Pre, or prepend a normal
2584 -- precondition to the declarations of the body and analyze it.
2586 procedure Process_Inherited_Preconditions
;
2587 -- Collect all inherited class-wide preconditions and merge them into
2588 -- one big precondition to be evaluated as pragma Check.
2590 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
2591 -- Collect all preconditions of subprogram Subp_Id and prepend their
2592 -- pragma Check equivalents to the declarations of the body.
2594 --------------------------
2595 -- Is_Prologue_Renaming --
2596 --------------------------
2598 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
2605 if Nkind
(Decl
) = N_Object_Renaming_Declaration
then
2606 Obj
:= Defining_Entity
(Decl
);
2609 if Nkind
(Nam
) = N_Selected_Component
then
2610 Pref
:= Prefix
(Nam
);
2611 Sel
:= Selector_Name
(Nam
);
2613 -- A discriminant renaming appears as
2614 -- Discr : constant ... := Prefix.Discr;
2616 if Ekind
(Obj
) = E_Constant
2617 and then Is_Entity_Name
(Sel
)
2618 and then Present
(Entity
(Sel
))
2619 and then Ekind
(Entity
(Sel
)) = E_Discriminant
2623 -- A protection field renaming appears as
2624 -- Prot : ... := _object._object;
2626 -- A renamed private component is just a component of
2627 -- _object, with an arbitrary name.
2629 elsif Ekind
(Obj
) = E_Variable
2630 and then Nkind
(Pref
) = N_Identifier
2631 and then Chars
(Pref
) = Name_uObject
2632 and then Nkind
(Sel
) = N_Identifier
2640 end Is_Prologue_Renaming
;
2642 -------------------------
2643 -- Merge_Preconditions --
2644 -------------------------
2646 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
) is
2647 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
;
2648 -- Return the boolean expression argument of a precondition while
2649 -- updating its parentheses count for the subsequent merge.
2651 function Message_Arg
(Prag
: Node_Id
) return Node_Id
;
2652 -- Return the message argument of a precondition
2654 --------------------
2655 -- Expression_Arg --
2656 --------------------
2658 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
is
2659 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2660 Arg
: constant Node_Id
:= Get_Pragma_Arg
(Next
(First
(Args
)));
2663 if Paren_Count
(Arg
) = 0 then
2664 Set_Paren_Count
(Arg
, 1);
2674 function Message_Arg
(Prag
: Node_Id
) return Node_Id
is
2675 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2677 return Get_Pragma_Arg
(Last
(Args
));
2682 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
2683 From_Msg
: constant Node_Id
:= Message_Arg
(From
);
2684 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
2685 Into_Msg
: constant Node_Id
:= Message_Arg
(Into
);
2686 Loc
: constant Source_Ptr
:= Sloc
(Into
);
2688 -- Start of processing for Merge_Preconditions
2691 -- Merge the two preconditions by "or else"-ing them
2695 Right_Opnd
=> Relocate_Node
(Into_Expr
),
2696 Left_Opnd
=> From_Expr
));
2698 -- Merge the two error messages to produce a single message of the
2701 -- failed precondition from ...
2702 -- also failed inherited precondition from ...
2704 if not Exception_Locations_Suppressed
then
2705 Start_String
(Strval
(Into_Msg
));
2706 Store_String_Char
(ASCII
.LF
);
2707 Store_String_Chars
(" also ");
2708 Store_String_Chars
(Strval
(From_Msg
));
2710 Set_Strval
(Into_Msg
, End_String
);
2712 end Merge_Preconditions
;
2714 ----------------------
2715 -- Prepend_To_Decls --
2716 ----------------------
2718 procedure Prepend_To_Decls
(Item
: Node_Id
) is
2719 Decls
: List_Id
:= Declarations
(Body_Decl
);
2722 -- Ensure that the body has a declarative list
2726 Set_Declarations
(Body_Decl
, Decls
);
2729 Prepend_To
(Decls
, Item
);
2730 end Prepend_To_Decls
;
2732 ------------------------------
2733 -- Prepend_To_Decls_Or_Save --
2734 ------------------------------
2736 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
) is
2737 Check_Prag
: Node_Id
;
2740 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
2742 -- Save the sole class-wide precondition (if any) for the next
2743 -- step, where it will be merged with inherited preconditions.
2745 if Class_Present
(Prag
) then
2746 pragma Assert
(No
(Class_Pre
));
2747 Class_Pre
:= Check_Prag
;
2749 -- Accumulate the corresponding Check pragmas at the top of the
2750 -- declarations. Prepending the items ensures that they will be
2751 -- evaluated in their original order.
2754 if Present
(Insert_Node
) then
2755 Insert_After
(Insert_Node
, Check_Prag
);
2757 Prepend_To_Decls
(Check_Prag
);
2760 Analyze
(Check_Prag
);
2762 end Prepend_To_Decls_Or_Save
;
2764 -------------------------------------
2765 -- Process_Inherited_Preconditions --
2766 -------------------------------------
2768 procedure Process_Inherited_Preconditions
is
2769 Subps
: constant Subprogram_List
:=
2770 Inherited_Subprograms
(Spec_Id
);
2771 Check_Prag
: Node_Id
;
2774 Subp_Id
: Entity_Id
;
2777 -- Process the contracts of all inherited subprograms, looking for
2778 -- class-wide preconditions.
2780 for Index
in Subps
'Range loop
2781 Subp_Id
:= Subps
(Index
);
2782 Items
:= Contract
(Subp_Id
);
2784 if Present
(Items
) then
2785 Prag
:= Pre_Post_Conditions
(Items
);
2786 while Present
(Prag
) loop
2787 if Pragma_Name
(Prag
) = Name_Precondition
2788 and then Class_Present
(Prag
)
2791 Build_Pragma_Check_Equivalent
2794 Inher_Id
=> Subp_Id
);
2796 -- The spec of an inherited subprogram already yielded
2797 -- a class-wide precondition. Merge the existing
2798 -- precondition with the current one using "or else".
2800 if Present
(Class_Pre
) then
2801 Merge_Preconditions
(Check_Prag
, Class_Pre
);
2803 Class_Pre
:= Check_Prag
;
2807 Prag
:= Next_Pragma
(Prag
);
2812 -- Add the merged class-wide preconditions
2814 if Present
(Class_Pre
) then
2815 Prepend_To_Decls
(Class_Pre
);
2816 Analyze
(Class_Pre
);
2818 end Process_Inherited_Preconditions
;
2820 -------------------------------
2821 -- Process_Preconditions_For --
2822 -------------------------------
2824 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
2825 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2828 Subp_Decl
: Node_Id
;
2831 -- Process the contract
2833 if Present
(Items
) then
2834 Prag
:= Pre_Post_Conditions
(Items
);
2835 while Present
(Prag
) loop
2836 if Pragma_Name
(Prag
) = Name_Precondition
then
2837 Prepend_To_Decls_Or_Save
(Prag
);
2840 Prag
:= Next_Pragma
(Prag
);
2844 -- The subprogram declaration being processed is actually a body
2845 -- stub. The stub may carry a precondition pragma, in which case
2846 -- it must be taken into account. The pragma appears after the
2849 Subp_Decl
:= Unit_Declaration_Node
(Subp_Id
);
2851 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
2853 -- Inspect the declarations following the body stub
2855 Decl
:= Next
(Subp_Decl
);
2856 while Present
(Decl
) loop
2858 -- Note that non-matching pragmas are skipped
2860 if Nkind
(Decl
) = N_Pragma
then
2861 if Pragma_Name
(Decl
) = Name_Precondition
then
2862 Prepend_To_Decls_Or_Save
(Decl
);
2865 -- Skip internally generated code
2867 elsif not Comes_From_Source
(Decl
) then
2870 -- Preconditions are usually grouped together. There is no
2871 -- need to inspect the whole declarative list.
2880 end Process_Preconditions_For
;
2884 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2887 -- Start of processing for Process_Preconditions
2890 -- Find the proper insertion point for all pragma Check equivalents
2892 if Present
(Decls
) then
2893 Decl
:= First
(Decls
);
2894 while Present
(Decl
) loop
2896 -- First source declaration terminates the search, because all
2897 -- preconditions must be evaluated prior to it, by definition.
2899 if Comes_From_Source
(Decl
) then
2902 -- Certain internally generated object renamings such as those
2903 -- for discriminants and protection fields must be elaborated
2904 -- before the preconditions are evaluated, as their expressions
2905 -- may mention the discriminants. The renamings include those
2906 -- for private components so we need to find the last such.
2908 elsif Is_Prologue_Renaming
(Decl
) then
2909 while Present
(Next
(Decl
))
2910 and then Is_Prologue_Renaming
(Next
(Decl
))
2915 Insert_Node
:= Decl
;
2917 -- Otherwise the declaration does not come from source. This
2918 -- also terminates the search, because internal code may raise
2919 -- exceptions which should not preempt the preconditions.
2929 -- The processing of preconditions is done in reverse order (body
2930 -- first), because each pragma Check equivalent is inserted at the
2931 -- top of the declarations. This ensures that the final order is
2932 -- consistent with following diagram:
2934 -- <inherited preconditions>
2935 -- <preconditions from spec>
2936 -- <preconditions from body>
2938 Process_Preconditions_For
(Body_Id
);
2940 if Present
(Spec_Id
) then
2941 Process_Preconditions_For
(Spec_Id
);
2942 Process_Inherited_Preconditions
;
2944 end Process_Preconditions
;
2948 Restore_Scope
: Boolean := False;
2950 Stmts
: List_Id
:= No_List
;
2951 Subp_Id
: Entity_Id
;
2953 -- Start of processing for Expand_Subprogram_Contract
2956 -- Obtain the entity of the initial declaration
2958 if Present
(Spec_Id
) then
2964 -- Do not perform expansion activity when it is not needed
2966 if not Expander_Active
then
2969 -- ASIS requires an unaltered tree
2971 elsif ASIS_Mode
then
2974 -- GNATprove does not need the executable semantics of a contract
2976 elsif GNATprove_Mode
then
2979 -- The contract of a generic subprogram or one declared in a generic
2980 -- context is not expanded, as the corresponding instance will provide
2981 -- the executable semantics of the contract.
2983 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
2986 -- All subprograms carry a contract, but for some it is not significant
2987 -- and should not be processed. This is a small optimization.
2989 elsif not Has_Significant_Contract
(Subp_Id
) then
2992 -- The contract of an ignored Ghost subprogram does not need expansion,
2993 -- because the subprogram and all calls to it will be removed.
2995 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
2999 -- Do not re-expand the same contract. This scenario occurs when a
3000 -- construct is rewritten into something else during its analysis
3001 -- (expression functions for instance).
3003 if Has_Expanded_Contract
(Subp_Id
) then
3006 -- Otherwise mark the subprogram
3009 Set_Has_Expanded_Contract
(Subp_Id
);
3012 -- Ensure that the formal parameters are visible when expanding all
3015 if not In_Open_Scopes
(Subp_Id
) then
3016 Restore_Scope
:= True;
3017 Push_Scope
(Subp_Id
);
3019 if Is_Generic_Subprogram
(Subp_Id
) then
3020 Install_Generic_Formals
(Subp_Id
);
3022 Install_Formals
(Subp_Id
);
3026 -- The expansion of a subprogram contract involves the creation of Check
3027 -- pragmas to verify the contract assertions of the spec and body in a
3028 -- particular order. The order is as follows:
3030 -- function Example (...) return ... is
3031 -- procedure _Postconditions (...) is
3033 -- <refined postconditions from body>
3034 -- <postconditions from body>
3035 -- <postconditions from spec>
3036 -- <inherited postconditions>
3037 -- <contract case consequences>
3038 -- <invariant check of function result>
3039 -- <invariant and predicate checks of parameters>
3040 -- end _Postconditions;
3042 -- <inherited preconditions>
3043 -- <preconditions from spec>
3044 -- <preconditions from body>
3045 -- <contract case conditions>
3047 -- <source declarations>
3049 -- <source statements>
3051 -- _Preconditions (Result);
3055 -- Routine _Postconditions holds all contract assertions that must be
3056 -- verified on exit from the related subprogram.
3058 -- Step 1: Handle all preconditions. This action must come before the
3059 -- processing of pragma Contract_Cases because the pragma prepends items
3060 -- to the body declarations.
3062 Process_Preconditions
;
3064 -- Step 2: Handle all postconditions. This action must come before the
3065 -- processing of pragma Contract_Cases because the pragma appends items
3068 Process_Postconditions
(Stmts
);
3070 -- Step 3: Handle pragma Contract_Cases. This action must come before
3071 -- the processing of invariants and predicates because those append
3072 -- items to list Stmts.
3074 Process_Contract_Cases
(Stmts
);
3076 -- Step 4: Apply invariant and predicate checks on a function result and
3077 -- all formals. The resulting checks are accumulated in list Stmts.
3079 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3081 -- Step 5: Construct procedure _Postconditions
3083 Build_Postconditions_Procedure
(Subp_Id
, Stmts
, Result
);
3085 if Restore_Scope
then
3088 end Expand_Subprogram_Contract
;
3090 ---------------------------------
3091 -- Inherit_Subprogram_Contract --
3092 ---------------------------------
3094 procedure Inherit_Subprogram_Contract
3096 From_Subp
: Entity_Id
)
3098 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3099 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3102 --------------------
3103 -- Inherit_Pragma --
3104 --------------------
3106 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3107 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3111 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3112 -- chains, therefore the node must be replicated. The new pragma is
3113 -- flagged as inherited for distinction purposes.
3115 if Present
(Prag
) then
3116 New_Prag
:= New_Copy_Tree
(Prag
);
3117 Set_Is_Inherited_Pragma
(New_Prag
);
3119 Add_Contract_Item
(New_Prag
, Subp
);
3123 -- Start of processing for Inherit_Subprogram_Contract
3126 -- Inheritance is carried out only when both entities are subprograms
3129 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3130 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3131 and then Present
(Contract
(From_Subp
))
3133 Inherit_Pragma
(Pragma_Extensions_Visible
);
3135 end Inherit_Subprogram_Contract
;
3137 -------------------------------------
3138 -- Instantiate_Subprogram_Contract --
3139 -------------------------------------
3141 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3142 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3143 -- Instantiate all contract-related source pragmas found in the list,
3144 -- starting with pragma First_Prag. Each instantiated pragma is added
3147 -------------------------
3148 -- Instantiate_Pragmas --
3149 -------------------------
3151 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3152 Inst_Prag
: Node_Id
;
3157 while Present
(Prag
) loop
3158 if Is_Generic_Contract_Pragma
(Prag
) then
3160 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3162 Set_Analyzed
(Inst_Prag
, False);
3163 Append_To
(L
, Inst_Prag
);
3166 Prag
:= Next_Pragma
(Prag
);
3168 end Instantiate_Pragmas
;
3172 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3174 -- Start of processing for Instantiate_Subprogram_Contract
3177 if Present
(Items
) then
3178 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3179 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3180 Instantiate_Pragmas
(Classifications
(Items
));
3182 end Instantiate_Subprogram_Contract
;
3184 ----------------------------------------
3185 -- Save_Global_References_In_Contract --
3186 ----------------------------------------
3188 procedure Save_Global_References_In_Contract
3192 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
3193 -- Save all global references in contract-related source pragmas found
3194 -- in the list, starting with pragma First_Prag.
3196 ------------------------------------
3197 -- Save_Global_References_In_List --
3198 ------------------------------------
3200 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
3205 while Present
(Prag
) loop
3206 if Is_Generic_Contract_Pragma
(Prag
) then
3207 Save_Global_References
(Prag
);
3210 Prag
:= Next_Pragma
(Prag
);
3212 end Save_Global_References_In_List
;
3216 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3218 -- Start of processing for Save_Global_References_In_Contract
3221 -- The entity of the analyzed generic copy must be on the scope stack
3222 -- to ensure proper detection of global references.
3224 Push_Scope
(Gen_Id
);
3226 if Permits_Aspect_Specifications
(Templ
)
3227 and then Has_Aspects
(Templ
)
3229 Save_Global_References_In_Aspects
(Templ
);
3232 if Present
(Items
) then
3233 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
3234 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
3235 Save_Global_References_In_List
(Classifications
(Items
));
3239 end Save_Global_References_In_Contract
;