spark_xrefs.ads (SPARK_Xref_Record): Remove inessential components.

2017-11-08  Piotr Trojanek  <trojanek@adacore.com>

	* spark_xrefs.ads (SPARK_Xref_Record): Remove inessential components.
	(SPARK_Scope_Record): Remove inessential components.
	* spark_xrefs.adb (dspark): Remove pretty-printing of removed record
	components.
	* lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove setting of
	removed record components.
	(Add_SPARK_Xrefs): Remove setting of removed record components.

From-SVN: r254538

gcc/ada/ChangeLog

+2017-11-08  Piotr Trojanek  <trojanek@adacore.com>
+
+	* spark_xrefs.ads (SPARK_Xref_Record): Remove inessential components.
+	(SPARK_Scope_Record): Remove inessential components.
+	* spark_xrefs.adb (dspark): Remove pretty-printing of removed record
+	components.
+	* lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove setting of
+	removed record components.
+	(Add_SPARK_Xrefs): Remove setting of removed record components.
+
+2017-11-08  Piotr Trojanek  <trojanek@adacore.com>
+
+	* lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove dead check for
+	empty entities.
+
 2017-11-08  Javier Miranda  <miranda@adacore.com>
 
 	* sem_disp.adb (Is_Inherited_Public_Operation): Extend the

gcc/ada/lib-xref-spark_specific.adb

@@ -120,14 +120,7 @@ package body SPARK_Specific is
       ---------------------
 
       procedure Add_SPARK_Scope (N : Node_Id) is
-         E   : constant Entity_Id  := Defining_Entity (N);
-         Loc : constant Source_Ptr := Sloc (E);
-
-         --  The character describing the kind of scope is chosen to be the
-         --  same as the one describing the corresponding entity in cross
-         --  references, see Xref_Entity_Letters in lib-xrefs.ads
-
-         Typ : Character;
+         E : constant Entity_Id := Defining_Entity (N);
 
       begin
          --  Ignore scopes without a proper location
@@ -144,18 +137,15 @@ package body SPARK_Specific is
                | E_Generic_Package
                | E_Generic_Procedure
                | E_Package
+               | E_Package_Body
                | E_Procedure
+               | E_Protected_Body
                | E_Protected_Type
+               | E_Task_Body
                | E_Task_Type
-            =>
-               Typ := Xref_Entity_Letters (Ekind (E));
-
-            when E_Package_Body
-               | E_Protected_Body
                | E_Subprogram_Body
-               | E_Task_Body
             =>
-               Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
+               null;
 
             when E_Void =>
 
@@ -179,9 +169,6 @@ package body SPARK_Specific is
              Scope_Num      => Scope_Id,
              Spec_File_Num  => 0,
              Spec_Scope_Num => 0,
-             Line           => Nat (Get_Logical_Line_Number (Loc)),
-             Stype          => Typ,
-             Col            => Nat (Get_Column_Number (Loc)),
              From_Xref      => 1,
              To_Xref        => 0,
              Scope_Entity   => E));
@@ -290,9 +277,6 @@ package body SPARK_Specific is
       function Entity_Of_Scope (S : Scope_Index) return Entity_Id;
       --  Return the entity which maps to the input scope index
 
-      function Get_Entity_Type (E : Entity_Id) return Character;
-      --  Return a character representing the type of entity
-
       function Get_Scope_Num (E : Entity_Id) return Nat;
       --  Return the scope number associated with the entity E
 
@@ -370,20 +354,6 @@ package body SPARK_Specific is
          return SPARK_Scope_Table.Table (S).Scope_Entity;
       end Entity_Of_Scope;
 
-      ---------------------
-      -- Get_Entity_Type --
-      ---------------------
-
-      function Get_Entity_Type (E : Entity_Id) return Character is
-      begin
-         case Ekind (E) is
-            when E_Out_Parameter    => return '<';
-            when E_In_Out_Parameter => return '=';
-            when E_In_Parameter     => return '>';
-            when others             => return '*';
-         end case;
-      end Get_Entity_Type;
-
       -------------------
       -- Get_Scope_Num --
       -------------------
@@ -651,9 +621,7 @@ package body SPARK_Specific is
 
       --  Local variables
 
-      Col        : Nat;
       From_Index : Xref_Index;
-      Line       : Nat;
       Prev_Loc   : Source_Ptr;
       Prev_Typ   : Character;
       Ref_Count  : Nat;
