[multiple changes]

2016-04-27  Bob Duff  <duff@adacore.com>

	* a-coinve.adb, a-comutr.adb, a-conhel.adb, a-convec.adb,
	exp_util.adb: Remove assertions that can fail in obscure cases when
	assertions are turned on but tampering checks are turned off.

2016-04-27  Javier Miranda  <miranda@adacore.com>

	* exp_ch6.adb (Add_Call_By_Copy_Code,
	Add_Simple_Call_By_Copy_Code, Expand_Actuals): Handle formals
	whose type comes from the limited view.

2016-04-27  Yannick Moy  <moy@adacore.com>

	* a-textio.adb: Complete previous patch.

2016-04-27  Yannick Moy  <moy@adacore.com>

	* inline.adb (Expand_Inlined_Call): Use Cannot_Inline instead of
	Error_Msg_N to issue message about impossibility to inline call,
	with slight change of message.

2016-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_spark.adb (Expand_Potential_Renaming): Removed.
	(Expand_SPARK): Update the call to expand a potential renaming.
	(Expand_SPARK_Potential_Renaming): New routine.
	* exp_spark.ads (Expand_SPARK_Potential_Renaming): New routine.
	* sem.adb Add with and use clauses for Exp_SPARK.
	(Analyze): Expand a non-overloaded potential renaming for SPARK.

2016-04-27  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch3.adb (Constrain_Discriminated_Type): In an instance,
	check full view for the presence of defaulted discriminants,
	even when the partial view of a private type has no visible and
	no unknown discriminants.

From-SVN: r235497

13 files changed, 188 insertions, 135 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 49106b9..a4a1c09 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,41 @@
+2016-04-27  Bob Duff  <duff@adacore.com>
+
+	* a-coinve.adb, a-comutr.adb, a-conhel.adb, a-convec.adb,
+	exp_util.adb: Remove assertions that can fail in obscure cases when
+	assertions are turned on but tampering checks are turned off.
+
+2016-04-27  Javier Miranda  <miranda@adacore.com>
+
+	* exp_ch6.adb (Add_Call_By_Copy_Code,
+	Add_Simple_Call_By_Copy_Code, Expand_Actuals): Handle formals
+	whose type comes from the limited view.
+
+2016-04-27  Yannick Moy  <moy@adacore.com>
+
+	* a-textio.adb: Complete previous patch.
+
+2016-04-27  Yannick Moy  <moy@adacore.com>
+
+	* inline.adb (Expand_Inlined_Call): Use Cannot_Inline instead of
+	Error_Msg_N to issue message about impossibility to inline call,
+	with slight change of message.
+
+2016-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_spark.adb (Expand_Potential_Renaming): Removed.
+	(Expand_SPARK): Update the call to expand a potential renaming.
+	(Expand_SPARK_Potential_Renaming): New routine.
+	* exp_spark.ads (Expand_SPARK_Potential_Renaming): New routine.
+	* sem.adb Add with and use clauses for Exp_SPARK.
+	(Analyze): Expand a non-overloaded potential renaming for SPARK.
+
+2016-04-27  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch3.adb (Constrain_Discriminated_Type): In an instance,
+	check full view for the presence of defaulted discriminants,
+	even when the partial view of a private type has no visible and
+	no unknown discriminants.
+
 2016-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* lib-xref.adb, exp_ch3.adb: Minor reformatting.
diff --git a/gcc/ada/a-coinve.adb b/gcc/ada/a-coinve.adb
index 230607c..3c19727 100644
--- a/gcc/ada/a-coinve.adb
+++ b/gcc/ada/a-coinve.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2016, 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- --
@@ -748,9 +748,6 @@ package body Ada.Containers.Indefinite_Vectors is
    end Finalize;
 
    procedure Finalize (Object : in out Iterator) is
-      pragma Warnings (Off);
-      pragma Assert (T_Check); -- not called if check suppressed
-      pragma Warnings (On);
    begin
       Unbusy (Object.Container.TC);
    end Finalize;
