]> git.ipfire.org Git - thirdparty/gcc.git/commit
[Ada] Adapt GNATprove expansion for slices with access prefix
authorpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Tue, 20 Aug 2019 09:50:29 +0000 (09:50 +0000)
committerpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Tue, 20 Aug 2019 09:50:29 +0000 (09:50 +0000)
commit832af6f73f83cb8ecbf80b8425f654b92d7bb173
treeccc47ba32b4f7cd5d4f8cdf4adb8e41f2807ecd5
parent952fd477845169f91c7c70cbf241743cb2b0e199
[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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@274740 138bc75d-0d04-0410-961f-82ee72b054a4
gcc/ada/ChangeLog
gcc/ada/exp_spark.adb