* [Ada] Update proofs of double arithmetic unit after prover changes
@ 2022-05-30 8:32 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-30 8:32 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 699 bytes --]
Changes in GNATprove (translation to Why3 and provers) result in proofs
being much less automatic, and requiring ghost code to detail
intermediate steps. In some cases, it is better to use the new By
mechanism to prove assertions in steps, as this avoids polluting the
proof context for other proofs. For that reason, add units s-spark.ads
and s-spcuop.ads/b to the runtime sources.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* Makefile.rtl: Add new units.
* libgnat/s-aridou.adb (Scaled_Divide): Add ghost code for provers.
* libgnat/s-spcuop.adb: New unit for ghost cut operations.
* libgnat/s-spcuop.ads: New unit for ghost cut operations.
* libgnat/s-spark.ads: New unit.
[-- Attachment #2: patch.diff.gz --]
[-- Type: application/gzip, Size: 5099 bytes --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-30 8:32 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-30 8:32 [Ada] Update proofs of double arithmetic unit after prover changes Pierre-Marie de Rodat
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).