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 /gcc/ada/gcc-interface | |
| 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 'gcc/ada/gcc-interface')
| -rw-r--r-- | gcc/ada/gcc-interface/Make-lang.in | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index 9507f2f..7b826f2 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -536,6 +536,8 @@ GNAT_ADA_OBJS+= \ ada/libgnat/s-secsta.o \ ada/libgnat/s-soflin.o \ ada/libgnat/s-soliin.o \ + ada/libgnat/s-spark.o \ + ada/libgnat/s-spcuop.o \ ada/libgnat/s-stache.o \ ada/libgnat/s-stalib.o \ ada/libgnat/s-stoele.o \ |