+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.
-- 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,
-- 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;
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;
-------------------
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;
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;
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;
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;
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;
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 :=
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);
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
if Ekind (T) in Private_Kind then
return True;
- 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;
+ elsif Is_Type (T) and then Has_Private_Declaration (T) then
+ return True;
- Next (N);
- end loop;
+ elsif Is_List_Member (Declaration_Node (T))
+ and then List_Containing (Declaration_Node (T)) =
+ Visible_Declarations (Specification (P))
+ then
+ return True;
- return False;
+ else
+ return False;
+ end if;
end Visible_Part_Type;
-- Start of processing for Check_For_Primitive_Subprogram
procedure Mark_Use_Type (E : Entity_Id) is
Curr : Node_Id;
+ Base : Entity_Id;
begin
-- Ignore void types and unresolved string literals and primitives
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))
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
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;
-- --
------------------------------------------------------------------------------
-with Output; use Output;
+with Output; use Output;
+with Sem_Util; use Sem_Util;
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;
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 = ");
-- 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;
-- 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;
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 (
-- 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 --
-----------------