Message ID | 20220512124009.GA781082@adacore.com |
---|---|
State | New |
Headers | show |
Series | [Ada] Remove useless pragma Warnings Off from runtime units | expand |
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 --
Hello, Jan-Benedict, On Jun 27, 2022, Jan-Benedict Glaw <jbglaw@lug-owl.de> wrote: > For me, this patch broke building a basic cross compiler using Debian > sid's "gcc-snapshot" package as the build/host compiler Thanks for reporting the problem you've encountered, and for your interest. AFAIK the general recommendation for building GCC is to either bootstrap it, using a native compiler that meets the build documented requirements, or use the same precompiled version of the compiler that you wish to cross-build. IIRC, this latter requirement is particularly important for canadian crosses, but it applies as a general recommendation, and GNAT often takes advantage of that to use features that will be disregarded by stage1 (no optimization, no fatal warnings, limited runtime, etc), but that must be available in later stages and in cross builds, which is easy to satisfy by using the same compiler version, and which is a given when bootstrapping. Of course it isn't always the case that you will run into problems when deviating from these recommendations, so it's perfectly possible that you get lucky building it all using compilers that don't meet the recommendations to get started, but that's counting on luck, not on a reliable procedure. See note Prerequisites in the GCC Installation manual for more details. I hope this helps,
> IIRC, this latter requirement is particularly important for canadian > crosses, but it applies as a general recommendation, and GNAT often > takes advantage of that to use features that will be disregarded by > stage1 (no optimization, no fatal warnings, limited runtime, etc), but > that must be available in later stages and in cross builds, which is > easy to satisfy by using the same compiler version, and which is a given > when bootstrapping. > > Of course it isn't always the case that you will run into problems when > deviating from these recommendations, so it's perfectly possible that > you get lucky building it all using compilers that don't meet the > recommendations to get started, but that's counting on luck, not on a > reliable procedure. > > See note Prerequisites in the GCC Installation manual for more details. Right, see https://gcc.gnu.org/install/prerequisites.html (GNAT section). The only combination that is guaranteed to work is to use the same version for the native compiler to build the cross. The error reported here is one example showing why using another version will not work in general. Arno
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 with System.Val_Util; use System.Val_Util; diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads --- a/gcc/ada/libgnat/s-valueu.ads +++ b/gcc/ada/libgnat/s-valueu.ads @@ -43,8 +43,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 with System.Val_Util; use System.Val_Util; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -41,8 +41,6 @@ pragma Assertion_Policy (Pre => Ignore, Post => Ignore, Contract_Cases => Ignore, Ghost => Ignore); -pragma Warnings (Off, "postcondition does not mention function result"); --- True postconditions are used to avoid inlining for GNATprove with System.Case_Util;