OSDN Git Service

* gcc-interface/Makefile.in (INCLUDES_FOR_SUBDIR): Add $(fsrcdir) by
[pf3gnuchains/gcc-fork.git] / gcc / ada / sem_res.adb
index de83fa2..e45be65 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -28,7 +28,6 @@ with Checks;   use Checks;
 with Debug;    use Debug;
 with Debug_A;  use Debug_A;
 with Einfo;    use Einfo;
-with Elists;   use Elists;
 with Errout;   use Errout;
 with Expander; use Expander;
 with Exp_Disp; use Exp_Disp;
@@ -65,6 +64,7 @@ with Sem_Elab; use Sem_Elab;
 with Sem_Eval; use Sem_Eval;
 with Sem_Intr; use Sem_Intr;
 with Sem_Util; use Sem_Util;
+with Targparm; use Targparm;
 with Sem_Type; use Sem_Type;
 with Sem_Warn; use Sem_Warn;
 with Sinfo;    use Sinfo;
@@ -84,11 +84,11 @@ package body Sem_Res is
    -----------------------
 
    --  Second pass (top-down) type checking and overload resolution procedures
-   --  Typ is the type required by context. These procedures propagate the
-   --  type information recursively to the descendants of N. If the node
-   --  is not overloaded, its Etype is established in the first pass. If
-   --  overloaded,  the Resolve routines set the correct type. For arith.
-   --  operators, the Etype is the base type of the context.
+   --  Typ is the type required by context. These procedures propagate the type
+   --  information recursively to the descendants of N. If the node is not
+   --  overloaded, its Etype is established in the first pass. If overloaded,
+   --  the Resolve routines set the correct type. For arith. operators, the
+   --  Etype is the base type of the context.
 
    --  Note that Resolve_Attribute is separated off in Sem_Attr
 
@@ -136,8 +136,8 @@ package body Sem_Res is
    --  the style check for Style_Check_Boolean_And_Or.
 
    function Is_Definite_Access_Type (E : Entity_Id) return Boolean;
-   --  Determine whether E is an access type declared by an access
-   --  declaration, and not an (anonymous) allocator type.
+   --  Determine whether E is an access type declared by an access declaration,
+   --  and not an (anonymous) allocator type.
 
    function Is_Predefined_Op (Nam : Entity_Id) return Boolean;
    --  Utility to check whether the entity for an operator is a predefined
@@ -226,11 +226,10 @@ package body Sem_Res is
    --  function with no arguments, and the return value is indexed.
 
    procedure Resolve_Intrinsic_Operator (N : Node_Id; Typ : Entity_Id);
-   --  A call to a user-defined intrinsic operator is rewritten as a call
-   --  to the corresponding predefined operator, with suitable conversions.
-   --  Note that this applies only for intrinsic operators that denote
-   --  predefined operators, not operators that are intrinsic imports of
-   --  back-end builtins.
+   --  A call to a user-defined intrinsic operator is rewritten as a call to
+   --  the corresponding predefined operator, with suitable conversions. Note
+   --  that this applies only for intrinsic operators that denote predefined
+   --  operators, not ones that are intrinsic imports of back-end builtins.
 
    procedure Resolve_Intrinsic_Unary_Operator (N : Node_Id; Typ : Entity_Id);
    --  Ditto, for unary operators (arithmetic ones and "not" on signed
@@ -270,19 +269,10 @@ package body Sem_Res is
    --  to integer conversion and Truncation attribute.
 
    function Unique_Fixed_Point_Type (N : Node_Id) return Entity_Id;
-   --  A universal_fixed expression in an universal context is unambiguous
-   --  if there is only one applicable fixed point type. Determining whether
-   --  there is only one requires a search over all visible entities, and
-   --  happens only in very pathological cases (see 6115-006).
-
-   function Valid_Conversion
-     (N       : Node_Id;
-      Target  : Entity_Id;
-      Operand : Node_Id) return Boolean;
-   --  Verify legality rules given in 4.6 (8-23). Target is the target
-   --  type of the conversion, which may be an implicit conversion of
-   --  an actual parameter to an anonymous access type (in which case
-   --  N denotes the actual parameter and N = Operand).
+   --  A universal_fixed expression in an universal context is unambiguous if
+   --  there is only one applicable fixed point type. Determining whether there
+   --  is only one requires a search over all visible entities, and happens
+   --  only in very pathological cases (see 6115-006).
 
    -------------------------
    -- Ambiguous_Character --
@@ -365,11 +355,11 @@ package body Sem_Res is
       if Current_Scope /= Scop
         and then Scope_Is_Transient
       then
-         --  This can only happen if a transient scope was created
-         --  for an inner expression, which will be removed upon
-         --  completion of the analysis of an enclosing construct.
-         --  The transient scope must have the suppress status of
-         --  the enclosing environment, not of this Analyze call.
+         --  This can only happen if a transient scope was created for an inner
+         --  expression, which will be removed upon completion of the analysis
+         --  of an enclosing construct. The transient scope must have the
+         --  suppress status of the enclosing environment, not of this Analyze
+         --  call.
 
          Scope_Stack.Table (Scope_Stack.Last).Save_Scope_Suppress :=
            Scope_Suppress;
@@ -457,13 +447,12 @@ package body Sem_Res is
 
          elsif Nkind (P) = N_Index_Or_Discriminant_Constraint then
 
-            --  The following check catches the unusual case where
-            --  a discriminant appears within an index constraint
-            --  that is part of a larger expression within a constraint
-            --  on a component, e.g. "C : Int range 1 .. F (new A(1 .. D))".
-            --  For now we only check case of record components, and
-            --  note that a similar check should also apply in the
-            --  case of discriminant constraints below. ???
+            --  The following check catches the unusual case where a
+            --  discriminant appears within an index constraint that is part of
+            --  a larger expression within a constraint on a component, e.g. "C
+            --  : Int range 1 .. F (new A(1 .. D))". For now we only check case
+            --  of record components, and note that a similar check should also
+            --  apply in the case of discriminant constraints below. ???
 
             --  Note that the check for N_Subtype_Declaration below is to
             --  detect the valid use of discriminants in the constraints of a
@@ -505,9 +494,9 @@ package body Sem_Res is
                CB : Entity_Id;
 
                function Large_Storage_Type (T : Entity_Id) return Boolean;
-               --  Return True if type T has a large enough range that
-               --  any array whose index type covered the whole range of
-               --  the type would likely raise Storage_Error.
+               --  Return True if type T has a large enough range that any
+               --  array whose index type covered the whole range of the type
+               --  would likely raise Storage_Error.
 
                ------------------------
                -- Large_Storage_Type --
@@ -551,8 +540,8 @@ package body Sem_Res is
                   goto No_Danger;
                end if;
 
-               --  Check the array allows a large range at this bound.
-               --  First find the array
+               --  Check the array allows a large range at this bound. First
+               --  find the array
 
                SI := Parent (P);
 
@@ -619,8 +608,8 @@ package body Sem_Res is
 
          return;
 
-      --  Otherwise, context is an expression. It should not be within
-      --  (i.e. a subexpression of) a constraint for a component.
+      --  Otherwise, context is an expression. It should not be within (i.e. a
+      --  subexpression of) a constraint for a component.
 
       else
          D := PN;
@@ -634,18 +623,18 @@ package body Sem_Res is
             exit when No (P);
          end loop;
 
-         --  If the discriminant is used in an expression that is a bound
-         --  of a scalar type, an Itype is created and the bounds are attached
-         --  to its range,  not to the original subtype indication. Such use
-         --  is of course a double fault.
+         --  If the discriminant is used in an expression that is a bound of a
+         --  scalar type, an Itype is created and the bounds are attached to
+         --  its range, not to the original subtype indication. Such use is of
+         --  course a double fault.
 
          if (Nkind (P) = N_Subtype_Indication
               and then Nkind_In (Parent (P), N_Component_Definition,
                                              N_Derived_Type_Definition)
               and then D = Constraint (P))
 
-         --  The constraint itself may be given by a subtype indication,
-         --  rather than by a more common discrete range.
+           --  The constraint itself may be given by a subtype indication,
+           --  rather than by a more common discrete range.
 
            or else (Nkind (P) = N_Subtype_Indication
                       and then
@@ -731,8 +720,8 @@ package body Sem_Res is
       C : Node_Id;
 
       function Same_Argument_List return Boolean;
-      --  Check whether list of actuals is identical to list of formals
-      --  of called function (which is also the enclosing scope).
+      --  Check whether list of actuals is identical to list of formals of
+      --  called function (which is also the enclosing scope).
 
       ------------------------
       -- Same_Argument_List --
@@ -819,8 +808,10 @@ package body Sem_Res is
 
          if Nkind_In (P, N_Or_Else,
                          N_And_Then,
-                         N_If_Statement,
-                         N_Case_Statement)
+                         N_Case_Expression,
+                         N_Case_Statement,
+                         N_Conditional_Expression,
+                         N_If_Statement)
          then
             return False;
 
@@ -867,7 +858,7 @@ package body Sem_Res is
                   exit when Nkind (Nod) /= N_Raise_Statement
                     and then
                       (Nkind (Nod) not in N_Raise_xxx_Error
-                         or else Present (Condition (Nod)));
+                        or else Present (Condition (Nod)));
                end;
             end if;
 
@@ -1016,9 +1007,9 @@ package body Sem_Res is
          --  functions, this is never a parameterless call (RM 4.1.4(6)).
 
          if Nkind (Parent (N)) = N_Attribute_Reference
-            and then (Attribute_Name (Parent (N)) = Name_Address
-              or else Attribute_Name (Parent (N)) = Name_Code_Address
-              or else Attribute_Name (Parent (N)) = Name_Access)
+            and then (Attribute_Name (Parent (N)) = Name_Address      or else
+                      Attribute_Name (Parent (N)) = Name_Code_Address or else
+                      Attribute_Name (Parent (N)) = Name_Access)
          then
             return False;
          end if;
@@ -1109,13 +1100,28 @@ package body Sem_Res is
                                                               E_Procedure)
                          and then Is_Overloaded (Selector_Name (N)))))
 
-      --  If one of the above three conditions is met, rewrite as call.
-      --  Apply the rewriting only once.
+      --  If one of the above three conditions is met, rewrite as call. Apply
+      --  the rewriting only once.
 
       then
          if Nkind (Parent (N)) /= N_Function_Call
            or else N /= Name (Parent (N))
          then
+
+            --  This may be a prefixed call that was not fully analyzed, e.g.
+            --  an actual in an instance.
+
+            if Ada_Version >= Ada_2005
+              and then Nkind (N) = N_Selected_Component
+              and then Is_Dispatching_Operation (Entity (Selector_Name (N)))
+            then
+               Analyze_Selected_Component (N);
+
+               if Nkind (N) /= N_Selected_Component then
+                  return;
+               end if;
+            end if;
+
             Nam := New_Copy (N);
 
             --  If overloaded, overload set belongs to new copy
@@ -1554,11 +1560,11 @@ package body Sem_Res is
 
       if Is_Private_Type (Typ) then
          case Nkind (N) is
-            when N_Op_Add  | N_Op_Subtract | N_Op_Multiply | N_Op_Divide |
-            N_Op_Expon     | N_Op_Mod      | N_Op_Rem      =>
+            when N_Op_Add   | N_Op_Subtract | N_Op_Multiply | N_Op_Divide |
+                 N_Op_Expon | N_Op_Mod      | N_Op_Rem      =>
                Resolve_Intrinsic_Operator (N, Typ);
 
-            when N_Op_Plus | N_Op_Minus    | N_Op_Abs      =>
+            when N_Op_Plus  | N_Op_Minus    | N_Op_Abs      =>
                Resolve_Intrinsic_Unary_Operator (N, Typ);
 
             when others =>
@@ -1580,6 +1586,8 @@ package body Sem_Res is
       Kind : Node_Kind;
 
    begin
+      --  Use CASE statement or array???
+
       if Is_Binary then
          if    Op_Name =  Name_Op_And      then
             Kind := N_Op_And;
@@ -1684,6 +1692,7 @@ package body Sem_Res is
       Tsk : Node_Id := Empty;
 
       function Process_Discr (Nod : Node_Id) return Traverse_Result;
+      --  Comment needed???
 
       -------------------
       -- Process_Discr --
@@ -1717,7 +1726,7 @@ package body Sem_Res is
    --  Start of processing for Replace_Actual_Discriminants
 
    begin
-      if not Expander_Active then
+      if not Full_Expander_Active then
          return;
       end if;
 
@@ -1775,8 +1784,8 @@ package body Sem_Res is
       begin
          return
            Sloc (Nod) = Standard_Location
-             or else Is_Predefined_File_Name (Unit_File_Name (
-                       Get_Source_Unit (Sloc (Nod))));
+             or else Is_Predefined_File_Name
+                       (Unit_File_Name (Get_Source_Unit (Sloc (Nod))));
       end Comes_From_Predefined_Lib_Unit;
 
       --------------------
@@ -1785,18 +1794,14 @@ package body Sem_Res is
 
       procedure Patch_Up_Value (N : Node_Id; Typ : Entity_Id) is
       begin
-         if Nkind (N) = N_Integer_Literal
-           and then Is_Real_Type (Typ)
-         then
+         if Nkind (N) = N_Integer_Literal and then Is_Real_Type (Typ) then
             Rewrite (N,
               Make_Real_Literal (Sloc (N),
                 Realval => UR_From_Uint (Intval (N))));
             Set_Etype (N, Universal_Real);
             Set_Is_Static_Expression (N);
 
-         elsif Nkind (N) = N_Real_Literal
-           and then Is_Integer_Type (Typ)
-         then
+         elsif Nkind (N) = N_Real_Literal and then Is_Integer_Type (Typ) then
             Rewrite (N,
               Make_Integer_Literal (Sloc (N),
                 Intval => UR_To_Uint (Realval (N))));
@@ -1804,7 +1809,7 @@ package body Sem_Res is
             Set_Is_Static_Expression (N);
 
          elsif Nkind (N) = N_String_Literal
