r274290 - in /trunk/gcc/ada: ChangeLog exp_attr...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Mon Aug 12 08:59:42 2019
New Revision: 274290

URL: https://gcc.gnu.org/viewcvs?rev=274290&root=gcc&view=rev
Log:
[Ada] More precise handling of Size/Object_Size in GNATprove

GNATprove does a partial expansion which did not allow getting the
most precise value for attributes Size/Object_Size. Now fixed.

There is no impact on compilation.

2019-08-12  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* exp_attr.adb, exp_attr.ads (Expand_Size_Attribute): New
	procedure to share part of the attribute expansion with
	GNATprove mode.
	(Expand_N_Attribute_Reference): Extract part of the
	Size/Object_Size expansion in the new procedure
	Expand_Size_Attribute.
	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Expand
	Size/Object_Size attributes using the new procedure
	Expand_Size_Attribute.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/exp_attr.adb
    trunk/gcc/ada/exp_attr.ads
    trunk/gcc/ada/exp_spark.adb