projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ebf0cb) | patch
[Ada] Reuse standard expansion of 'First and 'Last in GNATprove mode
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 12 Feb 2020 10:00:38 +0000 (11:00 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 8 Jun 2020 07:50:57 +0000 (03:50 -0400)
commitc382d0712fba76b6fce4a9aadc5a4487fad7efaf
tree6059aa2c8dc57dc9b4873e761c0f98983f061ebctree
parent3ebf0cbda50a5f5682456cdbb064576e0a08c0f7commit | diff
[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.
gcc/ada/exp_spark.adb diff | blob | history