https://gcc.gnu.org/g:c6e0eb60dfdad5be8b4ee30c6cfe264f63214e2e
commit r17-1321-gc6e0eb60dfdad5be8b4ee30c6cfe264f63214e2e Author: Piotr Trojanek <[email protected]> Date: Wed May 13 16:56:03 2026 +0200 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: --- gcc/ada/inline.adb | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index abaf997d9c28..265ebb5a317b 100644 --- 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,
