===================================================================
@@ -292,10 +292,55 @@
------------------------------------------------
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
+ CFS : constant Boolean := Comes_From_Source (N);
+ Loc : constant Source_Ptr := Sloc (N);
+ Obj_Id : constant Entity_Id := Defining_Entity (N);
+ Nam : constant Node_Id := Name (N);
+ Typ : constant Entity_Id := Etype (Subtype_Mark (N));
+
begin
- -- Unconditionally remove all side effects from the name
+ -- Transform a renaming of the form
- Evaluate_Name (Name (N));
+ -- Obj_Id : <subtype mark> renames <function call>;
+
+ -- into
+
+ -- Obj_Id : constant <subtype mark> := <function call>;
+
+ -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
+ -- a temporary to capture the function result. Once potential renamings
+ -- are rewritten for SPARK, the temporary may be leaked out into source
+ -- constructs and lead to confusing error diagnostics. Using an object
+ -- declaration prevents this unwanted side effect.
+
+ if Nkind (Nam) = N_Function_Call then
+ Rewrite (N,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Obj_Id,
+ Constant_Present => True,
+ Object_Definition => New_Occurrence_Of (Typ, Loc),
+ Expression => Nam));
+
+ -- Inherit the original Comes_From_Source status of the renaming
+
+ Set_Comes_From_Source (N, CFS);
+
+ -- Sever the link to the renamed function result because the entity
+ -- will no longer alias anything.
+
+ Set_Renamed_Object (Obj_Id, Empty);
+
+ -- Remove the entity of the renaming declaration from visibility as
+ -- the analysis of the object declaration will reintroduce it again.
+
+ Remove_Entity (Obj_Id);
+ Analyze (N);
+
+ -- Otherwise unconditionally remove all side effects from the name
+
+ else
+ Evaluate_Name (Nam);
+ end if;
end Expand_SPARK_N_Object_Renaming_Declaration;
------------------------
@@ -324,29 +369,30 @@
procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
- Ren_Id : constant Entity_Id := Entity (N);
+ Obj_Id : constant Entity_Id := Entity (N);
Typ : constant Entity_Id := Etype (N);
- Obj_Id : Node_Id;
+ Ren : Node_Id;
begin
-- Replace a reference to a renaming with the actual renamed object
- if Ekind (Ren_Id) in Object_Kind then
- Obj_Id := Renamed_Object (Ren_Id);
+ if Ekind (Obj_Id) in Object_Kind then
+ Ren := Renamed_Object (Obj_Id);
- if Present (Obj_Id) then
+ if Present (Ren) then
- -- The renamed object is an entity when instantiating generics
- -- or inlining bodies. In this case the renaming is part of the
- -- mapping "prologue" which links actuals to formals.
+ -- Instantiations and inlining of subprograms employ "prologues"
+ -- which map actual to formal parameters by means of renamings.
+ -- Replace a reference to a formal by the corresponding actual
+ -- parameter.
- if Nkind (Obj_Id) in N_Entity then
- Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
+ if Nkind (Ren) in N_Entity then
+ Rewrite (N, New_Occurrence_Of (Ren, Loc));
-- Otherwise the renamed object denotes a name
else
- Rewrite (N, New_Copy_Tree (Obj_Id, New_Sloc => Loc));
+ Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
Reset_Analyzed_Flags (N);
end if;
===================================================================
@@ -283,9 +283,9 @@
-- reference for future checks (see Analyze_Refined_State_In_Decls).
procedure Resolve_State (N : Node_Id);
- -- Handle the overloading of state names by parameterless functions. When N
- -- denotes a function, this routine finds the corresponding state and sets
- -- the entity of N to that of the state.
+ -- Handle the overloading of state names by functions. When N denotes a
+ -- function, this routine finds the corresponding state and sets the entity
+ -- of N to that of the state.
procedure Rewrite_Assertion_Kind
(N : Node_Id;
@@ -2811,9 +2811,10 @@
if Is_Entity_Name (Item) then
Item_Id := Entity_Of (Item);
- if Ekind_In (Item_Id, E_Abstract_State,
- E_Constant,
- E_Variable)
+ if Present (Item_Id)
+ and then Ekind_In (Item_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
then
-- The state or variable must be declared in the visible
-- declarations of the package (SPARK RM 7.1.5(7)).
@@ -2918,14 +2919,15 @@
if Is_Entity_Name (Input) then
Input_Id := Entity_Of (Input);
- if Ekind_In (Input_Id, E_Abstract_State,
- E_Constant,
- E_Generic_In_Out_Parameter,
- E_Generic_In_Parameter,
- E_In_Parameter,
- E_In_Out_Parameter,
- E_Out_Parameter,
- E_Variable)
+ if Present (Input_Id)
+ and then Ekind_In (Input_Id, E_Abstract_State,
+ E_Constant,
+ E_Generic_In_Out_Parameter,
+ E_Generic_In_Parameter,
+ E_In_Parameter,
+ E_In_Out_Parameter,
+ E_Out_Parameter,
+ E_Variable)
then
-- The input cannot denote states or objects declared
-- within the related package (SPARK RM 7.1.5(4)).
@@ -3073,7 +3075,8 @@
Decl := First (Visible_Declarations (Pack_Spec));
while Present (Decl) loop
if Comes_From_Source (Decl)
- and then Nkind (Decl) = N_Object_Declaration
+ and then Nkind_In (Decl, N_Object_Declaration,
+ N_Object_Renaming_Declaration)
then
Append_New_Elmt (Defining_Entity (Decl), States_And_Objs);
===================================================================
@@ -7117,23 +7117,46 @@
---------------
function Entity_Of (N : Node_Id) return Entity_Id is
- Id : Entity_Id;
+ Id : Entity_Id;
+ Ren : Node_Id;
begin
+ -- Assume that the arbitrary node does not have an entity
+
Id := Empty;
if Is_Entity_Name (N) then
Id := Entity (N);
- -- Follow a possible chain of renamings to reach the root renamed
- -- object.
+ -- Follow a possible chain of renamings to reach the earliest renamed
+ -- source object.
while Present (Id)
and then Is_Object (Id)
and then Present (Renamed_Object (Id))
loop
- if Is_Entity_Name (Renamed_Object (Id)) then
- Id := Entity (Renamed_Object (Id));
+ Ren := Renamed_Object (Id);
+
+ -- The reference renames an abstract state or a whole object
+
+ -- Obj : ...;
+ -- Ren : ... renames Obj;
+
+ if Is_Entity_Name (Ren) then
+ Id := Entity (Ren);
+
+ -- The reference renames a function result. Check the original
+ -- node in case expansion relocates the function call.
+
+ -- Ren : ... renames Func_Call;
+
+ elsif Nkind (Original_Node (Ren)) = N_Function_Call then
+ exit;
+
+ -- Otherwise the reference renames something which does not yield
+ -- an abstract state or a whole object. Treat the reference as not
+ -- having a proper entity for SPARK legality purposes.
+
else
Id := Empty;
exit;
@@ -20369,6 +20392,61 @@
end if;
end References_Generic_Formal_Type;
+ -------------------
+ -- Remove_Entity --
+ -------------------
+
+ procedure Remove_Entity (Id : Entity_Id) is
+ Scop : constant Entity_Id := Scope (Id);
+ Prev_Id : Entity_Id;
+
+ begin
+ -- Remove the entity from the homonym chain. When the entity is the
+ -- head of the chain, associate the entry in the name table with its
+ -- homonym effectively making it the new head of the chain.
+
+ if Current_Entity (Id) = Id then
+ Set_Name_Entity_Id (Chars (Id), Homonym (Id));
+
+ -- Otherwise link the previous and next homonyms
+
+ else
+ Prev_Id := Current_Entity (Id);
+ while Present (Prev_Id) and then Homonym (Prev_Id) /= Id loop
+ Prev_Id := Homonym (Prev_Id);
+ end loop;
+
+ Set_Homonym (Prev_Id, Homonym (Id));
+ end if;
+
+ -- Remove the entity from the scope entity chain. When the entity is
+ -- the head of the chain, set the next entity as the new head of the
+ -- chain.
+
+ if First_Entity (Scop) = Id then
+ Prev_Id := Empty;
+ Set_First_Entity (Scop, Next_Entity (Id));
+
+ -- Otherwise the entity is either in the middle of the chain or it acts
+ -- as its tail. Traverse and link the previous and next entities.
+
+ else
+ Prev_Id := First_Entity (Scop);
+ while Present (Prev_Id) and then Next_Entity (Prev_Id) /= Id loop
+ Next_Entity (Prev_Id);
+ end loop;
+
+ Set_Next_Entity (Prev_Id, Next_Entity (Id));
+ end if;
+
+ -- Handle the case where the entity acts as the tail of the scope entity
+ -- chain.
+
+ if Last_Entity (Scop) = Id then
+ Set_Last_Entity (Scop, Prev_Id);
+ end if;
+ end Remove_Entity;
+
--------------------
-- Remove_Homonym --
--------------------
@@ -20428,58 +20506,15 @@
-- Local variables
- Scop : constant Entity_Id := Scope (Id);
- Formal : Entity_Id;
- Prev_Id : Entity_Id;
+ Formal : Entity_Id;
-- Start of processing for Remove_Overloaded_Entity
begin
- -- Remove the entity from the homonym chain. When the entity is the
- -- head of the chain, associate the entry in the name table with its
- -- homonym effectively making it the new head of the chain.
+ -- Remove the entity from both the homonym and scope chains
- if Current_Entity (Id) = Id then
- Set_Name_Entity_Id (Chars (Id), Homonym (Id));
+ Remove_Entity (Id);
- -- Otherwise link the previous and next homonyms
-
- else
- Prev_Id := Current_Entity (Id);
- while Present (Prev_Id) and then Homonym (Prev_Id) /= Id loop
- Prev_Id := Homonym (Prev_Id);
- end loop;
-
- Set_Homonym (Prev_Id, Homonym (Id));
- end if;
-
- -- Remove the entity from the scope entity chain. When the entity is
- -- the head of the chain, set the next entity as the new head of the
- -- chain.
-
- if First_Entity (Scop) = Id then
- Prev_Id := Empty;
- Set_First_Entity (Scop, Next_Entity (Id));
-
- -- Otherwise the entity is either in the middle of the chain or it acts
- -- as its tail. Traverse and link the previous and next entities.
-
- else
- Prev_Id := First_Entity (Scop);
- while Present (Prev_Id) and then Next_Entity (Prev_Id) /= Id loop
- Next_Entity (Prev_Id);
- end loop;
-
- Set_Next_Entity (Prev_Id, Next_Entity (Id));
- end if;
-
- -- Handle the case where the entity acts as the tail of the scope entity
- -- chain.
-
- if Last_Entity (Scop) = Id then
- Set_Last_Entity (Scop, Prev_Id);
- end if;
-
-- The entity denotes a primitive subprogram. Remove it from the list of
-- primitives of the associated controlling type.
===================================================================
@@ -689,8 +689,9 @@
-- are entered using Sem_Ch6.Enter_Overloadable_Entity.
function Entity_Of (N : Node_Id) return Entity_Id;
- -- Return the entity of N or Empty. If N is a renaming, return the entity
- -- of the root renamed object.
+ -- Obtain the entity of arbitrary node N. If N is a renaming, return the
+ -- entity of the earliest renamed source abstract state or whole object.
+ -- If no suitable entity is available, return Empty.
procedure Explain_Limited_Type (T : Entity_Id; N : Node_Id);
-- This procedure is called after issuing a message complaining about an
@@ -2265,14 +2266,20 @@
-- Returns True if the expression Expr contains any references to a generic
-- type. This can only happen within a generic template.
+ procedure Remove_Entity (Id : Entity_Id);
+ -- Remove arbitrary entity Id from both the homonym and scope chains. Use
+ -- Remove_Overloaded_Entity for overloadable entities. Note: the removal
+ -- performed by this routine does not affect the visibility of existing
+ -- homonyms.
+
procedure Remove_Homonym (E : Entity_Id);
-- Removes E from the homonym chain
procedure Remove_Overloaded_Entity (Id : Entity_Id);
-- Remove arbitrary entity Id from the homonym chain, the scope chain and
- -- the primitive operations list of the associated controlling type. NOTE:
- -- the removal performed by this routine does not affect the visibility of
- -- existing homonyms.
+ -- the primitive operations list of the associated controlling type. Use
+ -- Remove_Entity for non-overloadable entities. Note: the removal performed
+ -- by this routine does not affect the visibility of existing homonyms.
function Remove_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
-- Returns the name of E without Suffix