From: Yannick Moy <moy@adacore.com>
Date: Wed, 5 Jan 2022 09:43:25 +0000 (+0100)
Subject: [Ada] Recover proof of Ada.Strings.Fixed with assertions
X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=87f152ba31e41df9225ff08682eca7b8fb66234b;p=test_jj.git

[Ada] Recover proof of Ada.Strings.Fixed with assertions

gcc/ada/

	* libgnat/a-strfix.adb (Insert, Overwrite): Add assertions.
---

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;