mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-05 22:01:27 +08:00
Code Issues Packages Projects Releases Wiki Activity

einfo.adb: Add node/list usage for Refined_State and Refinement_Constituents.

Browse Source 
2013-10-13  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb: Add node/list usage for Refined_State
	and Refinement_Constituents.
	(Get_Pragma): Update the
	initialization of Is_CDG to include Refined_Global and
	Refined_Depends. Rename constant Delayed to In_Contract and update
	all of its occurrences.
	(Is_Non_Volatile_State): New routine.
	(Is_Volatile_State): Removed.
	(Refined_State): New routine.
	(Refinement_Constituents): New routine.
	(Set_Refined_State): New routine.
	(Set_Refinement_Constituents): New routine.
	(Write_Field8_Name): Add output for Refinement_Constituents.
	(Write_Field10_Name): Add output for Refined_State.
	* einfo.ads: Add new synthesized attribute Is_Non_Volatile_State.
	Remove synthesized attribute Is_Volatile_State.  Add new
	attributes Refined_State and Refinement_Constituents along with
	usage in nodes.
	(Get_Pragma): Update the comment on usage.
	(Is_Non_Volatile_State): New routine.
	(Is_Volatile_State): Removed.
	(Refined_State): New routine and pragma Inline.
	(Refinement_Constituents): New routine and pragma Inline.
	(Set_Refined_State): New routine and pragma Inline.
	(Set_Refinement_Constituents): New routine and pragma Inline.
	* elists.ads, elists.adb (Clone): Removed.
	(New_Copy_Elist): New routine.
	(Remove): New routine.
	* sem_ch3.adb (Analyze_Declarations): Use Defining_Entity
	to get the entity of the subprogram [body].
	(Analyze_Object_Declaration): Add initialization for
	Refined_State.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
	for Refined_Global and Refined_Depends. Emit an error when
	the body requires Refined_Global, but the aspect/pragma is
	not present.
	* sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change
	procedure signature and add comment on usage.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Global.
	* sem_prag.adb (Analyze_Abstract_State): Add initialization
	of attributes Refined_State and Refinement_Constituents.
	(Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part,
	Analyze_Contract_Cases_In_Decl_Part): Remove local
	constant Arg1.
	(Analyze_Pragma): Add processing for pragma
	Refined_Global. The analysis of Refined_Post and Refined_Pre
	has been merged. Update an error message in the processing of
	pragma Refined_State.
	(Analyze_Refined_Global_In_Decl_Part): Provide implementation.
	(Analyze_Refined_Pragma): New routine.
	(Analyze_Refined_Pre_Post_Condition): Removed.
	(Analyze_Refined_State_In_Decl_Part): Update the call to Clone.
	(Analyze_Refinement_Clause): Make State_Id visible to all
	nested subprogram.
	(Check_Matching_Constituent): Establish
	a relation between a refined state and its constituent.
	(Collect_Hidden_States_In_Decls): Remove ??? comment. Look at
	the entity of the object declaration to establish its kind.
	* sem_util.adb: Alphabetize with and use clauses.
	(Contains_Refined_State): New routine.
	* sem_util.ads (Contains_Refined_State): New routine.

From-SVN: r203504
This commit is contained in:
Hristian Kirtchev 2013-10-13 16:31:00 +00:00 committed by Arnaud Charlet
parent ad0d71b531
commit ab8843fac0
12 changed files with 1387 additions and 139 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
gcc/ada/ChangeLog
View File

