projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fb00cc7) | patch
[Ada] Fix GNATprove support for iterated_component_associations
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 23 Sep 2020 14:38:10 +0000 (16:38 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Tue, 27 Oct 2020 09:19:33 +0000 (05:19 -0400)
commita026b59e7711ffa23137a1255f1acc5c73589412
treeb5b948f5f9f12583a34c33431655d4e3c46d6fd1tree
parentfb00cc7032bf1129373edd2bd99cf02fe03fd1d8commit | diff
[Ada] Fix GNATprove support for iterated_component_associations

gcc/ada/

* exp_spark.adb (Expand_SPARK_Array_Aggregate): Dedicated
routine for array aggregates; mostly reuses existing code, but
calls itself recursively for multi-dimensional array aggregates.
(Expand_SPARK_N_Aggregate): Call Expand_SPARK_Array_Aggregate to
do the actual expansion, starting from the first index of the
array type.
gcc/ada/exp_spark.adb diff | blob | history