| commit | bfcc4dd71b5e17488c85a42db86aef433ac712fd | |
| author | Yannick Moy <moy@adacore.com> | |
| Tue, 30 Nov 2021 10:43:40 +0000 (30 11:43 +0100) | ||
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | |
| Wed, 5 Jan 2022 11:32:36 +0000 (5 11:32 +0000) | ||
| tree | 16efe02c8e8ef41b4fb9c77412c4fbe92e79fea5 | treesnapshot (tar.gz zip) |
| parent | 7c58372ad22f94d21b15ae2f2838e761b36b3486 | commitdiff |
[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.
gcc/ada/
* libgnat/s-arit128.adb: Mark in SPARK.
* libgnat/s-arit128.ads: Add functional contracts.
| gcc/ada/libgnat/s-arit128.adb | diffblobblamehistory | |
| gcc/ada/libgnat/s-arit128.ads | diffblobblamehistory |