[Ada] Set range checks for for 'Update on arrays in GNATprove expansion

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.

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
+               --  Multi-dimensional array
-                  Expr      := Expression (Assoc);
-                  Comp_Type := Component_Type (Typ);
 
-                  if Is_Scalar_Type (Comp_Type) then
+               if Present (Next_Index (First_Index (Typ))) then
-                     Apply_Scalar_Range_Check (Expr, Comp_Type);
+                  Assoc := First (Component_Associations (Aggr));
-                  end if;
 
-                  Next (Assoc);
+                  while Present (Assoc) loop
-               end 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));
 

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);