From 35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 3 Jan 2021 16:01:20 +0100 Subject: 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. --- cparser/Elab.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'cparser') 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 *) -- cgit