Prove System.Image_U, making the connection with the space available in the string as computed with System.Width_U and the functions that support the other direction of 'Value in System.Value_U.
The units that support 'Image cannot be marked Pure anymore, as they now depend on non-pure units. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-imaged.ads: Remove Pure. * libgnat/s-imagef.ads: Remove Pure. * libgnat/s-imager.ads: Remove Pure. * libgnat/s-imageu.adb: Add ghost code. * libgnat/s-imageu.ads: Add contracts. * libgnat/s-imde128.ads: Remove Pure. * libgnat/s-imde32.ads: Remove Pure. * libgnat/s-imde64.ads: Remove Pure. * libgnat/s-imfi128.ads: Remove Pure. * libgnat/s-imfi32.ads: Remove Pure. * libgnat/s-imfi64.ads: Remove Pure. * libgnat/s-imgflt.ads: Remove Pure. * libgnat/s-imglfl.ads: Remove Pure. * libgnat/s-imgllf.ads: Remove Pure. * libgnat/s-imglllu.ads: Instantiate with ghost subprograms. * libgnat/s-imgllu.ads: Instantiate with ghost subprograms. * libgnat/s-imgrea.ads: Remove Pure. * libgnat/s-imguns.ads: Instantiate with ghost subprograms. * libgnat/s-imguti.ads: Remove Pure. * libgnat/s-valueu.adb (Prove_Iter_Scan_Based_Number_Ghost, Prove_Scan_Only_Decimal_Ghost): New lemmas. * libgnat/s-valueu.ads (Uns_Option): Do not make type ghost to be able to use it as formal in instantiations. (Only_Decimal_Ghost): New ghost query. (Prove_Iter_Scan_Based_Number_Ghost, Prove_Scan_Only_Decimal_Ghost): New lemmas. * libgnat/s-widlllu.ads: Adapt to changes in Width_U. * libgnat/s-widllu.ads: Adapt to changes in Width_U. * libgnat/s-widthu.adb: Change generic function in generic package in order to complete the postcondition. Tighten the upper bound on the result by 1. * libgnat/s-widthu.ads: Same. * libgnat/s-widuns.ads: Adapt to changes in Width_U. * gcc-interface/Make-lang.in: Add dependencies on a-nubinu, a-numeri.ads and a-widuns.ads.
patch.diff.gz
Description: application/gzip