@ -1,3 +1,68 @@
2013-10-13 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb: Add node/list usage for Refined_State
and Refinement_Constituents.
(Get_Pragma): Update the
initialization of Is_CDG to include Refined_Global and
Refined_Depends. Rename constant Delayed to In_Contract and update
all of its occurrences.
(Is_Non_Volatile_State): New routine.
(Is_Volatile_State): Removed.
(Refined_State): New routine.
(Refinement_Constituents): New routine.
(Set_Refined_State): New routine.
(Set_Refinement_Constituents): New routine.
(Write_Field8_Name): Add output for Refinement_Constituents.
(Write_Field10_Name): Add output for Refined_State.
* einfo.ads: Add new synthesized attribute Is_Non_Volatile_State.
Remove synthesized attribute Is_Volatile_State. Add new
attributes Refined_State and Refinement_Constituents along with
usage in nodes.
(Get_Pragma): Update the comment on usage.
(Is_Non_Volatile_State): New routine.
(Is_Volatile_State): Removed.
(Refined_State): New routine and pragma Inline.
(Refinement_Constituents): New routine and pragma Inline.
(Set_Refined_State): New routine and pragma Inline.
(Set_Refinement_Constituents): New routine and pragma Inline.
* elists.ads, elists.adb (Clone): Removed.
(New_Copy_Elist): New routine.
(Remove): New routine.
* sem_ch3.adb (Analyze_Declarations): Use Defining_Entity
to get the entity of the subprogram [body].
(Analyze_Object_Declaration): Add initialization for
Refined_State.
* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
for Refined_Global and Refined_Depends. Emit an error when
the body requires Refined_Global, but the aspect/pragma is
not present.
* sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change
procedure signature and add comment on usage.
* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
for aspect Refined_Global.
* sem_prag.adb (Analyze_Abstract_State): Add initialization
of attributes Refined_State and Refinement_Constituents.
(Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part,
Analyze_Contract_Cases_In_Decl_Part): Remove local
constant Arg1.
(Analyze_Pragma): Add processing for pragma
Refined_Global. The analysis of Refined_Post and Refined_Pre
has been merged. Update an error message in the processing of
pragma Refined_State.
(Analyze_Refined_Global_In_Decl_Part): Provide implementation.
(Analyze_Refined_Pragma): New routine.
(Analyze_Refined_Pre_Post_Condition): Removed.
(Analyze_Refined_State_In_Decl_Part): Update the call to Clone.
(Analyze_Refinement_Clause): Make State_Id visible to all
nested subprogram.
(Check_Matching_Constituent): Establish
a relation between a refined state and its constituent.
(Collect_Hidden_States_In_Decls): Remove ??? comment. Look at
the entity of the object declaration to establish its kind.
* sem_util.adb: Alphabetize with and use clauses.
(Contains_Refined_State): New routine.
* sem_util.ads (Contains_Refined_State): New routine.
2013-10-13 Thomas Quinot <quinot@adacore.com>
* scos.ads: Minor documentation clarification.

88
gcc/ada/einfo.adb
View File

@ -81,6 +81,7 @@ package body Einfo is
-- Normalized_First_Bit Uint8
-- Postcondition_Proc Node8
-- Refined_State_Pragma Node8
-- Refinement_Constituents Elist8
-- Return_Applies_To Node8
-- First_Exit_Statement Node8
@ -93,6 +94,7 @@ package body Einfo is
-- 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
@ -2648,12 +2650,24 @@ 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 Refined_State_Pragma (Id : E) return N is
begin
pragma Assert (Ekind (Id) = E_Package_Body);
return Node8 (Id);
end Refined_State_Pragma;
function Refinement_Constituents (Id : E) return L is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
return Elist8 (Id);
end Refinement_Constituents;
function Register_Exception_Call (Id : E) return N is
begin
pragma Assert (Ekind (Id) = E_Exception);
@ -5308,12 +5322,24 @@ 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_Refined_State_Pragma (Id : E; V : N) is
begin
pragma Assert (Ekind (Id) = E_Package_Body);
Set_Node8 (Id, V);
end Set_Refined_State_Pragma;
procedure Set_Refinement_Constituents (Id : E; V : L) is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
Set_Elist8 (Id, V);
end Set_Refinement_Constituents;
procedure Set_Register_Exception_Call (Id : E; V : N) is
begin
pragma Assert (Ekind (Id) = E_Exception);
@ -6266,21 +6292,26 @@ package body Einfo is
----------------
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
Is_CDG : constant Boolean :=
Id = Pragma_Depends or else Id = Pragma_Global;
Is_CTC : constant Boolean :=
Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case;
Is_PPC : constant Boolean :=
Id = Pragma_Precondition or else Id = Pragma_Postcondition;
Delayed : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
Item : Node_Id;
Items : Node_Id;
Is_CDG : constant Boolean :=
Id = Pragma_Depends
or else Id = Pragma_Global
or else Id = Pragma_Refined_Depends
or else Id = Pragma_Refined_Global;
Is_CTC : constant Boolean :=
Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case;
Is_PPC : constant Boolean :=
Id = Pragma_Precondition
or else Id = Pragma_Postcondition;
In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
Item : Node_Id;
Items : Node_Id;
begin
-- Handle delayed pragmas that appear in N_Contract nodes. Those have to
-- be extracted from their specialized list.
-- Handle pragmas that appear in N_Contract nodes. Those have to be
-- extracted from their specialized list.
if Delayed then
if In_Contract then
Items := Contract (E);
if No (Items) then
@ -6310,7 +6341,7 @@ package body Einfo is
-- All nodes in N_Contract are chained using Next_Pragma
elsif Delayed then
elsif In_Contract then
Item := Next_Pragma (Item);
-- Regular pragmas
@ -6712,6 +6743,17 @@ package body Einfo is
and then Has_Option (Id, Name_Input_Only);
end Is_Input_Only_State;
---------------------------
-- Is_Non_Volatile_State --
---------------------------
function Is_Non_Volatile_State (Id : E) return B is
begin
return
Ekind (Id) = E_Abstract_State
and then Has_Option (Id, Name_Non_Volatile);
end Is_Non_Volatile_State;
-------------------
-- Is_Null_State --
-------------------
@ -6872,17 +6914,6 @@ package body Einfo is
and then Is_Task_Type (Corresponding_Concurrent_Type (Id));
end Is_Task_Record_Type;
-----------------------
-- Is_Volatile_State --
-----------------------
function Is_Volatile_State (Id : E) return B is
begin
return
Ekind (Id) = E_Abstract_State
and then Has_Option (Id, Name_Volatile);
end Is_Volatile_State;
------------------------
-- Is_Wrapper_Package --
------------------------
@ -8309,6 +8340,9 @@ package body Einfo is
when E_Package_Body =>
Write_Str ("Refined_State_Pragma");
when E_Abstract_State =>
Write_Str ("Refinement_Constituents");
when E_Return_Statement =>
Write_Str ("Return_Applies_To");
@ -8358,7 +8392,7 @@ package body Einfo is
Concurrent_Kind =>
Write_Str ("Direct_Primitive_Operations");
when Float_Kind =>
when Float_Kind =>
Write_Str ("Float_Rep");
when E_In_Parameter |
@ -8375,6 +8409,10 @@ 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;

