Message ID | 20220518084331.GA3391399@adacore.com |
---|---|
State | New |
Headers | show |
Series | [Ada] Fix proof of runtime unit s-imageu | expand |
diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb --- a/gcc/ada/libgnat/s-imageu.adb +++ b/gcc/ada/libgnat/s-imageu.adb @@ -390,16 +390,9 @@ package body System.Image_U is Acc => Value) = Wrap_Option (V)); end loop; + pragma Assert (Value = 0); Prove_Unchanged; - pragma Assert - (Scan_Based_Number_Ghost - (Str => S, - From => P + 1, - To => P + Nb_Digits, - Base => 10, - Acc => Value) - = Wrap_Option (V)); P := P + Nb_Digits; end Set_Image_Unsigned;