projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a4bbe10) | patch
[Ada] Do not skip non-aliasing checking when inlining in GNATprove
authorYannick Moy <moy@adacore.com>
Mon, 19 Aug 2019 08:35:35 +0000 (08:35 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 19 Aug 2019 08:35:35 +0000 (08:35 +0000)
commitc811dd91e184db204073d04c28ed107888b39518
treefdffc74159e6b658e73dc2133acb7cebcae8e6bctree
parenta4bbe10deb69d4885baffde7fa42c0ba137e7dc8commit | diff
[Ada] Do not skip non-aliasing checking when inlining in GNATprove

When code is inlinined for proof in the special mode for GNATprove, Ada
rules about non-aliasing should still be checked. Now fixed.

There is no impact on compilation.

2019-08-19  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_res.adb (Resolve_Call): Check non-aliasing rules before
GNATprove inlining.

From-SVN: r274640
gcc/ada/ChangeLog diff | blob | history
gcc/ada/sem_res.adb diff | blob | history