@@ -1460,10 +1460,47 @@ package body Inline is
(N : Node_Id;
Subp : Entity_Id) return Boolean
is
+ function Has_Dereference (N : Node_Id) return Boolean;
+ -- Return whether N contains an explicit dereference
+
+ ---------------------
+ -- Has_Dereference --
+ ---------------------
+
+ function Has_Dereference (N : Node_Id) return Boolean is
+
+ function Process (N : Node_Id) return Traverse_Result;
+ -- Process one node in search for dereference
+
+ -------------
+ -- Process --
+ -------------
+
+ function Process (N : Node_Id) return Traverse_Result is
+ begin
+ if Nkind (N) = N_Explicit_Dereference then
+ return Abandon;
+ else
+ return OK;
+ end if;
+ end Process;
+
+ function Traverse is new Traverse_Func (Process);
+ -- Traverse tree to look for dereference
+
+ begin
+ return Traverse (N) = Abandon;
+ end Has_Dereference;
+
+ -- Local variables
+
F : Entity_Id;
A : Node_Id;
begin
+ -- Check if inlining may lead to missing a check on type conversion of
+ -- input parameters otherwise.
+
F := First_Formal (Subp);
A := First_Actual (N);
while Present (F) loop
@@ -1480,6 +1517,27 @@ package body Inline is
Next_Actual (A);
end loop;
+ -- Check if inlining may lead to introducing temporaries of access type,
+ -- which can lead to missing checks for memory leaks. This can only
+ -- come from an (IN-)OUT parameter transformed into a renaming by SPARK
+ -- expansion, whose side-effects are removed, and a dereference in the
+ -- corresponding actual. If the formal itself is of a deep type (it has
+ -- access subcomponents), the subprogram already cannot be inlined in
+ -- GNATprove mode.
+
+ F := First_Formal (Subp);
+ A := First_Actual (N);
+ while Present (F) loop
+ if Ekind (F) /= E_In_Parameter
+ and then Has_Dereference (A)
+ then
+ return False;
+ end if;
+
+ Next_Formal (F);
+ Next_Actual (A);
+ end loop;
+
return True;
end Call_Can_Be_Inlined_In_GNATprove_Mode;
@@ -146,8 +146,9 @@ package Inline is
(N : Node_Id;
Subp : Entity_Id) return Boolean;
-- Returns False if the call in node N to subprogram Subp cannot be inlined
- -- in GNATprove mode, because it may lead to missing a check on type
- -- conversion of input parameters otherwise. Returns True otherwise.
+ -- in GNATprove mode, because it may otherwise lead to missing a check
+ -- on type conversion of input parameters, or a missing memory leak on
+ -- an output parameter. Returns True otherwise.
function Can_Be_Inlined_In_GNATprove_Mode
(Spec_Id : Entity_Id;
@@ -7329,11 +7329,12 @@ package body Sem_Res is
("cannot inline & (in while loop condition)?", N, Nam_UA);
-- Do not inline calls which would possibly lead to missing a
- -- type conversion check on an input parameter.
+ -- type conversion check on an input parameter or a memory leak
+ -- on an output parameter.
elsif not Call_Can_Be_Inlined_In_GNATprove_Mode (N, Nam) then
Cannot_Inline
- ("cannot inline & (possible check on input parameters)?",
+ ("cannot inline & (possible check on parameters)?",
N, Nam_UA);
-- Otherwise, inline the call, issuing an info message when
From: Yannick Moy <moy@adacore.com> In some cases, inlining a call in GNATprove could lead to missing a memory leak. Recognize such cases and do not inline such calls. gcc/ada/ * inline.adb (Call_Can_Be_Inlined_In_GNATprove_Mode): Add case to prevent inlining of call. * inline.ads: Likewise. * sem_res.adb (Resolve_Call): Update comment and message. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/inline.adb | 58 +++++++++++++++++++++++++++++++++++++++++++++ gcc/ada/inline.ads | 5 ++-- gcc/ada/sem_res.adb | 5 ++-- 3 files changed, 64 insertions(+), 4 deletions(-)