[Ada] Further cleanup in inlining machinery
[platform/upstream/gcc.git] / gcc / ada / inline.adb
index c06e5cb..15cec51 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2019, 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- --
@@ -23,6 +23,8 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+with Alloc;
+with Aspects;  use Aspects;
 with Atree;    use Atree;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
@@ -50,8 +52,12 @@ with Sinfo;    use Sinfo;
 with Sinput;   use Sinput;
 with Snames;   use Snames;
 with Stand;    use Stand;
-with Uname;    use Uname;
+with Table;
 with Tbuild;   use Tbuild;
+with Uintp;    use Uintp;
+with Uname;    use Uname;
+
+with GNAT.HTable;
 
 package body Inline is
 
@@ -81,12 +87,83 @@ package body Inline is
    Backend_Calls : Elist_Id;
    --  List of inline calls passed to the backend
 
+   Backend_Instances : Elist_Id;
+   --  List of instances inlined for the backend
+
    Backend_Inlined_Subps : Elist_Id;
    --  List of subprograms inlined by the backend
 
    Backend_Not_Inlined_Subps : Elist_Id;
    --  List of subprograms that cannot be inlined by the backend
 
+   -----------------------------
+   --  Pending_Instantiations --
+   -----------------------------
+
+   --  We make entries in this table for the pending instantiations of generic
+   --  bodies that are created during semantic analysis. After the analysis is
+   --  complete, calling Instantiate_Bodies performs the actual instantiations.
+
+   package Pending_Instantiations is new Table.Table (
+     Table_Component_Type => Pending_Body_Info,
+     Table_Index_Type     => Int,
+     Table_Low_Bound      => 0,
+     Table_Initial        => Alloc.Pending_Instantiations_Initial,
+     Table_Increment      => Alloc.Pending_Instantiations_Increment,
+     Table_Name           => "Pending_Instantiations");
+
+   -------------------------------------
+   --  Called_Pending_Instantiations  --
+   -------------------------------------
+
+   --  With back-end inlining, the pending instantiations that are not in the
+   --  main unit or subunit are performed only after a call to the subprogram
+   --  instance, or to a subprogram within the package instance, is inlined.
+   --  Since such a call can be within a subsequent pending instantiation,
+   --  we make entries in this table that stores the index of these "called"
+   --  pending instantiations and perform them when the table is populated.
+
+   package Called_Pending_Instantiations is new Table.Table (
+     Table_Component_Type => Int,
+     Table_Index_Type     => Int,
+     Table_Low_Bound      => 0,
+     Table_Initial        => Alloc.Pending_Instantiations_Initial,
+     Table_Increment      => Alloc.Pending_Instantiations_Increment,
+     Table_Name           => "Called_Pending_Instantiations");
+
+   ---------------------------------
+   --  To_Pending_Instantiations  --
+   ---------------------------------
+
+   --  With back-end inlining, we also need to have a map from the pending
+   --  instantiations to their index in the Pending_Instantiations table.
+
+   Node_Table_Size : constant := 257;
+   --  Number of headers in hash table
+
+   subtype Node_Header_Num is Integer range 0 .. Node_Table_Size - 1;
+   --  Range of headers in hash table
+
+   function Node_Hash (Id : Node_Id) return Node_Header_Num;
+   --  Simple hash function for Node_Ids
+
+   package To_Pending_Instantiations is new GNAT.Htable.Simple_HTable
+     (Header_Num => Node_Header_Num,
+      Element    => Int,
+      No_Element => -1,
+      Key        => Node_Id,
+      Hash       => Node_Hash,
+      Equal      => "=");
+
+   -----------------
+   -- Node_Hash --
+   -----------------
+
+   function Node_Hash (Id : Node_Id) return Node_Header_Num is
+   begin
+      return Node_Header_Num (Id mod Node_Table_Size);
+   end Node_Hash;
+
    --------------------
    -- Inlined Bodies --
    --------------------
@@ -157,7 +234,6 @@ package body Inline is
       Name        : Entity_Id  := Empty;
       Next        : Subp_Index := No_Subp;
       First_Succ  : Succ_Index := No_Succ;
-      Listed      : Boolean    := False;
       Main_Call   : Boolean    := False;
       Processed   : Boolean    := False;
    end record;
@@ -179,8 +255,11 @@ package body Inline is
    --  called, and for the inlined subprogram that contains the call. If
    --  the call is in the main compilation unit, Caller is Empty.
 
-   procedure Add_Inlined_Subprogram (Index : Subp_Index);
-   --  Add the subprogram to the list of inlined subprogram for the unit
+   procedure Add_Inlined_Instance (E : Entity_Id);
+   --  Add instance E to the list of of inlined instances for the unit
+
+   procedure Add_Inlined_Subprogram (E : Entity_Id);
+   --  Add subprogram E to the list of inlined subprograms for the unit
 
    function Add_Subp (E : Entity_Id) return Subp_Index;
    --  Make entry in Inlined table for subprogram E, or return table index
@@ -193,14 +272,14 @@ package body Inline is
 
    function Has_Initialized_Type (E : Entity_Id) return Boolean;
    --  If a candidate for inlining contains type declarations for types with
-   --  non-trivial initialization procedures, they are not worth inlining.
+   --  nontrivial initialization procedures, they are not worth inlining.
 
    function Has_Single_Return (N : Node_Id) return Boolean;
    --  In general we cannot inline functions that return unconstrained type.
-   --  However, we can handle such functions if all return statements return a
-   --  local variable that is the only declaration in the body of the function.
-   --  In that case the call can be replaced by that local variable as is done
-   --  for other inlined calls.
+   --  However, we can handle such functions if all return statements return
+   --  a local variable that is the first declaration in the body of the
+   --  function. In that case the call can be replaced by that local
+   --  variable as is done for other inlined calls.
 
    function In_Main_Unit_Or_Subunit (E : Entity_Id) return Boolean;
    --  Return True if E is in the main unit or its spec or in a subunit
@@ -212,11 +291,21 @@ package body Inline is
    --  function anyway. This is also the case if the function is defined in a
    --  task body or within an entry (for example, an initialization procedure).
 
-   procedure Remove_Pragmas (Bod : Node_Id);
-   --  A pragma Unreferenced or pragma Unmodified that mentions a formal
-   --  parameter has no meaning when the body is inlined and the formals
-   --  are rewritten. Remove it from body to inline. The analysis of the
-   --  non-inlined body will handle the pragma properly.
+   procedure Remove_Aspects_And_Pragmas (Body_Decl : Node_Id);
+   --  Remove all aspects and/or pragmas that have no meaning in inlined body
+   --  Body_Decl. The analysis of these items is performed on the non-inlined
+   --  body. The items currently removed are:
+   --    Contract_Cases
+   --    Global
+   --    Depends
+   --    Postcondition
+   --    Precondition
+   --    Refined_Global
+   --    Refined_Depends
+   --    Refined_Post
+   --    Test_Case
+   --    Unmodified
+   --    Unreferenced
 
    ------------------------------
    -- Deferred Cleanup Actions --
@@ -280,7 +369,7 @@ package body Inline is
    -- Add_Inlined_Body --
    ----------------------
 
-   procedure Add_Inlined_Body (E : Entity_Id) is
+   procedure Add_Inlined_Body (E : Entity_Id; N : Node_Id) is
 
       type Inline_Level_Type is (Dont_Inline, Inline_Call, Inline_Package);
       --  Level of inlining for the call: Dont_Inline means no inlining,
@@ -288,10 +377,65 @@ package body Inline is
       --  Inline_Package means that the call is considered for inlining and
       --  its package compiled and scanned for more inlining opportunities.
 
+      function Is_Non_Loading_Expression_Function
+        (Id : Entity_Id) return Boolean;
+      --  Determine whether arbitrary entity Id denotes a subprogram which is
+      --  either
+      --
+      --    * An expression function
+      --
+      --    * A function completed by an expression function where both the
+      --      spec and body are in the same context.
+
       function Must_Inline return Inline_Level_Type;
       --  Inlining is only done if the call statement N is in the main unit,
       --  or within the body of another inlined subprogram.
 
+      ----------------------------------------
+      -- Is_Non_Loading_Expression_Function --
+      ----------------------------------------
+
+      function Is_Non_Loading_Expression_Function
+        (Id : Entity_Id) return Boolean
+      is
+         Body_Decl : Node_Id;
+         Body_Id   : Entity_Id;
+         Spec_Decl : Node_Id;
+
+      begin
+         --  A stand-alone expression function is transformed into a spec-body
+         --  pair in-place. Since both the spec and body are in the same list,
+         --  the inlining of such an expression function does not need to load
+         --  anything extra.
+
+         if Is_Expression_Function (Id) then
+            return True;
+
+         --  A function may be completed by an expression function
+
+         elsif Ekind (Id) = E_Function then
+            Spec_Decl := Unit_Declaration_Node (Id);
+
+            if Nkind (Spec_Decl) = N_Subprogram_Declaration then
+               Body_Id := Corresponding_Body (Spec_Decl);
+
+               if Present (Body_Id) then
+                  Body_Decl := Unit_Declaration_Node (Body_Id);
+
+                  --  The inlining of a completing expression function does
+                  --  not need to load anything extra when both the spec and
+                  --  body are in the same context.
+
+                  return
+                    Was_Expression_Function (Body_Decl)
+                      and then Parent (Spec_Decl) = Parent (Body_Decl);
+               end if;
+            end if;
+         end if;
+
+         return False;
+      end Is_Non_Loading_Expression_Function;
+
       -----------------
       -- Must_Inline --
       -----------------
@@ -336,15 +480,19 @@ package body Inline is
             return Inline_Package;
          end if;
 
-         --  The call is not in the main unit. See if it is in some inlined
-         --  subprogram. If so, inline the call and, if the inlining level is
-         --  set to 1, stop there; otherwise also compile the package as above.
+         --  The call is not in the main unit. See if it is in some subprogram
+         --  that can be inlined outside its unit. If so, inline the call and,
+         --  if the inlining level is set to 1, stop there; otherwise also
+         --  compile the package as above.
 
          Scop := Current_Scope;
          while Scope (Scop) /= Standard_Standard
            and then not Is_Child_Unit (Scop)
          loop
-            if Is_Overloadable (Scop) and then Is_Inlined (Scop) then
+            if Is_Overloadable (Scop)
+              and then Is_Inlined (Scop)
+              and then not Is_Nested (Scop)
+            then
                Add_Call (E, Scop);
 
                if Inline_Level = 1 then
@@ -360,89 +508,222 @@ package body Inline is
          return Dont_Inline;
       end Must_Inline;
 
-      Level : Inline_Level_Type;
+      Inst      : Entity_Id;
+      Inst_Decl : Node_Id;
+      Inst_Node : Node_Id;
+      Level     : Inline_Level_Type;
 
    --  Start of processing for Add_Inlined_Body
 
    begin
-      --  Find unit containing E, and add to list of inlined bodies if needed.
-      --  If the body is already present, no need to load any other unit. This
-      --  is the case for an initialization procedure, which appears in the
-      --  package declaration that contains the type. It is also the case if
-      --  the body has already been analyzed. Finally, if the unit enclosing
-      --  E is an instance, the instance body will be analyzed in any case,
-      --  and there is no need to add the enclosing unit (whose body might not
-      --  be available).
+      Append_New_Elmt (N, To => Backend_Calls);
 
-      --  Library-level functions must be handled specially, because there is
-      --  no enclosing package to retrieve. In this case, it is the body of
-      --  the function that will have to be loaded.
+      --  Skip subprograms that cannot or need not be inlined outside their
+      --  unit or parent subprogram.
 
       if Is_Abstract_Subprogram (E)
-        or else Is_Nested (E)
         or else Convention (E) = Convention_Protected
+        or else In_Main_Unit_Or_Subunit (E)
+        or else Is_Nested (E)
       then
          return;
       end if;
 
+      --  Find out whether the call must be inlined. Unless the result is
+      --  Dont_Inline, Must_Inline also creates an edge for the call in the
+      --  callgraph; however, it will not be activated until after Is_Called
+      --  is set on the subprogram.
+
       Level := Must_Inline;
-      if Level /= Dont_Inline then
-         declare
-            Pack : constant Entity_Id := Get_Code_Unit_Entity (E);
 
-         begin
-            if Pack = E then
+      if Level = Dont_Inline then
+         return;
+      end if;
 
-               --  Library-level inlined function. Add function itself to
-               --  list of needed units.
+      --  If a previous call to the subprogram has been inlined, nothing to do
 
-               Set_Is_Called (E);
-               Inlined_Bodies.Increment_Last;
-               Inlined_Bodies.Table (Inlined_Bodies.Last) := E;
+      if Is_Called (E) then
+         return;
+      end if;
 
-            elsif Ekind (Pack) = E_Package then
-               Set_Is_Called (E);
+      --  If the subprogram is an instance, then inline the instance
 
-               if Is_Generic_Instance (Pack) then
-                  null;
+      if Is_Generic_Instance (E) then
+         Add_Inlined_Instance (E);
+      end if;
 
-               --  Do not inline the package if the subprogram is an init proc
-               --  or other internally generated subprogram, because in that
-               --  case the subprogram body appears in the same unit that
-               --  declares the type, and that body is visible to the back end.
-               --  Do not inline it either if it is in the main unit.
+      --  Mark the subprogram as called
 
-               elsif Level = Inline_Package
-                 and then not Is_Inlined (Pack)
-                 and then not Is_Internal (E)
-                 and then not In_Main_Unit_Or_Subunit (Pack)
-               then
-                  Set_Is_Inlined (Pack);
-                  Inlined_Bodies.Increment_Last;
-                  Inlined_Bodies.Table (Inlined_Bodies.Last) := Pack;
+      Set_Is_Called (E);
+
+      --  If the call was generated by the compiler and is to a subprogram in
+      --  a run-time unit, we need to suppress debugging information for it,
+      --  so that the code that is eventually inlined will not affect the
+      --  debugging of the program. We do not do it if the call comes from
+      --  source because, even if the call is inlined, the user may expect it
+      --  to be present in the debugging information.
+
+      if not Comes_From_Source (N)
+        and then In_Extended_Main_Source_Unit (N)
+        and then Is_Predefined_Unit (Get_Source_Unit (E))
+      then
+         Set_Needs_Debug_Info (E, False);
+      end if;
+
+      --  If the subprogram is an expression function, or is completed by one
+      --  where both the spec and body are in the same context, then there is
+      --  no need to load any package body since the body of the function is
+      --  in the spec.
+
+      if Is_Non_Loading_Expression_Function (E) then
+         return;
+      end if;
+
+      --  Find unit containing E, and add to list of inlined bodies if needed.
+      --  Library-level functions must be handled specially, because there is
+      --  no enclosing package to retrieve. In this case, it is the body of
+      --  the function that will have to be loaded.
+
+      declare
+         Pack : constant Entity_Id := Get_Code_Unit_Entity (E);
+
+      begin
+         if Pack = E then
+            Inlined_Bodies.Increment_Last;
+            Inlined_Bodies.Table (Inlined_Bodies.Last) := E;
+
+         else
+            pragma Assert (Ekind (Pack) = E_Package);
+
+            --  If the subprogram is within an instance, inline the instance
 
-               --  Extend the -gnatn2 processing to -gnatn1 for Inline_Always
-               --  calls if the back-end takes care of inlining the call.
+            if Comes_From_Source (E) then
+               Inst := Scope (E);
+
+               while Present (Inst) and then Inst /= Standard_Standard loop
+                  exit when Is_Generic_Instance (Inst);
+                  Inst := Scope (Inst);
+               end loop;
 
