===================================================================
@@ -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
This patch changes the expansion of object renamings in SPARK to reuse the entity associated with the renaming when the name denotes a function call. The patch also modifies a routine used to extract the entity of references to abstract states and whole objects to handle renamings of function results. Together, both these changes allow for function result renamings in SPARK annotations. ------------ -- Source -- ------------ -- pack.ads package Pack with SPARK_Mode is type Lim_Rec is limited record Data : Integer; end record; function Get_Integer return Integer; function Get_Lim_Rec return Lim_Rec; function Get_String return String; end Pack; -- pack.adb package body Pack with SPARK_Mode is function Get_Integer return Integer is begin return 123; end Get_Integer; function Get_Lim_Rec return Lim_Rec is begin return Result : Lim_Rec; end Get_Lim_Rec; function Get_String return String is begin return "456"; end Get_String; package Nested with Initializes => (Int_Ren, Lim_Ren, Str_Ren) is Int_Ren : Integer renames Get_Integer; Lim_Ren : Lim_Rec renames Get_Lim_Rec; Str_Ren : String renames Get_String; procedure Proc with Global => (Int_Ren, Lim_Ren, Str_Ren), Depends => (null => (Int_Ren, Lim_Ren, Str_Ren)); end Nested; package body Nested is procedure Proc is begin null; end Proc; end Nested; end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.adb $ gcc -c pack.adb -gnatd.F pack.adb:9:14: warning: variable "Result" is read but never assigned pack.adb:9:14: warning: variable "Result" is read but never assigned Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-08 Hristian Kirtchev <kirtchev@adacore.com> * exp_spark.adb (Expand_SPARK_N_Object_Renaming_Declaration): Reimplemented. (Expand_SPARK_Potential_Renaming): Code clean up. * sem_prag.adb (Analyze_Initialization_Item): Add a guard in case the item does not have a proper entity. (Analyze_Input_Item): Add a guard in case the item does not have a proper entity. (Collect_States_And_Objects): Include object renamings in the items being collected. (Resolve_State): Update the documentation of this routine. * sem_util.adb (Entity_Of): Add circuitry to handle renamings of function results. (Remove_Entity): New routine. (Remove_Overloaded_Entity): Take advantage of factorization. * sem_util.ads (Entity_Of): Update the documentation of this routine. (Remove_Entity): New routine. (Remove_Overloaded_Entity): Update the documentation of this routine.