diff options
| author | Claire Dross <dross@adacore.com> | 2022-04-08 16:38:47 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-18 08:41:08 +0000 |
| commit | 6f8f9d1bcf55187cb81ef7b0ef1e23db1bc0d440 (patch) | |
| tree | 75d9b79de26a1a27e49d3742285dd37d480c14d3 /gcc/fortran/trans-openmp.cc | |
| parent | df4451ca663e251e5524ebedb34bbe0cbfc45e52 (diff) | |
| download | gcc-6f8f9d1bcf55187cb81ef7b0ef1e23db1bc0d440.zip gcc-6f8f9d1bcf55187cb81ef7b0ef1e23db1bc0d440.tar.gz gcc-6f8f9d1bcf55187cb81ef7b0ef1e23db1bc0d440.tar.bz2 | |
[Ada] Fix proof of runtime unit s-valeu
Update to provers caused some proof regressions. Fix the proof by
changing ghost code.
gcc/ada/
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertions.
Diffstat (limited to 'gcc/fortran/trans-openmp.cc')
0 files changed, 0 insertions, 0 deletions