[Ada] Set range checks flag on 'Update for GNATprove in expansion
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 29 Apr 2020 20:15:16 +0000 (22:15 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 6 Jul 2020 11:35:05 +0000 (07:35 -0400)
commit8f892a98cc4599b7562e041a53ecfa920c72551c
tree41774e2e1ec10a0caf01d0d23b195c44b4bfd14d
parent977b168196992b3f15d167c2f7d05cec38ac0302
[Ada] Set range checks flag on 'Update for GNATprove in expansion

gcc/ada/

* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Apply
scalar range checks.
* sem_attr.adb (Resolve_Attribute): Do not set scalar range
checks when resolving attribute Update.
gcc/ada/exp_spark.adb
gcc/ada/sem_attr.adb