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 <[email protected]>
* 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,
