https://gcc.gnu.org/g:a2374961f076842a458af3e9013b4dbb807ed983
commit r17-935-ga2374961f076842a458af3e9013b4dbb807ed983 Author: Claire Dross <[email protected]> Date: Wed Mar 11 17:56:51 2026 +0100 ada: Add volatile abstract state to creation functions in Interfaces.C.Strings The additional volatile abstract state is necessary to model the value of the new pointer. gcc/ada/ChangeLog: * libgnat/i-cstrin.ads: New C_Addresses volatile state to use as input of the New_String and New_Char_Array. Diff: --- gcc/ada/libgnat/i-cstrin.ads | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads index 220a38be68f6..30ca0b3081a5 100644 --- a/gcc/ada/libgnat/i-cstrin.ads +++ b/gcc/ada/libgnat/i-cstrin.ads @@ -47,7 +47,7 @@ pragma Assertion_Policy (Pre => Ignore); package Interfaces.C.Strings with SPARK_Mode => On, - Abstract_State => (C_Memory), + Abstract_State => (C_Memory, (C_Addresses with Synchronous)), Initializes => (C_Memory), Always_Terminates is @@ -81,13 +81,13 @@ is function New_Char_Array (Chars : char_array) return chars_ptr with Volatile_Function, Post => New_Char_Array'Result /= Null_Ptr, - Global => (Input => C_Memory); + Global => (Input => (C_Memory, C_Addresses)); -- Copy the contents of Chars into a newly allocated chars_ptr function New_String (Str : String) return chars_ptr with Volatile_Function, Post => New_String'Result /= Null_Ptr, - Global => (Input => C_Memory); + Global => (Input => (C_Memory, C_Addresses)); -- Copy the contents of Str into a newly allocated chars_ptr procedure Free (Item : in out chars_ptr) with
