[Ada] Proof of runtime units for integer exponentiation (checks off)

Pierre-Marie de Rodat derodat@adacore.com
Wed Jan 5 11:33:31 GMT 2022


This proves the generic unit System.Exponn instanciated for Integer,
Long_Long_Integer and Long_Long_Long_Integer. In order to be able to add
a suitable contract to the generic function, it is changed into a
generic package which contains the function. Instantiations are adapted.

GNATprove is called with switch --level=2.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/s-exnint.ads: Mark in SPARK. Adapt to change to
	package.
	* libgnat/s-exnlli.ads: Likewise.
	* libgnat/s-exnllli.ads: Likewise.
	* libgnat/s-exponn.adb: Add lemmas and ghost code. Secial case
	value zero as Left or Right to simplify proof.
	* libgnat/s-exponn.ads: Transform the generic function into a
	generic package with a function inside. Add a functional
	contract.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 12475 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20220105/f916c8a8/attachment.bin>


More information about the Gcc-patches mailing list