From: Arnaud Charlet Date: Tue, 12 May 2015 12:47:19 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=caf07df9db933fc7c97c41060dfa940fa78bb345;p=gcc.git [multiple changes] 2015-05-12 Hristian Kirtchev * einfo.adb Node32 is now used as Encapsulating_State. Node37 is now used as Associated_Entity. (Associated_Entity): New routine. (Encapsulating_State): Update the assertion guard to include constants. (Set_Associated_Entity): New routine. (Set_Encapsulating_State): Update the assertion guard to include constants. (Write_Field10_Name): Remove the output for Encapsulating_State. (Write_Field32_Name): Add output for Encapsulating_State. (Write_Field37_Name): Add output for Associated_Entity. * einfo.ads New attribute Associated_Entity along with placement in entities. Attribute Encapsulating_State now uses Node32. (Associated_Entity): New routine along with pragma Inline. (Set_Associated_Entity): New routine along with pragma Inline. * inline.ads Code reformatting. * sem_attr.adb (Analyze_Attribute): Correct the prefix of attribute 'Result when the context is a generic instantiation. (Analyze_Attribute_Old_Result): Pragmas Depends and Refined_Depends are a valid context for attribute 'Result. (Denote_Same_Function): Allow attribute 'Result to denote generic functions. * sem_ch3.adb Add with and use clauses for Sem_Ch12. (Analyze_Declarations): Capture global references within the contracts of packages, subprograms and their respective bodies. * sem_ch6.adb (Analyze_Aspects_On_Body_Or_Stub): Removed. (Analyze_Completion_Contract): Removed. (Analyze_Generic_Subprogram_Body): Enchange the aspects after creating the generic copy. Create a generic contract for the template. Analyze the aspects of the generic body. Analyze the contract of the generic body when it is a compilation unit and capture global references. (Analyze_Subprogram_Body_Contract): Code cleanup. (Analyze_Subprogram_Contract): Do not save global references here. (Save_Global_References_In_List): Removed. * sem_ch7.adb (Analyze_Package_Body_Contract): Code cleanup. (Analyze_Package_Body_Helper): Create a generic contract for the template. (Analyze_Package_Contract): Code cleanup. * sem_ch10.adb Add with and use clauses for Sem_Ch12. (Analyze_Compilation_Unit): Capture global references in a generic subprogram declaration that acts as a compilation unit. * sem_ch12.adb Add with and use clauses for Sem_Prag. Illustrate the implementation of generic contracts. Alphabetize various subprograms. (Analyze_Generic_Package_Declaration): Create a generic contract for the template. (Analyze_Generic_Subprogram_Declaration): Create a generic contract for the template. (Analyze_Subprogram_Instantiation): Instantiate the contract of the subprogram. (Copy_Generic_Node): Link defining entities of the generic template with the corresponding defining entities of the generic copy. Update the processing of pragmas. (Instantiate_Contract): Removed. (Instantiate_Subprogram_Contract): New routine. (Requires_Delayed_Save): New routine. (Save_Global_References): Rename formal parameter N to Templ. Various cleanups. (Save_Global_References_In_Aspects): Moved from the spec. (Save_Global_References_In_Contract): New routine. (Save_References_In_Aggregate): New routine. (Save_References_In_Char_Lit_Or_Op_Symbol): New routine. (Save_References_In_Descendants): New routine. (Save_References_In_Identifier): New routine. (Save_References_In_Operator): New routine. (Save_References_In_Pragma): New routine. * sem_ch12.ads (Save_Global_References): Rename formal parameter N to Templ. Update the comment on usage. (Save_Global_References_In_Aspects): Moved to the body. (Save_Global_References_In_Contract): New routine. * sem_ch13.adb (Analyze_Aspect_Specifications_On_Body_Or_Stub): New routine. * sem_ch13.ads (Analyze_Aspect_Specifications_On_Body_Or_Stub): New routine. * sem_prag.adb (Add_Item_To_Name_Buffer): Add support for generic parameters. (Analyze_Contract_Cases_In_Decl_Part): Code cleanup. (Analyze_Depends_Global): New routine. (Analyze_Depends_In_Decl_Part): Code cleanup. (Analyze_Global_In_Decl_Part): Code cleanup. (Analyze_Global_Item): Constants are now valid global items. Do not perform state-related checks in an instance. Change the way renamings are handled. (Analyze_Initial_Condition_In_Decl_Part): Code cleanup. (Analyze_Initializes_In_Decl_Part): Code cleanup. (Analyze_Input_Output): The analysis of attribute 'Result in the context of pragmas Depends or Refined_Depends now reuses the existing attribute analysis machinery. Constants and generic parameters are now valid dependency items. Do not perform state-related checks in an instance. Change the way renamings are handled. (Analyze_Pragma): Add a "characteristics" section for pragmas Abstract_State, Contract_Cases, Depends, Extensions_Visible, Global, Initial_Condition, Initializes, Post, Post_Class, Postcondition, Pre, Pre_Class, Precondition, Refined_Depends, Refined_Global, Refined_Post, Refined_State, Test_Case. (Analyze_Pre_Post_Condition): Do not create a generic template here. (Analyze_Pre_Post_Condition_In_Decl_Part): Code cleanup. (Analyze_Refined_Depends_Global_Post): New routine. (Analyze_Refined_Depends_In_Decl_Part): Code cleanup. (Analyze_Refined_Global_In_Decl_Part): Code cleanup. (Analyze_Refined_Pragma): Removed. (Analyze_Refined_State_In_Decl_Part): Code cleanup. (Analyze_Test_Case_In_Decl_Part): Code cleanup. (Check_Dependency_Clause): Do not perform this check in an instance. (Check_Function_Return): Add support for generic functions. (Check_In_Out_States): Do not perform this check in an instance. (Check_Input_States): Do not perform this check in an instance. (Check_Mode_Restriction_In_Function): Add support for generic functions. (Check_Output_States): Do not perform this check in an instance. (Check_Postcondition_Use_In_Inlined_Subprogram): Rename parameter Subp_Id to Spec_Id and update comment on usage. (Check_Proof_In_States): Do not perform this check in an instance. (Check_Refined_Global_Item): Add support for constants. (Check_Refined_Global_List): Do not perform this check in an instance. (Collect_Global_Items): Reimplemented. (Collect_Subprogram_Inputs_Outputs): Add support for generic parameters. (Create_Generic_Template): Removed. (Find_Related_Package_Or_Body): Moved to spec. (Find_Role): Add support for generic parameters and constants. (Get_Argument): Moved to spec. Rename parameter Spec_Id to Context_Id. (Match_Item): Add support for constants. (Preanalyze_Test_Case_Arg): Reimplemented. (Report_Extra_Clauses): Do not perform this check in an instance. (Report_Extra_Constituents): Do not perform this check in an instance. * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update the comment on usage. (Find_Related_Package_Or_Body): Moved from body. (Get_Argument): Moved from body. * sem_util.adb Add with and use clauses for Sem_Ch12. (Corresponding_Spec_Of): Add support for packages and package bodies. (Create_Generic_Contract): New routine. (Is_Contract_Annotation): Reimplemented. (Is_Generic_Declaration_Or_Body): New routine. (Is_Package_Contract_Annotation): New routine. (Is_Subprogram_Contract_Annotation): New routine. * sem_util.ads (Corresponding_Spec_Of): Update the comment on usage. (Create_Generic_Contract): New routine. (Is_Generic_Declaration_Or_Body): New routine. (Is_Package_Contract_Annotation): New routine. (Is_Subprogram_Contract_Annotation): New routine. * sinfo.adb (Is_Generic_Contract_Pragma): New routine. (Set_Is_Generic_Contract_Pragma): New routine. * sinfo.ads Add new attribute Is_Generic_Contract_Pragma along with occurrences in nodes. (Is_Generic_Contract_Pragma): New routine along with pragma Inline. (Set_Is_Generic_Contract_Pragma): New routine along with pragma Inline. * treepr.adb (Print_Entity_Info): Output fields 36 to 41. 2015-05-12 Robert Dewar * a-taster.ads: Minor comment fix: fix bad header, this is a pure RM unit. From-SVN: r223064 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d97ba6804c7..e1a377fe3ae 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,160 @@ +2015-05-12 Hristian Kirtchev + + * einfo.adb Node32 is now used as Encapsulating_State. + Node37 is now used as Associated_Entity. + (Associated_Entity): New routine. + (Encapsulating_State): Update the assertion guard + to include constants. + (Set_Associated_Entity): New routine. + (Set_Encapsulating_State): Update the assertion guard to + include constants. + (Write_Field10_Name): Remove the output for Encapsulating_State. + (Write_Field32_Name): Add output for Encapsulating_State. + (Write_Field37_Name): Add output for Associated_Entity. + * einfo.ads New attribute Associated_Entity along with placement + in entities. Attribute Encapsulating_State now uses Node32. + (Associated_Entity): New routine along with pragma Inline. + (Set_Associated_Entity): New routine along with pragma Inline. + * inline.ads Code reformatting. + * sem_attr.adb (Analyze_Attribute): Correct the prefix of + attribute 'Result when the context is a generic instantiation. + (Analyze_Attribute_Old_Result): Pragmas Depends and + Refined_Depends are a valid context for attribute 'Result. + (Denote_Same_Function): Allow attribute 'Result to denote + generic functions. + * sem_ch3.adb Add with and use clauses for Sem_Ch12. + (Analyze_Declarations): Capture global references within the + contracts of packages, subprograms and their respective bodies. + * sem_ch6.adb (Analyze_Aspects_On_Body_Or_Stub): Removed. + (Analyze_Completion_Contract): Removed. + (Analyze_Generic_Subprogram_Body): Enchange the aspects after + creating the generic copy. Create a generic contract for the + template. Analyze the aspects of the generic body. Analyze the + contract of the generic body when it is a compilation unit and + capture global references. + (Analyze_Subprogram_Body_Contract): Code cleanup. + (Analyze_Subprogram_Contract): Do not save global references here. + (Save_Global_References_In_List): Removed. + * sem_ch7.adb (Analyze_Package_Body_Contract): Code cleanup. + (Analyze_Package_Body_Helper): Create a generic contract for + the template. + (Analyze_Package_Contract): Code cleanup. + * sem_ch10.adb Add with and use clauses for Sem_Ch12. + (Analyze_Compilation_Unit): Capture global references in a + generic subprogram declaration that acts as a compilation unit. + * sem_ch12.adb Add with and use clauses for Sem_Prag. Illustrate + the implementation of generic contracts. Alphabetize various + subprograms. + (Analyze_Generic_Package_Declaration): + Create a generic contract for the template. + (Analyze_Generic_Subprogram_Declaration): Create a generic + contract for the template. + (Analyze_Subprogram_Instantiation): Instantiate the contract of the + subprogram. + (Copy_Generic_Node): Link defining entities of the generic template + with the corresponding defining entities of the generic copy. Update + the processing of pragmas. + (Instantiate_Contract): Removed. + (Instantiate_Subprogram_Contract): New routine. + (Requires_Delayed_Save): New routine. + (Save_Global_References): Rename formal parameter N to Templ. Various + cleanups. + (Save_Global_References_In_Aspects): Moved from the spec. + (Save_Global_References_In_Contract): New routine. + (Save_References_In_Aggregate): New routine. + (Save_References_In_Char_Lit_Or_Op_Symbol): New routine. + (Save_References_In_Descendants): New routine. + (Save_References_In_Identifier): New routine. + (Save_References_In_Operator): New routine. + (Save_References_In_Pragma): New routine. + * sem_ch12.ads (Save_Global_References): Rename formal + parameter N to Templ. Update the comment on usage. + (Save_Global_References_In_Aspects): Moved to the body. + (Save_Global_References_In_Contract): New routine. + * sem_ch13.adb (Analyze_Aspect_Specifications_On_Body_Or_Stub): + New routine. + * sem_ch13.ads (Analyze_Aspect_Specifications_On_Body_Or_Stub): + New routine. + * sem_prag.adb (Add_Item_To_Name_Buffer): Add support for + generic parameters. + (Analyze_Contract_Cases_In_Decl_Part): Code cleanup. + (Analyze_Depends_Global): New routine. + (Analyze_Depends_In_Decl_Part): Code cleanup. + (Analyze_Global_In_Decl_Part): Code cleanup. + (Analyze_Global_Item): Constants are now valid global items. Do + not perform state-related checks in an instance. Change the way + renamings are handled. (Analyze_Initial_Condition_In_Decl_Part): + Code cleanup. + (Analyze_Initializes_In_Decl_Part): Code cleanup. + (Analyze_Input_Output): The analysis of attribute 'Result in + the context of pragmas Depends or Refined_Depends now reuses + the existing attribute analysis machinery. Constants and + generic parameters are now valid dependency items. Do not + perform state-related checks in an instance. Change the way + renamings are handled. (Analyze_Pragma): Add a "characteristics" + section for pragmas Abstract_State, Contract_Cases, Depends, + Extensions_Visible, Global, Initial_Condition, Initializes, + Post, Post_Class, Postcondition, Pre, Pre_Class, Precondition, + Refined_Depends, Refined_Global, Refined_Post, Refined_State, Test_Case. + (Analyze_Pre_Post_Condition): Do not create a generic + template here. + (Analyze_Pre_Post_Condition_In_Decl_Part): Code cleanup. + (Analyze_Refined_Depends_Global_Post): New routine. + (Analyze_Refined_Depends_In_Decl_Part): Code cleanup. + (Analyze_Refined_Global_In_Decl_Part): Code cleanup. + (Analyze_Refined_Pragma): Removed. + (Analyze_Refined_State_In_Decl_Part): Code cleanup. + (Analyze_Test_Case_In_Decl_Part): Code cleanup. + (Check_Dependency_Clause): Do not perform this check in an instance. + (Check_Function_Return): Add support for generic functions. + (Check_In_Out_States): Do not perform this check in an instance. + (Check_Input_States): Do not perform this check in an instance. + (Check_Mode_Restriction_In_Function): Add support for generic functions. + (Check_Output_States): Do not perform this check in an instance. + (Check_Postcondition_Use_In_Inlined_Subprogram): Rename + parameter Subp_Id to Spec_Id and update comment on usage. + (Check_Proof_In_States): Do not perform this check in an instance. + (Check_Refined_Global_Item): Add support for constants. + (Check_Refined_Global_List): Do not perform this check in an instance. + (Collect_Global_Items): Reimplemented. + (Collect_Subprogram_Inputs_Outputs): Add support for generic parameters. + (Create_Generic_Template): Removed. + (Find_Related_Package_Or_Body): Moved to spec. + (Find_Role): Add support for generic parameters and constants. + (Get_Argument): Moved to spec. Rename parameter Spec_Id to Context_Id. + (Match_Item): Add support for constants. + (Preanalyze_Test_Case_Arg): Reimplemented. + (Report_Extra_Clauses): Do not perform this check in an instance. + (Report_Extra_Constituents): Do not perform this check in an instance. + * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update + the comment on usage. + (Find_Related_Package_Or_Body): Moved from body. + (Get_Argument): Moved from body. + * sem_util.adb Add with and use clauses for Sem_Ch12. + (Corresponding_Spec_Of): Add support for packages and package bodies. + (Create_Generic_Contract): New routine. + (Is_Contract_Annotation): Reimplemented. + (Is_Generic_Declaration_Or_Body): New routine. + (Is_Package_Contract_Annotation): New routine. + (Is_Subprogram_Contract_Annotation): New routine. + * sem_util.ads (Corresponding_Spec_Of): Update the comment on usage. + (Create_Generic_Contract): New routine. + (Is_Generic_Declaration_Or_Body): New routine. + (Is_Package_Contract_Annotation): New routine. + (Is_Subprogram_Contract_Annotation): New routine. + * sinfo.adb (Is_Generic_Contract_Pragma): New routine. + (Set_Is_Generic_Contract_Pragma): New routine. + * sinfo.ads Add new attribute Is_Generic_Contract_Pragma along + with occurrences in nodes. + (Is_Generic_Contract_Pragma): New routine along with pragma Inline. + (Set_Is_Generic_Contract_Pragma): New routine along with pragma Inline. + * treepr.adb (Print_Entity_Info): Output fields 36 to 41. + +2015-05-12 Robert Dewar + + * a-taster.ads: Minor comment fix: fix bad header, this is a + pure RM unit. + 2015-05-12 Robert Dewar * sem_intr.adb: (Check_Shift): Diagnose bad modulus value. diff --git a/gcc/ada/a-taster.ads b/gcc/ada/a-taster.ads index 5a496a83e5b..21408b54bbf 100644 --- a/gcc/ada/a-taster.ads +++ b/gcc/ada/a-taster.ads @@ -6,14 +6,10 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2005, Free Software Foundation, Inc. -- --- -- -- This specification is derived from the Ada Reference Manual for use with -- --- GNAT. The copyright notice above, and the license provisions that follow -- --- apply solely to the contents of the part following the private keyword. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- GNAT. In accordance with the copyright of that document, you can freely -- +-- copy and modify this specification, provided that if you redistribute a -- +-- modified version, any changes that you have made are clearly indicated. -- -- -- ------------------------------------------------------------------------------ diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 772195bd424..f364960fe0f 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -70,6 +70,7 @@ package body Einfo is -- Homonym Node4 -- First_Rep_Item Node6 -- Freeze_Node Node7 + -- Associated_Entity Node37 -- The usage of other fields (and the entity kinds to which it applies) -- depends on the particular field (see Einfo spec for details). @@ -88,7 +89,6 @@ package body Einfo is -- Part_Of_Constituents Elist9 -- Renaming_Map Uint9 - -- Encapsulating_State Node10 -- Direct_Primitive_Operations Elist10 -- Discriminal_Link Node10 -- Float_Rep Uint10 (but returns Float_Rep_Kind) @@ -215,10 +215,10 @@ package body Einfo is -- Related_Expression Node24 -- Subps_Index Uint24 - -- Interface_Alias Node25 - -- Interfaces Elist25 -- Debug_Renaming_Link Node25 -- DT_Offset_To_Top_Func Node25 + -- Interface_Alias Node25 + -- Interfaces Elist25 -- PPC_Wrapper Node25 -- Related_Array_Object Node25 -- Static_Discrete_Predicate List25 @@ -253,6 +253,7 @@ package body Einfo is -- Thunk_Entity Node31 -- Activation_Record_Component Node31 + -- Encapsulating_State Node32 -- SPARK_Pragma Node32 -- No_Tagged_Streams_Pragma Node32 @@ -264,7 +265,6 @@ package body Einfo is -- Import_Pragma Node35 -- (unused) Node36 - -- (unused) Node37 -- (unused) Node38 -- (unused) Node39 -- (unused) Node40 @@ -753,6 +753,11 @@ package body Einfo is return Uint14 (Id); end Alignment; + function Associated_Entity (Id : E) return E is + begin + return Node37 (Id); + end Associated_Entity; + function Associated_Formal_Package (Id : E) return E is begin pragma Assert (Ekind (Id) = E_Package); @@ -1111,8 +1116,8 @@ package body Einfo is function Encapsulating_State (Id : E) return N is begin - pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); - return Node10 (Id); + pragma Assert (Ekind_In (Id, E_Abstract_State, E_Constant, E_Variable)); + return Node32 (Id); end Encapsulating_State; function Enclosing_Scope (Id : E) return E is @@ -1176,7 +1181,8 @@ package body Einfo is E_Package, E_Package_Body, E_Subprogram_Body, - E_Variable) + E_Variable, + E_Void) or else Is_Subprogram_Or_Generic_Subprogram (Id)); return Node34 (Id); end Contract; @@ -3558,6 +3564,11 @@ package body Einfo is Set_Elist16 (Id, V); end Set_Access_Disp_Table; + procedure Set_Associated_Entity (Id : E; V : E) is + begin + Set_Node37 (Id, V); + end Set_Associated_Entity; + procedure Set_Associated_Formal_Package (Id : E; V : E) is begin Set_Node12 (Id, V); @@ -3733,13 +3744,13 @@ package body Einfo is begin pragma Assert (Ekind_In (Id, E_Entry, - E_Entry_Family, - E_Generic_Package, - E_Package, - E_Package_Body, - E_Subprogram_Body, - E_Variable, - E_Void) + E_Entry_Family, + E_Generic_Package, + E_Package, + E_Package_Body, + E_Subprogram_Body, + E_Variable, + E_Void) or else Is_Subprogram_Or_Generic_Subprogram (Id)); Set_Node34 (Id, V); end Set_Contract; @@ -3993,8 +4004,8 @@ package body Einfo is procedure Set_Encapsulating_State (Id : E; V : E) is begin - pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); - Set_Node10 (Id, V); + pragma Assert (Ekind_In (Id, E_Abstract_State, E_Constant, E_Variable)); + Set_Node32 (Id, V); end Set_Encapsulating_State; procedure Set_Enclosing_Scope (Id : E; V : E) is @@ -8993,7 +9004,7 @@ package body Einfo is ----------------------- procedure Write_Field6_Name (Id : Entity_Id) is - pragma Warnings (Off, Id); + pragma Unreferenced (Id); begin Write_Str ("First_Rep_Item"); end Write_Field6_Name; @@ -9003,7 +9014,7 @@ package body Einfo is ----------------------- procedure Write_Field7_Name (Id : Entity_Id) is - pragma Warnings (Off, Id); + pragma Unreferenced (Id); begin Write_Str ("Freeze_Node"); end Write_Field7_Name; @@ -9083,10 +9094,6 @@ package body Einfo is procedure Write_Field10_Name (Id : Entity_Id) is begin case Ekind (Id) is - when E_Abstract_State | - E_Variable => - Write_Str ("Encapsulating_State"); - when Class_Wide_Kind | Incomplete_Kind | E_Record_Type | @@ -9095,13 +9102,13 @@ package body Einfo is Concurrent_Kind => Write_Str ("Direct_Primitive_Operations"); - when Float_Kind => - Write_Str ("Float_Rep"); - when E_In_Parameter | E_Constant => Write_Str ("Discriminal_Link"); + when Float_Kind => + Write_Str ("Float_Rep"); + when E_Function | E_Package | E_Package_Body | @@ -9995,6 +10002,11 @@ package body Einfo is procedure Write_Field32_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Abstract_State | + E_Constant | + E_Variable => + Write_Str ("Encapsulating_State"); + when E_Function | E_Generic_Function | E_Generic_Package | @@ -10050,6 +10062,7 @@ package body Einfo is E_Package_Body | E_Subprogram_Body | E_Variable | + E_Void | Generic_Subprogram_Kind | Subprogram_Kind => Write_Str ("Contract"); @@ -10091,11 +10104,9 @@ package body Einfo is ------------------------ procedure Write_Field37_Name (Id : Entity_Id) is + pragma Unreferenced (Id); begin - case Ekind (Id) is - when others => - Write_Str ("Field37??"); - end case; + Write_Str ("Associated_Entity"); end Write_Field37_Name; ------------------------ diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index d752a1ed5aa..b9b5c42d846 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -436,6 +436,13 @@ package Einfo is -- definition clause with an (obsolescent) mod clause is converted -- into an attribute definition clause for this purpose. +-- Associated_Entity (Node37) +-- Defined in all entities. This field is similar to Associated_Node, but +-- applied to entities. The attribute links an entity from the generic +-- template with its corresponding entity in the analyzed generic copy. +-- The global references mechanism relies on the Associated_Entity to +-- infer the context. + -- Associated_Formal_Package (Node12) -- Defined in packages that are the actuals of formal_packages. Points -- to the entity in the declaration for the formal package. @@ -882,7 +889,6 @@ package Einfo is -- primitives that come from source must be stored in this list in the -- order of their occurrence in the sources. For incomplete types the -- list is always empty. --- -- When expansion is disabled the corresponding record type of a -- synchronized type is not constructed. In that case, such types -- carry this attribute directly, for ASIS use. @@ -1033,9 +1039,10 @@ package Einfo is -- then if there is no other elaboration code, obviously there is no -- need to set the flag. --- Encapsulating_State (Node10) --- Defined in abstract states and variables. Contains the entity of an --- ancestor state whose refinement utilizes this item as a constituent. +-- Encapsulating_State (Node32) +-- Defined in abstract states, constants and variables. Contains the +-- entity of an ancestor state whose refinement utilizes this item as +-- a constituent. -- Enclosing_Scope (Node18) -- Defined in labels. Denotes the innermost enclosing construct that @@ -1089,10 +1096,10 @@ package Einfo is -- 'COUNT when it applies to a family member. -- Contract (Node34) --- Defined in entry, entry family, package, package body, subprogram and --- subprogram body entities as well as their respective generic forms. A --- contract is also applicable to a variable. Points to the contract of --- the entity, holding various assertion items and data classifiers. +-- Defined in entry, entry family, [generic] package, package body, +-- [generic] subprogram, subprogram body and variable entities. Points +-- to the contract of the entity, holding various assertion items and +-- data classifiers. -- Entry_Parameters_Type (Node15) -- Defined in entries. Points to the access-to-record type that is @@ -1657,7 +1664,7 @@ package Einfo is -- Has_Inherited_Default_Init_Cond (Flag133) -- Defined in type and subtype entities. Set if a derived type inherits -- pragma Default_Initial_Condition from its parent type. This flag must --- be mutually exclusive with Had_Default_Init_Cond. +-- be mutually exclusive with Has_Default_Init_Cond. -- Has_Initial_Value (Flag219) -- Defined in entities for variables and out parameters. Set if there @@ -5238,6 +5245,7 @@ package Einfo is -- Etype (Node5) -- First_Rep_Item (Node6) -- Freeze_Node (Node7) + -- Associated_Entity (Node37) -- Address_Taken (Flag104) -- Can_Never_Be_Null (Flag38) @@ -5454,9 +5462,9 @@ package Einfo is -- E_Abstract_State -- Refinement_Constituents (Elist8) -- Part_Of_Constituents (Elist9) - -- Encapsulating_State (Node10) -- Body_References (Elist16) -- Non_Limited_View (Node19) + -- Encapsulating_State (Node32) -- From_Limited_With (Flag159) -- Has_Visible_Refinement (Flag263) -- Has_Non_Limited_View (synth) @@ -5615,6 +5623,7 @@ package Einfo is -- BIP_Initialization_Call (Node29) -- Last_Aggregate_Assignment (Node30) -- Activation_Record_Component (Node31) + -- Encapsulating_State (Node32) (constants only) -- Linker_Section_Pragma (Node33) -- Has_Alignment_Clause (Flag46) -- Has_Atomic_Components (Flag86) @@ -5964,7 +5973,6 @@ package Einfo is -- Alias (Node18) -- Extra_Accessibility_Of_Result (Node19) -- Last_Entity (Node20) - -- Has_Nested_Subprogram (Flag282) -- Subps_Index (Uint24) -- Overridden_Operation (Node26) -- Subprograms_For_Type (Node29) @@ -5972,6 +5980,7 @@ package Einfo is -- Contract (Node34) -- Import_Pragma (Node35) -- Has_Invariants (Flag232) + -- Has_Nested_Subprogram (Flag282) -- Is_Machine_Code_Subprogram (Flag137) -- Is_Pure (Flag44) -- Is_Intrinsic_Subprogram (Flag64) @@ -6017,8 +6026,8 @@ package Einfo is -- Package_Instantiation (Node26) -- Current_Use_Clause (Node27) -- Finalizer (Node28) (non-generic case only) - -- SPARK_Aux_Pragma (Node33) -- SPARK_Pragma (Node32) + -- SPARK_Aux_Pragma (Node33) -- Contract (Node34) -- Delay_Subprogram_Descriptors (Flag50) -- Body_Needed_For_SAL (Flag40) @@ -6054,8 +6063,8 @@ package Einfo is -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) -- Finalizer (Node28) (non-generic case only) - -- SPARK_Aux_Pragma (Node33) -- SPARK_Pragma (Node32) + -- SPARK_Aux_Pragma (Node33) -- Contract (Node34) -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Subprogram_Descriptors (Flag50) @@ -6325,7 +6334,6 @@ package Einfo is -- E_Variable -- Hiding_Loop_Variable (Node8) -- Current_Value (Node9) - -- Encapsulating_State (Node10) -- Esize (Uint12) -- Extra_Accessibility (Node13) -- Alignment (Uint14) @@ -6346,6 +6354,7 @@ package Einfo is -- BIP_Initialization_Call (Node29) -- Last_Aggregate_Assignment (Node30) -- Activation_Record_Component (Node31) + -- Encapsulating_State (Node32) -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Has_Alignment_Clause (Flag46) @@ -6616,6 +6625,7 @@ package Einfo is function Address_Taken (Id : E) return B; function Alias (Id : E) return E; function Alignment (Id : E) return U; + function Associated_Entity (Id : E) return E; function Associated_Formal_Package (Id : E) return E; function Associated_Node_For_Itype (Id : E) return N; function Associated_Storage_Pool (Id : E) return E; @@ -7267,6 +7277,7 @@ package Einfo is procedure Set_Address_Taken (Id : E; V : B := True); procedure Set_Alias (Id : E; V : E); procedure Set_Alignment (Id : E; V : U); + procedure Set_Associated_Entity (Id : E; V : E); procedure Set_Associated_Formal_Package (Id : E; V : E); procedure Set_Associated_Node_For_Itype (Id : E; V : N); procedure Set_Associated_Storage_Pool (Id : E; V : E); @@ -8039,6 +8050,7 @@ package Einfo is pragma Inline (Address_Taken); pragma Inline (Alias); pragma Inline (Alignment); + pragma Inline (Associated_Entity); pragma Inline (Associated_Formal_Package); pragma Inline (Associated_Node_For_Itype); pragma Inline (Associated_Storage_Pool); @@ -8537,6 +8549,7 @@ package Einfo is pragma Inline (Set_Address_Taken); pragma Inline (Set_Alias); pragma Inline (Set_Alignment); + pragma Inline (Set_Associated_Entity); pragma Inline (Set_Associated_Formal_Package); pragma Inline (Set_Associated_Node_For_Itype); pragma Inline (Set_Associated_Storage_Pool); diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads index bd22e45ef77..5d1c5bb7278 100644 --- a/gcc/ada/inline.ads +++ b/gcc/ada/inline.ads @@ -169,6 +169,16 @@ package Inline is -- enabled and the subprogram contains a construct that cannot be inlined, -- the problematic construct is flagged accordingly. + function Can_Be_Inlined_In_GNATprove_Mode + (Spec_Id : Entity_Id; + Body_Id : Entity_Id) return Boolean; + -- Returns True if the subprogram identified by Spec_Id and Body_Id can + -- be inlined in GNATprove mode. One but not both of Spec_Id and Body_Id + -- can be Empty. Body_Id is Empty when doing a partial check on a call + -- to a subprogram whose body has not been seen yet, to know whether this + -- subprogram could possibly be inlined. GNATprove relies on this to adapt + -- its treatment of the subprogram. + procedure Cannot_Inline (Msg : String; N : Node_Id; @@ -251,14 +261,4 @@ package Inline is -- If an instantiation appears in unreachable code, delete the pending -- body instance. - function Can_Be_Inlined_In_GNATprove_Mode - (Spec_Id : Entity_Id; - Body_Id : Entity_Id) return Boolean; - -- Returns True if the subprogram identified by Spec_Id and Body_Id can - -- be inlined in GNATprove mode. One but not both of Spec_Id and Body_Id - -- can be Empty. Body_Id is Empty when doing a partial check on a call - -- to a subprogram whose body has not been seen yet, to know whether this - -- subprogram could possibly be inlined. GNATprove relies on this to adapt - -- its treatment of the subprogram. - end Inline; diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 16cbccfb166..7a15789c2e4 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1295,6 +1295,14 @@ package body Sem_Attr is elsif Prag_Nam = Name_Contract_Cases then Check_Placement_In_Contract_Cases (Prag); + -- Attribute 'Result is allowed to appear in aspect or pragma + -- [Refined_]Depends (SPARK RM 6.1.5(11)). + + elsif Nam_In (Prag_Nam, Name_Depends, Name_Refined_Depends) + and then Aname = Name_Result + then + null; + elsif Nam_In (Prag_Nam, Name_Post, Name_Post_Class, Name_Postcondition, @@ -5123,17 +5131,21 @@ package body Sem_Attr is elsif Nkind (Subp_Spec) = N_Function_Specification and then Present (Generic_Parent (Subp_Spec)) - and then Ekind (Pref_Id) = E_Function - and then Present (Alias (Pref_Id)) - and then Alias (Pref_Id) = Spec_Id + and then Ekind_In (Pref_Id, E_Generic_Function, E_Function) then - return True; + if Generic_Parent (Subp_Spec) = Pref_Id then + return True; + + elsif Present (Alias (Pref_Id)) + and then Alias (Pref_Id) = Spec_Id + then + return True; + end if; + end if; -- Otherwise the prefix does not denote the related subprogram - else - return False; - end if; + return False; end Denote_Same_Function; -- Local variables @@ -5199,6 +5211,15 @@ package body Sem_Attr is if Ekind_In (Pref_Id, E_Function, E_Generic_Function) then if Denote_Same_Function (Pref_Id, Spec_Id) then + + -- Correct the prefix of the attribute when the context + -- is a generic function. + + if Pref_Id /= Spec_Id then + Rewrite (P, New_Occurrence_Of (Spec_Id, Loc)); + Analyze (P); + end if; + Set_Etype (N, Etype (Spec_Id)); -- Otherwise the prefix denotes some unrelated function diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 9f68d15123f..63d2cb75542 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -53,6 +53,7 @@ with Sem_Ch3; use Sem_Ch3; with Sem_Ch6; use Sem_Ch6; with Sem_Ch7; use Sem_Ch7; with Sem_Ch8; use Sem_Ch8; +with Sem_Ch12; use Sem_Ch12; with Sem_Dist; use Sem_Dist; with Sem_Prag; use Sem_Prag; with Sem_Util; use Sem_Util; @@ -939,6 +940,15 @@ package body Sem_Ch10 is N_Subprogram_Declaration) then Analyze_Subprogram_Contract (Defining_Entity (Unit_Node)); + + -- Capture all global references in a generic subprogram that acts as + -- a compilation unit now that the contract has been analyzed. + + if Is_Generic_Declaration_Or_Body (Unit_Node) then + Save_Global_References_In_Contract + (Templ => Original_Node (Unit_Node), + Gen_Id => Defining_Entity (Unit_Node)); + end if; end if; -- Generate distribution stubs if requested and no error diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index b362362e70d..cac9db9cbf3 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -59,6 +59,7 @@ with Sem_Disp; use Sem_Disp; with Sem_Elab; use Sem_Elab; with Sem_Elim; use Sem_Elim; with Sem_Eval; use Sem_Eval; +with Sem_Prag; use Sem_Prag; with Sem_Res; use Sem_Res; with Sem_Type; use Sem_Type; with Sem_Util; use Sem_Util; @@ -239,6 +240,118 @@ package body Sem_Ch12 is -- circularity is detected, and used to abandon compilation after the -- messages have been posted. + ----------------------------------------- + -- Implementation of Generic Contracts -- + ----------------------------------------- + + -- A "contract" is a collection of aspects and pragmas that either verify a + -- property of a construct at runtime or classify the data flow to and from + -- the construct in some fashion. + + -- Generic packages, subprograms and their respective bodies may be subject + -- to the following contract-related aspects or pragmas collectively known + -- as annotations: + + -- package subprogram [body] + -- Abstract_State Contract_Cases + -- Initial_Condition Depends + -- Initializes Extensions_Visible + -- Global + -- package body Post + -- Refined_State Post_Class + -- Postcondition + -- Pre + -- Pre_Class + -- Precondition + -- Refined_Depends + -- Refined_Global + -- Refined_Post + -- Test_Case + + -- Most package contract annotations utilize forward references to classify + -- data declared within the package [body]. Subprogram annotations then use + -- the classifications to further refine them. These inter dependencies are + -- problematic with respect to the implementation of generics because their + -- analysis, capture of global references and instantiation does not mesh + -- well with the existing mechanism. + + -- 1) Analysis of generic contracts is carried out the same way non-generic + -- contracts are analyzed: + + -- 1.1) General rule - a contract is analyzed after all related aspects + -- and pragmas are analyzed. This is done by routines + + -- Analyze_Package_Body_Contract + -- Analyze_Package_Contract + -- Analyze_Subprogram_Body_Contract + -- Analyze_Subprogram_Contract + + -- 1.2) Compilation unit - the contract is analyzed after Pragmas_After + -- are processed. + + -- 1.3) Compilation unit body - the contract is analyzed at the end of + -- the body declaration list. + + -- 1.4) Package - the contract is analyzed at the end of the private or + -- visible declarations, prior to analyzing the contracts of any nested + -- packages or subprograms. + + -- 1.5) Package body - the contract is analyzed at the end of the body + -- declaration list, prior to analyzing the contracts of any nested + -- packages or subprograms. + + -- 1.6) Subprogram - if the subprogram is declared inside a block, a + -- package or a subprogram, then its contract is analyzed at the end of + -- the enclosing declarations, otherwise the subprogram is a compilation + -- unit 1.2). + + -- 1.7) Subprogram body - if the subprogram body is declared inside a + -- block, a package body or a subprogram body, then its contract is + -- analyzed at the end of the enclosing declarations, otherwise the + -- subprogram is a compilation unit 1.3). + + -- 2) Capture of global references within contracts is done after capturing + -- global references within the generic template. There are two reasons for + -- this delay - pragma annotations are not part of the generic template in + -- the case of a generic subprogram declaration, and analysis of contracts + -- is delayed. + + -- Contract-related source pragmas within generic templates are prepared + -- for delayed capture of global references by routine + + -- Create_Generic_Contract + + -- The routine associates these pragmas with the contract of the template. + -- In the case of a generic subprogram declaration, the routine creates + -- generic templates for the pragmas declared after the subprogram because + -- they are not part of the template. + + -- generic -- template starts + -- procedure Gen_Proc (Input : Integer); -- template ends + -- pragma Precondition (Input > 0); -- requires own template + + -- 2.1) The capture of global references with aspect specifications and + -- source pragmas that apply to a generic unit must be suppressed when + -- the generic template is being processed because the contracts have not + -- been analyzed yet. Any attempts to capture global references at that + -- point will destroy the Associated_Node linkages and leave the template + -- undecorated. This delay is controlled by routine + + -- Requires_Delayed_Save + + -- 2.2) The real capture of global references within a contract is done + -- after the contract has been analyzed, by routine + + -- Save_Global_References_In_Contract + + -- 3) The instantiation of a generic contract occurs as part of the + -- instantiation of the contract owner. Generic subprogram declarations + -- require additional processing when the contract is specified by pragmas + -- because the pragmas are not part of the generic template. This is done + -- by routine + + -- Instantiate_Subprogram_Contract + Circularity_Detected : Boolean := False; -- This should really be reset on encountering a new main unit, but in -- practice we are not using multiple main units so it is not critical. @@ -476,6 +589,74 @@ package body Sem_Ch12 is -- packages, and the prefix of the formal type may be needed to resolve -- the ambiguity in the instance ??? + procedure Freeze_Subprogram_Body + (Inst_Node : Node_Id; + Gen_Body : Node_Id; + Pack_Id : Entity_Id); + -- The generic body may appear textually after the instance, including + -- in the proper body of a stub, or within a different package instance. + -- Given that the instance can only be elaborated after the generic, we + -- place freeze_nodes for the instance and/or for packages that may enclose + -- the instance and the generic, so that the back-end can establish the + -- proper order of elaboration. + + function Get_Associated_Node (N : Node_Id) return Node_Id; + -- In order to propagate semantic information back from the analyzed copy + -- to the original generic, we maintain links between selected nodes in the + -- generic and their corresponding copies. At the end of generic analysis, + -- the routine Save_Global_References traverses the generic tree, examines + -- the semantic information, and preserves the links to those nodes that + -- contain global information. At instantiation, the information from the + -- associated node is placed on the new copy, so that name resolution is + -- not repeated. + -- + -- Three kinds of source nodes have associated nodes: + -- + -- a) those that can reference (denote) entities, that is identifiers, + -- character literals, expanded_names, operator symbols, operators, + -- and attribute reference nodes. These nodes have an Entity field + -- and are the set of nodes that are in N_Has_Entity. + -- + -- b) aggregates (N_Aggregate and N_Extension_Aggregate) + -- + -- c) selected components (N_Selected_Component) + -- + -- For the first class, the associated node preserves the entity if it is + -- global. If the generic contains nested instantiations, the associated + -- node itself has been recopied, and a chain of them must be followed. + -- + -- For aggregates, the associated node allows retrieval of the type, which + -- may otherwise not appear in the generic. The view of this type may be + -- different between generic and instantiation, and the full view can be + -- installed before the instantiation is analyzed. For aggregates of type + -- extensions, the same view exchange may have to be performed for some of + -- the ancestor types, if their view is private at the point of + -- instantiation. + -- + -- Nodes that are selected components in the parse tree may be rewritten + -- as expanded names after resolution, and must be treated as potential + -- entity holders, which is why they also have an Associated_Node. + -- + -- Nodes that do not come from source, such as freeze nodes, do not appear + -- in the generic tree, and need not have an associated node. + -- + -- The associated node is stored in the Associated_Node field. Note that + -- this field overlaps Entity, which is fine, because the whole point is + -- that we don't need or want the normal Entity field in this situation. + + function Has_Been_Exchanged (E : Entity_Id) return Boolean; + -- Traverse the Exchanged_Views list to see if a type was private + -- and has already been flipped during this phase of instantiation. + + procedure Hide_Current_Scope; + -- When instantiating a generic child unit, the parent context must be + -- present, but the instance and all entities that may be generated + -- must be inserted in the current scope. We leave the current scope + -- on the stack, but make its entities invisible to avoid visibility + -- problems. This is reversed at the end of the instantiation. This is + -- not done for the instantiation of the bodies, which only require the + -- instances of the generic parents to be in scope. + function In_Same_Declarative_Part (F_Node : Node_Id; Inst : Node_Id) return Boolean; @@ -492,32 +673,31 @@ package body Sem_Ch12 is -- Used to determine whether its body should be elaborated to allow -- front-end inlining. - procedure Set_Instance_Env - (Gen_Unit : Entity_Id; - Act_Unit : Entity_Id); - -- Save current instance on saved environment, to be used to determine - -- the global status of entities in nested instances. Part of Save_Env. - -- called after verifying that the generic unit is legal for the instance, - -- The procedure also examines whether the generic unit is a predefined - -- unit, in order to set configuration switches accordingly. As a result - -- the procedure must be called after analyzing and freezing the actuals. + procedure Inherit_Context (Gen_Decl : Node_Id; Inst : Node_Id); + -- Add the context clause of the unit containing a generic unit to a + -- compilation unit that is, or contains, an instantiation. - procedure Set_Instance_Of (A : Entity_Id; B : Entity_Id); - -- Associate analyzed generic parameter with corresponding - -- instance. Used for semantic checks at instantiation time. + procedure Init_Env; + -- Establish environment for subsequent instantiation. Separated from + -- Save_Env because data-structures for visibility handling must be + -- initialized before call to Check_Generic_Child_Unit. - function Has_Been_Exchanged (E : Entity_Id) return Boolean; - -- Traverse the Exchanged_Views list to see if a type was private - -- and has already been flipped during this phase of instantiation. + procedure Inline_Instance_Body + (N : Node_Id; + Gen_Unit : Entity_Id; + Act_Decl : Node_Id); + -- If front-end inlining is requested, instantiate the package body, + -- and preserve the visibility of its compilation unit, to insure + -- that successive instantiations succeed. - procedure Hide_Current_Scope; - -- When instantiating a generic child unit, the parent context must be - -- present, but the instance and all entities that may be generated - -- must be inserted in the current scope. We leave the current scope - -- on the stack, but make its entities invisible to avoid visibility - -- problems. This is reversed at the end of the instantiation. This is - -- not done for the instantiation of the bodies, which only require the - -- instances of the generic parents to be in scope. + procedure Insert_Freeze_Node_For_Instance + (N : Node_Id; + F_Node : Node_Id); + -- N denotes a package or a subprogram instantiation and F_Node is the + -- associated freeze node. Insert the freeze node before the first source + -- body which follows immediately after N. If no such body is found, the + -- freeze node is inserted at the end of the declarative region which + -- contains N. procedure Install_Body (Act_Body : Node_Id; @@ -534,46 +714,11 @@ package body Sem_Ch12 is -- of packages that are early instantiations are delayed, and their freeze -- node appears after the generic body. - procedure Insert_Freeze_Node_For_Instance - (N : Node_Id; - F_Node : Node_Id); - -- N denotes a package or a subprogram instantiation and F_Node is the - -- associated freeze node. Insert the freeze node before the first source - -- body which follows immediately after N. If no such body is found, the - -- freeze node is inserted at the end of the declarative region which - -- contains N. - - procedure Freeze_Subprogram_Body - (Inst_Node : Node_Id; - Gen_Body : Node_Id; - Pack_Id : Entity_Id); - -- The generic body may appear textually after the instance, including - -- in the proper body of a stub, or within a different package instance. - -- Given that the instance can only be elaborated after the generic, we - -- place freeze_nodes for the instance and/or for packages that may enclose - -- the instance and the generic, so that the back-end can establish the - -- proper order of elaboration. - - procedure Init_Env; - -- Establish environment for subsequent instantiation. Separated from - -- Save_Env because data-structures for visibility handling must be - -- initialized before call to Check_Generic_Child_Unit. - procedure Install_Formal_Packages (Par : Entity_Id); -- Install the visible part of any formal of the parent that is a formal -- package. Note that for the case of a formal package with a box, this -- includes the formal part of the formal package (12.7(10/2)). - procedure Install_Parent (P : Entity_Id; In_Body : Boolean := False); - -- When compiling an instance of a child unit the parent (which is - -- itself an instance) is an enclosing scope that must be made - -- immediately visible. This procedure is also used to install the non- - -- generic parent of a generic child unit when compiling its body, so - -- that full views of types in the parent are made visible. - - procedure Remove_Parent (In_Body : Boolean := False); - -- Reverse effect after instantiation of child is complete - procedure Install_Hidden_Primitives (Prims_List : in out Elist_Id; Gen_T : Entity_Id; @@ -582,17 +727,12 @@ package body Sem_Ch12 is -- visibility of primitives of Gen_T. The list of primitives to which -- the suffix is removed is added to Prims_List to restore them later. - procedure Restore_Hidden_Primitives (Prims_List : in out Elist_Id); - -- Restore suffix 'P' to primitives of Prims_List and leave Prims_List - -- set to No_Elist. - - procedure Inline_Instance_Body - (N : Node_Id; - Gen_Unit : Entity_Id; - Act_Decl : Node_Id); - -- If front-end inlining is requested, instantiate the package body, - -- and preserve the visibility of its compilation unit, to insure - -- that successive instantiations succeed. + procedure Install_Parent (P : Entity_Id; In_Body : Boolean := False); + -- When compiling an instance of a child unit the parent (which is + -- itself an instance) is an enclosing scope that must be made + -- immediately visible. This procedure is also used to install the non- + -- generic parent of a generic child unit when compiling its body, so + -- that full views of types in the parent are made visible. -- The functions Instantiate_XXX perform various legality checks and build -- the declarations for instantiated generic parameters. In all of these @@ -662,54 +802,6 @@ package body Sem_Ch12 is -- instances in the current declarative part that precede the one being -- loaded. In that case a missing body is acceptable. - procedure Inherit_Context (Gen_Decl : Node_Id; Inst : Node_Id); - -- Add the context clause of the unit containing a generic unit to a - -- compilation unit that is, or contains, an instantiation. - - function Get_Associated_Node (N : Node_Id) return Node_Id; - -- In order to propagate semantic information back from the analyzed copy - -- to the original generic, we maintain links between selected nodes in the - -- generic and their corresponding copies. At the end of generic analysis, - -- the routine Save_Global_References traverses the generic tree, examines - -- the semantic information, and preserves the links to those nodes that - -- contain global information. At instantiation, the information from the - -- associated node is placed on the new copy, so that name resolution is - -- not repeated. - -- - -- Three kinds of source nodes have associated nodes: - -- - -- a) those that can reference (denote) entities, that is identifiers, - -- character literals, expanded_names, operator symbols, operators, - -- and attribute reference nodes. These nodes have an Entity field - -- and are the set of nodes that are in N_Has_Entity. - -- - -- b) aggregates (N_Aggregate and N_Extension_Aggregate) - -- - -- c) selected components (N_Selected_Component) - -- - -- For the first class, the associated node preserves the entity if it is - -- global. If the generic contains nested instantiations, the associated - -- node itself has been recopied, and a chain of them must be followed. - -- - -- For aggregates, the associated node allows retrieval of the type, which - -- may otherwise not appear in the generic. The view of this type may be - -- different between generic and instantiation, and the full view can be - -- installed before the instantiation is analyzed. For aggregates of type - -- extensions, the same view exchange may have to be performed for some of - -- the ancestor types, if their view is private at the point of - -- instantiation. - -- - -- Nodes that are selected components in the parse tree may be rewritten - -- as expanded names after resolution, and must be treated as potential - -- entity holders, which is why they also have an Associated_Node. - -- - -- Nodes that do not come from source, such as freeze nodes, do not appear - -- in the generic tree, and need not have an associated node. - -- - -- The associated node is stored in the Associated_Node field. Note that - -- this field overlaps Entity, which is fine, because the whole point is - -- that we don't need or want the normal Entity field in this situation. - procedure Map_Formal_Package_Entities (Form : Entity_Id; Act : Entity_Id); -- Within the generic part, entities in the formal package are -- visible. To validate subsequent type declarations, indicate @@ -739,6 +831,31 @@ package body Sem_Ch12 is -- before installing parents of generics, that are not visible for the -- actuals themselves. + procedure Remove_Parent (In_Body : Boolean := False); + -- Reverse effect after instantiation of child is complete + + procedure Restore_Hidden_Primitives (Prims_List : in out Elist_Id); + -- Restore suffix 'P' to primitives of Prims_List and leave Prims_List + -- set to No_Elist. + + procedure Save_Global_References_In_Aspects (N : Node_Id); + -- Save all global references found within the expressions of all aspects + -- that appear on node N. + + procedure Set_Instance_Env + (Gen_Unit : Entity_Id; + Act_Unit : Entity_Id); + -- Save current instance on saved environment, to be used to determine + -- the global status of entities in nested instances. Part of Save_Env. + -- called after verifying that the generic unit is legal for the instance, + -- The procedure also examines whether the generic unit is a predefined + -- unit, in order to set configuration switches accordingly. As a result + -- the procedure must be called after analyzing and freezing the actuals. + + procedure Set_Instance_Of (A : Entity_Id; B : Entity_Id); + -- Associate analyzed generic parameter with corresponding instance. Used + -- for semantic checks at instantiation time. + function True_Parent (N : Node_Id) return Node_Id; -- For a subunit, return parent of corresponding stub, else return -- parent of node. @@ -2305,10 +2422,11 @@ package body Sem_Ch12 is (Specification (Original_Node (Gen_Decl)), Empty, Instantiating => True)); - Renaming := Make_Package_Renaming_Declaration (Loc, + Renaming := + Make_Package_Renaming_Declaration (Loc, Defining_Unit_Name => Make_Defining_Identifier (Loc, Chars (Gen_Unit)), - Name => New_Occurrence_Of (Formal, Loc)); + Name => New_Occurrence_Of (Formal, Loc)); if Nkind (Gen_Id) = N_Identifier and then Chars (Gen_Id) = Chars (Pack_Id) @@ -3064,6 +3182,13 @@ package body Sem_Ch12 is -- do the same for their respective aspect specifications. Exchange_Aspects (N, New_N); + + -- Collect all contract-related source pragmas found within the template + -- and attach them to the contract of the package spec. This contract is + -- used in the capture of global references within annotations. + + Create_Generic_Contract (N); + Id := Defining_Entity (N); Generate_Definition (Id); @@ -3201,6 +3326,12 @@ package body Sem_Ch12 is Exchange_Aspects (N, New_N); + -- Collect all contract-related source pragmas found within the template + -- and attach them to the contract of the subprogram spec. This contract + -- is used in the capture of global references within annotations. + + Create_Generic_Contract (N); + Spec := Specification (N); Id := Defining_Entity (Spec); Generate_Definition (Id); @@ -4620,9 +4751,10 @@ package body Sem_Ch12 is -- aspects that appear in the generic. This renaming declaration is -- inserted after the instance declaration which it renames. - procedure Instantiate_Contract (Subp_Id : Entity_Id); - -- Instantiate all source pragmas found in the contract of subprogram - -- Subp_Id. The instantiated pragmas are added to list Renaming_List. + procedure Instantiate_Subprogram_Contract (Templ : Node_Id); + -- Instantiate all source pragmas found in the contract of the generic + -- subprogram declaration template denoted by Templ. The instantiated + -- pragmas are added to list Renaming_List. ------------------------------------ -- Analyze_Instance_And_Renamings -- @@ -4825,11 +4957,11 @@ package body Sem_Ch12 is end if; end Build_Subprogram_Renaming; - -------------------------- - -- Instantiate_Contract -- - -------------------------- + ------------------------------------- + -- Instantiate_Subprogram_Contract -- + ------------------------------------- - procedure Instantiate_Contract (Subp_Id : Entity_Id) is + procedure Instantiate_Subprogram_Contract (Templ : Node_Id) is procedure Instantiate_Pragmas (First_Prag : Node_Id); -- Instantiate all contract-related source pragmas found in the list -- starting with pragma First_Prag. Each instantiated pragma is added @@ -4846,18 +4978,9 @@ package body Sem_Ch12 is begin Prag := First_Prag; while Present (Prag) loop - if Comes_From_Source (Prag) - and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases, - Name_Depends, - Name_Extensions_Visible, - Name_Global, - Name_Postcondition, - Name_Precondition, - Name_Test_Case) - then + if Is_Generic_Contract_Pragma (Prag) then Inst_Prag := - Copy_Generic_Node - (Original_Node (Prag), Empty, Instantiating => True); + Copy_Generic_Node (Prag, Empty, Instantiating => True); Set_Analyzed (Inst_Prag, False); Append_To (Renaming_List, Inst_Prag); @@ -4869,9 +4992,9 @@ package body Sem_Ch12 is -- Local variables - Items : constant Node_Id := Contract (Subp_Id); + Items : constant Node_Id := Contract (Defining_Entity (Templ)); - -- Start of processing for Instantiate_Contract + -- Start of processing for Instantiate_Subprogram_Contract begin if Present (Items) then @@ -4879,7 +5002,7 @@ package body Sem_Ch12 is Instantiate_Pragmas (Contract_Test_Cases (Items)); Instantiate_Pragmas (Classifications (Items)); end if; - end Instantiate_Contract; + end Instantiate_Subprogram_Contract; -- Local variables @@ -5046,7 +5169,12 @@ package body Sem_Ch12 is end if; Append (Act_Decl, Renaming_List); - Instantiate_Contract (Gen_Unit); + + -- Contract-related source pragmas that follow a generic subprogram + -- must be instantiated explicitly because they are not part of the + -- subprogram template. + + Instantiate_Subprogram_Contract (Original_Node (Gen_Decl)); Build_Subprogram_Renaming; Analyze_Instance_And_Renamings; @@ -6888,7 +7016,6 @@ package body Sem_Ch12 is ---------------------- procedure Copy_Descendants is - use Atree.Unchecked_Access; -- This code section is part of the implementation of an untyped -- tree traversal, so it needs direct access to node fields. @@ -6987,11 +7114,12 @@ package body Sem_Ch12 is function In_Defining_Unit_Name (Nam : Node_Id) return Boolean is begin - return Present (Parent (Nam)) - and then (Nkind (Parent (Nam)) = N_Defining_Program_Unit_Name - or else - (Nkind (Parent (Nam)) = N_Expanded_Name - and then In_Defining_Unit_Name (Parent (Nam)))); + return + Present (Parent (Nam)) + and then (Nkind (Parent (Nam)) = N_Defining_Program_Unit_Name + or else + (Nkind (Parent (Nam)) = N_Expanded_Name + and then In_Defining_Unit_Name (Parent (Nam)))); end In_Defining_Unit_Name; -- Start of processing for Copy_Generic_Node @@ -7019,17 +7147,12 @@ package body Sem_Ch12 is Set_Parent (New_N, Parent_Id); end if; - -- If defining identifier, then all fields have been copied already - - if Nkind (New_N) in N_Entity then - null; - -- Special casing for identifiers and other entity names and operators - elsif Nkind_In (New_N, N_Identifier, - N_Character_Literal, - N_Expanded_Name, - N_Operator_Symbol) + if Nkind_In (New_N, N_Character_Literal, + N_Expanded_Name, + N_Identifier, + N_Operator_Symbol) or else Nkind (New_N) in N_Op then if not Instantiating then @@ -7160,6 +7283,19 @@ package body Sem_Ch12 is end if; end if; + -- Establish a link between an entity from the generic template and the + -- corresponding entity in the generic copy to be analyzed. + + elsif Nkind (N) in N_Entity then + if not Instantiating then + Set_Associated_Entity (N, New_N); + end if; + + -- Clear any existing link the copy may inherit from the replicated + -- generic template entity. + + Set_Associated_Entity (New_N, Empty); + -- Special casing for stubs elsif Nkind (N) in N_Body_Stub then @@ -7432,19 +7568,24 @@ package body Sem_Ch12 is S_Adjustment := Save_Adjustment; end; - -- Don't copy Ident or Comment pragmas, since the comment belongs to the - -- generic unit, not to the instantiating unit. - elsif Nkind (N) = N_Pragma and then Instantiating then - declare - Prag_Id : constant Pragma_Id := Get_Pragma_Id (N); - begin - if Prag_Id = Pragma_Ident or else Prag_Id = Pragma_Comment then - New_N := Make_Null_Statement (Sloc (N)); - else - Copy_Descendants; - end if; - end; + + -- Do not copy Comment or Ident pragmas their content is relevant to + -- the generic unit, not to the instantiating unit. + + if Nam_In (Pragma_Name (N), Name_Comment, Name_Ident) then + New_N := Make_Null_Statement (Sloc (N)); + + -- Do not copy pragmas generated from aspects because the pragmas do + -- not carry any semantic information, plus they will be regenerated + -- in the instance. + + elsif From_Aspect_Specification (N) then + New_N := Make_Null_Statement (Sloc (N)); + + else + Copy_Descendants; + end if; elsif Nkind_In (N, N_Integer_Literal, N_Real_Literal) then @@ -13516,10 +13657,18 @@ package body Sem_Ch12 is -- Save_Global_References -- ---------------------------- - procedure Save_Global_References (N : Node_Id) is + procedure Save_Global_References (Templ : Node_Id) is + + -- ??? it is horrible to use global variables in highly recursive code + + E : Entity_Id; + -- The entity of the current associated node + Gen_Scope : Entity_Id; - E : Entity_Id; - N2 : Node_Id; + -- The scope of the generic for which references are being saved + + N2 : Node_Id; + -- The current associated node function Is_Global (E : Entity_Id) return Boolean; -- Check whether entity is defined outside of generic unit. Examine the @@ -13548,7 +13697,7 @@ package body Sem_Ch12 is -- nodes. N can also be a character literal, identifier, or operator -- symbol node, but the call has no effect in these cases. - procedure Save_Global_Defaults (N1, N2 : Node_Id); + procedure Save_Global_Defaults (N1 : Node_Id; N2 : Node_Id); -- Default actuals in nested instances must be handled specially -- because there is no link to them from the original tree. When an -- actual subprogram is given by a default, we add an explicit generic @@ -13561,8 +13710,7 @@ package body Sem_Ch12 is -- so that it can be properly resolved in a subsequent instantiation. procedure Save_Global_Descendant (D : Union_Id); - -- Apply Save_Global_References recursively to the descendents of the - -- current node. + -- Apply Save_References recursively to the descendents of node D procedure Save_References (N : Node_Id); -- This is the recursive procedure that does the work, once the @@ -13630,7 +13778,6 @@ package body Sem_Ch12 is ------------------ procedure Reset_Entity (N : Node_Id) is - procedure Set_Global_Type (N : Node_Id; N2 : Node_Id); -- If the type of N2 is global to the generic unit, save the type in -- the generic node. Just as we perform name capture for explicit @@ -13654,14 +13801,12 @@ package body Sem_Ch12 is begin Set_Etype (N, Typ); - if Entity (N) /= N2 - and then Has_Private_View (Entity (N)) - then - -- If the entity of N is not the associated node, this is a - -- nested generic and it has an associated node as well, whose - -- type is already the full view (see below). Indicate that the - -- original node has a private view. + -- If the entity of N is not the associated node, this is a + -- nested generic and it has an associated node as well, whose + -- type is already the full view (see below). Indicate that the + -- original node has a private view. + if Entity (N) /= N2 and then Has_Private_View (Entity (N)) then Set_Has_Private_View (N); end if; @@ -13712,7 +13857,7 @@ package body Sem_Ch12 is begin N2 := Get_Associated_Node (N); - E := Entity (N2); + E := Entity (N2); if Present (E) then @@ -13721,12 +13866,12 @@ package body Sem_Ch12 is -- preserve in this case, since the expansion will be redone in -- the instance. - if not Nkind_In (E, N_Defining_Identifier, - N_Defining_Character_Literal, + if not Nkind_In (E, N_Defining_Character_Literal, + N_Defining_Identifier, N_Defining_Operator_Symbol) then Set_Associated_Node (N, Empty); - Set_Etype (N, Empty); + Set_Etype (N, Empty); return; end if; @@ -13767,11 +13912,11 @@ package body Sem_Ch12 is Set_Associated_Node (N, N2); Set_Global_Type (N, N2); - else - -- Renaming is local, and will be resolved in instance + -- Renaming is local, and will be resolved in instance + else Set_Associated_Node (N, Empty); - Set_Etype (N, Empty); + Set_Etype (N, Empty); end if; else @@ -13782,17 +13927,17 @@ package body Sem_Ch12 is and then Is_Generic_Type (Etype (N2)) and then (Base_Type (Etype (Right_Opnd (N2))) = Etype (N2) or else - Base_Type (Etype (Left_Opnd (N2))) = Etype (N2)) + Base_Type (Etype (Left_Opnd (N2))) = Etype (N2)) and then Is_Intrinsic_Subprogram (E) then null; - else - -- Entity is local. Mark generic node as unresolved. - -- Note that now it does not have an entity. + -- Entity is local. Mark generic node as unresolved. Note that now + -- it does not have an entity. + else Set_Associated_Node (N, Empty); - Set_Etype (N, Empty); + Set_Etype (N, Empty); end if; if Nkind (Parent (N)) in N_Generic_Instantiation @@ -13837,7 +13982,7 @@ package body Sem_Ch12 is and then Parent (N) = Name (Parent (Parent (N))) then Save_Global_Defaults - (Parent (Parent (N)), Parent (Parent ((N2)))); + (Parent (Parent (N)), Parent (Parent (N2))); end if; -- A selected component may denote a static constant that has been @@ -13852,9 +13997,6 @@ package body Sem_Ch12 is then Rewrite (Parent (N), New_Copy (Parent (N2))); Set_Analyzed (Parent (N), False); - - else - null; end if; -- A selected component may be transformed into a parameterless @@ -13907,17 +14049,20 @@ package body Sem_Ch12 is begin case Nkind (N) is when N_Binary_Op => - Save_Global_Descendant (Union_Id (Left_Opnd (N))); + Save_Global_Descendant (Union_Id (Left_Opnd (N))); Save_Global_Descendant (Union_Id (Right_Opnd (N))); when N_Unary_Op => Save_Global_Descendant (Union_Id (Right_Opnd (N))); - when N_Expanded_Name | N_Selected_Component => + when N_Expanded_Name | + N_Selected_Component => Save_Global_Descendant (Union_Id (Prefix (N))); Save_Global_Descendant (Union_Id (Selector_Name (N))); - when N_Identifier | N_Character_Literal | N_Operator_Symbol => + when N_Identifier | + N_Character_Literal | + N_Operator_Symbol => null; when others => @@ -13929,7 +14074,7 @@ package body Sem_Ch12 is -- Save_Global_Defaults -- -------------------------- - procedure Save_Global_Defaults (N1, N2 : Node_Id) is + procedure Save_Global_Defaults (N1 : Node_Id; N2 : Node_Id) is Loc : constant Source_Ptr := Sloc (N1); Assoc2 : constant List_Id := Generic_Associations (N2); Gen_Id : constant Entity_Id := Get_Generic_Entity (N2); @@ -13998,9 +14143,10 @@ package body Sem_Ch12 is if Is_Global (Actual) then Ndec := Make_Generic_Association (Loc, - Selector_Name => New_Occurrence_Of (Subp, Loc), - Explicit_Generic_Actual_Parameter => - New_Occurrence_Of (Actual, Loc)); + Selector_Name => + New_Occurrence_Of (Subp, Loc), + Explicit_Generic_Actual_Parameter => + New_Occurrence_Of (Actual, Loc)); Set_Associated_Node (Explicit_Generic_Actual_Parameter (Ndec), Def); @@ -14013,8 +14159,9 @@ package body Sem_Ch12 is elsif Present (Next (Act2)) then Ndec := Make_Generic_Association (Loc, - Selector_Name => New_Occurrence_Of (Subp, Loc), - Explicit_Generic_Actual_Parameter => Empty); + Selector_Name => + New_Occurrence_Of (Subp, Loc), + Explicit_Generic_Actual_Parameter => Empty); Append (Ndec, Assoc1); end if; @@ -14054,7 +14201,6 @@ package body Sem_Ch12 is (Selector_Name (Name (N1)), Selector_Name (Name (N2))); Set_Etype (Name (N1), Etype (Gen_Id)); end if; - end Save_Global_Defaults; ---------------------------- @@ -14107,99 +14253,197 @@ package body Sem_Ch12 is procedure Save_References (N : Node_Id) is Loc : constant Source_Ptr := Sloc (N); - begin - if N = Empty then - null; + function Requires_Delayed_Save (Nod : Node_Id) return Boolean; + -- Determine whether arbitrary node Nod requires delayed capture of + -- global references within its aspect specifications. - elsif Nkind_In (N, N_Character_Literal, N_Operator_Symbol) then - if Nkind (N) = Nkind (Get_Associated_Node (N)) then - Reset_Entity (N); + procedure Save_References_In_Aggregate (N : Node_Id); + -- Save all global references in [extension] aggregate node N - elsif Nkind (N) = N_Operator_Symbol - and then Nkind (Get_Associated_Node (N)) = N_String_Literal - then - Change_Operator_Symbol_To_String_Literal (N); - end if; + procedure Save_References_In_Char_Lit_Or_Op_Symbol (N : Node_Id); + -- Save all global references in a character literal or operator + -- symbol denoted by N. - elsif Nkind (N) in N_Op then - if Nkind (N) = Nkind (Get_Associated_Node (N)) then - if Nkind (N) = N_Op_Concat then - Set_Is_Component_Left_Opnd (N, - Is_Component_Left_Opnd (Get_Associated_Node (N))); + procedure Save_References_In_Descendants (N : Node_Id); + -- Save all global references in all descendants of node N - Set_Is_Component_Right_Opnd (N, - Is_Component_Right_Opnd (Get_Associated_Node (N))); - end if; + procedure Save_References_In_Identifier (N : Node_Id); + -- Save all global references in identifier node N - Reset_Entity (N); + procedure Save_References_In_Operator (N : Node_Id); + -- Save all global references in operator node N - else - -- Node may be transformed into call to a user-defined operator + procedure Save_References_In_Pragma (Prag : Node_Id); + -- Save all global references found within the expression of pragma + -- Prag. - N2 := Get_Associated_Node (N); + --------------------------- + -- Requires_Delayed_Save -- + --------------------------- - if Nkind (N2) = N_Function_Call then - E := Entity (Name (N2)); + function Requires_Delayed_Save (Nod : Node_Id) return Boolean is + begin + -- Generic packages and subprograms require delayed capture of + -- global references within their aspects due to the timing of + -- annotation analysis. - if Present (E) - and then Is_Global (E) - then - Set_Etype (N, Etype (N2)); - else - Set_Associated_Node (N, Empty); - Set_Etype (N, Empty); - end if; + if Nkind_In (Nod, N_Generic_Package_Declaration, + N_Generic_Subprogram_Declaration, + N_Package_Body, + N_Package_Body_Stub, + N_Subprogram_Body, + N_Subprogram_Body_Stub) + then + -- Since the capture of global references is done on the + -- unanalyzed generic template, there is no information around + -- to infer the context. Use the Associated_Entity linkages to + -- peek into the analyzed generic copy and determine what the + -- template corresponds to. + + if Nod = Templ then + return + Is_Generic_Declaration_Or_Body + (Unit_Declaration_Node + (Associated_Entity (Defining_Entity (Nod)))); + + -- Otherwise the generic unit being processed is not the top + -- level template. It is safe to capture of global references + -- within the generic unit because at this point the top level + -- copy is fully analyzed. - elsif Nkind_In (N2, N_Integer_Literal, - N_Real_Literal, - N_String_Literal) - then - if Present (Original_Node (N2)) - and then Nkind (Original_Node (N2)) = Nkind (N) - then + else + return False; + end if; - -- Operation was constant-folded. Whenever possible, - -- recover semantic information from unfolded node, - -- for ASIS use. + -- Otherwise capture the global references without interference - Set_Associated_Node (N, Original_Node (N2)); + else + return False; + end if; + end Requires_Delayed_Save; - if Nkind (N) = N_Op_Concat then - Set_Is_Component_Left_Opnd (N, - Is_Component_Left_Opnd (Get_Associated_Node (N))); - Set_Is_Component_Right_Opnd (N, - Is_Component_Right_Opnd (Get_Associated_Node (N))); - end if; + ---------------------------------- + -- Save_References_In_Aggregate -- + ---------------------------------- - Reset_Entity (N); + procedure Save_References_In_Aggregate (N : Node_Id) is + Nam : Node_Id; + Qual : Node_Id := Empty; + Typ : Entity_Id := Empty; - else - -- If original node is already modified, propagate - -- constant-folding to template. + use Atree.Unchecked_Access; + -- This code section is part of implementing an untyped tree + -- traversal, so it needs direct access to node fields. - Rewrite (N, New_Copy (N2)); - Set_Analyzed (N, False); - end if; + begin + N2 := Get_Associated_Node (N); - elsif Nkind (N2) = N_Identifier - and then Ekind (Entity (N2)) = E_Enumeration_Literal + if Present (N2) then + Typ := Etype (N2); + + -- In an instance within a generic, use the name of the actual + -- and not the original generic parameter. If the actual is + -- global in the current generic it must be preserved for its + -- instantiation. + + if Nkind (Parent (Typ)) = N_Subtype_Declaration + and then Present (Generic_Parent_Type (Parent (Typ))) then - -- Same if call was folded into a literal, but in this case - -- retain the entity to avoid spurious ambiguities if it is - -- overloaded at the point of instantiation or inlining. + Typ := Base_Type (Typ); + Set_Etype (N2, Typ); + end if; + end if; - Rewrite (N, New_Copy (N2)); - Set_Analyzed (N, False); + if No (N2) or else No (Typ) or else not Is_Global (Typ) then + Set_Associated_Node (N, Empty); + + -- If the aggregate is an actual in a call, it has been + -- resolved in the current context, to some local type. The + -- enclosing call may have been disambiguated by the aggregate, + -- and this disambiguation might fail at instantiation time + -- because the type to which the aggregate did resolve is not + -- preserved. In order to preserve some of this information, + -- wrap the aggregate in a qualified expression, using the id + -- of its type. For further disambiguation we qualify the type + -- name with its scope (if visible) because both id's will have + -- corresponding entities in an instance. This resolves most of + -- the problems with missing type information on aggregates in + -- instances. + + if Present (N2) + and then Nkind (N2) = Nkind (N) + and then Nkind (Parent (N2)) in N_Subprogram_Call + and then Present (Typ) + and then Comes_From_Source (Typ) + then + Nam := Make_Identifier (Loc, Chars (Typ)); + + if Is_Immediately_Visible (Scope (Typ)) then + Nam := + Make_Selected_Component (Loc, + Prefix => + Make_Identifier (Loc, Chars (Scope (Typ))), + Selector_Name => Nam); + end if; + + Qual := + Make_Qualified_Expression (Loc, + Subtype_Mark => Nam, + Expression => Relocate_Node (N)); end if; end if; - -- Complete operands check if node has not been constant-folded + Save_Global_Descendant (Field1 (N)); + Save_Global_Descendant (Field2 (N)); + Save_Global_Descendant (Field3 (N)); + Save_Global_Descendant (Field5 (N)); - if Nkind (N) in N_Op then - Save_Entity_Descendants (N); + if Present (Qual) then + Rewrite (N, Qual); end if; + end Save_References_In_Aggregate; + + ---------------------------------------------- + -- Save_References_In_Char_Lit_Or_Op_Symbol -- + ---------------------------------------------- + + procedure Save_References_In_Char_Lit_Or_Op_Symbol (N : Node_Id) is + begin + if Nkind (N) = Nkind (Get_Associated_Node (N)) then + Reset_Entity (N); + + elsif Nkind (N) = N_Operator_Symbol + and then Nkind (Get_Associated_Node (N)) = N_String_Literal + then + Change_Operator_Symbol_To_String_Literal (N); + end if; + end Save_References_In_Char_Lit_Or_Op_Symbol; + + ------------------------------------ + -- Save_References_In_Descendants -- + ------------------------------------ + + procedure Save_References_In_Descendants (N : Node_Id) is + use Atree.Unchecked_Access; + -- This code section is part of implementing an untyped tree + -- traversal, so it needs direct access to node fields. + + begin + Save_Global_Descendant (Field1 (N)); + Save_Global_Descendant (Field2 (N)); + Save_Global_Descendant (Field3 (N)); + Save_Global_Descendant (Field4 (N)); + Save_Global_Descendant (Field5 (N)); + end Save_References_In_Descendants; + + ----------------------------------- + -- Save_References_In_Identifier -- + ----------------------------------- + + procedure Save_References_In_Identifier (N : Node_Id) is + begin + -- The node did not undergo a transformation - elsif Nkind (N) = N_Identifier then if Nkind (N) = Nkind (Get_Associated_Node (N)) then -- If this is a discriminant reference, always save it. It is @@ -14210,50 +14454,47 @@ package body Sem_Ch12 is (N, Original_Discriminant (Get_Associated_Node (N))); Reset_Entity (N); + -- The analysis of the generic copy transformed the identifier + -- into another construct. Propagate the changes to the template. + else N2 := Get_Associated_Node (N); + -- The identifier denotes a call to a parameterless function. + -- Mark the node as resolved when the function is external. + if Nkind (N2) = N_Function_Call then E := Entity (Name (N2)); - -- Name resolves to a call to parameterless function. If - -- original entity is global, mark node as resolved. - - if Present (E) - and then Is_Global (E) - then + if Present (E) and then Is_Global (E) then Set_Etype (N, Etype (N2)); else Set_Associated_Node (N, Empty); Set_Etype (N, Empty); end if; + -- The identifier denotes a named number that was constant + -- folded. Preserve the original name for ASIS and undo the + -- constant folding which will be repeated in the instance. + elsif Nkind_In (N2, N_Integer_Literal, N_Real_Literal) and then Is_Entity_Name (Original_Node (N2)) then - -- Name resolves to named number that is constant-folded, - -- We must preserve the original name for ASIS use, and - -- undo the constant-folding, which will be repeated in - -- each instance. - Set_Associated_Node (N, Original_Node (N2)); Reset_Entity (N); - elsif Nkind (N2) = N_String_Literal then - - -- Name resolves to string literal. Perform the same - -- replacement in generic. + -- The identifier resolved to a string literal. Propagate this + -- information to the generic template. + elsif Nkind (N2) = N_String_Literal then Rewrite (N, New_Copy (N2)); - elsif Nkind (N2) = N_Explicit_Dereference then - - -- An identifier is rewritten as a dereference if it is the - -- prefix in an implicit dereference (call or attribute). - -- The analysis of an instantiation will expand the node - -- again, so we preserve the original tree but link it to - -- the resolved entity in case it is global. + -- The identifier is rewritten as a dereference if it is the + -- prefix of an implicit dereference. Preserve the original + -- tree as the analysis of the instance will expand the node + -- again, but preserve the resolved entity if it is global. + elsif Nkind (N2) = N_Explicit_Dereference then if Is_Entity_Name (Prefix (N2)) and then Present (Entity (Prefix (N2))) and then Is_Global (Entity (Prefix (N2))) @@ -14261,14 +14502,16 @@ package body Sem_Ch12 is Set_Associated_Node (N, Prefix (N2)); elsif Nkind (Prefix (N2)) = N_Function_Call + and then Present (Entity (Name (Prefix (N2)))) and then Is_Global (Entity (Name (Prefix (N2)))) then Rewrite (N, Make_Explicit_Dereference (Loc, - Prefix => Make_Function_Call (Loc, - Name => - New_Occurrence_Of - (Entity (Name (Prefix (N2))), Loc)))); + Prefix => + Make_Function_Call (Loc, + Name => + New_Occurrence_Of + (Entity (Name (Prefix (N2))), Loc)))); else Set_Associated_Node (N, Empty); @@ -14284,117 +14527,211 @@ package body Sem_Ch12 is then Set_Associated_Node (N, Original_Node (N2)); Reset_Entity (N); - - else - null; end if; end if; + end Save_References_In_Identifier; - elsif Nkind (N) in N_Entity then - null; + --------------------------------- + -- Save_References_In_Operator -- + --------------------------------- - else - declare - Qual : Node_Id := Empty; - Typ : Entity_Id := Empty; - Nam : Node_Id; + procedure Save_References_In_Operator (N : Node_Id) is + begin + -- The node did not undergo a transformation - use Atree.Unchecked_Access; - -- This code section is part of implementing an untyped tree - -- traversal, so it needs direct access to node fields. + if Nkind (N) = Nkind (Get_Associated_Node (N)) then + if Nkind (N) = N_Op_Concat then + Set_Is_Component_Left_Opnd (N, + Is_Component_Left_Opnd (Get_Associated_Node (N))); - begin - if Nkind_In (N, N_Aggregate, N_Extension_Aggregate) then - N2 := Get_Associated_Node (N); + Set_Is_Component_Right_Opnd (N, + Is_Component_Right_Opnd (Get_Associated_Node (N))); + end if; - if No (N2) then - Typ := Empty; + Reset_Entity (N); - else - Typ := Etype (N2); + -- The analysis of the generic copy transformed the operator into + -- some other construct. Propagate the changes to the template. - -- In an instance within a generic, use the name of the - -- actual and not the original generic parameter. If the - -- actual is global in the current generic it must be - -- preserved for its instantiation. + else + N2 := Get_Associated_Node (N); - if Nkind (Parent (Typ)) = N_Subtype_Declaration - and then - Present (Generic_Parent_Type (Parent (Typ))) - then - Typ := Base_Type (Typ); - Set_Etype (N2, Typ); - end if; - end if; + -- The operator resoved to a function call - if No (N2) or else No (Typ) or else not Is_Global (Typ) then + if Nkind (N2) = N_Function_Call then + E := Entity (Name (N2)); + + if Present (E) and then Is_Global (E) then + Set_Etype (N, Etype (N2)); + else Set_Associated_Node (N, Empty); + Set_Etype (N, Empty); + end if; - -- If the aggregate is an actual in a call, it has been - -- resolved in the current context, to some local type. - -- The enclosing call may have been disambiguated by the - -- aggregate, and this disambiguation might fail at - -- instantiation time because the type to which the - -- aggregate did resolve is not preserved. In order to - -- preserve some of this information, we wrap the - -- aggregate in a qualified expression, using the id of - -- its type. For further disambiguation we qualify the - -- type name with its scope (if visible) because both - -- id's will have corresponding entities in an instance. - -- This resolves most of the problems with missing type - -- information on aggregates in instances. - - if Nkind (N2) = Nkind (N) - and then Nkind (Parent (N2)) in N_Subprogram_Call - and then Comes_From_Source (Typ) - then - if Is_Immediately_Visible (Scope (Typ)) then - Nam := - Make_Selected_Component (Loc, - Prefix => - Make_Identifier (Loc, Chars (Scope (Typ))), - Selector_Name => - Make_Identifier (Loc, Chars (Typ))); - else - Nam := Make_Identifier (Loc, Chars (Typ)); - end if; + -- The operator was folded into a literal - Qual := - Make_Qualified_Expression (Loc, - Subtype_Mark => Nam, - Expression => Relocate_Node (N)); + elsif Nkind_In (N2, N_Integer_Literal, + N_Real_Literal, + N_String_Literal) + then + if Present (Original_Node (N2)) + and then Nkind (Original_Node (N2)) = Nkind (N) + then + -- Operation was constant-folded. Whenever possible, + -- recover semantic information from unfolded node, + -- for ASIS use. + + Set_Associated_Node (N, Original_Node (N2)); + + if Nkind (N) = N_Op_Concat then + Set_Is_Component_Left_Opnd (N, + Is_Component_Left_Opnd (Get_Associated_Node (N))); + Set_Is_Component_Right_Opnd (N, + Is_Component_Right_Opnd (Get_Associated_Node (N))); end if; - end if; - Save_Global_Descendant (Field1 (N)); - Save_Global_Descendant (Field2 (N)); - Save_Global_Descendant (Field3 (N)); - Save_Global_Descendant (Field5 (N)); + Reset_Entity (N); - if Present (Qual) then - Rewrite (N, Qual); + -- Propagate the constant folding back to the template + + else + Rewrite (N, New_Copy (N2)); + Set_Analyzed (N, False); end if; - -- All other cases than aggregates + -- The operator was folded into an enumeration literal. Retain + -- the entity to avoid spurious ambiguities if it is overloaded + -- at the point of instantiation or inlining. + + elsif Nkind (N2) = N_Identifier + and then Ekind (Entity (N2)) = E_Enumeration_Literal + then + Rewrite (N, New_Copy (N2)); + Set_Analyzed (N, False); + end if; + end if; + + -- Complete the operands check if node has not been constant + -- folded. + + if Nkind (N) in N_Op then + Save_Entity_Descendants (N); + end if; + end Save_References_In_Operator; + + ------------------------------- + -- Save_References_In_Pragma -- + ------------------------------- + + procedure Save_References_In_Pragma (Prag : Node_Id) is + Context : Node_Id; + Do_Save : Boolean := True; + + use Atree.Unchecked_Access; + -- This code section is part of implementing an untyped tree + -- traversal, so it needs direct access to node fields. + + begin + -- Do not save global references in pragmas generated from aspects + -- because the pragmas will be regenerated at instantiation time. + + if From_Aspect_Specification (Prag) then + Do_Save := False; + + -- The capture of global references within contract-related source + -- pragmas associated with generic packages, subprograms or their + -- respective bodies must be delayed due to timing of annotation + -- analysis. Global references are still captured in routine + -- Save_Global_References_In_Contract. + + elsif Is_Generic_Contract_Pragma (Prag) and then Prag /= Templ then + if Is_Package_Contract_Annotation (Prag) then + Context := Find_Related_Package_Or_Body (Prag); else - Save_Global_Descendant (Field1 (N)); - Save_Global_Descendant (Field2 (N)); - Save_Global_Descendant (Field3 (N)); - Save_Global_Descendant (Field4 (N)); - Save_Global_Descendant (Field5 (N)); + pragma Assert (Is_Subprogram_Contract_Annotation (Prag)); + Context := Find_Related_Subprogram_Or_Body (Prag); end if; - end; + + -- The use of Original_Node accounts for the case when the + -- related context is generic template. + + if Requires_Delayed_Save (Original_Node (Context)) then + Do_Save := False; + end if; + end if; + + -- For all other cases, save all global references within the + -- descendants, but skip the following semantic fields: + + -- Field1 - Next_Pragma + -- Field3 - Corresponding_Aspect + -- Field5 - Next_Rep_Item + + if Do_Save then + Save_Global_Descendant (Field2 (Prag)); + Save_Global_Descendant (Field4 (Prag)); + end if; + end Save_References_In_Pragma; + + -- Start of processing for Save_References + + begin + if N = Empty then + null; + + -- Aggregates + + elsif Nkind_In (N, N_Aggregate, N_Extension_Aggregate) then + Save_References_In_Aggregate (N); + + -- Character literals, operator symbols + + elsif Nkind_In (N, N_Character_Literal, N_Operator_Symbol) then + Save_References_In_Char_Lit_Or_Op_Symbol (N); + + -- Defining identifiers + + elsif Nkind (N) in N_Entity then + null; + + -- Identifiers + + elsif Nkind (N) = N_Identifier then + Save_References_In_Identifier (N); + + -- Operators + + elsif Nkind (N) in N_Op then + Save_References_In_Operator (N); + + -- Pragmas + + elsif Nkind (N) = N_Pragma then + Save_References_In_Pragma (N); + + else + Save_References_In_Descendants (N); end if; - -- Save all global references found within the aspects of the related - -- node. This is not done for generic subprograms because the aspects - -- must be delayed and analyzed at the end of the declarative part. - -- Only then can global references be saved. This action is performed - -- by the analysis of the generic subprogram contract. + -- Save all global references found within the aspect specifications + -- of the related node. - if Nkind (N) /= N_Generic_Subprogram_Declaration then - Save_Global_References_In_Aspects (N); + if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then + + -- The capture of global references within aspects associated with + -- generic packages, subprograms or their bodies must be delayed + -- due to timing of annotation analysis. Global references are + -- still captured in routine Save_Global_References_In_Contract. + + if Requires_Delayed_Save (N) then + null; + + -- Otherwise save all global references within the aspects + + else + Save_Global_References_In_Aspects (N); + end if; end if; end Save_References; @@ -14413,7 +14750,7 @@ package body Sem_Ch12 is Gen_Scope := Scope (Gen_Scope); end loop; - Save_References (N); + Save_References (Templ); end Save_Global_References; --------------------------------------- @@ -14425,19 +14762,74 @@ package body Sem_Ch12 is Expr : Node_Id; begin - if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then - Asp := First (Aspect_Specifications (N)); - while Present (Asp) loop - Expr := Expression (Asp); + Asp := First (Aspect_Specifications (N)); + while Present (Asp) loop + Expr := Expression (Asp); + + if Present (Expr) then + Save_Global_References (Expr); + end if; - if Present (Expr) then - Save_Global_References (Expr); + Next (Asp); + end loop; + end Save_Global_References_In_Aspects; + + ---------------------------------------- + -- Save_Global_References_In_Contract -- + ---------------------------------------- + + procedure Save_Global_References_In_Contract + (Templ : Node_Id; + Gen_Id : Entity_Id) + is + procedure Save_Global_References_In_List (First_Prag : Node_Id); + -- Save all global references in contract-related source pragmas found + -- in the list starting with pragma First_Prag. + + ------------------------------------ + -- Save_Global_References_In_List -- + ------------------------------------ + + procedure Save_Global_References_In_List (First_Prag : Node_Id) is + Prag : Node_Id; + + begin + Prag := First_Prag; + while Present (Prag) loop + if Is_Generic_Contract_Pragma (Prag) then + Save_Global_References (Prag); end if; - Next (Asp); + Prag := Next_Pragma (Prag); end loop; + end Save_Global_References_In_List; + + -- Local variables + + Items : constant Node_Id := Contract (Defining_Entity (Templ)); + + -- Start of processing for Save_Global_References_In_Contract + + begin + -- The entity of the analyzed generic copy must be on the scope stack + -- to ensure proper detection of global references. + + Push_Scope (Gen_Id); + + if Permits_Aspect_Specifications (Templ) + and then Has_Aspects (Templ) + then + Save_Global_References_In_Aspects (Templ); end if; - end Save_Global_References_In_Aspects; + + if Present (Items) then + Save_Global_References_In_List (Pre_Post_Conditions (Items)); + Save_Global_References_In_List (Contract_Test_Cases (Items)); + Save_Global_References_In_List (Classifications (Items)); + end if; + + Pop_Scope; + end Save_Global_References_In_Contract; -------------------------------------- -- Set_Copied_Sloc_For_Inlined_Body -- diff --git a/gcc/ada/sem_ch12.ads b/gcc/ada/sem_ch12.ads index 52e5f5ce6c8..53ff6c50e95 100644 --- a/gcc/ada/sem_ch12.ads +++ b/gcc/ada/sem_ch12.ads @@ -136,24 +136,28 @@ package Sem_Ch12 is -- pragma, or because a pragma appears for the instance in the scope. -- of the instance. - procedure Save_Global_References (N : Node_Id); + procedure Save_Global_References (Templ : Node_Id); -- Traverse the original generic unit, and capture all references to - -- entities that are defined outside of the generic in the analyzed - -- tree for the template. These references are copied into the original - -- tree, so that they appear automatically in every instantiation. - -- A critical invariant in this approach is that if an id in the generic - -- resolves to a local entity, the corresponding id in the instance - -- will resolve to the homologous entity in the instance, even though - -- the enclosing context for resolution is different, as long as the - -- global references have been captured as described here. + -- entities that are defined outside of the generic in the analyzed tree + -- for the template. These references are copied into the original tree, + -- so that they appear automatically in every instantiation. A critical + -- invariant in this approach is that if an id in the generic resolves to + -- a local entity, the corresponding id in the instance will resolve to + -- the homologous entity in the instance, even though the enclosing context + -- for resolution is different, as long as the global references have been + -- captured as described here. -- Because instantiations can be nested, the environment of the instance, -- involving the actuals and other data-structures, must be saved and -- restored in stack-like fashion. Front-end inlining also uses these -- structures for the management of private/full views. - procedure Save_Global_References_In_Aspects (N : Node_Id); - -- Save all global references in the aspect specifications of node N + procedure Save_Global_References_In_Contract + (Templ : Node_Id; + Gen_Id : Entity_Id); + -- Save all global references found within the aspect specifications and + -- the contract-related source pragmas assocated with generic template + -- Templ. Gen_Id denotes the entity of the analyzed generic copy. procedure Set_Copied_Sloc_For_Inlined_Body (N : Node_Id; E : Entity_Id); -- This procedure is used when a subprogram body is inlined. This process diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 7f1f1103617..30437ba5eea 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -3416,6 +3416,147 @@ package body Sem_Ch13 is end if; end Analyze_Aspect_Specifications; + --------------------------------------------------- + -- Analyze_Aspect_Specifications_On_Body_Or_Stub -- + --------------------------------------------------- + + procedure Analyze_Aspect_Specifications_On_Body_Or_Stub (N : Node_Id) is + Body_Id : constant Entity_Id := Defining_Entity (N); + + procedure Diagnose_Misplaced_Aspects (Spec_Id : Entity_Id); + -- Subprogram body [stub] N has aspects, but they are not properly + -- placed. Emit an error message depending on the aspects involved. + -- Spec_Id is the entity of the corresponding spec. + + -------------------------------- + -- Diagnose_Misplaced_Aspects -- + -------------------------------- + + procedure Diagnose_Misplaced_Aspects (Spec_Id : Entity_Id) is + procedure Misplaced_Aspect_Error + (Asp : Node_Id; + Ref_Nam : Name_Id); + -- Emit an error message concerning misplaced aspect Asp. Ref_Nam is + -- the name of the refined version of the aspect. + + ---------------------------- + -- Misplaced_Aspect_Error -- + ---------------------------- + + procedure Misplaced_Aspect_Error + (Asp : Node_Id; + Ref_Nam : Name_Id) + is + Asp_Nam : constant Name_Id := Chars (Identifier (Asp)); + Asp_Id : constant Aspect_Id := Get_Aspect_Id (Asp_Nam); + + begin + -- The corresponding spec already contains the aspect in question + -- and the one appearing on the body must be the refined form: + + -- procedure P with Global ...; + -- procedure P with Global ... is ... end P; + -- ^ + -- Refined_Global + + if Has_Aspect (Spec_Id, Asp_Id) then + Error_Msg_Name_1 := Asp_Nam; + + -- Subunits cannot carry aspects that apply to a subprogram + -- declaration. + + if Nkind (Parent (N)) = N_Subunit then + Error_Msg_N ("aspect % cannot apply to a subunit", Asp); + + -- Otherwise suggest the refined form + + else + Error_Msg_Name_2 := Ref_Nam; + Error_Msg_N ("aspect % should be %", Asp); + end if; + + -- Otherwise the aspect must appear on the spec, not on the body + + -- procedure P; + -- procedure P with Global ... is ... end P; + + else + Error_Msg_N + ("aspect specification must appear in subprogram declaration", + Asp); + end if; + end Misplaced_Aspect_Error; + + -- Local variables + + Asp : Node_Id; + Asp_Nam : Name_Id; + + -- Start of processing for Diagnose_Misplaced_Aspects + + begin + -- Iterate over the aspect specifications and emit specific errors + -- where applicable. + + Asp := First (Aspect_Specifications (N)); + while Present (Asp) loop + Asp_Nam := Chars (Identifier (Asp)); + + -- Do not emit errors on aspects that can appear on a subprogram + -- body. This scenario occurs when the aspect specification list + -- contains both misplaced and properly placed aspects. + + if Aspect_On_Body_Or_Stub_OK (Get_Aspect_Id (Asp_Nam)) then + null; + + -- Special diagnostics for SPARK aspects + + elsif Asp_Nam = Name_Depends then + Misplaced_Aspect_Error (Asp, Name_Refined_Depends); + + elsif Asp_Nam = Name_Global then + Misplaced_Aspect_Error (Asp, Name_Refined_Global); + + elsif Asp_Nam = Name_Post then + Misplaced_Aspect_Error (Asp, Name_Refined_Post); + + -- Otherwise a language-defined aspect is misplaced + + else + Error_Msg_N + ("aspect specification must appear in subprogram declaration", + Asp); + end if; + + Next (Asp); + end loop; + end Diagnose_Misplaced_Aspects; + + -- Local variables + + Spec_Id : Entity_Id; + + -- Start of processing for Analyze_Aspects_On_Body_Or_Stub + + begin + if Nkind (N) = N_Subprogram_Body_Stub then + Spec_Id := Corresponding_Spec_Of_Stub (N); + else + Spec_Id := Corresponding_Spec (N); + end if; + + -- Language-defined aspects cannot be associated with a subprogram body + -- [stub] if the subprogram has a spec. Certain implementation defined + -- aspects are allowed to break this rule (for all applicable cases, see + -- table Aspects.Aspect_On_Body_Or_Stub_OK). + + if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then + Diagnose_Misplaced_Aspects (Spec_Id); + else + Analyze_Aspect_Specifications (N, Body_Id); + end if; + end Analyze_Aspect_Specifications_On_Body_Or_Stub; + ----------------------- -- Analyze_At_Clause -- ----------------------- diff --git a/gcc/ada/sem_ch13.ads b/gcc/ada/sem_ch13.ads index b1bb1592b45..df779086065 100644 --- a/gcc/ada/sem_ch13.ads +++ b/gcc/ada/sem_ch13.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -42,6 +42,12 @@ package Sem_Ch13 is -- is the corresponding entity declared by the declaration node N. Callers -- should check that Has_Aspects (N) is True before calling this routine. + procedure Analyze_Aspect_Specifications_On_Body_Or_Stub (N : Node_Id); + -- Analyze the aspect specifications of [generic] subprogram body or stub + -- N. Callers should check that Has_Aspects (N) is True before calling the + -- routine. This routine diagnoses misplaced aspects that should appear on + -- the initial declaration of N and offers suggestions for replacements. + procedure Adjust_Record_For_Reverse_Bit_Order (R : Entity_Id); -- Called from Freeze where R is a record entity for which reverse bit -- order is specified and there is at least one component clause. Adjusts diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 3b72073a1f8..75bf87448a7 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -58,6 +58,7 @@ with Sem_Ch6; use Sem_Ch6; with Sem_Ch7; use Sem_Ch7; with Sem_Ch8; use Sem_Ch8; with Sem_Ch10; use Sem_Ch10; +with Sem_Ch12; use Sem_Ch12; with Sem_Ch13; use Sem_Ch13; with Sem_Dim; use Sem_Dim; with Sem_Disp; use Sem_Disp; @@ -2302,17 +2303,14 @@ package body Sem_Ch3 is -- Local variables - Context : Node_Id; + Context : Node_Id := Empty; Freeze_From : Entity_Id := Empty; Next_Decl : Node_Id; - Spec_Id : Entity_Id; + Pack_Decl : Node_Id := Empty; Body_Seen : Boolean := False; -- Flag set when the first body [stub] is encountered - In_Package_Body : Boolean := False; - -- Flag set when the current declaration list belongs to a package body - -- Start of processing for Analyze_Declarations begin @@ -2456,6 +2454,7 @@ package body Sem_Ch3 is Context := Parent (L); if Nkind (Context) = N_Package_Specification then + Pack_Decl := Parent (Context); -- When a package has private declarations, its contract must be -- analyzed at the end of the said declarations. This way both the @@ -2484,44 +2483,71 @@ package body Sem_Ch3 is end if; elsif Nkind (Context) = N_Package_Body then - In_Package_Body := True; - Spec_Id := Corresponding_Spec (Context); - + Pack_Decl := Context; Analyze_Package_Body_Contract (Defining_Entity (Context)); end if; - end if; - -- Analyze the contracts of subprogram declarations, subprogram bodies - -- and variables now due to the delayed visibility requirements of their - -- aspects. + -- Analyze the contracts of all subprogram declarations, subprogram + -- bodies and variables now due to the delayed visibility needs of + -- of their aspects and pragmas. Capture global references in generic + -- subprograms or bodies. - Decl := First (L); - while Present (Decl) loop - if Nkind (Decl) = N_Object_Declaration then - Analyze_Object_Contract (Defining_Entity (Decl)); + Decl := First (L); + while Present (Decl) loop + if Nkind (Decl) = N_Object_Declaration then + Analyze_Object_Contract (Defining_Entity (Decl)); - elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, - N_Generic_Subprogram_Declaration, - N_Subprogram_Declaration) - then - Analyze_Subprogram_Contract (Defining_Entity (Decl)); + elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, + N_Generic_Subprogram_Declaration, + N_Subprogram_Declaration) + then + Analyze_Subprogram_Contract (Defining_Entity (Decl)); - elsif Nkind (Decl) = N_Subprogram_Body then - Analyze_Subprogram_Body_Contract (Defining_Entity (Decl)); + elsif Nkind (Decl) = N_Subprogram_Body then + Analyze_Subprogram_Body_Contract (Defining_Entity (Decl)); - elsif Nkind (Decl) = N_Subprogram_Body_Stub then - Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); - end if; + elsif Nkind (Decl) = N_Subprogram_Body_Stub then + Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); + end if; - Next (Decl); - end loop; + -- Capture all global references in a generic subprogram or a body + -- [stub] now that the contract has been analyzed. + + if Nkind_In (Decl, N_Generic_Subprogram_Declaration, + N_Subprogram_Body, + N_Subprogram_Body_Stub) + and then Is_Generic_Declaration_Or_Body (Decl) + then + Save_Global_References_In_Contract + (Templ => Original_Node (Decl), + Gen_Id => Corresponding_Spec_Of (Decl)); + end if; + + Next (Decl); + end loop; + + -- The owner of the declarations is a package [body] + + if Present (Pack_Decl) then - -- State refinements are visible upto the end the of the package body - -- declarations. Hide the refinements from visibility to restore the - -- original state conditions. + -- Capture all global references in a generic package or a body + -- after all nested generic subprograms and bodies were subjected + -- to the same processing. - if In_Package_Body then - Remove_Visible_Refinements (Spec_Id); + if Is_Generic_Declaration_Or_Body (Pack_Decl) then + Save_Global_References_In_Contract + (Templ => Original_Node (Pack_Decl), + Gen_Id => Corresponding_Spec_Of (Pack_Decl)); + end if; + + -- State refinements are visible upto the end the of the package + -- body declarations. Hide the state refinements from visibility + -- to restore the original state conditions. + + if Nkind (Pack_Decl) = N_Package_Body then + Remove_Visible_Refinements (Corresponding_Spec (Pack_Decl)); + end if; + end if; end if; end Analyze_Declarations; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index d31cd905a96..42fb1ddd2f2 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1154,6 +1154,19 @@ package body Sem_Ch6 is if Nkind (N) /= N_Subprogram_Body_Stub then New_N := Copy_Generic_Node (N, Empty, Instantiating => False); Rewrite (N, New_N); + + -- Once the contents of the generic copy and the template are + -- swapped, do the same for their respective aspect specifications. + + Exchange_Aspects (N, New_N); + + -- Collect all contract-related source pragmas found within the + -- template and attach them to the contract of the subprogram body. + -- This contract is used in the capture of global references within + -- annotations. + + Create_Generic_Contract (N); + Start_Generic; end if; @@ -1293,10 +1306,35 @@ package body Sem_Ch6 is Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Body_Id, True); + -- Analyze any aspect specifications that appear on the generic + -- subprogram body. + + if Has_Aspects (N) then + Analyze_Aspect_Specifications_On_Body_Or_Stub (N); + end if; + Analyze_Declarations (Declarations (N)); Check_Completion; - Analyze (Handled_Statement_Sequence (N)); + -- When a generic subprogram body appears inside a package, its + -- contract is analyzed at the end of the package body declarations. + -- This is due to the delay with respect of the package contract upon + -- which the body contract may depend. When the generic subprogram + -- body is a compilation unit, this delay is not necessary. + + if Nkind (Parent (N)) = N_Compilation_Unit then + Analyze_Subprogram_Body_Contract (Body_Id); + + -- Capture all global references in a generic subprogram body + -- that acts as a compilation unit now that the contract has + -- been analyzed. + + Save_Global_References_In_Contract + (Templ => Original_Node (N), + Gen_Id => Gen_Id); + end if; + + Analyze (Handled_Statement_Sequence (N)); Save_Global_References (Original_Node (N)); -- Prior to exiting the scope, include generic formals again (if any @@ -2125,53 +2163,57 @@ package body Sem_Ch6 is -------------------------------------- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is - Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); + Items : constant Node_Id := Contract (Body_Id); + Mode : SPARK_Mode_Type; + Prag : Node_Id; + Prag_Nam : Name_Id; + Ref_Depends : Node_Id := Empty; + Ref_Global : Node_Id := Empty; - procedure Analyze_Completion_Contract (Spec_Id : Entity_Id); - -- Analyze all delayed pragmas chained on the contract of subprogram - -- body Body_Id as if they appeared at the end of a declarative region. - -- Spec_Id denotes the corresponding spec. The aspects in question are: - -- Refined_Depends - -- Refined_Global - -- Note that pragma Refined_Post is analyzed immediately + begin + -- When a subprogram body declaration is illegal, its defining entity is + -- left unanalyzed. There is nothing left to do in this case because the + -- body lacks a contract, or even a proper Ekind. - --------------------------------- - -- Analyze_Completion_Contract -- - --------------------------------- + if Ekind (Body_Id) = E_Void then + return; + end if; - procedure Analyze_Completion_Contract (Spec_Id : Entity_Id) is - Items : constant Node_Id := Contract (Body_Id); - Prag : Node_Id; - Prag_Nam : Name_Id; - Ref_Depends : Node_Id := Empty; - Ref_Global : Node_Id := Empty; + -- Due to the timing of contract analysis, delayed pragmas may be + -- subject to the wrong SPARK_Mode, usually that of the enclosing + -- context. To remedy this, restore the original SPARK_Mode of the + -- related subprogram body. - begin - -- All subprograms carry a contract, but for some it is not - -- significant and should not be processed. + Save_SPARK_Mode_And_Set (Body_Id, Mode); - if not Has_Significant_Contract (Spec_Id) then - return; + -- All subprograms carry a contract, but for some it is not significant + -- and should not be processed. - elsif Present (Items) then + if not Has_Significant_Contract (Body_Id) then + null; - -- Locate and store pragmas Refined_Depends and Refined_Global - -- since their order of analysis matters. + -- The subprogram body is a completion, analyze all delayed pragmas that + -- apply. Note that when the body is stand alone, the pragmas are always + -- analyzed on the spot. - Prag := Classifications (Items); - while Present (Prag) loop - Prag_Nam := Pragma_Name (Prag); + elsif Present (Items) then - if Prag_Nam = Name_Refined_Depends then - Ref_Depends := Prag; + -- Locate and store pragmas Refined_Depends and Refined_Global since + -- their order of analysis matters. - elsif Prag_Nam = Name_Refined_Global then - Ref_Global := Prag; - end if; + Prag := Classifications (Items); + while Present (Prag) loop + Prag_Nam := Pragma_Name (Prag); - Prag := Next_Pragma (Prag); - end loop; - end if; + if Prag_Nam = Name_Refined_Depends then + Ref_Depends := Prag; + + elsif Prag_Nam = Name_Refined_Global then + Ref_Global := Prag; + end if; + + Prag := Next_Pragma (Prag); + end loop; -- Analyze Refined_Global first as Refined_Depends may mention items -- classified in the global refinement. @@ -2186,43 +2228,6 @@ package body Sem_Ch6 is if Present (Ref_Depends) then Analyze_Refined_Depends_In_Decl_Part (Ref_Depends); end if; - end Analyze_Completion_Contract; - - -- Local variables - - Mode : SPARK_Mode_Type; - Spec_Id : Entity_Id; - - -- Start of processing for Analyze_Subprogram_Body_Contract - - begin - -- When a subprogram body declaration is illegal, its defining entity is - -- left unanalyzed. There is nothing left to do in this case because the - -- body lacks a contract, or even a proper Ekind. - - if Ekind (Body_Id) = E_Void then - return; - end if; - - -- Due to the timing of contract analysis, delayed pragmas may be - -- subject to the wrong SPARK_Mode, usually that of the enclosing - -- context. To remedy this, restore the original SPARK_Mode of the - -- related subprogram body. - - Save_SPARK_Mode_And_Set (Body_Id, Mode); - - if Nkind (Body_Decl) = N_Subprogram_Body_Stub then - Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); - else - Spec_Id := Corresponding_Spec (Body_Decl); - end if; - - -- The subprogram body is a completion, analyze all delayed pragmas that - -- apply. Note that when the body is stand alone, the pragmas are always - -- analyzed on the spot. - - if Present (Spec_Id) then - Analyze_Completion_Contract (Spec_Id); end if; -- Ensure that the contract cases or postconditions mention 'Result or @@ -2276,10 +2281,6 @@ package body Sem_Ch6 is -- chained beyond that point. It is initialized to Empty to deal with -- the case where there is no separate spec. - procedure Analyze_Aspects_On_Body_Or_Stub; - -- Analyze the aspect specifications of a subprogram body [stub]. It is - -- assumed that N has aspects. - function Body_Has_Contract return Boolean; -- Check whether unanalyzed body has an aspect or pragma that may -- generate a SPARK contract. @@ -2338,127 +2339,6 @@ package body Sem_Ch6 is -- indicator, check that it is consistent with the known status of the -- entity. - ------------------------------------- - -- Analyze_Aspects_On_Body_Or_Stub -- - ------------------------------------- - - procedure Analyze_Aspects_On_Body_Or_Stub is - procedure Diagnose_Misplaced_Aspects; - -- Subprogram body [stub] N has aspects, but they are not properly - -- placed. Provide precise diagnostics depending on the aspects - -- involved. - - -------------------------------- - -- Diagnose_Misplaced_Aspects -- - -------------------------------- - - procedure Diagnose_Misplaced_Aspects is - Asp : Node_Id; - Asp_Nam : Name_Id; - Asp_Id : Aspect_Id; - -- The current aspect along with its name and id - - procedure SPARK_Aspect_Error (Ref_Nam : Name_Id); - -- Emit an error message concerning SPARK aspect Asp. Ref_Nam is - -- the name of the refined version of the aspect. - - ------------------------ - -- SPARK_Aspect_Error -- - ------------------------ - - procedure SPARK_Aspect_Error (Ref_Nam : Name_Id) is - begin - -- The corresponding spec already contains the aspect in - -- question and the one appearing on the body must be the - -- refined form: - - -- procedure P with Global ...; - -- procedure P with Global ... is ... end P; - -- ^ - -- Refined_Global - - if Has_Aspect (Spec_Id, Asp_Id) then - Error_Msg_Name_1 := Asp_Nam; - - -- Subunits cannot carry aspects that apply to a subprogram - -- declaration. - - if Nkind (Parent (N)) = N_Subunit then - Error_Msg_N ("aspect % cannot apply to a subunit", Asp); - - else - Error_Msg_Name_2 := Ref_Nam; - Error_Msg_N ("aspect % should be %", Asp); - end if; - - -- Otherwise the aspect must appear in the spec, not in the - -- body: - - -- procedure P; - -- procedure P with Global ... is ... end P; - - else - Error_Msg_N - ("aspect specification must appear in subprogram " - & "declaration", Asp); - end if; - end SPARK_Aspect_Error; - - -- Start of processing for Diagnose_Misplaced_Aspects - - begin - -- Iterate over the aspect specifications and emit specific errors - -- where applicable. - - Asp := First (Aspect_Specifications (N)); - while Present (Asp) loop - Asp_Nam := Chars (Identifier (Asp)); - Asp_Id := Get_Aspect_Id (Asp_Nam); - - -- Do not emit errors on aspects that can appear on a - -- subprogram body. This scenario occurs when the aspect - -- specification list contains both misplaced and properly - -- placed aspects. - - if Aspect_On_Body_Or_Stub_OK (Asp_Id) then - null; - - -- Special diagnostics for SPARK aspects - - elsif Asp_Nam = Name_Depends then - SPARK_Aspect_Error (Name_Refined_Depends); - - elsif Asp_Nam = Name_Global then - SPARK_Aspect_Error (Name_Refined_Global); - - elsif Asp_Nam = Name_Post then - SPARK_Aspect_Error (Name_Refined_Post); - - else - Error_Msg_N - ("aspect specification must appear in subprogram " - & "declaration", Asp); - end if; - - Next (Asp); - end loop; - end Diagnose_Misplaced_Aspects; - - -- Start of processing for Analyze_Aspects_On_Body_Or_Stub - - begin - -- Language-defined aspects cannot be associated with a subprogram - -- body [stub] if the subprogram has a spec. Certain implementation - -- defined aspects are allowed to break this rule (for list, see - -- table Aspect_On_Body_Or_Stub_OK). - - if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then - Diagnose_Misplaced_Aspects; - else - Analyze_Aspect_Specifications (N, Body_Id); - end if; - end Analyze_Aspects_On_Body_Or_Stub; - ----------------------- -- Body_Has_Contract -- ----------------------- @@ -3637,18 +3517,15 @@ package body Sem_Ch6 is Set_Has_Completion (Body_Id); Check_Eliminated (Body_Id); - if Nkind (N) = N_Subprogram_Body_Stub then - - -- Analyze any aspect specifications that appear on the subprogram - -- body stub. + -- Analyze any aspect specifications that appear on the subprogram body + -- stub. Stop the analysis now as the stub does not have a declarative + -- or a statement part, and it cannot be inlined. + if Nkind (N) = N_Subprogram_Body_Stub then if Has_Aspects (N) then - Analyze_Aspects_On_Body_Or_Stub; + Analyze_Aspect_Specifications_On_Body_Or_Stub (N); end if; - -- Stop the analysis now as the stub cannot be inlined, plus it does - -- not have declarative or statement lists. - return; end if; @@ -3830,7 +3707,7 @@ package body Sem_Ch6 is -- Analyze any aspect specifications that appear on the subprogram body if Has_Aspects (N) then - Analyze_Aspects_On_Body_Or_Stub; + Analyze_Aspect_Specifications_On_Body_Or_Stub (N); end if; Analyze_Declarations (Declarations (N)); @@ -4119,57 +3996,14 @@ package body Sem_Ch6 is --------------------------------- procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is - procedure Save_Global_References_In_List (First_Prag : Node_Id); - -- Save all global references in contract-related source pragma found in - -- the list starting from pragma First_Prag. - - ------------------------------------ - -- Save_Global_References_In_List -- - ------------------------------------ - - procedure Save_Global_References_In_List (First_Prag : Node_Id) is - Prag : Node_Id; - - begin - Prag := First_Prag; - while Present (Prag) loop - if Comes_From_Source (Prag) - and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases, - Name_Depends, - Name_Extensions_Visible, - Name_Global, - Name_Postcondition, - Name_Precondition, - Name_Test_Case) - then - Save_Global_References (Original_Node (Prag)); - end if; - - Prag := Next_Pragma (Prag); - end loop; - end Save_Global_References_In_List; - - -- Local variables - - Items : constant Node_Id := Contract (Subp_Id); - Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); - Depends : Node_Id := Empty; - Global : Node_Id := Empty; - Mode : SPARK_Mode_Type; - Prag : Node_Id; - Prag_Nam : Name_Id; - Restore_Scope : Boolean := False; - - -- Start of processing for Analyze_Subprogram_Contract + Items : constant Node_Id := Contract (Subp_Id); + Depends : Node_Id := Empty; + Global : Node_Id := Empty; + Mode : SPARK_Mode_Type; + Prag : Node_Id; + Prag_Nam : Name_Id; begin - -- All subprograms carry a contract, but for some it is not significant - -- and should not be processed. - - if not Has_Significant_Contract (Subp_Id) then - return; - end if; - -- Due to the timing of contract analysis, delayed pragmas may be -- subject to the wrong SPARK_Mode, usually that of the enclosing -- context. To remedy this, restore the original SPARK_Mode of the @@ -4177,21 +4011,13 @@ package body Sem_Ch6 is Save_SPARK_Mode_And_Set (Subp_Id, Mode); - -- Ensure that the formal parameters are visible when analyzing all - -- contract items. - - if not In_Open_Scopes (Subp_Id) then - Restore_Scope := True; - Push_Scope (Subp_Id); + -- All subprograms carry a contract, but for some it is not significant + -- and should not be processed. - if Is_Generic_Subprogram (Subp_Id) then - Install_Generic_Formals (Subp_Id); - else - Install_Formals (Subp_Id); - end if; - end if; + if not Has_Significant_Contract (Subp_Id) then + null; - if Present (Items) then + elsif Present (Items) then -- Analyze pre- and postconditions @@ -4256,35 +4082,6 @@ package body Sem_Ch6 is Check_Result_And_Post_State (Subp_Id); end if; - -- The aspects and contract-related source pragmas associated with a - -- generic subprogram are treated separately from the declaration as - -- they need to be analyzed when the subprogram contract is analyzed. - -- Once this is done, global references can be successfully saved. - - if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then - - -- Save all global references found in the aspect specifications of - -- the parameter profile of the generic subprogram. - - Save_Global_References_In_Aspects (Original_Node (Subp_Decl)); - - -- Save all global references found in contract-related source - -- pragmas. These pragmas usually appear after the declaration of - -- the generic subprogram, either in the same declarative part or - -- in the Pragmas_After list when the generic subprogram is a - -- compilation unit. - - if Present (Items) then - Save_Global_References_In_List (Pre_Post_Conditions (Items)); - Save_Global_References_In_List (Contract_Test_Cases (Items)); - Save_Global_References_In_List (Classifications (Items)); - end if; - end if; - - if Restore_Scope then - End_Scope; - end if; - -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 8af1f346ebc..3369fad4aa8 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -187,9 +187,9 @@ package body Sem_Ch7 is ----------------------------------- procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is - Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); - Mode : SPARK_Mode_Type; - Prag : Node_Id; + Spec_Id : constant Entity_Id := Spec_Entity (Body_Id); + Mode : SPARK_Mode_Type; + Ref_State : Node_Id; begin -- Due to the timing of contract analysis, delayed pragmas may be @@ -199,13 +199,13 @@ package body Sem_Ch7 is Save_SPARK_Mode_And_Set (Body_Id, Mode); - Prag := Get_Pragma (Body_Id, Pragma_Refined_State); + Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State); -- The analysis of pragma Refined_State detects whether the spec has -- abstract states available for refinement. - if Present (Prag) then - Analyze_Refined_State_In_Decl_Part (Prag); + if Present (Ref_State) then + Analyze_Refined_State_In_Decl_Part (Ref_State); -- State refinement is required when the package declaration defines at -- least one abstract state. Null states are not considered. Refinement @@ -677,6 +677,13 @@ package body Sem_Ch7 is Exchange_Aspects (N, New_N); + -- Collect all contract-related source pragmas found within the + -- template and attach them to the contract of the package body. + -- This contract is used in the capture of global references within + -- annotations. + + Create_Generic_Contract (N); + -- Update Body_Id to point to the copied node for the remainder of -- the processing. @@ -940,8 +947,12 @@ package body Sem_Ch7 is ------------------------------ procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is - Mode : SPARK_Mode_Type; - Prag : Node_Id; + Items : constant Node_Id := Contract (Pack_Id); + Init : Node_Id := Empty; + Init_Cond : Node_Id := Empty; + Mode : SPARK_Mode_Type; + Prag : Node_Id; + Prag_Nam : Name_Id; begin -- Due to the timing of contract analysis, delayed pragmas may be @@ -951,19 +962,35 @@ package body Sem_Ch7 is Save_SPARK_Mode_And_Set (Pack_Id, Mode); - -- Analyze the initialization related pragmas. Initializes must come - -- before Initial_Condition due to item dependencies. + if Present (Items) then - Prag := Get_Pragma (Pack_Id, Pragma_Initializes); + -- Locate and store pragmas Initial_Condition and Initializes since + -- their order of analysis matters. - if Present (Prag) then - Analyze_Initializes_In_Decl_Part (Prag); - end if; + Prag := Classifications (Items); + while Present (Prag) loop + Prag_Nam := Pragma_Name (Prag); - Prag := Get_Pragma (Pack_Id, Pragma_Initial_Condition); + if Prag_Nam = Name_Initial_Condition then + Init_Cond := Prag; - if Present (Prag) then - Analyze_Initial_Condition_In_Decl_Part (Prag); + elsif Prag_Nam = Name_Initializes then + Init := Prag; + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Analyze the initialization related pragmas. Initializes must come + -- before Initial_Condition due to item dependencies. + + if Present (Init) then + Analyze_Initializes_In_Decl_Part (Init); + end if; + + if Present (Init_Cond) then + Analyze_Initial_Condition_In_Decl_Part (Init_Cond); + end if; end if; -- Check whether the lack of indicator Part_Of agrees with the placement diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index ede76850ad7..758aed07a72 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -204,10 +204,10 @@ package body Sem_Prag is procedure Check_Postcondition_Use_In_Inlined_Subprogram (Prag : Node_Id; - Subp_Id : Entity_Id); + Spec_Id : Entity_Id); -- Subsidiary to the analysis of pragmas Contract_Cases, Postcondition, -- Precondition, Refined_Post and Test_Case. Emit a warning when pragma - -- Prag is associated with subprogram Subp_Id subject to Inline_Always. + -- Prag is associated with subprogram Spec_Id subject to Inline_Always. procedure Check_State_And_Constituent_Use (States : Elist_Id; @@ -223,29 +223,6 @@ package body Sem_Prag is -- Find_Related_Subprogram_Or_Body. Emit an error on pragma Prag that -- duplicates previous pragma Prev. - function Find_Related_Package_Or_Body - (Prag : Node_Id; - Do_Checks : Boolean := False) return Node_Id; - -- Subsidiary to the analysis of pragmas Abstract_State, Initial_Condition, - -- Initializes and Refined_State. Find the declaration of the related - -- package [body] subject to pragma Prag. The return value is either - -- N_Package_Declaration, N_Package_Body or Empty if the placement of - -- the pragma is illegal. If flag Do_Checks is set, the routine reports - -- duplicate pragmas. - - function Get_Argument - (Prag : Node_Id; - Spec_Id : Entity_Id := Empty) return Node_Id; - -- Obtain the argument of pragma Prag depending on context and the nature - -- of the pragma. The argument is extracted in the following manner: - -- - -- When the pragma is generated from an aspect, return the corresponding - -- aspect for ASIS or when Spec_Id denotes a generic subprogram. - -- - -- Otherwise return the first argument of Prag - -- - -- Spec_Id denotes the entity of the subprogram spec where Prag resides - function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id; -- If Def_Id refers to a renamed subprogram, then the base subprogram (the -- original one, following the renaming chain) is returned. Otherwise the @@ -432,37 +409,29 @@ package body Sem_Prag is -- Local variables - All_Cases : Node_Id; - CCase : Node_Id; - Spec_Id : Entity_Id; - Subp_Decl : Node_Id; - Subp_Id : Entity_Id; + Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); + CCase : Node_Id; Restore_Scope : Boolean := False; - -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit -- Start of processing for Analyze_Contract_Cases_In_Decl_Part begin Set_Analyzed (N); - Subp_Decl := Find_Related_Subprogram_Or_Body (N); - Spec_Id := Corresponding_Spec_Of (Subp_Decl); - Subp_Id := Defining_Entity (Subp_Decl); - All_Cases := Expression (Get_Argument (N, Subp_Id)); - -- Single and multiple contract cases must appear in aggregate form. If -- this is not the case, then either the parser of the analysis of the -- pragma failed to produce an aggregate. - pragma Assert (Nkind (All_Cases) = N_Aggregate); + pragma Assert (Nkind (CCases) = N_Aggregate); - if Present (Component_Associations (All_Cases)) then + if Present (Component_Associations (CCases)) then -- Ensure that the formal parameters are visible when analyzing all -- clauses. This falls out of the general rule of aspects pertaining - -- to subprogram declarations. Skip the installation for subprogram - -- bodies because the formals are already visible. + -- to subprogram declarations. if not In_Open_Scopes (Spec_Id) then Restore_Scope := True; @@ -475,20 +444,23 @@ package body Sem_Prag is end if; end if; - CCase := First (Component_Associations (All_Cases)); + CCase := First (Component_Associations (CCases)); while Present (CCase) loop Analyze_Contract_Case (CCase); Next (CCase); end loop; + if Restore_Scope then + End_Scope; + end if; + -- Currently it is not possible to inline pre/postconditions on a -- subprogram subject to pragma Inline_Always. Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); - if Restore_Scope then - End_Scope; - end if; + -- Otherwise the pragma is illegal + else Error_Msg_N ("wrong syntax for constract cases", N); end if; @@ -499,7 +471,9 @@ package body Sem_Prag is ---------------------------------- procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is - Loc : constant Source_Ptr := Sloc (N); + Loc : constant Source_Ptr := Sloc (N); + Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); All_Inputs_Seen : Elist_Id := No_Elist; -- A list containing the entities of all the inputs processed so far. @@ -525,18 +499,11 @@ package body Sem_Prag is Result_Seen : Boolean := False; -- A flag set when Subp_Id'Result is processed - Spec_Id : Entity_Id; - -- The entity of the subprogram subject to pragma [Refined_]Depends - States_Seen : Elist_Id := No_Elist; -- A list containing the entities of all states processed so far. It -- helps in detecting illegal usage of a state and a corresponding -- constituent in pragma [Refined_]Depends. - Subp_Id : Entity_Id; - -- The entity of the subprogram [body or stub] subject to pragma - -- [Refined_]Depends. - Subp_Inputs : Elist_Id := No_Elist; Subp_Outputs : Elist_Id := No_Elist; -- Two lists containing the full set of inputs and output of the related @@ -545,11 +512,14 @@ package body Sem_Prag is procedure Add_Item_To_Name_Buffer (Item_Id : Entity_Id); -- Subsidiary routine to Check_Role and Check_Usage. Add the item kind -- to the name buffer. The individual kinds are as follows: - -- E_Abstract_State - "state" - -- E_In_Parameter - "parameter" - -- E_In_Out_Parameter - "parameter" - -- E_Out_Parameter - "parameter" - -- E_Variable - "global" + -- E_Abstract_State - "state" + -- E_Constant - "constant" + -- E_Generic_In_Out_Parameter - "generic parameter" + -- E_Generic_Out_Parameter - "generic parameter" + -- E_In_Parameter - "parameter" + -- E_In_Out_Parameter - "parameter" + -- E_Out_Parameter - "parameter" + -- E_Variable - "global" procedure Analyze_Dependency_Clause (Clause : Node_Id; @@ -592,6 +562,14 @@ package body Sem_Prag is if Ekind (Item_Id) = E_Abstract_State then Add_Str_To_Name_Buffer ("state"); + elsif Ekind (Item_Id) = E_Constant then + Add_Str_To_Name_Buffer ("constant"); + + elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter, + E_Generic_In_Parameter) + then + Add_Str_To_Name_Buffer ("generic parameter"); + elsif Is_Formal (Item_Id) then Add_Str_To_Name_Buffer ("parameter"); @@ -629,7 +607,7 @@ package body Sem_Prag is -- denotes an output. Flag Self_Ref should be set when the item is an -- output and the dependency clause has a "+". Flag Top_Level should -- be set whenever Item appears immediately within an input or output - -- list. Seen is a collection of all abstract states, variables and + -- list. Seen is a collection of all abstract states, objects and -- formals processed so far. Flag Null_Seen denotes whether a null -- input or output has been encountered. Flag Non_Null_Seen denotes -- whether a non-null input or output has been encountered. @@ -753,32 +731,17 @@ package body Sem_Prag is Error_Msg_N ("malformed dependency list", Item); end if; - -- Process Function'Result in the context of a dependency clause + -- Process attribute 'Result in the context of a dependency clause elsif Is_Attribute_Result (Item) then Non_Null_Seen := True; - -- It is sufficent to analyze the prefix of 'Result in order to - -- establish legality of the attribute. - - Analyze (Prefix (Item)); - - -- The prefix of 'Result must denote the function for which - -- pragma Depends applies (SPARK RM 6.1.5(11)). + Analyze (Item); - if not Is_Entity_Name (Prefix (Item)) - or else Ekind (Spec_Id) /= E_Function - or else Entity (Prefix (Item)) /= Spec_Id - then - Error_Msg_Name_1 := Name_Result; - SPARK_Msg_N - ("prefix of attribute % must denote the enclosing " - & "function", Item); + -- Attribute 'Result is allowed to appear on the output side of + -- a dependency clause (SPARK RM 6.1.5(6)). - -- Function'Result is allowed to appear on the output side of a - -- dependency clause (SPARK RM 6.1.5(6)). - - elsif Is_Input then + if Is_Input then SPARK_Msg_N ("function result cannot act as input", Item); elsif Null_Seen then @@ -841,6 +804,9 @@ package body Sem_Prag is if Present (Item_Id) then if Ekind_In (Item_Id, E_Abstract_State, + E_Constant, + E_Generic_In_Out_Parameter, + E_Generic_In_Parameter, E_In_Parameter, E_In_Out_Parameter, E_Out_Parameter, @@ -886,9 +852,26 @@ package body Sem_Prag is -- State related checks (SPARK RM 6.1.5(3)) if Ekind (Item_Id) = E_Abstract_State then - if Has_Visible_Refinement (Item_Id) then + + -- Package and subprogram bodies are instantiated + -- individually in a separate compiler pass. Due to + -- this mode of instantiation, the refinement of a + -- state may no longer be visible when a subprogram + -- body contract is instantiated. Since the generic + -- template is legal, do not perform this check in + -- the instance to circumvent this oddity. + + if Is_Generic_Instance (Spec_Id) then + null; + + -- An abstract state with visible refinement cannot + -- appear in pragma [Refined_]Depends as its place + -- must be taken by some of its constituents + -- (SPARK RM 6.1.4(7)). + + elsif Has_Visible_Refinement (Item_Id) then SPARK_Msg_NE - ("cannot mention state & in global refinement", + ("cannot mention state & in dependence relation", Item, Item_Id); SPARK_Msg_N ("\use its constituents instead", Item); return; @@ -908,7 +891,7 @@ package body Sem_Prag is -- When the item renames an entire object, replace the -- item with a reference to the object. - if Present (Renamed_Object (Entity (Item))) then + if Entity (Item) /= Item_Id then Rewrite (Item, New_Occurrence_Of (Item_Id, Sloc (Item))); Analyze (Item); @@ -921,7 +904,9 @@ package body Sem_Prag is Add_Item (Item_Id, States_Seen); end if; - if Ekind_In (Item_Id, E_Abstract_State, E_Variable) + if Ekind_In (Item_Id, E_Abstract_State, + E_Constant, + E_Variable) and then Present (Encapsulating_State (Item_Id)) then Add_Item (Item_Id, Constits_Seen); @@ -996,7 +981,9 @@ package body Sem_Prag is procedure Check_Function_Return is begin - if Ekind (Spec_Id) = E_Function and then not Result_Seen then + if Ekind_In (Spec_Id, E_Function, E_Generic_Function) + and then not Result_Seen + then SPARK_Msg_NE ("result of & must appear in exactly one output list", N, Spec_Id); @@ -1061,6 +1048,15 @@ package body Sem_Prag is Item_Is_Output := True; end if; + -- Generic parameter cases + + elsif Ekind (Item_Id) = E_Generic_In_Parameter then + Item_Is_Input := True; + + elsif Ekind (Item_Id) = E_Generic_In_Out_Parameter then + Item_Is_Input := True; + Item_Is_Output := True; + -- Parameter cases elsif Ekind (Item_Id) = E_In_Parameter then @@ -1091,16 +1087,16 @@ package body Sem_Prag is Item_Is_Output := True; end if; - -- Variable cases + -- Object cases - else pragma Assert (Ekind (Item_Id) = E_Variable); + else pragma Assert (Ekind_In (Item_Id, E_Constant, E_Variable)); - -- When pragma Global is present, the mode of the variable may + -- When pragma Global is present, the mode of the object may -- be further constrained by setting a more restrictive mode. if Global_Seen then - -- A variable has mode IN when its type is unconstrained or + -- An object has mode IN when its type is unconstrained or -- tagged because array bounds, discriminants or tags can be -- read. @@ -1114,7 +1110,7 @@ package body Sem_Prag is Item_Is_Output := True; end if; - -- Otherwise the variable has a default IN OUT mode + -- Otherwise the object has a default IN OUT mode else Item_Is_Input := True; @@ -1148,7 +1144,7 @@ package body Sem_Prag is Error_Msg := Name_Find; SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id); - Error_Msg_Name_1 := Chars (Subp_Id); + Error_Msg_Name_1 := Chars (Spec_Id); SPARK_Msg_NE ("\& is not part of the input or output set of subprogram %", Item, Item_Id); @@ -1299,7 +1295,7 @@ package body Sem_Prag is if Is_Formal (Item_Id) then Usage_Error (Item, Item_Id); - -- States and global variables are not used properly only when + -- States and global objects are not used properly only when -- the subprogram is subject to pragma Global. elsif Global_Seen then @@ -1348,8 +1344,8 @@ package body Sem_Prag is (Output : Node_Id; Inputs : Node_Id); -- Handle the various cases of output propagation to the input - -- list. Output denotes a self-referencial output item. Inputs is - -- the input list of a clause. + -- list. Output denotes a self-referencial output item. Inputs + -- is the input list of a clause. ---------------------- -- Propagate_Output -- @@ -1467,10 +1463,10 @@ package body Sem_Prag is end if; -- When performing the transformation in place, simply add the - -- output to the list of inputs (if not already there). This case - -- arises when dealing with the last output of an output list - - -- we perform the normalization in place to avoid generating a - -- malformed tree. + -- output to the list of inputs (if not already there). This + -- case arises when dealing with the last output of an output + -- list. Perform the normalization in place to avoid generating + -- a malformed tree. if In_Place then Propagate_Output (Output, Inputs); @@ -1503,8 +1499,8 @@ package body Sem_Prag is Expression => New_Copy_Tree (Inputs)); -- The new clause contains replicated content that has already - -- been analyzed. There is not need to reanalyze it or - -- renormalize it again. + -- been analyzed. There is not need to reanalyze or renormalize + -- it again. Set_Analyzed (New_Clause); @@ -1574,36 +1570,24 @@ package body Sem_Prag is -- Local variables - Clause : Node_Id; - Deps : Node_Id; - Errors : Nat; - Last_Clause : Node_Id; - Subp_Decl : Node_Id; + Deps : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); + Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl); + Clause : Node_Id; + Errors : Nat; + Last_Clause : Node_Id; Restore_Scope : Boolean := False; - -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit -- Start of processing for Analyze_Depends_In_Decl_Part begin Set_Analyzed (N); - Subp_Decl := Find_Related_Subprogram_Or_Body (N); - Subp_Id := Defining_Entity (Subp_Decl); - Deps := Expression (Get_Argument (N, Subp_Id)); - - -- The logic in this routine is used to analyze both pragma Depends and - -- pragma Refined_Depends since they have the same syntax and base - -- semantics. Find the entity of the corresponding spec when analyzing - -- Refined_Depends. - - Spec_Id := Corresponding_Spec_Of (Subp_Decl); - -- Empty dependency list if Nkind (Deps) = N_Null then - -- Gather all states, variables and formal parameters that the + -- Gather all states, objects and formal parameters that the -- subprogram may depend on. These items are obtained from the -- parameter profile or pragma [Refined_]Global (if available). @@ -1634,7 +1618,7 @@ package body Sem_Prag is if Present (Component_Associations (Deps)) then Last_Clause := Last (Component_Associations (Deps)); - -- Gather all states, variables and formal parameters that the + -- Gather all states, objects and formal parameters that the -- subprogram may depend on. These items are obtained from the -- parameter profile or pragma [Refined_]Global (if available). @@ -1646,8 +1630,7 @@ package body Sem_Prag is -- Ensure that the formal parameters are visible when analyzing -- all clauses. This falls out of the general rule of aspects - -- pertaining to subprogram declarations. Skip the installation - -- for subprogram bodies because the formals are already visible. + -- pertaining to subprogram declarations. if not In_Open_Scopes (Spec_Id) then Restore_Scope := True; @@ -1664,9 +1647,9 @@ package body Sem_Prag is while Present (Clause) loop Errors := Serious_Errors_Detected; - -- Normalization may create extra clauses that contain - -- replicated input and output names. There is no need to - -- reanalyze them. + -- The normalization mechanism may create extra clauses that + -- contain replicated input and output names. There is no need + -- to reanalyze them. if not Analyzed (Clause) then Set_Analyzed (Clause); @@ -1775,6 +1758,10 @@ package body Sem_Prag is --------------------------------- procedure Analyze_Global_In_Decl_Part (N : Node_Id) is + Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl); + Constits_Seen : Elist_Id := No_Elist; -- A list containing the entities of all constituents processed so far. -- It aids in detecting illegal usage of a state and a corresponding @@ -1784,18 +1771,11 @@ package body Sem_Prag is -- A list containing the entities of all the items processed so far. It -- plays a role in detecting distinct entities. - Spec_Id : Entity_Id; - -- The entity of the subprogram subject to pragma [Refined_]Global - States_Seen : Elist_Id := No_Elist; -- A list containing the entities of all states processed so far. It -- helps in detecting illegal usage of a state and a corresponding -- constituent in pragma [Refined_]Global. - Subp_Id : Entity_Id; - -- The entity of the subprogram [body or stub] subject to pragma - -- [Refined_]Global. - In_Out_Seen : Boolean := False; Input_Seen : Boolean := False; Output_Seen : Boolean := False; @@ -1819,8 +1799,8 @@ package body Sem_Prag is procedure Analyze_Global_Item (Item : Node_Id; Global_Mode : Name_Id); - -- Verify the legality of a single global item declaration. - -- Global_Mode denotes the current mode in effect. + -- Verify the legality of a single global item declaration denoted by + -- Item. Global_Mode denotes the current mode in effect. procedure Check_Duplicate_Mode (Mode : Node_Id; @@ -1882,28 +1862,25 @@ package body Sem_Prag is if Is_Formal (Item_Id) then if Scope (Item_Id) = Spec_Id then SPARK_Msg_NE - ("global item cannot reference parameter of subprogram", - Item, Spec_Id); + ("global item cannot reference parameter of " + & "subprogram &", Item, Spec_Id); return; end if; - -- A constant cannot act as a global item (SPARK RM 6.1.4(7)). - -- Do this check first to provide a better error diagnostic. - - elsif Ekind (Item_Id) = E_Constant then - SPARK_Msg_N ("global item cannot denote a constant", Item); - -- A formal object may act as a global item inside a generic elsif Is_Formal_Object (Item_Id) then null; -- The only legal references are those to abstract states and - -- variables (SPARK RM 6.1.4(4)). + -- objects (SPARK RM 6.1.4(4)). - elsif not Ekind_In (Item_Id, E_Abstract_State, E_Variable) then + elsif not Ekind_In (Item_Id, E_Abstract_State, + E_Constant, + E_Variable) + then SPARK_Msg_N - ("global item must denote variable or state", Item); + ("global item must denote object or state", Item); return; end if; @@ -1911,11 +1888,22 @@ package body Sem_Prag is if Ekind (Item_Id) = E_Abstract_State then + -- Package and subprogram bodies are instantiated + -- individually in a separate compiler pass. Due to this + -- mode of instantiation, the refinement of a state may + -- no longer be visible when a subprogram body contract + -- is instantiated. Since the generic template is legal, + -- do not perform this check in the instance to circumvent + -- this oddity. + + if Is_Generic_Instance (Spec_Id) then + null; + -- An abstract state with visible refinement cannot appear -- in pragma [Refined_]Global as its place must be taken by - -- some of its constituents (SPARK RM 6.1.4(8)). + -- some of its constituents (SPARK RM 6.1.4(7)). - if Has_Visible_Refinement (Item_Id) then + elsif Has_Visible_Refinement (Item_Id) then SPARK_Msg_NE ("cannot mention state & in global refinement", Item, Item_Id); @@ -1937,6 +1925,7 @@ package body Sem_Prag is -- rules. elsif SPARK_Mode = On + and then Ekind (Item_Id) = E_Variable and then Is_Effectively_Volatile (Item_Id) then -- An effectively volatile object cannot appear as a global @@ -1950,15 +1939,14 @@ package body Sem_Prag is -- An effectively volatile object with external property -- Effective_Reads set to True must have mode Output or - -- In_Out. + -- In_Out (SPARK RM 7.1.3(11)). elsif Effective_Reads_Enabled (Item_Id) and then Global_Mode = Name_Input then Error_Msg_NE ("volatile object & with property Effective_Reads must " - & "have mode In_Out or Output (SPARK RM 7.1.3(11))", - Item, Item_Id); + & "have mode In_Out or Output", Item, Item_Id); return; end if; end if; @@ -1966,7 +1954,7 @@ package body Sem_Prag is -- When the item renames an entire object, replace the item -- with a reference to the object. - if Present (Renamed_Object (Entity (Item))) then + if Entity (Item) /= Item_Id then Rewrite (Item, New_Occurrence_Of (Item_Id, Sloc (Item))); Analyze (Item); end if; @@ -1975,7 +1963,7 @@ package body Sem_Prag is -- (SPARK RM 6.1.4(4)). else - Error_Msg_N ("global item must denote variable or state", Item); + Error_Msg_N ("global item must denote object or state", Item); return; end if; @@ -1988,7 +1976,7 @@ package body Sem_Prag is -- The same entity might be referenced through various way. -- Check the entity of the item rather than the item itself - -- (SPARK RM 6.1.4(11)). + -- (SPARK RM 6.1.4(10)). if Contains (Seen, Item_Id) then SPARK_Msg_N ("duplicate global item", Item); @@ -2003,7 +1991,7 @@ package body Sem_Prag is Add_Item (Item_Id, States_Seen); end if; - if Ekind_In (Item_Id, E_Abstract_State, E_Variable) + if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable) and then Present (Encapsulating_State (Item_Id)) then Add_Item (Item_Id, Constits_Seen); @@ -2059,7 +2047,7 @@ package body Sem_Prag is Global_Seen => Dummy); -- The item is classified as In_Out or Output but appears as - -- an Input in an enclosing subprogram (SPARK RM 6.1.4(12)). + -- an Input in an enclosing subprogram (SPARK RM 6.1.4(11)). if Appears_In (Inputs, Item_Id) and then not Appears_In (Outputs, Item_Id) @@ -2087,7 +2075,7 @@ package body Sem_Prag is procedure Check_Mode_Restriction_In_Function (Mode : Node_Id) is begin - if Ekind (Spec_Id) = E_Function then + if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then SPARK_Msg_N ("global mode & is not applicable to functions", Mode); end if; @@ -2130,7 +2118,6 @@ package body Sem_Prag is Item := First (Expressions (List)); while Present (Item) loop Analyze_Global_Item (Item, Global_Mode); - Next (Item); end loop; @@ -2198,28 +2185,15 @@ package body Sem_Prag is -- Local variables - Items : Node_Id; - Subp_Decl : Node_Id; + Items : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); Restore_Scope : Boolean := False; - -- Set True if we do a Push_Scope requiring a Pop_Scope on exit -- Start of processing for Analyze_Global_In_Decl_Part begin Set_Analyzed (N); - Subp_Decl := Find_Related_Subprogram_Or_Body (N); - Subp_Id := Defining_Entity (Subp_Decl); - Items := Expression (Get_Argument (N, Subp_Id)); - - -- The logic in this routine is used to analyze both pragma Global and - -- pragma Refined_Global since they have the same syntax and base - -- semantics. Find the entity of the corresponding spec when analyzing - -- Refined_Global. - - Spec_Id := Corresponding_Spec_Of (Subp_Decl); - -- There is nothing to be done for a null global list if Nkind (Items) = N_Null then @@ -2266,7 +2240,9 @@ package body Sem_Prag is -------------------------------------------- procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is - Expr : constant Node_Id := Expression (Get_Argument (N)); + Pack_Decl : constant Node_Id := Find_Related_Package_Or_Body (N); + Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); + Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id)); begin Set_Analyzed (N); @@ -2283,8 +2259,8 @@ package body Sem_Prag is -------------------------------------- procedure Analyze_Initializes_In_Decl_Part (N : Node_Id) is - Pack_Spec : constant Node_Id := Parent (N); - Pack_Id : constant Entity_Id := Defining_Entity (Parent (Pack_Spec)); + Pack_Decl : constant Node_Id := Find_Related_Package_Or_Body (N); + Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); Constits_Seen : Elist_Id := No_Elist; -- A list containing the entities of all constituents processed so far. @@ -2572,7 +2548,8 @@ package body Sem_Prag is ---------------------------------- procedure Collect_States_And_Variables is - Decl : Node_Id; + Pack_Spec : constant Node_Id := Specification (Pack_Decl); + Decl : Node_Id; begin -- Collect the abstract states defined in the package (if any) @@ -2601,7 +2578,7 @@ package body Sem_Prag is -- Local variables - Inits : constant Node_Id := Expression (Get_Argument (N)); + Inits : constant Node_Id := Expression (Get_Argument (N, Pack_Id)); Init : Node_Id; -- Start of processing for Analyze_Initializes_In_Decl_Part @@ -2703,6 +2680,9 @@ package body Sem_Prag is -- In Ada 95 or 05 mode, these are implementation defined pragmas, so -- should be caught by the No_Implementation_Pragmas restriction. + procedure Analyze_Depends_Global; + -- Subsidiary to the analysis of pragma Depends and Global + procedure Analyze_Part_Of (Item_Id : Entity_Id; State : Node_Id; @@ -2717,7 +2697,7 @@ package body Sem_Prag is procedure Analyze_Pre_Post_Condition; -- Subsidiary to the analysis of pragmas Precondition and Postcondition - procedure Analyze_Refined_Pragma + procedure Analyze_Refined_Depends_Global_Post (Spec_Id : out Entity_Id; Body_Id : out Entity_Id; Legal : out Boolean); @@ -2941,14 +2921,6 @@ package body Sem_Prag is -- presence of at least one component. UU_Typ is the related Unchecked_ -- Union type. - procedure Create_Generic_Template - (Prag : Node_Id; - Subp_Id : Entity_Id); - -- Subsidiary routine to the processing of pragmas Contract_Cases, - -- Depends, Global, Postcondition, Precondition and Test_Case. Create - -- a generic template for pragma Prag when Prag is a source construct - -- and the related context denoted by Subp_Id is a generic subprogram. - procedure Ensure_Aggregate_Form (Arg : Node_Id); -- Subsidiary routine to the processing of pragmas Abstract_State, -- Contract_Cases, Depends, Global, Initializes, Refined_Depends, @@ -3273,6 +3245,75 @@ package body Sem_Prag is end if; end Ada_2012_Pragma; + ---------------------------- + -- Analyze_Depends_Global -- + ---------------------------- + + procedure Analyze_Depends_Global is + Spec_Id : Entity_Id; + Subp_Decl : Node_Id; + + begin + GNAT_Pragma; + Check_Arg_Count (1); + + -- Ensure the proper placement of the pragma. Depends/Global must be + -- associated with a subprogram declaration or a body that acts as a + -- spec. + + Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True); + + -- Generic subprogram + + if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + null; + + -- Body acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body + and then No (Corresponding_Spec (Subp_Decl)) + then + null; + + -- Body stub acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + null; + + -- Subprogram declaration + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + null; + + else + Pragma_Misplaced; + return; + end if; + + Spec_Id := Corresponding_Spec_Of (Subp_Decl); + + Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); + + -- Fully analyze the pragma when it appears inside a subprogram body + -- because it cannot benefit from forward references. + + if Nkind (Subp_Decl) = N_Subprogram_Body then + if Pragma_Name (N) = Name_Depends then + Analyze_Depends_In_Decl_Part (N); + + else pragma Assert (Pname = Name_Global); + Analyze_Global_In_Decl_Part (N); + end if; + end if; + + -- Chain the pragma on the contract for further processing by + -- Analyze_Depends_In_Decl_Part/Analyze_Global_In_Decl_Part. + + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + end Analyze_Depends_Global; + --------------------- -- Analyze_Part_Of -- --------------------- @@ -3444,7 +3485,6 @@ package body Sem_Prag is procedure Analyze_Pre_Post_Condition is Prag_Iden : constant Node_Id := Pragma_Identifier (N); Subp_Decl : Node_Id; - Subp_Id : Entity_Id; Duplicates_OK : Boolean := False; -- Flag set when a pre/postcondition allows multiple pragmas of the @@ -3582,13 +3622,6 @@ package body Sem_Prag is return; end if; - Subp_Id := Defining_Entity (Subp_Decl); - - -- Construct a generic template for the pragma when the context is a - -- generic subprogram and the pragma is a source construct. - - Create_Generic_Template (N, Subp_Id); - -- Fully analyze the pragma when it appears inside a subprogram -- body because it cannot benefit from forward references. @@ -3598,16 +3631,17 @@ package body Sem_Prag is Analyze_Pre_Post_Condition_In_Decl_Part (N); end if; - -- Chain the pragma on the contract for further processing + -- Chain the pragma on the contract for further processing by + -- Analyze_Pre_Post_Condition_In_Decl_Part. - Add_Contract_Item (N, Subp_Id); + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); end Analyze_Pre_Post_Condition; - ---------------------------- - -- Analyze_Refined_Pragma -- - ---------------------------- + ----------------------------------------- + -- Analyze_Refined_Depends_Global_Post -- + ----------------------------------------- - procedure Analyze_Refined_Pragma + procedure Analyze_Refined_Depends_Global_Post (Spec_Id : out Entity_Id; Body_Id : out Entity_Id; Legal : out Boolean) @@ -3680,11 +3714,11 @@ package body Sem_Prag is Name_Refined_Global, Name_Refined_State) then - Ensure_Aggregate_Form (Get_Argument (N)); + Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); end if; Legal := True; - end Analyze_Refined_Pragma; + end Analyze_Refined_Depends_Global_Post; -------------------------- -- Check_Ada_83_Warning -- @@ -5214,23 +5248,6 @@ package body Sem_Prag is end loop; end Check_Variant; - ----------------------------- - -- Create_Generic_Template -- - ----------------------------- - - procedure Create_Generic_Template - (Prag : Node_Id; - Subp_Id : Entity_Id) - is - begin - if Comes_From_Source (Prag) - and then Is_Generic_Subprogram (Subp_Id) - then - Rewrite - (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); - end if; - end Create_Generic_Template; - --------------------------- -- Ensure_Aggregate_Form -- --------------------------- @@ -9524,6 +9541,21 @@ package body Sem_Prag is -- ABSTRACT_STATE ::= name + -- Characteristics: + + -- * Analysis - The annotation is fully analyzed immediately upon + -- elaboration as it cannot forward reference entities. + + -- * Expansion - None. + + -- * Template - The annotation utilizes the generic template of the + -- related package declaration. + + -- * Globals - The annotation cannot reference global entities. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic package is instantiated. + when Pragma_Abstract_State => Abstract_State : declare Missing_Parentheses : Boolean := False; -- Flag set when a state declaration with options is not properly @@ -10130,7 +10162,7 @@ package body Sem_Prag is -- as a component association. if Nkind (State) = N_Component_Association then - Error_Msg_N ("\\use WITH to specify simple option", State); + Error_Msg_N ("\use WITH to specify simple option", State); end if; end Malformed_State_Error; @@ -10165,9 +10197,10 @@ package body Sem_Prag is return; end if; - Ensure_Aggregate_Form (Get_Argument (N)); Pack_Id := Defining_Entity (Pack_Decl); + Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); + -- Mark the associated package as Ghost if it is subject to aspect -- or pragma Ghost as this affects the declaration of an abstract -- state. @@ -10176,7 +10209,7 @@ package body Sem_Prag is Set_Is_Ghost_Entity (Pack_Id); end if; - States := Expression (Get_Argument (N)); + States := Expression (Get_Argument (N, Pack_Id)); -- Multiple non-null abstract states appear as an aggregate @@ -10206,16 +10239,16 @@ package body Sem_Prag is Analyze_Abstract_State (States, Pack_Id); end if; - -- Save the pragma for retrieval by other tools - - Add_Contract_Item (N, Pack_Id); - -- Verify the declaration order of pragmas Abstract_State and -- Initializes. Check_Declaration_Order (First => N, Second => Get_Pragma (Pack_Id, Pragma_Initializes)); + + -- Chain the pragma on the contract for completeness + + Add_Contract_Item (N, Pack_Id); end Abstract_State; ------------ @@ -11001,6 +11034,7 @@ package body Sem_Prag is end if; -- Chain the pragma on the contract for further processing + -- by Analyze_External_Property_In_Decl_Part. Add_Contract_Item (N, Obj_Id); end if; @@ -12004,9 +12038,41 @@ package body Sem_Prag is -- CONSEQUENCE ::= boolean_EXPRESSION + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expressions in: + + -- Analyze_Contract_Cases_In_Decl_Part + + -- * Expansion - The annotation is expanded during the expansion of + -- the related subprogram [body] contract as performed in: + + -- Expand_Subprogram_Contract + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: + + -- aspect on subprogram declaration + -- aspect on stand alone subprogram body + -- pragma on stand alone subprogram body + + -- The annotation must prepare its own template when it is: + + -- pragma on subprogram declaration + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. + when Pragma_Contract_Cases => Contract_Cases : declare + Spec_Id : Entity_Id; Subp_Decl : Node_Id; - Subp_Id : Entity_Id; begin GNAT_Pragma; @@ -12054,14 +12120,9 @@ package body Sem_Prag is return; end if; - Subp_Id := Defining_Entity (Subp_Decl); - - Ensure_Aggregate_Form (Get_Argument (N, Subp_Id)); - - -- Construct a generic template for the pragma when the context is - -- a generic subprogram and the pragma is a source construct. + Spec_Id := Corresponding_Spec_Of (Subp_Decl); - Create_Generic_Template (N, Subp_Id); + Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); -- Fully analyze the pragma when it appears inside a subprogram -- body because it cannot benefit from forward references. @@ -12070,9 +12131,10 @@ package body Sem_Prag is Analyze_Contract_Cases_In_Decl_Part (N); end if; - -- Chain the pragma on the contract for further processing + -- Chain the pragma on the contract for further processing by + -- Analyze_Contract_Cases_In_Decl_Part. - Add_Contract_Item (N, Subp_Id); + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); end Contract_Cases; ---------------- @@ -12717,65 +12779,37 @@ package body Sem_Prag is -- where FUNCTION_RESULT is a function Result attribute_reference - when Pragma_Depends => Depends : declare - Subp_Decl : Node_Id; - Subp_Id : Entity_Id; - - begin - GNAT_Pragma; - Check_Arg_Count (1); - - -- Ensure the proper placement of the pragma. Depends must be - -- associated with a subprogram declaration or a body that acts - -- as a spec. - - Subp_Decl := - Find_Related_Subprogram_Or_Body (N, Do_Checks => True); - - -- Body acts as spec - - if Nkind (Subp_Decl) = N_Subprogram_Body - and then No (Corresponding_Spec (Subp_Decl)) - then - null; - - -- Body stub acts as spec - - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub - and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) - then - null; - - -- Subprogram declaration + -- Characteristics: - elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then - null; + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks fully analyze + -- the dependency clauses in: - else - Pragma_Misplaced; - return; - end if; + -- Analyze_Depends_In_Decl_Part - Subp_Id := Defining_Entity (Subp_Decl); + -- * Expansion - None. - Ensure_Aggregate_Form (Get_Argument (N, Subp_Id)); + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: - -- Construct a generic template for the pragma when the context is - -- a generic subprogram and the pragma is a source construct. + -- aspect on subprogram declaration + -- aspect on stand alone subprogram body + -- pragma on stand alone subprogram body - Create_Generic_Template (N, Subp_Id); + -- The annotation must prepare its own template when it is: - -- When the pragma appears on a subprogram body, perform the full - -- analysis now. + -- pragma on subprogram declaration - if Nkind (Subp_Decl) = N_Subprogram_Body then - Analyze_Depends_In_Decl_Part (N); - end if; + -- * Globals - Capture of global references must occur after full + -- analysis. - -- Chain the pragma on the contract for further processing + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. - Add_Contract_Item (N, Subp_Id); - end Depends; + when Pragma_Depends => + Analyze_Depends_Global; --------------------- -- Detect_Blocking -- @@ -13640,13 +13674,38 @@ package body Sem_Prag is -- pragma Extensions_Visible [ (boolean_EXPRESSION) ]; + -- Characteristics: + + -- * Analysis - The annotation is fully analyzed immediately upon + -- elaboration as its expression must be static. + + -- * Expansion - None. + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: + + -- aspect on subprogram declaration + -- aspect on stand alone subprogram body + -- pragma on stand alone subprogram body + + -- The annotation must prepare its own template when it is: + + -- pragma on subprogram declaration + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. + when Pragma_Extensions_Visible => Extensions_Visible : declare Expr : Node_Id; Formal : Entity_Id; Has_OK_Formal : Boolean := False; Spec_Id : Entity_Id; Subp_Decl : Node_Id; - Subp_Id : Entity_Id; begin GNAT_Pragma; @@ -13688,7 +13747,6 @@ package body Sem_Prag is end if; Spec_Id := Corresponding_Spec_Of (Subp_Decl); - Subp_Id := Defining_Entity (Subp_Decl); -- Examine the formals of the related subprogram @@ -13726,15 +13784,10 @@ package body Sem_Prag is return; end if; - -- Construct a generic template for the pragma when the context is - -- a generic subprogram and the pragma is a source construct. - - Create_Generic_Template (N, Subp_Id); - -- Analyze the Boolean expression (if any) if Present (Arg1) then - Expr := Expression (Get_Argument (N)); + Expr := Expression (Get_Argument (N, Spec_Id)); Analyze_And_Resolve (Expr, Standard_Boolean); @@ -13745,9 +13798,9 @@ package body Sem_Prag is end if; end if; - -- Chain the pragma on the contract for further processing + -- Chain the pragma on the contract for completeness - Add_Contract_Item (N, Subp_Id); + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); end Extensions_Visible; -------------- @@ -14147,65 +14200,37 @@ package body Sem_Prag is -- GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM}) -- GLOBAL_ITEM ::= NAME - when Pragma_Global => Global : declare - Subp_Decl : Node_Id; - Subp_Id : Entity_Id; - - begin - GNAT_Pragma; - Check_Arg_Count (1); - - -- Ensure the proper placement of the pragma. Global must be - -- associated with a subprogram declaration or a body that acts - -- as a spec. - - Subp_Decl := - Find_Related_Subprogram_Or_Body (N, Do_Checks => True); - - -- Body acts as spec - - if Nkind (Subp_Decl) = N_Subprogram_Body - and then No (Corresponding_Spec (Subp_Decl)) - then - null; - - -- Body stub acts as spec - - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub - and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) - then - null; - - -- Subprogram declaration + -- Characteristics: - elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then - null; + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks fully analyze + -- the dependency clauses in: - else - Pragma_Misplaced; - return; - end if; + -- Analyze_Global_In_Decl_Part - Subp_Id := Defining_Entity (Subp_Decl); + -- * Expansion - None. - Ensure_Aggregate_Form (Get_Argument (N, Subp_Id)); + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: - -- Construct a generic template for the pragma when the context is - -- a generic subprogram and the pragma is a source construct. + -- aspect on subprogram declaration + -- aspect on stand alone subprogram body + -- pragma on stand alone subprogram body - Create_Generic_Template (N, Subp_Id); + -- The annotation must prepare its own template when it is: - -- When the pragma appears on a subprogram body, perform the full - -- analysis now. + -- pragma on subprogram declaration - if Nkind (Subp_Decl) = N_Subprogram_Body then - Analyze_Global_In_Decl_Part (N); - end if; + -- * Globals - Capture of global references must occur after full + -- analysis. - -- Chain the pragma on the contract for further processing + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. - Add_Contract_Item (N, Subp_Id); - end Global; + when Pragma_Global => + Analyze_Depends_Global; ----------- -- Ident -- @@ -14763,6 +14788,29 @@ package body Sem_Prag is -- pragma Initial_Condition (boolean_EXPRESSION); + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expression in: + + -- Analyze_Initial_Condition_In_Decl_Part + + -- * Expansion - The annotation is expanded during the expansion of + -- the package body whose declaration is subject to the annotation + -- as done in: + + -- Expand_Pragma_Initial_Condition + + -- * Template - The annotation utilizes the generic template of the + -- related package declaration. + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic package is instantiated. + when Pragma_Initial_Condition => Initial_Condition : declare Pack_Decl : Node_Id; Pack_Id : Entity_Id; @@ -14795,7 +14843,6 @@ package body Sem_Prag is -- the contract of the package. Pack_Id := Defining_Entity (Pack_Decl); - Add_Contract_Item (N, Pack_Id); -- Verify the declaration order of pragma Initial_Condition with -- respect to pragmas Abstract_State and Initializes when SPARK @@ -14810,6 +14857,11 @@ package body Sem_Prag is (First => Get_Pragma (Pack_Id, Pragma_Initializes), Second => N); end if; + + -- Chain the pragma on the contract for further processing by + -- Analyze_Initial_Condition_In_Decl_Part. + + Add_Contract_Item (N, Pack_Id); end Initial_Condition; ------------------------ @@ -14856,6 +14908,25 @@ package body Sem_Prag is -- INPUT ::= name + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expression in: + + -- Analyze_Initializes_In_Decl_Part + + -- * Expansion - None. + + -- * Template - The annotation utilizes the generic template of the + -- related package declaration. + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic package is instantiated. + when Pragma_Initializes => Initializes : declare Pack_Decl : Node_Id; Pack_Id : Entity_Id; @@ -14882,15 +14953,9 @@ package body Sem_Prag is return; end if; - Ensure_Aggregate_Form (Get_Argument (N)); - - -- The pragma must be analyzed at the end of the visible - -- declarations of the related package. Save the pragma for later - -- (see Analyze_Initializes_In_Decl_Part) by adding it to the - -- contract of the package. - Pack_Id := Defining_Entity (Pack_Decl); - Add_Contract_Item (N, Pack_Id); + + Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); -- Verify the declaration order of pragmas Abstract_State and -- Initializes when SPARK checks are enabled. @@ -14900,6 +14965,11 @@ package body Sem_Prag is (First => Get_Pragma (Pack_Id, Pragma_Abstract_State), Second => N); end if; + + -- Chain the pragma on the contract for further processing by + -- Analyze_Initializes_In_Decl_Part. + + Add_Contract_Item (N, Pack_Id); end Initializes; ------------ @@ -17308,7 +17378,7 @@ package body Sem_Prag is if not Comes_From_Source (Item_Id) then null; - -- The Part_Of indicator turns an abstract state or + -- The Part_Of indicator turns an abstract state or a -- variable into a constituent of the encapsulating -- state. @@ -17400,8 +17470,8 @@ package body Sem_Prag is Stmt := Prev (Stmt); end loop; - -- When the context is an object declaration, ensure that we are - -- dealing with a variable. + -- When the context is an object declaration, ensure that it is a + -- variable. if Nkind (Stmt) = N_Object_Declaration and then Ekind (Defining_Entity (Stmt)) /= E_Variable @@ -17434,11 +17504,6 @@ package body Sem_Prag is if Legal then State_Id := Entity (State); - -- Add the pragma to the contract of the item. This aids with - -- the detection of a missing but required Part_Of indicator. - - Add_Contract_Item (N, Item_Id); - -- The Part_Of indicator turns a variable into a constituent -- of the encapsulating state. @@ -17455,6 +17520,11 @@ package body Sem_Prag is State_Id => State_Id, Instance => Stmt); end if; + + -- Add the pragma to the contract of the item. This aids with + -- the detection of a missing but required Part_Of indicator. + + Add_Contract_Item (N, Item_Id); end if; end Part_Of; @@ -17687,6 +17757,38 @@ package body Sem_Prag is -- pragma Postcondition ([Check =>] Boolean_EXPRESSION -- [,[Message =>] String_EXPRESSION]); + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expression in: + + -- Analyze_Pre_Post_Condition_In_Decl_Part + + -- * Expansion - The annotation is expanded during the expansion of + -- the related subprogram [body] contract as performed in: + + -- Expand_Subprogram_Contract + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: + + -- aspect on subprogram declaration + -- aspect on stand alone subprogram body + -- pragma on stand alone subprogram body + + -- The annotation must prepare its own template when it is: + + -- pragma on subprogram declaration + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. + when Pragma_Post | Pragma_Post_Class | Pragma_Postcondition => @@ -17701,6 +17803,38 @@ package body Sem_Prag is -- pragma Precondition ([Check =>] Boolean_EXPRESSION -- [,[Message =>] String_EXPRESSION]); + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expression in: + + -- Analyze_Pre_Post_Condition_In_Decl_Part + + -- * Expansion - The annotation is expanded during the expansion of + -- the related subprogram [body] contract as performed in: + + -- Expand_Subprogram_Contract + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: + + -- aspect on subprogram declaration + -- aspect on stand alone subprogram body + -- pragma on stand alone subprogram body + + -- The annotation must prepare its own template when it is: + + -- pragma on subprogram declaration + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. + when Pragma_Pre | Pragma_Pre_Class | Pragma_Precondition => @@ -18541,6 +18675,26 @@ package body Sem_Prag is -- GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM}) -- GLOBAL_ITEM ::= NAME + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks fully analyze + -- the dependency clauses/global list in: + + -- Analyze_Refined_Depends_In_Decl_Part + -- Analyze_Refined_Global_In_Decl_Part + + -- * Expansion - None. + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram body. + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram body is instantiated. + when Pragma_Refined_Depends | Pragma_Refined_Global => Refined_Depends_Global : declare @@ -18549,11 +18703,10 @@ package body Sem_Prag is Spec_Id : Entity_Id; begin - Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal); + Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal); - -- Save the pragma in the contract of the subprogram body. The - -- remaining analysis is performed at the end of the enclosing - -- declarations. + -- Chain the pragma on the contract for further processing by + -- Analyze_Refined_[Depends|Global]_In_Decl_Part. if Legal then Add_Contract_Item (N, Body_Id); @@ -18566,13 +18719,32 @@ package body Sem_Prag is -- pragma Refined_Post (boolean_EXPRESSION); + -- Characteristics: + + -- * Analysis - The annotation is fully analyzed immediately upon + -- elaboration as it cannot forward reference entities. + + -- * Expansion - The annotation is expanded during the expansion of + -- the related subprogram body contract as performed in: + + -- Expand_Subprogram_Contract + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram body. + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram body is instantiated. + when Pragma_Refined_Post => Refined_Post : declare Body_Id : Entity_Id; Legal : Boolean; Spec_Id : Entity_Id; begin - Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal); + Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal); -- Fully analyze the pragma when it appears inside a subprogram -- body because it cannot benefit from forward references. @@ -18585,7 +18757,7 @@ package body Sem_Prag is Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); - -- Chain the pragma on the contract for easy retrieval + -- Chain the pragma on the contract for completeness Add_Contract_Item (N, Body_Id); end if; @@ -18610,6 +18782,25 @@ package body Sem_Prag is -- CONSTITUENT ::= object_NAME | state_NAME + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- refinement clauses in: + + -- Analyze_Refined_State_In_Decl_Part + + -- * Expansion - None. + + -- * Template - The annotation utilizes the template of the related + -- package body. + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic package body is instantiated. + when Pragma_Refined_State => Refined_State : declare Pack_Decl : Node_Id; Spec_Id : Entity_Id; @@ -18651,10 +18842,8 @@ package body Sem_Prag is return; end if; - -- The pragma must be analyzed at the end of the declarations as - -- it has visibility over the whole declarative region. Save the - -- pragma for later (see Analyze_Refined_State_In_Decl_Part) by - -- adding it to the contract of the package body. + -- Chain the pragma on the contract for further processing by + -- Analyze_Refined_State_In_Decl_Part. Add_Contract_Item (N, Defining_Entity (Pack_Decl)); end Refined_State; @@ -20197,6 +20386,33 @@ package body Sem_Prag is -- MODE_TYPE ::= Nominal | Robustness + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expressions in: + + -- Analyze_Test_Case_In_Decl_Part + + -- * Expansion - None. + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram when it is: + + -- aspect on subprogram declaration + + -- The annotation must prepare its own template when it is: + + -- pragma on subprogram declaration + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram is instantiated except for the + -- "pragma on subprogram declaration" case. In that scenario the + -- annotation must instantiate itself. + when Pragma_Test_Case => Test_Case : declare procedure Check_Distinct_Name (Subp_Id : Entity_Id); -- Ensure that the contract of subprogram Subp_Id does not contain @@ -20350,11 +20566,6 @@ package body Sem_Prag is Check_Distinct_Name (Subp_Id); - -- Construct a generic template for the pragma when the context is - -- a generic subprogram and the pragma is a source construct. - - Create_Generic_Template (N, Subp_Id); - -- Fully analyze the pragma when it appears inside a subprogram -- body because it cannot benefit from forward references. @@ -20364,7 +20575,8 @@ package body Sem_Prag is Analyze_Test_Case_In_Decl_Part (N); end if; - -- Chain the pragma on the contract for further processing + -- Chain the pragma on the contract for further processing by + -- Analyze_Test_Case_In_Decl_Part. Add_Contract_Item (N, Subp_Id); end Test_Case; @@ -21598,12 +21810,10 @@ package body Sem_Prag is -- Local variables Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); - Expr : constant Node_Id := - Expression (Get_Argument (N, Defining_Entity (Subp_Decl))); Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); Restore_Scope : Boolean := False; - -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit -- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part @@ -21633,17 +21843,14 @@ package body Sem_Prag is Process_Class_Wide_Condition (Expr, Spec_Id, Subp_Decl); end if; + if Restore_Scope then + End_Scope; + end if; + -- Currently it is not possible to inline pre/postconditions on a -- subprogram subject to pragma Inline_Always. Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); - - -- Remove the subprogram from the scope stack now that the pre-analysis - -- of the precondition/postcondition is done. - - if Restore_Scope then - End_Scope; - end if; end Analyze_Pre_Post_Condition_In_Decl_Part; ------------------------------------------ @@ -21843,7 +22050,9 @@ package body Sem_Prag is if Is_Entity_Name (Ref_Item) then Ref_Item_Id := Entity_Of (Ref_Item); - if Ekind_In (Ref_Item_Id, E_Abstract_State, E_Variable) + if Ekind_In (Ref_Item_Id, E_Abstract_State, + E_Constant, + E_Variable) and then Present (Encapsulating_State (Ref_Item_Id)) and then Encapsulating_State (Ref_Item_Id) = Dep_Item_Id @@ -21899,6 +22108,13 @@ package body Sem_Prag is -- Start of processing for Check_Dependency_Clause begin + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + return; + end if; + -- Examine all refinement clauses and compare them against the -- dependence clause. @@ -22125,10 +22341,16 @@ package body Sem_Prag is -- Start of processing for Check_Output_States begin + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + -- Inspect the outputs of pragma Depends looking for a state with a -- visible refinement. - if Present (Spec_Outputs) then + elsif Present (Spec_Outputs) then Item_Elmt := First_Elmt (Spec_Outputs); while Present (Item_Elmt) loop Item := Node (Item_Elmt); @@ -22336,16 +22558,25 @@ package body Sem_Prag is Clause : Node_Id; begin - if Present (Refinements) then + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + + elsif Present (Refinements) then Clause := First (Refinements); while Present (Clause) loop -- Do not complain about a null input refinement, since a null -- input legitimately matches anything. - if Nkind (Clause) /= N_Component_Association - or else Nkind (Expression (Clause)) /= N_Null + if Nkind (Clause) = N_Component_Association + and then Nkind (Expression (Clause)) = N_Null then + null; + + else SPARK_Msg_N ("unmatched or extra clause in dependence refinement", Clause); @@ -22361,10 +22592,10 @@ package body Sem_Prag is Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); Errors : constant Nat := Serious_Errors_Detected; - Refs : constant Node_Id := Expression (Get_Argument (N)); Clause : Node_Id; Deps : Node_Id; Dummy : Boolean; + Refs : Node_Id; -- Start of processing for Analyze_Refined_Depends_In_Decl_Part @@ -22387,7 +22618,7 @@ package body Sem_Prag is return; end if; - Deps := Expression (Get_Argument (Depends)); + Deps := Expression (Get_Argument (Depends, Spec_Id)); -- A null dependency relation renders the refinement useless because it -- cannot possibly mention abstract states with visible refinement. Note @@ -22454,6 +22685,8 @@ package body Sem_Prag is Dependencies := New_Copy_List_Tree (Component_Associations (Deps)); Normalize_Clauses (Dependencies); + Refs := Expression (Get_Argument (N, Spec_Id)); + if Nkind (Refs) = N_Null then Refinements := No_List; @@ -22518,6 +22751,9 @@ package body Sem_Prag is -- These list contain the entities of all Input, In_Out, Output and -- Proof_In items defined in the corresponding Global pragma. + Spec_Id : Entity_Id; + -- The entity of the subprogram subject to pragma Refined_Global + procedure Check_In_Out_States; -- Determine whether the corresponding Global pragma mentions In_Out -- states with visible refinement and if so, ensure that one of the @@ -22556,13 +22792,16 @@ package body Sem_Prag is -- Verify the legality of a single global list declaration. Global_Mode -- denotes the current mode in effect. - procedure Collect_Global_Items (Prag : Node_Id); - -- Gather all input, in out, output and Proof_In items of pragma Prag - -- in lists In_Items, In_Out_Items, Out_Items and Proof_In_Items. Flags - -- Has_In_State, Has_In_Out_State, Has_Out_State and Has_Proof_In_State - -- are set when there is at least one abstract state with visible - -- refinement available in the corresponding mode. Flag Has_Null_State - -- is set when at least state has a null refinement. + procedure Collect_Global_Items + (List : Node_Id; + Mode : Name_Id := Name_Input); + -- Gather all input, in out, output and Proof_In items from node List + -- and separate them in lists In_Items, In_Out_Items, Out_Items and + -- Proof_In_Items. Flags Has_In_State, Has_In_Out_State, Has_Out_State + -- and Has_Proof_In_State are set when there is at least one abstract + -- state with visible refinement available in the corresponding mode. + -- Flag Has_Null_State is set when at least state has a null refinement. + -- Mode enotes the current global mode in effect. function Present_Then_Remove (List : Elist_Id; @@ -22625,8 +22864,7 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (State_Id); SPARK_Msg_NE ("constituent & of state % must have mode Input, In_Out " - & "or Output in global refinement", - N, Constit_Id); + & "or Output in global refinement", N, Constit_Id); else Has_Missing := True; @@ -22667,10 +22905,16 @@ package body Sem_Prag is -- Start of processing for Check_In_Out_States begin + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + -- Inspect the In_Out items of the corresponding Global pragma -- looking for a state with a visible refinement. - if Has_In_Out_State and then Present (In_Out_Items) then + elsif Has_In_Out_State and then Present (In_Out_Items) then Item_Elmt := First_Elmt (In_Out_Items); while Present (Item_Elmt) loop Item_Id := Node (Item_Elmt); @@ -22751,10 +22995,16 @@ package body Sem_Prag is -- Start of processing for Check_Input_States begin - -- Inspect the Input items of the corresponding Global pragma - -- looking for a state with a visible refinement. + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + + -- Inspect the Input items of the corresponding Global pragma looking + -- for a state with a visible refinement. - if Has_In_State and then Present (In_Items) then + elsif Has_In_State and then Present (In_Items) then Item_Elmt := First_Elmt (In_Items); while Present (Item_Elmt) loop Item_Id := Node (Item_Elmt); @@ -22839,10 +23089,16 @@ package body Sem_Prag is -- Start of processing for Check_Output_States begin + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + -- Inspect the Output items of the corresponding Global pragma -- looking for a state with a visible refinement. - if Has_Out_State and then Present (Out_Items) then + elsif Has_Out_State and then Present (Out_Items) then Item_Elmt := First_Elmt (Out_Items); while Present (Item_Elmt) loop Item_Id := Node (Item_Elmt); @@ -22923,10 +23179,16 @@ package body Sem_Prag is -- Start of processing for Check_Proof_In_States begin + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + -- Inspect the Proof_In items of the corresponding Global pragma -- looking for a state with a visible refinement. - if Has_Proof_In_State and then Present (Proof_In_Items) then + elsif Has_Proof_In_State and then Present (Proof_In_Items) then Item_Elmt := First_Elmt (Proof_In_Items); while Present (Item_Elmt) loop Item_Id := Node (Item_Elmt); @@ -22990,11 +23252,12 @@ package body Sem_Prag is -- Start of processing for Check_Refined_Global_Item begin - -- When the state or variable acts as a constituent of another + -- When the state or object acts as a constituent of another -- state with a visible refinement, collect it for the state -- completeness checks performed later on. - if Present (Encapsulating_State (Item_Id)) + if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable) + and then Present (Encapsulating_State (Item_Id)) and then Has_Visible_Refinement (Encapsulating_State (Item_Id)) then if Global_Mode = Name_Input then @@ -23046,7 +23309,13 @@ package body Sem_Prag is -- Start of processing for Check_Refined_Global_List begin - if Nkind (List) = N_Null then + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + + elsif Nkind (List) = N_Null then null; -- Single global item declaration @@ -23103,135 +23372,121 @@ package body Sem_Prag is -- Collect_Global_Items -- -------------------------- - procedure Collect_Global_Items (Prag : Node_Id) is - procedure Process_Global_List - (List : Node_Id; - Mode : Name_Id := Name_Input); - -- Collect all items housed in a global list. Formal Mode denotes the + procedure Collect_Global_Items + (List : Node_Id; + Mode : Name_Id := Name_Input) + is + procedure Collect_Global_Item + (Item : Node_Id; + Item_Mode : Name_Id); + -- Add a single item to the appropriate list. Item_Mode denotes the -- current mode in effect. ------------------------- - -- Process_Global_List -- + -- Collect_Global_Item -- ------------------------- - procedure Process_Global_List - (List : Node_Id; - Mode : Name_Id := Name_Input) + procedure Collect_Global_Item + (Item : Node_Id; + Item_Mode : Name_Id) is - procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id); - -- Add a single item to the appropriate list. Formal Mode denotes - -- the current mode in effect. - - ------------------------- - -- Process_Global_Item -- - ------------------------- - - procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is - Item_Id : constant Entity_Id := - Available_View (Entity_Of (Item)); - -- The above handles abstract views of variables and states - -- built for limited with clauses. + Item_Id : constant Entity_Id := Available_View (Entity_Of (Item)); + -- The above handles abstract views of variables and states built + -- for limited with clauses. - begin - -- Signal that the global list contains at least one abstract - -- state with a visible refinement. Note that the refinement - -- may be null in which case there are no constituents. - - if Ekind (Item_Id) = E_Abstract_State then - if Has_Null_Refinement (Item_Id) then - Has_Null_State := True; + begin + -- Signal that the global list contains at least one abstract + -- state with a visible refinement. Note that the refinement may + -- be null in which case there are no constituents. - elsif Has_Non_Null_Refinement (Item_Id) then - if Mode = Name_Input then - Has_In_State := True; - elsif Mode = Name_In_Out then - Has_In_Out_State := True; - elsif Mode = Name_Output then - Has_Out_State := True; - elsif Mode = Name_Proof_In then - Has_Proof_In_State := True; - end if; + if Ekind (Item_Id) = E_Abstract_State then + if Has_Null_Refinement (Item_Id) then + Has_Null_State := True; + + elsif Has_Non_Null_Refinement (Item_Id) then + if Item_Mode = Name_Input then + Has_In_State := True; + elsif Item_Mode = Name_In_Out then + Has_In_Out_State := True; + elsif Item_Mode = Name_Output then + Has_Out_State := True; + elsif Item_Mode = Name_Proof_In then + Has_Proof_In_State := True; end if; end if; + end if; - -- Add the item to the proper list - - if Mode = Name_Input then - Add_Item (Item_Id, In_Items); - elsif Mode = Name_In_Out then - Add_Item (Item_Id, In_Out_Items); - elsif Mode = Name_Output then - Add_Item (Item_Id, Out_Items); - elsif Mode = Name_Proof_In then - Add_Item (Item_Id, Proof_In_Items); - end if; - end Process_Global_Item; - - -- Local variables + -- Add the item to the proper list - Item : Node_Id; + if Item_Mode = Name_Input then + Add_Item (Item_Id, In_Items); + elsif Item_Mode = Name_In_Out then + Add_Item (Item_Id, In_Out_Items); + elsif Item_Mode = Name_Output then + Add_Item (Item_Id, Out_Items); + elsif Item_Mode = Name_Proof_In then + Add_Item (Item_Id, Proof_In_Items); + end if; + end Collect_Global_Item; - -- Start of processing for Process_Global_List + -- Local variables - begin - if Nkind (List) = N_Null then - null; + Item : Node_Id; - -- Single global item declaration + -- Start of processing for Collect_Global_Items - elsif Nkind_In (List, N_Expanded_Name, - N_Identifier, - N_Selected_Component) - then - Process_Global_Item (List, Mode); + begin + if Nkind (List) = N_Null then + null; - -- Single global list or moded global list declaration + -- Single global item declaration - elsif Nkind (List) = N_Aggregate then + elsif Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) + then + Collect_Global_Item (List, Mode); - -- The declaration of a simple global list appear as a - -- collection of expressions. + -- Single global list or moded global list declaration - if Present (Expressions (List)) then - Item := First (Expressions (List)); - while Present (Item) loop - Process_Global_Item (Item, Mode); - Next (Item); - end loop; + elsif Nkind (List) = N_Aggregate then - -- The declaration of a moded global list appears as a - -- collection of component associations where individual - -- choices denote mode. + -- The declaration of a simple global list appear as a collection + -- of expressions. - elsif Present (Component_Associations (List)) then - Item := First (Component_Associations (List)); - while Present (Item) loop - Process_Global_List - (List => Expression (Item), - Mode => Chars (First (Choices (Item)))); + if Present (Expressions (List)) then + Item := First (Expressions (List)); + while Present (Item) loop + Collect_Global_Item (Item, Mode); + Next (Item); + end loop; - Next (Item); - end loop; + -- The declaration of a moded global list appears as a collection + -- of component associations where individual choices denote mode. - -- Invalid tree + elsif Present (Component_Associations (List)) then + Item := First (Component_Associations (List)); + while Present (Item) loop + Collect_Global_Items + (List => Expression (Item), + Mode => Chars (First (Choices (Item)))); - else - raise Program_Error; - end if; + Next (Item); + end loop; - -- To accomodate partial decoration of disabled SPARK features, - -- this routine may be called with illegal input. If this is the - -- case, do not raise Program_Error. + -- Invalid tree else - null; + raise Program_Error; end if; - end Process_Global_List; - -- Start of processing for Collect_Global_Items + -- To accomodate partial decoration of disabled SPARK features, this + -- routine may be called with illegal input. If this is the case, do + -- not raise Program_Error. - begin - Process_Global_List (Expression (Get_Argument (Prag))); + else + null; + end if; end Collect_Global_Items; ------------------------- @@ -23288,18 +23543,25 @@ package body Sem_Prag is -- Start of processing for Report_Extra_Constituents begin - Report_Extra_Constituents_In_List (In_Constits); - Report_Extra_Constituents_In_List (In_Out_Constits); - Report_Extra_Constituents_In_List (Out_Constits); - Report_Extra_Constituents_In_List (Proof_In_Constits); + -- Do not perform this check in an instance because it was already + -- performed successfully in the generic template. + + if Is_Generic_Instance (Spec_Id) then + null; + + else + Report_Extra_Constituents_In_List (In_Constits); + Report_Extra_Constituents_In_List (In_Out_Constits); + Report_Extra_Constituents_In_List (Out_Constits); + Report_Extra_Constituents_In_List (Proof_In_Constits); + end if; end Report_Extra_Constituents; -- Local variables Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Errors : constant Nat := Serious_Errors_Detected; - Items : constant Node_Id := Expression (Get_Argument (N)); - Spec_Id : Entity_Id; + Items : Node_Id; -- Start of processing for Analyze_Refined_Global_In_Decl_Part @@ -23311,6 +23573,7 @@ package body Sem_Prag is end if; Global := Get_Pragma (Spec_Id, Pragma_Global); + Items := Expression (Get_Argument (N, Spec_Id)); -- The subprogram declaration lacks pragma Global. This renders -- Refined_Global useless as there is nothing to refine. @@ -23324,40 +23587,53 @@ package body Sem_Prag is -- Extract all relevant items from the corresponding Global pragma - Collect_Global_Items (Global); + Collect_Global_Items (Expression (Get_Argument (Global, Spec_Id))); - -- Corresponding Global pragma must mention at least one state witha - -- visible refinement at the point Refined_Global is processed. States - -- with null refinements need Refined_Global pragma (SPARK RM 7.2.4(2)). + -- Package and subprogram bodies are instantiated individually in + -- a separate compiler pass. Due to this mode of instantiation, the + -- refinement of a state may no longer be visible when a subprogram + -- body contract is instantiated. Since the generic template is legal, + -- do not perform this check in the instance to circumvent this oddity. - if not Has_In_State - and then not Has_In_Out_State - and then not Has_Out_State - and then not Has_Proof_In_State - and then not Has_Null_State - then - SPARK_Msg_NE - ("useless refinement, subprogram & does not depend on abstract " - & "state with visible refinement", N, Spec_Id); - return; - end if; + if Is_Generic_Instance (Spec_Id) then + null; - -- The global refinement of inputs and outputs cannot be null when the - -- corresponding Global pragma contains at least one item except in the - -- case where we have states with null refinements. + -- Non-instance case - if Nkind (Items) = N_Null - and then - (Present (In_Items) - or else Present (In_Out_Items) - or else Present (Out_Items) - or else Present (Proof_In_Items)) - and then not Has_Null_State - then - SPARK_Msg_NE - ("refinement cannot be null, subprogram & has global items", - N, Spec_Id); - return; + else + -- The corresponding Global pragma must mention at least one state + -- witha visible refinement at the point Refined_Global is processed. + -- States with null refinements need Refined_Global pragma + -- (SPARK RM 7.2.4(2)). + + if not Has_In_State + and then not Has_In_Out_State + and then not Has_Out_State + and then not Has_Proof_In_State + and then not Has_Null_State + then + SPARK_Msg_NE + ("useless refinement, subprogram & does not depend on abstract " + & "state with visible refinement", N, Spec_Id); + return; + + -- The global refinement of inputs and outputs cannot be null when + -- the corresponding Global pragma contains at least one item except + -- in the case where we have states with null refinements. + + elsif Nkind (Items) = N_Null + and then + (Present (In_Items) + or else Present (In_Out_Items) + or else Present (Out_Items) + or else Present (Proof_In_Items)) + and then not Has_Null_State + then + SPARK_Msg_NE + ("refinement cannot be null, subprogram & has global items", + N, Spec_Id); + return; + end if; end if; -- Analyze Refined_Global as if it behaved as a regular pragma Global. @@ -23414,14 +23690,15 @@ package body Sem_Prag is ---------------------------------------- procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id) is + Body_Decl : constant Node_Id := Find_Related_Package_Or_Body (N); + Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); + Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); + Available_States : Elist_Id := No_Elist; -- A list of all abstract states defined in the package declaration that -- are available for refinement. The list is used to report unrefined -- states. - Body_Id : Entity_Id; - -- The body entity of the package subject to pragma Refined_State - Body_States : Elist_Id := No_Elist; -- A list of all hidden states that appear in the body of the related -- package. The list is used to report unused hidden states. @@ -23434,9 +23711,6 @@ package body Sem_Prag is -- A list that contains all refined states processed so far. The list is -- used to detect duplicate refinements. - Spec_Id : Entity_Id; - -- The spec entity of the package subject to pragma Refined_State - procedure Analyze_Refinement_Clause (Clause : Node_Id); -- Perform full analysis of a single refinement clause @@ -23745,7 +24019,7 @@ package body Sem_Prag is Resolve_State (Constit); -- Ensure that the constituent denotes a valid state or a - -- whole variable. + -- whole object (SPARK RM 7.2.2(5)). if Is_Entity_Name (Constit) then Constit_Id := Entity_Of (Constit); @@ -23755,8 +24029,8 @@ package body Sem_Prag is else SPARK_Msg_NE - ("constituent & must denote a variable or state (SPARK " - & "RM 7.2.2(5))", Constit, Constit_Id); + ("constituent & must denote object or state", + Constit, Constit_Id); end if; -- The constituent is illegal @@ -23866,6 +24140,7 @@ package body Sem_Prag is -- state ... has unused Part_Of constituents -- abstract state ... defined at ... + -- constant ... defined at ... -- variable ... defined at ... if not Posted then @@ -23881,8 +24156,7 @@ package body Sem_Prag is SPARK_Msg_NE ("\abstract state & defined #", State, Constit_Id); else - SPARK_Msg_NE - ("\variable & defined #", State, Constit_Id); + SPARK_Msg_NE ("\variable & defined #", State, Constit_Id); end if; Next_Elmt (Constit_Elmt); @@ -23989,7 +24263,6 @@ package body Sem_Prag is Constit := First (Expressions (Constit)); while Present (Constit) loop Analyze_Constituent (Constit); - Next (Constit); end loop; end if; @@ -24069,8 +24342,8 @@ package body Sem_Prag is -- A list containing all body states of Pack_Id procedure Collect_Visible_States (Pack_Id : Entity_Id); - -- Gather the entities of all abstract states and variables declared - -- in the visible state space of package Pack_Id. + -- Gather the entities of all abstract states and objects declared in + -- the visible state space of package Pack_Id. ---------------------------- -- Collect_Visible_States -- @@ -24115,7 +24388,7 @@ package body Sem_Prag is -- Start of processing for Collect_Body_States begin - -- Inspect the declarations of the body looking for source variables, + -- Inspect the declarations of the body looking for source objects, -- packages and package instantiations. Decl := First (Declarations (Pack_Body)); @@ -24123,8 +24396,8 @@ package body Sem_Prag is if Nkind (Decl) = N_Object_Declaration then Item_Id := Defining_Entity (Decl); - -- Capture source variables only as internally generated - -- temporaries cannot be named and participate in refinement. + -- Capture source variables as internally generated temporaries + -- cannot be named and participate in refinement. if Ekind (Item_Id) = E_Variable and then Comes_From_Source (Item_Id) @@ -24135,7 +24408,7 @@ package body Sem_Prag is elsif Nkind (Decl) = N_Package_Declaration then Item_Id := Defining_Entity (Decl); - -- Capture the visible abstract states and variables of a + -- Capture the visible abstract states and objects of a -- source package [instantiation]. if Comes_From_Source (Item_Id) then @@ -24187,6 +24460,7 @@ package body Sem_Prag is -- body of package ... has unused hidden states -- abstract state ... defined at ... + -- constant ... defined at ... -- variable ... defined at ... if not Posted then @@ -24201,8 +24475,7 @@ package body Sem_Prag is SPARK_Msg_NE ("\abstract state & defined #", Body_Id, State_Id); else - SPARK_Msg_NE - ("\variable & defined #", Body_Id, State_Id); + SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id); end if; Next_Elmt (State_Elmt); @@ -24212,18 +24485,14 @@ package body Sem_Prag is -- Local declarations - Body_Decl : constant Node_Id := Parent (N); - Clauses : constant Node_Id := Expression (Get_Argument (N)); - Clause : Node_Id; + Clauses : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); + Clause : Node_Id; -- Start of processing for Analyze_Refined_State_In_Decl_Part begin Set_Analyzed (N); - Body_Id := Defining_Entity (Body_Decl); - Spec_Id := Corresponding_Spec (Body_Decl); - -- Replicate the abstract states declared by the package because the -- matching algorithm will consume states. @@ -24274,21 +24543,18 @@ package body Sem_Prag is ------------------------------------ procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is - procedure Preanalyze_Test_Case_Arg - (Arg_Nam : Name_Id; - Spec_Id : Entity_Id); + Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + + procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id); -- Preanalyze one of the optional arguments "Requires" or "Ensures" - -- denoted by Arg_Nam. Spec_Id is the entity of the subprogram spec - -- subject to pragma Test_Case. + -- denoted by Arg_Nam. ------------------------------ -- Preanalyze_Test_Case_Arg -- ------------------------------ - procedure Preanalyze_Test_Case_Arg - (Arg_Nam : Name_Id; - Spec_Id : Entity_Id) - is + procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id) is Arg : Node_Id; begin @@ -24317,18 +24583,11 @@ package body Sem_Prag is -- Local variables - Spec_Id : Entity_Id; - Subp_Decl : Node_Id; - Restore_Scope : Boolean := False; - -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit -- Start of processing for Analyze_Test_Case_In_Decl_Part begin - Subp_Decl := Find_Related_Subprogram_Or_Body (N); - Spec_Id := Corresponding_Spec_Of (Subp_Decl); - -- Ensure that the formal parameters are visible when analyzing all -- clauses. This falls out of the general rule of aspects pertaining -- to subprogram declarations. @@ -24344,17 +24603,17 @@ package body Sem_Prag is end if; end if; - Preanalyze_Test_Case_Arg (Name_Requires, Spec_Id); - Preanalyze_Test_Case_Arg (Name_Ensures, Spec_Id); + Preanalyze_Test_Case_Arg (Name_Requires); + Preanalyze_Test_Case_Arg (Name_Ensures); + + if Restore_Scope then + End_Scope; + end if; -- Currently it is not possible to inline pre/postconditions on a -- subprogram subject to pragma Inline_Always. Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); - - if Restore_Scope then - End_Scope; - end if; end Analyze_Test_Case_In_Decl_Part; ---------------- @@ -24740,22 +24999,22 @@ package body Sem_Prag is procedure Check_Postcondition_Use_In_Inlined_Subprogram (Prag : Node_Id; - Subp_Id : Entity_Id) + Spec_Id : Entity_Id) is begin if Warn_On_Redundant_Constructs - and then Has_Pragma_Inline_Always (Subp_Id) + and then Has_Pragma_Inline_Always (Spec_Id) then Error_Msg_Name_1 := Original_Aspect_Pragma_Name (Prag); if From_Aspect_Specification (Prag) then Error_Msg_NE ("aspect % not enforced on inlined subprogram &?r?", - Corresponding_Aspect (Prag), Subp_Id); + Corresponding_Aspect (Prag), Spec_Id); else Error_Msg_NE ("pragma % not enforced on inlined subprogram &?r?", - Prag, Subp_Id); + Prag, Spec_Id); end if; end if; end Check_Postcondition_Use_In_Inlined_Subprogram; @@ -24921,9 +25180,12 @@ package body Sem_Prag is elsif Nkind (Clause) = N_Component_Association then Collect_Dependency_Item - (Expression (Clause), Is_Input => True); + (Item => Expression (Clause), + Is_Input => True); + Collect_Dependency_Item - (First (Choices (Clause)), Is_Input => False); + (Item => First (Choices (Clause)), + Is_Input => False); -- To accomodate partial decoration of disabled SPARK features, this -- routine may be called with illegal input. If this is the case, do @@ -25024,15 +25286,21 @@ package body Sem_Prag is begin Global_Seen := False; - -- Process all formal parameters + -- Process all [generic] formal parameters - Formal := First_Formal (Spec_Id); + Formal := First_Entity (Spec_Id); while Present (Formal) loop - if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then + if Ekind_In (Formal, E_Generic_In_Parameter, + E_In_Out_Parameter, + E_In_Parameter) + then Add_Item (Formal, Subp_Inputs); end if; - if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then + if Ekind_In (Formal, E_Generic_In_Out_Parameter, + E_In_Out_Parameter, + E_Out_Parameter) + then Add_Item (Formal, Subp_Outputs); -- Out parameters can act as inputs when the related type is @@ -25046,7 +25314,7 @@ package body Sem_Prag is end if; end if; - Next_Formal (Formal); + Next_Entity (Formal); end loop; -- When processing a subprogram body, look for pragmas Refined_Depends @@ -25056,7 +25324,8 @@ package body Sem_Prag is Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends); Global := Get_Pragma (Subp_Id, Pragma_Refined_Global); - -- Subprogram declaration case, look for pragmas Depends and Global + -- Subprogram declaration or stand alone body case, look for pragmas + -- Depends and Global else Depends := Get_Pragma (Spec_Id, Pragma_Depends); @@ -25392,21 +25661,20 @@ package body Sem_Prag is ------------------ function Get_Argument - (Prag : Node_Id; - Spec_Id : Entity_Id := Empty) return Node_Id + (Prag : Node_Id; + Context_Id : Entity_Id := Empty) return Node_Id is Args : constant List_Id := Pragma_Argument_Associations (Prag); begin - -- Use the expression of the original aspect if possible when compiling - -- for ASIS or when analyzing the template of a generic subprogram. In - -- both cases the aspect's tree must be decorated to allow for ASIS - -- queries or to save all global references in the generic context. + -- Use the expression of the original aspect when compiling for ASIS or + -- when analyzing the template of a generic unit. In both cases the + -- aspect's tree must be decorated to allow for ASIS queries or to save + -- the global references in the generic context. if From_Aspect_Specification (Prag) - and then - (ASIS_Mode or else (Present (Spec_Id) - and then Is_Generic_Subprogram (Spec_Id))) + and then (ASIS_Mode or else (Present (Context_Id) + and then Is_Generic_Unit (Context_Id))) then return Corresponding_Aspect (Prag); diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index cf80d52455d..cb3f82e647d 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -172,9 +172,10 @@ package Sem_Prag is -- inputs and outputs of subprogram Subp_Id in lists Subp_Inputs (inputs) -- and Subp_Outputs (outputs). The inputs and outputs are gathered from: -- 1) The formal parameters of the subprogram - -- 2) The items of pragma [Refined_]Global + -- 2) The generic formal parameters of the generic subprogram + -- 3) The items of pragma [Refined_]Global -- or - -- 3) The items of pragma [Refined_]Depends if there is no pragma + -- 4) The items of pragma [Refined_]Depends if there is no pragma -- [Refined_]Global present and flag Synthesize is set to True. -- If the subprogram has no inputs and/or outputs, then the returned list -- is No_Elist. Flag Global_Seen is set when the related subprogram has @@ -190,6 +191,16 @@ package Sem_Prag is -- True have their analysis delayed until after the main program is parsed -- and analyzed. + function Find_Related_Package_Or_Body + (Prag : Node_Id; + Do_Checks : Boolean := False) return Node_Id; + -- Subsidiary to the analysis of pragmas Abstract_State, Initial_Condition, + -- Initializes and Refined_State. Find the declaration of the related + -- package [body] subject to pragma Prag. The return value is either + -- N_Package_Declaration, N_Package_Body or Empty if the placement of + -- the pragma is illegal. If flag Do_Checks is set, the routine reports + -- duplicate pragmas. + function Find_Related_Subprogram_Or_Body (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; @@ -207,6 +218,20 @@ package Sem_Prag is -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if -- illegal. + function Get_Argument + (Prag : Node_Id; + Context_Id : Node_Id := Empty) return Node_Id; + -- Obtain the argument of pragma Prag depending on context and the nature + -- of the pragma. The argument is extracted in the following manner: + -- + -- When the pragma is generated from an aspect, return the corresponding + -- aspect for ASIS or when Context_Id denotes a generic unit. + -- + -- Otherwise return the first argument of Prag + -- + -- Context denotes the entity of the function, package or procedure where + -- Prag resides. + function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type; -- Given a pragma SPARK_Mode node, return corresponding mode id diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index b35a28c2be6..01dc53163d9 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -49,6 +49,7 @@ with Sem_Aux; use Sem_Aux; with Sem_Attr; use Sem_Attr; with Sem_Ch6; use Sem_Ch6; with Sem_Ch8; use Sem_Ch8; +with Sem_Ch12; use Sem_Ch12; with Sem_Ch13; use Sem_Ch13; with Sem_Disp; use Sem_Disp; with Sem_Eval; use Sem_Eval; @@ -4523,23 +4524,164 @@ package body Sem_Util is -- Corresponding_Spec_Of -- --------------------------- - function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id is + function Corresponding_Spec_Of (Decl : Node_Id) return Entity_Id is begin - if Nkind (Subp_Decl) = N_Subprogram_Body - and then Present (Corresponding_Spec (Subp_Decl)) + if Nkind_In (Decl, N_Package_Body, N_Subprogram_Body) + and then Present (Corresponding_Spec (Decl)) then - return Corresponding_Spec (Subp_Decl); + return Corresponding_Spec (Decl); - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub - and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) + elsif Nkind_In (Decl, N_Package_Body_Stub, N_Subprogram_Body_Stub) + and then Present (Corresponding_Spec_Of_Stub (Decl)) then - return Corresponding_Spec_Of_Stub (Subp_Decl); + return Corresponding_Spec_Of_Stub (Decl); else - return Defining_Entity (Subp_Decl); + return Defining_Entity (Decl); end if; end Corresponding_Spec_Of; + ----------------------------- + -- Create_Generic_Contract -- + ----------------------------- + + procedure Create_Generic_Contract (Unit : Node_Id) is + Templ : constant Node_Id := Original_Node (Unit); + Templ_Id : constant Entity_Id := Defining_Entity (Templ); + + procedure Add_Generic_Contract_Pragma (Prag : Node_Id); + -- Add a single contract-related source pragma Prag to the contract of + -- generic template Templ_Id. + + --------------------------------- + -- Add_Generic_Contract_Pragma -- + --------------------------------- + + procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is + Prag_Templ : Node_Id; + + begin + -- Mark the pragma to prevent the premature capture of global + -- references when capturing global references of the context + -- (see Save_References_In_Pragma). + + Set_Is_Generic_Contract_Pragma (Prag); + + -- Pragmas that apply to a generic subprogram declaration are not + -- part of the semantic structure of the generic template: + + -- generic + -- procedure Example (Formal : Integer); + -- pragma Precondition (Formal > 0); + + -- Create a generic template for such pragmas and link the template + -- of the pragma with the generic template. + + if Nkind (Templ) = N_Generic_Subprogram_Declaration then + Rewrite + (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); + Prag_Templ := Original_Node (Prag); + + Set_Is_Generic_Contract_Pragma (Prag_Templ); + Add_Contract_Item (Prag_Templ, Templ_Id); + + -- Otherwise link the pragma with the generic template + + else + Add_Contract_Item (Prag, Templ_Id); + end if; + end Add_Generic_Contract_Pragma; + + -- Local variables + + Context : constant Node_Id := Parent (Unit); + Decl : Node_Id := Empty; + + -- Start of processing for Create_Generic_Contract + + begin + -- A generic package declaration carries contract-related source pragmas + -- in its visible declarations. + + if Nkind (Templ) = N_Generic_Package_Declaration then + Set_Ekind (Templ_Id, E_Generic_Package); + + if Present (Visible_Declarations (Specification (Templ))) then + Decl := First (Visible_Declarations (Specification (Templ))); + end if; + + -- A generic package body carries contract-related source pragmas in its + -- declarations. + + elsif Nkind (Templ) = N_Package_Body then + Set_Ekind (Templ_Id, E_Package_Body); + + if Present (Declarations (Templ)) then + Decl := First (Declarations (Templ)); + end if; + + -- Generic subprogram declaration + + elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then + if Nkind (Specification (Templ)) = N_Function_Specification then + Set_Ekind (Templ_Id, E_Generic_Function); + else + Set_Ekind (Templ_Id, E_Generic_Procedure); + end if; + + -- When the generic subprogram acts as a compilation unit, inspect + -- the Pragmas_After list for contract-related source pragmas. + + if Nkind (Context) = N_Compilation_Unit then + if Present (Aux_Decls_Node (Context)) + and then Present (Pragmas_After (Aux_Decls_Node (Context))) + then + Decl := First (Pragmas_After (Aux_Decls_Node (Context))); + end if; + + -- Otherwise inspect the successive declarations for contract-related + -- source pragmas. + + else + Decl := Next (Unit); + end if; + + -- A generic subprogram body carries contract-related source pragmas in + -- its declarations. + + elsif Nkind (Templ) = N_Subprogram_Body then + Set_Ekind (Templ_Id, E_Subprogram_Body); + + if Present (Declarations (Templ)) then + Decl := First (Declarations (Templ)); + end if; + end if; + + -- Inspect the relevant declarations looking for contract-related source + -- pragmas and add them to the contract of the generic unit. + + while Present (Decl) loop + if Comes_From_Source (Decl) then + if Nkind (Decl) = N_Pragma then + + -- The source pragma is a contract annotation + + if Is_Contract_Annotation (Decl) then + Add_Generic_Contract_Pragma (Decl); + end if; + + -- The region where a contract-related source pragma may appear + -- ends with the first source non-pragma declaration or statement. + + else + exit; + end if; + end if; + + Next (Decl); + end loop; + end Create_Generic_Contract; + -------------------- -- Current_Entity -- -------------------- @@ -10541,33 +10683,10 @@ package body Sem_Util is ---------------------------- function Is_Contract_Annotation (Item : Node_Id) return Boolean is - Nam : Name_Id; - begin - if Nkind (Item) = N_Aspect_Specification then - Nam := Chars (Identifier (Item)); - - else pragma Assert (Nkind (Item) = N_Pragma); - Nam := Pragma_Name (Item); - end if; - - return Nam = Name_Abstract_State - or else Nam = Name_Contract_Cases - or else Nam = Name_Depends - or else Nam = Name_Extensions_Visible - or else Nam = Name_Global - or else Nam = Name_Initial_Condition - or else Nam = Name_Initializes - or else Nam = Name_Post - or else Nam = Name_Post_Class - or else Nam = Name_Postcondition - or else Nam = Name_Pre - or else Nam = Name_Pre_Class - or else Nam = Name_Precondition - or else Nam = Name_Refined_Depends - or else Nam = Name_Refined_Global - or else Nam = Name_Refined_State - or else Nam = Name_Test_Case; + return Is_Package_Contract_Annotation (Item) + or else + Is_Subprogram_Contract_Annotation (Item); end Is_Contract_Annotation; -------------------------------------- @@ -11426,6 +11545,45 @@ package body Sem_Util is end if; end Is_Fully_Initialized_Variant; + ------------------------------------ + -- Is_Generic_Declaration_Or_Body -- + ------------------------------------ + + function Is_Generic_Declaration_Or_Body (Decl : Node_Id) return Boolean is + Spec_Decl : Node_Id; + + begin + -- Package/subprogram body + + if Nkind_In (Decl, N_Package_Body, N_Subprogram_Body) + and then Present (Corresponding_Spec (Decl)) + then + Spec_Decl := Unit_Declaration_Node (Corresponding_Spec (Decl)); + + -- Package/subprogram body stub + + elsif Nkind_In (Decl, N_Package_Body_Stub, N_Subprogram_Body_Stub) + and then Present (Corresponding_Spec_Of_Stub (Decl)) + then + Spec_Decl := + Unit_Declaration_Node (Corresponding_Spec_Of_Stub (Decl)); + + -- All other cases + + else + Spec_Decl := Decl; + end if; + + -- Rather than inspecting the defining entity of the spec declaration, + -- look at its Nkind. This takes care of the case where the analysis of + -- a generic body modifies the Ekind of its spec to allow for recursive + -- calls. + + return + Nkind_In (Spec_Decl, N_Generic_Package_Declaration, + N_Generic_Subprogram_Declaration); + end Is_Generic_Declaration_Or_Body; + ---------------------------- -- Is_Inherited_Operation -- ---------------------------- @@ -11827,6 +11985,27 @@ package body Sem_Util is end if; end Is_OK_Variable_For_Out_Formal; + ------------------------------------ + -- Is_Package_Contract_Annotation -- + ------------------------------------ + + function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean is + Nam : Name_Id; + + begin + if Nkind (Item) = N_Aspect_Specification then + Nam := Chars (Identifier (Item)); + + else pragma Assert (Nkind (Item) = N_Pragma); + Nam := Pragma_Name (Item); + end if; + + return Nam = Name_Abstract_State + or else Nam = Name_Initial_Condition + or else Nam = Name_Initializes + or else Nam = Name_Refined_State; + end Is_Package_Contract_Annotation; + ----------------------------------- -- Is_Partially_Initialized_Type -- ----------------------------------- @@ -12530,6 +12709,39 @@ package body Sem_Util is or else Nkind (N) = N_Procedure_Call_Statement; end Is_Statement; + --------------------------------------- + -- Is_Subprogram_Contract_Annotation -- + --------------------------------------- + + function Is_Subprogram_Contract_Annotation + (Item : Node_Id) return Boolean + is + Nam : Name_Id; + + begin + if Nkind (Item) = N_Aspect_Specification then + Nam := Chars (Identifier (Item)); + + else pragma Assert (Nkind (Item) = N_Pragma); + Nam := Pragma_Name (Item); + end if; + + return Nam = Name_Contract_Cases + or else Nam = Name_Depends + or else Nam = Name_Extensions_Visible + or else Nam = Name_Global + or else Nam = Name_Post + or else Nam = Name_Post_Class + or else Nam = Name_Postcondition + or else Nam = Name_Pre + or else Nam = Name_Pre_Class + or else Nam = Name_Precondition + or else Nam = Name_Refined_Depends + or else Nam = Name_Refined_Global + or else Nam = Name_Refined_Post + or else Nam = Name_Test_Case; + end Is_Subprogram_Contract_Annotation; + -------------------------------------------------- -- Is_Subprogram_Stub_Without_Prior_Declaration -- -------------------------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 044047bc862..84d04903c72 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -53,7 +53,7 @@ package Sem_Util is -- Add pragma Prag to the contract of an entry, a package [body], a -- subprogram [body] or variable denoted by Id. The following are valid -- pragmas: - -- Abstract_States + -- Abstract_State -- Async_Readers -- Async_Writers -- Contract_Cases @@ -421,10 +421,14 @@ package Sem_Util is -- attribute, except in the case of formal private and derived types. -- Possible optimization??? - function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id; - -- Return the corresponding spec of Subp_Decl when it denotes a body [stub] - -- or the defining entity of subprogram declaration Subp_Decl in all other - -- cases. + function Corresponding_Spec_Of (Decl : Node_Id) return Entity_Id; + -- Return the corresponding spec of Decl when it denotes a package or a + -- subprogram [stub], or the defining entity of Decl. + + procedure Create_Generic_Contract (Unit : Node_Id); + -- Create a contract node for a generic package, generic subprogram or a + -- generic body denoted by Unit by collecting all source contract-related + -- pragmas in the contract of the unit. function Current_Entity (N : Node_Id) return Entity_Id; pragma Inline (Current_Entity); @@ -1283,6 +1287,10 @@ package Sem_Util is -- means that the result returned is not crucial, but should err on the -- side of thinking things are fully initialized if it does not know. + function Is_Generic_Declaration_Or_Body (Decl : Node_Id) return Boolean; + -- Determine whether arbitrary declaration Decl denotes a generic package, + -- a generic subprogram or a generic body. + function Is_Inherited_Operation (E : Entity_Id) return Boolean; -- E is a subprogram. Return True is E is an implicit operation inherited -- by a derived type declaration. @@ -1333,6 +1341,14 @@ package Sem_Util is -- the Is_Variable sense) with an untagged type target are considered view -- conversions and hence variables. + function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean; + -- Determine whether aspect specification or pragma Item is one of the + -- following package contract annotations: + -- Abstract_State + -- Initial_Condition + -- Initializes + -- Refined_State + function Is_Partially_Initialized_Type (Typ : Entity_Id; Include_Implicit : Boolean := True) return Boolean; @@ -1411,6 +1427,24 @@ package Sem_Util is -- the N_Statement_Other_Than_Procedure_Call subtype from Sinfo). -- Note that a label is *not* a statement, and will return False. + function Is_Subprogram_Contract_Annotation (Item : Node_Id) return Boolean; + -- Determine whether aspect specification or pragma Item is one of the + -- following subprogram contract annotations: + -- Contract_Cases + -- Depends + -- Extensions_Visible + -- Global + -- Post + -- Post_Class + -- Postcondition + -- Pre + -- Pre_Class + -- Precondition + -- Refined_Depends + -- Refined_Global + -- Refined_Post + -- Test_Case + function Is_Subprogram_Stub_Without_Prior_Declaration (N : Node_Id) return Boolean; -- Return True if N is a subprogram stub with no prior subprogram diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index e9f6dd7ab9d..136195ee33a 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -1872,6 +1872,14 @@ package body Sinfo is return Flag4 (N); end Is_Folded_In_Parser; + function Is_Generic_Contract_Pragma + (N : Node_Id) return Boolean is + begin + pragma Assert (False + or else NT (N).Nkind = N_Pragma); + return Flag2 (N); + end Is_Generic_Contract_Pragma; + function Is_Ignored (N : Node_Id) return Boolean is begin @@ -5069,6 +5077,14 @@ package body Sinfo is Set_Flag4 (N, Val); end Set_Is_Folded_In_Parser; + procedure Set_Is_Generic_Contract_Pragma + (N : Node_Id; Val : Boolean := True) is + begin + pragma Assert (False + or else NT (N).Nkind = N_Pragma); + Set_Flag2 (N, Val); + end Set_Is_Generic_Contract_Pragma; + procedure Set_Is_Ignored (N : Node_Id; Val : Boolean := True) is begin diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index c2a8bf6fbc3..5ced3564aa8 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1560,17 +1560,17 @@ package Sinfo is -- operand is of the component type of the result. Used in resolving -- concatenation nodes in instances. + -- Is_Controlling_Actual (Flag16-Sem) + -- This flag is set on in an expression that is a controlling argument in + -- a dispatching call. It is off in all other cases. See Sem_Disp for + -- details of its use. + -- Is_Delayed_Aspect (Flag14-Sem) -- Present in N_Pragma and N_Attribute_Definition_Clause nodes which -- come from aspect specifications, where the evaluation of the aspect -- must be delayed to the freeze point. This flag is also set True in -- the corresponding N_Aspect_Specification node. - -- Is_Controlling_Actual (Flag16-Sem) - -- This flag is set on in an expression that is a controlling argument in - -- a dispatching call. It is off in all other cases. See Sem_Disp for - -- details of its use. - -- Is_Disabled (Flag15-Sem) -- A flag set in an N_Aspect_Specification or N_Pragma node if there was -- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma) @@ -1601,6 +1601,29 @@ package Sinfo is -- objects. The wrapper prevents interference between exception handlers -- and At_End handlers. + -- Is_Generic_Contract_Pragma (Flag2-Sem) + -- This flag is present in N_Pragma nodes. It is set when the pragma is + -- a source construct, applies to a generic unit or its body and denotes + -- one of the following contract-related annotations: + -- Abstract_State + -- Contract_Cases + -- Depends + -- Extensions_Visible + -- Global + -- Initial_Condition + -- Initializes + -- Post + -- Post_Class + -- Postcondition + -- Pre + -- Pre_Class + -- Precondition + -- Refined_Depends + -- Refined_Global + -- Refined_Post + -- Refined_State + -- Test_Case + -- Is_Ignored (Flag9-Sem) -- A flag set in an N_Aspect_Specification or N_Pragma node if there was -- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma) @@ -2441,6 +2464,7 @@ package Sinfo is -- Is_Checked (Flag11-Sem) -- Is_Delayed_Aspect (Flag14-Sem) -- Is_Disabled (Flag15-Sem) + -- Is_Generic_Contract_Pragma (Flag2-Sem) -- Is_Ignored (Flag9-Sem) -- Is_Inherited (Flag4-Sem) -- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set @@ -7518,9 +7542,9 @@ package Sinfo is -- N_Contract -- Sloc points to the subprogram's name - -- Pre_Post_Conditions (Node1) (set to Empty if none) - -- Contract_Test_Cases (Node2) (set to Empty if none) - -- Classifications (Node3) (set to Empty if none) + -- Pre_Post_Conditions (Node1-Sem) (set to Empty if none) + -- Contract_Test_Cases (Node2-Sem) (set to Empty if none) + -- Classifications (Node3-Sem) (set to Empty if none) -- Pre_Post_Conditions contains a collection of pragmas that correspond -- to pre- and postconditions associated with an entry or a subprogram @@ -8696,7 +8720,7 @@ package Sinfo is subtype N_Unit_Body is Node_Kind range N_Package_Body .. - N_Subprogram_Body; + N_Subprogram_Body; --------------------------- -- Node Access Functions -- @@ -9285,6 +9309,9 @@ package Sinfo is function Is_Folded_In_Parser (N : Node_Id) return Boolean; -- Flag4 + function Is_Generic_Contract_Pragma + (N : Node_Id) return Boolean; -- Flag2 + function Is_Ignored (N : Node_Id) return Boolean; -- Flag9 @@ -10287,9 +10314,6 @@ package Sinfo is procedure Set_Is_Disabled (N : Node_Id; Val : Boolean := True); -- Flag15 - procedure Set_Is_Ignored - (N : Node_Id; Val : Boolean := True); -- Flag9 - procedure Set_Is_Dynamic_Coextension (N : Node_Id; Val : Boolean := True); -- Flag18 @@ -10308,6 +10332,12 @@ package Sinfo is procedure Set_Is_Folded_In_Parser (N : Node_Id; Val : Boolean := True); -- Flag4 + procedure Set_Is_Generic_Contract_Pragma + (N : Node_Id; Val : Boolean := True); -- Flag2 + + procedure Set_Is_Ignored + (N : Node_Id; Val : Boolean := True); -- Flag9 + procedure Set_Is_In_Discriminant_Check (N : Node_Id; Val : Boolean := True); -- Flag11 @@ -10913,7 +10943,7 @@ package Sinfo is N_Pragma => (1 => False, -- Next_Pragma (Node1-Sem) 2 => True, -- Pragma_Argument_Associations (List2) - 3 => False, -- unused + 3 => False, -- Corresponding_Aspect (Node3-Sem) 4 => True, -- Pragma_Identifier (Node4) 5 => False), -- Next_Rep_Item (Node5-Sem) @@ -12297,9 +12327,9 @@ package Sinfo is 5 => False), -- unused N_Contract => - (1 => False, -- Pre_Post_Conditions (Node1) - 2 => False, -- Contract_Test_Cases (Node2) - 3 => False, -- Classifications (Node3) + (1 => False, -- Pre_Post_Conditions (Node1-Sem) + 2 => False, -- Contract_Test_Cases (Node2-Sem) + 3 => False, -- Classifications (Node3-Sem) 4 => False, -- unused 5 => False), -- unused @@ -12695,6 +12725,7 @@ package Sinfo is pragma Inline (Is_Expanded_Build_In_Place_Call); pragma Inline (Is_Finalization_Wrapper); pragma Inline (Is_Folded_In_Parser); + pragma Inline (Is_Generic_Contract_Pragma); pragma Inline (Is_Ignored); pragma Inline (Is_In_Discriminant_Check); pragma Inline (Is_Inherited); @@ -13030,6 +13061,7 @@ package Sinfo is pragma Inline (Set_Is_Expanded_Build_In_Place_Call); pragma Inline (Set_Is_Finalization_Wrapper); pragma Inline (Set_Is_Folded_In_Parser); + pragma Inline (Set_Is_Generic_Contract_Pragma); pragma Inline (Set_Is_Ignored); pragma Inline (Set_Is_In_Discriminant_Check); pragma Inline (Set_Is_Inherited); diff --git a/gcc/ada/treepr.adb b/gcc/ada/treepr.adb index 9d09a57ddfe..103038a2bc9 100644 --- a/gcc/ada/treepr.adb +++ b/gcc/ada/treepr.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -731,6 +731,54 @@ package body Treepr is Print_Eol; end if; + if Field_Present (Field36 (Ent)) then + Print_Str (Prefix); + Write_Field36_Name (Ent); + Write_Str (" = "); + Print_Field (Field36 (Ent)); + Print_Eol; + end if; + + if Field_Present (Field37 (Ent)) then + Print_Str (Prefix); + Write_Field37_Name (Ent); + Write_Str (" = "); + Print_Field (Field37 (Ent)); + Print_Eol; + end if; + + if Field_Present (Field38 (Ent)) then + Print_Str (Prefix); + Write_Field38_Name (Ent); + Write_Str (" = "); + Print_Field (Field38 (Ent)); + Print_Eol; + end if; + + if Field_Present (Field39 (Ent)) then + Print_Str (Prefix); + Write_Field39_Name (Ent); + Write_Str (" = "); + Print_Field (Field39 (Ent)); + Print_Eol; + end if; + + if Field_Present (Field40 (Ent)) then + Print_Str (Prefix); + Write_Field40_Name (Ent); + Write_Str (" = "); + Print_Field (Field40 (Ent)); + Print_Eol; + end if; + + if Field_Present (Field41 (Ent)) then + Print_Str (Prefix); + Write_Field41_Name (Ent); + Write_Str (" = "); + Print_Field (Field41 (Ent)); + Print_Eol; + end if; + Write_Entity_Flags (Ent, Prefix); end Print_Entity_Info;