diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 64bd16cb8239e8272bed82fc0653977951537875..f7612dbb21ef6af07e5cfd3ce7080b3e507ce3dc 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9447,7 +9447,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
if !currentFunctionFDEC.svar.vname = "main" then
[],res
else begin
- Kernel.warning ~current:true
+ Kernel.warning ~current:true ~wkey:Kernel.wkey_cert_msc_37
"Body of function %s falls-through. \
Adding a return statement"
!currentFunctionFDEC.svar.vname;
@@ -9459,7 +9459,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
to get there anyway. *)
let null_ptr = makeCastT (zero ~loc) intType (TPtr(rt,[])) in
let res = Some (new_exp ~loc (Lval (mkMem null_ptr NoOffset))) in
- Kernel.warning ~current:true
+ Kernel.warning ~current:true ~wkey:Kernel.wkey_cert_msc_37
"Body of function %s falls-through. \
Adding a return statement"
!currentFunctionFDEC.svar.vname;
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index e21274bd4b33a08bc8ebb31782b30d56a9ebff6d..8b30799b24b82fa49b74dde6e385e750b5dc3191 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -167,6 +167,8 @@ let wkey_int_conversion =
let wkey_cert_exp_46 = register_warn_category "CERT:EXP:46"
+let wkey_cert_msc_37 = register_warn_category "CERT:MSC:37"
+
let wkey_cert_msc_38 = register_warn_category "CERT:MSC:38"
let () = set_warn_status wkey_cert_msc_38 Log.Werror
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index a6e7e409bca45d77489b1e2576724809180c2e6e..c971c83111ff2b386bab8668ef9e98ac605a40e2 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -163,6 +163,8 @@ val wkey_int_conversion: warn_category
val wkey_cert_exp_46: warn_category
+val wkey_cert_msc_37: warn_category
+
val wkey_cert_msc_38: warn_category
val wkey_cert_exp_10: warn_category
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index f660536e9e236ec1f877a8c608b7a719be8e96c5..234959f116a6401da5586a53f15da7d2bf6d312d 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp/stmtcompiler_test.i (no preprocessing)
-[kernel] tests/wp/stmtcompiler_test.i:136: Warning:
+[kernel:CERT:MSC:37] tests/wp/stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
[kernel] tests/wp/stmtcompiler_test.i:145: Warning:
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index 6e1e0c0d7c30baad20ca78800a4bacd2573751f7..26586447d5764c7e3c4c02dc6b7959ab4ddc592c 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp/stmtcompiler_test.i (no preprocessing)
-[kernel] tests/wp/stmtcompiler_test.i:136: Warning:
+[kernel:CERT:MSC:37] tests/wp/stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
[kernel] tests/wp/stmtcompiler_test.i:145: Warning:
diff --git a/tests/cil/oracle/bts297.res.oracle b/tests/cil/oracle/bts297.res.oracle
index 3a0e4f8ea87fff50e9d66e2808e60885dabab64c..17776bf4e66766ace872de8238cbab7ba2fa9746 100644
--- a/tests/cil/oracle/bts297.res.oracle
+++ b/tests/cil/oracle/bts297.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/cil/bts297.c (with preprocessing)
-[kernel] tests/cil/bts297.c:4: Warning:
+[kernel:CERT:MSC:37] tests/cil/bts297.c:4: Warning:
Body of function abrupt falls-through. Adding a return statement
/* Generated by Frama-C */
int abrupt(int x)
diff --git a/tests/misc/oracle/bts0452.res.oracle b/tests/misc/oracle/bts0452.res.oracle
index ac0e8049e5f7dd4953cfe79b0fc82e6494bb0e3f..2c73b32fed513083fe6a84000a7af2453996afd5 100644
--- a/tests/misc/oracle/bts0452.res.oracle
+++ b/tests/misc/oracle/bts0452.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/misc/bts0452.i (no preprocessing)
-[kernel] tests/misc/bts0452.i:13: Warning:
+[kernel:CERT:MSC:37] tests/misc/bts0452.i:13: Warning:
Body of function f falls-through. Adding a return statement
-[kernel] tests/misc/bts0452.i:27: Warning:
+[kernel:CERT:MSC:37] tests/misc/bts0452.i:27: Warning:
Body of function h falls-through. Adding a return statement
diff --git a/tests/slicing/oracle/use_spec.0.res.oracle b/tests/slicing/oracle/use_spec.0.res.oracle
index c0241861da45aac64f312fa4fbb8e007bbda5b39..429c7b8b3a50c9b5d224f74399a5250ed7ee4bae 100644
--- a/tests/slicing/oracle/use_spec.0.res.oracle
+++ b/tests/slicing/oracle/use_spec.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/slicing/use_spec.i (no preprocessing)
-[kernel] tests/slicing/use_spec.i:18: Warning:
+[kernel:CERT:MSC:37] tests/slicing/use_spec.i:18: Warning:
Body of function f falls-through. Adding a return statement
[slicing] slicing requests in progress...
[eva] Analyzing a complete application starting at main
diff --git a/tests/slicing/oracle/use_spec.1.res.oracle b/tests/slicing/oracle/use_spec.1.res.oracle
index 93c1f23b8401e200b1deb811ee98e82c384c6836..025d609b877a900cbb988f5dc144f145fdb72619 100644
--- a/tests/slicing/oracle/use_spec.1.res.oracle
+++ b/tests/slicing/oracle/use_spec.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/slicing/use_spec.i (no preprocessing)
-[kernel] tests/slicing/use_spec.i:18: Warning:
+[kernel:CERT:MSC:37] tests/slicing/use_spec.i:18: Warning:
Body of function f falls-through. Adding a return statement
[slicing] slicing requests in progress...
[eva] Analyzing a complete application starting at main2
diff --git a/tests/syntax/oracle/exit.res.oracle b/tests/syntax/oracle/exit.res.oracle
index 48e6416347fda39e32b5f9cba87b2ab3d568864e..a7022ad38e1eea851612a138341dd8e1790372ac 100644
--- a/tests/syntax/oracle/exit.res.oracle
+++ b/tests/syntax/oracle/exit.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/exit.c (with preprocessing)
-[kernel] tests/syntax/exit.c:16: Warning:
+[kernel:CERT:MSC:37] tests/syntax/exit.c:16: Warning:
Body of function g falls-through. Adding a return statement
/* Generated by Frama-C */
#include "stdlib.h"
diff --git a/tests/syntax/oracle/inline_calls.0.res.oracle b/tests/syntax/oracle/inline_calls.0.res.oracle
index fd9c8a925f562d51ed31387053cb1386b94bde5c..99c4c1192c5b3efd35493ec3ab1b390c16920f9e 100644
--- a/tests/syntax/oracle/inline_calls.0.res.oracle
+++ b/tests/syntax/oracle/inline_calls.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/inline_calls.i (no preprocessing)
-[kernel] tests/syntax/inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] tests/syntax/inline_calls.i:40: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/inline_calls.1.res.oracle b/tests/syntax/oracle/inline_calls.1.res.oracle
index 710e3f55ab8cf8e3f39397e47fc2793689810d59..8522e300317fddc165d539005f7ac2b7eef6e7ba 100644
--- a/tests/syntax/oracle/inline_calls.1.res.oracle
+++ b/tests/syntax/oracle/inline_calls.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/inline_calls.i (no preprocessing)
-[kernel] tests/syntax/inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] tests/syntax/inline_calls.i:40: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/inline_calls.2.res.oracle b/tests/syntax/oracle/inline_calls.2.res.oracle
index e58cc380f9b2732adceed26a9d54af2f23d6986d..944a217b290220957f3ca1d8767d2371c4177ebd 100644
--- a/tests/syntax/oracle/inline_calls.2.res.oracle
+++ b/tests/syntax/oracle/inline_calls.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/inline_calls.i (no preprocessing)
-[kernel] tests/syntax/inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] tests/syntax/inline_calls.i:40: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/noret.res.oracle b/tests/syntax/oracle/noret.res.oracle
index 26c634ad06fc8b7e85b4be755e5a24baa7fac5d1..34a2110369c6472c83ec7265a156f2d102373465 100644
--- a/tests/syntax/oracle/noret.res.oracle
+++ b/tests/syntax/oracle/noret.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/noret.i (no preprocessing)
-[kernel] tests/syntax/noret.i:5: Warning:
+[kernel:CERT:MSC:37] tests/syntax/noret.i:5: Warning:
Body of function foo falls-through. Adding a return statement
/* Generated by Frama-C */
struct s {
diff --git a/tests/syntax/oracle/one_ret_assert.res.oracle b/tests/syntax/oracle/one_ret_assert.res.oracle
index a567df1d5610d56ec82d753daeb08bde3c1ca5f2..8e5b81c296e7aed6955c080d3fed811950d336d0 100644
--- a/tests/syntax/oracle/one_ret_assert.res.oracle
+++ b/tests/syntax/oracle/one_ret_assert.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/one_ret_assert.i (no preprocessing)
-[kernel] tests/syntax/one_ret_assert.i:8: Warning:
+[kernel:CERT:MSC:37] tests/syntax/one_ret_assert.i:8: Warning:
Body of function g falls-through. Adding a return statement
/* Generated by Frama-C */
int X;
diff --git a/tests/syntax/oracle/vla_switch.res.oracle b/tests/syntax/oracle/vla_switch.res.oracle
index 55afc254bf0c44d5f760af4fe96de5936a0d7d28..dab614c53e409206667a6ee29ed0d95d5e9ddf45 100644
--- a/tests/syntax/oracle/vla_switch.res.oracle
+++ b/tests/syntax/oracle/vla_switch.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/vla_switch.i (no preprocessing)
-[kernel] tests/syntax/vla_switch.i:16: Warning:
+[kernel:CERT:MSC:37] tests/syntax/vla_switch.i:16: Warning:
Body of function case3 falls-through. Adding a return statement
[kernel] User Error: tests/syntax/vla_switch.i:7, cannot jump from switch statement bypassing initialization of variable b, declared at tests/syntax/vla_switch.i:9
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/audit-out.json b/tests/value/oracle/audit-out.json
index f9aa254ce113486f162682dd6cebdc83f2a6768d..23aa305f9c0060058b4df8ce27fde23d0ebc4f5c 100644
--- a/tests/value/oracle/audit-out.json
+++ b/tests/value/oracle/audit-out.json
@@ -51,11 +51,11 @@
"kernel": {
"warning-categories": {
"enabled": [
- "*", "CERT", "CERT:EXP", "CERT:EXP:46", "CERT:MSC", "CERT:MSC:38",
- "acsl-extension", "annot", "annot:missing-spec", "annot:multi-from",
- "annot-error", "audit", "check", "check:volatile", "cmdline",
- "ghost", "ghost:bad-use", "inline", "linker",
- "linker:drop-conflicting-unused", "parser",
+ "*", "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",
+ "check:volatile", "cmdline", "ghost", "ghost:bad-use", "inline",
+ "linker", "linker:drop-conflicting-unused", "parser",
"parser:conditional-feature", "pp", "pp:compilation-db", "typing",
"typing:implicit-conv-void-ptr",
"typing:implicit-function-declaration",
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 338f79ddc5e562248c7d3246b45271cb2c3c3945..153b5cdfa777c639fab3302534f98e58a68c1d67 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing tests/value/imprecise_invalid_write.i (no preprocessing)
-[kernel] tests/value/imprecise_invalid_write.i:5: Warning:
+[kernel:CERT:MSC:37] tests/value/imprecise_invalid_write.i:5: Warning:
Body of function main1 falls-through. Adding a return statement
-[kernel] tests/value/imprecise_invalid_write.i:10: Warning:
+[kernel:CERT:MSC:37] tests/value/imprecise_invalid_write.i:10: Warning:
Body of function main2 falls-through. Adding a return statement
-[kernel] tests/value/imprecise_invalid_write.i:17: Warning:
+[kernel:CERT:MSC:37] tests/value/imprecise_invalid_write.i:17: Warning:
Body of function main3 falls-through. Adding a return statement
[eva] Analyzing a complete application starting at main
[eva] Computing initial state