diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index acab6245091876b01d6013a235a8bbeb7b616c95..a023f02eea1f8f38c1b441d860f4e07316d39d0e 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -929,7 +929,7 @@ else_part: { let loc = Cil_datatype.Location.of_lexing_loc $sloc in Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use ~source:(fst loc) - "Invalid ghost else ignored@." ; + "Invalid ghost else ignored" ; in_block $5 } @@ -1296,9 +1296,27 @@ enumerator: let loc = Cil_datatype.Location.of_lexing_loc $sloc in ($1, { expr_node = NOTHING; expr_loc = loc }, loc) } +| IDENT just_attributes { + let attrs = $2 in + let loc = Cil_datatype.Location.of_lexing_loc $sloc in + Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes + ~source:(fst loc) + "Discarding attributes in enumerator (unsupported feature): %a" + Cprint.print_attributes attrs; + ($1, { expr_node = NOTHING; expr_loc = loc }, loc) + } | IDENT EQ expression { ($1, $3, Cil_datatype.Location.of_lexing_loc $sloc) } +| IDENT just_attributes EQ expression { + let attrs = $2 in + let loc = Cil_datatype.Location.of_lexing_loc $sloc in + Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes + ~source:(fst loc) + "Discarding attributes in enumerator (unsupported feature): %a" + Cprint.print_attributes attrs; + ($1, $4, loc) + } ; diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 5b11f4352b8c6e6a627218fb2afcb033c5cb2283..2cb8ce7036c7ed6070986cfa77a41c82064e7e7e 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -212,6 +212,8 @@ let () = set_warn_status wkey_audit Log.Werror let wkey_parser_unsupported = register_warn_category "parser:unsupported" +let wkey_parser_unsupported_attributes = register_warn_category "parser:unsupported:attributes" + 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 d9142b7318f091c656957404f1f90ad56b0ecedd..21bc5342c779a0b5452235e65f16ec4ec46cadfa 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -205,6 +205,9 @@ val wkey_audit: warn_category val wkey_parser_unsupported: warn_category (** Warning related to unsupported parsing-related features. *) +val wkey_parser_unsupported_attributes: warn_category +(** Warning related to unsupported attributes 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 b80ff7dde480bdca61583ab08da82fa153e10286..00cf86ae56d1b4d20a9fb14008edb85e659e4024 100644 --- a/tests/misc/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -61,8 +61,9 @@ "ghost:bad-use", "inline", "linker", "linker:drop-conflicting-unused", "linker:weak", "parser", "parser:conditional-feature", "parser:unnamed-typedef", - "parser:unsupported", "pp", "pp:compilation-db", "pp:line-directive", - "typing", "typing:implicit-conv-void-ptr", + "parser:unsupported", "parser:unsupported:attributes", "pp", + "pp:compilation-db", "pp:line-directive", "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/enum-attr-init.i b/tests/syntax/enum-attr-init.i new file mode 100644 index 0000000000000000000000000000000000000000..ada94efeba0c08e06920ebd8e087bbc9b0f09a86 --- /dev/null +++ b/tests/syntax/enum-attr-init.i @@ -0,0 +1,10 @@ +//excerpt based on glib's gregex.h +typedef enum { + G_REGEX_BSR_ANYCRLF = 1 << 23, + G_REGEX_JAVASCRIPT_COMPAT __attribute__((deprecated)) = 1 << 25 +} GRegexCompileFlags; + +enum enum2 { + FALSE __attribute__((false)), + TRUE __attribute__((true)) +}; diff --git a/tests/syntax/oracle/enum-attr-init.res.oracle b/tests/syntax/oracle/enum-attr-init.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..b74990576c2790c37f19b44e5685df85f51c8f42 --- /dev/null +++ b/tests/syntax/oracle/enum-attr-init.res.oracle @@ -0,0 +1,12 @@ +[kernel] Parsing enum-attr-init.i (no preprocessing) +[kernel:parser:unsupported:attributes] enum-attr-init.i:4: Warning: + Discarding attributes in enumerator (unsupported feature): + __attribute__((deprecated)) +[kernel:parser:unsupported:attributes] enum-attr-init.i:8: Warning: + Discarding attributes in enumerator (unsupported feature): + __attribute__((false)) +[kernel:parser:unsupported:attributes] enum-attr-init.i:9: Warning: + Discarding attributes in enumerator (unsupported feature): + __attribute__((true)) +/* Generated by Frama-C */ +