diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-01-19 14:02:30 +0100 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-01-19 14:02:30 +0100 |
| commit | 374c09e8b0560f150266deb324004e482f4c424e (patch) | |
| tree | 08e26e517839d3144e06cfbfac0cb3d8b665465b /gcc/ada | |
| parent | f67f94b8e2a276b70c51871e8ca0b85a98190b0a (diff) | |
| download | gcc-374c09e8b0560f150266deb324004e482f4c424e.zip gcc-374c09e8b0560f150266deb324004e482f4c424e.tar.gz gcc-374c09e8b0560f150266deb324004e482f4c424e.tar.bz2 | |
[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
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 9 | ||||
| -rw-r--r-- | gcc/ada/exp_ch7.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 2 |
3 files changed, 20 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 375f02b..ba2c120 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 c9b4870..0c21808 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 14948d5..dfbe4dd 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; |