From 0edbf7fa1228faabed48586c7f036afe311c1c51 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Tue, 1 Sep 2020 10:55:34 +0200 Subject: [PATCH] [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 | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 814268a..f6ef865 100644 --- 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; -- 2.7.4