[multiple changes]
2017-11-08 Piotr Trojanek <trojanek@adacore.com> * spark_xrefs.ads (SPARK_Xref_Record): Referenced object is now represented by Entity_Id. (SPARK_Scope_Record): Referenced scope (e.g. subprogram) is now represented by Entity_Id; this information is not repeated as Scope_Entity. (Heap): Moved from lib-xref-spark_specific.adb, to reside next to Name_Of_Heap_Variable. * spark_xrefs.adb (dspark): Adapt debug routine to above changes in data types. * lib-xref-spark_specific.adb: Adapt routines for populating SPARK scope and xrefs tables to above changes in data types. 2017-11-08 Justin Squirek <squirek@adacore.com> * sem_ch8.adb (Mark_Use_Clauses): Add condition to always mark the primitives of generic actuals. (Mark_Use_Type): Add recursive call to properly mark class-wide type's base type clauses as per ARM 8.4 (8.2/3). 2017-11-08 Ed Schonberg <schonberg@adacore.com> * sem_ch6.adb (Analyze_Generic_Subprobram_Body): Validate categorization dependency of the body, as is done for non-generic units. (New_Overloaded_Entity, Visible_Part_Type): Remove linear search through declarations (Simple optimization, no behavior change). From-SVN: r254539
This commit is contained in:
parent
013e9958f8
commit
3e5400f4ac
@ -1,3 +1,32 @@
|
||||
2017-11-08 Piotr Trojanek <trojanek@adacore.com>
|
||||
|
||||
* spark_xrefs.ads (SPARK_Xref_Record): Referenced object is now
|
||||
represented by Entity_Id.
|
||||
(SPARK_Scope_Record): Referenced scope (e.g. subprogram) is now
|
||||
represented by Entity_Id; this information is not repeated as
|
||||
Scope_Entity.
|
||||
(Heap): Moved from lib-xref-spark_specific.adb, to reside next to
|
||||
Name_Of_Heap_Variable.
|
||||
* spark_xrefs.adb (dspark): Adapt debug routine to above changes in
|
||||
data types.
|
||||
* lib-xref-spark_specific.adb: Adapt routines for populating SPARK
|
||||
scope and xrefs tables to above changes in data types.
|
||||
|
||||
2017-11-08 Justin Squirek <squirek@adacore.com>
|
||||
|
||||
* sem_ch8.adb (Mark_Use_Clauses): Add condition to always mark the
|
||||
primitives of generic actuals.
|
||||
(Mark_Use_Type): Add recursive call to properly mark class-wide type's
|
||||
base type clauses as per ARM 8.4 (8.2/3).
|
||||
|
||||
2017-11-08 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_ch6.adb (Analyze_Generic_Subprobram_Body): Validate
|
||||
categorization dependency of the body, as is done for non-generic
|
||||
units.
|
||||
(New_Overloaded_Entity, Visible_Part_Type): Remove linear search
|
||||
through declarations (Simple optimization, no behavior change).
|
||||
|
||||
2017-11-08 Piotr Trojanek <trojanek@adacore.com>
|
||||
|
||||
* spark_xrefs.ads (SPARK_Xref_Record): Remove inessential components.
|
||||
|
@ -66,9 +66,6 @@ package body SPARK_Specific is
|
||||
-- Local Variables --
|
||||
---------------------
|
||||
|
||||
Heap : Entity_Id := Empty;
|
||||
-- A special entity which denotes the heap object
|
||||
|
||||
package Drefs is new Table.Table (
|
||||
Table_Component_Type => Xref_Entry,
|
||||
Table_Index_Type => Xref_Entry_Number,
|
||||
@ -164,14 +161,13 @@ package body SPARK_Specific is
|
||||
-- range.
|
||||
|
||||
SPARK_Scope_Table.Append
|
||||
((Scope_Name => new String'(Unique_Name (E)),
|
||||
((Scope_Id => E,
|
||||
File_Num => Dspec,
|
||||
Scope_Num => Scope_Id,
|
||||
Spec_File_Num => 0,
|
||||
Spec_Scope_Num => 0,
|
||||
From_Xref => 1,
|
||||
To_Xref => 0,
|
||||
Scope_Entity => E));
|
||||
To_Xref => 0));
|
||||
|
||||
Scope_Id := Scope_Id + 1;
|
||||
end Add_SPARK_Scope;
|
||||
@ -351,7 +347,7 @@ package body SPARK_Specific is
|
||||
|
||||
function Entity_Of_Scope (S : Scope_Index) return Entity_Id is
|
||||
begin
|
||||
return SPARK_Scope_Table.Table (S).Scope_Entity;
|
||||
return SPARK_Scope_Table.Table (S).Scope_Id;
|
||||
end Entity_Of_Scope;
|
||||
|
||||
-------------------
|
||||
@ -423,7 +419,7 @@ package body SPARK_Specific is
|
||||
function Is_Past_Scope_Entity return Boolean is
|
||||
begin
|
||||
for Index in SPARK_Scope_Table.First .. S - 1 loop
|
||||
if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
|
||||
if SPARK_Scope_Table.Table (Index).Scope_Id = E then
|
||||
return True;
|
||||
end if;
|
||||
end loop;
|
||||
@ -435,7 +431,7 @@ package body SPARK_Specific is
|
||||
|
||||
begin
|
||||
for Index in S .. SPARK_Scope_Table.Last loop
|
||||
if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
|
||||
if SPARK_Scope_Table.Table (Index).Scope_Id = E then
|
||||
return True;
|
||||
end if;
|
||||
end loop;
|
||||
@ -634,7 +630,7 @@ package body SPARK_Specific is
|
||||
declare
|
||||
S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
|
||||
begin
|
||||
Set_Scope_Num (S.Scope_Entity, S.Scope_Num);
|
||||
Set_Scope_Num (S.Scope_Id, S.Scope_Num);
|
||||
end;
|
||||
end loop;
|
||||
|
||||
@ -800,10 +796,10 @@ package body SPARK_Specific is
|
||||
end if;
|
||||
|
||||
SPARK_Xref_Table.Append (
|
||||
(Entity_Name => new String'(Unique_Name (Ref.Ent)),
|
||||
File_Num => Dependency_Num (Ref.Lun),
|
||||
Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
|
||||
Rtype => Typ));
|
||||
(Entity => Unique_Entity (Ref.Ent),
|
||||
File_Num => Dependency_Num (Ref.Lun),
|
||||
Scope_Num => Get_Scope_Num (Ref.Ref_Scope),
|
||||
Rtype => Typ));
|
||||
end;
|
||||
end loop;
|
||||
|
||||
@ -948,7 +944,7 @@ package body SPARK_Specific is
|
||||
declare
|
||||
Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
|
||||
begin
|
||||
Entity_Hash_Table.Set (Srec.Scope_Entity, S);
|
||||
Entity_Hash_Table.Set (Srec.Scope_Id, S);
|
||||
end;
|
||||
end loop;
|
||||
|
||||
@ -959,14 +955,14 @@ package body SPARK_Specific is
|
||||
Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
|
||||
|
||||
Spec_Entity : constant Entity_Id :=
|
||||
Unique_Entity (Srec.Scope_Entity);
|
||||
Unique_Entity (Srec.Scope_Id);
|
||||
Spec_Scope : constant Scope_Index :=
|
||||
Entity_Hash_Table.Get (Spec_Entity);
|
||||
|
||||
begin
|
||||
-- Generic spec may be missing in which case Spec_Scope is zero
|
||||
|
||||
if Spec_Entity /= Srec.Scope_Entity
|
||||
if Spec_Entity /= Srec.Scope_Id
|
||||
and then Spec_Scope /= 0
|
||||
then
|
||||
Srec.Spec_File_Num :=
|
||||
|
@ -1510,6 +1510,7 @@ package body Sem_Ch6 is
|
||||
|
||||
Process_End_Label (Handled_Statement_Sequence (N), 't', Current_Scope);
|
||||
Update_Use_Clause_Chain;
|
||||
Validate_Categorization_Dependency (N, Gen_Id);
|
||||
End_Scope;
|
||||
Check_Subprogram_Order (N);
|
||||
|
||||
@ -10118,7 +10119,6 @@ package body Sem_Ch6 is
|
||||
|
||||
function Visible_Part_Type (T : Entity_Id) return Boolean is
|
||||
P : constant Node_Id := Unit_Declaration_Node (Scope (T));
|
||||
N : Node_Id;
|
||||
|
||||
begin
|
||||
-- If the entity is a private type, then it must be declared in a
|
||||
@ -10126,34 +10126,19 @@ package body Sem_Ch6 is
|
||||
|
||||
if Ekind (T) in Private_Kind then
|
||||
return True;
|
||||
|
||||
elsif Is_Type (T) and then Has_Private_Declaration (T) then
|
||||
return True;
|
||||
|
||||
elsif Is_List_Member (Declaration_Node (T))
|
||||
and then List_Containing (Declaration_Node (T)) =
|
||||
Visible_Declarations (Specification (P))
|
||||
then
|
||||
return True;
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
|
||||
-- Otherwise, we traverse the visible part looking for its
|
||||
-- corresponding declaration. We cannot use the declaration
|
||||
-- node directly because in the private part the entity of a
|
||||
-- private type is the one in the full view, which does not
|
||||
-- indicate that it is the completion of something visible.
|
||||
|
||||
N := First (Visible_Declarations (Specification (P)));
|
||||
while Present (N) loop
|
||||
if Nkind (N) = N_Full_Type_Declaration
|
||||
and then Present (Defining_Identifier (N))
|
||||
and then T = Defining_Identifier (N)
|
||||
then
|
||||
return True;
|
||||
|
||||
elsif Nkind_In (N, N_Private_Type_Declaration,
|
||||
N_Private_Extension_Declaration)
|
||||
and then Present (Defining_Identifier (N))
|
||||
and then T = Full_View (Defining_Identifier (N))
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
Next (N);
|
||||
end loop;
|
||||
|
||||
return False;
|
||||
end Visible_Part_Type;
|
||||
|
||||
-- Start of processing for Check_For_Primitive_Subprogram
|
||||
|
@ -8320,6 +8320,7 @@ package body Sem_Ch8 is
|
||||
|
||||
procedure Mark_Use_Type (E : Entity_Id) is
|
||||
Curr : Node_Id;
|
||||
Base : Entity_Id;
|
||||
|
||||
begin
|
||||
-- Ignore void types and unresolved string literals and primitives
|
||||
@ -8331,12 +8332,22 @@ package body Sem_Ch8 is
|
||||
return;
|
||||
end if;
|
||||
|
||||
-- Primitives with class-wide operands might additionally render
|
||||
-- their base type's use_clauses effective - so do a recursive check
|
||||
-- here.
|
||||
|
||||
Base := Base_Type (Etype (E));
|
||||
|
||||
if Ekind (Base) = E_Class_Wide_Type then
|
||||
Mark_Use_Type (Base);
|
||||
end if;
|
||||
|
||||
-- The package containing the type or operator function being used
|
||||
-- may be in use as well, so mark any use_package_clauses for it as
|
||||
-- effective. There are also additional sanity checks performed here
|
||||
-- for ignoring previous errors.
|
||||
|
||||
Mark_Use_Package (Scope (Base_Type (Etype (E))));
|
||||
Mark_Use_Package (Scope (Base));
|
||||
|
||||
if Nkind (E) in N_Op
|
||||
and then Present (Entity (E))
|
||||
@ -8345,7 +8356,7 @@ package body Sem_Ch8 is
|
||||
Mark_Use_Package (Scope (Entity (E)));
|
||||
end if;
|
||||
|
||||
Curr := Current_Use_Clause (Base_Type (Etype (E)));
|
||||
Curr := Current_Use_Clause (Base);
|
||||
while Present (Curr)
|
||||
and then not Is_Effective_Use_Clause (Curr)
|
||||
loop
|
||||
@ -8397,7 +8408,9 @@ package body Sem_Ch8 is
|
||||
or else Ekind_In (Id, E_Generic_Function,
|
||||
E_Generic_Procedure))
|
||||
and then (Is_Potentially_Use_Visible (Id)
|
||||
or else Is_Intrinsic_Subprogram (Id))
|
||||
or else Is_Intrinsic_Subprogram (Id)
|
||||
or else (Ekind_In (Id, E_Function, E_Procedure)
|
||||
and then Is_Generic_Actual_Subprogram (Id)))
|
||||
then
|
||||
Mark_Parameters (Id);
|
||||
end if;
|
||||
|
@ -23,7 +23,8 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Output; use Output;
|
||||
with Output; use Output;
|
||||
with Sem_Util; use Sem_Util;
|
||||
|
||||
package body SPARK_Xrefs is
|
||||
|
||||
@ -81,17 +82,13 @@ package body SPARK_Xrefs is
|
||||
Write_Int (Int (ASR.Scope_Num));
|
||||
Write_Str (" Scope_Name = """);
|
||||
|
||||
if ASR.Scope_Name /= null then
|
||||
Write_Str (ASR.Scope_Name.all);
|
||||
end if;
|
||||
Write_Str (Unique_Name (ASR.Scope_Id));
|
||||
|
||||
Write_Char ('"');
|
||||
Write_Str (" From = ");
|
||||
Write_Int (Int (ASR.From_Xref));
|
||||
Write_Str (" To = ");
|
||||
Write_Int (Int (ASR.To_Xref));
|
||||
Write_Str (" Scope_Entity = ");
|
||||
Write_Int (Int (ASR.Scope_Entity));
|
||||
Write_Eol;
|
||||
end;
|
||||
end loop;
|
||||
@ -111,9 +108,7 @@ package body SPARK_Xrefs is
|
||||
Write_Int (Int (Index));
|
||||
Write_Str (". Entity_Name = """);
|
||||
|
||||
if AXR.Entity_Name /= null then
|
||||
Write_Str (AXR.Entity_Name.all);
|
||||
end if;
|
||||
Write_Str (Unique_Name (AXR.Entity));
|
||||
|
||||
Write_Char ('"');
|
||||
Write_Str (" File_Num = ");
|
||||
|
@ -66,7 +66,7 @@ package SPARK_Xrefs is
|
||||
-- until a proper value is determined.
|
||||
|
||||
type SPARK_Xref_Record is record
|
||||
Entity_Name : String_Ptr;
|
||||
Entity : Entity_Id;
|
||||
-- Pointer to entity name in ALI file
|
||||
|
||||
File_Num : Nat;
|
||||
@ -109,7 +109,7 @@ package SPARK_Xrefs is
|
||||
-- determined.
|
||||
|
||||
type SPARK_Scope_Record is record
|
||||
Scope_Name : String_Ptr;
|
||||
Scope_Id : Entity_Id;
|
||||
-- Pointer to scope name in ALI file
|
||||
|
||||
File_Num : Nat;
|
||||
@ -131,12 +131,6 @@ package SPARK_Xrefs is
|
||||
|
||||
To_Xref : Xref_Index;
|
||||
-- Ending index in Xref table for this scope
|
||||
|
||||
-- The following component is only used in-memory, not printed out in
|
||||
-- ALI file.
|
||||
|
||||
Scope_Entity : Entity_Id := Empty;
|
||||
-- Entity (subprogram or package) for the scope
|
||||
end record;
|
||||
|
||||
package SPARK_Scope_Table is new Table.Table (
|
||||
@ -193,6 +187,11 @@ package SPARK_Xrefs is
|
||||
-- Name of special variable used in effects to denote reads and writes
|
||||
-- through explicit dereference.
|
||||
|
||||
Heap : Entity_Id := Empty;
|
||||
-- A special entity which denotes the heap object; it should be considered
|
||||
-- constant, but needs to be variable, because it can only be initialized
|
||||
-- after the node tables are created.
|
||||
|
||||
-----------------
|
||||
-- Subprograms --
|
||||
-----------------
|
||||
|
Loading…
Reference in New Issue
Block a user