Hi!
On Thu, 2022-05-12 12:40:09 +0000, Pierre-Marie de Rodat via Gcc-patches <gcc-patches@gcc.gnu.org> wrote: > GNAT does not issue a warning anymore on a postcondition of True (used > here to prevent inining inside GNATprove for proof). > > Tested on x86_64-pc-linux-gnu, committed on trunk > > gcc/ada/ > > * libgnat/s-valuei.ads: Remove pragma Warnings Off. > * libgnat/s-valueu.ads: Same. > * libgnat/s-valuti.ads: Same. > diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads > --- a/gcc/ada/libgnat/s-valuei.ads > +++ b/gcc/ada/libgnat/s-valuei.ads > @@ -37,8 +37,6 @@ pragma Assertion_Policy (Pre => Ignore, > Contract_Cases => Ignore, > Ghost => Ignore, > Subprogram_Variant => Ignore); > -pragma Warnings (Off, "postcondition does not mention function result"); > --- True postconditions are used to avoid inlining for GNATprove For me, this patch broke building a basic cross compiler using Debian sid's "gcc-snapshot" package as the build/host compiler: ../gcc/configure '--with-pkgversion=basepoints/gcc-13-1183-g70454c50b45, built at 1655800680' --prefix=/var/lib/laminar/run/gcc-vax-linux/5/toolchain-install --enable-werror-always --enable-languages=all --disable-gcov --disable-shared --disable-threads --target=vax-linux --without-headers [...] make V=1 all-gcc [...] /usr/lib/gcc-snapshot/bin/gcc -c -g -O2 -gnatpg -gnata -W -Wall -nostdinc -I- -I. -Iada/generated -Iada -I../../gcc/gcc/ada -Iada/libgnat -I../../gcc/gcc/ada/libgnat -Iada/gcc-interface -I../../gcc/gcc/ada/gcc-interface ../../gcc/gcc/ada/libgnat/s-valint.adb -o ada/libgnat/s-valint.o mkdir -p ada/libgnat/ /usr/lib/gcc-snapshot/bin/gcc -c -g -O2 -gnatpg -gnata -W -Wall -nostdinc -I- -I. -Iada/generated -Iada -I../../gcc/gcc/ada -Iada/libgnat -I../../gcc/gcc/ada/libgnat -Iada/gcc-interface -I../../gcc/gcc/ada/gcc-interface ../../gcc/gcc/ada/libgnat/s-valuns.adb -o ada/libgnat/s-valuns.o mkdir -p ada/libgnat/ /usr/lib/gcc-snapshot/bin/gcc -c -g -O2 -gnatpg -gnata -W -Wall -nostdinc -I- -I. -Iada/generated -Iada -I../../gcc/gcc/ada -Iada/libgnat -I../../gcc/gcc/ada/libgnat -Iada/gcc-interface -I../../gcc/gcc/ada/gcc-interface ../../gcc/gcc/ada/libgnat/s-valuti.adb -o ada/libgnat/s-valuti.o s-valuti.ads:63:06: warning: postcondition does not mention function result [-gnatw.t] make[1]: *** [../../gcc/gcc/ada/gcc-interface/Make-lang.in:167: ada/libgnat/s-valuti.o] Error 1 make[1]: Leaving directory '/var/lib/laminar/run/gcc-vax-linux/5/toolchain-build/gcc' make: *** [Makefile:4615: all-gcc] Error 2 I'm not an Ada developer, just keeping an eye on GCC and doing automated builds. Looking at the patch it seems that switching off the "postcondition does not mention function result" warning was done under the impression that only a _very_ new GCC is used and my "gcc-snapshot" package is too old to already contain the fixes submitted in the patches before this pragma removal. If that's correct, that boils down to a specific minimum version to build with, or adding back the pragmas to allow a bootstrap with an older compiler version. Thanks, Jan-Benedict --
signature.asc
Description: PGP signature
