diff options
| author | Yannick Moy <moy@adacore.com> | 2021-12-08 09:09:25 -0500 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-06 17:11:41 +0000 |
| commit | 42dd6f60d8fefe1b026989d78eabf0108c528e4b (patch) | |
| tree | 7b686a5d340f20a1b1500b95aa472ec5d4003ce5 /gcc/go | |
| parent | d2bc32602c58f14cddc8634fe36141137e2861d1 (diff) | |
| download | gcc-42dd6f60d8fefe1b026989d78eabf0108c528e4b.zip gcc-42dd6f60d8fefe1b026989d78eabf0108c528e4b.tar.gz gcc-42dd6f60d8fefe1b026989d78eabf0108c528e4b.tar.bz2 | |
[Ada] Proof of System.Generic_Array_Operations at silver level
gcc/ada/
* libgnat/a-ngcoar.adb: Add pragma to ignore assertions in
instance.
* libgnat/a-ngrear.adb: Likewise.
* libgnat/s-gearop.adb: Prove implementation is free of runtime
errors.
* libgnat/s-gearop.ads: Add contracts to protect against runtime
errors in the generic part.
Diffstat (limited to 'gcc/go')
0 files changed, 0 insertions, 0 deletions