1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- C O N T R A C T S --
9 -- Copyright (C) 2015, 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 Einfo; use Einfo;
29 with Elists; use Elists;
30 with Errout; use Errout;
31 with Exp_Prag; use Exp_Prag;
32 with Exp_Tss; use Exp_Tss;
33 with Exp_Util; use Exp_Util;
34 with Namet; use Namet;
35 with Nlists; use Nlists;
36 with Nmake; use Nmake;
39 with Sem_Aux; use Sem_Aux;
40 with Sem_Ch6; use Sem_Ch6;
41 with Sem_Ch8; use Sem_Ch8;
42 with Sem_Ch12; use Sem_Ch12;
43 with Sem_Disp; use Sem_Disp;
44 with Sem_Prag; use Sem_Prag;
45 with Sem_Util; use Sem_Util;
46 with Sinfo; use Sinfo;
47 with Snames; use Snames;
48 with Stringt; use Stringt;
49 with Tbuild; use Tbuild;
51 package body Contracts is
53 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
54 -- Expand the contracts of a subprogram body and its correspoding spec (if
55 -- any). This routine processes all [refined] pre- and postconditions as
56 -- well as Contract_Cases, invariants and predicates. Body_Id denotes the
57 -- entity of the subprogram body.
59 -----------------------
60 -- Add_Contract_Item --
61 -----------------------
63 procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
64 Items : Node_Id := Contract (Id);
66 procedure Add_Classification;
67 -- Prepend Prag to the list of classifications
69 procedure Add_Contract_Test_Case;
70 -- Prepend Prag to the list of contract and test cases
72 procedure Add_Pre_Post_Condition;
73 -- Prepend Prag to the list of pre- and postconditions
75 ------------------------
76 -- Add_Classification --
77 ------------------------
79 procedure Add_Classification is
81 Set_Next_Pragma (Prag, Classifications (Items));
82 Set_Classifications (Items, Prag);
83 end Add_Classification;
85 ----------------------------
86 -- Add_Contract_Test_Case --
87 ----------------------------
89 procedure Add_Contract_Test_Case is
91 Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
92 Set_Contract_Test_Cases (Items, Prag);
93 end Add_Contract_Test_Case;
95 ----------------------------
96 -- Add_Pre_Post_Condition --
97 ----------------------------
99 procedure Add_Pre_Post_Condition is
101 Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
102 Set_Pre_Post_Conditions (Items, Prag);
103 end Add_Pre_Post_Condition;
109 -- Start of processing for Add_Contract_Item
112 -- A contract must contain only pragmas
114 pragma Assert (Nkind (Prag) = N_Pragma);
115 Prag_Nam := Pragma_Name (Prag);
117 -- Create a new contract when adding the first item
120 Items := Make_Contract (Sloc (Id));
121 Set_Contract (Id, Items);
124 -- Contract items related to constants. Applicable pragmas are:
127 if Ekind (Id) = E_Constant then
128 if Prag_Nam = Name_Part_Of then
131 -- The pragma is not a proper contract item
137 -- Contract items related to [generic] packages or instantiations. The
138 -- applicable pragmas are:
142 -- Part_Of (instantiation only)
144 elsif Ekind_In (Id, E_Generic_Package, E_Package) then
145 if Nam_In (Prag_Nam, Name_Abstract_State,
146 Name_Initial_Condition,
151 -- Indicator Part_Of must be associated with a package instantiation
153 elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
156 -- The pragma is not a proper contract item
162 -- Contract items related to package bodies. The applicable pragmas are:
165 elsif Ekind (Id) = E_Package_Body then
166 if Prag_Nam = Name_Refined_State then
169 -- The pragma is not a proper contract item
175 -- Contract items related to subprogram or entry declarations. The
176 -- applicable pragmas are:
179 -- Extensions_Visible
186 elsif Ekind_In (Id, E_Entry, E_Entry_Family)
187 or else Is_Generic_Subprogram (Id)
188 or else Is_Subprogram (Id)
190 if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
191 Add_Pre_Post_Condition;
193 elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then
194 Add_Contract_Test_Case;
196 elsif Nam_In (Prag_Nam, Name_Depends,
197 Name_Extensions_Visible,
202 elsif Prag_Nam = Name_Volatile_Function
203 and then Ekind_In (Id, E_Function, E_Generic_Function)
207 -- The pragma is not a proper contract item
213 -- Contract items related to subprogram bodies. Applicable pragmas are:
220 elsif Ekind (Id) = E_Subprogram_Body then
221 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
224 elsif Nam_In (Prag_Nam, Name_Postcondition,
228 Add_Pre_Post_Condition;
230 -- The pragma is not a proper contract item
236 -- Contract items related to variables. Applicable pragmas are:
239 -- Constant_After_Elaboration
244 elsif Ekind (Id) = E_Variable then
245 if Nam_In (Prag_Nam, Name_Async_Readers,
247 Name_Constant_After_Elaboration,
248 Name_Effective_Reads,
249 Name_Effective_Writes,
254 -- The pragma is not a proper contract item
260 end Add_Contract_Item;
262 ---------------------------------------------
263 -- Analyze_Enclosing_Package_Body_Contract --
264 ---------------------------------------------
266 procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id) is
270 -- Climb the parent chain looking for an enclosing body. Do not use the
271 -- scope stack, as a body uses the entity of its corresponding spec.
273 Par := Parent (Body_Decl);
274 while Present (Par) loop
275 if Nkind (Par) = N_Package_Body then
276 Analyze_Package_Body_Contract
277 (Body_Id => Defining_Entity (Par),
278 Freeze_Id => Defining_Entity (Body_Decl));
285 end Analyze_Enclosing_Package_Body_Contract;
287 -----------------------------
288 -- Analyze_Object_Contract --
289 -----------------------------
291 procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
292 Obj_Typ : constant Entity_Id := Etype (Obj_Id);
293 AR_Val : Boolean := False;
294 AW_Val : Boolean := False;
295 ER_Val : Boolean := False;
296 EW_Val : Boolean := False;
299 Seen : Boolean := False;
302 -- The loop parameter in an element iterator over a formal container
303 -- is declared with an object declaration, but no contracts apply.
305 if Ekind (Obj_Id) = E_Loop_Parameter then
309 -- Do not analyze a contract multiple times
311 Items := Contract (Obj_Id);
313 if Present (Items) then
314 if Analyzed (Items) then
317 Set_Analyzed (Items);
321 -- Constant-related checks
323 if Ekind (Obj_Id) = E_Constant then
325 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
326 -- This check is relevant only when SPARK_Mode is on, as it is not
327 -- a standard Ada legality rule. Internally-generated constants that
328 -- map generic formals to actuals in instantiations are allowed to
332 and then Comes_From_Source (Obj_Id)
333 and then Is_Effectively_Volatile (Obj_Id)
334 and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
336 Error_Msg_N ("constant cannot be volatile", Obj_Id);
339 -- Variable-related checks
341 else pragma Assert (Ekind (Obj_Id) = E_Variable);
343 -- The following checks are relevant only when SPARK_Mode is on, as
344 -- they are not standard Ada legality rules. Internally generated
345 -- temporaries are ignored.
347 if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
348 if Is_Effectively_Volatile (Obj_Id) then
350 -- The declaration of an effectively volatile object must
351 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
353 if not Is_Library_Level_Entity (Obj_Id) then
355 ("volatile variable & must be declared at library level",
358 -- An object of a discriminated type cannot be effectively
359 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
361 elsif Has_Discriminants (Obj_Typ)
362 and then not Is_Protected_Type (Obj_Typ)
365 ("discriminated object & cannot be volatile", Obj_Id);
367 -- An object of a tagged type cannot be effectively volatile
368 -- (SPARK RM C.6(5)).
370 elsif Is_Tagged_Type (Obj_Typ) then
371 Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
374 -- The object is not effectively volatile
377 -- A non-effectively volatile object cannot have effectively
378 -- volatile components (SPARK RM 7.1.3(6)).
380 if not Is_Effectively_Volatile (Obj_Id)
381 and then Has_Volatile_Component (Obj_Typ)
384 ("non-volatile object & cannot have volatile components",
390 if Is_Ghost_Entity (Obj_Id) then
392 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
394 if Is_Effectively_Volatile (Obj_Id) then
395 Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
397 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
399 elsif Is_Imported (Obj_Id) then
400 Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
402 elsif Is_Exported (Obj_Id) then
403 Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
407 -- Analyze all external properties
409 Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
411 if Present (Prag) then
412 Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
416 Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
418 if Present (Prag) then
419 Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
423 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
425 if Present (Prag) then
426 Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
430 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
432 if Present (Prag) then
433 Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
437 -- Verify the mutual interaction of the various external properties
440 Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
444 -- Check whether the lack of indicator Part_Of agrees with the placement
445 -- of the object with respect to the state space.
447 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
450 Check_Missing_Part_Of (Obj_Id);
453 -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
454 -- exception to this is the object that represents the dispatch table of
455 -- a Ghost tagged type, as the symbol needs to be exported.
457 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
458 if Is_Exported (Obj_Id) then
459 Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
461 elsif Is_Imported (Obj_Id) then
462 Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
465 end Analyze_Object_Contract;
467 -----------------------------------
468 -- Analyze_Package_Body_Contract --
469 -----------------------------------
471 procedure Analyze_Package_Body_Contract
472 (Body_Id : Entity_Id;
473 Freeze_Id : Entity_Id := Empty)
475 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
476 Items : constant Node_Id := Contract (Body_Id);
477 Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
478 Mode : SPARK_Mode_Type;
482 -- Do not analyze a contract multiple times
484 if Present (Items) then
485 if Analyzed (Items) then
488 Set_Analyzed (Items);
492 -- Due to the timing of contract analysis, delayed pragmas may be
493 -- subject to the wrong SPARK_Mode, usually that of the enclosing
494 -- context. To remedy this, restore the original SPARK_Mode of the
495 -- related package body.
497 Save_SPARK_Mode_And_Set (Body_Id, Mode);
499 Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
501 -- The analysis of pragma Refined_State detects whether the spec has
502 -- abstract states available for refinement.
504 if Present (Ref_State) then
505 Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id);
507 -- State refinement is required when the package declaration defines at
508 -- least one abstract state. Null states are not considered. Refinement
509 -- is not enforced when SPARK checks are turned off.
511 elsif SPARK_Mode /= Off
512 and then Requires_State_Refinement (Spec_Id, Body_Id)
514 Error_Msg_N ("package & requires state refinement", Spec_Id);
517 -- Restore the SPARK_Mode of the enclosing context after all delayed
518 -- pragmas have been analyzed.
520 Restore_SPARK_Mode (Mode);
522 -- Capture all global references in a generic package body now that the
523 -- contract has been analyzed.
525 if Is_Generic_Declaration_Or_Body (Body_Decl) then
526 Save_Global_References_In_Contract
527 (Templ => Original_Node (Body_Decl),
530 end Analyze_Package_Body_Contract;
532 ------------------------------
533 -- Analyze_Package_Contract --
534 ------------------------------
536 procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
537 Items : constant Node_Id := Contract (Pack_Id);
538 Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
539 Init : Node_Id := Empty;
540 Init_Cond : Node_Id := Empty;
541 Mode : SPARK_Mode_Type;
546 -- Do not analyze a contract multiple times
548 if Present (Items) then
549 if Analyzed (Items) then
552 Set_Analyzed (Items);
556 -- Due to the timing of contract analysis, delayed pragmas may be
557 -- subject to the wrong SPARK_Mode, usually that of the enclosing
558 -- context. To remedy this, restore the original SPARK_Mode of the
561 Save_SPARK_Mode_And_Set (Pack_Id, Mode);
563 if Present (Items) then
565 -- Locate and store pragmas Initial_Condition and Initializes, since
566 -- their order of analysis matters.
568 Prag := Classifications (Items);
569 while Present (Prag) loop
570 Prag_Nam := Pragma_Name (Prag);
572 if Prag_Nam = Name_Initial_Condition then
575 elsif Prag_Nam = Name_Initializes then
579 Prag := Next_Pragma (Prag);
582 -- Analyze the initialization-related pragmas. Initializes must come
583 -- before Initial_Condition due to item dependencies.
585 if Present (Init) then
586 Analyze_Initializes_In_Decl_Part (Init);
589 if Present (Init_Cond) then
590 Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
594 -- Check whether the lack of indicator Part_Of agrees with the placement
595 -- of the package instantiation with respect to the state space.
597 if Is_Generic_Instance (Pack_Id) then
598 Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
601 Check_Missing_Part_Of (Pack_Id);
605 -- Restore the SPARK_Mode of the enclosing context after all delayed
606 -- pragmas have been analyzed.
608 Restore_SPARK_Mode (Mode);
610 -- Capture all global references in a generic package now that the
611 -- contract has been analyzed.
613 if Is_Generic_Declaration_Or_Body (Pack_Decl) then
614 Save_Global_References_In_Contract
615 (Templ => Original_Node (Pack_Decl),
618 end Analyze_Package_Contract;
620 --------------------------------------
621 -- Analyze_Subprogram_Body_Contract --
622 --------------------------------------
624 procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
625 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
626 Items : constant Node_Id := Contract (Body_Id);
627 Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Body_Decl);
628 Mode : SPARK_Mode_Type;
631 Ref_Depends : Node_Id := Empty;
632 Ref_Global : Node_Id := Empty;
635 -- When a subprogram body declaration is illegal, its defining entity is
636 -- left unanalyzed. There is nothing left to do in this case because the
637 -- body lacks a contract, or even a proper Ekind.
639 if Ekind (Body_Id) = E_Void then
642 -- Do not analyze a contract multiple times
644 elsif Present (Items) then
645 if Analyzed (Items) then
648 Set_Analyzed (Items);
652 -- Due to the timing of contract analysis, delayed pragmas may be
653 -- subject to the wrong SPARK_Mode, usually that of the enclosing
654 -- context. To remedy this, restore the original SPARK_Mode of the
655 -- related subprogram body.
657 Save_SPARK_Mode_And_Set (Body_Id, Mode);
659 -- All subprograms carry a contract, but for some it is not significant
660 -- and should not be processed.
662 if not Has_Significant_Contract (Body_Id) then
665 -- The subprogram body is a completion, analyze all delayed pragmas that
666 -- apply. Note that when the body is stand-alone, the pragmas are always
667 -- analyzed on the spot.
669 elsif Present (Items) then
671 -- Locate and store pragmas Refined_Depends and Refined_Global, since
672 -- their order of analysis matters.
674 Prag := Classifications (Items);
675 while Present (Prag) loop
676 Prag_Nam := Pragma_Name (Prag);
678 if Prag_Nam = Name_Refined_Depends then
681 elsif Prag_Nam = Name_Refined_Global then
685 Prag := Next_Pragma (Prag);
688 -- Analyze Refined_Global first, as Refined_Depends may mention items
689 -- classified in the global refinement.
691 if Present (Ref_Global) then
692 Analyze_Refined_Global_In_Decl_Part (Ref_Global);
695 -- Refined_Depends must be analyzed after Refined_Global in order to
696 -- see the modes of all global refinements.
698 if Present (Ref_Depends) then
699 Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
703 -- Ensure that the contract cases or postconditions mention 'Result or
704 -- define a post-state.
706 Check_Result_And_Post_State (Body_Id);
708 -- A stand-alone nonvolatile function body cannot have an effectively
709 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
710 -- check is relevant only when SPARK_Mode is on, as it is not a standard
711 -- legality rule. The check is performed here because Volatile_Function
712 -- is processed after the analysis of the related subprogram body.
715 and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
716 and then not Is_Volatile_Function (Body_Id)
718 Check_Nonvolatile_Function_Profile (Body_Id);
721 -- Restore the SPARK_Mode of the enclosing context after all delayed
722 -- pragmas have been analyzed.
724 Restore_SPARK_Mode (Mode);
726 -- Capture all global references in a generic subprogram body now that
727 -- the contract has been analyzed.
729 if Is_Generic_Declaration_Or_Body (Body_Decl) then
730 Save_Global_References_In_Contract
731 (Templ => Original_Node (Body_Decl),
735 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
736 -- invariants and predicates associated with body and its spec. Do not
737 -- expand the contract of subprogram body stubs.
739 if Nkind (Body_Decl) = N_Subprogram_Body then
740 Expand_Subprogram_Contract (Body_Id);
742 end Analyze_Subprogram_Body_Contract;
744 ---------------------------------
745 -- Analyze_Subprogram_Contract --
746 ---------------------------------
748 procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
749 Items : constant Node_Id := Contract (Subp_Id);
750 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
751 Depends : Node_Id := Empty;
752 Global : Node_Id := Empty;
753 Mode : SPARK_Mode_Type;
758 -- Do not analyze a contract multiple times
760 if Present (Items) then
761 if Analyzed (Items) then
764 Set_Analyzed (Items);
768 -- Due to the timing of contract analysis, delayed pragmas may be
769 -- subject to the wrong SPARK_Mode, usually that of the enclosing
770 -- context. To remedy this, restore the original SPARK_Mode of the
771 -- related subprogram body.
773 Save_SPARK_Mode_And_Set (Subp_Id, Mode);
775 -- All subprograms carry a contract, but for some it is not significant
776 -- and should not be processed.
778 if not Has_Significant_Contract (Subp_Id) then
781 elsif Present (Items) then
783 -- Analyze pre- and postconditions
785 Prag := Pre_Post_Conditions (Items);
786 while Present (Prag) loop
787 Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
788 Prag := Next_Pragma (Prag);
791 -- Analyze contract-cases and test-cases
793 Prag := Contract_Test_Cases (Items);
794 while Present (Prag) loop
795 Prag_Nam := Pragma_Name (Prag);
797 if Prag_Nam = Name_Contract_Cases then
798 Analyze_Contract_Cases_In_Decl_Part (Prag);
800 pragma Assert (Prag_Nam = Name_Test_Case);
801 Analyze_Test_Case_In_Decl_Part (Prag);
804 Prag := Next_Pragma (Prag);
807 -- Analyze classification pragmas
809 Prag := Classifications (Items);
810 while Present (Prag) loop
811 Prag_Nam := Pragma_Name (Prag);
813 if Prag_Nam = Name_Depends then
816 elsif Prag_Nam = Name_Global then
820 Prag := Next_Pragma (Prag);
823 -- Analyze Global first, as Depends may mention items classified in
824 -- the global categorization.
826 if Present (Global) then
827 Analyze_Global_In_Decl_Part (Global);
830 -- Depends must be analyzed after Global in order to see the modes of
833 if Present (Depends) then
834 Analyze_Depends_In_Decl_Part (Depends);
837 -- Ensure that the contract cases or postconditions mention 'Result
838 -- or define a post-state.
840 Check_Result_And_Post_State (Subp_Id);
843 -- A nonvolatile function cannot have an effectively volatile formal
844 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
845 -- only when SPARK_Mode is on, as it is not a standard legality rule.
846 -- The check is performed here because pragma Volatile_Function is
847 -- processed after the analysis of the related subprogram declaration.
850 and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
851 and then not Is_Volatile_Function (Subp_Id)
853 Check_Nonvolatile_Function_Profile (Subp_Id);
856 -- Restore the SPARK_Mode of the enclosing context after all delayed
857 -- pragmas have been analyzed.
859 Restore_SPARK_Mode (Mode);
861 -- Capture all global references in a generic subprogram now that the
862 -- contract has been analyzed.
864 if Is_Generic_Declaration_Or_Body (Subp_Decl) then
865 Save_Global_References_In_Contract
866 (Templ => Original_Node (Subp_Decl),
869 end Analyze_Subprogram_Contract;
871 -------------------------------------------
872 -- Analyze_Subprogram_Body_Stub_Contract --
873 -------------------------------------------
875 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
876 Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
877 Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
880 -- A subprogram body stub may act as its own spec or as the completion
881 -- of a previous declaration. Depending on the context, the contract of
882 -- the stub may contain two sets of pragmas.
884 -- The stub is a completion, the applicable pragmas are:
888 if Present (Spec_Id) then
889 Analyze_Subprogram_Body_Contract (Stub_Id);
891 -- The stub acts as its own spec, the applicable pragmas are:
900 Analyze_Subprogram_Contract (Stub_Id);
902 end Analyze_Subprogram_Body_Stub_Contract;
904 -----------------------------
905 -- Create_Generic_Contract --
906 -----------------------------
908 procedure Create_Generic_Contract (Unit : Node_Id) is
909 Templ : constant Node_Id := Original_Node (Unit);
910 Templ_Id : constant Entity_Id := Defining_Entity (Templ);
912 procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
913 -- Add a single contract-related source pragma Prag to the contract of
914 -- generic template Templ_Id.
916 ---------------------------------
917 -- Add_Generic_Contract_Pragma --
918 ---------------------------------
920 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
921 Prag_Templ : Node_Id;
924 -- Mark the pragma to prevent the premature capture of global
925 -- references when capturing global references of the context
926 -- (see Save_References_In_Pragma).
928 Set_Is_Generic_Contract_Pragma (Prag);
930 -- Pragmas that apply to a generic subprogram declaration are not
931 -- part of the semantic structure of the generic template:
934 -- procedure Example (Formal : Integer);
935 -- pragma Precondition (Formal > 0);
937 -- Create a generic template for such pragmas and link the template
938 -- of the pragma with the generic template.
940 if Nkind (Templ) = N_Generic_Subprogram_Declaration then
942 (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
943 Prag_Templ := Original_Node (Prag);
945 Set_Is_Generic_Contract_Pragma (Prag_Templ);
946 Add_Contract_Item (Prag_Templ, Templ_Id);
948 -- Otherwise link the pragma with the generic template
951 Add_Contract_Item (Prag, Templ_Id);
953 end Add_Generic_Contract_Pragma;
957 Context : constant Node_Id := Parent (Unit);
958 Decl : Node_Id := Empty;
960 -- Start of processing for Create_Generic_Contract
963 -- A generic package declaration carries contract-related source pragmas
964 -- in its visible declarations.
966 if Nkind (Templ) = N_Generic_Package_Declaration then
967 Set_Ekind (Templ_Id, E_Generic_Package);
969 if Present (Visible_Declarations (Specification (Templ))) then
970 Decl := First (Visible_Declarations (Specification (Templ)));
973 -- A generic package body carries contract-related source pragmas in its
976 elsif Nkind (Templ) = N_Package_Body then
977 Set_Ekind (Templ_Id, E_Package_Body);
979 if Present (Declarations (Templ)) then
980 Decl := First (Declarations (Templ));
983 -- Generic subprogram declaration
985 elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
986 if Nkind (Specification (Templ)) = N_Function_Specification then
987 Set_Ekind (Templ_Id, E_Generic_Function);
989 Set_Ekind (Templ_Id, E_Generic_Procedure);
992 -- When the generic subprogram acts as a compilation unit, inspect
993 -- the Pragmas_After list for contract-related source pragmas.
995 if Nkind (Context) = N_Compilation_Unit then
996 if Present (Aux_Decls_Node (Context))
997 and then Present (Pragmas_After (Aux_Decls_Node (Context)))
999 Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
1002 -- Otherwise inspect the successive declarations for contract-related
1006 Decl := Next (Unit);
1009 -- A generic subprogram body carries contract-related source pragmas in
1010 -- its declarations.
1012 elsif Nkind (Templ) = N_Subprogram_Body then
1013 Set_Ekind (Templ_Id, E_Subprogram_Body);
1015 if Present (Declarations (Templ)) then
1016 Decl := First (Declarations (Templ));
1020 -- Inspect the relevant declarations looking for contract-related source
1021 -- pragmas and add them to the contract of the generic unit.
1023 while Present (Decl) loop
1024 if Comes_From_Source (Decl) then
1025 if Nkind (Decl) = N_Pragma then
1027 -- The source pragma is a contract annotation
1029 if Is_Contract_Annotation (Decl) then
1030 Add_Generic_Contract_Pragma (Decl);
1033 -- The region where a contract-related source pragma may appear
1034 -- ends with the first source non-pragma declaration or statement.
1043 end Create_Generic_Contract;
1045 --------------------------------
1046 -- Expand_Subprogram_Contract --
1047 --------------------------------
1049 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is
1050 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
1051 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
1053 procedure Add_Invariant_And_Predicate_Checks
1054 (Subp_Id : Entity_Id;
1055 Stmts : in out List_Id;
1056 Result : out Node_Id);
1057 -- Process the result of function Subp_Id (if applicable) and all its
1058 -- formals. Add invariant and predicate checks where applicable. The
1059 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1060 -- function, Result contains the entity of parameter _Result, to be
1061 -- used in the creation of procedure _Postconditions.
1063 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
1064 -- Append a node to a list. If there is no list, create a new one. When
1065 -- the item denotes a pragma, it is added to the list only when it is
1068 procedure Build_Postconditions_Procedure
1069 (Subp_Id : Entity_Id;
1071 Result : Entity_Id);
1072 -- Create the body of procedure _Postconditions which handles various
1073 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1074 -- of statements to be checked on exit. Parameter Result is the entity
1075 -- of parameter _Result when Subp_Id denotes a function.
1077 function Build_Pragma_Check_Equivalent
1079 Subp_Id : Entity_Id := Empty;
1080 Inher_Id : Entity_Id := Empty) return Node_Id;
1081 -- Transform a [refined] pre- or postcondition denoted by Prag into an
1082 -- equivalent pragma Check. When the pre- or postcondition is inherited,
1083 -- the routine corrects the references of all formals of Inher_Id to
1084 -- point to the formals of Subp_Id.
1086 procedure Process_Contract_Cases (Stmts : in out List_Id);
1087 -- Process pragma Contract_Cases. This routine prepends items to the
1088 -- body declarations and appends items to list Stmts.
1090 procedure Process_Postconditions (Stmts : in out List_Id);
1091 -- Collect all [inherited] spec and body postconditions and accumulate
1092 -- their pragma Check equivalents in list Stmts.
1094 procedure Process_Preconditions;
1095 -- Collect all [inherited] spec and body preconditions and prepend their
1096 -- pragma Check equivalents to the declarations of the body.
1098 ----------------------------------------
1099 -- Add_Invariant_And_Predicate_Checks --
1100 ----------------------------------------
1102 procedure Add_Invariant_And_Predicate_Checks
1103 (Subp_Id : Entity_Id;
1104 Stmts : in out List_Id;
1105 Result : out Node_Id)
1107 procedure Add_Invariant_Access_Checks (Id : Entity_Id);
1108 -- Id denotes the return value of a function or a formal parameter.
1109 -- Add an invariant check if the type of Id is access to a type with
1110 -- invariants. The routine appends the generated code to Stmts.
1112 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
1113 -- Determine whether type Typ can benefit from invariant checks. To
1114 -- qualify, the type must have a non-null invariant procedure and
1115 -- subprogram Subp_Id must appear visible from the point of view of
1118 ---------------------------------
1119 -- Add_Invariant_Access_Checks --
1120 ---------------------------------
1122 procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
1123 Loc : constant Source_Ptr := Sloc (Body_Decl);
1130 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
1131 Typ := Designated_Type (Typ);
1133 if Invariant_Checks_OK (Typ) then
1135 Make_Explicit_Dereference (Loc,
1136 Prefix => New_Occurrence_Of (Id, Loc));
1137 Set_Etype (Ref, Typ);
1140 -- if <Id> /= null then
1141 -- <invariant_call (<Ref>)>
1146 Make_If_Statement (Loc,
1149 Left_Opnd => New_Occurrence_Of (Id, Loc),
1150 Right_Opnd => Make_Null (Loc)),
1151 Then_Statements => New_List (
1152 Make_Invariant_Call (Ref))),
1156 end Add_Invariant_Access_Checks;
1158 -------------------------
1159 -- Invariant_Checks_OK --
1160 -------------------------
1162 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
1163 function Has_Null_Body (Proc_Id : Entity_Id) return Boolean;
1164 -- Determine whether the body of procedure Proc_Id contains a sole
1165 -- null statement, possibly followed by an optional return.
1167 function Has_Public_Visibility_Of_Subprogram return Boolean;
1168 -- Determine whether type Typ has public visibility of subprogram
1175 function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is
1176 Body_Id : Entity_Id;
1183 Spec := Parent (Proc_Id);
1184 Decl := Parent (Spec);
1186 -- Retrieve the entity of the invariant procedure body
1188 if Nkind (Spec) = N_Procedure_Specification
1189 and then Nkind (Decl) = N_Subprogram_Declaration
1191 Body_Id := Corresponding_Body (Decl);
1193 -- The body acts as a spec
1199 -- The body will be generated later
1201 if No (Body_Id) then
1205 Spec := Parent (Body_Id);
1206 Decl := Parent (Spec);
1209 (Nkind (Spec) = N_Procedure_Specification
1210 and then Nkind (Decl) = N_Subprogram_Body);
1212 Stmt1 := First (Statements (Handled_Statement_Sequence (Decl)));
1214 -- Look for a null statement followed by an optional return
1217 if Nkind (Stmt1) = N_Null_Statement then
1218 Stmt2 := Next (Stmt1);
1220 if Present (Stmt2) then
1221 return Nkind (Stmt2) = N_Simple_Return_Statement;
1230 -----------------------------------------
1231 -- Has_Public_Visibility_Of_Subprogram --
1232 -----------------------------------------
1234 function Has_Public_Visibility_Of_Subprogram return Boolean is
1235 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
1238 -- An Initialization procedure must be considered visible even
1239 -- though it is internally generated.
1241 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
1244 elsif Ekind (Scope (Typ)) /= E_Package then
1247 -- Internally generated code is never publicly visible except
1248 -- for a subprogram that is the implementation of an expression
1249 -- function. In that case the visibility is determined by the
1252 elsif not Comes_From_Source (Subp_Decl)
1254 (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
1256 Comes_From_Source (Defining_Entity (Subp_Decl)))
1260 -- Determine whether the subprogram is declared in the visible
1261 -- declarations of the package containing the type.
1264 return List_Containing (Subp_Decl) =
1265 Visible_Declarations
1266 (Specification (Unit_Declaration_Node (Scope (Typ))));
1268 end Has_Public_Visibility_Of_Subprogram;
1270 -- Start of processing for Invariant_Checks_OK
1274 Has_Invariants (Typ)
1275 and then Present (Invariant_Procedure (Typ))
1276 and then not Has_Null_Body (Invariant_Procedure (Typ))
1277 and then Has_Public_Visibility_Of_Subprogram;
1278 end Invariant_Checks_OK;
1282 Loc : constant Source_Ptr := Sloc (Body_Decl);
1283 -- Source location of subprogram body contract
1288 -- Start of processing for Add_Invariant_And_Predicate_Checks
1293 -- Process the result of a function
1295 if Ekind (Subp_Id) = E_Function then
1296 Typ := Etype (Subp_Id);
1298 -- Generate _Result which is used in procedure _Postconditions to
1299 -- verify the return value.
1301 Result := Make_Defining_Identifier (Loc, Name_uResult);
1302 Set_Etype (Result, Typ);
1304 -- Add an invariant check when the return type has invariants and
1305 -- the related function is visible to the outside.
1307 if Invariant_Checks_OK (Typ) then
1310 Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
1314 -- Add an invariant check when the return type is an access to a
1315 -- type with invariants.
1317 Add_Invariant_Access_Checks (Result);
1320 -- Add invariant and predicates for all formals that qualify
1322 Formal := First_Formal (Subp_Id);
1323 while Present (Formal) loop
1324 Typ := Etype (Formal);
1326 if Ekind (Formal) /= E_In_Parameter
1327 or else Is_Access_Type (Typ)
1329 if Invariant_Checks_OK (Typ) then
1332 Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
1336 Add_Invariant_Access_Checks (Formal);
1338 -- Note: we used to add predicate checks for OUT and IN OUT
1339 -- formals here, but that was misguided, since such checks are
1340 -- performed on the caller side, based on the predicate of the
1341 -- actual, rather than the predicate of the formal.
1345 Next_Formal (Formal);
1347 end Add_Invariant_And_Predicate_Checks;
1349 -------------------------
1350 -- Append_Enabled_Item --
1351 -------------------------
1353 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
1355 -- Do not chain ignored or disabled pragmas
1357 if Nkind (Item) = N_Pragma
1358 and then (Is_Ignored (Item) or else Is_Disabled (Item))
1362 -- Otherwise, add the item
1369 -- If the pragma is a conjunct in a composite postcondition, it
1370 -- has been processed in reverse order. In the postcondition body
1371 -- it must appear before the others.
1373 if Nkind (Item) = N_Pragma
1374 and then From_Aspect_Specification (Item)
1375 and then Split_PPC (Item)
1377 Prepend (Item, List);
1379 Append (Item, List);
1382 end Append_Enabled_Item;
1384 ------------------------------------
1385 -- Build_Postconditions_Procedure --
1386 ------------------------------------
1388 procedure Build_Postconditions_Procedure
1389 (Subp_Id : Entity_Id;
1393 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
1394 -- Insert node Stmt before the first source declaration of the
1395 -- related subprogram's body. If no such declaration exists, Stmt
1396 -- becomes the last declaration.
1398 --------------------------------------------
1399 -- Insert_Before_First_Source_Declaration --
1400 --------------------------------------------
1402 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
1403 Decls : constant List_Id := Declarations (Body_Decl);
1407 -- Inspect the declarations of the related subprogram body looking
1408 -- for the first source declaration.
1410 if Present (Decls) then
1411 Decl := First (Decls);
1412 while Present (Decl) loop
1413 if Comes_From_Source (Decl) then
1414 Insert_Before (Decl, Stmt);
1421 -- If we get there, then the subprogram body lacks any source
1422 -- declarations. The body of _Postconditions now acts as the
1423 -- last declaration.
1425 Append (Stmt, Decls);
1427 -- Ensure that the body has a declaration list
1430 Set_Declarations (Body_Decl, New_List (Stmt));
1432 end Insert_Before_First_Source_Declaration;
1436 Loc : constant Source_Ptr := Sloc (Body_Decl);
1437 Params : List_Id := No_List;
1439 Proc_Id : Entity_Id;
1441 -- Start of processing for Build_Postconditions_Procedure
1444 -- Nothing to do if there are no actions to check on exit
1450 Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
1451 Set_Debug_Info_Needed (Proc_Id);
1452 Set_Postconditions_Proc (Subp_Id, Proc_Id);
1454 -- The related subprogram is a function: create the specification of
1455 -- parameter _Result.
1457 if Present (Result) then
1458 Params := New_List (
1459 Make_Parameter_Specification (Loc,
1460 Defining_Identifier => Result,
1462 New_Occurrence_Of (Etype (Result), Loc)));
1465 -- Insert _Postconditions before the first source declaration of the
1466 -- body. This ensures that the body will not cause any premature
1467 -- freezing, as it may mention types:
1469 -- procedure Proc (Obj : Array_Typ) is
1470 -- procedure _postconditions is
1473 -- end _postconditions;
1475 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
1478 -- In the example above, Obj is of type T but the incorrect placement
1479 -- of _Postconditions will cause a crash in gigi due to an out-of-
1480 -- order reference. The body of _Postconditions must be placed after
1481 -- the declaration of Temp to preserve correct visibility.
1483 -- Set an explicit End_Label to override the sloc of the implicit
1484 -- RETURN statement, and prevent it from inheriting the sloc of one
1485 -- the postconditions: this would cause confusing debug info to be
1486 -- produced, interfering with coverage-analysis tools.
1489 Make_Subprogram_Body (Loc,
1491 Make_Procedure_Specification (Loc,
1492 Defining_Unit_Name => Proc_Id,
1493 Parameter_Specifications => Params),
1495 Declarations => Empty_List,
1496 Handled_Statement_Sequence =>
1497 Make_Handled_Sequence_Of_Statements (Loc,
1498 Statements => Stmts,
1499 End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
1501 Insert_Before_First_Source_Declaration (Proc_Bod);
1503 end Build_Postconditions_Procedure;
1505 -----------------------------------
1506 -- Build_Pragma_Check_Equivalent --
1507 -----------------------------------
1509 function Build_Pragma_Check_Equivalent
1511 Subp_Id : Entity_Id := Empty;
1512 Inher_Id : Entity_Id := Empty) return Node_Id
1514 function Suppress_Reference (N : Node_Id) return Traverse_Result;
1515 -- Detect whether node N references a formal parameter subject to
1516 -- pragma Unreferenced. If this is the case, set Comes_From_Source
1517 -- to False to suppress the generation of a reference when analyzing
1520 ------------------------
1521 -- Suppress_Reference --
1522 ------------------------
1524 function Suppress_Reference (N : Node_Id) return Traverse_Result is
1528 if Is_Entity_Name (N) and then Present (Entity (N)) then
1529 Formal := Entity (N);
1531 -- The formal parameter is subject to pragma Unreferenced.
1532 -- Prevent the generation of a reference by resetting the
1533 -- Comes_From_Source flag.
1535 if Is_Formal (Formal)
1536 and then Has_Pragma_Unreferenced (Formal)
1538 Set_Comes_From_Source (N, False);
1543 end Suppress_Reference;
1545 procedure Suppress_References is
1546 new Traverse_Proc (Suppress_Reference);
1550 Loc : constant Source_Ptr := Sloc (Prag);
1551 Prag_Nam : constant Name_Id := Pragma_Name (Prag);
1552 Check_Prag : Node_Id;
1553 Formals_Map : Elist_Id;
1554 Inher_Formal : Entity_Id;
1557 Subp_Formal : Entity_Id;
1559 -- Start of processing for Build_Pragma_Check_Equivalent
1562 Formals_Map := No_Elist;
1564 -- When the pre- or postcondition is inherited, map the formals of
1565 -- the inherited subprogram to those of the current subprogram.
1567 if Present (Inher_Id) then
1568 pragma Assert (Present (Subp_Id));
1570 Formals_Map := New_Elmt_List;
1572 -- Create a relation <inherited formal> => <subprogram formal>
1574 Inher_Formal := First_Formal (Inher_Id);
1575 Subp_Formal := First_Formal (Subp_Id);
1576 while Present (Inher_Formal) and then Present (Subp_Formal) loop
1577 Append_Elmt (Inher_Formal, Formals_Map);
1578 Append_Elmt (Subp_Formal, Formals_Map);
1580 Next_Formal (Inher_Formal);
1581 Next_Formal (Subp_Formal);
1585 -- Copy the original pragma while performing substitutions (if
1592 New_Scope => Current_Scope);
1594 -- Mark the pragma as being internally generated and reset the
1597 Set_Analyzed (Check_Prag, False);
1598 Set_Comes_From_Source (Check_Prag, False);
1600 -- The tree of the original pragma may contain references to the
1601 -- formal parameters of the related subprogram. At the same time
1602 -- the corresponding body may mark the formals as unreferenced:
1604 -- procedure Proc (Formal : ...)
1605 -- with Pre => Formal ...;
1607 -- procedure Proc (Formal : ...) is
1608 -- pragma Unreferenced (Formal);
1611 -- This creates problems because all pragma Check equivalents are
1612 -- analyzed at the end of the body declarations. Since all source
1613 -- references have already been accounted for, reset any references
1614 -- to such formals in the generated pragma Check equivalent.
1616 Suppress_References (Check_Prag);
1618 if Present (Corresponding_Aspect (Prag)) then
1619 Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
1624 -- Convert the copy into pragma Check by correcting the name and
1625 -- adding a check_kind argument.
1627 Set_Pragma_Identifier
1628 (Check_Prag, Make_Identifier (Loc, Name_Check));
1630 Prepend_To (Pragma_Argument_Associations (Check_Prag),
1631 Make_Pragma_Argument_Association (Loc,
1632 Expression => Make_Identifier (Loc, Nam)));
1634 -- Update the error message when the pragma is inherited
1636 if Present (Inher_Id) then
1637 Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag));
1639 if Chars (Msg_Arg) = Name_Message then
1640 String_To_Name_Buffer (Strval (Expression (Msg_Arg)));
1642 -- Insert "inherited" to improve the error message
1644 if Name_Buffer (1 .. 8) = "failed p" then
1645 Insert_Str_In_Name_Buffer ("inherited ", 8);
1646 Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer);
1652 end Build_Pragma_Check_Equivalent;
1654 ----------------------------
1655 -- Process_Contract_Cases --
1656 ----------------------------
1658 procedure Process_Contract_Cases (Stmts : in out List_Id) is
1659 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
1660 -- Process pragma Contract_Cases for subprogram Subp_Id
1662 --------------------------------
1663 -- Process_Contract_Cases_For --
1664 --------------------------------
1666 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
1667 Items : constant Node_Id := Contract (Subp_Id);
1671 if Present (Items) then
1672 Prag := Contract_Test_Cases (Items);
1673 while Present (Prag) loop
1674 if Pragma_Name (Prag) = Name_Contract_Cases then
1675 Expand_Pragma_Contract_Cases
1678 Decls => Declarations (Body_Decl),
1682 Prag := Next_Pragma (Prag);
1685 end Process_Contract_Cases_For;
1687 -- Start of processing for Process_Contract_Cases
1690 Process_Contract_Cases_For (Body_Id);
1692 if Present (Spec_Id) then
1693 Process_Contract_Cases_For (Spec_Id);
1695 end Process_Contract_Cases;
1697 ----------------------------
1698 -- Process_Postconditions --
1699 ----------------------------
1701 procedure Process_Postconditions (Stmts : in out List_Id) is
1702 procedure Process_Body_Postconditions (Post_Nam : Name_Id);
1703 -- Collect all [refined] postconditions of a specific kind denoted
1704 -- by Post_Nam that belong to the body, and generate pragma Check
1705 -- equivalents in list Stmts.
1707 procedure Process_Spec_Postconditions;
1708 -- Collect all [inherited] postconditions of the spec, and generate
1709 -- pragma Check equivalents in list Stmts.
1711 ---------------------------------
1712 -- Process_Body_Postconditions --
1713 ---------------------------------
1715 procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
1716 Items : constant Node_Id := Contract (Body_Id);
1717 Unit_Decl : constant Node_Id := Parent (Body_Decl);
1722 -- Process the contract
1724 if Present (Items) then
1725 Prag := Pre_Post_Conditions (Items);
1726 while Present (Prag) loop
1727 if Pragma_Name (Prag) = Post_Nam then
1729 (Item => Build_Pragma_Check_Equivalent (Prag),
1733 Prag := Next_Pragma (Prag);
1737 -- The subprogram body being processed is actually the proper body
1738 -- of a stub with a corresponding spec. The subprogram stub may
1739 -- carry a postcondition pragma, in which case it must be taken
1740 -- into account. The pragma appears after the stub.
1742 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
1743 Decl := Next (Corresponding_Stub (Unit_Decl));
1744 while Present (Decl) loop
1746 -- Note that non-matching pragmas are skipped
1748 if Nkind (Decl) = N_Pragma then
1749 if Pragma_Name (Decl) = Post_Nam then
1751 (Item => Build_Pragma_Check_Equivalent (Decl),
1755 -- Skip internally generated code
1757 elsif not Comes_From_Source (Decl) then
1760 -- Postcondition pragmas are usually grouped together. There
1761 -- is no need to inspect the whole declarative list.
1770 end Process_Body_Postconditions;
1772 ---------------------------------
1773 -- Process_Spec_Postconditions --
1774 ---------------------------------
1776 procedure Process_Spec_Postconditions is
1777 Subps : constant Subprogram_List :=
1778 Inherited_Subprograms (Spec_Id);
1781 Subp_Id : Entity_Id;
1784 -- Process the contract
1786 Items := Contract (Spec_Id);
1788 if Present (Items) then
1789 Prag := Pre_Post_Conditions (Items);
1790 while Present (Prag) loop
1791 if Pragma_Name (Prag) = Name_Postcondition then
1793 (Item => Build_Pragma_Check_Equivalent (Prag),
1797 Prag := Next_Pragma (Prag);
1801 -- Process the contracts of all inherited subprograms, looking for
1802 -- class-wide postconditions.
1804 for Index in Subps'Range loop
1805 Subp_Id := Subps (Index);
1806 Items := Contract (Subp_Id);
1808 if Present (Items) then
1809 Prag := Pre_Post_Conditions (Items);
1810 while Present (Prag) loop
1811 if Pragma_Name (Prag) = Name_Postcondition
1812 and then Class_Present (Prag)
1816 Build_Pragma_Check_Equivalent
1819 Inher_Id => Subp_Id),
1823 Prag := Next_Pragma (Prag);
1827 end Process_Spec_Postconditions;
1829 -- Start of processing for Process_Postconditions
1832 -- The processing of postconditions is done in reverse order (body
1833 -- first) to ensure the following arrangement:
1835 -- <refined postconditions from body>
1836 -- <postconditions from body>
1837 -- <postconditions from spec>
1838 -- <inherited postconditions>
1840 Process_Body_Postconditions (Name_Refined_Post);
1841 Process_Body_Postconditions (Name_Postcondition);
1843 if Present (Spec_Id) then
1844 Process_Spec_Postconditions;
1846 end Process_Postconditions;
1848 ---------------------------
1849 -- Process_Preconditions --
1850 ---------------------------
1852 procedure Process_Preconditions is
1853 Class_Pre : Node_Id := Empty;
1854 -- The sole [inherited] class-wide precondition pragma that applies
1855 -- to the subprogram.
1857 Insert_Node : Node_Id := Empty;
1858 -- The insertion node after which all pragma Check equivalents are
1861 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
1862 -- Merge two class-wide preconditions by "or else"-ing them. The
1863 -- changes are accumulated in parameter Into. Update the error
1866 procedure Prepend_To_Decls (Item : Node_Id);
1867 -- Prepend a single item to the declarations of the subprogram body
1869 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
1870 -- Save a class-wide precondition into Class_Pre, or prepend a normal
1871 -- precondition to the declarations of the body and analyze it.
1873 procedure Process_Inherited_Preconditions;
1874 -- Collect all inherited class-wide preconditions and merge them into
1875 -- one big precondition to be evaluated as pragma Check.
1877 procedure Process_Preconditions_For (Subp_Id : Entity_Id);
1878 -- Collect all preconditions of subprogram Subp_Id and prepend their
1879 -- pragma Check equivalents to the declarations of the body.
1881 -------------------------
1882 -- Merge_Preconditions --
1883 -------------------------
1885 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
1886 function Expression_Arg (Prag : Node_Id) return Node_Id;
1887 -- Return the boolean expression argument of a precondition while
1888 -- updating its parentheses count for the subsequent merge.
1890 function Message_Arg (Prag : Node_Id) return Node_Id;
1891 -- Return the message argument of a precondition
1893 --------------------
1894 -- Expression_Arg --
1895 --------------------
1897 function Expression_Arg (Prag : Node_Id) return Node_Id is
1898 Args : constant List_Id := Pragma_Argument_Associations (Prag);
1899 Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
1902 if Paren_Count (Arg) = 0 then
1903 Set_Paren_Count (Arg, 1);
1913 function Message_Arg (Prag : Node_Id) return Node_Id is
1914 Args : constant List_Id := Pragma_Argument_Associations (Prag);
1916 return Get_Pragma_Arg (Last (Args));
1921 From_Expr : constant Node_Id := Expression_Arg (From);
1922 From_Msg : constant Node_Id := Message_Arg (From);
1923 Into_Expr : constant Node_Id := Expression_Arg (Into);
1924 Into_Msg : constant Node_Id := Message_Arg (Into);
1925 Loc : constant Source_Ptr := Sloc (Into);
1927 -- Start of processing for Merge_Preconditions
1930 -- Merge the two preconditions by "or else"-ing them
1934 Right_Opnd => Relocate_Node (Into_Expr),
1935 Left_Opnd => From_Expr));
1937 -- Merge the two error messages to produce a single message of the
1940 -- failed precondition from ...
1941 -- also failed inherited precondition from ...
1943 if not Exception_Locations_Suppressed then
1944 Start_String (Strval (Into_Msg));
1945 Store_String_Char (ASCII.LF);
1946 Store_String_Chars (" also ");
1947 Store_String_Chars (Strval (From_Msg));
1949 Set_Strval (Into_Msg, End_String);
1951 end Merge_Preconditions;
1953 ----------------------
1954 -- Prepend_To_Decls --
1955 ----------------------
1957 procedure Prepend_To_Decls (Item : Node_Id) is
1958 Decls : List_Id := Declarations (Body_Decl);
1961 -- Ensure that the body has a declarative list
1965 Set_Declarations (Body_Decl, Decls);
1968 Prepend_To (Decls, Item);
1969 end Prepend_To_Decls;
1971 ------------------------------
1972 -- Prepend_To_Decls_Or_Save --
1973 ------------------------------
1975 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
1976 Check_Prag : Node_Id;
1979 Check_Prag := Build_Pragma_Check_Equivalent (Prag);
1981 -- Save the sole class-wide precondition (if any) for the next
1982 -- step, where it will be merged with inherited preconditions.
1984 if Class_Present (Prag) then
1985 pragma Assert (No (Class_Pre));
1986 Class_Pre := Check_Prag;
1988 -- Accumulate the corresponding Check pragmas at the top of the
1989 -- declarations. Prepending the items ensures that they will be
1990 -- evaluated in their original order.
1993 if Present (Insert_Node) then
1994 Insert_After (Insert_Node, Check_Prag);
1996 Prepend_To_Decls (Check_Prag);
1999 Analyze (Check_Prag);
2001 end Prepend_To_Decls_Or_Save;
2003 -------------------------------------
2004 -- Process_Inherited_Preconditions --
2005 -------------------------------------
2007 procedure Process_Inherited_Preconditions is
2008 Subps : constant Subprogram_List :=
2009 Inherited_Subprograms (Spec_Id);
2010 Check_Prag : Node_Id;
2013 Subp_Id : Entity_Id;
2016 -- Process the contracts of all inherited subprograms, looking for
2017 -- class-wide preconditions.
2019 for Index in Subps'Range loop
2020 Subp_Id := Subps (Index);
2021 Items := Contract (Subp_Id);
2023 if Present (Items) then
2024 Prag := Pre_Post_Conditions (Items);
2025 while Present (Prag) loop
2026 if Pragma_Name (Prag) = Name_Precondition
2027 and then Class_Present (Prag)
2030 Build_Pragma_Check_Equivalent
2033 Inher_Id => Subp_Id);
2035 -- The spec of an inherited subprogram already yielded
2036 -- a class-wide precondition. Merge the existing
2037 -- precondition with the current one using "or else".
2039 if Present (Class_Pre) then
2040 Merge_Preconditions (Check_Prag, Class_Pre);
2042 Class_Pre := Check_Prag;
2046 Prag := Next_Pragma (Prag);
2051 -- Add the merged class-wide preconditions
2053 if Present (Class_Pre) then
2054 Prepend_To_Decls (Class_Pre);
2055 Analyze (Class_Pre);
2057 end Process_Inherited_Preconditions;
2059 -------------------------------
2060 -- Process_Preconditions_For --
2061 -------------------------------
2063 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
2064 Items : constant Node_Id := Contract (Subp_Id);
2067 Subp_Decl : Node_Id;
2070 -- Process the contract
2072 if Present (Items) then
2073 Prag := Pre_Post_Conditions (Items);
2074 while Present (Prag) loop
2075 if Pragma_Name (Prag) = Name_Precondition then
2076 Prepend_To_Decls_Or_Save (Prag);
2079 Prag := Next_Pragma (Prag);
2083 -- The subprogram declaration being processed is actually a body
2084 -- stub. The stub may carry a precondition pragma, in which case
2085 -- it must be taken into account. The pragma appears after the
2088 Subp_Decl := Unit_Declaration_Node (Subp_Id);
2090 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
2092 -- Inspect the declarations following the body stub
2094 Decl := Next (Subp_Decl);
2095 while Present (Decl) loop
2097 -- Note that non-matching pragmas are skipped
2099 if Nkind (Decl) = N_Pragma then
2100 if Pragma_Name (Decl) = Name_Precondition then
2101 Prepend_To_Decls_Or_Save (Decl);
2104 -- Skip internally generated code
2106 elsif not Comes_From_Source (Decl) then
2109 -- Preconditions are usually grouped together. There is no
2110 -- need to inspect the whole declarative list.
2119 end Process_Preconditions_For;
2123 Decls : constant List_Id := Declarations (Body_Decl);
2126 -- Start of processing for Process_Preconditions
2129 -- Find the last internally generated declaration, starting from the
2130 -- top of the body declarations. This ensures that discriminals and
2131 -- subtypes are properly visible to the pragma Check equivalents.
2133 if Present (Decls) then
2134 Decl := First (Decls);
2135 while Present (Decl) loop
2136 exit when Comes_From_Source (Decl);
2137 Insert_Node := Decl;
2142 -- The processing of preconditions is done in reverse order (body
2143 -- first), because each pragma Check equivalent is inserted at the
2144 -- top of the declarations. This ensures that the final order is
2145 -- consistent with following diagram:
2147 -- <inherited preconditions>
2148 -- <preconditions from spec>
2149 -- <preconditions from body>
2151 Process_Preconditions_For (Body_Id);
2153 if Present (Spec_Id) then
2154 Process_Preconditions_For (Spec_Id);
2155 Process_Inherited_Preconditions;
2157 end Process_Preconditions;
2161 Restore_Scope : Boolean := False;
2163 Stmts : List_Id := No_List;
2164 Subp_Id : Entity_Id;
2166 -- Start of processing for Expand_Subprogram_Contract
2169 -- Obtain the entity of the initial declaration
2171 if Present (Spec_Id) then
2177 -- Do not perform expansion activity when it is not needed
2179 if not Expander_Active then
2182 -- ASIS requires an unaltered tree
2184 elsif ASIS_Mode then
2187 -- GNATprove does not need the executable semantics of a contract
2189 elsif GNATprove_Mode then
2192 -- The contract of a generic subprogram or one declared in a generic
2193 -- context is not expanded, as the corresponding instance will provide
2194 -- the executable semantics of the contract.
2196 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
2199 -- All subprograms carry a contract, but for some it is not significant
2200 -- and should not be processed. This is a small optimization.
2202 elsif not Has_Significant_Contract (Subp_Id) then
2205 -- The contract of an ignored Ghost subprogram does not need expansion,
2206 -- because the subprogram and all calls to it will be removed.
2208 elsif Is_Ignored_Ghost_Entity (Subp_Id) then
2212 -- Do not re-expand the same contract. This scenario occurs when a
2213 -- construct is rewritten into something else during its analysis
2214 -- (expression functions for instance).
2216 if Has_Expanded_Contract (Subp_Id) then
2219 -- Otherwise mark the subprogram
2222 Set_Has_Expanded_Contract (Subp_Id);
2225 -- Ensure that the formal parameters are visible when expanding all
2228 if not In_Open_Scopes (Subp_Id) then
2229 Restore_Scope := True;
2230 Push_Scope (Subp_Id);
2232 if Is_Generic_Subprogram (Subp_Id) then
2233 Install_Generic_Formals (Subp_Id);
2235 Install_Formals (Subp_Id);
2239 -- The expansion of a subprogram contract involves the creation of Check
2240 -- pragmas to verify the contract assertions of the spec and body in a
2241 -- particular order. The order is as follows:
2243 -- function Example (...) return ... is
2244 -- procedure _Postconditions (...) is
2246 -- <refined postconditions from body>
2247 -- <postconditions from body>
2248 -- <postconditions from spec>
2249 -- <inherited postconditions>
2250 -- <contract case consequences>
2251 -- <invariant check of function result>
2252 -- <invariant and predicate checks of parameters>
2253 -- end _Postconditions;
2255 -- <inherited preconditions>
2256 -- <preconditions from spec>
2257 -- <preconditions from body>
2258 -- <contract case conditions>
2260 -- <source declarations>
2262 -- <source statements>
2264 -- _Preconditions (Result);
2268 -- Routine _Postconditions holds all contract assertions that must be
2269 -- verified on exit from the related subprogram.
2271 -- Step 1: Handle all preconditions. This action must come before the
2272 -- processing of pragma Contract_Cases because the pragma prepends items
2273 -- to the body declarations.
2275 Process_Preconditions;
2277 -- Step 2: Handle all postconditions. This action must come before the
2278 -- processing of pragma Contract_Cases because the pragma appends items
2281 Process_Postconditions (Stmts);
2283 -- Step 3: Handle pragma Contract_Cases. This action must come before
2284 -- the processing of invariants and predicates because those append
2285 -- items to list Stmts.
2287 Process_Contract_Cases (Stmts);
2289 -- Step 4: Apply invariant and predicate checks on a function result and
2290 -- all formals. The resulting checks are accumulated in list Stmts.
2292 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
2294 -- Step 5: Construct procedure _Postconditions
2296 Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
2298 if Restore_Scope then
2301 end Expand_Subprogram_Contract;
2303 ---------------------------------
2304 -- Inherit_Subprogram_Contract --
2305 ---------------------------------
2307 procedure Inherit_Subprogram_Contract
2309 From_Subp : Entity_Id)
2311 procedure Inherit_Pragma (Prag_Id : Pragma_Id);
2312 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
2315 --------------------
2316 -- Inherit_Pragma --
2317 --------------------
2319 procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
2320 Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
2324 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
2325 -- chains, therefore the node must be replicated. The new pragma is
2326 -- flagged as inherited for distinction purposes.
2328 if Present (Prag) then
2329 New_Prag := New_Copy_Tree (Prag);
2330 Set_Is_Inherited (New_Prag);
2332 Add_Contract_Item (New_Prag, Subp);
2336 -- Start of processing for Inherit_Subprogram_Contract
2339 -- Inheritance is carried out only when both entities are subprograms
2342 if Is_Subprogram_Or_Generic_Subprogram (Subp)
2343 and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
2344 and then Present (Contract (From_Subp))
2346 Inherit_Pragma (Pragma_Extensions_Visible);
2348 end Inherit_Subprogram_Contract;
2350 -------------------------------------
2351 -- Instantiate_Subprogram_Contract --
2352 -------------------------------------
2354 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
2355 procedure Instantiate_Pragmas (First_Prag : Node_Id);
2356 -- Instantiate all contract-related source pragmas found in the list,
2357 -- starting with pragma First_Prag. Each instantiated pragma is added
2360 -------------------------
2361 -- Instantiate_Pragmas --
2362 -------------------------
2364 procedure Instantiate_Pragmas (First_Prag : Node_Id) is
2365 Inst_Prag : Node_Id;
2370 while Present (Prag) loop
2371 if Is_Generic_Contract_Pragma (Prag) then
2373 Copy_Generic_Node (Prag, Empty, Instantiating => True);
2375 Set_Analyzed (Inst_Prag, False);
2376 Append_To (L, Inst_Prag);
2379 Prag := Next_Pragma (Prag);
2381 end Instantiate_Pragmas;
2385 Items : constant Node_Id := Contract (Defining_Entity (Templ));
2387 -- Start of processing for Instantiate_Subprogram_Contract
2390 if Present (Items) then
2391 Instantiate_Pragmas (Pre_Post_Conditions (Items));
2392 Instantiate_Pragmas (Contract_Test_Cases (Items));
2393 Instantiate_Pragmas (Classifications (Items));
2395 end Instantiate_Subprogram_Contract;
2397 ----------------------------------------
2398 -- Save_Global_References_In_Contract --
2399 ----------------------------------------
2401 procedure Save_Global_References_In_Contract
2405 procedure Save_Global_References_In_List (First_Prag : Node_Id);
2406 -- Save all global references in contract-related source pragmas found
2407 -- in the list, starting with pragma First_Prag.
2409 ------------------------------------
2410 -- Save_Global_References_In_List --
2411 ------------------------------------
2413 procedure Save_Global_References_In_List (First_Prag : Node_Id) is
2418 while Present (Prag) loop
2419 if Is_Generic_Contract_Pragma (Prag) then
2420 Save_Global_References (Prag);
2423 Prag := Next_Pragma (Prag);
2425 end Save_Global_References_In_List;
2429 Items : constant Node_Id := Contract (Defining_Entity (Templ));
2431 -- Start of processing for Save_Global_References_In_Contract
2434 -- The entity of the analyzed generic copy must be on the scope stack
2435 -- to ensure proper detection of global references.
2437 Push_Scope (Gen_Id);
2439 if Permits_Aspect_Specifications (Templ)
2440 and then Has_Aspects (Templ)
2442 Save_Global_References_In_Aspects (Templ);
2445 if Present (Items) then
2446 Save_Global_References_In_List (Pre_Post_Conditions (Items));
2447 Save_Global_References_In_List (Contract_Test_Cases (Items));
2448 Save_Global_References_In_List (Classifications (Items));
2452 end Save_Global_References_In_Contract;