@@ -817,14 +785,6 @@ package body SPARK_Specific is
                pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
             end loop;
 
-            if Ref.Ent = Heap then
-               Line := 0;
-               Col  := 0;
-            else
-               Line := Nat (Get_Logical_Line_Number (Ref_Entry.Def));
-               Col  := Nat (Get_Column_Number (Ref_Entry.Def));
-            end if;
-
             --  References to constant objects without variable inputs (see
             --  SPARK RM 3.3.1) are considered specially in SPARK section,
             --  because these will be translated as constants in the
@@ -841,14 +801,9 @@ package body SPARK_Specific is
 
             SPARK_Xref_Table.Append (
               (Entity_Name => new String'(Unique_Name (Ref.Ent)),
-               Entity_Line => Line,
-               Etype       => Get_Entity_Type (Ref.Ent),
-               Entity_Col  => Col,
                File_Num    => Dependency_Num (Ref.Lun),
                Scope_Num   => Get_Scope_Num (Ref.Ref_Scope),
-               Line        => Nat (Get_Logical_Line_Number (Ref.Loc)),
-               Rtype       => Typ,
-               Col         => Nat (Get_Column_Number (Ref.Loc))));
+               Rtype       => Typ));
          end;
       end loop;
 

gcc/ada/spark_xrefs.adb

@@ -86,12 +86,6 @@ package body SPARK_Xrefs is
             end if;
 
             Write_Char ('"');
-            Write_Str  ("  Line = ");
-            Write_Int  (Int (ASR.Line));
-            Write_Str  ("  Col = ");
-            Write_Int  (Int (ASR.Col));
-            Write_Str  ("  Type = ");
-            Write_Char (ASR.Stype);
             Write_Str  ("  From = ");
             Write_Int  (Int (ASR.From_Xref));
             Write_Str  ("  To = ");
@@ -122,18 +116,10 @@ package body SPARK_Xrefs is
             end if;
 
             Write_Char ('"');
-            Write_Str ("  Entity_Line = ");
-            Write_Int (Int (AXR.Entity_Line));
-            Write_Str ("  Entity_Col = ");
-            Write_Int (Int (AXR.Entity_Col));
             Write_Str ("  File_Num = ");
             Write_Int (Int (AXR.File_Num));
             Write_Str ("  Scope_Num = ");
             Write_Int (Int (AXR.Scope_Num));
-            Write_Str ("  Line = ");
-            Write_Int (Int (AXR.Line));
-            Write_Str ("  Col = ");
-            Write_Int (Int (AXR.Col));
             Write_Str ("  Type = ");
             Write_Char (AXR.Rtype);
             Write_Eol;

gcc/ada/spark_xrefs.ads

@@ -69,19 +69,6 @@ package SPARK_Xrefs is
       Entity_Name : String_Ptr;
       --  Pointer to entity name in ALI file
 
-      Entity_Line : Nat;
-      --  Line number for the entity referenced
-
-      Etype : Character;
-      --  Indicates type of entity, using code used in ALI file:
-      --    > = IN parameter
-      --    < = OUT parameter
-      --    = = IN OUT parameter
-      --    * = all other cases
-
-      Entity_Col : Nat;
-      --  Column number for the entity referenced
-
       File_Num : Nat;
       --  File dependency number for the cross-reference. Note that if no file
       --  entry is present explicitly, this is just a copy of the reference for
@@ -92,18 +79,12 @@ package SPARK_Xrefs is
       --  present explicitly, this is just a copy of the reference for the
       --  current cross-reference section.
 
-      Line : Nat;
-      --  Line number for the reference
-
       Rtype : Character;
       --  Indicates type of the reference, using code used in ALI file:
       --    r = reference
       --    c = reference to constant object
       --    m = modification
       --    s = call
-
-      Col : Nat;
-      --  Column number for the reference
    end record;
 
    package SPARK_Xref_Table is new Table.Table (
@@ -145,20 +126,6 @@ package SPARK_Xrefs is
       --  Set to the scope number for the scope corresponding to the spec of
       --  the current scope entity, if different, or else 0.
 
-      Line : Nat;
-      --  Line number for the scope
-
-      Stype : Character;
-      --  Indicates type of scope, using code used in ALI file:
-      --    K = package
-      --    T = task
-      --    U = procedure
-      --    V = function
-      --    Y = entry
-
-      Col : Nat;
-      --  Column number for the scope
-
       From_Xref : Xref_Index;
       --  Starting index in Xref table for this scope