From 87f152ba31e41df9225ff08682eca7b8fb66234b Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 5 Jan 2022 10:43:25 +0100 Subject: [PATCH] [Ada] Recover proof of Ada.Strings.Fixed with assertions gcc/ada/ * libgnat/a-strfix.adb (Insert, Overwrite): Add assertions. --- gcc/ada/libgnat/a-strfix.adb | 16 +++++++++++++--- 1 file 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; -- 2.7.4