diff options
| author | Yannick Moy <moy@adacore.com> | 2022-01-05 14:36:13 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-11 13:24:48 +0000 |
| commit | ee22e1aa71b30a699d051ca9aa65ddf342a2635b (patch) | |
| tree | 0d134e7fd89f6dbd204f5966f1d58abe1bfff989 /gcc/cp | |
| parent | 58a9ed1187e5ba190828dff6c5d1e88ebe7dbb3a (diff) | |
| download | gcc-ee22e1aa71b30a699d051ca9aa65ddf342a2635b.zip gcc-ee22e1aa71b30a699d051ca9aa65ddf342a2635b.tar.gz gcc-ee22e1aa71b30a699d051ca9aa65ddf342a2635b.tar.bz2 | |
[Ada] Adapt proof of System.Arith_Double
gcc/ada/
* libgnat/s-aridou.adb (Double_Divide): Adjust proof of lemma
Prove_Signs, call lemma for commutation of Big and
multiplication.
(Multiply_With_Ovflo_Check): Adjust postcondition of
Prove_Pos_Int.
(Scaled_Divide): Explicit commutation in the proof of lemma
Prove_Multiplication, add new lemma Prove_Shift_Progress for
congruence property that is not proved in a larger context, add
assertions at the end of the loop to state loop invariant
properties.
Diffstat (limited to 'gcc/cp')
0 files changed, 0 insertions, 0 deletions