OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

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.

From-SVN: r229357
This commit is contained in:
Arnaud Charlet 2015-10-26 14:23:35 +01:00
parent 90707ac1bb
commit 75b87c163f
22 changed files with 1960 additions and 819 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

144
gcc/ada/ChangeLog
View File

@ -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

24
gcc/ada/aspects.adb
View File

@ -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

34
gcc/ada/aspects.ads
View File

@ -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

17
gcc/ada/atree.adb
View File

@ -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);

6
gcc/ada/atree.ads
View File

@ -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);

1
gcc/ada/atree.h
View File

@ -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)

249
gcc/ada/contracts.adb
View File

@ -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
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
if Present (Prag) then
Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
Seen := True;
if Restore_Mode then
Restore_SPARK_Mode (Mode);
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;
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);

20
gcc/ada/contracts.ads
View File

@ -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

165
gcc/ada/einfo.adb
View File

@ -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 =>

86
gcc/ada/einfo.ads
View File

@ -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);

2
gcc/ada/exp_ch6.adb
View File

@ -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);

2
gcc/ada/exp_ch7.adb
View File

@ -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.

19
gcc/ada/freeze.adb
View File

@ -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

51
gcc/ada/sem_ch13.adb
View File

@ -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

35
gcc/ada/sem_ch3.adb
View File

@ -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

215
gcc/ada/sem_ch9.adb
View File

@ -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)));
O_Decl :=
-- 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:
-- 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_Protected_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 aspect Part_Of from the the original single protected
-- declaration to the anonymous object declaration. This emulates the
-- placement of an equivalent source pragma.
Move_Or_Merge_Aspects (N, To => Obj_Decl);
-- 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.
Relocate_Pragmas_To_Anonymous_Object (N, Obj_Decl);
-- 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:
T :=
Make_Defining_Identifier (Sloc (Id),
New_External_Name (Chars (Id), Suffix => "TK"));
-- task type Typ is ...;
T_Decl :=
Typ :=
Make_Defining_Identifier (Sloc (Obj_Id),
Chars => New_External_Name (Chars (Obj_Id), Suffix => "TK"));
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));
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.
-- 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:
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));
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;

66
gcc/ada/sem_elab.adb
View File

@ -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

1033
gcc/ada/sem_prag.adb
View File

File diff suppressed because it is too large Load Diff

28
gcc/ada/sem_prag.ads
View File

@ -151,10 +151,20 @@ package Sem_Prag is
Pragma_Type_Invariant_Class => True,
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);

512
gcc/ada/sem_util.adb
View File

@ -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;

69
gcc/ada/sem_util.ads
View File

@ -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;

1
gcc/ada/snames.ads-tmpl
View File

@ -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 + $;