[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.

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 814268a5708b892aef908f1e8d53ac0e566c4d96..f6ef86529862073a2d861f7611ebf83a5331268f 100644 (file)
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -248,17 +248,22 @@ package body Exp_SPARK is
                Index_Typ := First_Index (Typ);
 
                while Present (Index) loop
-                  --  The index denotes a range of elements
+                  --  If the index denotes a range of elements or a constrained
+                  --  subtype indication, then their low and high bounds
+                  --  already have range checks applied.
 
-                  if Nkind (Index) = N_Range then
-                     Apply_Scalar_Range_Check
-                       (Low_Bound  (Index), Base_Type (Etype (Index_Typ)));
-                     Apply_Scalar_Range_Check
-                       (High_Bound (Index), Base_Type (Etype (Index_Typ)));
+                  if Nkind (Index) in N_Range | N_Subtype_Indication then
+                     null;
 
-                  --  Otherwise the index denotes a single element
+                  --  Otherwise the index denotes a single expression where
+                  --  range checks need to be applied or a subtype name
+                  --  (without range constraints) where applying checks is
+                  --  harmless.
+                  --
+                  --  In delta_aggregate and Update attribute on array the
+                  --  others_choice is not allowed.
 
-                  else
+                  else pragma Assert (Nkind (Index) in N_Subexpr);
                      Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
                   end if;