[Ada] Fix crash in SPARK on array delta_aggregate with subtype_indication
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 1 Sep 2020 08:55:34 +0000 (10:55 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Fri, 23 Oct 2020 08:24:57 +0000 (04:24 -0400)
commit0edbf7fa1228faabed48586c7f036afe311c1c51
tree40cacc9df23f7fe4c3912071238adaf1f6ee782b
parentf2668d9058fd2f6299d2f4b3d5fff590d819361f
[Ada] Fix crash in SPARK on array delta_aggregate with subtype_indication

gcc/ada/

* exp_spark.adb (Expand_SPARK_Delta_Or_Update): Handle
subtype_indication; do not apply range checks for ranges; add
comment saying that others_choices is not allowed.
gcc/ada/exp_spark.adb