diff options
| author | Claire Dross <dross@adacore.com> | 2022-01-20 09:15:28 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-10 08:19:23 +0000 |
| commit | 336ea8f2d6ef528db37212ac7517330274a4793a (patch) | |
| tree | 656606babf94e468a1c8070ced70ea2ccb1c1960 /gcc/fold-const.cc | |
| parent | 7f8053225de072fed9c4822e589c853a6f5e47c4 (diff) | |
| download | gcc-336ea8f2d6ef528db37212ac7517330274a4793a.zip gcc-336ea8f2d6ef528db37212ac7517330274a4793a.tar.gz gcc-336ea8f2d6ef528db37212ac7517330274a4793a.tar.bz2 | |
[Ada] Proof of System.Val_Int at gold level
gcc/ada/
* libgnat/s-valint.ads: Add SPARK_Mode and pragma to ignore
assertions in instance and add additional ghost parameters to
the instance of Value_I.
* libgnat/s-vallli.ads: Idem.
* libgnat/s-valllli.ads: Idem.
* libgnat/s-valuei.ads, libgnat/s-valuei.adb: New generic
parameters for ghost functions from System.Valueu. Add
functional contracts.
Diffstat (limited to 'gcc/fold-const.cc')
0 files changed, 0 insertions, 0 deletions