diff options
| author | Claire Dross <dross@adacore.com> | 2021-12-15 20:10:06 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-11 13:24:47 +0000 |
| commit | 649b3efae598aaf855b8cc453749695dded9fa95 (patch) | |
| tree | b9315329a73e0dc11072d6346cc5a85cd5f602d2 /gcc/ada/inline.adb | |
| parent | 371b4ad7c423891d13f9b855f5fdd469a82f7160 (diff) | |
| download | gcc-649b3efae598aaf855b8cc453749695dded9fa95.zip gcc-649b3efae598aaf855b8cc453749695dded9fa95.tar.gz gcc-649b3efae598aaf855b8cc453749695dded9fa95.tar.bz2 | |
[Ada] Proof of System.Val_Uns at gold level
gcc/ada/
* libgnat/a-tiinau.ads: Use a procedure for the Scan parameter
instead of a function with side-effects.
* libgnat/a-tiinau.adb: Idem.
* libgnat/a-wtinau.ads: Idem.
* libgnat/a-wtinau.adb: Idem.
* libgnat/a-ztinau.ads: Idem.
* libgnat/a-ztinau.adb: Idem.
* libgnat/s-valint.ads: Change the function with side-effects
Scan_Integer into a procedure
* libgnat/s-vallli.ads: Idem.
* libgnat/s-valllli.ads: Idem.
* libgnat/s-vallllu.ads: Add SPARK_Mode and pragma to ignore
assertions in instance.
* libgnat/s-valllu.ads: Idem.
* libgnat/s-valuns.ads: Idem.
* libgnat/s-valuei.ads: Use a procedure for the
Scan_Raw_Unsigned parameter instead of a function with
side-effects and change the function with side-effects
Scan_Integer into a procedure.
* libgnat/s-valuei.adb: Idem.
* libgnat/s-valuti.ads: Introduce a ghost function that scans an
exponent and complete the postcondition of Scan_Exponent to also
describe the value of Ptr after the call. Fix the postcondition
of Scan_Underscore. Simplify the definition of
Scan_Natural_Ghost.
* libgnat/s-valuti.adb: Idem.
* libgnat/s-valboo.ads, libgnat/s-valboo.adb: Update calls to
First_Non_Space_Ghost.
* libgnat/s-valueu.ads: Add functional contracts.
* libgnat/s-valueu.adb: Idem.
Diffstat (limited to 'gcc/ada/inline.adb')
0 files changed, 0 insertions, 0 deletions