[multiple changes]

2015-10-20  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch6.adb (Expand_Call): Check for a call to a function
	declared in a Dimension I/O package, to handle the new Image
	function.

2015-10-20  Eric Botcazou  <ebotcazou@adacore.com>

	* inline.ads: Minor comment fixes.

2015-10-20  Bob Duff  <duff@adacore.com>

	* a-comutr.ads (Tree_Node_Access): Add No_Strict_Aliasing, because
	we're doing unchecked conversions with this pointer.

2015-10-20  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch9.adb (Next_Protected_Operation): An expression function
	used as a completion can be the next protected operation in a
	protected body.

2015-10-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Is_OK_Volatile_Context): Add a guard when checking a
	possible call to an instance of Ada.Unchecked_Conversion to avoid
	testing protected function calls. Allow references to protected objects
	in prefixed protected calls.
	(Is_Protected_Operation_Call): New routine.

2015-10-20  Yannick Moy  <moy@adacore.com>

	* exp_ch5.adb, exp_ch5.ads (Expand_Iterator_Loop_Over_Array): Make
	query public. Remove code handling with iterator loop over array
	of the 'in' form, which is not allowed in Ada.	* exp_spark.adb
	(Expand_SPARK): Expand loop statements that take the form of an
	iterator over an array.
	* sem_ch5.adb (Analyze_Loop_Statement): Do not analyze loop statements
	that take the form of an iterator over an array, so that the rewritten
	form gets analyzed instead.
	* sem_util.adb, sem_util.ads (Is_Iterator_Over_Array): New query
	to recognize iterators over arrays.

2015-10-20  Arnaud Charlet  <charlet@adacore.com>

	* s-excdeb.ads, s-excdeb.adb (Debug_Raise_Exception): Add
	parameter Message.
	* a-except.adb (Raise_Current_Excep): Update call to
	Debug_Raise_Exception.
	* a-except-2005.adb (Complete_Occurrence): Ditto.
	* sem_ch12.adb: Whitespace fix.

From-SVN: r229056

17 files changed, 217 insertions, 64 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 54ec2ef..4022dfc 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,54 @@
+2015-10-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch6.adb (Expand_Call): Check for a call to a function
+	declared in a Dimension I/O package, to handle the new Image
+	function.
+
+2015-10-20  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* inline.ads: Minor comment fixes.
+
+2015-10-20  Bob Duff  <duff@adacore.com>
+
+	* a-comutr.ads (Tree_Node_Access): Add No_Strict_Aliasing, because
+	we're doing unchecked conversions with this pointer.
+
+2015-10-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch9.adb (Next_Protected_Operation): An expression function
+	used as a completion can be the next protected operation in a
+	protected body.
+
+2015-10-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_res.adb (Is_OK_Volatile_Context): Add a guard when checking a
+	possible call to an instance of Ada.Unchecked_Conversion to avoid
+	testing protected function calls. Allow references to protected objects
+	in prefixed protected calls.
+	(Is_Protected_Operation_Call): New routine.
+
+2015-10-20  Yannick Moy  <moy@adacore.com>
+
+	* exp_ch5.adb, exp_ch5.ads (Expand_Iterator_Loop_Over_Array): Make
+	query public. Remove code handling with iterator loop over array
+	of the 'in' form, which is not allowed in Ada.	* exp_spark.adb
+	(Expand_SPARK): Expand loop statements that take the form of an
+	iterator over an array.
+	* sem_ch5.adb (Analyze_Loop_Statement): Do not analyze loop statements
+	that take the form of an iterator over an array, so that the rewritten
+	form gets analyzed instead.
+	* sem_util.adb, sem_util.ads (Is_Iterator_Over_Array): New query
+	to recognize iterators over arrays.
+
+2015-10-20  Arnaud Charlet  <charlet@adacore.com>
+
+	* s-excdeb.ads, s-excdeb.adb (Debug_Raise_Exception): Add
+	parameter Message.
+	* a-except.adb (Raise_Current_Excep): Update call to
+	Debug_Raise_Exception.
+	* a-except-2005.adb (Complete_Occurrence): Ditto.
+	* sem_ch12.adb: Whitespace fix.
+
 2015-10-20  Yannick Moy  <moy@adacore.com>
 
 	* sem_warn.adb (Is_OK_Fully_Initialized): Consider types with DIC as
