gcc.gnu.org Git - gcc.git/commit

]> gcc.gnu.org Git - gcc.git/commit

author	Yannick Moy <moy@adacore.com>
	Tue, 16 May 2023 13:16:13 +0000 (13:16 +0000)
committer	Marc Poulhiès <poulhies@adacore.com>
	Tue, 20 Jun 2023 07:30:48 +0000 (09:30 +0200)
commit	adc853f0661dcb4d1204d1a89ed49446ec01a980
tree	a0497b4b1ae1c4e058377272da6658c86f026cdf	tree
parent	ca27b8a030746d09ea61de62e1f3bc1337ebe737	commit \| diff

ada: Update annotations in runtime for proof

With bump of stable SPARK used for proof of the runtime,
some annotations need to change.

gcc/ada/

* libgnat/s-aridou.adb (Scaled_Divide): Add assertions.
* libgnat/s-valuti.adb: Add Loop_Variant.
* libgnat/s-valuti.ads: Add Exceptional_Cases on No_Return
procedure.

gcc/ada/libgnat/s-aridou.adb		diff \| blob \| blame \| history
gcc/ada/libgnat/s-valuti.adb		diff \| blob \| blame \| history
gcc/ada/libgnat/s-valuti.ads		diff \| blob \| blame \| history

GNU Compiler Collection

RSS Atom

This page took 0.070462 seconds and 6 git commands to generate.