+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.
+
+2017-11-08 Piotr Trojanek <trojanek@adacore.com>
+
+ * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove dead check for
+ empty entities.
+
2017-11-08 Javier Miranda <miranda@adacore.com>
* sem_disp.adb (Is_Inherited_Public_Operation): Extend the
---------------------
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
| 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 =>
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));
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
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 --
-------------------
-- Local variables
- Col : Nat;
From_Index : Xref_Index;
- Line : Nat;
Prev_Loc : Source_Ptr;
Prev_Typ : Character;
Ref_Count : Nat;
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
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;
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 = ");
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;
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
-- 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 (
-- 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
projects / gcc.git / commitdiff