mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-13 12:11:08 +08:00
Code Issues Packages Projects Releases Wiki Activity

2014-01-29 Hristian Kirtchev <kirtchev@adacore.com>

Browse Source 
* aspects.adb Add an entry for aspect Part_Of in table
	Canonical_Aspect.
	* aspects.ads Add an entry for aspect Part_Of in tables Aspect_Id,
	Aspect_Argument, Aspect_Names and Aspect_Delay.
	* atree.h Define Elist9.
	* atree.adb (Elist9): New routine.
	(Set_Elist9): New routine.
	* atree.ads (Elist9): New routine.
	(Set_Elist9): New routine.
	* einfo.adb Add Part_Of_Constituents and Encapsulating_State to
	the list of node usage.  Remove Refined_State from the list of
	node usage.
	(Encapsulating_State): New routine.
	(Get_Pragma):
	Handle pragma Part_Of; (Part_Of_Constituents): New routine.
	(Refined_State): Removed.
	(Set_Encapsulating_State): New routine.
	(Set_Part_Of_Constituents): New routine.
	(Set_Refined_State): Removed.
	(Write_Field9_Name): Add an entry
	for Part_Of_Constituents (Write_Field10_Name): Add an entry for
	Encapsulating_State. Remove the entry for Refined_State.
	* einfo.ads Add new attributes Encapsulating_State
	and Part_Of_Constituents alond with their usage in
	entities. Remove attribute Refined_State along with its
	usage in entities.
	(Encapsulating_State): New routine and
	pragma Inline.	(Get_Pragma): Update the comment on usage.
	(Part_Of_Constituents): New routine and pragma Inline.
	(Refined_State): Removed along with pragma Inline.
	(Set_Encapsulating_State): New routine and pragma Inline.
	(Set_Part_Of_Constituents): New routine and pragma Inline.
	(Set_Refined_State): Removed along with pragma Inline.
	* par-prag.adb Pragma Part_Of does not need any special processing
	by the parser.
	* sem_ch3.adb (Analyze_Declarations): Remove local variables
	Body_Id and Prag. Call separate routines to analyze the
	contract of a package [body].
	(Analyze_Object_Contract):
	Update the comment on usage. Remove local variables
	Items and Nam. Use Get_Pragma rather than traversing the
	classification list.  Verify whether the lack of indicator
	Part_Of agrees with the placement of the variable in state space.
	(Analyze_Object_Declaration): Initialize the encapsulating state
	of a variable.	(Requires_State_Refinement): Moved to sem_util.
	* sem_ch7.adb (Analyze_Package_Body_Contract): New routine.
	(Analyze_Package_Contract): New routine.
	* sem_ch7.ads (Analyze_Package_Body_Contract): New routine.
	(Analyze_Package_Contract): New routine.
	* sem_ch10.adb (Decorate_State): Initialize the encapsulating
	state and Part_Of constituents.
	* sem_ch13.adb (Analyze_Aspect_Specifications):
	Add processing for aspect Part_Of. Update all
	calls to Decorate_Delayed_Aspect_And_Pragma.
	(Check_Aspect_At_Freeze_Point): Aspect Part_Of does
	not need any special processing at freeze time.
	(Decorate_Delayed_Aspect_And_Pragma): Renamed to
	Decorate_Aspect_And_Pragma.  Add formal parameter Delayed and
	update the associated comment.
	* sem_prag.adb Add an entry for pragma Part_Of in table Sig_Flags.
	(Analyze_Abstract_State): Add new global variable State_Id. Remove
	local constants Errors and Loc. Remove local variables Is_Null
	and State_Nam. Create the entity of the abstract state on the
	spot, before all remaining checks are performed. Verify that a
	missing Part_Of option agrees with the placement of the abstract
	state within the state space.
	(Analyze_Depends_In_Decl_Part):
	Add new global variables Constits_Seen and States_Seen. Check
	that a state and a corresponding constituent do not appear
	in pragma [Refined_]Depends.
	(Analyze_Global_In_Decl_Part):
	Add new global variables Constits_Seen and States_Seen. Check
	that a state and a corresponding constituent do not appear
	in pragma [Refined_]Global.
	(Analyze_Global_Item):
	Remove the now obsolete code that deals with Part_Of.
	Add the entity of the global item to the list of processed
	items.	(Analyze_Initializes_In_Decl_Part): Add new global
	variables Constits_Seen and States_Seen. Check that a state
	and a corresponding constituent do not appear in pragma
	Initializes.
	(Analyze_Initialization_Item): Add the entity
	of the initialization item to the list of processed items.
	(Analyze_Input_Item): Add the entity of the initialization
	item to the list of processed items.
	(Analyze_Input_Output):
	Remove the now obsolete code that deals with Part_Of.  Add the
	entity of the input/output to the list of processed items.
	(Analyze_Part_Of): New routine.
	(Analyze_Part_Of_Option): Remove
	local constant Par_State. Add local constant Encaps and local
	variables Encaps_Id and Legal. Use Analyze_Part of to analyze
	the option. Turn the related state into a Part_Of constituent
	if the option is legal.
	(Analyze_Pragma): Add processing
	for pragma Part_Of.
	(Analyze_Refined_State_In_Decl_Part):
	Remove global constants Pack_Body and Spec_Id. Remove
	global variables Abstr_States and Hidden_States. Add new
	global variables Available_States, Body_Id, Body_States and
	Spec_Id. Add new local constant Body_Decl. Reimplement the
	logic that extracts the states available for refinement from
	the related package and the body hidden states of the said
	package.
	(Analyze_Refinement_Clause): Add local variable Part_Of_Constits.
	(Check_Applicable_Policy): Alphabetize body.
	(Check_Dependency_Clause): Replace Refined_State
	with Encapsulating_State.
	(Check_Matching_Constituent):
	Reimplement the logic that determines whether an item is a valid
	/ invalid constituent of the current refined state. Return when
	a construct does not denote a valid abstract state. Extract the
	list of Part_Of constituents for further analysis. Check that all
	Part_Of constituents of a state have been used in its refinement.
	(Check_Matching_State): Update the comment on usage. Operate
	on the list of available states.
	(Check_Missing_Part_Of): New routine.
	(Check_Refined_Global_Item): Replace Refined_State
	with Encapsulating_State.
	(Check_State_And_Constituent_Use): New routine.
	(Create_Abstract_State): New routine.
	(Is_Matching_Input): Replace Refined_State with Encapsulating_State.
	(Is_Part_Of): Removed.
	(Collect_Body_States): New routine.
	(Collect_Constituent): Replace Refined_State with Encapsulating_State.
	(Collect_Hidden_States): Removed.
	(Report_Unrefined_States): Change the profile of the procedure along
	with the comment on usage.
	(Report_Unused_Constituents): New routine.
	(Report_Unused_Hidden_States): Removed.
	(Report_Unused_States): New routine.
	* sem_prag.ads (Check_Missing_Part_Of): New routine.
	* sem_util.adb (Add_Contract_Item): Pragma Part_Of can now
	appear in the classification pragmas of a package instantiation
	or a variable.
	(Find_Placement_In_State_Space): New routine.
	(Is_Child): Removed.
	(Is_Child_Or_Sibling): Remove formal
	parameter Private_Child. Remove the private child checks.
	(Requires_State_Refinement): Moved from sem_ch3.
	* sem_util.ads Add new type State_Space_Kind along with
	comment on its usage and values.
	(Add_Contract_Item): Update the comment on usage.
	(Find_Body_Discriminal): Alphabetize spec.
	(Find_Placement_In_State_Space): New routine.
	(Is_Child_Or_Sibling): Remove formal parameter Private_Child
	and update the comment on usage.
	(Requires_State_Refinement): Moved from sem_ch3.
	* sinfo.ads: Update the documentation of N_Contract.
	* snames.ads-tmpl The predefined name for Part_Of is now used
	to denote a pragma. Add Pragma_Id for Part_Of.

