diff mbox series

[Ada] Ignore file and unit names when collecting SPARK cross-references

Message ID 20171108162252.GA60087@adacore.com
State New
Headers show
Series [Ada] Ignore file and unit names when collecting SPARK cross-references | expand

Commit Message

Pierre-Marie de Rodat Nov. 8, 2017, 4:22 p.m. UTC 
Human-readable file and unit names in SPARK cross-references were only
needed to make the ALI file human-redable. They are now removed (but can
be added to the debug routine dspark if needed).

Modified code is only executed as part of GNATprove, so no impact on the
frontend. Behaviour unaffected, so no test provided.

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

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

	* spark_xrefs.ads (SPARK_File_Record): Remove string components.
	* spark_xrefs.adb (dspark): Remove pretty-printing of removed
	SPARK_File_Record components.
	* lib-xref-spark_specific.adb (Add_SPARK_File): Do not store string
	representation of files/units.
diff mbox series

Patch

Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb	(revision 254540)
+++ lib-xref-spark_specific.adb	(working copy)
@@ -208,11 +208,6 @@ 
       procedure Traverse_Scopes is new
         Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
 
-      --  Local variables
-
-      File_Name      : String_Ptr;
-      Unit_File_Name : String_Ptr;
-
    --  Start of processing for Add_SPARK_File
 
    begin
@@ -240,29 +235,10 @@ 
          Traverse_Scopes (CU => Cunit (Ubody));
       end if;
 
-      --  Make entry for new file in file table
-
-      Get_Name_String (Reference_Name (File));
-      File_Name := new String'(Name_Buffer (1 .. Name_Len));
-
-      --  For subunits, also retrieve the file name of the unit. Only do so if
-      --  unit has an associated compilation unit.
-
-      if Present (Cunit (Unit (File)))
-        and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
-      then
-         Get_Name_String (Reference_Name (Main_Source_File));
-         Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len));
-      else
-         Unit_File_Name := null;
-      end if;
-
       SPARK_File_Table.Append (
-        (File_Name      => File_Name,
-         Unit_File_Name => Unit_File_Name,
-         File_Num       => Dspec,
-         From_Scope     => From,
-         To_Scope       => SPARK_Scope_Table.Last));
+        (File_Num   => Dspec,
+         From_Scope => From,
+         To_Scope   => SPARK_Scope_Table.Last));
    end Add_SPARK_File;
 
    ---------------------
Index: spark_xrefs.adb
===================================================================
--- spark_xrefs.adb	(revision 254539)
+++ spark_xrefs.adb	(working copy)
@@ -48,13 +48,6 @@ 
             Write_Int (Int (Index));
             Write_Str (".  File_Num = ");
             Write_Int (Int (AFR.File_Num));
-            Write_Str ("  File_Name = """);
-
-            if AFR.File_Name /= null then
-               Write_Str (AFR.File_Name.all);
-            end if;
-
-            Write_Char ('"');
             Write_Str ("  From = ");
             Write_Int (Int (AFR.From_Scope));
             Write_Str ("  To = ");
Index: spark_xrefs.ads
===================================================================
--- spark_xrefs.ads	(revision 254539)
+++ spark_xrefs.ads	(working copy)
@@ -154,13 +154,6 @@ 
    --  entries have been constructed.
 
    type SPARK_File_Record is record
-      File_Name : String_Ptr;
-      --  Pointer to file name in ALI file
-
-      Unit_File_Name : String_Ptr;
-      --  Pointer to file name for unit in ALI file, when File_Name refers to a
-      --  subunit; otherwise null.
-
       File_Num : Nat;
       --  Dependency number in ALI file