diff options
| author | Yannick Moy <moy@adacore.com> | 2022-01-05 10:43:25 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-11 13:24:48 +0000 |
| commit | 87f152ba31e41df9225ff08682eca7b8fb66234b (patch) | |
| tree | f30179a26a0d47da015c26b35321af090b6e35dc | |
| parent | 7aa3800216ea991050ec904a28c628cd7799021b (diff) | |
| download | gcc-87f152ba31e41df9225ff08682eca7b8fb66234b.zip gcc-87f152ba31e41df9225ff08682eca7b8fb66234b.tar.gz gcc-87f152ba31e41df9225ff08682eca7b8fb66234b.tar.bz2 | |
[Ada] Recover proof of Ada.Strings.Fixed with assertions
gcc/ada/
* libgnat/a-strfix.adb (Insert, Overwrite): Add assertions.
| -rw-r--r-- | gcc/ada/libgnat/a-strfix.adb | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb index 255738a..7475254 100644 --- a/gcc/ada/libgnat/a-strfix.adb +++ b/gcc/ada/libgnat/a-strfix.adb @@ -384,6 +384,10 @@ package body Ada.Strings.Fixed with SPARK_Mode is Source (Source'First .. Before - 1); Result (Front + 1 .. Front + New_Item'Length) := New_Item; + + pragma Assert + (Result (1 .. Before - Source'First) + = Source (Source'First .. Before - 1)); pragma Assert (Result (Before - Source'First + 1 @@ -558,15 +562,21 @@ package body Ada.Strings.Fixed with SPARK_Mode is if Position <= Source'Last - New_Item'Length then Result (Front + New_Item'Length + 1 .. Result'Last) := Source (Position + New_Item'Length .. Source'Last); + + pragma Assert + (Result + (Position - Source'First + New_Item'Length + 1 + .. Result'Last) + = Source (Position + New_Item'Length .. Source'Last)); end if; pragma Assert (if Position <= Source'Last - New_Item'Length then Result - (Position - Source'First + New_Item'Length + 1 - .. Result'Last) - = Source (Position + New_Item'Length .. Source'Last)); + (Position - Source'First + New_Item'Length + 1 + .. Result'Last) + = Source (Position + New_Item'Length .. Source'Last)); end return; end; end Overwrite; |