diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 79c2ce742daabc6dc7027060206454cf63347339..854196c6398b82fe99befaef62ad5f547a29716c 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,54 @@
+2011-08-02  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch5.adb (Expand_Iterator_Loop): Code cleanup and refactoring.
+	When a container is provided via a function call, generate a renaming
+	of the function result. This avoids the creation of a transient scope
+	and the premature finalization of the container.
+	* exp_ch7.adb (Is_Container_Cursor): Removed.
+	(Wrap_Transient_Declaration): Remove the supression of the finalization
+	of the list controller when the declaration denotes a container cursor,
+	it is not needed.
+
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* restrict.adb (Check_Formal_Restriction): only issue a warning if the
+	node is from source, instead of the original node being from source.
+	* sem_aggr.adb
+	(Resolve_Array_Aggregate): refine the check for a static expression, to
+	recognize also static ranges
+	* sem_ch3.adb, sem_ch3.ads (Analyze_Component_Declaration,
+	Array_Type_Declaration): postpone the test for the type being a subtype
+	mark after the type has been resolved, so that component-selection and
+	expanded-name are discriminated.
+	(Make_Index, Process_Range_Expr_In_Decl): add a parameter In_Iter_Schm
+	to distinguish the case of an iteration scheme, so that an error is
+	issed on a non-static range in SPARK except in an iteration scheme.
+	* sem_ch5.adb (Analyze_Iteration_Scheme): call Make_Index with
+	In_Iter_Schm = True.
+	* sem_ch6.adb (Analyze_Subprogram_Specification): refine the check for
+	user-defined operators so that they are allowed in renaming
+	* sem_ch8.adb
+	(Find_Selected_Component): refine the check for prefixing of operators
+	so that they are allowed in renaming. Move the checks for restrictions
+	on selector name after analysis discriminated between
+	component-selection and expanded-name.
+	* sem_res.adb (Resolve_Op_Concat_Arg): do not issue a warning on
+	concatenation argument of string type if it is static.
+	* sem_util.adb, sem_util.ads
+	(Check_Later_Vs_Basic_Declarations): add a new function
+	Is_Later_Declarative_Item to decice which declarations are allowed as
+	later items, in the two different modes Ada 83 and SPARK. In the SPARK
+	mode, add that renamings are considered as later items.
+	(Enclosing_Package): new function to return the enclosing package
+	(Enter_Name): correct the rule for homonyms in SPARK
+	(Is_SPARK_Initialization_Expr): default to returning True on nodes not
+	from source (result of expansion) to avoid issuing wrong warnings.
+
+2011-08-02  Ed Schonberg  <schonberg@adacore.com>
+
+	* errout.adb: On anything but an expression First_Node returns its
+	argument.
+
 2011-08-02  Pascal Obry  <obry@adacore.com>
 
 	* prj-proc.adb, make.adb, makeutl.adb: Minor reformatting.
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index cfe1d038e1a90367d81b38af021df7faa7c29490..06878e8ebb151e1e988cebff4ef32ee444720df6 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -1345,16 +1345,13 @@ package body Errout is
    --  Start of processing for First_Node
 
    begin
-      if Nkind (C) in N_Unit_Body
-        or else Nkind (C) in N_Proper_Body
-      then
-         return C;
-
-      else
+      if Nkind (C) in N_Subexpr then
          Earliest := Original_Node (C);
          Eloc := Sloc (Earliest);
          Search_Tree_First (Original_Node (C));
          return Earliest;
+      else
+         return C;
       end if;
    end First_Node;
 
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index de277662978defe5b1736e44187e55669d997fb2..a7b73cda222b1a5722cb81e5b381f1c181b79290 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -2766,106 +2766,104 @@ package body Exp_Ch5 is
    --------------------------
 
    procedure Expand_Iterator_Loop (N : Node_Id) is
-      Loc        : constant Source_Ptr := Sloc (N);
-      Isc        : constant Node_Id    := Iteration_Scheme (N);
-      I_Spec     : constant Node_Id    := Iterator_Specification (Isc);
-      Id         : constant Entity_Id  := Defining_Identifier (I_Spec);
-
-      Container : constant Node_Id := Name (I_Spec);
-      --  An expression whose type is an array or a predefined container
+      Isc    : constant Node_Id    := Iteration_Scheme (N);
+      I_Spec : constant Node_Id    := Iterator_Specification (Isc);
+      Id     : constant Entity_Id  := Defining_Identifier (I_Spec);
+      Loc    : constant Source_Ptr := Sloc (N);
+      Stats  : constant List_Id    := Statements (N);
 
-      Typ : constant Entity_Id  := Etype (Container);
+      Container     : constant Node_Id   := Name (I_Spec);
+      Container_Typ : constant Entity_Id := Etype (Container);
 
       Cursor   : Entity_Id;
       New_Loop : Node_Id;
-      Stats    : List_Id;
 
    begin
-      if Is_Array_Type (Typ) then
+      --  Processing for arrays
+
+      if Is_Array_Type (Container_Typ) then
+
+         --  for Element of Array loop
+         --
+         --  This case requires an internally generated cursor to iterate over
+         --  the array.
+
          if Of_Present (I_Spec) then
             Cursor := Make_Temporary (Loc, 'C');
 
-            --  for Elem of Arr loop ...
+            --  Generate:
+            --    Element : Component_Type renames Container (Cursor);
 
