]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 66643a9) | patch
[Ada] Recover proof of Scaled_Divide in System.Arith_64
authorYannick Moy <moy@adacore.com>
Mon, 11 Jul 2022 15:00:46 +0000 (15:00 +0000)
committerMarc Poulhiès <poulhies@adacore.com>
Fri, 2 Sep 2022 07:34:06 +0000 (09:34 +0200)
commit7c339b3b5a63bac5e5223e33cce4c9833153edbb
tree1ee1568c1a5589695d0d6dbab3e38b587c753938tree
parent66643a9fe96e66914f074bee84d1fc30915afcb5commit | diff
[Ada] Recover proof of Scaled_Divide in System.Arith_64

Proof of Scaled_Divide was impacted by changes in provers and Why3.
Recover it partially, leaving some unproved basic inferences to be
further investigated.

gcc/ada/

* libgnat/s-aridou.adb: Add or rework ghost code.
* libgnat/s-aridou.ads: Add Big_Positive subtype.
gcc/ada/libgnat/s-aridou.adb diff | blob | blame | history
gcc/ada/libgnat/s-aridou.ads diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git