diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-02-12 11:00:38 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-06-08 03:50:57 -0400 |
| commit | c382d0712fba76b6fce4a9aadc5a4487fad7efaf (patch) | |
| tree | 6059aa2c8dc57dc9b4873e761c0f98983f061ebc /gcc/ada/exp_spark.adb | |
| parent | 3ebf0cbda50a5f5682456cdbb064576e0a08c0f7 (diff) | |
| download | gcc-c382d0712fba76b6fce4a9aadc5a4487fad7efaf.zip gcc-c382d0712fba76b6fce4a9aadc5a4487fad7efaf.tar.gz gcc-c382d0712fba76b6fce4a9aadc5a4487fad7efaf.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/exp_spark.adb')
| -rw-r--r-- | gcc/ada/exp_spark.adb | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 5257f29..a54a162 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; |