diff options
| author | Yannick Moy <moy@adacore.com> | 2021-11-30 11:43:40 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-05 11:32:36 +0000 |
| commit | bfcc4dd71b5e17488c85a42db86aef433ac712fd (patch) | |
| tree | 16efe02c8e8ef41b4fb9c77412c4fbe92e79fea5 /gcc/ada/sem_ch3.adb | |
| parent | 7c58372ad22f94d21b15ae2f2838e761b36b3486 (diff) | |
| download | gcc-bfcc4dd71b5e17488c85a42db86aef433ac712fd.zip gcc-bfcc4dd71b5e17488c85a42db86aef433ac712fd.tar.gz gcc-bfcc4dd71b5e17488c85a42db86aef433ac712fd.tar.bz2 | |
[Ada] Add contracts for the proof of System.Arith_128
gcc/ada/
* libgnat/s-arit128.adb: Mark in SPARK.
* libgnat/s-arit128.ads: Add functional contracts.
Diffstat (limited to 'gcc/ada/sem_ch3.adb')
0 files changed, 0 insertions, 0 deletions