]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a58f70c) | patch
[Ada] Adapt proof of System.Arith_Double after update of Z3
authorYannick Moy <moy@adacore.com>
Wed, 2 Feb 2022 11:52:36 +0000 (12:52 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 11 May 2022 08:53:20 +0000 (08:53 +0000)
commit4c533da21d6298cdf9eb11df7353b8c8684c7756
tree0cba4d9c9160c50c696a2fdd16edc525479e8babtree | snapshot
parenta58f70c30c4900bb9024681e0b86e85d96cac2e7commit | diff
[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.
gcc/ada/libgnat/s-aridou.adb diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git