From 1cfad7e54f40a51c204b926ff9f365a5bc77c46a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 5 Mar 2021 12:05:52 +0100
Subject: [PATCH] [Kernel] add wkey CERT:MSC:37 to existing 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 | 2 ++
.../wp/tests/wp/oracle/stmtcompiler_test.res.oracle | 2 +-
tests/cil/oracle/bts297.res.oracle | 2 +-
tests/misc/oracle/bts0452.res.oracle | 4 ++--
tests/slicing/oracle/use_spec.0.res.oracle | 2 +-
tests/slicing/oracle/use_spec.1.res.oracle | 2 +-
tests/syntax/oracle/exit.res.oracle | 2 +-
tests/syntax/oracle/inline_calls.0.res.oracle | 2 +-
tests/syntax/oracle/inline_calls.1.res.oracle | 2 +-
tests/syntax/oracle/inline_calls.2.res.oracle | 2 +-
tests/syntax/oracle/noret.res.oracle | 2 +-
tests/syntax/oracle/one_ret_assert.res.oracle | 2 +-
tests/syntax/oracle/vla_switch.res.oracle | 2 +-
tests/value/oracle/audit-out.json | 10 +++++-----
tests/value/oracle/imprecise_invalid_write.res.oracle | 6 +++---
17 files changed, 27 insertions(+), 23 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 64bd16cb823..f7612dbb21e 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 e21274bd4b3..8b30799b24b 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 a6e7e409bca..c971c83111f 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 f660536e9e2..234959f116a 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/tests/cil/oracle/bts297.res.oracle b/tests/cil/oracle/bts297.res.oracle
index 3a0e4f8ea87..17776bf4e66 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 ac0e8049e5f..2c73b32fed5 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 c0241861da4..429c7b8b3a5 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 93c1f23b840..025d609b877 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 48e6416347f..a7022ad38e1 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 fd9c8a925f5..99c4c1192c5 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 710e3f55ab8..8522e300317 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 e58cc380f9b..944a217b290 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 26c634ad06f..34a2110369c 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 a567df1d561..8e5b81c296e 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 55afc254bf0..dab614c53e4 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 f9aa254ce11..23aa305f9c0 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 338f79ddc5e..153b5cdfa77 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
--
GitLab