This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
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.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |