[Ada] Remove useless pragma Warnings Off from runtime units

  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.
  

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