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.
From-SVN: r274290
