diff options
| author | Claire Dross <dross@adacore.com> | 2023-02-27 10:51:45 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-23 09:59:06 +0200 |
| commit | f0593467b5c3c915cfe710821b503afcc076a036 (patch) | |
| tree | 549c37ffe851c69b65db7c6441b8312cb3f69289 /gcc/ada/libgnarl | |
| parent | 375299752727a8b3d5a360905fade38122d82681 (diff) | |
| download | gcc-f0593467b5c3c915cfe710821b503afcc076a036.zip gcc-f0593467b5c3c915cfe710821b503afcc076a036.tar.gz gcc-f0593467b5c3c915cfe710821b503afcc076a036.tar.bz2 | |
ada: Update ghost code for proof of integer input functions
Introduce new ghost helper functions to facilitate proof.
gcc/ada/
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Use new helpers.
* libgnat/s-vauspe.ads (Raw_Unsigned_Starts_As_Based_Ghost,
Raw_Unsigned_Is_Based_Ghost): New ghost helper functions.
(Is_Raw_Unsigned_Format_Ghost, Scan_Split_No_Overflow_Ghost,
Scan_Split_Value_Ghost, Raw_Unsigned_Last_Ghost): Use new
helpers.
Diffstat (limited to 'gcc/ada/libgnarl')
0 files changed, 0 insertions, 0 deletions