diff --git a/gcc/ada/a-comutr.ads b/gcc/ada/a-comutr.ads
index 25fadf1..81a89e9 100644
--- a/gcc/ada/a-comutr.ads
+++ b/gcc/ada/a-comutr.ads
@@ -342,6 +342,9 @@ private
    type Tree_Node_Type;
    type Tree_Node_Access is access all Tree_Node_Type;
    pragma Convention (C, Tree_Node_Access);
+   pragma No_Strict_Aliasing (Tree_Node_Access);
+   --  The above-mentioned Unchecked_Conversion is a violation of the normal
+   --  aliasing rules.
 
    type Children_Type is record
       First : Tree_Node_Access;
diff --git a/gcc/ada/a-except-2005.adb b/gcc/ada/a-except-2005.adb
index 43a556d4..a346494 100644
--- a/gcc/ada/a-except-2005.adb
+++ b/gcc/ada/a-except-2005.adb
@@ -922,7 +922,9 @@ package body Ada.Exceptions is
       Call_Chain (X);
 
       --  Notify the debugger
-      Debug_Raise_Exception (E => SSL.Exception_Data_Ptr (X.Id));
+      Debug_Raise_Exception
+        (E       => SSL.Exception_Data_Ptr (X.Id),
+         Message => X.Msg (1 .. X.Msg_Length));
    end Complete_Occurrence;
 
    ---------------------------------------
diff --git a/gcc/ada/a-except.adb b/gcc/ada/a-except.adb
index a228a83..3b9caea 100644
--- a/gcc/ada/a-except.adb
+++ b/gcc/ada/a-except.adb
@@ -949,7 +949,7 @@ package body Ada.Exceptions is
       --  pragma Volatile is peculiar.
 
    begin
-      Debug_Raise_Exception (E => SSL.Exception_Data_Ptr (E));
+      Debug_Raise_Exception (E => SSL.Exception_Data_Ptr (E), Message => "");
       Process_Raise_Exception (E);
    end Raise_Current_Excep;
 
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index 4c66ce4..5b3dd75 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -130,9 +130,6 @@ package body Exp_Ch5 is
    --  Expand loop over arrays and containers that uses the form "for X of C"
    --  with an optional subtype mark, or "for Y in C".
 
