[Ada] Allow inlining for proof inside generics

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -850,9 +850,12 @@  package body Exp_SPARK is
    --  Start of processing for Expand_SPARK_Potential_Renaming
 
    begin
-      --  Replace a reference to a renaming with the actual renamed object
+      --  Replace a reference to a renaming with the actual renamed object.
+      --  Protect against previous errors leaving no entity in N.
 
-      if Is_Object (Obj_Id) then
+      if Present (Obj_Id)
+        and then Is_Object (Obj_Id)
+      then
          Ren := Renamed_Object (Obj_Id);
 
          if Present (Ren) then


diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1893,13 +1893,6 @@  package body Inline is
       then
          return False;
 
-      --  Subprograms in generic instances are currently not inlined, as this
-      --  interacts badly with the expansion of object renamings in GNATprove
-      --  mode.
-
-      elsif Instantiation_Location (Sloc (Id)) /= No_Location then
-         return False;
-
       --  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.
@@ -2643,6 +2636,75 @@  package body Inline is
       end if;
    end Check_And_Split_Unconstrained_Function;
 
+   ---------------------------------------------
+   -- Check_Object_Renaming_In_GNATprove_Mode --
+   ---------------------------------------------
+
+   procedure Check_Object_Renaming_In_GNATprove_Mode (Spec_Id : Entity_Id) is
+      Decl      : constant Node_Id := Unit_Declaration_Node (Spec_Id);
+      Body_Decl : constant Node_Id :=
+        Unit_Declaration_Node (Corresponding_Body (Decl));
+
+      function Check_Object_Renaming (N : Node_Id) return Traverse_Result;
+      --  Returns Abandon on node N if this is a reference to an object
+      --  renaming, which will be expanded into the renamed object in
+      --  GNATprove mode.
+
+      ---------------------------
+      -- Check_Object_Renaming --
+      ---------------------------
+
+      function Check_Object_Renaming (N : Node_Id) return Traverse_Result is
+      begin
+         case Nkind (Original_Node (N)) is
+            when N_Expanded_Name
+               | N_Identifier
+            =>
+               declare
+                  Obj_Id : constant Entity_Id := Entity (Original_Node (N));
+               begin
+                  --  Recognize the case when SPARK expansion rewrites a
+                  --  reference to an object renaming.
+
+                  if Present (Obj_Id)
+                    and then Is_Object (Obj_Id)
+                    and then Present (Renamed_Object (Obj_Id))
+                    and then Nkind (Renamed_Object (Obj_Id)) not in N_Entity
+
+                    --  Copy_Generic_Node called for inlining expects the
+                    --  references to global entities to have the same kind
+                    --  in the "generic" code and its "instantiation".
+
+                    and then Nkind (Original_Node (N)) /=
+                      Nkind (Renamed_Object (Obj_Id))
+                  then
+                     return Abandon;
+                  else
+                     return OK;
+                  end if;
+               end;
+
+            when others =>
+               return OK;
+         end case;
+      end Check_Object_Renaming;
+
+      function Check_All_Object_Renamings is new
+        Traverse_Func (Check_Object_Renaming);
+
+   --  Start of processing for Check_Object_Renaming_In_GNATprove_Mode
+
+   begin
+      --  Subprograms with object renamings replaced by the special SPARK
+      --  expansion cannot be inlined.
+
+      if Check_All_Object_Renamings (Body_Decl) /= OK then
+         Cannot_Inline ("cannot inline & (object renaming)?",
+                        Body_Decl, Spec_Id);
+         Set_Body_To_Inline (Decl, Empty);
+      end if;
+   end Check_Object_Renaming_In_GNATprove_Mode;
+
    -------------------------------------
    -- Check_Package_Body_For_Inlining --
    -------------------------------------


diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -198,6 +198,15 @@  package Inline is
    --  cases documented in Check_Body_To_Inline) then build the body-to-inline
    --  associated with N and attach it to the declaration node of Spec_Id.
 
+   procedure Check_Object_Renaming_In_GNATprove_Mode (Spec_Id : Entity_Id)
+   with
+     Pre => GNATprove_Mode;
+   --  This procedure is called only in GNATprove mode, on subprograms for
+   --  which a Body_To_Inline was created, to check if the subprogram has
+   --  references to object renamings which will be replaced by the special
+   --  SPARK expansion into nodes of a different kind, which is not expected
+   --  by the inlining mechanism. In that case, the Body_To_Inline is deleted.
+
    procedure Check_Package_Body_For_Inlining (N : Node_Id; P : Entity_Id);
    --  If front-end inlining is enabled and a package declaration contains
    --  inlined subprograms, load and compile the package body to collect the


diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -8122,7 +8122,10 @@  package body Sem_Ch12 is
                      Set_Entity (New_N, Entity (Name (Assoc)));
 
                   elsif Nkind (Assoc) in N_Entity
-                    and then Expander_Active
+                    and then (Expander_Active or
+                                (GNATprove_Mode
+                                  and then not In_Spec_Expression
+                                  and then not Inside_A_Generic))
                   then
                      --  Inlining case: we are copying a tree that contains
                      --  global entities, which are preserved in the copy to be


diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -5459,6 +5459,22 @@  package body Sem_Ch6 is
          end;
       end;
 
+      --  Check if a Body_To_Inline was created, but the subprogram has
+      --  references to object renamings which will be replaced by the special
+      --  SPARK expansion into nodes of a different kind, which is not expected
+      --  by the inlining mechanism. In that case, the Body_To_Inline is
+      --  deleted prior to being analyzed. This check needs to take place
+      --  after analysis of the subprogram body.
+
+      if GNATprove_Mode
+        and then Present (Spec_Id)
+        and then
+          Nkind (Unit_Declaration_Node (Spec_Id)) = N_Subprogram_Declaration
+        and then Present (Body_To_Inline (Unit_Declaration_Node (Spec_Id)))
+      then
+         Check_Object_Renaming_In_GNATprove_Mode (Spec_Id);
+      end if;
+
       --  Check for variables that are never modified
 
       declare