-            declare
-               Decl : constant Node_Id :=
-                        Make_Object_Renaming_Declaration (Loc,
-                          Defining_Identifier => Id,
-                          Subtype_Mark        =>
-                            New_Occurrence_Of (Component_Type (Typ), Loc),
-                          Name                =>
-                            Make_Indexed_Component (Loc,
-                              Prefix      => Relocate_Node (Container),
-                              Expressions =>
-                                New_List (New_Occurrence_Of (Cursor, Loc))));
-            begin
-               Stats := Statements (N);
-               Prepend (Decl, Stats);
+            Prepend_To (Stats,
+              Make_Object_Renaming_Declaration (Loc,
+                Defining_Identifier => Id,
+                Subtype_Mark =>
+                  New_Reference_To (Component_Type (Container_Typ), Loc),
+                Name =>
+                  Make_Indexed_Component (Loc,
+                    Prefix => Relocate_Node (Container),
+                    Expressions => New_List (
+                      New_Reference_To (Cursor, Loc)))));
 
-               New_Loop :=
-                 Make_Loop_Statement (Loc,
-                   Iteration_Scheme =>
-                     Make_Iteration_Scheme (Loc,
-                       Loop_Parameter_Specification =>
-                         Make_Loop_Parameter_Specification (Loc,
-                           Defining_Identifier         => Cursor,
-                           Discrete_Subtype_Definition =>
-                              Make_Attribute_Reference (Loc,
-                                Prefix         => Relocate_Node (Container),
-                                Attribute_Name => Name_Range),
-                           Reverse_Present => Reverse_Present (I_Spec))),
-                   Statements       => Stats,
-                   End_Label        => Empty);
-            end;
+         --  for Index in Array loop
+         --
+         --  This case utilizes the already given cursor name
 
          else
-            --  for Index in Array loop ...
-
-            --  The cursor (index into the array) is the source Id
-
             Cursor := Id;
-            New_Loop :=
-              Make_Loop_Statement (Loc,
-                Iteration_Scheme =>
-                  Make_Iteration_Scheme (Loc,
-                    Loop_Parameter_Specification =>
-                      Make_Loop_Parameter_Specification (Loc,
-                        Defining_Identifier         => Cursor,
-                        Discrete_Subtype_Definition =>
-                           Make_Attribute_Reference (Loc,
-                             Prefix         => Relocate_Node (Container),
-                             Attribute_Name => Name_Range),
-                        Reverse_Present => Reverse_Present (I_Spec))),
-                Statements       => Statements (N),
-                End_Label        => Empty);
          end if;
 
-      --  Iterators over containers
+         --  Generate:
+         --    for Cursor in [reverse] Container'Range loop
+         --       Element : Component_Type renames Container (Cursor);
+         --       --  for the "of" form
+         --
+         --       <original loop statements>
+         --    end loop;
+
+         New_Loop :=
+           Make_Loop_Statement (Loc,
+             Iteration_Scheme =>
+               Make_Iteration_Scheme (Loc,
+                 Loop_Parameter_Specification =>
+                   Make_Loop_Parameter_Specification (Loc,
+                     Defining_Identifier => Cursor,
+                       Discrete_Subtype_Definition =>
+                         Make_Attribute_Reference (Loc,
+                           Prefix => Relocate_Node (Container),
+                           Attribute_Name => Name_Range),
+                      Reverse_Present => Reverse_Present (I_Spec))),
+              Statements => Stats,
+              End_Label  => Empty);
+
+      --  Processing for containers
 
       else
          --  In both cases these require a cursor of the proper type
 
-         --    Cursor : P.Cursor_Type := Container.First;
-         --    while Cursor /= P.No_Element loop
+         --    Cursor : Pack.Cursor := Container.First;
+         --    while Cursor /= Pack.No_Element loop
+         --       Obj : Pack.Element_Type renames Element (Cursor);
+         --       --  for the "of" form
 
-         --       Obj : P.Element_Type renames Element (Cursor);
-         --       --  For the "of" form, the element name renames the element
-         --       --  designated by the cursor.
+         --       <original loop statements>
 
-         --       Statements;
-         --       P.Next (Cursor);
+         --       Pack.Next (Cursor);
          --    end loop;
 
-         --  with the obvious replacements if "reverse" is specified.
+         --  with the obvious replacements if "reverse" is specified. Pack is
+         --  the name of the package which instantiates the container.
 
          declare
             Element_Type : constant Entity_Id := Etype (Id);
-            Pack         : constant Entity_Id := Scope (Base_Type (Typ));
+            Pack         : constant Entity_Id :=
+                             Scope (Base_Type (Container_Typ));
+            Cntr         : Node_Id;
             Name_Init    : Name_Id;
             Name_Step    : Name_Id;
 
          begin
-            Stats := Statements (N);
+            --  The "of" case uses an internally generated cursor
 
             if Of_Present (I_Spec) then
                Cursor := Make_Temporary (Loc, 'C');
@@ -2873,16 +2871,6 @@ package body Exp_Ch5 is
                Cursor := Id;
             end if;
 
-            --  Must verify that the container has a reverse iterator ???
-
-            if Reverse_Present (I_Spec) then
-               Name_Init := Name_Last;
-               Name_Step := Name_Previous;
-            else
-               Name_Init := Name_First;
-               Name_Step := Name_Next;
-            end if;
-
             --  The code below only handles containers where Element is not a
             --  primitive operation of the container. This excludes for now the
             --  Hi-Lite formal containers. Generate:
