diff mbox series

[Ada] Don't collect inessential data about SPARK cross-references

Message ID 20171108154903.GA136032@adacore.com
State New
Headers show
Series [Ada] Don't collect inessential data about SPARK cross-references | expand

Commit Message

Pierre-Marie de Rodat Nov. 8, 2017, 3:49 p.m. UTC
Part of deconstructing SPARK cross-references, which are used to synthesize
Global contracts for code annotated with SPARK_Mode => Off.

Data like line and column numbers was only needed to make the xrefs in the
ALI file more readable. Now that the xrefs are not written to the ALI file
at all, there is no need to collect this data.

Removed code was only executed as part of GNATprove (and its behaviour
remains as it was), so no test.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
diff mbox series

Patch

Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb	(revision 254535)
+++ lib-xref-spark_specific.adb	(working copy)
@@ -120,15 +120,8 @@ 
       ---------------------
 
       procedure Add_SPARK_Scope (N : Node_Id) is
-         E   : constant Entity_Id  := Defining_Entity (N);
-         Loc : constant Source_Ptr := Sloc (E);
+         E : constant Entity_Id := Defining_Entity (N);
 
-         --  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;
-
       begin
          --  Ignore scopes without a proper location
 
@@ -144,18 +137,15 @@ 
                | 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 @@ 
              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 @@ 
       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 @@ 
          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 @@ 
 
       --  Local variables
 
-      Col        : Nat;
       From_Index : Xref_Index;
-      Line       : Nat;
       Prev_Loc   : Source_Ptr;
       Prev_Typ   : Character;
       Ref_Count  : Nat;
@@ -817,14 +785,6 @@ 
                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 @@ 
 
             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;
 
Index: spark_xrefs.adb
===================================================================
--- spark_xrefs.adb	(revision 254535)
+++ spark_xrefs.adb	(working copy)
@@ -86,12 +86,6 @@ 
             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 @@ 
             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;
Index: spark_xrefs.ads
===================================================================
--- spark_xrefs.ads	(revision 254535)
+++ spark_xrefs.ads	(working copy)
@@ -69,19 +69,6 @@ 
       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 @@ 
       --  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 @@ 
       --  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