]> git.ipfire.org Git - thirdparty/gcc.git/commit
[Ada] Fix proof of runtime unit s-imageu
authorClaire Dross <dross@adacore.com>
Mon, 11 Apr 2022 12:10:49 +0000 (14:10 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 18 May 2022 08:41:09 +0000 (08:41 +0000)
commit9f068ad0f2f1d65349ac564178cddbe9aec39f3a
treea9604e535ed8bae11c31398f2f6fe275ad624236
parent17cd8bf5a4204b56c337614c0c0752527409f993
[Ada] Fix proof of runtime unit s-imageu

Update to provers caused some proof regressions.  Fix the proof by
adding an assertion.

gcc/ada/

* libgnat/s-imageu.adb (Set_Image_Unsigned): Change assertion.
gcc/ada/libgnat/s-imageu.adb