-           and then Is_Character_Type (Typ)
+                 and then Is_Character_Type (Typ)
          then
             Set_Character_Literal_Name (Char_Code (Character'Pos ('A')));
             Rewrite (N,
@@ -1815,15 +1820,13 @@ package body Sem_Res is
             Set_Etype (N, Any_Character);
             Set_Is_Static_Expression (N);
 
-         elsif Nkind (N) /= N_String_Literal
-           and then Is_String_Type (Typ)
-         then
+         elsif Nkind (N) /= N_String_Literal and then Is_String_Type (Typ) then
             Rewrite (N,
               Make_String_Literal (Sloc (N),
                 Strval => End_String));
 
          elsif Nkind (N) = N_Range then
-            Patch_Up_Value (Low_Bound (N), Typ);
+            Patch_Up_Value (Low_Bound (N),  Typ);
             Patch_Up_Value (High_Bound (N), Typ);
          end if;
       end Patch_Up_Value;
@@ -1844,7 +1847,7 @@ package body Sem_Res is
          then
             Error_Msg_NE ("ambiguous call to&", Arg, Name (Arg));
 
-            --  Could use comments on what is going on here ???
+            --  Could use comments on what is going on here???
 
             Get_First_Interp (Name (Arg), I, It);
             while Present (It.Nam) loop
@@ -1892,13 +1895,13 @@ package body Sem_Res is
          return;
       end if;
 
-      --  Access attribute on remote subprogram cannot be used for
-      --  a non-remote access-to-subprogram type.
+      --  Access attribute on remote subprogram cannot be used for a non-remote
+      --  access-to-subprogram type.
 
       if Nkind (N) = N_Attribute_Reference
-        and then (Attribute_Name (N) = Name_Access
-                    or else Attribute_Name (N) = Name_Unrestricted_Access
-                    or else Attribute_Name (N) = Name_Unchecked_Access)
+        and then (Attribute_Name (N) = Name_Access              or else
+                  Attribute_Name (N) = Name_Unrestricted_Access or else
+                  Attribute_Name (N) = Name_Unchecked_Access)
         and then Comes_From_Source (N)
         and then Is_Entity_Name (Prefix (N))
         and then Is_Subprogram (Entity (Prefix (N)))
@@ -1918,8 +1921,7 @@ package body Sem_Res is
 
       if Nkind (N) = N_Attribute_Reference
         and then Comes_From_Source (N)
-        and then (Is_Remote_Call_Interface (Typ)
-                    or else Is_Remote_Types (Typ))
+        and then (Is_Remote_Call_Interface (Typ) or else Is_Remote_Types (Typ))
       then
          declare
             Attr      : constant Attribute_Id :=
@@ -1966,16 +1968,16 @@ package body Sem_Res is
                --   perform semantic checks against the corresponding
                --   remote entities.
 
-               if (Attr = Attribute_Access
-                    or else Attr = Attribute_Unchecked_Access
-                    or else Attr = Attribute_Unrestricted_Access)
-                 and then Expander_Active
+               if (Attr = Attribute_Access           or else
+                   Attr = Attribute_Unchecked_Access or else
+                   Attr = Attribute_Unrestricted_Access)
+                 and then Full_Expander_Active
                  and then Get_PCS_Name /= Name_No_DSA
                then
                   Check_Subtype_Conformant
                     (New_Id  => Entity (Prefix (N)),
                      Old_Id  => Designated_Type
-                       (Corresponding_Remote_Type (Typ)),
+                                  (Corresponding_Remote_Type (Typ)),
                      Err_Loc => N);
 
                   if Is_Remote then
@@ -2212,9 +2214,9 @@ package body Sem_Res is
                         end if;
 
                      --  If this is an indirect call, use the subprogram_type
-                     --  in the message, to have a meaningful location.
-                     --  Also indicate if this is an inherited operation,
-                     --  created by a type declaration.
+                     --  in the message, to have a meaningful location. Also
+                     --  indicate if this is an inherited operation, created
+                     --  by a type declaration.
 
                      elsif Nkind (N) = N_Function_Call
                        and then Nkind (Name (N)) = N_Explicit_Dereference
@@ -2279,6 +2281,22 @@ package body Sem_Res is
                elsif Nkind (N) = N_Conditional_Expression then
                   Set_Etype (N, Expr_Type);
 
+               --  AI05-0139-2: Expression is overloaded because type has
+               --  implicit dereference. If type matches context, no implicit
+               --  dereference is involved.
+
+               elsif Has_Implicit_Dereference (Expr_Type) then
+                  Set_Etype (N, Expr_Type);
+                  Set_Is_Overloaded (N, False);
+                  exit Interp_Loop;
+
+               elsif Is_Overloaded (N)
+                 and then Present (It.Nam)
+                 and then Ekind (It.Nam) = E_Discriminant
+                 and then Has_Implicit_Dereference (It.Nam)
+               then
+                  Build_Explicit_Dereference (N, It.Nam);
+
                --  For an explicit dereference, attribute reference, range,
                --  short-circuit form (which is not an operator node), or call
                --  with a name that is an explicit dereference, there is
@@ -2461,10 +2479,10 @@ package body Sem_Res is
                   procedure Check_Elmt (Aelmt : Node_Id) is
                   begin
                      --  If we have a nested aggregate, go inside it (to
-                     --  attempt a naked analyze-resolve of the aggregate
-                     --  can cause undesirable cascaded errors). Do not
-                     --  resolve expression if it needs a type from context,
-                     --  as for integer * fixed expression.
+                     --  attempt a naked analyze-resolve of the aggregate can
+                     --  cause undesirable cascaded errors). Do not resolve
+                     --  expression if it needs a type from context, as for
+                     --  integer * fixed expression.
 
                      if Nkind (Aelmt) = N_Aggregate then
                         Check_Aggr (Aelmt);
@@ -2489,9 +2507,8 @@ package body Sem_Res is
                end;
             end if;
 
-            --  If an error message was issued already, Found got reset
-            --  to True, so if it is still False, issue the standard
-            --  Wrong_Type message.
+            --  If an error message was issued already, Found got reset to
+            --  True, so if it is still False, issue standard Wrong_Type msg.
 
             if not Found then
                if Is_Overloaded (N)
@@ -2508,6 +2525,7 @@ package body Sem_Res is
                         --  Protected operation: retrieve operation name
 
                         Subp_Name := Selector_Name (Name (N));
+
                      else
                         raise Program_Error;
                      end if;
@@ -2538,6 +2556,7 @@ package body Sem_Res is
                   else
                      Error_Msg_N ("\use -gnatf for details", N);
                   end if;
+
                else
                   Wrong_Type (N, Typ);
                end if;
@@ -2561,17 +2580,17 @@ package body Sem_Res is
          --  types, rather than a specific type, propagate the actual type
          --  downward.
 
-         if Typ = Any_Integer
-           or else Typ = Any_Boolean
-           or else Typ = Any_Modular
-           or else Typ = Any_Real
-           or else Typ = Any_Discrete
+         if Typ = Any_Integer or else
+            Typ = Any_Boolean or else
+            Typ = Any_Modular or else
+            Typ = Any_Real    or else
+            Typ = Any_Discrete
          then
             Ctx_Type := Expr_Type;
 
-            --  Any_Fixed is legal in a real context only if a specific
-            --  fixed point type is imposed. If Norman Cohen can be
-            --  confused by this, it deserves a separate message.
+            --  Any_Fixed is legal in a real context only if a specific fixed-
+            --  point type is imposed. If Norman Cohen can be confused by this,
+            --  it deserves a separate message.
 
             if Typ = Any_Real
               and then Expr_Type = Any_Fixed
@@ -2733,6 +2752,22 @@ package body Sem_Res is
                Resolve_Unchecked_Type_Conversion                 (N, Ctx_Type);
          end case;
 
+         --  Ada 2012 (AI05-0149): Apply an (implicit) conversion to an
+         --  expression of an anonymous access type that occurs in the context
+         --  of a named general access type, except when the expression is that
+         --  of a membership test. This ensures proper legality checking in
+         --  terms of allowed conversions (expressions that would be illegal to
+         --  convert implicitly are allowed in membership tests).
+
+         if Ada_Version >= Ada_2012
+           and then Ekind (Ctx_Type) = E_General_Access_Type
+           and then Ekind (Etype (N)) = E_Anonymous_Access_Type
+           and then Nkind (Parent (N)) not in N_Membership_Test
+         then
+            Rewrite (N, Convert_To (Ctx_Type, Relocate_Node (N)));
+            Analyze_And_Resolve (N, Ctx_Type);
+         end if;
+
          --  If the subexpression was replaced by a non-subexpression, then
          --  all we do is to expand it. The only legitimate case we know of
          --  is converting procedure call statement to entry call statements,
@@ -2744,6 +2779,18 @@ package body Sem_Res is
             return;
          end if;
 
+         --  AI05-144-2: Check dangerous order dependence within an expression
+         --  that is not a subexpression. Exclude RHS of an assignment, because
+         --  both sides may have side-effects and the check must be performed
+         --  over the statement.
+
+         if Nkind (Parent (N)) not in N_Subexpr
+           and then Nkind (Parent (N)) /= N_Assignment_Statement
+           and then Nkind (Parent (N)) /= N_Procedure_Call_Statement
+         then
+            Check_Order_Dependence;
+         end if;
+
          --  The expression is definitely NOT overloaded at this point, so
          --  we reset the Is_Overloaded flag to avoid any confusion when
          --  reanalyzing the node.
@@ -2753,18 +2800,27 @@ package body Sem_Res is
          --  Freeze expression type, entity if it is a name, and designated
          --  type if it is an allocator (RM 13.14(10,11,13)).
 
-         --  Now that the resolution of the type of the node is complete,
-         --  and we did not detect an error, we can expand this node. We
-         --  skip the expand call if we are in a default expression, see
-         --  section "Handling of Default Expressions" in Sem spec.
+         --  Now that the resolution of the type of the node is complete, and
+         --  we did not detect an error, we can expand this node. We skip the
+         --  expand call if we are in a default expression, see section
+         --  "Handling of Default Expressions" in Sem spec.
 
          Debug_A_Exit ("resolving  ", N, "  (done)");
 
          --  We unconditionally freeze the expression, even if we are in
-         --  default expression mode (the Freeze_Expression routine tests
-         --  this flag and only freezes static types if it is set).
+         --  default expression mode (the Freeze_Expression routine tests this
+         --  flag and only freezes static types if it is set).
+
+         --  AI05-177 (Ada2012): Expression functions do not freeze. Only
+         --  their use (in an expanded call) freezes.
 
-         Freeze_Expression (N);
+         if Ekind (Current_Scope) /= E_Function
+           or else
+             Nkind (Original_Node (Unit_Declaration_Node (Current_Scope))) /=
+                                                        N_Expression_Function
+         then
+            Freeze_Expression (N);
+         end if;
 
          --  Now we can do the expansion
 
@@ -2864,13 +2920,10 @@ package body Sem_Res is
          --  not come from source, or this warning is off.
 
          if not Warn_On_Parameter_Order
-           or else
-             No (Parameter_Associations (N))
-           or else
-             not Nkind_In (Original_Node (N), N_Procedure_Call_Statement,
-                                              N_Function_Call)
-           or else
-             not Comes_From_Source (N)
+           or else No (Parameter_Associations (N))
+           or else not Nkind_In (Original_Node (N), N_Procedure_Call_Statement,
+                                                    N_Function_Call)
+           or else not Comes_From_Source (N)
          then
             return;
          end if;
@@ -3097,10 +3150,10 @@ package body Sem_Res is
                then
                   Analyze_And_Resolve (Actval, Base_Type (Etype (Actval)));
 
-               --  Resolve entities with their own type, which may differ
-               --  from the type of a reference in a generic context (the
-               --  view swapping mechanism did not anticipate the re-analysis
-               --  of default values in calls).
+               --  Resolve entities with their own type, which may differ from
+               --  the type of a reference in a generic context (the view
+               --  swapping mechanism did not anticipate the re-analysis of
+               --  default values in calls).
 
                elsif Is_Entity_Name (Actval) then
                   Analyze_And_Resolve (Actval, Etype (Entity (Actval)));
@@ -3110,8 +3163,8 @@ package body Sem_Res is
                end if;
             end if;
 
-            --  If default is a tag indeterminate function call, propagate
-            --  tag to obtain proper dispatching.
+            --  If default is a tag indeterminate function call, propagate tag
+            --  to obtain proper dispatching.
 
             if Is_Controlling_Formal (F)
               and then Nkind (Default_Value (F)) = N_Function_Call
@@ -3122,10 +3175,10 @@ package body Sem_Res is
          end if;
 
          --  If the default expression raises constraint error, then just
-         --  silently replace it with an N_Raise_Constraint_Error node,
-         --  since we already gave the warning on the subprogram spec.
-         --  If node is already a Raise_Constraint_Error leave as is, to
-         --  prevent loops in the warnings removal machinery.
+         --  silently replace it with an N_Raise_Constraint_Error node, since
+         --  we already gave the warning on the subprogram spec. If node is
+         --  already a Raise_Constraint_Error leave as is, to prevent loops in
+         --  the warnings removal machinery.
 
          if Raises_Constraint_Error (Actval)
            and then Nkind (Actval) /= N_Raise_Constraint_Error
@@ -3212,8 +3265,8 @@ package body Sem_Res is
 
             when N_Op_Concat =>
 
-               --  Concatenation is static when both operands are static
-               --  and the concatenation operator is a predefined one.
+               --  Concatenation is static when both operands are static and
+               --  the concatenation operator is a predefined one.
 
                return Scope (Entity (N)) = Standard_Standard
                         and then
@@ -3269,8 +3322,7 @@ package body Sem_Res is
          --  If the actual is an entity, generate a reference to it now. We
          --  do this before the actual is resolved, because a formal of some
          --  protected subprogram, or a task discriminant, will be rewritten
-         --  during expansion, and the reference to the source entity may
-         --  be lost.
+         --  during expansion, and the source entity reference may be lost.
 
          if Present (A)
            and then Is_Entity_Name (A)
@@ -3283,6 +3335,7 @@ package body Sem_Res is
                  and then Ekind (F) /= E_In_Parameter
                then
                   Generate_Reference (Orig_A, A, 'm');
+
                elsif not Is_Overloaded (A) then
                   Generate_Reference (Orig_A, A);
                end if;
@@ -3291,8 +3344,7 @@ package body Sem_Res is
 
          if Present (A)
            and then (Nkind (Parent (A)) /= N_Parameter_Association
-                       or else
-                     Chars (Selector_Name (Parent (A))) = Chars (F))
+                      or else Chars (Selector_Name (Parent (A))) = Chars (F))
          then
             --  If style checking mode on, check match of formal name
 
@@ -3322,45 +3374,55 @@ package body Sem_Res is
                if Ekind (F) = E_In_Out_Parameter
                  and then Is_Array_Type (Etype (F))
                then
-                  if Has_Aliased_Components (Etype (Expression (A)))
-                    /= Has_Aliased_Components (Etype (F))
-                  then
+                  --  In a view conversion, the conversion must be legal in
+                  --  both directions, and thus both component types must be
+                  --  aliased, or neither (4.6 (8)).
 
-                     --  In a view conversion, the conversion must be legal in
-                     --  both directions, and thus both component types must be
-                     --  aliased, or neither (4.6 (8)).
-
-                     --  The additional rule 4.6 (24.9.2) seems unduly
-                     --  restrictive: the privacy requirement should not apply
-                     --  to generic types, and should be checked in an
-                     --  instance. ARG query is in order ???
+                  --  The extra rule in 4.6 (24.9.2) seems unduly restrictive:
+                  --  the privacy requirement should not apply to generic
+                  --  types, and should be checked in an instance. ARG query
+                  --  is in order ???
 
+                  if Has_Aliased_Components (Etype (Expression (A))) /=
+                     Has_Aliased_Components (Etype (F))
+                  then
                      Error_Msg_N
                        ("both component types in a view conversion must be"
                          & " aliased, or neither", A);
 
+                  --  Comment here??? what set of cases???
+
                   elsif
                      not Same_Ancestor (Etype (F), Etype (Expression (A)))
                   then
+                     --  Check view conv between unrelated by ref array types
+
                      if Is_By_Reference_Type (Etype (F))
                         or else Is_By_Reference_Type (Etype (Expression (A)))
                      then
                         Error_Msg_N
                           ("view conversion between unrelated by reference " &
                            "array types not allowed (\'A'I-00246)", A);
-                     else
+
+                     --  In Ada 2005 mode, check view conversion component
+                     --  type cannot be private, tagged, or volatile. Note
+                     --  that we only apply this to source conversions. The
+                     --  generated code can contain conversions which are
+                     --  not subject to this test, and we cannot extract the
+                     --  component type in such cases since it is not present.
+
+                     elsif Comes_From_Source (A)
+                       and then Ada_Version >= Ada_2005
+                     then
                         declare
                            Comp_Type : constant Entity_Id :=
                                          Component_Type
                                            (Etype (Expression (A)));
                         begin
-                           if Comes_From_Source (A)
-                             and then Ada_Version >= Ada_2005
-                             and then
-                               ((Is_Private_Type (Comp_Type)
-                                   and then not Is_Generic_Type (Comp_Type))
-                                 or else Is_Tagged_Type (Comp_Type)
-                                 or else Is_Volatile (Comp_Type))
+                           if (Is_Private_Type (Comp_Type)
+                                 and then not Is_Generic_Type (Comp_Type))
+                             or else Is_Tagged_Type (Comp_Type)
+                             or else Is_Volatile (Comp_Type)
                            then
                               Error_Msg_N
                                 ("component type of a view conversion cannot"
@@ -3373,8 +3435,10 @@ package body Sem_Res is
                   end if;
                end if;
 
+               --  Resolve expression if conversion is all OK
+
                if (Conversion_OK (A)
-                     or else Valid_Conversion (A, Etype (A), Expression (A)))
+                    or else Valid_Conversion (A, Etype (A), Expression (A)))
                  and then not Is_Ref_To_Bit_Packed_Array (Expression (A))
                then
                   Resolve (Expression (A));
@@ -3388,11 +3452,11 @@ package body Sem_Res is
             elsif Nkind (A) = N_Function_Call
               and then Is_Limited_Record (Etype (F))
               and then not Is_Constrained (Etype (F))
-              and then Expander_Active
-              and then
-                (Is_Controlled (Etype (F)) or else Has_Task (Etype (F)))
+              and then Full_Expander_Active
+              and then (Is_Controlled (Etype (F)) or else Has_Task (Etype (F)))
             then
                Establish_Transient_Scope (A, False);
+               Resolve (A, Etype (F));
 
             --  A small optimization: if one of the actuals is a concatenation
             --  create a block around a procedure call to recover stack space.
@@ -3404,7 +3468,7 @@ package body Sem_Res is
 
             elsif Nkind (A) = N_Op_Concat
               and then Nkind (N) = N_Procedure_Call_Statement
-              and then Expander_Active
+              and then Full_Expander_Active
               and then
                 not (Is_Intrinsic_Subprogram (Nam)
                       and then Chars (Nam) = Name_Asm)
@@ -3467,7 +3531,7 @@ package body Sem_Res is
                      --  be removed in the expansion of the wrapped construct.
 
                      if (Is_Controlled (DDT) or else Has_Task (DDT))
-                       and then Expander_Active
+                       and then Full_Expander_Active
                      then
                         Establish_Transient_Scope (A, False);
                      end if;
@@ -3482,59 +3546,157 @@ package body Sem_Res is
                --   or because it is a generic actual, so use base type to
                --   locate concurrent type.
 
-               A_Typ := Base_Type (Etype (A));
                F_Typ := Base_Type (Etype (F));
 
-               declare
-                  Full_A_Typ : Entity_Id;
+               if Is_Tagged_Type (F_Typ)
+                 and then (Is_Concurrent_Type (F_Typ)
+                             or else Is_Concurrent_Record_Type (F_Typ))
+               then
+                  --  If the actual is overloaded, look for an interpretation
+                  --  that has a synchronized type.
+
+                  if not Is_Overloaded (A) then
+                     A_Typ := Base_Type (Etype (A));
 
-               begin
-                  if Present (Full_View (A_Typ)) then
-                     Full_A_Typ := Base_Type (Full_View (A_Typ));
                   else
-                     Full_A_Typ := A_Typ;
+                     declare
+                        Index : Interp_Index;
+                        It    : Interp;
+
+                     begin
+                        Get_First_Interp (A, Index, It);
+                        while Present (It.Typ) loop
+                           if Is_Concurrent_Type (It.Typ)
+                             or else Is_Concurrent_Record_Type (It.Typ)
+                           then
+                              A_Typ := Base_Type (It.Typ);
+                              exit;
+                           end if;
+
+                           Get_Next_Interp (Index, It);
+                        end loop;
+                     end;
                   end if;
 
-                  --  Tagged synchronized type (case 1): the actual is a
-                  --  concurrent type
+                  declare
+                     Full_A_Typ : Entity_Id;
 
-                  if Is_Concurrent_Type (A_Typ)
-                    and then Corresponding_Record_Type (A_Typ) = F_Typ
-                  then
-                     Rewrite (A,
-                       Unchecked_Convert_To
-                         (Corresponding_Record_Type (A_Typ), A));
-                     Resolve (A, Etype (F));
+                  begin
+                     if Present (Full_View (A_Typ)) then
+                        Full_A_Typ := Base_Type (Full_View (A_Typ));
+                     else
+                        Full_A_Typ := A_Typ;
+                     end if;
+
+                     --  Tagged synchronized type (case 1): the actual is a
+                     --  concurrent type.
 
-                  --  Tagged synchronized type (case 2): the formal is a
-                  --  concurrent type
+                     if Is_Concurrent_Type (A_Typ)
+                       and then Corresponding_Record_Type (A_Typ) = F_Typ
+                     then
+                        Rewrite (A,
+                          Unchecked_Convert_To
+                            (Corresponding_Record_Type (A_Typ), A));
+                        Resolve (A, Etype (F));
 
-                  elsif Ekind (Full_A_Typ) = E_Record_Type
-                    and then Present
+                     --  Tagged synchronized type (case 2): the formal is a
+                     --  concurrent type.
+
+                     elsif Ekind (Full_A_Typ) = E_Record_Type
+                       and then Present
                                (Corresponding_Concurrent_Type (Full_A_Typ))
-                    and then Is_Concurrent_Type (F_Typ)
-                    and then Present (Corresponding_Record_Type (F_Typ))
-                    and then Full_A_Typ = Corresponding_Record_Type (F_Typ)
-                  then
-                     Resolve (A, Corresponding_Record_Type (F_Typ));
+                       and then Is_Concurrent_Type (F_Typ)
+                       and then Present (Corresponding_Record_Type (F_Typ))
+                       and then Full_A_Typ = Corresponding_Record_Type (F_Typ)
+                     then
+                        Resolve (A, Corresponding_Record_Type (F_Typ));
 
-                  --  Common case
+                     --  Common case
 
-                  else
-                     Resolve (A, Etype (F));
-                  end if;
-               end;
+                     else
+                        Resolve (A, Etype (F));
+                     end if;
+                  end;
+               else
+
+                  --  not a synchronized operation.
+
+                  Resolve (A, Etype (F));
+               end if;
             end if;
 
             A_Typ := Etype (A);
             F_Typ := Etype (F);
 
-            --  Save actual for subsequent check on order dependence,
-            --  and indicate whether actual is modifiable. For AI05-0144
+            if Comes_From_Source (Original_Node (N))
+              and then Nkind_In (Original_Node (N), N_Function_Call,
+                                                    N_Procedure_Call_Statement)
+            then
+               --  In formal mode, check that actual parameters matching
+               --  formals of tagged types are objects (or ancestor type
+               --  conversions of objects), not general expressions.
+
+               if Is_Actual_Tagged_Parameter (A) then
+                  if Is_SPARK_Object_Reference (A) then
+                     null;
+
+                  elsif Nkind (A) = N_Type_Conversion then
+                     declare
+                        Operand     : constant Node_Id   := Expression (A);
+                        Operand_Typ : constant Entity_Id := Etype (Operand);
+                        Target_Typ  : constant Entity_Id := A_Typ;
+
+                     begin
+                        if not Is_SPARK_Object_Reference (Operand) then
+                           Check_SPARK_Restriction
+                             ("object required", Operand);
+
+                        --  In formal mode, the only view conversions are those
+                        --  involving ancestor conversion of an extended type.
+
+                        elsif not
+                          (Is_Tagged_Type (Target_Typ)
+                           and then not Is_Class_Wide_Type (Target_Typ)
+                           and then Is_Tagged_Type (Operand_Typ)
+                           and then not Is_Class_Wide_Type (Operand_Typ)
+                           and then Is_Ancestor (Target_Typ, Operand_Typ))
+                        then
+                           if Ekind_In
+                             (F, E_Out_Parameter, E_In_Out_Parameter)
+                           then
+                              Check_SPARK_Restriction
+                                ("ancestor conversion is the only permitted "
+                                 & "view conversion", A);
+                           else
+                              Check_SPARK_Restriction
+                                ("ancestor conversion required", A);
+                           end if;
 
-            --  Save_Actual (A,
-            --    Ekind (F) /= E_In_Parameter or else Is_Access_Type (F_Typ));
-            --  Why is this code commented out ???
+                        else
+                           null;
+                        end if;
+                     end;
+
+                  else
+                     Check_SPARK_Restriction ("object required", A);
+                  end if;
+
+               --  In formal mode, the only view conversions are those
+               --  involving ancestor conversion of an extended type.
+
+               elsif Nkind (A) = N_Type_Conversion
+                 and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
+               then
+                  Check_SPARK_Restriction
+                    ("ancestor conversion is the only permitted view "
+                     & "conversion", A);
+               end if;
+            end if;
+
+            --  Save actual for subsequent check on order dependence, and
+            --  indicate whether actual is modifiable. For AI05-0144-2.
+
+            Save_Actual (A, Ekind (F) /= E_In_Parameter);
 
             --  For mode IN, if actual is an entity, and the type of the formal
             --  has warnings suppressed, then we reset Never_Set_In_Source for
@@ -3573,7 +3735,7 @@ package body Sem_Res is
 
                if Is_Scalar_Type (A_Typ)
                  or else (Ekind (F) = E_In_Parameter
-                            and then not Is_Partially_Initialized_Type (A_Typ))
+                           and then not Is_Partially_Initialized_Type (A_Typ))
                then
                   Check_Unset_Reference (A);
                end if;
