From e9427de1bf3eb46ba1651a8fd2ce1feb7e8d63f1 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 10 Jul 2019 08:59:33 +0000 Subject: [PATCH] [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 gcc/ada/ * exp_util.adb (Remove_Side_Effects): Prefer renamings for objects of possible owning type in GNATprove mode. From-SVN: r273324 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/exp_util.adb | 12 +++++++++++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index cb2acf31d61..db33d646403 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-10 Yannick Moy + + * exp_util.adb (Remove_Side_Effects): Prefer renamings for + objects of possible owning type in GNATprove mode. + 2019-07-09 Ed Schonberg * 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 f13108092b5..2d88ee96b7c 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, -- 2.30.2