[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cb2acf31d61402a54fd3035148bd0b81435225aa..db33d6464032975f83e92238d6b03a7b2bad63fd 100644 (file)
--- 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 f13108092b57d7aa90d40183151178c5caaebf73..2d88ee96b7c3729b31939c6e7c4ac4ecc235cf10 100644 (file)
--- 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,