@@ -2893,33 +2881,52 @@ package body Exp_Ch5 is
                Prepend_To (Stats,
                  Make_Object_Renaming_Declaration (Loc,
                    Defining_Identifier => Id,
-                   Subtype_Mark        =>
+                   Subtype_Mark =>
                      New_Occurrence_Of (Element_Type, Loc),
-                   Name                =>
+                   Name =>
                      Make_Indexed_Component (Loc,
                        Prefix =>
                          Make_Selected_Component (Loc,
-                           Prefix        =>  New_Occurrence_Of (Pack, Loc),
+                           Prefix =>
+                             New_Occurrence_Of (Pack, Loc),
                            Selector_Name =>
                              Make_Identifier (Loc, Chars => Name_Element)),
-                       Expressions =>
-                         New_List (New_Occurrence_Of (Cursor, Loc)))));
+                       Expressions => New_List (
+                         New_Occurrence_Of (Cursor, Loc)))));
+            end if;
+
+            --  Determine the advancement and initialization steps for the
+            --  cursor.
+
+            --  Must verify that the container has a reverse iterator ???
+
+            if Reverse_Present (I_Spec) then
+               Name_Init := Name_Last;
+               Name_Step := Name_Previous;
+            else
+               Name_Init := Name_First;
+               Name_Step := Name_Next;
             end if;
 
-            --  For both iterator forms, add call to step operation (Next or
-            --  Previous) to advance cursor.
+            --  For both iterator forms, add a call to the step operation to
+            --  advance the cursor. Generate:
+            --
+            --    Pack.[Next | Prev] (Cursor);
 
             Append_To (Stats,
               Make_Procedure_Call_Statement (Loc,
                 Name =>
                   Make_Selected_Component (Loc,
-                    Prefix        => New_Occurrence_Of (Pack, Loc),
-                    Selector_Name => Make_Identifier (Loc, Name_Step)),
-                Parameter_Associations =>
-                  New_List (New_Occurrence_Of (Cursor, Loc))));
+                    Prefix =>
+                      New_Occurrence_Of (Pack, Loc),
+                    Selector_Name =>
+                      Make_Identifier (Loc, Name_Step)),
+
+                Parameter_Associations => New_List (
+                  New_Occurrence_Of (Cursor, Loc))));
 
             --  Generate:
-            --    while Cursor /= No_Element loop
+            --    while Cursor /= Pack.No_Element loop
             --       <Stats>
             --    end loop;
 
@@ -2940,30 +2947,53 @@ package body Exp_Ch5 is
                 Statements => Stats,
                 End_Label  => Empty);
 
-            --  When the cursor is internally generated, associate it with the
-            --  loop statement.
+            Cntr := Relocate_Node (Container);
 
-            if Of_Present (I_Spec) then
-               Set_Ekind (Cursor, E_Variable);
-               Set_Related_Expression (Cursor, New_Loop);
+            --  When the container is provided by a function call, create an
+            --  explicit renaming of the function result. Generate:
+            --
+            --    Cnn : Container_Typ renames Func_Call (...);
+            --
+            --  The renaming avoids the generation of a transient scope when
+            --  initializing the cursor and the premature finalization of the
+            --  container.
+
+            if Nkind (Cntr) = N_Function_Call then
+               declare
+                  Ren_Id : constant Entity_Id := Make_Temporary (Loc, 'C');
+
+               begin
+                  Insert_Action (N,
+                    Make_Object_Renaming_Declaration (Loc,
+                      Defining_Identifier => Ren_Id,
+                      Subtype_Mark =>
+                        New_Reference_To (Container_Typ, Loc),
+                      Name => Cntr));
+
+                  Cntr := New_Reference_To (Ren_Id, Loc);
+               end;
             end if;
 
             --  Create the declaration of the cursor and insert it before the
             --  source loop. Generate:
             --
-            --    C : Cursor_Type := Container.First;
+            --    C : Pack.Cursor_Type := Container.[First | Last];
 
             Insert_Action (N,
               Make_Object_Declaration (Loc,
                 Defining_Identifier => Cursor,
-                Object_Definition   =>
+                Object_Definition =>
                   Make_Selected_Component (Loc,
-                    Prefix        => New_Occurrence_Of (Pack, Loc),
-                    Selector_Name => Make_Identifier (Loc, Name_Cursor)),
+                    Prefix =>
+                      New_Occurrence_Of (Pack, Loc),
+                    Selector_Name =>
+                      Make_Identifier (Loc, Name_Cursor)),
+
                 Expression =>
                   Make_Selected_Component (Loc,
-                    Prefix        => Relocate_Node (Container),
-                    Selector_Name => Make_Identifier (Loc, Name_Init))));
+                    Prefix => Cntr,
+                    Selector_Name =>
+                      Make_Identifier (Loc, Name_Init))));
 
             --  If the range of iteration is given by a function call that
             --  returns a container, the finalization actions have been saved
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index a344d9318799f1d23c6322e683a074b7435e48bc..4d64b84b2a7314eb858dfa070f8c2b72d3342177 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -3427,36 +3427,6 @@ package body Exp_Ch7 is
       S              : Entity_Id;
       Uses_SS        : Boolean;
 
