GNATprove never collects cross-references to empty entities. Removed code most likely became dead at some point and this was not noticed. No test, as the removed code was only executed as part of GNATprove and its behaviour appears not affected.
Tested on x86_64-pc-linux-gnu, committed on trunk 2017-11-08 Piotr Trojanek <troja...@adacore.com> * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove dead check for empty entities.
Index: lib-xref-spark_specific.adb =================================================================== --- lib-xref-spark_specific.adb (revision 254532) +++ lib-xref-spark_specific.adb (working copy) @@ -657,7 +657,6 @@ Prev_Loc : Source_Ptr; Prev_Typ : Character; Ref_Count : Nat; - Ref_Name : String_Ptr; Scope_Id : Scope_Index; -- Start of processing for Add_SPARK_Xrefs @@ -818,10 +817,6 @@ pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); end loop; - if Present (Ref.Ent) then - Ref_Name := new String'(Unique_Name (Ref.Ent)); - end if; - if Ref.Ent = Heap then Line := 0; Col := 0; @@ -845,7 +840,7 @@ end if; SPARK_Xref_Table.Append ( - (Entity_Name => Ref_Name, + (Entity_Name => new String'(Unique_Name (Ref.Ent)), Entity_Line => Line, Etype => Get_Entity_Type (Ref.Ent), Entity_Col => Col,