diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-10 08:59:33 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-10 08:59:33 +0000 |
| commit | e9427de1bf3eb46ba1651a8fd2ce1feb7e8d63f1 (patch) | |
| tree | 164ce3cfd5a3ed037d11aee35da58ca446c19ae2 /gcc/ada/sysdep.c | |
| parent | a620ef15027baace38d591709474f1a9519ba657 (diff) | |
| download | gcc-e9427de1bf3eb46ba1651a8fd2ce1feb7e8d63f1.zip gcc-e9427de1bf3eb46ba1651a8fd2ce1feb7e8d63f1.tar.gz gcc-e9427de1bf3eb46ba1651a8fd2ce1feb7e8d63f1.tar.bz2 | |
[Ada] Use renamings in GNATprove mode for side-effects extraction
In the GNATprove mode for formal verification, prefer renamings over
declaration of a constant to extract side-effects from expressions,
whenever the constant could be of an owning type, as declaring a
constant of an owning type has an effect on ownership which is
undesirable.
There is no impact on compilation.
2019-07-10 Yannick Moy <moy@adacore.com>
gcc/ada/
* exp_util.adb (Remove_Side_Effects): Prefer renamings for
objects of possible owning type in GNATprove mode.
From-SVN: r273324
Diffstat (limited to 'gcc/ada/sysdep.c')
0 files changed, 0 insertions, 0 deletions