[Ada] Allow inlining for proof inside generics

For local subprograms without contracts inside generics, allow their
inlining for proof in GNATprove mode. This requires forbidding the
inlining of subprograms which contain references to object renamings,
which would be replaced in the SPARK expansion and violate assumptions
of the inlining code.

gcc/ada/

	* exp_spark.adb (Expand_SPARK_Potential_Renaming): Deal with no
	entity case.
	* inline.ads (Check_Object_Renaming_In_GNATprove_Mode): New
	procedure.
	* inline.adb (Check_Object_Renaming_In_GNATprove_Mode): New
	procedure.
	(Can_Be_Inlined_In_GNATprove_Mode): Remove case forbidding
	inlining for subprograms inside generics.
	* sem_ch12.adb (Copy_Generic_Node): Preserve global entities
	when inlining in GNATprove mode.
	* sem_ch6.adb (Analyse_Subprogram_Body_Helper): Remove body to
	inline if renaming is detected in GNATprove mode.

1 files changed, 16 insertions, 0 deletions

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 38ed14f27b3..2939394d88d 100644
--- 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