ada: Add intermediate assertions for proof of Super_Tail

Proof of Superbounded internal unit requires a little more help.

gcc/ada/

	* libgnat/a-strsup.adb: Add intermediate assertions.

diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index 25a843153f28390a8542ce3f5cf93af3ccafa0fb..c727575ee6bffd64ec2deb49b86fd4ff7737b13f 100644 (file)
--- a/gcc/ada/libgnat/a-strsup.adb
+++ b/gcc/ada/libgnat/a-strsup.adb
@@ -1788,6 +1788,12 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
                   Source.Data (1 .. Npad) := [others => Pad];
                   Source.Data (Npad + 1 .. Max_Length) :=
                     Temp (1 .. Max_Length - Npad);
+
+                  pragma Assert
+                    (Source.Data (1 .. Npad) = [1 .. Npad => Pad]);
+                  pragma Assert
+                    (Source.Data (Npad + 1 .. Max_Length)
+                     = Temp (1 .. Max_Length - Npad));
                end if;
 
             when Strings.Left =>