From d276374355196abe35e162795da94c112ee13b80 Mon Sep 17 00:00:00 2001
From: Joffrey Huguet <huguet@adacore.com>
Date: Wed, 11 May 2022 17:16:05 +0200
Subject: [PATCH] [Ada] Complete contracts of Interfaces.C.Strings subprograms

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

gcc/ada/

	* libgnat/i-cstrin.ads (Update): Add precondition.
---
 gcc/ada/libgnat/i-cstrin.ads | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads
index 62ef9df..faad7a0 100644
--- 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;
-- 
2.7.4