From-SVN: r207251
This commit is contained in:
Hristian Kirtchev 2014-01-29 15:30:21 +00:00 committed by Arnaud Charlet
parent 0830210cff
commit d7af5ea5e1
20 changed files with 1701 additions and 648 deletions

154
gcc/ada/ChangeLog

@ -1,3 +1,157 @@
2014-01-29 Hristian Kirtchev <kirtchev@adacore.com>
* aspects.adb Add an entry for aspect Part_Of in table
Canonical_Aspect.
* aspects.ads Add an entry for aspect Part_Of in tables Aspect_Id,
Aspect_Argument, Aspect_Names and Aspect_Delay.
* atree.h Define Elist9.
* atree.adb (Elist9): New routine.
(Set_Elist9): New routine.
* atree.ads (Elist9): New routine.
(Set_Elist9): New routine.
* einfo.adb Add Part_Of_Constituents and Encapsulating_State to
the list of node usage. Remove Refined_State from the list of
node usage.
(Encapsulating_State): New routine.
(Get_Pragma):
Handle pragma Part_Of; (Part_Of_Constituents): New routine.
(Refined_State): Removed.
(Set_Encapsulating_State): New routine.
(Set_Part_Of_Constituents): New routine.
(Set_Refined_State): Removed.
(Write_Field9_Name): Add an entry
for Part_Of_Constituents (Write_Field10_Name): Add an entry for
Encapsulating_State. Remove the entry for Refined_State.
* einfo.ads Add new attributes Encapsulating_State
and Part_Of_Constituents alond with their usage in
entities. Remove attribute Refined_State along with its
usage in entities.
(Encapsulating_State): New routine and
pragma Inline. (Get_Pragma): Update the comment on usage.
(Part_Of_Constituents): New routine and pragma Inline.
(Refined_State): Removed along with pragma Inline.
(Set_Encapsulating_State): New routine and pragma Inline.
(Set_Part_Of_Constituents): New routine and pragma Inline.
(Set_Refined_State): Removed along with pragma Inline.
* par-prag.adb Pragma Part_Of does not need any special processing
by the parser.
* sem_ch3.adb (Analyze_Declarations): Remove local variables
Body_Id and Prag. Call separate routines to analyze the
contract of a package [body].
(Analyze_Object_Contract):
Update the comment on usage. Remove local variables
Items and Nam. Use Get_Pragma rather than traversing the
classification list. Verify whether the lack of indicator
Part_Of agrees with the placement of the variable in state space.
(Analyze_Object_Declaration): Initialize the encapsulating state
of a variable. (Requires_State_Refinement): Moved to sem_util.
* sem_ch7.adb (Analyze_Package_Body_Contract): New routine.
(Analyze_Package_Contract): New routine.
* sem_ch7.ads (Analyze_Package_Body_Contract): New routine.
(Analyze_Package_Contract): New routine.
* sem_ch10.adb (Decorate_State): Initialize the encapsulating
state and Part_Of constituents.
* sem_ch13.adb (Analyze_Aspect_Specifications):
Add processing for aspect Part_Of. Update all
calls to Decorate_Delayed_Aspect_And_Pragma.
(Check_Aspect_At_Freeze_Point): Aspect Part_Of does
not need any special processing at freeze time.
(Decorate_Delayed_Aspect_And_Pragma): Renamed to
Decorate_Aspect_And_Pragma. Add formal parameter Delayed and
update the associated comment.
* sem_prag.adb Add an entry for pragma Part_Of in table Sig_Flags.
(Analyze_Abstract_State): Add new global variable State_Id. Remove
local constants Errors and Loc. Remove local variables Is_Null
and State_Nam. Create the entity of the abstract state on the
spot, before all remaining checks are performed. Verify that a
missing Part_Of option agrees with the placement of the abstract
state within the state space.
(Analyze_Depends_In_Decl_Part):
Add new global variables Constits_Seen and States_Seen. Check
that a state and a corresponding constituent do not appear
in pragma [Refined_]Depends.
(Analyze_Global_In_Decl_Part):
Add new global variables Constits_Seen and States_Seen. Check
that a state and a corresponding constituent do not appear
in pragma [Refined_]Global.
(Analyze_Global_Item):
Remove the now obsolete code that deals with Part_Of.
Add the entity of the global item to the list of processed
items. (Analyze_Initializes_In_Decl_Part): Add new global
variables Constits_Seen and States_Seen. Check that a state
and a corresponding constituent do not appear in pragma
Initializes.
(Analyze_Initialization_Item): Add the entity
of the initialization item to the list of processed items.
(Analyze_Input_Item): Add the entity of the initialization
item to the list of processed items.
(Analyze_Input_Output):
Remove the now obsolete code that deals with Part_Of. Add the
entity of the input/output to the list of processed items.
(Analyze_Part_Of): New routine.
(Analyze_Part_Of_Option): Remove
local constant Par_State. Add local constant Encaps and local
variables Encaps_Id and Legal. Use Analyze_Part of to analyze
the option. Turn the related state into a Part_Of constituent
if the option is legal.
(Analyze_Pragma): Add processing
for pragma Part_Of.
(Analyze_Refined_State_In_Decl_Part):
Remove global constants Pack_Body and Spec_Id. Remove
global variables Abstr_States and Hidden_States. Add new
global variables Available_States, Body_Id, Body_States and
Spec_Id. Add new local constant Body_Decl. Reimplement the
logic that extracts the states available for refinement from
the related package and the body hidden states of the said
package.
(Analyze_Refinement_Clause): Add local variable Part_Of_Constits.
(Check_Applicable_Policy): Alphabetize body.
(Check_Dependency_Clause): Replace Refined_State
with Encapsulating_State.
(Check_Matching_Constituent):
Reimplement the logic that determines whether an item is a valid
/ invalid constituent of the current refined state. Return when
a construct does not denote a valid abstract state. Extract the
list of Part_Of constituents for further analysis. Check that all
Part_Of constituents of a state have been used in its refinement.
(Check_Matching_State): Update the comment on usage. Operate
on the list of available states.
(Check_Missing_Part_Of): New routine.
(Check_Refined_Global_Item): Replace Refined_State
with Encapsulating_State.
(Check_State_And_Constituent_Use): New routine.
(Create_Abstract_State): New routine.
(Is_Matching_Input): Replace Refined_State with Encapsulating_State.
(Is_Part_Of): Removed.
(Collect_Body_States): New routine.
(Collect_Constituent): Replace Refined_State with Encapsulating_State.
(Collect_Hidden_States): Removed.
(Report_Unrefined_States): Change the profile of the procedure along
with the comment on usage.
(Report_Unused_Constituents): New routine.
(Report_Unused_Hidden_States): Removed.
(Report_Unused_States): New routine.
* sem_prag.ads (Check_Missing_Part_Of): New routine.
* sem_util.adb (Add_Contract_Item): Pragma Part_Of can now
appear in the classification pragmas of a package instantiation
or a variable.
(Find_Placement_In_State_Space): New routine.
(Is_Child): Removed.
(Is_Child_Or_Sibling): Remove formal
parameter Private_Child. Remove the private child checks.
(Requires_State_Refinement): Moved from sem_ch3.
* sem_util.ads Add new type State_Space_Kind along with
comment on its usage and values.
(Add_Contract_Item): Update the comment on usage.
(Find_Body_Discriminal): Alphabetize spec.
(Find_Placement_In_State_Space): New routine.
(Is_Child_Or_Sibling): Remove formal parameter Private_Child
and update the comment on usage.
(Requires_State_Refinement): Moved from sem_ch3.
* sinfo.ads: Update the documentation of N_Contract.
* snames.ads-tmpl The predefined name for Part_Of is now used
to denote a pragma. Add Pragma_Id for Part_Of.
2014-01-29 Emmanuel Briot <briot@adacore.com>
* s-regexp.adb (Create_Secondary_Table): Automatically grow the state

