diff options
| author | Claire Dross <dross@adacore.com> | 2023-01-04 14:41:30 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-15 11:36:41 +0200 |
| commit | f959a78b0d26513cd0802ac1402adc4ebdd4db67 (patch) | |
| tree | 8c9dcc9f6a54406e2f8fef5b54fd3ffef71122be /libgcc | |
| parent | c9ed0840840911e3e936f15327acda3f807d7142 (diff) | |
| download | gcc-f959a78b0d26513cd0802ac1402adc4ebdd4db67.zip gcc-f959a78b0d26513cd0802ac1402adc4ebdd4db67.tar.gz gcc-f959a78b0d26513cd0802ac1402adc4ebdd4db67.tar.bz2 | |
ada: Fix proof of runtime unit System.Value*
Use cut operations to restore the proof of System.Value*.
gcc/ada/
* libgnat/s-valueu.adb: Use cut operations inside assertion to
restore proofs
* gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Add s-spark and
s-spcuop dependencies.
Diffstat (limited to 'libgcc')
0 files changed, 0 insertions, 0 deletions