diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml index 9de8a8b51ffe830ec161e0ea64b3fe7c44c11652..a37810a3b3f5299ae30d6ad60ae49e071f30f5d6 100644 --- a/src/kernel_internals/typing/asm_contracts.ml +++ b/src/kernel_internals/typing/asm_contracts.ml @@ -143,7 +143,7 @@ class visit_assembly = let source = fst (Cil_datatype.Instr.loc i) in let once = true in Kernel.warning - ~once ~source + ~once ~source ~wkey:Kernel.wkey_asm "Clobber list contains \"memory\" argument. Assuming no \ side effects beyond those mentioned in operands." end; diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index dffe3cb4b69a0ed8e36137e4767117a5dd8c574e..a3f6205f58a601039b48491bbd43fb266504baa4 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -201,6 +201,8 @@ let () = set_warn_status wkey_audit Log.Werror let wkey_parser_unsupported = register_warn_category "parser:unsupported" +let wkey_asm = register_warn_category "assembly" + (* ************************************************************************* *) (** {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 8a935ac016f350fb82646c09f6c36fda4f53def3..52136e1a3953501b2698f3332a0b36c0f53f6b00 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -194,6 +194,9 @@ val wkey_audit: warn_category val wkey_parser_unsupported: warn_category (** Warning related to unsupported parsing-related features. *) +val wkey_asm: warn_category +(** Warnings related to assembly code. *) + (* ************************************************************************* *) (** {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 50dc81713305db352d3360952a9447313a6433cf..f12c5aae66e195c626524671d97d05842fc440bf 100644 --- a/tests/misc/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -54,7 +54,7 @@ "enabled": [ "*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:37", "CERT:MSC:38", "acsl-extension", "annot", "annot:missing-spec", - "annot:multi-from", "annot-error", "audit", "check", + "annot:multi-from", "annot-error", "assembly", "audit", "check", "check:volatile", "cmdline", "ghost", "ghost:bad-use", "inline", "linker", "linker:drop-conflicting-unused", "parser", "parser:conditional-feature", "parser:unsupported", "pp", diff --git a/tests/syntax/oracle/gnu-asm-aesni.res.oracle b/tests/syntax/oracle/gnu-asm-aesni.res.oracle index 009db9d96ab42af2b72897a78f16ec0ba3ebadab..ce6233fb1cc0eb63f194fe12f9ec8e11a633bd65 100644 --- a/tests/syntax/oracle/gnu-asm-aesni.res.oracle +++ b/tests/syntax/oracle/gnu-asm-aesni.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/syntax/gnu-asm-aesni.c (with preprocessing) -[kernel] tests/syntax/gnu-asm-aesni.c:93: Warning: +[kernel:assembly] tests/syntax/gnu-asm-aesni.c:93: Warning: Clobber list contains "memory" argument. Assuming no side effects beyond those mentioned in operands. /* Generated by Frama-C */ #include "__fc_builtin.h"