diff options
| author | Yannick Moy <moy@adacore.com> | 2021-11-24 17:20:59 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-02 16:26:28 +0000 |
| commit | 3a54dfa801a1cfb387c8c43e7610b11905db505c (patch) | |
| tree | 40a736016981b85ec70ac272c3f4d98f71dc58f0 /gcc/ada/gcc-interface/trans.c | |
| parent | 167be0845e555cf98a59d768002c7f48bf85fe11 (diff) | |
| download | gcc-3a54dfa801a1cfb387c8c43e7610b11905db505c.zip gcc-3a54dfa801a1cfb387c8c43e7610b11905db505c.tar.gz gcc-3a54dfa801a1cfb387c8c43e7610b11905db505c.tar.bz2 | |
[Ada] Proof of support units for 'Width on signed integers
gcc/ada/
* libgnat/s-widint.ads: Mark in SPARK.
* libgnat/s-widlli.ads: Likewise.
* libgnat/s-widllli.ads: Likewise.
* libgnat/s-widlllu.ads: Likewise.
* libgnat/s-widllu.ads: Disable ghost/contract.
* libgnat/s-widthi.adb: Replicate and adapt the proof from
s-widthu.adb.
* libgnat/s-widthi.ads: Add minimal postcondition.
* libgnat/s-widthu.adb: Fix comments in the modular case.
* libgnat/s-widthu.ads: Add minimal postcondition.
* libgnat/s-widuns.ads: Disable ghost/contract.
Diffstat (limited to 'gcc/ada/gcc-interface/trans.c')
0 files changed, 0 insertions, 0 deletions