diff options
author | Yannick Moy <moy@adacore.com> | 2019-08-12 08:59:42 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-08-12 08:59:42 +0000 |
commit | d39f6b24d401c8a945fae1488de0dea2252ec7ae (patch) | |
tree | 47025463fc6ac7c0e821c0258bc24adbab991749 /gcc/tree.c | |
parent | 08c8696d4884425839fc5cd14a8788fe53f031e4 (diff) | |
download | gcc-d39f6b24d401c8a945fae1488de0dea2252ec7ae.zip gcc-d39f6b24d401c8a945fae1488de0dea2252ec7ae.tar.gz gcc-d39f6b24d401c8a945fae1488de0dea2252ec7ae.tar.bz2 |
[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.
From-SVN: r274290
Diffstat (limited to 'gcc/tree.c')
0 files changed, 0 insertions, 0 deletions