[Ada] Complete contracts of Interfaces.C.Strings subprograms

[Ada] Complete contracts of Interfaces.C.Strings subprograms

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 208 bytes --]

This patch adds preconditions to Update procedures, to protect from
Update_Error propagations.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/i-cstrin.ads (Update): Add precondition.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1186 bytes --]

diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads
--- a/gcc/ada/libgnat/i-cstrin.ads
+++ b/gcc/ada/libgnat/i-cstrin.ads
@@ -36,7 +36,8 @@
 --  Preconditions in this unit are meant for analysis only, not for run-time
 --  checking, so that the expected exceptions are raised. This is enforced by
 --  setting the corresponding assertion policy to Ignore. These preconditions
---  do not protect against Storage_Error.
+--  protect from Dereference_Error and Update_Error, but not from
+--  Storage_Error.
 
 pragma Assertion_Policy (Pre => Ignore);
 
@@ -117,7 +118,9 @@ is
       Chars  : char_array;
       Check  : Boolean := True)
    with
-     Pre    => Item /= Null_Ptr,
+     Pre    =>
+       Item /= Null_Ptr
+         and then (if Check then Offset <= Strlen (Item) - Chars'Length),
      Global => (In_Out => C_Memory);
 
    procedure Update
@@ -126,7 +129,9 @@ is
       Str    : String;
       Check  : Boolean := True)
    with
-     Pre    => Item /= Null_Ptr,
+     Pre    =>
+       Item /= Null_Ptr
+         and then (if Check then Offset <= Strlen (Item) - Str'Length),
      Global => (In_Out => C_Memory);
 
    Update_Error : exception;