@@ -3618,7 +3780,13 @@ package body Sem_Res is
                --  Is_OK_Variable_For_Out_Formal generates the required
                --  reference in this case.
 
-               if not Is_OK_Variable_For_Out_Formal (A) then
+               --  A call to an initialization procedure for an aggregate
+               --  component may initialize a nested component of a constant
+               --  designated object. In this context the object is variable.
+
+               if not Is_OK_Variable_For_Out_Formal (A)
+                 and then not Is_Init_Proc (Nam)
+               then
                   Error_Msg_NE ("actual for& must be a variable", A, F);
                end if;
 
@@ -3671,7 +3839,7 @@ package body Sem_Res is
                  and then Has_Discriminants (F_Typ)
                  and then Is_Constrained (F_Typ)
                  and then (not Is_Derived_Type (F_Typ)
-                             or else Comes_From_Source (Nam))
+                            or else Comes_From_Source (Nam))
                then
                   Apply_Discriminant_Check (A, F_Typ);
 
@@ -3729,12 +3897,10 @@ package body Sem_Res is
                else
                   if Is_Scalar_Type (F_Typ) then
                      Apply_Scalar_Range_Check (A, A_Typ, F_Typ);
-
                   elsif Is_Array_Type (F_Typ)
                     and then Ekind (F) = E_Out_Parameter
                   then
                      Apply_Length_Check (A, F_Typ);
-
                   else
                      Apply_Range_Check (A, A_Typ, F_Typ);
                   end if;
@@ -3760,16 +3926,16 @@ package body Sem_Res is
                if Is_Atomic_Object (A)
                  and then not Is_Atomic (Etype (F))
                then
-                  Error_Msg_N
-                    ("cannot pass atomic argument to non-atomic formal",
-                     N);
+                  Error_Msg_NE
+                    ("cannot pass atomic argument to non-atomic formal&",
+                     A, F);
 
                elsif Is_Volatile_Object (A)
                  and then not Is_Volatile (Etype (F))
                then
-                  Error_Msg_N
-                    ("cannot pass volatile argument to non-volatile formal",
-                     N);
+                  Error_Msg_NE
+                    ("cannot pass volatile argument to non-volatile formal&",
+                     A, F);
                end if;
             end if;
 
@@ -3816,14 +3982,17 @@ package body Sem_Res is
                     ("& is not a dispatching operation of &!", A, Nam);
                end if;
 
+            --  Apply the checks described in 3.10.2(27): if the context is a
+            --  specific access-to-object, the actual cannot be class-wide.
+            --  Use base type to exclude access_to_subprogram cases.
+
             elsif Is_Access_Type (A_Typ)
               and then Is_Access_Type (F_Typ)
-              and then Ekind (F_Typ) /= E_Access_Subprogram_Type
-              and then Ekind (F_Typ) /= E_Anonymous_Access_Subprogram_Type
+              and then not Is_Access_Subprogram_Type (Base_Type (F_Typ))
               and then (Is_Class_Wide_Type (Designated_Type (A_Typ))
                          or else (Nkind (A) = N_Attribute_Reference
                                    and then
-                                     Is_Class_Wide_Type (Etype (Prefix (A)))))
+                                  Is_Class_Wide_Type (Etype (Prefix (A)))))
               and then not Is_Class_Wide_Type (Designated_Type (F_Typ))
               and then not Is_Controlling_Formal (F)
 
@@ -3837,9 +4006,7 @@ package body Sem_Res is
                Error_Msg_N
                  ("access to class-wide argument not allowed here!", A);
 
-               if Is_Subprogram (Nam)
-                 and then Comes_From_Source (Nam)
-               then
+               if Is_Subprogram (Nam) and then Comes_From_Source (Nam) then
                   Error_Msg_Node_2 := Designated_Type (F_Typ);
                   Error_Msg_NE
                     ("& is not a dispatching operation of &!", A, Nam);
@@ -3849,9 +4016,14 @@ package body Sem_Res is
             Eval_Actual (A);
 
             --  If it is a named association, treat the selector_name as a
-            --  proper identifier, and mark the corresponding entity.
+            --  proper identifier, and mark the corresponding entity. Ignore
+            --  this reference in Alfa mode, as it refers to an entity not in
+            --  scope at the point of reference, so the reference should be
+            --  ignored for computing effects of subprograms.
 
-            if Nkind (Parent (A)) = N_Parameter_Association then
+            if Nkind (Parent (A)) = N_Parameter_Association
+              and then not Alfa_Mode
+            then
                Set_Entity (Selector_Name (Parent (A)), F);
                Generate_Reference (F, Selector_Name (Parent (A)));
                Set_Etype (Selector_Name (Parent (A)), F_Typ);
@@ -3881,7 +4053,8 @@ package body Sem_Res is
    -----------------------
 
    procedure Resolve_Allocator (N : Node_Id; Typ : Entity_Id) is
-      E        : constant Node_Id := Expression (N);
+      Desig_T  : constant Entity_Id := Designated_Type (Typ);
+      E        : constant Node_Id   := Expression (N);
       Subtyp   : Entity_Id;
       Discrim  : Entity_Id;
       Constr   : Node_Id;
@@ -3903,40 +4076,6 @@ package body Sem_Res is
       --  If the allocator is an actual in a call, it is allowed to be class-
       --  wide when the context is not because it is a controlling actual.
 
-      procedure Propagate_Coextensions (Root : Node_Id);
-      --  Propagate all nested coextensions which are located one nesting
-      --  level down the tree to the node Root. Example:
-      --
-      --    Top_Record
-      --       Level_1_Coextension
-      --          Level_2_Coextension
-      --
-      --  The algorithm is paired with delay actions done by the Expander. In
-      --  the above example, assume all coextensions are controlled types.
-      --  The cycle of analysis, resolution and expansion will yield:
-      --
-      --  1) Analyze Top_Record
-      --  2) Analyze Level_1_Coextension
-      --  3) Analyze Level_2_Coextension
-      --  4) Resolve Level_2_Coextension. The allocator is marked as a
-      --       coextension.
-      --  5) Expand Level_2_Coextension. A temporary variable Temp_1 is
-      --       generated to capture the allocated object. Temp_1 is attached
-      --       to the coextension chain of Level_2_Coextension.
-      --  6) Resolve Level_1_Coextension. The allocator is marked as a
-      --       coextension. A forward tree traversal is performed which finds
-      --       Level_2_Coextension's list and copies its contents into its
-      --       own list.
-      --  7) Expand Level_1_Coextension. A temporary variable Temp_2 is
-      --       generated to capture the allocated object. Temp_2 is attached
-      --       to the coextension chain of Level_1_Coextension. Currently, the
-      --       contents of the list are [Temp_2, Temp_1].
-      --  8) Resolve Top_Record. A forward tree traversal is performed which
-      --       finds Level_1_Coextension's list and copies its contents into
-      --       its own list.
-      --  9) Expand Top_Record. Generate finalization calls for Temp_1 and
-      --       Temp_2 and attach them to Top_Record's finalization list.
-
       -------------------------------------------
       -- Check_Allocator_Discrim_Accessibility --
       -------------------------------------------
