ada: Enable inlining for subprograms with multiple return statements

With the support for forward GOTO statements in the GNATprove backend,
we can now inline subprograms with multiple return statements in the
frontend.

Also, fix inconsistent source locations in the inlined code, which were
now triggering assertion violations in the code for GNATprove
counterexamples.

gcc/ada/

	* inline.adb (Has_Single_Return_In_GNATprove_Mode): Remove.
	(Process_Formals): When rewriting an occurrence of a formal
	parameter, use location of the occurrence, not of the inlined
	call.

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 17b3099e6a65c7e386d87c533e700346678161e9..04cf1194009df805e247ca2e8b8b52a69c4e12e6 100644 (file)
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1090,14 +1090,6 @@ package body Inline is
       --  conflict with subsequent inlinings, so that it is unsafe to try to
       --  inline in such a case.
 
-      function Has_Single_Return_In_GNATprove_Mode return Boolean;
-      --  This function is called only in GNATprove mode, and it returns
-      --  True if the subprogram has no return statement or a single return
-      --  statement as last statement. It returns False for subprogram with
-      --  a single return as last statement inside one or more blocks, as
-      --  inlining would generate gotos in that case as well (although the
-      --  goto is useless in that case).
-
       function Uses_Secondary_Stack (Bod : Node_Id) return Boolean;
       --  If the body of the subprogram includes a call that returns an
       --  unconstrained type, the secondary stack is involved, and it is
@@ -1173,64 +1165,6 @@ package body Inline is
          return False;
       end Has_Pending_Instantiation;
 
-      -----------------------------------------
-      -- Has_Single_Return_In_GNATprove_Mode --
-      -----------------------------------------
-
-      function Has_Single_Return_In_GNATprove_Mode return Boolean is
-         Body_To_Inline : constant Node_Id := N;
-         Last_Statement : Node_Id := Empty;
-
-         function Check_Return (N : Node_Id) return Traverse_Result;
-         --  Returns OK on node N if this is not a return statement different
-         --  from the last statement in the subprogram.
-
-         ------------------
-         -- Check_Return --
-         ------------------
-
-         function Check_Return (N : Node_Id) return Traverse_Result is
-         begin
-            case Nkind (N) is
-               when N_Extended_Return_Statement
-                  | N_Simple_Return_Statement
-               =>
-                  if N = Last_Statement then
-                     return OK;
-                  else
-                     return Abandon;
-                  end if;
-
-               --  Skip locally declared subprogram bodies inside the body to
-               --  inline, as the return statements inside those do not count.
-
-               when N_Subprogram_Body =>
-                  if N = Body_To_Inline then
-                     return OK;
-                  else
-                     return Skip;
-                  end if;
-
-               when others =>
-                  return OK;
-            end case;
-         end Check_Return;
-
-         function Check_All_Returns is new Traverse_Func (Check_Return);
-
-      --  Start of processing for Has_Single_Return_In_GNATprove_Mode
-
-      begin
-         --  Retrieve the last statement
-
-         Last_Statement := Last (Statements (Handled_Statement_Sequence (N)));
-
-         --  Check that the last statement is the only possible return
-         --  statement in the subprogram.
-
-         return Check_All_Returns (N) = OK;
-      end Has_Single_Return_In_GNATprove_Mode;
-
       --------------------------
       -- Uses_Secondary_Stack --
       --------------------------
@@ -1275,16 +1209,6 @@ package body Inline is
       then
          return;
 
-      --  Subprograms that have return statements in the middle of the body are
-      --  inlined with gotos. GNATprove does not currently support gotos, so
-      --  we prevent such inlining.
-
-      elsif GNATprove_Mode
-        and then not Has_Single_Return_In_GNATprove_Mode
-      then
-         Cannot_Inline ("cannot inline & (multiple returns)?", N, Spec_Id);
-         return;
-
       --  Functions that return controlled types cannot currently be inlined
       --  because they require secondary stack handling; controlled actions
       --  may also interfere in complex ways with inlining.
@@ -3518,6 +3442,7 @@ package body Inline is
       ---------------------
 
       function Process_Formals (N : Node_Id) return Traverse_Result is
+         Loc : constant Source_Ptr := Sloc (N);
          A   : Entity_Id;
          E   : Entity_Id;
          Ret : Node_Id;
@@ -3544,13 +3469,13 @@ package body Inline is
 
                if Is_Entity_Name (A) then
                   Had_Private_View := Has_Private_View (N);
-                  Rewrite (N, New_Occurrence_Of (Entity (A), Sloc (N)));
+                  Rewrite (N, New_Occurrence_Of (Entity (A), Loc));
                   Set_Has_Private_View (N, Had_Private_View);
                   Check_Private_View (N);
 
                elsif Nkind (A) = N_Defining_Identifier then
                   Had_Private_View := Has_Private_View (N);
-                  Rewrite (N, New_Occurrence_Of (A, Sloc (N)));
+                  Rewrite (N, New_Occurrence_Of (A, Loc));
                   Set_Has_Private_View (N, Had_Private_View);
                   Check_Private_View (N);
 
@@ -3618,8 +3543,8 @@ package body Inline is
                  or else Yields_Universal_Type (Expression (N))
                then
                   Ret :=
-                    Make_Qualified_Expression (Sloc (N),
-                      Subtype_Mark => New_Occurrence_Of (Ret_Type, Sloc (N)),
+                    Make_Qualified_Expression (Loc,
+                      Subtype_Mark => New_Occurrence_Of (Ret_Type, Loc),
                       Expression   => Relocate_Node (Expression (N)));
 
                --  Use an unchecked type conversion between access types, for
@@ -3635,8 +3560,8 @@ package body Inline is
 
                else
                   Ret :=
-                    Make_Type_Conversion (Sloc (N),
-                      Subtype_Mark => New_Occurrence_Of (Ret_Type, Sloc (N)),
+                    Make_Type_Conversion (Loc,
+                      Subtype_Mark => New_Occurrence_Of (Ret_Type, Loc),
                       Expression   => Relocate_Node (Expression (N)));
                end if;
 
@@ -3715,7 +3640,7 @@ package body Inline is
          elsif Nkind (N) = N_Pragma
            and then Pragma_Name (N) = Name_Unreferenced
          then
-            Rewrite (N, Make_Null_Statement (Sloc (N)));
+            Rewrite (N, Make_Null_Statement (Loc));
             return OK;
 
          else