From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 83276 invoked by alias); 8 Nov 2017 15:49:07 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Received: (qmail 82930 invoked by uid 89); 8 Nov 2017 15:49:06 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-15.7 required=5.0 tests=AWL,BAYES_00,GIT_PATCH_1,GIT_PATCH_2,GIT_PATCH_3,KAM_ASCII_DIVIDERS,RCVD_IN_DNSWL_NONE,SPF_PASS autolearn=ham version=3.3.2 spammy= X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Wed, 08 Nov 2017 15:49:05 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id BEDF756B93; Wed, 8 Nov 2017 10:49:03 -0500 (EST) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id wpzM6AcfqkXd; Wed, 8 Nov 2017 10:49:03 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id AB4EE56A53; Wed, 8 Nov 2017 10:49:03 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4862) id A74F52FD; Wed, 8 Nov 2017 10:49:03 -0500 (EST) Date: Wed, 08 Nov 2017 16:06:00 -0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [Ada] Don't collect inessential data about SPARK cross-references Message-ID: <20171108154903.GA136032@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="UlVJffcvxoiEqYs2" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes X-SW-Source: 2017-11/txt/msg00607.txt.bz2 --UlVJffcvxoiEqYs2 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-length: 912 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 * 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. --UlVJffcvxoiEqYs2 Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename=difs Content-length: 7627 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 --UlVJffcvxoiEqYs2--