@@ -3947,7 +4086,7 @@ package body Sem_Res is
       is
       begin
          if Type_Access_Level (Etype (Disc_Exp)) >
-            Type_Access_Level (Alloc_Typ)
+            Deepest_Type_Access_Level (Alloc_Typ)
          then
             Error_Msg_N
               ("operand type has deeper level than allocator type", Disc_Exp);
@@ -3956,10 +4095,10 @@ package body Sem_Res is
          --  object must not be deeper than that of the allocator's type.
 
          elsif Nkind (Disc_Exp) = N_Attribute_Reference
-           and then Get_Attribute_Id (Attribute_Name (Disc_Exp))
-                      Attribute_Access
-           and then Object_Access_Level (Prefix (Disc_Exp))
-                      Type_Access_Level (Alloc_Typ)
+           and then Get_Attribute_Id (Attribute_Name (Disc_Exp)) =
+                      Attribute_Access
+           and then Object_Access_Level (Prefix (Disc_Exp)) >
+                      Deepest_Type_Access_Level (Alloc_Typ)
          then
             Error_Msg_N
               ("prefix of attribute has deeper level than allocator type",
@@ -3970,8 +4109,8 @@ package body Sem_Res is
 
          elsif Ekind (Etype (Disc_Exp)) = E_Anonymous_Access_Type
            and then Nkind (Disc_Exp) = N_Selected_Component
-           and then Object_Access_Level (Prefix (Disc_Exp))
-                      Type_Access_Level (Alloc_Typ)
+           and then Object_Access_Level (Prefix (Disc_Exp)) >
+                      Deepest_Type_Access_Level (Alloc_Typ)
          then
             Error_Msg_N
               ("access discriminant has deeper level than allocator type",
@@ -3990,140 +4129,14 @@ package body Sem_Res is
 
       function In_Dispatching_Context return Boolean is
          Par : constant Node_Id := Parent (N);
-      begin
-         return Nkind_In (Par, N_Function_Call, N_Procedure_Call_Statement)
-           and then Is_Entity_Name (Name (Par))
-           and then Is_Dispatching_Operation (Entity (Name (Par)));
-      end In_Dispatching_Context;
-
-      ----------------------------
-      -- Propagate_Coextensions --
-      ----------------------------
-
-      procedure Propagate_Coextensions (Root : Node_Id) is
-
-         procedure Copy_List (From : Elist_Id; To : Elist_Id);
-         --  Copy the contents of list From into list To, preserving the
-         --  order of elements.
-
-         function Process_Allocator (Nod : Node_Id) return Traverse_Result;
-         --  Recognize an allocator or a rewritten allocator node and add it
-         --  along with its nested coextensions to the list of Root.
-
-         ---------------
-         -- Copy_List --
-         ---------------
-
-         procedure Copy_List (From : Elist_Id; To : Elist_Id) is
-            From_Elmt : Elmt_Id;
-         begin
-            From_Elmt := First_Elmt (From);
-            while Present (From_Elmt) loop
-               Append_Elmt (Node (From_Elmt), To);
-               Next_Elmt (From_Elmt);
-            end loop;
-         end Copy_List;
-
-         -----------------------
-         -- Process_Allocator --
-         -----------------------
-
-         function Process_Allocator (Nod : Node_Id) return Traverse_Result is
-            Orig_Nod : Node_Id := Nod;
-
-         begin
-            --  This is a possible rewritten subtype indication allocator. Any
-            --  nested coextensions will appear as discriminant constraints.
-
-            if Nkind (Nod) = N_Identifier
-              and then Present (Original_Node (Nod))
-              and then Nkind (Original_Node (Nod)) = N_Subtype_Indication
-            then
-               declare
-                  Discr      : Node_Id;
-                  Discr_Elmt : Elmt_Id;
-
-               begin
-                  if Is_Record_Type (Entity (Nod)) then
-                     Discr_Elmt :=
-                       First_Elmt (Discriminant_Constraint (Entity (Nod)));
-                     while Present (Discr_Elmt) loop
-                        Discr := Node (Discr_Elmt);
-
-                        if Nkind (Discr) = N_Identifier
-                          and then Present (Original_Node (Discr))
-                          and then Nkind (Original_Node (Discr)) = N_Allocator
-                          and then Present (Coextensions (
-                                     Original_Node (Discr)))
-                        then
-                           if No (Coextensions (Root)) then
-                              Set_Coextensions (Root, New_Elmt_List);
-                           end if;
-
-                           Copy_List
-                             (From => Coextensions (Original_Node (Discr)),
-                              To   => Coextensions (Root));
-                        end if;
-
-                        Next_Elmt (Discr_Elmt);
-                     end loop;
-
-                     --  There is no need to continue the traversal of this
-                     --  subtree since all the information has already been
-                     --  propagated.
-
-                     return Skip;
-                  end if;
-               end;
-
-            --  Case of either a stand alone allocator or a rewritten allocator
-            --  with an aggregate.
-
-            else
-               if Present (Original_Node (Nod)) then
-                  Orig_Nod := Original_Node (Nod);
-               end if;
-
-               if Nkind (Orig_Nod) = N_Allocator then
-
-                  --  Propagate the list of nested coextensions to the Root
-                  --  allocator. This is done through list copy since a single
-                  --  allocator may have multiple coextensions. Do not touch
-                  --  coextensions roots.
-
-                  if not Is_Coextension_Root (Orig_Nod)
-                    and then Present (Coextensions (Orig_Nod))
-                  then
-                     if No (Coextensions (Root)) then
-                        Set_Coextensions (Root, New_Elmt_List);
-                     end if;
-
-                     Copy_List
-                       (From => Coextensions (Orig_Nod),
-                        To   => Coextensions (Root));
-                  end if;
-
-                  --  There is no need to continue the traversal of this
-                  --  subtree since all the information has already been
-                  --  propagated.
-
-                  return Skip;
-               end if;
-            end if;
-
-            --  Keep on traversing, looking for the next allocator
-
-            return OK;
-         end Process_Allocator;
-
-         procedure Process_Allocators is
-           new Traverse_Proc (Process_Allocator);
-
-      --  Start of processing for Propagate_Coextensions
 
       begin
-         Process_Allocators (Expression (Root));
-      end Propagate_Coextensions;
+         return
+           Nkind_In (Par, N_Function_Call,
+                          N_Procedure_Call_Statement)
+             and then Is_Entity_Name (Name (Par))
+             and then Is_Dispatching_Operation (Entity (Name (Par)));
+      end In_Dispatching_Context;
 
    --  Start of processing for Resolve_Allocator
 
@@ -4143,7 +4156,7 @@ package body Sem_Res is
 
       if Nkind (E) = N_Qualified_Expression then
          if Is_Class_Wide_Type (Etype (E))
-           and then not Is_Class_Wide_Type (Designated_Type (Typ))
+           and then not Is_Class_Wide_Type (Desig_T)
            and then not In_Dispatching_Context
          then
             Error_Msg_N
@@ -4157,7 +4170,7 @@ package body Sem_Res is
          --  class-wide matching is not allowed.
 
          if (Is_Class_Wide_Type (Etype (Expression (E)))
-                 or else Is_Class_Wide_Type (Etype (E)))
+              or else Is_Class_Wide_Type (Etype (E)))
            and then Base_Type (Etype (Expression (E))) /= Base_Type (Etype (E))
          then
             Wrong_Type (Expression (E), Etype (E));
@@ -4287,7 +4300,7 @@ package body Sem_Res is
       --  Expand_Allocator_Expression).
 
       if Ada_Version >= Ada_2005
-        and then Is_Class_Wide_Type (Designated_Type (Typ))
+        and then Is_Class_Wide_Type (Desig_T)
       then
          declare
             Exp_Typ : Entity_Id;
@@ -4301,7 +4314,9 @@ package body Sem_Res is
                Exp_Typ := Entity (E);
             end if;
 
-            if Type_Access_Level (Exp_Typ) > Type_Access_Level (Typ) then
+            if Type_Access_Level (Exp_Typ) >
+                 Deepest_Type_Access_Level (Typ)
+            then
                if In_Instance_Body then
                   Error_Msg_N ("?type in allocator has deeper level than" &
                                " designated class-wide type", E);
@@ -4329,9 +4344,9 @@ package body Sem_Res is
       if No_Pool_Assigned (Typ) then
          Error_Msg_N ("allocation from empty storage pool!", N);
 
-      --  If the context is an unchecked conversion, as may happen within
-      --  an inlined subprogram, the allocator is being resolved with its
-      --  own anonymous type. In that case, if the target type has a specific
+      --  If the context is an unchecked conversion, as may happen within an
+      --  inlined subprogram, the allocator is being resolved with its own
+      --  anonymous type. In that case, if the target type has a specific
       --  storage pool, it must be inherited explicitly by the allocator type.
 
       elsif Nkind (Parent (N)) = N_Unchecked_Type_Conversion
@@ -4345,6 +4360,15 @@ package body Sem_Res is
          Check_Restriction (No_Anonymous_Allocators, N);
       end if;
 
+      --  Check that an allocator with task parts isn't for a nested access
+      --  type when restriction No_Task_Hierarchy applies.
+
+      if not Is_Library_Level_Entity (Base_Type (Typ))
+        and then Has_Task (Base_Type (Desig_T))
+      then
+         Check_Restriction (No_Task_Hierarchy, N);
+      end if;
+
       --  An erroneous allocator may be rewritten as a raise Program_Error
       --  statement.
 
@@ -4357,6 +4381,26 @@ package body Sem_Res is
            and then Nkind (Associated_Node_For_Itype (Typ)) =
                       N_Discriminant_Specification
          then
+            declare
+               Discr : constant Entity_Id :=
+                         Defining_Identifier (Associated_Node_For_Itype (Typ));
+
+            begin
+               --  Ada 2012 AI05-0052: If the designated type of the allocator
+               --  is limited, then the allocator shall not be used to define
+               --  the value of an access discriminant unless the discriminated
+               --  type is immutably limited.
+
+               if Ada_Version >= Ada_2012
+                 and then Is_Limited_Type (Desig_T)
+                 and then not Is_Immutably_Limited_Type (Scope (Discr))
+               then
+                  Error_Msg_N
+                    ("only immutably limited types can have anonymous "
+                     & "access discriminants designating a limited type", N);
+               end if;
+            end;
+
             --  Avoid marking an allocator as a dynamic coextension if it is
             --  within a static construct.
 
@@ -4370,13 +4414,35 @@ package body Sem_Res is
             Set_Is_Dynamic_Coextension (N, False);
             Set_Is_Static_Coextension  (N, False);
          end if;
+      end if;
 
-         --  There is no need to propagate any nested coextensions if they
-         --  are marked as static since they will be rewritten on the spot.
+      --  Report a simple error: if the designated object is a local task,
+      --  its body has not been seen yet, and its activation will fail an
+      --  elaboration check.
 
-         if not Is_Static_Coextension (N) then
-            Propagate_Coextensions (N);
-         end if;
+      if Is_Task_Type (Desig_T)
+        and then Scope (Base_Type (Desig_T)) = Current_Scope
+        and then Is_Compilation_Unit (Current_Scope)
+        and then Ekind (Current_Scope) = E_Package
+        and then not In_Package_Body (Current_Scope)
+      then
+         Error_Msg_N ("cannot activate task before body seen?", N);
+         Error_Msg_N ("\Program_Error will be raised at run time?", N);
+      end if;
+
+      --  Ada 2012 (AI05-0111-3): Issue a warning whenever allocating a task
+      --  or a type containing tasks on a subpool since the deallocation of
+      --  the subpool may lead to undefined task behavior. Perform the check
+      --  only when the allocator has not been converted into a Program_Error
+      --  due to a previous error.
+
+      if Ada_Version >= Ada_2012
+        and then Nkind (N) = N_Allocator
+        and then Present (Subpool_Handle_Name (N))
+        and then Has_Task (Desig_T)
+      then
+         Error_Msg_N ("?allocation of task on subpool may lead to " &
+                      "undefined behavior", N);
       end if;
    end Resolve_Allocator;
 
@@ -4542,7 +4608,6 @@ package body Sem_Res is
             Get_First_Interp (N, Index, It);
             while Present (It.Typ) loop
                if Base_Type (It.Typ) = Base_Type (Standard_Integer) then
-
                   if Analyzed (N) then
                      Error_Msg_N ("ambiguous operand in fixed operation", N);
                   else
@@ -4550,7 +4615,6 @@ package body Sem_Res is
                   end if;
 
                elsif Is_Fixed_Point_Type (It.Typ) then
-
                   if Analyzed (N) then
                      Error_Msg_N ("ambiguous operand in fixed operation", N);
                   else
@@ -4619,20 +4683,22 @@ package body Sem_Res is
          Resolve_Intrinsic_Operator (N, Typ);
          return;
 
-      --  Special-case for mixed-mode universal expressions or fixed point
-      --  type operation: each argument is resolved separately. The same
-      --  treatment is required if one of the operands of a fixed point
-      --  operation is universal real, since in this case we don't do a
-      --  conversion to a specific fixed-point type (instead the expander
-      --  takes care of the case).
+      --  Special-case for mixed-mode universal expressions or fixed point type
+      --  operation: each argument is resolved separately. The same treatment
+      --  is required if one of the operands of a fixed point operation is
+      --  universal real, since in this case we don't do a conversion to a
+      --  specific fixed-point type (instead the expander handles the case).
+
+      --  Set the type of the node to its universal interpretation because
+      --  legality checks on an exponentiation operand need the context.
 
       elsif (B_Typ = Universal_Integer or else B_Typ = Universal_Real)
         and then Present (Universal_Interpretation (L))
         and then Present (Universal_Interpretation (R))
       then
+         Set_Etype (N, B_Typ);
          Resolve (L, Universal_Interpretation (L));
          Resolve (R, Universal_Interpretation (R));