-   procedure Expand_Iterator_Loop_Over_Array (N : Node_Id);
-   --  Expand loop over arrays that uses the form "for X of C"
-
    procedure Expand_Iterator_Loop_Over_Container
      (N             : Node_Id;
       Isc           : Node_Id;
@@ -3350,44 +3347,36 @@ package body Exp_Ch5 is
    begin
       --  for Element of Array loop
 
-      --  This case requires an internally generated cursor to iterate over
-      --  the array.
-
-      if Of_Present (I_Spec) then
-         Iterator := Make_Temporary (Loc, 'C');
-
-         --  Generate:
-         --    Element : Component_Type renames Array (Iterator);
-         --    Iterator is the index value, or a list of index values
-         --    in the case of a multidimensional array.
-
-         Ind_Comp :=
-           Make_Indexed_Component (Loc,
-             Prefix      => Relocate_Node (Array_Node),
-             Expressions => New_List (New_Occurrence_Of (Iterator, Loc)));
+      --  It requires an internally generated cursor to iterate over the array
 
-         Prepend_To (Stats,
-           Make_Object_Renaming_Declaration (Loc,
-             Defining_Identifier => Id,
-             Subtype_Mark        =>
-               New_Occurrence_Of (Component_Type (Array_Typ), Loc),
-             Name                => Ind_Comp));
+      pragma Assert (Of_Present (I_Spec));
 
-         --  Mark the loop variable as needing debug info, so that expansion
-         --  of the renaming will result in Materialize_Entity getting set via
-         --  Debug_Renaming_Declaration. (This setting is needed here because
-         --  the setting in Freeze_Entity comes after the expansion, which is
-         --  too late. ???)
+      Iterator := Make_Temporary (Loc, 'C');
 
-         Set_Debug_Info_Needed (Id);
-
-      --  for Index in Array loop
+      --  Generate:
+      --    Element : Component_Type renames Array (Iterator);
+      --    Iterator is the index value, or a list of index values
+      --    in the case of a multidimensional array.
 
-      --  This case utilizes the already given iterator name
+      Ind_Comp :=
+        Make_Indexed_Component (Loc,
+          Prefix      => Relocate_Node (Array_Node),
+          Expressions => New_List (New_Occurrence_Of (Iterator, Loc)));
 
-      else
-         Iterator := Id;
-      end if;
+      Prepend_To (Stats,
+        Make_Object_Renaming_Declaration (Loc,
+          Defining_Identifier => Id,
+          Subtype_Mark        =>
+            New_Occurrence_Of (Component_Type (Array_Typ), Loc),
+          Name                => Ind_Comp));
+
+      --  Mark the loop variable as needing debug info, so that expansion
+      --  of the renaming will result in Materialize_Entity getting set via
+      --  Debug_Renaming_Declaration. (This setting is needed here because
+      --  the setting in Freeze_Entity comes after the expansion, which is
+      --  too late. ???)
+
+      Set_Debug_Info_Needed (Id);
 
       --  Generate:
 
diff --git a/gcc/ada/exp_ch5.ads b/gcc/ada/exp_ch5.ads
index 7967164..9d85975 100644
--- a/gcc/ada/exp_ch5.ads
+++ b/gcc/ada/exp_ch5.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -35,4 +35,8 @@ package Exp_Ch5 is
    procedure Expand_N_Goto_Statement            (N : Node_Id);
    procedure Expand_N_If_Statement              (N : Node_Id);
    procedure Expand_N_Loop_Statement            (N : Node_Id);
+
+   procedure Expand_Iterator_Loop_Over_Array (N : Node_Id);
+   --  Expand loop over arrays that uses the form "for X of C"
+
 end Exp_Ch5;
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index e7d1dce..be7f729 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -2376,11 +2376,13 @@ package body Exp_Ch6 is
    --  Start of processing for Expand_Call
 
    begin
-      --  Expand the procedure call if the first actual has a dimension and if
-      --  the procedure is Put (Ada 2012).
+      --  Expand the function or procedure call if the first actual has a
+      --  declared dimension aspect, and the subprogram is declared in one
+      --  of the dimension I/O packages.
 
       if Ada_Version >= Ada_2012
-        and then Nkind (Call_Node) = N_Procedure_Call_Statement
+        and then
+           Nkind_In (Call_Node, N_Procedure_Call_Statement, N_Function_Call)
         and then Present (Parameter_Associations (Call_Node))
       then
          Expand_Put_Call_With_Symbol (Call_Node);
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 0cb3743..f027635 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -14295,9 +14295,14 @@ package body Exp_Ch9 is
       Next_Op : Node_Id;
 
    begin
+      --  Check whether there is a subsequent body for a protected operation
+      --  in the current protected body. In Ada2012 that includes expression
+      --  functions that are completions.
+
       Next_Op := Next (N);
       while Present (Next_Op)
-        and then not Nkind_In (Next_Op, N_Subprogram_Body, N_Entry_Body)
+        and then not Nkind_In (Next_Op,
+           N_Subprogram_Body, N_Entry_Body, N_Expression_Function)
       loop
          Next (Next_Op);
       end loop;
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index e3e875c..0fb5040 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -25,6 +25,7 @@
 
 with Atree;    use Atree;
 with Einfo;    use Einfo;
+with Exp_Ch5;  use Exp_Ch5;
 with Exp_Dbug; use Exp_Dbug;
 with Exp_Util; use Exp_Util;
 with Sem_Res;  use Sem_Res;
@@ -73,6 +74,26 @@ package body Exp_SPARK is
          when N_Object_Renaming_Declaration =>
             Expand_SPARK_N_Object_Renaming_Declaration (N);
 
+         --  Loop iterations over arrays need to be expanded, to avoid getting
+         --  two names referring to the same object in memory (the array and
+         --  the iterator) in GNATprove, especially since both can be written
+         --  (thus possibly leading to interferences due to aliasing). No such
+         --  problem arises with quantified expressions over arrays, which are
+         --  dealt with specially in GNATprove.
+
+         when N_Loop_Statement =>
+            declare
+               Scheme : constant Node_Id := Iteration_Scheme (N);
+            begin
+               if Present (Scheme)
+                 and then Present (Iterator_Specification (Scheme))
+                 and then
+                   Is_Iterator_Over_Array (Iterator_Specification (Scheme))
+               then
+                  Expand_Iterator_Loop_Over_Array (N);
+               end if;
+            end;
+
          --  In SPARK mode, no other constructs require expansion
 
          when others =>
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index 223c3dc..b007b36 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -30,17 +30,15 @@
 
 --  b) Compilation of unit bodies that contain the bodies of inlined sub-
 --  programs. This is done only if inlining is enabled (-gnatn). Full inlining
