From 993bb69300888129675d90425d2d6deeec8845cc Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 1 Oct 2021 17:02:15 +0200
Subject: [PATCH] [Kernel] add wkey for assembly warnings
---
src/kernel_internals/typing/asm_contracts.ml | 2 +-
src/kernel_services/plugin_entry_points/kernel.ml | 2 ++
src/kernel_services/plugin_entry_points/kernel.mli | 3 +++
tests/misc/oracle/audit-out.json | 2 +-
tests/syntax/oracle/gnu-asm-aesni.res.oracle | 2 +-
5 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 9de8a8b51ff..a37810a3b3f 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 dffe3cb4b69..a3f6205f58a 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 8a935ac016f..52136e1a395 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 50dc8171330..f12c5aae66e 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 009db9d96ab..ce6233fb1cc 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"
--
GitLab