-         Set_Etype (N, B_Typ);
 
       elsif (B_Typ = Universal_Real
               or else Etype (N) = Universal_Fixed
@@ -4648,8 +4714,8 @@ package body Sem_Res is
             Check_For_Visible_Operator (N, B_Typ);
          end if;
 
-         --  If context is a fixed type and one operand is integer, the
-         --  other is resolved with the type of the context.
+         --  If context is a fixed type and one operand is integer, the other
+         --  is resolved with the type of the context.
 
          if Is_Fixed_Point_Type (B_Typ)
            and then (Base_Type (TL) = Base_Type (Standard_Integer)
@@ -4703,7 +4769,9 @@ package body Sem_Res is
                end if;
 
                --  The expected type is "any real type" in contexts like
+
                --    type T is delta <universal_fixed-expression> ...
+
                --  in which case we need to set the type to Universal_Real
                --  so that static expression evaluation will work properly.
 
@@ -4724,8 +4792,8 @@ package body Sem_Res is
 
          elsif Etype (N) = Any_Fixed then
 
-            --  If no previous errors, this is only possible if one operand
-            --  is overloaded and the context is universal. Resolve as such.
+            --  If no previous errors, this is only possible if one operand is
+            --  overloaded and the context is universal. Resolve as such.
 
             Set_Etype (N, B_Typ);
          end if;
@@ -4771,6 +4839,20 @@ package body Sem_Res is
       Generate_Operator_Reference (N, Typ);
       Eval_Arithmetic_Op (N);
 
+      --  In SPARK, a multiplication or division with operands of fixed point
+      --  types shall be qualified or explicitly converted to identify the
+      --  result type.
+
+      if (Is_Fixed_Point_Type (Etype (L))
+           or else Is_Fixed_Point_Type (Etype (R)))
+        and then Nkind_In (N, N_Op_Multiply, N_Op_Divide)
+        and then
+          not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion)
+      then
+         Check_SPARK_Restriction
+           ("operation should be qualified or explicitly converted", N);
+      end if;
+
       --  Set overflow and division checking bit. Much cleverer code needed
       --  here eventually and perhaps the Resolve routines should be separated
       --  for the various arithmetic operations, since they will need
@@ -4790,18 +4872,38 @@ package body Sem_Res is
 
             if Compile_Time_Known_Value (Rop)
               and then ((Is_Integer_Type (Etype (Rop))
-                           and then Expr_Value (Rop) = Uint_0)
-                          or else
-                        (Is_Real_Type (Etype (Rop))
-                           and then Expr_Value_R (Rop) = Ureal_0))
+                          and then Expr_Value (Rop) = Uint_0)
+                         or else
+                           (Is_Real_Type (Etype (Rop))
+                             and then Expr_Value_R (Rop) = Ureal_0))
             then
-               --  Specialize the warning message according to the operation
+               --  Specialize the warning message according to the operation.
+               --  The following warnings are for the case
 
                case Nkind (N) is
                   when N_Op_Divide =>
-                     Apply_Compile_Time_Constraint_Error
-                       (N, "division by zero?", CE_Divide_By_Zero,
-                        Loc => Sloc (Right_Opnd (N)));
+
+                     --  For division, we have two cases, for float division
+                     --  of an unconstrained float type, on a machine where
+                     --  Machine_Overflows is false, we don't get an exception
+                     --  at run-time, but rather an infinity or Nan. The Nan
+                     --  case is pretty obscure, so just warn about infinities.
+
+                     if Is_Floating_Point_Type (Typ)
+                       and then not Is_Constrained (Typ)
+                       and then not Machine_Overflows_On_Target
+                     then
+                        Error_Msg_N
+                          ("float division by zero, " &
+                           "may generate '+'/'- infinity?", Right_Opnd (N));
+
+                        --  For all other cases, we get a Constraint_Error
+
+                     else
+                        Apply_Compile_Time_Constraint_Error
+                          (N, "division by zero?", CE_Divide_By_Zero,
+                           Loc => Sloc (Right_Opnd (N)));
+                     end if;
 
                   when N_Op_Rem =>
                      Apply_Compile_Time_Constraint_Error
@@ -4861,7 +4963,7 @@ package body Sem_Res is
                --  expander does, so we match its logic here).
 
                --  The second case is mod where either operand can be negative.
-               --  In this case, the back end has to generate additonal tests.
+               --  In this case, the back end has to generate additional tests.
 
                if (Nkind (N) = N_Op_Rem and then (LNeg and RNeg))
                     or else
@@ -5141,12 +5243,13 @@ package body Sem_Res is
       elsif (Needs_No_Actuals (Nam) or else Needs_One_Actual (Nam))
         and then
           ((Is_Array_Type (Etype (Nam))
-                   and then Covers (Typ, Component_Type (Etype (Nam))))
+             and then Covers (Typ, Component_Type (Etype (Nam))))
              or else (Is_Access_Type (Etype (Nam))
-                        and then Is_Array_Type (Designated_Type (Etype (Nam)))
-                        and then
-                          Covers (Typ,
-                            Component_Type (Designated_Type (Etype (Nam))))))
+                       and then Is_Array_Type (Designated_Type (Etype (Nam)))
+                       and then
+                         Covers
+                          (Typ,
+                           Component_Type (Designated_Type (Etype (Nam))))))
       then
          declare
             Index_Node : Node_Id;
@@ -5255,8 +5358,8 @@ package body Sem_Res is
            and then Check_Infinite_Recursion (N)
          then
             --  Here we detected and flagged an infinite recursion, so we do
-            --  not need to test the case below for further warnings. Also if
-            --  we now have a raise SE node, we are all done.
+            --  not need to test the case below for further warnings. Also we
+            --  are all done if we now have a raise SE node.
 
             if Nkind (N) = N_Raise_Storage_Error then
                return;
@@ -5298,6 +5401,9 @@ package body Sem_Res is
                      --  decrease false positives, without losing too many good
                      --  warnings. The idea is that these previous statements
                      --  may affect global variables the procedure depends on.
+                     --  We also exclude raise statements, that may arise from
+                     --  constraint checks and are probably unrelated to the
+                     --  intended control flow.
 
                      if Nkind (N) = N_Procedure_Call_Statement
                        and then Is_List_Member (N)
@@ -5307,7 +5413,10 @@ package body Sem_Res is
                         begin
                            P := Prev (N);
                            while Present (P) loop
-                              if Nkind (P) /= N_Assignment_Statement then
+                              if not Nkind_In (P,
+                                N_Assignment_Statement,
+                                N_Raise_Constraint_Error)
+                              then
                                  exit Scope_Loop;
                               end if;
 
@@ -5415,7 +5524,7 @@ package body Sem_Res is
       then
          null;
 
-      elsif Expander_Active
+      elsif Full_Expander_Active
         and then Is_Type (Etype (Nam))
         and then Requires_Transient_Scope (Etype (Nam))
         and then
@@ -5558,7 +5667,7 @@ package body Sem_Res is
       then
          Generate_Reference (Nam, Subp, 'R');
 
-      --  Normal case, not a dispatching call. Generate a call reference.
+      --  Normal case, not a dispatching call: generate a call reference
 
       else
          Generate_Reference (Nam, Subp, 's');
@@ -5571,9 +5680,10 @@ package body Sem_Res is
       --  Check for violation of restriction No_Specific_Termination_Handlers
       --  and warn on a potentially blocking call to Abort_Task.
 
-      if Is_RTE (Nam, RE_Set_Specific_Handler)
-           or else
-         Is_RTE (Nam, RE_Specific_Handler)
+      if Restriction_Check_Required (No_Specific_Termination_Handlers)
+        and then (Is_RTE (Nam, RE_Set_Specific_Handler)
+                    or else
+                  Is_RTE (Nam, RE_Specific_Handler))
       then
          Check_Restriction (No_Specific_Termination_Handlers, N);
 
@@ -5581,10 +5691,15 @@ package body Sem_Res is
          Check_Potentially_Blocking_Operation (N);
       end if;
 
-      --  A call to Ada.Real_Time.Timing_Events.Set_Handler violates
-      --  restriction No_Relative_Delay (AI-0211).
+      --  A call to Ada.Real_Time.Timing_Events.Set_Handler to set a relative
+      --  timing event violates restriction No_Relative_Delay (AI-0211). We
+      --  need to check the second argument to determine whether it is an
+      --  absolute or relative timing event.
 
-      if Is_RTE (Nam, RE_Set_Handler) then
+      if Restriction_Check_Required (No_Relative_Delay)
+        and then Is_RTE (Nam, RE_Set_Handler)
+        and then Is_RTE (Etype (Next_Actual (First_Actual (N))), RE_Time_Span)
+      then
          Check_Restriction (No_Relative_Delay, N);
       end if;
 
@@ -5597,6 +5712,61 @@ package body Sem_Res is
          Check_For_Eliminated_Subprogram (Subp, Nam);
       end if;
 
+      --  In formal mode, the primitive operations of a tagged type or type
+      --  extension do not include functions that return the tagged type.
+
+      --  Commented out as the call to Is_Inherited_Operation_For_Type may
+      --  cause an error because the type entity of the parent node of
+      --  Entity (Name (N) may not be set. ???
+      --  So why not just add a guard ???
+
+--      if Nkind (N) = N_Function_Call
+--        and then Is_Tagged_Type (Etype (N))
+--        and then Is_Entity_Name (Name (N))
+--        and then Is_Inherited_Operation_For_Type
+--                   (Entity (Name (N)), Etype (N))
+--      then
+--         Check_SPARK_Restriction ("function not inherited", N);
+--      end if;
+
+      --  Implement rule in 12.5.1 (23.3/2): In an instance, if the actual is
+      --  class-wide and the call dispatches on result in a context that does
+      --  not provide a tag, the call raises Program_Error.
+
+      if Nkind (N) = N_Function_Call
+        and then In_Instance
+        and then Is_Generic_Actual_Type (Typ)
+        and then Is_Class_Wide_Type (Typ)
+        and then Has_Controlling_Result (Nam)
+        and then Nkind (Parent (N)) = N_Object_Declaration
+      then
+         --  Verify that none of the formals are controlling
+
+         declare
+            Call_OK : Boolean := False;
+            F       : Entity_Id;
+
+         begin
+            F := First_Formal (Nam);
+            while Present (F) loop
+               if Is_Controlling_Formal (F) then
+                  Call_OK := True;
+                  exit;
+               end if;
+
+               Next_Formal (F);
+            end loop;
+
+            if not Call_OK then
+               Error_Msg_N ("!? cannot determine tag of result", N);
+               Error_Msg_N ("!? Program_Error will be raised", N);
+               Insert_Action (N,
+                 Make_Raise_Program_Error (Sloc (N),
+                    Reason => PE_Explicit_Raise));
+            end if;
+         end;
+      end if;
+
       --  All done, evaluate call and deal with elaboration issues
 
       Eval_Call (N);
@@ -5651,16 +5821,16 @@ package body Sem_Res is
       elsif B_Typ = Any_Character then
          return;
 
-      --  For Standard.Character or a type derived from it, check that
-      --  the literal is in range
+      --  For Standard.Character or a type derived from it, check that the
+      --  literal is in range.
 
       elsif Root_Type (B_Typ) = Standard_Character then
          if In_Character_Range (UI_To_CC (Char_Literal_Value (N))) then
             return;
          end if;
 
-      --  For Standard.Wide_Character or a type derived from it, check
-      --  that the literal is in range
+      --  For Standard.Wide_Character or a type derived from it, check that the
+      --  literal is in range.
 
       elsif Root_Type (B_Typ) = Standard_Wide_Character then
          if In_Wide_Character_Range (UI_To_CC (Char_Literal_Value (N))) then
@@ -5696,8 +5866,8 @@ package body Sem_Res is
       end if;
 
       --  If we fall through, then the literal does not match any of the
-      --  entries of the enumeration type. This isn't just a constraint
-      --  error situation, it is an illegality (see RM 4.2).
+      --  entries of the enumeration type. This isn't just a constraint error
+      --  situation, it is an illegality (see RM 4.2).
 
       Error_Msg_NE
         ("character not defined for }", N, First_Subtype (B_Typ));
@@ -5708,9 +5878,9 @@ package body Sem_Res is
    ---------------------------
 
    --  Context requires a boolean type, and plays no role in resolution.
-   --  Processing identical to that for equality operators. The result
-   --  type is the base type, which matters when pathological subtypes of
-   --  booleans with limited ranges are used.
+   --  Processing identical to that for equality operators. The result type is
+   --  the base type, which matters when pathological subtypes of booleans with
+   --  limited ranges are used.
 
    procedure Resolve_Comparison_Op (N : Node_Id; Typ : Entity_Id) is
       L : constant Node_Id := Left_Opnd (N);
@@ -5768,6 +5938,20 @@ package body Sem_Res is
       Generate_Operator_Reference (N, T);
       Check_Low_Bound_Tested (N);
 
+      --  In SPARK, ordering operators <, <=, >, >= are not defined for Boolean
+      --  types or array types except String.
+
+      if Is_Boolean_Type (T) then
+         Check_SPARK_Restriction
+           ("comparison is not defined on Boolean type", N);
+
+      elsif Is_Array_Type (T)
+        and then Base_Type (T) /= Standard_String
+      then
+         Check_SPARK_Restriction
+           ("comparison is not defined on array types other than String", N);
+      end if;
+
       --  Check comparison on unordered enumeration
 
       if Comes_From_Source (N)
@@ -5776,8 +5960,8 @@ package body Sem_Res is
          Error_Msg_N ("comparison on unordered enumeration type?", N);
       end if;
 
-      --  Evaluate the relation (note we do this after the above check
-      --  since this Eval call may change N to True/False.
+      --  Evaluate the relation (note we do this after the above check since
+      --  this Eval call may change N to True/False.
 
       Eval_Relational_Op (N);
    end Resolve_Comparison_Op;
@@ -5789,7 +5973,7 @@ package body Sem_Res is
    procedure Resolve_Conditional_Expression (N : Node_Id; Typ : Entity_Id) is
       Condition : constant Node_Id := First (Expressions (N));
       Then_Expr : constant Node_Id := Next (Condition);
-      Else_Expr : Node_Id := Next (Then_Expr);
+      Else_Expr : Node_Id          := Next (Then_Expr);
 
    begin
       Resolve (Condition, Any_Boolean);
@@ -5857,11 +6041,11 @@ package body Sem_Res is
             Set_Etype (N, Typ);
             Rewrite (Low_Bound (R),
               Make_Attribute_Reference (Sloc (Low_Bound (R)),
-                Prefix =>         New_Occurrence_Of (Typ, Sloc (R)),
+                Prefix         => New_Occurrence_Of (Typ, Sloc (R)),
                 Attribute_Name => Name_First));
             Rewrite (High_Bound (R),
               Make_Attribute_Reference (Sloc (High_Bound (R)),
-                Prefix =>         New_Occurrence_Of (Typ, Sloc (R)),
+                Prefix         => New_Occurrence_Of (Typ, Sloc (R)),
                 Attribute_Name => Name_First));
 
          else
@@ -5961,13 +6145,7 @@ package body Sem_Res is
          then
             null;
 
-         --  Allow reference to type specifically marked as being OK in this
-         --  context (this is used for example for type names in invariants).
-
-         elsif OK_To_Reference (E) then
-            null;
-
-         --  Any other use is an eror
+         --  Any other use is an error
 
          else
             Error_Msg_N
@@ -5993,9 +6171,9 @@ package body Sem_Res is
       elsif Ekind (E) = E_Out_Parameter
         and then Ada_Version = Ada_83
         and then (Nkind (Parent (N)) in N_Op
-                    or else (Nkind (Parent (N)) = N_Assignment_Statement
-                              and then N = Expression (Parent (N)))
-                    or else Nkind (Parent (N)) = N_Explicit_Dereference)
+                   or else (Nkind (Parent (N)) = N_Assignment_Statement
+                             and then N = Expression (Parent (N)))
+                   or else Nkind (Parent (N)) = N_Explicit_Dereference)
       then
          Error_Msg_N ("(Ada 83) illegal reading of out parameter", N);
 
@@ -6110,9 +6288,7 @@ package body Sem_Res is
 
       begin
          if not Has_Discriminants (Tsk)
-           or else (not Is_Entity_Name (Lo)
-                     and then
-                    not Is_Entity_Name (Hi))
+           or else (not Is_Entity_Name (Lo) and then not Is_Entity_Name (Hi))
          then
             return Entry_Index_Type (E);
 
@@ -6133,9 +6309,9 @@ package body Sem_Res is
    --  Start of processing of Resolve_Entry
 
    begin
-      --  Find name of entry being called, and resolve prefix of name
-      --  with its own type. The prefix can be overloaded, and the name
-      --  and signature of the entry must be taken into account.
+      --  Find name of entry being called, and resolve prefix of name with its
+      --  own type. The prefix can be overloaded, and the name and signature of
+      --  the entry must be taken into account.
 
       if Nkind (Entry_Name) = N_Indexed_Component then
 
@@ -6202,8 +6378,7 @@ package body Sem_Res is
         and then Is_Overloaded (Prefix (Entry_Name))
       then
          --  Use the entry name (which must be unique at this point) to find
-         --  the prefix that returns the corresponding task type or protected
-         --  type.
+         --  the prefix that returns the corresponding task/protected type.
 
          declare
             Pref : constant Node_Id := Prefix (Entry_Name);
@@ -6314,17 +6489,17 @@ package body Sem_Res is
          Was_Over := Is_Overloaded (Selector_Name (Prefix (Entry_Name)));
       end if;
 
-      --  We cannot in general check the maximum depth of protected entry
-      --  calls at compile time. But we can tell that any protected entry
-      --  call at all violates a specified nesting depth of zero.
+      --  We cannot in general check the maximum depth of protected entry calls
+      --  at compile time. But we can tell that any protected entry call at all
+      --  violates a specified nesting depth of zero.
 
       if Is_Protected_Type (Scope (Nam)) then
          Check_Restriction (Max_Entry_Queue_Length, N);
       end if;
 
       --  Use context type to disambiguate a protected function that can be
-      --  called without actuals and that returns an array type, and where
-      --  the argument list may be an indexing of the returned value.
+      --  called without actuals and that returns an array type, and where the
+      --  argument list may be an indexing of the returned value.
 
       if Ekind (Nam) = E_Function
         and then Needs_No_Actuals (Nam)
@@ -6335,8 +6510,10 @@ package body Sem_Res is
 
             or else (Is_Access_Type (Etype (Nam))
                       and then Is_Array_Type (Designated_Type (Etype (Nam)))
-                      and then Covers (Typ,
-                        Component_Type (Designated_Type (Etype (Nam))))))
+                      and then
+                        Covers
+                         (Typ,
+                          Component_Type (Designated_Type (Etype (Nam))))))
       then
          declare
             Index_Node : Node_Id;
