diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 655659d92b813eec05a9f09a624742febffaf6be..06d74aa1d67bc6ffca2692da322921dea0aa1d41 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -9777,8 +9777,8 @@ and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit = end else cabsPushGlobal (GEnumTagDecl(ei, CurrentLoc.get ())) | _ -> - Kernel.warning ~current:true - "Ignoring un-named typedef that does not introduce a struct or \ + Kernel.warning ~current:true ~wkey:Kernel.wkey_unnamed_typedef + "Ignoring unnamed typedef that does not introduce a struct or \ enumeration type" (* Now define the processors for body and statement *) diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index b713f0d331de2ed0bdb7315bc3071648e796ea5b..aafb804260788eb70d7f49e9e0f580f34feecb50 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -203,6 +203,8 @@ let wkey_parser_unsupported = register_warn_category "parser:unsupported" let wkey_asm = register_warn_category "asm:clobber" +let wkey_unnamed_typedef = register_warn_category "parser:unnamed-typedef" + (* ************************************************************************* *) (** {2 Specialised functors for building kernel parameters} *) (* ************************************************************************* *) diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index 5ea5fde2a77a23624c29bec4db21a10be00d4975..e0508fe996e284bcd40a660d1c9fdcd310d83201 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -197,6 +197,10 @@ val wkey_parser_unsupported: warn_category val wkey_asm: warn_category (** Warnings related to assembly code. *) +val wkey_unnamed_typedef: warn_category +(** Warning related to "unnamed typedef that does not introduce a struct + or enumeration type". *) + (* ************************************************************************* *) (** {2 Functors for late option registration} *) (** Kernel_function-related options cannot be registered in this module: diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json index cacd9f1deac9573453ddd26f1d5a2b18c478aebb..338cb7e071363126f729b393b9339543daaa0fe8 100644 --- a/tests/misc/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -57,8 +57,9 @@ "annot:multi-from", "annot-error", "asm", "asm:clobber", "audit", "check", "check:volatile", "cmdline", "ghost", "ghost:bad-use", "inline", "linker", "linker:drop-conflicting-unused", "parser", - "parser:conditional-feature", "parser:unsupported", "pp", - "pp:compilation-db", "typing", "typing:implicit-conv-void-ptr", + "parser:conditional-feature", "parser:unnamed-typedef", + "parser:unsupported", "pp", "pp:compilation-db", "typing", + "typing:implicit-conv-void-ptr", "typing:implicit-function-declaration", "typing:incompatible-pointer-types", "typing:incompatible-types-call", "typing:inconsistent-specifier",