48
gcc/ada/einfo.ads
View File

@ -2576,6 +2576,10 @@ package Einfo is
-- set right, at which point, these comments can be removed, and the
-- tests for static subtypes greatly simplified.
-- Is_Non_Volatile_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
-- option Non_Volatile.
-- Is_Null_Init_Proc (Flag178)
-- Defined in procedure entities. Set for generated init proc procedures
-- (used to initialize composite types), if the code for the procedure
@ -2977,10 +2981,6 @@ package Einfo is
-- optimizations on volatile objects should test Treat_As_Volatile
-- rather than testing this flag.
-- Is_Volatile_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
-- option Volatile.
-- Is_Wrapper_Package (synthesized)
-- Defined in package entities. Indicates that the package has been
-- created as a wrapper for a subprogram instantiation.
@ -3537,10 +3537,19 @@ 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.
-- Refined_State_Pragma (Node8)
-- Defined in [generic] package bodies. Contains the pragma that refines
-- all abstract states defined in the corresponding package declaration.
-- 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
-- the constituent_list of aspect/pragma Refined_State.
-- Register_Exception_Call (Node20)
-- Defined in exception entities. When an exception is declared,
-- a call is expanded to Register_Exception. This field points to
@ -5096,11 +5105,13 @@ package Einfo is
------------------------------------------
-- E_Abstract_State
-- Refinement_Constituents (Elist8)
-- Refined_State (Node10)
-- Is_External_State (synth)
-- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
-- Is_Output_Only_State (synth)
-- Is_Volatile_State (synth)
-- Is_Non_Volatile_State (synth)
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
@ -5913,6 +5924,7 @@ package Einfo is
-- E_Variable
-- Hiding_Loop_Variable (Node8)
-- Current_Value (Node9)
-- Refined_State (Node10)
-- Esize (Uint12)
-- Extra_Accessibility (Node13)
-- Alignment (Uint14)
@ -6540,7 +6552,9 @@ 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 Refined_State_Pragma (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;
function Related_Expression (Id : E) return N;
@ -6691,6 +6705,7 @@ package Einfo is
function Is_Ghost_Entity (Id : E) return B;
function Is_Ghost_Subprogram (Id : E) return B;
function Is_Input_Only_State (Id : E) return B;
function Is_Non_Volatile_State (Id : E) return B;
function Is_Null_State (Id : E) return B;
function Is_Output_Only_State (Id : E) return B;
function Is_Package_Or_Generic_Package (Id : E) return B;
@ -6703,7 +6718,6 @@ package Einfo is
function Is_Synchronized_Interface (Id : E) return B;
function Is_Task_Interface (Id : E) return B;
function Is_Task_Record_Type (Id : E) return B;
function Is_Volatile_State (Id : E) return B;
function Is_Wrapper_Package (Id : E) return B;
function Last_Formal (Id : E) return E;
function Machine_Emax_Value (Id : E) return U;
@ -7158,7 +7172,9 @@ 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_Refined_State_Pragma (Id : E; V : N);
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);
procedure Set_Related_Expression (Id : E; V : N);
@ -7403,11 +7419,17 @@ package Einfo is
-- Empty is returned.
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id;
-- Searches the Rep_Item chain for a given entity E, for an instance of
-- a pragma with the given pragma Id. If found, the value returned is the
-- N_Pragma node, otherwise Empty is returned. Delayed pragmas such as
-- Precondition, Postcondition, Contract_Cases, Depends and Global appear
-- in the N_Contract node of entity E and are also handled by this routine.
-- Searches the Rep_Item chain of entity E, for an instance of a pragma
-- with the given pragma Id. If found, the value returned is the N_Pragma
-- node, otherwise Empty is returned. The following contract pragmas that
-- appear in N_Contract nodes are also handled by this routine:
-- Contract_Cases
-- Depends
-- Global
-- Precondition
-- Postcondition
-- Refined_Depends
-- Refined_Global
function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id;
-- Searches the Rep_Item chain for a given entity E, for a record
@ -7908,7 +7930,9 @@ package Einfo is
pragma Inline (Referenced);
pragma Inline (Referenced_As_LHS);
pragma Inline (Referenced_As_Out_Parameter);
pragma Inline (Refined_State);
pragma Inline (Refined_State_Pragma);
pragma Inline (Refinement_Constituents);
pragma Inline (Register_Exception_Call);
pragma Inline (Related_Array_Object);
pragma Inline (Related_Expression);
@ -8324,7 +8348,9 @@ 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_Refined_State_Pragma);
pragma Inline (Set_Refinement_Constituents);
pragma Inline (Set_Register_Exception_Call);
pragma Inline (Set_Related_Array_Object);
pragma Inline (Set_Related_Expression);

