From 877a5a124a918f82f808c27b8cd64b5bd07f844f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 26 Oct 2015 11:57:17 +0100 Subject: [PATCH] [multiple changes] 2015-10-26 Claire Dross * sem_aux.ads (Number_Components): Can return 0 when called on an empty record. 2015-10-26 Hristian Kirtchev * contracts.adb (Analyze_Subprogram_Body_Contract): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. * einfo.adb SPARK_Pragma and SPARK_Aux_Pragma are now Node40 and Node41 respectively. (SPARK_Aux_Pragma): Update the assertion and node querry. (SPARK_Aux_Pragma_Inherited): Update the assertion and node query. (SPARK_Pragma): Update the assertion and node query. (SPARK_Pragma_Inherited): Update the assertion and node query. (Set_SPARK_Aux_Pragma): Update the assertion and node setting. (Set_SPARK_Aux_Pragma_Inherited): Update the assertion and node setting. (Set_SPARK_Pragma): Update the assertion and node setting. (Set_SPARK_Pragma_Inherited): Update the assertion and node setting. (Write_Field32_Name): Remove the output for SPARK_Pragma. (Write_Field33_Name): Remove the output for SPARK_Aux_Pragma. (Write_Field40_Name): Add output for SPARK_Pragma. (Write_Field41_Name): Add output for SPARK_Aux_Pragma. * einfo.ads Rewrite the documentation on attributes SPARK_Pragma, SPARK_Aux_Pragma, SPARK_Pragma_Inherited and SPARK_Aux_Pragma_Inherited. Update their uses in nodes. * exp_ch4.adb (Create_Anonymous_Master): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. * exp_ch9.adb (Expand_Entry_Declaration): Mark the barrier function as such. (Expand_N_Task_Body): Mark the task body as such. (Expand_N_Task_Type_Declaration): Mark the task body as such. * exp_unst.adb (Visit_Node): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. * sem_attr.adb (Analyze_Attribute_Old_Result): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Entry barrier functions do not inherit the SPARK_Mode from the context. (Build_Subprogram_Declaration): The matching spec is now marked as a source construct to mimic the original stand alone body. * sem_ch7.adb (Analyze_Package_Body_Helper): Code cleanup. * sem_ch9.adb Add with and use clauses for Contracts. (Analyze_Entry_Body): An entry body freezes the contract of the nearest enclosing package body. The entry body now inherits the SPARK_Mode from the context. (Analyze_Entry_Declaration): A protected entry declaration now inherits the SPARK_Mode from the context. (Analyze_Protected_Body): A protected body freezes the contract of the nearest enclosing package body. Set the Etype of a protected body as this is neede for proper aspect analysis. Protected bodies can now carry meaningful aspects and those are now analyzed. (Analyze_Protected_Type_Declaration): A protected type now inherits the SPARK_Mode from the context. (Analyze_Task_Body): A task body freezes the contract of the nearest enclosing package body. Set the Etype of a task body as this is needed for proper aspect analysis. A task body now inherits the SPARK_Mode from the context. Task bodies can now carry meaningful aspects and those are now analyzed. (Analyze_Task_Type_Declaration): A task type declaration now inherits the SPARK_Mode of from the context. * sem_ch10.adb (Analyze_Protected_Body_Stub): Protected body stubs can now carry meaningful aspects. (Analyze_Task_Body_Stub): Task body stubs can now carry meaningful aspects. * sem_ch13.adb (Analyze_Aspect_Specifications): Aspects SPARK_Mode Warnings now use routine Insert_Pragma as means of insertion into the tree. (Insert_After_SPARK_Mode): Clean up documentation. (Insert_Pragma): Clean up documentation. The routine is now capable of operating on synchronized units. * sem_prag.adb (Add_Entity_To_Name_Buffer): New routine. (Analyze_Contract_Cases_In_Decl_Part): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. (Analyze_Depends_Global): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. (Analyze_Depends_In_Decl_Part): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. (Analyze_Global_In_Decl_Part): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. (Analyze_Pragma): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. Update the detection of an illegal pragma Ghost when it applies to a task or protected unit. Reimplement the handling of pragma SPARK_Mode. (Analyze_Pre_Post_Condition_In_Decl_Part): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. (Analyze_Test_Case_In_Decl_Part): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. (Check_Library_Level_Entity): Update the comment on usage. Reimplemented to offer a more specialized errror context. (Check_Pragma_Conformance): Update profile and comment on usage. Handle error message output on single protected or task units. (Collect_Subprogram_Inputs_Outputs): Use Unique_Defining_Entity instead of Corresponding_Spec_Of. (Process_Body): New routine. (Process_Overloadable): New routine. (Process_Private_Part): New routine. (Process_Statement_Part): New routine. (Process_Visible_Part): New routine. (Set_SPARK_Context): New routine. (Set_SPARK_Flags): Removed. * sem_util.adb (Corresponding_Spec_Of): Removed. (Unique_Entity): Reimplemented to handle many more cases. * sem_util.ads (Corresponding_Spec_Of): Removed. (Unique_Defining_Entity): Update the comment on usage. * sinfo.ads (Is_Entry_Barrier_Function): Update the assertion. (Is_Task_Body_Procedure): New routine. (Set_Is_Entry_Barrier_Function): Update the assertion. (Set_Is_Task_Body_Procedure): New routine. * sinfo.adb Update the documentation of attribute Is_Entry_Barrier_Function along with use in nodes. Add new attribute Is_Task_Body_Procedure along with use in nodes. (Is_Task_Body_Procedure): New routine along with pragma Inline. (Set_Is_Task_Body_Procedure): New routine along with pragma Inline. From-SVN: r229328 --- gcc/ada/ChangeLog | 116 +++++++++ gcc/ada/contracts.adb | 2 +- gcc/ada/einfo.adb | 131 ++++++---- gcc/ada/einfo.ads | 85 ++++--- gcc/ada/exp_ch4.adb | 2 +- gcc/ada/exp_ch9.adb | 155 ++++++------ gcc/ada/exp_unst.adb | 2 +- gcc/ada/sem_attr.adb | 2 +- gcc/ada/sem_aux.adb | 2 +- gcc/ada/sem_aux.ads | 2 +- gcc/ada/sem_ch10.adb | 24 +- gcc/ada/sem_ch13.adb | 224 ++++++++++------- gcc/ada/sem_ch6.adb | 32 ++- gcc/ada/sem_ch7.adb | 12 +- gcc/ada/sem_ch9.adb | 185 +++++++++------ gcc/ada/sem_prag.adb | 647 ++++++++++++++++++++++++++++++++++---------------- gcc/ada/sem_util.adb | 128 +++++----- gcc/ada/sem_util.ads | 17 +- gcc/ada/sinfo.adb | 24 +- gcc/ada/sinfo.ads | 25 +- 20 files changed, 1173 insertions(+), 644 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1e7dfdb..9b61998 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,119 @@ +2015-10-26 Claire Dross + + * sem_aux.ads (Number_Components): Can return 0 when called on + an empty record. + +2015-10-26 Hristian Kirtchev + + * contracts.adb (Analyze_Subprogram_Body_Contract): Use + Unique_Defining_Entity instead of Corresponding_Spec_Of. + * einfo.adb SPARK_Pragma and SPARK_Aux_Pragma are now Node40 and + Node41 respectively. + (SPARK_Aux_Pragma): Update the assertion and node querry. + (SPARK_Aux_Pragma_Inherited): Update the assertion and node query. + (SPARK_Pragma): Update the assertion and node query. + (SPARK_Pragma_Inherited): Update the assertion and node query. + (Set_SPARK_Aux_Pragma): Update the assertion and node setting. + (Set_SPARK_Aux_Pragma_Inherited): Update the assertion and node setting. + (Set_SPARK_Pragma): Update the assertion and node setting. + (Set_SPARK_Pragma_Inherited): Update the assertion and node setting. + (Write_Field32_Name): Remove the output for SPARK_Pragma. + (Write_Field33_Name): Remove the output for SPARK_Aux_Pragma. + (Write_Field40_Name): Add output for SPARK_Pragma. + (Write_Field41_Name): Add output for SPARK_Aux_Pragma. + * einfo.ads Rewrite the documentation on attributes + SPARK_Pragma, SPARK_Aux_Pragma, SPARK_Pragma_Inherited and + SPARK_Aux_Pragma_Inherited. Update their uses in nodes. + * exp_ch4.adb (Create_Anonymous_Master): Use + Unique_Defining_Entity instead of Corresponding_Spec_Of. + * exp_ch9.adb (Expand_Entry_Declaration): Mark the barrier + function as such. + (Expand_N_Task_Body): Mark the task body as such. + (Expand_N_Task_Type_Declaration): Mark the task body as such. + * exp_unst.adb (Visit_Node): Use Unique_Defining_Entity instead + of Corresponding_Spec_Of. + * sem_attr.adb (Analyze_Attribute_Old_Result): Use + Unique_Defining_Entity instead of Corresponding_Spec_Of. + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Entry barrier + functions do not inherit the SPARK_Mode from the context. + (Build_Subprogram_Declaration): The matching spec is now marked + as a source construct to mimic the original stand alone body. + * sem_ch7.adb (Analyze_Package_Body_Helper): Code cleanup. + * sem_ch9.adb Add with and use clauses for Contracts. + (Analyze_Entry_Body): An entry body freezes the contract of + the nearest enclosing package body. The entry body now inherits + the SPARK_Mode from the context. + (Analyze_Entry_Declaration): A protected entry declaration now inherits + the SPARK_Mode from the context. + (Analyze_Protected_Body): A protected body freezes + the contract of the nearest enclosing package body. Set the + Etype of a protected body as this is neede for proper aspect + analysis. Protected bodies can now carry meaningful aspects and + those are now analyzed. + (Analyze_Protected_Type_Declaration): A protected type now inherits the + SPARK_Mode from the context. + (Analyze_Task_Body): A task body freezes the contract of the + nearest enclosing package body. Set the Etype of a task body + as this is needed for proper aspect analysis. A task body + now inherits the SPARK_Mode from the context. Task bodies + can now carry meaningful aspects and those are now analyzed. + (Analyze_Task_Type_Declaration): A task type declaration now + inherits the SPARK_Mode of from the context. + * sem_ch10.adb (Analyze_Protected_Body_Stub): Protected body + stubs can now carry meaningful aspects. + (Analyze_Task_Body_Stub): Task body stubs can now carry meaningful + aspects. + * sem_ch13.adb (Analyze_Aspect_Specifications): Aspects SPARK_Mode + Warnings now use routine Insert_Pragma as means of insertion into + the tree. + (Insert_After_SPARK_Mode): Clean up documentation. + (Insert_Pragma): Clean up documentation. The routine is now + capable of operating on synchronized units. + * sem_prag.adb (Add_Entity_To_Name_Buffer): New routine. + (Analyze_Contract_Cases_In_Decl_Part): Use + Unique_Defining_Entity instead of Corresponding_Spec_Of. + (Analyze_Depends_Global): Use Unique_Defining_Entity instead + of Corresponding_Spec_Of. + (Analyze_Depends_In_Decl_Part): Use Unique_Defining_Entity instead of + Corresponding_Spec_Of. + (Analyze_Global_In_Decl_Part): Use Unique_Defining_Entity instead of + Corresponding_Spec_Of. + (Analyze_Pragma): Use Unique_Defining_Entity instead of + Corresponding_Spec_Of. + Update the detection of an illegal pragma Ghost when it applies + to a task or protected unit. Reimplement the handling of + pragma SPARK_Mode. + (Analyze_Pre_Post_Condition_In_Decl_Part): Use Unique_Defining_Entity + instead of Corresponding_Spec_Of. + (Analyze_Test_Case_In_Decl_Part): Use Unique_Defining_Entity instead of + Corresponding_Spec_Of. + (Check_Library_Level_Entity): Update the comment on usage. + Reimplemented to offer a more specialized errror context. + (Check_Pragma_Conformance): Update profile and comment on usage. + Handle error message output on single protected or task units. + (Collect_Subprogram_Inputs_Outputs): Use Unique_Defining_Entity + instead of Corresponding_Spec_Of. + (Process_Body): New routine. + (Process_Overloadable): New routine. + (Process_Private_Part): New routine. + (Process_Statement_Part): New routine. + (Process_Visible_Part): New routine. + (Set_SPARK_Context): New routine. + (Set_SPARK_Flags): Removed. + * sem_util.adb (Corresponding_Spec_Of): Removed. + (Unique_Entity): Reimplemented to handle many more cases. + * sem_util.ads (Corresponding_Spec_Of): Removed. + (Unique_Defining_Entity): Update the comment on usage. + * sinfo.ads (Is_Entry_Barrier_Function): Update the assertion. + (Is_Task_Body_Procedure): New routine. + (Set_Is_Entry_Barrier_Function): Update the assertion. + (Set_Is_Task_Body_Procedure): New routine. + * sinfo.adb Update the documentation of attribute + Is_Entry_Barrier_Function along with use in nodes. Add new + attribute Is_Task_Body_Procedure along with use in nodes. + (Is_Task_Body_Procedure): New routine along with pragma Inline. + (Set_Is_Task_Body_Procedure): New routine along with pragma Inline. + 2015-10-26 Gary Dismukes * sem_ch13.adb: Minor reformatting. diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index e8409b5..fa678bf 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -624,7 +624,7 @@ package body Contracts 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); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Body_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); Mode : SPARK_Mode_Type; Prag : Node_Id; Prag_Nam : Name_Id; diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 5cca0fa..08072f2 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -255,11 +255,9 @@ package body Einfo is -- Activation_Record_Component Node31 -- Encapsulating_State Node32 - -- SPARK_Pragma Node32 -- No_Tagged_Streams_Pragma Node32 -- Linker_Section_Pragma Node33 - -- SPARK_Aux_Pragma Node33 -- Contract Node34 @@ -267,12 +265,13 @@ package body Einfo is -- Anonymous_Master Node36 - -- (Class_Wide_Preconds) List38 + -- Class_Wide_Preconds List38 - -- (Class_Wide_Postconds) List39 + -- Class_Wide_Postconds List39 - -- (unused) Node40 - -- (unused) Node41 + -- SPARK_Pragma Node40 + + -- SPARK_Aux_Pragma Node41 --------------------------------------------- -- Usage of Flags in Defining Entity Nodes -- @@ -3113,8 +3112,11 @@ package body Einfo is pragma Assert (Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); - return Node33 (Id); + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Type, -- synchronized variants + E_Task_Type)); + return Node41 (Id); end SPARK_Aux_Pragma; function SPARK_Aux_Pragma_Inherited (Id : E) return B is @@ -3122,14 +3124,19 @@ package body Einfo is pragma Assert (Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Type, -- synchronized variants + E_Task_Type)); return Flag266 (Id); end SPARK_Aux_Pragma_Inherited; function SPARK_Pragma (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Function, -- subprogram variants + (Ekind_In (Id, E_Entry, -- overloadable variants + E_Entry_Family, + E_Function, E_Generic_Function, E_Generic_Procedure, E_Procedure, @@ -3137,14 +3144,21 @@ package body Einfo is or else Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); - return Node32 (Id); + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Body, -- synchronized variants + E_Protected_Type, + E_Task_Body, + E_Task_Type)); + return Node40 (Id); end SPARK_Pragma; function SPARK_Pragma_Inherited (Id : E) return B is begin pragma Assert - (Ekind_In (Id, E_Function, -- subprogram variants + (Ekind_In (Id, E_Entry, -- overloadable variants + E_Entry_Family, + E_Function, E_Generic_Function, E_Generic_Procedure, E_Procedure, @@ -3152,7 +3166,12 @@ package body Einfo is or else Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Body, -- synchronized variants + E_Protected_Type, + E_Task_Body, + E_Task_Type)); return Flag265 (Id); end SPARK_Pragma_Inherited; @@ -6124,9 +6143,11 @@ package body Einfo is pragma Assert (Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); - - Set_Node33 (Id, V); + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Type, -- synchronized variants + E_Task_Type)); + Set_Node41 (Id, V); end Set_SPARK_Aux_Pragma; procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is @@ -6134,15 +6155,19 @@ package body Einfo is pragma Assert (Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); - + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Type, -- synchronized variants + E_Task_Type)); Set_Flag266 (Id, V); end Set_SPARK_Aux_Pragma_Inherited; procedure Set_SPARK_Pragma (Id : E; V : N) is begin pragma Assert - (Ekind_In (Id, E_Function, -- subprogram variants + (Ekind_In (Id, E_Entry, -- overloadable variants + E_Entry_Family, + E_Function, E_Generic_Function, E_Generic_Procedure, E_Procedure, @@ -6150,15 +6175,21 @@ package body Einfo is or else Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); - - Set_Node32 (Id, V); + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Body, -- synchronized variants + E_Protected_Type, + E_Task_Body, + E_Task_Type)); + Set_Node40 (Id, V); end Set_SPARK_Pragma; procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True) is begin pragma Assert - (Ekind_In (Id, E_Function, -- subprogram variants + (Ekind_In (Id, E_Entry, -- overloadable variants + E_Entry_Family, + E_Function, E_Generic_Function, E_Generic_Procedure, E_Procedure, @@ -6166,8 +6197,12 @@ package body Einfo is or else Ekind_In (Id, E_Generic_Package, -- package variants E_Package, - E_Package_Body)); - + E_Package_Body) + or else + Ekind_In (Id, E_Protected_Body, -- synchronized variants + E_Protected_Type, + E_Task_Body, + E_Task_Type)); Set_Flag265 (Id, V); end Set_SPARK_Pragma_Inherited; @@ -10141,16 +10176,6 @@ package body Einfo is E_Variable => Write_Str ("Encapsulating_State"); - when E_Function | - E_Generic_Function | - E_Generic_Package | - E_Generic_Procedure | - E_Package | - E_Package_Body | - E_Procedure | - E_Subprogram_Body => - Write_Str ("SPARK_Pragma"); - when Type_Kind => Write_Str ("No_Tagged_Streams_Pragma"); @@ -10166,11 +10191,6 @@ package body Einfo is procedure Write_Field33_Name (Id : Entity_Id) is begin case Ekind (Id) is - when E_Generic_Package | - E_Package | - E_Package_Body => - Write_Str ("SPARK_Aux_Pragma"); - when E_Constant | E_Variable | Subprogram_Kind | @@ -10259,7 +10279,8 @@ package body Einfo is procedure Write_Field38_Name (Id : Entity_Id) is begin case Ekind (Id) is - when E_Function | E_Procedure => + when E_Function | + E_Procedure => Write_Str ("Class-wide preconditions"); when others => @@ -10274,7 +10295,8 @@ package body Einfo is procedure Write_Field39_Name (Id : Entity_Id) is begin case Ekind (Id) is - when E_Function | E_Procedure => + when E_Function | + E_Procedure => Write_Str ("Class-wide postcondition"); when others => @@ -10289,6 +10311,22 @@ package body Einfo is procedure Write_Field40_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Entry | + E_Entry_Family | + E_Function | + E_Generic_Function | + E_Generic_Package | + E_Generic_Procedure | + E_Package | + E_Package_Body | + E_Procedure | + E_Protected_Body | + E_Protected_Type | + E_Subprogram_Body | + E_Task_Body | + E_Task_Type => + Write_Str ("SPARK_Pragma"); + when others => Write_Str ("Field40??"); end case; @@ -10301,6 +10339,13 @@ package body Einfo is procedure Write_Field41_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Generic_Package | + E_Package | + E_Package_Body | + E_Protected_Type | + E_Task_Type => + Write_Str ("SPARK_Aux_Pragma"); + when others => Write_Str ("Field41??"); end case; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index ae22e96..ecefb11 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -4070,35 +4070,36 @@ package Einfo is -- Small of the type, either as given in a representation clause, or -- as computed (as a power of two) by the compiler. --- SPARK_Aux_Pragma (Node33) --- Present in package spec and body entities. For a package spec entity --- it relates to the SPARK mode setting for the private part. This field --- points to the N_Pragma node that applies to the private part. This is --- either set with a local SPARK_Mode pragma in the private part or it is --- inherited from the SPARK mode that applies to the rest of the spec. --- For a package body, it similarly applies to the SPARK mode setting for --- the elaboration sequence after the BEGIN. In the case where the pragma --- is inherited, the SPARK_Aux_Pragma_Inherited flag is set in the --- package spec or body entity. +-- SPARK_Aux_Pragma (Node41) +-- Present in [generic] package specs, package bodies and synchronized +-- types. For package specs and synchronized types it refers to the SPARK +-- mode setting for the private part. This field points to the N_Pragma +-- node that either appears in the private part or is inherited from the +-- enclosing context. For package bodies, it refers to the SPARK mode of +-- the elaboration sequence after the BEGIN. The fields points to the +-- N_Pragma node that either appears in the statement sequence or is +-- inherited from the enclosing context. In all cases, if the pragma is +-- inherited, then the SPARK_Aux_Pragma_Inherited flag is set. -- SPARK_Aux_Pragma_Inherited (Flag266) --- Present in the entities of subprogram specs and bodies as well as --- in package specs and bodies. Set if the SPARK_Aux_Pragma field --- points to a pragma that is inherited, rather than a local one. - --- SPARK_Pragma (Node32) --- Present in the entities of subprogram specs and bodies as well as in --- package specs and bodies. 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 [generic] package specs, package bodies and synchronized +-- types. Set if the SPARK_Aux_Pragma field points to a pragma that 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. -- SPARK_Pragma_Inherited (Flag265) --- Present in the entities of subprogram specs and bodies as well as in --- package specs and bodies. Set if the SPARK_Pragma field points to a --- pragma that is inherited, rather than a local one. +-- 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. -- Spec_Entity (Node19) -- Defined in package body entities. Points to corresponding package @@ -5756,12 +5757,14 @@ package Einfo is -- PPC_Wrapper (Node25) -- Extra_Formals (Node28) -- Contract (Node34) + -- SPARK_Pragma (Node40) (protected kind) -- Needs_No_Actuals (Flag22) -- Uses_Sec_Stack (Flag95) -- Default_Expressions_Processed (Flag108) -- Entry_Accepted (Flag152) -- Sec_Stack_Needed_For_Return (Flag167) -- Has_Expanded_Contract (Flag240) + -- SPARK_Pragma_Inherited (Flag265) (protected kind) -- Address_Clause (synth) -- Entry_Index_Type (synth) -- First_Formal (synth) @@ -5864,13 +5867,13 @@ package Einfo is -- Subprograms_For_Type (Node29) -- Corresponding_Equality (Node30) (implicit /= only) -- Thunk_Entity (Node31) (thunk case only) - -- SPARK_Pragma (Node32) -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Import_Pragma (Node35) (non-generic case only) -- Anonymous_Master (Node36) (non-generic case only) -- Class_Wide_Preconds (List38) -- Class_Wide_Postconds (List39) + -- SPARK_Pragma (Node40) -- Body_Needed_For_SAL (Flag40) -- Contains_Ignored_Ghost_Code (Flag279) -- Default_Expressions_Processed (Flag108) @@ -6086,10 +6089,10 @@ package Einfo is -- Package_Instantiation (Node26) -- Current_Use_Clause (Node27) -- Finalizer (Node28) (non-generic case only) - -- SPARK_Pragma (Node32) - -- SPARK_Aux_Pragma (Node33) -- Contract (Node34) -- Anonymous_Master (Node36) (non-generic case only) + -- SPARK_Pragma (Node40) + -- SPARK_Aux_Pragma (Node41) -- Delay_Subprogram_Descriptors (Flag50) -- Body_Needed_For_SAL (Flag40) -- Contains_Ignored_Ghost_Code (Flag279) @@ -6123,10 +6126,10 @@ package Einfo is -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) -- Finalizer (Node28) (non-generic case only) - -- SPARK_Pragma (Node32) - -- SPARK_Aux_Pragma (Node33) -- Contract (Node34) -- Anonymous_Master (Node36) + -- SPARK_Pragma (Node40) + -- SPARK_Aux_Pragma (Node41) -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Subprogram_Descriptors (Flag50) -- SPARK_Aux_Pragma_Inherited (Flag266) @@ -6174,13 +6177,13 @@ package Einfo is -- Extra_Formals (Node28) -- Static_Initialization (Node30) (init_proc only) -- Thunk_Entity (Node31) (thunk case only) - -- SPARK_Pragma (Node32) -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Import_Pragma (Node35) (non-generic case only) -- Anonymous_Master (Node36) (non-generic case only) -- Class_Wide_Preconds (List38) -- Class_Wide_Postconds (List39) + -- SPARK_Pragma (Node40) -- Body_Needed_For_SAL (Flag40) -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Cleanups (Flag114) @@ -6233,6 +6236,8 @@ package Einfo is -- Number_Formals (synth) -- E_Protected_Body + -- SPARK_Pragma (Node40) + -- SPARK_Pragma_Inherited (Flag265) -- (any others??? First/Last Entity, Scope_Depth???) -- E_Protected_Object @@ -6247,14 +6252,18 @@ package Einfo is -- Last_Entity (Node20) -- Discriminant_Constraint (Elist21) -- Scope_Depth_Value (Uint22) - -- Scope_Depth (synth) -- Stored_Constraint (Elist23) - -- Has_Interrupt_Handler (synth) + -- SPARK_Pragma (Node40) + -- SPARK_Aux_Pragma (Node41) -- Sec_Stack_Needed_For_Return (Flag167) ??? + -- SPARK_Aux_Pragma_Inherited (Flag266) + -- SPARK_Pragma_Inherited (Flag265) -- Uses_Lock_Free (Flag188) -- Uses_Sec_Stack (Flag95) ??? -- Has_Entries (synth) + -- Has_Interrupt_Handler (synth) -- Number_Entries (synth) + -- Scope_Depth (synth) -- E_Record_Type -- E_Record_Subtype @@ -6351,9 +6360,9 @@ package Einfo is -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) -- Extra_Formals (Node28) - -- SPARK_Pragma (Node32) -- Contract (Node34) -- Anonymous_Master (Node36) + -- SPARK_Pragma (Node40) -- Contains_Ignored_Ghost_Code (Flag279) -- SPARK_Pragma_Inherited (Flag265) -- Scope_Depth (synth) @@ -6369,6 +6378,8 @@ package Einfo is -- (plus type attributes) -- E_Task_Body + -- SPARK_Pragma (Node40) + -- SPARK_Pragma_Inherited (Flag265) -- (any others??? First/Last Entity, Scope_Depth???) -- E_Task_Type @@ -6385,11 +6396,15 @@ package Einfo is -- Task_Body_Procedure (Node25) -- Storage_Size_Variable (Node26) (base type only) -- Relative_Deadline_Variable (Node28) (base type only) + -- SPARK_Pragma (Node40) + -- SPARK_Aux_Pragma (Node41) -- Delay_Cleanups (Flag114) -- Has_Master_Entity (Flag21) -- Has_Storage_Size_Clause (Flag23) (base type only) - -- Uses_Sec_Stack (Flag95) ??? -- Sec_Stack_Needed_For_Return (Flag167) ??? + -- SPARK_Aux_Pragma_Inherited (Flag266) + -- SPARK_Pragma_Inherited (Flag265) + -- Uses_Sec_Stack (Flag95) ??? -- Has_Entries (synth) -- Number_Entries (synth) -- (plus type attributes) diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index fa263b5..aa3d19f 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -463,7 +463,7 @@ package body Exp_Ch4 is -- Local variables Loc : constant Source_Ptr := Sloc (Unit_Id); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Unit_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Unit_Decl); Decls : List_Id; FM_Id : Entity_Id; Pref : Character; diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 05b3530..00b3b60 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -1019,14 +1019,16 @@ package body Exp_Ch9 is -- (whether coming from this routine, or directly from source). if Opt.Suppress_Control_Flow_Optimizations then - Stmt := Make_Implicit_If_Statement (Cond, - Condition => Cond, - Then_Statements => New_List ( - Make_Simple_Return_Statement (Loc, - New_Occurrence_Of (Standard_True, Loc))), - Else_Statements => New_List ( - Make_Simple_Return_Statement (Loc, - New_Occurrence_Of (Standard_False, Loc)))); + Stmt := + Make_Implicit_If_Statement (Cond, + Condition => Cond, + Then_Statements => New_List ( + Make_Simple_Return_Statement (Loc, + New_Occurrence_Of (Standard_True, Loc))), + + Else_Statements => New_List ( + Make_Simple_Return_Statement (Loc, + New_Occurrence_Of (Standard_False, Loc)))); else Stmt := Make_Simple_Return_Statement (Loc, Cond); @@ -1061,22 +1063,24 @@ package body Exp_Ch9 is begin Set_Debug_Info_Needed (Def_Id); - return Make_Function_Specification (Loc, - Defining_Unit_Name => Def_Id, - Parameter_Specifications => New_List ( - Make_Parameter_Specification (Loc, - Defining_Identifier => - Make_Defining_Identifier (Loc, Name_uO), - Parameter_Type => - New_Occurrence_Of (RTE (RE_Address), Loc)), - - Make_Parameter_Specification (Loc, - Defining_Identifier => - Make_Defining_Identifier (Loc, Name_uE), - Parameter_Type => - New_Occurrence_Of (RTE (RE_Protected_Entry_Index), Loc))), - - Result_Definition => New_Occurrence_Of (Standard_Boolean, Loc)); + return + Make_Function_Specification (Loc, + Defining_Unit_Name => Def_Id, + Parameter_Specifications => New_List ( + Make_Parameter_Specification (Loc, + Defining_Identifier => + Make_Defining_Identifier (Loc, Name_uO), + Parameter_Type => + New_Occurrence_Of (RTE (RE_Address), Loc)), + + Make_Parameter_Specification (Loc, + Defining_Identifier => + Make_Defining_Identifier (Loc, Name_uE), + Parameter_Type => + New_Occurrence_Of (RTE (RE_Protected_Entry_Index), Loc))), + + Result_Definition => + New_Occurrence_Of (Standard_Boolean, Loc)); end Build_Barrier_Function_Specification; -------------------------- @@ -6260,7 +6264,7 @@ package body Exp_Ch9 is -- version of it because it is never called. if Expander_Active then - B_F := Build_Barrier_Function (N, Ent, Prot); + B_F := Build_Barrier_Function (N, Ent, Prot); Func := Barrier_Function (Ent); Set_Corresponding_Spec (B_F, Func); @@ -8827,8 +8831,9 @@ package body Exp_Ch9 is -- the specs refer to this type. procedure Expand_N_Protected_Type_Declaration (N : Node_Id) is - Loc : constant Source_Ptr := Sloc (N); - Prot_Typ : constant Entity_Id := Defining_Identifier (N); + Discr_Map : constant Elist_Id := New_Elmt_List; + Loc : constant Source_Ptr := Sloc (N); + Prot_Typ : constant Entity_Id := Defining_Identifier (N); Lock_Free_Active : constant Boolean := Uses_Lock_Free (Prot_Typ); -- This flag indicates whether the lock free implementation is active @@ -8836,20 +8841,19 @@ package body Exp_Ch9 is Pdef : constant Node_Id := Protected_Definition (N); -- This contains two lists; one for visible and one for private decls - Rec_Decl : Node_Id; + Body_Arr : Node_Id; + Body_Id : Entity_Id; Cdecls : List_Id; - Discr_Map : constant Elist_Id := New_Elmt_List; - Priv : Node_Id; - New_Priv : Node_Id; Comp : Node_Id; Comp_Id : Entity_Id; - Sub : Node_Id; Current_Node : Node_Id := N; - Entries_Aggr : Node_Id; - Body_Id : Entity_Id; - Body_Arr : Node_Id; E_Count : Int; + Entries_Aggr : Node_Id; + New_Priv : Node_Id; Object_Comp : Node_Id; + Priv : Node_Id; + Rec_Decl : Node_Id; + Sub : Node_Id; procedure Check_Inlining (Subp : Entity_Id); -- If the original operation has a pragma Inline, propagate the flag @@ -9020,6 +9024,7 @@ package body Exp_Ch9 is Make_Subprogram_Declaration (Loc, Specification => Build_Barrier_Function_Specification (Loc, Bdef)); + Set_Is_Entry_Barrier_Function (Sub); Insert_After (Current_Node, Sub); Analyze (Sub); @@ -9146,13 +9151,12 @@ package body Exp_Ch9 is elsif Restriction_Active (No_Implicit_Heap_Allocations) then if not Discriminated_Size (Defining_Identifier (Priv)) then - -- Any object of the type will be non-static. Error_Msg_N ("component has non-static size??", Priv); Error_Msg_NE - ("\creation of protected object of type& will" - & " violate restriction " + ("\creation of protected object of type& will " + & "violate restriction " & "No_Implicit_Heap_Allocations??", Priv, Prot_Typ); else @@ -9172,24 +9176,22 @@ package body Exp_Ch9 is then if not Discriminated_Size (Defining_Identifier (Priv)) then - -- Any object of the type will be non-static. Error_Msg_N ("component has non-static size??", Priv); Error_Msg_NE - ("\creation of protected object of type& will" - & " violate restriction " + ("\creation of protected object of type& will " + & "violate restriction " & "No_Implicit_Protected_Object_Allocations??", Priv, Prot_Typ); else - -- Object will be non-static if discriminants are. Error_Msg_NE ("creation of protected object of type& with " - & "non-static discriminants will violate " - & " restriction" - & " No_Implicit_Protected_Object_Allocations??", + & "non-static discriminants will violate " + & "restriction " + & "No_Implicit_Protected_Object_Allocations??", Priv, Prot_Typ); end if; end if; @@ -9202,10 +9204,10 @@ package body Exp_Ch9 is declare Old_Comp : constant Node_Id := Component_Definition (Priv); Oent : constant Entity_Id := Defining_Identifier (Priv); - New_Comp : Node_Id; Nent : constant Entity_Id := Make_Defining_Identifier (Sloc (Oent), Chars => Chars (Oent)); + New_Comp : Node_Id; begin if Present (Subtype_Indication (Old_Comp)) then @@ -9213,15 +9215,15 @@ package body Exp_Ch9 is Make_Component_Definition (Sloc (Oent), Aliased_Present => False, Subtype_Indication => - New_Copy_Tree (Subtype_Indication (Old_Comp), - Discr_Map)); + New_Copy_Tree + (Subtype_Indication (Old_Comp), Discr_Map)); else New_Comp := Make_Component_Definition (Sloc (Oent), Aliased_Present => False, Access_Definition => - New_Copy_Tree (Access_Definition (Old_Comp), - Discr_Map)); + New_Copy_Tree + (Access_Definition (Old_Comp), Discr_Map)); end if; New_Priv := @@ -9289,12 +9291,12 @@ package body Exp_Ch9 is if not Lock_Free_Active then declare - Ritem : Node_Id; - Num_Attach_Handler : Int := 0; - Protection_Subtype : Node_Id; Entry_Count_Expr : constant Node_Id := Build_Entry_Count_Expression (Prot_Typ, Cdecls, Loc); + Num_Attach_Handler : Int := 0; + Protection_Subtype : Node_Id; + Ritem : Node_Id; begin if Has_Attach_Handler (Prot_Typ) then @@ -9486,9 +9488,7 @@ package body Exp_Ch9 is end if; elsif Nkind (Comp) = N_Entry_Declaration then - Expand_Entry_Declaration (Comp); - end if; Next (Comp); @@ -9518,28 +9518,31 @@ package body Exp_Ch9 is case Corresponding_Runtime_Package (Prot_Typ) is when System_Tasking_Protected_Objects_Entries => - Body_Arr := Make_Object_Declaration (Loc, - Defining_Identifier => Body_Id, - Aliased_Present => True, - Object_Definition => - Make_Subtype_Indication (Loc, - Subtype_Mark => New_Occurrence_Of ( - RTE (RE_Protected_Entry_Body_Array), Loc), - Constraint => - Make_Index_Or_Discriminant_Constraint (Loc, - Constraints => New_List ( - Make_Range (Loc, - Make_Integer_Literal (Loc, 1), - Make_Integer_Literal (Loc, E_Count))))), - Expression => Entries_Aggr); + Body_Arr := + Make_Object_Declaration (Loc, + Defining_Identifier => Body_Id, + Aliased_Present => True, + Object_Definition => + Make_Subtype_Indication (Loc, + Subtype_Mark => + New_Occurrence_Of + (RTE (RE_Protected_Entry_Body_Array), Loc), + Constraint => + Make_Index_Or_Discriminant_Constraint (Loc, + Constraints => New_List ( + Make_Range (Loc, + Make_Integer_Literal (Loc, 1), + Make_Integer_Literal (Loc, E_Count))))), + Expression => Entries_Aggr); when System_Tasking_Protected_Objects_Single_Entry => - Body_Arr := Make_Object_Declaration (Loc, - Defining_Identifier => Body_Id, - Aliased_Present => True, - Object_Definition => New_Occurrence_Of - (RTE (RE_Entry_Body), Loc), - Expression => Remove_Head (Expressions (Entries_Aggr))); + Body_Arr := + Make_Object_Declaration (Loc, + Defining_Identifier => Body_Id, + Aliased_Present => True, + Object_Definition => + New_Occurrence_Of (RTE (RE_Entry_Body), Loc), + Expression => Remove_Head (Expressions (Entries_Aggr))); when others => raise Program_Error; @@ -11512,6 +11515,7 @@ package body Exp_Ch9 is Specification => Build_Task_Proc_Specification (Ttyp), Declarations => Declarations (N), Handled_Statement_Sequence => Handled_Statement_Sequence (N)); + Set_Is_Task_Body_Procedure (New_N); -- If the task contains generic instantiations, cleanup actions are -- delayed until after instantiation. Transfer the activation chain to @@ -12052,6 +12056,7 @@ package body Exp_Ch9 is Body_Decl := Make_Subprogram_Declaration (Loc, Specification => Proc_Spec); + Set_Is_Task_Body_Procedure (Body_Decl); Insert_After (Rec_Decl, Body_Decl); diff --git a/gcc/ada/exp_unst.adb b/gcc/ada/exp_unst.adb index bbd11f9..1bea872 100644 --- a/gcc/ada/exp_unst.adb +++ b/gcc/ada/exp_unst.adb @@ -520,7 +520,7 @@ package body Exp_Unst is -- of no corresponding body being available is ignored for now. elsif Nkind (N) = N_Subprogram_Body then - Ent := Corresponding_Spec_Of (N); + Ent := Unique_Defining_Entity (N); -- Ignore generic subprogram diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 21b66d4..009379d 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1351,7 +1351,7 @@ package body Sem_Attr is -- If we get here, then the attribute is legal Legal := True; - Spec_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id := Unique_Defining_Entity (Subp_Decl); end Analyze_Attribute_Old_Result; --------------------------------- diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb index ea83e83..c85a9f3 100644 --- a/gcc/ada/sem_aux.adb +++ b/gcc/ada/sem_aux.adb @@ -1380,7 +1380,7 @@ package body Sem_Aux is -- Number_Components -- ----------------------- - function Number_Components (Typ : Entity_Id) return Pos is + function Number_Components (Typ : Entity_Id) return Nat is N : Int; Comp : Entity_Id; diff --git a/gcc/ada/sem_aux.ads b/gcc/ada/sem_aux.ads index db0931e..ba60284 100644 --- a/gcc/ada/sem_aux.ads +++ b/gcc/ada/sem_aux.ads @@ -377,7 +377,7 @@ package Sem_Aux is -- The result returned is the next _Tag field in this record, or Empty -- if this is the last such field. - function Number_Components (Typ : Entity_Id) return Pos; + function Number_Components (Typ : Entity_Id) return Nat; -- Typ is a record type, yields number of components (including -- discriminants) in type. diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 41ceb3d..2599228 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -1926,17 +1926,6 @@ package body Sem_Ch10 is Error_Msg_N ("missing specification for Protected body", N); else - -- Currently there are no language-defined aspects that can apply to - -- a protected body stub. Issue an error and remove the aspects to - -- prevent cascaded errors. - - if Has_Aspects (N) then - Error_Msg_N - ("aspects on protected bodies are not allowed", - First (Aspect_Specifications (N))); - Remove_Aspects (N); - end if; - Set_Scope (Defining_Entity (N), Current_Scope); Set_Has_Completion (Etype (Nam)); Set_Corresponding_Spec_Of_Stub (N, Nam); @@ -2390,17 +2379,6 @@ package body Sem_Ch10 is Error_Msg_N ("missing specification for task body", N); else - -- Currently there are no language-defined aspects that can apply to - -- a task body stub. Issue an error and remove the aspects to prevent - -- cascaded errors. - - if Has_Aspects (N) then - Error_Msg_N - ("aspects on task bodies are not allowed", - First (Aspect_Specifications (N))); - Remove_Aspects (N); - end if; - Set_Scope (Defining_Entity (N), Current_Scope); Generate_Reference (Nam, Defining_Identifier (N), 'b'); Set_Corresponding_Spec_Of_Stub (N, Nam); @@ -2425,7 +2403,7 @@ package body Sem_Ch10 is if Expander_Active then Insert_After (N, Make_Assignment_Statement (Loc, - Name => + Name => Make_Identifier (Loc, Chars => New_External_Name (Chars (Etype (Nam)), 'E')), Expression => New_Occurrence_Of (Standard_True, Loc))); diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 93da049..ae02bdd 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1212,15 +1212,28 @@ package body Sem_Ch13 is (Prag : Node_Id; Ins_Nod : Node_Id; Decls : List_Id); - -- Subsidiary to the analysis of aspects Abstract_State, Ghost, - -- Initializes, Initial_Condition and Refined_State. Insert node Prag - -- before node Ins_Nod. If Ins_Nod is for pragma SPARK_Mode, then skip - -- SPARK_Mode. Decls is the associated declarative list where Prag is to - -- reside. + -- Subsidiary to the analysis of aspects + -- Abstract_State + -- Ghost + -- Initializes + -- Initial_Condition + -- Refined_State + -- Insert node Prag before node Ins_Nod. If Ins_Nod is for pragma + -- SPARK_Mode, then skip SPARK_Mode. Decls is the associated declarative + -- list where Prag is to reside. procedure Insert_Pragma (Prag : Node_Id); - -- Subsidiary to the analysis of aspects Attach_Handler, Contract_Cases, - -- Depends, Global, Post, Pre, Refined_Depends and Refined_Global. + -- Subsidiary to the analysis of aspects + -- Attach_Handler + -- Contract_Cases + -- Depends + -- Global + -- Post + -- Pre + -- Refined_Depends + -- Refined_Global + -- SPARK_Mode + -- Warnings -- Insert pragma Prag such that it mimics the placement of a source -- pragma of the same kind. -- @@ -1277,46 +1290,123 @@ package body Sem_Ch13 is ------------------- procedure Insert_Pragma (Prag : Node_Id) is - Aux : Node_Id; - Decl : Node_Id; + Aux : Node_Id; + Decl : Node_Id; + Decls : List_Id; begin - if Nkind (N) = N_Subprogram_Body then - if Present (Declarations (N)) then - - -- Skip other internally generated pragmas from aspects to find - -- the proper insertion point. As a result the order of pragmas - -- is the same as the order of aspects. - - -- As precondition pragmas generated from conjuncts in the - -- precondition aspect are presented in reverse order to - -- Insert_Pragma, insert them in the correct order here by not - -- skipping previously inserted precondition pragmas when the - -- current pragma is a precondition. - - Decl := First (Declarations (N)); - while Present (Decl) loop - if Nkind (Decl) = N_Pragma - and then From_Aspect_Specification (Decl) - and then not (Get_Pragma_Id (Decl) = Pragma_Precondition - and then - Get_Pragma_Id (Prag) = Pragma_Precondition) - then - Next (Decl); - else - exit; - end if; - end loop; + -- When the aspect appears on a package, protected unit, subprogram + -- or task unit body, insert the generated pragma at the top of the + -- body declarations to emulate the behavior of a source pragma. + + -- package body Pack with Aspect is - if Present (Decl) then - Insert_Before (Decl, Prag); + -- package body Pack is + -- pragma Prag; + + if Nkind_In (N, N_Package_Body, + N_Protected_Body, + N_Subprogram_Body, + N_Task_Body) + then + Decls := Declarations (N); + + if No (Decls) then + Decls := New_List; + Set_Declarations (N, Decls); + end if; + + -- Skip other internally generated pragmas from aspects to find + -- the proper insertion point. As a result the order of pragmas + -- is the same as the order of aspects. + + -- As precondition pragmas generated from conjuncts in the + -- precondition aspect are presented in reverse order to + -- Insert_Pragma, insert them in the correct order here by not + -- skipping previously inserted precondition pragmas when the + -- current pragma is a precondition. + + Decl := First (Decls); + while Present (Decl) loop + if Nkind (Decl) = N_Pragma + and then From_Aspect_Specification (Decl) + and then not (Get_Pragma_Id (Decl) = Pragma_Precondition + and then + Get_Pragma_Id (Prag) = Pragma_Precondition) + then + Next (Decl); else - Append (Prag, Declarations (N)); + exit; end if; + end loop; + + if Present (Decl) then + Insert_Before (Decl, Prag); else - Set_Declarations (N, New_List (Prag)); + Append_To (Decls, Prag); + end if; + + -- When the aspect is associated with a [generic] package declaration + -- insert the generated pragma at the top of the visible declarations + -- to emulate the behavior of a source pragma. + + -- package Pack with Aspect is + + -- package Pack is + -- pragma Prag; + + elsif Nkind_In (N, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Decls := Visible_Declarations (Specification (N)); + + if No (Decls) then + Decls := New_List; + Set_Visible_Declarations (Specification (N), Decls); + end if; + + Prepend_To (Decls, Prag); + + -- When the aspect is associated with a protected unit declaration, + -- insert the generated pragma at the top of the visible declarations + -- the emulate the behavior of a source pragma. + + -- protected [type] Prot with Aspect is + + -- protected [type] Prot is + -- pragma Prag; + + elsif Nkind (N) = N_Protected_Type_Declaration then + Decls := Visible_Declarations (Protected_Definition (N)); + + if No (Decls) then + Decls := New_List; + Set_Visible_Declarations (Protected_Definition (N), Decls); end if; + Prepend_To (Decls, Prag); + + -- When the aspect is associated with a task unit declaration with a + -- definition, insert the generated pragma at the top of the visible + -- declarations the emulate the behavior of a source pragma. + + -- task [type] Prot with Aspect is + + -- task [type] Prot is + -- pragma Prag; + + elsif Nkind (N) = N_Task_Type_Declaration + and then Present (Task_Definition (N)) + then + Decls := Visible_Declarations (Task_Definition (N)); + + if No (Decls) then + Decls := New_List; + Set_Visible_Declarations (Task_Definition (N), Decls); + end if; + + Prepend_To (Decls, Prag); + -- When the context is a library unit, the pragma is added to the -- Pragmas_After list. @@ -1329,7 +1419,7 @@ package body Sem_Ch13 is Prepend (Prag, Pragmas_After (Aux)); - -- Default + -- Default, the pragma is inserted after the context else Insert_After (N, Prag); @@ -2128,11 +2218,9 @@ package body Sem_Ch13 is goto Continue; - -- For tasks + -- For tasks pass the aspect as an attribute else - -- Pass the aspect as an attribute - Aitem := Make_Attribute_Definition_Clause (Loc, Name => Ent, @@ -2151,6 +2239,10 @@ package body Sem_Ch13 is Expression => New_Occurrence_Of (E, Loc))), Pragma_Name => Chars (Id)); + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + -- Case 2c: Aspects corresponding to pragmas with three -- arguments. @@ -2657,54 +2749,16 @@ package body Sem_Ch13 is -- SPARK_Mode - when Aspect_SPARK_Mode => SPARK_Mode : declare - Decls : List_Id; - - begin + when Aspect_SPARK_Mode => Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Loc, Expression => Relocate_Node (Expr))), Pragma_Name => Name_SPARK_Mode); - -- When the aspect appears on a package or a subprogram - -- body, insert the generated pragma at the top of the body - -- declarations to emulate the behavior of a source pragma. - - if Nkind_In (N, N_Package_Body, N_Subprogram_Body) then - Decorate (Aspect, Aitem); - - Decls := Declarations (N); - - if No (Decls) then - Decls := New_List; - Set_Declarations (N, Decls); - end if; - - Prepend_To (Decls, Aitem); - goto Continue; - - -- When the aspect is associated with a [generic] package - -- declaration, insert the generated pragma at the top of - -- the visible declarations to emulate the behavior of a - -- source pragma. - - elsif Nkind_In (N, N_Generic_Package_Declaration, - N_Package_Declaration) - then - Decorate (Aspect, Aitem); - - Decls := Visible_Declarations (Specification (N)); - - if No (Decls) then - Decls := New_List; - Set_Visible_Declarations (Specification (N), Decls); - end if; - - Prepend_To (Decls, Aitem); - goto Continue; - end if; - end SPARK_Mode; + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; -- Refined_Depends diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 495df3d..56a13de 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -2364,6 +2364,7 @@ package body Sem_Ch6 is Subp_Decl := Make_Subprogram_Declaration (Loc, Specification => Copy_Subprogram_Spec (Body_Spec)); + Set_Comes_From_Source (Subp_Decl, True); -- Relocate the aspects of the subprogram body to the new subprogram -- spec because it acts as the initial declaration. @@ -3467,10 +3468,19 @@ package body Sem_Ch6 is Generate_Reference_To_Formals (Body_Id); end if; - -- Set SPARK_Mode from context + -- Set the SPARK_Mode from the current context (may be overwritten later + -- with explicit pragma). This is not done for entry barrier functions + -- because they are generated outside the protected type and should not + -- carry the mode of the enclosing context. - Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); - Set_SPARK_Pragma_Inherited (Body_Id); + if Nkind (N) = N_Subprogram_Body + and then Is_Entry_Barrier_Function (N) + then + null; + else + Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Body_Id); + end if; -- If the return type is an anonymous access type whose designated type -- is the limited view of a class-wide type and the non-limited view is @@ -4047,11 +4057,19 @@ package body Sem_Ch6 is Generate_Definition (Designator); - -- Set SPARK mode from current context (may be overwritten later with - -- explicit pragma). + -- Set the SPARK mode from the current context (may be overwritten later + -- with explicit pragma). This is not done for entry barrier functions + -- because they are generated outside the protected type and should not + -- carry the mode of the enclosing context. - Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma); - Set_SPARK_Pragma_Inherited (Designator); + if Nkind (N) = N_Subprogram_Declaration + and then Is_Entry_Barrier_Function (N) + then + null; + else + Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Designator); + end if; -- A subprogram declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 4874844..1ebda33 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -718,15 +718,9 @@ package body Sem_Ch7 is -- Set SPARK_Mode only for non-generic package if Ekind (Spec_Id) = E_Package then - - -- Set SPARK_Mode from context - - Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); - Set_SPARK_Pragma_Inherited (Body_Id); - - -- Set elaboration code SPARK mode the same for now - - Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id)); + Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); + Set_SPARK_Aux_Pragma (Body_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Body_Id); Set_SPARK_Aux_Pragma_Inherited (Body_Id); end if; diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 728d17d..3494eb5 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -23,42 +23,43 @@ -- -- ------------------------------------------------------------------------------ -with Aspects; use Aspects; -with Atree; use Atree; -with Checks; use Checks; -with Debug; use Debug; -with Einfo; use Einfo; -with Errout; use Errout; -with Exp_Ch9; use Exp_Ch9; -with Elists; use Elists; -with Freeze; use Freeze; -with Layout; use Layout; -with Lib.Xref; use Lib.Xref; -with Namet; use Namet; -with Nlists; use Nlists; -with Nmake; use Nmake; -with Opt; use Opt; -with Restrict; use Restrict; -with Rident; use Rident; -with Rtsfind; use Rtsfind; -with Sem; use Sem; -with Sem_Aux; use Sem_Aux; -with Sem_Ch3; use Sem_Ch3; -with Sem_Ch5; use Sem_Ch5; -with Sem_Ch6; use Sem_Ch6; -with Sem_Ch8; use Sem_Ch8; -with Sem_Ch13; use Sem_Ch13; -with Sem_Eval; use Sem_Eval; -with Sem_Res; use Sem_Res; -with Sem_Type; use Sem_Type; -with Sem_Util; use Sem_Util; -with Sem_Warn; use Sem_Warn; -with Snames; use Snames; -with Stand; use Stand; -with Sinfo; use Sinfo; +with Aspects; use Aspects; +with Atree; use Atree; +with Checks; use Checks; +with Contracts; use Contracts; +with Debug; use Debug; +with Einfo; use Einfo; +with Errout; use Errout; +with Exp_Ch9; use Exp_Ch9; +with Elists; use Elists; +with Freeze; use Freeze; +with Layout; use Layout; +with Lib.Xref; use Lib.Xref; +with Namet; use Namet; +with Nlists; use Nlists; +with Nmake; use Nmake; +with Opt; use Opt; +with Restrict; use Restrict; +with Rident; use Rident; +with Rtsfind; use Rtsfind; +with Sem; use Sem; +with Sem_Aux; use Sem_Aux; +with Sem_Ch3; use Sem_Ch3; +with Sem_Ch5; use Sem_Ch5; +with Sem_Ch6; use Sem_Ch6; +with Sem_Ch8; use Sem_Ch8; +with Sem_Ch13; use Sem_Ch13; +with Sem_Eval; use Sem_Eval; +with Sem_Res; use Sem_Res; +with Sem_Type; use Sem_Type; +with Sem_Util; use Sem_Util; +with Sem_Warn; use Sem_Warn; +with Snames; use Snames; +with Stand; use Stand; +with Sinfo; use Sinfo; with Style; -with Tbuild; use Tbuild; -with Uintp; use Uintp; +with Tbuild; use Tbuild; +with Uintp; use Uintp; package body Sem_Ch9 is @@ -1190,6 +1191,13 @@ package body Sem_Ch9 is Entry_Name : Entity_Id; begin + -- An entry body "freezes" the contract of the nearest enclosing + -- package body. This ensures that any annotations referenced by the + -- contract of an entry or subprogram body declared within the current + -- protected body are available. + + Analyze_Enclosing_Package_Body_Contract (N); + Tasking_Used := True; -- Entry_Name is initialized to Any_Id. It should get reset to the @@ -1209,6 +1217,12 @@ package body Sem_Ch9 is Set_Etype (Id, Standard_Void_Type); Set_Accept_Address (Id, New_Elmt_List); + -- Set the SPARK_Mode from the current context (may be overwritten later + -- with an explicit pragma). + + Set_SPARK_Pragma (Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Id); + E := First_Entity (P_Type); while Present (E) loop if Chars (E) = Chars (Id) @@ -1217,7 +1231,7 @@ package body Sem_Ch9 is then Entry_Name := E; Set_Convention (Id, Convention (E)); - Set_Corresponding_Body (Parent (Entry_Name), Id); + Set_Corresponding_Body (Parent (E), Id); Check_Fully_Conformant (Id, E, N); if Ekind (Id) = E_Entry_Family then @@ -1601,6 +1615,15 @@ package body Sem_Ch9 is Set_Convention (Def_Id, Convention_Entry); Set_Accept_Address (Def_Id, New_Elmt_List); + -- Set the SPARK_Mode from the current context (may be overwritten later + -- with an explicit pragma). Task entries are excluded because they are + -- not completed by entry bodies. + + if Ekind (Current_Scope) = E_Protected_Type then + Set_SPARK_Pragma (Def_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Def_Id); + end if; + -- Process formals if Present (Formals) then @@ -1730,29 +1753,19 @@ package body Sem_Ch9 is -- Start of processing for Analyze_Protected_Body begin + -- A protected body "freezes" the contract of the nearest enclosing + -- package body. This ensures that any annotations referenced by the + -- contract of an entry or subprogram body declared within the current + -- protected body are available. + + Analyze_Enclosing_Package_Body_Contract (N); + Tasking_Used := True; Set_Ekind (Body_Id, E_Protected_Body); + Set_Etype (Body_Id, Standard_Void_Type); Spec_Id := Find_Concurrent_Spec (Body_Id); - -- Protected bodies are currently removed by the expander. Since there - -- are no language-defined aspects that apply to a protected body, it is - -- not worth changing the whole expansion to accomodate implementation- - -- defined aspects. Plus we cannot possibly known the semantics of such - -- future implementation-defined aspects in order to plan ahead. - - if Has_Aspects (N) then - Error_Msg_N - ("aspects on protected bodies are not allowed", - First (Aspect_Specifications (N))); - - -- Remove illegal aspects to prevent cascaded errors later on - - Remove_Aspects (N); - end if; - - if Present (Spec_Id) - and then Ekind (Spec_Id) = E_Protected_Type - then + if Present (Spec_Id) and then Ekind (Spec_Id) = E_Protected_Type then null; elsif Present (Spec_Id) @@ -1776,6 +1789,10 @@ package body Sem_Ch9 is Spec_Id := Etype (Spec_Id); end if; + if Has_Aspects (N) then + Analyze_Aspect_Specifications (N, Body_Id); + end if; + Push_Scope (Spec_Id); Set_Corresponding_Spec (N, Spec_Id); Set_Corresponding_Body (Parent (Spec_Id), Body_Id); @@ -1967,6 +1984,15 @@ package body Sem_Ch9 is Set_Etype (T, T); Set_Has_Delayed_Freeze (T, True); Set_Stored_Constraint (T, No_Elist); + + -- Set the SPARK_Mode from the current context (may be overwritten later + -- with an explicit pragma). + + Set_SPARK_Pragma (T, SPARK_Mode_Pragma); + Set_SPARK_Aux_Pragma (T, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (T); + Set_SPARK_Aux_Pragma_Inherited (T); + Push_Scope (T); if Ada_Version >= Ada_2005 then @@ -2719,33 +2745,23 @@ package body Sem_Ch9 is -- a single task, since Spec_Id is set to the task type). begin + -- A task body "freezes" the contract of the nearest enclosing package + -- body. This ensures that any annotations referenced by the contract + -- of an entry or subprogram body declared within the current protected + -- body are available. + + Analyze_Enclosing_Package_Body_Contract (N); + Tasking_Used := True; - Set_Ekind (Body_Id, E_Task_Body); Set_Scope (Body_Id, Current_Scope); + Set_Ekind (Body_Id, E_Task_Body); + Set_Etype (Body_Id, Standard_Void_Type); Spec_Id := Find_Concurrent_Spec (Body_Id); - -- Task bodies are transformed into a subprogram spec and body pair by - -- the expander. Since there are no language-defined aspects that apply - -- to a task body, it is not worth changing the whole expansion to - -- accomodate implementation-defined aspects. Plus we cannot possibly - -- know semantics of such aspects in order to plan ahead. - - if Has_Aspects (N) then - Error_Msg_N - ("aspects on task bodies are not allowed", - First (Aspect_Specifications (N))); - - -- Remove illegal aspects to prevent cascaded errors later on - - Remove_Aspects (N); - end if; - -- The spec is either a task type declaration, or a single task -- declaration for which we have created an anonymous type. - if Present (Spec_Id) - and then Ekind (Spec_Id) = E_Task_Type - then + if Present (Spec_Id) and then Ekind (Spec_Id) = E_Task_Type then null; elsif Present (Spec_Id) @@ -2779,6 +2795,16 @@ package body Sem_Ch9 is Spec_Id := Etype (Spec_Id); end if; + -- Set the SPARK_Mode from the current context (may be overwritten later + -- with an explicit pragma). + + Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Body_Id); + + if Has_Aspects (N) then + Analyze_Aspect_Specifications (N, Body_Id); + end if; + Push_Scope (Spec_Id); Set_Corresponding_Spec (N, Spec_Id); Set_Corresponding_Body (Parent (Spec_Id), Body_Id); @@ -2939,6 +2965,15 @@ package body Sem_Ch9 is Set_Etype (T, T); Set_Has_Delayed_Freeze (T, True); Set_Stored_Constraint (T, No_Elist); + + -- Set the SPARK_Mode from the current context (may be overwritten later + -- with an explicit pragma). + + Set_SPARK_Pragma (T, SPARK_Mode_Pragma); + Set_SPARK_Aux_Pragma (T, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (T); + Set_SPARK_Aux_Pragma_Inherited (T); + Push_Scope (T); if Ada_Version >= Ada_2005 then diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index d97bc86..0795b21 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -387,7 +387,7 @@ package body Sem_Prag is -- Local variables Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; @@ -460,7 +460,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); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); All_Inputs_Seen : Elist_Id := No_Elist; -- A list containing the entities of all the inputs processed so far. @@ -1750,7 +1750,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); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl); Constits_Seen : Elist_Id := No_Elist; @@ -3328,7 +3328,7 @@ package body Sem_Prag is return; end if; - Spec_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id := Unique_Defining_Entity (Subp_Decl); -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -12327,7 +12327,7 @@ package body Sem_Prag is return; end if; - Spec_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id := Unique_Defining_Entity (Subp_Decl); -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. @@ -14003,7 +14003,7 @@ package body Sem_Prag is return; end if; - Spec_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id := Unique_Defining_Entity (Subp_Decl); -- Mark the pragma as Ghost if the related subprogram is also -- Ghost. This also ensures that any expansion performed further @@ -14255,14 +14255,6 @@ package body Sem_Prag is Check_No_Identifiers; Check_At_Most_N_Arguments (1); - Context := Parent (N); - - -- Handle compilation units - - if Nkind (Context) = N_Compilation_Unit_Aux then - Context := Unit (Parent (Context)); - end if; - Id := Empty; Stmt := Prev (N); while Present (Stmt) loop @@ -14276,14 +14268,12 @@ package body Sem_Prag is Error_Msg_N ("pragma % duplicates pragma declared#", N); end if; - -- Protected and task types cannot be subject to pragma Ghost - -- (SPARK RM 6.9(19)). + -- Task unit declared without a definition cannot be subject to + -- pragma Ghost (SPARK RM 6.9(19)). - elsif Nkind (Stmt) = N_Protected_Type_Declaration then - Error_Pragma ("pragma % cannot apply to a protected type"); - return; - - elsif Nkind (Stmt) = N_Task_Type_Declaration then + elsif Nkind_In (Stmt, N_Single_Task_Declaration, + N_Task_Type_Declaration) + then Error_Pragma ("pragma % cannot apply to a task type"); return; @@ -14343,6 +14333,27 @@ package body Sem_Prag is Stmt := Prev (Stmt); end loop; + Context := Parent (N); + + -- Handle compilation units + + if Nkind (Context) = N_Compilation_Unit_Aux then + Context := Unit (Parent (Context)); + end if; + + -- Protected and task types cannot be subject to pragma Ghost + -- (SPARK RM 6.9(19)). + + if Nkind_In (Context, N_Protected_Body, N_Protected_Definition) + then + Error_Pragma ("pragma % cannot apply to a protected type"); + return; + + elsif Nkind_In (Context, N_Task_Body, N_Task_Definition) then + Error_Pragma ("pragma % cannot apply to a task type"); + return; + end if; + if No (Id) then -- When pragma Ghost is associated with a [generic] package, it @@ -19428,32 +19439,62 @@ package body Sem_Prag is procedure Check_Pragma_Conformance (Context_Pragma : Node_Id; - Entity_Pragma : Node_Id; - Entity : Entity_Id); - -- If Context_Pragma is not Empty, verify that the new pragma N - -- is compatible with the pragma Context_Pragma that was inherited + Entity : Entity_Id; + Entity_Pragma : Node_Id); + -- Subsidiary to routines Process_xxx. Verify the SPARK_Mode + -- conformance of pragma N depending the following scenarios: + -- + -- If pragma Context_Pragma is not Empty, verify that pragma N is + -- compatible with the pragma Context_Pragma that was inherited -- from the context: - -- . if Context_Pragma is ON, then the new mode can be anything - -- . if Context_Pragma is OFF, then the only allowed new mode is - -- also OFF. + -- * If the mode of Context_Pragma is ON, then the new mode can + -- be anything. + -- * If the mode of Context_Pragma is OFF, then the only allowed + -- new mode is also OFF. Emit error if this is not the case. -- - -- If Entity is not Empty, verify that the new pragma N is - -- compatible with Entity_Pragma, the SPARK_Mode previously set - -- for Entity (which may be Empty): - -- . if Entity_Pragma is ON, then the new mode can be anything - -- . if Entity_Pragma is OFF, then the only allowed new mode is - -- also OFF. - -- . if Entity_Pragma is Empty, we always issue an error, as this - -- corresponds to a case where a previous section of Entity - -- had no SPARK_Mode set. + -- If Entity is not Empty, verify that pragma N is compatible with + -- pragma Entity_Pragma that belongs to Entity. + -- * If Entity_Pragma is Empty, always issue an error as this + -- corresponds to the case where a previous section of Entity + -- has no SPARK_Mode set. + -- * If the mode of Entity_Pragma is ON, then the new mode can + -- be anything. + -- * If the mode of Entity_Pragma is OFF, then the only allowed + -- new mode is also OFF. Emit error if this is not the case. procedure Check_Library_Level_Entity (E : Entity_Id); - -- Verify that pragma is applied to library-level entity E - - procedure Set_SPARK_Flags; - -- Sets SPARK_Mode from Mode_Id and SPARK_Mode_Pragma from N, - -- and ensures that Dynamic_Elaboration_Checks are off if the - -- call sets SPARK_Mode On. + -- Subsidiary to routines Process_xxx. Verify that the related + -- entity E subject to pragma SPARK_Mode is library-level. + + procedure Process_Body (Decl : Node_Id); + -- Verify the legality of pragma SPARK_Mode when it appears as the + -- top of the body declarations of entry, package, protected unit, + -- subprogram or task unit body denoted by Decl. + + procedure Process_Overloadable (Decl : Node_Id); + -- Verify the legality of pragma SPARK_Mode when it applies to an + -- entry or [generic] subprogram declaration denoted by Decl. + + procedure Process_Private_Part (Decl : Node_Id); + -- Verify the legality of pragma SPARK_Mode when it appears at the + -- top of the private declarations of a package spec, protected or + -- task unit declaration denoted by Decl. + + procedure Process_Statement_Part (Decl : Node_Id); + -- Verify the legality of pragma SPARK_Mode when it appears at the + -- top of the statement sequence of a package body denoted by node + -- Decl. + + procedure Process_Visible_Part (Decl : Node_Id); + -- Verify the legality of pragma SPARK_Mode when it appears at the + -- top of the visible declarations of a package spec, protected or + -- task unit declaration denoted by Decl. The routine is also used + -- on protected or task units declared without a definition. + + procedure Set_SPARK_Context; + -- Subsidiary to routines Process_xxx. Set the global variables + -- which represent the mode of the context from pragma N. Ensure + -- that Dynamic_Elaboration_Checks are off if the new mode is On. ------------------------------ -- Check_Pragma_Conformance -- @@ -19461,18 +19502,21 @@ package body Sem_Prag is procedure Check_Pragma_Conformance (Context_Pragma : Node_Id; - Entity_Pragma : Node_Id; - Entity : Entity_Id) + Entity : Entity_Id; + Entity_Pragma : Node_Id) is - Arg : Node_Id := Arg1; + Err_Id : Entity_Id; + Err_N : Node_Id; begin -- The current pragma may appear without an argument. If this -- is the case, associate all error messages with the pragma -- itself. - if No (Arg) then - Arg := N; + if Present (Arg1) then + Err_N := Arg1; + else + Err_N := N; end if; -- The mode of the current pragma is compared against that of @@ -19488,18 +19532,31 @@ package body Sem_Prag is and then Get_SPARK_Mode_From_Pragma (N) = On then Error_Msg_N - ("cannot change SPARK_Mode from Off to On", Arg); + ("cannot change SPARK_Mode from Off to On", Err_N); Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma); - Error_Msg_N ("\SPARK_Mode was set to Off#", Arg); + Error_Msg_N ("\SPARK_Mode was set to Off#", Err_N); raise Pragma_Exit; end if; end if; -- The mode of the current pragma is compared against that of - -- an initial package/subprogram declaration. + -- an initial package, protected type, subprogram or task type + -- declaration. if Present (Entity) then + -- A simple protected or task type is transformed into an + -- anonymous type whose name cannot be used to issue error + -- messages. Recover the original entity of the type. + + if Ekind_In (Entity, E_Protected_Type, E_Task_Type) then + Err_Id := + Defining_Entity + (Original_Node (Unit_Declaration_Node (Entity))); + else + Err_Id := Entity; + end if; + -- Both the initial declaration and the completion carry -- SPARK_Mode pragmas. @@ -19512,11 +19569,11 @@ package body Sem_Prag is if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off and then Get_SPARK_Mode_From_Pragma (N) = On then - Error_Msg_N ("incorrect use of SPARK_Mode", Arg); + Error_Msg_N ("incorrect use of SPARK_Mode", Err_N); Error_Msg_Sloc := Sloc (Entity_Pragma); Error_Msg_NE ("\value Off was set for SPARK_Mode on&#", - Arg, Entity); + Err_N, Err_Id); raise Pragma_Exit; end if; @@ -19525,11 +19582,11 @@ package body Sem_Prag is -- it cannot "complete". else - Error_Msg_N ("incorrect use of SPARK_Mode", Arg); - Error_Msg_Sloc := Sloc (Entity); + Error_Msg_N ("incorrect use of SPARK_Mode", Err_N); + Error_Msg_Sloc := Sloc (Err_Id); Error_Msg_NE ("\no value was set for SPARK_Mode on&#", - Arg, Entity); + Err_N, Err_Id); raise Pragma_Exit; end if; end if; @@ -19540,33 +19597,256 @@ package body Sem_Prag is -------------------------------- procedure Check_Library_Level_Entity (E : Entity_Id) is - MsgF : constant String := "incorrect placement of pragma%"; + procedure Add_Entity_To_Name_Buffer; + -- Add the E_Kind of entity E to the name buffer - begin - if not Is_Library_Level_Entity (E) then - Error_Msg_Name_1 := Pname; - Error_Msg_N (Fix_Error (MsgF), N); + ------------------------------- + -- Add_Entity_To_Name_Buffer -- + ------------------------------- - if Ekind_In (E, E_Generic_Package, - E_Package, - E_Package_Body) + procedure Add_Entity_To_Name_Buffer is + begin + if Ekind_In (E, E_Entry, E_Entry_Family) then + Add_Str_To_Name_Buffer ("entry"); + + elsif Ekind_In (E, E_Generic_Package, + E_Package, + E_Package_Body) then - Error_Msg_NE - ("\& is not a library-level package", N, E); + Add_Str_To_Name_Buffer ("package"); + + elsif Ekind_In (E, E_Protected_Body, E_Protected_Type) then + Add_Str_To_Name_Buffer ("protected unit"); + + elsif Ekind_In (E, E_Function, + E_Generic_Function, + E_Generic_Procedure, + E_Procedure, + E_Subprogram_Body) + then + Add_Str_To_Name_Buffer ("subprogram"); + else - Error_Msg_NE - ("\& is not a library-level subprogram", N, E); + pragma Assert (Ekind_In (E, E_Task_Body, E_Task_Type)); + Add_Str_To_Name_Buffer ("task unit"); end if; + end Add_Entity_To_Name_Buffer; + + -- Local variables + + Msg_1 : constant String := "incorrect placement of pragma%"; + Msg_2 : Name_Id; + + -- Start of processing for Check_Library_Level_Entity + + begin + if not Is_Library_Level_Entity (E) then + Error_Msg_Name_1 := Pname; + Error_Msg_N (Fix_Error (Msg_1), N); + + Name_Len := 0; + Add_Str_To_Name_Buffer ("\& is not a library-level "); + Add_Entity_To_Name_Buffer; + + Msg_2 := Name_Find; + Error_Msg_NE (Get_Name_String (Msg_2), N, E); raise Pragma_Exit; end if; end Check_Library_Level_Entity; - --------------------- - -- Set_SPARK_Flags -- - --------------------- + ------------------ + -- Process_Body -- + ------------------ + + procedure Process_Body (Decl : Node_Id) is + Body_Id : constant Entity_Id := Defining_Entity (Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Decl); - procedure Set_SPARK_Flags is + begin + -- Ignore pragma when applied to the special body created for + -- inlining, recognized by its internal name _Parent. + + if Chars (Body_Id) = Name_uParent then + return; + end if; + + Check_Library_Level_Entity (Body_Id); + + -- For entry bodies, verify the legality against: + -- * The mode of the context + -- * The mode of the spec (if any) + + if Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then + + -- A stand alone subprogram body + + if Body_Id = Spec_Id then + Check_Pragma_Conformance + (Context_Pragma => SPARK_Pragma (Body_Id), + Entity => Empty, + Entity_Pragma => Empty); + + -- An entry or subprogram body that completes a previous + -- declaration. + + else + Check_Pragma_Conformance + (Context_Pragma => SPARK_Pragma (Body_Id), + Entity => Spec_Id, + Entity_Pragma => SPARK_Pragma (Spec_Id)); + end if; + + Set_SPARK_Context; + Set_SPARK_Pragma (Body_Id, N); + Set_SPARK_Pragma_Inherited (Body_Id, False); + + -- For package bodies, verify the legality against: + -- * The mode of the context + -- * The mode of the private part + + -- This case is separated from protected and task bodies + -- because the statement part of the package body inherits + -- the mode of the body declarations. + + elsif Nkind (Decl) = N_Package_Body then + Check_Pragma_Conformance + (Context_Pragma => SPARK_Pragma (Body_Id), + Entity => Spec_Id, + Entity_Pragma => SPARK_Aux_Pragma (Spec_Id)); + + Set_SPARK_Context; + Set_SPARK_Pragma (Body_Id, N); + Set_SPARK_Pragma_Inherited (Body_Id, False); + Set_SPARK_Aux_Pragma (Body_Id, N); + Set_SPARK_Aux_Pragma_Inherited (Body_Id, True); + + -- For protected and task bodies, verify the legality against: + -- * The mode of the context + -- * The mode of the private part + + else + pragma Assert + (Nkind_In (Decl, N_Protected_Body, N_Task_Body)); + + Check_Pragma_Conformance + (Context_Pragma => SPARK_Pragma (Body_Id), + Entity => Spec_Id, + Entity_Pragma => SPARK_Aux_Pragma (Spec_Id)); + + Set_SPARK_Context; + Set_SPARK_Pragma (Body_Id, N); + Set_SPARK_Pragma_Inherited (Body_Id, False); + end if; + end Process_Body; + + -------------------------- + -- Process_Overloadable -- + -------------------------- + + procedure Process_Overloadable (Decl : Node_Id) is + Spec_Id : constant Entity_Id := Defining_Entity (Decl); + + begin + Check_Library_Level_Entity (Spec_Id); + + -- Verify the legality against: + -- * The mode of the context + + Check_Pragma_Conformance + (Context_Pragma => SPARK_Pragma (Spec_Id), + Entity => Empty, + Entity_Pragma => Empty); + + Set_SPARK_Pragma (Spec_Id, N); + Set_SPARK_Pragma_Inherited (Spec_Id, False); + end Process_Overloadable; + + -------------------------- + -- Process_Private_Part -- + -------------------------- + + procedure Process_Private_Part (Decl : Node_Id) is + Spec_Id : constant Entity_Id := Defining_Entity (Decl); + + begin + Check_Library_Level_Entity (Spec_Id); + + -- Verify the legality against: + -- * The mode of the visible declarations + + Check_Pragma_Conformance + (Context_Pragma => Empty, + Entity => Spec_Id, + Entity_Pragma => SPARK_Pragma (Spec_Id)); + + Set_SPARK_Context; + Set_SPARK_Aux_Pragma (Spec_Id, N); + Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False); + end Process_Private_Part; + + ---------------------------- + -- Process_Statement_Part -- + ---------------------------- + + procedure Process_Statement_Part (Decl : Node_Id) is + Body_Id : constant Entity_Id := Defining_Entity (Decl); + + begin + Check_Library_Level_Entity (Body_Id); + + -- Verify the legality against: + -- * The mode of the body declarations + + Check_Pragma_Conformance + (Context_Pragma => Empty, + Entity => Body_Id, + Entity_Pragma => SPARK_Pragma (Body_Id)); + + Set_SPARK_Context; + Set_SPARK_Aux_Pragma (Body_Id, N); + Set_SPARK_Aux_Pragma_Inherited (Body_Id, False); + end Process_Statement_Part; + + -------------------------- + -- Process_Visible_Part -- + -------------------------- + + procedure Process_Visible_Part (Decl : Node_Id) is + Spec_Id : constant Entity_Id := Defining_Entity (Decl); + + begin + Check_Library_Level_Entity (Spec_Id); + + -- Verify the legality against: + -- * The mode of the context + + Check_Pragma_Conformance + (Context_Pragma => SPARK_Pragma (Spec_Id), + Entity => Empty, + Entity_Pragma => Empty); + + -- A task unit declared without a definition does not set the + -- SPARK_Mode of the context because the task does not have any + -- entries that could inherit the mode. + + if not Nkind_In (Decl, N_Single_Task_Declaration, + N_Task_Type_Declaration) + then + Set_SPARK_Context; + end if; + + Set_SPARK_Pragma (Spec_Id, N); + Set_SPARK_Pragma_Inherited (Spec_Id, False); + Set_SPARK_Aux_Pragma (Spec_Id, N); + Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True); + end Process_Visible_Part; + + ----------------------- + -- Set_SPARK_Context -- + ----------------------- + + procedure Set_SPARK_Context is begin SPARK_Mode := Mode_Id; SPARK_Mode_Pragma := N; @@ -19574,14 +19854,12 @@ package body Sem_Prag is if SPARK_Mode = On then Dynamic_Elaboration_Checks := False; end if; - end Set_SPARK_Flags; + end Set_SPARK_Context; -- Local variables - Body_Id : Entity_Id; Context : Node_Id; Mode : Name_Id; - Spec_Id : Entity_Id; Stmt : Node_Id; -- Start of processing for Do_SPARK_Mode @@ -19624,7 +19902,7 @@ package body Sem_Prag is raise Pragma_Exit; end if; - Set_SPARK_Flags; + Set_SPARK_Context; -- The pragma acts as a configuration pragma in a compilation unit @@ -19635,7 +19913,7 @@ package body Sem_Prag is and then List_Containing (N) = Context_Items (Context) then Check_Valid_Configuration_Pragma; - Set_SPARK_Flags; + Set_SPARK_Context; -- Otherwise the placement of the pragma within the tree dictates -- its associated construct. Inspect the declarative list where @@ -19645,7 +19923,8 @@ package body Sem_Prag is Stmt := Prev (N); while Present (Stmt) loop - -- Skip prior pragmas, but check for duplicates + -- Skip prior pragmas, but check for duplicates. Note that + -- this also takes care of pragmas generated for aspects. if Nkind (Stmt) = N_Pragma then if Pragma_Name (Stmt) = Pname then @@ -19655,26 +19934,30 @@ package body Sem_Prag is raise Pragma_Exit; end if; - -- The pragma applies to a [generic] subprogram declaration. - -- Note that this case covers an internally generated spec - -- for a stand alone body. + -- The pragma applies to an expression function that has + -- already been rewritten into a subprogram declaration. - -- [generic] - -- procedure Proc ...; - -- pragma SPARK_Mode ..; + -- function Expr_Func return ... is (...); + -- pragma SPARK_Mode ...; - elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration, - N_Subprogram_Declaration) + elsif Nkind (Stmt) = N_Subprogram_Declaration + and then Nkind (Original_Node (Stmt)) = + N_Expression_Function then - Spec_Id := Defining_Entity (Stmt); - Check_Library_Level_Entity (Spec_Id); - Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Spec_Id), - Entity_Pragma => Empty, - Entity => Empty); + Process_Overloadable (Stmt); + return; + + -- The pragma applies to a task unit without a definition. + -- This also handles the case where a single task unit is + -- rewritten into a task type declaration. + + -- task [type] Tsk; + -- pragma SPARK_Mode ...; - Set_SPARK_Pragma (Spec_Id, N); - Set_SPARK_Pragma_Inherited (Spec_Id, False); + elsif Nkind_In (Stmt, N_Single_Task_Declaration, + N_Task_Type_Declaration) + then + Process_Visible_Part (Stmt); return; -- Skip internally generated code @@ -19682,6 +19965,25 @@ package body Sem_Prag is elsif not Comes_From_Source (Stmt) then null; + -- The pragma applies to an entry or [generic] subprogram + -- declaration. + + -- entry Ent ...; + -- pragma SPARK_Mode ...; + + -- [generic] + -- procedure Proc ...; + -- pragma SPARK_Mode ...; + + elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration, + N_Subprogram_Declaration) + or else (Nkind (Stmt) = N_Entry_Declaration + and then Is_Protected_Type + (Scope (Defining_Entity (Stmt)))) + then + Process_Overloadable (Stmt); + return; + -- Otherwise the pragma does not apply to a legal construct -- or it does not appear at the top of a declarative or a -- statement list. Issue an error and stop the analysis. @@ -19704,65 +20006,51 @@ package body Sem_Prag is Context := Unit (Parent (Context)); end if; - -- The pragma appears within package declarations - - if Nkind (Context) = N_Package_Specification then - Spec_Id := Defining_Entity (Context); - Check_Library_Level_Entity (Spec_Id); - - -- The pragma is at the top of the visible declarations - - -- package Pack is - -- pragma SPARK_Mode ...; + -- The pragma appears at the top of entry, package, protected + -- unit, subprogram or task unit body declarations. - if List_Containing (N) = Visible_Declarations (Context) then - Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Spec_Id), - Entity_Pragma => Empty, - Entity => Empty); - Set_SPARK_Flags; - - Set_SPARK_Pragma (Spec_Id, N); - Set_SPARK_Pragma_Inherited (Spec_Id, False); - Set_SPARK_Aux_Pragma (Spec_Id, N); - Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True); + -- entry Ent when ... is + -- pragma SPARK_Mode ...; - -- The pragma is at the top of the private declarations + -- package body Pack is + -- pragma SPARK_Mode ...; - -- package Pack is - -- private - -- pragma SPARK_Mode ...; + -- procedure Proc ... is + -- pragma SPARK_Mode; - else - Check_Pragma_Conformance - (Context_Pragma => Empty, - Entity_Pragma => SPARK_Pragma (Spec_Id), - Entity => Spec_Id); - Set_SPARK_Flags; + -- protected body Prot is + -- pragma SPARK_Mode ...; - Set_SPARK_Aux_Pragma (Spec_Id, N); - Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False); - end if; + if Nkind_In (Context, N_Entry_Body, + N_Package_Body, + N_Protected_Body, + N_Subprogram_Body, + N_Task_Body) + then + Process_Body (Context); - -- The pragma appears at the top of package body declarations + -- The pragma appears at the top of the visible or private + -- declaration of a package spec, protected or task unit. - -- package body Pack is + -- package Pack is + -- pragma SPARK_Mode ...; + -- private -- pragma SPARK_Mode ...; - elsif Nkind (Context) = N_Package_Body then - Spec_Id := Corresponding_Spec (Context); - Body_Id := Defining_Entity (Context); - Check_Library_Level_Entity (Body_Id); - Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Body_Id), - Entity_Pragma => SPARK_Aux_Pragma (Spec_Id), - Entity => Spec_Id); - Set_SPARK_Flags; + -- protected [type] Prot is + -- pragma SPARK_Mode ...; + -- private + -- pragma SPARK_Mode ...; - Set_SPARK_Pragma (Body_Id, N); - Set_SPARK_Pragma_Inherited (Body_Id, False); - Set_SPARK_Aux_Pragma (Body_Id, N); - Set_SPARK_Aux_Pragma_Inherited (Body_Id, True); + elsif Nkind_In (Context, N_Package_Specification, + N_Protected_Definition, + N_Task_Definition) + then + if List_Containing (N) = Visible_Declarations (Context) then + Process_Visible_Part (Parent (Context)); + else + Process_Private_Part (Parent (Context)); + end if; -- The pragma appears at the top of package body statements @@ -19773,18 +20061,7 @@ package body Sem_Prag is elsif Nkind (Context) = N_Handled_Sequence_Of_Statements and then Nkind (Parent (Context)) = N_Package_Body then - Context := Parent (Context); - Spec_Id := Corresponding_Spec (Context); - Body_Id := Defining_Entity (Context); - Check_Library_Level_Entity (Body_Id); - Check_Pragma_Conformance - (Context_Pragma => Empty, - Entity_Pragma => SPARK_Pragma (Body_Id), - Entity => Body_Id); - Set_SPARK_Flags; - - Set_SPARK_Aux_Pragma (Body_Id, N); - Set_SPARK_Aux_Pragma_Inherited (Body_Id, False); + Process_Statement_Part (Parent (Context)); -- The pragma appeared as an aspect of a [generic] subprogram -- declaration that acts as a compilation unit. @@ -19796,57 +20073,7 @@ package body Sem_Prag is elsif Nkind_In (Context, N_Generic_Subprogram_Declaration, N_Subprogram_Declaration) then - Spec_Id := Defining_Entity (Context); - Check_Library_Level_Entity (Spec_Id); - Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Spec_Id), - Entity_Pragma => Empty, - Entity => Empty); - - Set_SPARK_Pragma (Spec_Id, N); - Set_SPARK_Pragma_Inherited (Spec_Id, False); - - -- The pragma appears at the top of subprogram body - -- declarations. - - -- procedure Proc ... is - -- pragma SPARK_Mode; - - elsif Nkind (Context) = N_Subprogram_Body then - Spec_Id := Corresponding_Spec (Context); - Context := Specification (Context); - Body_Id := Defining_Entity (Context); - - -- Ignore pragma when applied to the special body created - -- for inlining, recognized by its internal name _Parent. - - if Chars (Body_Id) = Name_uParent then - return; - end if; - - Check_Library_Level_Entity (Body_Id); - - -- The body is a completion of a previous declaration - - if Present (Spec_Id) then - Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Body_Id), - Entity_Pragma => SPARK_Pragma (Spec_Id), - Entity => Spec_Id); - - -- The body acts as spec - - else - Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Body_Id), - Entity_Pragma => Empty, - Entity => Empty); - end if; - - Set_SPARK_Flags; - - Set_SPARK_Pragma (Body_Id, N); - Set_SPARK_Pragma_Inherited (Body_Id, False); + Process_Overloadable (Context); -- The pragma does not apply to a legal construct, issue error @@ -21559,7 +21786,7 @@ package body Sem_Prag is return; end if; - Spec_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id := Unique_Defining_Entity (Subp_Decl); if not Ekind_In (Spec_Id, E_Function, E_Generic_Function) then Pragma_Misplaced; @@ -22186,7 +22413,7 @@ package body Sem_Prag is -- Local variables Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; @@ -24864,7 +25091,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); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id); -- Preanalyze one of the optional arguments "Requires" or "Ensures" @@ -25845,7 +26072,7 @@ package body Sem_Prag is -- Local variables Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); Clause : Node_Id; Clauses : Node_Id; Depends : Node_Id; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 634b479..4a86c71 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -4766,27 +4766,6 @@ package body Sem_Util is end if; end Corresponding_Generic_Type; - --------------------------- - -- Corresponding_Spec_Of -- - --------------------------- - - function Corresponding_Spec_Of (Decl : Node_Id) return Entity_Id is - begin - if Nkind_In (Decl, N_Package_Body, N_Subprogram_Body) - and then Present (Corresponding_Spec (Decl)) - then - return Corresponding_Spec (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 (Decl); - - else - return Defining_Entity (Decl); - end if; - end Corresponding_Spec_Of; - -------------------- -- Current_Entity -- -------------------- @@ -19031,9 +19010,31 @@ package body Sem_Util is U := Full_View (E); end if; - when Type_Kind => - if Present (Full_View (E)) then - U := Full_View (E); + when Entry_Kind => + if Nkind (Parent (E)) = N_Entry_Body then + declare + Prot_Item : Entity_Id; + begin + -- Traverse the entity list of the protected type and locate + -- an entry declaration which matches the entry body. + + Prot_Item := First_Entity (Scope (E)); + while Present (Prot_Item) loop + if Ekind (Prot_Item) = E_Entry + and then Corresponding_Body (Parent (Prot_Item)) = E + then + U := Prot_Item; + exit; + end if; + + Next_Entity (Prot_Item); + end loop; + end; + end if; + + when Formal_Kind => + if Present (Spec_Entity (E)) then + U := Spec_Entity (E); end if; when E_Package_Body => @@ -19043,7 +19044,30 @@ package body Sem_Util is P := Parent (P); end if; - U := Corresponding_Spec (P); + if Nkind (P) = N_Package_Body + and then Present (Corresponding_Spec (P)) + then + U := Corresponding_Spec (P); + + elsif Nkind (P) = N_Package_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (P)) + then + U := Corresponding_Spec_Of_Stub (P); + end if; + + when E_Protected_Body => + P := Parent (E); + + if Nkind (P) = N_Protected_Body + and then Present (Corresponding_Spec (P)) + then + U := Corresponding_Spec (P); + + elsif Nkind (P) = N_Protected_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (P)) + then + U := Corresponding_Spec_Of_Stub (P); + end if; when E_Subprogram_Body => P := Parent (E); @@ -19054,48 +19078,34 @@ package body Sem_Util is P := Parent (P); - if Nkind (P) = N_Subprogram_Body_Stub then - if Present (Library_Unit (P)) then - - -- Get to the function or procedure (generic) entity through - -- the body entity. - - U := - Unique_Entity (Defining_Entity (Get_Body_From_Stub (P))); - end if; - else + if Nkind (P) = N_Subprogram_Body + and then Present (Corresponding_Spec (P)) + then U := Corresponding_Spec (P); - end if; - when Formal_Kind => - if Present (Spec_Entity (E)) then - U := Spec_Entity (E); + elsif Nkind (P) = N_Subprogram_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (P)) + then + U := Corresponding_Spec_Of_Stub (P); end if; when E_Task_Body => P := Parent (E); - U := Corresponding_Spec (P); - when E_Entry => - if Nkind (Parent (E)) = N_Entry_Body then - declare - Decl : Entity_Id := First_Entity (Scope (E)); - begin - -- Traverse the entity list of the protected object - -- and locate an entry declaration with a matching - -- Corresponding_Body. + if Nkind (P) = N_Task_Body + and then Present (Corresponding_Spec (P)) + then + U := Corresponding_Spec (P); - while Present (Decl) loop - if Ekind (Decl) = E_Entry - and then Corresponding_Body (Parent (Decl)) = E - then - U := Decl; - exit; - end if; - Next_Entity (Decl); - end loop; - pragma Assert (Present (Decl)); - end; + elsif Nkind (P) = N_Task_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (P)) + then + U := Corresponding_Spec_Of_Stub (P); + end if; + + when Type_Kind => + if Present (Full_View (E)) then + U := Full_View (E); end if; when others => diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index d7d08e6..2349252 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -413,10 +413,6 @@ package Sem_Util is -- attribute, except in the case of formal private and derived types. -- Possible optimization??? - 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. - function Current_Entity (N : Node_Id) return Entity_Id; pragma Inline (Current_Entity); -- Find the currently visible definition for a given identifier, that is to @@ -2092,12 +2088,13 @@ package Sem_Util is function Unique_Defining_Entity (N : Node_Id) return Entity_Id; -- Return the entity which represents declaration N, so that different -- views of the same entity have the same unique defining entity: - -- * package spec and body; - -- * subprogram declaration, subprogram stub and subprogram body; - -- * entry declaration and entry body; - -- * task declaration, task body stub and task body; - -- * private view and full view of a type; - -- * private view and full view of a deferred constant. + -- * entry declaration and entry body + -- * package spec and body + -- * protected type declaration, protected body stub and protected body + -- * private view and full view of a deferred constant + -- * private view and full view of a type + -- * subprogram declaration, subprogram stub and subprogram body + -- * task type declaration, task body stub and task body -- In other cases, return the defining entity for N. function Unique_Entity (E : Entity_Id) return Entity_Id; diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index 0fc3851..7f2d9a8 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -1848,7 +1848,8 @@ package body Sinfo is (N : Node_Id) return Boolean is begin pragma Assert (False - or else NT (N).Nkind = N_Subprogram_Body); + or else NT (N).Nkind = N_Subprogram_Body + or else NT (N).Nkind = N_Subprogram_Declaration); return Flag8 (N); end Is_Entry_Barrier_Function; @@ -2005,6 +2006,15 @@ package body Sinfo is return Flag6 (N); end Is_Task_Allocation_Block; + function Is_Task_Body_Procedure + (N : Node_Id) return Boolean is + begin + pragma Assert (False + or else NT (N).Nkind = N_Subprogram_Body + or else NT (N).Nkind = N_Subprogram_Declaration); + return Flag1 (N); + end Is_Task_Body_Procedure; + function Is_Task_Master (N : Node_Id) return Boolean is begin @@ -5069,7 +5079,8 @@ package body Sinfo is (N : Node_Id; Val : Boolean := True) is begin pragma Assert (False - or else NT (N).Nkind = N_Subprogram_Body); + or else NT (N).Nkind = N_Subprogram_Body + or else NT (N).Nkind = N_Subprogram_Declaration); Set_Flag8 (N, Val); end Set_Is_Entry_Barrier_Function; @@ -5226,6 +5237,15 @@ package body Sinfo is Set_Flag6 (N, Val); end Set_Is_Task_Allocation_Block; + procedure Set_Is_Task_Body_Procedure + (N : Node_Id; Val : Boolean := True) is + begin + pragma Assert (False + or else NT (N).Nkind = N_Subprogram_Body + or else NT (N).Nkind = N_Subprogram_Declaration); + Set_Flag1 (N, Val); + end Set_Is_Task_Body_Procedure; + procedure Set_Is_Task_Master (N : Node_Id; Val : Boolean := True) is begin diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 5f2f092..613ea4c6 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1571,7 +1571,7 @@ package Sinfo is -- concatenation nodes in instances. -- Is_Controlling_Actual (Flag16-Sem) - -- This flag is set on in an expression that is a controlling argument in + -- This flag is set on 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. @@ -1596,9 +1596,9 @@ package Sinfo is -- the enclosing object. -- Is_Entry_Barrier_Function (Flag8-Sem) - -- This flag is set in an N_Subprogram_Body node which is the expansion - -- of an entry barrier from a protected entry body. It is used for the - -- circuitry checking for incorrect use of Current_Task. + -- This flag is set on N_Subprogram_Declaration and N_Subprogram_Body + -- nodes which emulate the barrier function of a protected entry body. + -- The flag is used when checking for incorrect use of Current_Task. -- Is_Expanded_Build_In_Place_Call (Flag11-Sem) -- This flag is set in an N_Function_Call node to indicate that the extra @@ -1728,6 +1728,10 @@ package Sinfo is -- Expunge_Unactivated_Tasks to complete any tasks that have been -- allocated but not activated when the allocator completes abnormally. + -- Is_Task_Body_Procedure (Flag1-Sem) + -- This flag is set on N_Subprogram_Declaration and N_Subprogram_Body + -- nodes which emulate the body of a task unit. + -- Is_Task_Master (Flag5-Sem) -- A flag set in a Subprogram_Body, Block_Statement or Task_Body node to -- indicate that the construct is a task master (i.e. has declared tasks @@ -4953,6 +4957,8 @@ package Sinfo is -- Body_To_Inline (Node3-Sem) -- Corresponding_Body (Node5-Sem) -- Parent_Spec (Node4-Sem) + -- Is_Entry_Barrier_Function (Flag8-Sem) + -- Is_Task_Body_Procedure (Flag1-Sem) ------------------------------------------ -- 6.1 Abstract Subprogram Declaration -- @@ -5192,8 +5198,9 @@ package Sinfo is -- Acts_As_Spec (Flag4-Sem) -- Bad_Is_Detected (Flag15) used only by parser -- Do_Storage_Check (Flag17-Sem) - -- Is_Protected_Subprogram_Body (Flag7-Sem) -- Is_Entry_Barrier_Function (Flag8-Sem) + -- Is_Protected_Subprogram_Body (Flag7-Sem) + -- Is_Task_Body_Procedure (Flag1-Sem) -- Is_Task_Master (Flag5-Sem) -- Was_Originally_Stub (Flag13-Sem) -- Has_Relative_Deadline_Pragma (Flag9-Sem) @@ -9384,6 +9391,9 @@ package Sinfo is function Is_Task_Allocation_Block (N : Node_Id) return Boolean; -- Flag6 + function Is_Task_Body_Procedure + (N : Node_Id) return Boolean; -- Flag1 + function Is_Task_Master (N : Node_Id) return Boolean; -- Flag5 @@ -10413,6 +10423,9 @@ package Sinfo is procedure Set_Is_Task_Allocation_Block (N : Node_Id; Val : Boolean := True); -- Flag6 + procedure Set_Is_Task_Body_Procedure + (N : Node_Id; Val : Boolean := True); -- Flag1 + procedure Set_Is_Task_Master (N : Node_Id; Val : Boolean := True); -- Flag5 @@ -12780,6 +12793,7 @@ package Sinfo is pragma Inline (Is_Static_Expression); pragma Inline (Is_Subprogram_Descriptor); pragma Inline (Is_Task_Allocation_Block); + pragma Inline (Is_Task_Body_Procedure); pragma Inline (Is_Task_Master); pragma Inline (Iteration_Scheme); pragma Inline (Itype); @@ -13118,6 +13132,7 @@ package Sinfo is pragma Inline (Set_Is_Static_Expression); pragma Inline (Set_Is_Subprogram_Descriptor); pragma Inline (Set_Is_Task_Allocation_Block); + pragma Inline (Set_Is_Task_Body_Procedure); pragma Inline (Set_Is_Task_Master); pragma Inline (Set_Iteration_Scheme); pragma Inline (Set_Iterator_Specification); -- 2.7.4