-      function Is_Container_Cursor (Decl : Node_Id) return Boolean;
-      --  Determine whether object declaration Decl is a cursor used to iterate
-      --  over an Ada 2005/12 container.
-
-      -------------------------
-      -- Is_Container_Cursor --
-      -------------------------
-
-      function Is_Container_Cursor (Decl : Node_Id) return Boolean is
-         Def_Id : constant Entity_Id := Defining_Identifier (Decl);
-         Expr   : constant Node_Id   := Expression (Decl);
-
-      begin
-         --  A cursor declaration appears in the following form:
-         --
-         --    Index : Pack.Cursor := First (...);
-
-         return
-           Chars (Etype (Def_Id)) = Name_Cursor
-             and then Present (Expr)
-             and then Nkind (Expr) = N_Function_Call
-             and then Chars (Name (Expr)) = Name_First
-             and then
-               (Nkind (Parent (Decl)) = N_Expression_With_Actions
-                  or else
-                Nkind (Related_Expression (Def_Id)) = N_Loop_Statement);
-      end Is_Container_Cursor;
-
-   --  Start of processing for Wrap_Transient_Declaration
-
    begin
       S := Current_Scope;
       Enclosing_S := Scope (S);
@@ -3534,27 +3504,6 @@ package body Exp_Ch7 is
          then
             null;
 
-         --  The declaration of a container cursor is a special context where
-         --  the finalization of the list controller needs to be supressed. In
-         --  the following simplified example:
-         --
-         --    LC   : Simple_List_Controller;
-         --    Temp : Ptr_Typ := Container_Creator_Function'Reference;
-         --    Deep_Tag_Attach (Temp, LC);
-         --    Obj  : Pack.Cursor := First (Temp.all);
-         --    Finalize (LC);
-         --    <execute the loop>
-         --
-         --  the finalization of the list controller destroys the contents of
-         --  container Temp, and as a result Obj points to nothing. Note that
-         --  Temp will be finalized by the finalization list of the enclosing
-         --  scope.
-
-         elsif Ada_Version >= Ada_2012
-           and then Is_Container_Cursor (N)
-         then
-            null;
-
          --  Finalize the list controller
 
          else
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 1190f690b215dea2ecc718f69e8f2da234a84016..08af7e688f91f1a3f826db119cfa6d42ce22a28b 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -117,7 +117,7 @@ package body Restrict is
       Msg_Issued          : Boolean;
       Save_Error_Msg_Sloc : Source_Ptr;
    begin
-      if Force or else Comes_From_Source (Original_Node (N)) then
+      if Force or else Comes_From_Source (N) then
 
          --  Since the call to Restriction_Msg from Check_Restriction may set
          --  Error_Msg_Sloc to the location of the pragma restriction, save and
@@ -125,16 +125,16 @@ package body Restrict is
 
          --  ??? N in call to Check_Restriction should be First_Node (N), but
          --  this causes an exception to be raised when analyzing osint.adb.
-         --  To be modified.
+         --  To be modified together with the calls to Error_Msg_N.
 
          Save_Error_Msg_Sloc := Error_Msg_Sloc;
          Check_Restriction (Msg_Issued, SPARK, N);  --  N -> First_Node (N)
          Error_Msg_Sloc := Save_Error_Msg_Sloc;
 
          if Msg_Issued then
-            Error_Msg_F ("\\| " & Msg, N);
+            Error_Msg_N ("\\| " & Msg, N);  --  Error_Msg_N -> Error_Msg_F
          elsif SPARK_Mode then
-            Error_Msg_F ("|~~" & Msg, N);
+            Error_Msg_N ("|~~" & Msg, N);  --  Error_Msg_N -> Error_Msg_F
          end if;
       end if;
    end Check_Formal_Restriction;
@@ -145,7 +145,7 @@ package body Restrict is
    begin
       pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
 
-      if Comes_From_Source (Original_Node (N)) then
+      if Comes_From_Source (N) then
 
          --  Since the call to Restriction_Msg from Check_Restriction may set
          --  Error_Msg_Sloc to the location of the pragma restriction, save and
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index d76c35f7d58e271683737446a082d9d0c13d061e..421d04c9f20788c125c4af7f7641fb6397c445de 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -1838,7 +1838,10 @@ package body Sem_Aggr is
 
                      --  In SPARK or ALFA, the choice must be static
 
-                     if not Is_Static_Expression (Choice) then
+                     if not (Is_Static_Expression (Choice)
+                              or else (Nkind (Choice) = N_Range
+                                        and then Is_Static_Range (Choice)))
+                     then
                         Check_Formal_Restriction
                           ("choice should be static", Choice);
                      end if;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 16a6b7dc77f872b4d0f95232863906d1f87660f6..1884d03cb1076bdf1e74740b086957815acfe256 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1782,13 +1782,13 @@ package body Sem_Ch3 is
       Enter_Name (Id);
 
       if Present (Typ) then
+         T := Find_Type_Of_Object
+                (Subtype_Indication (Component_Definition (N)), N);
+
          if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
             Check_Formal_Restriction ("subtype mark required", Typ);
          end if;
 
-         T := Find_Type_Of_Object
-                (Subtype_Indication (Component_Definition (N)), N);
-
       --  Ada 2005 (AI-230): Access Definition case
 
       else
@@ -4597,12 +4597,12 @@ package body Sem_Ch3 is
 
       Nb_Index := 1;
       while Present (Index) loop
+         Analyze (Index);
+
          if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
             Check_Formal_Restriction ("subtype mark required", Index);
          end if;
 
