aboutsummaryrefslogtreecommitdiff
path: root/gnattools
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 /gnattools
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 'gnattools')
0 files changed, 0 insertions, 0 deletions