2017-11-08 Piotr Trojanek <trojanek@adacore.com>
+ * spark_xrefs.ads (SPARK_Scope_Record): Remove Spec_File_Num and
+ Spec_Scope_Num components.
+ * spark_xrefs.adb (dspark): Skip pretty-printing to removed components.
+ * lib-xref-spark_specific.adb (Add_SPARK_Scope): Skip initialization of
+ removed components.
+ (Collect_SPARK_Xrefs): Skip setting proper values of removed
+ components.
+
+2017-11-08 Gary Dismukes <dismukes@adacore.com>
+
+ * exp_ch4.adb (Expand_N_Type_Conversion): Add test that the selector
+ name is a discriminant in check for unconditional accessibility
+ violation within instances.
+
+2017-11-08 Piotr Trojanek <trojanek@adacore.com>
+
* lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case
for constants (with variable input).
(Is_Constant_Object_Without_Variable_Input): Remove.
elsif In_Instance_Body
and then Ekind (Operand_Type) = E_Anonymous_Access_Type
and then Nkind (Operand) = N_Selected_Component
+ and then Ekind (Entity (Selector_Name (Operand))) = E_Discriminant
and then Object_Access_Level (Operand) >
Type_Access_Level (Target_Type)
then
((Entity => E,
File_Num => Dspec,
Scope_Num => Scope_Id,
- Spec_File_Num => 0,
- Spec_Scope_Num => 0,
From_Xref => 1,
To_Xref => 0));
Sdep := Sdep_Next;
end loop;
- -- Fill in the spec information when relevant
-
- declare
- package Entity_Hash_Table is new
- GNAT.HTable.Simple_HTable
- (Header_Num => Entity_Hashed_Range,
- Element => Scope_Index,
- No_Element => 0,
- Key => Entity_Id,
- Hash => Entity_Hash,
- Equal => "=");
-
- begin
- -- Fill in the hash-table
-
- for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
- declare
- Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
- begin
- Entity_Hash_Table.Set (Srec.Entity, S);
- end;
- end loop;
-
- -- Use the hash-table to locate spec entities
-
- for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop
- declare
- Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S);
-
- Spec_Entity : constant Entity_Id :=
- Unique_Entity (Srec.Entity);
- 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.Entity
- and then Spec_Scope /= 0
- then
- Srec.Spec_File_Num :=
- SPARK_Scope_Table.Table (Spec_Scope).File_Num;
- Srec.Spec_Scope_Num :=
- SPARK_Scope_Table.Table (Spec_Scope).Scope_Num;
- end if;
- end;
- end loop;
- end;
-
-- Generate SPARK cross-reference information
Add_SPARK_Xrefs;
begin
Write_Str (" ");
Write_Int (Int (Index));
- Write_Str (". File_Num = ");
- Write_Int (Int (ASR.File_Num));
- Write_Str (" Scope_Num = ");
- Write_Int (Int (ASR.Scope_Num));
Write_Str (" Scope_Name = """);
Write_Str (Unique_Name (ASR.Entity));
Scope_Num : Pos;
-- Set to the scope number for the scope
- Spec_File_Num : Nat;
- -- Set to the file dependency number for the scope corresponding to the
- -- spec of the current scope entity, if different, or else 0.
-
- Spec_Scope_Num : Nat;
- -- Set to the scope number for the scope corresponding to the spec of
- -- the current scope entity, if different, or else 0.
-
From_Xref : Xref_Index;
-- Starting index in Xref table for this scope