diff options
| author | Yannick Moy <moy@adacore.com> | 2023-01-17 08:06:54 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-16 10:30:55 +0200 |
| commit | c850b1a7dcd13a3f1c288b5334188ba7406c2141 (patch) | |
| tree | cb26155c58a904fd78e8531d6b0f620431055980 /gcc/ada/usage.adb | |
| parent | fa1c2ec1bb5e6363839dce55421cdc6c3dd19726 (diff) | |
| download | gcc-c850b1a7dcd13a3f1c288b5334188ba7406c2141.zip gcc-c850b1a7dcd13a3f1c288b5334188ba7406c2141.tar.gz gcc-c850b1a7dcd13a3f1c288b5334188ba7406c2141.tar.bz2 | |
ada: Restore proof of System.Arith_Double
Use Assert_And_Cut to simplify proof of second part of the Scaled_Divide.
Add intermediate assertions and simplify where necessary.
gcc/ada/
* libgnat/s-aridou.adb:
(Big3): Remove override made useless.
(Lemma_Quot_Rem): Add new lemma and justify it, as no prover
manages to prove it.
(Lemma_Div_Pow2): Use new lemma Lemma_Quot_Rem.
(Prove_Scaled_Mult_Decomposition_Regroup3): Retype for
simplification.
(Scaled_Divide): Remove useless assertions.Decompose some
assertions with cut operations. Use Assert_And_Cut for second
half. Add assertions.
Diffstat (limited to 'gcc/ada/usage.adb')
0 files changed, 0 insertions, 0 deletions