https://gcc.gnu.org/g:079cbf59c5110b290917d09935afec0d7fe29acc
commit r17-863-g079cbf59c5110b290917d09935afec0d7fe29acc Author: Claire Dross <[email protected]> Date: Thu Feb 19 17:06:09 2026 +0100 ada: Implement restrictions for unchecked union in inlining for GNATprove Do not inline calls when a formal parameter has an unchecked union type as it might lead to missing checks for UU restrictions. gcc/ada/ChangeLog: * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline subprograms with formals of an unchecked union type. Diff: --- gcc/ada/inline.adb | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 05675723ee51..7c8b43ca5773 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1428,7 +1428,7 @@ package body Inline is and then not Same_Type (Etype (F), Etype (A)) and then (Is_By_Reference_Type (Etype (A)) - or else Is_Limited_Type (Etype (A))) + or else Is_Limited_Type (Etype (A))) then return False; end if; @@ -1477,6 +1477,11 @@ package body Inline is -- inlining, if the address clause mentions a constant view of a mutable -- object at call site. + function Has_Formal_Of_UU_Type + (Id : Entity_Id) return Boolean; + -- Returns true if the subprogram has at least one formal parameter of + -- an unchecked conversion type. + function Has_Formal_Or_Result_Of_Deep_Type (Id : Entity_Id) return Boolean; -- Returns true if the subprogram has at least one formal parameter or @@ -1581,6 +1586,35 @@ package body Inline is (Body_Node) = Abandon; end Has_Constant_With_Address_Clause; + --------------------------- + -- Has_Formal_Of_UU_Type -- + --------------------------- + + function Has_Formal_Of_UU_Type + (Id : Entity_Id) return Boolean + is + Subp_Id : constant Entity_Id := Ultimate_Alias (Id); + Formal : Entity_Id; + Formal_Typ : Entity_Id; + + begin + -- Inspect all parameters of the subprogram looking for a formal + -- of an unchecked union type. + + Formal := First_Formal (Subp_Id); + while Present (Formal) loop + Formal_Typ := Etype (Formal); + + if Is_Unchecked_Union (Formal_Typ) then + return True; + end if; + + Next_Formal (Formal); + end loop; + + return False; + end Has_Formal_Of_UU_Type; + --------------------------------------- -- Has_Formal_Or_Result_Of_Deep_Type -- --------------------------------------- @@ -2066,6 +2100,14 @@ package body Inline is elsif Has_Formal_Or_Result_Of_Deep_Type (Id) then return False; + -- Do not inline calls if a parameter has an uncked union type as + -- inlining might cause an object to have inferrable discriminants + -- while it would not be the case without inlining, resulting in + -- checks for UU restrictions being missed. + + elsif Has_Formal_Of_UU_Type (Id) then + return False; + -- Do not inline subprograms which may be traversal functions. Such -- inlining introduces temporary variables of named access type for -- which assignments are move instead of borrow/observe, possibly
