diff options
| author | Yannick Moy <moy@adacore.com> | 2022-02-04 15:20:20 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-12 12:38:36 +0000 |
| commit | 91d68769419b64ef9843c4c1eac5261217693b1e (patch) | |
| tree | 5b71311910b10b848c80e12e11fbe68d7d5e1cc6 /gcc/ada/libgnat/s-imagef.ads | |
| parent | a4f6f9f1769ab691d28da4579c61c13d5d1c2bda (diff) | |
| download | gcc-91d68769419b64ef9843c4c1eac5261217693b1e.zip gcc-91d68769419b64ef9843c4c1eac5261217693b1e.tar.gz gcc-91d68769419b64ef9843c4c1eac5261217693b1e.tar.bz2 | |
[Ada] Proof of 'Image support for signed integers
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.
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.
Diffstat (limited to 'gcc/ada/libgnat/s-imagef.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-imagef.ads | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/s-imagef.ads b/gcc/ada/libgnat/s-imagef.ads index c16d2c5..13ea22f 100644 --- a/gcc/ada/libgnat/s-imagef.ads +++ b/gcc/ada/libgnat/s-imagef.ads @@ -36,6 +36,7 @@ generic type Int is range <>; + type Uns is mod <>; with procedure Scaled_Divide (X, Y, Z : Int; |