From c382d0712fba76b6fce4a9aadc5a4487fad7efaf Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Wed, 12 Feb 2020 11:00:38 +0100 Subject: [PATCH] [Ada] Reuse standard expansion of 'First and 'Last in GNATprove mode 2020-06-08 Piotr Trojanek gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Apply standard expansion to attributes First and Last. --- 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; -- 2.30.2