[Ada] Do not remove side effects from any object declarations in SPARK

[Ada] Do not remove side effects from any object declarations in SPARK

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 621 bytes --]

In GNATprove mode we special-case the removal of side effect to do
nothing for object declarations. However, this special casing applied
only to some object declarations; now it applies to all.

This patch only affects GNATprove, where it prevents recursive expansion
of object declaration of a very particular record type (with explicitly
specified Size attribute to be less than 64 and having no
discriminants).

Compilation is not affected.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* exp_util.adb (Remove_Side_Effects): Move special-casing for
	GNATprove to be applied to all object declarations.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1663 bytes --]

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -11324,6 +11324,14 @@ package body Exp_Util is
         and then Is_Class_Wide_Type (Etype (Exp))
       then
          return;
+
+      --  An expression which is in SPARK mode is considered side effect free
+      --  if the resulting value is captured by a variable or a constant.
+
+      elsif GNATprove_Mode
+        and then Nkind (Parent (Exp)) = N_Object_Declaration
+      then
+         return;
       end if;
 
       --  The remaining processing is done with all checks suppressed
@@ -11576,15 +11584,6 @@ package body Exp_Util is
       --  Otherwise we generate a reference to the expression
 
       else
-         --  An expression which is in SPARK mode is considered side effect
-         --  free if the resulting value is captured by a variable or a
-         --  constant.
-
-         if GNATprove_Mode
-           and then Nkind (Parent (Exp)) = N_Object_Declaration
-         then
-            goto Leave;
-
          --  When generating C code we cannot consider side effect free object
          --  declarations that have discriminants and are initialized by means
          --  of a function call since on this target there is no secondary
@@ -11598,7 +11597,7 @@ package body Exp_Util is
          --  be identified here to avoid entering into a never-ending loop
          --  generating internal object declarations.
 
-         elsif Modify_Tree_For_C
+         if Modify_Tree_For_C
            and then Nkind (Parent (Exp)) = N_Object_Declaration
            and then
              (Nkind (Exp) /= N_Function_Call