ada: Fix decoration of iterated component association for GNATprove
commitf34b31156d2868775c698db0ffa68bccadb685fb
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 3 May 2023 13:26:23 +0000 (3 15:26 +0200)
committerMarc Poulhiès <poulhies@adacore.com>
Tue, 13 Jun 2023 07:31:46 +0000 (13 09:31 +0200)
treed238818746ea24b89ee46335af1950cc211ad98f
parentd38366cbaedee32faba1664a8f529875f1128ae5
ada: Fix decoration of iterated component association for GNATprove

This patch is an alternative solution for a recent fix in analysis of
iterated component association.

To recap, if the iterated expression is an aggregate, we want to
propagate the component type downward with a call to Resolve_Aggr_Expr;
otherwise we want this expression to be only preanalysed (since the
association might need to be repeatedly evaluated), but also we need to
apply predicate and range checks to the expression itself (these are
required for GNATprove).

It turns out that Resolve_Aggr_Expr already knows how to deal with a
nested aggregate and also works for GNATprove, where it both preanalyzes
the expression and applies necessary checks.

In other words, expression of the iterated component association is now
resolved just like expression of an ordinary array aggregate.

gcc/ada/

* sem_aggr.adb (Resolve_Iterated_Component_Association): Simply resolve
the expression.
gcc/ada/sem_aggr.adb