diff options
| author | Yannick Moy <moy@adacore.com> | 2023-06-28 13:56:26 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-07-10 14:41:38 +0200 |
| commit | 4a58185d67029f866577a551888cabf2ac71d9b8 (patch) | |
| tree | 7f75db04a50c4f4e604ca1ad2855f8b5a0ca6ab2 /libgcc/floatunsixf.c | |
| parent | 92eeb32df4f134e96265631511b6b26609aa9c12 (diff) | |
| download | gcc-4a58185d67029f866577a551888cabf2ac71d9b8.zip gcc-4a58185d67029f866577a551888cabf2ac71d9b8.tar.gz gcc-4a58185d67029f866577a551888cabf2ac71d9b8.tar.bz2 | |
ada: Adapt proof of System.Arith_Double to remove CVC4
The proof of System.Arith_Double still required the use of
CVC4, now replaced by its successor cvc5. Adapt the proof to be
able to remove CVC4 in the proof of run-time units.
gcc/ada/
* libgnat/s-aridou.adb (Lemma_Div_Mult): New simple lemma.
(Lemma_Powers_Of_2_Commutation): State post in else branch.
(Lemma_Div_Pow2): Introduce local lemma and use it.
(Scaled_Divide): Use cut operations in assertions, lemmas, new
assertions. Introduce local lemma and use it.
Diffstat (limited to 'libgcc/floatunsixf.c')
0 files changed, 0 insertions, 0 deletions