-               elsif Level = Inline_Call
-                 and then Has_Pragma_Inline_Always (E)
-                 and then Back_End_Inlining
+               if Present (Inst)
+                 and then Is_Generic_Instance (Inst)
+                 and then not Is_Called (Inst)
                then
-                  Set_Is_Inlined (Pack);
-                  Inlined_Bodies.Increment_Last;
-                  Inlined_Bodies.Table (Inlined_Bodies.Last) := Pack;
+                  --  Do not add a pending instantiation if the body exits
+                  --  already, or if the instance is a compilation unit, or
+                  --  the instance node is missing.
+
+                  Inst_Decl := Unit_Declaration_Node (Inst);
+                  if Present (Corresponding_Body (Inst_Decl))
+                    or else Nkind (Parent (Inst_Decl)) = N_Compilation_Unit
+                    or else No (Next (Inst_Decl))
+                  then
+                     Set_Is_Called (Inst);
+
+                  else
+                     --  If the inlined call itself appears within an instance,
+                     --  ensure that the enclosing instance body is available.
+                     --  This is necessary because Sem_Ch12.Might_Inline_Subp
+                     --  does not recurse into nested instantiations.
+
+                     if not Is_Inlined (Inst) and then In_Instance then
+                        Set_Is_Inlined (Inst);
+
+                        --  The instantiation node usually follows the package
+                        --  declaration for the instance. If the generic unit
+                        --  has aspect specifications, they are transformed
+                        --  into pragmas in the instance, and the instance node
+                        --  appears after them.
+
+                        Inst_Node := Next (Inst_Decl);
+
+                        while Nkind (Inst_Node) /= N_Package_Instantiation loop
+                           Inst_Node := Next (Inst_Node);
+                        end loop;
+
+                        Add_Pending_Instantiation (Inst_Node, Inst_Decl);
+                     end if;
+
+                     Add_Inlined_Instance (Inst);
+                  end if;
                end if;
             end if;
-         end;
-      end if;
+
+            --  If the unit containing E is an instance, then the instance body
+            --  will be analyzed in any case, see Sem_Ch12.Might_Inline_Subp.
+
+            if Is_Generic_Instance (Pack) then
+               null;
+
+            --  Do not inline the package if the subprogram is an init proc
+            --  or other internally generated subprogram, because in that
+            --  case the subprogram body appears in the same unit that
+            --  declares the type, and that body is visible to the back end.
+            --  Do not inline it either if it is in the main unit.
+            --  Extend the -gnatn2 processing to -gnatn1 for Inline_Always
+            --  calls if the back-end takes care of inlining the call.
+            --  Note that Level is in Inline_Call | Inline_Packag here.
+
+            elsif ((Level = Inline_Call
+                      and then Has_Pragma_Inline_Always (E)
+                      and then Back_End_Inlining)
+                    or else Level = Inline_Package)
+              and then not Is_Inlined (Pack)
+              and then not Is_Internal (E)
+              and then not In_Main_Unit_Or_Subunit (Pack)
+            then
+               Set_Is_Inlined (Pack);
+               Inlined_Bodies.Increment_Last;
+               Inlined_Bodies.Table (Inlined_Bodies.Last) := Pack;
+            end if;
+         end if;
+
+         --  Ensure that Analyze_Inlined_Bodies will be invoked after
+         --  completing the analysis of the current unit.
+
+         Inline_Processing_Required := True;
+      end;
    end Add_Inlined_Body;
 
+   --------------------------
+   -- Add_Inlined_Instance --
+   --------------------------
+
+   procedure Add_Inlined_Instance (E : Entity_Id) is
+      Decl_Node : constant Node_Id := Unit_Declaration_Node (E);
+      Index     : Int;
+
+   begin
+      --  This machinery is only used with back-end inlining
+
+      if not Back_End_Inlining then
+         return;
+      end if;
+
+      --  Register the instance in the list
+
+      Append_New_Elmt (Decl_Node, To => Backend_Instances);
+
+      --  Retrieve the index of its corresponding pending instantiation
+      --  and mark this corresponding pending instantiation as needed.
+
+      Index := To_Pending_Instantiations.Get (Decl_Node);
+      if Index >= 0 then
+         Called_Pending_Instantiations.Append (Index);
+      else
+         pragma Assert (False);
+         null;
+      end if;
+
+      Set_Is_Called (E);
+   end Add_Inlined_Instance;
+
    ----------------------------
    -- Add_Inlined_Subprogram --
    ----------------------------
 
-   procedure Add_Inlined_Subprogram (Index : Subp_Index) is
-      E    : constant Entity_Id := Inlined.Table (Index).Name;
+   procedure Add_Inlined_Subprogram (E : Entity_Id) is
+      Decl : constant Node_Id   := Parent (Declaration_Node (E));
       Pack : constant Entity_Id := Get_Code_Unit_Entity (E);
 
       procedure Register_Backend_Inlined_Subprogram (Subp : Entity_Id);
@@ -473,18 +754,17 @@ package body Inline is
    --  Start of processing for Add_Inlined_Subprogram
 
    begin
-      --  If the subprogram is to be inlined, and if its unit is known to be
-      --  inlined or is an instance whose body will be analyzed anyway or the
-      --  subprogram has been generated by the compiler, and if it is declared
-      --  at the library level not in the main unit, and if it can be inlined
-      --  by the back-end, then insert it in the list of inlined subprograms.
-
-      if Is_Inlined (E)
-        and then (Is_Inlined (Pack)
-                   or else Is_Generic_Instance (Pack)
-                   or else Is_Internal (E))
-        and then not In_Main_Unit_Or_Subunit (E)
-        and then not Is_Nested (E)
+      --  We can inline the subprogram if its unit is known to be inlined or is
+      --  an instance whose body will be analyzed anyway or the subprogram was
+      --  generated as a body by the compiler (for example an initialization
+      --  procedure) or its declaration was provided along with the body (for
+      --  example an expression function) and it does not declare types with
+      --  nontrivial initialization procedures.
+
+      if (Is_Inlined (Pack)
+           or else Is_Generic_Instance (Pack)
+           or else Nkind (Decl) = N_Subprogram_Body
+           or else Present (Corresponding_Body (Decl)))
         and then not Has_Initialized_Type (E)
       then
          Register_Backend_Inlined_Subprogram (E);
@@ -496,13 +776,69 @@ package body Inline is
          end if;
 
          Last_Inlined := E;
+
       else
          Register_Backend_Not_Inlined_Subprogram (E);
       end if;
-
-      Inlined.Table (Index).Listed := True;
    end Add_Inlined_Subprogram;
 
+   --------------------------------
+   --  Add_Pending_Instantiation --
+   --------------------------------
+
+   procedure Add_Pending_Instantiation (Inst : Node_Id; Act_Decl : Node_Id) is
+      Act_Decl_Id : Entity_Id;
+      Index       : Int;
+
+   begin
+      --  Here is a defense against a ludicrous number of instantiations
+      --  caused by a circular set of instantiation attempts.
+
+      if Pending_Instantiations.Last >= Maximum_Instantiations then
+         Error_Msg_Uint_1 := UI_From_Int (Maximum_Instantiations);
+         Error_Msg_N ("too many instantiations, exceeds max of^", Inst);
+         Error_Msg_N ("\limit can be changed using -gnateinn switch", Inst);
+         raise Unrecoverable_Error;
+      end if;
+
+      --  Capture the body of the generic instantiation along with its context
+      --  for later processing by Instantiate_Bodies.
+
+      Pending_Instantiations.Append
+        ((Act_Decl                 => Act_Decl,
+          Config_Switches          => Save_Config_Switches,
+          Current_Sem_Unit         => Current_Sem_Unit,
+          Expander_Status          => Expander_Active,
+          Inst_Node                => Inst,
+          Local_Suppress_Stack_Top => Local_Suppress_Stack_Top,
+          Scope_Suppress           => Scope_Suppress,
+          Warnings                 => Save_Warnings));
+
+      --  With back-end inlining, also associate the index to the instantiation
+
+      if Back_End_Inlining then
+         Act_Decl_Id := Defining_Entity (Act_Decl);
+         Index := Pending_Instantiations.Last;
+
+         To_Pending_Instantiations.Set (Act_Decl, Index);
+
+         --  If an instantiation is either a compilation unit or is in the main
+         --  unit or subunit or is a nested subprogram, then its body is needed
+         --  as per the analysis already done in Analyze_Package_Instantiation
+         --  and Analyze_Subprogram_Instantiation.
+
+         if Nkind (Parent (Inst)) = N_Compilation_Unit
+           or else In_Main_Unit_Or_Subunit (Act_Decl_Id)
+           or else (Is_Subprogram (Act_Decl_Id)
+                     and then Is_Nested (Act_Decl_Id))
+         then
+            Called_Pending_Instantiations.Append (Index);
+
+            Set_Is_Called (Act_Decl_Id);
+         end if;
+      end if;
+   end Add_Pending_Instantiation;
+
    ------------------------
    -- Add_Scope_To_Clean --
    ------------------------
@@ -567,7 +903,6 @@ package body Inline is
          Inlined.Table (Inlined.Last).Name        := E;
          Inlined.Table (Inlined.Last).Next        := No_Subp;
          Inlined.Table (Inlined.Last).First_Succ  := No_Succ;
-         Inlined.Table (Inlined.Last).Listed      := False;
          Inlined.Table (Inlined.Last).Main_Call   := False;
          Inlined.Table (Inlined.Last).Processed   := False;
       end New_Entry;
@@ -622,57 +957,6 @@ package body Inline is
          Table_Name           => "Pending_Inlined");
       --  The workpile used to compute the transitive closure
 
-      function Is_Ancestor_Of_Main
-        (U_Name : Entity_Id;
-         Nam    : Node_Id) return Boolean;
-      --  Determine whether the unit whose body is loaded is an ancestor of
-      --  the main unit, and has a with_clause on it. The body is not
-      --  analyzed yet, so the check is purely lexical: the name of the with
-      --  clause is a selected component, and names of ancestors must match.
-
-      -------------------------
-      -- Is_Ancestor_Of_Main --
-      -------------------------
-
-      function Is_Ancestor_Of_Main
-        (U_Name : Entity_Id;
-         Nam    : Node_Id) return Boolean
-      is
-         Pref : Node_Id;
-
-      begin
-         if Nkind (Nam) /= N_Selected_Component then
-            return False;
-
-         else
-            if Chars (Selector_Name (Nam)) /=
-               Chars (Cunit_Entity (Main_Unit))
-            then
-               return False;
-            end if;
-
-            Pref := Prefix (Nam);
-            if Nkind (Pref) = N_Identifier then
-
-               --  Par is an ancestor of Par.Child.
-
-               return Chars (Pref) = Chars (U_Name);
-
-            elsif Nkind (Pref) = N_Selected_Component
-              and then Chars (Selector_Name (Pref)) = Chars (U_Name)
-            then
-               --  Par.Child is an ancestor of Par.Child.Grand.
-
-               return True;   --  should check that ancestor match
-
-            else
-               --  A is an ancestor of A.B.C if it is an ancestor of A.B
-
-               return Is_Ancestor_Of_Main (U_Name, Pref);
-            end if;
-         end if;
-      end Is_Ancestor_Of_Main;
-
    --  Start of processing for Analyze_Inlined_Bodies
 
    begin
@@ -698,14 +982,19 @@ package body Inline is
                Comp_Unit := Parent (Comp_Unit);
             end loop;
 
-            --  Load the body, unless it is the main unit, or is an instance
-            --  whose body has already been analyzed.
+            --  Load the body if it exists and contains inlineable entities,
+            --  unless it is the main unit, or is an instance whose body has
+            --  already been analyzed.
 
             if Present (Comp_Unit)
               and then Comp_Unit /= Cunit (Main_Unit)
               and then Body_Required (Comp_Unit)
-              and then (Nkind (Unit (Comp_Unit)) /= N_Package_Declaration
-                         or else No (Corresponding_Body (Unit (Comp_Unit))))
+              and then
+                (Nkind (Unit (Comp_Unit)) /= N_Package_Declaration
+                  or else
+                    (No (Corresponding_Body (Unit (Comp_Unit)))
+                      and then Body_Needed_For_Inlining
+                                 (Defining_Entity (Unit (Comp_Unit)))))
             then
                declare
                   Bname : constant Unit_Name_Type :=
@@ -716,7 +1005,7 @@ package body Inline is
                begin
                   if not Is_Loaded (Bname) then
                      Style_Check := False;
-                     Load_Needed_Body (Comp_Unit, OK, Do_Analyze => False);
+                     Load_Needed_Body (Comp_Unit, OK);
 
                      if not OK then
 
@@ -730,65 +1019,33 @@ package body Inline is
                         Error_Msg_File_1 :=
                           Get_File_Name (Bname, Subunit => False);
                         Error_Msg_N ("\but file{ was not found!??", Comp_Unit);
-
-                     else
-                        --  If the package to be inlined is an ancestor unit of
-                        --  the main unit, and it has a semantic dependence on
-                        --  it, the inlining cannot take place to prevent an
-                        --  elaboration circularity. The desired body is not
-                        --  analyzed yet, to prevent the completion of Taft
-                        --  amendment types that would lead to elaboration
-                        --  circularities in gigi.
-
-                        declare
-                           U_Id      : constant Entity_Id :=
-                                         Defining_Entity (Unit (Comp_Unit));
-                           Body_Unit : constant Node_Id :=
-                                         Library_Unit (Comp_Unit);
-                           Item      : Node_Id;
-
-                        begin
-                           Item := First (Context_Items (Body_Unit));
-                           while Present (Item) loop
-                              if Nkind (Item) = N_With_Clause
-                                and then
-                                  Is_Ancestor_Of_Main (U_Id, Name (Item))
-                              then
-                                 Set_Is_Inlined (U_Id, False);
-                                 exit;
-                              end if;
-
-                              Next (Item);
-                           end loop;
-
-                           --  If no suspicious with_clauses, analyze the body.
-
-                           if Is_Inlined (U_Id) then
-                              Semantics (Body_Unit);
-                           end if;
-                        end;
                      end if;
                   end if;
                end;
             end if;
 
             J := J + 1;
-         end loop;
 
-         --  The analysis of required bodies may have produced additional
-         --  generic instantiations. To obtain further inlining, we perform
-         --  another round of generic body instantiations. Establishing a
-         --  fully recursive loop between inlining and generic instantiations
-         --  is unlikely to yield more than this one additional pass.
+            if J > Inlined_Bodies.Last then
+
+               --  The analysis of required bodies may have produced additional
+               --  generic instantiations. To obtain further inlining, we need
+               --  to perform another round of generic body instantiations.
 
-         Instantiate_Bodies;
+               Instantiate_Bodies;
+
+               --  Symmetrically, the instantiation of required generic bodies
+               --  may have caused additional bodies to be inlined. To obtain
+               --  further inlining, we keep looping over the inlined bodies.
+            end if;
+         end loop;
 
          --  The list of inlined subprograms is an overestimate, because it
          --  includes inlined functions called from functions that are compiled
          --  as part of an inlined package, but are not themselves called. An
          --  accurate computation of just those subprograms that are needed
          --  requires that we perform a transitive closure over the call graph,
