From: Arnaud Charlet <charlet@gcc.gnu.org>
Date: Thu, 19 Jan 2017 13:02:30 +0000 (+0100)
Subject: [multiple changes]
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=374c09e8b0560f150266deb324004e482f4c424e;p=gcc.git

[multiple changes]

2017-01-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* lib-xref-spark_specific.adb: Minor reformatting.
	* exp_ch7.adb (Add_Parent_Invariants): Do not process array types.

2017-01-19  Tristan Gingold  <gingold@adacore.com>

	* fe.h (Constant_Value): Export.

From-SVN: r244628
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 375f02bf02b..ba2c1207e28 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,12 @@
+2017-01-19  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* lib-xref-spark_specific.adb: Minor reformatting.
+	* exp_ch7.adb (Add_Parent_Invariants): Do not process array types.
+
+2017-01-19  Tristan Gingold  <gingold@adacore.com>
+
+	* fe.h (Constant_Value): Export.
+
 2017-01-19  Javier Miranda  <miranda@adacore.com>
 
 	* exp_aggr.adb (Pass_Aggregate_To_Back_End): Renamed as
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index c9b487083d6..0c2180847ba 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -3745,6 +3745,16 @@ package body Exp_Ch7 is
          --  The partial view of Par_Typ
 
       begin
+         --  Do not process array types because they cannot have true parent
+         --  types. This also prevents the generation of a duplicate invariant
+         --  check when the input type is an array base type because its Etype
+         --  denotes the first subtype, both of which share the same component
+         --  type.
+
+         if Is_Array_Type (T) then
+            return;
+         end if;
+
          --  Climb the parent type chain
 
          Curr_Typ := T;
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 14948d50579..dfbe4dd3419 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -703,7 +703,7 @@ package body SPARK_Specific is
 
       declare
          Drefs_Table : Drefs.Table_Type
-           renames Drefs.Table (Drefs.First .. Drefs.Last);
+                         renames Drefs.Table (Drefs.First .. Drefs.Last);
       begin
          Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table));
          Nrefs := Nrefs + Drefs_Table'Length;