@@ -6345,12 +6522,11 @@ package body Sem_Res is
             Index_Node :=
               Make_Indexed_Component (Loc,
                 Prefix =>
-                  Make_Function_Call (Loc,
-                    Name => Relocate_Node (Entry_Name)),
+                  Make_Function_Call (Loc, Name => Relocate_Node (Entry_Name)),
                 Expressions => Parameter_Associations (N));
 
-            --  Since we are correcting a node classification error made by
-            --  the parser, we call Replace rather than Rewrite.
+            --  Since we are correcting a node classification error made by the
+            --  parser, we call Replace rather than Rewrite.
 
             Replace (N, Index_Node);
             Set_Etype (Prefix (N), Etype (Nam));
@@ -6365,12 +6541,13 @@ package body Sem_Res is
         and then Current_Scope /= PPC_Wrapper (Nam)
       then
          --  Rewrite as call to the precondition wrapper, adding the task
-         --  object to the list of actuals. If the call is to a member of
-         --  an entry family, include the index as well.
+         --  object to the list of actuals. If the call is to a member of an
+         --  entry family, include the index as well.
 
          declare
             New_Call    : Node_Id;
             New_Actuals : List_Id;
+
          begin
             New_Actuals := New_List (Obj);
 
@@ -6392,8 +6569,8 @@ package body Sem_Res is
       end if;
 
       --  The operation name may have been overloaded. Order the actuals
-      --  according to the formals of the resolved entity, and set the
-      --  return type to that of the operation.
+      --  according to the formals of the resolved entity, and set the return
+      --  type to that of the operation.
 
       if Was_Over then
          Normalize_Actuals (N, Nam, False, Norm_OK);
@@ -6468,7 +6645,7 @@ package body Sem_Res is
       --  Protected functions can return on the secondary stack, in which
       --  case we must trigger the transient scope mechanism.
 
-      elsif Expander_Active
+      elsif Full_Expander_Active
         and then Requires_Transient_Scope (Etype (Nam))
       then
          Establish_Transient_Scope (N, Sec_Stack => True);
@@ -6576,9 +6753,9 @@ package body Sem_Res is
       end if;
 
       if T /= Any_Type then
-         if T = Any_String
-           or else T = Any_Composite
-           or else T = Any_Character
+         if T = Any_String    or else
+            T = Any_Composite or else
+            T = Any_Character
          then
             if T = Any_Character then
                Ambiguous_Character (L);
@@ -6617,6 +6794,26 @@ package body Sem_Res is
          Resolve (L, T);
          Resolve (R, T);
 
+         --  In SPARK, equality operators = and /= for array types other than
+         --  String are only defined when, for each index position, the
+         --  operands have equal static bounds.
+
+         if Is_Array_Type (T) then
+            --  Protect call to Matching_Static_Array_Bounds to avoid costly
+            --  operation if not needed.
+
+            if Restriction_Check_Required (SPARK)
+              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_SPARK_Restriction
+                 ("array types should have matching static bounds", N);
+            end if;
+         end if;
+
          --  If the unique type is a class-wide type then it will be expanded
          --  into a dispatching call to the predefined primitive. Therefore we
          --  check here for potential violation of such restriction.
@@ -6649,7 +6846,7 @@ package body Sem_Res is
            or else Comes_From_Source (Entity (N))
            or else Ekind (Entity (N)) = E_Operator
            or else Is_Intrinsic_Subprogram
-             (Corresponding_Equality (Entity (N)))
+                     (Corresponding_Equality (Entity (N)))
          then
             Eval_Relational_Op (N);
 
@@ -6669,7 +6866,7 @@ package body Sem_Res is
 
          --  Why the Expander_Active test here ???
 
-         if Expander_Active
+         if Full_Expander_Active
            and then
              (Ekind_In (T, E_Anonymous_Access_Type,
                            E_Anonymous_Access_Subprogram_Type)
@@ -6823,8 +7020,10 @@ package body Sem_Res is
                      and then Covers (Typ, Component_Type (It.Typ)))
                  or else (Is_Access_Type (It.Typ)
                             and then Is_Array_Type (Designated_Type (It.Typ))
-                            and then Covers
-                              (Typ, Component_Type (Designated_Type (It.Typ))))
+                            and then
+                              Covers
+                                (Typ,
+                                 Component_Type (Designated_Type (It.Typ))))
                then
                   if Found then
                      It := Disambiguate (P, I1, I, Any_Type);
@@ -6956,11 +7155,35 @@ package body Sem_Res is
       Arg1    : Node_Id;
       Arg2    : Node_Id;
 
+      function Convert_Operand (Opnd : Node_Id) return Node_Id;
+      --  If the operand is a literal, it cannot be the expression in a
+      --  conversion. Use a qualified expression instead.
+
+      function Convert_Operand (Opnd : Node_Id) return Node_Id is
+         Loc : constant Source_Ptr := Sloc (Opnd);
+         Res : Node_Id;
+      begin
+         if Nkind_In (Opnd, N_Integer_Literal, N_Real_Literal) then
+            Res :=
+              Make_Qualified_Expression (Loc,
+                Subtype_Mark => New_Occurrence_Of (Btyp, Loc),
+                Expression   => Relocate_Node (Opnd));
+            Analyze (Res);
+
+         else
+            Res := Unchecked_Convert_To (Btyp, Opnd);
+         end if;
+
+         return Res;
+      end Convert_Operand;
+
+   --  Start of processing for Resolve_Intrinsic_Operator
+
    begin
       --  We must preserve the original entity in a generic setting, so that
       --  the legality of the operation can be verified in an instance.
 
-      if not Expander_Active then
+      if not Full_Expander_Active then
          return;
       end if;
 
@@ -6973,17 +7196,22 @@ package body Sem_Res is
       Set_Entity (N, Op);
       Set_Is_Overloaded (N, False);
 
-      --  If the operand type is private, rewrite with suitable conversions on
-      --  the operands and the result, to expose the proper underlying numeric
-      --  type.
+      --  If the result or operand types are private, rewrite with unchecked
+      --  conversions on the operands and the result, to expose the proper
+      --  underlying numeric type.
 
-      if Is_Private_Type (Typ) then
-         Arg1 := Unchecked_Convert_To (Btyp, Left_Opnd  (N));
+      if Is_Private_Type (Typ)
+        or else Is_Private_Type (Etype (Left_Opnd (N)))
+        or else Is_Private_Type (Etype (Right_Opnd (N)))
+      then
+         Arg1 := Convert_Operand (Left_Opnd (N));
+         --  Unchecked_Convert_To (Btyp, Left_Opnd  (N));
+         --  What on earth is this commented out fragment of code???
 
          if Nkind (N) = N_Op_Expon then
             Arg2 := Unchecked_Convert_To (Standard_Integer, Right_Opnd (N));
          else
-            Arg2 := Unchecked_Convert_To (Btyp, Right_Opnd (N));
+            Arg2 := Convert_Operand (Right_Opnd (N));
          end if;
 
          if Nkind (Arg1) = N_Type_Conversion then
@@ -7122,6 +7350,7 @@ package body Sem_Res is
            ("no modular type available in this context", N);
          Set_Etype (N, Any_Type);
          return;
+
       elsif Is_Modular_Integer_Type (Typ)
         and then Etype (Left_Opnd (N)) = Universal_Integer
         and then Etype (Right_Opnd (N)) = Universal_Integer
@@ -7129,6 +7358,48 @@ package body Sem_Res is
          Check_For_Visible_Operator (N, B_Typ);
       end if;
 
+      --  Replace AND by AND THEN, or OR by OR ELSE, if Short_Circuit_And_Or
+      --  is active and the result type is standard Boolean (do not mess with
+      --  ops that return a nonstandard Boolean type, because something strange
+      --  is going on).
+
+      --  Note: you might expect this replacement to be done during expansion,
+      --  but that doesn't work, because when the pragma Short_Circuit_And_Or
+      --  is used, no part of the right operand of an "and" or "or" operator
+      --  should be executed if the left operand would short-circuit the
+      --  evaluation of the corresponding "and then" or "or else". If we left
+      --  the replacement to expansion time, then run-time checks associated
+      --  with such operands would be evaluated unconditionally, due to being
+      --  before the condition prior to the rewriting as short-circuit forms
+      --  during expansion.
+
+      if Short_Circuit_And_Or
+        and then B_Typ = Standard_Boolean
+        and then Nkind_In (N, N_Op_And, N_Op_Or)
+      then
+         if Nkind (N) = N_Op_And then
+            Rewrite (N,
+              Make_And_Then (Sloc (N),
+                Left_Opnd  => Relocate_Node (Left_Opnd (N)),
+                Right_Opnd => Relocate_Node (Right_Opnd (N))));
+            Analyze_And_Resolve (N, B_Typ);
+
+         --  Case of OR changed to OR ELSE
+
+         else
+            Rewrite (N,
+              Make_Or_Else (Sloc (N),
+                Left_Opnd  => Relocate_Node (Left_Opnd (N)),
+                Right_Opnd => Relocate_Node (Right_Opnd (N))));
+            Analyze_And_Resolve (N, B_Typ);
+         end if;
+
+         --  Return now, since analysis of the rewritten ops will take care of
+         --  other reference bookkeeping and expression folding.
+
+         return;
+      end if;
+
       Resolve (Left_Opnd (N), B_Typ);
       Resolve (Right_Opnd (N), B_Typ);
 
@@ -7138,15 +7409,43 @@ package body Sem_Res is
       Set_Etype (N, B_Typ);
       Generate_Operator_Reference (N, B_Typ);
       Eval_Logical_Op (N);
+
+      --  In SPARK, logical operations AND, OR and XOR for arrays are defined
+      --  only when both operands have same static lower and higher 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
+      then
+         declare
+            Left_Typ  : constant Node_Id := Etype (Left_Opnd (N));
+            Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
+
+         begin
+            --  Protect call to Matching_Static_Array_Bounds to avoid costly
+            --  operation if not needed.
+
+            if Restriction_Check_Required (SPARK)
+              and then Base_Type (Left_Typ) = Base_Type (Right_Typ)
+              and then Left_Typ /= Any_Composite  --  or Left_Opnd in error
+              and then Right_Typ /= Any_Composite  --  or Right_Opnd in error
+              and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ)
+            then
+               Check_SPARK_Restriction
+                 ("array types should have matching static bounds", N);
+            end if;
+         end;
+      end if;
    end Resolve_Logical_Op;
 
    ---------------------------
    -- Resolve_Membership_Op --
    ---------------------------
 
-   --  The context can only be a boolean type, and does not determine
-   --  the arguments. Arguments should be unambiguous, but the preference
-   --  rule for universal types applies.
+   --  The context can only be a boolean type, and does not determine the
+   --  arguments. Arguments should be unambiguous, but the preference rule for
+   --  universal types applies.
 
    procedure Resolve_Membership_Op (N : Node_Id; Typ : Entity_Id) is
       pragma Warnings (Off, Typ);
@@ -7156,8 +7455,8 @@ package body Sem_Res is
       T : Entity_Id;
 
       procedure Resolve_Set_Membership;
-      --  Analysis has determined a unique type for the left operand.
-      --  Use it to resolve the disjuncts.
+      --  Analysis has determined a unique type for the left operand. Use it to
+      --  resolve the disjuncts.
 
       ----------------------------
       -- Resolve_Set_Membership --
@@ -7198,7 +7497,8 @@ package body Sem_Res is
 
       elsif not Is_Overloaded (R)
         and then
-          (Etype (R) = Universal_Integer or else
+          (Etype (R) = Universal_Integer
+             or else
            Etype (R) = Universal_Real)
         and then Is_Overloaded (L)
       then
@@ -7224,7 +7524,6 @@ package body Sem_Res is
         and then not Is_Interface (Etype (R))
       then
          return;
-
       else
          T := Intersect_Types (L, R);
       end if;
@@ -7384,6 +7683,11 @@ package body Sem_Res is
          exit when NN = N;
          NN := Parent (NN);
       end loop;
+
+      if Base_Type (Etype (N)) /= Standard_String then
+         Check_SPARK_Restriction
+           ("result of concatenation should have type String", N);
+      end if;
    end Resolve_Op_Concat;
 
    ---------------------------
@@ -7397,25 +7701,46 @@ package body Sem_Res is
       Is_Comp : Boolean)
    is
       Btyp : constant Entity_Id := Base_Type (Typ);
+      Ctyp : constant Entity_Id := Component_Type (Typ);
 
    begin
       if In_Instance then
          if Is_Comp
            or else (not Is_Overloaded (Arg)
                      and then Etype (Arg) /= Any_Composite
-                     and then Covers (Component_Type (Typ), Etype (Arg)))
+                     and then Covers (Ctyp, Etype (Arg)))
          then
-            Resolve (Arg, Component_Type (Typ));
+            Resolve (Arg, Ctyp);
          else
             Resolve (Arg, Btyp);
          end if;
 
-      elsif Has_Compatible_Type (Arg, Component_Type (Typ)) then
+      --  If both Array & Array and Array & Component are visible, there is a
+      --  potential ambiguity that must be reported.
+
+      elsif Has_Compatible_Type (Arg, Ctyp) then
          if Nkind (Arg) = N_Aggregate
-           and then Is_Composite_Type (Component_Type (Typ))
+           and then Is_Composite_Type (Ctyp)
          then
-            if Is_Private_Type (Component_Type (Typ)) then
+            if Is_Private_Type (Ctyp) then
                Resolve (Arg, Btyp);
+
+            --  If the operation is user-defined and not overloaded use its
+            --  profile. The operation may be a renaming, in which case it has
+            --  been rewritten, and we want the original profile.
+
+            elsif not Is_Overloaded (N)
+              and then Comes_From_Source (Entity (Original_Node (N)))
+              and then Ekind (Entity (Original_Node (N))) = E_Function
+            then
+               Resolve (Arg,
+                 Etype
+                   (Next_Formal (First_Formal (Entity (Original_Node (N))))));
+               return;
+
+            --  Otherwise an aggregate may match both the array type and the
+            --  component type.
+
             else
                Error_Msg_N ("ambiguous aggregate must be qualified", Arg);
                Set_Etype (Arg, Any_Type);