-         --  starting from calls in the main program.
+         --  starting from calls in the main compilation unit.
 
          for Index in Inlined.First .. Inlined.Last loop
             if not Is_Called (Inlined.Table (Index).Name) then
@@ -835,10 +1092,8 @@ package body Inline is
          --  subprograms for the unit.
 
          for Index in Inlined.First .. Inlined.Last loop
-            if Is_Called (Inlined.Table (Index).Name)
-              and then not Inlined.Table (Index).Listed
-            then
-               Add_Inlined_Subprogram (Index);
+            if Is_Called (Inlined.Table (Index).Name) then
+               Add_Inlined_Subprogram (Inlined.Table (Index).Name);
             end if;
          end loop;
 
@@ -857,6 +1112,10 @@ package body Inline is
       Body_To_Analyze : Node_Id;
       Max_Size        : constant := 10;
 
+      function Has_Extended_Return return Boolean;
+      --  This function returns True if the subprogram has an extended return
+      --  statement.
+
       function Has_Pending_Instantiation return Boolean;
       --  If some enclosing body contains instantiations that appear before
       --  the corresponding generic body, the enclosing body has a freeze node
@@ -874,8 +1133,51 @@ package body Inline is
 
       function Uses_Secondary_Stack (Bod : Node_Id) return Boolean;
       --  If the body of the subprogram includes a call that returns an
-      --  unconstrained type, the secondary stack is involved, and it
-      --  is not worth inlining.
+      --  unconstrained type, the secondary stack is involved, and it is
+      --  not worth inlining.
+
+      -------------------------
+      -- Has_Extended_Return --
+      -------------------------
+
+      function Has_Extended_Return return Boolean is
+         Body_To_Inline : constant Node_Id := N;
+
+         function Check_Return (N : Node_Id) return Traverse_Result;
+         --  Returns OK on node N if this is not an extended return statement
+
+         ------------------
+         -- Check_Return --
+         ------------------
+
+         function Check_Return (N : Node_Id) return Traverse_Result is
+         begin
+            case Nkind (N) is
+               when N_Extended_Return_Statement =>
+                  return Abandon;
+
+               --  Skip locally declared subprogram bodies inside the body to
+               --  inline, as the return statements inside those do not count.
+
+               when N_Subprogram_Body =>
+                  if N = Body_To_Inline then
+                     return OK;
+                  else
+                     return Skip;
+                  end if;
+
+               when others =>
+                  return OK;
+            end case;
+         end Check_Return;
+
+         function Check_All_Returns is new Traverse_Func (Check_Return);
+
+      --  Start of processing for Has_Extended_Return
+
+      begin
+         return Check_All_Returns (N) /= OK;
+      end Has_Extended_Return;
 
       -------------------------------
       -- Has_Pending_Instantiation --
@@ -909,6 +1211,7 @@ package body Inline is
       -----------------------------------------
 
       function Has_Single_Return_In_GNATprove_Mode return Boolean is
+         Body_To_Inline : constant Node_Id := N;
          Last_Statement : Node_Id := Empty;
 
          function Check_Return (N : Node_Id) return Traverse_Result;
@@ -921,18 +1224,29 @@ package body Inline is
 
          function Check_Return (N : Node_Id) return Traverse_Result is
          begin
-            if Nkind_In (N, N_Simple_Return_Statement,
-                            N_Extended_Return_Statement)
-            then
-               if N = Last_Statement then
-                  return OK;
-               else
-                  return Abandon;
-               end if;
+            case Nkind (N) is
+               when N_Extended_Return_Statement
+                  | N_Simple_Return_Statement
+               =>
+                  if N = Last_Statement then
+                     return OK;
+                  else
+                     return Abandon;
+                  end if;
 
-            else
-               return OK;
-            end if;
+               --  Skip locally declared subprogram bodies inside the body to
+               --  inline, as the return statements inside those do not count.
+
+               when N_Subprogram_Body =>
+                  if N = Body_To_Inline then
+                     return OK;
+                  else
+                     return Skip;
+                  end if;
+
+               when others =>
+                  return OK;
+            end case;
          end Check_Return;
 
          function Check_All_Returns is new Traverse_Func (Check_Return);
@@ -1004,24 +1318,9 @@ package body Inline is
          Cannot_Inline ("cannot inline & (multiple returns)?", N, Spec_Id);
          return;
 
-      --  Functions that return unconstrained composite types require
-      --  secondary stack handling, and cannot currently be inlined, unless
-      --  all return statements return a local variable that is the first
-      --  local declaration in the body.
-
-      elsif Ekind (Spec_Id) = E_Function
-        and then not Is_Scalar_Type (Etype (Spec_Id))
-        and then not Is_Access_Type (Etype (Spec_Id))
-        and then not Is_Constrained (Etype (Spec_Id))
-      then
-         if not Has_Single_Return (N) then
-            Cannot_Inline
-              ("cannot inline & (unconstrained return type)?", N, Spec_Id);
-            return;
-         end if;
-
-      --  Ditto for functions that return controlled types, where controlled
-      --  actions interfere in complex ways with inlining.
+      --  Functions that return controlled types cannot currently be inlined
+      --  because they require secondary stack handling; controlled actions
+      --  may also interfere in complex ways with inlining.
 
       elsif Ekind (Spec_Id) = E_Function
         and then Needs_Finalization (Etype (Spec_Id))
@@ -1076,12 +1375,12 @@ package body Inline is
       --  generic, so that the proper global references are preserved.
 
       --  Note that we do not do this at the library level, because it is not
-      --  needed, and furthermore this causes trouble if front end inlining
+      --  needed, and furthermore this causes trouble if front-end inlining
       --  is activated (-gnatN).
 
       if In_Instance and then Scope (Current_Scope) /= Standard_Standard then
          Save_Env (Scope (Current_Scope), Scope (Current_Scope));
-         Original_Body := Copy_Generic_Node (N, Empty, True);
+         Original_Body := Copy_Generic_Node (N, Empty, Instantiating => True);
       else
          Original_Body := Copy_Separate_Tree (N);
       end if;
@@ -1097,21 +1396,23 @@ package body Inline is
       Set_Parameter_Specifications (Specification (Original_Body), No_List);
       Set_Defining_Unit_Name
         (Specification (Original_Body),
-          Make_Defining_Identifier (Sloc (N), Name_uParent));
+         Make_Defining_Identifier (Sloc (N), Name_uParent));
       Set_Corresponding_Spec (Original_Body, Empty);
 
-      --  Remove those pragmas that have no meaining in an inlined body.
+      --  Remove all aspects/pragmas that have no meaning in an inlined body
 
-      Remove_Pragmas (Original_Body);
+      Remove_Aspects_And_Pragmas (Original_Body);
 
-      Body_To_Analyze := Copy_Generic_Node (Original_Body, Empty, False);
+      Body_To_Analyze :=
+        Copy_Generic_Node (Original_Body, Empty, Instantiating => False);
 
       --  Set return type of function, which is also global and does not need
       --  to be resolved.
 
       if Ekind (Spec_Id) = E_Function then
-         Set_Result_Definition (Specification (Body_To_Analyze),
-           New_Occurrence_Of (Etype (Spec_Id), Sloc (N)));
+         Set_Result_Definition
+           (Specification (Body_To_Analyze),
+            New_Occurrence_Of (Etype (Spec_Id), Sloc (N)));
       end if;
 
       if No (Declarations (N)) then
@@ -1120,9 +1421,9 @@ package body Inline is
          Append (Body_To_Analyze, Declarations (N));
       end if;
 
-      --  The body to inline is pre-analyzed.  In GNATprove mode we must
-      --  disable full analysis as well so that light expansion does not
-      --  take place either, and name resolution is unaffected.
+      --  The body to inline is preanalyzed. In GNATprove mode we must disable
+      --  full analysis as well so that light expansion does not take place
+      --  either, and name resolution is unaffected.
 
       Expander_Mode_Save_And_Set (False);
       Full_Analysis := False;
@@ -1142,235 +1443,211 @@ package body Inline is
          Restore_Env;
       end if;
 
-      --  If secondary stack is used, there is no point in inlining. We have
-      --  already issued the warning in this case, so nothing to do.
+      --  Functions that return unconstrained composite types require
+      --  secondary stack handling, and cannot currently be inlined, unless
+      --  all return statements return a local variable that is the first
+      --  local declaration in the body. We had to delay this check until
+      --  the body of the function is analyzed since Has_Single_Return()
+      --  requires a minimum decoration.
 
-      if Uses_Secondary_Stack (Body_To_Analyze) then
-         return;
-      end if;
+      if Ekind (Spec_Id) = E_Function
+        and then not Is_Scalar_Type (Etype (Spec_Id))
+        and then not Is_Access_Type (Etype (Spec_Id))
+        and then not Is_Constrained (Etype (Spec_Id))
+      then
+         if not Has_Single_Return (Body_To_Analyze)
 
-      Set_Body_To_Inline (Decl, Original_Body);
-      Set_Ekind (Defining_Entity (Original_Body), Ekind (Spec_Id));
-      Set_Is_Inlined (Spec_Id);
-   end Build_Body_To_Inline;
-
-   -------------------
-   -- Cannot_Inline --
-   -------------------
-
-   procedure Cannot_Inline
-     (Msg        : String;
-      N          : Node_Id;
-      Subp       : Entity_Id;
-      Is_Serious : Boolean := False)
-   is
-   begin
-      --  In GNATprove mode, inlining is the technical means by which the
-      --  higher-level goal of contextual analysis is reached, so issue
-      --  messages about failure to apply contextual analysis to a
-      --  subprogram, rather than failure to inline it.
+           --  Skip inlining if the function returns an unconstrained type
+           --  using an extended return statement, since this part of the
+           --  new inlining model is not yet supported by the current
+           --  implementation. ???
 
-      if GNATprove_Mode
-        and then Msg (Msg'First .. Msg'First + 12) = "cannot inline"
-      then
-         declare
-            Len1 : constant Positive :=
-              String (String'("cannot inline"))'Length;
-            Len2 : constant Positive :=
-              String (String'("info: no contextual analysis of"))'Length;
+           or else (Returns_Unconstrained_Type (Spec_Id)
+                     and then Has_Extended_Return)
+         then
+            Cannot_Inline
+              ("cannot inline & (unconstrained return type)?", N, Spec_Id);
+            return;
+         end if;
 
-            New_Msg : String (1 .. Msg'Length + Len2 - Len1);
+      --  If secondary stack is used, there is no point in inlining. We have
+      --  already issued the warning in this case, so nothing to do.
 
-         begin
-            New_Msg (1 .. Len2) := "info: no contextual analysis of";
-            New_Msg (Len2 + 1 .. Msg'Length + Len2 - Len1) :=
-              Msg (Msg'First + Len1 .. Msg'Last);
-            Cannot_Inline (New_Msg, N, Subp, Is_Serious);
-            return;
-         end;
+      elsif Uses_Secondary_Stack (Body_To_Analyze) then
+         return;
       end if;
 
-      pragma Assert (Msg (Msg'Last) = '?');
-
-      --  Legacy front end inlining model
+      Set_Body_To_Inline (Decl, Original_Body);
+      Set_Ekind (Defining_Entity (Original_Body), Ekind (Spec_Id));
+      Set_Is_Inlined (Spec_Id);
+   end Build_Body_To_Inline;
 
-      if not Back_End_Inlining then
+   -------------------------------------------
+   -- Call_Can_Be_Inlined_In_GNATprove_Mode --
+   -------------------------------------------
 
-         --  Do not emit warning if this is a predefined unit which is not
-         --  the main unit. With validity checks enabled, some predefined
-         --  subprograms may contain nested subprograms and become ineligible
-         --  for inlining.
+   function Call_Can_Be_Inlined_In_GNATprove_Mode
+    (N    : Node_Id;
+     Subp : Entity_Id) return Boolean
+   is
+      F : Entity_Id;
+      A : Node_Id;
 
-         if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Subp)))
-           and then not In_Extended_Main_Source_Unit (Subp)
+   begin
+      F := First_Formal (Subp);
+      A := First_Actual (N);
+      while Present (F) loop
+         if Ekind (F) /= E_Out_Parameter
+           and then not Same_Type (Etype (F), Etype (A))
+           and then
+             (Is_By_Reference_Type (Etype (A))
+               or else Is_Limited_Type (Etype (A)))
          then
-            null;
-
-         --  In GNATprove mode, issue a warning, and indicate that the
-         --  subprogram is not always inlined by setting flag Is_Inlined_Always
-         --  to False.
-
-         elsif GNATprove_Mode then
-            Set_Is_Inlined_Always (Subp, False);
-            Error_Msg_NE (Msg & "p?", N, Subp);
-
-         elsif Has_Pragma_Inline_Always (Subp) then
-
-            --  Remove last character (question mark) to make this into an
-            --  error, because the Inline_Always pragma cannot be obeyed.
-
-            Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
-
-         elsif Ineffective_Inline_Warnings then
-            Error_Msg_NE (Msg & "p?", N, Subp);
+            return False;
          end if;
 
-         return;
-
-      --  New semantics
-
-      elsif Is_Serious then
+         Next_Formal (F);
+         Next_Actual (A);
+      end loop;
 
-         --  Remove last character (question mark) to make this into an error.
+      return True;
+   end Call_Can_Be_Inlined_In_GNATprove_Mode;
 
-         Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
+   --------------------------------------
+   -- Can_Be_Inlined_In_GNATprove_Mode --
+   --------------------------------------
 
-      --  In GNATprove mode, issue a warning, and indicate that the subprogram
-      --  is not always inlined by setting flag Is_Inlined_Always to False.
+   function Can_Be_Inlined_In_GNATprove_Mode
+     (Spec_Id : Entity_Id;
+      Body_Id : Entity_Id) return Boolean
+   is
+      function Has_Formal_With_Discriminant_Dependent_Fields
+        (Id : Entity_Id) return Boolean;
+      --  Returns true if the subprogram has at least one formal parameter of
+      --  an unconstrained record type with per-object constraints on component
+      --  types.
 
-      elsif GNATprove_Mode then
-         Set_Is_Inlined_Always (Subp, False);
-         Error_Msg_NE (Msg & "p?", N, Subp);
+      function Has_Some_Contract (Id : Entity_Id) return Boolean;
+      --  Return True if subprogram Id has any contract. The presence of
+      --  Extensions_Visible or Volatile_Function is also considered as a
+      --  contract here.
 
-      --  Do not issue errors/warnings when compiling with optimizations
+      function Is_Unit_Subprogram (Id : Entity_Id) return Boolean;
+      --  Return True if subprogram Id defines a compilation unit
+      --  Shouldn't this be in Sem_Aux???
 
-      elsif Optimization_Level = 0 then
+      function In_Package_Spec (Id : Entity_Id) return Boolean;
+      --  Return True if subprogram Id is defined in the package specification,
+      --  either its visible or private part.
 
-         --  Do not emit warning if this is a predefined unit which is not
-         --  the main unit. This behavior is currently provided for backward
-         --  compatibility but it will be removed when we enforce the
-         --  strictness of the new rules.
+      ---------------------------------------------------
+      -- Has_Formal_With_Discriminant_Dependent_Fields --
+      ---------------------------------------------------
 
-         if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Subp)))
-           and then not In_Extended_Main_Source_Unit (Subp)
-         then
-            null;
+      function Has_Formal_With_Discriminant_Dependent_Fields
+        (Id : Entity_Id) return Boolean
+      is
+         function Has_Discriminant_Dependent_Component
+           (Typ : Entity_Id) return Boolean;
+         --  Determine whether unconstrained record type Typ has at least one
+         --  component that depends on a discriminant.
 
