diff mbox series

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

Message ID 20220111133224.GA748817@adacore.com
State Committed
Commit 87f152ba31e41df9225ff08682eca7b8fb66234b
Headers
Series [Ada] Recover proof of Ada.Strings.Fixed with assertions |

Commit Message

Pierre-Marie de Rodat Jan. 11, 2022, 1:32 p.m. UTC 
  Changes in GNATprove make it necessary to add assertions here.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

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

Patch

diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb
--- 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;