-         Analyze (Index);
-
          --  Add a subtype declaration for each index of private array type
          --  declaration whose etype is also private. For example:
 
@@ -4672,12 +4672,12 @@ package body Sem_Ch3 is
       --  Process subtype indication if one is present
 
       if Present (Component_Typ) then
+         Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
+
          if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
             Check_Formal_Restriction ("subtype mark required", Component_Typ);
          end if;
 
-         Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
-
       --  Ada 2005 (AI-230): Access Definition case
 
       else pragma Assert (Present (Access_Definition (Component_Def)));
@@ -16140,7 +16140,8 @@ package body Sem_Ch3 is
      (I            : Node_Id;
       Related_Nod  : Node_Id;
       Related_Id   : Entity_Id := Empty;
-      Suffix_Index : Nat := 1)
+      Suffix_Index : Nat := 1;
+      In_Iter_Schm : Boolean := False)
    is
       R      : Node_Id;
       T      : Entity_Id;
@@ -16252,7 +16253,7 @@ package body Sem_Ch3 is
          end if;
 
          R := I;
-         Process_Range_Expr_In_Decl (R, T);
+         Process_Range_Expr_In_Decl (R, T, In_Iter_Schm => In_Iter_Schm);
 
       elsif Nkind (I) = N_Subtype_Indication then
 
@@ -16269,7 +16270,8 @@ package body Sem_Ch3 is
          R := Range_Expression (Constraint (I));
 
          Resolve (R, T);
-         Process_Range_Expr_In_Decl (R, Entity (Subtype_Mark (I)));
+         Process_Range_Expr_In_Decl
+           (R, Entity (Subtype_Mark (I)), In_Iter_Schm => In_Iter_Schm);
 
       elsif Nkind (I) = N_Attribute_Reference then
 
@@ -17908,10 +17910,11 @@ package body Sem_Ch3 is
    --------------------------------
 
    procedure Process_Range_Expr_In_Decl
-     (R           : Node_Id;
-      T           : Entity_Id;
-      Check_List  : List_Id := Empty_List;
-      R_Check_Off : Boolean := False)
+     (R            : Node_Id;
+      T            : Entity_Id;
+      Check_List   : List_Id := Empty_List;
+      R_Check_Off  : Boolean := False;
+      In_Iter_Schm : Boolean := False)
    is
       Lo, Hi      : Node_Id;
       R_Checks    : Check_Result;
@@ -17922,7 +17925,13 @@ package body Sem_Ch3 is
       Analyze_And_Resolve (R, Base_Type (T));
 
       if Nkind (R) = N_Range then
-         if not Is_Static_Range (R) then
+
+         --  In SPARK/ALFA, all ranges should be static, with the exception of
+         --  the discrete type definition of a loop parameter specification.
+
+         if not In_Iter_Schm
+           and then not Is_Static_Range (R)
+         then
             Check_Formal_Restriction ("range should be static", R);
          end if;
 
diff --git a/gcc/ada/sem_ch3.ads b/gcc/ada/sem_ch3.ads
index 7888a3200b0125fc196ef48851bd4090bd1126d6..514cdf3f0f9b6fe30f1da616de714c5881e6591b 100644
--- a/gcc/ada/sem_ch3.ads
+++ b/gcc/ada/sem_ch3.ads
@@ -192,14 +192,17 @@ package Sem_Ch3 is
      (I            : Node_Id;
       Related_Nod  : Node_Id;
       Related_Id   : Entity_Id := Empty;
-      Suffix_Index : Nat := 1);
+      Suffix_Index : Nat := 1;
+      In_Iter_Schm : Boolean := False);
    --  Process an index that is given in an array declaration, an entry
    --  family declaration or a loop iteration. The index is given by an
    --  index declaration (a 'box'), or by a discrete range. The later can
    --  be the name of a discrete type, or a subtype indication.
    --
    --  Related_Nod is the node where the potential generated implicit types
-   --  will be inserted. The 2 last parameters are used for creating the name.
+   --  will be inserted. The next last parameters are used for creating the
+   --  name. In_Iter_Schm is True if Make_Index is called on the discrete
+   --  subtype definition in an iteration scheme.
 
    procedure Make_Class_Wide_Type (T : Entity_Id);
    --  A Class_Wide_Type is created for each tagged type definition. The
@@ -251,10 +254,11 @@ package Sem_Ch3 is
    --    Priv_T is the private view of the type whose full declaration is in N.
 
    procedure Process_Range_Expr_In_Decl
-     (R           : Node_Id;
-      T           : Entity_Id;
-      Check_List  : List_Id := Empty_List;
-      R_Check_Off : Boolean := False);
+     (R            : Node_Id;
+      T            : Entity_Id;
+      Check_List   : List_Id := Empty_List;
+      R_Check_Off  : Boolean := False;
+      In_Iter_Schm : Boolean := False);
    --  Process a range expression that appears in a declaration context. The
    --  range is analyzed and resolved with the base type of the given type, and
    --  an appropriate check for expressions in non-static contexts made on the
@@ -265,7 +269,8 @@ package Sem_Ch3 is
    --  when the subprogram is called from Build_Record_Init_Proc and is used to
    --  return a set of constraint checking statements generated by the Checks
    --  package. R_Check_Off is set to True when the call to Range_Check is to
