]> gcc.gnu.org Git - gcc.git/commit
git://gcc.gnu.org / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75fb45f) | patch
ada: Recover proof of runtime units
authorYannick Moy <moy@adacore.com>
Mon, 16 Jan 2023 10:55:08 +0000 (10:55 +0000)
committerMarc Poulhiès <poulhies@adacore.com>
Mon, 15 May 2023 09:36:43 +0000 (11:36 +0200)
commita398b5479c9c928f7d9999de8b0c6580b733e6a8
treeec9ebb5ba8a8db3dc01a4b6cd7bb21a40a7597d3tree
parent75fb45f0692270efa1a89590e0d7dd0688101e8bcommit | diff
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.
gcc/ada/libgnat/a-strsup.adb diff | blob | blame | history
gcc/ada/libgnat/s-expmod.adb diff | blob | blame | history
GNU Compiler Collection
This page took 0.066826 seconds and 5 git commands to generate.