[gcc(refs/users/aoliva/heads/testme)] [Ada] Reuse standard expansion of 'First and 'Last in GNATprove mode

[Alexandre Oliva]

https://gcc.gnu.org/g:c382d0712fba76b6fce4a9aadc5a4487fad7efaf

commit c382d0712fba76b6fce4a9aadc5a4487fad7efaf
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Wed Feb 12 11:00:38 2020 +0100

    [Ada] Reuse standard expansion of 'First and 'Last in GNATprove mode
    
    2020-06-08  Piotr Trojanek  <trojanek@adacore.com>
    
    gcc/ada/
    
            * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Apply
            standard expansion to attributes First and Last.

Diff:
---
 gcc/ada/exp_spark.adb | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 5257f29677b..a54a16235a8 100644
--- a/gcc/ada/exp_spark.adb
+++ b/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;