diff options
| author | Yannick Moy <moy@adacore.com> | 2022-02-10 11:54:44 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-12 12:38:38 +0000 |
| commit | 86c7b1617f0ae0da828d1107795f57c96c848d8f (patch) | |
| tree | b5852ca8d5ede3dcf72b8c94f53b3eba433d885a /gcc/ada/libgnat/system-linux-mips.ads | |
| parent | bbb4320baea245dc5abab35aba7d6225bc9f70fe (diff) | |
| download | gcc-86c7b1617f0ae0da828d1107795f57c96c848d8f.zip gcc-86c7b1617f0ae0da828d1107795f57c96c848d8f.tar.gz gcc-86c7b1617f0ae0da828d1107795f57c96c848d8f.tar.bz2 | |
[Ada] Add ghost code to facilitate proof with SPARK
Proof of generic units for Long_Long_Long_Unsigned instantiations is
harder for provers, as they have to deal with larger values. Add ghost
code to make the proof easier.
gcc/ada/
* libgnat/s-imageu.adb (Set_Image_Unsigned): Add lemma.
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertion.
Diffstat (limited to 'gcc/ada/libgnat/system-linux-mips.ads')
0 files changed, 0 insertions, 0 deletions