Re: [Ada] Remove useless pragma Warnings Off from runtime units

[Jan-Benedict Glaw <jbglaw@lug-owl.de>]

[-- Attachment #1: Type: text/plain, Size: 3283 bytes --]

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

-- 

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 195 bytes --]