diff mbox series

[Ada] Remove dead check in collecting SPARK cross-references

Message ID 20171108153909.GA120228@adacore.com
State New
Headers show
Series [Ada] Remove dead check in collecting SPARK cross-references | expand

Commit Message

Pierre-Marie de Rodat Nov. 8, 2017, 3:39 p.m. UTC 
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  <trojanek@adacore.com>

	* lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove dead check for
	empty entities.
diff mbox series

Patch

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,