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