| commit | f959a78b0d26513cd0802ac1402adc4ebdd4db67 | |
| author | Claire Dross <dross@adacore.com> | |
| Wed, 4 Jan 2023 13:41:30 +0000 (4 14:41 +0100) | ||
| committer | Marc Poulhiès <poulhies@adacore.com> | |
| Mon, 15 May 2023 09:36:41 +0000 (15 11:36 +0200) | ||
| tree | 8c9dcc9f6a54406e2f8fef5b54fd3ffef71122be | treesnapshot (tar.gz zip) |
| parent | c9ed0840840911e3e936f15327acda3f807d7142 | commitdiff |
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.
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.
| gcc/ada/gcc-interface/Make-lang.in | diffblobblamehistory | |
| gcc/ada/libgnat/s-valueu.adb | diffblobblamehistory |