diff options
| author | Yannick Moy <moy@adacore.com> | 2022-04-19 15:46:05 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-30 08:29:02 +0000 |
| commit | 40e01041b3593c72f3d52013953fbfbe0011abb8 (patch) | |
| tree | 783be6a33b2d7a363219000b4a326e179021faf2 /gcc/ada/makeusg.adb | |
| parent | 33dec214f0270ac86c445e08c32843b73e44fb23 (diff) | |
[Ada] Update proofs of double arithmetic unit after prover changes
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.
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.
Diffstat (limited to 'gcc/ada/makeusg.adb')
0 files changed, 0 insertions, 0 deletions