OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Use renamings in GNATprove mode for side-effects extraction

Browse Source 
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
This commit is contained in:
Yannick Moy 2019-07-10 08:59:33 +00:00 committed by Pierre-Marie de Rodat
parent a620ef1502
commit e9427de1bf
2 changed files with 16 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
gcc/ada/ChangeLog
View File

@ -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

12
gcc/ada/exp_util.adb
View File

@ -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,