diff options
| author | Yannick Moy <moy@adacore.com> | 2023-01-18 10:50:54 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-16 10:30:56 +0200 |
| commit | fd0f8d2486678e401b076b74e9f1ae2cb224ba76 (patch) | |
| tree | a691795bd9cdc91557a686b20a8b1e226e0bfa1a /gcc/ada | |
| parent | 24917325cef92b535f909facdbe1d40c8f1f602a (diff) | |
| download | gcc-fd0f8d2486678e401b076b74e9f1ae2cb224ba76.zip gcc-fd0f8d2486678e401b076b74e9f1ae2cb224ba76.tar.gz gcc-fd0f8d2486678e401b076b74e9f1ae2cb224ba76.tar.bz2 | |
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.
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/libgnat/a-strsup.adb | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb index 25a8431..c727575 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 => |