77
gcc/ada/elists.adb
View File

@ -158,34 +158,6 @@ package body Elists is
end loop;
end Append_Unique_Elmt;
-----------
-- Clone --
------------
function Clone (List : Elist_Id) return Elist_Id is
Result : Elist_Id;
Elmt : Elmt_Id;
begin
if List = No_Elist then
return No_Elist;
-- Replicate the contents of the input list while preserving the
-- original order.
else
Result := New_Elmt_List;
Elmt := First_Elmt (List);
while Present (Elmt) loop
Append_Elmt (Node (Elmt), Result);
Next_Elmt (Elmt);
end loop;
return Result;
end if;
end Clone;
--------------
-- Contains --
--------------
@ -315,6 +287,34 @@ package body Elists is
Elmts.Release;
end Lock;
--------------------
-- New_Copy_Elist --
--------------------
function New_Copy_Elist (List : Elist_Id) return Elist_Id is
Result : Elist_Id;
Elmt : Elmt_Id;
begin
if List = No_Elist then
return No_Elist;
-- Replicate the contents of the input list while preserving the
-- original order.
else
Result := New_Elmt_List;
Elmt := First_Elmt (List);
while Present (Elmt) loop
Append_Elmt (Node (Elmt), Result);
Next_Elmt (Elmt);
end loop;
return Result;
end if;
end New_Copy_Elist;
-------------------
-- New_Elmt_List --
-------------------
@ -425,6 +425,27 @@ package body Elists is
return Elmt /= No_Elmt;
end Present;
------------
-- Remove --
------------
procedure Remove (List : Elist_Id; N : Node_Or_Entity_Id) is
Elmt : Elmt_Id;
begin
if Present (List) then
Elmt := First_Elmt (List);
while Present (Elmt) loop
if Node (Elmt) = N then
Remove_Elmt (List, Elmt);
exit;
end if;
Next_Elmt (Elmt);
end loop;
end if;
end Remove;
-----------------
-- Remove_Elmt --
-----------------

12
gcc/ada/elists.ads
View File