@@ -7450,15 +7775,15 @@ package body Sem_Res is
                          Arg, Component_Type (Typ));
 
                   else
-                     Error_Msg_N
-                       ("ambiguous operand for concatenation!", Arg);
+                     Error_Msg_N ("ambiguous operand for concatenation!", Arg);
+
                      Get_First_Interp (Arg, I, It);
                      while Present (It.Nam) loop
                         Error_Msg_Sloc := Sloc (It.Nam);
 
-                        if Base_Type (It.Typ) = Base_Type (Typ)
-                          or else Base_Type (It.Typ) =
-                            Base_Type (Component_Type (Typ))
+                        if Base_Type (It.Typ) = Btyp
+                             or else
+                           Base_Type (It.Typ) = Base_Type (Ctyp)
                         then
                            Error_Msg_N -- CODEFIX
                              ("\\possible interpretation#", Arg);
@@ -7487,6 +7812,34 @@ package body Sem_Res is
          Resolve (Arg, Btyp);
       end if;
 
+      --  Concatenation is restricted in SPARK: each operand must be either a
+      --  string literal, the name of a string constant, a static character or
+      --  string expression, or another concatenation. Arg cannot be a
+      --  concatenation here as callers of Resolve_Op_Concat_Arg call it
+      --  separately on each final operand, past concatenation operations.
+
+      if Is_Character_Type (Etype (Arg)) then
+         if not Is_Static_Expression (Arg) then
+            Check_SPARK_Restriction
+              ("character operand for concatenation should be static", Arg);
+         end if;
+
+      elsif Is_String_Type (Etype (Arg)) then
+         if not (Nkind_In (Arg, N_Identifier, N_Expanded_Name)
+                  and then Is_Constant_Object (Entity (Arg)))
+           and then not Is_Static_Expression (Arg)
+         then
+            Check_SPARK_Restriction
+              ("string operand for concatenation should be static", Arg);
+         end if;
+
+      --  Do not issue error on an operand that is neither a character nor a
+      --  string, as the error is issued in Resolve_Op_Concat.
+
+      else
+         null;
+      end if;
+
       Check_Unset_Reference (Arg);
    end Resolve_Op_Concat_Arg;
 
@@ -7568,6 +7921,14 @@ package body Sem_Res is
       if Is_Fixed_Point_Type (Typ) and then Comes_From_Source (N) then
          Error_Msg_N ("exponentiation not available for fixed point", N);
          return;
+
+      elsif Nkind (Parent (N)) in N_Op
+        and then Is_Fixed_Point_Type (Etype (Parent (N)))
+        and then Etype (N) = Universal_Real
+        and then Comes_From_Source (N)
+      then
+         Error_Msg_N ("exponentiation not available for fixed point", N);
+         return;
       end if;
 
       if Comes_From_Source (N)
@@ -7617,10 +7978,10 @@ package body Sem_Res is
       B_Typ : Entity_Id;
 
       function Parent_Is_Boolean return Boolean;
-      --  This function determines if the parent node is a boolean operator
-      --  or operation (comparison op, membership test, or short circuit form)
-      --  and the not in question is the left operand of this operation.
-      --  Note that if the not is in parens, then false is returned.
+      --  This function determines if the parent node is a boolean operator or
+      --  operation (comparison op, membership test, or short circuit form) and
+      --  the not in question is the left operand of this operation. Note that
+      --  if the not is in parens, then false is returned.
 
       -----------------------
       -- Parent_Is_Boolean --
@@ -7693,7 +8054,7 @@ package body Sem_Res is
          Set_Etype (N, Any_Type);
          return;
 
-      --  OK resolution of not
+      --  OK resolution of NOT
 
       else
          --  Warn if non-boolean types involved. This is a case like not a < b
@@ -7755,12 +8116,25 @@ package body Sem_Res is
    begin
       Resolve (Expr, Target_Typ);
 
-      --  A qualified expression requires an exact match of the type,
-      --  class-wide matching is not allowed. However, if the qualifying
-      --  type is specific and the expression has a class-wide type, it
-      --  may still be okay, since it can be the result of the expansion
-      --  of a call to a dispatching function, so we also have to check
-      --  class-wideness of the type of the expression's original node.
+      --  Protect call to Matching_Static_Array_Bounds to avoid costly
+      --  operation if not needed.
+
+      if Restriction_Check_Required (SPARK)
+        and then 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_SPARK_Restriction
+           ("array types should have matching static bounds", N);
+      end if;
+
+      --  A qualified expression requires an exact match of the type, class-
+      --  wide matching is not allowed. However, if the qualifying type is
+      --  specific and the expression has a class-wide type, it may still be
+      --  okay, since it can be the result of the expansion of a call to a
+      --  dispatching function, so we also have to check class-wideness of the
+      --  type of the expression's original node.
 
       if (Is_Class_Wide_Type (Target_Typ)
            or else
@@ -7790,10 +8164,30 @@ package body Sem_Res is
 
    procedure Resolve_Quantified_Expression (N : Node_Id; Typ : Entity_Id) is
    begin
-      --  The loop structure is already resolved during its analysis, only the
-      --  resolution of the condition needs to be done.
+      if not Alfa_Mode then
+
+         --  If expansion is enabled, analysis is delayed until the expresssion
+         --  is rewritten as a loop.
+
+         if Operating_Mode /= Check_Semantics then
+            return;
+         end if;
+
+         --  The loop structure is already resolved during its analysis, only
+         --  the resolution of the condition needs to be done. Expansion is
+         --  disabled so that checks and other generated code are inserted in
+         --  the tree after expression has been rewritten as a loop.
 
-      Resolve (Condition (N), Typ);
+         Expander_Mode_Save_And_Set (False);
+         Resolve (Condition (N), Typ);
+         Expander_Mode_Restore;
+
+      --  In Alfa mode, we need normal expansion in order to properly introduce
+      --  the necessary transient scopes.
+
+      else
+         Resolve (Condition (N), Typ);
+      end if;
    end Resolve_Quantified_Expression;
 
    -------------------
@@ -7879,13 +8273,12 @@ package body Sem_Res is
          return;
       end if;
 
-      --  If bounds are static, constant-fold them, so size computations
-      --  are identical between front-end and back-end. Do not perform this
+      --  If bounds are static, constant-fold them, so size computations are
+      --  identical between front-end and back-end. Do not perform this
       --  transformation while analyzing generic units, as type information
-      --  would then be lost when reanalyzing the constant node in the
-      --  instance.
+      --  would be lost when reanalyzing the constant node in the instance.
 
-      if Is_Discrete_Type (Typ) and then Expander_Active then
+      if Is_Discrete_Type (Typ) and then Full_Expander_Active then
          if Is_OK_Static_Expression (L) then
             Fold_Uint  (L, Expr_Value (L), Is_Static_Expression (L));
          end if;
@@ -7905,8 +8298,8 @@ package body Sem_Res is
 
    begin
       --  Special processing for fixed-point literals to make sure that the
-      --  value is an exact multiple of small where this is required. We
-      --  skip this for the universal real case, and also for generic types.
+      --  value is an exact multiple of small where this is required. We skip
+      --  this for the universal real case, and also for generic types.
 
       if Is_Fixed_Point_Type (Typ)
         and then Typ /= Universal_Fixed
@@ -7925,8 +8318,8 @@ package body Sem_Res is
 
             if Den /= 1 then
 
-               --  For a source program literal for a decimal fixed-point
-               --  type, this is statically illegal (RM 4.9(36)).
+               --  For a source program literal for a decimal fixed-point type,
+               --  this is statically illegal (RM 4.9(36)).
 
                if Is_Decimal_Fixed_Point_Type (Typ)
                  and then Actual_Typ = Universal_Real
@@ -7986,11 +8379,11 @@ package body Sem_Res is
 
       Resolve (P, Designated_Type (Etype (N)));
 
-      --  If we are taking the reference of a volatile entity, then treat
-      --  it as a potential modification of this entity. This is much too
-      --  conservative, but is necessary because remove side effects can
-      --  result in transformations of normal assignments into reference
-      --  sequences that otherwise fail to notice the modification.
+      --  If we are taking the reference of a volatile entity, then treat it as
+      --  a potential modification of this entity. This is too conservative,
+      --  but necessary because remove side effects can cause transformations
+      --  of normal assignments into reference sequences that otherwise fail to
+      --  notice the modification.
 
       if Is_Entity_Name (P) and then Treat_As_Volatile (Entity (P)) then
          Note_Possible_Modification (P, Sure => False);
@@ -8048,7 +8441,10 @@ package body Sem_Res is
                T := It.Typ;
             end if;
 
-            if Is_Record_Type (T) then
+            --  Locate selected component. For a private prefix the selector
+            --  can denote a discriminant.
+
+            if Is_Record_Type (T) or else Is_Private_Type (T) then
 
                --  The visible components of a class-wide type are those of
                --  the root type.
@@ -8177,8 +8573,8 @@ package body Sem_Res is
 
       --  If the array type is atomic, and is packed, and we are in a left side
       --  context, then this is worth a warning, since we have a situation
-      --  where the access to the component may cause extra read/writes of
-      --  the atomic array object, which could be considered unexpected.
+      --  where the access to the component may cause extra read/writes of the
+      --  atomic array object, which could be considered unexpected.
 
       if Nkind (N) = N_Selected_Component
         and then (Is_Atomic (T)
@@ -8228,11 +8624,8 @@ package body Sem_Res is
       R     : constant Node_Id   := Right_Opnd (N);
 
    begin
-      --  Why are the calls to Check_Order_Dependence commented out ???
       Resolve (L, B_Typ);
-      --  Check_Order_Dependence;   --  For AI05-0144
       Resolve (R, B_Typ);
-      --  Check_Order_Dependence;   --  For AI05-0144
 
       --  Check for issuing warning for always False assert/check, this happens
       --  when assertions are turned off, in which case the pragma Assert/Check
@@ -8430,11 +8823,11 @@ package body Sem_Res is
          end;
 
       --  Maybe this should just be "else", instead of checking for the
-      --  specific case of slice??? This is needed for the case where
-      --  the prefix is an Image attribute, which gets expanded to a
-      --  slice, and so has a constrained subtype which we want to use
-      --  for the slice range check applied below (the range check won't
-      --  get done if the unconstrained subtype of the 'Image is used).
+      --  specific case of slice??? This is needed for the case where the
+      --  prefix is an Image attribute, which gets expanded to a slice, and so
+      --  has a constrained subtype which we want to use for the slice range
+      --  check applied below (the range check won't get done if the
+      --  unconstrained subtype of the 'Image is used).
 
       elsif Nkind (Name) = N_Slice then
          Array_Type := Etype (Name);
@@ -8455,8 +8848,8 @@ package body Sem_Res is
 
             --  Ensure that side effects in the bounds are properly handled
 
-            Remove_Side_Effects (Low_Bound  (Drange), Variable_Ref => True);
-            Remove_Side_Effects (High_Bound (Drange), Variable_Ref => True);
+            Force_Evaluation (Low_Bound (Drange));
+            Force_Evaluation (High_Bound (Drange));
 
             --  Do not apply the range check to nodes associated with the
             --  frontend expansion of the dispatch table. We first check
@@ -8670,8 +9063,8 @@ package body Sem_Res is
          --  has compile time known bounds. If yes we can directly check
          --  whether the evaluation of the string will raise constraint error.
          --  Otherwise we need to transform the string literal into the
-         --  corresponding character aggregate and let the aggregate
-         --  code do the checking.
+         --  corresponding character aggregate and let the aggregate code do
+         --  the checking.
 
          if Is_Standard_Character_Type (R_Typ) then
 
@@ -8740,6 +9133,7 @@ package body Sem_Res is
                P := P + 1;
 
             --  Should we have a call to Skip_Wide here ???
+
             --  ???     else
             --             Skip_Wide (P);
 
@@ -8868,6 +9262,35 @@ package body Sem_Res is
 
       Resolve (Operand);
 
+      --  In SPARK, a type conversion between array types should be restricted
+      --  to types which have matching static bounds.
+
+      --  Protect call to Matching_Static_Array_Bounds to avoid costly
+      --  operation if not needed.
+
+      if Restriction_Check_Required (SPARK)
+        and then 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_SPARK_Restriction
+           ("array types should have matching static bounds", N);
+      end if;
+
+      --  In formal mode, the operand of an ancestor type conversion must be an
+      --  object (not an expression).
+
+      if Is_Tagged_Type (Target_Typ)
+        and then not Is_Class_Wide_Type (Target_Typ)
+        and then Is_Tagged_Type (Operand_Typ)
+        and then not Is_Class_Wide_Type (Operand_Typ)
+        and then Is_Ancestor (Target_Typ, Operand_Typ)
+        and then not Is_SPARK_Object_Reference (Operand)
+      then
+         Check_SPARK_Restriction ("object required", Operand);
+      end if;
+
       --  Note: we do the Eval_Type_Conversion call before applying the
       --  required checks for a subtype conversion. This is important, since
       --  both are prepared under certain circumstances to change the type
@@ -8957,13 +9380,13 @@ package body Sem_Res is
             then
                null;
 
-            --  Finally, if this type conversion occurs in a context that
-            --  requires a prefix, and the expression is a qualified expression
-            --  then the type conversion is not redundant, because a qualified
-            --  expression is not a prefix, whereas a type conversion is. For
-            --  example, "X := T'(Funx(...)).Y;" is illegal because a selected
-            --  component requires a prefix, but a type conversion makes it
-            --  legal: "X := T(T'(Funx(...))).Y;"
+            --  Finally, if this type conversion occurs in a context requiring
+            --  a prefix, and the expression is a qualified expression then the
+            --  type conversion is not redundant, since a qualified expression
+            --  is not a prefix, whereas a type conversion is. For example, "X
+            --  := T'(Funx(...)).Y;" is illegal because a selected component
+            --  requires a prefix, but a type conversion makes it legal: "X :=
+            --  T(T'(Funx(...))).Y;"
 
             --  In Ada 2012, a qualified expression is a name, so this idiom is
             --  no longer needed, but we still suppress the warning because it
@@ -9003,7 +9426,7 @@ package body Sem_Res is
       --  expression coincides with the target type.
 
       if Ada_Version >= Ada_2005
-        and then Expander_Active
+        and then Full_Expander_Active
         and then Operand_Typ /= Target_Typ
       then
          declare
@@ -9105,6 +9528,12 @@ package body Sem_Res is
       Hi    : Uint;
 
    begin
+      if Is_Modular_Integer_Type (Typ) and then Nkind (N) /= N_Op_Not then
+         Error_Msg_Name_1 := Chars (Typ);
+         Check_SPARK_Restriction
+           ("unary operator not defined for modular type%", N);
+      end if;
+
       --  Deal with intrinsic unary operators
 
       if Comes_From_Source (N)
@@ -9459,6 +9888,7 @@ package body Sem_Res is
          --  scheme).
 
          Set_Scalar_Range (Index_Subtype, New_Copy_Tree (Drange));
+         Set_Parent       (Scalar_Range (Index_Subtype), Index_Subtype);
          Set_Etype        (Index_Subtype, Index_Type);
          Set_Size_Info    (Index_Subtype, Index_Type);
          Set_RM_Size      (Index_Subtype, RM_Size (Index_Type));
@@ -9481,9 +9911,9 @@ package body Sem_Res is
 
       Set_Etype (N, Slice_Subtype);
 
-      --  For packed slice subtypes, freeze immediately (except in the
-      --  case of being in a "spec expression" where we never freeze
-      --  when we first see the expression).
+      --  For packed slice subtypes, freeze immediately (except in the case of
+      --  being in a "spec expression" where we never freeze when we first see
+      --  the expression).
 
       if Is_Packed (Slice_Subtype) and not In_Spec_Expression then
          Freeze_Itype (Slice_Subtype, N);
@@ -9492,9 +9922,10 @@ package body Sem_Res is
       --  so that the itype is frozen at the proper place in the tree (i.e. at
       --  the point where actions for the slice are analyzed). Note that this
       --  is different from freezing the itype immediately, which might be
-      --  premature (e.g. if the slice is within a transient scope).
+      --  premature (e.g. if the slice is within a transient scope). This needs
+      --  to be done only if expansion is enabled.
 
-      else
+      elsif Full_Expander_Active then
          Ensure_Defined (Typ => Slice_Subtype, N => N);
       end if;
    end Set_Slice_Subtype;
@@ -9531,29 +9962,62 @@ package body Sem_Res is
          Set_String_Literal_Low_Bound (Subtype_Id, Low_Bound);
 
       else
-         Set_String_Literal_Low_Bound
-           (Subtype_Id, Make_Integer_Literal (Loc, 1));
-         Set_Etype (String_Literal_Low_Bound (Subtype_Id), Standard_Positive);
-
-         --  Build bona fide subtype for the string, and wrap it in an
-         --  unchecked conversion, because the backend expects the
-         --  String_Literal_Subtype to have a static lower bound.
+         --  If the lower bound is not static we create a range for the string
+         --  literal, using the index type and the known length of the literal.
+         --  The index type is not necessarily Positive, so the upper bound is
+         --  computed as  T'Val (T'Pos (Low_Bound) + L - 1)
 
          declare
             Index_List    : constant List_Id    := New_List;
             Index_Type    : constant Entity_Id := Etype (First_Index (Typ));
-            High_Bound    : constant Node_Id :=
+
+            High_Bound : constant Node_Id :=
+                           Make_Attribute_Reference (Loc,
+                             Attribute_Name => Name_Val,
+                             Prefix         =>
+                               New_Occurrence_Of (Index_Type, Loc),
+                             Expressions    => New_List (
                                Make_Op_Add (Loc,
-                                  Left_Opnd => New_Copy_Tree (Low_Bound),
-                                  Right_Opnd =>
-                                    Make_Integer_Literal (Loc,
-                                      String_Length (Strval (N)) - 1));
+                                 Left_Opnd  =>
+                                   Make_Attribute_Reference (Loc,
+                                     Attribute_Name => Name_Pos,
+                                     Prefix         =>
+                                       New_Occurrence_Of (Index_Type, Loc),
+                                     Expressions    =>
+                                       New_List (New_Copy_Tree (Low_Bound))),
+                                 Right_Opnd =>
+                                   Make_Integer_Literal (Loc,
+                                     String_Length (Strval (N)) - 1))));
+
             Array_Subtype : Entity_Id;
             Index_Subtype : Entity_Id;
             Drange        : Node_Id;
             Index         : Node_Id;
 
          begin
+            if Is_Integer_Type (Index_Type) then
+               Set_String_Literal_Low_Bound
+                 (Subtype_Id, Make_Integer_Literal (Loc, 1));
+
+            else
+               --  If the index type is an enumeration type, build bounds
+               --  expression with attributes.
+
+               Set_String_Literal_Low_Bound
+                 (Subtype_Id,
+                  Make_Attribute_Reference (Loc,
+                    Attribute_Name => Name_First,
+                    Prefix         =>
+                      New_Occurrence_Of (Base_Type (Index_Type), Loc)));
+               Set_Etype (String_Literal_Low_Bound (Subtype_Id), Index_Type);
+            end if;
+
+            Analyze_And_Resolve (String_Literal_Low_Bound (Subtype_Id));
+
+            --  Build bona fide subtype for the string, and wrap it in an
+            --  unchecked conversion, because the backend expects the
+            --  String_Literal_Subtype to have a static lower bound.
+
             Index_Subtype :=
               Create_Itype (Subtype_Kind (Ekind (Index_Type)), N);
             Drange := Make_Range (Loc, New_Copy_Tree (Low_Bound), High_Bound);
@@ -9697,8 +10161,7 @@ package body Sem_Res is
             while Present (T2) loop
                if Is_Fixed_Point_Type (T2)
                  and then Scope (Base_Type (T2)) = Scop
-                 and then (Is_Potentially_Use_Visible (T2)
-                             or else In_Use (T2))
+                 and then (Is_Potentially_Use_Visible (T2) or else In_Use (T2))
                then
                   if Present (T1) then
                      Fixed_Point_Error;
@@ -9729,18 +10192,32 @@ package body Sem_Res is
    ----------------------
 
    function Valid_Conversion
-     (N       : Node_Id;
-      Target  : Entity_Id;
-      Operand : Node_Id) return Boolean
+     (N           : Node_Id;
+      Target      : Entity_Id;
+      Operand     : Node_Id;
+      Report_Errs : Boolean := True) return Boolean
    is
       Target_Type : constant Entity_Id := Base_Type (Target);
-      Opnd_Type   : Entity_Id := Etype (Operand);
+      Opnd_Type   : Entity_Id          := Etype (Operand);
 
       function Conversion_Check
         (Valid : Boolean;
          Msg   : String) return Boolean;
       --  Little routine to post Msg if Valid is False, returns Valid value
 
+      --  The following are badly named, this kind of overloading is actively
+      --  confusing in reading code, please rename to something like
+      --  Error_Msg_N_If_Reporting ???
+
+      procedure Error_Msg_N (Msg : String; N : Node_Or_Entity_Id);
+      --  If Report_Errs, then calls Errout.Error_Msg_N with its arguments
+
+      procedure Error_Msg_NE
+        (Msg : String;
+         N   : Node_Or_Entity_Id;
+         E   : Node_Or_Entity_Id);
+      --  If Report_Errs, then calls Errout.Error_Msg_NE with its arguments
+
       function Valid_Tagged_Conversion
         (Target_Type : Entity_Id;
          Opnd_Type   : Entity_Id) return Boolean;
@@ -9759,13 +10236,51 @@ package body Sem_Res is
          Msg   : String) return Boolean
       is
       begin
-         if not Valid then
+         if not Valid
+
+            --  A generic unit has already been analyzed and we have verified
+            --  that a particular conversion is OK in that context. Since the
+            --  instance is reanalyzed without relying on the relationships
+            --  established during the analysis of the generic, it is possible
+            --  to end up with inconsistent views of private types. Do not emit
+            --  the error message in such cases. The rest of the machinery in
+            --  Valid_Conversion still ensures the proper compatibility of
+            --  target and operand types.
+
+           and then not In_Instance
+         then
             Error_Msg_N (Msg, Operand);
          end if;
 
          return Valid;
       end Conversion_Check;
 
+      -----------------
+      -- Error_Msg_N --
+      -----------------
+
+      procedure Error_Msg_N (Msg : String; N : Node_Or_Entity_Id) is
+      begin
+         if Report_Errs then
+            Errout.Error_Msg_N (Msg, N);
+         end if;
+      end Error_Msg_N;
+
+      ------------------
+      -- Error_Msg_NE --
+      ------------------
+
+      procedure Error_Msg_NE
+        (Msg : String;
+         N   : Node_Or_Entity_Id;
+         E   : Node_Or_Entity_Id)
+      is
+      begin
+         if Report_Errs then
+            Errout.Error_Msg_NE (Msg, N, E);
+         end if;
+      end Error_Msg_NE;
+
       ----------------------------
       -- Valid_Array_Conversion --
       ----------------------------
@@ -9837,21 +10352,23 @@ package body Sem_Res is
                --  checks that must be applied to such conversions to prevent
                --  out-of-scope references.
 
-            elsif
-              Ekind_In (Target_Comp_Base, E_Anonymous_Access_Type,
-                                          E_Anonymous_Access_Subprogram_Type)
+            elsif Ekind_In
+                    (Target_Comp_Base, E_Anonymous_Access_Type,
+                                       E_Anonymous_Access_Subprogram_Type)
               and then Ekind (Opnd_Comp_Base) = Ekind (Target_Comp_Base)
               and then
                 Subtypes_Statically_Match (Target_Comp_Type, Opnd_Comp_Type)
             then
                if Type_Access_Level (Target_Type) <
-                   Type_Access_Level (Opnd_Type)
+                    Deepest_Type_Access_Level (Opnd_Type)
                then
                   if In_Instance_Body then
-                     Error_Msg_N ("?source array type " &
-                       "has deeper accessibility level than target", Operand);
-                     Error_Msg_N ("\?Program_Error will be raised at run time",
-                         Operand);
+                     Error_Msg_N
+                       ("?source array type has " &
+                        "deeper accessibility level than target", Operand);
+                     Error_Msg_N
+                       ("\?Program_Error will be raised at run time",
+                        Operand);
                      Rewrite (N,
                        Make_Raise_Program_Error (Sloc (N),
                          Reason => PE_Accessibility_Check_Failed));
@@ -9861,10 +10378,12 @@ package body Sem_Res is
                   --  Conversion not allowed because of accessibility levels
 
                   else
-                     Error_Msg_N ("source array type " &
-                       "has deeper accessibility level than target", Operand);
+                     Error_Msg_N
+                       ("source array type has " &
+                       "deeper accessibility level than target", Operand);
                      return False;
                   end if;
+
                else
                   null;
                end if;
@@ -9884,7 +10403,7 @@ package body Sem_Res is
             --  All of this is checked in Subtypes_Statically_Match.
 
             if not Subtypes_Statically_Match
-                            (Target_Comp_Type, Opnd_Comp_Type)
+                     (Target_Comp_Type, Opnd_Comp_Type)
             then
                Error_Msg_N
                  ("component subtypes must statically match", Operand);
@@ -10082,7 +10601,7 @@ package body Sem_Res is
          --  this situation can arise in source code.
 
          elsif In_Instance or else In_Inlined_Body then
-               return True;
+            return True;
 
          --  Otherwise we need the conversion check
 
@@ -10118,7 +10637,7 @@ package body Sem_Res is
 
          if Ekind (Target_Type) /= E_Anonymous_Access_Type then
             if Type_Access_Level (Opnd_Type) >
-               Type_Access_Level (Target_Type)
+               Deepest_Type_Access_Level (Target_Type)
             then
                --  In an instance, this is a run-time check, but one we know
                --  will fail, so generate an appropriate warning. The raise
@@ -10130,6 +10649,7 @@ package body Sem_Res is
                      Operand);
                   Error_Msg_N
                     ("\?Program_Error will be raised at run time", Operand);
