diff options
| author | Yannick Moy <moy@adacore.com> | 2022-02-01 12:33:54 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-11 08:53:22 +0000 |
| commit | b0fd3e3120e83bcd783d5c2443bade7cef20814a (patch) | |
| tree | df06a6aebedbae5b9613493b22eaa40f96d48d60 /gcc/ada/libgnat/s-imagef.ads | |
| parent | 48a2e84929bba9aa60497c39c18c332ebfbd256e (diff) | |
| download | gcc-b0fd3e3120e83bcd783d5c2443bade7cef20814a.zip gcc-b0fd3e3120e83bcd783d5c2443bade7cef20814a.tar.gz gcc-b0fd3e3120e83bcd783d5c2443bade7cef20814a.tar.bz2 | |
[Ada] Proof of 'Image support for unsigned integers
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.
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.
Diffstat (limited to 'gcc/ada/libgnat/s-imagef.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-imagef.ads | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/s-imagef.ads b/gcc/ada/libgnat/s-imagef.ads index 67892b1..c16d2c5 100644 --- a/gcc/ada/libgnat/s-imagef.ads +++ b/gcc/ada/libgnat/s-imagef.ads @@ -43,7 +43,6 @@ generic Round : Boolean); package System.Image_F is - pragma Pure; procedure Image_Fixed (V : Int; |