[Ada] Fix inlining in GNATprove inside quantified expressions
authorYannick Moy <moy@adacore.com>
Fri, 5 Jul 2019 07:01:58 +0000 (07:01 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Fri, 5 Jul 2019 07:01:58 +0000 (07:01 +0000)
commit85ee7b4903e320b8f22ac0350afcd07263d2a5d6
treec0a8554a62bde176db6e24ccf9f73e22bf598244
parent8518042a54fde0880fabc3e380e9549ad13de601
[Ada] Fix inlining in GNATprove inside quantified expressions

Calls to local subprograms in GNATprove may be inlined in some case, but
it should not be the case inside quantified expressions which are
handled as expressions inside GNATprove. Because quantified expressions
are only preanalayzed, the detection of the impossible inlining was not
performed.  Now fixed.

There is no impact on compilation.

2019-07-05  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_res.adb (Resolve_Call): Cannot inline in quantified
expressions.
* sem_util.adb, sem_util.ads (In_Quantified_Expression): New
function.

From-SVN: r273105
gcc/ada/ChangeLog
gcc/ada/sem_res.adb
gcc/ada/sem_util.adb
gcc/ada/sem_util.ads