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