From 85e8404061d11c4c8464c85b09bd2fa30fd6a0da Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 7 Dec 2021 16:35:38 +0100
Subject: [PATCH] [Kernel] add wkey for unnamed typedef warning
---
src/kernel_internals/typing/cabs2cil.ml | 4 ++--
src/kernel_services/plugin_entry_points/kernel.ml | 2 ++
src/kernel_services/plugin_entry_points/kernel.mli | 4 ++++
tests/misc/oracle/audit-out.json | 5 +++--
4 files changed, 11 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 655659d92b8..06d74aa1d67 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 b713f0d331d..aafb8042607 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 5ea5fde2a77..e0508fe996e 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 cacd9f1deac..338cb7e0713 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",
--
GitLab