* [Ada] Fix proof of runtime unit System.Value* and System.Image*
@ 2022-09-02 7:53 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-09-02 7:53 UTC (permalink / raw)
To: gcc-patches; +Cc: Claire Dross
[-- Attachment #1: Type: text/plain, Size: 1675 bytes --]
Refactor specification of the Value* and Image* units and fix proofs.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
[-- Attachment #2: patch.diff.gz --]
[-- Type: application/gzip, Size: 25454 bytes --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-09-02 7:53 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-09-02 7:53 [Ada] Fix proof of runtime unit System.Value* and System.Image* Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).