From: Pierre-Marie de Rodat <derodat@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Piotr Trojanek <trojanek@adacore.com>
Subject: [Ada] Don't collect inessential data about SPARK cross-references
Date: Wed, 08 Nov 2017 16:06:00 -0000 [thread overview]
Message-ID: <20171108154903.GA136032@adacore.com> (raw)
[-- 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
reply other threads:[~2017-11-08 15:49 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20171108154903.GA136032@adacore.com \
--to=derodat@adacore.com \
--cc=gcc-patches@gcc.gnu.org \
--cc=trojanek@adacore.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
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).