[Ada] Adapt GNATprove expansion for slices with access prefix
authorYannick Moy <moy@adacore.com>
Tue, 20 Aug 2019 09:50:29 +0000 (09:50 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 20 Aug 2019 09:50:29 +0000 (09:50 +0000)
commitdd6e65c618576b52c46bc6fbf28ac6b91bce2951
treeccc47ba32b4f7cd5d4f8cdf4adb8e41f2807ecd5
parentd4e4e88a4c1b13bc480603ad96672ce079e32ffb
[Ada] Adapt GNATprove expansion for slices with access prefix

The special expansion done in GNATprove mode should be adapted to slices
where the prefix has access type, like indexed expressions.

There is no impact on compilation.

2019-08-20  Yannick Moy  <moy@adacore.com>

gcc/ada/

* exp_spark.adb (Expand_SPARK_N_Slice_Or_Indexed_Component):
Renaming of function to apply to slices as well.
(Expand_SPARK): Expand prefix of slices of access type.

From-SVN: r274740
gcc/ada/ChangeLog
gcc/ada/exp_spark.adb