[kernel] New warning category for multiple froms

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

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
 

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

tests/rte/oracle/assign5.res.oracle

 [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;

tests/syntax/oracle/multiple_froms.res.oracle

 [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;