projects / test_jj.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 544b30f) | patch
[Ada] Proof of System.Arith_32 for double arithmetic on 32bits
authorYannick Moy <moy@adacore.com>
Thu, 25 Nov 2021 14:35:39 +0000 (15:35 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Thu, 2 Dec 2021 16:26:30 +0000 (16:26 +0000)
commitb5e57389c511b645ce66581ab5aba5dff7ea831b
treec64180704b81efb4638ab3331f8a6fe8ff86039ctree | snapshot
parent544b30f81e53ee636aac905be63cc1ed0de88119commit | diff
[Ada] Proof of System.Arith_32 for double arithmetic on 32bits

gcc/ada/

* libgnat/s-arit32.adb: Add ghost instances and lemmas.
(Scaled_Divide32): Add ghost code to prove. Minor code
modification to return early in error when divisor is zero.
* libgnat/s-arit32.ads: Add ghost instances and utilities.
(Scaled_Divide32): Add contract.
gcc/ada/libgnat/s-arit32.adb diff | blob | history
gcc/ada/libgnat/s-arit32.ads diff | blob | history