diff mbox series

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

Message ID 20230516083940.1500958-1-poulhies@adacore.com
State Accepted
Headers
Series [COMMITTED] ada: Add intermediate assertions for proof of Super_Tail |

Checks

Context Check Description
snail/gcc-patch-check success Github commit url

Commit Message

Marc Poulhiès May 16, 2023, 8:39 a.m. UTC 
  From: Yannick Moy <moy@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 mbox series

Patch

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 =>