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 <troja...@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.
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