diff --git a/gcc/ada/a-comutr.adb b/gcc/ada/a-comutr.adb
index 68d49aa..7804b0f 100644
--- a/gcc/ada/a-comutr.adb
+++ b/gcc/ada/a-comutr.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2016, 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- --
@@ -47,7 +47,8 @@ package body Ada.Containers.Multiway_Trees is
    record
       Container : Tree_Access;
       Subtree   : Tree_Node_Access;
-   end record;
+   end record
+     with Disable_Controlled => not T_Check;
 
    overriding procedure Finalize (Object : in out Root_Iterator);
 
@@ -71,7 +72,8 @@ package body Ada.Containers.Multiway_Trees is
    ---------------------
 
    type Child_Iterator is new Root_Iterator and
-     Tree_Iterator_Interfaces.Reversible_Iterator with null record;
+     Tree_Iterator_Interfaces.Reversible_Iterator with null record
+       with Disable_Controlled => not T_Check;
 
    overriding function First (Object : Child_Iterator) return Cursor;
 
diff --git a/gcc/ada/a-conhel.adb b/gcc/ada/a-conhel.adb
index f433250..864b217 100644
--- a/gcc/ada/a-conhel.adb
+++ b/gcc/ada/a-conhel.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---             Copyright (C) 2015, Free Software Foundation, Inc.           --
+--           Copyright (C) 2015-2016, 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- --
@@ -36,10 +36,6 @@ package body Ada.Containers.Helpers is
       ------------
 
       procedure Adjust (Control : in out Reference_Control_Type) is
-         pragma Warnings (Off);
-         --  GNAT warns here if checks are turned off, but assertions on
-         pragma Assert (T_Check); -- not called if check suppressed
-         pragma Warnings (On);
       begin
          if Control.T_Counts /= null then
             Lock (Control.T_Counts.all);
@@ -62,9 +58,6 @@ package body Ada.Containers.Helpers is
       --------------
 
       procedure Finalize (Control : in out Reference_Control_Type) is
-         pragma Warnings (Off);
-         pragma Assert (T_Check); -- not called if check suppressed
-         pragma Warnings (On);
       begin
          if Control.T_Counts /= null then
             Unlock (Control.T_Counts.all);
diff --git a/gcc/ada/a-convec.adb b/gcc/ada/a-convec.adb
index 380a10b..d77e011 100644
--- a/gcc/ada/a-convec.adb
+++ b/gcc/ada/a-convec.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2004-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2016, 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- --
@@ -617,9 +617,6 @@ package body Ada.Containers.Vectors is
    end Finalize;
 
    procedure Finalize (Object : in out Iterator) is
-      pragma Warnings (Off);
-      pragma Assert (T_Check); -- not called if check suppressed
-      pragma Warnings (On);
    begin
       Unbusy (Object.Container.TC);
    end Finalize;
diff --git a/gcc/ada/a-textio.adb b/gcc/ada/a-textio.adb
index 61d6acc..59f9190 100644
--- a/gcc/ada/a-textio.adb
+++ b/gcc/ada/a-textio.adb
@@ -714,11 +714,12 @@ package body Ada.Text_IO is
 
       function Get_Rest (S : String) return String is
 
-         --  Each time we allocate a buffer the same size as what we have
-         --  read so far. This limits us to a logarithmic number of calls
-         --  to Get_Rest and also ensures only a linear use of stack space.
+         --  The first time we allocate a buffer of size 500. Each following
+         --  time we allocate a buffer the same size as what we have read so
+         --  far. This limits us to a logarithmic number of calls to Get_Rest
+         --  and also ensures only a linear use of stack space.
 
-         Buffer : String (1 .. S'Length);
+         Buffer : String (1 .. Integer'Max (500, S'Length));
          Last   : Natural;
 
       begin
@@ -731,43 +732,26 @@ package body Ada.Text_IO is
                return R;
 
             else
