From: Yannick Moy <moy@adacore.com>
Date: Wed, 18 Jan 2023 10:50:54 +0000 (+0000)
Subject: ada: Add intermediate assertions for proof of Super_Tail
X-Git-Tag: basepoints/gcc-15~9260
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=fd0f8d2486678e401b076b74e9f1ae2cb224ba76;p=thirdparty%2Fgcc.git

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 25a843153f28..c727575ee6bf 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 =>