[Ada] Expand controlling functions wrappers in GNATprove mode
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 24 Nov 2021 22:21:07 +0000 (23:21 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 5 Jan 2022 11:32:37 +0000 (11:32 +0000)
commit3531f20f6cff7e43dcde44b200467872a925188f
treef3bf8a89d0eb7a63e034bd31930339f45357d6b9
parent48b8a564c9565635db0a93b9b1e6a31d38547981
[Ada] Expand controlling functions wrappers in GNATprove mode

gcc/ada/

* exp_ch3.ads (Make_Controlling_Function_Wrappers): Move
declaration from body to spec, so it can be called by
SPARK-specific expansion.
* exp_ch3.adb (Make_Controlling_Function_Wrappers): Likewise.
* exp_spark.adb (SPARK_Freeze_Type): Enable expansion of
wrappers for function with controlling result types.
gcc/ada/exp_ch3.adb
gcc/ada/exp_ch3.ads
gcc/ada/exp_spark.adb