---  requires that a) an b) be mutually recursive, because each step may
---  generate another generic expansion and further inlined calls. For now each
---  of them uses a workpile algorithm, but they are called independently from
---  Frontend, and thus are not mutually recursive.
+--  requires that a) and b) be mutually recursive, because each step may
+--  generate another generic expansion and further inlined calls.
 
 --  c) Front-end inlining for Inline_Always subprograms. This is primarily an
 --  expansion activity that is performed for performance reasons, and when the
---  target does not use the gcc backend.
+--  target does not use the GCC back end.
 
 --  d) Front-end inlining for GNATprove, to perform source transformations
---  to simplify formal verification. The machinery used is the same than for
+--  to simplify formal verification. The machinery used is the same as for
 --  Inline_Always subprograms, but there are fewer restrictions on the source
 --  of subprograms.
 
diff --git a/gcc/ada/s-excdeb.adb b/gcc/ada/s-excdeb.adb
index 851d5e6..d9410f0 100644
--- a/gcc/ada/s-excdeb.adb
+++ b/gcc/ada/s-excdeb.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---         Copyright (C) 2006-2013, Free Software Foundation, Inc.          --
+--         Copyright (C) 2006-2015, Free Software Foundation, Inc.          --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -37,8 +37,10 @@ package body System.Exceptions_Debug is
    -- Debug_Raise_Exception --
    ---------------------------
 
-   procedure Debug_Raise_Exception (E : SSL.Exception_Data_Ptr) is
-      pragma Inspection_Point (E);
+   procedure Debug_Raise_Exception
+     (E : SSL.Exception_Data_Ptr; Message : String)
+   is
+      pragma Inspection_Point (E, Message);
    begin
       null;
    end Debug_Raise_Exception;
diff --git a/gcc/ada/s-excdeb.ads b/gcc/ada/s-excdeb.ads
index 9984d7b..21e6b52 100644
--- a/gcc/ada/s-excdeb.ads
+++ b/gcc/ada/s-excdeb.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2006-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2006-2015, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -46,7 +46,8 @@ package System.Exceptions_Debug is
    --  To let some of the hooks below have formal parameters typed in
    --  accordance with what GDB expects.
 
-   procedure Debug_Raise_Exception (E : SSL.Exception_Data_Ptr);
+   procedure Debug_Raise_Exception
+     (E : SSL.Exception_Data_Ptr; Message : String);
    pragma Export
      (Ada, Debug_Raise_Exception, "__gnat_debug_raise_exception");
    --  Hook called at a "raise" point for an exception E, when it is
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index beb6757..3410973 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -4904,9 +4904,9 @@ package body Sem_Ch12 is
          Set_Debug_Info_Needed   (Anon_Id);
          Act_Decl_Id := New_Copy (Anon_Id);
 
-         Set_Parent            (Act_Decl_Id, Parent (Anon_Id));
-         Set_Chars             (Act_Decl_Id, Chars (Defining_Entity (N)));
-         Set_Sloc              (Act_Decl_Id, Sloc (Defining_Entity (N)));
+         Set_Parent (Act_Decl_Id, Parent (Anon_Id));
+         Set_Chars  (Act_Decl_Id, Chars (Defining_Entity (N)));
+         Set_Sloc   (Act_Decl_Id, Sloc (Defining_Entity (N)));
 
          --  Subprogram instance comes from source only if generic does
 
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 3e2e26b..4f60c96 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -3336,16 +3336,33 @@ package body Sem_Ch5 is
       --  types the actual subtype of the components will only be determined
       --  when the cursor declaration is analyzed.
 
-      --  If the expander is not active, or in SPARK mode, then we want to
-      --  analyze the loop body now even in the Ada 2012 iterator case, since
-      --  the rewriting will not be done. Insert the loop variable in the
-      --  current scope, if not done when analysing the iteration scheme.
-      --  Set its kind properly to detect improper uses in the loop body.
+      --  If the expander is not active then we want to analyze the loop body
+      --  now even in the Ada 2012 iterator case, since the rewriting will not
+      --  be done. Insert the loop variable in the current scope, if not done
+      --  when analysing the iteration scheme.  Set its kind properly to detect
+      --  improper uses in the loop body.
+
+      --  In GNATprove mode, we do one of the above depending on the kind of
+      --  loop. If it is an iterator over an array, then we do not analyze the
+      --  loop now. We will analyze it after it has been rewritten by the
+      --  special SPARK expansion which is activated in GNATprove mode. We need
+      --  to do this so that other expansions that should occur in GNATprove
+      --  mode take into account the specificities of the rewritten loop, in
+      --  particular the introduction of a renaming (which needs to be
+      --  expanded).
+
+      --  In other cases in GNATprove mode then we want to analyze the loop
+      --  body now, since no rewriting will occur.
 
       if Present (Iter)
         and then Present (Iterator_Specification (Iter))
       then
