projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f0b7fdd) | patch
[Ada] Add contracts to System.Address_To_Access_Conversions
authorJoffrey Huguet <huguet@adacore.com>
Mon, 9 May 2022 13:25:30 +0000 (15:25 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Thu, 2 Jun 2022 09:06:37 +0000 (09:06 +0000)
commitf03f48a3843046a4ee888db3b86c0efe3812e2c7
tree006cb320f1a4edcdb6b9f540098a1e67a79e690atree | snapshot
parentf0b7fddbefbe7af7c14ed5f2def49bbdb4a6c919commit | diff
[Ada] Add contracts to System.Address_To_Access_Conversions

This patch adds SPARK annotations to subprograms from
System.Address_To_Access_Conversions. To_Pointer is considered to have
no global items, if the returned value has no aliases. To_Address is
forbidden in SPARK because addresses are not handled.

gcc/ada/

* libgnat/s-atacco.ads (To_Pointer): Add Global => null.
(To_Address): Add SPARK_Mode => Off.
gcc/ada/libgnat/s-atacco.ads diff | blob | history
Domain: System / Toolchain;