ada: Prevent inlining in GNATprove for memory leaks

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.

3 files changed, 64 insertions, 4 deletions

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 2ec92ca..98bed86 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -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;
 
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index 3df0a01..bc90c0c 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -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;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 075c0d8..67062c6 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -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