-   --  be skipped.
+   --  be skipped. In_Iter_Schm is True if Process_Range_Expr_In_Decl is called
+   --  on the discrete subtype definition in an iteration scheme.
 
    function Process_Subtype
      (S           : Node_Id;
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 4c92b6ed0b9c63eb7136a6015b948bd35c985ed4..7dd2e89c799c995c441d1e6094da0212d5e1f2a1 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2060,7 +2060,7 @@ package body Sem_Ch5 is
 
                Check_Controlled_Array_Attribute (DS);
 
-               Make_Index (DS, LP);
+               Make_Index (DS, LP, In_Iter_Schm => True);
 
                Set_Ekind (Id, E_Loop_Parameter);
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 97f57a93353d060edb7ce5d8846225fe6b51d8c9..186664673f295a97fcfa49c47b4ec889276f9c1c 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3073,9 +3073,12 @@ package body Sem_Ch6 is
    --  Start of processing for Analyze_Subprogram_Specification
 
    begin
-      --  User-defined operator is not allowed in SPARK or ALFA
+      --  User-defined operator is not allowed in SPARK or ALFA, except as
+      --  a renaming.
 
-      if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol then
+      if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
+        and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
+      then
          Check_Formal_Restriction ("user-defined operator is not allowed", N);
       end if;
 
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index a07449c009736b1c1768e38c8a1102f9f0da708f..90da2a64aab161dd9087c4aa7ca28d3cd162e55f 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -5348,13 +5348,15 @@ package body Sem_Ch8 is
       end if;
 
       --  Selector name cannot be a character literal or an operator symbol in
-      --  SPARK.
+      --  SPARK, except for the operator symbol in a renaming.
 
       if SPARK_Mode or else Restriction_Check_Required (SPARK) then
          if Nkind (Selector_Name (N)) = N_Character_Literal then
             Check_Formal_Restriction
               ("character literal cannot be prefixed", N);
-         elsif Nkind (Selector_Name (N)) = N_Operator_Symbol then
+         elsif Nkind (Selector_Name (N)) = N_Operator_Symbol
+           and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
+         then
             Check_Formal_Restriction ("operator symbol cannot be prefixed", N);
          end if;
       end if;
@@ -5485,18 +5487,6 @@ package body Sem_Ch8 is
       elsif Is_Entity_Name (P) then
          P_Name := Entity (P);
 
-         --  Selector name is restricted in SPARK
-
-         if SPARK_Mode or else Restriction_Check_Required (SPARK) then
-            if Is_Subprogram (P_Name) then
-               Check_Formal_Restriction
-                 ("prefix of expanded name cannot be a subprogram", P);
-            elsif Ekind (P_Name) = E_Loop then
-               Check_Formal_Restriction
-                 ("prefix of expanded name cannot be a loop statement", P);
-            end if;
-         end if;
-
          --  The prefix may denote an enclosing type which is the completion
          --  of an incomplete type declaration.
 
@@ -5693,6 +5683,20 @@ package body Sem_Ch8 is
             end if;
          end if;
 
+         --  Selector name is restricted in SPARK
+
+         if Nkind (N) = N_Expanded_Name
+           and then (SPARK_Mode or else Restriction_Check_Required (SPARK))
+         then
+            if Is_Subprogram (P_Name) then
+               Check_Formal_Restriction
+                 ("prefix of expanded name cannot be a subprogram", P);
+            elsif Ekind (P_Name) = E_Loop then
+               Check_Formal_Restriction
+                 ("prefix of expanded name cannot be a loop statement", P);
+            end if;
+         end if;
+
       else
          --  If prefix is not the name of an entity, it must be an expression,
          --  whose type is appropriate for a record. This is determined by
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index f32e05274516e0e281d956586fb7459de4911da5..3f778c3a809b145d4820b293e68c0035d1adbf43 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6786,6 +6786,8 @@ package body Sem_Res is
          if Is_Array_Type (T)
            and then Base_Type (T) /= Standard_String
            and then Base_Type (Etype (L)) = Base_Type (Etype (R))
+           and then Etype (L) /= Any_Composite  --  or else L in error
+           and then Etype (R) /= Any_Composite  --  or else R in error
            and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
          then
             Check_Formal_Restriction
@@ -7322,17 +7324,21 @@ package body Sem_Res is
       --  bounds. Of course the types have to match, so only check if operands
       --  are compatible and the node itself has no errors.
 
-      if Is_Array_Type (B_Typ)
-        and then Nkind (N) in N_Binary_Op
-        and then
-          Base_Type (Etype (Left_Opnd (N)))
-            = Base_Type (Etype (Right_Opnd (N)))
-        and then not Matching_Static_Array_Bounds (Etype (Left_Opnd (N)),
-                                                   Etype (Right_Opnd (N)))
-      then
-         Check_Formal_Restriction
-           ("array types should have matching static bounds", N);
-      end if;
+      declare
+         Left_Typ  : constant Node_Id := Etype (Left_Opnd (N));
+         Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
+      begin
+         if Is_Array_Type (B_Typ)
+           and then Nkind (N) in N_Binary_Op
+           and then Base_Type (Left_Typ) = Base_Type (Right_Typ)
+           and then Left_Typ /= Any_Composite  --  or else Left_Opnd in error
+           and then Right_Typ /= Any_Composite  --  or else Right_Opnd in error
+           and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ)
+         then
+            Check_Formal_Restriction
+              ("array types should have matching static bounds", N);
+         end if;
+      end;
 
    end Resolve_Logical_Op;
 
