Expansion of array delta_aggregate in GNATprove mode needs handled
ranges and expressions (including type identifiers), but not
subtype_indications (e.g. "A with delta Integer range 1 .. 10 => 0").
Also, call Apply_Scalar_Range_Check didn't seem necessary for ranges and
likewise it makes no difference for subtype_indication, so remove it.
This patch only affects GNATprove; compilation is unaffected.
Tested on x86_64-pc-linux-gnu, committed on trunk
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
--- 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;
