diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 9da7b7b8aa99f82d8cbea9be670fba5607c41bbb..414df24d4048e6e7e8500351b1241c00dc86f700 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -1190,7 +1190,17 @@ decl_spec_wo_type: /* ISO 6.7 */ decl_spec_list: | decl_spec_wo_type decl_spec_list_opt { fst $1 :: $2, snd $1 } -| type_spec decl_spec_list_opt_no_named { SpecType(fst $1) :: $2, snd $1 } +| type_spec pragma* (* pragma accepted by GCC *) decl_spec_list_opt_no_named + { + let pragmas = $2 in + if pragmas != [] then begin + let loc = Cabshelper.get_definitionloc (List.hd pragmas) in + Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_pragma + ~once:true ~source:(fst loc) + "Discarding _Pragma's in function declaration" + end; + SpecType(fst $1) :: $3, snd $1 + } decl_spec_list_no_named: | decl_spec_wo_type decl_spec_list_opt_no_named { fst $1 :: $2, snd $1 } diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 86bb74a82b3a7b84659215afdda5a8e5b1c2b8f3..d4fff3d5b98449f14cd15cbd8ed2581f013ee6ba 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -223,6 +223,8 @@ let wkey_parser_unsupported = register_warn_category "parser:unsupported" let wkey_parser_unsupported_attributes = register_warn_category "parser:unsupported:attributes" +let wkey_parser_unsupported_pragma = register_warn_category "parser:unsupported:pragma" + let wkey_asm = register_warn_category "asm:clobber" let wkey_unnamed_typedef = register_warn_category "parser:unnamed-typedef" diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index 940ff68224fd6a3bc668c24f323072a3619a25fe..13e35743a12a0bde3dc27e575bdf4e1bcd98023d 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -220,6 +220,9 @@ val wkey_parser_unsupported: warn_category val wkey_parser_unsupported_attributes: warn_category (** Warning related to unsupported attributes during parsing. *) +val wkey_parser_unsupported_pragma: warn_category +(** Warning related to unsupported _Pragma's during parsing. *) + val wkey_asm: warn_category (** Warnings related to assembly code. *) diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json index da80b2ca65374be357e44b1ca62fea739281239a..0307758ad6290a6a5ea7f4fc5d4105fd2618319b 100644 --- a/tests/misc/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -62,8 +62,9 @@ "linker:drop-conflicting-unused", "linker:weak", "parser", "parser:conditional-feature", "parser:unnamed-typedef", "parser:unsupported", "parser:unsupported:attributes", - "plugin-not-loaded", "pp", "pp:compilation-db", "pp:line-directive", - "too-large-array", "typing", "typing:implicit-conv-void-ptr", + "parser:unsupported:pragma", "plugin-not-loaded", "pp", + "pp:compilation-db", "pp:line-directive", "too-large-array", + "typing", "typing:implicit-conv-void-ptr", "typing:implicit-function-declaration", "typing:incompatible-pointer-types", "typing:incompatible-types-call", "typing:inconsistent-specifier", diff --git a/tests/syntax/oracle/pragma_operator.res.oracle b/tests/syntax/oracle/pragma_operator.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..9dfdd735b25ebcceb8138f41029610684be50937 --- /dev/null +++ b/tests/syntax/oracle/pragma_operator.res.oracle @@ -0,0 +1,30 @@ +[kernel] Parsing pragma_operator.c (with preprocessing) +[kernel:parser:unsupported:pragma] pragma_operator.c:3: Warning: + Discarding _Pragma's in function declaration +[kernel:parser:unsupported:pragma] pragma_operator.c:7: Warning: + Discarding _Pragma's in function declaration +[kernel:parser:unsupported:pragma] pragma_operator.c:9: Warning: + Discarding _Pragma's in function declaration +[kernel:parser:unsupported:pragma] pragma_operator.c:12: Warning: + Discarding _Pragma's in function declaration +/* Generated by Frama-C */ +int main(void) +{ + int __retres; + __retres = 0; + return __retres; +} + +void main2(void); + +void main2(void) +{ + return; +} + +void main3(void) +{ + return; +} + + diff --git a/tests/syntax/pragma_operator.c b/tests/syntax/pragma_operator.c new file mode 100644 index 0000000000000000000000000000000000000000..93742b107c99f5113c3a70fcc47b26a67dd812ed --- /dev/null +++ b/tests/syntax/pragma_operator.c @@ -0,0 +1,13 @@ +// The pragma below is allowed by GCC (14), but only on a .c file. +// Clang (18) also accepts it on a .i file. +int _Pragma("entrypoint") main( void) { + return 0; +} + +void _Pragma("entrypoint") main2(); + +void _Pragma("entrypoint") main2() { +} + +void _Pragma("entrypoint") _Pragma("another pragma") _Pragma("") main3() { +}