1
gcc/ada/aspects.adb

@ -523,6 +523,7 @@ package body Aspects is
Aspect_Object_Size => Aspect_Object_Size,
Aspect_Output => Aspect_Output,
Aspect_Pack => Aspect_Pack,
Aspect_Part_Of => Aspect_Part_Of,
Aspect_Persistent_BSS => Aspect_Persistent_BSS,
Aspect_Post => Aspect_Post,
Aspect_Postcondition => Aspect_Post,

4
gcc/ada/aspects.ads

@ -107,6 +107,7 @@ package Aspects is
Aspect_Machine_Radix,
Aspect_Object_Size, -- GNAT
Aspect_Output,
Aspect_Part_Of, -- GNAT
Aspect_Post,
Aspect_Postcondition,
Aspect_Pre,
@ -330,6 +331,7 @@ package Aspects is
Aspect_Machine_Radix => Expression,
Aspect_Object_Size => Expression,
Aspect_Output => Name,
Aspect_Part_Of => Expression,
Aspect_Post => Expression,
Aspect_Postcondition => Expression,
Aspect_Pre => Expression,
@ -429,6 +431,7 @@ package Aspects is
Aspect_Object_Size => Name_Object_Size,
Aspect_Output => Name_Output,
Aspect_Pack => Name_Pack,
Aspect_Part_Of => Name_Part_Of,
Aspect_Persistent_BSS => Name_Persistent_BSS,
Aspect_Post => Name_Post,
Aspect_Postcondition => Name_Postcondition,
@ -679,6 +682,7 @@ package Aspects is
Aspect_Convention => Never_Delay,
Aspect_Dimension => Never_Delay,
Aspect_Dimension_System => Never_Delay,
Aspect_Part_Of => Never_Delay,
Aspect_Refined_Post => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,

17
gcc/ada/atree.adb

@ -2758,6 +2758,17 @@ package body Atree is
end if;
end Elist8;
function Elist9 (N : Node_Id) return Elist_Id is
pragma Assert (Nkind (N) in N_Entity);
Value : constant Union_Id := Nodes.Table (N + 1).Field9;
begin
if Value = 0 then
return No_Elist;
else
return Elist_Id (Value);
end if;
end Elist9;
function Elist10 (N : Node_Id) return Elist_Id is
pragma Assert (Nkind (N) in N_Entity);
Value : constant Union_Id := Nodes.Table (N + 1).Field10;
@ -5476,6 +5487,12 @@ package body Atree is
Nodes.Table (N + 1).Field8 := Union_Id (Val);
end Set_Elist8;
procedure Set_Elist9 (N : Node_Id; Val : Elist_Id) is
begin
pragma Assert (Nkind (N) in N_Entity);
Nodes.Table (N + 1).Field9 := Union_Id (Val);
end Set_Elist9;
procedure Set_Elist10 (N : Node_Id; Val : Elist_Id) is
begin
pragma Assert (Nkind (N) in N_Entity);

6
gcc/ada/atree.ads

@ -1279,6 +1279,9 @@ package Atree is
function Elist8 (N : Node_Id) return Elist_Id;
pragma Inline (Elist8);
function Elist9 (N : Node_Id) return Elist_Id;
pragma Inline (Elist9);
function Elist10 (N : Node_Id) return Elist_Id;
pragma Inline (Elist10);
@ -2585,6 +2588,9 @@ package Atree is
procedure Set_Elist8 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist8);
procedure Set_Elist9 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist9);
procedure Set_Elist10 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist10);

1
gcc/ada/atree.h

@ -501,6 +501,7 @@ extern Node_Id Current_Error_Node;
#define Elist4(N) Field4 (N)
#define Elist5(N) Field5 (N)
#define Elist8(N) Field8 (N)
#define Elist9(N) Field9 (N)
#define Elist10(N) Field10 (N)
#define Elist13(N) Field13 (N)
#define Elist15(N) Field15 (N)

51
gcc/ada/einfo.adb

@ -86,14 +86,15 @@ package body Einfo is
-- Class_Wide_Type Node9
-- Current_Value Node9
-- Part_Of_Constituents Elist9
-- Renaming_Map Uint9
-- Encapsulating_State Node10
-- Direct_Primitive_Operations Elist10
-- Discriminal_Link Node10
-- Float_Rep Uint10 (but returns Float_Rep_Kind)
-- Handler_Records List10
-- Normalized_Position_Max Uint10
-- Refined_State Node10
-- Component_Bit_Offset Uint11
-- Full_View Node11
@ -1059,6 +1060,12 @@ package body Einfo is
return Flag174 (Id);
end Elaboration_Entity_Required;
function Encapsulating_State (Id : E) return N is
begin
pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
return Node10 (Id);
end Encapsulating_State;
function Enclosing_Scope (Id : E) return E is
begin
return Node18 (Id);
@ -2630,6 +2637,12 @@ package body Einfo is
return Node19 (Base_Type (Id));
end Parent_Subtype;
function Part_Of_Constituents (Id : E) return L is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
return Elist9 (Id);
end Part_Of_Constituents;
function Postcondition_Proc (Id : E) return E is
begin
pragma Assert (Ekind (Id) = E_Procedure);
@ -2705,12 +2718,6 @@ package body Einfo is
return Flag227 (Id);
end Referenced_As_Out_Parameter;
function Refined_State (Id : E) return N is
begin
pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
return Node10 (Id);
end Refined_State;
function Refinement_Constituents (Id : E) return L is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
@ -3714,6 +3721,12 @@ package body Einfo is
Set_Flag174 (Id, V);
end Set_Elaboration_Entity_Required;
procedure Set_Encapsulating_State (Id : E; V : E) is
begin
pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
Set_Node10 (Id, V);
end Set_Encapsulating_State;
procedure Set_Enclosing_Scope (Id : E; V : E) is
begin
Set_Node18 (Id, V);
@ -5352,6 +5365,12 @@ package body Einfo is
Set_Node19 (Id, V);
end Set_Parent_Subtype;
procedure Set_Part_Of_Constituents (Id : E; V : L) is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
Set_Elist9 (Id, V);
end Set_Part_Of_Constituents;
procedure Set_Postcondition_Proc (Id : E; V : E) is
begin
pragma Assert (Ekind (Id) = E_Procedure);
@ -5435,12 +5454,6 @@ package body Einfo is
Set_Flag227 (Id, V);
end Set_Referenced_As_Out_Parameter;
procedure Set_Refined_State (Id : E; V : E) is
begin
pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
Set_Node10 (Id, V);
end Set_Refined_State;
procedure Set_Refinement_Constituents (Id : E; V : L) is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
@ -6445,6 +6458,7 @@ package body Einfo is
Id = Pragma_Global or else
Id = Pragma_Initial_Condition or else
Id = Pragma_Initializes or else
Id = Pragma_Part_Of or else
Id = Pragma_Refined_Depends or else
Id = Pragma_Refined_Global or else
Id = Pragma_Refined_State;
@ -8535,6 +8549,9 @@ 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 |
@ -8555,6 +8572,10 @@ package body Einfo is
procedure Write_Field10_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
when E_Abstract_State |
E_Variable =>
Write_Str ("Encapsulating_State");
when Class_Wide_Kind |
Incomplete_Kind |
E_Record_Type |
@ -8580,10 +8601,6 @@ package body Einfo is
E_Discriminant =>
Write_Str ("Normalized_Position_Max");
when E_Abstract_State |
E_Variable =>
Write_Str ("Refined_State");
when others =>
Write_Str ("Field10??");
end case;