-               return Get_Rest (R);
+               pragma Assert (Last = Buffer'Last);
+
+               --  If the String has the same length as the buffer, and there
+               --  is no end of line, check whether we are at the end of file,
+               --  in which case we have the full String in the buffer.
+
+               if End_Of_File (File) then
+                  return R;
+
+               else
+                  return Get_Rest (R);
+               end if;
             end if;
          end;
       end Get_Rest;
 
-      --  Local variables
-
-      Buffer : String (1 .. 500);
-      ch     : int;
-      Last   : Natural;
-
    --  Start of processing for Get_Line
 
    begin
-      Get_Line (File, Buffer, Last);
-
-      if Last < Buffer'Last then
-         return Buffer (1 .. Last);
-
-      --  If the String has the same length as the buffer, and there is no end
-      --  of line, check whether we are at the end of file, in which case we
-      --  have the full String in the buffer.
-
-      elsif Last = Buffer'Last then
-         ch := Getc (File);
-
-         if ch = EOF then
-            return Buffer;
-
-         else
-            Ungetc (ch, File);
-            return Get_Rest (Buffer (1 .. Last));
-         end if;
-
-      else
-         return Get_Rest (Buffer (1 .. Last));
-      end if;
+      return Get_Rest ("");
    end Get_Line;
 
    function Get_Line return String is
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 1d3ab7d..c34f17d 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -1198,14 +1198,14 @@ package body Exp_Ch6 is
       ---------------------------
 
       procedure Add_Call_By_Copy_Code is
+         Crep  : Boolean;
          Expr  : Node_Id;
+         F_Typ : Entity_Id := Etype (Formal);
+         Indic : Node_Id;
          Init  : Node_Id;
          Temp  : Entity_Id;
-         Indic : Node_Id;
-         Var   : Entity_Id;
-         F_Typ : constant Entity_Id := Etype (Formal);
          V_Typ : Entity_Id;
-         Crep  : Boolean;
+         Var   : Entity_Id;
 
       begin
          if not Is_Legal_Copy then
@@ -1214,6 +1214,14 @@ package body Exp_Ch6 is
 
          Temp := Make_Temporary (Loc, 'T', Actual);
 
+         --  Handle formals whose type comes from the limited view
+
+         if From_Limited_With (F_Typ)
+           and then Has_Non_Limited_View (F_Typ)
+         then
+            F_Typ := Non_Limited_View (F_Typ);
+         end if;
+
          --  Use formal type for temp, unless formal type is an unconstrained
          --  array, in which case we don't have to worry about bounds checks,
          --  and we use the actual type, since that has appropriate bounds.
@@ -1221,7 +1229,7 @@ package body Exp_Ch6 is
          if Is_Array_Type (F_Typ) and then not Is_Constrained (F_Typ) then
             Indic := New_Occurrence_Of (Etype (Actual), Loc);
          else
-            Indic := New_Occurrence_Of (Etype (Formal), Loc);
+            Indic := New_Occurrence_Of (F_Typ, Loc);
          end if;
 
          if Nkind (Actual) = N_Type_Conversion then
@@ -1473,20 +1481,28 @@ package body Exp_Ch6 is
       ----------------------------------
 
       procedure Add_Simple_Call_By_Copy_Code is
-         Temp   : Entity_Id;
          Decl   : Node_Id;
+         F_Typ  : Entity_Id := Etype (Formal);
          Incod  : Node_Id;
-         Outcod : Node_Id;
+         Indic  : Node_Id;
          Lhs    : Node_Id;
+         Outcod : Node_Id;
          Rhs    : Node_Id;
-         Indic  : Node_Id;
-         F_Typ  : constant Entity_Id := Etype (Formal);
+         Temp   : Entity_Id;
 
       begin
          if not Is_Legal_Copy then
             return;
          end if;
 
+         --  Handle formals whose type comes from the limited view
+
+         if From_Limited_With (F_Typ)
+           and then Has_Non_Limited_View (F_Typ)
+         then
+            F_Typ := Non_Limited_View (F_Typ);
+         end if;
+
          --  Use formal type for temp, unless formal type is an unconstrained
          --  array, in which case we don't have to worry about bounds checks,
          --  and we use the actual type, since that has appropriate bounds.
@@ -1494,7 +1510,7 @@ package body Exp_Ch6 is
          if Is_Array_Type (F_Typ) and then not Is_Constrained (F_Typ) then
             Indic := New_Occurrence_Of (Etype (Actual), Loc);
          else
-            Indic := New_Occurrence_Of (Etype (Formal), Loc);
+            Indic := New_Occurrence_Of (F_Typ, Loc);
          end if;
 
          --  Prepare to generate code
@@ -1517,7 +1533,7 @@ package body Exp_Ch6 is
          if Ekind (Formal) = E_Out_Parameter then
             Incod := Empty;
 
-            if Has_Discriminants (Etype (Formal)) then
+            if Has_Discriminants (F_Typ) then
                Indic := New_Occurrence_Of (Etype (Actual), Loc);
             end if;
 
@@ -1719,6 +1735,14 @@ package body Exp_Ch6 is
          E_Formal := Etype (Formal);
          E_Actual := Etype (Actual);
 
+         --  Handle formals whose type comes from the limited view
+
+         if From_Limited_With (E_Formal)
+           and then Has_Non_Limited_View (E_Formal)
+         then
+            E_Formal := Non_Limited_View (E_Formal);
+         end if;
+
          if Is_Scalar_Type (E_Formal)
            or else Nkind (Actual) = N_Slice
          then
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index bd86d18..6ac38d6 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --
@@ -42,10 +42,6 @@ package body Exp_SPARK is
    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
    --  Perform name evaluation for a renamed object
 
-   procedure Expand_Potential_Renaming (N : Node_Id);
-   --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
-   --  replace N with the renamed object.
-
    ------------------
    -- Expand_SPARK --
    ------------------
@@ -73,7 +69,7 @@ package body Exp_SPARK is
 
          when N_Expanded_Name |
               N_Identifier    =>
-            Expand_Potential_Renaming (N);
+            Expand_SPARK_Potential_Renaming (N);
 
          when N_Object_Renaming_Declaration =>
             Expand_SPARK_N_Object_Renaming_Declaration (N);
@@ -116,41 +112,41 @@ package body Exp_SPARK is
       Evaluate_Name (Name (N));
    end Expand_SPARK_N_Object_Renaming_Declaration;
 
-   -------------------------------
-   -- Expand_Potential_Renaming --
-   -------------------------------
+   -------------------------------------
+   -- Expand_SPARK_Potential_Renaming --
+   -------------------------------------
 
-   procedure Expand_Potential_Renaming (N : Node_Id) is
-      Id     : constant Entity_Id  := Entity (N);
+   procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
       Loc    : constant Source_Ptr := Sloc (N);
+      Ren_Id : constant Entity_Id  := Entity (N);
       Typ    : constant Entity_Id  := Etype (N);
-      Ren_Id : Node_Id;
+      Obj_Id : Node_Id;
 
    begin
       --  Replace a reference to a renaming with the actual renamed object
 
-      if Ekind (Id) in Object_Kind then
-         Ren_Id := Renamed_Object (Id);
+      if Ekind (Ren_Id) in Object_Kind then
+         Obj_Id := Renamed_Object (Ren_Id);
 
-         if Present (Ren_Id) then
+         if Present (Obj_Id) then
 
             --  The renamed object is an entity when instantiating generics
             --  or inlining bodies. In this case the renaming is part of the
             --  mapping "prologue" which links actuals to formals.
 
-            if Nkind (Ren_Id) in N_Entity then
-               Rewrite (N, New_Occurrence_Of (Ren_Id, Loc));
+            if Nkind (Obj_Id) in N_Entity then
+               Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
 
             --  Otherwise the renamed object denotes a name
 
             else
-               Rewrite (N, New_Copy_Tree (Ren_Id));
+               Rewrite (N, New_Copy_Tree (Obj_Id));
                Reset_Analyzed_Flags (N);
             end if;
 
             Analyze_And_Resolve (N, Typ);
          end if;
       end if;
-   end Expand_Potential_Renaming;
+   end Expand_SPARK_Potential_Renaming;
 
 end Exp_SPARK;
diff --git a/gcc/ada/exp_spark.ads b/gcc/ada/exp_spark.ads
index 750d66b..9fc7f69 100644
--- a/gcc/ada/exp_spark.ads
+++ b/gcc/ada/exp_spark.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2011-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2011-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -35,4 +35,8 @@ package Exp_SPARK is
 
    procedure Expand_SPARK (N : Node_Id);
 
+   procedure Expand_SPARK_Potential_Renaming (N : Node_Id);
+   --  N must denote an N_Expanded_Name or N_Identifier. If N is a reference to
+   --  a renaming, replace N with the renamed object.
+
 end Exp_SPARK;
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index fe0f588..954855d 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -7028,6 +7028,9 @@ package body Exp_Util is
       elsif Disable_Controlled (T) then
          return False;
 
+      elsif Is_Class_Wide_Type (T) and then Disable_Controlled (Etype (T)) then
+         return False;
+
       else
          --  Class-wide types are treated as controlled because derivations
          --  from the root type can introduce controlled components.
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 4a04e11..9b142c1 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -2761,17 +2761,9 @@ package body Inline is
       --  subprograms this must be done explicitly.
 
       if In_Open_Scopes (Subp) then
-         Error_Msg_N ("call to recursive subprogram cannot be inlined??", N);
+         Cannot_Inline
+           ("cannot inline call to recursive subprogram?", N, Subp);
          Set_Is_Inlined (Subp, False);
-
-         --  In GNATprove mode, issue a warning, and indicate that the
-         --  subprogram is not always inlined by setting flag Is_Inlined_Always
-         --  to False.
-
-         if GNATprove_Mode then
-            Set_Is_Inlined_Always (Subp, False);
-         end if;
-
          return;
 
       --  Skip inlining if this is not a true inlining since the attribute
@@ -2787,8 +2779,8 @@ package body Inline is
 
       elsif Is_Unc
         and then
-          Nkind (First (Statements (Handled_Statement_Sequence (Orig_Bod))))
-            = N_Extended_Return_Statement
+          Nkind (First (Statements (Handled_Statement_Sequence (Orig_Bod)))) =
+            N_Extended_Return_Statement
         and then not Back_End_Inlining
       then
          return;
diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb
index 7ed6a15..36c6298 100644
--- a/gcc/ada/sem.adb
+++ b/gcc/ada/sem.adb
@@ -23,39 +23,40 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Atree;    use Atree;
-with Debug;    use Debug;
-with Debug_A;  use Debug_A;
-with Elists;   use Elists;
-with Expander; use Expander;
-with Fname;    use Fname;
-with Ghost;    use Ghost;
-with Lib;      use Lib;
-with Lib.Load; use Lib.Load;
-with Nlists;   use Nlists;
-with Output;   use Output;
-with Restrict; use Restrict;
-with Sem_Attr; use Sem_Attr;
-with Sem_Aux;  use Sem_Aux;
-with Sem_Ch2;  use Sem_Ch2;
-with Sem_Ch3;  use Sem_Ch3;
-with Sem_Ch4;  use Sem_Ch4;
-with Sem_Ch5;  use Sem_Ch5;
-with Sem_Ch6;  use Sem_Ch6;
-with Sem_Ch7;  use Sem_Ch7;
-with Sem_Ch8;  use Sem_Ch8;
-with Sem_Ch9;  use Sem_Ch9;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch11; use Sem_Ch11;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Prag; use Sem_Prag;
-with Sem_Util; use Sem_Util;
-with Sinfo;    use Sinfo;
-with Stand;    use Stand;
-with Stylesw;  use Stylesw;
-with Uintp;    use Uintp;
-with Uname;    use Uname;
+with Atree;     use Atree;
+with Debug;     use Debug;
+with Debug_A;   use Debug_A;
+with Elists;    use Elists;
+with Exp_SPARK; use Exp_SPARK;
+with Expander;  use Expander;
+with Fname;     use Fname;
+with Ghost;     use Ghost;
+with Lib;       use Lib;
+with Lib.Load;  use Lib.Load;
+with Nlists;    use Nlists;
+with Output;    use Output;
+with Restrict;  use Restrict;
+with Sem_Attr;  use Sem_Attr;
+with Sem_Aux;   use Sem_Aux;
+with Sem_Ch2;   use Sem_Ch2;
+with Sem_Ch3;   use Sem_Ch3;
+with Sem_Ch4;   use Sem_Ch4;
+with Sem_Ch5;   use Sem_Ch5;
+with Sem_Ch6;   use Sem_Ch6;
+with Sem_Ch7;   use Sem_Ch7;
+with Sem_Ch8;   use Sem_Ch8;
+with Sem_Ch9;   use Sem_Ch9;
+with Sem_Ch10;  use Sem_Ch10;
+with Sem_Ch11;  use Sem_Ch11;
+with Sem_Ch12;  use Sem_Ch12;
+with Sem_Ch13;  use Sem_Ch13;
+with Sem_Prag;  use Sem_Prag;
+with Sem_Util;  use Sem_Util;
+with Sinfo;     use Sinfo;
+with Stand;     use Stand;
+with Stylesw;   use Stylesw;
+with Uintp;     use Uintp;
+with Uname;     use Uname;
 
 with Unchecked_Deallocation;
 
@@ -726,6 +727,21 @@ package body Sem is
                   and then Etype (N) = Standard_Void_Type)
       then
          Expand (N);
