diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-06-01 14:40:30 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-06-01 14:40:30 +0200 |
| commit | 9eccbd39710aab5d6bfe021c57f50a1916d37f70 (patch) | |
| tree | c35b886a25269892e896dcb7494e624a5944c639 /cparser | |
| parent | 39710f78062a4a999c079b58181a58e62b78c30b (diff) | |
| download | compcert-kvx-9eccbd39710aab5d6bfe021c57f50a1916d37f70.tar.gz compcert-kvx-9eccbd39710aab5d6bfe021c57f50a1916d37f70.zip | |
Support `# 0 ...` preprocessed line directive
Before, the line number had to start with a nonzero digit. However,
the GCC 11 preprocessor was observed to produce `# 0 ...` directives.
Fixes: #398
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Lexer.mll | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 94e490ca..42980d30 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -393,7 +393,7 @@ and string_literal startp accu = parse (* We assume gcc -E syntax but try to tolerate variations. *) and hash = parse | whitespace_char_no_newline + - (decimal_constant as n) + (digit + as n) whitespace_char_no_newline * "\"" ([^ '\n' '\"']* as file) "\"" [^ '\n']* '\n' |