diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 7a425c05b53a61284af693ecbe7fe3f595e44ab0..c3456688d68f94611757c0b3ebda22fee7812886 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -599,7 +599,8 @@ let deferred_raise ~fatal event msg =
else AbortError event.evt_plugin
in
let finally = finally_raise exn in
- logwithfinal finally channel ?append ~kind:event.evt_kind msg
+ (* change the kind to avoid re-appending 'Error' to the message *)
+ logwithfinal finally channel ?append ~kind:Result msg
let treat_deferred_error () =
match !deferred_exn with
@@ -611,8 +612,8 @@ let treat_deferred_error () =
| Some s when s = unreported_error -> ""
| Some s -> s
in
- deferred_raise ~fatal:false event
- "warning %s treated as deferred error:" wkey
+ deferred_raise ~fatal:false { event with evt_kind = Error }
+ "Deferred error: warning as error %s:" wkey
| DError event ->
deferred_raise ~fatal:false event
"Deferred error message was emitted during execution:"
diff --git a/src/plugins/server/tests/batch/wrong.t/run.t b/src/plugins/server/tests/batch/wrong.t/run.t
index 88c6925e34e071de783c1bd7a5789ead06cc87e8..d54464200a2c74345fdf61a451686cd16222a3fd 100644
--- a/src/plugins/server/tests/batch/wrong.t/run.t
+++ b/src/plugins/server/tests/batch/wrong.t/run.t
@@ -4,7 +4,8 @@
[server] User Error: [batch] "unknown request": request "kernel.unknown" not found
[server] User Error: [batch] "wrong data": request "kernel.ast.printFunction" not found
[server] Output "wrong.out.json"
- [server] User Error: Deferred error message was emitted during execution. See above messages for more information.
+ [server] Deferred error message was emitted during execution:
+ [batch] "unknown request": request "kernel.unknown" not found
[kernel] Plug-in server aborted: invalid user input.
[1]
$ cat wrong.out.json
diff --git a/src/plugins/wp/tests/wp/oracle/main_called.res.oracle b/src/plugins/wp/tests/wp/oracle/main_called.res.oracle
index 91be9fd49b8b4a52be4c34885f19ad1c98baa4e0..111236dfd239c15a805eb219b5d6c82164ff1c46 100644
--- a/src/plugins/wp/tests/wp/oracle/main_called.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/main_called.res.oracle
@@ -6,7 +6,7 @@
This case is not supported yet (skipped verification).
[wp] Warning: No goal generated
[wp] No proof obligations
-[wp] User Error: Deferred error message was emitted during execution:
+[wp] Deferred error message was emitted during execution:
Main entry point function 'main' is (potentially) recursive.
This case is not supported yet (skipped verification).
[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
index 64bcfd672f31e0790ded2c1f41579b14b29983d2..261d1aeb6baaa7b717e908825bde5f31ef78b97c 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
@@ -16,7 +16,7 @@ Goal Instance of 'Pre-condition 'qed_ok,Rmain' in 'main'' in 'call_main' at call
Prove: true.
------------------------------------------------------------
-[wp] User Error: Deferred error message was emitted during execution:
+[wp] Deferred error message was emitted during execution:
Main entry point function 'main' is (potentially) recursive.
This case is not supported yet (skipped verification).
[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
index 36cc360ff042bfb0637d89b099a79d072c2fa9ed..ae753332412fb4af1b83a593eef332cbc23dad9e 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
@@ -8,7 +8,7 @@
[wp] User Error: Main entry point function 'main' is (potentially) recursive.
This case is not supported yet (skipped verification).
[wp] No proof obligations
-[wp] User Error: Deferred error message was emitted during execution:
+[wp] Deferred error message was emitted during execution:
Main entry point function 'main' is (potentially) recursive.
This case is not supported yet (skipped verification).
[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
index d726ead78f0c65a68882bd8bf9c8ba3f0d996547..80c0495c242118a3ce50d7a203fbf350c80e5a45 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
@@ -22,7 +22,7 @@ Goal Instance of 'Pre-condition 'qed_ok,Rf' in 'f'' in 'double_call' at initiali
Prove: true.
------------------------------------------------------------
-[wp] User Error: Deferred error message was emitted during execution:
+[wp] Deferred error message was emitted during execution:
Main entry point function 'main' is (potentially) recursive.
This case is not supported yet (skipped verification).
[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index 51093e723505ca1f25b5b30948eeedc837ff8593..29e32ed3efc54abd2e27c79e70cc741c174d91ca 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -31,5 +31,7 @@
call_main 4 - 4 100%
call_g 4 - 4 100%
------------------------------------------------------------
-[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[wp] Deferred error message was emitted during execution:
+ Main entry point function 'main' is (potentially) recursive.
+ This case is not supported yet (skipped verification).
[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
index 7626e418a06b742861746c2e5bb1a7fc6015267c..c124b6c0e25bcae90729d52f63b2ed845b20ea4a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle
@@ -3,6 +3,6 @@
[wp] User Error: Library Module not found
[wp] Running WP plugin...
[wp] No proof obligations
-[wp] User Error: Deferred error message was emitted during execution:
+[wp] Deferred error message was emitted during execution:
Library Module not found
[kernel] Plug-in wp aborted: invalid user input.
diff --git a/tests/cil/oracle/ghost_cfg.0.res.oracle b/tests/cil/oracle/ghost_cfg.0.res.oracle
index 8fd6e6a5253fd99e84d2b57ab877c21d74f1345a..5312ba5fb8e460f4897136f24a9dd288441426d4 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -37,7 +37,7 @@
/*@ ghost goto X; */
[kernel:ghost:bad-use] ghost_cfg.c:109: Warning:
'__retres' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel] Warning: warning ghost:bad-use treated as deferred error:
+[kernel] Deferred error: warning as error ghost:bad-use:
ghost_cfg.c:10: Ghost code breaks CFG starting at:
/*@ ghost goto X; */
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/cil/oracle/ghost_cfg.1.res.oracle b/tests/cil/oracle/ghost_cfg.1.res.oracle
index 0448e9490f95a39d2f4e8589fec8a3bf606af5ab..1057a06adddb17f429a2b8f456f2cfa518896936 100644
--- a/tests/cil/oracle/ghost_cfg.1.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing ghost_cfg.c (with preprocessing)
[kernel] ghost_cfg.c:154: User Error:
'goto X;' would jump from normal statement to ghost code
-[kernel] User Error: Deferred error message was emitted during execution:
+[kernel] Deferred error message was emitted during execution:
ghost_cfg.c:154: 'goto X;' would jump from normal statement to ghost code
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/debug_category.14.res.oracle b/tests/misc/oracle/debug_category.14.res.oracle
index a23f0ff8463c73970509e3446bc5942f650fb4a6..6073d7fb31cea02c9d062f6922e56b9b8316543a 100644
--- a/tests/misc/oracle/debug_category.14.res.oracle
+++ b/tests/misc/oracle/debug_category.14.res.oracle
@@ -3,7 +3,7 @@
[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:
+[test] Deferred error: warning as error a:
Warning A
(warn-error-once: no further messages from category 'a' will be emitted)
[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 24eb2787f227400b3417a6c89d639eedaabc4be6..a29ab32fe7aa9d67047a378568d520af0b060890 100644
--- a/tests/misc/oracle/debug_category.15.res.oracle
+++ b/tests/misc/oracle/debug_category.15.res.oracle
@@ -3,6 +3,6 @@
[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:
+[test] Deferred error message was emitted during execution:
Testing error function
[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 05ddb3b964e48824c4d98ad919e9c47506211d8d..29bcf983ee6ab3dd3f984e7a43306bb82b6a89ac 100644
--- a/tests/misc/oracle/debug_category.16.res.oracle
+++ b/tests/misc/oracle/debug_category.16.res.oracle
@@ -2,6 +2,6 @@
[test] Warning: Uncategorized warning
[test:a] Warning: Warning A
[test:a] Warning: Another Warning A
-[test] Failure: Deferred error message was emitted during execution:
+[test] Deferred error message was emitted during execution:
Silent error
[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
index 9175eca5cbcb173c0d9b7180c85dc5affc38b916..ebfdc38a7f55719c99e8da0d3c660a5388d97e14 100644
--- a/tests/misc/oracle/debug_category.17.res.oracle
+++ b/tests/misc/oracle/debug_category.17.res.oracle
@@ -3,7 +3,7 @@
[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:
+[test] Deferred internal error message was emitted during execution:
Testing failure function
[kernel] Current source was: <unknown>
The full backtrace is:
diff --git a/tests/misc/oracle/debug_category.8.res.oracle b/tests/misc/oracle/debug_category.8.res.oracle
index ce16a8ff180d532472446d3b43e1f9b51bc13d68..54dab8c4e1c9a50812e03c57b9b59dd89092ae61 100644
--- a/tests/misc/oracle/debug_category.8.res.oracle
+++ b/tests/misc/oracle/debug_category.8.res.oracle
@@ -2,6 +2,6 @@
[test] Warning: Uncategorized warning
[test:a] Warning: Warning A
[test:a] Warning: Another Warning A
-[test] Warning: warning a treated as deferred error:
+[test] Deferred error: warning as error a:
Warning A
[kernel] Plug-in test aborted: invalid user input.
diff --git a/tests/misc/user_directories.unix.t/run.t b/tests/misc/user_directories.unix.t/run.t
index d37609b9f5f9058977e87375af0f49ccf9881e91..241bc8a3abb250ca5f4408be8416b21f451a1470 100644
--- a/tests/misc/user_directories.unix.t/run.t
+++ b/tests/misc/user_directories.unix.t/run.t
@@ -186,7 +186,8 @@ Customized kernel var > xdg var
Bad home value
$ HOME= dune exec --cache=disabled -- frama-c
[dirs] User Error: Failure when creating directories
- [dirs] User Error: Deferred error message was emitted during execution. See above messages for more information.
+ [dirs] Deferred error message was emitted during execution:
+ Failure when creating directories
[kernel] Plug-in dirs aborted: invalid user input.
[1]
diff --git a/tests/spec/oracle/Extend_errors.3.res.oracle b/tests/spec/oracle/Extend_errors.3.res.oracle
index f893faa813a57608b9a338cdec352fbe977a1cb7..51589b3dc9993ff77318185a3469357edd6be5c9 100644
--- a/tests/spec/oracle/Extend_errors.3.res.oracle
+++ b/tests/spec/oracle/Extend_errors.3.res.oracle
@@ -4,6 +4,6 @@
Ignoring unregistered extension 'bar' of plug-in myplugin1
[kernel:plugin-not-loaded] Extend_errors.c:33: Warning:
Ignoring extension 'bar' for unloaded plug-in unknown_plugin
-[kernel] Warning: warning extension-unknown treated as deferred error:
+[kernel] Deferred error: warning as error extension-unknown:
Extend_errors.c:32: Ignoring unregistered extension 'bar' of plug-in myplugin1
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/import_errors.2.res.oracle b/tests/spec/oracle/import_errors.2.res.oracle
index aafb590e9481c94e3cba683e957d69bd23edfa40..6c46069e65f6e80519e78624db7b7d0741cb2843 100644
--- a/tests/spec/oracle/import_errors.2.res.oracle
+++ b/tests/spec/oracle/import_errors.2.res.oracle
@@ -2,6 +2,6 @@
[kernel] Parsing import_errors.c (with preprocessing)
[kernel:extension-unknown] import_errors.c:40: Warning:
Ignoring unregistered module importer extension 'toto' of plug-in myplugin1
-[kernel] Warning: warning extension-unknown treated as deferred error:
+[kernel] Deferred error: warning as error extension-unknown:
import_errors.c:40: Ignoring unregistered module importer extension 'toto' of plug-in myplugin1
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/import_errors.3.res.oracle b/tests/spec/oracle/import_errors.3.res.oracle
index 59d145fb2faaf23fad0dee78b7f3ede5d3ddad6a..512a05613c560f577b616371a6f59e54cb7bc545 100644
--- a/tests/spec/oracle/import_errors.3.res.oracle
+++ b/tests/spec/oracle/import_errors.3.res.oracle
@@ -2,6 +2,6 @@
[kernel] Parsing import_errors.c (with preprocessing)
[kernel:extension-unknown] import_errors.c:44: Warning:
Ignoring unregistered module importer extension 'toto'
-[kernel] Warning: warning extension-unknown treated as deferred error:
+[kernel] Deferred error: warning as error extension-unknown:
import_errors.c:44: Ignoring unregistered module importer extension 'toto'
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.1.res.oracle b/tests/syntax/oracle/cert_msc_38.1.res.oracle
index 3f1bf2f4589d1b851a2668f3dd22a9004d3a54c9..6affd1fe76856012bfef0df5395fef33c949869c 100644
--- a/tests/syntax/oracle/cert_msc_38.1.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:33: Warning:
Attempt to declare errno as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C
-[kernel] Warning: warning CERT:MSC:38 treated as deferred error:
+[kernel] Deferred error: warning as error CERT:MSC:38:
cert_msc_38.c:33: Attempt to declare errno as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.2.res.oracle b/tests/syntax/oracle/cert_msc_38.2.res.oracle
index 6d067c08966d150faf7ccafdb693d2e4e3ef9d8b..9053bad7caeeae6b337bb484752ede57989175fd 100644
--- a/tests/syntax/oracle/cert_msc_38.2.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.2.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:38: Warning:
Attempt to declare math_errhandling as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C
-[kernel] Warning: warning CERT:MSC:38 treated as deferred error:
+[kernel] Deferred error: warning as error CERT:MSC:38:
cert_msc_38.c:38: Attempt to declare math_errhandling as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.7.res.oracle b/tests/syntax/oracle/cert_msc_38.7.res.oracle
index 21c18c167b7bb1e92d9fa0f5e9aca9bddd2426df..336bd2392f78f9646cec732a94dec7560951db3e 100644
--- a/tests/syntax/oracle/cert_msc_38.7.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.7.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing cert_msc_38.c (with preprocessing)
[kernel:CERT:MSC:38] cert_msc_38.c:60: Warning:
setjmp is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] Warning: warning CERT:MSC:38 treated as deferred error:
+[kernel] Deferred error: warning as error CERT:MSC:38:
cert_msc_38.c:60: setjmp is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_incompat.res.oracle b/tests/syntax/oracle/ghost_cv_incompat.res.oracle
index 67144a2682d9c7de445d5d2ff41ee4666be77beb..e35d4ba7926deebc91a2cc76689f766965bd0b15 100644
--- a/tests/syntax/oracle/ghost_cv_incompat.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_incompat.res.oracle
@@ -93,6 +93,6 @@
Invalid cast of '& g_0' from 'int \ghost *' to 'int *'
[kernel:ghost:bad-use] ghost_cv_incompat.i:194: Warning:
Invalid cast of '& g_0' from 'int \ghost *' to 'int *'
-[kernel] Warning: warning ghost:bad-use treated as deferred error:
+[kernel] Deferred error: warning as error ghost:bad-use:
ghost_cv_incompat.i:27: Invalid cast of '& ng' from 'int *' to 'int \ghost *'
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle b/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
index 4d5eba0305e79dba044063a0c51eba6fae1eb822..e0d860d893f5482d2983a33c830e67c0e03f2613 100644
--- a/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
@@ -57,6 +57,6 @@
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] ghost_cv_invalid_use.i:162: Warning:
Call to non-ghost function from ghost code is not allowed
-[kernel] Warning: warning ghost:bad-use treated as deferred error:
+[kernel] Deferred error: warning as error ghost:bad-use:
ghost_cv_invalid_use.i:14: 'ng' is a non-ghost lvalue, it cannot be assigned in ghost code
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle b/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle
index 1c84f13933e32e0c2c2a7db91ce5f5019c569252..421297c4f236614b34ab945f8ad0e5c32eecce9a 100644
--- a/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle
@@ -27,6 +27,6 @@
Invalid type for 'param': indirection from non-ghost to ghost
[kernel:ghost:bad-use] ghost_cv_var_decl.c:166: Warning:
Invalid type for 'pptrg': indirection from non-ghost to ghost
-[kernel] Warning: warning ghost:bad-use treated as deferred error:
+[kernel] Deferred error: warning as error ghost:bad-use:
ghost_cv_var_decl.c:152: No definition, nor assigns specification for ghost function 'decl_bad_return_type'
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/too_large_array.res.oracle b/tests/syntax/oracle/too_large_array.res.oracle
index 0e7bd1d67b305b692466a812cf057694fadce13a..d5d9b4e03f57e739e40aabb0c46b7cb9024ca115 100644
--- a/tests/syntax/oracle/too_large_array.res.oracle
+++ b/tests/syntax/oracle/too_large_array.res.oracle
@@ -3,6 +3,6 @@
Array length is too large.
[kernel] too_large_array.i:12: Warning:
Cannot represent length of array as an attribute
-[kernel] Warning: warning too-large-array treated as deferred error:
+[kernel] Deferred error: warning as error too-large-array:
too_large_array.i:12: Array length is too large.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index c539276b5271aff91e9c791fb3410fdda8c0d1d1..814f106104f15d6c5002db330dd3a0591e525d13 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -29,6 +29,6 @@
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
-[kernel] Warning: warning annot-error treated as deferred error:
+[kernel] Deferred error: warning as error annot-error:
very_large_integers.c:132: Invalid slevel directive. Ignoring code annotation
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
index 77c360b499a70035566cfb11d6a7deacfac6ff26..ee2372e951710bca47f897e146a0bd4d82277f30 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -50,7 +50,7 @@
Frama_C_entropy_source; x; y; tmp; tmp_0; tmp_1
[inout] Inputs for function main_fail:
Frama_C_entropy_source
-[eva] Warning: warning assigns:missing treated as deferred error:
+[eva] Deferred error: warning as error assigns:missing:
recursion.c:426: Recursive call to sum_nospec without assigns clause.
Generating probably incomplete assigns to interpret the call.
Try to increase the -eva-unroll-recursive-calls parameter or write a correct specification for function sum_nospec.
diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle
index a82c098f3a1124a585a91636c24fa3a48cf56f27..25c745dd936f56f16d6154fba07ad8bc1de8fd6f 100644
--- a/tests/value/oracle/use_spec.0.res.oracle
+++ b/tests/value/oracle/use_spec.0.res.oracle
@@ -74,6 +74,6 @@
x; y
Sure outputs:
w; z
-[eva] Warning: warning assigns:missing treated as deferred error:
+[eva] Deferred error: warning as error assigns:missing:
No assigns specified for function 'f' for which option -eva-use-spec is set. Generating potentially incorrect assigns.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle/use_spec.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle
index f3e0269226cc04e147a796139fb2146cf7540aa0..9d2c754b2e6e34babac58ff50d3ebb39c5a04e4b 100644
--- a/tests/value/oracle/use_spec.1.res.oracle
+++ b/tests/value/oracle/use_spec.1.res.oracle
@@ -74,6 +74,6 @@
x; y
Sure outputs:
w; z
-[eva] Warning: warning assigns:missing treated as deferred error:
+[eva] Deferred error: warning as error assigns:missing:
No assigns specified for function 'f' for which option -eva-use-spec is set. Generating potentially incorrect assigns.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle/va_list.1.res.oracle b/tests/value/oracle/va_list.1.res.oracle
index 2a493c5ef3c670e835f1b9dc2f66b01ff52db8fb..794562d8b449ee76cf3ba291f4a5c60ee2330375 100644
--- a/tests/value/oracle/va_list.1.res.oracle
+++ b/tests/value/oracle/va_list.1.res.oracle
@@ -30,6 +30,6 @@
vlParameters; tmp
[inout] Inputs for function main:
\nothing
-[eva] User Error: Deferred error message was emitted during execution:
+[eva] Deferred error message was emitted during execution:
va_list.c:14: functions returning variadic arguments must be stubbed
[kernel] Plug-in eva aborted: invalid user input.