From f03f48a3843046a4ee888db3b86c0efe3812e2c7 Mon Sep 17 00:00:00 2001 From: Joffrey Huguet Date: Mon, 9 May 2022 15:25:30 +0200 Subject: [PATCH] [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 | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/gcc/ada/libgnat/s-atacco.ads b/gcc/ada/libgnat/s-atacco.ads index 736210dc98b..b3559ffed79 100644 --- a/gcc/ada/libgnat/s-atacco.ads +++ b/gcc/ada/libgnat/s-atacco.ads @@ -54,8 +54,10 @@ package System.Address_To_Access_Conversions is -- optimizations that may cause unexpected results based on the assumption -- of no strict aliasing. - function To_Pointer (Value : Address) return Object_Pointer; - function To_Address (Value : Object_Pointer) return Address; + function To_Pointer (Value : Address) return Object_Pointer with + Global => null; + function To_Address (Value : Object_Pointer) return Address with + SPARK_Mode => Off; pragma Import (Intrinsic, To_Pointer); pragma Import (Intrinsic, To_Address); -- 2.47.2