diff options
| author | Yannick Moy <moy@adacore.com> | 2021-11-25 15:35:39 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-02 16:26:30 +0000 |
| commit | b5e57389c511b645ce66581ab5aba5dff7ea831b (patch) | |
| tree | c64180704b81efb4638ab3331f8a6fe8ff86039c /gcc/ada/gcc-interface/decl.c | |
| parent | 544b30f81e53ee636aac905be63cc1ed0de88119 (diff) | |
| download | gcc-b5e57389c511b645ce66581ab5aba5dff7ea831b.zip gcc-b5e57389c511b645ce66581ab5aba5dff7ea831b.tar.gz gcc-b5e57389c511b645ce66581ab5aba5dff7ea831b.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/gcc-interface/decl.c')
0 files changed, 0 insertions, 0 deletions