diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-03 16:01:20 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-07 08:57:22 +0100 |
| commit | 35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5 (patch) | |
| tree | c89a0466e9ab0c68baa7d4d41e21549b0c02ef88 /cparser | |
| parent | aba0e740f25ffa5c338dfa76cab71144802cebc2 (diff) | |
| download | compcert-kvx-35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5.tar.gz compcert-kvx-35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5.zip | |
Ignore and warn about pragmas inside functions
Pragmas can occur either outside external declarations, at the top level
of a compilation unit, or within a compound statement, inside a function
definition.
The parse tree in cparse/C.mli cannot represent pragmas occuring within
a compound statement.
In this case, the elaborator used to silently move the pragma to top
level, just before the function definition where the pragma occurs.
It looks safer to just ignore pragmas occurring inside a function
definition, and emit a specific warning.
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index bb9f8aca..2e02275c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2871,7 +2871,10 @@ let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) (* pragma *) | PRAGMA(s, loc) -> - emit_elab env loc (Gpragma s); + if local then + warning loc Unknown_pragmas "pragmas are ignored inside functions" + else + emit_elab env loc (Gpragma s); ([], env) (* static assertion *) |