diff options
| author | Yannick Moy <moy@adacore.com> | 2022-07-07 09:38:42 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-07-13 10:01:16 +0000 |
| commit | 4709037646e9b0aa66815f86ebf98a97eb663186 (patch) | |
| tree | aa5b3e1e87aec40d1510c396f8da617a77a30ac5 /gcc/ada/gcc-interface/utils.cc | |
| parent | d03a7f8c247d73258b80891c79358b745c379992 (diff) | |
| download | gcc-4709037646e9b0aa66815f86ebf98a97eb663186.zip gcc-4709037646e9b0aa66815f86ebf98a97eb663186.tar.gz gcc-4709037646e9b0aa66815f86ebf98a97eb663186.tar.bz2 | |
[Ada] Fix proof of runtime unit System.Arith_64
After changes in provers and Why3, changes are needed to recover
automatic proof of System.Arith_64. This is the first part of it.
gcc/ada/
* libgnat/s-aridou.adb (Lemma_Mult_Div, Lemma_Powers): New
lemmas.
(Prove_Sign_Quotient): New local lemma.
(Prove_Signs): Expand definition of Big_R and Big_Q in the
postcondition. Add intermediate assertions.
(Double_Divide): Call new lemma.
(Lemma_Div_Eq): Provide body for proving lemma.
(Lemma_Powers_Of_2, Lemma_Shift_Without_Drop,
Prove_Dividend_Scaling, Prove_Multiplication, Prove_Z_Low): Call
lemmas, add intermediate assertions.
Diffstat (limited to 'gcc/ada/gcc-interface/utils.cc')
0 files changed, 0 insertions, 0 deletions