From 2fb2df19e5d050ce65fbeae28d19e2ec1c0078f5 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 26 Sep 2024 17:38:09 +0200
Subject: [PATCH] [tests] Update test oracles
---
tests/misc/Debug_category.ml | 16 ++++++++--------
tests/misc/debug_category.i | 3 ++-
tests/misc/oracle/debug_category.0.res.oracle | 12 ++++++------
tests/misc/oracle/debug_category.1.res.oracle | 17 ++++++-----------
tests/misc/oracle/debug_category.10.res.oracle | 4 ++--
tests/misc/oracle/debug_category.11.res.oracle | 5 ++---
tests/misc/oracle/debug_category.12.res.oracle | 4 ++--
tests/misc/oracle/debug_category.13.res.oracle | 6 ++----
tests/misc/oracle/debug_category.14.res.oracle | 8 ++++----
tests/misc/oracle/debug_category.15.res.oracle | 3 ++-
tests/misc/oracle/debug_category.16.res.oracle | 13 ++-----------
tests/misc/oracle/debug_category.17.res.oracle | 15 +++++++++++++++
tests/misc/oracle/debug_category.2.res.oracle | 6 ++++++
tests/misc/oracle/debug_category.3.res.oracle | 3 ---
tests/misc/oracle/debug_category.4.res.oracle | 6 +++---
tests/misc/oracle/debug_category.5.res.oracle | 6 ------
tests/misc/oracle/debug_category.6.res.oracle | 14 ++++++++++++--
tests/misc/oracle/debug_category.7.res.oracle | 2 --
tests/misc/oracle/debug_category.8.res.oracle | 3 ++-
tests/misc/oracle/debug_category.9.res.oracle | 5 +++--
20 files changed, 79 insertions(+), 72 deletions(-)
create mode 100644 tests/misc/oracle/debug_category.17.res.oracle
diff --git a/tests/misc/Debug_category.ml b/tests/misc/Debug_category.ml
index 01515996ec8..e3350258da5 100644
--- a/tests/misc/Debug_category.ml
+++ b/tests/misc/Debug_category.ml
@@ -6,15 +6,15 @@ include
let help = "test"
end)
-let akey = register_category "a"
-let ckey = register_category "a:b:c"
-let bkey = register_category "a:b"
-let dkey = register_category "d"
+let akey = register_category ~help:"A short description for a" "a"
+let ckey = register_category ~help:"A short description for a::b::c" "a:b:c"
+let bkey = register_category ~help:"A short description for a::b" "a:b"
+let dkey = register_category ~help:"A short description for d" "d"
-let wkey = register_warn_category "a"
-let wkey_vis_err = register_warn_category "test-vis-err"
-let wkey_inv_err = register_warn_category "test-inv-err"
-let wkey_failure = register_warn_category "test-failure"
+let wkey = register_warn_category ~help:"A short description for a" "a"
+let wkey_vis_err = register_warn_category ~help:"A short description for test-vis-err" "test-vis-err"
+let wkey_inv_err = register_warn_category ~help:"A short description for test-inv-err" "test-inv-err"
+let wkey_failure = register_warn_category ~help:"A short description for test-failure" "test-failure"
let () = set_warn_status wkey_vis_err Log.Winactive
let () = set_warn_status wkey_inv_err Log.Winactive
let () = set_warn_status wkey_failure Log.Winactive
diff --git a/tests/misc/debug_category.i b/tests/misc/debug_category.i
index f4b77fa6c36..c9771f21c1d 100644
--- a/tests/misc/debug_category.i
+++ b/tests/misc/debug_category.i
@@ -1,7 +1,8 @@
/* run.config*
MODULE: Debug_category
EXIT: 0
- OPT: -test-msg-key help -test-warn-key="a=inactive"
+ OPT: -test-msg-key help
+ OPT: -test-warn-key help -test-warn-key="a=inactive"
OPT: -test-msg-key a -test-warn-key="a=inactive"
OPT: -test-msg-key a -test-msg-key="-a:b" -test-warn-key="a=inactive"
OPT: -test-msg-key a -test-msg-key="-a:b" -test-msg-key a:b:c -test-warn-key="a=inactive"
diff --git a/tests/misc/oracle/debug_category.0.res.oracle b/tests/misc/oracle/debug_category.0.res.oracle
index 32b25410f78..6281af6ac7c 100644
--- a/tests/misc/oracle/debug_category.0.res.oracle
+++ b/tests/misc/oracle/debug_category.0.res.oracle
@@ -1,6 +1,6 @@
-[test] Available message categories are:
- *
- a
- a:b
- a:b:c
- d
+[test] Message categories for test are:
+ * : All categories
+ a : A short description for a
+ a:b : A short description for a::b
+ a:b:c : A short description for a::b::c
+ d : A short description for d
diff --git a/tests/misc/oracle/debug_category.1.res.oracle b/tests/misc/oracle/debug_category.1.res.oracle
index 7452d354800..c5e413169e7 100644
--- a/tests/misc/oracle/debug_category.1.res.oracle
+++ b/tests/misc/oracle/debug_category.1.res.oracle
@@ -1,11 +1,6 @@
-[kernel] Parsing debug_category.i (no preprocessing)
-[test] Warning: Uncategorized warning
-[test:a] A is enabled
-[test:a:b] B is enabled
-[test:a:b:c] C is enabled
-[test:a] A is enabled
-[test:a:b] B is enabled
-[test:a:b:c] C is enabled
-[test:a] A is enabled
-[test:a:b] B is enabled
-[test:a:b:c] C is enabled
+[test] Warning categories for test are
+ * : active : All warning categories
+ a : inactive : A short description for a
+ test-failure : inactive : A short description for test-failure
+ test-inv-err : inactive : A short description for test-inv-err
+ test-vis-err : inactive : A short description for test-vis-err
diff --git a/tests/misc/oracle/debug_category.10.res.oracle b/tests/misc/oracle/debug_category.10.res.oracle
index e1d1746e2bc..b34487855db 100644
--- a/tests/misc/oracle/debug_category.10.res.oracle
+++ b/tests/misc/oracle/debug_category.10.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test] User Error: warning treated as fatal error.
-[kernel] Plug-in test aborted: invalid user input.
+[test:a] Warning A
+[test:a] Another Warning A
diff --git a/tests/misc/oracle/debug_category.11.res.oracle b/tests/misc/oracle/debug_category.11.res.oracle
index 6fb0b39bd06..e1d1746e2bc 100644
--- a/tests/misc/oracle/debug_category.11.res.oracle
+++ b/tests/misc/oracle/debug_category.11.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test:a] Warning:
- Warning A
- (warn-once: no further messages from category 'a' will be emitted)
+[test] User Error: warning treated as fatal error.
+[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/debug_category.12.res.oracle b/tests/misc/oracle/debug_category.12.res.oracle
index 8f40020822c..6fb0b39bd06 100644
--- a/tests/misc/oracle/debug_category.12.res.oracle
+++ b/tests/misc/oracle/debug_category.12.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test:a]
+[test:a] Warning:
Warning A
- (warn-feedback-once: no further messages from category 'a' will be emitted)
+ (warn-once: no further messages from category 'a' will be emitted)
diff --git a/tests/misc/oracle/debug_category.13.res.oracle b/tests/misc/oracle/debug_category.13.res.oracle
index f7d982e9f13..8f40020822c 100644
--- a/tests/misc/oracle/debug_category.13.res.oracle
+++ b/tests/misc/oracle/debug_category.13.res.oracle
@@ -1,7 +1,5 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test:a] Warning:
+[test:a]
Warning A
- (warn-error-once: no further messages from category 'a' will be emitted)
-[test] Warning: warning a treated as deferred error. See above messages for more information.
-[kernel] Plug-in test aborted: invalid user input.
+ (warn-feedback-once: no further messages from category 'a' will be emitted)
diff --git a/tests/misc/oracle/debug_category.14.res.oracle b/tests/misc/oracle/debug_category.14.res.oracle
index b33ecc559a4..f7d982e9f13 100644
--- a/tests/misc/oracle/debug_category.14.res.oracle
+++ b/tests/misc/oracle/debug_category.14.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test:a] Warning: Warning A
-[test] User Error: Testing error function
-[test:a] Warning: Another Warning A
-[test] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[test:a] Warning:
+ Warning A
+ (warn-error-once: no further messages from category 'a' will be emitted)
+[test] Warning: warning a treated as deferred error. See above messages for more information.
[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/debug_category.15.res.oracle b/tests/misc/oracle/debug_category.15.res.oracle
index 6857c762cdb..b33ecc559a4 100644
--- a/tests/misc/oracle/debug_category.15.res.oracle
+++ b/tests/misc/oracle/debug_category.15.res.oracle
@@ -1,6 +1,7 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
[test:a] Warning: Warning A
+[test] User Error: Testing error function
[test:a] Warning: Another Warning A
-[test] Failure: Deferred error message was emitted during execution.
+[test] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/debug_category.16.res.oracle b/tests/misc/oracle/debug_category.16.res.oracle
index 64448bd5bd4..6857c762cdb 100644
--- a/tests/misc/oracle/debug_category.16.res.oracle
+++ b/tests/misc/oracle/debug_category.16.res.oracle
@@ -1,15 +1,6 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
[test:a] Warning: Warning A
-[test] Failure: Testing failure function
[test:a] Warning: Another Warning A
-[test] Failure: Deferred internal error message was emitted during execution. See above messages for more information.
-[kernel] Current source was: <unknown>
- The full backtrace is:
-
- Plug-in test aborted: internal error.
- Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
- Your Frama-C version is VERSION
- Note that a version and a backtrace alone often do not contain enough
- information to understand the bug. Guidelines for reporting bugs are at:
- https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
+[test] Failure: Deferred error message was emitted during execution.
+[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/debug_category.17.res.oracle b/tests/misc/oracle/debug_category.17.res.oracle
new file mode 100644
index 00000000000..64448bd5bd4
--- /dev/null
+++ b/tests/misc/oracle/debug_category.17.res.oracle
@@ -0,0 +1,15 @@
+[kernel] Parsing debug_category.i (no preprocessing)
+[test] Warning: Uncategorized warning
+[test:a] Warning: Warning A
+[test] Failure: Testing failure function
+[test:a] Warning: Another Warning A
+[test] Failure: Deferred internal error message was emitted during execution. See above messages for more information.
+[kernel] Current source was: <unknown>
+ The full backtrace is:
+
+ Plug-in test aborted: internal error.
+ Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
+ Your Frama-C version is VERSION
+ Note that a version and a backtrace alone often do not contain enough
+ information to understand the bug. Guidelines for reporting bugs are at:
+ https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
diff --git a/tests/misc/oracle/debug_category.2.res.oracle b/tests/misc/oracle/debug_category.2.res.oracle
index 8c6f9e506b9..7452d354800 100644
--- a/tests/misc/oracle/debug_category.2.res.oracle
+++ b/tests/misc/oracle/debug_category.2.res.oracle
@@ -1,5 +1,11 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
[test:a] A is enabled
+[test:a:b] B is enabled
+[test:a:b:c] C is enabled
[test:a] A is enabled
+[test:a:b] B is enabled
+[test:a:b:c] C is enabled
[test:a] A is enabled
+[test:a:b] B is enabled
+[test:a:b:c] C is enabled
diff --git a/tests/misc/oracle/debug_category.3.res.oracle b/tests/misc/oracle/debug_category.3.res.oracle
index ae35aa6bd0c..8c6f9e506b9 100644
--- a/tests/misc/oracle/debug_category.3.res.oracle
+++ b/tests/misc/oracle/debug_category.3.res.oracle
@@ -1,8 +1,5 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
[test:a] A is enabled
-[test:a:b:c] C is enabled
[test:a] A is enabled
-[test:a:b:c] C is enabled
[test:a] A is enabled
-[test:a:b:c] C is enabled
diff --git a/tests/misc/oracle/debug_category.4.res.oracle b/tests/misc/oracle/debug_category.4.res.oracle
index 69c1ff4aaf6..ae35aa6bd0c 100644
--- a/tests/misc/oracle/debug_category.4.res.oracle
+++ b/tests/misc/oracle/debug_category.4.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
+[test:a] A is enabled
[test:a:b:c] C is enabled
-[test:d] D is enabled
+[test:a] A is enabled
[test:a:b:c] C is enabled
-[test:d] D is enabled
+[test:a] A is enabled
[test:a:b:c] C is enabled
-[test:d] D is enabled
diff --git a/tests/misc/oracle/debug_category.5.res.oracle b/tests/misc/oracle/debug_category.5.res.oracle
index baaa05f1f56..69c1ff4aaf6 100644
--- a/tests/misc/oracle/debug_category.5.res.oracle
+++ b/tests/misc/oracle/debug_category.5.res.oracle
@@ -1,14 +1,8 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test:a] A is enabled
-[test:a:b] B is enabled
[test:a:b:c] C is enabled
[test:d] D is enabled
-[test:a] A is enabled
-[test:a:b] B is enabled
[test:a:b:c] C is enabled
[test:d] D is enabled
-[test:a] A is enabled
-[test:a:b] B is enabled
[test:a:b:c] C is enabled
[test:d] D is enabled
diff --git a/tests/misc/oracle/debug_category.6.res.oracle b/tests/misc/oracle/debug_category.6.res.oracle
index 6aa66ddb11b..baaa05f1f56 100644
--- a/tests/misc/oracle/debug_category.6.res.oracle
+++ b/tests/misc/oracle/debug_category.6.res.oracle
@@ -1,4 +1,14 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test:a] Warning: Warning A
-[test:a] Warning: Another Warning A
+[test:a] A is enabled
+[test:a:b] B is enabled
+[test:a:b:c] C is enabled
+[test:d] D is enabled
+[test:a] A is enabled
+[test:a:b] B is enabled
+[test:a:b:c] C is enabled
+[test:d] D is enabled
+[test:a] A is enabled
+[test:a:b] B is enabled
+[test:a:b:c] C is enabled
+[test:d] D is enabled
diff --git a/tests/misc/oracle/debug_category.7.res.oracle b/tests/misc/oracle/debug_category.7.res.oracle
index 66200a611db..6aa66ddb11b 100644
--- a/tests/misc/oracle/debug_category.7.res.oracle
+++ b/tests/misc/oracle/debug_category.7.res.oracle
@@ -2,5 +2,3 @@
[test] Warning: Uncategorized warning
[test:a] Warning: Warning A
[test:a] Warning: Another Warning A
-[test] Warning: warning a treated as deferred error. See above messages for more information.
-[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/debug_category.8.res.oracle b/tests/misc/oracle/debug_category.8.res.oracle
index ebba70ad529..66200a611db 100644
--- a/tests/misc/oracle/debug_category.8.res.oracle
+++ b/tests/misc/oracle/debug_category.8.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
[test:a] Warning: Warning A
-[test] User Error: warning a treated as fatal error.
+[test:a] Warning: Another Warning A
+[test] Warning: warning a treated as deferred error. See above messages for more information.
[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/oracle/debug_category.9.res.oracle b/tests/misc/oracle/debug_category.9.res.oracle
index b34487855db..ebba70ad529 100644
--- a/tests/misc/oracle/debug_category.9.res.oracle
+++ b/tests/misc/oracle/debug_category.9.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing debug_category.i (no preprocessing)
[test] Warning: Uncategorized warning
-[test:a] Warning A
-[test:a] Another Warning A
+[test:a] Warning: Warning A
+[test] User Error: warning a treated as fatal error.
+[kernel] Plug-in test aborted: invalid user input.
--
GitLab