30
gcc/ada/einfo.ads

@ -976,6 +976,10 @@ package Einfo is
-- then if there is no other elaboration code, obviously there is no
-- need to set the flag.
-- Encapsulating_State (Node10)
-- Defined in abstract states and variables. Contains the entity of an
-- ancestor state whose refinement utilizes this item as a constituent.
-- Enclosing_Scope (Node18)
-- Defined in labels. Denotes the innermost enclosing construct that
-- contains the label. Identical to the scope of the label, except for
@ -3435,6 +3439,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).
-- Postcondition_Proc (Node8)
-- Defined only in procedure entities, saves the entity of the generated
-- postcondition proc if one is present, otherwise is set to Empty. Used
@ -3549,10 +3557,6 @@ package Einfo is
-- we have a separate warning for variables that are only assigned and
-- never read, and out parameters are a special case.
-- Refined_State (Node10)
-- Defined in abstract states and variables. Contains the entity of an
-- ancestor state whose refinement mentions this item.
-- Refinement_Constituents (Elist8)
-- Present in abstract state entities. Contains all the constituents that
-- refine the state, in other words, all the hidden states that appear in
@ -5146,7 +5150,8 @@ package Einfo is
-- E_Abstract_State
-- Refinement_Constituents (Elist8)
-- Refined_State (Node10)
-- Part_Of_Constituents (Elist9)
-- Encapsulating_State (Node10)
-- Body_References (Elist16)
-- Non_Limited_View (Node17)
-- From_Limited_With (Flag159)
@ -5982,7 +5987,7 @@ package Einfo is
-- E_Variable
-- Hiding_Loop_Variable (Node8)
-- Current_Value (Node9)
-- Refined_State (Node10)
-- Encapsulating_State (Node10)
-- Esize (Uint12)
-- Extra_Accessibility (Node13)
-- Alignment (Uint14)
@ -6328,6 +6333,7 @@ package Einfo is
function Elaborate_Body_Desirable (Id : E) return B;
function Elaboration_Entity (Id : E) return E;
function Elaboration_Entity_Required (Id : E) return B;
function Encapsulating_State (Id : E) return E;
function Enclosing_Scope (Id : E) return E;
function Entry_Accepted (Id : E) return B;
function Entry_Bodies_Array (Id : E) return E;
@ -6604,6 +6610,7 @@ package Einfo is
function Package_Instantiation (Id : E) return N;
function Packed_Array_Type (Id : E) return E;
function Parent_Subtype (Id : E) return E;
function Part_Of_Constituents (Id : E) return L;
function Postcondition_Proc (Id : E) return E;
function Prival (Id : E) return E;
function Prival_Link (Id : E) return E;
@ -6617,7 +6624,6 @@ package Einfo is
function Referenced (Id : E) return B;
function Referenced_As_LHS (Id : E) return B;
function Referenced_As_Out_Parameter (Id : E) return B;
function Refined_State (Id : E) return E;
function Refinement_Constituents (Id : E) return L;
function Register_Exception_Call (Id : E) return N;
function Related_Array_Object (Id : E) return E;
@ -6949,6 +6955,7 @@ package Einfo is
procedure Set_Elaborate_Body_Desirable (Id : E; V : B := True);
procedure Set_Elaboration_Entity (Id : E; V : E);
procedure Set_Elaboration_Entity_Required (Id : E; V : B := True);
procedure Set_Encapsulating_State (Id : E; V : E);
procedure Set_Enclosing_Scope (Id : E; V : E);
procedure Set_Entry_Accepted (Id : E; V : B := True);
procedure Set_Entry_Bodies_Array (Id : E; V : E);
@ -7228,6 +7235,7 @@ package Einfo is
procedure Set_Package_Instantiation (Id : E; V : N);
procedure Set_Packed_Array_Type (Id : E; V : E);
procedure Set_Parent_Subtype (Id : E; V : E);
procedure Set_Part_Of_Constituents (Id : E; V : L);
procedure Set_Postcondition_Proc (Id : E; V : E);
procedure Set_Prival (Id : E; V : E);
procedure Set_Prival_Link (Id : E; V : E);
@ -7241,7 +7249,6 @@ package Einfo is
procedure Set_Referenced (Id : E; V : B := True);
procedure Set_Referenced_As_LHS (Id : E; V : B := True);
procedure Set_Referenced_As_Out_Parameter (Id : E; V : B := True);
procedure Set_Refined_State (Id : E; V : E);
procedure Set_Refinement_Constituents (Id : E; V : L);
procedure Set_Register_Exception_Call (Id : E; V : N);
procedure Set_Related_Array_Object (Id : E; V : E);
@ -7504,6 +7511,7 @@ package Einfo is
-- Global
-- Initial_Condition
-- Initializes
-- Part_Of
-- Precondition
-- Postcondition
-- Refined_Depends
@ -7680,6 +7688,7 @@ package Einfo is
pragma Inline (Elaborate_Body_Desirable);
pragma Inline (Elaboration_Entity);
pragma Inline (Elaboration_Entity_Required);
pragma Inline (Encapsulating_State);
pragma Inline (Enclosing_Scope);
pragma Inline (Entry_Accepted);
pragma Inline (Entry_Bodies_Array);
@ -8000,6 +8009,7 @@ package Einfo is
pragma Inline (Packed_Array_Type);
pragma Inline (Parameter_Mode);
pragma Inline (Parent_Subtype);
pragma Inline (Part_Of_Constituents);
pragma Inline (Postcondition_Proc);
pragma Inline (Prival);
pragma Inline (Prival_Link);
@ -8013,7 +8023,6 @@ package Einfo is
pragma Inline (Referenced);
pragma Inline (Referenced_As_LHS);
pragma Inline (Referenced_As_Out_Parameter);
pragma Inline (Refined_State);
pragma Inline (Refinement_Constituents);
pragma Inline (Register_Exception_Call);
pragma Inline (Related_Array_Object);
@ -8149,6 +8158,7 @@ package Einfo is
pragma Inline (Set_Elaborate_Body_Desirable);
pragma Inline (Set_Elaboration_Entity);
pragma Inline (Set_Elaboration_Entity_Required);
pragma Inline (Set_Encapsulating_State);
pragma Inline (Set_Enclosing_Scope);
pragma Inline (Set_Entry_Accepted);
pragma Inline (Set_Entry_Bodies_Array);
@ -8424,6 +8434,7 @@ package Einfo is
pragma Inline (Set_Package_Instantiation);
pragma Inline (Set_Packed_Array_Type);
pragma Inline (Set_Parent_Subtype);
pragma Inline (Set_Part_Of_Constituents);
pragma Inline (Set_Postcondition_Proc);
pragma Inline (Set_Prival);
pragma Inline (Set_Prival_Link);
@ -8437,7 +8448,6 @@ package Einfo is
pragma Inline (Set_Referenced);
pragma Inline (Set_Referenced_As_LHS);
pragma Inline (Set_Referenced_As_Out_Parameter);
pragma Inline (Set_Refined_State);
pragma Inline (Set_Refinement_Constituents);
pragma Inline (Set_Register_Exception_Call);
pragma Inline (Set_Related_Array_Object);

1
gcc/ada/par-prag.adb

@ -1236,6 +1236,7 @@ begin
Pragma_Overflow_Mode |
Pragma_Overriding_Renamings |
Pragma_Pack |
Pragma_Part_Of |
Pragma_Partition_Elaboration_Policy |
Pragma_Passive |
Pragma_Preelaborable_Initialization |

3
gcc/ada/sem_ch10.adb