-         elsif Has_Pragma_Inline_Always (Subp) then
+         ------------------------------------------
+         -- Has_Discriminant_Dependent_Component --
+         ------------------------------------------
 
-            --  Emit a warning if this is a call to a runtime subprogram
-            --  which is located inside a generic. Previously this call
-            --  was silently skipped.
+         function Has_Discriminant_Dependent_Component
+           (Typ : Entity_Id) return Boolean
+         is
+            Comp : Entity_Id;
 
-            if Is_Generic_Instance (Subp) then
-               declare
-                  Gen_P : constant Entity_Id := Generic_Parent (Parent (Subp));
-               begin
-                  if Is_Predefined_File_Name
-                       (Unit_File_Name (Get_Source_Unit (Gen_P)))
-                  then
-                     Set_Is_Inlined (Subp, False);
-                     Error_Msg_NE (Msg & "p?", N, Subp);
-                     return;
-                  end if;
-               end;
-            end if;
+         begin
+            --  Inspect all components of the record type looking for one that
+            --  depends on a discriminant.
 
-            --  Remove last character (question mark) to make this into an
-            --  error, because the Inline_Always pragma cannot be obeyed.
+            Comp := First_Component (Typ);
+            while Present (Comp) loop
+               if Has_Discriminant_Dependent_Constraint (Comp) then
+                  return True;
+               end if;
 
-            Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
+               Next_Component (Comp);
+            end loop;
 
-         else pragma Assert (Front_End_Inlining);
-            Set_Is_Inlined (Subp, False);
+            return False;
+         end Has_Discriminant_Dependent_Component;
 
-            --  When inlining cannot take place we must issue an error.
-            --  For backward compatibility we still report a warning.
+         --  Local variables
 
-            if Ineffective_Inline_Warnings then
-               Error_Msg_NE (Msg & "p?", N, Subp);
-            end if;
-         end if;
+         Subp_Id    : constant Entity_Id := Ultimate_Alias (Id);
+         Formal     : Entity_Id;
+         Formal_Typ : Entity_Id;
 
-      --  Compiling with optimizations enabled it is too early to report
-      --  problems since the backend may still perform inlining. In order
-      --  to report unhandled inlinings the program must be compiled with
-      --  -Winline and the error is reported by the backend.
+      --  Start of processing for
+      --  Has_Formal_With_Discriminant_Dependent_Fields
 
-      else
-         null;
-      end if;
-   end Cannot_Inline;
-
-   --------------------------------------
-   -- Can_Be_Inlined_In_GNATprove_Mode --
-   --------------------------------------
+      begin
+         --  Inspect all parameters of the subprogram looking for a formal
+         --  of an unconstrained record type with at least one discriminant
+         --  dependent component.
 
-   function Can_Be_Inlined_In_GNATprove_Mode
-     (Spec_Id : Entity_Id;
-      Body_Id : Entity_Id) return Boolean
-   is
-      function Has_Some_Contract (Id : Entity_Id) return Boolean;
-      --  Returns True if subprogram Id has any contract (Pre, Post, Global,
-      --  Depends, etc.)
+         Formal := First_Formal (Subp_Id);
+         while Present (Formal) loop
+            Formal_Typ := Etype (Formal);
 
-      function Is_Unit_Subprogram (Id : Entity_Id) return Boolean;
-      --  Returns True if subprogram Id defines a compilation unit
-      --  Shouldn't this be in Sem_Aux???
+            if Is_Record_Type (Formal_Typ)
+              and then not Is_Constrained (Formal_Typ)
+              and then Has_Discriminant_Dependent_Component (Formal_Typ)
+            then
+               return True;
+            end if;
 
-      function In_Package_Visible_Spec (Id : Node_Id) return Boolean;
-      --  Returns True if subprogram Id is defined in the visible part of a
-      --  package specification.
+            Next_Formal (Formal);
+         end loop;
 
-      function Is_Expression_Function (Id : Entity_Id) return Boolean;
-      --  Returns True if subprogram Id was defined originally as an expression
-      --  function.
+         return False;
+      end Has_Formal_With_Discriminant_Dependent_Fields;
 
       -----------------------
       -- Has_Some_Contract --
       -----------------------
 
       function Has_Some_Contract (Id : Entity_Id) return Boolean is
-         Items : constant Node_Id := Contract (Id);
-      begin
-         return Present (Items)
-           and then (Present (Pre_Post_Conditions (Items)) or else
-                     Present (Contract_Test_Cases (Items)) or else
-                     Present (Classifications     (Items)));
-      end Has_Some_Contract;
-
-      -----------------------------
-      -- In_Package_Visible_Spec --
-      -----------------------------
-
-      function In_Package_Visible_Spec  (Id : Node_Id) return Boolean is
-         Decl : Node_Id := Parent (Parent (Id));
-         P    : Node_Id;
+         Items : Node_Id;
 
       begin
-         if Nkind (Parent (Id)) = N_Defining_Program_Unit_Name then
-            Decl := Parent (Decl);
+         --  A call to an expression function may precede the actual body which
+         --  is inserted at the end of the enclosing declarations. Ensure that
+         --  the related entity is decorated before inspecting the contract.
+
+         if Is_Subprogram_Or_Generic_Subprogram (Id) then
+            Items := Contract (Id);
+
+            --  Note that Classifications is not Empty when Extensions_Visible
+            --  or Volatile_Function is present, which causes such subprograms
+            --  to be considered to have a contract here. This is fine as we
+            --  want to avoid inlining these too.
+
+            return Present (Items)
+              and then (Present (Pre_Post_Conditions (Items)) or else
+                        Present (Contract_Test_Cases (Items)) or else
+                        Present (Classifications     (Items)));
          end if;
 
-         P := Parent (Decl);
+         return False;
+      end Has_Some_Contract;
 
-         return Nkind (P) = N_Package_Specification
-           and then List_Containing (Decl) = Visible_Declarations (P);
-      end In_Package_Visible_Spec;
+      ---------------------
+      -- In_Package_Spec --
+      ---------------------
 
-      ----------------------------
-      -- Is_Expression_Function --
-      ----------------------------
+      function In_Package_Spec (Id : Entity_Id) return Boolean is
+         P : constant Node_Id := Parent (Subprogram_Spec (Id));
+         --  Parent of the subprogram's declaration
 
-      function Is_Expression_Function (Id : Entity_Id) return Boolean is
-         Decl : Node_Id := Parent (Parent (Id));
       begin
-         if Nkind (Parent (Id)) = N_Defining_Program_Unit_Name then
-            Decl := Parent (Decl);
-         end if;
-
-         return Nkind (Original_Node (Decl)) = N_Expression_Function;
-      end Is_Expression_Function;
+         return Nkind (Enclosing_Declaration (P)) = N_Package_Declaration;
+      end In_Package_Spec;
 
       ------------------------
       -- Is_Unit_Subprogram --
@@ -1388,9 +1665,10 @@ package body Inline is
 
       --  Local declarations
 
-      Id : Entity_Id;  --  Procedure or function entity for the subprogram
+      Id : Entity_Id;
+      --  Procedure or function entity for the subprogram
 
-   --  Start of Can_Be_Inlined_In_GNATprove_Mode
+   --  Start of processing for Can_Be_Inlined_In_GNATprove_Mode
 
    begin
       pragma Assert (Present (Spec_Id) or else Present (Body_Id));
@@ -1415,13 +1693,31 @@ package body Inline is
       if Is_Unit_Subprogram (Id) then
          return False;
 
-      --  Do not inline subprograms declared in the visible part of a package
+      --  Do not inline subprograms declared in package specs, because they are
+      --  not local, i.e. can be called either from anywhere (if declared in
+      --  visible part) or from the child units (if declared in private part).
+
+      elsif In_Package_Spec (Id) then
+         return False;
+
+      --  Do not inline subprograms declared in other units. This is important
+      --  in particular for subprograms defined in the private part of a
+      --  package spec, when analyzing one of its child packages, as otherwise
+      --  we issue spurious messages about the impossibility to inline such
+      --  calls.
 
-      elsif In_Package_Visible_Spec (Id) then
+      elsif not In_Extended_Main_Code_Unit (Id) then
+         return False;
+
+      --  Do not inline subprograms marked No_Return, possibly used for
+      --  signaling errors, which GNATprove handles specially.
+
+      elsif No_Return (Id) then
          return False;
 
       --  Do not inline subprograms that have a contract on the spec or the
-      --  body. Use the contract(s) instead in GNATprove.
+      --  body. Use the contract(s) instead in GNATprove. This also prevents
+      --  inlining of subprograms with Extensions_Visible or Volatile_Function.
 
       elsif (Present (Spec_Id) and then Has_Some_Contract (Spec_Id))
                or else
@@ -1451,7 +1747,8 @@ package body Inline is
       elsif Present (Spec_Id)
         and then
           (No (SPARK_Pragma (Spec_Id))
-            or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
+            or else
+           Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) /= On)
       then
          return False;
 
@@ -1461,11 +1758,27 @@ package body Inline is
       elsif Instantiation_Location (Sloc (Id)) /= No_Location then
          return False;
 
-      --  Don't inline predicate functions (treated specially by GNATprove)
+      --  Do not inline subprograms and entries defined inside protected types,
+      --  which typically are not helper subprograms, which also avoids getting
+      --  spurious messages on calls that cannot be inlined.
+
+      elsif Within_Protected_Type (Id) then
+         return False;
+
+      --  Do not inline predicate functions (treated specially by GNATprove)
 
       elsif Is_Predicate_Function (Id) then
          return False;
 
+      --  Do not inline subprograms with a parameter of an unconstrained
+      --  record type if it has discrimiant dependent fields. Indeed, with
+      --  such parameters, the frontend cannot always ensure type compliance
+      --  in record component accesses (in particular with records containing
+      --  packed arrays).
+
+      elsif Has_Formal_With_Discriminant_Dependent_Fields (Id) then
+         return False;
+
       --  Otherwise, this is a subprogram declared inside the private part of a
       --  package, or inside a package body, or locally in a subprogram, and it
       --  does not have any contract. Inline it.
@@ -1475,6 +1788,144 @@ package body Inline is
       end if;
    end Can_Be_Inlined_In_GNATprove_Mode;
 
