diff options
| author | Joffrey Huguet <huguet@adacore.com> | 2022-05-11 17:16:05 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-06-02 09:06:39 +0000 |
| commit | d276374355196abe35e162795da94c112ee13b80 (patch) | |
| tree | 72ab8b2facdf5a40edd6e66ff4884034c0c10e3d | |
| parent | 2689914091d4c552d775338215a95a6fe10945f9 (diff) | |
| download | gcc-d276374355196abe35e162795da94c112ee13b80.zip gcc-d276374355196abe35e162795da94c112ee13b80.tar.gz gcc-d276374355196abe35e162795da94c112ee13b80.tar.bz2 | |
[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.
| -rw-r--r-- | gcc/ada/libgnat/i-cstrin.ads | 11 |
1 files 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; |