+
+      --  Replace a reference to a renaming with the renamed object for SPARK.
+      --  In general this modification is performed by Expand_SPARK, however
+      --  certain constructs may not reach the resolution or expansion phase
+      --  and thus remain unchanged. The replacement is not performed when the
+      --  construct is overloaded as resolution must first take place. This is
+      --  also not done when analyzing a generic to preserve the original tree
+      --  and because the reference may become overloaded in the instance.
+
+      elsif GNATprove_Mode
+        and then Nkind_In (N, N_Expanded_Name, N_Identifier)
+        and then not Is_Overloaded (N)
+        and then not Inside_A_Generic
+      then
+         Expand_SPARK_Potential_Renaming (N);
       end if;
 
       Ghost_Mode := Save_Ghost_Mode;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 63704fb..0d378ec 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -13033,7 +13033,7 @@ package body Sem_Ch3 is
       Related_Nod : Node_Id;
       For_Access  : Boolean := False)
    is
-      E     : constant Entity_Id := Entity (Subtype_Mark (S));
+      E     : Entity_Id := Entity (Subtype_Mark (S));
       T     : Entity_Id;
       C     : Node_Id;
       Elist : Elist_Id := New_Elmt_List;
@@ -13083,15 +13083,22 @@ package body Sem_Ch3 is
       end if;
 
       --  In an instance it may be necessary to retrieve the full view of a