@@ -7702,9 +7708,9 @@ package body Sem_Res is
          end if;
 
       elsif Is_String_Type (Etype (Arg)) then
-         if Nkind (Arg) /= N_String_Literal then
+         if not Is_Static_Expression (Arg) then
             Check_Formal_Restriction
-              ("string operand for concatenation should be a literal", N);
+              ("string operand for concatenation should be static", N);
          end if;
 
       --  Do not issue error on an operand that is neither a character nor a
@@ -7984,6 +7990,7 @@ package body Sem_Res is
 
       if Is_Array_Type (Target_Typ)
         and then Is_Array_Type (Etype (Expr))
+        and then Etype (Expr) /= Any_Composite  --  or else Expr in error
         and then not Matching_Static_Array_Bounds (Target_Typ, Etype (Expr))
       then
          Check_Formal_Restriction
@@ -9109,6 +9116,7 @@ package body Sem_Res is
 
       if Is_Array_Type (Target_Typ)
         and then Is_Array_Type (Operand_Typ)
+        and then Operand_Typ /= Any_Composite  --  or else Operand in error
         and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ)
       then
          Check_Formal_Restriction
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index a16c06a7113db97f6af6b3f625272b7fbdbdd0bf..5239f5dd104efbef50111f5bf80cf101f6e53925 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -1111,6 +1111,45 @@ package body Sem_Util is
    is
       Body_Sloc : Source_Ptr;
       Decl      : Node_Id;
+
+      function Is_Later_Declarative_Item (Decl : Node_Id) return Boolean;
+      --  Return whether Decl is considered as a declarative item.
+      --  When During_Parsing is True, the semantics of Ada 83 is followed.
+      --  When During_Parsing is False, the semantics of SPARK is followed.
+
+      -------------------------------
+      -- Is_Later_Declarative_Item --
+      -------------------------------
+
+      function Is_Later_Declarative_Item (Decl : Node_Id) return Boolean is
+      begin
+         if Nkind (Decl) in N_Later_Decl_Item then
+            return True;
+
+         elsif Nkind (Decl) = N_Pragma then
+            return True;
+
+         elsif During_Parsing then
+            return False;
+
+         --  In SPARK, a package declaration is not considered as a later
+         --  declarative item.
+
+         elsif Nkind (Decl) = N_Package_Declaration then
+            return False;
+
+         --  In SPARK, a renaming is considered as a later declarative item
+
+         elsif Nkind (Decl) in N_Renaming_Declaration then
+            return True;
+
+         else
+            return False;
+         end if;
+      end Is_Later_Declarative_Item;
+
+   --  Start of Check_Later_Vs_Basic_Declarations
+
    begin
       Decl := First (Decls);
 
@@ -1131,12 +1170,7 @@ package body Sem_Util is
             Body_Sloc := Sloc (Decl);
 
             Inner : while Present (Decl) loop
-               if (Nkind (Decl) not in N_Later_Decl_Item
-                    or else (not During_Parsing
-                              and then
-                                Nkind (Decl) = N_Package_Declaration))
-                 and then Nkind (Decl) /= N_Pragma
-               then
+               if not Is_Later_Declarative_Item (Decl) then
                   if During_Parsing then
                      if Ada_Version = Ada_83 then
                         Error_Msg_Sloc := Body_Sloc;
@@ -2896,6 +2930,30 @@ package body Sem_Util is
       return Current_Node;
    end Enclosing_Lib_Unit_Node;
 
+   -----------------------
+   -- Enclosing_Package --
+   -----------------------
+
+   function Enclosing_Package (E : Entity_Id) return Entity_Id is
+      Dynamic_Scope : constant Entity_Id := Enclosing_Dynamic_Scope (E);
+
+   begin
+      if Dynamic_Scope = Standard_Standard then
+         return Standard_Standard;
+
+      elsif Dynamic_Scope = Empty then
+         return Empty;
+
+      elsif Ekind_In (Dynamic_Scope, E_Package, E_Package_Body,
+                      E_Generic_Package)
+      then
+         return Dynamic_Scope;
+
+      else
+         return Enclosing_Package (Dynamic_Scope);
+      end if;
+   end Enclosing_Package;
+
    --------------------------
    -- Enclosing_Subprogram --
    --------------------------
@@ -3260,38 +3318,51 @@ package body Sem_Util is
       --  Declaring a homonym is not allowed in SPARK or ALFA ...
 
       if Present (C)
+        and then (Restriction_Check_Required (SPARK)
+                   or else Formal_Verification_Mode)
+      then
 
-        --  ... unless the new declaration is in a subprogram, and the visible
-        --  declaration is a variable declaration or a parameter specification
-        --  outside that subprogram.
+         declare
+            Enclosing_Subp : constant Node_Id := Enclosing_Subprogram (Def_Id);
+            Enclosing_Pack : constant Node_Id := Enclosing_Package (Def_Id);
+            Other_Scope    : constant Node_Id := Enclosing_Dynamic_Scope (C);
+         begin
 
-        and then not
-          (Nkind_In (Parent (Parent (Def_Id)), N_Subprogram_Body,
-                                               N_Function_Specification,
-                                               N_Procedure_Specification)
-           and then
-             Nkind_In (Parent (C), N_Object_Declaration,
-                                   N_Parameter_Specification))
+            --  ... unless the new declaration is in a subprogram, and the
+            --  visible declaration is a variable declaration or a parameter
+            --  specification outside that subprogram.
 
