diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2023-11-29 21:33:30 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-01-09 14:13:29 +0100 |
| commit | bfacdd11d992c47771574470987ae8954a5b12fd (patch) | |
| tree | 2f152d8b300b24dc9e15a91fde4ff0fb26606a42 /gcc/alloc-pool.h | |
| parent | 33b1173361b08919ef9011e335072925d38327df (diff) | |
| download | gcc-bfacdd11d992c47771574470987ae8954a5b12fd.zip gcc-bfacdd11d992c47771574470987ae8954a5b12fd.tar.gz gcc-bfacdd11d992c47771574470987ae8954a5b12fd.tar.bz2 | |
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.
Diffstat (limited to 'gcc/alloc-pool.h')
0 files changed, 0 insertions, 0 deletions