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 | |
| 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')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/exp_util.adb | 12 |
2 files changed, 16 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index cb2acf3..db33d64 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-10 Yannick Moy <moy@adacore.com> + + * exp_util.adb (Remove_Side_Effects): Prefer renamings for + objects of possible owning type in GNATprove mode. + 2019-07-09 Ed Schonberg <schonberg@adacore.com> * sem_ch3.adb (Analyze_Object_Declaration): If the object type diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index f131080..2d88ee9 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -11333,7 +11333,17 @@ package body Exp_Util is -- Generate: -- Rnn : Exp_Type renames Expr; - if Renaming_Req then + -- In GNATprove mode, we prefer to use renamings for intermediate + -- variables to definition of constants, due to the implicit move + -- operation that such a constant definition causes as part of the + -- support in GNATprove for ownership pointers. Hence we generate + -- a renaming for a reference to an object of a non-scalar type. + + if Renaming_Req + or else (GNATprove_Mode + and then Is_Object_Reference (Exp) + and then not Is_Scalar_Type (Exp_Type)) + then E := Make_Object_Renaming_Declaration (Loc, Defining_Identifier => Def_Id, |