[gcc r12-6460] [Ada] Recover proof of Ada.Strings.Fixed with assertions

[gcc r12-6460] [Ada] Recover proof of Ada.Strings.Fixed with assertions

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:87f152ba31e41df9225ff08682eca7b8fb66234b

commit r12-6460-g87f152ba31e41df9225ff08682eca7b8fb66234b
Author: Yannick Moy <moy@adacore.com>
Date:   Wed Jan 5 10:43:25 2022 +0100

    [Ada] Recover proof of Ada.Strings.Fixed with assertions
    
    gcc/ada/
    
            * libgnat/a-strfix.adb (Insert, Overwrite): Add assertions.

Diff:
---
 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 255738a229b..74752543024 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;