[Ada] Remove SPARK-specific expansion of array aggregates

[gcc.git] / gcc / ada / exp_spark.adb

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 9bdd3d0aa201ba1613657b5078ef98fc73726e50..883a819ec7997b7f6da6af0ecffc2d3700c1410a 100644 (file)
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -36,6 +36,7 @@ with Nlists;   use Nlists;
 with Nmake;    use Nmake;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
+with Sem_Ch8;  use Sem_Ch8;
 with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
@@ -73,7 +74,7 @@ package body Exp_SPARK is
    --  Rewrite operator /= based on operator = when defined explicitly
 
    procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id);
-   --  Common expansion of attribute Update and delta_aggregate
+   --  Common expansion for attribute Update and delta aggregates
 
    ------------------
    -- Expand_SPARK --
@@ -168,7 +169,7 @@ package body Exp_SPARK is
 
       if Is_Array_Type (Typ) then
 
-         --  Multi-dimensional array
+         --  Multidimensional arrays
 
          if Present (Next_Index (First_Index (Typ))) then
             Assoc := First (Component_Associations (Aggr));
@@ -206,7 +207,7 @@ package body Exp_SPARK is
                Next (Assoc);
             end loop;
 
-         --  One-dimensional array
+         --  One-dimensional arrays
 
          else
             Assoc := First (Component_Associations (Aggr));
@@ -215,25 +216,45 @@ package body Exp_SPARK is
                Expr      := Expression (Assoc);
                Comp_Type := Component_Type (Typ);
 
+               --  Analyze expression of the iterated_component_association
+               --  with its index parameter in scope.
+
+               if Nkind (Assoc) = N_Iterated_Component_Association then
+                  Push_Scope (Scope (Defining_Identifier (Assoc)));
+                  Enter_Name (Defining_Identifier (Assoc));
+                  Analyze_And_Resolve (Expr, Comp_Type);
+               end if;
+
                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
+               --  Restore scope of the iterated_component_association
 
-                  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));
+               if Nkind (Assoc) = N_Iterated_Component_Association then
+                  End_Scope;
+               end if;
 
-                     --  Otherwise the index denotes a single element
+               Index     := First (Choice_List (Assoc));
+               Index_Typ := First_Index (Typ);
 
-                  else
+               while Present (Index) loop
+                  --  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) in N_Range | N_Subtype_Indication then
+                     null;
+
+                  --  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 pragma Assert (Nkind (Index) in N_Subexpr);
                      Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
                   end if;
 
@@ -246,13 +267,13 @@ package body Exp_SPARK is
 
       else pragma Assert (Is_Record_Type (Typ));
 
-         --  If the aggregate has multiple component choices, e.g.
+         --  If the aggregate has multiple component choices, e.g.:
          --
          --    X'Update (A | B | C => 123)
          --
-         --  then each component might be of a different type and might
-         --  or might not require a range check. We first rewrite
-         --  associations into single-component choices, e.g.:
+         --  then each component might be of a different type and might or
+         --  might not require a range check. We first rewrite associations
+         --  into single-component choices, e.g.:
          --
          --    X'Update (A => 123, B => 123, C => 123)
          --
@@ -400,13 +421,16 @@ package body Exp_SPARK is
          --  flag as the compiler assumes attributes always fit in this type.
          --  Since in SPARK_Mode we do not take Storage_Error into account, we
          --  cannot make this assumption and need to produce a check.
-         --  ??? It should be enough to add this check for attributes 'Length
-         --  and 'Range_Length when the type is as big as Long_Long_Integer.
+         --  ??? It should be enough to add this check for attributes
+         --  'Length, 'Range_Length and 'Pos when the type is as big
+         --  as Long_Long_Integer.
 
          declare
             Typ : Entity_Id;
          begin
-            if Attr_Id = Attribute_Range_Length then
+            if Attr_Id = Attribute_Range_Length
+              or else Attr_Id = Attribute_Pos
+            then
                Typ := Etype (Prefix (N));
 
             elsif Attr_Id = Attribute_Length then
@@ -421,6 +445,9 @@ package body Exp_SPARK is
             if Present (Typ)
               and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
             then
+               --  ??? This should rather be a range check, but this would
+               --  crash GNATprove which somehow recovers the proper kind
+               --  of check anyway.
                Set_Do_Overflow_Check (N);
             end if;
          end;