diff options
| author | Joffrey Huguet <huguet@adacore.com> | 2023-12-06 12:04:51 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-01-09 14:13:30 +0100 |
| commit | c1ebec34788353bf126a1df1c75e1ee2110c8795 (patch) | |
| tree | 1150188659b6e33be37ae28ee8e40c0ff9f67c12 | |
| parent | e3da93d988c0bb5da0eb4f6cdb75a63983ea2b33 (diff) | |
| download | gcc-c1ebec34788353bf126a1df1c75e1ee2110c8795.zip gcc-c1ebec34788353bf126a1df1c75e1ee2110c8795.tar.gz gcc-c1ebec34788353bf126a1df1c75e1ee2110c8795.tar.bz2 | |
ada: Fix precondition in Interfaces.C.Strings
The precondition of both Update procedures in Interfaces.C.Strings were
incorrect. This patch fixes this.
gcc/ada/
* libgnat/i-cstrin.ads (Update): Fix precondition.
| -rw-r--r-- | gcc/ada/libgnat/i-cstrin.ads | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads index 9f1577f..3f55ddf 100644 --- a/gcc/ada/libgnat/i-cstrin.ads +++ b/gcc/ada/libgnat/i-cstrin.ads @@ -121,8 +121,9 @@ is with Pre => Item /= Null_Ptr - and then Strlen (Item) <= size_t'Last - Offset - and then Strlen (Item) + Offset <= Chars'Length, + and then (Chars'First /= 0 or else Chars'Last /= size_t'Last) + and then Chars'Length <= size_t'Last - Offset + and then Chars'Length + Offset <= Strlen (Item), Global => (In_Out => C_Memory); procedure Update @@ -133,8 +134,8 @@ is with Pre => Item /= Null_Ptr - and then Strlen (Item) <= size_t'Last - Offset - and then Strlen (Item) + Offset <= Str'Length, + and then Str'Length <= size_t'Last - Offset + and then Str'Length + Offset <= Strlen (Item), Global => (In_Out => C_Memory); Update_Error : exception; |