[COMMITTED] ada: Add intermediate assertions for proof of Super_Tail

[Marc Poulhiès via Gcc-patches]

From: Yannick Moy <m...@adacore.com>

Proof of Superbounded internal unit requires a little more help.

gcc/ada/

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

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-strsup.adb | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index 25a843153f2..c727575ee6b 100644
--- 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 =>
-- 
2.40.0