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/gcc-interface | |
| 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/gcc-interface')
| -rw-r--r-- | gcc/ada/gcc-interface/Make-lang.in | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index a8d8899..1e245ed 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -486,6 +486,8 @@ GNAT_ADA_OBJS+= \ ada/libgnat/a-except.o \ ada/libgnat/a-exctra.o \ ada/libgnat/a-ioexce.o \ + ada/libgnat/a-nubinu.o \ + ada/libgnat/a-numeri.o \ ada/libgnat/ada.o \ ada/libgnat/g-byorma.o \ ada/libgnat/g-heasor.o \ @@ -542,7 +544,8 @@ GNAT_ADA_OBJS+= \ ada/libgnat/s-wchcnv.o \ ada/libgnat/s-wchcon.o \ ada/libgnat/s-wchjis.o \ - ada/libgnat/s-wchstw.o + ada/libgnat/s-wchstw.o \ + ada/libgnat/s-widuns.o endif # Object files for gnat executables @@ -649,6 +652,8 @@ GNATBIND_OBJS += \ ada/libgnat/a-assert.o \ ada/libgnat/a-elchha.o \ ada/libgnat/a-except.o \ + ada/libgnat/a-nubinu.o \ + ada/libgnat/a-numeri.o \ ada/libgnat/ada.o \ ada/libgnat/g-byorma.o \ ada/libgnat/g-hesora.o \ @@ -693,6 +698,7 @@ GNATBIND_OBJS += \ ada/libgnat/s-wchcon.o \ ada/libgnat/s-wchjis.o \ ada/libgnat/s-wchstw.o \ + ada/libgnat/s-widuns.o \ ada/adaint.o \ ada/argv.o \ ada/cio.o \ |