From d636b4d0e46b55ef94af1fafaa053be198c7f2a3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 9 Aug 2024 18:14:11 +0200
Subject: [PATCH] [kernel] add wkey 'project' for save/load warnings
---
src/libraries/project/project.ml | 2 +-
src/libraries/project/project_skeleton.ml | 1 +
src/libraries/project/project_skeleton.mli | 1 +
tests/misc/oracle/audit-out.json | 4 ++--
tests/misc/oracle/my_visitor.1.res.oracle | 6 ++++--
tests/misc/oracle/orphan_emitter.res.oracle | 3 ++-
tests/saveload/oracle/basic.0.res.oracle | 3 ++-
tests/saveload/oracle/basic.4.res.oracle | 3 ++-
tests/saveload/oracle/deps.1.res.oracle | 3 ++-
tests/saveload/oracle/deps.2.res.oracle | 3 ++-
tests/saveload/oracle/deps.4.res.oracle | 6 ++++--
tests/saveload/oracle/segfault_datatypes.res.oracle | 3 ++-
12 files changed, 25 insertions(+), 13 deletions(-)
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index ec66fdebc10..efd97ce0af5 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -151,7 +151,7 @@ module States_operations = struct
let unserialize ?selection dst loaded_states =
let pp_err fmt n msg_sing msg_plural =
if n > 0 then begin
- warning ~once:true
+ warning ~once:true ~wkey
fmt
n
(if n = 1 then "" else "s")
diff --git a/src/libraries/project/project_skeleton.ml b/src/libraries/project/project_skeleton.ml
index 117344bf220..3251b340743 100644
--- a/src/libraries/project/project_skeleton.ml
+++ b/src/libraries/project/project_skeleton.ml
@@ -27,6 +27,7 @@
module Output = struct
include Cmdline.Kernel_log
let dkey = register_category "project"
+ let wkey = register_warn_category "project"
end
(* ************************************************************************** *)
diff --git a/src/libraries/project/project_skeleton.mli b/src/libraries/project/project_skeleton.mli
index c6c7e4b8969..7db8448429c 100644
--- a/src/libraries/project/project_skeleton.mli
+++ b/src/libraries/project/project_skeleton.mli
@@ -31,6 +31,7 @@
module Output : sig
include Log.Messages
val dkey: category
+ val wkey: warn_category
(** @since Fluorine-20130401 *)
end
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 0307758ad62..f078d477d54 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -63,8 +63,8 @@
"parser:conditional-feature", "parser:unnamed-typedef",
"parser:unsupported", "parser:unsupported:attributes",
"parser:unsupported:pragma", "plugin-not-loaded", "pp",
- "pp:compilation-db", "pp:line-directive", "too-large-array",
- "typing", "typing:implicit-conv-void-ptr",
+ "pp:compilation-db", "pp:line-directive", "project",
+ "too-large-array", "typing", "typing:implicit-conv-void-ptr",
"typing:implicit-function-declaration",
"typing:incompatible-pointer-types",
"typing:incompatible-types-call", "typing:inconsistent-specifier",
diff --git a/tests/misc/oracle/my_visitor.1.res.oracle b/tests/misc/oracle/my_visitor.1.res.oracle
index d7de4e33c03..ebb3e44d45d 100644
--- a/tests/misc/oracle/my_visitor.1.res.oracle
+++ b/tests/misc/oracle/my_visitor.1.res.oracle
@@ -1,9 +1,11 @@
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 13 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
-[kernel] Warning: 13 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 13 states in saved file ignored. They are invalid in this Frama-C configuration.
/* Generated by Frama-C */
int f(void)
{
diff --git a/tests/misc/oracle/orphan_emitter.res.oracle b/tests/misc/oracle/orphan_emitter.res.oracle
index 54742d6322b..4ec5b3c8d75 100644
--- a/tests/misc/oracle/orphan_emitter.res.oracle
+++ b/tests/misc/oracle/orphan_emitter.res.oracle
@@ -1,2 +1,3 @@
[kernel] Warning: emitter emitter1: correctness parameter -orphan does not exist anymore. Ignored.
-[kernel] Warning: 9 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 9 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/tests/saveload/oracle/basic.0.res.oracle b/tests/saveload/oracle/basic.0.res.oracle
index 0fe986b70a1..fc631301809 100644
--- a/tests/saveload/oracle/basic.0.res.oracle
+++ b/tests/saveload/oracle/basic.0.res.oracle
@@ -1 +1,2 @@
-[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 1 state in saved file ignored. It is invalid in this Frama-C configuration.
diff --git a/tests/saveload/oracle/basic.4.res.oracle b/tests/saveload/oracle/basic.4.res.oracle
index eeed93b93d1..49d86b7d41e 100644
--- a/tests/saveload/oracle/basic.4.res.oracle
+++ b/tests/saveload/oracle/basic.4.res.oracle
@@ -1 +1,2 @@
-[kernel] Warning: 9 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 9 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/tests/saveload/oracle/deps.1.res.oracle b/tests/saveload/oracle/deps.1.res.oracle
index 86d7a2aa4ea..1d5bc198f26 100644
--- a/tests/saveload/oracle/deps.1.res.oracle
+++ b/tests/saveload/oracle/deps.1.res.oracle
@@ -1 +1,2 @@
-[kernel] Warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/tests/saveload/oracle/deps.2.res.oracle b/tests/saveload/oracle/deps.2.res.oracle
index 86d7a2aa4ea..1d5bc198f26 100644
--- a/tests/saveload/oracle/deps.2.res.oracle
+++ b/tests/saveload/oracle/deps.2.res.oracle
@@ -1 +1,2 @@
-[kernel] Warning: 2 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 2 states in saved file ignored. They are invalid in this Frama-C configuration.
diff --git a/tests/saveload/oracle/deps.4.res.oracle b/tests/saveload/oracle/deps.4.res.oracle
index 0ace314a020..7aaa68b760b 100644
--- a/tests/saveload/oracle/deps.4.res.oracle
+++ b/tests/saveload/oracle/deps.4.res.oracle
@@ -1,2 +1,4 @@
-[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
-[kernel] Warning: 1 state in memory reset to their default value. It is inconsistent in this Frama_C configuration.
+[kernel:project] Warning:
+ 1 state in saved file ignored. It is invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 1 state in memory reset to their default value. It is inconsistent in this Frama_C configuration.
diff --git a/tests/saveload/oracle/segfault_datatypes.res.oracle b/tests/saveload/oracle/segfault_datatypes.res.oracle
index 0fe986b70a1..fc631301809 100644
--- a/tests/saveload/oracle/segfault_datatypes.res.oracle
+++ b/tests/saveload/oracle/segfault_datatypes.res.oracle
@@ -1 +1,2 @@
-[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
+[kernel:project] Warning:
+ 1 state in saved file ignored. It is invalid in this Frama-C configuration.
--
GitLab