aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorArnaud Charlet <charlet@adacore.com>2016-06-22 09:55:42 +0000
committerArnaud Charlet <charlet@adacore.com>2016-06-22 09:55:42 +0000
commit961a451b8bf03f7d01cfd85c1a95349ceab15a06 (patch)
treeef830972e9d2e1878bfd955a0b9be903d0abe9d5
parentcd136627be049a348774905e636fc78c6dc7bc2c (diff)
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. git-svn-id: https://gcc.gnu.org/svn/gcc/trunk@237685 138bc75d-0d04-0410-961f-82ee72b054a4
-rw-r--r--gcc/ada/ChangeLog5
-rw-r--r--gcc/ada/lib-xref-spark_specific.adb48
2 files changed, 43 insertions, 10 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index a8b4fcb2353..dd2f6796335 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 8bc660309ac..ce4ded82d50 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;