Prove System.Image_I, similarly to the proof done for System.Image_U. The contracts make the connection between the result of Image_Integer, the available space computed with System.Width_U and the result of 'Value as computed by Value_Integer.
I/O units that now depend on non-pure units are also marked not Pure
anymore.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-imagef.adb: Adapt to new signature of Image_I, by
providing ghost imported subprograms. For now, no contract is
used on these subprograms, as System.Image_F is not proved.
* libgnat/s-imagef.ads: Add modular type Uns as formal
parameter, to use in defining Int_Params for instantiating
Image_I.
* libgnat/s-imagei.adb: Add contracts and ghost code.
* libgnat/s-imagei.ads: Replace Int formal parameter by package
Int_Params, which bundles type Int and Uns with ghost
subprograms. Add contracts.
* libgnat/s-imfi128.ads: Adapt to new formal of Image_F.
* libgnat/s-imfi32.ads: Adapt to new formal of Image_F.
* libgnat/s-imfi64.ads: Adapt to new formal of Image_F.
* libgnat/s-imgint.ads: Adapt to new formals of Image_I.
* libgnat/s-imglli.ads: Adapt to new formals of Image_I.
* libgnat/s-imgllli.ads: Adapt to new formals of Image_I.
* libgnat/s-valint.ads: Adapt to new formals of Value_I.
* libgnat/s-vallli.ads: Adapt to new formals of Value_I.
* libgnat/s-valllli.ads: Adapt to new formals of Value_I.
* libgnat/s-valuei.adb (Prove_Scan_Only_Decimal_Ghost): New
ghost lemma.
* libgnat/s-valuei.ads: New formal parameters to prove the new
lemma.
* libgnat/s-valuti.ads (Int_Params): Define a generic package to
be used as a trait-like formal parameter in Image_I and other
generics that need to instantiate Image_I.
* libgnat/s-widthu.ads (Big_10): Qualify the 10 literal.
patch.diff.gz
Description: application/gzip
