From: Piotr Trojanek Date: Fri, 19 Jun 2020 15:14:42 +0000 (+0200) Subject: [Ada] Do not remove side effects from any object declarations in SPARK X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d43123ee06f0cef47ffcacad8f6c9f9d753c1841;p=gcc.git [Ada] Do not remove side effects from any object declarations in SPARK gcc/ada/ * exp_util.adb (Remove_Side_Effects): Move special-casing for GNATprove to be applied to all object declarations. --- diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 0f8505f1ad7..13af3e8dce9 100644 --- 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