1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- C O N T R A C T S --
9 -- Copyright (C) 2015-2016, 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
)
387 Analyze_Entry_Or_Subprogram_Contract
388 (Subp_Id
=> Defining_Entity
(Decl
),
389 Freeze_Id
=> Freeze_Id
);
391 -- Entry or subprogram bodies
393 elsif Nkind_In
(Decl
, N_Entry_Body
, N_Subprogram_Body
) then
394 Analyze_Entry_Or_Subprogram_Body_Contract
(Defining_Entity
(Decl
));
398 elsif Nkind
(Decl
) = N_Object_Declaration
then
399 Analyze_Object_Contract
400 (Obj_Id
=> Defining_Entity
(Decl
),
401 Freeze_Id
=> Freeze_Id
);
405 elsif Nkind_In
(Decl
, N_Protected_Type_Declaration
,
406 N_Single_Protected_Declaration
)
408 Analyze_Protected_Contract
(Defining_Entity
(Decl
));
410 -- Subprogram body stubs
412 elsif Nkind
(Decl
) = N_Subprogram_Body_Stub
then
413 Analyze_Subprogram_Body_Stub_Contract
(Defining_Entity
(Decl
));
417 elsif Nkind_In
(Decl
, N_Single_Task_Declaration
,
418 N_Task_Type_Declaration
)
420 Analyze_Task_Contract
(Defining_Entity
(Decl
));
422 -- For type declarations, we need to do the pre-analysis of
423 -- Iterable aspect specifications.
424 -- Other type aspects need to be resolved here???
426 elsif Nkind
(Decl
) = N_Private_Type_Declaration
427 and then Present
(Aspect_Specifications
(Decl
))
430 E
: constant Entity_Id
:= Defining_Identifier
(Decl
);
431 It
: constant Node_Id
:= Find_Aspect
(E
, Aspect_Iterable
);
434 Validate_Iterable_Aspect
(E
, It
);
441 end Analyze_Contracts
;
443 -----------------------------------------------
444 -- Analyze_Entry_Or_Subprogram_Body_Contract --
445 -----------------------------------------------
447 procedure Analyze_Entry_Or_Subprogram_Body_Contract
(Body_Id
: Entity_Id
) is
448 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
449 Items
: constant Node_Id
:= Contract
(Body_Id
);
450 Spec_Id
: constant Entity_Id
:= Unique_Defining_Entity
(Body_Decl
);
451 Mode
: SPARK_Mode_Type
;
454 -- When a subprogram body declaration is illegal, its defining entity is
455 -- left unanalyzed. There is nothing left to do in this case because the
456 -- body lacks a contract, or even a proper Ekind.
458 if Ekind
(Body_Id
) = E_Void
then
461 -- Do not analyze a contract multiple times
463 elsif Present
(Items
) then
464 if Analyzed
(Items
) then
467 Set_Analyzed
(Items
);
471 -- Due to the timing of contract analysis, delayed pragmas may be
472 -- subject to the wrong SPARK_Mode, usually that of the enclosing
473 -- context. To remedy this, restore the original SPARK_Mode of the
474 -- related subprogram body.
476 Save_SPARK_Mode_And_Set
(Body_Id
, Mode
);
478 -- Ensure that the contract cases or postconditions mention 'Result or
479 -- define a post-state.
481 Check_Result_And_Post_State
(Body_Id
);
483 -- A stand-alone nonvolatile function body cannot have an effectively
484 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
485 -- check is relevant only when SPARK_Mode is on, as it is not a standard
486 -- legality rule. The check is performed here because Volatile_Function
487 -- is processed after the analysis of the related subprogram body.
490 and then Ekind_In
(Body_Id
, E_Function
, E_Generic_Function
)
491 and then not Is_Volatile_Function
(Body_Id
)
493 Check_Nonvolatile_Function_Profile
(Body_Id
);
496 -- Restore the SPARK_Mode of the enclosing context after all delayed
497 -- pragmas have been analyzed.
499 Restore_SPARK_Mode
(Mode
);
501 -- Capture all global references in a generic subprogram body now that
502 -- the contract has been analyzed.
504 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
505 Save_Global_References_In_Contract
506 (Templ
=> Original_Node
(Body_Decl
),
510 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
511 -- invariants and predicates associated with body and its spec. Do not
512 -- expand the contract of subprogram body stubs.
514 if Nkind
(Body_Decl
) = N_Subprogram_Body
then
515 Expand_Subprogram_Contract
(Body_Id
);
517 end Analyze_Entry_Or_Subprogram_Body_Contract
;
519 ------------------------------------------
520 -- Analyze_Entry_Or_Subprogram_Contract --
521 ------------------------------------------
523 procedure Analyze_Entry_Or_Subprogram_Contract
524 (Subp_Id
: Entity_Id
;
525 Freeze_Id
: Entity_Id
:= Empty
)
527 Items
: constant Node_Id
:= Contract
(Subp_Id
);
528 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
530 Skip_Assert_Exprs
: constant Boolean :=
531 Ekind_In
(Subp_Id
, E_Entry
, E_Entry_Family
)
532 and then not ASIS_Mode
533 and then not GNATprove_Mode
;
535 Depends
: Node_Id
:= Empty
;
536 Global
: Node_Id
:= Empty
;
537 Mode
: SPARK_Mode_Type
;
542 -- Do not analyze a contract multiple times
544 if Present
(Items
) then
545 if Analyzed
(Items
) then
548 Set_Analyzed
(Items
);
552 -- Due to the timing of contract analysis, delayed pragmas may be
553 -- subject to the wrong SPARK_Mode, usually that of the enclosing
554 -- context. To remedy this, restore the original SPARK_Mode of the
555 -- related subprogram body.
557 Save_SPARK_Mode_And_Set
(Subp_Id
, Mode
);
559 -- All subprograms carry a contract, but for some it is not significant
560 -- and should not be processed.
562 if not Has_Significant_Contract
(Subp_Id
) then
565 elsif Present
(Items
) then
567 -- Do not analyze the pre/postconditions of an entry declaration
568 -- unless annotating the original tree for ASIS or GNATprove. The
569 -- real analysis occurs when the pre/postconditons are relocated to
570 -- the contract wrapper procedure (see Build_Contract_Wrapper).
572 if Skip_Assert_Exprs
then
575 -- Otherwise analyze the pre/postconditions
578 Prag
:= Pre_Post_Conditions
(Items
);
579 while Present
(Prag
) loop
580 Analyze_Pre_Post_Condition_In_Decl_Part
(Prag
, Freeze_Id
);
581 Prag
:= Next_Pragma
(Prag
);
585 -- Analyze contract-cases and test-cases
587 Prag
:= Contract_Test_Cases
(Items
);
588 while Present
(Prag
) loop
589 Prag_Nam
:= Pragma_Name
(Prag
);
591 if Prag_Nam
= Name_Contract_Cases
then
593 -- Do not analyze the contract cases of an entry declaration
594 -- unless annotating the original tree for ASIS or GNATprove.
595 -- The real analysis occurs when the contract cases are moved
596 -- to the contract wrapper procedure (Build_Contract_Wrapper).
598 if Skip_Assert_Exprs
then
601 -- Otherwise analyze the contract cases
604 Analyze_Contract_Cases_In_Decl_Part
(Prag
, Freeze_Id
);
607 pragma Assert
(Prag_Nam
= Name_Test_Case
);
608 Analyze_Test_Case_In_Decl_Part
(Prag
);
611 Prag
:= Next_Pragma
(Prag
);
614 -- Analyze classification pragmas
616 Prag
:= Classifications
(Items
);
617 while Present
(Prag
) loop
618 Prag_Nam
:= Pragma_Name
(Prag
);
620 if Prag_Nam
= Name_Depends
then
623 elsif Prag_Nam
= Name_Global
then
627 Prag
:= Next_Pragma
(Prag
);
630 -- Analyze Global first, as Depends may mention items classified in
631 -- the global categorization.
633 if Present
(Global
) then
634 Analyze_Global_In_Decl_Part
(Global
);
637 -- Depends must be analyzed after Global in order to see the modes of
640 if Present
(Depends
) then
641 Analyze_Depends_In_Decl_Part
(Depends
);
644 -- Ensure that the contract cases or postconditions mention 'Result
645 -- or define a post-state.
647 Check_Result_And_Post_State
(Subp_Id
);
650 -- A nonvolatile function cannot have an effectively volatile formal
651 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
652 -- only when SPARK_Mode is on, as it is not a standard legality rule.
653 -- The check is performed here because pragma Volatile_Function is
654 -- processed after the analysis of the related subprogram declaration.
657 and then Ekind_In
(Subp_Id
, E_Function
, E_Generic_Function
)
658 and then not Is_Volatile_Function
(Subp_Id
)
660 Check_Nonvolatile_Function_Profile
(Subp_Id
);
663 -- Restore the SPARK_Mode of the enclosing context after all delayed
664 -- pragmas have been analyzed.
666 Restore_SPARK_Mode
(Mode
);
668 -- Capture all global references in a generic subprogram now that the
669 -- contract has been analyzed.
671 if Is_Generic_Declaration_Or_Body
(Subp_Decl
) then
672 Save_Global_References_In_Contract
673 (Templ
=> Original_Node
(Subp_Decl
),
676 end Analyze_Entry_Or_Subprogram_Contract
;
678 -----------------------------
679 -- Analyze_Object_Contract --
680 -----------------------------
682 procedure Analyze_Object_Contract
684 Freeze_Id
: Entity_Id
:= Empty
)
686 Obj_Typ
: constant Entity_Id
:= Etype
(Obj_Id
);
687 AR_Val
: Boolean := False;
688 AW_Val
: Boolean := False;
689 ER_Val
: Boolean := False;
690 EW_Val
: Boolean := False;
692 Mode
: SPARK_Mode_Type
;
695 Restore_Mode
: Boolean := False;
696 Seen
: Boolean := False;
699 -- The loop parameter in an element iterator over a formal container
700 -- is declared with an object declaration, but no contracts apply.
702 if Ekind
(Obj_Id
) = E_Loop_Parameter
then
706 -- Do not analyze a contract multiple times
708 Items
:= Contract
(Obj_Id
);
710 if Present
(Items
) then
711 if Analyzed
(Items
) then
714 Set_Analyzed
(Items
);
718 -- The anonymous object created for a single concurrent type inherits
719 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
720 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
721 -- of the enclosing context. To remedy this, restore the original mode
722 -- of the related anonymous object.
724 if Is_Single_Concurrent_Object
(Obj_Id
)
725 and then Present
(SPARK_Pragma
(Obj_Id
))
727 Restore_Mode
:= True;
728 Save_SPARK_Mode_And_Set
(Obj_Id
, Mode
);
731 -- Constant-related checks
733 if Ekind
(Obj_Id
) = E_Constant
then
735 -- Analyze indicator Part_Of
737 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
739 -- Check whether the lack of indicator Part_Of agrees with the
740 -- placement of the constant with respect to the state space.
743 Check_Missing_Part_Of
(Obj_Id
);
746 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
747 -- This check is relevant only when SPARK_Mode is on, as it is not
748 -- a standard Ada legality rule. Internally-generated constants that
749 -- map generic formals to actuals in instantiations are allowed to
753 and then Comes_From_Source
(Obj_Id
)
754 and then Is_Effectively_Volatile
(Obj_Id
)
755 and then No
(Corresponding_Generic_Association
(Parent
(Obj_Id
)))
757 Error_Msg_N
("constant cannot be volatile", Obj_Id
);
760 -- Variable-related checks
762 else pragma Assert
(Ekind
(Obj_Id
) = E_Variable
);
764 -- Analyze all external properties
766 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Readers
);
768 if Present
(Prag
) then
769 Analyze_External_Property_In_Decl_Part
(Prag
, AR_Val
);
773 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Async_Writers
);
775 if Present
(Prag
) then
776 Analyze_External_Property_In_Decl_Part
(Prag
, AW_Val
);
780 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Reads
);
782 if Present
(Prag
) then
783 Analyze_External_Property_In_Decl_Part
(Prag
, ER_Val
);
787 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Effective_Writes
);
789 if Present
(Prag
) then
790 Analyze_External_Property_In_Decl_Part
(Prag
, EW_Val
);
794 -- Verify the mutual interaction of the various external properties
797 Check_External_Properties
(Obj_Id
, AR_Val
, AW_Val
, ER_Val
, EW_Val
);
800 -- The anonymous object created for a single concurrent type carries
801 -- pragmas Depends and Globat of the type.
803 if Is_Single_Concurrent_Object
(Obj_Id
) then
805 -- Analyze Global first, as Depends may mention items classified
806 -- in the global categorization.
808 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Global
);
810 if Present
(Prag
) then
811 Analyze_Global_In_Decl_Part
(Prag
);
814 -- Depends must be analyzed after Global in order to see the modes
815 -- of all global items.
817 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Depends
);
819 if Present
(Prag
) then
820 Analyze_Depends_In_Decl_Part
(Prag
);
824 Prag
:= Get_Pragma
(Obj_Id
, Pragma_Part_Of
);
826 -- Analyze indicator Part_Of
828 if Present
(Prag
) then
829 Analyze_Part_Of_In_Decl_Part
(Prag
, Freeze_Id
);
831 -- The variable is a constituent of a single protected/task type
832 -- and behaves as a component of the type. Verify that references
833 -- to the variable occur within the definition or body of the type
836 if Present
(Encapsulating_State
(Obj_Id
))
837 and then Is_Single_Concurrent_Object
838 (Encapsulating_State
(Obj_Id
))
839 and then Present
(Part_Of_References
(Obj_Id
))
841 Ref_Elmt
:= First_Elmt
(Part_Of_References
(Obj_Id
));
842 while Present
(Ref_Elmt
) loop
843 Check_Part_Of_Reference
(Obj_Id
, Node
(Ref_Elmt
));
844 Next_Elmt
(Ref_Elmt
);
848 -- Otherwise check whether the lack of indicator Part_Of agrees with
849 -- the placement of the variable with respect to the state space.
852 Check_Missing_Part_Of
(Obj_Id
);
855 -- The following checks are relevant only when SPARK_Mode is on, as
856 -- they are not standard Ada legality rules. Internally generated
857 -- temporaries are ignored.
859 if SPARK_Mode
= On
and then Comes_From_Source
(Obj_Id
) then
860 if Is_Effectively_Volatile
(Obj_Id
) then
862 -- The declaration of an effectively volatile object must
863 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
865 if not Is_Library_Level_Entity
(Obj_Id
) then
867 ("volatile variable & must be declared at library level",
870 -- An object of a discriminated type cannot be effectively
871 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
873 elsif Has_Discriminants
(Obj_Typ
)
874 and then not Is_Protected_Type
(Obj_Typ
)
877 ("discriminated object & cannot be volatile", Obj_Id
);
879 -- An object of a tagged type cannot be effectively volatile
880 -- (SPARK RM C.6(5)).
882 elsif Is_Tagged_Type
(Obj_Typ
) then
883 Error_Msg_N
("tagged object & cannot be volatile", Obj_Id
);
886 -- The object is not effectively volatile
889 -- A non-effectively volatile object cannot have effectively
890 -- volatile components (SPARK RM 7.1.3(6)).
892 if not Is_Effectively_Volatile
(Obj_Id
)
893 and then Has_Volatile_Component
(Obj_Typ
)
896 ("non-volatile object & cannot have volatile components",
905 if Comes_From_Source
(Obj_Id
) and then Is_Ghost_Entity
(Obj_Id
) then
907 -- A Ghost object cannot be of a type that yields a synchronized
908 -- object (SPARK RM 6.9(19)).
910 if Yields_Synchronized_Object
(Obj_Typ
) then
911 Error_Msg_N
("ghost object & cannot be synchronized", Obj_Id
);
913 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
914 -- SPARK RM 6.9(19)).
916 elsif Is_Effectively_Volatile
(Obj_Id
) then
917 Error_Msg_N
("ghost object & cannot be volatile", Obj_Id
);
919 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
920 -- One exception to this is the object that represents the dispatch
921 -- table of a Ghost tagged type, as the symbol needs to be exported.
923 elsif Is_Exported
(Obj_Id
) then
924 Error_Msg_N
("ghost object & cannot be exported", Obj_Id
);
926 elsif Is_Imported
(Obj_Id
) then
927 Error_Msg_N
("ghost object & cannot be imported", Obj_Id
);
931 -- Restore the SPARK_Mode of the enclosing context after all delayed
932 -- pragmas have been analyzed.
935 Restore_SPARK_Mode
(Mode
);
937 end Analyze_Object_Contract
;
939 -----------------------------------
940 -- Analyze_Package_Body_Contract --
941 -----------------------------------
943 procedure Analyze_Package_Body_Contract
944 (Body_Id
: Entity_Id
;
945 Freeze_Id
: Entity_Id
:= Empty
)
947 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
948 Items
: constant Node_Id
:= Contract
(Body_Id
);
949 Spec_Id
: constant Entity_Id
:= Spec_Entity
(Body_Id
);
950 Mode
: SPARK_Mode_Type
;
954 -- Do not analyze a contract multiple times
956 if Present
(Items
) then
957 if Analyzed
(Items
) then
960 Set_Analyzed
(Items
);
964 -- Due to the timing of contract analysis, delayed pragmas may be
965 -- subject to the wrong SPARK_Mode, usually that of the enclosing
966 -- context. To remedy this, restore the original SPARK_Mode of the
967 -- related package body.
969 Save_SPARK_Mode_And_Set
(Body_Id
, Mode
);
971 Ref_State
:= Get_Pragma
(Body_Id
, Pragma_Refined_State
);
973 -- The analysis of pragma Refined_State detects whether the spec has
974 -- abstract states available for refinement.
976 if Present
(Ref_State
) then
977 Analyze_Refined_State_In_Decl_Part
(Ref_State
, Freeze_Id
);
980 -- Restore the SPARK_Mode of the enclosing context after all delayed
981 -- pragmas have been analyzed.
983 Restore_SPARK_Mode
(Mode
);
985 -- Capture all global references in a generic package body now that the
986 -- contract has been analyzed.
988 if Is_Generic_Declaration_Or_Body
(Body_Decl
) then
989 Save_Global_References_In_Contract
990 (Templ
=> Original_Node
(Body_Decl
),
993 end Analyze_Package_Body_Contract
;
995 ------------------------------
996 -- Analyze_Package_Contract --
997 ------------------------------
999 procedure Analyze_Package_Contract
(Pack_Id
: Entity_Id
) is
1000 Items
: constant Node_Id
:= Contract
(Pack_Id
);
1001 Pack_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Pack_Id
);
1002 Init
: Node_Id
:= Empty
;
1003 Init_Cond
: Node_Id
:= Empty
;
1004 Mode
: SPARK_Mode_Type
;
1009 -- Do not analyze a contract multiple times
1011 if Present
(Items
) then
1012 if Analyzed
(Items
) then
1015 Set_Analyzed
(Items
);
1019 -- Due to the timing of contract analysis, delayed pragmas may be
1020 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1021 -- context. To remedy this, restore the original SPARK_Mode of the
1024 Save_SPARK_Mode_And_Set
(Pack_Id
, Mode
);
1026 if Present
(Items
) then
1028 -- Locate and store pragmas Initial_Condition and Initializes, since
1029 -- their order of analysis matters.
1031 Prag
:= Classifications
(Items
);
1032 while Present
(Prag
) loop
1033 Prag_Nam
:= Pragma_Name
(Prag
);
1035 if Prag_Nam
= Name_Initial_Condition
then
1038 elsif Prag_Nam
= Name_Initializes
then
1042 Prag
:= Next_Pragma
(Prag
);
1045 -- Analyze the initialization-related pragmas. Initializes must come
1046 -- before Initial_Condition due to item dependencies.
1048 if Present
(Init
) then
1049 Analyze_Initializes_In_Decl_Part
(Init
);
1052 if Present
(Init_Cond
) then
1053 Analyze_Initial_Condition_In_Decl_Part
(Init_Cond
);
1057 -- Check whether the lack of indicator Part_Of agrees with the placement
1058 -- of the package instantiation with respect to the state space.
1060 if Is_Generic_Instance
(Pack_Id
) then
1061 Prag
:= Get_Pragma
(Pack_Id
, Pragma_Part_Of
);
1064 Check_Missing_Part_Of
(Pack_Id
);
1068 -- Restore the SPARK_Mode of the enclosing context after all delayed
1069 -- pragmas have been analyzed.
1071 Restore_SPARK_Mode
(Mode
);
1073 -- Capture all global references in a generic package now that the
1074 -- contract has been analyzed.
1076 if Is_Generic_Declaration_Or_Body
(Pack_Decl
) then
1077 Save_Global_References_In_Contract
1078 (Templ
=> Original_Node
(Pack_Decl
),
1081 end Analyze_Package_Contract
;
1083 --------------------------------
1084 -- Analyze_Previous_Contracts --
1085 --------------------------------
1087 procedure Analyze_Previous_Contracts
(Body_Decl
: Node_Id
) is
1088 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_Decl
);
1089 Orig_Decl
: constant Node_Id
:= Original_Node
(Body_Decl
);
1094 -- A body that is in the process of being inlined appears from source,
1095 -- but carries name _parent. Such a body does not cause "freezing" of
1098 if Chars
(Body_Id
) = Name_uParent
then
1102 -- Climb the parent chain looking for an enclosing package body. Do not
1103 -- use the scope stack, as a body uses the entity of its corresponding
1106 Par
:= Parent
(Body_Decl
);
1107 while Present
(Par
) loop
1108 if Nkind
(Par
) = N_Package_Body
then
1109 Analyze_Package_Body_Contract
1110 (Body_Id
=> Defining_Entity
(Par
),
1111 Freeze_Id
=> Defining_Entity
(Body_Decl
));
1115 -- Do not look for an enclosing package body when the construct which
1116 -- causes freezing is a body generated for an expression function and
1117 -- it appears within a package spec. This ensures that the traversal
1118 -- will not reach too far up the parent chain and attempt to freeze a
1119 -- package body which should not be frozen.
1121 -- package body Enclosing_Body
1122 -- with Refined_State => (State => Var)
1124 -- package Nested is
1125 -- type Some_Type is ...;
1126 -- function Cause_Freezing return ...;
1128 -- function Cause_Freezing is (...);
1131 -- Var : Nested.Some_Type;
1133 elsif Nkind
(Par
) = N_Package_Declaration
1134 and then Nkind
(Orig_Decl
) = N_Expression_Function
1139 Par
:= Parent
(Par
);
1142 -- Analyze the contracts of all eligible construct up to the body which
1143 -- caused the "freezing".
1145 if Is_List_Member
(Body_Decl
) then
1147 (L
=> List_Containing
(Body_Decl
),
1148 Freeze_Nod
=> Body_Decl
,
1149 Freeze_Id
=> Body_Id
);
1151 end Analyze_Previous_Contracts
;
1153 --------------------------------
1154 -- Analyze_Protected_Contract --
1155 --------------------------------
1157 procedure Analyze_Protected_Contract
(Prot_Id
: Entity_Id
) is
1158 Items
: constant Node_Id
:= Contract
(Prot_Id
);
1161 -- Do not analyze a contract multiple times
1163 if Present
(Items
) then
1164 if Analyzed
(Items
) then
1167 Set_Analyzed
(Items
);
1170 end Analyze_Protected_Contract
;
1172 -------------------------------------------
1173 -- Analyze_Subprogram_Body_Stub_Contract --
1174 -------------------------------------------
1176 procedure Analyze_Subprogram_Body_Stub_Contract
(Stub_Id
: Entity_Id
) is
1177 Stub_Decl
: constant Node_Id
:= Parent
(Parent
(Stub_Id
));
1178 Spec_Id
: constant Entity_Id
:= Corresponding_Spec_Of_Stub
(Stub_Decl
);
1181 -- A subprogram body stub may act as its own spec or as the completion
1182 -- of a previous declaration. Depending on the context, the contract of
1183 -- the stub may contain two sets of pragmas.
1185 -- The stub is a completion, the applicable pragmas are:
1189 if Present
(Spec_Id
) then
1190 Analyze_Entry_Or_Subprogram_Body_Contract
(Stub_Id
);
1192 -- The stub acts as its own spec, the applicable pragmas are:
1201 Analyze_Entry_Or_Subprogram_Contract
(Stub_Id
);
1203 end Analyze_Subprogram_Body_Stub_Contract
;
1205 ---------------------------
1206 -- Analyze_Task_Contract --
1207 ---------------------------
1209 procedure Analyze_Task_Contract
(Task_Id
: Entity_Id
) is
1210 Items
: constant Node_Id
:= Contract
(Task_Id
);
1211 Mode
: SPARK_Mode_Type
;
1215 -- Do not analyze a contract multiple times
1217 if Present
(Items
) then
1218 if Analyzed
(Items
) then
1221 Set_Analyzed
(Items
);
1225 -- Due to the timing of contract analysis, delayed pragmas may be
1226 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1227 -- context. To remedy this, restore the original SPARK_Mode of the
1228 -- related task unit.
1230 Save_SPARK_Mode_And_Set
(Task_Id
, Mode
);
1232 -- Analyze Global first, as Depends may mention items classified in the
1233 -- global categorization.
1235 Prag
:= Get_Pragma
(Task_Id
, Pragma_Global
);
1237 if Present
(Prag
) then
1238 Analyze_Global_In_Decl_Part
(Prag
);
1241 -- Depends must be analyzed after Global in order to see the modes of
1242 -- all global items.
1244 Prag
:= Get_Pragma
(Task_Id
, Pragma_Depends
);
1246 if Present
(Prag
) then
1247 Analyze_Depends_In_Decl_Part
(Prag
);
1250 -- Restore the SPARK_Mode of the enclosing context after all delayed
1251 -- pragmas have been analyzed.
1253 Restore_SPARK_Mode
(Mode
);
1254 end Analyze_Task_Contract
;
1256 -------------------------------------------------
1257 -- Build_And_Analyze_Contract_Only_Subprograms --
1258 -------------------------------------------------
1260 procedure Build_And_Analyze_Contract_Only_Subprograms
(L
: List_Id
) is
1261 procedure Analyze_Contract_Only_Subprograms
;
1262 -- Analyze the contract-only subprograms of L
1264 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
);
1265 -- Append the contract-only bodies of Subp_List to its declarations list
1267 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
;
1268 -- If E is an entity for a non-imported subprogram specification with
1269 -- pre/postconditions and we are compiling with CodePeer mode, then
1270 -- this procedure will create a wrapper to help Gnat2scil process its
1271 -- contracts. Return Empty if the wrapper cannot be built.
1273 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
;
1274 -- Build the contract-only subprograms of all eligible subprograms found
1277 function Has_Private_Declarations
(N
: Node_Id
) return Boolean;
1278 -- Return True for package specs, task definitions, and protected type
1279 -- definitions whose list of private declarations is not empty.
1281 ---------------------------------------
1282 -- Analyze_Contract_Only_Subprograms --
1283 ---------------------------------------
1285 procedure Analyze_Contract_Only_Subprograms
is
1286 procedure Analyze_Contract_Only_Bodies
;
1287 -- Analyze all the contract-only bodies of L
1289 ----------------------------------
1290 -- Analyze_Contract_Only_Bodies --
1291 ----------------------------------
1293 procedure Analyze_Contract_Only_Bodies
is
1298 while Present
(Decl
) loop
1299 if Nkind
(Decl
) = N_Subprogram_Body
1300 and then Is_Contract_Only_Body
1301 (Defining_Unit_Name
(Specification
(Decl
)))
1308 end Analyze_Contract_Only_Bodies
;
1310 -- Start of processing for Analyze_Contract_Only_Subprograms
1313 if Ekind
(Current_Scope
) /= E_Package
then
1314 Analyze_Contract_Only_Bodies
;
1318 Pkg_Spec
: constant Node_Id
:=
1319 Package_Specification
(Current_Scope
);
1322 if not Has_Private_Declarations
(Pkg_Spec
) then
1323 Analyze_Contract_Only_Bodies
;
1325 -- For packages with private declarations, the contract-only
1326 -- bodies of subprograms defined in the visible part of the
1327 -- package are added to its private declarations (to ensure
1328 -- that they do not cause premature freezing of types and also
1329 -- that they are analyzed with proper visibility). Hence they
1330 -- will be analyzed later.
1332 elsif Visible_Declarations
(Pkg_Spec
) = L
then
1335 elsif Private_Declarations
(Pkg_Spec
) = L
then
1336 Analyze_Contract_Only_Bodies
;
1340 end Analyze_Contract_Only_Subprograms
;
1342 --------------------------------------
1343 -- Append_Contract_Only_Subprograms --
1344 --------------------------------------
1346 procedure Append_Contract_Only_Subprograms
(Subp_List
: List_Id
) is
1348 if No
(Subp_List
) then
1352 if Ekind
(Current_Scope
) /= E_Package
then
1353 Append_List
(Subp_List
, To
=> L
);
1357 Pkg_Spec
: constant Node_Id
:=
1358 Package_Specification
(Current_Scope
);
1361 if not Has_Private_Declarations
(Pkg_Spec
) then
1362 Append_List
(Subp_List
, To
=> L
);
1364 -- If the package has private declarations then append them to
1365 -- its private declarations; they will be analyzed when the
1366 -- contracts of its private declarations are analyzed.
1371 To
=> Private_Declarations
(Pkg_Spec
));
1375 end Append_Contract_Only_Subprograms
;
1377 ------------------------------------
1378 -- Build_Contract_Only_Subprogram --
1379 ------------------------------------
1381 -- This procedure takes care of building a wrapper to generate better
1382 -- analysis results in the case of a call to a subprogram whose body
1383 -- is unavailable to CodePeer but whose specification includes Pre/Post
1384 -- conditions. The body might be unavailable for any of a number or
1385 -- reasons (it is imported, the .adb file is simply missing, or the
1386 -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
1387 -- pragma). The built subprogram has the following contents:
1388 -- * check preconditions
1389 -- * call the subprogram
1390 -- * check postconditions
1392 function Build_Contract_Only_Subprogram
(E
: Entity_Id
) return Node_Id
is
1393 Loc
: constant Source_Ptr
:= Sloc
(E
);
1395 Missing_Body_Name
: constant Name_Id
:=
1396 New_External_Name
(Chars
(E
), "__missing_body");
1398 function Build_Missing_Body_Decls
return List_Id
;
1399 -- Build the declaration of the missing body subprogram and its
1400 -- corresponding pragma Import.
1402 function Build_Missing_Body_Subprogram_Call
return Node_Id
;
1403 -- Build the call to the missing body subprogram
1405 function Skip_Contract_Only_Subprogram
(E
: Entity_Id
) return Boolean;
1406 -- Return True for cases where the wrapper is not needed or we cannot
1409 ------------------------------
1410 -- Build_Missing_Body_Decls --
1411 ------------------------------
1413 function Build_Missing_Body_Decls
return List_Id
is
1414 Spec
: constant Node_Id
:= Declaration_Node
(E
);
1420 Make_Subprogram_Declaration
(Loc
, Copy_Subprogram_Spec
(Spec
));
1421 Set_Chars
(Defining_Entity
(Decl
), Missing_Body_Name
);
1425 Chars
=> Name_Import
,
1426 Pragma_Argument_Associations
=> New_List
(
1427 Make_Pragma_Argument_Association
(Loc
,
1428 Expression
=> Make_Identifier
(Loc
, Name_Ada
)),
1430 Make_Pragma_Argument_Association
(Loc
,
1431 Expression
=> Make_Identifier
(Loc
, Missing_Body_Name
))));
1433 return New_List
(Decl
, Prag
);
1434 end Build_Missing_Body_Decls
;
1436 ----------------------------------------
1437 -- Build_Missing_Body_Subprogram_Call --
1438 ----------------------------------------
1440 function Build_Missing_Body_Subprogram_Call
return Node_Id
is
1447 -- Build parameter list that we need
1449 Forml
:= First_Formal
(E
);
1450 while Present
(Forml
) loop
1451 Append_To
(Parms
, Make_Identifier
(Loc
, Chars
(Forml
)));
1452 Next_Formal
(Forml
);
1455 -- Build the call to the missing body subprogram
1457 if Ekind_In
(E
, E_Function
, E_Generic_Function
) then
1459 Make_Simple_Return_Statement
(Loc
,
1461 Make_Function_Call
(Loc
,
1463 Make_Identifier
(Loc
, Missing_Body_Name
),
1464 Parameter_Associations
=> Parms
));
1468 Make_Procedure_Call_Statement
(Loc
,
1470 Make_Identifier
(Loc
, Missing_Body_Name
),
1471 Parameter_Associations
=> Parms
);
1473 end Build_Missing_Body_Subprogram_Call
;
1475 -----------------------------------
1476 -- Skip_Contract_Only_Subprogram --
1477 -----------------------------------
1479 function Skip_Contract_Only_Subprogram
1480 (E
: Entity_Id
) return Boolean
1482 function Depends_On_Enclosing_Private_Type
return Boolean;
1483 -- Return True if some formal of E (or its return type) are
1484 -- private types defined in an enclosing package.
1486 function Some_Enclosing_Package_Has_Private_Decls
return Boolean;
1487 -- Return True if some enclosing package of the current scope has
1488 -- private declarations.
1490 ---------------------------------------
1491 -- Depends_On_Enclosing_Private_Type --
1492 ---------------------------------------
1494 function Depends_On_Enclosing_Private_Type
return Boolean is
1495 function Defined_In_Enclosing_Package
1496 (Typ
: Entity_Id
) return Boolean;
1497 -- Return True if Typ is an entity defined in an enclosing
1498 -- package of the current scope.
1500 ----------------------------------
1501 -- Defined_In_Enclosing_Package --
1502 ----------------------------------
1504 function Defined_In_Enclosing_Package
1505 (Typ
: Entity_Id
) return Boolean
1507 Scop
: Entity_Id
:= Scope
(Current_Scope
);
1510 while Scop
/= Scope
(Typ
)
1511 and then not Is_Compilation_Unit
(Scop
)
1513 Scop
:= Scope
(Scop
);
1516 return Scop
= Scope
(Typ
);
1517 end Defined_In_Enclosing_Package
;
1521 Param_E
: Entity_Id
;
1524 -- Start of processing for Depends_On_Enclosing_Private_Type
1527 Param_E
:= First_Entity
(E
);
1528 while Present
(Param_E
) loop
1529 Typ
:= Etype
(Param_E
);
1531 if Is_Private_Type
(Typ
)
1532 and then Defined_In_Enclosing_Package
(Typ
)
1537 Next_Entity
(Param_E
);
1541 Ekind
(E
) = E_Function
1542 and then Is_Private_Type
(Etype
(E
))
1543 and then Defined_In_Enclosing_Package
(Etype
(E
));
1544 end Depends_On_Enclosing_Private_Type
;
1546 ----------------------------------------------
1547 -- Some_Enclosing_Package_Has_Private_Decls --
1548 ----------------------------------------------
1550 function Some_Enclosing_Package_Has_Private_Decls
return Boolean is
1551 Scop
: Entity_Id
:= Current_Scope
;
1552 Pkg_Spec
: Node_Id
:= Package_Specification
(Scop
);
1556 if Ekind
(Scop
) = E_Package
1557 and then Has_Private_Declarations
1558 (Package_Specification
(Scop
))
1560 Pkg_Spec
:= Package_Specification
(Scop
);
1563 exit when Is_Compilation_Unit
(Scop
);
1564 Scop
:= Scope
(Scop
);
1567 return Pkg_Spec
/= Package_Specification
(Current_Scope
);
1568 end Some_Enclosing_Package_Has_Private_Decls
;
1570 -- Start of processing for Skip_Contract_Only_Subprogram
1573 if not CodePeer_Mode
1574 or else Inside_A_Generic
1575 or else not Is_Subprogram
(E
)
1576 or else Is_Abstract_Subprogram
(E
)
1577 or else Is_Imported
(E
)
1578 or else No
(Contract
(E
))
1579 or else No
(Pre_Post_Conditions
(Contract
(E
)))
1580 or else Is_Contract_Only_Body
(E
)
1581 or else Convention
(E
) = Convention_Protected
1585 -- We do not support building the contract-only subprogram if E
1586 -- is a subprogram declared in a nested package that has some
1587 -- formal or return type depending on a private type defined in
1588 -- an enclosing package.
1590 elsif Ekind
(Current_Scope
) = E_Package
1591 and then Some_Enclosing_Package_Has_Private_Decls
1592 and then Depends_On_Enclosing_Private_Type
1594 if Debug_Flag_Dot_KK
then
1596 Saved_Mode
: constant Warning_Mode_Type
:= Warning_Mode
;
1599 -- Warnings are disabled by default under CodePeer_Mode
1600 -- (see switch-c). Enable them temporarily.
1602 Warning_Mode
:= Normal
;
1604 ("cannot generate contract-only subprogram?", E
);
1605 Warning_Mode
:= Saved_Mode
;
1613 end Skip_Contract_Only_Subprogram
;
1615 -- Start of processing for Build_Contract_Only_Subprogram
1618 -- Test cases where the wrapper is not needed and cases where we
1621 if Skip_Contract_Only_Subprogram
(E
) then
1625 -- Note on calls to Copy_Separate_Tree. The trees we are copying
1626 -- here are fully analyzed, but we definitely want fully syntactic
1627 -- unanalyzed trees in the body we construct, so that the analysis
1628 -- generates the right visibility, and that is exactly what the
1629 -- calls to Copy_Separate_Tree give us.
1632 Name
: constant Name_Id
:=
1633 New_External_Name
(Chars
(E
), "__contract_only");
1639 Make_Subprogram_Body
(Loc
,
1641 Copy_Subprogram_Spec
(Declaration_Node
(E
)),
1643 Build_Missing_Body_Decls
,
1644 Handled_Statement_Sequence
=>
1645 Make_Handled_Sequence_Of_Statements
(Loc
,
1646 Statements
=> New_List
(
1647 Build_Missing_Body_Subprogram_Call
),
1648 End_Label
=> Make_Identifier
(Loc
, Name
)));
1650 Id
:= Defining_Unit_Name
(Specification
(Bod
));
1652 -- Copy only the pre/postconditions of the original contract
1653 -- since it is what we need, but also because pragmas stored in
1654 -- the other fields have N_Pragmas with N_Aspect_Specifications
1655 -- that reference their associated pragma (thus causing an endless
1656 -- loop when trying to copy the subtree).
1659 New_Contract
: constant Node_Id
:= Make_Contract
(Sloc
(E
));
1662 Set_Pre_Post_Conditions
(New_Contract
,
1663 Copy_Separate_Tree
(Pre_Post_Conditions
(Contract
(E
))));
1664 Set_Contract
(Id
, New_Contract
);
1667 -- Fix the name of this new subprogram and link the original
1668 -- subprogram with its Contract_Only_Body subprogram.
1670 Set_Chars
(Id
, Name
);
1671 Set_Is_Contract_Only_Body
(Id
);
1672 Set_Contract_Only_Body
(E
, Id
);
1676 end Build_Contract_Only_Subprogram
;
1678 -------------------------------------
1679 -- Build_Contract_Only_Subprograms --
1680 -------------------------------------
1682 function Build_Contract_Only_Subprograms
(L
: List_Id
) return List_Id
is
1685 Result
: List_Id
:= No_List
;
1686 Subp_Id
: Entity_Id
;
1690 while Present
(Decl
) loop
1691 if Nkind
(Decl
) = N_Subprogram_Declaration
then
1692 Subp_Id
:= Defining_Unit_Name
(Specification
(Decl
));
1693 New_Subp
:= Build_Contract_Only_Subprogram
(Subp_Id
);
1695 if Present
(New_Subp
) then
1700 Append_To
(Result
, New_Subp
);
1708 end Build_Contract_Only_Subprograms
;
1710 ------------------------------
1711 -- Has_Private_Declarations --
1712 ------------------------------
1714 function Has_Private_Declarations
(N
: Node_Id
) return Boolean is
1716 if not Nkind_In
(N
, N_Package_Specification
,
1717 N_Protected_Definition
,
1723 Present
(Private_Declarations
(N
))
1724 and then Is_Non_Empty_List
(Private_Declarations
(N
));
1726 end Has_Private_Declarations
;
1730 Subp_List
: List_Id
;
1732 -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
1735 Subp_List
:= Build_Contract_Only_Subprograms
(L
);
1736 Append_Contract_Only_Subprograms
(Subp_List
);
1737 Analyze_Contract_Only_Subprograms
;
1738 end Build_And_Analyze_Contract_Only_Subprograms
;
1740 -----------------------------
1741 -- Create_Generic_Contract --
1742 -----------------------------
1744 procedure Create_Generic_Contract
(Unit
: Node_Id
) is
1745 Templ
: constant Node_Id
:= Original_Node
(Unit
);
1746 Templ_Id
: constant Entity_Id
:= Defining_Entity
(Templ
);
1748 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
);
1749 -- Add a single contract-related source pragma Prag to the contract of
1750 -- generic template Templ_Id.
1752 ---------------------------------
1753 -- Add_Generic_Contract_Pragma --
1754 ---------------------------------
1756 procedure Add_Generic_Contract_Pragma
(Prag
: Node_Id
) is
1757 Prag_Templ
: Node_Id
;
1760 -- Mark the pragma to prevent the premature capture of global
1761 -- references when capturing global references of the context
1762 -- (see Save_References_In_Pragma).
1764 Set_Is_Generic_Contract_Pragma
(Prag
);
1766 -- Pragmas that apply to a generic subprogram declaration are not
1767 -- part of the semantic structure of the generic template:
1770 -- procedure Example (Formal : Integer);
1771 -- pragma Precondition (Formal > 0);
1773 -- Create a generic template for such pragmas and link the template
1774 -- of the pragma with the generic template.
1776 if Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1778 (Prag
, Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> False));
1779 Prag_Templ
:= Original_Node
(Prag
);
1781 Set_Is_Generic_Contract_Pragma
(Prag_Templ
);
1782 Add_Contract_Item
(Prag_Templ
, Templ_Id
);
1784 -- Otherwise link the pragma with the generic template
1787 Add_Contract_Item
(Prag
, Templ_Id
);
1789 end Add_Generic_Contract_Pragma
;
1793 Context
: constant Node_Id
:= Parent
(Unit
);
1794 Decl
: Node_Id
:= Empty
;
1796 -- Start of processing for Create_Generic_Contract
1799 -- A generic package declaration carries contract-related source pragmas
1800 -- in its visible declarations.
1802 if Nkind
(Templ
) = N_Generic_Package_Declaration
then
1803 Set_Ekind
(Templ_Id
, E_Generic_Package
);
1805 if Present
(Visible_Declarations
(Specification
(Templ
))) then
1806 Decl
:= First
(Visible_Declarations
(Specification
(Templ
)));
1809 -- A generic package body carries contract-related source pragmas in its
1812 elsif Nkind
(Templ
) = N_Package_Body
then
1813 Set_Ekind
(Templ_Id
, E_Package_Body
);
1815 if Present
(Declarations
(Templ
)) then
1816 Decl
:= First
(Declarations
(Templ
));
1819 -- Generic subprogram declaration
1821 elsif Nkind
(Templ
) = N_Generic_Subprogram_Declaration
then
1822 if Nkind
(Specification
(Templ
)) = N_Function_Specification
then
1823 Set_Ekind
(Templ_Id
, E_Generic_Function
);
1825 Set_Ekind
(Templ_Id
, E_Generic_Procedure
);
1828 -- When the generic subprogram acts as a compilation unit, inspect
1829 -- the Pragmas_After list for contract-related source pragmas.
1831 if Nkind
(Context
) = N_Compilation_Unit
then
1832 if Present
(Aux_Decls_Node
(Context
))
1833 and then Present
(Pragmas_After
(Aux_Decls_Node
(Context
)))
1835 Decl
:= First
(Pragmas_After
(Aux_Decls_Node
(Context
)));
1838 -- Otherwise inspect the successive declarations for contract-related
1842 Decl
:= Next
(Unit
);
1845 -- A generic subprogram body carries contract-related source pragmas in
1846 -- its declarations.
1848 elsif Nkind
(Templ
) = N_Subprogram_Body
then
1849 Set_Ekind
(Templ_Id
, E_Subprogram_Body
);
1851 if Present
(Declarations
(Templ
)) then
1852 Decl
:= First
(Declarations
(Templ
));
1856 -- Inspect the relevant declarations looking for contract-related source
1857 -- pragmas and add them to the contract of the generic unit.
1859 while Present
(Decl
) loop
1860 if Comes_From_Source
(Decl
) then
1861 if Nkind
(Decl
) = N_Pragma
then
1863 -- The source pragma is a contract annotation
1865 if Is_Contract_Annotation
(Decl
) then
1866 Add_Generic_Contract_Pragma
(Decl
);
1869 -- The region where a contract-related source pragma may appear
1870 -- ends with the first source non-pragma declaration or statement.
1879 end Create_Generic_Contract
;
1881 --------------------------------
1882 -- Expand_Subprogram_Contract --
1883 --------------------------------
1885 procedure Expand_Subprogram_Contract
(Body_Id
: Entity_Id
) is
1886 Body_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Body_Id
);
1887 Spec_Id
: constant Entity_Id
:= Corresponding_Spec
(Body_Decl
);
1889 procedure Add_Invariant_And_Predicate_Checks
1890 (Subp_Id
: Entity_Id
;
1891 Stmts
: in out List_Id
;
1892 Result
: out Node_Id
);
1893 -- Process the result of function Subp_Id (if applicable) and all its
1894 -- formals. Add invariant and predicate checks where applicable. The
1895 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1896 -- function, Result contains the entity of parameter _Result, to be
1897 -- used in the creation of procedure _Postconditions.
1899 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
);
1900 -- Append a node to a list. If there is no list, create a new one. When
1901 -- the item denotes a pragma, it is added to the list only when it is
1904 procedure Build_Postconditions_Procedure
1905 (Subp_Id
: Entity_Id
;
1907 Result
: Entity_Id
);
1908 -- Create the body of procedure _Postconditions which handles various
1909 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1910 -- of statements to be checked on exit. Parameter Result is the entity
1911 -- of parameter _Result when Subp_Id denotes a function.
1913 procedure Process_Contract_Cases
(Stmts
: in out List_Id
);
1914 -- Process pragma Contract_Cases. This routine prepends items to the
1915 -- body declarations and appends items to list Stmts.
1917 procedure Process_Postconditions
(Stmts
: in out List_Id
);
1918 -- Collect all [inherited] spec and body postconditions and accumulate
1919 -- their pragma Check equivalents in list Stmts.
1921 procedure Process_Preconditions
;
1922 -- Collect all [inherited] spec and body preconditions and prepend their
1923 -- pragma Check equivalents to the declarations of the body.
1925 ----------------------------------------
1926 -- Add_Invariant_And_Predicate_Checks --
1927 ----------------------------------------
1929 procedure Add_Invariant_And_Predicate_Checks
1930 (Subp_Id
: Entity_Id
;
1931 Stmts
: in out List_Id
;
1932 Result
: out Node_Id
)
1934 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
);
1935 -- Id denotes the return value of a function or a formal parameter.
1936 -- Add an invariant check if the type of Id is access to a type with
1937 -- invariants. The routine appends the generated code to Stmts.
1939 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean;
1940 -- Determine whether type Typ can benefit from invariant checks. To
1941 -- qualify, the type must have a non-null invariant procedure and
1942 -- subprogram Subp_Id must appear visible from the point of view of
1945 ---------------------------------
1946 -- Add_Invariant_Access_Checks --
1947 ---------------------------------
1949 procedure Add_Invariant_Access_Checks
(Id
: Entity_Id
) is
1950 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
1957 if Is_Access_Type
(Typ
) and then not Is_Access_Constant
(Typ
) then
1958 Typ
:= Designated_Type
(Typ
);
1960 if Invariant_Checks_OK
(Typ
) then
1962 Make_Explicit_Dereference
(Loc
,
1963 Prefix
=> New_Occurrence_Of
(Id
, Loc
));
1964 Set_Etype
(Ref
, Typ
);
1967 -- if <Id> /= null then
1968 -- <invariant_call (<Ref>)>
1973 Make_If_Statement
(Loc
,
1976 Left_Opnd
=> New_Occurrence_Of
(Id
, Loc
),
1977 Right_Opnd
=> Make_Null
(Loc
)),
1978 Then_Statements
=> New_List
(
1979 Make_Invariant_Call
(Ref
))),
1983 end Add_Invariant_Access_Checks
;
1985 -------------------------
1986 -- Invariant_Checks_OK --
1987 -------------------------
1989 function Invariant_Checks_OK
(Typ
: Entity_Id
) return Boolean is
1990 function Has_Public_Visibility_Of_Subprogram
return Boolean;
1991 -- Determine whether type Typ has public visibility of subprogram
1994 -----------------------------------------
1995 -- Has_Public_Visibility_Of_Subprogram --
1996 -----------------------------------------
1998 function Has_Public_Visibility_Of_Subprogram
return Boolean is
1999 Subp_Decl
: constant Node_Id
:= Unit_Declaration_Node
(Subp_Id
);
2002 -- An Initialization procedure must be considered visible even
2003 -- though it is internally generated.
2005 if Is_Init_Proc
(Defining_Entity
(Subp_Decl
)) then
2008 elsif Ekind
(Scope
(Typ
)) /= E_Package
then
2011 -- Internally generated code is never publicly visible except
2012 -- for a subprogram that is the implementation of an expression
2013 -- function. In that case the visibility is determined by the
2016 elsif not Comes_From_Source
(Subp_Decl
)
2018 (Nkind
(Original_Node
(Subp_Decl
)) /= N_Expression_Function
2020 Comes_From_Source
(Defining_Entity
(Subp_Decl
)))
2024 -- Determine whether the subprogram is declared in the visible
2025 -- declarations of the package containing the type.
2028 return List_Containing
(Subp_Decl
) =
2029 Visible_Declarations
2030 (Specification
(Unit_Declaration_Node
(Scope
(Typ
))));
2032 end Has_Public_Visibility_Of_Subprogram
;
2034 -- Start of processing for Invariant_Checks_OK
2038 Has_Invariants
(Typ
)
2039 and then Present
(Invariant_Procedure
(Typ
))
2040 and then not Has_Null_Body
(Invariant_Procedure
(Typ
))
2041 and then Has_Public_Visibility_Of_Subprogram
;
2042 end Invariant_Checks_OK
;
2046 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2047 -- Source location of subprogram body contract
2052 -- Start of processing for Add_Invariant_And_Predicate_Checks
2057 -- Process the result of a function
2059 if Ekind
(Subp_Id
) = E_Function
then
2060 Typ
:= Etype
(Subp_Id
);
2062 -- Generate _Result which is used in procedure _Postconditions to
2063 -- verify the return value.
2065 Result
:= Make_Defining_Identifier
(Loc
, Name_uResult
);
2066 Set_Etype
(Result
, Typ
);
2068 -- Add an invariant check when the return type has invariants and
2069 -- the related function is visible to the outside.
2071 if Invariant_Checks_OK
(Typ
) then
2074 Make_Invariant_Call
(New_Occurrence_Of
(Result
, Loc
)),
2078 -- Add an invariant check when the return type is an access to a
2079 -- type with invariants.
2081 Add_Invariant_Access_Checks
(Result
);
2084 -- Add invariant and predicates for all formals that qualify
2086 Formal
:= First_Formal
(Subp_Id
);
2087 while Present
(Formal
) loop
2088 Typ
:= Etype
(Formal
);
2090 if Ekind
(Formal
) /= E_In_Parameter
2091 or else Is_Access_Type
(Typ
)
2093 if Invariant_Checks_OK
(Typ
) then
2096 Make_Invariant_Call
(New_Occurrence_Of
(Formal
, Loc
)),
2100 Add_Invariant_Access_Checks
(Formal
);
2102 -- Note: we used to add predicate checks for OUT and IN OUT
2103 -- formals here, but that was misguided, since such checks are
2104 -- performed on the caller side, based on the predicate of the
2105 -- actual, rather than the predicate of the formal.
2109 Next_Formal
(Formal
);
2111 end Add_Invariant_And_Predicate_Checks
;
2113 -------------------------
2114 -- Append_Enabled_Item --
2115 -------------------------
2117 procedure Append_Enabled_Item
(Item
: Node_Id
; List
: in out List_Id
) is
2119 -- Do not chain ignored or disabled pragmas
2121 if Nkind
(Item
) = N_Pragma
2122 and then (Is_Ignored
(Item
) or else Is_Disabled
(Item
))
2126 -- Otherwise, add the item
2133 -- If the pragma is a conjunct in a composite postcondition, it
2134 -- has been processed in reverse order. In the postcondition body
2135 -- it must appear before the others.
2137 if Nkind
(Item
) = N_Pragma
2138 and then From_Aspect_Specification
(Item
)
2139 and then Split_PPC
(Item
)
2141 Prepend
(Item
, List
);
2143 Append
(Item
, List
);
2146 end Append_Enabled_Item
;
2148 ------------------------------------
2149 -- Build_Postconditions_Procedure --
2150 ------------------------------------
2152 procedure Build_Postconditions_Procedure
2153 (Subp_Id
: Entity_Id
;
2157 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
);
2158 -- Insert node Stmt before the first source declaration of the
2159 -- related subprogram's body. If no such declaration exists, Stmt
2160 -- becomes the last declaration.
2162 --------------------------------------------
2163 -- Insert_Before_First_Source_Declaration --
2164 --------------------------------------------
2166 procedure Insert_Before_First_Source_Declaration
(Stmt
: Node_Id
) is
2167 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2171 -- Inspect the declarations of the related subprogram body looking
2172 -- for the first source declaration.
2174 if Present
(Decls
) then
2175 Decl
:= First
(Decls
);
2176 while Present
(Decl
) loop
2177 if Comes_From_Source
(Decl
) then
2178 Insert_Before
(Decl
, Stmt
);
2185 -- If we get there, then the subprogram body lacks any source
2186 -- declarations. The body of _Postconditions now acts as the
2187 -- last declaration.
2189 Append
(Stmt
, Decls
);
2191 -- Ensure that the body has a declaration list
2194 Set_Declarations
(Body_Decl
, New_List
(Stmt
));
2196 end Insert_Before_First_Source_Declaration
;
2200 Loc
: constant Source_Ptr
:= Sloc
(Body_Decl
);
2201 Params
: List_Id
:= No_List
;
2203 Proc_Decl
: Node_Id
;
2204 Proc_Id
: Entity_Id
;
2205 Proc_Spec
: Node_Id
;
2207 -- Start of processing for Build_Postconditions_Procedure
2210 -- Nothing to do if there are no actions to check on exit
2216 Proc_Id
:= Make_Defining_Identifier
(Loc
, Name_uPostconditions
);
2217 Set_Debug_Info_Needed
(Proc_Id
);
2218 Set_Postconditions_Proc
(Subp_Id
, Proc_Id
);
2220 -- Force the front-end inlining of _Postconditions when generating C
2221 -- code, since its body may have references to itypes defined in the
2222 -- enclosing subprogram, which would cause problems for unnesting
2223 -- routines in the absence of inlining.
2225 if Generate_C_Code
then
2226 Set_Has_Pragma_Inline
(Proc_Id
);
2227 Set_Has_Pragma_Inline_Always
(Proc_Id
);
2228 Set_Is_Inlined
(Proc_Id
);
2231 -- The related subprogram is a function: create the specification of
2232 -- parameter _Result.
2234 if Present
(Result
) then
2235 Params
:= New_List
(
2236 Make_Parameter_Specification
(Loc
,
2237 Defining_Identifier
=> Result
,
2239 New_Occurrence_Of
(Etype
(Result
), Loc
)));
2243 Make_Procedure_Specification
(Loc
,
2244 Defining_Unit_Name
=> Proc_Id
,
2245 Parameter_Specifications
=> Params
);
2247 Proc_Decl
:= Make_Subprogram_Declaration
(Loc
, Proc_Spec
);
2249 -- Insert _Postconditions before the first source declaration of the
2250 -- body. This ensures that the body will not cause any premature
2251 -- freezing, as it may mention types:
2253 -- procedure Proc (Obj : Array_Typ) is
2254 -- procedure _postconditions is
2257 -- end _postconditions;
2259 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
2262 -- In the example above, Obj is of type T but the incorrect placement
2263 -- of _Postconditions will cause a crash in gigi due to an out-of-
2264 -- order reference. The body of _Postconditions must be placed after
2265 -- the declaration of Temp to preserve correct visibility.
2267 Insert_Before_First_Source_Declaration
(Proc_Decl
);
2268 Analyze
(Proc_Decl
);
2270 -- Set an explicit End_Label to override the sloc of the implicit
2271 -- RETURN statement, and prevent it from inheriting the sloc of one
2272 -- the postconditions: this would cause confusing debug info to be
2273 -- produced, interfering with coverage-analysis tools.
2276 Make_Subprogram_Body
(Loc
,
2278 Copy_Subprogram_Spec
(Proc_Spec
),
2279 Declarations
=> Empty_List
,
2280 Handled_Statement_Sequence
=>
2281 Make_Handled_Sequence_Of_Statements
(Loc
,
2282 Statements
=> Stmts
,
2283 End_Label
=> Make_Identifier
(Loc
, Chars
(Proc_Id
))));
2285 Insert_After_And_Analyze
(Proc_Decl
, Proc_Bod
);
2286 end Build_Postconditions_Procedure
;
2288 ----------------------------
2289 -- Process_Contract_Cases --
2290 ----------------------------
2292 procedure Process_Contract_Cases
(Stmts
: in out List_Id
) is
2293 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
);
2294 -- Process pragma Contract_Cases for subprogram Subp_Id
2296 --------------------------------
2297 -- Process_Contract_Cases_For --
2298 --------------------------------
2300 procedure Process_Contract_Cases_For
(Subp_Id
: Entity_Id
) is
2301 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2305 if Present
(Items
) then
2306 Prag
:= Contract_Test_Cases
(Items
);
2307 while Present
(Prag
) loop
2308 if Pragma_Name
(Prag
) = Name_Contract_Cases
then
2309 Expand_Pragma_Contract_Cases
2312 Decls
=> Declarations
(Body_Decl
),
2316 Prag
:= Next_Pragma
(Prag
);
2319 end Process_Contract_Cases_For
;
2321 -- Start of processing for Process_Contract_Cases
2324 Process_Contract_Cases_For
(Body_Id
);
2326 if Present
(Spec_Id
) then
2327 Process_Contract_Cases_For
(Spec_Id
);
2329 end Process_Contract_Cases
;
2331 ----------------------------
2332 -- Process_Postconditions --
2333 ----------------------------
2335 procedure Process_Postconditions
(Stmts
: in out List_Id
) is
2336 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
);
2337 -- Collect all [refined] postconditions of a specific kind denoted
2338 -- by Post_Nam that belong to the body, and generate pragma Check
2339 -- equivalents in list Stmts.
2341 procedure Process_Spec_Postconditions
;
2342 -- Collect all [inherited] postconditions of the spec, and generate
2343 -- pragma Check equivalents in list Stmts.
2345 ---------------------------------
2346 -- Process_Body_Postconditions --
2347 ---------------------------------
2349 procedure Process_Body_Postconditions
(Post_Nam
: Name_Id
) is
2350 Items
: constant Node_Id
:= Contract
(Body_Id
);
2351 Unit_Decl
: constant Node_Id
:= Parent
(Body_Decl
);
2356 -- Process the contract
2358 if Present
(Items
) then
2359 Prag
:= Pre_Post_Conditions
(Items
);
2360 while Present
(Prag
) loop
2361 if Pragma_Name
(Prag
) = Post_Nam
then
2363 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2367 Prag
:= Next_Pragma
(Prag
);
2371 -- The subprogram body being processed is actually the proper body
2372 -- of a stub with a corresponding spec. The subprogram stub may
2373 -- carry a postcondition pragma, in which case it must be taken
2374 -- into account. The pragma appears after the stub.
2376 if Present
(Spec_Id
) and then Nkind
(Unit_Decl
) = N_Subunit
then
2377 Decl
:= Next
(Corresponding_Stub
(Unit_Decl
));
2378 while Present
(Decl
) loop
2380 -- Note that non-matching pragmas are skipped
2382 if Nkind
(Decl
) = N_Pragma
then
2383 if Pragma_Name
(Decl
) = Post_Nam
then
2385 (Item
=> Build_Pragma_Check_Equivalent
(Decl
),
2389 -- Skip internally generated code
2391 elsif not Comes_From_Source
(Decl
) then
2394 -- Postcondition pragmas are usually grouped together. There
2395 -- is no need to inspect the whole declarative list.
2404 end Process_Body_Postconditions
;
2406 ---------------------------------
2407 -- Process_Spec_Postconditions --
2408 ---------------------------------
2410 procedure Process_Spec_Postconditions
is
2411 Subps
: constant Subprogram_List
:=
2412 Inherited_Subprograms
(Spec_Id
);
2415 Subp_Id
: Entity_Id
;
2418 -- Process the contract
2420 Items
:= Contract
(Spec_Id
);
2422 if Present
(Items
) then
2423 Prag
:= Pre_Post_Conditions
(Items
);
2424 while Present
(Prag
) loop
2425 if Pragma_Name
(Prag
) = Name_Postcondition
then
2427 (Item
=> Build_Pragma_Check_Equivalent
(Prag
),
2431 Prag
:= Next_Pragma
(Prag
);
2435 -- Process the contracts of all inherited subprograms, looking for
2436 -- class-wide postconditions.
2438 for Index
in Subps
'Range loop
2439 Subp_Id
:= Subps
(Index
);
2440 Items
:= Contract
(Subp_Id
);
2442 if Present
(Items
) then
2443 Prag
:= Pre_Post_Conditions
(Items
);
2444 while Present
(Prag
) loop
2445 if Pragma_Name
(Prag
) = Name_Postcondition
2446 and then Class_Present
(Prag
)
2450 Build_Pragma_Check_Equivalent
2453 Inher_Id
=> Subp_Id
),
2457 Prag
:= Next_Pragma
(Prag
);
2461 end Process_Spec_Postconditions
;
2463 -- Start of processing for Process_Postconditions
2466 -- The processing of postconditions is done in reverse order (body
2467 -- first) to ensure the following arrangement:
2469 -- <refined postconditions from body>
2470 -- <postconditions from body>
2471 -- <postconditions from spec>
2472 -- <inherited postconditions>
2474 Process_Body_Postconditions
(Name_Refined_Post
);
2475 Process_Body_Postconditions
(Name_Postcondition
);
2477 if Present
(Spec_Id
) then
2478 Process_Spec_Postconditions
;
2480 end Process_Postconditions
;
2482 ---------------------------
2483 -- Process_Preconditions --
2484 ---------------------------
2486 procedure Process_Preconditions
is
2487 Class_Pre
: Node_Id
:= Empty
;
2488 -- The sole [inherited] class-wide precondition pragma that applies
2489 -- to the subprogram.
2491 Insert_Node
: Node_Id
:= Empty
;
2492 -- The insertion node after which all pragma Check equivalents are
2495 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean;
2496 -- Determine whether arbitrary declaration Decl denotes a renaming of
2497 -- a discriminant or protection field _object.
2499 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
);
2500 -- Merge two class-wide preconditions by "or else"-ing them. The
2501 -- changes are accumulated in parameter Into. Update the error
2504 procedure Prepend_To_Decls
(Item
: Node_Id
);
2505 -- Prepend a single item to the declarations of the subprogram body
2507 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
);
2508 -- Save a class-wide precondition into Class_Pre, or prepend a normal
2509 -- precondition to the declarations of the body and analyze it.
2511 procedure Process_Inherited_Preconditions
;
2512 -- Collect all inherited class-wide preconditions and merge them into
2513 -- one big precondition to be evaluated as pragma Check.
2515 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
);
2516 -- Collect all preconditions of subprogram Subp_Id and prepend their
2517 -- pragma Check equivalents to the declarations of the body.
2519 --------------------------
2520 -- Is_Prologue_Renaming --
2521 --------------------------
2523 function Is_Prologue_Renaming
(Decl
: Node_Id
) return Boolean is
2530 if Nkind
(Decl
) = N_Object_Renaming_Declaration
then
2531 Obj
:= Defining_Entity
(Decl
);
2534 if Nkind
(Nam
) = N_Selected_Component
then
2535 Pref
:= Prefix
(Nam
);
2536 Sel
:= Selector_Name
(Nam
);
2538 -- A discriminant renaming appears as
2539 -- Discr : constant ... := Prefix.Discr;
2541 if Ekind
(Obj
) = E_Constant
2542 and then Is_Entity_Name
(Sel
)
2543 and then Present
(Entity
(Sel
))
2544 and then Ekind
(Entity
(Sel
)) = E_Discriminant
2548 -- A protection field renaming appears as
2549 -- Prot : ... := _object._object;
2551 -- A renamed private component is just a component of
2552 -- _object, with an arbitrary name.
2554 elsif Ekind
(Obj
) = E_Variable
2555 and then Nkind
(Pref
) = N_Identifier
2556 and then Chars
(Pref
) = Name_uObject
2557 and then Nkind
(Sel
) = N_Identifier
2565 end Is_Prologue_Renaming
;
2567 -------------------------
2568 -- Merge_Preconditions --
2569 -------------------------
2571 procedure Merge_Preconditions
(From
: Node_Id
; Into
: Node_Id
) is
2572 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
;
2573 -- Return the boolean expression argument of a precondition while
2574 -- updating its parentheses count for the subsequent merge.
2576 function Message_Arg
(Prag
: Node_Id
) return Node_Id
;
2577 -- Return the message argument of a precondition
2579 --------------------
2580 -- Expression_Arg --
2581 --------------------
2583 function Expression_Arg
(Prag
: Node_Id
) return Node_Id
is
2584 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2585 Arg
: constant Node_Id
:= Get_Pragma_Arg
(Next
(First
(Args
)));
2588 if Paren_Count
(Arg
) = 0 then
2589 Set_Paren_Count
(Arg
, 1);
2599 function Message_Arg
(Prag
: Node_Id
) return Node_Id
is
2600 Args
: constant List_Id
:= Pragma_Argument_Associations
(Prag
);
2602 return Get_Pragma_Arg
(Last
(Args
));
2607 From_Expr
: constant Node_Id
:= Expression_Arg
(From
);
2608 From_Msg
: constant Node_Id
:= Message_Arg
(From
);
2609 Into_Expr
: constant Node_Id
:= Expression_Arg
(Into
);
2610 Into_Msg
: constant Node_Id
:= Message_Arg
(Into
);
2611 Loc
: constant Source_Ptr
:= Sloc
(Into
);
2613 -- Start of processing for Merge_Preconditions
2616 -- Merge the two preconditions by "or else"-ing them
2620 Right_Opnd
=> Relocate_Node
(Into_Expr
),
2621 Left_Opnd
=> From_Expr
));
2623 -- Merge the two error messages to produce a single message of the
2626 -- failed precondition from ...
2627 -- also failed inherited precondition from ...
2629 if not Exception_Locations_Suppressed
then
2630 Start_String
(Strval
(Into_Msg
));
2631 Store_String_Char
(ASCII
.LF
);
2632 Store_String_Chars
(" also ");
2633 Store_String_Chars
(Strval
(From_Msg
));
2635 Set_Strval
(Into_Msg
, End_String
);
2637 end Merge_Preconditions
;
2639 ----------------------
2640 -- Prepend_To_Decls --
2641 ----------------------
2643 procedure Prepend_To_Decls
(Item
: Node_Id
) is
2644 Decls
: List_Id
:= Declarations
(Body_Decl
);
2647 -- Ensure that the body has a declarative list
2651 Set_Declarations
(Body_Decl
, Decls
);
2654 Prepend_To
(Decls
, Item
);
2655 end Prepend_To_Decls
;
2657 ------------------------------
2658 -- Prepend_To_Decls_Or_Save --
2659 ------------------------------
2661 procedure Prepend_To_Decls_Or_Save
(Prag
: Node_Id
) is
2662 Check_Prag
: Node_Id
;
2665 Check_Prag
:= Build_Pragma_Check_Equivalent
(Prag
);
2667 -- Save the sole class-wide precondition (if any) for the next
2668 -- step, where it will be merged with inherited preconditions.
2670 if Class_Present
(Prag
) then
2671 pragma Assert
(No
(Class_Pre
));
2672 Class_Pre
:= Check_Prag
;
2674 -- Accumulate the corresponding Check pragmas at the top of the
2675 -- declarations. Prepending the items ensures that they will be
2676 -- evaluated in their original order.
2679 if Present
(Insert_Node
) then
2680 Insert_After
(Insert_Node
, Check_Prag
);
2682 Prepend_To_Decls
(Check_Prag
);
2685 Analyze
(Check_Prag
);
2687 end Prepend_To_Decls_Or_Save
;
2689 -------------------------------------
2690 -- Process_Inherited_Preconditions --
2691 -------------------------------------
2693 procedure Process_Inherited_Preconditions
is
2694 Subps
: constant Subprogram_List
:=
2695 Inherited_Subprograms
(Spec_Id
);
2696 Check_Prag
: Node_Id
;
2699 Subp_Id
: Entity_Id
;
2702 -- Process the contracts of all inherited subprograms, looking for
2703 -- class-wide preconditions.
2705 for Index
in Subps
'Range loop
2706 Subp_Id
:= Subps
(Index
);
2707 Items
:= Contract
(Subp_Id
);
2709 if Present
(Items
) then
2710 Prag
:= Pre_Post_Conditions
(Items
);
2711 while Present
(Prag
) loop
2712 if Pragma_Name
(Prag
) = Name_Precondition
2713 and then Class_Present
(Prag
)
2716 Build_Pragma_Check_Equivalent
2719 Inher_Id
=> Subp_Id
);
2721 -- The spec of an inherited subprogram already yielded
2722 -- a class-wide precondition. Merge the existing
2723 -- precondition with the current one using "or else".
2725 if Present
(Class_Pre
) then
2726 Merge_Preconditions
(Check_Prag
, Class_Pre
);
2728 Class_Pre
:= Check_Prag
;
2732 Prag
:= Next_Pragma
(Prag
);
2737 -- Add the merged class-wide preconditions
2739 if Present
(Class_Pre
) then
2740 Prepend_To_Decls
(Class_Pre
);
2741 Analyze
(Class_Pre
);
2743 end Process_Inherited_Preconditions
;
2745 -------------------------------
2746 -- Process_Preconditions_For --
2747 -------------------------------
2749 procedure Process_Preconditions_For
(Subp_Id
: Entity_Id
) is
2750 Items
: constant Node_Id
:= Contract
(Subp_Id
);
2753 Subp_Decl
: Node_Id
;
2756 -- Process the contract
2758 if Present
(Items
) then
2759 Prag
:= Pre_Post_Conditions
(Items
);
2760 while Present
(Prag
) loop
2761 if Pragma_Name
(Prag
) = Name_Precondition
then
2762 Prepend_To_Decls_Or_Save
(Prag
);
2765 Prag
:= Next_Pragma
(Prag
);
2769 -- The subprogram declaration being processed is actually a body
2770 -- stub. The stub may carry a precondition pragma, in which case
2771 -- it must be taken into account. The pragma appears after the
2774 Subp_Decl
:= Unit_Declaration_Node
(Subp_Id
);
2776 if Nkind
(Subp_Decl
) = N_Subprogram_Body_Stub
then
2778 -- Inspect the declarations following the body stub
2780 Decl
:= Next
(Subp_Decl
);
2781 while Present
(Decl
) loop
2783 -- Note that non-matching pragmas are skipped
2785 if Nkind
(Decl
) = N_Pragma
then
2786 if Pragma_Name
(Decl
) = Name_Precondition
then
2787 Prepend_To_Decls_Or_Save
(Decl
);
2790 -- Skip internally generated code
2792 elsif not Comes_From_Source
(Decl
) then
2795 -- Preconditions are usually grouped together. There is no
2796 -- need to inspect the whole declarative list.
2805 end Process_Preconditions_For
;
2809 Decls
: constant List_Id
:= Declarations
(Body_Decl
);
2812 -- Start of processing for Process_Preconditions
2815 -- Find the proper insertion point for all pragma Check equivalents
2817 if Present
(Decls
) then
2818 Decl
:= First
(Decls
);
2819 while Present
(Decl
) loop
2821 -- First source declaration terminates the search, because all
2822 -- preconditions must be evaluated prior to it, by definition.
2824 if Comes_From_Source
(Decl
) then
2827 -- Certain internally generated object renamings such as those
2828 -- for discriminants and protection fields must be elaborated
2829 -- before the preconditions are evaluated, as their expressions
2830 -- may mention the discriminants. The renamings include those
2831 -- for private components so we need to find the last such.
2833 elsif Is_Prologue_Renaming
(Decl
) then
2834 while Present
(Next
(Decl
))
2835 and then Is_Prologue_Renaming
(Next
(Decl
))
2840 Insert_Node
:= Decl
;
2842 -- Otherwise the declaration does not come from source. This
2843 -- also terminates the search, because internal code may raise
2844 -- exceptions which should not preempt the preconditions.
2854 -- The processing of preconditions is done in reverse order (body
2855 -- first), because each pragma Check equivalent is inserted at the
2856 -- top of the declarations. This ensures that the final order is
2857 -- consistent with following diagram:
2859 -- <inherited preconditions>
2860 -- <preconditions from spec>
2861 -- <preconditions from body>
2863 Process_Preconditions_For
(Body_Id
);
2865 if Present
(Spec_Id
) then
2866 Process_Preconditions_For
(Spec_Id
);
2867 Process_Inherited_Preconditions
;
2869 end Process_Preconditions
;
2873 Restore_Scope
: Boolean := False;
2875 Stmts
: List_Id
:= No_List
;
2876 Subp_Id
: Entity_Id
;
2878 -- Start of processing for Expand_Subprogram_Contract
2881 -- Obtain the entity of the initial declaration
2883 if Present
(Spec_Id
) then
2889 -- Do not perform expansion activity when it is not needed
2891 if not Expander_Active
then
2894 -- ASIS requires an unaltered tree
2896 elsif ASIS_Mode
then
2899 -- GNATprove does not need the executable semantics of a contract
2901 elsif GNATprove_Mode
then
2904 -- The contract of a generic subprogram or one declared in a generic
2905 -- context is not expanded, as the corresponding instance will provide
2906 -- the executable semantics of the contract.
2908 elsif Is_Generic_Subprogram
(Subp_Id
) or else Inside_A_Generic
then
2911 -- All subprograms carry a contract, but for some it is not significant
2912 -- and should not be processed. This is a small optimization.
2914 elsif not Has_Significant_Contract
(Subp_Id
) then
2917 -- The contract of an ignored Ghost subprogram does not need expansion,
2918 -- because the subprogram and all calls to it will be removed.
2920 elsif Is_Ignored_Ghost_Entity
(Subp_Id
) then
2924 -- Do not re-expand the same contract. This scenario occurs when a
2925 -- construct is rewritten into something else during its analysis
2926 -- (expression functions for instance).
2928 if Has_Expanded_Contract
(Subp_Id
) then
2931 -- Otherwise mark the subprogram
2934 Set_Has_Expanded_Contract
(Subp_Id
);
2937 -- Ensure that the formal parameters are visible when expanding all
2940 if not In_Open_Scopes
(Subp_Id
) then
2941 Restore_Scope
:= True;
2942 Push_Scope
(Subp_Id
);
2944 if Is_Generic_Subprogram
(Subp_Id
) then
2945 Install_Generic_Formals
(Subp_Id
);
2947 Install_Formals
(Subp_Id
);
2951 -- The expansion of a subprogram contract involves the creation of Check
2952 -- pragmas to verify the contract assertions of the spec and body in a
2953 -- particular order. The order is as follows:
2955 -- function Example (...) return ... is
2956 -- procedure _Postconditions (...) is
2958 -- <refined postconditions from body>
2959 -- <postconditions from body>
2960 -- <postconditions from spec>
2961 -- <inherited postconditions>
2962 -- <contract case consequences>
2963 -- <invariant check of function result>
2964 -- <invariant and predicate checks of parameters>
2965 -- end _Postconditions;
2967 -- <inherited preconditions>
2968 -- <preconditions from spec>
2969 -- <preconditions from body>
2970 -- <contract case conditions>
2972 -- <source declarations>
2974 -- <source statements>
2976 -- _Preconditions (Result);
2980 -- Routine _Postconditions holds all contract assertions that must be
2981 -- verified on exit from the related subprogram.
2983 -- Step 1: Handle all preconditions. This action must come before the
2984 -- processing of pragma Contract_Cases because the pragma prepends items
2985 -- to the body declarations.
2987 Process_Preconditions
;
2989 -- Step 2: Handle all postconditions. This action must come before the
2990 -- processing of pragma Contract_Cases because the pragma appends items
2993 Process_Postconditions
(Stmts
);
2995 -- Step 3: Handle pragma Contract_Cases. This action must come before
2996 -- the processing of invariants and predicates because those append
2997 -- items to list Stmts.
2999 Process_Contract_Cases
(Stmts
);
3001 -- Step 4: Apply invariant and predicate checks on a function result and
3002 -- all formals. The resulting checks are accumulated in list Stmts.
3004 Add_Invariant_And_Predicate_Checks
(Subp_Id
, Stmts
, Result
);
3006 -- Step 5: Construct procedure _Postconditions
3008 Build_Postconditions_Procedure
(Subp_Id
, Stmts
, Result
);
3010 if Restore_Scope
then
3013 end Expand_Subprogram_Contract
;
3015 ---------------------------------
3016 -- Inherit_Subprogram_Contract --
3017 ---------------------------------
3019 procedure Inherit_Subprogram_Contract
3021 From_Subp
: Entity_Id
)
3023 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
);
3024 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3027 --------------------
3028 -- Inherit_Pragma --
3029 --------------------
3031 procedure Inherit_Pragma
(Prag_Id
: Pragma_Id
) is
3032 Prag
: constant Node_Id
:= Get_Pragma
(From_Subp
, Prag_Id
);
3036 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3037 -- chains, therefore the node must be replicated. The new pragma is
3038 -- flagged as inherited for distinction purposes.
3040 if Present
(Prag
) then
3041 New_Prag
:= New_Copy_Tree
(Prag
);
3042 Set_Is_Inherited_Pragma
(New_Prag
);
3044 Add_Contract_Item
(New_Prag
, Subp
);
3048 -- Start of processing for Inherit_Subprogram_Contract
3051 -- Inheritance is carried out only when both entities are subprograms
3054 if Is_Subprogram_Or_Generic_Subprogram
(Subp
)
3055 and then Is_Subprogram_Or_Generic_Subprogram
(From_Subp
)
3056 and then Present
(Contract
(From_Subp
))
3058 Inherit_Pragma
(Pragma_Extensions_Visible
);
3060 end Inherit_Subprogram_Contract
;
3062 -------------------------------------
3063 -- Instantiate_Subprogram_Contract --
3064 -------------------------------------
3066 procedure Instantiate_Subprogram_Contract
(Templ
: Node_Id
; L
: List_Id
) is
3067 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
);
3068 -- Instantiate all contract-related source pragmas found in the list,
3069 -- starting with pragma First_Prag. Each instantiated pragma is added
3072 -------------------------
3073 -- Instantiate_Pragmas --
3074 -------------------------
3076 procedure Instantiate_Pragmas
(First_Prag
: Node_Id
) is
3077 Inst_Prag
: Node_Id
;
3082 while Present
(Prag
) loop
3083 if Is_Generic_Contract_Pragma
(Prag
) then
3085 Copy_Generic_Node
(Prag
, Empty
, Instantiating
=> True);
3087 Set_Analyzed
(Inst_Prag
, False);
3088 Append_To
(L
, Inst_Prag
);
3091 Prag
:= Next_Pragma
(Prag
);
3093 end Instantiate_Pragmas
;
3097 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3099 -- Start of processing for Instantiate_Subprogram_Contract
3102 if Present
(Items
) then
3103 Instantiate_Pragmas
(Pre_Post_Conditions
(Items
));
3104 Instantiate_Pragmas
(Contract_Test_Cases
(Items
));
3105 Instantiate_Pragmas
(Classifications
(Items
));
3107 end Instantiate_Subprogram_Contract
;
3109 ----------------------------------------
3110 -- Save_Global_References_In_Contract --
3111 ----------------------------------------
3113 procedure Save_Global_References_In_Contract
3117 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
);
3118 -- Save all global references in contract-related source pragmas found
3119 -- in the list, starting with pragma First_Prag.
3121 ------------------------------------
3122 -- Save_Global_References_In_List --
3123 ------------------------------------
3125 procedure Save_Global_References_In_List
(First_Prag
: Node_Id
) is
3130 while Present
(Prag
) loop
3131 if Is_Generic_Contract_Pragma
(Prag
) then
3132 Save_Global_References
(Prag
);
3135 Prag
:= Next_Pragma
(Prag
);
3137 end Save_Global_References_In_List
;
3141 Items
: constant Node_Id
:= Contract
(Defining_Entity
(Templ
));
3143 -- Start of processing for Save_Global_References_In_Contract
3146 -- The entity of the analyzed generic copy must be on the scope stack
3147 -- to ensure proper detection of global references.
3149 Push_Scope
(Gen_Id
);
3151 if Permits_Aspect_Specifications
(Templ
)
3152 and then Has_Aspects
(Templ
)
3154 Save_Global_References_In_Aspects
(Templ
);
3157 if Present
(Items
) then
3158 Save_Global_References_In_List
(Pre_Post_Conditions
(Items
));
3159 Save_Global_References_In_List
(Contract_Test_Cases
(Items
));
3160 Save_Global_References_In_List
(Classifications
(Items
));
3164 end Save_Global_References_In_Contract
;