diff options
| author | Yannick Moy <moy@adacore.com> | 2023-05-16 13:16:13 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-20 09:30:48 +0200 |
| commit | adc853f0661dcb4d1204d1a89ed49446ec01a980 (patch) | |
| tree | a0497b4b1ae1c4e058377272da6658c86f026cdf /libcpp | |
| parent | ca27b8a030746d09ea61de62e1f3bc1337ebe737 (diff) | |
| download | gcc-adc853f0661dcb4d1204d1a89ed49446ec01a980.zip gcc-adc853f0661dcb4d1204d1a89ed49446ec01a980.tar.gz gcc-adc853f0661dcb4d1204d1a89ed49446ec01a980.tar.bz2 | |
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.
Diffstat (limited to 'libcpp')
0 files changed, 0 insertions, 0 deletions