* [Ada] Don't collect inessential data about SPARK cross-references
@ 2017-11-08 16:06 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2017-11-08 16:06 UTC (permalink / raw)
To: gcc-patches; +Cc: Piotr Trojanek
[-- Attachment #1: Type: text/plain, Size: 912 bytes --]
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.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 7627 bytes --]
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2017-11-08 15:49 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-11-08 16:06 [Ada] Don't collect inessential data about SPARK cross-references Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).