-         if not Expander_Active then
+         if GNATprove_Mode
+           and then Is_Iterator_Over_Array (Iterator_Specification (Iter))
+         then
+            null;
+
+         elsif not Expander_Active then
             declare
                I_Spec : constant Node_Id   := Iterator_Specification (Iter);
                Id     : constant Entity_Id := Defining_Identifier (I_Spec);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 9d7e6da..2f5b8ca95 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6834,6 +6834,11 @@ package body Sem_Res is
         (Context : Node_Id;
          Obj_Ref : Node_Id) return Boolean
       is
+         function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean;
+         --  Determine whether an arbitrary node denotes a call to a protected
+         --  entry, function or procedure in prefixed form where the prefix is
+         --  Obj_Ref.
+
          function Within_Check (Nod : Node_Id) return Boolean;
          --  Determine whether an arbitrary node appears in a check node
 
@@ -6844,6 +6849,36 @@ package body Sem_Res is
          --  Determine whether an arbitrary entity appears in a volatile
          --  function.
 
+         ---------------------------------
+         -- Is_Protected_Operation_Call --
+         ---------------------------------
+
+         function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean is
+            Pref : Node_Id;
+            Subp : Node_Id;
+
+         begin
+            --  A call to a protected operations retains its selected component
+            --  form as opposed to other prefixed calls that are transformed in
+            --  expanded names.
+
+            if Nkind (Nod) = N_Selected_Component then
+               Pref := Prefix (Nod);
+               Subp := Selector_Name (Nod);
+
+               return
+                 Pref = Obj_Ref
+                   and then Is_Protected_Type (Etype (Pref))
+                   and then Is_Entity_Name (Subp)
+                   and then Ekind_In (Entity (Subp), E_Entry,
+                                                     E_Entry_Family,
+                                                     E_Function,
+                                                     E_Procedure);
+            else
+               return False;
+            end if;
+         end Is_Protected_Operation_Call;
+
          ------------------
          -- Within_Check --
          ------------------
@@ -6958,11 +6993,18 @@ package body Sem_Res is
          --  instance of Unchecked_Conversion whose result is renamed.
 
          elsif Nkind (Context) = N_Function_Call
+           and then Is_Entity_Name (Name (Context))
            and then Is_Unchecked_Conversion_Instance (Entity (Name (Context)))
            and then Nkind (Parent (Context)) = N_Object_Renaming_Declaration
          then
             return True;
 
+         --  The volatile object is actually the prefix in a protected entry,
+         --  function, or procedure call.
+
+         elsif Is_Protected_Operation_Call (Context) then
+            return True;
+
          --  The volatile object appears as the expression of a simple return
          --  statement that applies to a volatile function.
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 0c6e2b00..cc17f01 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12064,6 +12064,17 @@ package body Sem_Util is
       end if;
    end Is_Iterator;
 
+   ----------------------------
+   -- Is_Iterator_Over_Array --
+   ----------------------------
+
+   function Is_Iterator_Over_Array (N : Node_Id) return Boolean is
+      Container     : constant Node_Id   := Name (N);
+      Container_Typ : constant Entity_Id := Base_Type (Etype (Container));
+   begin
+      return Is_Array_Type (Container_Typ);
+   end Is_Iterator_Over_Array;
+
    ------------
    -- Is_LHS --
    ------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 5583aa0..e882f16 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1354,6 +1354,11 @@ package Sem_Util is
    --  AI05-0139-2: Check whether Typ is one of the predefined interfaces in
    --  Ada.Iterator_Interfaces, or it is derived from one.
 
+   function Is_Iterator_Over_Array (N : Node_Id) return Boolean;
+   --  N is an iterator specification. Returns True iff N is an iterator over
+   --  an array, either inside a loop of the form 'for X of A' or a quantified
+   --  expression of the form 'for all/some X of A' where A is of array type.
+
    type Is_LHS_Result is (Yes, No, Unknown);
    function Is_LHS (N : Node_Id) return Is_LHS_Result;
    --  Returns Yes if N is definitely used as Name in an assignment statement.