diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly index c907f613247d97a8997b55d73ce6792e4b9042ee..8a41fe69f4f24827622a3d4d6c56ed638821d3eb 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 0ddeab5c75a42c32227c2d5099582104a5a112c4..27e2b1cd3fe12941cac241bd352aad73593f1e89 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 f62ba3b05e3b0e7eaae81d3e521ffc219007cccf..c6ffe271274d0566b44115791d6a158d672cc056 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 2b943239facff3e2b164518daf2779695f53fa14..52d1def1f07ac9c260c9f52025366357dfa448a3 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 a7738a18dbf6118340e45c04b38ffa7a23707503..b90f4dc55f6e2c31b6f7656f8f8cc0ecfa6cf03d 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;