From 013e9958f80bbba91f14dba7f1fa83ac9809ad7d Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Wed, 8 Nov 2017 15:48:46 +0000 Subject: [PATCH] spark_xrefs.ads (SPARK_Xref_Record): Remove inessential components. 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. From-SVN: r254538 --- gcc/ada/ChangeLog | 15 ++++++++++ gcc/ada/lib-xref-spark_specific.adb | 57 ++++--------------------------------- gcc/ada/spark_xrefs.adb | 14 --------- gcc/ada/spark_xrefs.ads | 33 --------------------- 4 files changed, 21 insertions(+), 98 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8826c77..b607ce6 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,18 @@ +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. + +2017-11-08 Piotr Trojanek + + * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove dead check for + empty entities. + 2017-11-08 Javier Miranda * sem_disp.adb (Is_Inherited_Public_Operation): Extend the diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 4837718..3950719 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -120,14 +120,7 @@ package body SPARK_Specific is --------------------- procedure Add_SPARK_Scope (N : Node_Id) is - E : constant Entity_Id := Defining_Entity (N); - Loc : constant Source_Ptr := Sloc (E); - - -- 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; + E : constant Entity_Id := Defining_Entity (N); begin -- Ignore scopes without a proper location @@ -144,18 +137,15 @@ package body SPARK_Specific is | 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 @@ package body SPARK_Specific is 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 @@ package body SPARK_Specific is 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 @@ package body SPARK_Specific is 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 @@ package body SPARK_Specific is -- Local variables - Col : Nat; From_Index : Xref_Index; - Line : Nat; Prev_Loc : Source_Ptr; Prev_Typ : Character; Ref_Count : Nat; @@ -817,14 +785,6 @@ package body SPARK_Specific is 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 @@ package body SPARK_Specific is 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; diff --git a/gcc/ada/spark_xrefs.adb b/gcc/ada/spark_xrefs.adb index ca4e69d..ebec6c4 100644 --- a/gcc/ada/spark_xrefs.adb +++ b/gcc/ada/spark_xrefs.adb @@ -86,12 +86,6 @@ package body SPARK_Xrefs is 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 @@ package body SPARK_Xrefs is 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; diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index 7fb2939..962b7af 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -69,19 +69,6 @@ package SPARK_Xrefs is 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 @@ package SPARK_Xrefs is -- 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 @@ package SPARK_Xrefs is -- 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 -- 2.7.4