diff options
| author | Yannick Moy <moy@adacore.com> | 2023-01-16 10:55:08 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-15 11:36:43 +0200 |
| commit | a398b5479c9c928f7d9999de8b0c6580b733e6a8 (patch) | |
| tree | ec9ebb5ba8a8db3dc01a4b6cd7bb21a40a7597d3 /libgcc | |
| parent | 75fb45f0692270efa1a89590e0d7dd0688101e8b (diff) | |
| download | gcc-a398b5479c9c928f7d9999de8b0c6580b733e6a8.zip gcc-a398b5479c9c928f7d9999de8b0c6580b733e6a8.tar.gz gcc-a398b5479c9c928f7d9999de8b0c6580b733e6a8.tar.bz2 | |
ada: Recover proof of runtime units
Changes needed to make proof go through, after some change in
GNAT and SPARK.
gcc/ada/
* libgnat/a-strsup.adb (Super_Slice): Reorder component assignment
to avoid failing predicate check related to initialization.
* libgnat/s-expmod.adb (Exp_Modular): Add intermediate assertion.
Diffstat (limited to 'libgcc')
0 files changed, 0 insertions, 0 deletions