git.ipfire.org Git - thirdparty/gcc.git/commit

]> git.ipfire.org Git - thirdparty/gcc.git/commit

projects / thirdparty / gcc.git / commit

author	Piotr Trojanek <trojanek@adacore.com>
	Wed, 29 Nov 2023 20:33:30 +0000 (21:33 +0100)
committer	Marc Poulhiès <poulhies@adacore.com>
	Tue, 9 Jan 2024 13:13:29 +0000 (14:13 +0100)
commit	bfacdd11d992c47771574470987ae8954a5b12fd
tree	2f152d8b300b24dc9e15a91fde4ff0fb26606a42	tree
parent	33b1173361b08919ef9011e335072925d38327df	commit \| diff

ada: Document new SPARK aspect and pragma Always_Terminates

Add description of a recently added SPARK contract.

gcc/ada/

* doc/gnat_rm/implementation_defined_aspects.rst,
doc/gnat_rm/implementation_defined_pragmas.rst: Add sections for
Always_Terminates.
* gnat-style.texi: Regenerate.
* gnat_rm.texi: Regenerate.
* gnat_ugn.texi: Regenerate.

Mirror of https://gcc.gnu.org/git/gcc.git

RSS Atom

gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst		diff \| blob \| blame \| history
gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst		diff \| blob \| blame \| history
gcc/ada/gnat-style.texi		diff \| blob \| blame \| history
gcc/ada/gnat_rm.texi		diff \| blob \| blame \| history
gcc/ada/gnat_ugn.texi		diff \| blob \| blame \| history