Index: exp_spark.adb =================================================================== --- exp_spark.adb (revision 251863) +++ exp_spark.adb (working copy) @@ -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 : renames ; + + -- into + + -- Obj_Id : constant := ; + + -- 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; Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 251866) +++ sem_prag.adb (working copy) @@ -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); Index: sem_util.adb =================================================================== --- sem_util.adb (revision 251863) +++ sem_util.adb (working copy) @@ -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. Index: sem_util.ads =================================================================== --- sem_util.ads (revision 251863) +++ sem_util.ads (working copy) @@ -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