diff options
| author | Yannick Moy <moy@adacore.com> | 2022-02-02 12:52:36 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-11 08:53:20 +0000 |
| commit | 4c533da21d6298cdf9eb11df7353b8c8684c7756 (patch) | |
| tree | 0cba4d9c9160c50c696a2fdd16edc525479e8bab /gcc/ada/gcc-interface | |
| parent | a58f70c30c4900bb9024681e0b86e85d96cac2e7 (diff) | |
| download | gcc-4c533da21d6298cdf9eb11df7353b8c8684c7756.zip gcc-4c533da21d6298cdf9eb11df7353b8c8684c7756.tar.gz gcc-4c533da21d6298cdf9eb11df7353b8c8684c7756.tar.bz2 | |
[Ada] Adapt proof of System.Arith_Double after update of Z3
Update to version 4.8.14 of prover Z3 requires minor adjustments of the
ghost code to add necessary intermediate assertions that drive the
automatic proof.
gcc/ada/
* libgnat/s-aridou.adb (Double_Divide, Scaled_Divide): Add
intermediate assertions.
Diffstat (limited to 'gcc/ada/gcc-interface')
0 files changed, 0 insertions, 0 deletions