[Ada] Reuse standard expansion of 'First and 'Last in GNATprove mode

[Pierre-Marie de Rodat]

Expansion of attribute Enum_Rep applied to First and Last attributes,
both in the standard compilation mode and in the GNATprove mode, relies
on those First and Last attributes being already expanded. However, they
were only expanded in the standard compilation mode; now they are also
expanded in the GNATprove mode.

This change only affects GNATprove; GNAT and other backends are not
affected.

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

2020-06-08  Piotr Trojanek  <troja...@adacore.com>

gcc/ada/

        * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Apply
        standard expansion to attributes First and Last.
--- gcc/ada/exp_spark.adb
+++ gcc/ada/exp_spark.adb
@@ -295,6 +295,13 @@ package body Exp_SPARK is
                      Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
             Analyze_And_Resolve (N, Standard_Boolean);
          end if;
+
+      --  For attributes First and Last simply reuse the standard expansion
+
+      elsif Attr_Id = Attribute_First
+        or else Attr_Id = Attribute_Last
+      then
+         Exp_Attr.Expand_N_Attribute_Reference (N);
       end if;
    end Expand_SPARK_N_Attribute_Reference;