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. The
488 -- check only applies to source subprograms and not to generated TSS
492 and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
493 and then Comes_From_Source (Spec_Id)
494 and then not Is_Volatile_Function (Body_Id)
496 Check_Nonvolatile_Function_Profile (Body_Id);
499 -- Restore the SPARK_Mode of the enclosing context after all delayed
500 -- pragmas have been analyzed.
502 Restore_SPARK_Mode (Mode);
504 -- Capture all global references in a generic subprogram body now that
505 -- the contract has been analyzed.
507 if Is_Generic_Declaration_Or_Body (Body_Decl) then
508 Save_Global_References_In_Contract
509 (Templ => Original_Node (Body_Decl),
513 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
514 -- invariants and predicates associated with body and its spec. Do not
515 -- expand the contract of subprogram body stubs.
517 if Nkind (Body_Decl) = N_Subprogram_Body then
518 Expand_Subprogram_Contract (Body_Id);
520 end Analyze_Entry_Or_Subprogram_Body_Contract;
522 ------------------------------------------
523 -- Analyze_Entry_Or_Subprogram_Contract --
524 ------------------------------------------
526 procedure Analyze_Entry_Or_Subprogram_Contract
527 (Subp_Id : Entity_Id;
528 Freeze_Id : Entity_Id := Empty)
530 Items : constant Node_Id := Contract (Subp_Id);
531 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
533 Skip_Assert_Exprs : constant Boolean :=
534 Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
535 and then not ASIS_Mode
536 and then not GNATprove_Mode;
538 Depends : Node_Id := Empty;
539 Global : Node_Id := Empty;
540 Mode : SPARK_Mode_Type;
545 -- Do not analyze a contract multiple times
547 if Present (Items) then
548 if Analyzed (Items) then
551 Set_Analyzed (Items);
555 -- Due to the timing of contract analysis, delayed pragmas may be
556 -- subject to the wrong SPARK_Mode, usually that of the enclosing
557 -- context. To remedy this, restore the original SPARK_Mode of the
558 -- related subprogram body.
560 Save_SPARK_Mode_And_Set (Subp_Id, Mode);
562 -- All subprograms carry a contract, but for some it is not significant
563 -- and should not be processed.
565 if not Has_Significant_Contract (Subp_Id) then
568 elsif Present (Items) then
570 -- Do not analyze the pre/postconditions of an entry declaration
571 -- unless annotating the original tree for ASIS or GNATprove. The
572 -- real analysis occurs when the pre/postconditons are relocated to
573 -- the contract wrapper procedure (see Build_Contract_Wrapper).
575 if Skip_Assert_Exprs then
578 -- Otherwise analyze the pre/postconditions
581 Prag := Pre_Post_Conditions (Items);
582 while Present (Prag) loop
583 Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
584 Prag := Next_Pragma (Prag);
588 -- Analyze contract-cases and test-cases
590 Prag := Contract_Test_Cases (Items);
591 while Present (Prag) loop
592 Prag_Nam := Pragma_Name (Prag);
594 if Prag_Nam = Name_Contract_Cases then
596 -- Do not analyze the contract cases of an entry declaration
597 -- unless annotating the original tree for ASIS or GNATprove.
598 -- The real analysis occurs when the contract cases are moved
599 -- to the contract wrapper procedure (Build_Contract_Wrapper).
601 if Skip_Assert_Exprs then
604 -- Otherwise analyze the contract cases
607 Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
610 pragma Assert (Prag_Nam = Name_Test_Case);
611 Analyze_Test_Case_In_Decl_Part (Prag);
614 Prag := Next_Pragma (Prag);
617 -- Analyze classification pragmas
619 Prag := Classifications (Items);
620 while Present (Prag) loop
621 Prag_Nam := Pragma_Name (Prag);
623 if Prag_Nam = Name_Depends then
626 elsif Prag_Nam = Name_Global then
630 Prag := Next_Pragma (Prag);
633 -- Analyze Global first, as Depends may mention items classified in
634 -- the global categorization.
636 if Present (Global) then
637 Analyze_Global_In_Decl_Part (Global);
640 -- Depends must be analyzed after Global in order to see the modes of
643 if Present (Depends) then
644 Analyze_Depends_In_Decl_Part (Depends);
647 -- Ensure that the contract cases or postconditions mention 'Result
648 -- or define a post-state.
650 Check_Result_And_Post_State (Subp_Id);
653 -- A nonvolatile function cannot have an effectively volatile formal
654 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
655 -- only when SPARK_Mode is on, as it is not a standard legality rule.
656 -- The check is performed here because pragma Volatile_Function is
657 -- processed after the analysis of the related subprogram declaration.
660 and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
661 and then not Is_Volatile_Function (Subp_Id)
663 Check_Nonvolatile_Function_Profile (Subp_Id);
666 -- Restore the SPARK_Mode of the enclosing context after all delayed
667 -- pragmas have been analyzed.
669 Restore_SPARK_Mode (Mode);
671 -- Capture all global references in a generic subprogram now that the
672 -- contract has been analyzed.
674 if Is_Generic_Declaration_Or_Body (Subp_Decl) then
675 Save_Global_References_In_Contract
676 (Templ => Original_Node (Subp_Decl),
679 end Analyze_Entry_Or_Subprogram_Contract;
681 -----------------------------
682 -- Analyze_Object_Contract --
683 -----------------------------
685 procedure Analyze_Object_Contract
687 Freeze_Id : Entity_Id := Empty)
689 Obj_Typ : constant Entity_Id := Etype (Obj_Id);
690 AR_Val : Boolean := False;
691 AW_Val : Boolean := False;
692 ER_Val : Boolean := False;
693 EW_Val : Boolean := False;
695 Mode : SPARK_Mode_Type;
698 Restore_Mode : Boolean := False;
699 Seen : Boolean := False;
702 -- The loop parameter in an element iterator over a formal container
703 -- is declared with an object declaration, but no contracts apply.
705 if Ekind (Obj_Id) = E_Loop_Parameter then
709 -- Do not analyze a contract multiple times
711 Items := Contract (Obj_Id);
713 if Present (Items) then
714 if Analyzed (Items) then
717 Set_Analyzed (Items);
721 -- The anonymous object created for a single concurrent type inherits
722 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
723 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
724 -- of the enclosing context. To remedy this, restore the original mode
725 -- of the related anonymous object.
727 if Is_Single_Concurrent_Object (Obj_Id)
728 and then Present (SPARK_Pragma (Obj_Id))
730 Restore_Mode := True;
731 Save_SPARK_Mode_And_Set (Obj_Id, Mode);
734 -- Constant-related checks
736 if Ekind (Obj_Id) = E_Constant then
738 -- Analyze indicator Part_Of
740 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
742 -- Check whether the lack of indicator Part_Of agrees with the
743 -- placement of the constant with respect to the state space.
746 Check_Missing_Part_Of (Obj_Id);
749 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
750 -- This check is relevant only when SPARK_Mode is on, as it is not
751 -- a standard Ada legality rule. Internally-generated constants that
752 -- map generic formals to actuals in instantiations are allowed to
756 and then Comes_From_Source (Obj_Id)
757 and then Is_Effectively_Volatile (Obj_Id)
758 and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
760 Error_Msg_N ("constant cannot be volatile", Obj_Id);
763 -- Variable-related checks
765 else pragma Assert (Ekind (Obj_Id) = E_Variable);
767 -- Analyze all external properties
769 Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
771 if Present (Prag) then
772 Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
776 Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
778 if Present (Prag) then
779 Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
783 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
785 if Present (Prag) then
786 Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
790 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
792 if Present (Prag) then
793 Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
797 -- Verify the mutual interaction of the various external properties
800 Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
803 -- The anonymous object created for a single concurrent type carries
804 -- pragmas Depends and Globat of the type.
806 if Is_Single_Concurrent_Object (Obj_Id) then
808 -- Analyze Global first, as Depends may mention items classified
809 -- in the global categorization.
811 Prag := Get_Pragma (Obj_Id, Pragma_Global);
813 if Present (Prag) then
814 Analyze_Global_In_Decl_Part (Prag);
817 -- Depends must be analyzed after Global in order to see the modes
818 -- of all global items.
820 Prag := Get_Pragma (Obj_Id, Pragma_Depends);
822 if Present (Prag) then
823 Analyze_Depends_In_Decl_Part (Prag);
827 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
829 -- Analyze indicator Part_Of
831 if Present (Prag) then
832 Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id);
834 -- The variable is a constituent of a single protected/task type
835 -- and behaves as a component of the type. Verify that references
836 -- to the variable occur within the definition or body of the type
839 if Present (Encapsulating_State (Obj_Id))
840 and then Is_Single_Concurrent_Object
841 (Encapsulating_State (Obj_Id))
842 and then Present (Part_Of_References (Obj_Id))
844 Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id));
845 while Present (Ref_Elmt) loop
846 Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt));
847 Next_Elmt (Ref_Elmt);
851 -- Otherwise check whether the lack of indicator Part_Of agrees with
852 -- the placement of the variable with respect to the state space.
855 Check_Missing_Part_Of (Obj_Id);
858 -- The following checks are relevant only when SPARK_Mode is on, as
859 -- they are not standard Ada legality rules. Internally generated
860 -- temporaries are ignored.
862 if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
863 if Is_Effectively_Volatile (Obj_Id) then
865 -- The declaration of an effectively volatile object must
866 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
868 if not Is_Library_Level_Entity (Obj_Id) then
870 ("volatile variable & must be declared at library level",
873 -- An object of a discriminated type cannot be effectively
874 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
876 elsif Has_Discriminants (Obj_Typ)
877 and then not Is_Protected_Type (Obj_Typ)
880 ("discriminated object & cannot be volatile", Obj_Id);
883 -- The object is not effectively volatile
886 -- A non-effectively volatile object cannot have effectively
887 -- volatile components (SPARK RM 7.1.3(6)).
889 if not Is_Effectively_Volatile (Obj_Id)
890 and then Has_Volatile_Component (Obj_Typ)
893 ("non-volatile object & cannot have volatile components",
902 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
904 -- A Ghost object cannot be of a type that yields a synchronized
905 -- object (SPARK RM 6.9(19)).
907 if Yields_Synchronized_Object (Obj_Typ) then
908 Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
910 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
911 -- SPARK RM 6.9(19)).
913 elsif Is_Effectively_Volatile (Obj_Id) then
914 Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
916 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
917 -- One exception to this is the object that represents the dispatch
918 -- table of a Ghost tagged type, as the symbol needs to be exported.
920 elsif Is_Exported (Obj_Id) then
921 Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
923 elsif Is_Imported (Obj_Id) then
924 Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
928 -- Restore the SPARK_Mode of the enclosing context after all delayed
929 -- pragmas have been analyzed.
932 Restore_SPARK_Mode (Mode);
934 end Analyze_Object_Contract;
936 -----------------------------------
937 -- Analyze_Package_Body_Contract --
938 -----------------------------------
940 procedure Analyze_Package_Body_Contract
941 (Body_Id : Entity_Id;
942 Freeze_Id : Entity_Id := Empty)
944 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
945 Items : constant Node_Id := Contract (Body_Id);
946 Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
947 Mode : SPARK_Mode_Type;
951 -- Do not analyze a contract multiple times
953 if Present (Items) then
954 if Analyzed (Items) then
957 Set_Analyzed (Items);
961 -- Due to the timing of contract analysis, delayed pragmas may be
962 -- subject to the wrong SPARK_Mode, usually that of the enclosing
963 -- context. To remedy this, restore the original SPARK_Mode of the
964 -- related package body.
966 Save_SPARK_Mode_And_Set (Body_Id, Mode);
968 Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
970 -- The analysis of pragma Refined_State detects whether the spec has
971 -- abstract states available for refinement.
973 if Present (Ref_State) then
974 Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id);
977 -- Restore the SPARK_Mode of the enclosing context after all delayed
978 -- pragmas have been analyzed.
980 Restore_SPARK_Mode (Mode);
982 -- Capture all global references in a generic package body now that the
983 -- contract has been analyzed.
985 if Is_Generic_Declaration_Or_Body (Body_Decl) then
986 Save_Global_References_In_Contract
987 (Templ => Original_Node (Body_Decl),
990 end Analyze_Package_Body_Contract;
992 ------------------------------
993 -- Analyze_Package_Contract --
994 ------------------------------
996 procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
997 Items : constant Node_Id := Contract (Pack_Id);
998 Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
999 Init : Node_Id := Empty;
1000 Init_Cond : Node_Id := Empty;
1001 Mode : SPARK_Mode_Type;
1006 -- Do not analyze a contract multiple times
1008 if Present (Items) then
1009 if Analyzed (Items) then
1012 Set_Analyzed (Items);
1016 -- Due to the timing of contract analysis, delayed pragmas may be
1017 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1018 -- context. To remedy this, restore the original SPARK_Mode of the
1021 Save_SPARK_Mode_And_Set (Pack_Id, Mode);
1023 if Present (Items) then
1025 -- Locate and store pragmas Initial_Condition and Initializes, since
1026 -- their order of analysis matters.
1028 Prag := Classifications (Items);
1029 while Present (Prag) loop
1030 Prag_Nam := Pragma_Name (Prag);
1032 if Prag_Nam = Name_Initial_Condition then
1035 elsif Prag_Nam = Name_Initializes then
1039 Prag := Next_Pragma (Prag);
1042 -- Analyze the initialization-related pragmas. Initializes must come
1043 -- before Initial_Condition due to item dependencies.
1045 if Present (Init) then
1046 Analyze_Initializes_In_Decl_Part (Init);
1049 if Present (Init_Cond) then
1050 Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
1054 -- Check whether the lack of indicator Part_Of agrees with the placement
1055 -- of the package instantiation with respect to the state space.
1057 if Is_Generic_Instance (Pack_Id) then
1058 Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
1061 Check_Missing_Part_Of (Pack_Id);
1065 -- Restore the SPARK_Mode of the enclosing context after all delayed
1066 -- pragmas have been analyzed.
1068 Restore_SPARK_Mode (Mode);
1070 -- Capture all global references in a generic package now that the
1071 -- contract has been analyzed.
1073 if Is_Generic_Declaration_Or_Body (Pack_Decl) then
1074 Save_Global_References_In_Contract
1075 (Templ => Original_Node (Pack_Decl),
1078 end Analyze_Package_Contract;
1080 --------------------------------
1081 -- Analyze_Previous_Contracts --
1082 --------------------------------
1084 procedure Analyze_Previous_Contracts (Body_Decl : Node_Id) is
1085 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
1086 Orig_Decl : constant Node_Id := Original_Node (Body_Decl);
1091 -- A body that is in the process of being inlined appears from source,
1092 -- but carries name _parent. Such a body does not cause "freezing" of
1095 if Chars (Body_Id) = Name_uParent then
1099 -- Climb the parent chain looking for an enclosing package body. Do not
1100 -- use the scope stack, as a body uses the entity of its corresponding
1103 Par := Parent (Body_Decl);
1104 while Present (Par) loop
1105 if Nkind (Par) = N_Package_Body then
1106 Analyze_Package_Body_Contract
1107 (Body_Id => Defining_Entity (Par),
1108 Freeze_Id => Defining_Entity (Body_Decl));
1112 -- Do not look for an enclosing package body when the construct which
1113 -- causes freezing is a body generated for an expression function and
1114 -- it appears within a package spec. This ensures that the traversal
1115 -- will not reach too far up the parent chain and attempt to freeze a
1116 -- package body which should not be frozen.
1118 -- package body Enclosing_Body
1119 -- with Refined_State => (State => Var)
1121 -- package Nested is
1122 -- type Some_Type is ...;
1123 -- function Cause_Freezing return ...;
1125 -- function Cause_Freezing is (...);
1128 -- Var : Nested.Some_Type;
1130 elsif Nkind (Par) = N_Package_Declaration
1131 and then Nkind (Orig_Decl) = N_Expression_Function
1136 Par := Parent (Par);
1139 -- Analyze the contracts of all eligible construct up to the body which
1140 -- caused the "freezing".
1142 if Is_List_Member (Body_Decl) then
1144 (L => List_Containing (Body_Decl),
1145 Freeze_Nod => Body_Decl,
1146 Freeze_Id => Body_Id);
1148 end Analyze_Previous_Contracts;
1150 --------------------------------
1151 -- Analyze_Protected_Contract --
1152 --------------------------------
1154 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
1155 Items : constant Node_Id := Contract (Prot_Id);
1158 -- Do not analyze a contract multiple times
1160 if Present (Items) then
1161 if Analyzed (Items) then
1164 Set_Analyzed (Items);
1167 end Analyze_Protected_Contract;
1169 -------------------------------------------
1170 -- Analyze_Subprogram_Body_Stub_Contract --
1171 -------------------------------------------
1173 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
1174 Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
1175 Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
1178 -- A subprogram body stub may act as its own spec or as the completion
1179 -- of a previous declaration. Depending on the context, the contract of
1180 -- the stub may contain two sets of pragmas.
1182 -- The stub is a completion, the applicable pragmas are:
1186 if Present (Spec_Id) then
1187 Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
1189 -- The stub acts as its own spec, the applicable pragmas are:
1198 Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
1200 end Analyze_Subprogram_Body_Stub_Contract;
1202 ---------------------------
1203 -- Analyze_Task_Contract --
1204 ---------------------------
1206 procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
1207 Items : constant Node_Id := Contract (Task_Id);
1208 Mode : SPARK_Mode_Type;
1212 -- Do not analyze a contract multiple times
1214 if Present (Items) then
1215 if Analyzed (Items) then
1218 Set_Analyzed (Items);
1222 -- Due to the timing of contract analysis, delayed pragmas may be
1223 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1224 -- context. To remedy this, restore the original SPARK_Mode of the
1225 -- related task unit.
1227 Save_SPARK_Mode_And_Set (Task_Id, Mode);
1229 -- Analyze Global first, as Depends may mention items classified in the
1230 -- global categorization.
1232 Prag := Get_Pragma (Task_Id, Pragma_Global);
1234 if Present (Prag) then
1235 Analyze_Global_In_Decl_Part (Prag);
1238 -- Depends must be analyzed after Global in order to see the modes of
1239 -- all global items.
1241 Prag := Get_Pragma (Task_Id, Pragma_Depends);
1243 if Present (Prag) then
1244 Analyze_Depends_In_Decl_Part (Prag);
1247 -- Restore the SPARK_Mode of the enclosing context after all delayed
1248 -- pragmas have been analyzed.
1250 Restore_SPARK_Mode (Mode);
1251 end Analyze_Task_Contract;
1253 -------------------------------------------------
1254 -- Build_And_Analyze_Contract_Only_Subprograms --
1255 -------------------------------------------------
1257 procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is
1258 procedure Analyze_Contract_Only_Subprograms;
1259 -- Analyze the contract-only subprograms of L
1261 procedure Append_Contract_Only_Subprograms (Subp_List : List_Id);
1262 -- Append the contract-only bodies of Subp_List to its declarations list
1264 function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id;
1265 -- If E is an entity for a non-imported subprogram specification with
1266 -- pre/postconditions and we are compiling with CodePeer mode, then
1267 -- this procedure will create a wrapper to help Gnat2scil process its
1268 -- contracts. Return Empty if the wrapper cannot be built.
1270 function Build_Contract_Only_Subprograms (L : List_Id) return List_Id;
1271 -- Build the contract-only subprograms of all eligible subprograms found
1274 function Has_Private_Declarations (N : Node_Id) return Boolean;
1275 -- Return True for package specs, task definitions, and protected type
1276 -- definitions whose list of private declarations is not empty.
1278 ---------------------------------------
1279 -- Analyze_Contract_Only_Subprograms --
1280 ---------------------------------------
1282 procedure Analyze_Contract_Only_Subprograms is
1283 procedure Analyze_Contract_Only_Bodies;
1284 -- Analyze all the contract-only bodies of L
1286 ----------------------------------
1287 -- Analyze_Contract_Only_Bodies --
1288 ----------------------------------
1290 procedure Analyze_Contract_Only_Bodies is
1295 while Present (Decl) loop
1296 if Nkind (Decl) = N_Subprogram_Body
1297 and then Is_Contract_Only_Body
1298 (Defining_Unit_Name (Specification (Decl)))
1305 end Analyze_Contract_Only_Bodies;
1307 -- Start of processing for Analyze_Contract_Only_Subprograms
1310 if Ekind (Current_Scope) /= E_Package then
1311 Analyze_Contract_Only_Bodies;
1315 Pkg_Spec : constant Node_Id :=
1316 Package_Specification (Current_Scope);
1319 if not Has_Private_Declarations (Pkg_Spec) then
1320 Analyze_Contract_Only_Bodies;
1322 -- For packages with private declarations, the contract-only
1323 -- bodies of subprograms defined in the visible part of the
1324 -- package are added to its private declarations (to ensure
1325 -- that they do not cause premature freezing of types and also
1326 -- that they are analyzed with proper visibility). Hence they
1327 -- will be analyzed later.
1329 elsif Visible_Declarations (Pkg_Spec) = L then
1332 elsif Private_Declarations (Pkg_Spec) = L then
1333 Analyze_Contract_Only_Bodies;
1337 end Analyze_Contract_Only_Subprograms;
1339 --------------------------------------
1340 -- Append_Contract_Only_Subprograms --
1341 --------------------------------------
1343 procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is
1345 if No (Subp_List) then
1349 if Ekind (Current_Scope) /= E_Package then
1350 Append_List (Subp_List, To => L);
1354 Pkg_Spec : constant Node_Id :=
1355 Package_Specification (Current_Scope);
1358 if not Has_Private_Declarations (Pkg_Spec) then
1359 Append_List (Subp_List, To => L);
1361 -- If the package has private declarations then append them to
1362 -- its private declarations; they will be analyzed when the
1363 -- contracts of its private declarations are analyzed.
1368 To => Private_Declarations (Pkg_Spec));
1372 end Append_Contract_Only_Subprograms;
1374 ------------------------------------
1375 -- Build_Contract_Only_Subprogram --
1376 ------------------------------------
1378 -- This procedure takes care of building a wrapper to generate better
1379 -- analysis results in the case of a call to a subprogram whose body
1380 -- is unavailable to CodePeer but whose specification includes Pre/Post
1381 -- conditions. The body might be unavailable for any of a number or
1382 -- reasons (it is imported, the .adb file is simply missing, or the
1383 -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
1384 -- pragma). The built subprogram has the following contents:
1385 -- * check preconditions
1386 -- * call the subprogram
1387 -- * check postconditions
1389 function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is
1390 Loc : constant Source_Ptr := Sloc (E);
1392 Missing_Body_Name : constant Name_Id :=
1393 New_External_Name (Chars (E), "__missing_body");
1395 function Build_Missing_Body_Decls return List_Id;
1396 -- Build the declaration of the missing body subprogram and its
1397 -- corresponding pragma Import.
1399 function Build_Missing_Body_Subprogram_Call return Node_Id;
1400 -- Build the call to the missing body subprogram
1402 function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean;
1403 -- Return True for cases where the wrapper is not needed or we cannot
1406 ------------------------------
1407 -- Build_Missing_Body_Decls --
1408 ------------------------------
1410 function Build_Missing_Body_Decls return List_Id is
1411 Spec : constant Node_Id := Declaration_Node (E);
1417 Make_Subprogram_Declaration (Loc, Copy_Subprogram_Spec (Spec));
1418 Set_Chars (Defining_Entity (Decl), Missing_Body_Name);
1422 Chars => Name_Import,
1423 Pragma_Argument_Associations => New_List (
1424 Make_Pragma_Argument_Association (Loc,
1425 Expression => Make_Identifier (Loc, Name_Ada)),
1427 Make_Pragma_Argument_Association (Loc,
1428 Expression => Make_Identifier (Loc, Missing_Body_Name))));
1430 return New_List (Decl, Prag);
1431 end Build_Missing_Body_Decls;
1433 ----------------------------------------
1434 -- Build_Missing_Body_Subprogram_Call --
1435 ----------------------------------------
1437 function Build_Missing_Body_Subprogram_Call return Node_Id is
1444 -- Build parameter list that we need
1446 Forml := First_Formal (E);
1447 while Present (Forml) loop
1448 Append_To (Parms, Make_Identifier (Loc, Chars (Forml)));
1449 Next_Formal (Forml);
1452 -- Build the call to the missing body subprogram
1454 if Ekind_In (E, E_Function, E_Generic_Function) then
1456 Make_Simple_Return_Statement (Loc,
1458 Make_Function_Call (Loc,
1460 Make_Identifier (Loc, Missing_Body_Name),
1461 Parameter_Associations => Parms));
1465 Make_Procedure_Call_Statement (Loc,
1467 Make_Identifier (Loc, Missing_Body_Name),
1468 Parameter_Associations => Parms);
1470 end Build_Missing_Body_Subprogram_Call;
1472 -----------------------------------
1473 -- Skip_Contract_Only_Subprogram --
1474 -----------------------------------
1476 function Skip_Contract_Only_Subprogram
1477 (E : Entity_Id) return Boolean
1479 function Depends_On_Enclosing_Private_Type return Boolean;
1480 -- Return True if some formal of E (or its return type) are
1481 -- private types defined in an enclosing package.
1483 function Some_Enclosing_Package_Has_Private_Decls return Boolean;
1484 -- Return True if some enclosing package of the current scope has
1485 -- private declarations.
1487 ---------------------------------------
1488 -- Depends_On_Enclosing_Private_Type --
1489 ---------------------------------------
1491 function Depends_On_Enclosing_Private_Type return Boolean is
1492 function Defined_In_Enclosing_Package
1493 (Typ : Entity_Id) return Boolean;
1494 -- Return True if Typ is an entity defined in an enclosing
1495 -- package of the current scope.
1497 ----------------------------------
1498 -- Defined_In_Enclosing_Package --
1499 ----------------------------------
1501 function Defined_In_Enclosing_Package
1502 (Typ : Entity_Id) return Boolean
1504 Scop : Entity_Id := Scope (Current_Scope);
1507 while Scop /= Scope (Typ)
1508 and then not Is_Compilation_Unit (Scop)
1510 Scop := Scope (Scop);
1513 return Scop = Scope (Typ);
1514 end Defined_In_Enclosing_Package;
1518 Param_E : Entity_Id;
1521 -- Start of processing for Depends_On_Enclosing_Private_Type
1524 Param_E := First_Entity (E);
1525 while Present (Param_E) loop
1526 Typ := Etype (Param_E);
1528 if Is_Private_Type (Typ)
1529 and then Defined_In_Enclosing_Package (Typ)
1534 Next_Entity (Param_E);
1538 Ekind (E) = E_Function
1539 and then Is_Private_Type (Etype (E))
1540 and then Defined_In_Enclosing_Package (Etype (E));
1541 end Depends_On_Enclosing_Private_Type;
1543 ----------------------------------------------
1544 -- Some_Enclosing_Package_Has_Private_Decls --
1545 ----------------------------------------------
1547 function Some_Enclosing_Package_Has_Private_Decls return Boolean is
1548 Scop : Entity_Id := Current_Scope;
1549 Pkg_Spec : Node_Id := Package_Specification (Scop);
1553 if Ekind (Scop) = E_Package
1554 and then Has_Private_Declarations
1555 (Package_Specification (Scop))
1557 Pkg_Spec := Package_Specification (Scop);
1560 exit when Is_Compilation_Unit (Scop);
1561 Scop := Scope (Scop);
1564 return Pkg_Spec /= Package_Specification (Current_Scope);
1565 end Some_Enclosing_Package_Has_Private_Decls;
1567 -- Start of processing for Skip_Contract_Only_Subprogram
1570 if not CodePeer_Mode
1571 or else Inside_A_Generic
1572 or else not Is_Subprogram (E)
1573 or else Is_Abstract_Subprogram (E)
1574 or else Is_Imported (E)
1575 or else No (Contract (E))
1576 or else No (Pre_Post_Conditions (Contract (E)))
1577 or else Is_Contract_Only_Body (E)
1578 or else Convention (E) = Convention_Protected
1582 -- We do not support building the contract-only subprogram if E
1583 -- is a subprogram declared in a nested package that has some
1584 -- formal or return type depending on a private type defined in
1585 -- an enclosing package.
1587 elsif Ekind (Current_Scope) = E_Package
1588 and then Some_Enclosing_Package_Has_Private_Decls
1589 and then Depends_On_Enclosing_Private_Type
1591 if Debug_Flag_Dot_KK then
1593 Saved_Mode : constant Warning_Mode_Type := Warning_Mode;
1596 -- Warnings are disabled by default under CodePeer_Mode
1597 -- (see switch-c). Enable them temporarily.
1599 Warning_Mode := Normal;
1601 ("cannot generate contract-only subprogram?", E);
1602 Warning_Mode := Saved_Mode;
1610 end Skip_Contract_Only_Subprogram;
1612 -- Start of processing for Build_Contract_Only_Subprogram
1615 -- Test cases where the wrapper is not needed and cases where we
1618 if Skip_Contract_Only_Subprogram (E) then
1622 -- Note on calls to Copy_Separate_Tree. The trees we are copying
1623 -- here are fully analyzed, but we definitely want fully syntactic
1624 -- unanalyzed trees in the body we construct, so that the analysis
1625 -- generates the right visibility, and that is exactly what the
1626 -- calls to Copy_Separate_Tree give us.
1629 Name : constant Name_Id :=
1630 New_External_Name (Chars (E), "__contract_only");
1636 Make_Subprogram_Body (Loc,
1638 Copy_Subprogram_Spec (Declaration_Node (E)),
1640 Build_Missing_Body_Decls,
1641 Handled_Statement_Sequence =>
1642 Make_Handled_Sequence_Of_Statements (Loc,
1643 Statements => New_List (
1644 Build_Missing_Body_Subprogram_Call),
1645 End_Label => Make_Identifier (Loc, Name)));
1647 Id := Defining_Unit_Name (Specification (Bod));
1649 -- Copy only the pre/postconditions of the original contract
1650 -- since it is what we need, but also because pragmas stored in
1651 -- the other fields have N_Pragmas with N_Aspect_Specifications
1652 -- that reference their associated pragma (thus causing an endless
1653 -- loop when trying to copy the subtree).
1656 New_Contract : constant Node_Id := Make_Contract (Sloc (E));
1659 Set_Pre_Post_Conditions (New_Contract,
1660 Copy_Separate_Tree (Pre_Post_Conditions (Contract (E))));
1661 Set_Contract (Id, New_Contract);
1664 -- Fix the name of this new subprogram and link the original
1665 -- subprogram with its Contract_Only_Body subprogram.
1667 Set_Chars (Id, Name);
1668 Set_Is_Contract_Only_Body (Id);
1669 Set_Contract_Only_Body (E, Id);
1673 end Build_Contract_Only_Subprogram;
1675 -------------------------------------
1676 -- Build_Contract_Only_Subprograms --
1677 -------------------------------------
1679 function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is
1682 Result : List_Id := No_List;
1683 Subp_Id : Entity_Id;
1687 while Present (Decl) loop
1688 if Nkind (Decl) = N_Subprogram_Declaration then
1689 Subp_Id := Defining_Unit_Name (Specification (Decl));
1690 New_Subp := Build_Contract_Only_Subprogram (Subp_Id);
1692 if Present (New_Subp) then
1697 Append_To (Result, New_Subp);
1705 end Build_Contract_Only_Subprograms;
1707 ------------------------------
1708 -- Has_Private_Declarations --
1709 ------------------------------
1711 function Has_Private_Declarations (N : Node_Id) return Boolean is
1713 if not Nkind_In (N, N_Package_Specification,
1714 N_Protected_Definition,
1720 Present (Private_Declarations (N))
1721 and then Is_Non_Empty_List (Private_Declarations (N));
1723 end Has_Private_Declarations;
1727 Subp_List : List_Id;
1729 -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
1732 Subp_List := Build_Contract_Only_Subprograms (L);
1733 Append_Contract_Only_Subprograms (Subp_List);
1734 Analyze_Contract_Only_Subprograms;
1735 end Build_And_Analyze_Contract_Only_Subprograms;
1737 -----------------------------
1738 -- Create_Generic_Contract --
1739 -----------------------------
1741 procedure Create_Generic_Contract (Unit : Node_Id) is
1742 Templ : constant Node_Id := Original_Node (Unit);
1743 Templ_Id : constant Entity_Id := Defining_Entity (Templ);
1745 procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
1746 -- Add a single contract-related source pragma Prag to the contract of
1747 -- generic template Templ_Id.
1749 ---------------------------------
1750 -- Add_Generic_Contract_Pragma --
1751 ---------------------------------
1753 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
1754 Prag_Templ : Node_Id;
1757 -- Mark the pragma to prevent the premature capture of global
1758 -- references when capturing global references of the context
1759 -- (see Save_References_In_Pragma).
1761 Set_Is_Generic_Contract_Pragma (Prag);
1763 -- Pragmas that apply to a generic subprogram declaration are not
1764 -- part of the semantic structure of the generic template:
1767 -- procedure Example (Formal : Integer);
1768 -- pragma Precondition (Formal > 0);
1770 -- Create a generic template for such pragmas and link the template
1771 -- of the pragma with the generic template.
1773 if Nkind (Templ) = N_Generic_Subprogram_Declaration then
1775 (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
1776 Prag_Templ := Original_Node (Prag);
1778 Set_Is_Generic_Contract_Pragma (Prag_Templ);
1779 Add_Contract_Item (Prag_Templ, Templ_Id);
1781 -- Otherwise link the pragma with the generic template
1784 Add_Contract_Item (Prag, Templ_Id);
1786 end Add_Generic_Contract_Pragma;
1790 Context : constant Node_Id := Parent (Unit);
1791 Decl : Node_Id := Empty;
1793 -- Start of processing for Create_Generic_Contract
1796 -- A generic package declaration carries contract-related source pragmas
1797 -- in its visible declarations.
1799 if Nkind (Templ) = N_Generic_Package_Declaration then
1800 Set_Ekind (Templ_Id, E_Generic_Package);
1802 if Present (Visible_Declarations (Specification (Templ))) then
1803 Decl := First (Visible_Declarations (Specification (Templ)));
1806 -- A generic package body carries contract-related source pragmas in its
1809 elsif Nkind (Templ) = N_Package_Body then
1810 Set_Ekind (Templ_Id, E_Package_Body);
1812 if Present (Declarations (Templ)) then
1813 Decl := First (Declarations (Templ));
1816 -- Generic subprogram declaration
1818 elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
1819 if Nkind (Specification (Templ)) = N_Function_Specification then
1820 Set_Ekind (Templ_Id, E_Generic_Function);
1822 Set_Ekind (Templ_Id, E_Generic_Procedure);
1825 -- When the generic subprogram acts as a compilation unit, inspect
1826 -- the Pragmas_After list for contract-related source pragmas.
1828 if Nkind (Context) = N_Compilation_Unit then
1829 if Present (Aux_Decls_Node (Context))
1830 and then Present (Pragmas_After (Aux_Decls_Node (Context)))
1832 Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
1835 -- Otherwise inspect the successive declarations for contract-related
1839 Decl := Next (Unit);
1842 -- A generic subprogram body carries contract-related source pragmas in
1843 -- its declarations.
1845 elsif Nkind (Templ) = N_Subprogram_Body then
1846 Set_Ekind (Templ_Id, E_Subprogram_Body);
1848 if Present (Declarations (Templ)) then
1849 Decl := First (Declarations (Templ));
1853 -- Inspect the relevant declarations looking for contract-related source
1854 -- pragmas and add them to the contract of the generic unit.
1856 while Present (Decl) loop
1857 if Comes_From_Source (Decl) then
1858 if Nkind (Decl) = N_Pragma then
1860 -- The source pragma is a contract annotation
1862 if Is_Contract_Annotation (Decl) then
1863 Add_Generic_Contract_Pragma (Decl);
1866 -- The region where a contract-related source pragma may appear
1867 -- ends with the first source non-pragma declaration or statement.
1876 end Create_Generic_Contract;
1878 --------------------------------
1879 -- Expand_Subprogram_Contract --
1880 --------------------------------
1882 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is
1883 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
1884 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
1886 procedure Add_Invariant_And_Predicate_Checks
1887 (Subp_Id : Entity_Id;
1888 Stmts : in out List_Id;
1889 Result : out Node_Id);
1890 -- Process the result of function Subp_Id (if applicable) and all its
1891 -- formals. Add invariant and predicate checks where applicable. The
1892 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1893 -- function, Result contains the entity of parameter _Result, to be
1894 -- used in the creation of procedure _Postconditions.
1896 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
1897 -- Append a node to a list. If there is no list, create a new one. When
1898 -- the item denotes a pragma, it is added to the list only when it is
1901 procedure Build_Postconditions_Procedure
1902 (Subp_Id : Entity_Id;
1904 Result : Entity_Id);
1905 -- Create the body of procedure _Postconditions which handles various
1906 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1907 -- of statements to be checked on exit. Parameter Result is the entity
1908 -- of parameter _Result when Subp_Id denotes a function.
1910 procedure Process_Contract_Cases (Stmts : in out List_Id);
1911 -- Process pragma Contract_Cases. This routine prepends items to the
1912 -- body declarations and appends items to list Stmts.
1914 procedure Process_Postconditions (Stmts : in out List_Id);
1915 -- Collect all [inherited] spec and body postconditions and accumulate
1916 -- their pragma Check equivalents in list Stmts.
1918 procedure Process_Preconditions;
1919 -- Collect all [inherited] spec and body preconditions and prepend their
1920 -- pragma Check equivalents to the declarations of the body.
1922 ----------------------------------------
1923 -- Add_Invariant_And_Predicate_Checks --
1924 ----------------------------------------
1926 procedure Add_Invariant_And_Predicate_Checks
1927 (Subp_Id : Entity_Id;
1928 Stmts : in out List_Id;
1929 Result : out Node_Id)
1931 procedure Add_Invariant_Access_Checks (Id : Entity_Id);
1932 -- Id denotes the return value of a function or a formal parameter.
1933 -- Add an invariant check if the type of Id is access to a type with
1934 -- invariants. The routine appends the generated code to Stmts.
1936 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
1937 -- Determine whether type Typ can benefit from invariant checks. To
1938 -- qualify, the type must have a non-null invariant procedure and
1939 -- subprogram Subp_Id must appear visible from the point of view of
1942 ---------------------------------
1943 -- Add_Invariant_Access_Checks --
1944 ---------------------------------
1946 procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
1947 Loc : constant Source_Ptr := Sloc (Body_Decl);
1954 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
1955 Typ := Designated_Type (Typ);
1957 if Invariant_Checks_OK (Typ) then
1959 Make_Explicit_Dereference (Loc,
1960 Prefix => New_Occurrence_Of (Id, Loc));
1961 Set_Etype (Ref, Typ);
1964 -- if <Id> /= null then
1965 -- <invariant_call (<Ref>)>
1970 Make_If_Statement (Loc,
1973 Left_Opnd => New_Occurrence_Of (Id, Loc),
1974 Right_Opnd => Make_Null (Loc)),
1975 Then_Statements => New_List (
1976 Make_Invariant_Call (Ref))),
1980 end Add_Invariant_Access_Checks;
1982 -------------------------
1983 -- Invariant_Checks_OK --
1984 -------------------------
1986 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
1987 function Has_Public_Visibility_Of_Subprogram return Boolean;
1988 -- Determine whether type Typ has public visibility of subprogram
1991 -----------------------------------------
1992 -- Has_Public_Visibility_Of_Subprogram --
1993 -----------------------------------------
1995 function Has_Public_Visibility_Of_Subprogram return Boolean is
1996 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
1999 -- An Initialization procedure must be considered visible even
2000 -- though it is internally generated.
2002 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
2005 elsif Ekind (Scope (Typ)) /= E_Package then
2008 -- Internally generated code is never publicly visible except
2009 -- for a subprogram that is the implementation of an expression
2010 -- function. In that case the visibility is determined by the
2013 elsif not Comes_From_Source (Subp_Decl)
2015 (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
2017 Comes_From_Source (Defining_Entity (Subp_Decl)))
2021 -- Determine whether the subprogram is declared in the visible
2022 -- declarations of the package containing the type, or in the
2023 -- visible declaration of a child unit of that package.
2027 Decls : constant List_Id :=
2028 List_Containing (Subp_Decl);
2029 Subp_Scope : constant Entity_Id :=
2030 Scope (Defining_Entity (Subp_Decl));
2031 Typ_Scope : constant Entity_Id := Scope (Typ);
2035 Decls = Visible_Declarations
2036 (Specification (Unit_Declaration_Node (Typ_Scope)))
2039 (Ekind (Subp_Scope) = E_Package
2040 and then Typ_Scope /= Subp_Scope
2041 and then Is_Child_Unit (Subp_Scope)
2043 Is_Ancestor_Package (Typ_Scope, Subp_Scope)
2045 Decls = Visible_Declarations
2047 (Unit_Declaration_Node (Subp_Scope))));
2050 end Has_Public_Visibility_Of_Subprogram;
2052 -- Start of processing for Invariant_Checks_OK
2056 Has_Invariants (Typ)
2057 and then Present (Invariant_Procedure (Typ))
2058 and then not Has_Null_Body (Invariant_Procedure (Typ))
2059 and then Has_Public_Visibility_Of_Subprogram;
2060 end Invariant_Checks_OK;
2064 Loc : constant Source_Ptr := Sloc (Body_Decl);
2065 -- Source location of subprogram body contract
2070 -- Start of processing for Add_Invariant_And_Predicate_Checks
2075 -- Process the result of a function
2077 if Ekind (Subp_Id) = E_Function then
2078 Typ := Etype (Subp_Id);
2080 -- Generate _Result which is used in procedure _Postconditions to
2081 -- verify the return value.
2083 Result := Make_Defining_Identifier (Loc, Name_uResult);
2084 Set_Etype (Result, Typ);
2086 -- Add an invariant check when the return type has invariants and
2087 -- the related function is visible to the outside.
2089 if Invariant_Checks_OK (Typ) then
2092 Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
2096 -- Add an invariant check when the return type is an access to a
2097 -- type with invariants.
2099 Add_Invariant_Access_Checks (Result);
2102 -- Add invariant and predicates for all formals that qualify
2104 Formal := First_Formal (Subp_Id);
2105 while Present (Formal) loop
2106 Typ := Etype (Formal);
2108 if Ekind (Formal) /= E_In_Parameter
2109 or else Is_Access_Type (Typ)
2111 if Invariant_Checks_OK (Typ) then
2114 Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
2118 Add_Invariant_Access_Checks (Formal);
2120 -- Note: we used to add predicate checks for OUT and IN OUT
2121 -- formals here, but that was misguided, since such checks are
2122 -- performed on the caller side, based on the predicate of the
2123 -- actual, rather than the predicate of the formal.
2127 Next_Formal (Formal);
2129 end Add_Invariant_And_Predicate_Checks;
2131 -------------------------
2132 -- Append_Enabled_Item --
2133 -------------------------
2135 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
2137 -- Do not chain ignored or disabled pragmas
2139 if Nkind (Item) = N_Pragma
2140 and then (Is_Ignored (Item) or else Is_Disabled (Item))
2144 -- Otherwise, add the item
2151 -- If the pragma is a conjunct in a composite postcondition, it
2152 -- has been processed in reverse order. In the postcondition body
2153 -- it must appear before the others.
2155 if Nkind (Item) = N_Pragma
2156 and then From_Aspect_Specification (Item)
2157 and then Split_PPC (Item)
2159 Prepend (Item, List);
2161 Append (Item, List);
2164 end Append_Enabled_Item;
2166 ------------------------------------
2167 -- Build_Postconditions_Procedure --
2168 ------------------------------------
2170 procedure Build_Postconditions_Procedure
2171 (Subp_Id : Entity_Id;
2175 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
2176 -- Insert node Stmt before the first source declaration of the
2177 -- related subprogram's body. If no such declaration exists, Stmt
2178 -- becomes the last declaration.
2180 --------------------------------------------
2181 -- Insert_Before_First_Source_Declaration --
2182 --------------------------------------------
2184 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
2185 Decls : constant List_Id := Declarations (Body_Decl);
2189 -- Inspect the declarations of the related subprogram body looking
2190 -- for the first source declaration.
2192 if Present (Decls) then
2193 Decl := First (Decls);
2194 while Present (Decl) loop
2195 if Comes_From_Source (Decl) then
2196 Insert_Before (Decl, Stmt);
2203 -- If we get there, then the subprogram body lacks any source
2204 -- declarations. The body of _Postconditions now acts as the
2205 -- last declaration.
2207 Append (Stmt, Decls);
2209 -- Ensure that the body has a declaration list
2212 Set_Declarations (Body_Decl, New_List (Stmt));
2214 end Insert_Before_First_Source_Declaration;
2218 Loc : constant Source_Ptr := Sloc (Body_Decl);
2219 Params : List_Id := No_List;
2221 Proc_Decl : Node_Id;
2222 Proc_Id : Entity_Id;
2223 Proc_Spec : Node_Id;
2225 -- Start of processing for Build_Postconditions_Procedure
2228 -- Nothing to do if there are no actions to check on exit
2234 Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
2235 Set_Debug_Info_Needed (Proc_Id);
2236 Set_Postconditions_Proc (Subp_Id, Proc_Id);
2238 -- Force the front-end inlining of _Postconditions when generating C
2239 -- code, since its body may have references to itypes defined in the
2240 -- enclosing subprogram, which would cause problems for unnesting
2241 -- routines in the absence of inlining.
2243 if Modify_Tree_For_C then
2244 Set_Has_Pragma_Inline (Proc_Id);
2245 Set_Has_Pragma_Inline_Always (Proc_Id);
2246 Set_Is_Inlined (Proc_Id);
2249 -- The related subprogram is a function: create the specification of
2250 -- parameter _Result.
2252 if Present (Result) then
2253 Params := New_List (
2254 Make_Parameter_Specification (Loc,
2255 Defining_Identifier => Result,
2257 New_Occurrence_Of (Etype (Result), Loc)));
2261 Make_Procedure_Specification (Loc,
2262 Defining_Unit_Name => Proc_Id,
2263 Parameter_Specifications => Params);
2265 Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
2267 -- Insert _Postconditions before the first source declaration of the
2268 -- body. This ensures that the body will not cause any premature
2269 -- freezing, as it may mention types:
2271 -- procedure Proc (Obj : Array_Typ) is
2272 -- procedure _postconditions is
2275 -- end _postconditions;
2277 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
2280 -- In the example above, Obj is of type T but the incorrect placement
2281 -- of _Postconditions will cause a crash in gigi due to an out-of-
2282 -- order reference. The body of _Postconditions must be placed after
2283 -- the declaration of Temp to preserve correct visibility.
2285 Insert_Before_First_Source_Declaration (Proc_Decl);
2286 Analyze (Proc_Decl);
2288 -- Set an explicit End_Label to override the sloc of the implicit
2289 -- RETURN statement, and prevent it from inheriting the sloc of one
2290 -- the postconditions: this would cause confusing debug info to be
2291 -- produced, interfering with coverage-analysis tools.
2294 Make_Subprogram_Body (Loc,
2296 Copy_Subprogram_Spec (Proc_Spec),
2297 Declarations => Empty_List,
2298 Handled_Statement_Sequence =>
2299 Make_Handled_Sequence_Of_Statements (Loc,
2300 Statements => Stmts,
2301 End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
2303 Insert_After_And_Analyze (Proc_Decl, Proc_Bod);
2304 end Build_Postconditions_Procedure;
2306 ----------------------------
2307 -- Process_Contract_Cases --
2308 ----------------------------
2310 procedure Process_Contract_Cases (Stmts : in out List_Id) is
2311 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
2312 -- Process pragma Contract_Cases for subprogram Subp_Id
2314 --------------------------------
2315 -- Process_Contract_Cases_For --
2316 --------------------------------
2318 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
2319 Items : constant Node_Id := Contract (Subp_Id);
2323 if Present (Items) then
2324 Prag := Contract_Test_Cases (Items);
2325 while Present (Prag) loop
2326 if Pragma_Name (Prag) = Name_Contract_Cases then
2327 Expand_Pragma_Contract_Cases
2330 Decls => Declarations (Body_Decl),
2334 Prag := Next_Pragma (Prag);
2337 end Process_Contract_Cases_For;
2339 -- Start of processing for Process_Contract_Cases
2342 Process_Contract_Cases_For (Body_Id);
2344 if Present (Spec_Id) then
2345 Process_Contract_Cases_For (Spec_Id);
2347 end Process_Contract_Cases;
2349 ----------------------------
2350 -- Process_Postconditions --
2351 ----------------------------
2353 procedure Process_Postconditions (Stmts : in out List_Id) is
2354 procedure Process_Body_Postconditions (Post_Nam : Name_Id);
2355 -- Collect all [refined] postconditions of a specific kind denoted
2356 -- by Post_Nam that belong to the body, and generate pragma Check
2357 -- equivalents in list Stmts.
2359 procedure Process_Spec_Postconditions;
2360 -- Collect all [inherited] postconditions of the spec, and generate
2361 -- pragma Check equivalents in list Stmts.
2363 ---------------------------------
2364 -- Process_Body_Postconditions --
2365 ---------------------------------
2367 procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
2368 Items : constant Node_Id := Contract (Body_Id);
2369 Unit_Decl : constant Node_Id := Parent (Body_Decl);
2374 -- Process the contract
2376 if Present (Items) then
2377 Prag := Pre_Post_Conditions (Items);
2378 while Present (Prag) loop
2379 if Pragma_Name (Prag) = Post_Nam then
2381 (Item => Build_Pragma_Check_Equivalent (Prag),
2385 Prag := Next_Pragma (Prag);
2389 -- The subprogram body being processed is actually the proper body
2390 -- of a stub with a corresponding spec. The subprogram stub may
2391 -- carry a postcondition pragma, in which case it must be taken
2392 -- into account. The pragma appears after the stub.
2394 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
2395 Decl := Next (Corresponding_Stub (Unit_Decl));
2396 while Present (Decl) loop
2398 -- Note that non-matching pragmas are skipped
2400 if Nkind (Decl) = N_Pragma then
2401 if Pragma_Name (Decl) = Post_Nam then
2403 (Item => Build_Pragma_Check_Equivalent (Decl),
2407 -- Skip internally generated code
2409 elsif not Comes_From_Source (Decl) then
2412 -- Postcondition pragmas are usually grouped together. There
2413 -- is no need to inspect the whole declarative list.
2422 end Process_Body_Postconditions;
2424 ---------------------------------
2425 -- Process_Spec_Postconditions --
2426 ---------------------------------
2428 procedure Process_Spec_Postconditions is
2429 Subps : constant Subprogram_List :=
2430 Inherited_Subprograms (Spec_Id);
2433 Subp_Id : Entity_Id;
2436 -- Process the contract
2438 Items := Contract (Spec_Id);
2440 if Present (Items) then
2441 Prag := Pre_Post_Conditions (Items);
2442 while Present (Prag) loop
2443 if Pragma_Name (Prag) = Name_Postcondition then
2445 (Item => Build_Pragma_Check_Equivalent (Prag),
2449 Prag := Next_Pragma (Prag);
2453 -- Process the contracts of all inherited subprograms, looking for
2454 -- class-wide postconditions.
2456 for Index in Subps'Range loop
2457 Subp_Id := Subps (Index);
2458 Items := Contract (Subp_Id);
2460 if Present (Items) then
2461 Prag := Pre_Post_Conditions (Items);
2462 while Present (Prag) loop
2463 if Pragma_Name (Prag) = Name_Postcondition
2464 and then Class_Present (Prag)
2468 Build_Pragma_Check_Equivalent
2471 Inher_Id => Subp_Id),
2475 Prag := Next_Pragma (Prag);
2479 end Process_Spec_Postconditions;
2481 -- Start of processing for Process_Postconditions
2484 -- The processing of postconditions is done in reverse order (body
2485 -- first) to ensure the following arrangement:
2487 -- <refined postconditions from body>
2488 -- <postconditions from body>
2489 -- <postconditions from spec>
2490 -- <inherited postconditions>
2492 Process_Body_Postconditions (Name_Refined_Post);
2493 Process_Body_Postconditions (Name_Postcondition);
2495 if Present (Spec_Id) then
2496 Process_Spec_Postconditions;
2498 end Process_Postconditions;
2500 ---------------------------
2501 -- Process_Preconditions --
2502 ---------------------------
2504 procedure Process_Preconditions is
2505 Class_Pre : Node_Id := Empty;
2506 -- The sole [inherited] class-wide precondition pragma that applies
2507 -- to the subprogram.
2509 Insert_Node : Node_Id := Empty;
2510 -- The insertion node after which all pragma Check equivalents are
2513 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
2514 -- Determine whether arbitrary declaration Decl denotes a renaming of
2515 -- a discriminant or protection field _object.
2517 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
2518 -- Merge two class-wide preconditions by "or else"-ing them. The
2519 -- changes are accumulated in parameter Into. Update the error
2522 procedure Prepend_To_Decls (Item : Node_Id);
2523 -- Prepend a single item to the declarations of the subprogram body
2525 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
2526 -- Save a class-wide precondition into Class_Pre, or prepend a normal
2527 -- precondition to the declarations of the body and analyze it.
2529 procedure Process_Inherited_Preconditions;
2530 -- Collect all inherited class-wide preconditions and merge them into
2531 -- one big precondition to be evaluated as pragma Check.
2533 procedure Process_Preconditions_For (Subp_Id : Entity_Id);
2534 -- Collect all preconditions of subprogram Subp_Id and prepend their
2535 -- pragma Check equivalents to the declarations of the body.
2537 --------------------------
2538 -- Is_Prologue_Renaming --
2539 --------------------------
2541 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
2548 if Nkind (Decl) = N_Object_Renaming_Declaration then
2549 Obj := Defining_Entity (Decl);
2552 if Nkind (Nam) = N_Selected_Component then
2553 Pref := Prefix (Nam);
2554 Sel := Selector_Name (Nam);
2556 -- A discriminant renaming appears as
2557 -- Discr : constant ... := Prefix.Discr;
2559 if Ekind (Obj) = E_Constant
2560 and then Is_Entity_Name (Sel)
2561 and then Present (Entity (Sel))
2562 and then Ekind (Entity (Sel)) = E_Discriminant
2566 -- A protection field renaming appears as
2567 -- Prot : ... := _object._object;
2569 -- A renamed private component is just a component of
2570 -- _object, with an arbitrary name.
2572 elsif Ekind (Obj) = E_Variable
2573 and then Nkind (Pref) = N_Identifier
2574 and then Chars (Pref) = Name_uObject
2575 and then Nkind (Sel) = N_Identifier
2583 end Is_Prologue_Renaming;
2585 -------------------------
2586 -- Merge_Preconditions --
2587 -------------------------
2589 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
2590 function Expression_Arg (Prag : Node_Id) return Node_Id;
2591 -- Return the boolean expression argument of a precondition while
2592 -- updating its parentheses count for the subsequent merge.
2594 function Message_Arg (Prag : Node_Id) return Node_Id;
2595 -- Return the message argument of a precondition
2597 --------------------
2598 -- Expression_Arg --
2599 --------------------
2601 function Expression_Arg (Prag : Node_Id) return Node_Id is
2602 Args : constant List_Id := Pragma_Argument_Associations (Prag);
2603 Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
2606 if Paren_Count (Arg) = 0 then
2607 Set_Paren_Count (Arg, 1);
2617 function Message_Arg (Prag : Node_Id) return Node_Id is
2618 Args : constant List_Id := Pragma_Argument_Associations (Prag);
2620 return Get_Pragma_Arg (Last (Args));
2625 From_Expr : constant Node_Id := Expression_Arg (From);
2626 From_Msg : constant Node_Id := Message_Arg (From);
2627 Into_Expr : constant Node_Id := Expression_Arg (Into);
2628 Into_Msg : constant Node_Id := Message_Arg (Into);
2629 Loc : constant Source_Ptr := Sloc (Into);
2631 -- Start of processing for Merge_Preconditions
2634 -- Merge the two preconditions by "or else"-ing them
2638 Right_Opnd => Relocate_Node (Into_Expr),
2639 Left_Opnd => From_Expr));
2641 -- Merge the two error messages to produce a single message of the
2644 -- failed precondition from ...
2645 -- also failed inherited precondition from ...
2647 if not Exception_Locations_Suppressed then
2648 Start_String (Strval (Into_Msg));
2649 Store_String_Char (ASCII.LF);
2650 Store_String_Chars (" also ");
2651 Store_String_Chars (Strval (From_Msg));
2653 Set_Strval (Into_Msg, End_String);
2655 end Merge_Preconditions;
2657 ----------------------
2658 -- Prepend_To_Decls --
2659 ----------------------
2661 procedure Prepend_To_Decls (Item : Node_Id) is
2662 Decls : List_Id := Declarations (Body_Decl);
2665 -- Ensure that the body has a declarative list
2669 Set_Declarations (Body_Decl, Decls);
2672 Prepend_To (Decls, Item);
2673 end Prepend_To_Decls;
2675 ------------------------------
2676 -- Prepend_To_Decls_Or_Save --
2677 ------------------------------
2679 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
2680 Check_Prag : Node_Id;
2683 Check_Prag := Build_Pragma_Check_Equivalent (Prag);
2685 -- Save the sole class-wide precondition (if any) for the next
2686 -- step, where it will be merged with inherited preconditions.
2688 if Class_Present (Prag) then
2689 pragma Assert (No (Class_Pre));
2690 Class_Pre := Check_Prag;
2692 -- Accumulate the corresponding Check pragmas at the top of the
2693 -- declarations. Prepending the items ensures that they will be
2694 -- evaluated in their original order.
2697 if Present (Insert_Node) then
2698 Insert_After (Insert_Node, Check_Prag);
2700 Prepend_To_Decls (Check_Prag);
2703 Analyze (Check_Prag);
2705 end Prepend_To_Decls_Or_Save;
2707 -------------------------------------
2708 -- Process_Inherited_Preconditions --
2709 -------------------------------------
2711 procedure Process_Inherited_Preconditions is
2712 Subps : constant Subprogram_List :=
2713 Inherited_Subprograms (Spec_Id);
2714 Check_Prag : Node_Id;
2717 Subp_Id : Entity_Id;
2720 -- Process the contracts of all inherited subprograms, looking for
2721 -- class-wide preconditions.
2723 for Index in Subps'Range loop
2724 Subp_Id := Subps (Index);
2725 Items := Contract (Subp_Id);
2727 if Present (Items) then
2728 Prag := Pre_Post_Conditions (Items);
2729 while Present (Prag) loop
2730 if Pragma_Name (Prag) = Name_Precondition
2731 and then Class_Present (Prag)
2734 Build_Pragma_Check_Equivalent
2737 Inher_Id => Subp_Id);
2739 -- The spec of an inherited subprogram already yielded
2740 -- a class-wide precondition. Merge the existing
2741 -- precondition with the current one using "or else".
2743 if Present (Class_Pre) then
2744 Merge_Preconditions (Check_Prag, Class_Pre);
2746 Class_Pre := Check_Prag;
2750 Prag := Next_Pragma (Prag);
2755 -- Add the merged class-wide preconditions
2757 if Present (Class_Pre) then
2758 Prepend_To_Decls (Class_Pre);
2759 Analyze (Class_Pre);
2761 end Process_Inherited_Preconditions;
2763 -------------------------------
2764 -- Process_Preconditions_For --
2765 -------------------------------
2767 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
2768 Items : constant Node_Id := Contract (Subp_Id);
2771 Subp_Decl : Node_Id;
2774 -- Process the contract
2776 if Present (Items) then
2777 Prag := Pre_Post_Conditions (Items);
2778 while Present (Prag) loop
2779 if Pragma_Name (Prag) = Name_Precondition then
2780 Prepend_To_Decls_Or_Save (Prag);
2783 Prag := Next_Pragma (Prag);
2787 -- The subprogram declaration being processed is actually a body
2788 -- stub. The stub may carry a precondition pragma, in which case
2789 -- it must be taken into account. The pragma appears after the
2792 Subp_Decl := Unit_Declaration_Node (Subp_Id);
2794 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
2796 -- Inspect the declarations following the body stub
2798 Decl := Next (Subp_Decl);
2799 while Present (Decl) loop
2801 -- Note that non-matching pragmas are skipped
2803 if Nkind (Decl) = N_Pragma then
2804 if Pragma_Name (Decl) = Name_Precondition then
2805 Prepend_To_Decls_Or_Save (Decl);
2808 -- Skip internally generated code
2810 elsif not Comes_From_Source (Decl) then
2813 -- Preconditions are usually grouped together. There is no
2814 -- need to inspect the whole declarative list.
2823 end Process_Preconditions_For;
2827 Decls : constant List_Id := Declarations (Body_Decl);
2830 -- Start of processing for Process_Preconditions
2833 -- Find the proper insertion point for all pragma Check equivalents
2835 if Present (Decls) then
2836 Decl := First (Decls);
2837 while Present (Decl) loop
2839 -- First source declaration terminates the search, because all
2840 -- preconditions must be evaluated prior to it, by definition.
2842 if Comes_From_Source (Decl) then
2845 -- Certain internally generated object renamings such as those
2846 -- for discriminants and protection fields must be elaborated
2847 -- before the preconditions are evaluated, as their expressions
2848 -- may mention the discriminants. The renamings include those
2849 -- for private components so we need to find the last such.
2851 elsif Is_Prologue_Renaming (Decl) then
2852 while Present (Next (Decl))
2853 and then Is_Prologue_Renaming (Next (Decl))
2858 Insert_Node := Decl;
2860 -- Otherwise the declaration does not come from source. This
2861 -- also terminates the search, because internal code may raise
2862 -- exceptions which should not preempt the preconditions.
2872 -- The processing of preconditions is done in reverse order (body
2873 -- first), because each pragma Check equivalent is inserted at the
2874 -- top of the declarations. This ensures that the final order is
2875 -- consistent with following diagram:
2877 -- <inherited preconditions>
2878 -- <preconditions from spec>
2879 -- <preconditions from body>
2881 Process_Preconditions_For (Body_Id);
2883 if Present (Spec_Id) then
2884 Process_Preconditions_For (Spec_Id);
2885 Process_Inherited_Preconditions;
2887 end Process_Preconditions;
2891 Restore_Scope : Boolean := False;
2893 Stmts : List_Id := No_List;
2894 Subp_Id : Entity_Id;
2896 -- Start of processing for Expand_Subprogram_Contract
2899 -- Obtain the entity of the initial declaration
2901 if Present (Spec_Id) then
2907 -- Do not perform expansion activity when it is not needed
2909 if not Expander_Active then
2912 -- ASIS requires an unaltered tree
2914 elsif ASIS_Mode then
2917 -- GNATprove does not need the executable semantics of a contract
2919 elsif GNATprove_Mode then
2922 -- The contract of a generic subprogram or one declared in a generic
2923 -- context is not expanded, as the corresponding instance will provide
2924 -- the executable semantics of the contract.
2926 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
2929 -- All subprograms carry a contract, but for some it is not significant
2930 -- and should not be processed. This is a small optimization.
2932 elsif not Has_Significant_Contract (Subp_Id) then
2935 -- The contract of an ignored Ghost subprogram does not need expansion,
2936 -- because the subprogram and all calls to it will be removed.
2938 elsif Is_Ignored_Ghost_Entity (Subp_Id) then
2942 -- Do not re-expand the same contract. This scenario occurs when a
2943 -- construct is rewritten into something else during its analysis
2944 -- (expression functions for instance).
2946 if Has_Expanded_Contract (Subp_Id) then
2949 -- Otherwise mark the subprogram
2952 Set_Has_Expanded_Contract (Subp_Id);
2955 -- Ensure that the formal parameters are visible when expanding all
2958 if not In_Open_Scopes (Subp_Id) then
2959 Restore_Scope := True;
2960 Push_Scope (Subp_Id);
2962 if Is_Generic_Subprogram (Subp_Id) then
2963 Install_Generic_Formals (Subp_Id);
2965 Install_Formals (Subp_Id);
2969 -- The expansion of a subprogram contract involves the creation of Check
2970 -- pragmas to verify the contract assertions of the spec and body in a
2971 -- particular order. The order is as follows:
2973 -- function Example (...) return ... is
2974 -- procedure _Postconditions (...) is
2976 -- <refined postconditions from body>
2977 -- <postconditions from body>
2978 -- <postconditions from spec>
2979 -- <inherited postconditions>
2980 -- <contract case consequences>
2981 -- <invariant check of function result>
2982 -- <invariant and predicate checks of parameters>
2983 -- end _Postconditions;
2985 -- <inherited preconditions>
2986 -- <preconditions from spec>
2987 -- <preconditions from body>
2988 -- <contract case conditions>
2990 -- <source declarations>
2992 -- <source statements>
2994 -- _Preconditions (Result);
2998 -- Routine _Postconditions holds all contract assertions that must be
2999 -- verified on exit from the related subprogram.
3001 -- Step 1: Handle all preconditions. This action must come before the
3002 -- processing of pragma Contract_Cases because the pragma prepends items
3003 -- to the body declarations.
3005 Process_Preconditions;
3007 -- Step 2: Handle all postconditions. This action must come before the
3008 -- processing of pragma Contract_Cases because the pragma appends items
3011 Process_Postconditions (Stmts);
3013 -- Step 3: Handle pragma Contract_Cases. This action must come before
3014 -- the processing of invariants and predicates because those append
3015 -- items to list Stmts.
3017 Process_Contract_Cases (Stmts);
3019 -- Step 4: Apply invariant and predicate checks on a function result and
3020 -- all formals. The resulting checks are accumulated in list Stmts.
3022 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
3024 -- Step 5: Construct procedure _Postconditions
3026 Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
3028 if Restore_Scope then
3031 end Expand_Subprogram_Contract;
3033 ---------------------------------
3034 -- Inherit_Subprogram_Contract --
3035 ---------------------------------
3037 procedure Inherit_Subprogram_Contract
3039 From_Subp : Entity_Id)
3041 procedure Inherit_Pragma (Prag_Id : Pragma_Id);
3042 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
3045 --------------------
3046 -- Inherit_Pragma --
3047 --------------------
3049 procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
3050 Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
3054 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
3055 -- chains, therefore the node must be replicated. The new pragma is
3056 -- flagged as inherited for distinction purposes.
3058 if Present (Prag) then
3059 New_Prag := New_Copy_Tree (Prag);
3060 Set_Is_Inherited_Pragma (New_Prag);
3062 Add_Contract_Item (New_Prag, Subp);
3066 -- Start of processing for Inherit_Subprogram_Contract
3069 -- Inheritance is carried out only when both entities are subprograms
3072 if Is_Subprogram_Or_Generic_Subprogram (Subp)
3073 and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
3074 and then Present (Contract (From_Subp))
3076 Inherit_Pragma (Pragma_Extensions_Visible);
3078 end Inherit_Subprogram_Contract;
3080 -------------------------------------
3081 -- Instantiate_Subprogram_Contract --
3082 -------------------------------------
3084 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
3085 procedure Instantiate_Pragmas (First_Prag : Node_Id);
3086 -- Instantiate all contract-related source pragmas found in the list,
3087 -- starting with pragma First_Prag. Each instantiated pragma is added
3090 -------------------------
3091 -- Instantiate_Pragmas --
3092 -------------------------
3094 procedure Instantiate_Pragmas (First_Prag : Node_Id) is
3095 Inst_Prag : Node_Id;
3100 while Present (Prag) loop
3101 if Is_Generic_Contract_Pragma (Prag) then
3103 Copy_Generic_Node (Prag, Empty, Instantiating => True);
3105 Set_Analyzed (Inst_Prag, False);
3106 Append_To (L, Inst_Prag);
3109 Prag := Next_Pragma (Prag);
3111 end Instantiate_Pragmas;
3115 Items : constant Node_Id := Contract (Defining_Entity (Templ));
3117 -- Start of processing for Instantiate_Subprogram_Contract
3120 if Present (Items) then
3121 Instantiate_Pragmas (Pre_Post_Conditions (Items));
3122 Instantiate_Pragmas (Contract_Test_Cases (Items));
3123 Instantiate_Pragmas (Classifications (Items));
3125 end Instantiate_Subprogram_Contract;
3127 ----------------------------------------
3128 -- Save_Global_References_In_Contract --
3129 ----------------------------------------
3131 procedure Save_Global_References_In_Contract
3135 procedure Save_Global_References_In_List (First_Prag : Node_Id);
3136 -- Save all global references in contract-related source pragmas found
3137 -- in the list, starting with pragma First_Prag.
3139 ------------------------------------
3140 -- Save_Global_References_In_List --
3141 ------------------------------------
3143 procedure Save_Global_References_In_List (First_Prag : Node_Id) is
3148 while Present (Prag) loop
3149 if Is_Generic_Contract_Pragma (Prag) then
3150 Save_Global_References (Prag);
3153 Prag := Next_Pragma (Prag);
3155 end Save_Global_References_In_List;
3159 Items : constant Node_Id := Contract (Defining_Entity (Templ));
3161 -- Start of processing for Save_Global_References_In_Contract
3164 -- The entity of the analyzed generic copy must be on the scope stack
3165 -- to ensure proper detection of global references.
3167 Push_Scope (Gen_Id);
3169 if Permits_Aspect_Specifications (Templ)
3170 and then Has_Aspects (Templ)
3172 Save_Global_References_In_Aspects (Templ);
3175 if Present (Items) then
3176 Save_Global_References_In_List (Pre_Post_Conditions (Items));
3177 Save_Global_References_In_List (Contract_Test_Cases (Items));
3178 Save_Global_References_In_List (Classifications (Items));
3182 end Save_Global_References_In_Contract;