diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 144 | ||||
| -rw-r--r-- | gcc/ada/aspects.adb | 24 | ||||
| -rw-r--r-- | gcc/ada/aspects.ads | 34 | ||||
| -rw-r--r-- | gcc/ada/atree.adb | 17 | ||||
| -rw-r--r-- | gcc/ada/atree.ads | 6 | ||||
| -rw-r--r-- | gcc/ada/atree.h | 1 | ||||
| -rw-r--r-- | gcc/ada/contracts.adb | 249 | ||||
| -rw-r--r-- | gcc/ada/contracts.ads | 20 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 165 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 86 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/exp_ch7.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/freeze.adb | 19 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 51 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 35 | ||||
| -rw-r--r-- | gcc/ada/sem_ch9.adb | 219 | ||||
| -rw-r--r-- | gcc/ada/sem_elab.adb | 66 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 1033 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 28 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 512 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 69 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 1 |
22 files changed, 1962 insertions, 821 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 49aab44..f93439e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,147 @@ +2015-10-26 Bob Duff <duff@adacore.com> + + * exp_ch7.adb, exp_ch6.adb: Minor comment fix. + +2015-10-26 Hristian Kirtchev <kirtchev@adacore.com> + + * aspects.adb (Move_Or_Merge_Aspects): Move all aspects related + to a single concurrent type declaration to the declaration + of the anonymous object if they qualify. + (Relocate_Aspect): Update comment on usage. + * aspects.ads Add new sectioon on aspect specifications on single + concurrent types. Add new table Aspect_On_Anonymous_Object_OK. + (Move_Or_Merge_Aspects): Udate the comment on usage. + * atree.adb (Elist36): New routine. + (Set_Elist36): New routine. + * atree.ads (Elist36): New routine along with pragma Inline. + (Set_Elist36): New routine along with pragma Inline. + * atree.h: Elist36 is now an alias for Field36. + * contracts.adb (Add_Contract_Item): Add processing + for protected units and extra processing for variables. + (Analyze_Object_Contract): Code cleanup. The processing of + Part_Of now depends on wherer the object is a constant or + a variable. Add processing for pragmas Depends and Global + when they apply to a single concurrent object. Verify that a + variable which is part of a single concurrent type has full + default initialization. Set/restore the SPARK_Mode of a single + concurrent object. + (Analyze_Protected_Contract): New routine. + * contracts.ads (Add_Contract_Item): Update the comment on usage. + (Analyze_Object_Contract): Update the comment on usage. + (Analyze_Protected_Contract): New routine. + (Analyze_Task_Contract): Update the comment on usage. + * einfo.adb Part_Of_Constituents now uses Elist10. + (Anonymous_Object): New routine. + (Contract): Code cleanup. + (Has_Option): Remove the assumption that the only simple + option is External. + (Is_Synchronized_State): New routine. + (Part_Of_Constituents): This attribute applies to + variables and uses Elist10. + (Set_Anonymous_Object): New routine. + (Set_Contract): Code cleanup. + (Set_Part_Of_Constituents): This attribute applies to variables and + uses Elist10. + (Set_SPARK_Aux_Pragma): Code cleanup. + (Set_SPARK_Aux_Pragma_Inherited): Code cleanup. + (Set_SPARK_Pragma): Code cleanup. This attribute applies to + variables. + (Set_SPARK_Pragma_Inherited): Code cleanup. This + attribute applies to variables. + (SPARK_Aux_Pragma): Code cleanup. + (SPARK_Aux_Pragma_Inherited): Code cleanup. + (SPARK_Pragma): Code cleanup. This attribute applies to variables. + (SPARK_Pragma_Inherited): Code cleanup. This attribute applies + to variables. + (Write_Field9_Name): Remove the output for Part_Of_Constituents. + (Write_Field10_Name): Add output for Part_Of_Constituents. + (Write_Field30_Name): Add output for Anonymous_Object. + (Write_Field34_Name): Output SPARK_Pragma + for protected types and variables. + * einfo.ads: New attributes Anonymous_Object and + Is_Synchronized_State along with usage in entities. Update + the documentation of attributes Contract Encapsulating_State + Part_Of_Constituents SPARK_Aux_Pragma SPARK_Aux_Pragma_Inherited + SPARK_Pragma SPARK_Pragma_Inherited (Anonymous_Object): New + routine along with pragma Inline. + (Is_Synchronized_State): New routine. + (Set_Anonymous_Object): New routine along with pragma Inline. + * freeze.adb (Freeze_Record_Type): Ensure that a non-synchronized + record does not have synchronized components. + * sem_ch3.adb (Analyze_Declarations): Code cleanup. Analyze the + contract of protected units. + * sem_ch9.adb Add with and use clauses for Sem_Prag. Code cleanup. + (Analyze_Single_Protected_Declaration): Reimplemented. + (Analyze_Single_Task_Declaration): Reimplemented. + * sem_ch13.adb (Analyze_Aspect_Specifications): Aspect Part_Of + can now apply to a single concurrent type declaration. Rely on + Insert_Pragma to place the pragma. Update the error message on + usage to reflect the new context. + (Insert_Pragma): When inserting + pragmas for a protected or task type, create a definition if + the type lacks one. + * sem_elab.adb (Check_A_Call): Code cleanup. Issue error message + related to elaboration issues for SPARK when SPARK_Mode is "on" + and the offending entity comes from source. + * sem_prag.adb (Analyze_Abstract_State): Add new flag + Synchronous_Seen. Update the analysis of simple options Externa, + Ghost and Synchronous. Update various error messages to reflect + the use of single concurrent types. + (Analyze_Depends_Global): Pragmas Depends and Global can now apply to + a single task type or a single concurrent object created for a task + type. + (Analyze_Depends_In_Decl_Part): Do not push a scope when the + context is a single concurrent object. (Analyze_Part_Of): + Moved out of Analyze_Pragma. The routine has a new profile + and comment on usage. + (Analyze_Part_Of_In_Decl_Part): New routine. + (Analyze_Part_Of_Option): Update the call to Analyze_Part_Of. + (Analyze_Pragma): Pragma Abstract_State can + now carry simple option Synchronous. Pragma Part_Of can now + apply to a single concurrent type declaration. The analysis + of pragma Part_Of is delayed when the context is a single + concurrent object. + (Analyze_Refined_Depends_In_Decl_Part): Use the anonymous object when + the context is a single concurren type. + (Analyze_Refined_Global_In_Decl_Part): Use the + anonymous object when the context is a single concurren type. + (Check_Ghost_Constituent): Removed. + (Check_Matching_Constituent): Renamed to Match_Constituent. + (Check_Matching_State): Renamed to Match_State. + (Collect_Constituent): Update the comment + on usage. Verify various legality rules related to ghost and + synchronized entities. + (Find_Related_Declaration_Or_Body): A single task declaration is no + longer a valid context for a pragma. + (Fix_Msg): Moved to Sem_Util. + (Process_Overloadable): Add processing for single task objects. + (Process_Visible_Part): Add processing for single concurrent + types. + (Relocate_Pragmas_To_Anonymous_Object): New routine. + * sem_prag.ads Add new table Pragma_On_Anonymous_Object_OK. + (Analyze_Part_Of_In_Decl_Part): New routine. + (Relocate_Pragmas_To_Anonymous_Object): New routine. + * sem_util.adb (Defining_Entity): Code cleanup. + (Fix_Msg): Moved from Sem_Prag and augmented to handle + mode replacements. + (Has_Full_Default_Initialization): New routine. + (Is_Descendant_Of_Suspension_Object): Moved out of + Is_Effectively_Volatile. + (Is_Single_Concurrent_Object): New routine. + (Is_Single_Concurrent_Type): New routine. + (Is_Single_Concurrent_Type_Declaration): New routine. + (Is_Synchronized_Object): New routine. + (Yields_Synchronized_Object): New routine. + * sem_util.ads (Fix_Msg): Moved form Sem_Prag. Update the + comment on usage. + (Has_Full_Default_Initialization): New routine. + (Is_Single_Concurrent_Object): New routine. + (Is_Single_Concurrent_Type): New routine. + (Is_Single_Concurrent_Type_Declaration): New routine. + (Is_Synchronized_Object): New routine. + (Yields_Synchronized_Object): New routine. + * snames.ads-tmpl: Add name Synchronous. + 2015-10-26 Jerome Lambourg <lambourg@adacore.com> * sysdep.c (__gnat_get_task_options): Refine the workaround for diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index f42e9bf..e2bf1ea 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -338,8 +338,7 @@ package body Aspects is procedure Move_Or_Merge_Aspects (From : Node_Id; To : Node_Id) is procedure Relocate_Aspect (Asp : Node_Id); - -- Asp denotes an aspect specification of node From. Relocate the Asp to - -- the aspect specifications of node To (if any). + -- Move aspect specification Asp to the aspect specifications of node To --------------------- -- Relocate_Aspect -- @@ -360,8 +359,8 @@ package body Aspects is Set_Has_Aspects (To); end if; - -- Remove the aspect from node From's aspect specifications and - -- append it to node To. + -- Remove the aspect from its original owner and relocate it to node + -- To. Remove (Asp); Append (Asp, Asps); @@ -403,6 +402,23 @@ package body Aspects is Relocate_Aspect (Asp); end if; + -- When moving or merging aspects from a single concurrent type + -- declaration, relocate only those aspects that may apply to the + -- anonymous object created for the type. + + -- Note: It is better to use Is_Single_Concurrent_Type_Declaration + -- here, but Aspects and Sem_Util have incompatible licenses. + + elsif Nkind_In + (Original_Node (From), N_Single_Protected_Declaration, + N_Single_Task_Declaration) + then + Asp_Id := Get_Aspect_Id (Asp); + + if Aspect_On_Anonymous_Object_OK (Asp_Id) then + Relocate_Aspect (Asp); + end if; + -- Default case - relocate the aspect to its new owner else diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 8b7fca8..55c51a1 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -794,7 +794,7 @@ package Aspects is -- package body P with SPARK_Mode is ...; -- The table should be synchronized with Pragma_On_Body_Or_Stub_OK in unit - -- Sem_Prag if the aspects below are implemented by a pragma. + -- Sem_Prag. Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean := (Aspect_Refined_Depends => True, @@ -804,6 +804,26 @@ package Aspects is Aspect_Warnings => True, others => False); + ------------------------------------------------------------------- + -- Handling of Aspects Specifications on Single Concurrent Types -- + ------------------------------------------------------------------- + + -- Certain aspects that appear on the following nodes + + -- N_Single_Protected_Declaration + -- N_Single_Task_Declaration + + -- are treated as if they apply to the anonymous object produced by the + -- analysis of a single concurrent type. The following table lists all + -- aspects that should apply to the anonymous object. The table should + -- be synchronized with Pragma_On_Anonymous_Object_OK in unit Sem_Prag. + + Aspect_On_Anonymous_Object_OK : constant array (Aspect_Id) of Boolean := + (Aspect_Depends => True, + Aspect_Global => True, + Aspect_Part_Of => True, + others => False); + --------------------------------------------------- -- Handling of Aspect Specifications in the Tree -- --------------------------------------------------- @@ -861,10 +881,14 @@ package Aspects is procedure Move_Or_Merge_Aspects (From : Node_Id; To : Node_Id); -- Relocate the aspect specifications of node From to node To. If To has - -- aspects, the aspects of From are added to the aspects of To. If From has - -- no aspects, the routine has no effect. When From denotes a subprogram - -- body stub that also acts as a spec, the only aspects relocated to node - -- To are those from table Aspect_On_Body_Or_Stub_OK and preconditions. + -- aspects, the aspects of From are appended to the aspects of To. If From + -- has no aspects, the routine has no effect. Special behavior: + -- * When node From denotes a subprogram body stub without a previous + -- declaration, the only aspects relocated to node To are those found + -- in table Aspect_On_Body_Or_Stub_OK. + -- * When node From denotes a single synchronized type declaration, the + -- only aspects relocated to node To are those found in table + -- Aspect_On_Anonymous_Object_OK. function Permits_Aspect_Specifications (N : Node_Id) return Boolean; -- Returns True if the node N is a declaration node that permits aspect diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 973bdde..8df26b4 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -3103,6 +3103,17 @@ package body Atree is end if; end Elist26; + function Elist36 (N : Node_Id) return Elist_Id is + pragma Assert (Nkind (N) in N_Entity); + Value : constant Union_Id := Nodes.Table (N + 6).Field6; + begin + if Value = 0 then + return No_Elist; + else + return Elist_Id (Value); + end if; + end Elist36; + function Name1 (N : Node_Id) return Name_Id is begin pragma Assert (N <= Nodes.Last); @@ -5878,6 +5889,12 @@ package body Atree is Nodes.Table (N + 4).Field8 := Union_Id (Val); end Set_Elist26; + procedure Set_Elist36 (N : Node_Id; Val : Elist_Id) is + begin + pragma Assert (Nkind (N) in N_Entity); + Nodes.Table (N + 6).Field6 := Union_Id (Val); + end Set_Elist36; + procedure Set_Name1 (N : Node_Id; Val : Name_Id) is begin pragma Assert (N <= Nodes.Last); diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 0b4d245..75939c6 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -1412,6 +1412,9 @@ package Atree is function Elist26 (N : Node_Id) return Elist_Id; pragma Inline (Elist26); + function Elist36 (N : Node_Id) return Elist_Id; + pragma Inline (Elist36); + function Name1 (N : Node_Id) return Name_Id; pragma Inline (Name1); @@ -2769,6 +2772,9 @@ package Atree is procedure Set_Elist26 (N : Node_Id; Val : Elist_Id); pragma Inline (Set_Elist26); + procedure Set_Elist36 (N : Node_Id; Val : Elist_Id); + pragma Inline (Set_Elist36); + procedure Set_Name1 (N : Node_Id; Val : Name_Id); pragma Inline (Set_Name1); diff --git a/gcc/ada/atree.h b/gcc/ada/atree.h index adb636a..f92961e 100644 --- a/gcc/ada/atree.h +++ b/gcc/ada/atree.h @@ -525,6 +525,7 @@ extern Node_Id Current_Error_Node; #define Elist24(N) Field24 (N) #define Elist25(N) Field25 (N) #define Elist26(N) Field26 (N) +#define Elist36(N) Field36 (N) #define Name1(N) Field1 (N) #define Name2(N) Field2 (N) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 5ef6094..3e6258a 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -228,6 +228,19 @@ package body Contracts is raise Program_Error; end if; + -- Protected units, the applicable pragmas are: + -- Part_Of + + elsif Ekind (Id) = E_Protected_Type then + if Prag_Nam = Name_Part_Of then + Add_Classification; + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; + -- Subprogram bodies, the applicable pragmas are: -- Postcondition -- Precondition @@ -268,9 +281,10 @@ package body Contracts is -- Task units, the applicable pragmas are: -- Depends -- Global + -- Part_Of elsif Ekind (Id) = E_Task_Type then - if Nam_In (Prag_Nam, Name_Depends, Name_Global) then + if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then Add_Classification; -- The pragma is not a proper contract item @@ -283,16 +297,20 @@ package body Contracts is -- Async_Readers -- Async_Writers -- Constant_After_Elaboration + -- Depends -- Effective_Reads -- Effective_Writes + -- Global -- Part_Of elsif Ekind (Id) = E_Variable then if Nam_In (Prag_Nam, Name_Async_Readers, Name_Async_Writers, Name_Constant_After_Elaboration, + Name_Depends, Name_Effective_Reads, Name_Effective_Writes, + Name_Global, Name_Part_Of) then Add_Classification; @@ -565,14 +583,17 @@ package body Contracts is ----------------------------- procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is - Obj_Typ : constant Entity_Id := Etype (Obj_Id); - AR_Val : Boolean := False; - AW_Val : Boolean := False; - ER_Val : Boolean := False; - EW_Val : Boolean := False; - Items : Node_Id; - Prag : Node_Id; - Seen : Boolean := False; + Obj_Typ : constant Entity_Id := Etype (Obj_Id); + AR_Val : Boolean := False; + AW_Val : Boolean := False; + Encap_Id : Entity_Id; + ER_Val : Boolean := False; + EW_Val : Boolean := False; + Items : Node_Id; + Mode : SPARK_Mode_Type; + Prag : Node_Id; + Restore_Mode : Boolean := False; + Seen : Boolean := False; begin -- The loop parameter in an element iterator over a formal container @@ -612,10 +633,106 @@ package body Contracts is Error_Msg_N ("constant cannot be volatile", Obj_Id); end if; + Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); + + -- Check whether the lack of indicator Part_Of agrees with the + -- placement of the constant with respect to the state space. + + if No (Prag) then + Check_Missing_Part_Of (Obj_Id); + end if; + -- Variable-related checks else pragma Assert (Ekind (Obj_Id) = E_Variable); + -- The anonymous object created for a single concurrent type inherits + -- the SPARK_Mode from the type. Due to the timing of contract + -- analysis, delayed pragmas may be subject to the wrong SPARK_Mode, + -- usually that of the enclosing context. To remedy this, restore the + -- original SPARK_Mode of the related variable. + + if Is_Single_Concurrent_Object (Obj_Id) + and then Present (SPARK_Pragma (Obj_Id)) + then + Restore_Mode := True; + Save_SPARK_Mode_And_Set (Obj_Id, Mode); + end if; + + -- Analyze all external properties + + Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, AR_Val); + Seen := True; + end if; + + Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, AW_Val); + Seen := True; + end if; + + Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, ER_Val); + Seen := True; + end if; + + Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, EW_Val); + Seen := True; + end if; + + -- Verify the mutual interaction of the various external properties + + if Seen then + Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); + end if; + + -- The anonymous object created for a single concurrent type carries + -- pragmas Depends and Globat of the type. + + if Is_Single_Concurrent_Object (Obj_Id) then + + -- Analyze Global first, as Depends may mention items classified + -- in the global categorization. + + Prag := Get_Pragma (Obj_Id, Pragma_Global); + + if Present (Prag) then + Analyze_Global_In_Decl_Part (Prag); + end if; + + -- Depends must be analyzed after Global in order to see the modes + -- of all global items. + + Prag := Get_Pragma (Obj_Id, Pragma_Depends); + + if Present (Prag) then + Analyze_Depends_In_Decl_Part (Prag); + end if; + end if; + + Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); + + -- Analyze indicator Part_Of + + if Present (Prag) then + Analyze_Part_Of_In_Decl_Part (Prag); + + -- Otherwise check whether the lack of indicator Part_Of agrees with + -- the placement of the variable with respect to the state space. + + else + Check_Missing_Part_Of (Obj_Id); + end if; + -- The following checks are relevant only when SPARK_Mode is on, as -- they are not standard Ada legality rules. Internally generated -- temporaries are ignored. @@ -661,6 +778,28 @@ package body Contracts is Obj_Id); end if; end if; + + -- A variable whose Part_Of pragma specifies a single concurrent + -- type as encapsulator must be (SPARK RM 9.4): + -- * Of a type that defines full default initialization, or + -- * Declared with a default value, or + -- * Imported + + Encap_Id := Encapsulating_State (Obj_Id); + + if Present (Encap_Id) + and then Is_Single_Concurrent_Object (Encap_Id) + and then not Has_Full_Default_Initialization (Etype (Obj_Id)) + and then not Has_Initial_Value (Obj_Id) + and then not Is_Imported (Obj_Id) + then + Error_Msg_N ("& requires full default initialization", Obj_Id); + + Error_Msg_Name_1 := Chars (Encap_Id); + Error_Msg_N + (Fix_Msg (Encap_Id, "\object acts as constituent of single " + & "protected type %"), Obj_Id); + end if; end if; if Is_Ghost_Entity (Obj_Id) then @@ -680,50 +819,12 @@ package body Contracts is end if; end if; - -- Analyze all external properties - - Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, AR_Val); - Seen := True; - end if; - - Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, AW_Val); - Seen := True; + if Restore_Mode then + Restore_SPARK_Mode (Mode); end if; - - Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, ER_Val); - Seen := True; - end if; - - Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, EW_Val); - Seen := True; - end if; - - -- Verify the mutual interaction of the various external properties - - if Seen then - Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); - end if; - end if; - - -- Check whether the lack of indicator Part_Of agrees with the placement - -- of the object with respect to the state space. - - Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); - - if No (Prag) then - Check_Missing_Part_Of (Obj_Id); end if; -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One @@ -893,6 +994,50 @@ package body Contracts is end if; end Analyze_Package_Contract; + -------------------------------- + -- Analyze_Protected_Contract -- + -------------------------------- + + procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is + Items : constant Node_Id := Contract (Prot_Id); + Mode : SPARK_Mode_Type; + + begin + -- Do not analyze a contract multiple times + + if Present (Items) then + if Analyzed (Items) then + return; + else + Set_Analyzed (Items); + end if; + end if; + + -- Due to the timing of contract analysis, delayed pragmas may be + -- subject to the wrong SPARK_Mode, usually that of the enclosing + -- context. To remedy this, restore the original SPARK_Mode of the + -- related protected unit. + + Save_SPARK_Mode_And_Set (Prot_Id, Mode); + + -- A protected type must define full default initialization + -- (SPARK RM 9.4). This check is relevant only when SPARK_Mode is on as + -- it is not a standard Ada legality rule. + + if SPARK_Mode = On + and then not Has_Full_Default_Initialization (Prot_Id) + then + Error_Msg_N + ("protected type & must define full default initialization", + Prot_Id); + end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + Restore_SPARK_Mode (Mode); + end Analyze_Protected_Contract; + ------------------------------------------- -- Analyze_Subprogram_Body_Stub_Contract -- ------------------------------------------- @@ -949,7 +1094,7 @@ package body Contracts is -- Due to the timing of contract analysis, delayed pragmas may be -- subject to the wrong SPARK_Mode, usually that of the enclosing -- context. To remedy this, restore the original SPARK_Mode of the - -- related subprogram body. + -- related task unit. Save_SPARK_Mode_And_Set (Task_Id, Mode); diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index 3814dfc..96ea79f 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -32,8 +32,9 @@ package Contracts is procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id); -- Add pragma Prag to the contract of a constant, entry, entry family, - -- [generic] package, package body, [generic] subprogram, subprogram body, - -- variable or task unit denoted by Id. The following are valid pragmas: + -- [generic] package, package body, protected unit, [generic] subprogram, + -- subprogram body, variable or task unit denoted by Id. The following are + -- valid pragmas: -- Abstract_State -- Async_Readers -- Async_Writers @@ -91,8 +92,10 @@ package Contracts is -- considered are: -- Async_Readers -- Async_Writers + -- Depends (single concurrent object) -- Effective_Reads -- Effective_Writes + -- Global (single concurrent object) -- Part_Of procedure Analyze_Package_Body_Contract @@ -114,8 +117,13 @@ package Contracts is -- Initializes -- Part_Of + procedure Analyze_Protected_Contract (Prot_Id : Entity_Id); + -- Analyze all delayed pragmas chained on the contract of protected unit + -- Prot_Id if they appeared at the end of a declarative region. Currently + -- there are no such pragmas. + procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id); - -- Analyze all delayed pragmas chained on the contract of a subprogram body + -- Analyze all delayed pragmas chained on the contract of subprogram body -- stub Stub_Id as if they appeared at the end of a declarative region. The -- pragmas in question are: -- Contract_Cases @@ -129,9 +137,9 @@ package Contracts is -- Test_Case procedure Analyze_Task_Contract (Task_Id : Entity_Id); - -- Analyze all delayed pragmas chained on the contract of a task unit - -- Task_Id as if they appeared at the end of a declarative region. The - -- pragmas in question are: + -- Analyze all delayed pragmas chained on the contract of task unit Task_Id + -- as if they appeared at the end of a declarative region. The pragmas in + -- question are: -- Depends -- Global diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 930e18e..b618047 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -86,7 +86,6 @@ package body Einfo is -- Class_Wide_Type Node9 -- Current_Value Node9 - -- Part_Of_Constituents Elist9 -- Renaming_Map Uint9 -- Direct_Primitive_Operations Elist10 @@ -94,6 +93,7 @@ package body Einfo is -- Float_Rep Uint10 (but returns Float_Rep_Kind) -- Handler_Records List10 -- Normalized_Position_Max Uint10 + -- Part_Of_Constituents Elist10 -- Component_Bit_Offset Uint11 -- Full_View Node11 @@ -246,6 +246,7 @@ package body Einfo is -- BIP_Initialization_Call Node29 -- Subprograms_For_Type Node29 + -- Anonymous_Object Node30 -- Corresponding_Equality Node30 -- Last_Aggregate_Assignment Node30 -- Static_Initialization Node30 @@ -661,13 +662,7 @@ package body Einfo is Opt := First (Expressions (Decl)); while Present (Opt) loop - - -- Currently the only simple option allowed is External - - if Nkind (Opt) = N_Identifier - and then Chars (Opt) = Name_External - and then Chars (Opt) = Option_Nam - then + if Nkind (Opt) = N_Identifier and then Chars (Opt) = Option_Nam then return True; end if; @@ -766,6 +761,12 @@ package body Einfo is return Node36 (Id); end Anonymous_Master; + function Anonymous_Object (Id : E) return E is + begin + pragma Assert (Ekind_In (Id, E_Protected_Type, E_Task_Type)); + return Node30 (Id); + end Anonymous_Object; + function Associated_Entity (Id : E) return E is begin return Node37 (Id); @@ -1205,7 +1206,11 @@ package body Einfo is function Contract (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Constant, -- object variants + (Ekind_In (Id, E_Protected_Type, -- concurrent variants + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Constant, -- object variants E_Variable) or else Ekind_In (Id, E_Entry, -- overloadable variants @@ -1221,9 +1226,7 @@ package body Einfo is E_Package, E_Package_Body) or else - Ekind_In (Id, E_Task_Body, -- synchronized variants - E_Task_Type, - E_Void)); -- special purpose + Ekind (Id) = E_Void); -- special purpose return Node34 (Id); end Contract; @@ -2847,8 +2850,8 @@ package body Einfo is function Part_Of_Constituents (Id : E) return L is begin - pragma Assert (Ekind (Id) = E_Abstract_State); - return Elist9 (Id); + pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); + return Elist10 (Id); end Part_Of_Constituents; function Partial_View_Has_Unknown_Discr (Id : E) return B is @@ -3113,31 +3116,36 @@ package body Einfo is function SPARK_Aux_Pragma (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Generic_Package, -- package variants - E_Package, - E_Package_Body) + (Ekind_In (Id, E_Protected_Type, -- concurrent variants + E_Task_Type) or else - Ekind_In (Id, E_Protected_Type, -- synchronized variants - E_Task_Type)); + Ekind_In (Id, E_Generic_Package, -- package variants + E_Package, + E_Package_Body)); return Node41 (Id); end SPARK_Aux_Pragma; function SPARK_Aux_Pragma_Inherited (Id : E) return B is begin pragma Assert - (Ekind_In (Id, E_Generic_Package, -- package variants - E_Package, - E_Package_Body) + (Ekind_In (Id, E_Protected_Type, -- concurrent variants + E_Task_Type) or else - Ekind_In (Id, E_Protected_Type, -- synchronized variants - E_Task_Type)); + Ekind_In (Id, E_Generic_Package, -- package variants + E_Package, + E_Package_Body)); return Flag266 (Id); end SPARK_Aux_Pragma_Inherited; function SPARK_Pragma (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Entry, -- overloadable variants + (Ekind_In (Id, E_Protected_Body, -- concurrent variants + E_Protected_Type, + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Entry, -- overloadable variants E_Entry_Family, E_Function, E_Generic_Function, @@ -3150,17 +3158,19 @@ package body Einfo is E_Package, E_Package_Body) or else - Ekind_In (Id, E_Protected_Body, -- synchronized variants - E_Protected_Type, - E_Task_Body, - E_Task_Type)); + Ekind (Id) = E_Variable); -- variable return Node40 (Id); end SPARK_Pragma; function SPARK_Pragma_Inherited (Id : E) return B is begin pragma Assert - (Ekind_In (Id, E_Entry, -- overloadable variants + (Ekind_In (Id, E_Protected_Body, -- concurrent variants + E_Protected_Type, + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Entry, -- overloadable variants E_Entry_Family, E_Function, E_Generic_Function, @@ -3173,10 +3183,7 @@ package body Einfo is E_Package, E_Package_Body) or else - Ekind_In (Id, E_Protected_Body, -- synchronized variants - E_Protected_Type, - E_Task_Body, - E_Task_Type)); + Ekind (Id) = E_Variable); -- variable return Flag265 (Id); end SPARK_Pragma_Inherited; @@ -3648,6 +3655,12 @@ package body Einfo is Set_Node36 (Id, V); end Set_Anonymous_Master; + procedure Set_Anonymous_Object (Id : E; V : E) is + begin + pragma Assert (Ekind_In (Id, E_Protected_Type, E_Task_Type)); + Set_Node30 (Id, V); + end Set_Anonymous_Object; + procedure Set_Associated_Entity (Id : E; V : E) is begin Set_Node37 (Id, V); @@ -3839,7 +3852,11 @@ package body Einfo is procedure Set_Contract (Id : E; V : N) is begin pragma Assert - (Ekind_In (Id, E_Constant, -- object variants + (Ekind_In (Id, E_Protected_Type, -- concurrent variants + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Constant, -- object variants E_Variable) or else Ekind_In (Id, E_Entry, -- overloadable variants @@ -3855,9 +3872,7 @@ package body Einfo is E_Package, E_Package_Body) or else - Ekind_In (Id, E_Task_Body, -- synchronized variants - E_Task_Type, - E_Void)); -- special purpose + Ekind (Id) = E_Void); -- special purpose Set_Node34 (Id, V); end Set_Contract; @@ -5871,8 +5886,8 @@ package body Einfo is procedure Set_Part_Of_Constituents (Id : E; V : L) is begin - pragma Assert (Ekind (Id) = E_Abstract_State); - Set_Elist9 (Id, V); + pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable)); + Set_Elist10 (Id, V); end Set_Part_Of_Constituents; procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True) is @@ -6149,31 +6164,36 @@ package body Einfo is procedure Set_SPARK_Aux_Pragma (Id : E; V : N) is begin pragma Assert - (Ekind_In (Id, E_Generic_Package, -- package variants - E_Package, - E_Package_Body) + (Ekind_In (Id, E_Protected_Type, -- concurrent variants + E_Task_Type) or else - Ekind_In (Id, E_Protected_Type, -- synchronized variants - E_Task_Type)); + Ekind_In (Id, E_Generic_Package, -- package variants + E_Package, + E_Package_Body)); Set_Node41 (Id, V); end Set_SPARK_Aux_Pragma; procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is begin pragma Assert - (Ekind_In (Id, E_Generic_Package, -- package variants - E_Package, - E_Package_Body) + (Ekind_In (Id, E_Protected_Type, -- concurrent variants + E_Task_Type) or else - Ekind_In (Id, E_Protected_Type, -- synchronized variants - E_Task_Type)); + Ekind_In (Id, E_Generic_Package, -- package variants + E_Package, + E_Package_Body)); 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_Entry, -- overloadable variants + (Ekind_In (Id, E_Protected_Body, -- concurrent variants + E_Protected_Type, + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Entry, -- overloadable variants E_Entry_Family, E_Function, E_Generic_Function, @@ -6186,17 +6206,19 @@ package body Einfo is E_Package, E_Package_Body) or else - Ekind_In (Id, E_Protected_Body, -- synchronized variants - E_Protected_Type, - E_Task_Body, - E_Task_Type)); + Ekind (Id) = E_Variable); -- variable 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_Entry, -- overloadable variants + (Ekind_In (Id, E_Protected_Body, -- concurrent variants + E_Protected_Type, + E_Task_Body, + E_Task_Type) + or else + Ekind_In (Id, E_Entry, -- overloadable variants E_Entry_Family, E_Function, E_Generic_Function, @@ -6209,10 +6231,7 @@ package body Einfo is E_Package, E_Package_Body) or else - Ekind_In (Id, E_Protected_Body, -- synchronized variants - E_Protected_Type, - E_Task_Body, - E_Task_Type)); + Ekind (Id) = E_Variable); -- variable Set_Flag265 (Id, V); end Set_SPARK_Pragma_Inherited; @@ -7744,6 +7763,17 @@ package body Einfo is end if; end Is_Synchronized_Interface; + --------------------------- + -- Is_Synchronized_State -- + --------------------------- + + function Is_Synchronized_State (Id : E) return B is + begin + return + Ekind (Id) = E_Abstract_State + and then Has_Option (Id, Name_Synchronous); + end Is_Synchronized_State; + ----------------------- -- Is_Task_Interface -- ----------------------- @@ -9249,9 +9279,6 @@ package body Einfo is when Object_Kind => Write_Str ("Current_Value"); - when E_Abstract_State => - Write_Str ("Part_Of_Constituents"); - when E_Function | E_Generic_Function | E_Generic_Package | @@ -9297,6 +9324,10 @@ package body Einfo is E_Discriminant => Write_Str ("Normalized_Position_Max"); + when E_Abstract_State | + E_Variable => + Write_Str ("Part_Of_Constituents"); + when others => Write_Str ("Field10??"); end case; @@ -10134,6 +10165,10 @@ package body Einfo is procedure Write_Field30_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Protected_Type | + E_Task_Type => + Write_Str ("Anonymous_Object"); + when E_Function => Write_Str ("Corresponding_Equality"); @@ -10232,6 +10267,7 @@ package body Einfo is E_Package | E_Package_Body | E_Procedure | + E_Protected_Type | E_Subprogram_Body | E_Task_Body | E_Task_Type | @@ -10342,7 +10378,8 @@ package body Einfo is E_Protected_Type | E_Subprogram_Body | E_Task_Body | - E_Task_Type => + E_Task_Type | + E_Variable => Write_Str ("SPARK_Pragma"); when others => diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index ae4ad47..8b91ee4 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -444,6 +444,10 @@ package Einfo is -- finalization master that services most anonymous access-to-controlled -- allocations that occur within the unit. +-- Anonymous_Object (Node30) +-- Present in protected and task type entities. Contains the entity of +-- the anonymous object created for a single protected or task type. + -- Associated_Entity (Node37) -- Defined in all entities. This field is similar to Associated_Node, but -- applied to entities. The attribute links an entity from the generic @@ -706,9 +710,9 @@ package Einfo is -- Contract (Node34) -- Defined in constant, entry, entry family, operator, [generic] package, --- package body, [generic] subprogram, subprogram body, variable and task --- type entities. Points to the contract of the entity, holding various --- assertion items and data classifiers. +-- package body, protected type, [generic] subprogram, subprogram body, +-- variable and task type entities. Points to the contract of the entity, +-- holding various assertion items and data classifiers. -- Corresponding_Concurrent_Type (Node18) -- Defined in record types that are constructed by the expander to @@ -1074,9 +1078,9 @@ package Einfo is -- need to set the flag. -- Encapsulating_State (Node32) --- Defined in abstract states, constants and variables. Contains the --- entity of an ancestor state whose refinement utilizes this item as --- a constituent. +-- Defined in abstract state, constant and variable entities. Contains +-- the entity of an ancestor state or a single concurrent type whose +-- refinement utilizes this item as a constituent. -- Enclosing_Scope (Node18) -- Defined in labels. Denotes the innermost enclosing construct that @@ -3080,6 +3084,10 @@ package Einfo is -- synchronized, task, or protected, or is derived from a synchronized -- interface. +-- Is_Synchronized_State (synthesized) +-- Applies to all entities, true for abstract states that are subject to +-- option Synchronous. + -- Is_Tag (Flag78) -- Defined in E_Component and E_Constant entities. For regular tagged -- type this flag is set on the tag component (whose name is Name_uTag). @@ -3675,9 +3683,10 @@ package Einfo is -- case it points to the subtype of the parent type. This is the type -- that is used as the Etype of the _parent field. --- Part_Of_Constituents (Elist9) --- Present in abstract state entities. Contains all constituents that are --- subject to indicator Part_Of (both aspect and option variants). +-- Part_Of_Constituents (Elist10) +-- Present in abstract state and variable entities. Contains all +-- constituents that are subject to indicator Part_Of (both aspect and +-- option variants). -- Partial_View_Has_Unknown_Discr (Flag280) -- Present in all types. Set to Indicate that the partial view of a type @@ -4064,36 +4073,36 @@ package Einfo is -- as computed (as a power of two) by the compiler. -- 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 +-- Present in concurrent type, [generic] package spec and package body +-- entities. For concurrent types and package specs 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 [generic] package specs, package bodies and synchronized --- types. Set if the SPARK_Aux_Pragma field points to a pragma that is +-- Present in concurrent type, [generic] package spec and package body +-- entities. 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, operators, [generic] packages, package bodies, --- [generic] subprograms, subprogram bodies and synchronized types. --- Points to the N_Pragma node that applies to the spec or body. This --- is either set by a local SPARK_Mode pragma or is inherited from the --- context (from an outer scope for the spec case or from the spec for --- the body case). In the case where it is inherited the flag --- SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma is --- applicable. +-- Present in concurrent type, entry, operator, [generic] package, +-- package body, [generic] subprogram, subprogram body and variable +-- entities. Points to the N_Pragma node that applies to the initial +-- declaration or body. This is either set by a local SPARK_Mode pragma +-- or is inherited from the context (from an outer scope for the spec +-- case or from the spec for the body case). In the case where it is +-- inherited the flag SPARK_Pragma_Inherited is set. Empty if no +-- SPARK_Mode pragma is applicable. -- SPARK_Pragma_Inherited (Flag265) --- Present in entries, operators, [generic] packages, package bodies, --- [generic] subprograms, subprogram bodies and synchronized types. Set --- if the SPARK_Pragma attribute points to a pragma that is inherited, --- rather than a local one. +-- Present in concurrent type, entry, operator, [generic] package, +-- package body, [generic] subprogram, subprogram body and variable +-- entities. 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 @@ -5507,7 +5516,7 @@ package Einfo is -- E_Abstract_State -- Refinement_Constituents (Elist8) - -- Part_Of_Constituents (Elist9) + -- Part_Of_Constituents (Elist10) -- Body_References (Elist16) -- Non_Limited_View (Node19) -- Encapsulating_State (Node32) @@ -5518,6 +5527,7 @@ package Einfo is -- Has_Null_Refinement (synth) -- Is_External_State (synth) -- Is_Null_State (synth) + -- Is_Synchronized_State (synth) -- E_Access_Protected_Subprogram_Type -- Equivalent_Type (Node18) @@ -6248,6 +6258,8 @@ package Einfo is -- Discriminant_Constraint (Elist21) -- Scope_Depth_Value (Uint22) -- Stored_Constraint (Elist23) + -- Anonymous_Object (Node30) + -- Contract (Node34) -- SPARK_Pragma (Node40) -- SPARK_Aux_Pragma (Node41) -- Sec_Stack_Needed_For_Return (Flag167) ??? @@ -6261,6 +6273,7 @@ package Einfo is -- Has_Interrupt_Handler (synth) -- Number_Entries (synth) -- Scope_Depth (synth) + -- (plus type attributes) -- E_Record_Type -- E_Record_Subtype @@ -6389,11 +6402,11 @@ package Einfo is -- Last_Entity (Node20) -- Discriminant_Constraint (Elist21) -- Scope_Depth_Value (Uint22) - -- Scope_Depth (synth) -- Stored_Constraint (Elist23) -- Task_Body_Procedure (Node25) -- Storage_Size_Variable (Node26) (base type only) -- Relative_Deadline_Variable (Node28) (base type only) + -- Anonymous_Object (Node30) -- Contract (Node34) -- SPARK_Pragma (Node40) -- SPARK_Aux_Pragma (Node41) @@ -6408,11 +6421,13 @@ package Einfo is -- First_Component_Or_Discriminant (synth) -- Has_Entries (synth) -- Number_Entries (synth) + -- Scope_Depth (synth) -- (plus type attributes) -- E_Variable -- Hiding_Loop_Variable (Node8) -- Current_Value (Node9) + -- Part_Of_Constituents (Elist10) -- Esize (Uint12) -- Extra_Accessibility (Node13) -- Alignment (Uint14) @@ -6436,6 +6451,7 @@ package Einfo is -- Encapsulating_State (Node32) -- Linker_Section_Pragma (Node33) -- Contract (Node34) + -- SPARK_Pragma (Node40) -- Has_Alignment_Clause (Flag46) -- Has_Atomic_Components (Flag86) -- Has_Biased_Representation (Flag139) @@ -6457,6 +6473,7 @@ package Einfo is -- OK_To_Rename (Flag247) -- Optimize_Alignment_Space (Flag241) -- Optimize_Alignment_Time (Flag242) + -- SPARK_Pragma_Inherited (Flag265) -- Suppress_Initialization (Flag105) -- Treat_As_Volatile (Flag41) -- Address_Clause (synth) @@ -6707,6 +6724,7 @@ package Einfo is function Alias (Id : E) return E; function Alignment (Id : E) return U; function Anonymous_Master (Id : E) return E; + function Anonymous_Object (Id : E) return E; function Associated_Entity (Id : E) return E; function Associated_Formal_Package (Id : E) return E; function Associated_Node_For_Itype (Id : E) return N; @@ -7258,6 +7276,7 @@ package Einfo is function Is_Standard_String_Type (Id : E) return B; function Is_String_Type (Id : E) return B; function Is_Synchronized_Interface (Id : E) return B; + function Is_Synchronized_State (Id : E) return B; function Is_Task_Interface (Id : E) return B; function Is_Task_Record_Type (Id : E) return B; function Is_Wrapper_Package (Id : E) return B; @@ -7369,6 +7388,7 @@ package Einfo is procedure Set_Alias (Id : E; V : E); procedure Set_Alignment (Id : E; V : U); procedure Set_Anonymous_Master (Id : E; V : E); + procedure Set_Anonymous_Object (Id : E; V : E); procedure Set_Associated_Entity (Id : E; V : E); procedure Set_Associated_Formal_Package (Id : E; V : E); procedure Set_Associated_Node_For_Itype (Id : E; V : N); @@ -8148,6 +8168,7 @@ package Einfo is pragma Inline (Alias); pragma Inline (Alignment); pragma Inline (Anonymous_Master); + pragma Inline (Anonymous_Object); pragma Inline (Associated_Entity); pragma Inline (Associated_Formal_Package); pragma Inline (Associated_Node_For_Itype); @@ -8655,6 +8676,7 @@ package Einfo is pragma Inline (Set_Alias); pragma Inline (Set_Alignment); pragma Inline (Set_Anonymous_Master); + pragma Inline (Set_Anonymous_Object); pragma Inline (Set_Associated_Entity); pragma Inline (Set_Associated_Formal_Package); pragma Inline (Set_Associated_Node_For_Itype); diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index b848858..f95841e 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -3291,7 +3291,7 @@ package body Exp_Ch6 is if Subp = Eq_Prim_Op then - -- Mark the node as analyzed to avoid reanalizing this + -- Mark the node as analyzed to avoid reanalyzing this -- dispatching call (which would cause a never-ending loop) Prev_Call := Relocate_Node (Call_Node); diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 58a3322..f4db92f 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -1285,7 +1285,7 @@ package body Exp_Ch7 is Prepend_To (Decls, Counter_Decl); Prepend_To (Decls, Counter_Typ_Decl); - -- The counter and its associated type must be manually analized + -- The counter and its associated type must be manually analyzed -- since N has already been analyzed. Use the scope of the spec -- when inserting in a package. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index f67bc36..e09fbd2 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -4322,6 +4322,25 @@ package body Freeze is Next_Component (Comp); end loop; end if; + + -- A type which does not yield a synchronized object cannot have + -- a component that yields a synchronized object (SPARK RM 9.5). + + if not Yields_Synchronized_Object (Rec) then + Comp := First_Component (Rec); + while Present (Comp) loop + if Comes_From_Source (Comp) + and then Yields_Synchronized_Object (Etype (Comp)) + then + Error_Msg_Name_1 := Chars (Rec); + Error_Msg_N + ("component & of non-synchronized type % cannot be " + & "synchronized", Comp); + end if; + + Next_Component (Comp); + end loop; + end if; end if; -- Make sure that if we have an iterator aspect, then we have diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index d187023..d02d8e5 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1254,6 +1254,7 @@ package body Sem_Ch13 is Aux : Node_Id; Decl : Node_Id; Decls : List_Id; + Def : Node_Id; begin -- When the aspect appears on a package, protected unit, subprogram @@ -1370,32 +1371,52 @@ package body Sem_Ch13 is -- pragma Prag; elsif Nkind (N) = N_Protected_Type_Declaration then - Decls := Visible_Declarations (Protected_Definition (N)); + Def := Protected_Definition (N); + + if No (Def) then + Def := + Make_Protected_Definition (Sloc (N), + Visible_Declarations => New_List, + End_Label => Empty); + + Set_Protected_Definition (N, Def); + end if; + + Decls := Visible_Declarations (Def); if No (Decls) then Decls := New_List; - Set_Visible_Declarations (Protected_Definition (N), Decls); + Set_Visible_Declarations (Def, 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. + -- When the aspect is associated with a task unit declaration, insert + -- 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)); + elsif Nkind (N) = N_Task_Type_Declaration then + Def := Task_Definition (N); + + if No (Def) then + Def := + Make_Task_Definition (Sloc (N), + Visible_Declarations => New_List, + End_Label => Empty); + + Set_Task_Definition (N, Def); + end if; + + Decls := Visible_Declarations (Def); if No (Decls) then Decls := New_List; - Set_Visible_Declarations (Task_Definition (N), Decls); + Set_Visible_Declarations (Def, Decls); end if; Prepend_To (Decls, Prag); @@ -2626,6 +2647,7 @@ package body Sem_Ch13 is when Aspect_Part_Of => if Nkind_In (N, N_Object_Declaration, N_Package_Instantiation) + or else Is_Single_Concurrent_Type_Declaration (N) then Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( @@ -2633,10 +2655,15 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_Part_Of); + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + else Error_Msg_NE - ("aspect & must apply to a variable or package " - & "instantiation", Aspect, Id); + ("aspect & must apply to package instantiation, " + & "object, single protected type or single task type", + Aspect, Id); end if; -- SPARK_Mode diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 7358c0d..881921d 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2495,29 +2495,46 @@ package body Sem_Ch3 is Analyze_Package_Body_Contract (Defining_Entity (Context)); end if; - -- Analyze the contracts of all subprogram declarations, subprogram - -- bodies and variables due to the delayed visibility needs of their - -- aspects and pragmas. + -- Analyze the contracts of eligible constructs (see below) due to + -- the delayed visibility needs of their aspects and pragmas. Decl := First (L); while Present (Decl) loop - if Nkind (Decl) = N_Object_Declaration then - Analyze_Object_Contract (Defining_Entity (Decl)); - elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, - N_Entry_Declaration, - N_Generic_Subprogram_Declaration, - N_Subprogram_Declaration) + -- Entry or subprogram declarations + + if Nkind_In (Decl, N_Abstract_Subprogram_Declaration, + N_Entry_Declaration, + N_Generic_Subprogram_Declaration, + N_Subprogram_Declaration) then Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl)); + -- Entry or subprogram bodies + elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl)); + -- Objects + + elsif Nkind (Decl) = N_Object_Declaration then + Analyze_Object_Contract (Defining_Entity (Decl)); + + -- Protected untis + + elsif Nkind_In (Decl, N_Protected_Type_Declaration, + N_Single_Protected_Declaration) + then + Analyze_Protected_Contract (Defining_Entity (Decl)); + + -- Subprogram body stubs + elsif Nkind (Decl) = N_Subprogram_Body_Stub then Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); + -- Task units + elsif Nkind_In (Decl, N_Single_Task_Declaration, N_Task_Type_Declaration) then diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 62d7251..f3235dd 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -50,6 +50,7 @@ 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_Prag; use Sem_Prag; with Sem_Res; use Sem_Res; with Sem_Type; use Sem_Type; with Sem_Util; use Sem_Util; @@ -2112,20 +2113,23 @@ package body Sem_Ch9 is or else From_Aspect_Specification (Prio_Item) then Error_Msg_Name_1 := Chars (Identifier (Prio_Item)); - Error_Msg_NE ("aspect% for & has no effect when Lock_Free" & - " given??", Prio_Item, Id); + Error_Msg_NE + ("aspect% for & has no effect when Lock_Free given??", + Prio_Item, Id); -- Pragma case else Error_Msg_Name_1 := Pragma_Name (Prio_Item); - Error_Msg_NE ("pragma% for & has no effect when Lock_Free" & - " given??", Prio_Item, Id); + Error_Msg_NE + ("pragma% for & has no effect when Lock_Free given??", + Prio_Item, Id); end if; end if; end; - if not Allows_Lock_Free_Implementation (N, True) then + if not Allows_Lock_Free_Implementation (N, Lock_Free_Given => True) + then return; end if; end if; @@ -2149,16 +2153,18 @@ package body Sem_Ch9 is or else From_Aspect_Specification (Prio_Item)) and then Chars (Identifier (Prio_Item)) = Name_Priority then - Error_Msg_N ("aspect Interrupt_Priority is preferred " - & "in presence of handlers??", Prio_Item); + Error_Msg_N + ("aspect Interrupt_Priority is preferred in presence of " + & "handlers??", Prio_Item); -- Pragma case elsif Nkind (Prio_Item) = N_Pragma and then Pragma_Name (Prio_Item) = Name_Priority then - Error_Msg_N ("pragma Interrupt_Priority is preferred " - & "in presence of handlers??", Prio_Item); + Error_Msg_N + ("pragma Interrupt_Priority is preferred in presence of " + & "handlers??", Prio_Item); end if; end if; end; @@ -2612,49 +2618,80 @@ package body Sem_Ch9 is ------------------------------------------ procedure Analyze_Single_Protected_Declaration (N : Node_Id) is - Loc : constant Source_Ptr := Sloc (N); - Id : constant Node_Id := Defining_Identifier (N); - T : Entity_Id; - T_Decl : Node_Id; - O_Decl : Node_Id; - O_Name : constant Entity_Id := Id; + Loc : constant Source_Ptr := Sloc (N); + Obj_Id : constant Node_Id := Defining_Identifier (N); + Obj_Decl : Node_Id; + Typ : Entity_Id; begin - Generate_Definition (Id); + Generate_Definition (Obj_Id); Tasking_Used := True; - -- The node is rewritten as a protected type declaration, in exact - -- analogy with what is done with single tasks. + -- A single protected declaration is transformed into a pair of an + -- anonymous protected type and an object of that type. Generate: - T := - Make_Defining_Identifier (Sloc (Id), - New_External_Name (Chars (Id), 'T')); + -- protected type Typ is ...; - T_Decl := + Typ := + Make_Defining_Identifier (Sloc (Obj_Id), + Chars => New_External_Name (Chars (Obj_Id), 'T')); + + Rewrite (N, Make_Protected_Type_Declaration (Loc, - Defining_Identifier => T, + Defining_Identifier => Typ, Protected_Definition => Relocate_Node (Protected_Definition (N)), - Interface_List => Interface_List (N)); + Interface_List => Interface_List (N))); + + -- Use the original defining identifier of the single protected + -- declaration in the generated object declaration to allow for debug + -- information to be attached to it when compiling with -gnatD. The + -- parent of the entity is the new object declaration. The single + -- protected declaration is not used in semantics or code generation, + -- but is scanned when generating debug information, and therefore needs + -- the updated Sloc information from the entity (see Sprint). Generate: - O_Decl := + -- Obj : Typ; + + Obj_Decl := Make_Object_Declaration (Loc, - Defining_Identifier => O_Name, - Object_Definition => Make_Identifier (Loc, Chars (T))); + Defining_Identifier => Obj_Id, + Object_Definition => New_Occurrence_Of (Typ, Loc)); + + -- Relocate the aspects that appear on the original single protected + -- declaration to the object as the object is the visible name. + + Set_Comes_From_Source (Obj_Decl, True); + + Insert_After (N, Obj_Decl); + Mark_Rewrite_Insertion (Obj_Decl); + + -- Relocate aspect Part_Of from the the original single protected + -- declaration to the anonymous object declaration. This emulates the + -- placement of an equivalent source pragma. - Rewrite (N, T_Decl); - Insert_After (N, O_Decl); - Mark_Rewrite_Insertion (O_Decl); + Move_Or_Merge_Aspects (N, To => Obj_Decl); - -- Enter names of type and object before analysis, because the name of - -- the object may be used in its own body. + -- Relocate pragma Part_Of from the visible declarations of the original + -- single protected declaration to the anonymous object declaration. The + -- new placement better reflects the role of the pragma. - Enter_Name (T); - Set_Ekind (T, E_Protected_Type); - Set_Etype (T, T); + Relocate_Pragmas_To_Anonymous_Object (N, Obj_Decl); - Enter_Name (O_Name); - Set_Ekind (O_Name, E_Variable); - Set_Etype (O_Name, T); + -- Enter the names of the anonymous protected type and the object before + -- analysis takes places, because the name of the object may be used in + -- its own body. + + Enter_Name (Typ); + Set_Ekind (Typ, E_Protected_Type); + Set_Etype (Typ, Typ); + Set_Anonymous_Object (Typ, Obj_Id); + + Enter_Name (Obj_Id); + Set_Ekind (Obj_Id, E_Variable); + Set_Etype (Obj_Id, Typ); + Set_Part_Of_Constituents (Obj_Id, New_Elmt_List); + Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Obj_Id); -- Instead of calling Analyze on the new node, call the proper analysis -- procedure directly. Otherwise the node would be expanded twice, with @@ -2663,7 +2700,7 @@ package body Sem_Ch9 is Analyze_Protected_Type_Declaration (N); if Has_Aspects (N) then - Analyze_Aspect_Specifications (N, Id); + Analyze_Aspect_Specifications (N, Obj_Id); end if; end Analyze_Single_Protected_Declaration; @@ -2672,58 +2709,81 @@ package body Sem_Ch9 is ------------------------------------- procedure Analyze_Single_Task_Declaration (N : Node_Id) is - Loc : constant Source_Ptr := Sloc (N); - Id : constant Node_Id := Defining_Identifier (N); - T : Entity_Id; - T_Decl : Node_Id; - O_Decl : Node_Id; - O_Name : constant Entity_Id := Id; + Loc : constant Source_Ptr := Sloc (N); + Obj_Id : constant Node_Id := Defining_Identifier (N); + Obj_Decl : Node_Id; + Typ : Entity_Id; begin - Generate_Definition (Id); + Generate_Definition (Obj_Id); Tasking_Used := True; - -- The node is rewritten as a task type declaration, followed by an - -- object declaration of that anonymous task type. + -- A single task declaration is transformed into a pait of an anonymous + -- task type and an object of that type. Generate: + + -- task type Typ is ...; - T := - Make_Defining_Identifier (Sloc (Id), - New_External_Name (Chars (Id), Suffix => "TK")); + Typ := + Make_Defining_Identifier (Sloc (Obj_Id), + Chars => New_External_Name (Chars (Obj_Id), Suffix => "TK")); - T_Decl := + Rewrite (N, Make_Task_Type_Declaration (Loc, - Defining_Identifier => T, + Defining_Identifier => Typ, Task_Definition => Relocate_Node (Task_Definition (N)), - Interface_List => Interface_List (N)); - - -- We use the original defining identifier of the single task in the - -- generated object declaration, so that debugging information can - -- be attached to it when compiling with -gnatD. The parent of the - -- entity is the new object declaration. The single_task_declaration - -- is not used further in semantics or code generation, but is scanned - -- when generating debug information, and therefore needs the updated - -- Sloc information for the entity (see Sprint). Aspect specifications - -- are moved from the single task node to the object declaration node. - - O_Decl := + Interface_List => Interface_List (N))); + + -- Use the original defining identifier of the single task declaration + -- in the generated object declaration to allow for debug information + -- to be attached to it when compiling with -gnatD. The parent of the + -- entity is the new object declaration. The single task declaration + -- is not used in semantics or code generation, but is scanned when + -- generating debug information, and therefore needs the updated Sloc + -- information from the entity (see Sprint). Generate: + + -- Obj : Typ; + + Obj_Decl := Make_Object_Declaration (Loc, - Defining_Identifier => O_Name, - Object_Definition => Make_Identifier (Loc, Chars (T))); + Defining_Identifier => Obj_Id, + Object_Definition => New_Occurrence_Of (Typ, Loc)); - Rewrite (N, T_Decl); - Insert_After (N, O_Decl); - Mark_Rewrite_Insertion (O_Decl); + -- Relocate the aspects that appear on the original single protected + -- declaration to the object as the object is the visible name. - -- Enter names of type and object before analysis, because the name of - -- the object may be used in its own body. + Set_Comes_From_Source (Obj_Decl, True); - Enter_Name (T); - Set_Ekind (T, E_Task_Type); - Set_Etype (T, T); + Insert_After (N, Obj_Decl); + Mark_Rewrite_Insertion (Obj_Decl); - Enter_Name (O_Name); - Set_Ekind (O_Name, E_Variable); - Set_Etype (O_Name, T); + -- Relocate aspects Depends, Global and Part_Of from the original single + -- task declaration to the anonymous object declaration. This emulates + -- the placement of an equivalent source pragma. + + Move_Or_Merge_Aspects (N, To => Obj_Decl); + + -- Relocate pragmas Depends, Global and Part_Of from the visible + -- declarations of the original single protected declaration to the + -- anonymous object declaration. The new placement better reflects the + -- role of the pragmas. + + Relocate_Pragmas_To_Anonymous_Object (N, Obj_Decl); + + -- Enter the names of the anonymous task type and the object before + -- analysis takes places, because the name of the object may be used + -- in its own body. + + Enter_Name (Typ); + Set_Ekind (Typ, E_Task_Type); + Set_Etype (Typ, Typ); + Set_Anonymous_Object (Typ, Obj_Id); + + Enter_Name (Obj_Id); + Set_Ekind (Obj_Id, E_Variable); + Set_Etype (Obj_Id, Typ); + Set_Part_Of_Constituents (Obj_Id, New_Elmt_List); + Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Obj_Id); -- Instead of calling Analyze on the new node, call the proper analysis -- procedure directly. Otherwise the node would be expanded twice, with @@ -2732,7 +2792,7 @@ package body Sem_Ch9 is Analyze_Task_Type_Declaration (N); if Has_Aspects (N) then - Analyze_Aspect_Specifications (N, Id); + Analyze_Aspect_Specifications (N, Obj_Id); end if; end Analyze_Single_Task_Declaration; @@ -3499,4 +3559,5 @@ package body Sem_Ch9 is Next_Entity (E); end loop; end Install_Declarations; + end Sem_Ch9; diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index b206682..7f3b42a 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -567,9 +567,29 @@ package body Sem_Elab is -- Local variables - Loc : constant Source_Ptr := Sloc (N); - Ent : Entity_Id; - Decl : Node_Id; + Loc : constant Source_Ptr := Sloc (N); + + Inst_Case : constant Boolean := Nkind (N) in N_Generic_Instantiation; + -- Indicates if we have instantiation case + + Ent : Entity_Id; + Callee_Unit_Internal : Boolean; + Caller_Unit_Internal : Boolean; + Decl : Node_Id; + Inst_Callee : Source_Ptr; + Inst_Caller : Source_Ptr; + Unit_Callee : Unit_Number_Type; + Unit_Caller : Unit_Number_Type; + + Body_Acts_As_Spec : Boolean; + -- Set to true if call is to body acting as spec (no separate spec) + + Cunit_SC : Boolean := False; + -- Set to suppress dynamic elaboration checks where one of the + -- enclosing scopes has Elaboration_Checks_Suppressed set, or else + -- if a pragma Elaborate[_All] applies to that scope, in which case + -- warnings on the scope are also suppressed. For the internal case, + -- we ignore this flag. E_Scope : Entity_Id; -- Top level scope of entity for called subprogram. This value includes @@ -577,6 +597,9 @@ package body Sem_Elab is -- non-visible unit. This is the scope that is to be investigated to -- see whether an elaboration check is required. + Issue_In_SPARK : Boolean; + -- Flag set when a source entity is called during elaboration in SPARK + W_Scope : Entity_Id; -- Top level scope of directly called entity for subprogram. This -- differs from E_Scope in the case where renamings or derivations @@ -589,28 +612,6 @@ package body Sem_Elab is -- on this intermediate package. These special cases are handled in -- Set_Elaboration_Constraint. - Body_Acts_As_Spec : Boolean; - -- Set to true if call is to body acting as spec (no separate spec) - - Inst_Case : constant Boolean := Nkind (N) in N_Generic_Instantiation; - -- Indicates if we have instantiation case - - Caller_Unit_Internal : Boolean; - Callee_Unit_Internal : Boolean; - - Inst_Caller : Source_Ptr; - Inst_Callee : Source_Ptr; - - Unit_Caller : Unit_Number_Type; - Unit_Callee : Unit_Number_Type; - - Cunit_SC : Boolean := False; - -- Set to suppress dynamic elaboration checks where one of the - -- enclosing scopes has Elaboration_Checks_Suppressed set, or else - -- if a pragma Elaborate[_All] applies to that scope, in which case - -- warnings on the scope are also suppressed. For the internal case, - -- we ignore this flag. - -- Start of processing for Check_A_Call begin @@ -752,9 +753,7 @@ package body Sem_Elab is declare Ent : constant Entity_Id := Get_Referenced_Ent (N); begin - if Is_Init_Proc (Ent) - and then not In_Same_Extended_Unit (N, Ent) - then + if Is_Init_Proc (Ent) and then not In_Same_Extended_Unit (N, Ent) then W_Scope := Scope (Ent); else W_Scope := E; @@ -967,6 +966,8 @@ package body Sem_Elab is return; end if; + Issue_In_SPARK := SPARK_Mode = On and Comes_From_Source (Ent); + -- Now check if an Elaborate_All (or dynamic check) is needed if not Suppress_Elaboration_Warnings (Ent) @@ -980,10 +981,9 @@ package body Sem_Elab is -- Instantiation case if Inst_Case then - if SPARK_Mode = On then + if Issue_In_SPARK then Error_Msg_NE ("instantiation of & during elaboration in SPARK", N, Ent); - else Elab_Warning ("instantiation of & may raise Program_Error?l?", @@ -999,7 +999,7 @@ package body Sem_Elab is -- Variable reference in SPARK mode - elsif Variable_Case then + elsif Variable_Case and Issue_In_SPARK then Error_Msg_NE ("reference to & during elaboration in SPARK", N, Ent); @@ -1015,7 +1015,7 @@ package body Sem_Elab is "info: implicit call to & during elaboration?$?", Ent); - elsif SPARK_Mode = On then + elsif Issue_In_SPARK then Error_Msg_NE ("call to & during elaboration in SPARK", N, Ent); else @@ -1031,7 +1031,7 @@ package body Sem_Elab is -- Case of Elaborate_All not present and required, for SPARK this -- is an error, so give an error message. - if SPARK_Mode = On then + if Issue_In_SPARK then Error_Msg_NE ("\Elaborate_All pragma required for&", N, W_Scope); -- Otherwise we generate an implicit pragma. For a subprogram diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 3972ac3..0b6e64d 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -174,6 +174,19 @@ package body Sem_Prag is -- to Uppercase or Lowercase, then a new string literal with appropriate -- casing is constructed. + procedure Analyze_Part_Of + (Indic : Node_Id; + Item_Id : Entity_Id; + Encap : Node_Id; + Encap_Id : out Entity_Id; + Legal : out Boolean); + -- Subsidiary to Analyze_Part_Of_In_Decl_Part, Analyze_Part_Of_Option and + -- Analyze_Pragma. Perform full analysis of indicator Part_Of. Indic is the + -- Part_Of indicator. Item_Id is the entity of an abstract state, object or + -- package instantiation. Encap denotes the encapsulating state or single + -- concurrent type. Encap_Id is the entity of Encap. Flag Legal is set when + -- the indicator is legal. + function Appears_In (List : Elist_Id; Item_Id : Entity_Id) return Boolean; -- Subsidiary to analysis of pragmas Depends, Global and Refined_Depends. -- Query whether a particular item appears in a mixed list of nodes and @@ -209,12 +222,6 @@ package body Sem_Prag is -- Do_Checks is set, the routine reports duplicate pragmas. The routine -- returns Empty when reaching the start of the node chain. - function Fix_Msg (Id : Entity_Id; Msg : String) return String; - -- Replace all occurrences of "subprogram" in string Msg with a specific - -- word depending on the Ekind of Id as follows: - -- * When Id is an entry [family], replace with "entry" - -- * When Id is a task type, replace with "task unit" - function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id; -- If Def_Id refers to a renamed subprogram, then the base subprogram (the -- original one, following the renaming chain) is returned. Otherwise the @@ -1636,11 +1643,17 @@ package body Sem_Prag is Subp_Outputs => Subp_Outputs, Global_Seen => Global_Seen); + -- When pragma [Refined_]Depends appears on a single concurrent + -- type, it is relocated to the anonymous object. + + if Is_Single_Concurrent_Object (Spec_Id) then + null; + -- Ensure that the formal parameters are visible when analyzing -- all clauses. This falls out of the general rule of aspects -- pertaining to subprogram declarations. - if not In_Open_Scopes (Spec_Id) then + elsif not In_Open_Scopes (Spec_Id) then Restore_Scope := True; Push_Scope (Spec_Id); @@ -2258,11 +2271,17 @@ package body Sem_Prag is -- messages. else + -- When pragma [Refined_]Global appears on a single concurrent type, + -- it is relocated to the anonymous object. + + if Is_Single_Concurrent_Object (Spec_Id) then + null; + -- Ensure that the formal parameters are visible when processing an -- item. This falls out of the general rule of aspects pertaining to -- subprogram declarations. - if not In_Open_Scopes (Spec_Id) then + elsif not In_Open_Scopes (Spec_Id) then Restore_Scope := True; Push_Scope (Spec_Id); @@ -2709,6 +2728,287 @@ package body Sem_Prag is Set_Is_Analyzed_Pragma (N); end Analyze_Initializes_In_Decl_Part; + --------------------- + -- Analyze_Part_Of -- + --------------------- + + procedure Analyze_Part_Of + (Indic : Node_Id; + Item_Id : Entity_Id; + Encap : Node_Id; + Encap_Id : out Entity_Id; + Legal : out Boolean) + is + Encap_Typ : Entity_Id; + Item_Decl : Node_Id; + Pack_Id : Entity_Id; + Placement : State_Space_Kind; + Parent_Unit : Entity_Id; + + begin + -- Assume that the indicator is illegal + + Encap_Id := Empty; + Legal := False; + + if Nkind_In (Encap, N_Expanded_Name, + N_Identifier, + N_Selected_Component) + then + Analyze (Encap); + Resolve_State (Encap); + + Encap_Id := Entity (Encap); + + -- The encapsulator is an abstract state + + if Ekind (Encap_Id) = E_Abstract_State then + null; + + -- The encapsulator is a single concurrent type (SPARK RM 9.3) + + elsif Is_Single_Concurrent_Object (Encap_Id) then + null; + + -- Otherwise the encapsulator is not a legal choice + + else + SPARK_Msg_N + ("indicator Part_Of must denote abstract state, single " + & "protected type or single task type", Encap); + return; + end if; + + -- This is a syntax error, always report + + else + Error_Msg_N + ("indicator Part_Of must denote abstract state, single protected " + & "type or single task type", Encap); + return; + end if; + + -- Catch a case where indicator Part_Of denotes the abstract view of a + -- variable which appears as an abstract state (SPARK RM 10.1.2 2). + + if From_Limited_With (Encap_Id) + and then Present (Non_Limited_View (Encap_Id)) + and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable + then + SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap); + SPARK_Msg_N ("\& denotes abstract view of object", Encap); + return; + end if; + + -- The encapsulator is an abstract state + + if Ekind (Encap_Id) = E_Abstract_State then + + -- Determine where the object, package instantiation or state lives + -- with respect to the enclosing packages or package bodies. + + Find_Placement_In_State_Space + (Item_Id => Item_Id, + Placement => Placement, + Pack_Id => Pack_Id); + + -- The item appears in a non-package construct with a declarative + -- part (subprogram, block, etc). As such, the item is not allowed + -- to be a part of an encapsulating state because the item is not + -- visible. + + if Placement = Not_In_Package then + SPARK_Msg_N + ("indicator Part_Of cannot appear in this context " + & "(SPARK RM 7.2.6(5))", Indic); + Error_Msg_Name_1 := Chars (Scope (Encap_Id)); + SPARK_Msg_NE + ("\& is not part of the hidden state of package %", + Indic, Item_Id); + + -- The item appears in the visible state space of some package. In + -- general this scenario does not warrant Part_Of except when the + -- package is a private child unit and the encapsulating state is + -- declared in a parent unit or a public descendant of that parent + -- unit. + + elsif Placement = Visible_State_Space then + if Is_Child_Unit (Pack_Id) + and then Is_Private_Descendant (Pack_Id) + then + -- A variable or state abstraction which is part of the visible + -- state of a private child unit (or one of its public + -- descendants) must have its Part_Of indicator specified. The + -- Part_Of indicator must denote a state abstraction declared + -- by either the parent unit of the private unit or by a public + -- descendant of that parent unit. + + -- Find nearest private ancestor (which can be the current unit + -- itself). + + Parent_Unit := Pack_Id; + while Present (Parent_Unit) loop + exit when + Private_Present + (Parent (Unit_Declaration_Node (Parent_Unit))); + Parent_Unit := Scope (Parent_Unit); + end loop; + + Parent_Unit := Scope (Parent_Unit); + + if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then + SPARK_Msg_NE + ("indicator Part_Of must denote abstract state or public " + & "descendant of & (SPARK RM 7.2.6(3))", + Indic, Parent_Unit); + + elsif Scope (Encap_Id) = Parent_Unit + or else + (Is_Ancestor_Package (Parent_Unit, Scope (Encap_Id)) + and then not Is_Private_Descendant (Scope (Encap_Id))) + then + null; + + else + SPARK_Msg_NE + ("indicator Part_Of must denote abstract state or public " + & "descendant of & (SPARK RM 7.2.6(3))", + Indic, Parent_Unit); + end if; + + -- Indicator Part_Of is not needed when the related package is not + -- a private child unit or a public descendant thereof. + + else + SPARK_Msg_N + ("indicator Part_Of cannot appear in this context " + & "(SPARK RM 7.2.6(5))", Indic); + Error_Msg_Name_1 := Chars (Pack_Id); + SPARK_Msg_NE + ("\& is declared in the visible part of package %", + Indic, Item_Id); + end if; + + -- When the item appears in the private state space of a package, the + -- encapsulating state must be declared in the same package. + + elsif Placement = Private_State_Space then + if Scope (Encap_Id) /= Pack_Id then + SPARK_Msg_NE + ("indicator Part_Of must designate an abstract state of " + & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id); + Error_Msg_Name_1 := Chars (Pack_Id); + SPARK_Msg_NE + ("\& is declared in the private part of package %", + Indic, Item_Id); + end if; + + -- Items declared in the body state space of a package do not need + -- Part_Of indicators as the refinement has already been seen. + + else + SPARK_Msg_N + ("indicator Part_Of cannot appear in this context " + & "(SPARK RM 7.2.6(5))", Indic); + + if Scope (Encap_Id) = Pack_Id then + Error_Msg_Name_1 := Chars (Pack_Id); + SPARK_Msg_NE + ("\& is declared in the body of package %", Indic, Item_Id); + end if; + end if; + + -- The encapsulator is a single concurrent type + + else + Encap_Typ := Etype (Encap_Id); + + -- Only abstract states and variables can act as constituents of an + -- encapsulating single concurrent type. + + if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then + null; + + -- The constituent is a constant + + elsif Ekind (Item_Id) = E_Constant then + Error_Msg_Name_1 := Chars (Encap_Id); + SPARK_Msg_NE + (Fix_Msg (Encap_Typ, "consant & cannot act as constituent of " + & "single protected type %"), Indic, Item_Id); + + -- The constituent is a package instantiation + + else + Error_Msg_Name_1 := Chars (Encap_Id); + SPARK_Msg_NE + (Fix_Msg (Encap_Typ, "package instantiation & cannot act as " + & "constituent of single protected type %"), Indic, Item_Id); + end if; + + -- When the item denotes an abstract state of a nested package, use + -- the declaration of the package to detect proper placement. + + -- package Pack is + -- task T; + -- package Nested + -- with Abstract_State => (State with Part_Of => T) + + if Ekind (Item_Id) = E_Abstract_State then + Item_Decl := Unit_Declaration_Node (Scope (Item_Id)); + else + Item_Decl := Declaration_Node (Item_Id); + end if; + + -- Both the item and its encapsulating single concurrent type must + -- appear in the same declarative region (SPARK RM 9.3). Note that + -- privacy is ignored. + + if Parent (Item_Decl) /= Parent (Declaration_Node (Encap_Id)) then + Error_Msg_Name_1 := Chars (Encap_Id); + SPARK_Msg_NE + (Fix_Msg (Encap_Typ, "constituent & must be declared " + & "immediately within the same region as single protected " + & "type %"), Indic, Item_Id); + end if; + end if; + + Legal := True; + end Analyze_Part_Of; + + ---------------------------------- + -- Analyze_Part_Of_In_Decl_Part -- + ---------------------------------- + + procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id) is + Var_Decl : constant Node_Id := Find_Related_Context (N); + Var_Id : constant Entity_Id := Defining_Entity (Var_Decl); + Encap_Id : Entity_Id; + Legal : Boolean; + + begin + -- Detect any discrepancies between the placement of the variable with + -- respect to general state space and the encapsulating state or single + -- concurrent type. + + Analyze_Part_Of + (Indic => N, + Item_Id => Var_Id, + Encap => Get_Pragma_Arg (First (Pragma_Argument_Associations (N))), + Encap_Id => Encap_Id, + Legal => Legal); + + -- The Part_Of indicator turns the variable into a constituent of the + -- encapsulating state or single concurrent type. + + if Legal then + pragma Assert (Present (Encap_Id)); + + Append_Elmt (Var_Id, Part_Of_Constituents (Encap_Id)); + Set_Encapsulating_State (Var_Id, Encap_Id); + end if; + end Analyze_Part_Of_In_Decl_Part; + -------------------- -- Analyze_Pragma -- -------------------- @@ -2775,17 +3075,6 @@ package body Sem_Prag is -- Inspect the remainder of the list containing pragma N and look for -- a pragma that matches Id. If found, analyze the pragma. - procedure Analyze_Part_Of - (Item_Id : Entity_Id; - State : Node_Id; - Indic : Node_Id; - Legal : out Boolean); - -- Subsidiary to the analysis of pragmas Abstract_State and Part_Of. - -- Perform full analysis of indicator Part_Of. Item_Id is the entity of - -- an abstract state, object, or package instantiation. State is the - -- encapsulating state. Indic is the Part_Of indicator. Flag Legal is - -- set when the indicator is legal. - procedure Analyze_Pre_Post_Condition; -- Subsidiary to the analysis of pragmas Precondition and Postcondition @@ -3374,6 +3663,16 @@ package body Sem_Prag is elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then null; + -- Object declaration of a single concurrent type + + elsif Nkind (Subp_Decl) = N_Object_Declaration then + null; + + -- Single task type + + elsif Nkind (Subp_Decl) = N_Single_Task_Declaration then + null; + -- Subprogram body acts as spec elsif Nkind (Subp_Decl) = N_Subprogram_Body @@ -3393,7 +3692,7 @@ package body Sem_Prag is elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then null; - -- Task unit + -- Task type elsif Nkind (Subp_Decl) = N_Task_Type_Declaration then null; @@ -3408,14 +3707,24 @@ package body Sem_Prag is Legal := True; Spec_Id := Unique_Defining_Entity (Subp_Decl); - -- When the related context is an entry, it must be a protected entry - -- (SPARK RM 6.1.4(6)). + -- When the related context is an entry, the entry must belong to a + -- protected unit (SPARK RM 6.1.4(6)). if Is_Entry_Declaration (Spec_Id) and then Ekind (Scope (Spec_Id)) /= E_Protected_Type then Pragma_Misplaced; return; + + -- When the related context is an anonymous object created for a + -- simple concurrent type, the type must be a task + -- (SPARK RM 6.1.4(6)). + + elsif Is_Single_Concurrent_Object (Spec_Id) + and then Ekind (Etype (Spec_Id)) /= E_Task_Type + then + Pragma_Misplaced; + return; end if; -- A pragma that applies to a Ghost entity becomes Ghost for the @@ -3456,183 +3765,6 @@ package body Sem_Prag is end loop; end Analyze_If_Present; - --------------------- - -- Analyze_Part_Of -- - --------------------- - - procedure Analyze_Part_Of - (Item_Id : Entity_Id; - State : Node_Id; - Indic : Node_Id; - Legal : out Boolean) - is - Pack_Id : Entity_Id; - Placement : State_Space_Kind; - Parent_Unit : Entity_Id; - State_Id : Entity_Id; - - begin - -- Assume that the pragma/option is illegal - - Legal := False; - - if Nkind_In (State, N_Expanded_Name, - N_Identifier, - N_Selected_Component) - then - Analyze (State); - Resolve_State (State); - - if Is_Entity_Name (State) - and then Ekind (Entity (State)) = E_Abstract_State - then - State_Id := Entity (State); - - else - SPARK_Msg_N - ("indicator Part_Of must denote an abstract state", State); - return; - end if; - - -- This is a syntax error, always report - - else - Error_Msg_N - ("indicator Part_Of must denote an abstract state", State); - return; - end if; - - -- Catch a case where indicator Part_Of denotes the abstract view of - -- a variable which appears as an abstract state (SPARK RM 10.1.2 2). - - if From_Limited_With (State_Id) - and then Present (Non_Limited_View (State_Id)) - and then Ekind (Non_Limited_View (State_Id)) = E_Variable - then - SPARK_Msg_N - ("indicator Part_Of must denote an abstract state", State); - SPARK_Msg_N ("\& denotes abstract view of object", State); - return; - end if; - - -- Determine where the state, object or the package instantiation - -- lives with respect to the enclosing packages or package bodies (if - -- any). This placement dictates the legality of the encapsulating - -- state. - - Find_Placement_In_State_Space - (Item_Id => Item_Id, - Placement => Placement, - Pack_Id => Pack_Id); - - -- The item appears in a non-package construct with a declarative - -- part (subprogram, block, etc). As such, the item is not allowed - -- to be a part of an encapsulating state because the item is not - -- visible. - - if Placement = Not_In_Package then - SPARK_Msg_N - ("indicator Part_Of cannot appear in this context " - & "(SPARK RM 7.2.6(5))", Indic); - Error_Msg_Name_1 := Chars (Scope (State_Id)); - SPARK_Msg_NE - ("\& is not part of the hidden state of package %", - Indic, Item_Id); - - -- The item appears in the visible state space of some package. In - -- general this scenario does not warrant Part_Of except when the - -- package is a private child unit and the encapsulating state is - -- declared in a parent unit or a public descendant of that parent - -- unit. - - elsif Placement = Visible_State_Space then - if Is_Child_Unit (Pack_Id) - and then Is_Private_Descendant (Pack_Id) - then - -- A variable or state abstraction which is part of the - -- visible state of a private child unit (or one of its public - -- descendants) must have its Part_Of indicator specified. The - -- Part_Of indicator must denote a state abstraction declared - -- by either the parent unit of the private unit or by a public - -- descendant of that parent unit. - - -- Find nearest private ancestor (which can be the current unit - -- itself). - - Parent_Unit := Pack_Id; - while Present (Parent_Unit) loop - exit when Private_Present - (Parent (Unit_Declaration_Node (Parent_Unit))); - Parent_Unit := Scope (Parent_Unit); - end loop; - - Parent_Unit := Scope (Parent_Unit); - - if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then - SPARK_Msg_NE - ("indicator Part_Of must denote an abstract state or " - & "public descendant of & (SPARK RM 7.2.6(3))", - Indic, Parent_Unit); - - elsif Scope (State_Id) = Parent_Unit - or else (Is_Ancestor_Package (Parent_Unit, Scope (State_Id)) - and then - not Is_Private_Descendant (Scope (State_Id))) - then - null; - - else - SPARK_Msg_NE - ("indicator Part_Of must denote an abstract state or " - & "public descendant of & (SPARK RM 7.2.6(3))", - Indic, Parent_Unit); - end if; - - -- Indicator Part_Of is not needed when the related package is not - -- a private child unit or a public descendant thereof. - - else - SPARK_Msg_N - ("indicator Part_Of cannot appear in this context " - & "(SPARK RM 7.2.6(5))", Indic); - Error_Msg_Name_1 := Chars (Pack_Id); - SPARK_Msg_NE - ("\& is declared in the visible part of package %", - Indic, Item_Id); - end if; - - -- When the item appears in the private state space of a package, the - -- encapsulating state must be declared in the same package. - - elsif Placement = Private_State_Space then - if Scope (State_Id) /= Pack_Id then - SPARK_Msg_NE - ("indicator Part_Of must designate an abstract state of " - & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id); - Error_Msg_Name_1 := Chars (Pack_Id); - SPARK_Msg_NE - ("\& is declared in the private part of package %", - Indic, Item_Id); - end if; - - -- Items declared in the body state space of a package do not need - -- Part_Of indicators as the refinement has already been seen. - - else - SPARK_Msg_N - ("indicator Part_Of cannot appear in this context " - & "(SPARK RM 7.2.6(5))", Indic); - - if Scope (State_Id) = Pack_Id then - Error_Msg_Name_1 := Chars (Pack_Id); - SPARK_Msg_NE - ("\& is declared in the body of package %", Indic, Item_Id); - end if; - end if; - - Legal := True; - end Analyze_Part_Of; - -------------------------------- -- Analyze_Pre_Post_Condition -- -------------------------------- @@ -9681,7 +9813,7 @@ package body Sem_Prag is -- SIMPLE_OPTION -- | NAME_VALUE_OPTION - -- SIMPLE_OPTION ::= Ghost + -- SIMPLE_OPTION ::= Ghost | Synchronous -- NAME_VALUE_OPTION ::= -- Part_Of => ABSTRACT_STATE @@ -9751,13 +9883,15 @@ package body Sem_Prag is is -- Flags used to verify the consistency of options - AR_Seen : Boolean := False; - AW_Seen : Boolean := False; - ER_Seen : Boolean := False; - EW_Seen : Boolean := False; - External_Seen : Boolean := False; - Others_Seen : Boolean := False; - Part_Of_Seen : Boolean := False; + AR_Seen : Boolean := False; + AW_Seen : Boolean := False; + ER_Seen : Boolean := False; + EW_Seen : Boolean := False; + External_Seen : Boolean := False; + Ghost_Seen : Boolean := False; + Others_Seen : Boolean := False; + Part_Of_Seen : Boolean := False; + Synchronous_Seen : Boolean := False; -- Flags used to store the static value of all external states' -- expressions. @@ -9822,8 +9956,6 @@ package body Sem_Prag is Props : Node_Id := Empty; begin - Check_Duplicate_Option (Opt, External_Seen); - if Nkind (Opt) = N_Component_Association then Props := Expression (Opt); end if; @@ -9996,27 +10128,29 @@ package body Sem_Prag is ---------------------------- procedure Analyze_Part_Of_Option (Opt : Node_Id) is - Encaps : constant Node_Id := Expression (Opt); - Encaps_Id : Entity_Id; - Legal : Boolean; + Encap : constant Node_Id := Expression (Opt); + Encap_Id : Entity_Id; + Legal : Boolean; begin Check_Duplicate_Option (Opt, Part_Of_Seen); Analyze_Part_Of - (Item_Id => State_Id, - State => Encaps, - Indic => First (Choices (Opt)), - Legal => Legal); + (Indic => First (Choices (Opt)), + Item_Id => State_Id, + Encap => Encap, + Encap_Id => Encap_Id, + Legal => Legal); - -- The Part_Of indicator turns an abstract state into a - -- constituent of the encapsulating state. + -- The Part_Of indicator transforms the abstract state into + -- a constituent of the encapsulating state or single + -- concurrent type. if Legal then - Encaps_Id := Entity (Encaps); + pragma Assert (Present (Encap_Id)); - Append_Elmt (State_Id, Part_Of_Constituents (Encaps_Id)); - Set_Encapsulating_State (State_Id, Encaps_Id); + Append_Elmt (State_Id, Part_Of_Constituents (Encap_Id)); + Set_Encapsulating_State (State_Id, Encap_Id); end if; end Analyze_Part_Of_Option; @@ -10179,26 +10313,41 @@ package body Sem_Prag is Ancestor_Part (State)); end if; - -- Options External and Ghost appear as expressions + -- Options External, Ghost and Synchronous appear as + -- expressions. Opt := First (Expressions (State)); while Present (Opt) loop if Nkind (Opt) = N_Identifier then + + -- External + if Chars (Opt) = Name_External then + Check_Duplicate_Option (Opt, External_Seen); Analyze_External_Option (Opt); + -- Ghost + elsif Chars (Opt) = Name_Ghost then + Check_Duplicate_Option (Opt, Ghost_Seen); + if Present (State_Id) then Set_Is_Ghost_Entity (State_Id); end if; + -- Synchronous + + elsif Chars (Opt) = Name_Synchronous then + Check_Duplicate_Option (Opt, Synchronous_Seen); + -- Option Part_Of without an encapsulating state is - -- illegal. (SPARK RM 7.1.4(9)). + -- illegal (SPARK RM 7.1.4(9)). elsif Chars (Opt) = Name_Part_Of then SPARK_Msg_N - ("indicator Part_Of must denote an abstract " - & "state", Opt); + ("indicator Part_Of must denote abstract state, " + & "single protected type or single task type", + Opt); -- Do not emit an error message when a previous state -- declaration with options was not parenthesized as @@ -17626,10 +17775,10 @@ package body Sem_Prag is -- Local variables + Encap : Node_Id; + Encap_Id : Entity_Id; Item_Id : Entity_Id; Legal : Boolean; - State : Node_Id; - State_Id : Entity_Id; Stmt : Node_Id; -- Start of processing for Part_Of @@ -17651,6 +17800,11 @@ package body Sem_Prag is elsif Nkind (Stmt) = N_Package_Instantiation then null; + -- Single concurrent type declaration + + elsif Is_Single_Concurrent_Type_Declaration (Stmt) then + null; + -- Otherwise the pragma is associated with an illegal construct else @@ -17667,47 +17821,58 @@ package body Sem_Prag is end if; Item_Id := Defining_Entity (Stmt); - State := Get_Pragma_Arg (Arg1); + Encap := Get_Pragma_Arg (Arg1); -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. Mark_Pragma_As_Ghost (N, Item_Id); - -- Detect any discrepancies between the placement of the object - -- or package instantiation with respect to state space and the - -- encapsulating state. + -- Chain the pragma on the contract for further processing by + -- Analyze_Part_Of_In_Decl_Part or for completeness. - Analyze_Part_Of - (Item_Id => Item_Id, - State => State, - Indic => N, - Legal => Legal); + Add_Contract_Item (N, Item_Id); - if Legal then + -- A variable may act as consituent of a single concurrent type + -- which in turn could be declared after the variable. Due to this + -- discrepancy, the full analysis of indicator Part_Of is delayed + -- until the end of the enclosing declarative region (see routine + -- Analyze_Part_Of_In_Decl_Part). - -- Add the pragma to the contract of the item. This aids with - -- the detection of a missing but required Part_Of indicator. + if Ekind (Item_Id) = E_Variable then + null; - Add_Contract_Item (N, Item_Id); + -- Otherwise indicator Part_Of applies to a constant or a package + -- instantiation. - -- The Part_Of indicator turns an object into a constituent of - -- the encapsulating state. + else + -- Detect any discrepancies between the placement of the + -- constant or package instantiation with respect to state + -- space and the encapsulating state. - State_Id := Entity (State); + Analyze_Part_Of + (Indic => N, + Item_Id => Item_Id, + Encap => Encap, + Encap_Id => Encap_Id, + Legal => Legal); - if Ekind_In (Item_Id, E_Constant, E_Variable) then - Append_Elmt (Item_Id, Part_Of_Constituents (State_Id)); - Set_Encapsulating_State (Item_Id, State_Id); + if Legal then + pragma Assert (Present (Encap_Id)); - -- Propagate the Part_Of indicator to the visible state space - -- of the package instantiation. + if Ekind (Item_Id) = E_Constant then + Append_Elmt (Item_Id, Part_Of_Constituents (Encap_Id)); + Set_Encapsulating_State (Item_Id, Encap_Id); - else - Propagate_Part_Of - (Pack_Id => Item_Id, - State_Id => State_Id, - Instance => Stmt); + -- Propagate the Part_Of indicator to the visible state + -- space of the package instantiation. + + else + Propagate_Part_Of + (Pack_Id => Item_Id, + State_Id => Encap_Id, + Instance => Stmt); + end if; end if; end if; end Part_Of; @@ -19963,7 +20128,8 @@ package body Sem_Prag is -------------------------- procedure Process_Overloadable (Decl : Node_Id) is - Spec_Id : constant Entity_Id := Defining_Entity (Decl); + Spec_Id : constant Entity_Id := Defining_Entity (Decl); + Spec_Typ : constant Entity_Id := Etype (Spec_Id); begin Check_Library_Level_Entity (Spec_Id); @@ -19978,6 +20144,25 @@ package body Sem_Prag is Set_SPARK_Pragma (Spec_Id, N); Set_SPARK_Pragma_Inherited (Spec_Id, False); + + -- When the pragma applies to the anonymous object created for + -- a single task type, decorate the type as well. This scenario + -- arises when the single task type lacks a task definition, + -- therefore there is no issue with respect to a potential + -- pragma SPARK_Mode in the private part. + + -- task type Anon_Task_Typ; + -- Obj : Anon_Task_Typ; + -- pragma SPARK_Mode ...; + + if Is_Single_Concurrent_Object (Spec_Id) + and then Ekind (Spec_Typ) = E_Task_Type + then + Set_SPARK_Pragma (Spec_Typ, N); + Set_SPARK_Pragma_Inherited (Spec_Typ, False); + Set_SPARK_Aux_Pragma (Spec_Typ, N); + Set_SPARK_Aux_Pragma_Inherited (Spec_Typ, True); + end if; end Process_Overloadable; -------------------------- @@ -20032,6 +20217,7 @@ package body Sem_Prag is procedure Process_Visible_Part (Decl : Node_Id) is Spec_Id : constant Entity_Id := Defining_Entity (Decl); + Obj_Id : Entity_Id; begin Check_Library_Level_Entity (Spec_Id); @@ -20058,6 +20244,23 @@ package body Sem_Prag is Set_SPARK_Pragma_Inherited (Spec_Id, False); Set_SPARK_Aux_Pragma (Spec_Id, N); Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True); + + -- When the pragma applies to a single protected or task type, + -- decorate the corresponding anonymous object as well. + + -- protected Anon_Prot_Typ is + -- pragma SPARK_Mode ...; + -- ... + -- end Anon_Prot_Typ; + + -- Obj : Anon_Prot_Typ; + + if Is_Single_Concurrent_Type (Spec_Id) then + Obj_Id := Anonymous_Object (Spec_Id); + + Set_SPARK_Pragma (Obj_Id, N); + Set_SPARK_Pragma_Inherited (Obj_Id, False); + end if; end Process_Visible_Part; ----------------------- @@ -20165,19 +20368,6 @@ package body Sem_Prag is 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 ...; - - elsif Nkind_In (Stmt, N_Single_Task_Declaration, - N_Task_Type_Declaration) - then - Process_Visible_Part (Stmt); - return; - -- Skip internally generated code elsif not Comes_From_Source (Stmt) then @@ -20202,6 +20392,20 @@ package body Sem_Prag is Process_Overloadable (Stmt); return; + -- The pragma applies to the anonymous object created for a + -- single concurrent type. + + -- protected type Anon_Prot_Typ ...; + -- Obj : Anon_Prot_Typ; + -- pragma SPARK_Mode ...; + + elsif Nkind (Stmt) = N_Object_Declaration + and then Is_Single_Concurrent_Object + (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. @@ -23469,6 +23673,15 @@ package body Sem_Prag is end if; Spec_Id := Unique_Defining_Entity (Body_Decl); + + -- Use the anonymous object as the proper spec when Refined_Depends + -- applies to the body of a single task type. The object carries the + -- proper Chars as well as all non-refined versions of pragmas. + + if Is_Single_Concurrent_Type (Spec_Id) then + Spec_Id := Anonymous_Object (Spec_Id); + end if; + Depends := Get_Pragma (Spec_Id, Pragma_Depends); -- Subprogram declarations lacks pragma Depends. Refined_Depends is @@ -24438,8 +24651,17 @@ package body Sem_Prag is end if; Spec_Id := Unique_Defining_Entity (Body_Decl); - Global := Get_Pragma (Spec_Id, Pragma_Global); - Items := Expression (Get_Argument (N, Spec_Id)); + + -- Use the anonymous object as the proper spec when Refined_Global + -- applies to the body of a single task type. The object carries the + -- proper Chars as well as all non-refined versions of pragmas. + + if Is_Single_Concurrent_Type (Spec_Id) then + Spec_Id := Anonymous_Object (Spec_Id); + end if; + + Global := Get_Pragma (Spec_Id, Pragma_Global); + Items := Expression (Get_Argument (N, Spec_Id)); -- The subprogram declaration lacks pragma Global. This renders -- Refined_Global useless as there is nothing to refine. @@ -24636,7 +24858,7 @@ package body Sem_Prag is -- should be set when the property applies to the refined state. If -- this is not the case, emit an error message. - procedure Check_Matching_State; + procedure Match_State; -- Determine whether the state being refined appears in list -- Available_States. Emit an error when attempting to re-refine the -- state or when the state is not defined in the package declaration, @@ -24650,26 +24872,21 @@ package body Sem_Prag is ------------------------- procedure Analyze_Constituent (Constit : Node_Id) is - procedure Check_Ghost_Constituent (Constit_Id : Entity_Id); - -- Verify that the constituent Constit_Id is a Ghost entity if the - -- abstract state being refined is also Ghost. If this is the case - -- verify that the Ghost policy in effect at the point of state - -- and constituent declaration is the same. - - procedure Check_Matching_Constituent (Constit_Id : Entity_Id); + procedure Match_Constituent (Constit_Id : Entity_Id); -- Determine whether constituent Constit denoted by its entity -- Constit_Id appears in Body_States. Emit an error when the -- constituent is not a valid hidden state of the related package -- or when it is used more than once. Otherwise remove the -- constituent from Body_States. - -------------------------------- - -- Check_Matching_Constituent -- - -------------------------------- + ----------------------- + -- Match_Constituent -- + ----------------------- - procedure Check_Matching_Constituent (Constit_Id : Entity_Id) is + procedure Match_Constituent (Constit_Id : Entity_Id) is procedure Collect_Constituent; - -- Add constituent Constit_Id to the refinements of State_Id + -- Verify the legality of constituent Constit_Id and add it to + -- the refinements of State_Id. ------------------------- -- Collect_Constituent -- @@ -24677,6 +24894,64 @@ package body Sem_Prag is procedure Collect_Constituent is begin + if Is_Ghost_Entity (State_Id) then + if Is_Ghost_Entity (Constit_Id) then + + -- The Ghost policy in effect at the point of abstract + -- state declaration and constituent must match + -- (SPARK RM 6.9(16)). + + if Is_Checked_Ghost_Entity (State_Id) + and then Is_Ignored_Ghost_Entity (Constit_Id) + then + Error_Msg_Sloc := Sloc (Constit); + + SPARK_Msg_N + ("incompatible ghost policies in effect", State); + SPARK_Msg_NE + ("\abstract state & declared with ghost policy " + & "Check", State, State_Id); + SPARK_Msg_NE + ("\constituent & declared # with ghost policy " + & "Ignore", State, Constit_Id); + + elsif Is_Ignored_Ghost_Entity (State_Id) + and then Is_Checked_Ghost_Entity (Constit_Id) + then + Error_Msg_Sloc := Sloc (Constit); + + SPARK_Msg_N + ("incompatible ghost policies in effect", State); + SPARK_Msg_NE + ("\abstract state & declared with ghost policy " + & "Ignore", State, State_Id); + SPARK_Msg_NE + ("\constituent & declared # with ghost policy " + & "Check", State, Constit_Id); + end if; + + -- A constituent of a Ghost abstract state must be a + -- Ghost entity (SPARK RM 7.2.2(12)). + + else + SPARK_Msg_NE + ("constituent of ghost state & must be ghost", + Constit, State_Id); + end if; + end if; + + -- A synchronized state must be refined by a synchronized + -- object or another synchronized state (SPARK RM 9.6). + + if Is_Synchronized_State (State_Id) + and then not Is_Synchronized_Object (Constit_Id) + and then not Is_Synchronized_State (Constit_Id) + then + SPARK_Msg_NE + ("constituent of synchronized state & must be " + & "synchronized", Constit, State_Id); + end if; + -- Add the constituent to the list of processed items to aid -- with the detection of duplicates. @@ -24723,7 +24998,7 @@ package body Sem_Prag is State_Elmt : Elmt_Id; - -- Start of processing for Check_Matching_Constituent + -- Start of processing for Match_Constituent begin -- Detect a duplicate use of a constituent @@ -24738,7 +25013,6 @@ package body Sem_Prag is if Present (Encapsulating_State (Constit_Id)) then if Encapsulating_State (Constit_Id) = State_Id then - Check_Ghost_Constituent (Constit_Id); Remove (Part_Of_Constits, Constit_Id); Collect_Constituent; @@ -24751,8 +25025,8 @@ package body Sem_Prag is ("& cannot act as constituent of state %", Constit, Constit_Id); SPARK_Msg_NE - ("\Part_Of indicator specifies & as encapsulating " - & "state", Constit, Encapsulating_State (Constit_Id)); + ("\Part_Of indicator specifies encapsulator &", + Constit, Encapsulating_State (Constit_Id)); end if; -- The only other source of legal constituents is the body @@ -24767,7 +25041,6 @@ package body Sem_Prag is -- been encountered. if Node (State_Elmt) = Constit_Id then - Check_Ghost_Constituent (Constit_Id); Remove_Elmt (Body_States, State_Elmt); Collect_Constituent; return; @@ -24797,60 +25070,7 @@ package body Sem_Prag is & "hidden state of package %", Constit, Constit_Id); end if; end if; - end Check_Matching_Constituent; - - ----------------------------- - -- Check_Ghost_Constituent -- - ----------------------------- - - procedure Check_Ghost_Constituent (Constit_Id : Entity_Id) is - begin - if Is_Ghost_Entity (State_Id) then - if Is_Ghost_Entity (Constit_Id) then - - -- The Ghost policy in effect at the point of abstract - -- state declaration and constituent must match - -- (SPARK RM 6.9(16)). - - if Is_Checked_Ghost_Entity (State_Id) - and then Is_Ignored_Ghost_Entity (Constit_Id) - then - Error_Msg_Sloc := Sloc (Constit); - - SPARK_Msg_N - ("incompatible ghost policies in effect", State); - SPARK_Msg_NE - ("\abstract state & declared with ghost policy " - & "Check", State, State_Id); - SPARK_Msg_NE - ("\constituent & declared # with ghost policy " - & "Ignore", State, Constit_Id); - - elsif Is_Ignored_Ghost_Entity (State_Id) - and then Is_Checked_Ghost_Entity (Constit_Id) - then - Error_Msg_Sloc := Sloc (Constit); - - SPARK_Msg_N - ("incompatible ghost policies in effect", State); - SPARK_Msg_NE - ("\abstract state & declared with ghost policy " - & "Ignore", State, State_Id); - SPARK_Msg_NE - ("\constituent & declared # with ghost policy " - & "Check", State, Constit_Id); - end if; - - -- A constituent of a Ghost abstract state must be a Ghost - -- entity (SPARK RM 7.2.2(12)). - - else - SPARK_Msg_NE - ("constituent of ghost state & must be ghost", - Constit, State_Id); - end if; - end if; - end Check_Ghost_Constituent; + end Match_Constituent; -- Local variables @@ -24950,7 +25170,7 @@ package body Sem_Prag is E_Constant, E_Variable) then - Check_Matching_Constituent (Constit_Id); + Match_Constituent (Constit_Id); -- Otherwise the constituent is illegal @@ -25002,11 +25222,11 @@ package body Sem_Prag is end if; end Check_External_Property; - -------------------------- - -- Check_Matching_State -- - -------------------------- + ----------------- + -- Match_State -- + ----------------- - procedure Check_Matching_State is + procedure Match_State is State_Elmt : Elmt_Id; begin @@ -25046,7 +25266,7 @@ package body Sem_Prag is SPARK_Msg_NE ("cannot refine state, & is not defined in package %", State, State_Id); - end Check_Matching_State; + end Match_State; -------------------------------- -- Report_Unused_Constituents -- @@ -25139,11 +25359,10 @@ package body Sem_Prag is -- is not defined in the package declaration. elsif Ekind (State_Id) = E_Abstract_State then - Check_Matching_State; + Match_State; else - SPARK_Msg_NE - ("& must denote an abstract state", State, State_Id); + SPARK_Msg_NE ("& must denote abstract state", State, State_Id); return; end if; @@ -26119,7 +26338,7 @@ package body Sem_Prag is begin -- Since a constituent may be part of a larger constituent set, climb - -- the encapsulated state chain looking for a state that appears in + -- the encapsulating state chain looking for a state that appears in -- the same context. State_Id := Encapsulating_State (Constit_Id); @@ -26640,14 +26859,6 @@ package body Sem_Prag is elsif Present (Generic_Parent (Specification (Stmt))) then return Stmt; end if; - - -- The pragma applies to a single task declaration rewritten as a - -- task type. - - elsif Nkind (Stmt) = N_Task_Type_Declaration - and then Nkind (Original_Node (Stmt)) = N_Single_Task_Declaration - then - return Stmt; end if; -- Return the current construct which is either a subprogram body, @@ -26791,56 +27002,6 @@ package body Sem_Prag is end if; end Find_Related_Package_Or_Body; - ------------- - -- Fix_Msg -- - ------------- - - function Fix_Msg (Id : Entity_Id; Msg : String) return String is - Msg_Last : constant Natural := Msg'Last; - Msg_Index : Natural; - Res : String (Msg'Range) := (others => ' '); - Res_Index : Natural; - - begin - -- Copy all characters from the input message Msg to result Res with - -- suitable replacements. - - Msg_Index := Msg'First; - Res_Index := Res'First; - while Msg_Index <= Msg_Last loop - - -- Replace "subprogram" with a different word - - if Msg_Index <= Msg_Last - 10 - and then Msg (Msg_Index .. Msg_Index + 9) = "subprogram" - then - if Ekind_In (Id, E_Entry, E_Entry_Family) then - Res (Res_Index .. Res_Index + 4) := "entry"; - Res_Index := Res_Index + 5; - - elsif Ekind_In (Id, E_Task_Body, E_Task_Type) then - Res (Res_Index .. Res_Index + 8) := "task unit"; - Res_Index := Res_Index + 9; - - else - Res (Res_Index .. Res_Index + 9) := "subprogram"; - Res_Index := Res_Index + 10; - end if; - - Msg_Index := Msg_Index + 10; - - -- Otherwise copy the character - - else - Res (Res_Index) := Msg (Msg_Index); - Msg_Index := Msg_Index + 1; - Res_Index := Res_Index + 1; - end if; - end loop; - - return Res (Res'First .. Res_Index - 1); - end Fix_Msg; - ------------------ -- Get_Argument -- ------------------ @@ -27692,6 +27853,60 @@ package body Sem_Prag is end loop; end Record_Possible_Body_Reference; + ------------------------------------------ + -- Relocate_Pragmas_To_Anonymous_Object -- + ------------------------------------------ + + procedure Relocate_Pragmas_To_Anonymous_Object + (Typ_Decl : Node_Id; + Obj_Decl : Node_Id) + is + Decl : Node_Id; + Def : Node_Id; + Next_Decl : Node_Id; + + begin + if Nkind (Typ_Decl) = N_Protected_Type_Declaration then + Def := Protected_Definition (Typ_Decl); + else + pragma Assert (Nkind (Typ_Decl) = N_Task_Type_Declaration); + Def := Task_Definition (Typ_Decl); + end if; + + -- The concurrent definition has a visible declaration list. Inspect it + -- and relocate all canidate pragmas. + + if Present (Def) and then Present (Visible_Declarations (Def)) then + Decl := First (Visible_Declarations (Def)); + while Present (Decl) loop + + -- Preserve the following declaration for iteration purposes due + -- to possible relocation of a pragma. + + Next_Decl := Next (Decl); + + if Nkind (Decl) = N_Pragma + and then Pragma_On_Anonymous_Object_OK (Get_Pragma_Id (Decl)) + then + Remove (Decl); + Insert_After (Obj_Decl, Decl); + + -- Skip internally generated code + + elsif not Comes_From_Source (Decl) then + null; + + -- No candidate pragmas are available for relocation + + else + exit; + end if; + + Decl := Next_Decl; + end loop; + end if; + end Relocate_Pragmas_To_Anonymous_Object; + ------------------------------ -- Relocate_Pragmas_To_Body -- ------------------------------ diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index e8c647e..7ec4ebb 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -152,9 +152,19 @@ package Sem_Prag is others => False); -- The following table lists all the implementation-defined pragmas that + -- should apply to the anonymous object produced by the analysis of a + -- single protected or task type. The table should be synchronized with + -- Aspect_On_Anonymous_Object_OK in unit Aspects. + + Pragma_On_Anonymous_Object_OK : constant array (Pragma_Id) of Boolean := + (Pragma_Depends => True, + Pragma_Global => True, + Pragma_Part_Of => True, + others => False); + + -- The following table lists all the implementation-defined pragmas that -- may apply to a body stub (no language defined pragmas apply). The table - -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if - -- the pragmas below implement an aspect. + -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects. Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean := (Pragma_Refined_Depends => True, @@ -195,9 +205,11 @@ package Sem_Prag is procedure Analyze_Initializes_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Initializes + procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id); + -- Perform full analysis of delayed pragma Part_Of + procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id); - -- Perform preanalysis of [refined] precondition or postcondition pragma - -- N that appears on a subprogram declaration or body [stub]. + -- Perform full analysis of pragmas Precondition and Postcondition procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id); -- Preform full analysis of delayed pragma Refined_Depends. This routine @@ -436,6 +448,14 @@ package Sem_Prag is -- Suppress_All at this stage, since it can appear after the unit instead -- of before (actually we allow it to appear anywhere). + procedure Relocate_Pragmas_To_Anonymous_Object + (Typ_Decl : Node_Id; + Obj_Decl : Node_Id); + -- Relocate all pragmas that appear in the visible declarations of task or + -- protected type declaration Typ_Decl after the declaration of anonymous + -- object Obj_Decl. Table Pragmas_On_Anonymous_Object_OK contains the list + -- of candidate pragmas. + procedure Relocate_Pragmas_To_Body (Subp_Body : Node_Id; Target_Body : Node_Id := Empty); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 1ac0a2f..3125b37 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -4951,75 +4951,71 @@ package body Sem_Util is --------------------- function Defining_Entity (N : Node_Id) return Entity_Id is - K : constant Node_Kind := Nkind (N); Err : Entity_Id := Empty; begin - case K is - when - N_Subprogram_Declaration | - N_Abstract_Subprogram_Declaration | - N_Subprogram_Body | - N_Package_Declaration | - N_Subprogram_Renaming_Declaration | - N_Subprogram_Body_Stub | - N_Generic_Subprogram_Declaration | - N_Generic_Package_Declaration | - N_Formal_Subprogram_Declaration | - N_Expression_Function + case Nkind (N) is + when N_Abstract_Subprogram_Declaration | + N_Expression_Function | + N_Formal_Subprogram_Declaration | + N_Generic_Package_Declaration | + N_Generic_Subprogram_Declaration | + N_Package_Declaration | + N_Subprogram_Body | + N_Subprogram_Body_Stub | + N_Subprogram_Declaration | + N_Subprogram_Renaming_Declaration => return Defining_Entity (Specification (N)); - when - N_Component_Declaration | - N_Defining_Program_Unit_Name | - N_Discriminant_Specification | - N_Entry_Body | - N_Entry_Declaration | - N_Entry_Index_Specification | - N_Exception_Declaration | - N_Exception_Renaming_Declaration | - N_Formal_Object_Declaration | - N_Formal_Package_Declaration | - N_Formal_Type_Declaration | - N_Full_Type_Declaration | - N_Implicit_Label_Declaration | - N_Incomplete_Type_Declaration | - N_Loop_Parameter_Specification | - N_Number_Declaration | - N_Object_Declaration | - N_Object_Renaming_Declaration | - N_Package_Body_Stub | - N_Parameter_Specification | - N_Private_Extension_Declaration | - N_Private_Type_Declaration | - N_Protected_Body | - N_Protected_Body_Stub | - N_Protected_Type_Declaration | - N_Single_Protected_Declaration | - N_Single_Task_Declaration | - N_Subtype_Declaration | - N_Task_Body | - N_Task_Body_Stub | - N_Task_Type_Declaration + when N_Component_Declaration | + N_Defining_Program_Unit_Name | + N_Discriminant_Specification | + N_Entry_Body | + N_Entry_Declaration | + N_Entry_Index_Specification | + N_Exception_Declaration | + N_Exception_Renaming_Declaration | + N_Formal_Object_Declaration | + N_Formal_Package_Declaration | + N_Formal_Type_Declaration | + N_Full_Type_Declaration | + N_Implicit_Label_Declaration | + N_Incomplete_Type_Declaration | + N_Loop_Parameter_Specification | + N_Number_Declaration | + N_Object_Declaration | + N_Object_Renaming_Declaration | + N_Package_Body_Stub | + N_Parameter_Specification | + N_Private_Extension_Declaration | + N_Private_Type_Declaration | + N_Protected_Body | + N_Protected_Body_Stub | + N_Protected_Type_Declaration | + N_Single_Protected_Declaration | + N_Single_Task_Declaration | + N_Subtype_Declaration | + N_Task_Body | + N_Task_Body_Stub | + N_Task_Type_Declaration => return Defining_Identifier (N); when N_Subunit => return Defining_Entity (Proper_Body (N)); - when - N_Function_Instantiation | - N_Function_Specification | - N_Generic_Function_Renaming_Declaration | - N_Generic_Package_Renaming_Declaration | - N_Generic_Procedure_Renaming_Declaration | - N_Package_Body | - N_Package_Instantiation | - N_Package_Renaming_Declaration | - N_Package_Specification | - N_Procedure_Instantiation | - N_Procedure_Specification + when N_Function_Instantiation | + N_Function_Specification | + N_Generic_Function_Renaming_Declaration | + N_Generic_Package_Renaming_Declaration | + N_Generic_Procedure_Renaming_Declaration | + N_Package_Body | + N_Package_Instantiation | + N_Package_Renaming_Declaration | + N_Package_Specification | + N_Procedure_Instantiation | + N_Procedure_Specification => declare Nam : constant Node_Id := Defining_Unit_Name (N); @@ -5028,8 +5024,8 @@ package body Sem_Util is if Nkind (Nam) in N_Entity then return Nam; - -- For Error, make up a name and attach to declaration - -- so we can continue semantic analysis + -- For Error, make up a name and attach to declaration so we + -- can continue semantic analysis. elsif Nam = Error then Err := Make_Temporary (Sloc (N), 'T'); @@ -5044,10 +5040,8 @@ package body Sem_Util is end if; end; - when - N_Block_Statement | - N_Loop_Statement - => + when N_Block_Statement | + N_Loop_Statement => return Entity (Identifier (N)); when others => @@ -7088,6 +7082,70 @@ package body Sem_Util is end if; end First_Actual; + ------------- + -- Fix_Msg -- + ------------- + + function Fix_Msg (Id : Entity_Id; Msg : String) return String is + Is_Task : constant Boolean := + Ekind_In (Id, E_Task_Body, E_Task_Type) + or else (Is_Single_Concurrent_Object (Id) + and then Ekind (Etype (Id)) = E_Task_Type); + Msg_Last : constant Natural := Msg'Last; + Msg_Index : Natural; + Res : String (Msg'Range) := (others => ' '); + Res_Index : Natural; + + begin + -- Copy all characters from the input message Msg to result Res with + -- suitable replacements. + + Msg_Index := Msg'First; + Res_Index := Res'First; + while Msg_Index <= Msg_Last loop + + -- Replace "subprogram" with a different word + + if Msg_Index <= Msg_Last - 10 + and then Msg (Msg_Index .. Msg_Index + 9) = "subprogram" + then + if Ekind_In (Id, E_Entry, E_Entry_Family) then + Res (Res_Index .. Res_Index + 4) := "entry"; + Res_Index := Res_Index + 5; + + elsif Is_Task then + Res (Res_Index .. Res_Index + 8) := "task unit"; + Res_Index := Res_Index + 9; + + else + Res (Res_Index .. Res_Index + 9) := "subprogram"; + Res_Index := Res_Index + 10; + end if; + + Msg_Index := Msg_Index + 10; + + -- Replace "protected" with a different word + + elsif Msg_Index <= Msg_Last - 9 + and then Msg (Msg_Index .. Msg_Index + 8) = "protected" + and then Is_Task + then + Res (Res_Index .. Res_Index + 3) := "task"; + Res_Index := Res_Index + 4; + Msg_Index := Msg_Index + 9; + + -- Otherwise copy the character + + else + Res (Res_Index) := Msg (Msg_Index); + Msg_Index := Msg_Index + 1; + Res_Index := Res_Index + 1; + end if; + end loop; + + return Res (Res'First .. Res_Index - 1); + end Fix_Msg; + ----------------------- -- Gather_Components -- ----------------------- @@ -8740,6 +8798,92 @@ package body Sem_Util is end if; end Has_Enabled_Property; + ------------------------------------- + -- Has_Full_Default_Initialization -- + ------------------------------------- + + function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is + Comp : Entity_Id; + + begin + -- A scalar type is fully default initialized if it is subjec to aspect + -- Default_Value. + + if Is_Scalar_Type (Typ) then + return Has_Default_Aspect (Typ); + + -- An array type is fully default initialized if its element type is + -- scalar and the array type carries aspect Default_Component_Value or + -- the element type is fully default initialized. + + elsif Is_Array_Type (Typ) then + return + Has_Default_Aspect (Typ) + or else Has_Full_Default_Initialization (Component_Type (Typ)); + + -- A protected type, record type or type extension is fully default + -- initialized if all its components either carry an initialization + -- expression or have a type that is fully default initialized. The + -- parent type of a type extension must be fully default initialized. + + elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then + + -- Inspect all entities defined in the scope of the type, looking for + -- uninitialized components. + + Comp := First_Entity (Typ); + while Present (Comp) loop + if Ekind (Comp) = E_Component + and then Comes_From_Source (Comp) + and then No (Expression (Parent (Comp))) + and then not Has_Full_Default_Initialization (Etype (Comp)) + then + return False; + end if; + + Next_Entity (Comp); + end loop; + + -- Ensure that the parent type of a type extension is fully default + -- initialized. + + if Etype (Typ) /= Typ + and then not Has_Full_Default_Initialization (Etype (Typ)) + then + return False; + end if; + + -- If we get here, then all components and parent portion are fully + -- default initialized. + + return True; + + -- A task type is fully default initialized by default + + elsif Is_Task_Type (Typ) then + return True; + end if; + + -- A private type and by extension its full view is fully default + -- initialized if it is subject to pragma Default_Initial_Condition + -- with a non-null argument or inherits the pragma from a parent type. + -- Since any type can act as the full view of a private type, this check + -- is separated from the circuitry above. + + if Has_Default_Init_Cond (Typ) + or else Has_Inherited_Default_Init_Cond (Typ) + then + return + Nkind (First (Pragma_Argument_Associations (Get_Pragma + (Typ, Pragma_Default_Initial_Condition)))) /= N_Null; + + -- Otherwise the type is not fully default initialized + + else + return False; + end if; + end Has_Full_Default_Initialization; + -------------------- -- Has_Infinities -- -------------------- @@ -11357,6 +11501,42 @@ package body Sem_Util is end if; end Is_Descendent_Of; + ---------------------------------------- + -- Is_Descendant_Of_Suspension_Object -- + ---------------------------------------- + + function Is_Descendant_Of_Suspension_Object + (Typ : Entity_Id) return Boolean + is + Cur_Typ : Entity_Id; + Par_Typ : Entity_Id; + + begin + -- Climb the type derivation chain checking each parent type against + -- Suspension_Object. + + Cur_Typ := Base_Type (Typ); + while Present (Cur_Typ) loop + Par_Typ := Etype (Cur_Typ); + + -- The current type is a match + + if Is_Suspension_Object (Cur_Typ) then + return True; + + -- Stop the traversal once the root of the derivation chain has been + -- reached. In that case the current type is its own base type. + + elsif Cur_Typ = Par_Typ then + exit; + end if; + + Cur_Typ := Base_Type (Par_Typ); + end loop; + + return False; + end Is_Descendant_Of_Suspension_Object; + --------------------------------------------- -- Is_Double_Precision_Floating_Point_Type -- --------------------------------------------- @@ -11376,50 +11556,6 @@ package body Sem_Util is ----------------------------- function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is - function Is_Descendant_Of_Suspension_Object - (Typ : Entity_Id) return Boolean; - -- Determine whether type Typ is a descendant of type Suspension_Object - -- defined in Ada.Synchronous_Task_Control. - - ---------------------------------------- - -- Is_Descendant_Of_Suspension_Object -- - ---------------------------------------- - - function Is_Descendant_Of_Suspension_Object - (Typ : Entity_Id) return Boolean - is - Cur_Typ : Entity_Id; - Par_Typ : Entity_Id; - - begin - -- Climb the type derivation chain checking each parent type against - -- Suspension_Object. - - Cur_Typ := Base_Type (Typ); - while Present (Cur_Typ) loop - Par_Typ := Etype (Cur_Typ); - - -- The current type is a match - - if Is_Suspension_Object (Cur_Typ) then - return True; - - -- Stop the traversal once the root of the derivation chain has - -- been reached. In that case the current type is its own base - -- type. - - elsif Cur_Typ = Par_Typ then - exit; - end if; - - Cur_Typ := Base_Type (Par_Typ); - end loop; - - return False; - end Is_Descendant_Of_Suspension_Object; - - -- Start of processing for Is_Effectively_Volatile - begin if Is_Type (Id) then @@ -12969,6 +13105,41 @@ package body Sem_Util is end if; end Is_Selector_Name; + --------------------------------- + -- Is_Single_Concurrent_Object -- + --------------------------------- + + function Is_Single_Concurrent_Object (Id : Entity_Id) return Boolean is + begin + return + Ekind (Id) = E_Variable + and then Is_Single_Concurrent_Type (Etype (Id)); + end Is_Single_Concurrent_Object; + + ------------------------------- + -- Is_Single_Concurrent_Type -- + ------------------------------- + + function Is_Single_Concurrent_Type (Id : Entity_Id) return Boolean is + begin + return + Ekind_In (Id, E_Protected_Type, E_Task_Type) + and then Is_Single_Concurrent_Type_Declaration + (Declaration_Node (Id)); + end Is_Single_Concurrent_Type; + + ------------------------------------------- + -- Is_Single_Concurrent_Type_Declaration -- + ------------------------------------------- + + function Is_Single_Concurrent_Type_Declaration + (N : Node_Id) return Boolean + is + begin + return Nkind_In (Original_Node (N), N_Single_Protected_Declaration, + N_Single_Task_Declaration); + end Is_Single_Concurrent_Type_Declaration; + --------------------------------------------- -- Is_Single_Precision_Floating_Point_Type -- --------------------------------------------- @@ -13231,6 +13402,49 @@ package body Sem_Util is and then Scope (Scope (Scope (Id))) = Standard_Standard; end Is_Suspension_Object; + ---------------------------- + -- Is_Synchronized_Object -- + ---------------------------- + + function Is_Synchronized_Object (Id : Entity_Id) return Boolean is + Prag : Node_Id; + + begin + if Is_Object (Id) then + + -- The object is synchronized if it is of a type that yields a + -- synchronized object. + + if Yields_Synchronized_Object (Etype (Id)) then + return True; + + -- The object is synchronized if it is atomic and Async_Writers is + -- enabled. + + elsif Is_Atomic (Id) and then Async_Writers_Enabled (Id) then + return True; + + -- A constant is a synchronized object by default + + elsif Ekind (Id) = E_Constant then + return True; + + -- A variable is a synchronized object if it is subject to pragma + -- Constant_After_Elaboration. + + elsif Ekind (Id) = E_Variable then + Prag := Get_Pragma (Id, Pragma_Constant_After_Elaboration); + + return Present (Prag) and then Is_Enabled_Pragma (Prag); + end if; + end if; + + -- Otherwise the input is not an object or it does not qualify as a + -- synchronized object. + + return False; + end Is_Synchronized_Object; + --------------------------------- -- Is_Synchronized_Tagged_Type -- --------------------------------- @@ -19880,4 +20094,88 @@ package body Sem_Util is end if; end Wrong_Type; + -------------------------------- + -- Yields_Synchronized_Object -- + -------------------------------- + + function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean is + Id : Entity_Id; + + begin + -- An array type yields a synchronized object if its component type + -- yields a synchronized object. + + if Is_Array_Type (Typ) then + return Yields_Synchronized_Object (Component_Type (Typ)); + + -- A descendant of type Ada.Synchronous_Task_Control.Suspension_Object + -- yields a synchronized object by default. + + elsif Is_Descendant_Of_Suspension_Object (Typ) then + return True; + + -- A protected type yields a synchronized object by default + + elsif Is_Protected_Type (Typ) then + return True; + + -- A record type or type extension yields a synchronized object when its + -- discriminants (if any) lack default values and all components are of + -- a type that yelds a synchronized object. + + elsif Is_Record_Type (Typ) then + + -- Inspect all entities defined in the scope of the type, looking for + -- components of a type that does not yeld a synchronized object or + -- for discriminants with default values. + + Id := First_Entity (Typ); + while Present (Id) loop + if Comes_From_Source (Id) then + if Ekind (Id) = E_Component + and then not Yields_Synchronized_Object (Etype (Id)) + then + return False; + + elsif Ekind (Id) = E_Discriminant + and then Present (Expression (Parent (Id))) + then + return False; + end if; + end if; + + Next_Entity (Id); + end loop; + + -- Ensure that the parent type of a type extension yields a + -- synchronized object. + + if Etype (Typ) /= Typ + and then not Yields_Synchronized_Object (Etype (Typ)) + then + return False; + end if; + + -- If we get here, then all discriminants lack default values and all + -- components are of a type that yields a synchronized object. + + return True; + + -- A synchronized interface type yields a synchronized object by default + + elsif Is_Synchronized_Interface (Typ) then + return True; + + -- A task type yelds a synchronized object by default + + elsif Is_Task_Type (Typ) then + return True; + + -- Otherwise the type does not yield a synchronized object + + else + return False; + end if; + end Yields_Synchronized_Object; + end Sem_Util; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index c68eb08..95534d9 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -765,6 +765,17 @@ package Sem_Util is -- Note that the value returned is always the expression (not the -- N_Parameter_Association nodes, even if named association is used). + function Fix_Msg (Id : Entity_Id; Msg : String) return String; + -- Replace all occurrences of a particular word in string Msg depending on + -- 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 + -- body. + -- * Replace "protected" with + -- - "task" when Id is a single task object, task type or task body + -- All other non-matching words remain as is + procedure Gather_Components (Typ : Entity_Id; Comp_List : Node_Id; @@ -953,9 +964,6 @@ package Sem_Util is -- as an access type internally, this function tests only for access types -- known to the programmer. See also Has_Tagged_Component. - function Has_Defaulted_Discriminants (Typ : Entity_Id) return Boolean; - -- Simple predicate to test for defaulted discriminants - type Alignment_Result is (Known_Compatible, Unknown, Known_Incompatible); -- Result of Has_Compatible_Alignment test, description found below. Note -- that the values are arranged in increasing order of problematicness. @@ -983,6 +991,9 @@ package Sem_Util is function Has_Declarations (N : Node_Id) return Boolean; -- Determines if the node can have declarations + function Has_Defaulted_Discriminants (Typ : Entity_Id) return Boolean; + -- Simple predicate to test for defaulted discriminants + function Has_Denormals (E : Entity_Id) return Boolean; -- Determines if the floating-point type E supports denormal numbers. -- Returns False if E is not a floating-point type. @@ -997,6 +1008,19 @@ package Sem_Util is -- Determine whether subprogram Subp_Id has an effectively volatile formal -- parameter or returns an effectively volatile value. + function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ defines "full default initialization" as + -- specified by SPARK RM 3.1. To qualify as such, the type must be + -- * A scalar type with specified Default_Value + -- * An array-of-scalar type with specified Default_Component_Value + -- * An array type whose element type defines full default initialization + -- * A protected type, record type or type extension whose components + -- either include a default expression or have a type which defines + -- full default initialization. In the case of type extensions, the + -- parent type defines full default initialization. + -- * A task type + -- * A private type whose Default_Initial_Condition is non-null + function Has_Infinities (E : Entity_Id) return Boolean; -- Determines if the range of the floating-point type E includes -- infinities. Returns False if E is not a floating-point type. @@ -1274,6 +1298,13 @@ package Sem_Util is -- This is the RM definition, a type is a descendent of another type if it -- is the same type or is derived from a descendent of the other type. + function Is_Descendant_Of_Suspension_Object + (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ is a descendant of type Suspension_Object + -- defined in Ada.Synchronous_Task_Control. This version is different from + -- Is_Descendent_Of as the detection of Suspension_Object does not involve + -- an entity and by extension a call to RTSfind. + function Is_Double_Precision_Floating_Point_Type (E : Entity_Id) return Boolean; -- Return whether E is a double precision floating point type, @@ -1463,6 +1494,18 @@ package Sem_Util is -- represent use of the N_Identifier node for a true identifier, when -- normally such nodes represent a direct name. + function Is_Single_Concurrent_Object (Id : Entity_Id) return Boolean; + -- Determine whether arbitrary entity Id denotes the anonymous object + -- created for a single protected or single task type. + + function Is_Single_Concurrent_Type (Id : Entity_Id) return Boolean; + -- Determine whether arbitrary entity Id denotes a single protected or + -- single task type. + + function Is_Single_Concurrent_Type_Declaration (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes the declaration of a single + -- protected type or single task type. + function Is_Single_Precision_Floating_Point_Type (E : Entity_Id) return Boolean; -- Return whether E is a single precision floating point type, @@ -1520,6 +1563,15 @@ package Sem_Util is -- Determine whether arbitrary entity Id denotes Suspension_Object defined -- in Ada.Synchronous_Task_Control. + function Is_Synchronized_Object (Id : Entity_Id) return Boolean; + -- Determine whether entity Id denotes an object and if it does, whether + -- this object is synchronized as specified in SPARK RM 9.1. To qualify as + -- such, the object must be + -- * Of a type that yields a synchronized object + -- * An atomic object with enabled Async_Writers + -- * A constant + -- * A variable subject to pragma Constant_After_Elaboration + function Is_Synchronized_Tagged_Type (E : Entity_Id) return Boolean; -- Returns True if E is a synchronized tagged type (AARM 3.9.4 (6/2)) @@ -2161,4 +2213,15 @@ package Sem_Util is -- does not have to be a subexpression, anything with an Etype field may -- be used. + function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ "yields synchronized object" as specified by + -- SPARK RM 9.1. To qualify as such, a type must be + -- * An array type whose element type yields a synchronized object + -- * A descendant of type Ada.Synchronous_Task_Control.Suspension_Object + -- * A protected type + -- * A record type or type extension without defaulted discriminants + -- whose components are of a type that yields a synchronized object. + -- * A synchronized interface type + -- * A task type + end Sem_Util; diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index c0860e4..6d9ca7d 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -788,6 +788,7 @@ package Snames is Name_Strict : constant Name_Id := N + $; Name_Subunit_File_Name : constant Name_Id := N + $; Name_Suppressed : constant Name_Id := N + $; + Name_Synchronous : constant Name_Id := N + $; Name_Task_Stack_Size_Default : constant Name_Id := N + $; Name_Task_Type : constant Name_Id := N + $; Name_Time_Slicing_Enabled : constant Name_Id := N + $; |