GNATprove now picks frontend cross-references directly from memory and
not from an ALI file), so there is no need to convert them to strings;
it is cleaner and more efficient to store them as Entity_Ids. No test
provided, because the behaviour is not affected.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-11-08 Piotr Trojanek <troja...@adacore.com>
* spark_xrefs.ads (SPARK_Xref_Record): Referenced object is now
represented by Entity_Id.
(SPARK_Scope_Record): Referenced scope (e.g. subprogram) is now
represented by Entity_Id; this information is not repeated as
Scope_Entity.
(Heap): Moved from lib-xref-spark_specific.adb, to reside next to
Name_Of_Heap_Variable.
* spark_xrefs.adb (dspark): Adapt debug routine to above changes in
data types.
* lib-xref-spark_specific.adb: Adapt routines for populating SPARK
scope and xrefs tables to above changes in data types.
Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb (revision 254538)
+++ lib-xref-spark_specific.adb (working copy)
@@ -66,9 +66,6 @@
-- Local Variables --
---------------------
- Heap : Entity_Id := Empty;
- -- A special entity which denotes the heap object
-
package Drefs is new Table.Table (
Table_Component_Type => Xref_Entry,
Table_Index_Type => Xref_Entry_Number,
@@ -164,14 +161,13 @@
-- range.
SPARK_Scope_Table.Append
- ((Scope_Name => new String'(Unique_Name (E)),
+ ((Scope_Id => E,
File_Num => Dspec,
Scope_Num => Scope_Id,
Spec_File_Num => 0,
Spec_Scope_Num => 0,
From_Xref => 1,
- To_Xref => 0,
- Scope_Entity => E));
+ To_Xref => 0));
Scope_Id := Scope_Id + 1;
end Add_SPARK_Scope;
@@ -351,7 +347,7 @@
function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
begin
- return SPARK_Scope_Table.Table (S).Scope_Entity;
+ return SPARK_Scope_Table.Table (S).Scope_Id;
end Entity_Of_Scope;
-------------------
@@ -423,7 +419,7 @@
function Is_Past_Scope_Entity return Boolean is
begin
for Index in SPARK_Scope_Table.First .. S - 1 loop
- if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
+ if SPARK_Scope_Table.Table (Index).Scope_Id = E then
return True;
end if;
end loop;
@@ -435,7 +431,7 @@
begin
for Index in S .. SPARK_Scope_Table.Last loop
- if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
+ if SPARK_Scope_Table.Table (Index).Scope_Id = E then
return True;
end if;
end loop;
@@ -634,7 +630,7 @@
declare
S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
begin
- Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
+ Set_Scope_Num (S.Scope_Id, S.Scope_Num);
end;
end loop;
@@ -800,10 +796,10 @@
end if;
SPARK_Xref_Table.Append (
- (Entity_Name => new String'(Unique_Name (Ref.Ent)),
- File_Num => Dependency_Num (Ref.Lun),
- Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
- Rtype => Typ));
+ (Entity => Unique_Entity (Ref.Ent),
+ File_Num => Dependency_Num (Ref.Lun),
+ Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
+ Rtype => Typ));
end;
end loop;
@@ -948,7 +944,7 @@
declare
Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
begin
- Entity_Hash_Table.Set (Srec.Scope_Entity, S);
+ Entity_Hash_Table.Set (Srec.Scope_Id, S);
end;
end loop;
@@ -959,14 +955,14 @@
Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
Spec_Entity : constant Entity_Id :=
- Unique_Entity (Srec.Scope_Entity);
+ Unique_Entity (Srec.Scope_Id);
Spec_Scope : constant Scope_Index :=
Entity_Hash_Table.Get (Spec_Entity);
begin
-- Generic spec may be missing in which case Spec_Scope is zero
- if Spec_Entity /= Srec.Scope_Entity
+ if Spec_Entity /= Srec.Scope_Id
and then Spec_Scope /= 0
then
Srec.Spec_File_Num :=
Index: spark_xrefs.adb
===================================================================
--- spark_xrefs.adb (revision 254538)
+++ spark_xrefs.adb (working copy)
@@ -23,7 +23,8 @@
-- --
------------------------------------------------------------------------------
-with Output; use Output;
+with Output; use Output;
+with Sem_Util; use Sem_Util;
package body SPARK_Xrefs is
@@ -81,17 +82,13 @@
Write_Int (Int (ASR.Scope_Num));
Write_Str (" Scope_Name = """);
- if ASR.Scope_Name /= null then
- Write_Str (ASR.Scope_Name.all);
- end if;
+ Write_Str (Unique_Name (ASR.Scope_Id));
Write_Char ('"');
Write_Str (" From = ");
Write_Int (Int (ASR.From_Xref));
Write_Str (" To = ");
Write_Int (Int (ASR.To_Xref));
- Write_Str (" Scope_Entity = ");
- Write_Int (Int (ASR.Scope_Entity));
Write_Eol;
end;
end loop;
@@ -111,9 +108,7 @@
Write_Int (Int (Index));
Write_Str (". Entity_Name = """);
- if AXR.Entity_Name /= null then
- Write_Str (AXR.Entity_Name.all);
- end if;
+ Write_Str (Unique_Name (AXR.Entity));
Write_Char ('"');
Write_Str (" File_Num = ");
Index: spark_xrefs.ads
===================================================================
--- spark_xrefs.ads (revision 254538)
+++ spark_xrefs.ads (working copy)
@@ -66,7 +66,7 @@
-- until a proper value is determined.
type SPARK_Xref_Record is record
- Entity_Name : String_Ptr;
+ Entity : Entity_Id;
-- Pointer to entity name in ALI file
File_Num : Nat;
@@ -109,7 +109,7 @@
-- determined.
type SPARK_Scope_Record is record
- Scope_Name : String_Ptr;
+ Scope_Id : Entity_Id;
-- Pointer to scope name in ALI file
File_Num : Nat;
@@ -131,12 +131,6 @@
To_Xref : Xref_Index;
-- Ending index in Xref table for this scope
-
- -- The following component is only used in-memory, not printed out in
- -- ALI file.
-
- Scope_Entity : Entity_Id := Empty;
- -- Entity (subprogram or package) for the scope
end record;
package SPARK_Scope_Table is new Table.Table (
@@ -193,6 +187,11 @@
-- Name of special variable used in effects to denote reads and writes
-- through explicit dereference.
+ Heap : Entity_Id := Empty;
+ -- A special entity which denotes the heap object; it should be considered
+ -- constant, but needs to be variable, because it can only be initialized
+ -- after the node tables are created.
+
-----------------
-- Subprograms --
-----------------