+   -------------------
+   -- Cannot_Inline --
+   -------------------
+
+   procedure Cannot_Inline
+     (Msg        : String;
+      N          : Node_Id;
+      Subp       : Entity_Id;
+      Is_Serious : Boolean := False)
+   is
+   begin
+      --  In GNATprove mode, inlining is the technical means by which the
+      --  higher-level goal of contextual analysis is reached, so issue
+      --  messages about failure to apply contextual analysis to a
+      --  subprogram, rather than failure to inline it.
+
+      if GNATprove_Mode
+        and then Msg (Msg'First .. Msg'First + 12) = "cannot inline"
+      then
+         declare
+            Len1 : constant Positive :=
+              String (String'("cannot inline"))'Length;
+            Len2 : constant Positive :=
+              String (String'("info: no contextual analysis of"))'Length;
+
+            New_Msg : String (1 .. Msg'Length + Len2 - Len1);
+
+         begin
+            New_Msg (1 .. Len2) := "info: no contextual analysis of";
+            New_Msg (Len2 + 1 .. Msg'Length + Len2 - Len1) :=
+              Msg (Msg'First + Len1 .. Msg'Last);
+            Cannot_Inline (New_Msg, N, Subp, Is_Serious);
+            return;
+         end;
+      end if;
+
+      pragma Assert (Msg (Msg'Last) = '?');
+
+      --  Legacy front-end inlining model
+
+      if not Back_End_Inlining then
+
+         --  Do not emit warning if this is a predefined unit which is not
+         --  the main unit. With validity checks enabled, some predefined
+         --  subprograms may contain nested subprograms and become ineligible
+         --  for inlining.
+
+         if Is_Predefined_Unit (Get_Source_Unit (Subp))
+           and then not In_Extended_Main_Source_Unit (Subp)
+         then
+            null;
+
+         --  In GNATprove mode, issue a warning when -gnatd_f is set, and
+         --  indicate that the subprogram is not always inlined by setting
+         --  flag Is_Inlined_Always to False.
+
+         elsif GNATprove_Mode then
+            Set_Is_Inlined_Always (Subp, False);
+
+            if Debug_Flag_Underscore_F then
+               Error_Msg_NE (Msg, N, Subp);
+            end if;
+
+         elsif Has_Pragma_Inline_Always (Subp) then
+
+            --  Remove last character (question mark) to make this into an
+            --  error, because the Inline_Always pragma cannot be obeyed.
+
+            Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
+
+         elsif Ineffective_Inline_Warnings then
+            Error_Msg_NE (Msg & "p?", N, Subp);
+         end if;
+
+      --  New semantics relying on back-end inlining
+
+      elsif Is_Serious then
+
+         --  Remove last character (question mark) to make this into an error.
+
+         Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
+
+      --  In GNATprove mode, issue a warning when -gnatd_f is set, and
+      --  indicate that the subprogram is not always inlined by setting
+      --  flag Is_Inlined_Always to False.
+
+      elsif GNATprove_Mode then
+         Set_Is_Inlined_Always (Subp, False);
+
+         if Debug_Flag_Underscore_F then
+            Error_Msg_NE (Msg, N, Subp);
+         end if;
+
+      else
+
+         --  Do not emit warning if this is a predefined unit which is not
+         --  the main unit. This behavior is currently provided for backward
+         --  compatibility but it will be removed when we enforce the
+         --  strictness of the new rules.
+
+         if Is_Predefined_Unit (Get_Source_Unit (Subp))
+           and then not In_Extended_Main_Source_Unit (Subp)
+         then
+            null;
+
+         elsif Has_Pragma_Inline_Always (Subp) then
+
+            --  Emit a warning if this is a call to a runtime subprogram
+            --  which is located inside a generic. Previously this call
+            --  was silently skipped.
+
+            if Is_Generic_Instance (Subp) then
+               declare
+                  Gen_P : constant Entity_Id := Generic_Parent (Parent (Subp));
+               begin
+                  if Is_Predefined_Unit (Get_Source_Unit (Gen_P)) then
+                     Set_Is_Inlined (Subp, False);
+                     Error_Msg_NE (Msg & "p?", N, Subp);
+                     return;
+                  end if;
+               end;
+            end if;
+
+            --  Remove last character (question mark) to make this into an
+            --  error, because the Inline_Always pragma cannot be obeyed.
+
+            Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
+
+         else
+            Set_Is_Inlined (Subp, False);
+
+            if Ineffective_Inline_Warnings then
+               Error_Msg_NE (Msg & "p?", N, Subp);
+            end if;
+         end if;
+      end if;
+   end Cannot_Inline;
+
    --------------------------------------------
    -- Check_And_Split_Unconstrained_Function --
    --------------------------------------------
@@ -1488,19 +1939,28 @@ package body Inline is
       --  Use generic machinery to build an unexpanded body for the subprogram.
       --  This body is subsequently used for inline expansions at call sites.
 
+      procedure Build_Return_Object_Formal
+        (Loc      : Source_Ptr;
+         Obj_Decl : Node_Id;
+         Formals  : List_Id);
+      --  Create a formal parameter for return object declaration Obj_Decl of
+      --  an extended return statement and add it to list Formals.
+
       function Can_Split_Unconstrained_Function (N : Node_Id) return Boolean;
       --  Return true if we generate code for the function body N, the function
       --  body N has no local declarations and its unique statement is a single
       --  extended return statement with a handled statements sequence.
 
-      procedure Generate_Subprogram_Body
-        (N              : Node_Id;
-         Body_To_Inline : out Node_Id);
-      --  Generate a parameterless duplicate of subprogram body N. Occurrences
-      --  of pragmas referencing the formals are removed since they have no
-      --  meaning when the body is inlined and the formals are rewritten (the
-      --  analysis of the non-inlined body will handle these pragmas properly).
-      --  A new internal name is associated with Body_To_Inline.
+      procedure Copy_Formals
+        (Loc     : Source_Ptr;
+         Subp_Id : Entity_Id;
+         Formals : List_Id);
+      --  Create new formal parameters from the formal parameters of subprogram
+      --  Subp_Id and add them to list Formals.
+
+      function Copy_Return_Object (Obj_Decl : Node_Id) return Node_Id;
+      --  Create a copy of return object declaration Obj_Decl of an extended
+      --  return statement.
 
       procedure Split_Unconstrained_Function
         (N       : Node_Id;
@@ -1508,7 +1968,7 @@ package body Inline is
       --  N is an inlined function body that returns an unconstrained type and
       --  has a single extended return statement. Split N in two subprograms:
       --  a procedure P' and a function F'. The formals of P' duplicate the
-      --  formals of N plus an extra formal which is used return a value;
+      --  formals of N plus an extra formal which is used to return a value;
       --  its body is composed by the declarations and list of statements
       --  of the extended return statement of N.
 
@@ -1517,17 +1977,79 @@ package body Inline is
       --------------------------
 
       procedure Build_Body_To_Inline (N : Node_Id; Spec_Id : Entity_Id) is
+         procedure Generate_Subprogram_Body
+           (N              : Node_Id;
+            Body_To_Inline : out Node_Id);
+         --  Generate a parameterless duplicate of subprogram body N. Note that
+         --  occurrences of pragmas referencing the formals are removed since
+         --  they have no meaning when the body is inlined and the formals are
+         --  rewritten (the analysis of the non-inlined body will handle these
+         --  pragmas). A new internal name is associated with Body_To_Inline.
+
+         ------------------------------
+         -- Generate_Subprogram_Body --
+         ------------------------------
+
+         procedure Generate_Subprogram_Body
+           (N              : Node_Id;
+            Body_To_Inline : out Node_Id)
+         is
+         begin
+            --  Within an instance, the body to inline must be treated as a
+            --  nested generic so that proper global references are preserved.
+
+            --  Note that we do not do this at the library level, because it
+            --  is not needed, and furthermore this causes trouble if front
+            --  end inlining is activated (-gnatN).
+
+            if In_Instance
+              and then Scope (Current_Scope) /= Standard_Standard
+            then
+               Body_To_Inline :=
+                 Copy_Generic_Node (N, Empty, Instantiating => True);
+            else
+               --  ??? Shouldn't this use New_Copy_Tree? What about global
+               --  references captured in the body to inline?
+
+               Body_To_Inline := Copy_Separate_Tree (N);
+            end if;
+
+            --  Remove aspects/pragmas that have no meaning in an inlined body
+
+            Remove_Aspects_And_Pragmas (Body_To_Inline);
+
+            --  We need to capture references to the formals in order
+            --  to substitute the actuals at the point of inlining, i.e.
+            --  instantiation. To treat the formals as globals to the body to
+            --  inline, we nest it within a dummy parameterless subprogram,
+            --  declared within the real one.
+
+            Set_Parameter_Specifications
+              (Specification (Body_To_Inline), No_List);
+
+            --  A new internal name is associated with Body_To_Inline to avoid
+            --  conflicts when the non-inlined body N is analyzed.
+
+            Set_Defining_Unit_Name (Specification (Body_To_Inline),
+               Make_Defining_Identifier (Sloc (N), New_Internal_Name ('P')));
+            Set_Corresponding_Spec (Body_To_Inline, Empty);
+         end Generate_Subprogram_Body;
+
+         --  Local variables
+
          Decl            : constant Node_Id := Unit_Declaration_Node (Spec_Id);
          Original_Body   : Node_Id;
          Body_To_Analyze : Node_Id;
 
+      --  Start of processing for Build_Body_To_Inline
+
       begin
          pragma Assert (Current_Scope = Spec_Id);
 
          --  Within an instance, the body to inline must be treated as a nested
          --  generic, so that the proper global references are preserved. We
          --  do not do this at the library level, because it is not needed, and
-         --  furthermore this causes trouble if front end inlining is activated
+         --  furthermore this causes trouble if front-end inlining is activated
          --  (-gnatN).
 
          if In_Instance
@@ -1536,14 +2058,14 @@ package body Inline is
             Save_Env (Scope (Current_Scope), Scope (Current_Scope));
          end if;
 
-         --  We need to capture references to the formals in order
-         --  to substitute the actuals at the point of inlining, i.e.
-         --  instantiation. To treat the formals as globals to the body to
-         --  inline, we nest it within a dummy parameterless subprogram,
-         --  declared within the real one.
+         --  Capture references to formals in order to substitute the actuals
+         --  at the point of inlining or instantiation. To treat the formals
+         --  as globals to the body to inline, nest the body within a dummy
+         --  parameterless subprogram, declared within the real one.
 
          Generate_Subprogram_Body (N, Original_Body);
-         Body_To_Analyze := Copy_Generic_Node (Original_Body, Empty, False);
+         Body_To_Analyze :=
+           Copy_Generic_Node (Original_Body, Empty, Instantiating => False);
 
          --  Set return type of function, which is also global and does not
          --  need to be resolved.
@@ -1579,31 +2101,70 @@ package body Inline is
          Set_Ekind (Defining_Entity (Original_Body), Ekind (Spec_Id));
       end Build_Body_To_Inline;
 
+      --------------------------------
+      -- Build_Return_Object_Formal --
+      --------------------------------
+
+      procedure Build_Return_Object_Formal
+        (Loc      : Source_Ptr;
+         Obj_Decl : Node_Id;
+         Formals  : List_Id)
+      is
+         Obj_Def : constant Node_Id   := Object_Definition (Obj_Decl);
+         Obj_Id  : constant Entity_Id := Defining_Entity   (Obj_Decl);
+         Typ_Def : Node_Id;
+
+      begin
+         --  Build the type definition of the formal parameter. The use of
+         --  New_Copy_Tree ensures that global references preserved in the
+         --  case of generics.
+
+         if Is_Entity_Name (Obj_Def) then
+            Typ_Def := New_Copy_Tree (Obj_Def);
+         else
+            Typ_Def := New_Copy_Tree (Subtype_Mark (Obj_Def));
+         end if;
+
+         --  Generate:
+         --
+         --    Obj_Id : [out] Typ_Def
+
+         --  Mode OUT should not be used when the return object is declared as
+         --  a constant. Check the definition of the object declaration because
+         --  the object has not been analyzed yet.
+
+         Append_To (Formals,
+           Make_Parameter_Specification (Loc,
+             Defining_Identifier    =>
+               Make_Defining_Identifier (Loc, Chars (Obj_Id)),
+             In_Present             => False,
+             Out_Present            => not Constant_Present (Obj_Decl),
+             Null_Exclusion_Present => False,
+             Parameter_Type         => Typ_Def));
+      end Build_Return_Object_Formal;
+
       --------------------------------------
       -- Can_Split_Unconstrained_Function --
       --------------------------------------
 
-      function Can_Split_Unconstrained_Function (N : Node_Id) return Boolean
-      is
-         Ret_Node : constant Node_Id :=
-                      First (Statements (Handled_Statement_Sequence (N)));
-         D : Node_Id;
+      function Can_Split_Unconstrained_Function (N : Node_Id) return Boolean is
+         Stmt : constant Node_Id :=
+                  First (Statements (Handled_Statement_Sequence (N)));
+         Decl : Node_Id;
 
       begin
          --  No user defined declarations allowed in the function except inside
          --  the unique return statement; implicit labels are the only allowed
          --  declarations.
 
-         if not Is_Empty_List (Declarations (N)) then
-            D := First (Declarations (N));
-            while Present (D) loop
-               if Nkind (D) /= N_Implicit_Label_Declaration then
-                  return False;
-               end if;
+         Decl := First (Declarations (N));
+         while Present (Decl) loop
+            if Nkind (Decl) /= N_Implicit_Label_Declaration then
+               return False;
+            end if;
 
-               Next (D);
-            end loop;
-         end if;
+            Next (Decl);
+         end loop;
 
          --  We only split the inlined function when we are generating the code
          --  of its body; otherwise we leave duplicated split subprograms in
@@ -1611,59 +2172,70 @@ package body Inline is
          --  time.
 
          return In_Extended_Main_Code_Unit (N)
-           and then Present (Ret_Node)
-           and then Nkind (Ret_Node) = N_Extended_Return_Statement
-           and then No (Next (Ret_Node))
-           and then Present (Handled_Statement_Sequence (Ret_Node));
+           and then Present (Stmt)
+           and then Nkind (Stmt) = N_Extended_Return_Statement
+           and then No (Next (Stmt))
+           and then Present (Handled_Statement_Sequence (Stmt));
       end Can_Split_Unconstrained_Function;
 
-      -----------------------------
-      -- Generate_Body_To_Inline --
-      -----------------------------
+      ------------------
+      -- Copy_Formals --
+      ------------------
 
-      procedure Generate_Subprogram_Body
-        (N              : Node_Id;
-         Body_To_Inline : out Node_Id)
+      procedure Copy_Formals
+        (Loc     : Source_Ptr;
+         Subp_Id : Entity_Id;
+         Formals : List_Id)
       is
-      begin
-         --  Within an instance, the body to inline must be treated as a nested
-         --  generic, so that the proper global references are preserved.
-
-         --  Note that we do not do this at the library level, because it
-         --  is not needed, and furthermore this causes trouble if front
-         --  end inlining is activated (-gnatN).
-
-         if In_Instance
-           and then Scope (Current_Scope) /= Standard_Standard
-         then
-            Body_To_Inline := Copy_Generic_Node (N, Empty, True);
-         else
-            Body_To_Inline := Copy_Separate_Tree (N);
-         end if;
+         Formal : Entity_Id;
+         Spec   : Node_Id;
 
-         --  A pragma Unreferenced or pragma Unmodified that mentions a formal
-         --  parameter has no meaning when the body is inlined and the formals
-         --  are rewritten. Remove it from body to inline. The analysis of the
-         --  non-inlined body will handle the pragma properly.
+      begin
+         Formal := First_Formal (Subp_Id);
+         while Present (Formal) loop
+            Spec := Parent (Formal);
 
-         Remove_Pragmas (Body_To_Inline);
+            --  Create an exact copy of the formal parameter. The use of
+            --  New_Copy_Tree ensures that global references are preserved
+            --  in case of generics.
 
-         --  We need to capture references to the formals in order
-         --  to substitute the actuals at the point of inlining, i.e.
-         --  instantiation. To treat the formals as globals to the body to
-         --  inline, we nest it within a dummy parameterless subprogram,
-         --  declared within the real one.
+            Append_To (Formals,
+              Make_Parameter_Specification (Loc,
+                Defining_Identifier    =>
+                  Make_Defining_Identifier (Sloc (Formal), Chars (Formal)),
+                In_Present             => In_Present  (Spec),
+                Out_Present            => Out_Present (Spec),
+                Null_Exclusion_Present => Null_Exclusion_Present (Spec),
+                Parameter_Type         =>
+                  New_Copy_Tree (Parameter_Type (Spec)),
+                Expression             => New_Copy_Tree (Expression (Spec))));
+
+            Next_Formal (Formal);
+         end loop;
+      end Copy_Formals;
 
-         Set_Parameter_Specifications
-           (Specification (Body_To_Inline), No_List);
+      ------------------------
+      -- Copy_Return_Object --
+      ------------------------
 
-         --  A new internal name is associated with Body_To_Inline to avoid
-         --  conflicts when the non-inlined body N is analyzed.
+      function Copy_Return_Object (Obj_Decl : Node_Id) return Node_Id is
+         Obj_Id  : constant Entity_Id := Defining_Entity (Obj_Decl);
 
-         Set_Defining_Unit_Name (Specification (Body_To_Inline),
-            Make_Defining_Identifier (Sloc (N), New_Internal_Name ('P')));
-         Set_Corresponding_Spec (Body_To_Inline, Empty);
-      end Generate_Subprogram_Body;
+      begin
+         --  The use of New_Copy_Tree ensures that global references are
+         --  preserved in case of generics.
+
+         return
+           Make_Object_Declaration (Sloc (Obj_Decl),
+             Defining_Identifier    =>
+               Make_Defining_Identifier (Sloc (Obj_Id), Chars (Obj_Id)),
+             Aliased_Present        => Aliased_Present  (Obj_Decl),
+             Constant_Present       => Constant_Present (Obj_Decl),
+             Null_Exclusion_Present => Null_Exclusion_Present (Obj_Decl),
+             Object_Definition      =>
+               New_Copy_Tree (Object_Definition (Obj_Decl)),
+             Expression             => New_Copy_Tree (Expression (Obj_Decl)));
+      end Copy_Return_Object;
 
       ----------------------------------
       -- Split_Unconstrained_Function --
@@ -1674,10 +2246,10 @@ package body Inline is
          Spec_Id  : Entity_Id)
       is
          Loc      : constant Source_Ptr := Sloc (N);
-         Ret_Node : constant Node_Id :=
+         Ret_Stmt : constant Node_Id :=
                       First (Statements (Handled_Statement_Sequence (N)));
          Ret_Obj  : constant Node_Id :=
-                      First (Return_Object_Declarations (Ret_Node));
+                      First (Return_Object_Declarations (Ret_Stmt));
 
          procedure Build_Procedure
            (Proc_Id   : out Entity_Id;
@@ -1693,58 +2265,35 @@ package body Inline is
            (Proc_Id   : out Entity_Id;
             Decl_List : out List_Id)
          is
-            Formal         : Entity_Id;
-            Formal_List    : constant List_Id := New_List;
-            Proc_Spec      : Node_Id;
-            Proc_Body      : Node_Id;
-            Subp_Name      : constant Name_Id := New_Internal_Name ('F');
-            Body_Decl_List : List_Id := No_List;
-            Param_Type     : Node_Id;
+            Formals   : constant List_Id   := New_List;
+            Subp_Name : constant Name_Id   := New_Internal_Name ('F');
 
-         begin
-            if Nkind (Object_Definition (Ret_Obj)) = N_Identifier then
-               Param_Type :=
-                 New_Copy (Object_Definition (Ret_Obj));
-            else
-               Param_Type :=
-                 New_Copy (Subtype_Mark (Object_Definition (Ret_Obj)));
-            end if;
+            Body_Decls : List_Id := No_List;
+            Decl       : Node_Id;
+            Proc_Body  : Node_Id;
+            Proc_Spec  : Node_Id;
 
-            Append_To (Formal_List,
-              Make_Parameter_Specification (Loc,
-                Defining_Identifier    =>
-                  Make_Defining_Identifier (Loc,
-                    Chars => Chars (Defining_Identifier (Ret_Obj))),
-                In_Present             => False,
-                Out_Present            => True,
-                Null_Exclusion_Present => False,
-                Parameter_Type         => Param_Type));
+         begin
+            --  Create formal parameters for the return object and all formals
+            --  of the unconstrained function in order to pass their values to
+            --  the procedure.
 
-            Formal := First_Formal (Spec_Id);
-            while Present (Formal) loop
-               Append_To (Formal_List,
-                 Make_Parameter_Specification (Loc,
-                   Defining_Identifier    =>
-                     Make_Defining_Identifier (Sloc (Formal),
-                       Chars => Chars (Formal)),
-                   In_Present             => In_Present (Parent (Formal)),
-                   Out_Present            => Out_Present (Parent (Formal)),
-                   Null_Exclusion_Present =>
-                     Null_Exclusion_Present (Parent (Formal)),
-                   Parameter_Type         =>
-                     New_Occurrence_Of (Etype (Formal), Loc),
-                   Expression             =>
-                     Copy_Separate_Tree (Expression (Parent (Formal)))));
+            Build_Return_Object_Formal
+              (Loc      => Loc,
+               Obj_Decl => Ret_Obj,
+               Formals  => Formals);
 
-               Next_Formal (Formal);
-            end loop;
+            Copy_Formals
+              (Loc     => Loc,
+               Subp_Id => Spec_Id,
+               Formals => Formals);
 
             Proc_Id := Make_Defining_Identifier (Loc, Chars => Subp_Name);
 
             Proc_Spec :=
               Make_Procedure_Specification (Loc,
                 Defining_Unit_Name       => Proc_Id,
-                Parameter_Specifications => Formal_List);
+                Parameter_Specifications => Formals);
 
             Decl_List := New_List;
 
@@ -1756,37 +2305,30 @@ package body Inline is
             --  Copy these declarations to the built procedure.
 
             if Present (Declarations (N)) then
-               Body_Decl_List := New_List;
+               Body_Decls := New_List;
 
-               declare
-                  D     : Node_Id;
-                  New_D : Node_Id;
+               Decl := First (Declarations (N));
+               while Present (Decl) loop
+                  pragma Assert (Nkind (Decl) = N_Implicit_Label_Declaration);
 
-               begin
-                  D := First (Declarations (N));
-                  while Present (D) loop
-                     pragma Assert (Nkind (D) = N_Implicit_Label_Declaration);
-
-                     New_D :=
-                       Make_Implicit_Label_Declaration (Loc,
-                         Make_Defining_Identifier (Loc,
-                           Chars => Chars (Defining_Identifier (D))),
-                         Label_Construct => Empty);
-                     Append_To (Body_Decl_List, New_D);
-
-                     Next (D);
-                  end loop;
-               end;
+                  Append_To (Body_Decls,
+                    Make_Implicit_Label_Declaration (Loc,
+                      Make_Defining_Identifier (Loc,
+                        Chars => Chars (Defining_Identifier (Decl))),
+                      Label_Construct => Empty));
+
+                  Next (Decl);
+               end loop;
             end if;
 
-            pragma Assert (Present (Handled_Statement_Sequence (Ret_Node)));
+            pragma Assert (Present (Handled_Statement_Sequence (Ret_Stmt)));
 
             Proc_Body :=
               Make_Subprogram_Body (Loc,
-                Specification => Copy_Separate_Tree (Proc_Spec),
-                Declarations  => Body_Decl_List,
+                Specification              => Copy_Subprogram_Spec (Proc_Spec),
+                Declarations               => Body_Decls,
                 Handled_Statement_Sequence =>
-                  Copy_Separate_Tree (Handled_Statement_Sequence (Ret_Node)));
+                  New_Copy_Tree (Handled_Statement_Sequence (Ret_Stmt)));
 
             Set_Defining_Unit_Name (Specification (Proc_Body),
                Make_Defining_Identifier (Loc, Subp_Name));
@@ -1796,10 +2338,10 @@ package body Inline is
 
          --  Local variables
 
-         New_Obj   : constant Node_Id := Copy_Separate_Tree (Ret_Obj);
+         New_Obj   : constant Node_Id := Copy_Return_Object (Ret_Obj);
          Blk_Stmt  : Node_Id;
-         Proc_Id   : Entity_Id;
          Proc_Call : Node_Id;
+         Proc_Id   : Entity_Id;
 
       --  Start of processing for Split_Unconstrained_Function
 
@@ -1814,6 +2356,7 @@ package body Inline is
             Pop_Scope;
             Build_Procedure (Proc_Id, Decl_List);
             Insert_Actions (N, Decl_List);
+            Set_Is_Inlined (Proc_Id);
             Push_Scope (Scope);
          end;
 
@@ -1843,14 +2386,14 @@ package body Inline is
                 Parameter_Associations => Actual_List);
          end;
 
-         --  Generate
+         --  Generate:
 
          --    declare
          --       New_Obj : ...
          --    begin
-         --       main_1__F1b (New_Obj, ...);
-         --       return Obj;
-         --    end B10b;
+         --       Proc (New_Obj, ...);
+         --       return New_Obj;
+         --    end;
 
          Blk_Stmt :=
            Make_Block_Statement (Loc,
@@ -1866,7 +2409,7 @@ package body Inline is
                        New_Occurrence_Of
                          (Defining_Identifier (New_Obj), Loc)))));
 
-         Rewrite (Ret_Node, Blk_Stmt);
+         Rewrite (Ret_Stmt, Blk_Stmt);
       end Split_Unconstrained_Function;
 
       --  Local variables
@@ -1894,44 +2437,6 @@ package body Inline is
          return;
       end if;
 
-      --  Do not inline any subprogram that contains nested subprograms,
-      --  since the backend inlining circuit seems to generate uninitialized
-      --  references in this case. We know this happens in the case of front
-      --  end ZCX support, but it also appears it can happen in other cases
-      --  as well. The backend often rejects attempts to inline in the case
-      --  of nested procedures anyway, so little if anything is lost by this.
-      --  Note that this is test is for the benefit of the back-end. There
-      --  is a separate test for front-end inlining that also rejects nested
-      --  subprograms.
-
-      --  Do not do this test if errors have been detected, because in some
-      --  error cases, this code blows up, and we don't need it anyway if
-      --  there have been errors, since we won't get to the linker anyway.
-
-      declare
-         P_Ent : Node_Id;
-
-      begin
-         P_Ent := Body_Id;
-         loop
-            P_Ent := Scope (P_Ent);
-            exit when No (P_Ent) or else P_Ent = Standard_Standard;
-
-            if Is_Subprogram (P_Ent) then
-               Set_Is_Inlined (P_Ent, False);
-
-               if Comes_From_Source (P_Ent)
-                 and then (Has_Pragma_Inline (P_Ent))
-               then
-                  Cannot_Inline
-                    ("cannot inline& (nested subprogram)?", N, P_Ent,
-                     Is_Serious => True);
-                  return;
-               end if;
-            end if;
-         end loop;
-      end;
-
       --  No action needed in stubs since the attribute Body_To_Inline
       --  is not available
 
@@ -1945,6 +2450,18 @@ package body Inline is
       elsif Present (Body_To_Inline (Decl)) then
          return;
 
+      --  Do not generate a body to inline for protected functions, because the
+      --  transformation generates a call to a protected procedure, causing
+      --  spurious errors. We don't inline protected operations anyway, so
+      --  this is no loss. We might as well ignore intrinsics and foreign
+      --  conventions as well -- just allow Ada conventions.
+
+      elsif not (Convention (Spec_Id) = Convention_Ada
+        or else Convention (Spec_Id) = Convention_Ada_Pass_By_Copy
+        or else Convention (Spec_Id) = Convention_Ada_Pass_By_Reference)
+      then
+         return;
+
       --  Check excluded declarations
 
       elsif Present (Declarations (N))
@@ -2150,54 +2667,73 @@ package body Inline is
      Subp      : Entity_Id;
      Orig_Subp : Entity_Id)
    is
