ada: Fix SPARK expansion of container aggregates
22 November 2023 at 15:43
ada: Fix SPARK expansion of container aggregates GNATprove supports container aggregates, except for indexed aggregates. It needs all expressions to have suitable target types and Do_Range_Check flags, which are added by the special expansion for GNATprove. There is no impact on code generation. gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Aggregate): New procedure for the special expansion. (Expand_SPARK): Call the new expansion procedure. * sem_util.adb (Is_Container_Aggregate): Implement missing test.