]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d2bc326) | patch
[Ada] Proof of System.Generic_Array_Operations at silver level
authorYannick Moy <moy@adacore.com>
Wed, 8 Dec 2021 14:09:25 +0000 (09:09 -0500)
committerPierre-Marie de Rodat <derodat@adacore.com>
Thu, 6 Jan 2022 17:11:41 +0000 (17:11 +0000)
commit42dd6f60d8fefe1b026989d78eabf0108c528e4b
tree7b686a5d340f20a1b1500b95aa472ec5d4003ce5tree | snapshot
parentd2bc32602c58f14cddc8634fe36141137e2861d1commit | diff
[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.
gcc/ada/libgnat/a-ngcoar.adb diff | blob | blame | history
gcc/ada/libgnat/a-ngrear.adb diff | blob | blame | history
gcc/ada/libgnat/s-gearop.adb diff | blob | blame | history
gcc/ada/libgnat/s-gearop.ads diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git