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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-10 Yannick Moy <m...@adacore.com>
gcc/ada/
* exp_util.adb (Remove_Side_Effects): Prefer renamings for
objects of possible owning type in GNATprove mode.--- gcc/ada/exp_util.adb
+++ 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,
