From: Joffrey Huguet <huguet@adacore.com>
Date: Wed, 11 May 2022 15:16:05 +0000 (+0200)
Subject: [Ada] Complete contracts of Interfaces.C.Strings subprograms
X-Git-Tag: basepoints/gcc-14~6271
X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=d276374355196abe35e162795da94c112ee13b80;p=thirdparty%2Fgcc.git

[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.
---

diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads
index 62ef9df383d..faad7a0b73b 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;