[Ada] Set range checks flag on 'Update for GNATprove in expansion

[Pierre-Marie de Rodat]

Range check flag on scalar expression in attribute Update was originally
set when this attribute is expanded into a sequence of assignment.
However, in GNATprove mode we have a custom expansion, which does
nothing with attribute Update; in particular, it didn't set the required
range check. As a workaround, we set this flag while resolving the
attribute, both for GNAT
and GNATprove.

Yet, this didn't really work for attribute Update in subprograms
"inlined for proof", where for some reason no checks at all were
inserted.

Also, this extra range check was unnecessary for a code like this:

   type T is record C : Natural; end record;
   X : T := (C => 1);
   Y : T := X'Update (C => X.C + 1);

because an overflow check (which is emitted anyway) is enough to protect
from a failing range check. A similar code, just without attribute
Update, does not have a range check:

   Y.C := X.C + 1;

This extra range check was hurting both compilation (by generating
useless run-time checks) and proof (by triggering messages about checks
that can never fail).

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 3980 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20200706/7862ac40/attachment-0001.bin>