+      Decls     : constant List_Id    := New_List;
+      Is_Predef : constant Boolean    :=
+                    Is_Predefined_Unit (Get_Source_Unit (Subp));
       Loc       : constant Source_Ptr := Sloc (N);
-      Is_Predef : constant Boolean :=
-                    Is_Predefined_File_Name
-                      (Unit_File_Name (Get_Source_Unit (Subp)));
-      Orig_Bod  : constant Node_Id :=
+      Orig_Bod  : constant Node_Id    :=
                     Body_To_Inline (Unit_Declaration_Node (Subp));
 
+      Uses_Back_End : constant Boolean :=
+                        Back_End_Inlining and then Optimization_Level > 0;
+      --  The back-end expansion is used if the target supports back-end
+      --  inlining and some level of optimixation is required; otherwise
+      --  the inlining takes place fully as a tree expansion.
+
       Blk      : Node_Id;
       Decl     : Node_Id;
-      Decls    : constant List_Id := New_List;
-      Exit_Lab : Entity_Id        := Empty;
+      Exit_Lab : Entity_Id := Empty;
       F        : Entity_Id;
       A        : Node_Id;
-      Lab_Decl : Node_Id;
+      Lab_Decl : Node_Id   := Empty;
       Lab_Id   : Node_Id;
       New_A    : Node_Id;
-      Num_Ret  : Int := 0;
+      Num_Ret  : Nat       := 0;
       Ret_Type : Entity_Id;
-
-      Targ : Node_Id;
-      --  The target of the call. If context is an assignment statement then
-      --  this is the left-hand side of the assignment, else it is a temporary
-      --  to which the return value is assigned prior to rewriting the call.
-
-      Targ1 : Node_Id;
-      --  A separate target used when the return type is unconstrained
-
       Temp     : Entity_Id;
       Temp_Typ : Entity_Id;
 
-      Return_Object : Entity_Id := Empty;
-      --  Entity in declaration in an extended_return_statement
-
       Is_Unc      : Boolean;
       Is_Unc_Decl : Boolean;
       --  If the type returned by the function is unconstrained and the call
       --  can be inlined, special processing is required.
 
+      Return_Object : Entity_Id := Empty;
+      --  Entity in declaration in an extended_return_statement
+
+      Targ : Node_Id := Empty;
+      --  The target of the call. If context is an assignment statement then
+      --  this is the left-hand side of the assignment, else it is a temporary
+      --  to which the return value is assigned prior to rewriting the call.
+
+      Targ1 : Node_Id := Empty;
+      --  A separate target used when the return type is unconstrained
+
+      procedure Declare_Postconditions_Result;
+      --  When generating C code, declare _Result, which may be used in the
+      --  inlined _Postconditions procedure to verify the return value.
+
       procedure Make_Exit_Label;
       --  Build declaration for exit label to be used in Return statements,
       --  sets Exit_Lab (the label node) and Lab_Decl (corresponding implicit
       --  declaration). Does nothing if Exit_Lab already set.
 
+      procedure Make_Loop_Labels_Unique (HSS : Node_Id);
+      --  When compiling for CCG and performing front-end inlining, replace
+      --  loop names and references to them so that they do not conflict with
+      --  homographs in the current subprogram.
+
       function Process_Formals (N : Node_Id) return Traverse_Result;
       --  Replace occurrence of a formal with the corresponding actual, or the
       --  thunk generated for it. Replace a return statement with an assignment
       --  to the target of the call, with appropriate conversions if needed.
 
+      function Process_Formals_In_Aspects (N : Node_Id) return Traverse_Result;
+      --  Because aspects are linked indirectly to the rest of the tree,
+      --  replacement of formals appearing in aspect specifications must
+      --  be performed in a separate pass, using an instantiation of the
+      --  previous subprogram over aspect specifications reachable from N.
+
       function Process_Sloc (Nod : Node_Id) return Traverse_Result;
       --  If the call being expanded is that of an internal subprogram, set the
       --  sloc of the generated block to that of the call itself, so that the
@@ -2221,8 +2757,47 @@ package body Inline is
       --  If procedure body has no local variables, inline body without
       --  creating block, otherwise rewrite call with block.
 
-      function Formal_Is_Used_Once (Formal : Entity_Id) return Boolean;
-      --  Determine whether a formal parameter is used only once in Orig_Bod
+      function Formal_Is_Used_Once (Formal : Entity_Id) return Boolean;
+      --  Determine whether a formal parameter is used only once in Orig_Bod
+
+      -----------------------------------
+      -- Declare_Postconditions_Result --
+      -----------------------------------
+
+      procedure Declare_Postconditions_Result is
+         Enclosing_Subp : constant Entity_Id := Scope (Subp);
+
+      begin
+         pragma Assert
+           (Modify_Tree_For_C
+             and then Is_Subprogram (Enclosing_Subp)
+             and then Present (Postconditions_Proc (Enclosing_Subp)));
+
+         if Ekind (Enclosing_Subp) = E_Function then
+            if Nkind (First (Parameter_Associations (N))) in
+                 N_Numeric_Or_String_Literal
+            then
+               Append_To (Declarations (Blk),
+                 Make_Object_Declaration (Loc,
+                   Defining_Identifier =>
+                     Make_Defining_Identifier (Loc, Name_uResult),
+                   Constant_Present    => True,
+                   Object_Definition   =>
+                     New_Occurrence_Of (Etype (Enclosing_Subp), Loc),
+                   Expression          =>
+                     New_Copy_Tree (First (Parameter_Associations (N)))));
+            else
+               Append_To (Declarations (Blk),
+                 Make_Object_Renaming_Declaration (Loc,
+                   Defining_Identifier =>
+                     Make_Defining_Identifier (Loc, Name_uResult),
+                   Subtype_Mark        =>
+                     New_Occurrence_Of (Etype (Enclosing_Subp), Loc),
+                   Name                =>
+                     New_Copy_Tree (First (Parameter_Associations (N)))));
+            end if;
+         end if;
+      end Declare_Postconditions_Result;
 
       ---------------------
       -- Make_Exit_Label --
@@ -2242,6 +2817,61 @@ package body Inline is
          end if;
       end Make_Exit_Label;
 
+      -----------------------------
+      -- Make_Loop_Labels_Unique --
+      -----------------------------
+
+      procedure Make_Loop_Labels_Unique (HSS : Node_Id) is
+         function Process_Loop (N : Node_Id) return Traverse_Result;
+
+         ------------------
+         -- Process_Loop --
+         ------------------
+
+         function Process_Loop (N : Node_Id) return Traverse_Result is
+            Id  : Entity_Id;
+
+         begin
+            if Nkind (N) = N_Loop_Statement
+              and then Present (Identifier (N))
+            then
+               --  Create new external name for loop and update the
+               --  corresponding entity.
+
+               Id := Entity (Identifier (N));
+               Set_Chars (Id, New_External_Name (Chars (Id), 'L', -1));
+               Set_Chars (Identifier (N), Chars (Id));
+
+            elsif Nkind (N) = N_Exit_Statement
+              and then Present (Name (N))
+            then
+               --  The exit statement must name an enclosing loop, whose name
+               --  has already been updated.
+
+               Set_Chars (Name (N), Chars (Entity (Name (N))));
+            end if;
+
+            return OK;
+         end Process_Loop;
+
+         procedure Update_Loop_Names is new Traverse_Proc (Process_Loop);
+
+         --  Local variables
+
+         Stmt : Node_Id;
+
+      --  Start of processing for Make_Loop_Labels_Unique
+
+      begin
+         if Modify_Tree_For_C then
+            Stmt := First (Statements (HSS));
+            while Present (Stmt) loop
+               Update_Loop_Names (Stmt);
+               Next (Stmt);
+            end loop;
+         end if;
+      end Make_Loop_Labels_Unique;
+
       ---------------------
       -- Process_Formals --
       ---------------------
