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

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Apply
	scalar range checks.
	* sem_attr.adb (Resolve_Attribute): Do not set scalar range
	checks when resolving attribute Update.

2 files changed, 47 insertions, 28 deletions

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 207bb06..1f95aa4 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -251,6 +251,53 @@ package body Exp_SPARK is
             Analyze_And_Resolve (N, Standard_Boolean);
          end if;
 
+      elsif Attr_Id = Attribute_Update then
+         declare
+            Aggr : constant Node_Id := First (Expressions (N));
+            --  The aggregate expression
+
+            Assoc     : Node_Id;
+            Comp      : Node_Id;
+            Comp_Type : Node_Id;
+            Expr      : Node_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);
+
+                  if Is_Scalar_Type (Comp_Type) then
+                     Apply_Scalar_Range_Check (Expr, Comp_Type);
+                  end if;
+
+                  Next (Assoc);
+               end loop;
+
+            else pragma Assert (Is_Record_Type (Typ));
+
+               Assoc := First (Component_Associations (Aggr));
+               while Present (Assoc) loop
+                  Expr      := Expression (Assoc);
+                  Comp      := First (Choices (Assoc));
+                  Comp_Type := Etype (Entity (Comp));
+
+                  --  Use the type of the first component from the Choices
+                  --  list, as multiple components can only appear there if
+                  --  they have exactly the same type.
+
+                  if Is_Scalar_Type (Comp_Type) then
+                     Apply_Scalar_Range_Check (Expr, Comp_Type);
+                  end if;
+
+                  Next (Assoc);
+               end loop;
+            end if;
+         end;
       end if;
    end Expand_SPARK_N_Attribute_Reference;
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index d012418..4f11206 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -11995,26 +11995,6 @@ package body Sem_Attr is
                   Expr := Expression (Assoc);
                   Resolve (Expr, Component_Type (Typ));
 
-                  --  For scalar array components set Do_Range_Check when
-                  --  needed. Constraint checking on non-scalar components
-                  --  is done in Aggregate_Constraint_Checks, but only if
-                  --  full analysis is enabled. These flags are not set in
-                  --  the front-end in GnatProve mode.
-
-                  if Is_Scalar_Type (Component_Type (Typ))
-                    and then not Is_OK_Static_Expression (Expr)
-                    and then not Range_Checks_Suppressed (Component_Type (Typ))
-                  then
-                     if Is_Entity_Name (Expr)
-                       and then Etype (Expr) = Component_Type (Typ)
-                     then
-                        null;
-
-                     else
-                        Set_Do_Range_Check (Expr);
-                     end if;
-                  end if;
-
                   --  The choices in the association are static constants,
                   --  or static aggregates each of whose components belongs
                   --  to the proper index type. However, they must also
@@ -12072,14 +12052,6 @@ package body Sem_Attr is
                     and then not Error_Posted (Comp)
                   then
                      Resolve (Expr, Etype (Entity (Comp)));
-
-                     if Is_Scalar_Type (Etype (Entity (Comp)))
-                       and then not Is_OK_Static_Expression (Expr)
-                       and then not Range_Checks_Suppressed
-                                      (Etype (Entity (Comp)))
-                     then
-                        Set_Do_Range_Check (Expr);
-                     end if;
                   end if;
 
                   Next (Assoc);