1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- C O N T R A C T S --
9 -- Copyright (C) 2015-2016, Free Software Foundation, Inc. --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
26 with Aspects; use Aspects;
27 with Atree; use Atree;
28 with 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_Ch13; use Sem_Ch13;
44 with Sem_Disp; use Sem_Disp;
45 with Sem_Prag; use Sem_Prag;
46 with Sem_Util; use Sem_Util;
47 with Sinfo; use Sinfo;
48 with Snames; use Snames;
49 with Stringt; use Stringt;
50 with Tbuild; use Tbuild;
52 package body Contracts is
54 procedure Analyze_Contracts
57 Freeze_Id : Entity_Id);
58 -- Subsidiary to the one parameter version of Analyze_Contracts and routine
59 -- Analyze_Previous_Constracts. Analyze the contracts of all constructs in
60 -- the list L. If Freeze_Nod is set, then the analysis stops when the node
61 -- is reached. Freeze_Id is the entity of some related context which caused
62 -- freezing up to node Freeze_Nod.
64 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
65 -- Expand the contracts of a subprogram body and its correspoding spec (if
66 -- any). This routine processes all [refined] pre- and postconditions as
67 -- well as Contract_Cases, invariants and predicates. Body_Id denotes the
68 -- entity of the subprogram body.
70 -----------------------
71 -- Add_Contract_Item --
72 -----------------------
74 procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
75 Items : Node_Id := Contract (Id);
77 procedure Add_Classification;
78 -- Prepend Prag to the list of classifications
80 procedure Add_Contract_Test_Case;
81 -- Prepend Prag to the list of contract and test cases
83 procedure Add_Pre_Post_Condition;
84 -- Prepend Prag to the list of pre- and postconditions
86 ------------------------
87 -- Add_Classification --
88 ------------------------
90 procedure Add_Classification is
92 Set_Next_Pragma (Prag, Classifications (Items));
93 Set_Classifications (Items, Prag);
94 end Add_Classification;
96 ----------------------------
97 -- Add_Contract_Test_Case --
98 ----------------------------
100 procedure Add_Contract_Test_Case is
102 Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
103 Set_Contract_Test_Cases (Items, Prag);
104 end Add_Contract_Test_Case;
106 ----------------------------
107 -- Add_Pre_Post_Condition --
108 ----------------------------
110 procedure Add_Pre_Post_Condition is
112 Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
113 Set_Pre_Post_Conditions (Items, Prag);
114 end Add_Pre_Post_Condition;
118 -- A contract must contain only pragmas
120 pragma Assert (Nkind (Prag) = N_Pragma);
121 Prag_Nam : constant Name_Id := Pragma_Name (Prag);
123 -- Start of processing for Add_Contract_Item
126 -- Create a new contract when adding the first item
129 Items := Make_Contract (Sloc (Id));
130 Set_Contract (Id, Items);
133 -- Constants, the applicable pragmas are:
136 if Ekind (Id) = E_Constant then
137 if Prag_Nam = Name_Part_Of then
140 -- The pragma is not a proper contract item
146 -- Entry bodies, the applicable pragmas are:
151 elsif Is_Entry_Body (Id) then
152 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
155 elsif Prag_Nam = Name_Refined_Post then
156 Add_Pre_Post_Condition;
158 -- The pragma is not a proper contract item
164 -- Entry or subprogram declarations, the applicable pragmas are:
168 -- Extensions_Visible
176 elsif Is_Entry_Declaration (Id)
177 or else Ekind_In (Id, E_Function,
182 if Nam_In (Prag_Nam, Name_Attach_Handler, Name_Interrupt_Handler)
183 and then Ekind_In (Id, E_Generic_Procedure, E_Procedure)
187 elsif Nam_In (Prag_Nam, Name_Depends,
188 Name_Extensions_Visible,
193 elsif Prag_Nam = Name_Volatile_Function
194 and then Ekind_In (Id, E_Function, E_Generic_Function)
198 elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then
199 Add_Contract_Test_Case;
201 elsif Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
202 Add_Pre_Post_Condition;
204 -- The pragma is not a proper contract item
210 -- Packages or instantiations, the applicable pragmas are:
214 -- Part_Of (instantiation only)
216 elsif Ekind_In (Id, E_Generic_Package, E_Package) then
217 if Nam_In (Prag_Nam, Name_Abstract_State,
218 Name_Initial_Condition,
223 -- Indicator Part_Of must be associated with a package instantiation
225 elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
228 -- The pragma is not a proper contract item
234 -- Package bodies, the applicable pragmas are:
237 elsif Ekind (Id) = E_Package_Body then
238 if Prag_Nam = Name_Refined_State then
241 -- The pragma is not a proper contract item
247 -- Protected units, the applicable pragmas are:
250 elsif Ekind (Id) = E_Protected_Type then
251 if Prag_Nam = Name_Part_Of then
254 -- The pragma is not a proper contract item
260 -- Subprogram bodies, the applicable pragmas are:
267 elsif Ekind (Id) = E_Subprogram_Body then
268 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
271 elsif Nam_In (Prag_Nam, Name_Postcondition,
275 Add_Pre_Post_Condition;
277 -- The pragma is not a proper contract item
283 -- Task bodies, the applicable pragmas are:
287 elsif Ekind (Id) = E_Task_Body then
288 if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
291 -- The pragma is not a proper contract item
297 -- Task units, the applicable pragmas are:
302 elsif Ekind (Id) = E_Task_Type then
303 if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then
306 -- The pragma is not a proper contract item
312 -- Variables, the applicable pragmas are:
315 -- Constant_After_Elaboration
322 elsif Ekind (Id) = E_Variable then
323 if Nam_In (Prag_Nam, Name_Async_Readers,
325 Name_Constant_After_Elaboration,
327 Name_Effective_Reads,
328 Name_Effective_Writes,
334 -- The pragma is not a proper contract item
340 end Add_Contract_Item;
342 -----------------------
343 -- Analyze_Contracts --
344 -----------------------
346 procedure Analyze_Contracts (L : List_Id) is
348 Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty);
349 end Analyze_Contracts;
351 procedure Analyze_Contracts
353 Freeze_Nod : Node_Id;
354 Freeze_Id : Entity_Id)
360 while Present (Decl) loop
362 -- The caller requests that the traversal stops at a particular node
363 -- that causes contract "freezing".
365 if Present (Freeze_Nod) and then Decl = Freeze_Nod then
369 -- Entry or subprogram declarations
371 if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
373 N_Generic_Subprogram_Declaration,
374 N_Subprogram_Declaration)
376 Analyze_Entry_Or_Subprogram_Contract
377 (Subp_Id => Defining_Entity (Decl),
378 Freeze_Id => Freeze_Id);
380 -- Entry or subprogram bodies
382 elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
383 Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl));
387 elsif Nkind (Decl) = N_Object_Declaration then
388 Analyze_Object_Contract
389 (Obj_Id => Defining_Entity (Decl),
390 Freeze_Id => Freeze_Id);
394 elsif Nkind_In (Decl, N_Protected_Type_Declaration,
395 N_Single_Protected_Declaration)
397 Analyze_Protected_Contract (Defining_Entity (Decl));
399 -- Subprogram body stubs
401 elsif Nkind (Decl) = N_Subprogram_Body_Stub then
402 Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
406 elsif Nkind_In (Decl, N_Single_Task_Declaration,
407 N_Task_Type_Declaration)
409 Analyze_Task_Contract (Defining_Entity (Decl));
411 -- For type declarations, we need to do the pre-analysis of
412 -- Iterable aspect specifications.
413 -- Other type aspects need to be resolved here???
415 elsif Nkind (Decl) = N_Private_Type_Declaration
416 and then Present (Aspect_Specifications (Decl))
419 E : constant Entity_Id := Defining_Identifier (Decl);
420 It : constant Node_Id := Find_Aspect (E, Aspect_Iterable);
423 Validate_Iterable_Aspect (E, It);
430 end Analyze_Contracts;
432 -----------------------------------------------
433 -- Analyze_Entry_Or_Subprogram_Body_Contract --
434 -----------------------------------------------
436 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
437 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
438 Items : constant Node_Id := Contract (Body_Id);
439 Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
440 Mode : SPARK_Mode_Type;
443 -- When a subprogram body declaration is illegal, its defining entity is
444 -- left unanalyzed. There is nothing left to do in this case because the
445 -- body lacks a contract, or even a proper Ekind.
447 if Ekind (Body_Id) = E_Void then
450 -- Do not analyze a contract multiple times
452 elsif Present (Items) then
453 if Analyzed (Items) then
456 Set_Analyzed (Items);
460 -- Due to the timing of contract analysis, delayed pragmas may be
461 -- subject to the wrong SPARK_Mode, usually that of the enclosing
462 -- context. To remedy this, restore the original SPARK_Mode of the
463 -- related subprogram body.
465 Save_SPARK_Mode_And_Set (Body_Id, Mode);
467 -- Ensure that the contract cases or postconditions mention 'Result or
468 -- define a post-state.
470 Check_Result_And_Post_State (Body_Id);
472 -- A stand-alone nonvolatile function body cannot have an effectively
473 -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
474 -- check is relevant only when SPARK_Mode is on, as it is not a standard
475 -- legality rule. The check is performed here because Volatile_Function
476 -- is processed after the analysis of the related subprogram body.
479 and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
480 and then not Is_Volatile_Function (Body_Id)
482 Check_Nonvolatile_Function_Profile (Body_Id);
485 -- Restore the SPARK_Mode of the enclosing context after all delayed
486 -- pragmas have been analyzed.
488 Restore_SPARK_Mode (Mode);
490 -- Capture all global references in a generic subprogram body now that
491 -- the contract has been analyzed.
493 if Is_Generic_Declaration_Or_Body (Body_Decl) then
494 Save_Global_References_In_Contract
495 (Templ => Original_Node (Body_Decl),
499 -- Deal with preconditions, [refined] postconditions, Contract_Cases,
500 -- invariants and predicates associated with body and its spec. Do not
501 -- expand the contract of subprogram body stubs.
503 if Nkind (Body_Decl) = N_Subprogram_Body then
504 Expand_Subprogram_Contract (Body_Id);
506 end Analyze_Entry_Or_Subprogram_Body_Contract;
508 ------------------------------------------
509 -- Analyze_Entry_Or_Subprogram_Contract --
510 ------------------------------------------
512 procedure Analyze_Entry_Or_Subprogram_Contract
513 (Subp_Id : Entity_Id;
514 Freeze_Id : Entity_Id := Empty)
516 Items : constant Node_Id := Contract (Subp_Id);
517 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
519 Skip_Assert_Exprs : constant Boolean :=
520 Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
521 and then not ASIS_Mode
522 and then not GNATprove_Mode;
524 Depends : Node_Id := Empty;
525 Global : Node_Id := Empty;
526 Mode : SPARK_Mode_Type;
531 -- Do not analyze a contract multiple times
533 if Present (Items) then
534 if Analyzed (Items) then
537 Set_Analyzed (Items);
541 -- Due to the timing of contract analysis, delayed pragmas may be
542 -- subject to the wrong SPARK_Mode, usually that of the enclosing
543 -- context. To remedy this, restore the original SPARK_Mode of the
544 -- related subprogram body.
546 Save_SPARK_Mode_And_Set (Subp_Id, Mode);
548 -- All subprograms carry a contract, but for some it is not significant
549 -- and should not be processed.
551 if not Has_Significant_Contract (Subp_Id) then
554 elsif Present (Items) then
556 -- Do not analyze the pre/postconditions of an entry declaration
557 -- unless annotating the original tree for ASIS or GNATprove. The
558 -- real analysis occurs when the pre/postconditons are relocated to
559 -- the contract wrapper procedure (see Build_Contract_Wrapper).
561 if Skip_Assert_Exprs then
564 -- Otherwise analyze the pre/postconditions
567 Prag := Pre_Post_Conditions (Items);
568 while Present (Prag) loop
569 Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
570 Prag := Next_Pragma (Prag);
574 -- Analyze contract-cases and test-cases
576 Prag := Contract_Test_Cases (Items);
577 while Present (Prag) loop
578 Prag_Nam := Pragma_Name (Prag);
580 if Prag_Nam = Name_Contract_Cases then
582 -- Do not analyze the contract cases of an entry declaration
583 -- unless annotating the original tree for ASIS or GNATprove.
584 -- The real analysis occurs when the contract cases are moved
585 -- to the contract wrapper procedure (Build_Contract_Wrapper).
587 if Skip_Assert_Exprs then
590 -- Otherwise analyze the contract cases
593 Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
596 pragma Assert (Prag_Nam = Name_Test_Case);
597 Analyze_Test_Case_In_Decl_Part (Prag);
600 Prag := Next_Pragma (Prag);
603 -- Analyze classification pragmas
605 Prag := Classifications (Items);
606 while Present (Prag) loop
607 Prag_Nam := Pragma_Name (Prag);
609 if Prag_Nam = Name_Depends then
612 elsif Prag_Nam = Name_Global then
616 Prag := Next_Pragma (Prag);
619 -- Analyze Global first, as Depends may mention items classified in
620 -- the global categorization.
622 if Present (Global) then
623 Analyze_Global_In_Decl_Part (Global);
626 -- Depends must be analyzed after Global in order to see the modes of
629 if Present (Depends) then
630 Analyze_Depends_In_Decl_Part (Depends);
633 -- Ensure that the contract cases or postconditions mention 'Result
634 -- or define a post-state.
636 Check_Result_And_Post_State (Subp_Id);
639 -- A nonvolatile function cannot have an effectively volatile formal
640 -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
641 -- only when SPARK_Mode is on, as it is not a standard legality rule.
642 -- The check is performed here because pragma Volatile_Function is
643 -- processed after the analysis of the related subprogram declaration.
646 and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
647 and then not Is_Volatile_Function (Subp_Id)
649 Check_Nonvolatile_Function_Profile (Subp_Id);
652 -- Restore the SPARK_Mode of the enclosing context after all delayed
653 -- pragmas have been analyzed.
655 Restore_SPARK_Mode (Mode);
657 -- Capture all global references in a generic subprogram now that the
658 -- contract has been analyzed.
660 if Is_Generic_Declaration_Or_Body (Subp_Decl) then
661 Save_Global_References_In_Contract
662 (Templ => Original_Node (Subp_Decl),
665 end Analyze_Entry_Or_Subprogram_Contract;
667 -----------------------------
668 -- Analyze_Object_Contract --
669 -----------------------------
671 procedure Analyze_Object_Contract
673 Freeze_Id : Entity_Id := Empty)
675 Obj_Typ : constant Entity_Id := Etype (Obj_Id);
676 AR_Val : Boolean := False;
677 AW_Val : Boolean := False;
678 ER_Val : Boolean := False;
679 EW_Val : Boolean := False;
681 Mode : SPARK_Mode_Type;
684 Restore_Mode : Boolean := False;
685 Seen : Boolean := False;
688 -- The loop parameter in an element iterator over a formal container
689 -- is declared with an object declaration, but no contracts apply.
691 if Ekind (Obj_Id) = E_Loop_Parameter then
695 -- Do not analyze a contract multiple times
697 Items := Contract (Obj_Id);
699 if Present (Items) then
700 if Analyzed (Items) then
703 Set_Analyzed (Items);
707 -- The anonymous object created for a single concurrent type inherits
708 -- the SPARK_Mode from the type. Due to the timing of contract analysis,
709 -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
710 -- of the enclosing context. To remedy this, restore the original mode
711 -- of the related anonymous object.
713 if Is_Single_Concurrent_Object (Obj_Id)
714 and then Present (SPARK_Pragma (Obj_Id))
716 Restore_Mode := True;
717 Save_SPARK_Mode_And_Set (Obj_Id, Mode);
720 -- Constant-related checks
722 if Ekind (Obj_Id) = E_Constant then
724 -- Analyze indicator Part_Of
726 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
728 -- Check whether the lack of indicator Part_Of agrees with the
729 -- placement of the constant with respect to the state space.
732 Check_Missing_Part_Of (Obj_Id);
735 -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
736 -- This check is relevant only when SPARK_Mode is on, as it is not
737 -- a standard Ada legality rule. Internally-generated constants that
738 -- map generic formals to actuals in instantiations are allowed to
742 and then Comes_From_Source (Obj_Id)
743 and then Is_Effectively_Volatile (Obj_Id)
744 and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
746 Error_Msg_N ("constant cannot be volatile", Obj_Id);
749 -- Variable-related checks
751 else pragma Assert (Ekind (Obj_Id) = E_Variable);
753 -- Analyze all external properties
755 Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
757 if Present (Prag) then
758 Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
762 Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
764 if Present (Prag) then
765 Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
769 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
771 if Present (Prag) then
772 Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
776 Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
778 if Present (Prag) then
779 Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
783 -- Verify the mutual interaction of the various external properties
786 Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
789 -- The anonymous object created for a single concurrent type carries
790 -- pragmas Depends and Globat of the type.
792 if Is_Single_Concurrent_Object (Obj_Id) then
794 -- Analyze Global first, as Depends may mention items classified
795 -- in the global categorization.
797 Prag := Get_Pragma (Obj_Id, Pragma_Global);
799 if Present (Prag) then
800 Analyze_Global_In_Decl_Part (Prag);
803 -- Depends must be analyzed after Global in order to see the modes
804 -- of all global items.
806 Prag := Get_Pragma (Obj_Id, Pragma_Depends);
808 if Present (Prag) then
809 Analyze_Depends_In_Decl_Part (Prag);
813 Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
815 -- Analyze indicator Part_Of
817 if Present (Prag) then
818 Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id);
820 -- The variable is a constituent of a single protected/task type
821 -- and behaves as a component of the type. Verify that references
822 -- to the variable occur within the definition or body of the type
825 if Present (Encapsulating_State (Obj_Id))
826 and then Is_Single_Concurrent_Object
827 (Encapsulating_State (Obj_Id))
828 and then Present (Part_Of_References (Obj_Id))
830 Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id));
831 while Present (Ref_Elmt) loop
832 Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt));
833 Next_Elmt (Ref_Elmt);
837 -- Otherwise check whether the lack of indicator Part_Of agrees with
838 -- the placement of the variable with respect to the state space.
841 Check_Missing_Part_Of (Obj_Id);
844 -- The following checks are relevant only when SPARK_Mode is on, as
845 -- they are not standard Ada legality rules. Internally generated
846 -- temporaries are ignored.
848 if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
849 if Is_Effectively_Volatile (Obj_Id) then
851 -- The declaration of an effectively volatile object must
852 -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
854 if not Is_Library_Level_Entity (Obj_Id) then
856 ("volatile variable & must be declared at library level",
859 -- An object of a discriminated type cannot be effectively
860 -- volatile except for protected objects (SPARK RM 7.1.3(5)).
862 elsif Has_Discriminants (Obj_Typ)
863 and then not Is_Protected_Type (Obj_Typ)
866 ("discriminated object & cannot be volatile", Obj_Id);
868 -- An object of a tagged type cannot be effectively volatile
869 -- (SPARK RM C.6(5)).
871 elsif Is_Tagged_Type (Obj_Typ) then
872 Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
875 -- The object is not effectively volatile
878 -- A non-effectively volatile object cannot have effectively
879 -- volatile components (SPARK RM 7.1.3(6)).
881 if not Is_Effectively_Volatile (Obj_Id)
882 and then Has_Volatile_Component (Obj_Typ)
885 ("non-volatile object & cannot have volatile components",
894 if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
896 -- A Ghost object cannot be of a type that yields a synchronized
897 -- object (SPARK RM 6.9(19)).
899 if Yields_Synchronized_Object (Obj_Typ) then
900 Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
902 -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
903 -- SPARK RM 6.9(19)).
905 elsif Is_Effectively_Volatile (Obj_Id) then
906 Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
908 -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
909 -- One exception to this is the object that represents the dispatch
910 -- table of a Ghost tagged type, as the symbol needs to be exported.
912 elsif Is_Exported (Obj_Id) then
913 Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
915 elsif Is_Imported (Obj_Id) then
916 Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
920 -- Restore the SPARK_Mode of the enclosing context after all delayed
921 -- pragmas have been analyzed.
924 Restore_SPARK_Mode (Mode);
926 end Analyze_Object_Contract;
928 -----------------------------------
929 -- Analyze_Package_Body_Contract --
930 -----------------------------------
932 procedure Analyze_Package_Body_Contract
933 (Body_Id : Entity_Id;
934 Freeze_Id : Entity_Id := Empty)
936 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
937 Items : constant Node_Id := Contract (Body_Id);
938 Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
939 Mode : SPARK_Mode_Type;
943 -- Do not analyze a contract multiple times
945 if Present (Items) then
946 if Analyzed (Items) then
949 Set_Analyzed (Items);
953 -- Due to the timing of contract analysis, delayed pragmas may be
954 -- subject to the wrong SPARK_Mode, usually that of the enclosing
955 -- context. To remedy this, restore the original SPARK_Mode of the
956 -- related package body.
958 Save_SPARK_Mode_And_Set (Body_Id, Mode);
960 Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
962 -- The analysis of pragma Refined_State detects whether the spec has
963 -- abstract states available for refinement.
965 if Present (Ref_State) then
966 Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id);
969 -- Restore the SPARK_Mode of the enclosing context after all delayed
970 -- pragmas have been analyzed.
972 Restore_SPARK_Mode (Mode);
974 -- Capture all global references in a generic package body now that the
975 -- contract has been analyzed.
977 if Is_Generic_Declaration_Or_Body (Body_Decl) then
978 Save_Global_References_In_Contract
979 (Templ => Original_Node (Body_Decl),
982 end Analyze_Package_Body_Contract;
984 ------------------------------
985 -- Analyze_Package_Contract --
986 ------------------------------
988 procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
989 Items : constant Node_Id := Contract (Pack_Id);
990 Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
991 Init : Node_Id := Empty;
992 Init_Cond : Node_Id := Empty;
993 Mode : SPARK_Mode_Type;
998 -- Do not analyze a contract multiple times
1000 if Present (Items) then
1001 if Analyzed (Items) then
1004 Set_Analyzed (Items);
1008 -- Due to the timing of contract analysis, delayed pragmas may be
1009 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1010 -- context. To remedy this, restore the original SPARK_Mode of the
1013 Save_SPARK_Mode_And_Set (Pack_Id, Mode);
1015 if Present (Items) then
1017 -- Locate and store pragmas Initial_Condition and Initializes, since
1018 -- their order of analysis matters.
1020 Prag := Classifications (Items);
1021 while Present (Prag) loop
1022 Prag_Nam := Pragma_Name (Prag);
1024 if Prag_Nam = Name_Initial_Condition then
1027 elsif Prag_Nam = Name_Initializes then
1031 Prag := Next_Pragma (Prag);
1034 -- Analyze the initialization-related pragmas. Initializes must come
1035 -- before Initial_Condition due to item dependencies.
1037 if Present (Init) then
1038 Analyze_Initializes_In_Decl_Part (Init);
1041 if Present (Init_Cond) then
1042 Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
1046 -- Check whether the lack of indicator Part_Of agrees with the placement
1047 -- of the package instantiation with respect to the state space.
1049 if Is_Generic_Instance (Pack_Id) then
1050 Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
1053 Check_Missing_Part_Of (Pack_Id);
1057 -- Restore the SPARK_Mode of the enclosing context after all delayed
1058 -- pragmas have been analyzed.
1060 Restore_SPARK_Mode (Mode);
1062 -- Capture all global references in a generic package now that the
1063 -- contract has been analyzed.
1065 if Is_Generic_Declaration_Or_Body (Pack_Decl) then
1066 Save_Global_References_In_Contract
1067 (Templ => Original_Node (Pack_Decl),
1070 end Analyze_Package_Contract;
1072 --------------------------------
1073 -- Analyze_Previous_Contracts --
1074 --------------------------------
1076 procedure Analyze_Previous_Contracts (Body_Decl : Node_Id) is
1077 Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
1081 -- A body that is in the process of being inlined appears from source,
1082 -- but carries name _parent. Such a body does not cause "freezing" of
1085 if Chars (Body_Id) = Name_uParent then
1089 -- Climb the parent chain looking for an enclosing package body. Do not
1090 -- use the scope stack, as a body uses the entity of its corresponding
1093 Par := Parent (Body_Decl);
1094 while Present (Par) loop
1095 if Nkind (Par) = N_Package_Body then
1096 Analyze_Package_Body_Contract
1097 (Body_Id => Defining_Entity (Par),
1098 Freeze_Id => Defining_Entity (Body_Decl));
1103 Par := Parent (Par);
1106 -- Analyze the contracts of all eligible construct up to the body which
1107 -- caused the "freezing".
1109 if Is_List_Member (Body_Decl) then
1111 (L => List_Containing (Body_Decl),
1112 Freeze_Nod => Body_Decl,
1113 Freeze_Id => Body_Id);
1115 end Analyze_Previous_Contracts;
1117 --------------------------------
1118 -- Analyze_Protected_Contract --
1119 --------------------------------
1121 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
1122 Items : constant Node_Id := Contract (Prot_Id);
1125 -- Do not analyze a contract multiple times
1127 if Present (Items) then
1128 if Analyzed (Items) then
1131 Set_Analyzed (Items);
1134 end Analyze_Protected_Contract;
1136 -------------------------------------------
1137 -- Analyze_Subprogram_Body_Stub_Contract --
1138 -------------------------------------------
1140 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
1141 Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
1142 Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
1145 -- A subprogram body stub may act as its own spec or as the completion
1146 -- of a previous declaration. Depending on the context, the contract of
1147 -- the stub may contain two sets of pragmas.
1149 -- The stub is a completion, the applicable pragmas are:
1153 if Present (Spec_Id) then
1154 Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
1156 -- The stub acts as its own spec, the applicable pragmas are:
1165 Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
1167 end Analyze_Subprogram_Body_Stub_Contract;
1169 ---------------------------
1170 -- Analyze_Task_Contract --
1171 ---------------------------
1173 procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
1174 Items : constant Node_Id := Contract (Task_Id);
1175 Mode : SPARK_Mode_Type;
1179 -- Do not analyze a contract multiple times
1181 if Present (Items) then
1182 if Analyzed (Items) then
1185 Set_Analyzed (Items);
1189 -- Due to the timing of contract analysis, delayed pragmas may be
1190 -- subject to the wrong SPARK_Mode, usually that of the enclosing
1191 -- context. To remedy this, restore the original SPARK_Mode of the
1192 -- related task unit.
1194 Save_SPARK_Mode_And_Set (Task_Id, Mode);
1196 -- Analyze Global first, as Depends may mention items classified in the
1197 -- global categorization.
1199 Prag := Get_Pragma (Task_Id, Pragma_Global);
1201 if Present (Prag) then
1202 Analyze_Global_In_Decl_Part (Prag);
1205 -- Depends must be analyzed after Global in order to see the modes of
1206 -- all global items.
1208 Prag := Get_Pragma (Task_Id, Pragma_Depends);
1210 if Present (Prag) then
1211 Analyze_Depends_In_Decl_Part (Prag);
1214 -- Restore the SPARK_Mode of the enclosing context after all delayed
1215 -- pragmas have been analyzed.
1217 Restore_SPARK_Mode (Mode);
1218 end Analyze_Task_Contract;
1220 -----------------------------
1221 -- Create_Generic_Contract --
1222 -----------------------------
1224 procedure Create_Generic_Contract (Unit : Node_Id) is
1225 Templ : constant Node_Id := Original_Node (Unit);
1226 Templ_Id : constant Entity_Id := Defining_Entity (Templ);
1228 procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
1229 -- Add a single contract-related source pragma Prag to the contract of
1230 -- generic template Templ_Id.
1232 ---------------------------------
1233 -- Add_Generic_Contract_Pragma --
1234 ---------------------------------
1236 procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
1237 Prag_Templ : Node_Id;
1240 -- Mark the pragma to prevent the premature capture of global
1241 -- references when capturing global references of the context
1242 -- (see Save_References_In_Pragma).
1244 Set_Is_Generic_Contract_Pragma (Prag);
1246 -- Pragmas that apply to a generic subprogram declaration are not
1247 -- part of the semantic structure of the generic template:
1250 -- procedure Example (Formal : Integer);
1251 -- pragma Precondition (Formal > 0);
1253 -- Create a generic template for such pragmas and link the template
1254 -- of the pragma with the generic template.
1256 if Nkind (Templ) = N_Generic_Subprogram_Declaration then
1258 (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
1259 Prag_Templ := Original_Node (Prag);
1261 Set_Is_Generic_Contract_Pragma (Prag_Templ);
1262 Add_Contract_Item (Prag_Templ, Templ_Id);
1264 -- Otherwise link the pragma with the generic template
1267 Add_Contract_Item (Prag, Templ_Id);
1269 end Add_Generic_Contract_Pragma;
1273 Context : constant Node_Id := Parent (Unit);
1274 Decl : Node_Id := Empty;
1276 -- Start of processing for Create_Generic_Contract
1279 -- A generic package declaration carries contract-related source pragmas
1280 -- in its visible declarations.
1282 if Nkind (Templ) = N_Generic_Package_Declaration then
1283 Set_Ekind (Templ_Id, E_Generic_Package);
1285 if Present (Visible_Declarations (Specification (Templ))) then
1286 Decl := First (Visible_Declarations (Specification (Templ)));
1289 -- A generic package body carries contract-related source pragmas in its
1292 elsif Nkind (Templ) = N_Package_Body then
1293 Set_Ekind (Templ_Id, E_Package_Body);
1295 if Present (Declarations (Templ)) then
1296 Decl := First (Declarations (Templ));
1299 -- Generic subprogram declaration
1301 elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
1302 if Nkind (Specification (Templ)) = N_Function_Specification then
1303 Set_Ekind (Templ_Id, E_Generic_Function);
1305 Set_Ekind (Templ_Id, E_Generic_Procedure);
1308 -- When the generic subprogram acts as a compilation unit, inspect
1309 -- the Pragmas_After list for contract-related source pragmas.
1311 if Nkind (Context) = N_Compilation_Unit then
1312 if Present (Aux_Decls_Node (Context))
1313 and then Present (Pragmas_After (Aux_Decls_Node (Context)))
1315 Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
1318 -- Otherwise inspect the successive declarations for contract-related
1322 Decl := Next (Unit);
1325 -- A generic subprogram body carries contract-related source pragmas in
1326 -- its declarations.
1328 elsif Nkind (Templ) = N_Subprogram_Body then
1329 Set_Ekind (Templ_Id, E_Subprogram_Body);
1331 if Present (Declarations (Templ)) then
1332 Decl := First (Declarations (Templ));
1336 -- Inspect the relevant declarations looking for contract-related source
1337 -- pragmas and add them to the contract of the generic unit.
1339 while Present (Decl) loop
1340 if Comes_From_Source (Decl) then
1341 if Nkind (Decl) = N_Pragma then
1343 -- The source pragma is a contract annotation
1345 if Is_Contract_Annotation (Decl) then
1346 Add_Generic_Contract_Pragma (Decl);
1349 -- The region where a contract-related source pragma may appear
1350 -- ends with the first source non-pragma declaration or statement.
1359 end Create_Generic_Contract;
1361 --------------------------------
1362 -- Expand_Subprogram_Contract --
1363 --------------------------------
1365 procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is
1366 Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
1367 Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
1369 procedure Add_Invariant_And_Predicate_Checks
1370 (Subp_Id : Entity_Id;
1371 Stmts : in out List_Id;
1372 Result : out Node_Id);
1373 -- Process the result of function Subp_Id (if applicable) and all its
1374 -- formals. Add invariant and predicate checks where applicable. The
1375 -- routine appends all the checks to list Stmts. If Subp_Id denotes a
1376 -- function, Result contains the entity of parameter _Result, to be
1377 -- used in the creation of procedure _Postconditions.
1379 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
1380 -- Append a node to a list. If there is no list, create a new one. When
1381 -- the item denotes a pragma, it is added to the list only when it is
1384 procedure Build_Postconditions_Procedure
1385 (Subp_Id : Entity_Id;
1387 Result : Entity_Id);
1388 -- Create the body of procedure _Postconditions which handles various
1389 -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
1390 -- of statements to be checked on exit. Parameter Result is the entity
1391 -- of parameter _Result when Subp_Id denotes a function.
1393 procedure Process_Contract_Cases (Stmts : in out List_Id);
1394 -- Process pragma Contract_Cases. This routine prepends items to the
1395 -- body declarations and appends items to list Stmts.
1397 procedure Process_Postconditions (Stmts : in out List_Id);
1398 -- Collect all [inherited] spec and body postconditions and accumulate
1399 -- their pragma Check equivalents in list Stmts.
1401 procedure Process_Preconditions;
1402 -- Collect all [inherited] spec and body preconditions and prepend their
1403 -- pragma Check equivalents to the declarations of the body.
1405 ----------------------------------------
1406 -- Add_Invariant_And_Predicate_Checks --
1407 ----------------------------------------
1409 procedure Add_Invariant_And_Predicate_Checks
1410 (Subp_Id : Entity_Id;
1411 Stmts : in out List_Id;
1412 Result : out Node_Id)
1414 procedure Add_Invariant_Access_Checks (Id : Entity_Id);
1415 -- Id denotes the return value of a function or a formal parameter.
1416 -- Add an invariant check if the type of Id is access to a type with
1417 -- invariants. The routine appends the generated code to Stmts.
1419 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
1420 -- Determine whether type Typ can benefit from invariant checks. To
1421 -- qualify, the type must have a non-null invariant procedure and
1422 -- subprogram Subp_Id must appear visible from the point of view of
1425 ---------------------------------
1426 -- Add_Invariant_Access_Checks --
1427 ---------------------------------
1429 procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
1430 Loc : constant Source_Ptr := Sloc (Body_Decl);
1437 if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
1438 Typ := Designated_Type (Typ);
1440 if Invariant_Checks_OK (Typ) then
1442 Make_Explicit_Dereference (Loc,
1443 Prefix => New_Occurrence_Of (Id, Loc));
1444 Set_Etype (Ref, Typ);
1447 -- if <Id> /= null then
1448 -- <invariant_call (<Ref>)>
1453 Make_If_Statement (Loc,
1456 Left_Opnd => New_Occurrence_Of (Id, Loc),
1457 Right_Opnd => Make_Null (Loc)),
1458 Then_Statements => New_List (
1459 Make_Invariant_Call (Ref))),
1463 end Add_Invariant_Access_Checks;
1465 -------------------------
1466 -- Invariant_Checks_OK --
1467 -------------------------
1469 function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
1470 function Has_Public_Visibility_Of_Subprogram return Boolean;
1471 -- Determine whether type Typ has public visibility of subprogram
1474 -----------------------------------------
1475 -- Has_Public_Visibility_Of_Subprogram --
1476 -----------------------------------------
1478 function Has_Public_Visibility_Of_Subprogram return Boolean is
1479 Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
1482 -- An Initialization procedure must be considered visible even
1483 -- though it is internally generated.
1485 if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
1488 elsif Ekind (Scope (Typ)) /= E_Package then
1491 -- Internally generated code is never publicly visible except
1492 -- for a subprogram that is the implementation of an expression
1493 -- function. In that case the visibility is determined by the
1496 elsif not Comes_From_Source (Subp_Decl)
1498 (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
1500 Comes_From_Source (Defining_Entity (Subp_Decl)))
1504 -- Determine whether the subprogram is declared in the visible
1505 -- declarations of the package containing the type.
1508 return List_Containing (Subp_Decl) =
1509 Visible_Declarations
1510 (Specification (Unit_Declaration_Node (Scope (Typ))));
1512 end Has_Public_Visibility_Of_Subprogram;
1514 -- Start of processing for Invariant_Checks_OK
1518 Has_Invariants (Typ)
1519 and then Present (Invariant_Procedure (Typ))
1520 and then not Has_Null_Body (Invariant_Procedure (Typ))
1521 and then Has_Public_Visibility_Of_Subprogram;
1522 end Invariant_Checks_OK;
1526 Loc : constant Source_Ptr := Sloc (Body_Decl);
1527 -- Source location of subprogram body contract
1532 -- Start of processing for Add_Invariant_And_Predicate_Checks
1537 -- Process the result of a function
1539 if Ekind (Subp_Id) = E_Function then
1540 Typ := Etype (Subp_Id);
1542 -- Generate _Result which is used in procedure _Postconditions to
1543 -- verify the return value.
1545 Result := Make_Defining_Identifier (Loc, Name_uResult);
1546 Set_Etype (Result, Typ);
1548 -- Add an invariant check when the return type has invariants and
1549 -- the related function is visible to the outside.
1551 if Invariant_Checks_OK (Typ) then
1554 Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
1558 -- Add an invariant check when the return type is an access to a
1559 -- type with invariants.
1561 Add_Invariant_Access_Checks (Result);
1564 -- Add invariant and predicates for all formals that qualify
1566 Formal := First_Formal (Subp_Id);
1567 while Present (Formal) loop
1568 Typ := Etype (Formal);
1570 if Ekind (Formal) /= E_In_Parameter
1571 or else Is_Access_Type (Typ)
1573 if Invariant_Checks_OK (Typ) then
1576 Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
1580 Add_Invariant_Access_Checks (Formal);
1582 -- Note: we used to add predicate checks for OUT and IN OUT
1583 -- formals here, but that was misguided, since such checks are
1584 -- performed on the caller side, based on the predicate of the
1585 -- actual, rather than the predicate of the formal.
1589 Next_Formal (Formal);
1591 end Add_Invariant_And_Predicate_Checks;
1593 -------------------------
1594 -- Append_Enabled_Item --
1595 -------------------------
1597 procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
1599 -- Do not chain ignored or disabled pragmas
1601 if Nkind (Item) = N_Pragma
1602 and then (Is_Ignored (Item) or else Is_Disabled (Item))
1606 -- Otherwise, add the item
1613 -- If the pragma is a conjunct in a composite postcondition, it
1614 -- has been processed in reverse order. In the postcondition body
1615 -- it must appear before the others.
1617 if Nkind (Item) = N_Pragma
1618 and then From_Aspect_Specification (Item)
1619 and then Split_PPC (Item)
1621 Prepend (Item, List);
1623 Append (Item, List);
1626 end Append_Enabled_Item;
1628 ------------------------------------
1629 -- Build_Postconditions_Procedure --
1630 ------------------------------------
1632 procedure Build_Postconditions_Procedure
1633 (Subp_Id : Entity_Id;
1637 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
1638 -- Insert node Stmt before the first source declaration of the
1639 -- related subprogram's body. If no such declaration exists, Stmt
1640 -- becomes the last declaration.
1642 --------------------------------------------
1643 -- Insert_Before_First_Source_Declaration --
1644 --------------------------------------------
1646 procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
1647 Decls : constant List_Id := Declarations (Body_Decl);
1651 -- Inspect the declarations of the related subprogram body looking
1652 -- for the first source declaration.
1654 if Present (Decls) then
1655 Decl := First (Decls);
1656 while Present (Decl) loop
1657 if Comes_From_Source (Decl) then
1658 Insert_Before (Decl, Stmt);
1665 -- If we get there, then the subprogram body lacks any source
1666 -- declarations. The body of _Postconditions now acts as the
1667 -- last declaration.
1669 Append (Stmt, Decls);
1671 -- Ensure that the body has a declaration list
1674 Set_Declarations (Body_Decl, New_List (Stmt));
1676 end Insert_Before_First_Source_Declaration;
1680 Loc : constant Source_Ptr := Sloc (Body_Decl);
1681 Params : List_Id := No_List;
1683 Proc_Decl : Node_Id;
1684 Proc_Id : Entity_Id;
1685 Proc_Spec : Node_Id;
1687 -- Start of processing for Build_Postconditions_Procedure
1690 -- Nothing to do if there are no actions to check on exit
1696 Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
1697 Set_Debug_Info_Needed (Proc_Id);
1698 Set_Postconditions_Proc (Subp_Id, Proc_Id);
1700 -- Force the front-end inlining of _Postconditions when generating C
1701 -- code, since its body may have references to itypes defined in the
1702 -- enclosing subprogram, which would cause problems for unnesting
1703 -- routines in the absence of inlining.
1705 if Generate_C_Code then
1706 Set_Has_Pragma_Inline (Proc_Id);
1707 Set_Has_Pragma_Inline_Always (Proc_Id);
1708 Set_Is_Inlined (Proc_Id);
1711 -- The related subprogram is a function: create the specification of
1712 -- parameter _Result.
1714 if Present (Result) then
1715 Params := New_List (
1716 Make_Parameter_Specification (Loc,
1717 Defining_Identifier => Result,
1719 New_Occurrence_Of (Etype (Result), Loc)));
1723 Make_Procedure_Specification (Loc,
1724 Defining_Unit_Name => Proc_Id,
1725 Parameter_Specifications => Params);
1727 Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
1729 -- Insert _Postconditions before the first source declaration of the
1730 -- body. This ensures that the body will not cause any premature
1731 -- freezing, as it may mention types:
1733 -- procedure Proc (Obj : Array_Typ) is
1734 -- procedure _postconditions is
1737 -- end _postconditions;
1739 -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
1742 -- In the example above, Obj is of type T but the incorrect placement
1743 -- of _Postconditions will cause a crash in gigi due to an out-of-
1744 -- order reference. The body of _Postconditions must be placed after
1745 -- the declaration of Temp to preserve correct visibility.
1747 Insert_Before_First_Source_Declaration (Proc_Decl);
1748 Analyze (Proc_Decl);
1750 -- Set an explicit End_Label to override the sloc of the implicit
1751 -- RETURN statement, and prevent it from inheriting the sloc of one
1752 -- the postconditions: this would cause confusing debug info to be
1753 -- produced, interfering with coverage-analysis tools.
1756 Make_Subprogram_Body (Loc,
1758 Copy_Subprogram_Spec (Proc_Spec),
1759 Declarations => Empty_List,
1760 Handled_Statement_Sequence =>
1761 Make_Handled_Sequence_Of_Statements (Loc,
1762 Statements => Stmts,
1763 End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
1765 Insert_After_And_Analyze (Proc_Decl, Proc_Bod);
1766 end Build_Postconditions_Procedure;
1768 ----------------------------
1769 -- Process_Contract_Cases --
1770 ----------------------------
1772 procedure Process_Contract_Cases (Stmts : in out List_Id) is
1773 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
1774 -- Process pragma Contract_Cases for subprogram Subp_Id
1776 --------------------------------
1777 -- Process_Contract_Cases_For --
1778 --------------------------------
1780 procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
1781 Items : constant Node_Id := Contract (Subp_Id);
1785 if Present (Items) then
1786 Prag := Contract_Test_Cases (Items);
1787 while Present (Prag) loop
1788 if Pragma_Name (Prag) = Name_Contract_Cases then
1789 Expand_Pragma_Contract_Cases
1792 Decls => Declarations (Body_Decl),
1796 Prag := Next_Pragma (Prag);
1799 end Process_Contract_Cases_For;
1801 -- Start of processing for Process_Contract_Cases
1804 Process_Contract_Cases_For (Body_Id);
1806 if Present (Spec_Id) then
1807 Process_Contract_Cases_For (Spec_Id);
1809 end Process_Contract_Cases;
1811 ----------------------------
1812 -- Process_Postconditions --
1813 ----------------------------
1815 procedure Process_Postconditions (Stmts : in out List_Id) is
1816 procedure Process_Body_Postconditions (Post_Nam : Name_Id);
1817 -- Collect all [refined] postconditions of a specific kind denoted
1818 -- by Post_Nam that belong to the body, and generate pragma Check
1819 -- equivalents in list Stmts.
1821 procedure Process_Spec_Postconditions;
1822 -- Collect all [inherited] postconditions of the spec, and generate
1823 -- pragma Check equivalents in list Stmts.
1825 ---------------------------------
1826 -- Process_Body_Postconditions --
1827 ---------------------------------
1829 procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
1830 Items : constant Node_Id := Contract (Body_Id);
1831 Unit_Decl : constant Node_Id := Parent (Body_Decl);
1836 -- Process the contract
1838 if Present (Items) then
1839 Prag := Pre_Post_Conditions (Items);
1840 while Present (Prag) loop
1841 if Pragma_Name (Prag) = Post_Nam then
1843 (Item => Build_Pragma_Check_Equivalent (Prag),
1847 Prag := Next_Pragma (Prag);
1851 -- The subprogram body being processed is actually the proper body
1852 -- of a stub with a corresponding spec. The subprogram stub may
1853 -- carry a postcondition pragma, in which case it must be taken
1854 -- into account. The pragma appears after the stub.
1856 if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
1857 Decl := Next (Corresponding_Stub (Unit_Decl));
1858 while Present (Decl) loop
1860 -- Note that non-matching pragmas are skipped
1862 if Nkind (Decl) = N_Pragma then
1863 if Pragma_Name (Decl) = Post_Nam then
1865 (Item => Build_Pragma_Check_Equivalent (Decl),
1869 -- Skip internally generated code
1871 elsif not Comes_From_Source (Decl) then
1874 -- Postcondition pragmas are usually grouped together. There
1875 -- is no need to inspect the whole declarative list.
1884 end Process_Body_Postconditions;
1886 ---------------------------------
1887 -- Process_Spec_Postconditions --
1888 ---------------------------------
1890 procedure Process_Spec_Postconditions is
1891 Subps : constant Subprogram_List :=
1892 Inherited_Subprograms (Spec_Id);
1895 Subp_Id : Entity_Id;
1898 -- Process the contract
1900 Items := Contract (Spec_Id);
1902 if Present (Items) then
1903 Prag := Pre_Post_Conditions (Items);
1904 while Present (Prag) loop
1905 if Pragma_Name (Prag) = Name_Postcondition then
1907 (Item => Build_Pragma_Check_Equivalent (Prag),
1911 Prag := Next_Pragma (Prag);
1915 -- Process the contracts of all inherited subprograms, looking for
1916 -- class-wide postconditions.
1918 for Index in Subps'Range loop
1919 Subp_Id := Subps (Index);
1920 Items := Contract (Subp_Id);
1922 if Present (Items) then
1923 Prag := Pre_Post_Conditions (Items);
1924 while Present (Prag) loop
1925 if Pragma_Name (Prag) = Name_Postcondition
1926 and then Class_Present (Prag)
1930 Build_Pragma_Check_Equivalent
1933 Inher_Id => Subp_Id),
1937 Prag := Next_Pragma (Prag);
1941 end Process_Spec_Postconditions;
1943 -- Start of processing for Process_Postconditions
1946 -- The processing of postconditions is done in reverse order (body
1947 -- first) to ensure the following arrangement:
1949 -- <refined postconditions from body>
1950 -- <postconditions from body>
1951 -- <postconditions from spec>
1952 -- <inherited postconditions>
1954 Process_Body_Postconditions (Name_Refined_Post);
1955 Process_Body_Postconditions (Name_Postcondition);
1957 if Present (Spec_Id) then
1958 Process_Spec_Postconditions;
1960 end Process_Postconditions;
1962 ---------------------------
1963 -- Process_Preconditions --
1964 ---------------------------
1966 procedure Process_Preconditions is
1967 Class_Pre : Node_Id := Empty;
1968 -- The sole [inherited] class-wide precondition pragma that applies
1969 -- to the subprogram.
1971 Insert_Node : Node_Id := Empty;
1972 -- The insertion node after which all pragma Check equivalents are
1975 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
1976 -- Determine whether arbitrary declaration Decl denotes a renaming of
1977 -- a discriminant or protection field _object.
1979 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
1980 -- Merge two class-wide preconditions by "or else"-ing them. The
1981 -- changes are accumulated in parameter Into. Update the error
1984 procedure Prepend_To_Decls (Item : Node_Id);
1985 -- Prepend a single item to the declarations of the subprogram body
1987 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
1988 -- Save a class-wide precondition into Class_Pre, or prepend a normal
1989 -- precondition to the declarations of the body and analyze it.
1991 procedure Process_Inherited_Preconditions;
1992 -- Collect all inherited class-wide preconditions and merge them into
1993 -- one big precondition to be evaluated as pragma Check.
1995 procedure Process_Preconditions_For (Subp_Id : Entity_Id);
1996 -- Collect all preconditions of subprogram Subp_Id and prepend their
1997 -- pragma Check equivalents to the declarations of the body.
1999 --------------------------
2000 -- Is_Prologue_Renaming --
2001 --------------------------
2003 function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
2010 if Nkind (Decl) = N_Object_Renaming_Declaration then
2011 Obj := Defining_Entity (Decl);
2014 if Nkind (Nam) = N_Selected_Component then
2015 Pref := Prefix (Nam);
2016 Sel := Selector_Name (Nam);
2018 -- A discriminant renaming appears as
2019 -- Discr : constant ... := Prefix.Discr;
2021 if Ekind (Obj) = E_Constant
2022 and then Is_Entity_Name (Sel)
2023 and then Present (Entity (Sel))
2024 and then Ekind (Entity (Sel)) = E_Discriminant
2028 -- A protection field renaming appears as
2029 -- Prot : ... := _object._object;
2031 -- A renamed private component is just a component of
2032 -- _object, with an arbitrary name.
2034 elsif Ekind (Obj) = E_Variable
2035 and then Nkind (Pref) = N_Identifier
2036 and then Chars (Pref) = Name_uObject
2037 and then Nkind (Sel) = N_Identifier
2045 end Is_Prologue_Renaming;
2047 -------------------------
2048 -- Merge_Preconditions --
2049 -------------------------
2051 procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
2052 function Expression_Arg (Prag : Node_Id) return Node_Id;
2053 -- Return the boolean expression argument of a precondition while
2054 -- updating its parentheses count for the subsequent merge.
2056 function Message_Arg (Prag : Node_Id) return Node_Id;
2057 -- Return the message argument of a precondition
2059 --------------------
2060 -- Expression_Arg --
2061 --------------------
2063 function Expression_Arg (Prag : Node_Id) return Node_Id is
2064 Args : constant List_Id := Pragma_Argument_Associations (Prag);
2065 Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
2068 if Paren_Count (Arg) = 0 then
2069 Set_Paren_Count (Arg, 1);
2079 function Message_Arg (Prag : Node_Id) return Node_Id is
2080 Args : constant List_Id := Pragma_Argument_Associations (Prag);
2082 return Get_Pragma_Arg (Last (Args));
2087 From_Expr : constant Node_Id := Expression_Arg (From);
2088 From_Msg : constant Node_Id := Message_Arg (From);
2089 Into_Expr : constant Node_Id := Expression_Arg (Into);
2090 Into_Msg : constant Node_Id := Message_Arg (Into);
2091 Loc : constant Source_Ptr := Sloc (Into);
2093 -- Start of processing for Merge_Preconditions
2096 -- Merge the two preconditions by "or else"-ing them
2100 Right_Opnd => Relocate_Node (Into_Expr),
2101 Left_Opnd => From_Expr));
2103 -- Merge the two error messages to produce a single message of the
2106 -- failed precondition from ...
2107 -- also failed inherited precondition from ...
2109 if not Exception_Locations_Suppressed then
2110 Start_String (Strval (Into_Msg));
2111 Store_String_Char (ASCII.LF);
2112 Store_String_Chars (" also ");
2113 Store_String_Chars (Strval (From_Msg));
2115 Set_Strval (Into_Msg, End_String);
2117 end Merge_Preconditions;
2119 ----------------------
2120 -- Prepend_To_Decls --
2121 ----------------------
2123 procedure Prepend_To_Decls (Item : Node_Id) is
2124 Decls : List_Id := Declarations (Body_Decl);
2127 -- Ensure that the body has a declarative list
2131 Set_Declarations (Body_Decl, Decls);
2134 Prepend_To (Decls, Item);
2135 end Prepend_To_Decls;
2137 ------------------------------
2138 -- Prepend_To_Decls_Or_Save --
2139 ------------------------------
2141 procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
2142 Check_Prag : Node_Id;
2145 Check_Prag := Build_Pragma_Check_Equivalent (Prag);
2147 -- Save the sole class-wide precondition (if any) for the next
2148 -- step, where it will be merged with inherited preconditions.
2150 if Class_Present (Prag) then
2151 pragma Assert (No (Class_Pre));
2152 Class_Pre := Check_Prag;
2154 -- Accumulate the corresponding Check pragmas at the top of the
2155 -- declarations. Prepending the items ensures that they will be
2156 -- evaluated in their original order.
2159 if Present (Insert_Node) then
2160 Insert_After (Insert_Node, Check_Prag);
2162 Prepend_To_Decls (Check_Prag);
2165 Analyze (Check_Prag);
2167 end Prepend_To_Decls_Or_Save;
2169 -------------------------------------
2170 -- Process_Inherited_Preconditions --
2171 -------------------------------------
2173 procedure Process_Inherited_Preconditions is
2174 Subps : constant Subprogram_List :=
2175 Inherited_Subprograms (Spec_Id);
2176 Check_Prag : Node_Id;
2179 Subp_Id : Entity_Id;
2182 -- Process the contracts of all inherited subprograms, looking for
2183 -- class-wide preconditions.
2185 for Index in Subps'Range loop
2186 Subp_Id := Subps (Index);
2187 Items := Contract (Subp_Id);
2189 if Present (Items) then
2190 Prag := Pre_Post_Conditions (Items);
2191 while Present (Prag) loop
2192 if Pragma_Name (Prag) = Name_Precondition
2193 and then Class_Present (Prag)
2196 Build_Pragma_Check_Equivalent
2199 Inher_Id => Subp_Id);
2201 -- The spec of an inherited subprogram already yielded
2202 -- a class-wide precondition. Merge the existing
2203 -- precondition with the current one using "or else".
2205 if Present (Class_Pre) then
2206 Merge_Preconditions (Check_Prag, Class_Pre);
2208 Class_Pre := Check_Prag;
2212 Prag := Next_Pragma (Prag);
2217 -- Add the merged class-wide preconditions
2219 if Present (Class_Pre) then
2220 Prepend_To_Decls (Class_Pre);
2221 Analyze (Class_Pre);
2223 end Process_Inherited_Preconditions;
2225 -------------------------------
2226 -- Process_Preconditions_For --
2227 -------------------------------
2229 procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
2230 Items : constant Node_Id := Contract (Subp_Id);
2233 Subp_Decl : Node_Id;
2236 -- Process the contract
2238 if Present (Items) then
2239 Prag := Pre_Post_Conditions (Items);
2240 while Present (Prag) loop
2241 if Pragma_Name (Prag) = Name_Precondition then
2242 Prepend_To_Decls_Or_Save (Prag);
2245 Prag := Next_Pragma (Prag);
2249 -- The subprogram declaration being processed is actually a body
2250 -- stub. The stub may carry a precondition pragma, in which case
2251 -- it must be taken into account. The pragma appears after the
2254 Subp_Decl := Unit_Declaration_Node (Subp_Id);
2256 if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
2258 -- Inspect the declarations following the body stub
2260 Decl := Next (Subp_Decl);
2261 while Present (Decl) loop
2263 -- Note that non-matching pragmas are skipped
2265 if Nkind (Decl) = N_Pragma then
2266 if Pragma_Name (Decl) = Name_Precondition then
2267 Prepend_To_Decls_Or_Save (Decl);
2270 -- Skip internally generated code
2272 elsif not Comes_From_Source (Decl) then
2275 -- Preconditions are usually grouped together. There is no
2276 -- need to inspect the whole declarative list.
2285 end Process_Preconditions_For;
2289 Decls : constant List_Id := Declarations (Body_Decl);
2292 -- Start of processing for Process_Preconditions
2295 -- Find the proper insertion point for all pragma Check equivalents
2297 if Present (Decls) then
2298 Decl := First (Decls);
2299 while Present (Decl) loop
2301 -- First source declaration terminates the search, because all
2302 -- preconditions must be evaluated prior to it, by definition.
2304 if Comes_From_Source (Decl) then
2307 -- Certain internally generated object renamings such as those
2308 -- for discriminants and protection fields must be elaborated
2309 -- before the preconditions are evaluated, as their expressions
2310 -- may mention the discriminants. The renamings include those
2311 -- for private components so we need to find the last such.
2313 elsif Is_Prologue_Renaming (Decl) then
2314 while Present (Next (Decl))
2315 and then Is_Prologue_Renaming (Next (Decl))
2320 Insert_Node := Decl;
2322 -- Otherwise the declaration does not come from source. This
2323 -- also terminates the search, because internal code may raise
2324 -- exceptions which should not preempt the preconditions.
2334 -- The processing of preconditions is done in reverse order (body
2335 -- first), because each pragma Check equivalent is inserted at the
2336 -- top of the declarations. This ensures that the final order is
2337 -- consistent with following diagram:
2339 -- <inherited preconditions>
2340 -- <preconditions from spec>
2341 -- <preconditions from body>
2343 Process_Preconditions_For (Body_Id);
2345 if Present (Spec_Id) then
2346 Process_Preconditions_For (Spec_Id);
2347 Process_Inherited_Preconditions;
2349 end Process_Preconditions;
2353 Restore_Scope : Boolean := False;
2355 Stmts : List_Id := No_List;
2356 Subp_Id : Entity_Id;
2358 -- Start of processing for Expand_Subprogram_Contract
2361 -- Obtain the entity of the initial declaration
2363 if Present (Spec_Id) then
2369 -- Do not perform expansion activity when it is not needed
2371 if not Expander_Active then
2374 -- ASIS requires an unaltered tree
2376 elsif ASIS_Mode then
2379 -- GNATprove does not need the executable semantics of a contract
2381 elsif GNATprove_Mode then
2384 -- The contract of a generic subprogram or one declared in a generic
2385 -- context is not expanded, as the corresponding instance will provide
2386 -- the executable semantics of the contract.
2388 elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
2391 -- All subprograms carry a contract, but for some it is not significant
2392 -- and should not be processed. This is a small optimization.
2394 elsif not Has_Significant_Contract (Subp_Id) then
2397 -- The contract of an ignored Ghost subprogram does not need expansion,
2398 -- because the subprogram and all calls to it will be removed.
2400 elsif Is_Ignored_Ghost_Entity (Subp_Id) then
2404 -- Do not re-expand the same contract. This scenario occurs when a
2405 -- construct is rewritten into something else during its analysis
2406 -- (expression functions for instance).
2408 if Has_Expanded_Contract (Subp_Id) then
2411 -- Otherwise mark the subprogram
2414 Set_Has_Expanded_Contract (Subp_Id);
2417 -- Ensure that the formal parameters are visible when expanding all
2420 if not In_Open_Scopes (Subp_Id) then
2421 Restore_Scope := True;
2422 Push_Scope (Subp_Id);
2424 if Is_Generic_Subprogram (Subp_Id) then
2425 Install_Generic_Formals (Subp_Id);
2427 Install_Formals (Subp_Id);
2431 -- The expansion of a subprogram contract involves the creation of Check
2432 -- pragmas to verify the contract assertions of the spec and body in a
2433 -- particular order. The order is as follows:
2435 -- function Example (...) return ... is
2436 -- procedure _Postconditions (...) is
2438 -- <refined postconditions from body>
2439 -- <postconditions from body>
2440 -- <postconditions from spec>
2441 -- <inherited postconditions>
2442 -- <contract case consequences>
2443 -- <invariant check of function result>
2444 -- <invariant and predicate checks of parameters>
2445 -- end _Postconditions;
2447 -- <inherited preconditions>
2448 -- <preconditions from spec>
2449 -- <preconditions from body>
2450 -- <contract case conditions>
2452 -- <source declarations>
2454 -- <source statements>
2456 -- _Preconditions (Result);
2460 -- Routine _Postconditions holds all contract assertions that must be
2461 -- verified on exit from the related subprogram.
2463 -- Step 1: Handle all preconditions. This action must come before the
2464 -- processing of pragma Contract_Cases because the pragma prepends items
2465 -- to the body declarations.
2467 Process_Preconditions;
2469 -- Step 2: Handle all postconditions. This action must come before the
2470 -- processing of pragma Contract_Cases because the pragma appends items
2473 Process_Postconditions (Stmts);
2475 -- Step 3: Handle pragma Contract_Cases. This action must come before
2476 -- the processing of invariants and predicates because those append
2477 -- items to list Stmts.
2479 Process_Contract_Cases (Stmts);
2481 -- Step 4: Apply invariant and predicate checks on a function result and
2482 -- all formals. The resulting checks are accumulated in list Stmts.
2484 Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
2486 -- Step 5: Construct procedure _Postconditions
2488 Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
2490 if Restore_Scope then
2493 end Expand_Subprogram_Contract;
2495 ---------------------------------
2496 -- Inherit_Subprogram_Contract --
2497 ---------------------------------
2499 procedure Inherit_Subprogram_Contract
2501 From_Subp : Entity_Id)
2503 procedure Inherit_Pragma (Prag_Id : Pragma_Id);
2504 -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
2507 --------------------
2508 -- Inherit_Pragma --
2509 --------------------
2511 procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
2512 Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
2516 -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
2517 -- chains, therefore the node must be replicated. The new pragma is
2518 -- flagged as inherited for distinction purposes.
2520 if Present (Prag) then
2521 New_Prag := New_Copy_Tree (Prag);
2522 Set_Is_Inherited_Pragma (New_Prag);
2524 Add_Contract_Item (New_Prag, Subp);
2528 -- Start of processing for Inherit_Subprogram_Contract
2531 -- Inheritance is carried out only when both entities are subprograms
2534 if Is_Subprogram_Or_Generic_Subprogram (Subp)
2535 and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
2536 and then Present (Contract (From_Subp))
2538 Inherit_Pragma (Pragma_Extensions_Visible);
2540 end Inherit_Subprogram_Contract;
2542 -------------------------------------
2543 -- Instantiate_Subprogram_Contract --
2544 -------------------------------------
2546 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
2547 procedure Instantiate_Pragmas (First_Prag : Node_Id);
2548 -- Instantiate all contract-related source pragmas found in the list,
2549 -- starting with pragma First_Prag. Each instantiated pragma is added
2552 -------------------------
2553 -- Instantiate_Pragmas --
2554 -------------------------
2556 procedure Instantiate_Pragmas (First_Prag : Node_Id) is
2557 Inst_Prag : Node_Id;
2562 while Present (Prag) loop
2563 if Is_Generic_Contract_Pragma (Prag) then
2565 Copy_Generic_Node (Prag, Empty, Instantiating => True);
2567 Set_Analyzed (Inst_Prag, False);
2568 Append_To (L, Inst_Prag);
2571 Prag := Next_Pragma (Prag);
2573 end Instantiate_Pragmas;
2577 Items : constant Node_Id := Contract (Defining_Entity (Templ));
2579 -- Start of processing for Instantiate_Subprogram_Contract
2582 if Present (Items) then
2583 Instantiate_Pragmas (Pre_Post_Conditions (Items));
2584 Instantiate_Pragmas (Contract_Test_Cases (Items));
2585 Instantiate_Pragmas (Classifications (Items));
2587 end Instantiate_Subprogram_Contract;
2589 ----------------------------------------
2590 -- Save_Global_References_In_Contract --
2591 ----------------------------------------
2593 procedure Save_Global_References_In_Contract
2597 procedure Save_Global_References_In_List (First_Prag : Node_Id);
2598 -- Save all global references in contract-related source pragmas found
2599 -- in the list, starting with pragma First_Prag.
2601 ------------------------------------
2602 -- Save_Global_References_In_List --
2603 ------------------------------------
2605 procedure Save_Global_References_In_List (First_Prag : Node_Id) is
2610 while Present (Prag) loop
2611 if Is_Generic_Contract_Pragma (Prag) then
2612 Save_Global_References (Prag);
2615 Prag := Next_Pragma (Prag);
2617 end Save_Global_References_In_List;
2621 Items : constant Node_Id := Contract (Defining_Entity (Templ));
2623 -- Start of processing for Save_Global_References_In_Contract
2626 -- The entity of the analyzed generic copy must be on the scope stack
2627 -- to ensure proper detection of global references.
2629 Push_Scope (Gen_Id);
2631 if Permits_Aspect_Specifications (Templ)
2632 and then Has_Aspects (Templ)
2634 Save_Global_References_In_Aspects (Templ);
2637 if Present (Items) then
2638 Save_Global_References_In_List (Pre_Post_Conditions (Items));
2639 Save_Global_References_In_List (Contract_Test_Cases (Items));
2640 Save_Global_References_In_List (Classifications (Items));
2644 end Save_Global_References_In_Contract;