aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/ChangeLog10
-rw-r--r--gcc/ada/lib-xref-spark_specific.adb9
-rw-r--r--gcc/ada/sem_ch4.adb2
-rw-r--r--gcc/ada/spark_xrefs.ads5
4 files changed, 16 insertions, 10 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index be7a8bb..51aa930 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,15 @@
2017-11-08 Piotr Trojanek <trojanek@adacore.com>
+ * spark_xrefs.ads (SPARK_Scope_Record): Remove File_Num component.
+ * lib-xref-spark_specific.adb (Add_SPARK_Scope): Skip initialization of
+ removed component.
+
+2017-11-08 Gary Dismukes <dismukes@adacore.com>
+
+ * sem_ch4.adb: Minor typo fix.
+
+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.
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 56bcf5d..df0c5bb 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -161,11 +161,10 @@ package body SPARK_Specific is
-- range.
SPARK_Scope_Table.Append
- ((Entity => E,
- File_Num => Dspec,
- Scope_Num => Scope_Id,
- From_Xref => 1,
- To_Xref => 0));
+ ((Entity => E,
+ Scope_Num => Scope_Id,
+ From_Xref => 1,
+ To_Xref => 0));
Scope_Id := Scope_Id + 1;
end Add_SPARK_Scope;
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index cfc4db7..2ef5747 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -418,7 +418,7 @@ package body Sem_Ch4 is
-- Delta aggregates have a base component that determines the type of the
-- enclosing aggregate so its type can be ascertained earlier. This also
-- allows delta aggregates to appear in the context of a record type with
- -- a private extension, as per the latest update of AI2-0127.
+ -- a private extension, as per the latest update of AI12-0127.
procedure Analyze_Aggregate (N : Node_Id) is
begin
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index a5d3373..df1d8e89 100644
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -104,11 +104,8 @@ package SPARK_Xrefs is
Entity : Entity_Id;
-- Entity that is represented by the scope
- File_Num : Nat;
- -- Set to the file dependency number for the scope
-
Scope_Num : Pos;
- -- Set to the scope number for the scope
+ -- Set to the scope number within the enclosing unit
From_Xref : Xref_Index;
-- Starting index in Xref table for this scope