This is a follow-up of a recent change, where setting of range checks
for 'Update on records was moved from Resolve_Attribute (where it was
shared between GNAT and GNATprove) to custom expansion for GNATprove
(and GNAT sets them as well in its own expansion). This patch does the
same for 'Update on arrays.
Just like the previous patch, this one also eliminates unnecessary
checks, for example, on a code like this:
type T is array (Positive range <>) of Boolean;
function P return Positive;
X : T := ...'Update (P => ...); -- no need for range check
we no longer emit a range check for the result of P being in T'Range,
while still generating them where required, e.g.:
function N return Natural;
X : T := ...'Update (N => ...); -- range check needed
Also, range checks for single-dimensional arrays were added in both
analysis and resolution, while for multi-dimensional arrays only in
resulution, which was inconsistent.
Note: attribute Update is soon to be replaced by delta_aggregate. This
cleanup is for reusing its implementation (if possible) or at least to
mirror it and not introduce more confusion.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Add scalar
range checks for 'Update on arrays just like for 'Update on
records.
* sem_attr.adb (Analyze_Array_Component_Update): Do not set
range checks for single-dimensional arrays.
(Resolve_Attribute): Do not set range checks for both single-
and multi- dimensional arrays.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
@@ -258,25 +258,91 @@ package body Exp_SPARK is
Assoc : Node_Id;
Comp : Node_Id;
- Comp_Type : Node_Id;
+ Comp_Type : Entity_Id;
Expr : Node_Id;
+ Index : Node_Id;
+ Index_Typ : Entity_Id;
begin
-- Apply scalar range checks on the updated components, if needed
if Is_Array_Type (Typ) then
- Assoc := First (Component_Associations (Aggr));
- while Present (Assoc) loop
- Expr := Expression (Assoc);
- Comp_Type := Component_Type (Typ);
+ -- Multi-dimensional array
- if Is_Scalar_Type (Comp_Type) then
- Apply_Scalar_Range_Check (Expr, Comp_Type);
- end if;
+ if Present (Next_Index (First_Index (Typ))) then
+ Assoc := First (Component_Associations (Aggr));
- Next (Assoc);
- end loop;
+ while Present (Assoc) loop
+ Expr := Expression (Assoc);
+ Comp_Type := Component_Type (Typ);
+
+ if Is_Scalar_Type (Comp_Type) then
+ Apply_Scalar_Range_Check (Expr, Comp_Type);
+ end if;
+
+ -- The current association contains a sequence of indexes
+ -- denoting an element of a multidimensional array:
+ --
+ -- (Index_1, ..., Index_N)
+
+ Expr := First (Choices (Assoc));
+
+ pragma Assert (Nkind (Aggr) = N_Aggregate);
+
+ while Present (Expr) loop
+ Index := First (Expressions (Expr));
+ Index_Typ := First_Index (Typ);
+
+ while Present (Index_Typ) loop
+ Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+ Next (Index);
+ Next_Index (Index_Typ);
+ end loop;
+
+ Next (Expr);
+ end loop;
+
+ Next (Assoc);
+ end loop;
+
+ -- One-dimensional array
+
+ else
+ Assoc := First (Component_Associations (Aggr));
+
+ while Present (Assoc) loop
+ Expr := Expression (Assoc);
+ Comp_Type := Component_Type (Typ);
+
+ if Is_Scalar_Type (Comp_Type) then
+ Apply_Scalar_Range_Check (Expr, Comp_Type);
+ end if;
+
+ Index := First (Choices (Assoc));
+ Index_Typ := First_Index (Typ);
+
+ while Present (Index) loop
+ -- The index denotes a range of elements
+
+ if Nkind (Index) = N_Range then
+ Apply_Scalar_Range_Check
+ (Low_Bound (Index), Etype (Index_Typ));
+ Apply_Scalar_Range_Check
+ (High_Bound (Index), Etype (Index_Typ));
+
+ -- Otherwise the index denotes a single element
+
+ else
+ Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+ end if;
+
+ Next (Index);
+ end loop;
+
+ Next (Assoc);
+ end loop;
+ end if;
else pragma Assert (Is_Record_Type (Typ));
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -6764,30 +6764,10 @@ package body Sem_Attr is
Analyze_And_Resolve (Low, Etype (Index_Typ));
Analyze_And_Resolve (High, Etype (Index_Typ));
- -- Add a range check to ensure that the bounds of the
- -- range are within the index type when this cannot be
- -- determined statically.
-
- if not Is_OK_Static_Expression (Low) then
- Set_Do_Range_Check (Low);
- end if;
-
- if not Is_OK_Static_Expression (High) then
- Set_Do_Range_Check (High);
- end if;
-
-- Otherwise the index denotes a single element
else
Analyze_And_Resolve (Index, Etype (Index_Typ));
-
- -- Add a range check to ensure that the index is within
- -- the index type when it is not possible to determine
- -- this statically.
-
- if not Is_OK_Static_Expression (Index) then
- Set_Do_Range_Check (Index);
- end if;
end if;
Next (Index);
@@ -12019,14 +11999,12 @@ package body Sem_Attr is
if Nkind (C) /= N_Aggregate then
Analyze_And_Resolve (C, Etype (Indx));
- Apply_Constraint_Check (C, Etype (Indx));
Check_Non_Static_Context (C);
else
C_E := First (Expressions (C));
while Present (C_E) loop
Analyze_And_Resolve (C_E, Etype (Indx));
- Apply_Constraint_Check (C_E, Etype (Indx));
Check_Non_Static_Context (C_E);
Next (C_E);