-        --  ... or the new declaration is in a package, and the visible
-        --  declaration occurs outside that package.
+            if Present (Enclosing_Subp)
+              and then Nkind_In (Parent (C), N_Object_Declaration,
+                                 N_Parameter_Specification)
+              and then not Scope_Within_Or_Same (Other_Scope, Enclosing_Subp)
+            then
+               null;
 
-        and then not
-          Nkind_In (Parent (Parent (Def_Id)), N_Package_Specification,
-                                              N_Package_Body)
+            --  ... or the new declaration is in a package, and the visible
+            --  declaration occurs outside that package.
 
-        --  ... or the new declaration is a component declaration in a record
-        --  type definition.
+            elsif Present (Enclosing_Pack)
+              and then not Scope_Within_Or_Same (Other_Scope, Enclosing_Pack)
+            then
+               null;
 
-        and then Nkind (Parent (Def_Id)) /= N_Component_Declaration
+            --  ... or the new declaration is a component declaration in a
+            --  record type definition.
 
-        --  Don't issue error for non-source entities
+            elsif Nkind (Parent (Def_Id)) = N_Component_Declaration then
+               null;
 
-        and then Comes_From_Source (Def_Id)
-        and then Comes_From_Source (C)
-      then
-         Error_Msg_Sloc := Sloc (C);
-         Check_Formal_Restriction ("redeclaration of identifier &#", Def_Id);
+            --  Don't issue error for non-source entities
+
+            elsif Comes_From_Source (Def_Id)
+              and then Comes_From_Source (C)
+            then
+               Error_Msg_Sloc := Sloc (C);
+               Check_Formal_Restriction
+                 ("redeclaration of identifier &#", Def_Id);
+            end if;
+         end;
       end if;
 
       --  Warn if new entity hides an old one
@@ -7432,23 +7503,25 @@ package body Sem_Util is
       Is_Ok     : Boolean;
       Expr      : Node_Id;
       Comp_Assn : Node_Id;
-      Choice    : Node_Id;
 
    begin
       Is_Ok := True;
 
+      if not Comes_From_Source (N) then
+         goto Done;
+      end if;
+
       pragma Assert (Nkind (N) in N_Subexpr);
 
       case Nkind (N) is
          when N_Character_Literal |
               N_Integer_Literal   |
               N_Real_Literal      |
-              N_String_Literal    |
-              N_Expanded_Name     |
-              N_Membership_Test   =>
+              N_String_Literal    =>
             null;
 
-         when N_Identifier =>
+         when N_Identifier    |
+              N_Expanded_Name =>
             if Is_Entity_Name (N)
               and then Present (Entity (N))  --  needed in some cases
             then
@@ -7459,7 +7532,11 @@ package body Sem_Util is
                        E_Named_Real          =>
                      null;
                   when others =>
-                     Is_Ok := False;
+                     if Is_Type (Entity (N)) then
+                        null;
+                     else
+                        Is_Ok := False;
+                     end if;
                end case;
             end if;
 
@@ -7470,7 +7547,9 @@ package body Sem_Util is
          when N_Unary_Op =>
             Is_Ok := Is_SPARK_Initialization_Expr (Right_Opnd (N));
 
-         when N_Binary_Op | N_Short_Circuit =>
+         when N_Binary_Op       |
+              N_Short_Circuit   |
+              N_Membership_Test =>
             Is_Ok := Is_SPARK_Initialization_Expr (Left_Opnd (N))
               and then Is_SPARK_Initialization_Expr (Right_Opnd (N));
 
@@ -7492,18 +7571,6 @@ package body Sem_Util is
 
             Comp_Assn := First (Component_Associations (N));
             while Present (Comp_Assn) loop
-               Choice := First (Choices (Comp_Assn));
-               while Present (Choice) loop
-                  if Nkind (Choice) in N_Subexpr
-                    and then not Is_SPARK_Initialization_Expr (Choice)
-                  then
-                     Is_Ok := False;
-                     goto Done;
-                  end if;
-
-                  Next (Choice);
-               end loop;
-
                Expr := Expression (Comp_Assn);
                if Present (Expr)  --  needed for box association
                  and then not Is_SPARK_Initialization_Expr (Expr)
@@ -7530,6 +7597,12 @@ package body Sem_Util is
                Next (Expr);
             end loop;
 
+         --  Selected components might be expanded named not yet resolved, so
+         --  default on the safe side. (Eg on sparklex.ads)
+
+         when N_Selected_Component =>
+            null;
+
          when others =>
             Is_Ok := False;
       end case;
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index c52b68a507e3c4a61cf0cfe22443371c066c3c0d..aeb35571be1b4846489af1a39c08b599c884310f 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -339,6 +339,10 @@ package Sem_Util is
    --  Returns the enclosing N_Compilation_Unit Node that is the root of a
    --  subtree containing N.
 
+   function Enclosing_Package (E : Entity_Id) return Entity_Id;
+   --  Utility function to return the Ada entity of the package enclosing
+   --  the entity E, if any. Returns Empty if no enclosing package.
+
    function Enclosing_Subprogram (E : Entity_Id) return Entity_Id;
    --  Utility function to return the Ada entity of the subprogram enclosing
    --  the entity E, if any. Returns Empty if no enclosing subprogram.