Changes in GNATprove (translation to Why3 and provers) result in proofs being much less automatic, and requiring ghost code to detail intermediate steps. In some cases, it is better to use the new By mechanism to prove assertions in steps, as this avoids polluting the proof context for other proofs. For that reason, add units s-spark.ads and s-spcuop.ads/b to the runtime sources.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* Makefile.rtl: Add new units.
* libgnat/s-aridou.adb (Scaled_Divide): Add ghost code for provers.
* libgnat/s-spcuop.adb: New unit for ghost cut operations.
* libgnat/s-spcuop.ads: New unit for ghost cut operations.
* libgnat/s-spark.ads: New unit.
patch.diff.gz
Description: application/gzip