+
                else
                   Error_Msg_N
                     ("cannot convert local pointer to non-local access type",
@@ -10150,7 +10670,7 @@ package body Sem_Res is
 
                if Nkind (Operand) = N_Selected_Component
                  and then Object_Access_Level (Operand) >
-                          Type_Access_Level (Target_Type)
+                   Deepest_Type_Access_Level (Target_Type)
                then
                   --  In an instance, this is a run-time check, but one we know
                   --  will fail, so generate an appropriate warning. The raise
@@ -10218,9 +10738,83 @@ package body Sem_Res is
 
          if Ekind (Target_Type) /= E_Anonymous_Access_Type
            or else Is_Local_Anonymous_Access (Target_Type)
+           or else Nkind (Associated_Node_For_Itype (Target_Type)) =
+                     N_Object_Declaration
          then
-            if Type_Access_Level (Opnd_Type)
-              > Type_Access_Level (Target_Type)
+            --  Ada 2012 (AI05-0149): Perform legality checking on implicit
+            --  conversions from an anonymous access type to a named general
+            --  access type. Such conversions are not allowed in the case of
+            --  access parameters and stand-alone objects of an anonymous
+            --  access type. The implicit conversion case is recognized by
+            --  testing that Comes_From_Source is False and that it's been
+            --  rewritten. The Comes_From_Source test isn't sufficient because
+            --  nodes in inlined calls to predefined library routines can have
+            --  Comes_From_Source set to False. (Is there a better way to test
+            --  for implicit conversions???)
+
+            if Ada_Version >= Ada_2012
+              and then not Comes_From_Source (N)
+              and then N /= Original_Node (N)
+              and then Ekind (Target_Type) = E_General_Access_Type
+              and then Ekind (Opnd_Type) = E_Anonymous_Access_Type
+            then
+               if Is_Itype (Opnd_Type) then
+
+                  --  Implicit conversions aren't allowed for objects of an
+                  --  anonymous access type, since such objects have nonstatic
+                  --  levels in Ada 2012.
+
+                  if Nkind (Associated_Node_For_Itype (Opnd_Type)) =
+                       N_Object_Declaration
+                  then
+                     Error_Msg_N
+                       ("implicit conversion of stand-alone anonymous " &
+                        "access object not allowed", Operand);
+                     return False;
+
+                  --  Implicit conversions aren't allowed for anonymous access
+                  --  parameters. The "not Is_Local_Anonymous_Access_Type" test
+                  --  is done to exclude anonymous access results.
+
+                  elsif not Is_Local_Anonymous_Access (Opnd_Type)
+                    and then Nkind_In (Associated_Node_For_Itype (Opnd_Type),
+                                       N_Function_Specification,
+                                       N_Procedure_Specification)
+                  then
+                     Error_Msg_N
+                       ("implicit conversion of anonymous access formal " &
+                        "not allowed", Operand);
+                     return False;
+
+                  --  This is a case where there's an enclosing object whose
+                  --  to which the "statically deeper than" relationship does
+                  --  not apply (such as an access discriminant selected from
+                  --  a dereference of an access parameter).
+
+                  elsif Object_Access_Level (Operand)
+                          = Scope_Depth (Standard_Standard)
+                  then
+                     Error_Msg_N
+                       ("implicit conversion of anonymous access value " &
+                        "not allowed", Operand);
+                     return False;
+
+                  --  In other cases, the level of the operand's type must be
+                  --  statically less deep than that of the target type, else
+                  --  implicit conversion is disallowed (by RM12-8.6(27.1/3)).
+
+                  elsif Type_Access_Level (Opnd_Type) >
+                        Deepest_Type_Access_Level (Target_Type)
+                  then
+                     Error_Msg_N
+                       ("implicit conversion of anonymous access value " &
+                        "violates accessibility", Operand);
+                     return False;
+                  end if;
+               end if;
+
+            elsif Type_Access_Level (Opnd_Type) >
+                    Deepest_Type_Access_Level (Target_Type)
             then
                --  In an instance, this is a run-time check, but one we know
                --  will fail, so generate an appropriate warning. The raise
@@ -10258,7 +10852,7 @@ package body Sem_Res is
 
                if Nkind (Operand) = N_Selected_Component
                  and then Object_Access_Level (Operand) >
-                          Type_Access_Level (Target_Type)
+                          Deepest_Type_Access_Level (Target_Type)
                then
                   --  In an instance, this is a run-time check, but one we know
                   --  will fail, so generate an appropriate warning. The raise
@@ -10430,7 +11024,7 @@ package body Sem_Res is
          --  Check the static accessibility rule of 4.6(20)
 
          if Type_Access_Level (Opnd_Type) >
-            Type_Access_Level (Target_Type)
+            Deepest_Type_Access_Level (Target_Type)
          then
             Error_Msg_N
               ("operand type has deeper accessibility level than target",
@@ -10480,6 +11074,11 @@ package body Sem_Res is
               N);
          return True;
 
+      --  If it was legal in the generic, it's legal in the instance
+
+      elsif In_Instance_Body then
+         return True;
+
       --  If both are tagged types, check legality of view conversions
 
       elsif Is_Tagged_Type (Target_Type)