diff options
author | Arnaud Charlet <charlet@adacore.com> | 2016-06-22 09:55:42 +0000 |
---|---|---|
committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-06-22 11:55:42 +0200 |
commit | b48a45e33c1022f9b60437131e3d6e640345cc54 (patch) | |
tree | ef830972e9d2e1878bfd955a0b9be903d0abe9d5 /gcc | |
parent | 22da877084b5911b10f33195eea7487b1aeedb86 (diff) | |
download | gcc-b48a45e33c1022f9b60437131e3d6e640345cc54.zip gcc-b48a45e33c1022f9b60437131e3d6e640345cc54.tar.gz gcc-b48a45e33c1022f9b60437131e3d6e640345cc54.tar.bz2 |
lib-xref-spark_specific.adb (Generate_Dereference): Assignment to not commented local variables replaced with direct uses of their...
2016-06-22 Arnaud Charlet <charlet@adacore.com>
* lib-xref-spark_specific.adb (Generate_Dereference): Assignment to not
commented local variables replaced with direct uses of their values.
From-SVN: r237685
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
-rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 48 |
2 files changed, 43 insertions, 10 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index a8b4fcb..dd2f679 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2016-06-22 Arnaud Charlet <charlet@adacore.com> + + * lib-xref-spark_specific.adb (Generate_Dereference): Assignment to not + commented local variables replaced with direct uses of their values. + 2016-06-22 Hristian Kirtchev <kirtchev@adacore.com> * exp_ch7.adb (Add_Invariant): Replace the diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 8bc6603..ce4ded8 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -929,7 +929,40 @@ package body SPARK_Specific is and then Cunit_Entity (Sdep_Table (D1)) = Cunit_Entity (Sdep_Table (D1 + 1)) then - D2 := D1 + 1; + declare + Cunit1 : Node_Id renames Cunit (Sdep_Table (D1)); + Cunit2 : Node_Id renames Cunit (Sdep_Table (D1 + 1)); + begin + -- Both Cunit point to compilation unit nodes + pragma Assert (Nkind (Cunit1) = N_Compilation_Unit + and then + Nkind (Cunit2) = N_Compilation_Unit); + + -- Do not depend on the sorting order, which is based on + -- Unit_Name and for library-level instances of nested + -- generic-packages they are equal. + + -- If declaration comes before the body then just set D2 + if Nkind (Unit (Cunit1)) = N_Package_Declaration + and then + Nkind (Unit (Cunit2)) = N_Package_Body + then + D2 := D1 + 1; + + -- If body comes before declaration then set D2 and adjust D1 + + elsif Nkind (Unit (Cunit1)) = N_Package_Body + and then + Nkind (Unit (Cunit2)) = N_Package_Declaration + then + D2 := D1; + D1 := D1 + 1; + + else + + raise Program_Error; + end if; + end; else D2 := D1; end if; @@ -945,7 +978,7 @@ package body SPARK_Specific is Dspec => D2); end if; - D1 := D2 + 1; + D1 := Pos'Max (D1, D2) + 1; end loop; -- Fill in the spec information when relevant @@ -1164,9 +1197,7 @@ package body SPARK_Specific is -- Local variables - Loc : constant Source_Ptr := Sloc (N); - Index : Nat; - Ref_Scope : Entity_Id; + Loc : constant Source_Ptr := Sloc (N); -- Start of processing for Generate_Dereference @@ -1174,10 +1205,9 @@ package body SPARK_Specific is if Loc > No_Location then Drefs.Increment_Last; - Index := Drefs.Last; declare - Deref_Entry : Xref_Entry renames Drefs.Table (Index); + Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last); Deref : Xref_Key renames Deref_Entry.Key; begin @@ -1185,8 +1215,6 @@ package body SPARK_Specific is Create_Heap; end if; - Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N); - Deref.Ent := Heap; Deref.Loc := Loc; Deref.Typ := Typ; @@ -1199,7 +1227,7 @@ package body SPARK_Specific is Deref.Eun := Main_Unit; Deref.Lun := Get_Top_Level_Code_Unit (Loc); - Deref.Ref_Scope := Ref_Scope; + Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N); Deref.Ent_Scope := Cunit_Entity (Main_Unit); Deref_Entry.Def := No_Location; |