@ -137,12 +137,20 @@ package Elists is
-- Add a new element (N) right after the pre-existing element Elmt
-- It is invalid to call this subprogram with Elmt = No_Elmt.
function New_Copy_Elist (List : Elist_Id) return Elist_Id;
-- Replicate the contents of a list. Internal list nodes are not shared and
-- order of elements is preserved.
procedure Replace_Elmt (Elmt : Elmt_Id; New_Node : Node_Or_Entity_Id);
pragma Inline (Replace_Elmt);
-- Causes the given element of the list to refer to New_Node, the node
-- which was previously referred to by Elmt is effectively removed from
-- the list and replaced by New_Node.
procedure Remove (List : Elist_Id; N : Node_Or_Entity_Id);
-- Remove a node or an entity from a list. If the list does not contain the
-- item in question, the routine has no effect.
procedure Remove_Elmt (List : Elist_Id; Elmt : Elmt_Id);
-- Removes Elmt from the given list. The node itself is not affected,
-- but the space used by the list element may be (but is not required
@ -153,10 +161,6 @@ package Elists is
-- affected, but the space used by the list element may be (but is not
-- required to be) freed for reuse in a subsequent Append_Elmt call.
function Clone (List : Elist_Id) return Elist_Id;
-- Create a copy of the input list. Internal list nodes are not shared and
-- order of elements is preserved.
function Contains (List : Elist_Id; N : Node_Or_Entity_Id) return Boolean;
-- Perform a sequential search to determine whether the given list contains
-- a node or an entity.

15
gcc/ada/sem_ch13.adb
View File

@ -1977,10 +1977,21 @@ package body Sem_Ch13 is
-- Refined_Global
-- ??? To be implemented
-- Aspect Refined_Global must be delayed because it can mention
-- state refinements introduced by aspect Refined_State. Since
-- Refined_State is already delayed due to forward references,
-- so is Refined_Global.
when Aspect_Refined_Global =>
null;
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_Global);
Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
Insert_Delayed_Pragma (Aitem);
goto Continue;
-- Refined_Post

15
gcc/ada/sem_ch3.adb
View File

@ -2233,12 +2233,10 @@ package body Sem_Ch3 is
Decl := First (L);
while Present (Decl) loop
if Nkind (Decl) = N_Subprogram_Body then
Analyze_Subprogram_Body_Contract
(Defining_Unit_Name (Specification (Decl)));
Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
elsif Nkind (Decl) = N_Subprogram_Declaration then
Analyze_Subprogram_Contract
(Defining_Unit_Name (Specification (Decl)));
Analyze_Subprogram_Contract (Defining_Entity (Decl));
end if;
Next (Decl);
@ -3540,7 +3538,7 @@ package body Sem_Ch3 is
if Constant_Present (N) then
Set_Ekind (Id, E_Constant);
Set_Is_True_Constant (Id, True);
Set_Is_True_Constant (Id);
else
Set_Ekind (Id, E_Variable);
@ -3763,6 +3761,13 @@ package body Sem_Ch3 is
end if;
<<Leave>>
-- Initialize the refined state of a variable here because this is a
-- common destination for legal and illegal object declarations.
if Ekind (Id) = E_Variable then
Set_Refined_State (Id, Empty);
end if;
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;

43
gcc/ada/sem_ch6.adb
View File

@ -1975,12 +1975,47 @@ package body Sem_Ch6 is
-- Analyze_Subprogram_Body_Contract --
--------------------------------------
-- ??? To be implemented
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
Prag : Node_Id;
Has_Refined_Global : Boolean := False;
procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id) is
pragma Unreferenced (Subp);
begin
null;
-- When a subprogram body declaration is erroneous, its defining entity
-- is left unanalyzed. There is nothing left to do in this case because
-- the body lacks a contract.
if not Analyzed (Body_Id) then
return;
end if;
Prag := Classifications (Contract (Body_Id));
while Present (Prag) loop
if Pragma_Name (Prag) = Name_Refined_Depends then
Analyze_Refined_Depends_In_Decl_Part (Prag);
elsif Pragma_Name (Prag) = Name_Refined_Global then
Has_Refined_Global := True;
Analyze_Refined_Global_In_Decl_Part (Prag);
end if;
Prag := Next_Pragma (Prag);
end loop;
-- When the corresponding Global aspect/pragma references a state with
-- visible refinement, the body requires Refined_Global.
if not Has_Refined_Global and then Present (Spec_Id) then
Prag := Get_Pragma (Spec_Id, Pragma_Global);
if Present (Prag) and then Contains_Refined_State (Prag) then
Error_Msg_NE
("body of subprogram & requires global refinement",
Body_Decl, Spec_Id);
end if;
end if;
end Analyze_Subprogram_Body_Contract;
------------------------------------

