Skip to content
Snippets Groups Projects
Commit 993bb693 authored by Andre Maroneze's avatar Andre Maroneze Committed by Virgile Prevosto
Browse files

[Kernel] add wkey for assembly warnings

parent 4bba8bc0
No related branches found
No related tags found
No related merge requests found
...@@ -143,7 +143,7 @@ class visit_assembly = ...@@ -143,7 +143,7 @@ class visit_assembly =
let source = fst (Cil_datatype.Instr.loc i) in let source = fst (Cil_datatype.Instr.loc i) in
let once = true in let once = true in
Kernel.warning Kernel.warning
~once ~source ~once ~source ~wkey:Kernel.wkey_asm
"Clobber list contains \"memory\" argument. Assuming no \ "Clobber list contains \"memory\" argument. Assuming no \
side effects beyond those mentioned in operands." side effects beyond those mentioned in operands."
end; end;
......
...@@ -201,6 +201,8 @@ let () = set_warn_status wkey_audit Log.Werror ...@@ -201,6 +201,8 @@ let () = set_warn_status wkey_audit Log.Werror
let wkey_parser_unsupported = register_warn_category "parser:unsupported" let wkey_parser_unsupported = register_warn_category "parser:unsupported"
let wkey_asm = register_warn_category "assembly"
(* ************************************************************************* *) (* ************************************************************************* *)
(** {2 Specialised functors for building kernel parameters} *) (** {2 Specialised functors for building kernel parameters} *)
(* ************************************************************************* *) (* ************************************************************************* *)
......
...@@ -194,6 +194,9 @@ val wkey_audit: warn_category ...@@ -194,6 +194,9 @@ val wkey_audit: warn_category
val wkey_parser_unsupported: warn_category val wkey_parser_unsupported: warn_category
(** Warning related to unsupported parsing-related features. *) (** Warning related to unsupported parsing-related features. *)
val wkey_asm: warn_category
(** Warnings related to assembly code. *)
(* ************************************************************************* *) (* ************************************************************************* *)
(** {2 Functors for late option registration} *) (** {2 Functors for late option registration} *)
(** Kernel_function-related options cannot be registered in this module: (** Kernel_function-related options cannot be registered in this module:
......
...@@ -54,7 +54,7 @@ ...@@ -54,7 +54,7 @@
"enabled": [ "enabled": [
"*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:37", "*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:37",
"CERT:MSC:38", "acsl-extension", "annot", "annot:missing-spec", "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", "check:volatile", "cmdline", "ghost", "ghost:bad-use", "inline",
"linker", "linker:drop-conflicting-unused", "parser", "linker", "linker:drop-conflicting-unused", "parser",
"parser:conditional-feature", "parser:unsupported", "pp", "parser:conditional-feature", "parser:unsupported", "pp",
......
[kernel] Parsing tests/syntax/gnu-asm-aesni.c (with preprocessing) [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. Clobber list contains "memory" argument. Assuming no side effects beyond those mentioned in operands.
/* Generated by Frama-C */ /* Generated by Frama-C */
#include "__fc_builtin.h" #include "__fc_builtin.h"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment