From b2df74b1046ed578a0328bb476097e75f6fdbeb2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 12 Nov 2020 08:33:46 +0100
Subject: [PATCH] [kernel] New warning category for multiple froms
---
src/kernel_internals/parsing/logic_parser.mly | 2 +-
src/kernel_services/plugin_entry_points/kernel.ml | 2 ++
src/kernel_services/plugin_entry_points/kernel.mli | 2 ++
tests/rte/oracle/assign5.res.oracle | 6 ++++--
tests/syntax/oracle/multiple_froms.res.oracle | 6 ++++--
5 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index c907f613247..8a41fe69f4f 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -143,7 +143,7 @@
List.(for_all (fun e -> exists (is_same_lexpr e) lin) l)
in
let drop d k =
- Kernel.warning ~current:false
+ Kernel.warning ~current:false ~wkey:Kernel.wkey_multi_from
"Drop '%a' \\from at %a for more precise one at %a"
Logic_print.print_lexpr curloc
Cil_datatype.Location.pretty d.lexpr_loc
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 0ddeab5c75a..27e2b1cd3fe 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -185,6 +185,8 @@ let wkey_no_proto = register_warn_category "typing:no-proto"
let wkey_missing_spec = register_warn_category "annot:missing-spec"
+let wkey_multi_from = register_warn_category "annot:multi-from"
+
let wkey_decimal_float = register_warn_category "parser:decimal-float"
let () = set_warn_status wkey_decimal_float Log.Wonce
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index f62ba3b05e3..c6ffe271274 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -175,6 +175,8 @@ val wkey_no_proto: warn_category
val wkey_missing_spec: warn_category
+val wkey_multi_from: warn_category
+
val wkey_decimal_float: warn_category
val wkey_acsl_extension: warn_category
diff --git a/tests/rte/oracle/assign5.res.oracle b/tests/rte/oracle/assign5.res.oracle
index 2b943239fac..52d1def1f07 100644
--- a/tests/rte/oracle/assign5.res.oracle
+++ b/tests/rte/oracle/assign5.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/rte/assign5.c (with preprocessing)
-[kernel] Warning: Drop '*p' \from at tests/rte/assign5.c:9 for more precise one at tests/rte/assign5.c:10
-[kernel] Warning: Drop '*p' \from at tests/rte/assign5.c:19 for more precise one at tests/rte/assign5.c:18
+[kernel:annot:multi-from] Warning:
+ Drop '*p' \from at tests/rte/assign5.c:9 for more precise one at tests/rte/assign5.c:10
+[kernel:annot:multi-from] Warning:
+ Drop '*p' \from at tests/rte/assign5.c:19 for more precise one at tests/rte/assign5.c:18
[rte] annotating function main
/* Generated by Frama-C */
/*@ assigns *p;
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
index a7738a18dbf..b90f4dc55f6 100644
--- a/tests/syntax/oracle/multiple_froms.res.oracle
+++ b/tests/syntax/oracle/multiple_froms.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/syntax/multiple_froms.i (no preprocessing)
-[kernel] Warning: Drop 'b' \from at tests/syntax/multiple_froms.i:9 for more precise one at tests/syntax/multiple_froms.i:10
-[kernel] Warning: Drop 'a' \from at tests/syntax/multiple_froms.i:7 for more precise one at tests/syntax/multiple_froms.i:6
+[kernel:annot:multi-from] Warning:
+ Drop 'b' \from at tests/syntax/multiple_froms.i:9 for more precise one at tests/syntax/multiple_froms.i:10
+[kernel:annot:multi-from] Warning:
+ Drop 'a' \from at tests/syntax/multiple_froms.i:7 for more precise one at tests/syntax/multiple_froms.i:6
/* Generated by Frama-C */
int a;
int b;
--
GitLab