diff options
| author | Yannick Moy <moy@adacore.com> | 2023-01-23 17:09:40 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-16 10:30:58 +0200 |
| commit | 8ebdd4431829c61228ec92f906cb9f7a2141325f (patch) | |
| tree | 78ce2d490bd043318ff355a2f4ff8666612be803 /libgcc/udivmod.c | |
| parent | bac7eb85ef0caca4e55b362f688776dbea14feb9 (diff) | |
| download | gcc-8ebdd4431829c61228ec92f906cb9f7a2141325f.tar.gz | |
ada: Update proof of runtime units
Following changes in GNATprove, proofs need to be amended.
gcc/ada/
* libgnat/s-aridou.adb (Lemma_Div_Pow2): Add assertion.
* libgnat/s-arit32.adb (Lemma_Abs_Div_Commutation): Simplify.
* libgnat/s-expmod.adb (Lemma_Exp_Mod): Add assertions.
(Lemma_Euclidean_Mod): Add body to lemma.
(Lemma_Mult_Mod): Add assertion.
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Modify assertion.
* libgnat/s-vauspe.ads (Raw_Unsigned_Last_Ghost): Add
postcondition.
* libgnat/s-widthi.adb: Use more precise types.
Diffstat (limited to 'libgcc/udivmod.c')
0 files changed, 0 insertions, 0 deletions