6
gcc/ada/sem_ch6.ads
View File

@ -46,10 +46,10 @@ package Sem_Ch6 is
procedure Analyze_Subprogram_Declaration (N : Node_Id);
procedure Analyze_Subprogram_Body (N : Node_Id);
procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id);
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed aspects chained on the contract of subprogram body
-- Subp as if they appeared at the end of a declarative region. The aspects
-- in question are:
-- Body_Id as if they appeared at the end of a declarative region. The
-- aspects in question are:
-- Refined_Depends
-- Refined_Global

1027
gcc/ada/sem_prag.adb
View File

File diff suppressed because it is too large Load Diff

123
gcc/ada/sem_util.adb
View File

@ -27,8 +27,8 @@ with Atree; use Atree;
with Casing; use Casing;
with Checks; use Checks;
with Debug; use Debug;
with Errout; use Errout;
with Elists; use Elists;
with Errout; use Errout;
with Exp_Ch11; use Exp_Ch11;
with Exp_Disp; use Exp_Disp;
with Exp_Util; use Exp_Util;
@ -3157,6 +3157,127 @@ package body Sem_Util is
end if;
end Conditional_Delay;
----------------------------
-- Contains_Refined_State --
----------------------------
function Contains_Refined_State (Prag : Node_Id) return Boolean is
function Has_Refined_State (List : Node_Id) return Boolean;
-- Determine whether a global list mentions a state with a visible
-- refinement.
-----------------------
-- Has_Refined_State --
-----------------------
function Has_Refined_State (List : Node_Id) return Boolean is
function Is_Refined_State (Item : Node_Id) return Boolean;
-- Determine whether Item is a reference to an abstract state with a
-- visible refinement.
----------------------
-- Is_Refined_State --
----------------------
function Is_Refined_State (Item : Node_Id) return Boolean is
Item_Id : Entity_Id;
begin
if Nkind (Item) = N_Null then
return False;
else
Item_Id := Entity_Of (Item);
return
Ekind (Item_Id) = E_Abstract_State
and then Present (Refinement_Constituents (Item_Id));
end if;
end Is_Refined_State;
-- Local variables
Item : Node_Id;
-- Start of processing for Has_Refined_State
begin
-- A null global list does not mention any states
if Nkind (List) = N_Null then
return False;
-- Single global item declaration
elsif Nkind_In (List, N_Expanded_Name,
N_Identifier,
N_Selected_Component)
then
return Is_Refined_State (List);
-- Simple global list or moded global list declaration
elsif Nkind (List) = N_Aggregate then
-- The declaration of a simple global list appear as a collection
-- of expressions.
if Present (Expressions (List)) then
Item := First (Expressions (List));
while Present (Item) loop
if Is_Refined_State (Item) then
return True;
end if;
Next (Item);
end loop;
-- The declaration of a moded global list appears as a collection
-- of component associations where individual choices denote
-- modes.
else
Item := First (Component_Associations (List));
while Present (Item) loop
if Has_Refined_State (Expression (Item)) then
return True;
end if;
Next (Item);
end loop;
end if;
-- If we get here, then the simple/moded global list did not
-- mention any states with a visible refinement.
return False;
-- Something went horribly wrong, we have a malformed tree
else
raise Program_Error;
end if;
end Has_Refined_State;
-- Local variables
Arg : constant Node_Id :=
Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
Nam : constant Name_Id := Pragma_Name (Prag);
-- Start of processing for Contains_Refined_State
begin
-- ??? To be implemented
if Nam = Name_Depends then
return False;
else pragma Assert (Nam = Name_Global);
return Has_Refined_State (Arg);
end if;
end Contains_Refined_State;
-------------------------
-- Copy_Component_List --
-------------------------

7
gcc/ada/sem_util.ads
View File

@ -326,6 +326,13 @@ package Sem_Util is
-- Sets the Has_Delayed_Freeze flag of New if the Delayed_Freeze flag of
-- Old is set and Old has no yet been Frozen (i.e. Is_Frozen is false).
function Contains_Refined_State (Prag : Node_Id) return Boolean;
-- Determine whether pragma Prag contains a reference to the entity of an
-- abstract state with a visible refinement. Prag must denote one of the
-- following pragmas:
-- Depends
-- Global
function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id;
-- Utility to create a parameter profile for a new subprogram spec, when
-- the subprogram has a body that acts as spec. This is done for some cases