From f99ff327e1901a374b4fb79b13be067b49c2c2ed Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 26 Oct 2015 12:26:32 +0100 Subject: [PATCH] [multiple changes] 2015-10-26 Hristian Kirtchev * aspects.adb Add an entry for entry bodies in table Has_Aspect_Specifications_Flag. (Aspects_On_Body_Or_Stub_OK): Entry bodies now allow for certain aspects. * contracts.adb (Add_Contract_Items): Code cleanup. Add processing for entry bodies, entry declarations and task units. (Analyze_Subprogram_Body_Contract): Renamed to Analyze_Entry_Or_Subprogram_Body_Contract. Do not analyze the contract of an entry body unless annotating the original tree. (Analyze_Subprogram_Contract): Renamed to Analyze_Entry_Or_Subprogram_Contract. Do not analyze the contract of an entry declaration unless annotating the original tree. (Analyze_Task_Contract): New routine. * contracts.ads (Add_Contract_Item): Update the comment on usage. (Analyze_Package_Body_Contract): Update comment on usage. (Analyze_Package_Contract): Update the comment on usage. (Analyze_Subprogram_Body_Contract): Renamed to Analyze_Entry_Or_Subprogram_Body_Contract. (Analyze_Subprogram_Body_Stub_Contract): Update the comment on usage. (Analyze_Subprogram_Contract): Renamed to Analyze_Entry_Or_Subprogram_Contract. (Analyze_Task_Contract): New routine. * einfo.adb (Contract): Restructure the assertion to include entries and task units. (SPARK_Pragma): This attribute now applies to operators. (SPARK_Pragma_Inherited): This flag now applies to operators. (Set_Contract): Restructure the assertion to include entries and task units. (Set_SPARK_Pragma): This attribute now applies to operators. (Set_SPARK_Pragma_Inherited): This flag now applies to operators. (Write_Field34_Name): Write out all Ekinds that have a contract. (Write_Field40_Name): SPARK_Pragma now applies to operators. * einfo.ads: Update the documentation of attribute Contract along with usage in nodes. Update the documentation of attributes SPARK_Pragma and SPARK_Pragma_Inherited. * exp_ch6.adb (Freeze_Subprogram): Update the call to Analyze_Subprogram_Contract. * par-ch9.adb (P_Entry_Barrier): Do not parse keyword "is" as it is not part of the entry barrier production. (P_Entry_Body): Parse the optional aspect specifications. Diagnose misplaced aspects. * sem_attr.adb (Analyze_Attribute_Old_Result): Update the call to Find_Related_Subprogram_Or_Body. * sem_aux.adb (Unit_Declaration_Node) Add an entry for entry declarations and bodies. * sem_ch3.adb (Analyze_Declarations): Analyze the contracts of entry declarations, entry bodies and task units. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Update the call to Analyze_Subprogram_Body_Contract. (Analyze_Subprogram_Body_Helper): Update the call to Analyze_Subprogram_Body_Contract. * sem_ch9.adb (Analyze_Entry_Body): Analyze the aspect specifications and the contract. * sem_ch10.adb (Analyze_Compilation_Unit): Update the call to Analyze_Subprogram_Contract. * sem_ch12.adb (Save_References_In_Pragma): Update the call to Find_Related_Subprogram_Or_Body. * sem_ch13.adb (Analyze_Aspects_On_Body_Or_Stub): Use Unique_Defining_Entity rather than rummaging around in nodes. (Diagnose_Misplaced_Aspects): Update comment on usage. Update the error messages to accomondate the increasing number of contexts. * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. (Analyze_Depends_Global): Update the call to Find_Related_Subprogram_Or_Body. Add processing for entry declarations. (Analyze_Depends_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Task units have no formal parameters to install. (Analyze_Global_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Task units have no formal parameters to install. (Analyze_Global_Item): Use Fix_Msg to handle the increasing number of contexts. (Analyze_Pragma): Update the call to Find_Related_Subprogram_Or_Body. Perform full analysis when various pragmas appear in an entry body. (Analyze_Pre_Post_Condition): Update the call to Find_Related_Subprogram_Or_Body. Perform full analysis when the pragma appears in an entry body. (Analyze_Pre_Post_Condition_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. (Analyze_Refined_Depends_Global_Post): Update the call to Find_Related_Subprogram_Or_Body. Use Fix_Msg to handle the increasing number of contexts. (Analyze_Refined_Depends_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain the entity of the spec. Use Fix_Msg to handle the increasing number of contexts. (Analyze_Refined_Global_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain the entity of the spec. Use Fix_Msg to handle the increasing number of contexts. (Analyze_Test_Case_In_Decl_Part): Update the call to Find_Related_Subprogram_Or_Body. (Check_Dependency_Clause): Use Fix_Msg to handle the increasing number of contexts. (Check_Mode_Restriction_In_Enclosing_Context): Use Fix_Msg to handle the increasing number of contexts. (Collect_Subprogram_Inputs_Outputs): Use the refined versions of the pragmas when the context is an entry body or a task body. (Find_Related_Subprogram_Or_Body): Renamed to Find_Related_Declaration_Or_Body. Add processing for entries and task units. (Fix_Msg): New routine. (Role_Error): Use Fix_Msg to handle the increasing number of contexts. * sem_prag.ads (Find_Related_Subprogram_Or_Body): Renamed to Find_Related_Declaration_Or_Body. Update the comment on usage. * sem_util.adb (Is_Entry_Body): New routine. (Is_Entry_Declaration): New routine. * sem_util.ads (Is_Entry_Body): New routine. (Is_Entry_Declaration): New routine. 2015-10-26 Ed Schonberg * inline.adb (Has_Excluded_Declaration): A subtype declaration with a predicate aspect generates a subprogram, and therefore prevents the inlining of the enclosing subprogram. * osint.ads: Fix typo. From-SVN: r229333 --- gcc/ada/ChangeLog | 123 +++++++++ gcc/ada/aspects.adb | 4 +- gcc/ada/contracts.adb | 583 +++++++++++++++++++++++++----------------- gcc/ada/contracts.ads | 75 +++--- gcc/ada/einfo.adb | 66 +++-- gcc/ada/einfo.ads | 41 +-- gcc/ada/exp_ch6.adb | 2 +- gcc/ada/inline.adb | 31 +++ gcc/ada/osint.ads | 2 +- gcc/ada/par-ch9.adb | 97 ++++--- gcc/ada/sem_attr.adb | 2 +- gcc/ada/sem_aux.adb | 6 +- gcc/ada/sem_ch10.adb | 2 +- gcc/ada/sem_ch12.adb | 3 +- gcc/ada/sem_ch13.adb | 20 +- gcc/ada/sem_ch3.adb | 13 +- gcc/ada/sem_ch6.adb | 4 +- gcc/ada/sem_ch9.adb | 14 +- gcc/ada/sem_prag.adb | 471 +++++++++++++++++++++------------- gcc/ada/sem_prag.ads | 35 ++- gcc/ada/sem_util.adb | 22 ++ gcc/ada/sem_util.ads | 6 + 22 files changed, 1068 insertions(+), 554 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2e3f50e79cf..ae7c1a460ae 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,126 @@ +2015-10-26 Hristian Kirtchev + + * aspects.adb Add an entry for entry bodies in table + Has_Aspect_Specifications_Flag. + (Aspects_On_Body_Or_Stub_OK): Entry bodies now allow for certain + aspects. + * contracts.adb (Add_Contract_Items): Code cleanup. Add + processing for entry bodies, entry declarations and task units. + (Analyze_Subprogram_Body_Contract): Renamed + to Analyze_Entry_Or_Subprogram_Body_Contract. Do not + analyze the contract of an entry body unless annotating the + original tree. + (Analyze_Subprogram_Contract): Renamed to + Analyze_Entry_Or_Subprogram_Contract. Do not analyze the contract + of an entry declaration unless annotating the original tree. + (Analyze_Task_Contract): New routine. + * contracts.ads (Add_Contract_Item): Update the comment on usage. + (Analyze_Package_Body_Contract): Update comment on usage. + (Analyze_Package_Contract): Update the comment on usage. + (Analyze_Subprogram_Body_Contract): Renamed to + Analyze_Entry_Or_Subprogram_Body_Contract. + (Analyze_Subprogram_Body_Stub_Contract): Update the comment on usage. + (Analyze_Subprogram_Contract): Renamed to + Analyze_Entry_Or_Subprogram_Contract. + (Analyze_Task_Contract): New routine. + * einfo.adb (Contract): Restructure the assertion to include + entries and task units. + (SPARK_Pragma): This attribute now applies to operators. + (SPARK_Pragma_Inherited): This flag now applies to operators. + (Set_Contract): Restructure the assertion to include entries and task + units. + (Set_SPARK_Pragma): This attribute now applies to operators. + (Set_SPARK_Pragma_Inherited): This flag now applies to operators. + (Write_Field34_Name): Write out all Ekinds that have a contract. + (Write_Field40_Name): SPARK_Pragma now applies to operators. + * einfo.ads: Update the documentation of attribute Contract along + with usage in nodes. Update the documentation of attributes + SPARK_Pragma and SPARK_Pragma_Inherited. + * exp_ch6.adb (Freeze_Subprogram): Update the call to + Analyze_Subprogram_Contract. + * par-ch9.adb (P_Entry_Barrier): Do not parse keyword "is" as it + is not part of the entry barrier production. + (P_Entry_Body): Parse the optional aspect specifications. Diagnose + misplaced aspects. + * sem_attr.adb (Analyze_Attribute_Old_Result): Update the call + to Find_Related_Subprogram_Or_Body. + * sem_aux.adb (Unit_Declaration_Node) Add an entry for entry + declarations and bodies. + * sem_ch3.adb (Analyze_Declarations): Analyze the contracts of + entry declarations, entry bodies and task units. + * sem_ch6.adb (Analyze_Generic_Subprogram_Body): + Update the call to Analyze_Subprogram_Body_Contract. + (Analyze_Subprogram_Body_Helper): Update the call to + Analyze_Subprogram_Body_Contract. + * sem_ch9.adb (Analyze_Entry_Body): Analyze the aspect + specifications and the contract. + * sem_ch10.adb (Analyze_Compilation_Unit): Update the call to + Analyze_Subprogram_Contract. + * sem_ch12.adb (Save_References_In_Pragma): Update the call to + Find_Related_Subprogram_Or_Body. + * sem_ch13.adb (Analyze_Aspects_On_Body_Or_Stub): Use + Unique_Defining_Entity rather than rummaging around in nodes. + (Diagnose_Misplaced_Aspects): Update comment on usage. Update the + error messages to accomondate the increasing number of contexts. + * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): + Update the call to Find_Related_Subprogram_Or_Body. + (Analyze_Depends_Global): Update the call to + Find_Related_Subprogram_Or_Body. Add processing for entry + declarations. + (Analyze_Depends_In_Decl_Part): Update the call + to Find_Related_Subprogram_Or_Body. Task units have no formal + parameters to install. (Analyze_Global_In_Decl_Part): Update + the call to Find_Related_Subprogram_Or_Body. Task units have no + formal parameters to install. + (Analyze_Global_Item): Use Fix_Msg to handle the increasing number of + contexts. + (Analyze_Pragma): Update the call to Find_Related_Subprogram_Or_Body. + Perform full analysis when various pragmas appear in an entry body. + (Analyze_Pre_Post_Condition): Update the call to + Find_Related_Subprogram_Or_Body. Perform full analysis when the pragma + appears in an entry body. + (Analyze_Pre_Post_Condition_In_Decl_Part): Update the call to + Find_Related_Subprogram_Or_Body. + (Analyze_Refined_Depends_Global_Post): Update + the call to Find_Related_Subprogram_Or_Body. Use + Fix_Msg to handle the increasing number of contexts. + (Analyze_Refined_Depends_In_Decl_Part): Update + the call to Find_Related_Subprogram_Or_Body. Use + Unique_Defining_Entity to obtain the entity of the + spec. Use Fix_Msg to handle the increasing number of contexts. + (Analyze_Refined_Global_In_Decl_Part): Update the call to + Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain + the entity of the spec. Use Fix_Msg to handle the increasing number of + contexts. + (Analyze_Test_Case_In_Decl_Part): Update the call to + Find_Related_Subprogram_Or_Body. + (Check_Dependency_Clause): Use Fix_Msg to handle the increasing number + of contexts. + (Check_Mode_Restriction_In_Enclosing_Context): Use + Fix_Msg to handle the increasing number of contexts. + (Collect_Subprogram_Inputs_Outputs): Use the refined + versions of the pragmas when the context is an entry body or + a task body. + (Find_Related_Subprogram_Or_Body): Renamed to + Find_Related_Declaration_Or_Body. Add processing for entries + and task units. + (Fix_Msg): New routine. + (Role_Error): Use Fix_Msg to handle the increasing number of contexts. + * sem_prag.ads (Find_Related_Subprogram_Or_Body): Renamed to + Find_Related_Declaration_Or_Body. Update the comment on usage. + * sem_util.adb (Is_Entry_Body): New routine. + (Is_Entry_Declaration): New routine. + * sem_util.ads (Is_Entry_Body): New routine. + (Is_Entry_Declaration): New routine. + +2015-10-26 Ed Schonberg + + * inline.adb (Has_Excluded_Declaration): A subtype declaration + with a predicate aspect generates a subprogram, and therefore + prevents the inlining of the enclosing subprogram. + * osint.ads: Fix typo. + + 2015-10-26 Ed Schonberg * sem_case.adb (Check_Choice_Set): Choose initial choice range diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 3fc20498fc1..f42e9bfd723 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -154,7 +154,8 @@ package body Aspects is pragma Assert (Has_Aspects (N)); pragma Assert (Nkind (N) in N_Body_Stub - or else Nkind_In (N, N_Package_Body, + or else Nkind_In (N, N_Entry_Body, + N_Package_Body, N_Protected_Body, N_Subprogram_Body, N_Task_Body)); @@ -427,6 +428,7 @@ package body Aspects is Has_Aspect_Specifications_Flag : constant array (Node_Kind) of Boolean := (N_Abstract_Subprogram_Declaration => True, N_Component_Declaration => True, + N_Entry_Body => True, N_Entry_Declaration => True, N_Exception_Declaration => True, N_Exception_Renaming_Declaration => True, diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index e41ae2054d0..87c39fbd551 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -121,7 +121,7 @@ package body Contracts is Set_Contract (Id, Items); end if; - -- Contract items related to constants. Applicable pragmas are: + -- Constants, the applicable pragmas are: -- Part_Of if Ekind (Id) = E_Constant then @@ -134,37 +134,17 @@ package body Contracts is raise Program_Error; end if; - -- Contract items related to [generic] packages or instantiations. The - -- applicable pragmas are: - -- Abstract_States - -- Initial_Condition - -- Initializes - -- Part_Of (instantiation only) - - elsif Ekind_In (Id, E_Generic_Package, E_Package) then - if Nam_In (Prag_Nam, Name_Abstract_State, - Name_Initial_Condition, - Name_Initializes) - then - Add_Classification; - - -- Indicator Part_Of must be associated with a package instantiation + -- Entry bodies, the applicable pragmas are: + -- Refined_Depends + -- Refined_Global + -- Refined_Post - elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then + elsif Is_Entry_Body (Id) then + if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then Add_Classification; - -- The pragma is not a proper contract item - - else - raise Program_Error; - end if; - - -- Contract items related to package bodies. The applicable pragmas are: - -- Refined_States - - elsif Ekind (Id) = E_Package_Body then - if Prag_Nam = Name_Refined_State then - Add_Classification; + elsif Prag_Nam = Name_Refined_Post then + Add_Pre_Post_Condition; -- The pragma is not a proper contract item @@ -172,8 +152,7 @@ package body Contracts is raise Program_Error; end if; - -- Contract items related to subprogram or entry declarations. The - -- applicable pragmas are: + -- Entry or subprogram declarations, the applicable pragmas are: -- Contract_Cases -- Depends -- Extensions_Visible @@ -183,9 +162,11 @@ package body Contracts is -- Test_Case -- Volatile_Function - elsif Ekind_In (Id, E_Entry, E_Entry_Family) - or else Is_Generic_Subprogram (Id) - or else Is_Subprogram (Id) + elsif Is_Entry_Declaration (Id) + or else Ekind_In (Id, E_Function, + E_Generic_Function, + E_Generic_Procedure, + E_Procedure) then if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then Add_Pre_Post_Condition; @@ -210,7 +191,44 @@ package body Contracts is raise Program_Error; end if; - -- Contract items related to subprogram bodies. Applicable pragmas are: + -- Packages or instantiations, the applicable pragmas are: + -- Abstract_States + -- Initial_Condition + -- Initializes + -- Part_Of (instantiation only) + + elsif Ekind_In (Id, E_Generic_Package, E_Package) then + if Nam_In (Prag_Nam, Name_Abstract_State, + Name_Initial_Condition, + Name_Initializes) + then + Add_Classification; + + -- Indicator Part_Of must be associated with a package instantiation + + elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then + Add_Classification; + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; + + -- Package bodies, the applicable pragmas are: + -- Refined_States + + elsif Ekind (Id) = E_Package_Body then + if Prag_Nam = Name_Refined_State then + Add_Classification; + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; + + -- Subprogram bodies, the applicable pragmas are: -- Postcondition -- Precondition -- Refined_Depends @@ -233,7 +251,35 @@ package body Contracts is raise Program_Error; end if; - -- Contract items related to variables. Applicable pragmas are: + -- Task bodies, the applicable pragmas are: + -- Refined_Depends + -- Refined_Global + + elsif Ekind (Id) = E_Task_Body then + if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then + Add_Classification; + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; + + -- Task units, the applicable pragmas are: + -- Depends + -- Global + + elsif Ekind (Id) = E_Task_Type then + if Nam_In (Prag_Nam, Name_Depends, Name_Global) then + Add_Classification; + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; + + -- Variables, the applicable pragmas are: -- Async_Readers -- Async_Writers -- Constant_After_Elaboration @@ -284,6 +330,231 @@ package body Contracts is end loop; end Analyze_Enclosing_Package_Body_Contract; + ----------------------------------------------- + -- Analyze_Entry_Or_Subprogram_Body_Contract -- + ----------------------------------------------- + + procedure Analyze_Entry_Or_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); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); + Mode : SPARK_Mode_Type; + + 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; + + -- Do not analyze the contract of an entry body unless annotating the + -- original tree. It is preferable to analyze the contract after the + -- entry body has been transformed into a subprogram body to properly + -- handle references to unpacked formals. + + elsif Ekind_In (Body_Id, E_Entry, E_Entry_Family) + and then not ASIS_Mode + and then not GNATprove_Mode + then + return; + + -- Do not analyze a contract multiple times + + elsif Present (Items) then + if Analyzed (Items) then + return; + else + Set_Analyzed (Items); + end if; + 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); + + -- Ensure that the contract cases or postconditions mention 'Result or + -- define a post-state. + + Check_Result_And_Post_State (Body_Id); + + -- A stand-alone nonvolatile function body cannot have an effectively + -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This + -- check is relevant only when SPARK_Mode is on, as it is not a standard + -- legality rule. The check is performed here because Volatile_Function + -- is processed after the analysis of the related subprogram body. + + if SPARK_Mode = On + and then Ekind_In (Body_Id, E_Function, E_Generic_Function) + and then not Is_Volatile_Function (Body_Id) + then + Check_Nonvolatile_Function_Profile (Body_Id); + end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + Restore_SPARK_Mode (Mode); + + -- Capture all global references in a generic subprogram body now that + -- the contract has been analyzed. + + if Is_Generic_Declaration_Or_Body (Body_Decl) then + Save_Global_References_In_Contract + (Templ => Original_Node (Body_Decl), + Gen_Id => Spec_Id); + end if; + + -- Deal with preconditions, [refined] postconditions, Contract_Cases, + -- invariants and predicates associated with body and its spec. Do not + -- expand the contract of subprogram body stubs. + + if Nkind (Body_Decl) = N_Subprogram_Body then + Expand_Subprogram_Contract (Body_Id); + end if; + end Analyze_Entry_Or_Subprogram_Body_Contract; + + ------------------------------------------ + -- Analyze_Entry_Or_Subprogram_Contract -- + ------------------------------------------ + + procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id) is + 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; + + begin + -- Do not analyze the contract of an entry declaration unless annotating + -- the original tree. It is preferable to analyze the contract after the + -- entry declaration has been transformed into a subprogram declaration + -- to properly handle references to unpacked formals. + + if Ekind_In (Subp_Id, E_Entry, E_Entry_Family) + and then not ASIS_Mode + and then not GNATprove_Mode + then + return; + + -- Do not analyze a contract multiple times + + elsif Present (Items) then + if Analyzed (Items) then + return; + else + Set_Analyzed (Items); + end if; + 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 (Subp_Id, Mode); + + -- 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 + null; + + elsif Present (Items) then + + -- Analyze pre- and postconditions + + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + Analyze_Pre_Post_Condition_In_Decl_Part (Prag); + Prag := Next_Pragma (Prag); + end loop; + + -- Analyze contract-cases and test-cases + + Prag := Contract_Test_Cases (Items); + while Present (Prag) loop + Prag_Nam := Pragma_Name (Prag); + + if Prag_Nam = Name_Contract_Cases then + Analyze_Contract_Cases_In_Decl_Part (Prag); + else + pragma Assert (Prag_Nam = Name_Test_Case); + Analyze_Test_Case_In_Decl_Part (Prag); + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Analyze classification pragmas + + Prag := Classifications (Items); + while Present (Prag) loop + Prag_Nam := Pragma_Name (Prag); + + if Prag_Nam = Name_Depends then + Depends := Prag; + + elsif Prag_Nam = Name_Global then + Global := Prag; + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Analyze Global first, as Depends may mention items classified in + -- the global categorization. + + if Present (Global) then + Analyze_Global_In_Decl_Part (Global); + end if; + + -- Depends must be analyzed after Global in order to see the modes of + -- all global items. + + if Present (Depends) then + Analyze_Depends_In_Decl_Part (Depends); + end if; + + -- Ensure that the contract cases or postconditions mention 'Result + -- or define a post-state. + + Check_Result_And_Post_State (Subp_Id); + end if; + + -- A nonvolatile function cannot have an effectively volatile formal + -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant + -- only when SPARK_Mode is on, as it is not a standard legality rule. + -- The check is performed here because pragma Volatile_Function is + -- processed after the analysis of the related subprogram declaration. + + if SPARK_Mode = On + and then Ekind_In (Subp_Id, E_Function, E_Generic_Function) + and then not Is_Volatile_Function (Subp_Id) + then + Check_Nonvolatile_Function_Profile (Subp_Id); + end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + Restore_SPARK_Mode (Mode); + + -- Capture all global references in a generic subprogram now that the + -- contract has been analyzed. + + if Is_Generic_Declaration_Or_Body (Subp_Decl) then + Save_Global_References_In_Contract + (Templ => Original_Node (Subp_Decl), + Gen_Id => Subp_Id); + end if; + end Analyze_Entry_Or_Subprogram_Contract; + ----------------------------- -- Analyze_Object_Contract -- ----------------------------- @@ -617,94 +888,47 @@ package body Contracts is end if; end Analyze_Package_Contract; - -------------------------------------- - -- Analyze_Subprogram_Body_Contract -- - -------------------------------------- + ------------------------------------------- + -- Analyze_Subprogram_Body_Stub_Contract -- + ------------------------------------------- - 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); - Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); - Mode : SPARK_Mode_Type; + procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is + Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); 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; - - -- Do not analyze a contract multiple times - - elsif Present (Items) then - if Analyzed (Items) then - return; - else - Set_Analyzed (Items); - end if; - 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); - - -- Ensure that the contract cases or postconditions mention 'Result or - -- define a post-state. - - Check_Result_And_Post_State (Body_Id); - - -- A stand-alone nonvolatile function body cannot have an effectively - -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This - -- check is relevant only when SPARK_Mode is on, as it is not a standard - -- legality rule. The check is performed here because Volatile_Function - -- is processed after the analysis of the related subprogram body. - - if SPARK_Mode = On - and then Ekind_In (Body_Id, E_Function, E_Generic_Function) - and then not Is_Volatile_Function (Body_Id) - then - Check_Nonvolatile_Function_Profile (Body_Id); - end if; - - -- Restore the SPARK_Mode of the enclosing context after all delayed - -- pragmas have been analyzed. - - Restore_SPARK_Mode (Mode); + -- A subprogram body stub may act as its own spec or as the completion + -- of a previous declaration. Depending on the context, the contract of + -- the stub may contain two sets of pragmas. - -- Capture all global references in a generic subprogram body now that - -- the contract has been analyzed. + -- The stub is a completion, the applicable pragmas are: + -- Refined_Depends + -- Refined_Global - if Is_Generic_Declaration_Or_Body (Body_Decl) then - Save_Global_References_In_Contract - (Templ => Original_Node (Body_Decl), - Gen_Id => Spec_Id); - end if; + if Present (Spec_Id) then + Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id); - -- Deal with preconditions, [refined] postconditions, Contract_Cases, - -- invariants and predicates associated with body and its spec. Do not - -- expand the contract of subprogram body stubs. + -- The stub acts as its own spec, the applicable pragmas are: + -- Contract_Cases + -- Depends + -- Global + -- Postcondition + -- Precondition + -- Test_Case - if Nkind (Body_Decl) = N_Subprogram_Body then - Expand_Subprogram_Contract (Body_Id); + else + Analyze_Entry_Or_Subprogram_Contract (Stub_Id); end if; - end Analyze_Subprogram_Body_Contract; + end Analyze_Subprogram_Body_Stub_Contract; - --------------------------------- - -- Analyze_Subprogram_Contract -- - --------------------------------- + --------------------------- + -- Analyze_Task_Contract -- + --------------------------- - procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is - 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; + procedure Analyze_Task_Contract (Task_Id : Entity_Id) is + Items : constant Node_Id := Contract (Task_Id); + Mode : SPARK_Mode_Type; + Prag : Node_Id; begin -- Do not analyze a contract multiple times @@ -722,136 +946,31 @@ package body Contracts is -- context. To remedy this, restore the original SPARK_Mode of the -- related subprogram body. - Save_SPARK_Mode_And_Set (Subp_Id, Mode); - - -- 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 - null; - - elsif Present (Items) then - - -- Analyze pre- and postconditions - - Prag := Pre_Post_Conditions (Items); - while Present (Prag) loop - Analyze_Pre_Post_Condition_In_Decl_Part (Prag); - Prag := Next_Pragma (Prag); - end loop; - - -- Analyze contract-cases and test-cases - - Prag := Contract_Test_Cases (Items); - while Present (Prag) loop - Prag_Nam := Pragma_Name (Prag); - - if Prag_Nam = Name_Contract_Cases then - Analyze_Contract_Cases_In_Decl_Part (Prag); - else - pragma Assert (Prag_Nam = Name_Test_Case); - Analyze_Test_Case_In_Decl_Part (Prag); - end if; - - Prag := Next_Pragma (Prag); - end loop; - - -- Analyze classification pragmas - - Prag := Classifications (Items); - while Present (Prag) loop - Prag_Nam := Pragma_Name (Prag); - - if Prag_Nam = Name_Depends then - Depends := Prag; - - elsif Prag_Nam = Name_Global then - Global := Prag; - end if; - - Prag := Next_Pragma (Prag); - end loop; - - -- Analyze Global first, as Depends may mention items classified in - -- the global categorization. - - if Present (Global) then - Analyze_Global_In_Decl_Part (Global); - end if; - - -- Depends must be analyzed after Global in order to see the modes of - -- all global items. + Save_SPARK_Mode_And_Set (Task_Id, Mode); - if Present (Depends) then - Analyze_Depends_In_Decl_Part (Depends); - end if; + -- Analyze Global first, as Depends may mention items classified in the + -- global categorization. - -- Ensure that the contract cases or postconditions mention 'Result - -- or define a post-state. + Prag := Get_Pragma (Task_Id, Pragma_Global); - Check_Result_And_Post_State (Subp_Id); + if Present (Prag) then + Analyze_Global_In_Decl_Part (Prag); end if; - -- A nonvolatile function cannot have an effectively volatile formal - -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant - -- only when SPARK_Mode is on, as it is not a standard legality rule. - -- The check is performed here because pragma Volatile_Function is - -- processed after the analysis of the related subprogram declaration. + -- Depends must be analyzed after Global in order to see the modes of + -- all global items. - if SPARK_Mode = On - and then Ekind_In (Subp_Id, E_Function, E_Generic_Function) - and then not Is_Volatile_Function (Subp_Id) - then - Check_Nonvolatile_Function_Profile (Subp_Id); + Prag := Get_Pragma (Task_Id, Pragma_Depends); + + if Present (Prag) then + Analyze_Depends_In_Decl_Part (Prag); end if; -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. Restore_SPARK_Mode (Mode); - - -- Capture all global references in a generic subprogram now that the - -- contract has been analyzed. - - if Is_Generic_Declaration_Or_Body (Subp_Decl) then - Save_Global_References_In_Contract - (Templ => Original_Node (Subp_Decl), - Gen_Id => Subp_Id); - end if; - end Analyze_Subprogram_Contract; - - ------------------------------------------- - -- Analyze_Subprogram_Body_Stub_Contract -- - ------------------------------------------- - - procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is - Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); - - begin - -- A subprogram body stub may act as its own spec or as the completion - -- of a previous declaration. Depending on the context, the contract of - -- the stub may contain two sets of pragmas. - - -- The stub is a completion, the applicable pragmas are: - -- Refined_Depends - -- Refined_Global - - if Present (Spec_Id) then - Analyze_Subprogram_Body_Contract (Stub_Id); - - -- The stub acts as its own spec, the applicable pragmas are: - -- Contract_Cases - -- Depends - -- Global - -- Postcondition - -- Precondition - -- Test_Case - - else - Analyze_Subprogram_Contract (Stub_Id); - end if; - end Analyze_Subprogram_Body_Stub_Contract; + end Analyze_Task_Contract; ----------------------------- -- Create_Generic_Contract -- diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index 6f911a36fc2..3814dfc8277 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -31,9 +31,9 @@ with Types; use Types; package Contracts is procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id); - -- Add pragma Prag to the contract of a constant, entry, package [body], - -- subprogram [body], or variable denoted by Id. The following are valid - -- pragmas: + -- Add pragma Prag to the contract of a constant, entry, entry family, + -- [generic] package, package body, [generic] subprogram, subprogram body, + -- variable or task unit denoted by Id. The following are valid pragmas: -- Abstract_State -- Async_Readers -- Async_Writers @@ -60,6 +60,31 @@ package Contracts is -- Analyze the contract of the nearest package body (if any) enclosing -- package or subprogram body Body_Decl. + procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id); + -- Analyze all delayed pragmas chained on the contract of entry or + -- subprogram body Body_Id as if they appeared at the end of a declarative + -- region. Pragmas in question are: + -- Contract_Cases (stand alone subprogram body) + -- Depends (stand alone subprogram body) + -- Global (stand alone subprogram body) + -- Postcondition (stand alone subprogram body) + -- Precondition (stand alone subprogram body) + -- Refined_Depends + -- Refined_Global + -- Refined_Post + -- Test_Case (stand alone subprogram body) + + procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id); + -- Analyze all delayed pragmas chained on the contract of entry or + -- subprogram Subp_Id as if they appeared at the end of a declarative + -- region. The pragmas in question are: + -- Contract_Cases + -- Depends + -- Global + -- Postcondition + -- Precondition + -- Test_Case + procedure Analyze_Object_Contract (Obj_Id : Entity_Id); -- Analyze all delayed pragmas chained on the contract of object Obj_Id as -- if they appeared at the end of the declarative region. The pragmas to be @@ -73,51 +98,26 @@ package Contracts is procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id; Freeze_Id : Entity_Id := Empty); - -- Analyze all delayed aspects chained on the contract of package body + -- Analyze all delayed pragmas chained on the contract of package body -- Body_Id as if they appeared at the end of a declarative region. The - -- aspects that are considered are: + -- pragmas that are considered are: -- Refined_State -- -- Freeze_Id is the entity of a [generic] package body or a [generic] -- subprogram body which "freezes" the contract of Body_Id. procedure Analyze_Package_Contract (Pack_Id : Entity_Id); - -- Analyze all delayed aspects chained on the contract of package Pack_Id - -- as if they appeared at the end of a declarative region. The aspects + -- Analyze all delayed pragmas chained on the contract of package Pack_Id + -- as if they appeared at the end of a declarative region. The pragmas -- that are considered are: -- Initial_Condition -- Initializes -- Part_Of - procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id); - -- Analyze all delayed aspects chained on the contract of subprogram body - -- Body_Id as if they appeared at the end of a declarative region. Aspects - -- in question are: - -- Contract_Cases (stand alone body) - -- Depends (stand alone body) - -- Global (stand alone body) - -- Postcondition (stand alone body) - -- Precondition (stand alone body) - -- Refined_Depends - -- Refined_Global - -- Refined_Post - -- Test_Case (stand alone body) - - procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id); - -- Analyze all delayed aspects chained on the contract of subprogram - -- Subp_Id as if they appeared at the end of a declarative region. The - -- aspects in question are: - -- Contract_Cases - -- Depends - -- Global - -- Postcondition - -- Precondition - -- Test_Case - procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id); - -- Analyze all delayed aspects chained on the contract of a subprogram body + -- Analyze all delayed pragmas chained on the contract of a subprogram body -- stub Stub_Id as if they appeared at the end of a declarative region. The - -- aspects in question are: + -- pragmas in question are: -- Contract_Cases -- Depends -- Global @@ -128,6 +128,13 @@ package Contracts is -- Refined_Post -- Test_Case + procedure Analyze_Task_Contract (Task_Id : Entity_Id); + -- Analyze all delayed pragmas chained on the contract of a task unit + -- Task_Id as if they appeared at the end of a declarative region. The + -- pragmas in question are: + -- Depends + -- Global + 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 diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 08072f23010..d7d19ab5117 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -1205,16 +1205,25 @@ package body Einfo is function Contract (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Constant, - E_Entry, + (Ekind_In (Id, E_Constant, -- object variants + E_Variable) + or else + Ekind_In (Id, E_Entry, -- overloadable variants E_Entry_Family, - E_Generic_Package, + E_Function, + E_Generic_Function, + E_Generic_Procedure, + E_Operator, + E_Procedure, + E_Subprogram_Body) + or else + Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body, - E_Subprogram_Body, - E_Variable, - E_Void) - or else Is_Subprogram_Or_Generic_Subprogram (Id)); + E_Package_Body) + or else + Ekind_In (Id, E_Task_Body, -- synchronized variants + E_Task_Type, + E_Void)); -- special purpose return Node34 (Id); end Contract; @@ -3139,6 +3148,7 @@ package body Einfo is E_Function, E_Generic_Function, E_Generic_Procedure, + E_Operator, E_Procedure, E_Subprogram_Body) or else @@ -3161,6 +3171,7 @@ package body Einfo is E_Function, E_Generic_Function, E_Generic_Procedure, + E_Operator, E_Procedure, E_Subprogram_Body) or else @@ -3834,16 +3845,25 @@ package body Einfo is procedure Set_Contract (Id : E; V : N) is begin pragma Assert - (Ekind_In (Id, E_Constant, - E_Entry, + (Ekind_In (Id, E_Constant, -- object variants + E_Variable) + or else + Ekind_In (Id, E_Entry, -- overloadable variants E_Entry_Family, - E_Generic_Package, + E_Function, + E_Generic_Function, + E_Generic_Procedure, + E_Operator, + E_Procedure, + E_Subprogram_Body) + or else + Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body, - E_Subprogram_Body, - E_Variable, - E_Void) - or else Is_Subprogram_Or_Generic_Subprogram (Id)); + E_Package_Body) + or else + Ekind_In (Id, E_Task_Body, -- synchronized variants + E_Task_Type, + E_Void)); -- special purpose Set_Node34 (Id, V); end Set_Contract; @@ -6170,6 +6190,7 @@ package body Einfo is E_Function, E_Generic_Function, E_Generic_Procedure, + E_Operator, E_Procedure, E_Subprogram_Body) or else @@ -6192,6 +6213,7 @@ package body Einfo is E_Function, E_Generic_Function, E_Generic_Procedure, + E_Operator, E_Procedure, E_Subprogram_Body) or else @@ -10212,14 +10234,19 @@ package body Einfo is when E_Constant | E_Entry | E_Entry_Family | + E_Function | + E_Generic_Function | E_Generic_Package | + E_Generic_Procedure | + E_Operator | E_Package | E_Package_Body | + E_Procedure | E_Subprogram_Body | + E_Task_Body | + E_Task_Type | E_Variable | - E_Void | - Generic_Subprogram_Kind | - Subprogram_Kind => + E_Void => Write_Str ("Contract"); when others => @@ -10317,6 +10344,7 @@ package body Einfo is E_Generic_Function | E_Generic_Package | E_Generic_Procedure | + E_Operator | E_Package | E_Package_Body | E_Procedure | diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index ecefb11916a..e74a0a7ffc2 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -705,10 +705,10 @@ package Einfo is -- of declaration, procedure call, assignment statement or pragma. -- Contract (Node34) --- Defined in constant, 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. +-- Defined in constant, entry, entry family, operator, [generic] package, +-- package body, [generic] subprogram, subprogram body, variable and task +-- type entities. Points to the contract of the entity, holding various +-- assertion items and data classifiers. -- Corresponding_Concurrent_Type (Node18) -- Defined in record types that are constructed by the expander to @@ -4087,19 +4087,20 @@ package Einfo is -- inherited, rather than a local one. -- SPARK_Pragma (Node40) --- Present in entries, [generic] package specs, package bodies, [generic] --- subprogram specs, subprogram bodies and synchronized types. Points to --- the N_Pragma node that applies to the spec or body. This is either set --- by a local SPARK_Mode pragma or is inherited from the context (from an --- outer scope for the spec case or from the spec for the body case). In --- the case where it is inherited the flag SPARK_Pragma_Inherited is set. --- Empty if no SPARK_Mode pragma is applicable. +-- Present in entries, operators, [generic] packages, package bodies, +-- [generic] subprograms, subprogram bodies and synchronized types. +-- Points to the N_Pragma node that applies to the spec or body. This +-- is either set by a local SPARK_Mode pragma or is inherited from the +-- context (from an outer scope for the spec case or from the spec for +-- the body case). In the case where it is inherited the flag +-- SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma is +-- applicable. -- SPARK_Pragma_Inherited (Flag265) --- Present in entries, [generic] package specs, package bodies, [generic] --- subprogram specs, subprogram bodies and synchronized types. Set if the --- SPARK_Pragma attribute points to a pragma that is inherited, rather --- than a local one. +-- Present in entries, operators, [generic] packages, package bodies, +-- [generic] subprograms, subprogram bodies and synchronized types. Set +-- if the SPARK_Pragma attribute points to a pragma that is inherited, +-- rather than a local one. -- Spec_Entity (Node19) -- Defined in package body entities. Points to corresponding package @@ -6041,13 +6042,15 @@ package Einfo is -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Import_Pragma (Node35) + -- SPARK_Pragma (Node40) + -- Default_Expressions_Processed (Flag108) -- Has_Invariants (Flag232) -- Has_Nested_Subprogram (Flag282) - -- Is_Machine_Code_Subprogram (Flag137) - -- Is_Pure (Flag44) -- Is_Intrinsic_Subprogram (Flag64) + -- Is_Machine_Code_Subprogram (Flag137) -- Is_Primitive (Flag218) - -- Default_Expressions_Processed (Flag108) + -- Is_Pure (Flag44) + -- SPARK_Pragma_Inherited (Flag265) -- Aren't there more flags and fields? seems like this list should be -- more similar to the E_Function list, which is much longer ??? @@ -6378,6 +6381,7 @@ package Einfo is -- (plus type attributes) -- E_Task_Body + -- Contract (Node34) -- SPARK_Pragma (Node40) -- SPARK_Pragma_Inherited (Flag265) -- (any others??? First/Last Entity, Scope_Depth???) @@ -6396,6 +6400,7 @@ package Einfo is -- Task_Body_Procedure (Node25) -- Storage_Size_Variable (Node26) (base type only) -- Relative_Deadline_Variable (Node28) (base type only) + -- Contract (Node34) -- SPARK_Pragma (Node40) -- SPARK_Aux_Pragma (Node41) -- Delay_Cleanups (Flag114) diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 07003a4dc59..a666ab22b85 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -7105,7 +7105,7 @@ package body Exp_Ch6 is if Nkind (Parent (Subp)) = N_Procedure_Specification and then Null_Present (Parent (Subp)) then - Analyze_Subprogram_Contract (Subp); + Analyze_Entry_Or_Subprogram_Contract (Subp); end if; end Freeze_Subprogram; diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 0d16affb06e..2bee1927c2d 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -3513,6 +3513,37 @@ package body Inline is ("cannot inline & (nested procedure instantiation)?", D, Subp); return True; + + -- Subtype declarations with predicates will generate predicate + -- functions, i.e. nested subprogram bodies, so inlining is not + -- possible. + + elsif Nkind (D) = N_Subtype_Declaration + and then Present (Aspect_Specifications (D)) + then + declare + A : Node_Id; + A_Id : Aspect_Id; + + begin + A := First (Aspect_Specifications (D)); + while Present (A) loop + A_Id := Get_Aspect_Id (Chars (Identifier (A))); + + if A_Id = Aspect_Predicate + or else A_Id = Aspect_Static_Predicate + or else A_Id = Aspect_Dynamic_Predicate + then + Cannot_Inline + ("cannot inline & " + & "(subtype declaration with predicate)?", + D, Subp); + return True; + end if; + + Next (A); + end loop; + end; end if; Next (D); diff --git a/gcc/ada/osint.ads b/gcc/ada/osint.ads index 6347e4d413b..2e6f0904de3 100644 --- a/gcc/ada/osint.ads +++ b/gcc/ada/osint.ads @@ -760,7 +760,7 @@ private -- for this file. This routine merely constructs the name. procedure Write_Info (Info : String); - -- Implement Write_Binder_Info, Write_Debug_Info, and Write_Library_Info + -- Implements Write_Binder_Info, Write_Debug_Info, and Write_Library_Info procedure Write_With_Check (A : Address; N : Integer); -- Writes N bytes from buffer starting at address A to file whose FD is diff --git a/gcc/ada/par-ch9.adb b/gcc/ada/par-ch9.adb index d2aeb5a797a..1137823133e 100644 --- a/gcc/ada/par-ch9.adb +++ b/gcc/ada/par-ch9.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2013, 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- -- @@ -1089,7 +1089,6 @@ package body Ch9 is Resync_Past_Semicolon; Pop_Scope_Stack; -- discard unused entry return Error; - end P_Accept_Statement; ------------------------ @@ -1098,12 +1097,45 @@ package body Ch9 is -- Parsed by P_Expression (4.4) + -------------------------- + -- 9.5.2 Entry Barrier -- + -------------------------- + + -- ENTRY_BARRIER ::= when CONDITION + + -- Error_Recovery: cannot raise Error_Resync + + function P_Entry_Barrier return Node_Id is + Bnode : Node_Id; + + begin + if Token = Tok_When then + Scan; -- past WHEN; + Bnode := P_Expression_No_Right_Paren; + + if Token = Tok_Colon_Equal then + Error_Msg_SC -- CODEFIX + ("|"":="" should be ""="""); + Scan; + Bnode := P_Expression_No_Right_Paren; + end if; + + else + T_When; -- to give error message + Bnode := Error; + end if; + + return Bnode; + end P_Entry_Barrier; + ----------------------- -- 9.5.2 Entry Body -- ----------------------- -- ENTRY_BODY ::= - -- entry DEFINING_IDENTIFIER ENTRY_BODY_FORMAL_PART ENTRY_BARRIER is + -- entry DEFINING_IDENTIFIER ENTRY_BODY_FORMAL_PART + -- [ASPECT_SPECIFICATIONS] ENTRY_BARRIER + -- is -- DECLARATIVE_PART -- begin -- HANDLED_SEQUENCE_OF_STATEMENTS @@ -1114,6 +1146,7 @@ package body Ch9 is -- Error_Recovery: cannot raise Error_Resync function P_Entry_Body return Node_Id is + Dummy_Node : Node_Id; Entry_Node : Node_Id; Formal_Part_Node : Node_Id; Name_Node : Node_Id; @@ -1135,8 +1168,34 @@ package body Ch9 is Formal_Part_Node := P_Entry_Body_Formal_Part; Set_Entry_Body_Formal_Part (Entry_Node, Formal_Part_Node); + -- Ada 2012 (AI12-0169): Aspect specifications may appear on an entry + -- body immediately after the formal part. Do not parse the aspect + -- specifications directly because the "when" of the entry barrier may + -- be interpreted as a misused "with". + + if Token = Tok_With then + P_Aspect_Specifications (Entry_Node, Semicolon => False); + end if; + Set_Condition (Formal_Part_Node, P_Entry_Barrier); + + -- Detect an illegal placement of aspect specifications following the + -- entry barrier. + + -- entry E ... when Barrier with Aspect is + + if Token = Tok_With then + Error_Msg_SC ("aspect specifications must come before entry barrier"); + + -- Consume the illegal aspects to allow for parsing to continue + + Dummy_Node := New_Node (N_Entry_Body, Sloc (Entry_Node)); + P_Aspect_Specifications (Dummy_Node, Semicolon => False); + end if; + + TF_Is; Parse_Decls_Begin_End (Entry_Node); + return Entry_Node; end P_Entry_Body; @@ -1185,38 +1244,6 @@ package body Ch9 is return Fpart_Node; end P_Entry_Body_Formal_Part; - -------------------------- - -- 9.5.2 Entry Barrier -- - -------------------------- - - -- ENTRY_BARRIER ::= when CONDITION - - -- Error_Recovery: cannot raise Error_Resync - - function P_Entry_Barrier return Node_Id is - Bnode : Node_Id; - - begin - if Token = Tok_When then - Scan; -- past WHEN; - Bnode := P_Expression_No_Right_Paren; - - if Token = Tok_Colon_Equal then - Error_Msg_SC -- CODEFIX - ("|"":="" should be ""="""); - Scan; - Bnode := P_Expression_No_Right_Paren; - end if; - - else - T_When; -- to give error message - Bnode := Error; - end if; - - TF_Is; - return Bnode; - end P_Entry_Barrier; - -------------------------------------- -- 9.5.2 Entry Index Specification -- -------------------------------------- diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 009379df824..e08709fd2ac 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1330,7 +1330,7 @@ package body Sem_Attr is if Nkind (Prag) = N_Aspect_Specification then Subp_Decl := Parent (Prag); else - Subp_Decl := Find_Related_Subprogram_Or_Body (Prag); + Subp_Decl := Find_Related_Declaration_Or_Body (Prag); end if; -- The aspect or pragma where the attribute resides should be diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb index c85a9f366d7..b7bf9f4d5c6 100644 --- a/gcc/ada/sem_aux.adb +++ b/gcc/ada/sem_aux.adb @@ -819,8 +819,8 @@ package body Sem_Aux is -- Generic subprogram body elsif Is_Subprogram (S) - and then Nkind (Unit_Declaration_Node (S)) - = N_Generic_Subprogram_Declaration + and then Nkind (Unit_Declaration_Node (S)) = + N_Generic_Subprogram_Declaration then return True; end if; @@ -1649,6 +1649,8 @@ package body Sem_Aux is -- Isn't there some better way to express the following ??? while Nkind (N) /= N_Abstract_Subprogram_Declaration + and then Nkind (N) /= N_Entry_Body + and then Nkind (N) /= N_Entry_Declaration and then Nkind (N) /= N_Formal_Package_Declaration and then Nkind (N) /= N_Function_Instantiation and then Nkind (N) /= N_Generic_Package_Declaration diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 2599228b858..5de074e1f25 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -939,7 +939,7 @@ package body Sem_Ch10 is if Nkind_In (Unit_Node, N_Generic_Subprogram_Declaration, N_Subprogram_Declaration) then - Analyze_Subprogram_Contract (Defining_Entity (Unit_Node)); + Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Unit_Node)); 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 bb4095b0df4..e7d076ae6bb 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -14796,10 +14796,9 @@ package body Sem_Ch12 is 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 pragma Assert (Is_Subprogram_Contract_Annotation (Prag)); - Context := Find_Related_Subprogram_Or_Body (Prag); + Context := Find_Related_Declaration_Or_Body (Prag); end if; -- The use of Original_Node accounts for the case when the diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 2797c6309e5..cf2ba436cb1 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -3474,9 +3474,9 @@ package body Sem_Ch13 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. + -- Body [stub] N has aspects, but they are not properly placed. Emit an + -- error message depending on the aspects involved. Spec_Id denotes the + -- entity of the corresponding spec. -------------------------------- -- Diagnose_Misplaced_Aspects -- @@ -3532,7 +3532,7 @@ package body Sem_Ch13 is else Error_Msg_N - ("aspect specification must appear in subprogram declaration", + ("aspect specification must appear on initial declaration", Asp); end if; end Misplaced_Aspect_Error; @@ -3574,7 +3574,7 @@ package body Sem_Ch13 is else Error_Msg_N - ("aspect specification must appear in subprogram declaration", + ("aspect specification must appear on initial declaration", Asp); end if; @@ -3584,23 +3584,17 @@ package body Sem_Ch13 is -- Local variables - Spec_Id : Entity_Id; + Spec_Id : constant Entity_Id := Unique_Defining_Entity (N); -- 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 + if Spec_Id /= Body_Id and then not Aspects_On_Body_Or_Stub_OK (N) then Diagnose_Misplaced_Aspects (Spec_Id); else Analyze_Aspect_Specifications (N, Body_Id); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 09c72f7a904..e1eadd19d52 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2505,16 +2505,23 @@ package body Sem_Ch3 is Analyze_Object_Contract (Defining_Entity (Decl)); elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, + N_Entry_Declaration, N_Generic_Subprogram_Declaration, N_Subprogram_Declaration) then - Analyze_Subprogram_Contract (Defining_Entity (Decl)); + Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl)); - elsif Nkind (Decl) = N_Subprogram_Body then - Analyze_Subprogram_Body_Contract (Defining_Entity (Decl)); + elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then + Analyze_Entry_Or_Subprogram_Body_Contract + (Defining_Entity (Decl)); elsif Nkind (Decl) = N_Subprogram_Body_Stub then Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); + + elsif Nkind_In (Decl, N_Single_Task_Declaration, + N_Task_Type_Declaration) + then + Analyze_Task_Contract (Defining_Entity (Decl)); end if; Next (Decl); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 98eafd761c8..ec92bf45813 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1385,7 +1385,7 @@ package body Sem_Ch6 is -- have been analyzed. This ensures that any contract-related pragmas -- are available through the N_Contract node of the body. - Analyze_Subprogram_Body_Contract (Body_Id); + Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id); Analyze (Handled_Statement_Sequence (N)); Save_Global_References (Original_Node (N)); @@ -3789,7 +3789,7 @@ package body Sem_Ch6 is -- after the declarations of the body have been processed as pragmas -- are now chained on the contract of the subprogram body. - Analyze_Subprogram_Body_Contract (Body_Id); + Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id); -- If SPARK_Mode for body is not On, disable frontend inlining for this -- subprogram in GNATprove mode, as its body should not be analyzed. diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 3494eb56766..62d72516d4f 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -1213,8 +1213,8 @@ package body Sem_Ch9 is Set_Ekind (Id, E_Entry); end if; - Set_Scope (Id, Current_Scope); Set_Etype (Id, Standard_Void_Type); + Set_Scope (Id, Current_Scope); Set_Accept_Address (Id, New_Elmt_List); -- Set the SPARK_Mode from the current context (may be overwritten later @@ -1223,6 +1223,12 @@ package body Sem_Ch9 is Set_SPARK_Pragma (Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Id); + -- Analyze any aspect specifications that appear on the entry body + + if Has_Aspects (N) then + Analyze_Aspect_Specifications_On_Body_Or_Stub (N); + end if; + E := First_Entity (P_Type); while Present (E) loop if Chars (E) = Chars (Id) @@ -1352,6 +1358,12 @@ package body Sem_Ch9 is Inspect_Deferred_Constant_Completion (Decls); end if; + -- Process the contract of the subprogram body after all declarations + -- have been analyzed. This ensures that any contract-related pragmas + -- are available through the N_Contract node of the body. + + Analyze_Entry_Or_Subprogram_Body_Contract (Id); + if Present (Stats) then Analyze (Stats); end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index b3e90b592e7..cbefd3898a7 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -209,6 +209,12 @@ package body Sem_Prag is -- Do_Checks is set, the routine reports duplicate pragmas. The routine -- returns Empty when reaching the start of the node chain. + function Fix_Msg (Id : Entity_Id; Msg : String) return String; + -- Replace all occurrences of "subprogram" in string Msg with a specific + -- word depending on the Ekind of Id as follows: + -- * When Id is an entry [family], replace with "entry" + -- * When Id is a task type, replace with "task unit" + 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 @@ -386,7 +392,7 @@ package body Sem_Prag is -- Local variables - Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); @@ -465,7 +471,7 @@ package body Sem_Prag is procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is Loc : constant Source_Ptr := Sloc (N); - Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); All_Inputs_Seen : Elist_Id := No_Elist; @@ -1144,8 +1150,8 @@ package body Sem_Prag is Error_Msg_Name_1 := Chars (Spec_Id); SPARK_Msg_NE - ("\& is not part of the input or output set of subprogram %", - Item, Item_Id); + (Fix_Msg (Spec_Id, "\& is not part of the input or output " + & "set of subprogram %"), Item, Item_Id); -- The mode of the item and its role in pragma [Refined_]Depends -- are in conflict. Construct a detailed message explaining the @@ -1638,7 +1644,9 @@ package body Sem_Prag is Restore_Scope := True; Push_Scope (Spec_Id); - if Is_Generic_Subprogram (Spec_Id) then + if Ekind (Spec_Id) = E_Task_Type then + null; + elsif Is_Generic_Subprogram (Spec_Id) then Install_Generic_Formals (Spec_Id); else Install_Formals (Spec_Id); @@ -1772,7 +1780,7 @@ 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); + Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl); @@ -1876,8 +1884,8 @@ 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); + (Fix_Msg (Spec_Id, "global item cannot reference " + & "parameter of subprogram &"), Item, Spec_Id); return; end if; @@ -2096,9 +2104,10 @@ package body Sem_Prag is SPARK_Msg_NE ("global item & cannot have mode In_Out or Output", Item, Item_Id); + SPARK_Msg_NE - ("\item already appears as input of subprogram &", - Item, Context); + (Fix_Msg (Subp_Id, "\item already appears as input of " + & "subprogram &"), Item, Context); -- Stop the traversal once an error has been detected @@ -2257,7 +2266,9 @@ package body Sem_Prag is Restore_Scope := True; Push_Scope (Spec_Id); - if Is_Generic_Subprogram (Spec_Id) then + if Ekind (Spec_Id) = E_Task_Type then + null; + elsif Is_Generic_Subprogram (Spec_Id) then Install_Generic_Formals (Spec_Id); else Install_Formals (Spec_Id); @@ -3351,21 +3362,26 @@ package body Sem_Prag is -- associated with a subprogram declaration or a body that acts as a -- spec. - Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True); + Subp_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True); + + -- Entry + + if Nkind (Subp_Decl) = N_Entry_Declaration then + null; -- Generic subprogram - if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then null; - -- Body acts as spec + -- Subprogram 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 + -- Subprogram body stub acts as spec elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) @@ -3377,6 +3393,11 @@ package body Sem_Prag is elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then null; + -- Task unit + + elsif Nkind (Subp_Decl) = N_Task_Type_Declaration then + null; + else Pragma_Misplaced; return; @@ -3387,6 +3408,16 @@ package body Sem_Prag is Legal := True; Spec_Id := Unique_Defining_Entity (Subp_Decl); + -- When the related context is an entry, it must be a protected entry + -- (SPARK RM 6.1.4(6)). + + if Is_Entry_Declaration (Spec_Id) + and then Ekind (Scope (Spec_Id)) /= E_Protected_Type + then + Pragma_Misplaced; + return; + end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -3686,7 +3717,8 @@ package body Sem_Prag is -- Ensure the proper placement of the pragma Subp_Decl := - Find_Related_Subprogram_Or_Body (N, Do_Checks => not Duplicates_OK); + Find_Related_Declaration_Or_Body + (N, Do_Checks => not Duplicates_OK); -- When a pre/postcondition pragma applies to an abstract subprogram, -- its original form must be an aspect with 'Class. @@ -3759,10 +3791,11 @@ package body Sem_Prag is Mark_Pragma_As_Ghost (N, Subp_Id); - -- Fully analyze the pragma when it appears inside a subprogram - -- body because it cannot benefit from forward references. + -- Fully analyze the pragma when it appears inside an entry or + -- subprogram body because it cannot benefit from forward references. - if Nkind_In (Subp_Decl, N_Subprogram_Body, + if Nkind_In (Subp_Decl, N_Entry_Body, + N_Subprogram_Body, N_Subprogram_Body_Stub) then -- The legality checks of pragmas Precondition and Postcondition @@ -3801,23 +3834,36 @@ package body Sem_Prag is -- Verify the placement of the pragma and check for duplicates. The -- pragma must apply to a subprogram body [stub]. - Body_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True); + Body_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True); + + -- Entry body + + if Nkind (Body_Decl) = N_Entry_Body then + null; + + -- Subprogram body - -- Extract the entities of the spec and body + elsif Nkind (Body_Decl) = N_Subprogram_Body then + null; - if Nkind (Body_Decl) = N_Subprogram_Body then - Body_Id := Defining_Entity (Body_Decl); - Spec_Id := Corresponding_Spec (Body_Decl); + -- Subprogram body stub elsif Nkind (Body_Decl) = N_Subprogram_Body_Stub then - Body_Id := Defining_Entity (Body_Decl); - Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); + null; + + -- Task body + + elsif Nkind (Body_Decl) = N_Task_Body then + null; else Pragma_Misplaced; return; end if; + Body_Id := Defining_Entity (Body_Decl); + Spec_Id := Unique_Defining_Entity (Body_Decl); + -- The pragma must apply to the second declaration of a subprogram. -- In other words, the body [stub] cannot acts as a spec. @@ -3839,10 +3885,17 @@ package body Sem_Prag is Spec_Decl := Unit_Declaration_Node (Spec_Id); + -- The proper context of a entry declaration is the declaration of + -- the enclosing synchronized type. + + if Nkind (Spec_Decl) = N_Entry_Declaration then + Spec_Decl := Parent (Parent (Spec_Decl)); + end if; + if Nkind (Parent (Spec_Decl)) /= N_Package_Specification then Error_Pragma - ("pragma % must apply to the body of a subprogram declared in a " - & "package specification"); + (Fix_Msg (Spec_Id, "pragma % must apply to the body of " + & "subprogram declared in a package specification")); return; end if; @@ -12275,7 +12328,7 @@ package body Sem_Prag is -- as a spec. Subp_Decl := - Find_Related_Subprogram_Or_Body (N, Do_Checks => True); + Find_Related_Declaration_Or_Body (N, Do_Checks => True); -- Generic subprogram @@ -12319,10 +12372,12 @@ package body Sem_Prag is Mark_Pragma_As_Ghost (N, Spec_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. + -- Fully analyze the pragma when it appears inside an entry + -- or subprogram body because it cannot benefit from forward + -- references. - if Nkind_In (Subp_Decl, N_Subprogram_Body, + if Nkind_In (Subp_Decl, N_Entry_Body, + N_Subprogram_Body, N_Subprogram_Body_Stub) then -- The legality checks of pragma Contract_Cases are affected by @@ -13046,10 +13101,12 @@ package body Sem_Prag is Add_Contract_Item (N, Spec_Id); - -- Fully analyze the pragma when it appears inside a subprogram - -- body because it cannot benefit from forward references. + -- Fully analyze the pragma when it appears inside an entry + -- or subprogram body because it cannot benefit from forward + -- references. - if Nkind_In (Subp_Decl, N_Subprogram_Body, + if Nkind_In (Subp_Decl, N_Entry_Body, + N_Subprogram_Body, N_Subprogram_Body_Stub) then -- The legality checks of pragmas Depends and Global are @@ -13993,7 +14050,7 @@ package body Sem_Prag is Check_At_Most_N_Arguments (1); Subp_Decl := - Find_Related_Subprogram_Or_Body (N, Do_Checks => True); + Find_Related_Declaration_Or_Body (N, Do_Checks => True); -- Generic subprogram declaration @@ -14564,10 +14621,12 @@ package body Sem_Prag is Add_Contract_Item (N, Spec_Id); - -- Fully analyze the pragma when it appears inside a subprogram - -- body because it cannot benefit from forward references. + -- Fully analyze the pragma when it appears inside an entry + -- or subprogram body because it cannot benefit from forward + -- references. - if Nkind_In (Subp_Decl, N_Subprogram_Body, + if Nkind_In (Subp_Decl, N_Entry_Body, + N_Subprogram_Body, N_Subprogram_Body_Stub) then -- The legality checks of pragmas Depends and Global are @@ -20991,7 +21050,7 @@ package body Sem_Prag is return; end if; - Subp_Decl := Find_Related_Subprogram_Or_Body (N); + Subp_Decl := Find_Related_Declaration_Or_Body (N); -- Find the enclosing context @@ -21067,10 +21126,12 @@ package body Sem_Prag is Check_Distinct_Name (Subp_Id); - -- Fully analyze the pragma when it appears inside a subprogram - -- body because it cannot benefit from forward references. + -- Fully analyze the pragma when it appears inside an entry + -- or subprogram body because it cannot benefit from forward + -- references. - if Nkind_In (Subp_Decl, N_Subprogram_Body, + if Nkind_In (Subp_Decl, N_Entry_Body, + N_Subprogram_Body, N_Subprogram_Body_Stub) then -- The legality checks of pragma Test_Case are affected by the @@ -21910,7 +21971,7 @@ package body Sem_Prag is Check_At_Most_N_Arguments (1); Subp_Decl := - Find_Related_Subprogram_Or_Body (N, Do_Checks => True); + Find_Related_Declaration_Or_Body (N, Do_Checks => True); -- Generic subprogram @@ -22575,7 +22636,7 @@ package body Sem_Prag is -- Local variables - Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); @@ -22773,9 +22834,9 @@ package body Sem_Prag is Item_Id := Available_View (Entity_Of (Item)); - return Ekind (Item_Id) = E_Abstract_State - and then Has_Null_Refinement (Item_Id); - + return + Ekind (Item_Id) = E_Abstract_State + and then Has_Null_Refinement (Item_Id); else return False; end if; @@ -23059,8 +23120,8 @@ package body Sem_Prag is if not Clause_Matched then SPARK_Msg_NE - ("dependence clause of subprogram & has no matching refinement " - & "in body", Dep_Clause, Spec_Id); + (Fix_Msg (Spec_Id, "dependence clause of subprogram & has no " + & "matching refinement in body"), Dep_Clause, Spec_Id); end if; end Check_Dependency_Clause; @@ -23377,7 +23438,7 @@ package body Sem_Prag is -- Local variables - Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Body_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); Errors : constant Nat := Serious_Errors_Detected; Clause : Node_Id; @@ -23394,12 +23455,7 @@ package body Sem_Prag is return; end if; - 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; - + Spec_Id := Unique_Defining_Entity (Body_Decl); Depends := Get_Pragma (Spec_Id, Pragma_Depends); -- Subprogram declarations lacks pragma Depends. Refined_Depends is @@ -23407,8 +23463,8 @@ package body Sem_Prag is if No (Depends) then SPARK_Msg_NE - ("useless refinement, declaration of subprogram & lacks aspect or " - & "pragma Depends", N, Spec_Id); + (Fix_Msg (Spec_Id, "useless refinement, declaration of subprogram " + & "& lacks aspect or pragma Depends"), N, Spec_Id); goto Leave; end if; @@ -23421,8 +23477,8 @@ package body Sem_Prag is if Nkind (Deps) = N_Null then SPARK_Msg_NE - ("useless refinement, subprogram & does not depend on abstract " - & "state with visible refinement", N, Spec_Id); + (Fix_Msg (Spec_Id, "useless refinement, subprogram & does not " + & "depend on abstract state with visible refinement"), N, Spec_Id); goto Leave; end if; @@ -24355,7 +24411,7 @@ package body Sem_Prag is -- Local variables - Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Body_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); Errors : constant Nat := Serious_Errors_Detected; Items : Node_Id; @@ -24368,22 +24424,17 @@ package body Sem_Prag is return; end if; - 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; - - Global := Get_Pragma (Spec_Id, Pragma_Global); - Items := Expression (Get_Argument (N, Spec_Id)); + Spec_Id := Unique_Defining_Entity (Body_Decl); + 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. if No (Global) then SPARK_Msg_NE - ("useless refinement, declaration of subprogram & lacks aspect or " - & "pragma Global", N, Spec_Id); + (Fix_Msg (Spec_Id, "useless refinement, declaration of subprogram " + & "& lacks aspect or pragma Global"), N, Spec_Id); goto Leave; end if; @@ -24415,8 +24466,9 @@ package body Sem_Prag is 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); + (Fix_Msg (Spec_Id, "useless refinement, subprogram & does not " + & "depend on abstract state with visible refinement"), + N, Spec_Id); goto Leave; -- The global refinement of inputs and outputs cannot be null when @@ -24432,8 +24484,8 @@ package body Sem_Prag is and then not Has_Null_State then SPARK_Msg_NE - ("refinement cannot be null, subprogram & has global items", - N, Spec_Id); + (Fix_Msg (Spec_Id, "refinement cannot be null, subprogram & has " + & "global items"), N, Spec_Id); goto Leave; end if; end if; @@ -25292,7 +25344,7 @@ package body Sem_Prag is ------------------------------------ procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is - Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id); @@ -26326,10 +26378,13 @@ package body Sem_Prag is Next_Entity (Formal); end loop; - -- When processing a subprogram body, look for pragmas Refined_Depends - -- and Refined_Global as they specify the inputs and outputs. + -- When processing an entry, subprogram or task body, look for pragmas + -- Refined_Depends and Refined_Global as they specify the inputs and + -- outputs. - if Ekind (Subp_Id) = E_Subprogram_Body then + if Is_Entry_Body (Subp_Id) + or else Ekind_In (Subp_Id, E_Subprogram_Body, E_Task_Body) + then Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends); Global := Get_Pragma (Subp_Id, Pragma_Refined_Global); @@ -26469,99 +26524,11 @@ package body Sem_Prag is return Empty; end Find_Related_Context; - ---------------------------------- - -- Find_Related_Package_Or_Body -- - ---------------------------------- - - function Find_Related_Package_Or_Body - (Prag : Node_Id; - Do_Checks : Boolean := False) return Node_Id - is - Context : constant Node_Id := Parent (Prag); - Prag_Nam : constant Name_Id := Pragma_Name (Prag); - Stmt : Node_Id; - - begin - Stmt := Prev (Prag); - while Present (Stmt) loop - - -- Skip prior pragmas, but check for duplicates - - if Nkind (Stmt) = N_Pragma then - if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then - Duplication_Error - (Prag => Prag, - Prev => Stmt); - end if; - - -- Skip internally generated code - - elsif not Comes_From_Source (Stmt) then - if Nkind (Stmt) = N_Subprogram_Declaration then - - -- The subprogram declaration is an internally generated spec - -- for an expression function. - - if Nkind (Original_Node (Stmt)) = N_Expression_Function then - return Stmt; - - -- The subprogram is actually an instance housed within an - -- anonymous wrapper package. - - elsif Present (Generic_Parent (Specification (Stmt))) then - return Stmt; - end if; - end if; - - -- Return the current source construct which is illegal - - else - return Stmt; - end if; - - Prev (Stmt); - end loop; - - -- If we fall through, then the pragma was either the first declaration - -- or it was preceded by other pragmas and no source constructs. - - -- The pragma is associated with a package. The immediate context in - -- this case is the specification of the package. - - if Nkind (Context) = N_Package_Specification then - return Parent (Context); - - -- The pragma appears in the declarations of a package body - - elsif Nkind (Context) = N_Package_Body then - return Context; - - -- The pragma appears in the statements of a package body - - elsif Nkind (Context) = N_Handled_Sequence_Of_Statements - and then Nkind (Parent (Context)) = N_Package_Body - then - return Parent (Context); - - -- The pragma is a byproduct of aspect expansion, return the related - -- context of the original aspect. This case has a lower priority as - -- the above circuitry pinpoints precisely the related context. - - elsif Present (Corresponding_Aspect (Prag)) then - return Parent (Corresponding_Aspect (Prag)); - - -- No candidate packge [body] found - - else - return Empty; - end if; - end Find_Related_Package_Or_Body; - - ------------------------------------- - -- Find_Related_Subprogram_Or_Body -- - ------------------------------------- + -------------------------------------- + -- Find_Related_Declaration_Or_Body -- + -------------------------------------- - function Find_Related_Subprogram_Or_Body + function Find_Related_Declaration_Or_Body (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id is @@ -26604,7 +26571,7 @@ package body Sem_Prag is Name_Refined_Post); -- Refinement pragmas must be associated with a subprogram body [stub] - -- Start of processing for Find_Related_Subprogram_Or_Body + -- Start of processing for Find_Related_Declaration_Or_Body begin Stmt := Prev (Prag); @@ -26660,6 +26627,14 @@ package body Sem_Prag is elsif Present (Generic_Parent (Specification (Stmt))) then return Stmt; end if; + + -- The pragma applies to a single task declaration rewritten as a + -- task type. + + elsif Nkind (Stmt) = N_Task_Type_Declaration + and then Nkind (Original_Node (Stmt)) = N_Single_Task_Declaration + then + return Stmt; end if; -- Return the current construct which is either a subprogram body, @@ -26680,6 +26655,11 @@ package body Sem_Prag is if Nkind (Context) = N_Compilation_Unit_Aux then return Unit (Parent (Context)); + -- The pragma appears inside the declarations of an entry body + + elsif Nkind (Context) = N_Entry_Body then + return Context; + -- The pragma appears inside the statements of a subprogram body. This -- placement is the result of subprogram contract expansion. @@ -26691,6 +26671,11 @@ package body Sem_Prag is elsif Nkind (Context) = N_Subprogram_Body then return Context; + -- The pragma appears inside the declarative part of a task body + + elsif Nkind (Context) = N_Task_Body then + return Context; + -- The pragma is a byproduct of aspect expansion, return the related -- context of the original aspect. This case has a lower priority as -- the above circuitry pinpoints precisely the related context. @@ -26703,7 +26688,145 @@ package body Sem_Prag is else return Empty; end if; - end Find_Related_Subprogram_Or_Body; + end Find_Related_Declaration_Or_Body; + + ---------------------------------- + -- Find_Related_Package_Or_Body -- + ---------------------------------- + + function Find_Related_Package_Or_Body + (Prag : Node_Id; + Do_Checks : Boolean := False) return Node_Id + is + Context : constant Node_Id := Parent (Prag); + Prag_Nam : constant Name_Id := Pragma_Name (Prag); + Stmt : Node_Id; + + begin + Stmt := Prev (Prag); + while Present (Stmt) loop + + -- Skip prior pragmas, but check for duplicates + + if Nkind (Stmt) = N_Pragma then + if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then + Duplication_Error + (Prag => Prag, + Prev => Stmt); + end if; + + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + if Nkind (Stmt) = N_Subprogram_Declaration then + + -- The subprogram declaration is an internally generated spec + -- for an expression function. + + if Nkind (Original_Node (Stmt)) = N_Expression_Function then + return Stmt; + + -- The subprogram is actually an instance housed within an + -- anonymous wrapper package. + + elsif Present (Generic_Parent (Specification (Stmt))) then + return Stmt; + end if; + end if; + + -- Return the current source construct which is illegal + + else + return Stmt; + end if; + + Prev (Stmt); + end loop; + + -- If we fall through, then the pragma was either the first declaration + -- or it was preceded by other pragmas and no source constructs. + + -- The pragma is associated with a package. The immediate context in + -- this case is the specification of the package. + + if Nkind (Context) = N_Package_Specification then + return Parent (Context); + + -- The pragma appears in the declarations of a package body + + elsif Nkind (Context) = N_Package_Body then + return Context; + + -- The pragma appears in the statements of a package body + + elsif Nkind (Context) = N_Handled_Sequence_Of_Statements + and then Nkind (Parent (Context)) = N_Package_Body + then + return Parent (Context); + + -- The pragma is a byproduct of aspect expansion, return the related + -- context of the original aspect. This case has a lower priority as + -- the above circuitry pinpoints precisely the related context. + + elsif Present (Corresponding_Aspect (Prag)) then + return Parent (Corresponding_Aspect (Prag)); + + -- No candidate packge [body] found + + else + return Empty; + end if; + end Find_Related_Package_Or_Body; + + ------------- + -- Fix_Msg -- + ------------- + + function Fix_Msg (Id : Entity_Id; Msg : String) return String is + Msg_Last : constant Natural := Msg'Last; + Msg_Index : Natural; + Res : String (Msg'Range) := (others => ' '); + Res_Index : Natural; + + begin + -- Copy all characters from the input message Msg to result Res with + -- suitable replacements. + + Msg_Index := Msg'First; + Res_Index := Res'First; + while Msg_Index <= Msg_Last loop + + -- Replace "subprogram" with a different word + + if Msg_Index <= Msg_Last - 10 + and then Msg (Msg_Index .. Msg_Index + 9) = "subprogram" + then + if Ekind_In (Id, E_Entry, E_Entry_Family) then + Res (Res_Index .. Res_Index + 4) := "entry"; + Res_Index := Res_Index + 5; + + elsif Ekind_In (Id, E_Task_Body, E_Task_Type) then + Res (Res_Index .. Res_Index + 8) := "task unit"; + Res_Index := Res_Index + 9; + + else + Res (Res_Index .. Res_Index + 9) := "subprogram"; + Res_Index := Res_Index + 10; + end if; + + Msg_Index := Msg_Index + 10; + + -- Otherwise copy the character + + else + Res (Res_Index) := Msg (Msg_Index); + Msg_Index := Msg_Index + 1; + Res_Index := Res_Index + 1; + end if; + end loop; + + return Res (Res'First .. Res_Index - 1); + end Fix_Msg; ------------------ -- Get_Argument -- diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 45a3ebcc2ea..e8c647e4dda 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -327,22 +327,29 @@ package Sem_Prag is -- the pragma is illegal. If flag Do_Checks is set, the routine reports -- duplicate pragmas. - function Find_Related_Subprogram_Or_Body + function Find_Related_Declaration_Or_Body (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; - -- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global, - -- Refined_Depends, Refined_Global and Refined_Post and attribute 'Result. - -- Find the declaration of the related subprogram [body or stub] subject - -- to pragma Prag. If flag Do_Checks is set, the routine reports duplicate - -- pragmas and detects improper use of refinement pragmas in stand alone - -- expression functions. The returned value depends on the related pragma - -- as follows: - -- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding - -- N_Subprogram_Declaration node or if the pragma applies to a stand - -- alone body, the N_Subprogram_Body node or Empty if illegal. - -- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield - -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if - -- illegal. + -- Subsidiary to the analysis of pragmas + -- Contract_Cases + -- Depends + -- Extensions_Visible + -- Global + -- Post + -- Post_Class + -- Postcondition + -- Pre + -- Pre_Class + -- Precondition + -- Refined_Depends + -- Refined_Global + -- Refined_Post + -- Test_Case + -- as well as attributes 'Old and 'Result. Find the declaration of the + -- related entry, subprogram or task type [body] subject to pragma Prag. + -- If flag Do_Checks is set, the routine reports duplicate pragmas and + -- detects improper use of refinement pragmas in stand alone expression + -- functions. function Get_Argument (Prag : Node_Id; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 313591add7a..de8472af9a4 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -11444,6 +11444,28 @@ package body Sem_Util is end if; end Is_Effectively_Volatile_Object; + ------------------- + -- Is_Entry_Body -- + ------------------- + + function Is_Entry_Body (Id : Entity_Id) return Boolean is + begin + return + Ekind_In (Id, E_Entry, E_Entry_Family) + and then Nkind (Unit_Declaration_Node (Id)) = N_Entry_Body; + end Is_Entry_Body; + + -------------------------- + -- Is_Entry_Declaration -- + -------------------------- + + function Is_Entry_Declaration (Id : Entity_Id) return Boolean is + begin + return + Ekind_In (Id, E_Entry, E_Entry_Family) + and then Nkind (Unit_Declaration_Node (Id)) = N_Entry_Declaration; + end Is_Entry_Declaration; + ---------------------------- -- Is_Expression_Function -- ---------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 2d5cb5ef90a..867aa00dbb0 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1283,6 +1283,12 @@ package Sem_Util is -- Determine whether an arbitrary node denotes an effectively volatile -- object (SPARK RM 7.1.2). + function Is_Entry_Body (Id : Entity_Id) return Boolean; + -- Determine whether entity Id is the body entity of an entry [family] + + function Is_Entry_Declaration (Id : Entity_Id) return Boolean; + -- Determine whether entity Id is the spec entity of an entry [family] + function Is_Expression_Function (Subp : Entity_Id) return Boolean; -- Predicate to determine whether a scope entity comes from a rewritten -- expression function call, and should be inlined unconditionally. Also -- 2.30.2