-      --  type with unknown discriminants. In other contexts the constraint
-      --  is illegal.
+      --  type with unknown discriminants, or a full view with defaulted
+      --  discriminants. In other contexts the constraint is illegal.
 
       if In_Instance
         and then Is_Private_Type (T)
-        and then Has_Unknown_Discriminants (T)
         and then Present (Full_View (T))
+        and then
+          (Has_Unknown_Discriminants (T)
+             or else (not Has_Discriminants (T)
+               and then Has_Discriminants (Full_View (T))
+               and then Present
+                 (Discriminant_Default_Value
+                    (First_Discriminant (Full_View (T))))))
       then
          T := Full_View (T);
+         E := Full_View (E);
       end if;
 
       --  Ada 2005 (AI-412): Constrained incomplete subtypes are illegal.
@@ -20522,14 +20529,14 @@ package body Sem_Ch3 is
 
       May_Have_Null_Exclusion : Boolean;
 
-      procedure Check_Incomplete (T : Entity_Id);
+      procedure Check_Incomplete (T : Node_Id);
       --  Called to verify that an incomplete type is not used prematurely
 
       ----------------------
       -- Check_Incomplete --
       ----------------------
 
-      procedure Check_Incomplete (T : Entity_Id) is
+      procedure Check_Incomplete (T : Node_Id) is
       begin
          --  Ada 2005 (AI-412): Incomplete subtypes are legal