@ -5532,8 +5532,9 @@ package body Sem_Ch10 is
Set_Ekind (Ent, E_Abstract_State);
Set_Etype (Ent, Standard_Void_Type);
Set_Scope (Ent, Scop);
Set_Refined_State (Ent, Empty);
Set_Encapsulating_State (Ent, Empty);
Set_Refinement_Constituents (Ent, New_Elmt_List);
Set_Part_Of_Constituents (Ent, New_Elmt_List);
end Decorate_State;
-------------------

84
gcc/ada/sem_ch13.adb

@ -1140,33 +1140,35 @@ package body Sem_Ch13 is
-----------------------------------
procedure Analyze_Aspect_Specifications (N : Node_Id; E : Entity_Id) is
procedure Decorate_Delayed_Aspect_And_Pragma
(Asp : Node_Id;
Prag : Node_Id);
-- Establish the linkages between a delayed aspect and its corresponding
-- pragma. Set all delay-related flags on both constructs.
procedure Decorate_Aspect_And_Pragma
(Asp : Node_Id;
Prag : Node_Id;
Delayed : Boolean := False);
-- Establish the linkages between an aspect and its corresponding
-- pragma. Flag Delayed should be set when both constructs are delayed.
procedure Insert_Delayed_Pragma (Prag : Node_Id);
-- Insert a postcondition-like pragma into the tree depending on the
-- context. Prag must denote one of the following: Pre, Post, Depends,
-- Global or Contract_Cases.
----------------------------------------
-- Decorate_Delayed_Aspect_And_Pragma --
----------------------------------------
--------------------------------
-- Decorate_Aspect_And_Pragma --
--------------------------------
procedure Decorate_Delayed_Aspect_And_Pragma
(Asp : Node_Id;
Prag : Node_Id)
procedure Decorate_Aspect_And_Pragma
(Asp : Node_Id;
Prag : Node_Id;
Delayed : Boolean := False)
is
begin
Set_Aspect_Rep_Item (Asp, Prag);
Set_Aspect_Rep_Item (Asp, Prag);
Set_Corresponding_Aspect (Prag, Asp);
Set_From_Aspect_Specification (Prag);
Set_Is_Delayed_Aspect (Prag);
Set_Is_Delayed_Aspect (Asp);
Set_Is_Delayed_Aspect (Prag, Delayed);
Set_Is_Delayed_Aspect (Asp, Delayed);
Set_Parent (Prag, Asp);
end Decorate_Delayed_Aspect_And_Pragma;
end Decorate_Aspect_And_Pragma;
---------------------------
-- Insert_Delayed_Pragma --
@ -2004,7 +2006,7 @@ package body Sem_Ch13 is
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Abstract_State);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma (Aspect, Aitem);
if No (Decls) then
Decls := New_List;
@ -2036,7 +2038,8 @@ package body Sem_Ch13 is
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Depends);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma
(Aspect, Aitem, Delayed => True);
Insert_Delayed_Pragma (Aitem);
goto Continue;
@ -2054,7 +2057,8 @@ package body Sem_Ch13 is
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Global);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma
(Aspect, Aitem, Delayed => True);
Insert_Delayed_Pragma (Aitem);
goto Continue;
@ -2079,7 +2083,9 @@ package body Sem_Ch13 is
Expression => Relocate_Node (Expr))),
Pragma_Name =>
Name_Initial_Condition);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma
(Aspect, Aitem, Delayed => True);
if No (Decls) then
Decls := New_List;
@ -2117,7 +2123,9 @@ package body Sem_Ch13 is
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Initializes);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma
(Aspect, Aitem, Delayed => True);
if No (Decls) then
Decls := New_List;
@ -2135,6 +2143,24 @@ package body Sem_Ch13 is
goto Continue;
end Initializes;
-- Part_Of
when Aspect_Part_Of =>
if Nkind_In (N, N_Object_Declaration,
N_Package_Instantiation)
then
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Part_Of);
else
Error_Msg_NE
("aspect & must apply to a variable or package "
& "instantiation", Aspect, Id);
end if;
-- SPARK_Mode
when Aspect_SPARK_Mode => SPARK_Mode : declare
@ -2152,7 +2178,8 @@ package body Sem_Ch13 is
-- emulate the behavior of a source pragma.
if Nkind (N) = N_Package_Body then
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma (Aspect, Aitem);
Decls := Declarations (N);
if No (Decls) then
@ -2168,7 +2195,8 @@ package body Sem_Ch13 is
-- declarations to emulate the behavior of a source pragma.
elsif Nkind (N) = N_Package_Declaration then
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma (Aspect, Aitem);
Decls := Visible_Declarations (Specification (N));
if No (Decls) then
@ -2195,7 +2223,8 @@ package body Sem_Ch13 is
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_Depends);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma
(Aspect, Aitem, Delayed => True);
Insert_Delayed_Pragma (Aitem);
goto Continue;
@ -2213,7 +2242,8 @@ package body Sem_Ch13 is
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_Global);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma
(Aspect, Aitem, Delayed => True);
Insert_Delayed_Pragma (Aitem);
goto Continue;
@ -2245,7 +2275,7 @@ package body Sem_Ch13 is
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_State);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma (Aspect, Aitem);
if No (Decls) then
Decls := New_List;
@ -2515,7 +2545,8 @@ package body Sem_Ch13 is
Expression => Relocate_Node (Expr))),
Pragma_Name => Nam);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Decorate_Aspect_And_Pragma
(Aspect, Aitem, Delayed => True);
Insert_Delayed_Pragma (Aitem);
goto Continue;
@ -7989,6 +8020,7 @@ package body Sem_Ch13 is
Aspect_Implicit_Dereference |
Aspect_Initial_Condition |
Aspect_Initializes |
Aspect_Part_Of |
Aspect_Post |
Aspect_Postcondition |
Aspect_Pre |

205
gcc/ada/sem_ch3.adb

