aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/inline.ads
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2017-01-13 10:22:23 +0000
committerArnaud Charlet <charlet@gcc.gnu.org>2017-01-13 11:22:23 +0100
commit3de3a1be9ee8c46efce3714cbbecaae0c7efe3f0 (patch)
treee031513a067f8fa4ff85971c4baa742f200c3de5 /gcc/ada/inline.ads
parent4ccff88b71d7988940c736f123071b11fb614d05 (diff)
downloadgcc-3de3a1be9ee8c46efce3714cbbecaae0c7efe3f0.zip
gcc-3de3a1be9ee8c46efce3714cbbecaae0c7efe3f0.tar.gz
gcc-3de3a1be9ee8c46efce3714cbbecaae0c7efe3f0.tar.bz2
inline.adb, inline.ads (Call_Can_Be_Inlined_In_GNATprove_Mode): New function to detect when a call may be inlined or not in GNATprove mode.
2017-01-13 Yannick Moy <moy@adacore.com> * inline.adb, inline.ads (Call_Can_Be_Inlined_In_GNATprove_Mode): New function to detect when a call may be inlined or not in GNATprove mode. (Expand_Inlined_Call): Ensure that a temporary is always created in the cases where a type conversion may be needed on an input parameter in GNATprove mode, so that GNATprove sees the check to perform. * sem_res.adb (Resolve_Call): In GNATprove mode, skip inlining when not applicable due to actual requiring type conversion with possible check but no temporary value can be copied for GNATprove to see the check. From-SVN: r244408
Diffstat (limited to 'gcc/ada/inline.ads')
-rw-r--r--gcc/ada/inline.ads9
1 files changed, 8 insertions, 1 deletions
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index 04662b8..96cff58 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -167,6 +167,13 @@ package Inline is
-- enabled and the subprogram contains a construct that cannot be inlined,
-- the problematic construct is flagged accordingly.
+ function Call_Can_Be_Inlined_In_GNATprove_Mode
+ (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.
+
function Can_Be_Inlined_In_GNATprove_Mode
(Spec_Id : Entity_Id;
Body_Id : Entity_Id) return Boolean;