[Ada] Add range check for GNATprove on 'Pos to Long_Integer conversion

[Pierre-Marie de Rodat]

In GNAT mode attribute Pos is typically expanded into either a type
conversion (unless applied to enumeration types with custom
representation values) and analysis of this type conversion adds check
flags as required.

In GNATprove mode we expand the attribute with
Apply_Universal_Integer_Attribute_Checks, which adds a type conversion,
but its analysis only adds check flags if the size of the target type is
smaller than the size of universal integer. This should be fixed in the
compiler itself, but we already had a workaround for 'Length and
'Range_Length.

This patch extends the existing workaround to 'Pos, which is enough to
solve the problem in GNATprove; the compiler is not affected by this
patch.

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

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference) Extend
	existing workaround to 'Pos.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 1497 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20200727/1a707aa2/attachment-0001.bin>