@ -99,6 +99,7 @@ package body Sem_Ch3 is
-- Async_Writers
-- Effective_Reads
-- Effective_Writes
-- Part_Of
procedure Build_Derived_Type
(N : Node_Id;
@ -2086,12 +2087,6 @@ package body Sem_Ch3 is
-- If the states have visible refinement, remove the visibility of each
-- constituent at the end of the package body declarations.
function Requires_State_Refinement
(Spec_Id : Entity_Id;
Body_Id : Entity_Id) return Boolean;
-- Determine whether a package denoted by its spec and body entities
-- requires refinement of abstract states.
-----------------
-- Adjust_Decl --
-----------------
@ -2185,89 +2180,11 @@ package body Sem_Ch3 is
end if;
end Remove_Visible_Refinements;
-------------------------------
-- Requires_State_Refinement --
-------------------------------
function Requires_State_Refinement
(Spec_Id : Entity_Id;
Body_Id : Entity_Id) return Boolean
is
function Mode_Is_Off (Prag : Node_Id) return Boolean;
-- Given pragma SPARK_Mode, determine whether the mode is Off
-----------------
-- Mode_Is_Off --
-----------------
function Mode_Is_Off (Prag : Node_Id) return Boolean is
Mode : Node_Id;
begin
-- The default SPARK mode is On
if No (Prag) then
return False;
end if;
Mode :=
Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
-- Then the pragma lacks an argument, the default mode is On
if No (Mode) then
return False;
else
return Chars (Mode) = Name_Off;
end if;
end Mode_Is_Off;
-- Start of processing for Requires_State_Refinement
begin
-- A package that does not define at least one abstract state cannot
-- possibly require refinement.
if No (Abstract_States (Spec_Id)) then
return False;
-- The package instroduces a single null state which does not merit
-- refinement.
elsif Has_Null_Abstract_State (Spec_Id) then
return False;
-- Check whether the package body is subject to pragma SPARK_Mode. If
-- it is and the mode is Off, the package body is considered to be in
-- regular Ada and does not require refinement.
elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then
return False;
-- The body's SPARK_Mode may be inherited from a similar pragma that
-- appears in the private declarations of the spec. The pragma we are
-- interested appears as the second entry in SPARK_Pragma.
elsif Present (SPARK_Pragma (Spec_Id))
and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id)))
then
return False;
-- The spec defines at least one abstract state and the body has no
-- way of circumventing the refinement.
else
return True;
end if;
end Requires_State_Refinement;
-- Local variables
Body_Id : Entity_Id;
Context : Node_Id;
Freeze_From : Entity_Id := Empty;
Next_Decl : Node_Id;
Prag : Node_Id;
Spec_Id : Entity_Id;
Body_Seen : Boolean := False;
@ -2415,54 +2332,21 @@ package body Sem_Ch3 is
Decl := Next_Decl;
end loop;
-- Analyze the contracts of packages and their bodies
if Present (L) then
Context := Parent (L);
-- Analyze pragmas Initializes and Initial_Condition of a package at
-- the end of the visible declarations as the pragmas have visibility
-- over the said region.
if Nkind (Context) = N_Package_Specification
and then L = Visible_Declarations (Context)
then
Spec_Id := Defining_Entity (Parent (Context));
Prag := Get_Pragma (Spec_Id, Pragma_Initializes);
if Present (Prag) then
Analyze_Initializes_In_Decl_Part (Prag);
end if;
Prag := Get_Pragma (Spec_Id, Pragma_Initial_Condition);
if Present (Prag) then
Analyze_Initial_Condition_In_Decl_Part (Prag);
end if;
-- Analyze the state refinements within a package body now, after
-- all hidden states have been encountered and freely visible.
-- Refinements must be processed before pragmas Refined_Depends and
-- Refined_Global because the last two may mention constituents.
Analyze_Package_Contract (Defining_Entity (Context));
elsif Nkind (Context) = N_Package_Body then
In_Package_Body := True;
Body_Id := Defining_Entity (Context);
Spec_Id := Corresponding_Spec (Context);
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
-- The analysis of pragma Refined_State detects whether the spec
-- has abstract states available for refinement.
if Present (Prag) then
Analyze_Refined_State_In_Decl_Part (Prag);
-- State refinement is required when the package declaration has
-- abstract states. Null states are not considered.
elsif Requires_State_Refinement (Spec_Id, Body_Id) then
Error_Msg_NE
("package & requires state refinement", Context, Spec_Id);
end if;
Analyze_Package_Body_Contract (Defining_Entity (Context));
end if;
end if;
@ -2472,14 +2356,14 @@ package body Sem_Ch3 is
Decl := First (L);
while Present (Decl) loop
if Nkind (Decl) = N_Subprogram_Body then
if Nkind (Decl) = N_Object_Declaration then
Analyze_Object_Contract (Defining_Entity (Decl));
elsif Nkind (Decl) = N_Subprogram_Body then
Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
elsif Nkind (Decl) = N_Subprogram_Declaration then
Analyze_Subprogram_Contract (Defining_Entity (Decl));
elsif Nkind (Decl) = N_Object_Declaration then
Analyze_Object_Contract (Defining_Entity (Decl));
end if;
Next (Decl);
@ -3078,8 +2962,6 @@ package body Sem_Ch3 is
AW_Val : Boolean := False;
ER_Val : Boolean := False;
EW_Val : Boolean := False;
Items : Node_Id;
Nam : Name_Id;
Prag : Node_Id;
Seen : Boolean := False;
@ -3127,45 +3009,50 @@ package body Sem_Ch3 is
end if;
end if;
-- Examine the contract
-- Analyze all external properties
Items := Contract (Obj_Id);
Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
if Present (Items) then
-- Analyze classification pragmas
Prag := Classifications (Items);
while Present (Prag) loop
Nam := Pragma_Name (Prag);
if Nam = Name_Async_Readers then
Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
Seen := True;
elsif Nam = Name_Async_Writers then
Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
Seen := True;
elsif Nam = Name_Effective_Reads then
Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
Seen := True;
else pragma Assert (Nam = Name_Effective_Writes);
Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
Seen := True;
end if;
Prag := Next_Pragma (Prag);
end loop;
if Present (Prag) then
Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
Seen := True;
end if;
-- Once all external properties have been processed, verify their
-- mutual interaction.
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;
-- Check whether the lack of indicator Part_Of agrees with the
-- placement of the variable 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;
end if;
end Analyze_Object_Contract;
@ -4117,7 +4004,7 @@ package body Sem_Ch3 is
-- common destination for legal and illegal object declarations.
if Ekind (Id) = E_Variable then
Set_Refined_State (Id, Empty);
Set_Encapsulating_State (Id, Empty);
end if;
if Has_Aspects (N) then

63
gcc/ada/sem_ch7.adb

@ -174,6 +174,31 @@ package body Sem_Ch7 is
end if;
end Analyze_Package_Body;
-----------------------------------
-- Analyze_Package_Body_Contract --
-----------------------------------
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
Prag : Node_Id;
begin
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
-- The analysis of pragma Refined_State detects whether the spec has
-- abstract states available for refinement.
if Present (Prag) then
Analyze_Refined_State_In_Decl_Part (Prag);
-- State refinement is required when the package declaration has
-- abstract states. Null states are not considered.
elsif Requires_State_Refinement (Spec_Id, Body_Id) then
Error_Msg_N ("package & requires state refinement", Spec_Id);
end if;
end Analyze_Package_Body_Contract;
---------------------------------
-- Analyze_Package_Body_Helper --
---------------------------------
@ -801,6 +826,41 @@ package body Sem_Ch7 is
end if;
end Analyze_Package_Body_Helper;
------------------------------
-- Analyze_Package_Contract --
------------------------------
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
Prag : Node_Id;
begin
-- Analyze the initialization related pragmas. Initializes must come
-- before Initial_Condition due to item dependencies.
Prag := Get_Pragma (Pack_Id, Pragma_Initializes);
if Present (Prag) then
Analyze_Initializes_In_Decl_Part (Prag);
end if;
Prag := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
if Present (Prag) then
Analyze_Initial_Condition_In_Decl_Part (Prag);
end if;
-- Check whether the lack of indicator Part_Of agrees with the placement
-- of the package instantiation with respect to the state space.
if Is_Generic_Instance (Pack_Id) then
Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
if No (Prag) then
Check_Missing_Part_Of (Pack_Id);
end if;
end if;
end Analyze_Package_Contract;
---------------------------------
-- Analyze_Package_Declaration --
---------------------------------
@ -2850,8 +2910,7 @@ package body Sem_Ch7 is
not Is_Null_State (Node (First_Elmt (Abstract_States (P))))
then
Error_Msg_N
("?Y?info: & requires body (non-null abstract state aspect)",
P);
("?Y?info: & requires body (non-null abstract state aspect)", P);
end if;
-- Otherwise search entity chain for entity requiring completion

14
gcc/ada/sem_ch7.ads

@ -32,6 +32,20 @@ package Sem_Ch7 is
procedure Analyze_Package_Specification (N : Node_Id);
procedure Analyze_Private_Type_Declaration (N : Node_Id);
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed aspects chained on the contract of package body
-- Body_Id as if they appeared at the end of a declarative region. The
-- aspects in consideration are:
-- Refined_State
procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
-- Analyze all delayed aspects chained on the contract of package Pack_Id
-- as if they appeared at the end of a declarative region. The aspects in
-- consideration are:
-- Initial_Condition
-- Initializes
-- Part_Of
procedure End_Package_Scope (P : Entity_Id);
-- Calls Uninstall_Declarations, and then pops the scope stack

1387
gcc/ada/sem_prag.adb

File diff suppressed because it is too large Load Diff

5
gcc/ada/sem_prag.ads

