exp_spark.adb (Expand_SPARK_Attribute_Reference): For attributes which return Univers...
authorClaire Dross <dross@adacore.com>
Mon, 23 Jan 2017 11:19:56 +0000 (11:19 +0000)
committerArnaud Charlet <charlet@gcc.gnu.org>
Mon, 23 Jan 2017 11:19:56 +0000 (12:19 +0100)
commitd553a695b917d3240fcf8ca5ea9e09ad8dd8a5f3
treedb41c8e1c5a062bf3dd5dd48a8dbfcba6f173090
parent6d67bea9215e3d0ca6fb9dbd55124907a395f746
exp_spark.adb (Expand_SPARK_Attribute_Reference): For attributes which return Universal_Integer...

2017-01-23  Claire Dross  <dross@adacore.com>

* exp_spark.adb (Expand_SPARK_Attribute_Reference): For attributes
which return Universal_Integer, force the overflow check flag for
Length and Range_Length for types as big as Long_Long_Integer.

From-SVN: r244777
gcc/ada/ChangeLog
gcc/ada/exp_spark.adb