@@ -2266,11 +2896,11 @@ package body Inline is
                --  analyzed with the full view).
 
                if Is_Entity_Name (A) then
-                  Rewrite (N, New_Occurrence_Of (Entity (A), Loc));
+                  Rewrite (N, New_Occurrence_Of (Entity (A), Sloc (N)));
                   Check_Private_View (N);
 
                elsif Nkind (A) = N_Defining_Identifier then
-                  Rewrite (N, New_Occurrence_Of (A, Loc));
+                  Rewrite (N, New_Occurrence_Of (A, Sloc (N)));
                   Check_Private_View (N);
 
                --  Numeric literal
@@ -2301,6 +2931,7 @@ package body Inline is
 
          elsif Nkind (N) = N_Simple_Return_Statement then
             if No (Expression (N)) then
+               Num_Ret := Num_Ret + 1;
                Make_Exit_Label;
                Rewrite (N,
                  Make_Goto_Statement (Loc, Name => New_Copy (Lab_Id)));
@@ -2320,27 +2951,42 @@ package body Inline is
                end if;
 
                --  Because of the presence of private types, the views of the
-               --  expression and the context may be different, so place an
-               --  unchecked conversion to the context type to avoid spurious
+               --  expression and the context may be different, so place
+               --  a type conversion to the context type to avoid spurious
                --  errors, e.g. when the expression is a numeric literal and
                --  the context is private. If the expression is an aggregate,
                --  use a qualified expression, because an aggregate is not a
-               --  legal argument of a conversion. Ditto for numeric literals,
-               --  which must be resolved to a specific type.
+               --  legal argument of a conversion. Ditto for numeric, character
+               --  and string literals, and attributes that yield a universal
+               --  type, because those must be resolved to a specific type.
 
                if Nkind_In (Expression (N), N_Aggregate,
+                                            N_Character_Literal,
                                             N_Null,
-                                            N_Real_Literal,
-                                            N_Integer_Literal)
+                                            N_String_Literal)
+                 or else Yields_Universal_Type (Expression (N))
                then
                   Ret :=
                     Make_Qualified_Expression (Sloc (N),
                       Subtype_Mark => New_Occurrence_Of (Ret_Type, Sloc (N)),
                       Expression   => Relocate_Node (Expression (N)));
-               else
+
+               --  Use an unchecked type conversion between access types, for
+               --  which a type conversion would not always be valid, as no
+               --  check may result from the conversion.
+
+               elsif Is_Access_Type (Ret_Type) then
                   Ret :=
                     Unchecked_Convert_To
                       (Ret_Type, Relocate_Node (Expression (N)));
+
+               --  Otherwise use a type conversion, which may trigger a check
+
+               else
+                  Ret :=
+                    Make_Type_Conversion (Sloc (N),
+                      Subtype_Mark => New_Occurrence_Of (Ret_Type, Sloc (N)),
+                      Expression   => Relocate_Node (Expression (N)));
                end if;
 
                if Nkind (Targ) = N_Defining_Identifier then
@@ -2428,6 +3074,30 @@ package body Inline is
 
       procedure Replace_Formals is new Traverse_Proc (Process_Formals);
 
+      --------------------------------
+      -- Process_Formals_In_Aspects --
+      --------------------------------
+
+      function Process_Formals_In_Aspects
+        (N : Node_Id) return Traverse_Result
+      is
+         A : Node_Id;
+
+      begin
+         if Has_Aspects (N) then
+            A := First (Aspect_Specifications (N));
+            while Present (A) loop
+               Replace_Formals (Expression (A));
+
+               Next (A);
+            end loop;
+         end if;
+         return OK;
+      end Process_Formals_In_Aspects;
+
+      procedure Replace_Formals_In_Aspects is
+        new Traverse_Proc (Process_Formals_In_Aspects);
+
       ------------------
       -- Process_Sloc --
       ------------------
@@ -2494,6 +3164,8 @@ package body Inline is
          Fst : constant Node_Id := First (Statements (HSS));
 
       begin
+         Make_Loop_Labels_Unique (HSS);
+
          --  Optimize simple case: function body is a single return statement,
          --  which has been expanded into an assignment.
 
@@ -2581,6 +3253,8 @@ package body Inline is
          HSS  : constant Node_Id := Handled_Statement_Sequence (Blk);
 
       begin
+         Make_Loop_Labels_Unique (HSS);
+
          --  If there is a transient scope for N, this will be the scope of the
          --  actions for N, and the statements in Blk need to be within this
          --  scope. For example, they need to have visibility on the constant
@@ -2663,7 +3337,7 @@ package body Inline is
    begin
       --  Initializations for old/new semantics
 
-      if not Back_End_Inlining then
+      if not Uses_Back_End then
          Is_Unc      := Is_Array_Type (Etype (Subp))
                           and then not Is_Constrained (Etype (Subp));
          Is_Unc_Decl := False;
@@ -2680,36 +3354,17 @@ 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
-      --  Body_To_Inline is also set for renamings (see sinfo.ads)
+      --  Body_To_Inline is also set for renamings (see sinfo.ads). For a
+      --  true inlining, Orig_Bod has code rather than being an entity.
 
       elsif Nkind (Orig_Bod) in N_Entity then
          return;
-
-      --  Skip inlining if the function returns an unconstrained type using
-      --  an extended return statement since this part of the new inlining
-      --  model which is not yet supported by the current implementation. ???
-
-      elsif Is_Unc
-        and then
-          Nkind (First (Statements (Handled_Statement_Sequence (Orig_Bod))))
-            = N_Extended_Return_Statement
-        and then not Back_End_Inlining
-      then
-         return;
       end if;
 
       if Nkind (Orig_Bod) = N_Defining_Identifier
@@ -2744,7 +3399,7 @@ package body Inline is
 
       --  Old semantics
 
-      if not Back_End_Inlining then
+      if not Uses_Back_End then
          declare
             Bod : Node_Id;
 
@@ -2760,6 +3415,16 @@ package body Inline is
                Set_Declarations (Blk, New_List);
             end if;
 
+            --  When generating C code, declare _Result, which may be used to
+            --  verify the return value.
+
+            if Modify_Tree_For_C
+              and then Nkind (N) = N_Procedure_Call_Statement
+              and then Chars (Name (N)) = Name_uPostconditions
+            then
+               Declare_Postconditions_Result;
+            end if;
+
             --  For the unconstrained case, capture the name of the local
             --  variable that holds the result. This must be the first
             --  declaration in the block, because its bounds cannot depend
@@ -2778,6 +3443,20 @@ package body Inline is
                begin
                   First_Decl := First (Declarations (Blk));
 
+                  --  If the body is a single extended return statement,the
+                  --  resulting block is a nested block.
+
+                  if No (First_Decl) then
+                     First_Decl :=
+                       First (Statements (Handled_Statement_Sequence (Blk)));
+
+                     if Nkind (First_Decl) = N_Block_Statement then
+                        First_Decl := First (Declarations (First_Decl));
+                     end if;
+                  end if;
+
+                  --  No front-end inlining possible
+
                   if Nkind (First_Decl) /= N_Object_Declaration then
                      return;
                   end if;
@@ -2813,8 +3492,8 @@ package body Inline is
             --  The semantic analyzer checked that frontend-inlined functions
             --  returning unconstrained types have no declarations and have
             --  a single extended return statement. As part of its processing
-            --  the function was split in two subprograms: a procedure P and
-            --  a function F that has a block with a call to procedure P (see
+            --  the function was split into two subprograms: a procedure P' and
+            --  a function F' that has a block with a call to procedure P' (see
             --  Split_Unconstrained_Function).
 
             else
@@ -2926,8 +3605,10 @@ package body Inline is
 
          elsif Base_Type (Etype (F)) = Base_Type (Etype (A))
            and then Etype (F) /= Base_Type (Etype (F))
+           and then Is_Constrained (Etype (F))
          then
             Temp_Typ := Etype (F);
+
          else
             Temp_Typ := Etype (A);
          end if;
@@ -2937,19 +3618,26 @@ package body Inline is
 
          --  If the actual is a literal and the formal has its address taken,
          --  we cannot pass the literal itself as an argument, so its value
-         --  must be captured in a temporary.
+         --  must be captured in a temporary. Skip this optimization in
+         --  GNATprove mode, to make sure any check on a type conversion
+         --  will be issued.
 
          if (Is_Entity_Name (A)
               and then
-               (not Is_Scalar_Type (Etype (A))
-                 or else Ekind (Entity (A)) = E_Enumeration_Literal))
+                (not Is_Scalar_Type (Etype (A))
+                  or else Ekind (Entity (A)) = E_Enumeration_Literal)
+              and then not GNATprove_Mode)
 
          --  When the actual is an identifier and the corresponding formal is
          --  used only once in the original body, the formal can be substituted
-         --  directly with the actual parameter.
+         --  directly with the actual parameter. Skip this optimization in
+         --  GNATprove mode, to make sure any check on a type conversion
+         --  will be issued.
 
-           or else (Nkind (A) = N_Identifier
-             and then Formal_Is_Used_Once (F))
+           or else
+             (Nkind (A) = N_Identifier
+               and then Formal_Is_Used_Once (F)
+               and then not GNATprove_Mode)
 
            or else
              (Nkind_In (A, N_Real_Literal,
@@ -2982,8 +3670,17 @@ package body Inline is
                    Subtype_Mark => New_Occurrence_Of (Etype (F), Loc),
                    Expression   => Relocate_Node (Expression (A)));
 
-            elsif Etype (F) /= Etype (A) then
-               New_A := Unchecked_Convert_To (Etype (F), Relocate_Node (A));
+            --  In GNATprove mode, keep the most precise type of the actual for
+            --  the temporary variable, when the formal type is unconstrained.
+            --  Otherwise, the AST may contain unexpected assignment statements
+            --  to a temporary variable of unconstrained type renaming a local
+            --  variable of constrained type, which is not expected by
+            --  GNATprove.
+
+            elsif Etype (F) /= Etype (A)
+              and then (not GNATprove_Mode or else Is_Constrained (Etype (F)))
+            then
+               New_A    := Unchecked_Convert_To (Etype (F), Relocate_Node (A));
                Temp_Typ := Etype (F);
 
             else
@@ -3019,7 +3716,29 @@ package body Inline is
                    Constant_Present    => True,
                    Object_Definition   => New_Occurrence_Of (Temp_Typ, Loc),
                    Expression          => New_A);
+
             else
+               --  In GNATprove mode, make an explicit copy of input
+               --  parameters when formal and actual types differ, to make
+               --  sure any check on the type conversion will be issued.
+               --  The legality of the copy is ensured by calling first
+               --  Call_Can_Be_Inlined_In_GNATprove_Mode.
+
+               if GNATprove_Mode
+                 and then Ekind (F) /= E_Out_Parameter
+                 and then not Same_Type (Etype (F), Etype (A))
+               then
+                  pragma Assert (not Is_By_Reference_Type (Etype (A)));
+                  pragma Assert (not Is_Limited_Type (Etype (A)));
+
+                  Append_To (Decls,
+                    Make_Object_Declaration (Loc,
+                      Defining_Identifier => Make_Temporary (Loc, 'C'),
+                      Constant_Present    => True,
+                      Object_Definition   => New_Occurrence_Of (Temp_Typ, Loc),
+                      Expression          => New_Copy_Tree (New_A)));
+               end if;
+
                Decl :=
                  Make_Object_Renaming_Declaration (Loc,
                    Defining_Identifier => Temp,
@@ -3068,7 +3787,7 @@ package body Inline is
          --  of the result of a call to an inlined function that returns
          --  an unconstrained type
 
-         elsif Back_End_Inlining
+         elsif Uses_Back_End
            and then Nkind (Parent (N)) = N_Object_Declaration
            and then Is_Unc
          then
@@ -3120,7 +3839,7 @@ package body Inline is
          --  avoid generating undesired extra calls and goto statements.
 
          --     Given:
-         --                 function Func (...) return ...
+         --                 function Func (...) return String is
          --                 begin
          --                    declare
          --                       Result : String (1 .. 4);
@@ -3128,7 +3847,7 @@ package body Inline is
          --                       Proc (Result, ...);
          --                       return Result;
          --                    end;
-         --                 end F;
+         --                 end Func;
 
          --                 Result : String := Func (...);
 
@@ -3191,6 +3910,7 @@ package body Inline is
       --  Attach block to tree before analysis and rewriting.
 
       Replace_Formals (Blk);
+      Replace_Formals_In_Aspects (Blk);
       Set_Parent (Blk, N);
 
       if GNATprove_Mode then
@@ -3208,8 +3928,9 @@ package body Inline is
 
       elsif Present (Exit_Lab) then
 
-         --  If the body was a single expression, the single return statement
-         --  and the corresponding label are useless.
+         --  If there's a single return statement at the end of the subprogram,
+         --  the corresponding goto statement and the corresponding label are
+         --  useless.
 
          if Num_Ret = 1
            and then
@@ -3347,8 +4068,7 @@ package body Inline is
          end if;
 
          return Present (Conv)
-           and then Is_Predefined_File_Name
-                      (Unit_File_Name (Get_Source_Unit (Conv)))
+           and then Is_Predefined_Unit (Get_Source_Unit (Conv))
            and then Is_Intrinsic_Subprogram (Conv);
       end Is_Unchecked_Conversion;
 
@@ -3363,18 +4083,30 @@ package body Inline is
 
       D := First (Decls);
       while Present (D) loop
-         if Nkind (D) = N_Subprogram_Body then
+
+         --  First declarations universally excluded
+
+         if Nkind (D) = N_Package_Declaration then
             Cannot_Inline
-              ("cannot inline & (nested subprogram)?",
-               D, Subp);
+              ("cannot inline & (nested package declaration)?", D, Subp);
+            return True;
+
+         elsif Nkind (D) = N_Package_Instantiation then
+            Cannot_Inline
+              ("cannot inline & (nested package instantiation)?", D, Subp);
             return True;
+         end if;
+
+         --  Then declarations excluded only for front-end inlining
+
+         if Back_End_Inlining then
+            null;
 
          elsif Nkind (D) = N_Task_Type_Declaration
            or else Nkind (D) = N_Single_Task_Declaration
          then
             Cannot_Inline
-              ("cannot inline & (nested task type declaration)?",
-               D, Subp);
+              ("cannot inline & (nested task type declaration)?", D, Subp);
             return True;
 
          elsif Nkind (D) = N_Protected_Type_Declaration
@@ -3385,31 +4117,52 @@ package body Inline is
                D, Subp);
             return True;
 
-         elsif Nkind (D) = N_Package_Declaration then
+         elsif Nkind (D) = N_Subprogram_Body then
             Cannot_Inline
-              ("cannot inline & (nested package declaration)?",
-               D, Subp);
+              ("cannot inline & (nested subprogram)?", D, Subp);
             return True;
 
          elsif Nkind (D) = N_Function_Instantiation
            and then not Is_Unchecked_Conversion (D)
          then
             Cannot_Inline
-              ("cannot inline & (nested function instantiation)?",
-               D, Subp);
+              ("cannot inline & (nested function instantiation)?", D, Subp);
             return True;
 
          elsif Nkind (D) = N_Procedure_Instantiation then
             Cannot_Inline
-              ("cannot inline & (nested procedure instantiation)?",
-               D, Subp);
+              ("cannot inline & (nested procedure instantiation)?", D, Subp);
             return True;
 