@ -139,6 +139,11 @@ package Sem_Prag is
-- is the related variable or state. Ensure legality of the combination and
-- issue an error for an illegal combination.
procedure Check_Missing_Part_Of (Item_Id : Entity_Id);
-- Determine whether the placement within the state space of an abstract
-- state, variable or package instantiation denoted by Item_Id requires the
-- use of indicator/option Part_Of. If this is the case, emit an error.
function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean;
-- N is a pragma appearing in a configuration pragma file. Most such
-- pragmas are analyzed when the file is read, before parsing and analyzing

206
gcc/ada/sem_util.adb

@ -233,11 +233,12 @@ package body Sem_Util is
Nam := Original_Aspect_Name (Prag);
-- Contract items related to [generic] packages. The applicable pragmas
-- are:
-- Contract items related to [generic] packages or instantiations. The
-- applicable pragmas are:
-- Abstract_States
-- Initial_Condition
-- Initializes
-- Part_Of (instantiation only)
if Ekind_In (Id, E_Generic_Package, E_Package) then
if Nam_In (Nam, Name_Abstract_State,
@ -247,6 +248,12 @@ package body Sem_Util is
Set_Next_Pragma (Prag, Classifications (Items));
Set_Classifications (Items, Prag);
-- Indicator Part_Of must be associated with a package instantiation
elsif Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
Set_Next_Pragma (Prag, Classifications (Items));
Set_Classifications (Items, Prag);
-- The pragma is not a proper contract item
else
@ -355,12 +362,14 @@ package body Sem_Util is
-- Async_Writers
-- Effective_Reads
-- Effective_Writes
-- Part_Of
elsif Ekind (Id) = E_Variable then
if Nam_In (Nam, Name_Async_Readers,
Name_Async_Writers,
Name_Effective_Reads,
Name_Effective_Writes)
Name_Effective_Writes,
Name_Part_Of)
then
Set_Next_Pragma (Prag, Classifications (Items));
Set_Classifications (Items, Prag);
@ -4201,6 +4210,7 @@ package body Sem_Util is
Set_Defining_Unit_Name (N, Err);
return Err;
-- If not an entity, get defining identifier
else
@ -5827,6 +5837,75 @@ package body Sem_Util is
end if;
end Find_Parameter_Type;
-----------------------------------
-- Find_Placement_In_State_Space --
-----------------------------------
procedure Find_Placement_In_State_Space
(Item_Id : Entity_Id;
Placement : out State_Space_Kind;
Pack_Id : out Entity_Id)
is
Context : Entity_Id;
begin
-- Assume that the item does not appear in the state space of a package
Pack_Id := Empty;
-- Climb the scope stack and examine the enclosing context
Context := Scope (Item_Id);
while Present (Context) and then Context /= Standard_Standard loop
if Ekind (Context) = E_Package then
Pack_Id := Context;
-- A package body is a cut off point for the traversal as the item
-- cannot be visible to the outside from this point on. Note that
-- this test must be done first as a body is also classified as a
-- private part.
if In_Package_Body (Context) then
Placement := Body_State_Space;
return;
-- The private part of a package is a cut off point for the
-- traversal as the item cannot be visible to the outside from
-- this point on.
elsif In_Private_Part (Context) then
Placement := Private_State_Space;
return;
-- When the item appears in the visible state space of a package,
-- continue to climb the scope stack as this may not be the final
-- state space.
else
Placement := Visible_State_Space;
-- The visible state space of a private child unit acts as the
-- proper placement of an item.
if Is_Child_Unit (Context)
and then Is_Private_Descendant (Context)
then
return;
end if;
end if;
-- The item or its enclosing package appear in a construct that has
-- no state space.
else
Placement := Not_In_Package;
return;
end if;
Context := Scope (Context);
end loop;
end Find_Placement_In_State_Space;
-----------------------------
-- Find_Static_Alternative --
-----------------------------
@ -8948,9 +9027,8 @@ package body Sem_Util is
-------------------------
function Is_Child_Or_Sibling
(Pack_1 : Entity_Id;
Pack_2 : Entity_Id;
Private_Child : Boolean) return Boolean
(Pack_1 : Entity_Id;
Pack_2 : Entity_Id) return Boolean
is
function Distance_From_Standard (Pack : Entity_Id) return Nat;
-- Given an arbitrary package, return the number of "climbs" necessary
@ -8964,10 +9042,6 @@ package body Sem_Util is
-- climb the scope chain until the said depth is reached. The pointer
-- to the package and its depth a modified during the climb.
function Is_Child (Pack : Entity_Id) return Boolean;
-- Given a package Pack, determine whether it is a child package that
-- satisfies the privacy requirement (if set).
----------------------------
-- Distance_From_Standard --
----------------------------
@ -9011,26 +9085,6 @@ package body Sem_Util is
end loop;
end Equalize_Depths;
--------------
-- Is_Child --
--------------
function Is_Child (Pack : Entity_Id) return Boolean is
begin
if Is_Child_Unit (Pack) then
if Private_Child then
return Is_Private_Descendant (Pack);
else
return True;
end if;
-- The package is nested, it cannot act a child or a sibling
else
return False;
end if;
end Is_Child;
-- Local variables
P_1 : Entity_Id := Pack_1;
@ -9062,7 +9116,10 @@ package body Sem_Util is
-- P_1 P_1
elsif P_1_Depth > P_2_Depth then
Equalize_Depths (P_1, P_1_Depth, P_2_Depth);
Equalize_Depths
(Pack => P_1,
Depth => P_1_Depth,
Depth_To_Reach => P_2_Depth);
P_1_Child := True;
-- (root) P_1
@ -9072,7 +9129,10 @@ package body Sem_Util is
-- P_2 P_2
elsif P_2_Depth > P_1_Depth then
Equalize_Depths (P_2, P_2_Depth, P_1_Depth);
Equalize_Depths
(Pack => P_2,
Depth => P_2_Depth,
Depth_To_Reach => P_1_Depth);
P_2_Child := True;
end if;
@ -9088,9 +9148,10 @@ package body Sem_Util is
if P_1 = P_2 then
if P_1_Child then
return Is_Child (Pack_1);
return Is_Child_Unit (Pack_1);
else pragma Assert (P_2_Child);
return Is_Child (Pack_2);
return Is_Child_Unit (Pack_2);
end if;
-- The packages may come from the same package chain or from entirely
@ -9107,7 +9168,7 @@ package body Sem_Util is
-- The two packages may be siblings
if P_1 = P_2 then
return Is_Child (Pack_1) and then Is_Child (Pack_2);
return Is_Child_Unit (Pack_1) and then Is_Child_Unit (Pack_2);
end if;
P_1 := Scope (P_1);
@ -14554,6 +14615,81 @@ package body Sem_Util is
end if;
end Require_Entity;
-------------------------------
-- Requires_State_Refinement --
-------------------------------
function Requires_State_Refinement
(Spec_Id : Entity_Id;
Body_Id : Entity_Id) return Boolean
is
function Mode_Is_Off (Prag : Node_Id) return Boolean;
-- Given pragma SPARK_Mode, determine whether the mode is Off
-----------------
-- Mode_Is_Off --
-----------------
function Mode_Is_Off (Prag : Node_Id) return Boolean is
Mode : Node_Id;
begin
-- The default SPARK mode is On
if No (Prag) then
return False;
end if;
Mode := Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
-- Then the pragma lacks an argument, the default mode is On
if No (Mode) then
return False;
else
return Chars (Mode) = Name_Off;
end if;
end Mode_Is_Off;
-- Start of processing for Requires_State_Refinement
begin
-- A package that does not define at least one abstract state cannot
-- possibly require refinement.
if No (Abstract_States (Spec_Id)) then
return False;
-- The package instroduces a single null state which does not merit
-- refinement.
elsif Has_Null_Abstract_State (Spec_Id) then
return False;
-- Check whether the package body is subject to pragma SPARK_Mode. If
-- it is and the mode is Off, the package body is considered to be in
-- regular Ada and does not require refinement.
elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then
return False;
-- The body's SPARK_Mode may be inherited from a similar pragma that
-- appears in the private declarations of the spec. The pragma we are
-- interested appears as the second entry in SPARK_Pragma.
elsif Present (SPARK_Pragma (Spec_Id))
and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id)))
then
return False;
-- The spec defines at least one abstract state and the body has no way
-- of circumventing the refinement.
else
return True;
end if;
end Requires_State_Refinement;
------------------------------
-- Requires_Transient_Scope --
------------------------------

