Compilation warnings with GCC>=11

[pierregoutagny]

Compiling with GCC version 11.1.0 produces several pre-processor warnings :
Steps to reproduce, with a minimal example:

1. Install GCC version 11.1.0 and CompCert version 3.9
2. Try to compile a file min.c, containing int main() { return 0; }, with the command ccomp hello.c

The following errors are printed:

min.c:1: warning: unrecognized '#' line
min.c:2: warning: unrecognized '#' line
min.c:3: warning: unrecognized '#' line
/usr/include/stdc-predef.h:1: warning: unrecognized '#' line

I have tried the same steps with GCC version 10.2.0, but the warnings do not appear.

A possible explanation suggested by @monniaux could be the use of null line numbers in linemarkers by GCC 11.
With GCC 11.1.0, the preprocessor produces the following results:

$ gcc -E min.c
# 0 "min.c"
# 0 "<built-in>"
# 0 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
# 0 "<command-line>" 2
# 1 "min.c"
int main() { return 0; }

With GCC 10.2.0:

$ gcc -E min.c
# 1 "min.c"
# 1 "<built-in>"
# 1 "<command-line>"
# 31 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
# 32 "<command-line>" 2
# 1 "min.c"
int main() { return 0; }

[xavierleroy]

Thanks for the report. There was no good reason to restrict line numbers in # NNN ... directives to be nonzero. This should be fixed in commit 9eccbd3 .

[m-schmidt]

The reason for the restriction may have been a confusion of # 0 with the #line directive? The standard (6.10.4p3 if I remember correctly) forbids #line 0 explicitly.