diff options
Diffstat (limited to 'gcc/ada/libgnat/s-valueu.adb')
| -rw-r--r-- | gcc/ada/libgnat/s-valueu.adb | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index f1456a1..461d957 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -590,6 +590,10 @@ package body System.Value_U is if Str (P) = Base_Char then Ptr.all := P + 1; pragma Assert (Ptr.all = Last_Num_Based + 2); + pragma Assert + (if not Overflow then + Based_Val = Scan_Based_Number_Ghost + (Str, P, Last_Num_Based, Base, Uval)); Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval); pragma Assert (if not Overflow then Uval = Based_Val.Value); exit; |