From ec98bb7dacad52c04092fee6de9cbf3b1d8c6b66 Mon Sep 17 00:00:00 2001 From: Pierre-Marie de Rodat Date: Wed, 8 Nov 2017 16:52:32 +0000 Subject: [PATCH] [multiple changes] 2017-11-08 Piotr Trojanek * 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 * exp_ch4.adb (Expand_N_Type_Conversion): Add test that the selector name is a discriminant in check for unconditional accessibility violation within instances. From-SVN: r254545 --- gcc/ada/ChangeLog | 16 ++++++++++++ gcc/ada/exp_ch4.adb | 1 + gcc/ada/lib-xref-spark_specific.adb | 51 ------------------------------------- gcc/ada/spark_xrefs.adb | 4 --- gcc/ada/spark_xrefs.ads | 8 ------ 5 files changed, 17 insertions(+), 63 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index beff132..be7a8bb 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,21 @@ 2017-11-08 Piotr Trojanek + * 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 + + * 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 + * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Remove special-case for constants (with variable input). (Is_Constant_Object_Without_Variable_Input): Remove. diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index 0ef9979..86d4883 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -11279,6 +11279,7 @@ package body Exp_Ch4 is 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 diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 37349fa..56bcf5d 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -164,8 +164,6 @@ package body SPARK_Specific is ((Entity => E, File_Num => Dspec, Scope_Num => Scope_Id, - Spec_File_Num => 0, - Spec_Scope_Num => 0, From_Xref => 1, To_Xref => 0)); @@ -836,55 +834,6 @@ package body SPARK_Specific is 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; diff --git a/gcc/ada/spark_xrefs.adb b/gcc/ada/spark_xrefs.adb index 552ed59..cea28a6 100644 --- a/gcc/ada/spark_xrefs.adb +++ b/gcc/ada/spark_xrefs.adb @@ -69,10 +69,6 @@ package body SPARK_Xrefs is 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)); diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index 4223003..a5d3373 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -110,14 +110,6 @@ package SPARK_Xrefs is 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 -- 2.7.4