]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3752997) | patch
ada: Update ghost code for proof of integer input functions
authorClaire Dross <dross@adacore.com>
Mon, 27 Feb 2023 10:51:45 +0000 (10:51 +0000)
committerMarc Poulhiès <poulhies@adacore.com>
Tue, 23 May 2023 07:59:06 +0000 (09:59 +0200)
commitf0593467b5c3c915cfe710821b503afcc076a036
tree549c37ffe851c69b65db7c6441b8312cb3f69289tree
parent375299752727a8b3d5a360905fade38122d82681commit | diff
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.
gcc/ada/libgnat/s-valueu.adb diff | blob | blame | history
gcc/ada/libgnat/s-vauspe.ads diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git