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 --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads
index 220a38be68f65c48bed3127567834a8022e81e93..30ca0b3081a560b6bbe1384e7558602b94fb23b5 100644 (file)
--- 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