113
gcc/ada/sem_util.ads

@ -44,8 +44,9 @@ package Sem_Util is
-- freeze node of E.
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
-- Add pragma Prag to the contract of an entry, a package [body] or a
-- subprogram [body] denoted by Id. The following are valid pragmas:
-- Add pragma Prag to the contract of an entry, a package [body], a
-- subprogram [body] or variable denoted by Id. The following are valid
-- pragmas:
-- Abstract_States
-- Async_Readers
-- Async_Writers
@ -56,6 +57,7 @@ package Sem_Util is
-- Global
-- Initial_Condition
-- Initializes
-- Part_Of
-- Postcondition
-- Precondition
-- Refined_Depends
@ -571,6 +573,12 @@ package Sem_Util is
-- Call is set to the node for the corresponding call. If the node N is not
-- an actual parameter then Formal and Call are set to Empty.
function Find_Body_Discriminal
(Spec_Discriminant : Entity_Id) return Entity_Id;
-- Given a discriminant of the record type that implements a task or
-- protected type, return the discriminal of the corresponding discriminant
-- of the actual concurrent type.
function Find_Corresponding_Discriminant
(Id : Node_Id;
Typ : Entity_Id) return Entity_Id;
@ -600,17 +608,93 @@ package Sem_Util is
-- Return the type of formal parameter Param as determined by its
-- specification.
-- The following type describes the placement of an arbitrary entity with
-- respect to SPARK visible / hidden state space.
type State_Space_Kind is
(Not_In_Package,
-- An entity is not in the visible, private or body state space when
-- the immediate enclosing construct is not a package.
Visible_State_Space,
-- An entity is in the visible state space when it appears immediately
-- within the visible declarations of a package or when it appears in
-- the visible state space of a nested package which in turn is declared
-- in the visible declarations of an enclosing package:
-- package Pack is
-- Visible_Variable : ...
-- package Nested
-- with Abstract_State => Visible_State
-- is
-- Visible_Nested_Variable : ...
-- end Nested;
-- end Pack;
-- Entities associated with a package instantiation inherit the state
-- space from the instance placement:
-- generic
-- package Gen is
-- Generic_Variable : ...
-- end Gen;
-- with Gen;
-- package Pack is
-- package Inst is new Gen;
-- -- Generic_Variable is in the visible state space of Pack
-- end Pack;
Private_State_Space,
-- An entity is in the private state space when it appears immediately
-- within the private declarations of a package or when it appears in
-- the visible state space of a nested package which in turn is declared
-- in the private declarations of an enclosing package:
-- package Pack is
-- private
-- Private_Variable : ...
-- package Nested
-- with Abstract_State => Private_State
-- is
-- Private_Nested_Variable : ...
-- end Nested;
-- end Pack;
-- The same placement principle applies to package instantiations
Body_State_Space);
-- An entity is in the body state space when it appears immediately
-- within the declarations of a package body or when it appears in the
-- visible state space of a nested package which in turn is declared in
-- the declarations of an enclosing package body:
-- package body Pack is
-- Body_Variable : ...
-- package Nested
-- with Abstract_State => Body_State
-- is
-- Body_Nested_Variable : ...
-- end Nested;
-- end Pack;
-- The same placement principle applies to package instantiations
procedure Find_Placement_In_State_Space
(Item_Id : Entity_Id;
Placement : out State_Space_Kind;
Pack_Id : out Entity_Id);
-- Determine the state space placement of an item. Item_Id denotes the
-- entity of an abstract state, variable or package instantiation.
-- Placement captures the precise placement of the item in the enclosing
-- state space. If the state space is that of a package, Pack_Id denotes
-- its entity, otherwise Pack_Id is Empty.
function Find_Static_Alternative (N : Node_Id) return Node_Id;
-- N is a case statement whose expression is a compile-time value.
-- Determine the alternative chosen, so that the code of non-selected
-- alternatives, and the warnings that may apply to them, are removed.
function Find_Body_Discriminal
(Spec_Discriminant : Entity_Id) return Entity_Id;
-- Given a discriminant of the record type that implements a task or
-- protected type, return the discriminal of the corresponding discriminant
-- of the actual concurrent type.
function First_Actual (Node : Node_Id) return Node_Id;
-- Node is an N_Function_Call or N_Procedure_Call_Statement node. The
-- result returned is the first actual parameter in declaration order
@ -1006,14 +1090,11 @@ package Sem_Util is
-- Returns True if N is a call to a CPP constructor
function Is_Child_Or_Sibling
(Pack_1 : Entity_Id;
Pack_2 : Entity_Id;
Private_Child : Boolean) return Boolean;
(Pack_1 : Entity_Id;
Pack_2 : Entity_Id) return Boolean;
-- Determine the following relations between two arbitrary packages:
-- 1) One package is the parent of a child package
-- 2) Both packages are siblings and share a common parent
-- If flag Private_Child is set, then the child in case 1) or both siblings
-- in case 2) must be private.
function Is_Concurrent_Interface (T : Entity_Id) return Boolean;
-- First determine whether type T is an interface and then check whether
@ -1540,6 +1621,12 @@ package Sem_Util is
-- This is used as a defense mechanism against ill-formed trees caused by
-- previous errors (particularly in -gnatq mode).
function Requires_State_Refinement
(Spec_Id : Entity_Id;
Body_Id : Entity_Id) return Boolean;
-- Determine whether a package denoted by its spec and body entities
-- requires refinement of abstract states.
function Requires_Transient_Scope (Id : Entity_Id) return Boolean;
-- Id is a type entity. The result is True when temporaries of this type
-- need to be wrapped in a transient scope to be reclaimed properly when a

1
gcc/ada/sinfo.ads

@ -7283,6 +7283,7 @@ package Sinfo is
-- Global
-- Initial_Condition
-- Initializes
-- Part_Of
-- Refined_Depends
-- Refined_Global
-- Refined_States

3
gcc/ada/snames.ads-tmpl

@ -565,6 +565,7 @@ package Snames is
Name_Ordered : constant Name_Id := N + $; -- GNAT
Name_Pack : constant Name_Id := N + $;
Name_Page : constant Name_Id := N + $;
Name_Part_Of : constant Name_Id := N + $; -- GNAT
Name_Passive : constant Name_Id := N + $; -- GNAT
Name_Post : constant Name_Id := N + $; -- GNAT
Name_Postcondition : constant Name_Id := N + $; -- GNAT
@ -761,7 +762,6 @@ package Snames is
Name_Optional : constant Name_Id := N + $;
Name_Policy : constant Name_Id := N + $;
Name_Parameter_Types : constant Name_Id := N + $;
Name_Part_Of : constant Name_Id := N + $;
Name_Proof_In : constant Name_Id := N + $;
Name_Reason : constant Name_Id := N + $;
Name_Reference : constant Name_Id := N + $;
@ -1870,6 +1870,7 @@ package Snames is
Pragma_Ordered,
Pragma_Pack,
Pragma_Page,
Pragma_Part_Of,
Pragma_Passive,
Pragma_Post,
Pragma_Postcondition,