From 378dc6ca34677edf03df66aee0581fe92eb1fb06 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 26 Oct 2015 16:34:11 +0100 Subject: [PATCH] [multiple changes] 2015-10-26 Hristian Kirtchev * atree.ads, atree.adb (Ekind_In): New 10 and 11 parameter versions. * contracts.ads, contracts.adb (Analyze_Initial_Declaration_Contract): New routine. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Analyze the contract of the initial declaration. (Analyze_Subprogram_Body_Helper): Analyze the contract of the initial declaration. * sem_ch7.adb (Analyze_Package_Body_Helper): Analyze the contract of the initial declaration. * sem_ch9.adb (Analyze_Entry_Body): Analyze the contract of the initial declaration. (Analyze_Protected_Body): Analyze the contract of the initial declaration. (Analyze_Task_Body): Analyze the contract of the initial declaration. * sem_prag.adb (Add_Entity_To_Name_Buffer): Use "type" rather than "unit" as it makes the error messages sound better. (Add_Item_To_Name_Buffer): Update comment on usage. The routine now supports discriminants and current instances of concurrent types. (Analyze_Depends_In_Decl_Part): Install the discriminants of a task type. (Analyze_Global_In_Decl_Part): Install the discriminants of a task type. (Analyze_Global_Item): Add processing for current instances of concurrent types and include discriminants as valid global items. (Analyze_Input_Output): Discriminants and current instances of concurrent types are now valid items. Update various error messages. (Check_Usage): Current instances of protected and task types behaves as formal parameters. (Collect_Subprogram_Inputs_Outputs): There is no longer need to manually analyze [Refined_]Global thanks to freezing of initial declaration contracts. Add processing for the current instance of a concurrent type. (Find_Role): Add categorizations for discriminants, protected and task types. (Is_CCT_Instance): New routine. (Match_Items): Update the comment on usage. Update internal comments. * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update the comment on usage. * sem_util.adb (Entity_Of): Ensure that the entity is an object when traversing a potential renaming chain. (Fix_Msg): Use "type" rather than "unit" as it makes the error messages sound better. * sem_util.ads (Fix_Msg): Update the comment on usage. 2015-10-26 Arnaud Charlet * par.adb (Par): Do not generate an error when generating SCIL for predefined units or new children of system and co. 2015-10-26 Ed Schonberg * einfo.adb: Access_Disp_Table applies to a private extension. From-SVN: r229373 --- gcc/ada/ChangeLog | 56 +++++++++ gcc/ada/atree.adb | 90 ++++++++++++++ gcc/ada/atree.ads | 54 +++++++++ gcc/ada/contracts.adb | 33 ++++++ gcc/ada/contracts.ads | 6 +- gcc/ada/einfo.adb | 1 + gcc/ada/par.adb | 3 + gcc/ada/sem_ch6.adb | 17 +++ gcc/ada/sem_ch7.adb | 8 ++ gcc/ada/sem_ch9.adb | 23 +++- gcc/ada/sem_prag.adb | 266 +++++++++++++++++++++++++++++++++++------- gcc/ada/sem_prag.ads | 5 +- gcc/ada/sem_util.adb | 7 +- gcc/ada/sem_util.ads | 2 +- 14 files changed, 521 insertions(+), 50 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 4806519dd2b..cec92831d62 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,59 @@ +2015-10-26 Hristian Kirtchev + + * atree.ads, atree.adb (Ekind_In): New 10 and 11 parameter versions. + * contracts.ads, contracts.adb (Analyze_Initial_Declaration_Contract): + New routine. + * sem_ch6.adb (Analyze_Generic_Subprogram_Body): + Analyze the contract of the initial declaration. + (Analyze_Subprogram_Body_Helper): Analyze the contract of the + initial declaration. + * sem_ch7.adb (Analyze_Package_Body_Helper): Analyze the contract + of the initial declaration. + * sem_ch9.adb (Analyze_Entry_Body): Analyze the contract of + the initial declaration. + (Analyze_Protected_Body): Analyze + the contract of the initial declaration. + (Analyze_Task_Body): Analyze the contract of the initial declaration. + * sem_prag.adb (Add_Entity_To_Name_Buffer): Use "type" rather + than "unit" as it makes the error messages sound better. + (Add_Item_To_Name_Buffer): Update comment on usage. The routine + now supports discriminants and current instances of concurrent + types. + (Analyze_Depends_In_Decl_Part): Install the discriminants + of a task type. + (Analyze_Global_In_Decl_Part): Install the discriminants of a task type. + (Analyze_Global_Item): Add processing for current instances of + concurrent types and include discriminants as valid global items. + (Analyze_Input_Output): Discriminants and current instances of + concurrent types are now valid items. Update various error messages. + (Check_Usage): Current instances of protected and task types behaves + as formal parameters. + (Collect_Subprogram_Inputs_Outputs): There is + no longer need to manually analyze [Refined_]Global thanks to + freezing of initial declaration contracts. Add processing for + the current instance of a concurrent type. + (Find_Role): Add categorizations for discriminants, protected and task + types. + (Is_CCT_Instance): New routine. + (Match_Items): Update the comment on usage. Update internal comments. + * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update the + comment on usage. + * sem_util.adb (Entity_Of): Ensure that the entity is an object + when traversing a potential renaming chain. + (Fix_Msg): Use "type" rather than "unit" as it makes the error messages + sound better. + * sem_util.ads (Fix_Msg): Update the comment on usage. + +2015-10-26 Arnaud Charlet + + * par.adb (Par): Do not generate an error when generating + SCIL for predefined units or new children of system and co. + +2015-10-26 Ed Schonberg + + * einfo.adb: Access_Disp_Table applies to a private + extension. + 2015-10-26 Ed Schonberg * sem_res.adb (Resolve_Generalized_Indexing): In ASIS mode, when diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 8df26b40e30..b03da914165 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -1125,6 +1125,60 @@ package body Atree is T = V9; end Ekind_In; + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8 or else + T = V9 or else + T = V10; + end Ekind_In; + + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind; + V11 : Entity_Kind) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8 or else + T = V9 or else + T = V10 or else + T = V11; + end Ekind_In; + function Ekind_In (E : Entity_Id; V1 : Entity_Kind; @@ -1225,6 +1279,42 @@ package body Atree is return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9); end Ekind_In; + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind) return Boolean + is + begin + return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9, V10); + end Ekind_In; + + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind; + V11 : Entity_Kind) return Boolean + is + begin + return + Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11); + end Ekind_In; + ------------------------ -- Set_Reporting_Proc -- ------------------------ diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 75939c68ed8..56763c74d27 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -802,6 +802,33 @@ package Atree is V8 : Entity_Kind; V9 : Entity_Kind) return Boolean; + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind) return Boolean; + + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind; + V11 : Entity_Kind) return Boolean; + function Ekind_In (T : Entity_Kind; V1 : Entity_Kind; @@ -870,6 +897,33 @@ package Atree is V8 : Entity_Kind; V9 : Entity_Kind) return Boolean; + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind) return Boolean; + + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind; + V10 : Entity_Kind; + V11 : Entity_Kind) return Boolean; + pragma Inline (Ekind_In); -- Inline all above functions diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 3e6258a11bb..30318dc63f6 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -578,6 +578,39 @@ package body Contracts is end if; end Analyze_Entry_Or_Subprogram_Contract; + ------------------------------------------ + -- Analyze_Initial_Declaration_Contract -- + ------------------------------------------ + + procedure Analyze_Initial_Declaration_Contract (Body_Decl : Node_Id) is + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); + + begin + -- Note that stubs are excluded because the compiler always analyzes the + -- proper body when a stub is encountered. + + if Nkind (Body_Decl) = N_Entry_Body then + Analyze_Entry_Or_Subprogram_Contract (Spec_Id); + + elsif Nkind (Body_Decl) = N_Package_Body then + Analyze_Package_Contract (Spec_Id); + + elsif Nkind (Body_Decl) = N_Protected_Body then + Analyze_Protected_Contract (Spec_Id); + + elsif Nkind (Body_Decl) = N_Subprogram_Body then + if Present (Corresponding_Spec (Body_Decl)) then + Analyze_Entry_Or_Subprogram_Contract (Spec_Id); + end if; + + elsif Nkind (Body_Decl) = N_Task_Body then + Analyze_Task_Contract (Spec_Id); + + else + raise Program_Error; + end if; + end Analyze_Initial_Declaration_Contract; + ----------------------------- -- Analyze_Object_Contract -- ----------------------------- diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index 96ea79f8b99..21c609d5b2a 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -58,7 +58,7 @@ package Contracts is -- Volatile_Function procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id); - -- Analyze the contract of the nearest package body (if any) enclosing + -- Analyze the contract of the nearest package body (if any) which encloses -- package or subprogram body Body_Decl. procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id); @@ -86,6 +86,10 @@ package Contracts is -- Precondition -- Test_Case + procedure Analyze_Initial_Declaration_Contract (Body_Decl : Node_Id); + -- Analyze the contract of the initial declaration of entry body, package + -- body, protected body, subprogram body or task body Body_Decl. + procedure Analyze_Object_Contract (Obj_Id : Entity_Id); -- Analyze all delayed pragmas chained on the contract of object Obj_Id as -- if they appeared at the end of the declarative region. The pragmas to be diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index b618047ce04..8769631e4c2 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -705,6 +705,7 @@ package body Einfo is function Access_Disp_Table (Id : E) return L is begin pragma Assert (Ekind_In (Id, E_Record_Type, + E_Record_Type_With_Private, E_Record_Subtype)); return Elist16 (Implementation_Base_Type (Id)); end Access_Disp_Table; diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index a4658bf6939..dc573876276 100644 --- a/gcc/ada/par.adb +++ b/gcc/ada/par.adb @@ -1577,11 +1577,14 @@ begin -- versions of these files. Another exception is System.RPC -- and its children. This allows a user to supply their own -- communication layer. + -- Similarly we do not generate an error in CodePeer mode + -- to allow users to analyze third party compier packages. if Comp_Unit_Node /= Error and then Operating_Mode = Generate_Code and then Current_Source_Unit = Main_Unit and then not GNAT_Mode + and then not CodePeer_Mode then declare Uname : constant String := diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 97d85200587..f6ecdcf5790 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1378,6 +1378,15 @@ package body Sem_Ch6 is Analyze_Aspect_Specifications_On_Body_Or_Stub (N); end if; + -- A generic subprogram body "freezes" the contract of its initial + -- declaration. This analysis depends on attribute Corresponding_Spec + -- being set. Only bodies coming from source should cause this type + -- of "freezing". + + if Comes_From_Source (N) then + Analyze_Initial_Declaration_Contract (N); + end if; + Analyze_Declarations (Declarations (N)); Check_Completion; @@ -3756,6 +3765,14 @@ package body Sem_Ch6 is Analyze_Aspect_Specifications_On_Body_Or_Stub (N); end if; + -- A subprogram body "freezes" the contract of its initial declaration. + -- This analysis depends on attribute Corresponding_Spec being set. Only + -- bodies coming from source should cause this type of "freezing". + + if Comes_From_Source (N) then + Analyze_Initial_Declaration_Contract (N); + end if; + Analyze_Declarations (Declarations (N)); -- Verify that the SPARK_Mode of the body agrees with that of its spec diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 1ebda333b6c..229d29dbe3a 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -763,6 +763,14 @@ package body Sem_Ch7 is Declare_Inherited_Private_Subprograms (Spec_Id); end if; + -- A package body "freezes" the contract of its initial declaration. + -- This analysis depends on attribute Corresponding_Spec being set. Only + -- bodies coming from source shuld cause this type of "freezing". + + if Comes_From_Source (N) then + Analyze_Initial_Declaration_Contract (N); + end if; + if Present (Declarations (N)) then Analyze_Declarations (Declarations (N)); Inspect_Deferred_Constant_Completion (Declarations (N)); diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index f3235dd52e4..2b3e42bf098 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -1354,6 +1354,11 @@ package body Sem_Ch9 is (Sloc (N), Entry_Name, P_Type, N, Decls); end if; + -- An entry body "freezes" the contract of its initial declaration. This + -- analysis depends on attribute Corresponding_Body being set. + + Analyze_Initial_Declaration_Contract (N); + if Present (Decls) then Analyze_Declarations (Decls); Inspect_Deferred_Constant_Completion (Decls); @@ -1811,11 +1816,14 @@ package body Sem_Ch9 is Set_Corresponding_Body (Parent (Spec_Id), Body_Id); Set_Has_Completion (Spec_Id); Install_Declarations (Spec_Id); - Expand_Protected_Body_Declarations (N, Spec_Id); - Last_E := Last_Entity (Spec_Id); + -- A protected body "freezes" the contract of its initial declaration. + -- This analysis depends on attribute Corresponding_Spec being set. + + Analyze_Initial_Declaration_Contract (N); + Analyze_Declarations (Declarations (N)); -- For visibility purposes, all entities in the body are private. Set @@ -2818,9 +2826,9 @@ package body Sem_Ch9 is 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. + -- body. This ensures that 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); @@ -2884,6 +2892,11 @@ package body Sem_Ch9 is Install_Declarations (Spec_Id); Last_E := Last_Entity (Spec_Id); + -- A task body "freezes" the contract of its initial declaration. This + -- analysis depends on attribute Corresponding_Spec being set. + + Analyze_Initial_Declaration_Contract (N); + Analyze_Declarations (Decls); Inspect_Deferred_Constant_Completion (Decls); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 912d75ecaf7..c7c3f377ba8 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -237,6 +237,11 @@ package body Sem_Prag is -- Determine whether dependency clause Clause is surrounded by extra -- parentheses. If this is the case, issue an error message. + function Is_CCT_Instance (Ref : Node_Id) return Boolean; + -- Subsidiary to the analysis of pragmas [Refined_]Depends and [Refined_] + -- Global. Determine whether reference Ref denotes the current instance of + -- a concurrent type. + function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean; -- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of -- pragma Depends. Determine whether the type of dependency item Item is @@ -520,11 +525,14 @@ package body Sem_Prag is -- to the name buffer. The individual kinds are as follows: -- E_Abstract_State - "state" -- E_Constant - "constant" + -- E_Discriminant - "discriminant" -- E_Generic_In_Out_Parameter - "generic parameter" -- E_Generic_Out_Parameter - "generic parameter" -- E_In_Parameter - "parameter" -- E_In_Out_Parameter - "parameter" -- E_Out_Parameter - "parameter" + -- E_Protected_Type - "current instance of protected type" + -- E_Task_Type - "current instance of task type" -- E_Variable - "global" procedure Analyze_Dependency_Clause @@ -571,6 +579,9 @@ package body Sem_Prag is elsif Ekind (Item_Id) = E_Constant then Add_Str_To_Name_Buffer ("constant"); + elsif Ekind (Item_Id) = E_Discriminant then + Add_Str_To_Name_Buffer ("discriminant"); + elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter, E_Generic_In_Parameter) then @@ -579,6 +590,12 @@ package body Sem_Prag is elsif Is_Formal (Item_Id) then Add_Str_To_Name_Buffer ("parameter"); + elsif Ekind (Item_Id) = E_Protected_Type then + Add_Str_To_Name_Buffer ("current instance of protected type"); + + elsif Ekind (Item_Id) = E_Task_Type then + Add_Str_To_Name_Buffer ("current instance of task type"); + elsif Ekind (Item_Id) = E_Variable then Add_Str_To_Name_Buffer ("global"); @@ -811,13 +828,27 @@ package body Sem_Prag is if Present (Item_Id) then if Ekind_In (Item_Id, E_Abstract_State, E_Constant, + E_Discriminant, E_Generic_In_Out_Parameter, E_Generic_In_Parameter, E_In_Parameter, E_In_Out_Parameter, E_Out_Parameter, + E_Protected_Type, + E_Task_Type, E_Variable) then + -- The item denotes a concurrent type, but it is not the + -- current instance of an enclosing concurrent type. + + if Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) + and then not Is_CCT_Instance (Item) + then + SPARK_Msg_N + ("invalid use of subtype mark in dependency " + & "relation", Item); + end if; + -- Ensure that the item fulfils its role as input and/or -- output as specified by pragma Global or the enclosing -- context. @@ -923,8 +954,8 @@ package body Sem_Prag is else SPARK_Msg_N - ("item must denote parameter, variable, or state", - Item); + ("item must denote parameter, variable, state or " + & "current instance of concurren type", Item); end if; -- All other input/output items are illegal @@ -932,7 +963,8 @@ package body Sem_Prag is else Error_Msg_N - ("item must denote parameter, variable, or state", Item); + ("item must denote parameter, variable, state or current " + & "instance of concurrent type", Item); end if; end if; end Analyze_Input_Output; @@ -1059,6 +1091,9 @@ package body Sem_Prag is elsif Ekind (Item_Id) = E_Constant then Item_Is_Input := True; + elsif Ekind (Item_Id) = E_Discriminant then + Item_Is_Input := True; + -- Generic parameter cases elsif Ekind (Item_Id) = E_Generic_In_Parameter then @@ -1098,6 +1133,29 @@ package body Sem_Prag is Item_Is_Output := True; end if; + -- Protected types + + elsif Ekind (Item_Id) = E_Protected_Type then + + -- A protected type acts as a formal parameter of mode IN when + -- it applies to a protected function. + + if Ekind (Spec_Id) = E_Function then + Item_Is_Input := True; + + -- Otherwise the protected type acts as a formal of mode IN OUT + + else + Item_Is_Input := True; + Item_Is_Output := True; + end if; + + -- Task types + + elsif Ekind (Item_Id) = E_Task_Type then + Item_Is_Input := True; + Item_Is_Output := True; + -- Variable case else pragma Assert (Ekind (Item_Id) = E_Variable); @@ -1303,7 +1361,12 @@ package body Sem_Prag is if Present (Item_Id) and then not Contains (Used_Items, Item_Id) then - if Is_Formal (Item_Id) then + -- The current instance of a concurrent type behaves as a + -- formal parameter (SPARK RM 6.1.4). + + if Is_Formal (Item_Id) + or else Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) + then Usage_Error (Item_Id); -- States and global objects are not used properly only when @@ -1658,9 +1721,13 @@ package body Sem_Prag is Push_Scope (Spec_Id); if Ekind (Spec_Id) = E_Task_Type then - null; + if Has_Discriminants (Spec_Id) then + Install_Discriminants (Spec_Id); + end if; + elsif Is_Generic_Subprogram (Spec_Id) then Install_Generic_Formals (Spec_Id); + else Install_Formals (Spec_Id); end if; @@ -1902,20 +1969,68 @@ package body Sem_Prag is return; end if; + -- A global item may denote a concurrent type as long as it is + -- the current instance of an enclosing concurrent type + -- (SPARK RM 6.1.4). + + elsif Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) then + if Is_CCT_Instance (Item) then + + -- Pragma [Refined_]Global associated with a protected + -- subprogram cannot mention the current instance of a + -- protected type because the instance behaves as a + -- formal parameter. + + if Ekind (Item_Id) = E_Protected_Type + and then Scope (Spec_Id) = Item_Id + then + Error_Msg_Name_1 := Chars (Item_Id); + SPARK_Msg_NE + (Fix_Msg (Spec_Id, "global item of subprogram & " + & "cannot reference current instance of protected " + & "type %"), Item, Spec_Id); + return; + + -- Pragma [Refined_]Global associated with a task type + -- cannot mention the current instance of a task type + -- because the instance behaves as a formal parameter. + + elsif Ekind (Item_Id) = E_Task_Type + and then Spec_Id = Item_Id + then + Error_Msg_Name_1 := Chars (Item_Id); + SPARK_Msg_NE + (Fix_Msg (Spec_Id, "global item of subprogram & " + & "cannot reference current instance of task type " + & "%"), Item, Spec_Id); + return; + end if; + + -- Otherwise the global item denotes a subtype mark that is + -- not a current instance. + + else + SPARK_Msg_N + ("invalid use of subtype mark in global list", Item); + return; + end if; + -- A formal object may act as a global item inside a generic elsif Is_Formal_Object (Item_Id) then null; - -- The only legal references are those to abstract states and - -- objects (SPARK RM 6.1.4(4)). + -- The only legal references are those to abstract states, + -- discriminants and objects (SPARK RM 6.1.4(4)). elsif not Ekind_In (Item_Id, E_Abstract_State, E_Constant, + E_Discriminant, E_Variable) then SPARK_Msg_N - ("global item must denote object or state", Item); + ("global item must denote object, state or current " + & "instance of concurrent type", Item); return; end if; @@ -1971,8 +2086,8 @@ package body Sem_Prag is elsif Ekind (Item_Id) = E_Constant then - -- A constant is read-only item, therefore it cannot act as - -- an output. + -- A constant is a read-only item, therefore it cannot act + -- as an output. if Nam_In (Global_Mode, Name_In_Out, Name_Output) then SPARK_Msg_NE @@ -1980,6 +2095,19 @@ package body Sem_Prag is return; end if; + -- Discriminant related checks + + elsif Ekind (Item_Id) = E_Discriminant then + + -- A discriminant is a read-only item, therefore it cannot + -- act as an output. + + if Nam_In (Global_Mode, Name_In_Out, Name_Output) then + SPARK_Msg_NE + ("discriminant & cannot act as output", Item, Item_Id); + return; + end if; + -- Variable related checks. These are only relevant when -- SPARK_Mode is on as they are not standard Ada legality -- rules. @@ -2025,7 +2153,9 @@ package body Sem_Prag is -- (SPARK RM 6.1.4(4)). else - Error_Msg_N ("global item must denote object or state", Item); + Error_Msg_N + ("global item must denote object, state or current instance " + & "of concurrent type", Item); return; end if; @@ -2286,9 +2416,13 @@ package body Sem_Prag is Push_Scope (Spec_Id); if Ekind (Spec_Id) = E_Task_Type then - null; + if Has_Discriminants (Spec_Id) then + Install_Discriminants (Spec_Id); + end if; + elsif Is_Generic_Subprogram (Spec_Id) then Install_Generic_Formals (Spec_Id); + else Install_Formals (Spec_Id); end if; @@ -20040,7 +20174,7 @@ package body Sem_Prag is Add_Str_To_Name_Buffer ("package"); elsif Ekind_In (E, E_Protected_Body, E_Protected_Type) then - Add_Str_To_Name_Buffer ("protected unit"); + Add_Str_To_Name_Buffer ("protected type"); elsif Ekind_In (E, E_Function, E_Generic_Function, @@ -20052,7 +20186,7 @@ package body Sem_Prag is else pragma Assert (Ekind_In (E, E_Task_Body, E_Task_Type)); - Add_Str_To_Name_Buffer ("task unit"); + Add_Str_To_Name_Buffer ("task type"); end if; end Add_Entity_To_Name_Buffer; @@ -23030,17 +23164,19 @@ package body Sem_Prag is -- 1) Both items denote null -- 2) Dep_Item denotes null and Ref_Item is Empty (special case) -- 3) Both items denote attribute 'Result - -- 4) Both items denote the same formal parameter - -- 5) Both items denote the same object - -- 6) Dep_Item is an abstract state with visible null refinement + -- 4) Both items denote the same object + -- 5) Both items denote the same formal parameter + -- 6) Both items denote the same current instance of a type + -- 7) Both items denote the same discriminant + -- 8) Dep_Item is an abstract state with visible null refinement -- and Ref_Item denotes null. - -- 7) Dep_Item is an abstract state with visible null refinement + -- 9) Dep_Item is an abstract state with visible null refinement -- and Ref_Item is Empty (special case). - -- 8) Dep_Item is an abstract state with visible non-null + -- 10) Dep_Item is an abstract state with visible non-null -- refinement and Ref_Item denotes one of its constituents. - -- 9) Dep_Item is an abstract state without a visible refinement + -- 11) Dep_Item is an abstract state without a visible refinement -- and Ref_Item denotes the same state. - -- When scenario 8 is in effect, the entity of the abstract state + -- When scenario 10 is in effect, the entity of the abstract state -- denoted by Dep_Item is added to list Refined_States. procedure Record_Item (Item_Id : Entity_Id); @@ -23127,7 +23263,8 @@ package body Sem_Prag is then Matched := True; - -- Abstract states, formal parameters and objects + -- Abstract states, current instances of concurrent types, + -- discriminants, formal parameters and objects. elsif Is_Entity_Name (Dep_Item) then @@ -23175,7 +23312,8 @@ package body Sem_Prag is Matched := True; end if; - -- A formal parameter or an object matches itself + -- A current instance of a concurrent type, discriminant, + -- formal parameter or an object matches itself. elsif Is_Entity_Name (Ref_Item) and then Entity_Of (Ref_Item) = Dep_Item_Id @@ -26364,7 +26502,7 @@ package body Sem_Prag is Depends : Node_Id; Formal : Entity_Id; Global : Node_Id; - List : Node_Id; + Typ : Entity_Id; -- Start of processing for Collect_Subprogram_Inputs_Outputs @@ -26425,21 +26563,7 @@ package body Sem_Prag is if Present (Global) then Global_Seen := True; - List := Expression (Get_Argument (Global, Spec_Id)); - - -- The pragma may not have been analyzed because of the arbitrary - -- declaration order of aspects. Make sure that it is analyzed for - -- the purposes of item extraction. - - if not Analyzed (List) then - if Pragma_Name (Global) = Name_Refined_Global then - Analyze_Refined_Global_In_Decl_Part (Global); - else - Analyze_Global_In_Decl_Part (Global); - end if; - end if; - - Collect_Global_List (List); + Collect_Global_List (Expression (Get_Argument (Global, Spec_Id))); -- When the related subprogram lacks pragma [Refined_]Global, fall back -- to [Refined_]Depends if the caller requests this behavior. Synthesize @@ -26463,6 +26587,45 @@ package body Sem_Prag is Collect_Dependency_Clause (Clauses); end if; end if; + + if Ekind (Scope (Spec_Id)) = E_Protected_Type then + Typ := Scope (Spec_Id); + + -- A single protected type declaration does not have a current + -- instance because the type is technically an object. + + if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then + null; + + -- Otherwise the current instance of the protected type acts as a + -- formal parameter of mode IN for functions and IN OUT for entries + -- and procedures (SPARK RM 6.1.4). + + else + Append_New_Elmt (Typ, Subp_Inputs); + + if Ekind_In (Spec_Id, E_Entry, E_Entry_Family, E_Procedure) then + Append_New_Elmt (Typ, Subp_Outputs); + end if; + end if; + + elsif Ekind (Spec_Id) = E_Task_Type then + Typ := Spec_Id; + + -- A single task type declaration does not have a current instance + -- because the type is technically an object. + + if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then + null; + + -- Otherwise the current instance of the task type acts as a formal + -- parameter of mode IN OUT (SPARK RM 6.1.4). + + else + Append_New_Elmt (Typ, Subp_Inputs); + Append_New_Elmt (Typ, Subp_Outputs); + end if; + end if; end Collect_Subprogram_Inputs_Outputs; --------------------------------- @@ -27022,6 +27185,31 @@ package body Sem_Prag is return Add_Config_Static_String (Arg); end Is_Config_Static_String; + --------------------- + -- Is_CCT_Instance -- + --------------------- + + function Is_CCT_Instance (Ref : Node_Id) return Boolean is + Ref_Id : constant Entity_Id := Entity (Ref); + S : Entity_Id; + + begin + -- Climb the scope chain looking for an enclosing concurrent type that + -- matches the referenced entity. + + S := Current_Scope; + while Present (S) and then S /= Standard_Standard loop + if Ekind_In (S, E_Protected_Type, E_Task_Type) and then S = Ref_Id + then + return True; + end if; + + S := Scope (S); + end loop; + + return False; + end Is_CCT_Instance; + ------------------------------- -- Is_Elaboration_SPARK_Mode -- ------------------------------- diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 784578a4da0..a4e0bd843c0 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -300,9 +300,10 @@ package Sem_Prag is -- and Subp_Outputs (outputs). The inputs and outputs are gathered from: -- 1) The formal parameters of the subprogram -- 2) The generic formal parameters of the generic subprogram - -- 3) The items of pragma [Refined_]Global + -- 3) The current instance of a concurrent type + -- 4) The items of pragma [Refined_]Global -- or - -- 4) The items of pragma [Refined_]Depends if there is no pragma + -- 5) The items of pragma [Refined_]Depends if there is no pragma -- [Refined_]Global present and flag Synthesize is set to True. -- If the subprogram has no inputs and/or outputs, then the returned list -- is No_Elist. Flag Global_Seen is set when the related subprogram has diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 01d6737551c..112c6e764ac 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -6347,7 +6347,10 @@ package body Sem_Util is -- Follow a possible chain of renamings to reach the root renamed -- object. - while Present (Id) and then Present (Renamed_Object (Id)) loop + while Present (Id) + and then Is_Object (Id) + and then Present (Renamed_Object (Id)) + loop if Is_Entity_Name (Renamed_Object (Id)) then Id := Entity (Renamed_Object (Id)); else @@ -7113,7 +7116,7 @@ package body Sem_Util is Res_Index := Res_Index + 5; elsif Is_Task then - Res (Res_Index .. Res_Index + 8) := "task unit"; + Res (Res_Index .. Res_Index + 8) := "task type"; Res_Index := Res_Index + 9; else diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 95534d948d7..67bc7f19403 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -770,7 +770,7 @@ package Sem_Util is -- the Ekind of Id as follows: -- * Replace "subprogram" with -- - "entry" when Id is an entry [family] - -- - "task unit" when Id is a single task object, task type or task + -- - "task type" when Id is a single task object, task type or task -- body. -- * Replace "protected" with -- - "task" when Id is a single task object, task type or task body -- 2.30.2