From e688280c979a52fc4ee2f6589cfcd0aeb994df32 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 23 Jan 2025 08:55:56 +0100
Subject: [PATCH] [Kernel] slightly reformulate deferred error messages
---
src/kernel_services/plugin_entry_points/log.ml | 7 ++++---
src/plugins/server/tests/batch/wrong.t/run.t | 3 ++-
src/plugins/wp/tests/wp/oracle/main_called.res.oracle | 2 +-
src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle | 2 +-
src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle | 2 +-
src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle | 2 +-
.../wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle | 4 +++-
.../wp/tests/wp_plugin/oracle/import_unexisting.res.oracle | 2 +-
tests/cil/oracle/ghost_cfg.0.res.oracle | 2 +-
tests/cil/oracle/ghost_cfg.1.res.oracle | 2 +-
tests/misc/oracle/debug_category.14.res.oracle | 2 +-
tests/misc/oracle/debug_category.15.res.oracle | 2 +-
tests/misc/oracle/debug_category.16.res.oracle | 2 +-
tests/misc/oracle/debug_category.17.res.oracle | 2 +-
tests/misc/oracle/debug_category.8.res.oracle | 2 +-
tests/misc/user_directories.unix.t/run.t | 3 ++-
tests/spec/oracle/Extend_errors.3.res.oracle | 2 +-
tests/spec/oracle/import_errors.2.res.oracle | 2 +-
tests/spec/oracle/import_errors.3.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.1.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.2.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.7.res.oracle | 2 +-
tests/syntax/oracle/ghost_cv_incompat.res.oracle | 2 +-
tests/syntax/oracle/ghost_cv_invalid_use.res.oracle | 2 +-
tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle | 2 +-
tests/syntax/oracle/too_large_array.res.oracle | 2 +-
tests/syntax/oracle/very_large_integers.11.res.oracle | 2 +-
tests/value/oracle/recursion.2.res.oracle | 2 +-
tests/value/oracle/use_spec.0.res.oracle | 2 +-
tests/value/oracle/use_spec.1.res.oracle | 2 +-
tests/value/oracle/va_list.1.res.oracle | 2 +-
31 files changed, 38 insertions(+), 33 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 7a425c05b53..c3456688d68 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 88c6925e34e..d54464200a2 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 91be9fd49b8..111236dfd23 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 64bcfd672f3..261d1aeb6ba 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 36cc360ff04..ae753332412 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 d726ead78f0..80c0495c242 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 51093e72350..29e32ed3efc 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 7626e418a06..c124b6c0e25 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 8fd6e6a5253..5312ba5fb8e 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 0448e9490f9..1057a06addd 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 a23f0ff8463..6073d7fb31c 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 24eb2787f22..a29ab32fe7a 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 05ddb3b964e..29bcf983ee6 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 9175eca5cbc..ebfdc38a7f5 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 ce16a8ff180..54dab8c4e1c 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 d37609b9f5f..241bc8a3abb 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 f893faa813a..51589b3dc99 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 aafb590e948..6c46069e65f 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 59d145fb2fa..512a05613c5 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 3f1bf2f4589..6affd1fe768 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 6d067c08966..9053bad7cae 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 21c18c167b7..336bd2392f7 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 67144a2682d..e35d4ba7926 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 4d5eba0305e..e0d860d893f 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 1c84f13933e..421297c4f23 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 0e7bd1d67b3..d5d9b4e03f5 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 c539276b527..814f106104f 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 77c360b499a..ee2372e9517 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 a82c098f3a1..25c745dd936 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 f3e0269226c..9d2c754b2e6 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 2a493c5ef3c..794562d8b44 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.
--
GitLab