diff options
| author | Joffrey Huguet <huguet@adacore.com> | 2022-05-09 15:25:30 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-06-02 09:06:37 +0000 |
| commit | f03f48a3843046a4ee888db3b86c0efe3812e2c7 (patch) | |
| tree | 006cb320f1a4edcdb6b9f540098a1e67a79e690a /gcc/gcov-tool.cc | |
| parent | f0b7fddbefbe7af7c14ed5f2def49bbdb4a6c919 (diff) | |
| download | gcc-f03f48a3843046a4ee888db3b86c0efe3812e2c7.zip gcc-f03f48a3843046a4ee888db3b86c0efe3812e2c7.tar.gz gcc-f03f48a3843046a4ee888db3b86c0efe3812e2c7.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/gcov-tool.cc')
0 files changed, 0 insertions, 0 deletions