@@ -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
From: Piotr Trojanek <trojanek@adacore.com> 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. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/inline.adb | 91 ++++------------------------------------------ 1 file changed, 8 insertions(+), 83 deletions(-)