ada: Inline for proof without creating extra objects

When inlining subprogram calls in GNATprove mode, we were creating object
declarations only to force checks that would be otherwise missed with object
renamings. Now ghat GNATprove emits those checks for object renamings anyway
(as required by Ada 2022), we no longer need those extra objects.

gcc/ada/ChangeLog:

	* inline.adb (Establish_Actual_Mapping_For_Inlined_Call): Do not create
	object declarations when actual is captured in an object renaming.

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index abaf997d9c281cf0d9ff366cb79dd1df6a944e7f..265ebb5a317b73ce91c1bd7670743219760c211c 100644 (file)
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -3326,27 +3326,6 @@ package body Inline is
                    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,