* [Ada] Prevent generation of gotos during inlining for GNATprove
@ 2014-10-30 11:35 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2014-10-30 11:35 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 404 bytes --]
In GNATprove mode, the special frontend inlining could generate gotos on
return statements inside blocks, thus causing errors in GNATprove later.
Now prevent inlining of such subprograms.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-10-30 Yannick Moy <moy@adacore.com>
* inline.adb (Has_Single_Return_In_GNATprove_Mode):
Return False when return statement is inside one or more blocks.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 2090 bytes --]
Index: inline.adb
===================================================================
--- inline.adb (revision 216770)
+++ inline.adb (working copy)
@@ -933,7 +933,10 @@
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.
+ -- 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
@@ -1003,15 +1006,10 @@
-- Start of processing for Has_Single_Return_In_GNATprove_Mode
begin
- -- Retrieve last statement inside possible block statements
+ -- Retrieve the last statement
Last_Statement := Last (Statements (Handled_Statement_Sequence (N)));
- while Nkind (Last_Statement) = N_Block_Statement loop
- Last_Statement :=
- Last (Statements (Handled_Statement_Sequence (Last_Statement)));
- end loop;
-
-- Check that the last statement is the only possible return
-- statement in the subprogram.
@@ -2049,16 +2047,15 @@
OK : Boolean;
begin
- if Is_Compilation_Unit (P)
+ if Front_End_Inlining
+ and then Is_Compilation_Unit (P)
and then not Is_Generic_Instance (P)
then
Bname := Get_Body_Name (Get_Unit_Name (Unit (N)));
E := First_Entity (P);
while Present (E) loop
- if Has_Pragma_Inline_Always (E)
- or else (Front_End_Inlining and then Has_Pragma_Inline (E))
- then
+ if Has_Pragma_Inline (E) then
if not Is_Loaded (Bname) then
Load_Needed_Body (N, OK);
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2014-10-30 11:34 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-10-30 11:35 [Ada] Prevent generation of gotos during inlining for GNATprove Arnaud Charlet
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).