projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e841d4d) | patch
[Ada] Prevent inlining inside condition of while loop in GNATprove
authorYannick Moy <moy@adacore.com>
Fri, 13 Dec 2019 09:03:56 +0000 (09:03 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Fri, 13 Dec 2019 09:03:56 +0000 (09:03 +0000)
commit2e3795d016a7263c82a4f64a7204f416d12a72da
tree50251f6c4c7b8928e9a446e70b716e274ee54f7ctree
parente841d4d8b3d1e64fe2f31329c8644ceca341874fcommit | diff
[Ada] Prevent inlining inside condition of while loop in GNATprove

2019-12-13  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_res.adb (Resolve_Call): Prevent inlining inside while loop
conditions.
* sem_util.adb, sem_util.ads (In_While_Loop_Condition): New
query function.

From-SVN: r279347
gcc/ada/ChangeLog diff | blob | history
gcc/ada/sem_res.adb diff | blob | history
gcc/ada/sem_util.adb diff | blob | history
gcc/ada/sem_util.ads diff | blob | history