diff options
author | Claire Dross <dross@adacore.com> | 2022-07-07 16:04:24 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-02 09:34:06 +0200 |
commit | b3ae28dca103a45bb97ec5b47acad9b9380d1113 (patch) | |
tree | 758efad64a9473025b84166258a29c1f229079a6 /gcc/gcc.cc | |
parent | 6713cc703c0914f993891d8ccb8167b29a8855cc (diff) | |
download | gcc-b3ae28dca103a45bb97ec5b47acad9b9380d1113.zip gcc-b3ae28dca103a45bb97ec5b47acad9b9380d1113.tar.gz gcc-b3ae28dca103a45bb97ec5b47acad9b9380d1113.tar.bz2 |
[Ada] Fix proof of runtime unit System.Value* and System.Image*
Refactor specification of the Value* and Image* units and fix proofs.
gcc/ada/
* libgnat/a-nbnbig.ads: Add Always_Return annotation.
* libgnat/s-vaispe.ads: New ghost unit for the specification of
System.Value_I. Restore proofs.
* libgnat/s-vauspe.ads: New ghost unit for the specification of
System.Value_U. Restore proofs.
* libgnat/s-valuei.adb: The specification only subprograms are
moved to System.Value_I_Spec. Restore proofs.
* libgnat/s-valueu.adb: The specification only subprograms are
moved to System.Value_U_Spec. Restore proofs.
* libgnat/s-valuti.ads
(Uns_Params): Generic unit used to bundle together the
specification functions of System.Value_U_Spec.
(Int_Params): Generic unit used to bundle together the
specification functions of System.Value_I_Spec.
* libgnat/s-imagef.adb: It is now possible to instantiate the
appropriate specification units instead of creating imported ghost
subprograms.
* libgnat/s-imagei.adb: Update to refactoring of specifications
and fix proofs.
* libgnat/s-imageu.adb: Likewise.
* libgnat/s-imgint.ads: Ghost parameters are grouped together in a
package now.
* libgnat/s-imglli.ads: Likewise.
* libgnat/s-imgllu.ads: Likewise.
* libgnat/s-imgllli.ads: Likewise.
* libgnat/s-imglllu.ads: Likewise.
* libgnat/s-imguns.ads: Likewise.
* libgnat/s-vallli.ads: Likewise.
* libgnat/s-valllli.ads: Likewise.
* libgnat/s-imagei.ads: Likewise.
* libgnat/s-imageu.ads: Likewise.
* libgnat/s-vaispe.adb: Likewise.
* libgnat/s-valint.ads: Likewise.
* libgnat/s-valuei.ads: Likewise.
* libgnat/s-valueu.ads: Likewise.
* libgnat/s-vauspe.adb: Likewise.
Diffstat (limited to 'gcc/gcc.cc')
0 files changed, 0 insertions, 0 deletions