diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 4 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 6 |
2 files changed, 9 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 948d0fa..17c27abc 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,9 @@ 2019-07-09 Yannick Moy <moy@adacore.com> + * sinfo.ads: Refine comment for Do_Range_Check. + +2019-07-09 Yannick Moy <moy@adacore.com> + * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Expand attribute reference on Enum_Rep. diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index b1e57bf..7be56cb 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -754,7 +754,11 @@ package Sinfo is -- GNATprove mode. As a special case, the front end does not insert a -- Do_Division_Check flag on float exponentiation expressions, for the case -- where the value is 0.0 and the exponent is negative, although this case - -- does lead to a division check failure. + -- does lead to a division check failure. As another special case, + -- the frontend does not insert a Do_Range_Check on an allocator where + -- the designated type is scalar, and the designated type is more + -- constrained than the type of the initialized allocator value or the type + -- of the default value for an uninitialized allocator. -- Note: the expander always takes care of the Do_Range check case, -- so this flag will never be set in the expanded tree passed to the |