-         elsif Nkind (D) = N_Package_Instantiation then
-            Cannot_Inline
-              ("cannot inline & (nested package instantiation)?",
-               D, Subp);
-            return True;
+         --  Subtype declarations with predicates will generate predicate
+         --  functions, i.e. nested subprogram bodies, so inlining is not
+         --  possible.
+
+         elsif Nkind (D) = N_Subtype_Declaration
+           and then Present (Aspect_Specifications (D))
+         then
+            declare
+               A    : Node_Id;
+               A_Id : Aspect_Id;
+
+            begin
+               A := First (Aspect_Specifications (D));
+               while Present (A) loop
+                  A_Id := Get_Aspect_Id (Chars (Identifier (A)));
+
+                  if A_Id = Aspect_Predicate
+                    or else A_Id = Aspect_Static_Predicate
+                    or else A_Id = Aspect_Dynamic_Predicate
+                  then
+                     Cannot_Inline
+                       ("cannot inline & (subtype declaration with "
+                        & "predicate)?", D, Subp);
+                     return True;
+                  end if;
+
+                  Next (A);
+               end loop;
+            end;
          end if;
 
          Next (D);
@@ -3546,7 +4299,7 @@ package body Inline is
    --------------------------
 
    function Has_Initialized_Type (E : Entity_Id) return Boolean is
-      E_Body : constant Node_Id := Get_Subprogram_Body (E);
+      E_Body : constant Node_Id := Subprogram_Body (E);
       Decl   : Node_Id;
 
    begin
@@ -3588,25 +4341,31 @@ package body Inline is
             if Present (Expression (N))
               and then Is_Entity_Name (Expression (N))
             then
+               pragma Assert (Present (Entity (Expression (N))));
+
                if No (Return_Statement) then
                   Return_Statement := N;
                   return OK;
 
-               elsif Chars (Expression (N)) =
-                     Chars (Expression (Return_Statement))
-               then
-                  return OK;
-
                else
-                  return Abandon;
+                  pragma Assert
+                    (Present (Entity (Expression (Return_Statement))));
+
+                  if Entity (Expression (N)) =
+                       Entity (Expression (Return_Statement))
+                  then
+                     return OK;
+                  else
+                     return Abandon;
+                  end if;
                end if;
 
-            --  A return statement within an extended return is a noop
-            --  after inlining.
+            --  A return statement within an extended return is a noop after
+            --  inlining.
 
             elsif No (Expression (N))
-              and then
-                Nkind (Parent (Parent (N))) = N_Extended_Return_Statement
+              and then Nkind (Parent (Parent (N))) =
+                         N_Extended_Return_Statement
             then
                return OK;
 
@@ -3645,10 +4404,11 @@ package body Inline is
          return True;
 
       else
-         return Present (Declarations (N))
-           and then Present (First (Declarations (N)))
-           and then Chars (Expression (Return_Statement)) =
-                    Chars (Defining_Identifier (First (Declarations (N))));
+         return
+           Present (Declarations (N))
+             and then Present (First (Declarations (N)))
+             and then Entity (Expression (Return_Statement)) =
+                        Defining_Identifier (First (Declarations (N)));
       end if;
    end Has_Single_Return;
 
@@ -3680,7 +4440,6 @@ package body Inline is
 
    procedure Initialize is
    begin
-      Pending_Descriptor.Init;
       Pending_Instantiations.Init;
       Inlined_Bodies.Init;
       Successors.Init;
@@ -3692,6 +4451,7 @@ package body Inline is
 
       Inlined_Calls := No_Elist;
       Backend_Calls := No_Elist;
+      Backend_Instances := No_Elist;
       Backend_Inlined_Subps := No_Elist;
       Backend_Not_Inlined_Subps := No_Elist;
    end Initialize;
@@ -3708,9 +4468,36 @@ package body Inline is
    --  the body is an internal error.
 
    procedure Instantiate_Bodies is
-      J    : Int;
+
+      procedure Instantiate_Body (Info : Pending_Body_Info);
+      --  Instantiate a pending body
+
+      ------------------------
+      --  Instantiate_Body  --
+      ------------------------
+
+      procedure Instantiate_Body (Info : Pending_Body_Info) is
+      begin
+         --  If the instantiation node is absent, it has been removed as part
+         --  of unreachable code.
+
+         if No (Info.Inst_Node) then
+            null;
+
+         elsif Nkind (Info.Act_Decl) = N_Package_Declaration then
+            Instantiate_Package_Body (Info);
+            Add_Scope_To_Clean (Defining_Entity (Info.Act_Decl));
+
+         else
+            Instantiate_Subprogram_Body (Info);
+         end if;
+      end Instantiate_Body;
+
+      J, K  : Nat;
       Info : Pending_Body_Info;
 
+   --  Start of processing for Instantiate_Bodies
+
    begin
       if Serious_Errors_Detected = 0 then
          Expander_Active := (Operating_Mode = Opt.Generate_Code);
@@ -3723,41 +4510,45 @@ package body Inline is
 
          --  A body instantiation may generate additional instantiations, so
          --  the following loop must scan to the end of a possibly expanding
-         --  set (that's why we can't simply use a FOR loop here).
+         --  set (that's why we cannot simply use a FOR loop here). We must
+         --  also capture the element lest the set be entirely reallocated.
 
          J := 0;
-         while J <= Pending_Instantiations.Last
-           and then Serious_Errors_Detected = 0
-         loop
-            Info := Pending_Instantiations.Table (J);
-
-            --  If the instantiation node is absent, it has been removed
-            --  as part of unreachable code.
-
-            if No (Info.Inst_Node) then
-               null;
+         if Back_End_Inlining then
+            while J <= Called_Pending_Instantiations.Last
+              and then Serious_Errors_Detected = 0
+            loop
+               K := Called_Pending_Instantiations.Table (J);
+               Info := Pending_Instantiations.Table (K);
+               Instantiate_Body (Info);
 
-            elsif Nkind (Info.Act_Decl) = N_Package_Declaration then
-               Instantiate_Package_Body (Info);
-               Add_Scope_To_Clean (Defining_Entity (Info.Act_Decl));
+               J := J + 1;
+            end loop;
 
-            else
-               Instantiate_Subprogram_Body (Info);
-            end if;
+         else
+            while J <= Pending_Instantiations.Last
+              and then Serious_Errors_Detected = 0
+            loop
+               Info := Pending_Instantiations.Table (J);
+               Instantiate_Body (Info);
 
-            J := J + 1;
-         end loop;
+               J := J + 1;
+            end loop;
+         end if;
 
          --  Reset the table of instantiations. Additional instantiations
          --  may be added through inlining, when additional bodies are
          --  analyzed.
 
-         Pending_Instantiations.Init;
+         if Back_End_Inlining then
+            Called_Pending_Instantiations.Init;
+         else
+            Pending_Instantiations.Init;
+         end if;
 
          --  We can now complete the cleanup actions of scopes that contain
          --  pending instantiations (skipped for generic units, since we
          --  never need any cleanups in generic units).
-         --  pending instantiations.
 
          if Expander_Active
            and then not Is_Generic_Unit (Main_Unit_Entity)
@@ -3781,7 +4572,7 @@ package body Inline is
    begin
       Scop := Scope (E);
       while Scop /= Standard_Standard loop
-         if Ekind (Scop) in Subprogram_Kind then
+         if Is_Subprogram (Scop) then
             return True;
 
          elsif Ekind (Scop) = E_Task_Type
@@ -3819,7 +4610,7 @@ package body Inline is
          while Present (Elmt) loop
             Nod := Node (Elmt);
 
-            if In_Extended_Main_Code_Unit (Nod) then
+            if not In_Internal_Unit (Nod) then
                Count := Count + 1;
 
                if Count = 1 then
@@ -3848,7 +4639,7 @@ package body Inline is
          while Present (Elmt) loop
             Nod := Node (Elmt);
 
-            if In_Extended_Main_Code_Unit (Nod) then
+            if not In_Internal_Unit (Nod) then
                Count := Count + 1;
 
                if Count = 1 then
@@ -3867,33 +4658,61 @@ package body Inline is
          end loop;
       end if;
 
+      --  Generate listing of instances inlined for the backend
+
+      if Present (Backend_Instances) then
+         Count := 0;
+
+         Elmt := First_Elmt (Backend_Instances);
+         while Present (Elmt) loop
+            Nod := Node (Elmt);
+
+            if not In_Internal_Unit (Nod) then
+               Count := Count + 1;
+
+               if Count = 1 then
+                  Write_Str ("List of instances inlined for the backend");
+                  Write_Eol;
+               end if;
+
+               Write_Str ("  ");
+               Write_Int (Count);
+               Write_Str (":");
+               Write_Location (Sloc (Nod));
+               Output.Write_Eol;
+            end if;
+
+            Next_Elmt (Elmt);
+         end loop;
+      end if;
+
       --  Generate listing of subprograms passed to the backend
 
-      if Present (Backend_Inlined_Subps)
-        and then Back_End_Inlining
-      then
+      if Present (Backend_Inlined_Subps) and then Back_End_Inlining then
          Count := 0;
 
          Elmt := First_Elmt (Backend_Inlined_Subps);
          while Present (Elmt) loop
             Nod := Node (Elmt);
 
-            Count := Count + 1;
+            if not In_Internal_Unit (Nod) then
+               Count := Count + 1;
 
-            if Count = 1 then
-               Write_Str
-                 ("List of inlined subprograms passed to the backend");
-               Write_Eol;
-            end if;
+               if Count = 1 then
+                  Write_Str
+                    ("List of inlined subprograms passed to the backend");
+                  Write_Eol;
+               end if;
 
-            Write_Str ("  ");
-            Write_Int (Count);
-            Write_Str (":");
-            Write_Name (Chars (Nod));
-            Write_Str (" (");
-            Write_Location (Sloc (Nod));
-            Write_Str (")");
-            Output.Write_Eol;
+               Write_Str ("  ");
+               Write_Int (Count);
+               Write_Str (":");
+               Write_Name (Chars (Nod));
+               Write_Str (" (");
+               Write_Location (Sloc (Nod));
+               Write_Str (")");
+               Output.Write_Eol;
+            end if;
 
             Next_Elmt (Elmt);
          end loop;
@@ -3901,31 +4720,31 @@ package body Inline is
 
       --  Generate listing of subprograms that cannot be inlined by the backend
 
-      if Present (Backend_Not_Inlined_Subps)
-        and then Back_End_Inlining
-      then
+      if Present (Backend_Not_Inlined_Subps) and then Back_End_Inlining then
          Count := 0;
 
          Elmt := First_Elmt (Backend_Not_Inlined_Subps);
          while Present (Elmt) loop
             Nod := Node (Elmt);
 
-            Count := Count + 1;
+            if not In_Internal_Unit (Nod) then
+               Count := Count + 1;
 
-            if Count = 1 then
-               Write_Str
-                 ("List of subprograms that cannot be inlined by the backend");
-               Write_Eol;
-            end if;
+               if Count = 1 then
+                  Write_Str
+                    ("List of subprograms that cannot be inlined by backend");
+                  Write_Eol;
+               end if;
 
-            Write_Str ("  ");
-            Write_Int (Count);
-            Write_Str (":");
-            Write_Name (Chars (Nod));
-            Write_Str (" (");
-            Write_Location (Sloc (Nod));
-            Write_Str (")");
-            Output.Write_Eol;
+               Write_Str ("  ");
+               Write_Int (Count);
+               Write_Str (":");
+               Write_Name (Chars (Nod));
+               Write_Str (" (");
+               Write_Location (Sloc (Nod));
+               Write_Str (")");
+               Output.Write_Eol;
+            end if;
 
             Next_Elmt (Elmt);
          end loop;
@@ -3938,24 +4757,80 @@ package body Inline is
 
    procedure Lock is
    begin
-      Pending_Instantiations.Locked := True;
-      Inlined_Bodies.Locked := True;
-      Successors.Locked := True;
-      Inlined.Locked := True;
       Pending_Instantiations.Release;
+      Pending_Instantiations.Locked := True;
       Inlined_Bodies.Release;
+      Inlined_Bodies.Locked := True;
       Successors.Release;
+      Successors.Locked := True;
       Inlined.Release;
+      Inlined.Locked := True;
    end Lock;
 
-   ---------------------------
-   -- Register_Backend_Call --
-   ---------------------------
+   --------------------------------
+   -- Remove_Aspects_And_Pragmas --
+   --------------------------------
+
+   procedure Remove_Aspects_And_Pragmas (Body_Decl : Node_Id) is
+      procedure Remove_Items (List : List_Id);
+      --  Remove all useless aspects/pragmas from a particular list
+
+      ------------------
+      -- Remove_Items --
+      ------------------
+
+      procedure Remove_Items (List : List_Id) is
+         Item      : Node_Id;
+         Item_Id   : Node_Id;
+         Next_Item : Node_Id;
+
+      begin
+         --  Traverse the list looking for an aspect specification or a pragma
+
+         Item := First (List);
+         while Present (Item) loop
+            Next_Item := Next (Item);
+
+            if Nkind (Item) = N_Aspect_Specification then
+               Item_Id := Identifier (Item);
+            elsif Nkind (Item) = N_Pragma then
+               Item_Id := Pragma_Identifier (Item);
+            else
+               Item_Id := Empty;
+            end if;
+
+            if Present (Item_Id)
+              and then Nam_In (Chars (Item_Id), Name_Contract_Cases,
+                                                Name_Global,
+                                                Name_Depends,
+                                                Name_Postcondition,
+                                                Name_Precondition,
+                                                Name_Refined_Global,
+                                                Name_Refined_Depends,
+                                                Name_Refined_Post,
+                                                Name_Test_Case,
+                                                Name_Unmodified,
+                                                Name_Unreferenced,
+                                                Name_Unused)
+            then
+               Remove (Item);
+            end if;
+
+            Item := Next_Item;
+         end loop;
+      end Remove_Items;
+
+   --  Start of processing for Remove_Aspects_And_Pragmas
 
-   procedure Register_Backend_Call (N : Node_Id) is
    begin
-      Append_New_Elmt (N, To => Backend_Calls);
-   end Register_Backend_Call;
+      Remove_Items (Aspect_Specifications (Body_Decl));
+      Remove_Items (Declarations          (Body_Decl));
+
+      --  Pragmas Unmodified, Unreferenced, and Unused may additionally appear
+      --  in the body of the subprogram.
+
+      Remove_Items (Statements (Handled_Statement_Sequence (Body_Decl)));
+   end Remove_Aspects_And_Pragmas;
 
    --------------------------
    -- Remove_Dead_Instance --
@@ -3976,31 +4851,4 @@ package body Inline is
       end loop;
    end Remove_Dead_Instance;
 
-   --------------------
-   -- Remove_Pragmas --
-   --------------------
-
-   procedure Remove_Pragmas (Bod : Node_Id) is
-      Decl : Node_Id;
-      Nxt  : Node_Id;
-
-   begin
-      Decl := First (Declarations (Bod));
-      while Present (Decl) loop
-         Nxt := Next (Decl);
-
-         if Nkind (Decl) = N_Pragma
-           and then Nam_In (Pragma_Name (Decl), Name_Contract_Cases,
-                                                Name_Precondition,
-                                                Name_Postcondition,
-                                                Name_Unreferenced,
-                                                Name_Unmodified)
-         then
-            Remove (Decl);
-         end if;
-
-         Decl := Nxt;
-      end loop;
-   end Remove_Pragmas;
-
 end Inline;