diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 207b2a4271edc18c074a4072e3e54eb752364fbb..10a4ec0697ffe7c600de4fb8a291f9e07e6d8159 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -241,16 +241,8 @@ let rec echo_lines ?(prefix=false) output text p q =
let add_source buffer = function
| None -> ()
| Some src ->
- (* Avoid printing ':0:' if the position is unknown. *)
- if Filepath.is_empty_pos src
- then Buffer.add_string buffer "<unknown location> "
- else begin
- Buffer.add_string buffer
- (Filepath.Normalized.to_pretty_string src.Filepath.pos_path);
- Buffer.add_string buffer ":" ;
- Buffer.add_string buffer (string_of_int src.Filepath.pos_lnum);
- Buffer.add_string buffer ": "
- end
+ let fmt = Format.formatter_of_buffer buffer in
+ Format.fprintf fmt "%a: @?" Filepath.pp_pos src
let add_category buffer = function
| None -> ()
@@ -562,11 +554,6 @@ let deferred_exn = ref DNo_exn
let unreported_error = "##unreported-error##"
-let unreported_event { evt_category } =
- match evt_category with
- | None -> false
- | Some s -> s = unreported_error
-
(* we keep track of at most one deferred exception, ordered by seriousness
(internal error > user error > warning-as-error). the rationale is that
an internal error might cause subsequent errors or warning, but the reverse
@@ -585,44 +572,42 @@ let update_deferred_exn exn =
let warn_event_as_error event = update_deferred_exn (DWarn_as_error event)
-let deferred_raise ~fatal ~unreported event msg =
+let deferred_raise ~fatal event msg =
(* reset deferred flag. *)
let () = deferred_exn := DNo_exn in
let channel = new_channel event.evt_plugin in
- let append =
- if unreported then None else
- Some
- (fun fmt ->
- Format.fprintf fmt " See above messages for more information.@\n")
+ let pp_pos fmt pos = Format.fprintf fmt "%a: " Filepath.pp_pos pos in
+ let pp_pos_opt = Pretty_utils.pp_opt pp_pos in
+ let print_event fmt =
+ Format.fprintf fmt "@\n%a%s" pp_pos_opt event.evt_source event.evt_message
in
+ let append = Some print_event in
let exn =
if fatal then AbortFatal event.evt_plugin
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
| DNo_exn -> ()
| DWarn_as_error event ->
- let unreported = unreported_event event in
let wkey =
match event.evt_category with
| None -> ""
| Some s when s = unreported_error -> ""
| Some s -> s
in
- deferred_raise ~fatal:false ~unreported 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 ->
- let unreported = unreported_event event in
- deferred_raise ~fatal:false ~unreported event
- "Deferred error message was emitted during execution."
+ deferred_raise ~fatal:false event
+ "Deferred error message was emitted during execution:"
| DFatal event ->
- let unreported = unreported_event event in
- deferred_raise ~fatal:true ~unreported event
- "Deferred internal error message was emitted during execution."
+ deferred_raise ~fatal:true event
+ "Deferred internal error message was emitted during execution:"
(* -------------------------------------------------------------------------- *)
(* --- Messages Interface --- *)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 3193c18420457e03f2d4129767171a26325da0bf..ba739ec3de0d64711ee34723bd059037335c6e55 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -229,7 +229,9 @@ let rec skip_dot file_name =
else file_name
let pretty file_name =
- if Filename.is_relative file_name then
+ if file_name = "" then
+ "<unknown location>"
+ else if Filename.is_relative file_name then
skip_dot file_name
else
let path = insert cwd file_name in
@@ -297,6 +299,8 @@ module Normalized = struct
let pretty fmt p =
if is_special_stdout p then
Format.fprintf fmt "<stdout>"
+ else if is_empty p then
+ Format.fprintf fmt "<unknown location>"
else
Format.fprintf fmt "%s" (pretty p)
let pp_abs fmt p = Format.fprintf fmt "%s" p
@@ -337,7 +341,11 @@ let empty_pos = {
}
let pp_pos fmt pos =
- Format.fprintf fmt "%a:%d" Normalized.pretty pos.pos_path pos.pos_lnum
+ let path = pos.pos_path in
+ if Normalized.(is_empty path || is_special_stdout path) then
+ Format.fprintf fmt "%a" Normalized.pretty path
+ else
+ Format.fprintf fmt "%a:%d" Normalized.pretty path pos.pos_lnum
let is_empty_pos pos = pos == empty_pos
diff --git a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
index 960635f47e9055f7ffce2a06d2fa45b9324868fe..186a3452a787b9e653e3b0db06b7ac6fe76b3ea6 100644
--- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
@@ -18,7 +18,7 @@
no \from part for clause
'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'.
Assuming \from \nothing so that the analysis can continue, but be aware this is probably incorrect.
-[eva:alarm] <unknown location> Warning:
+[eva:alarm] <unknown location>: Warning:
function square_root_aux, behavior Buchi_property_behavior: postcondition got status unknown.
[eva:alarm] floats.i:11: Warning:
non-finite float value.
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
index eda04cca2f426021910934e62da87f3285e2738f..02aa64405ee8998bf36a0656966d25223fd3f65a 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
@@ -18,7 +18,7 @@
no \from part for clause
'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'.
Assuming \from \nothing so that the analysis can continue, but be aware this is probably incorrect.
-[eva:alarm] <unknown location> Warning:
+[eva:alarm] <unknown location>: Warning:
function square_root_aux, behavior Buchi_property_behavior: postcondition got status unknown.
[eva:alarm] floats.i:11: Warning:
non-finite float value.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle
index 331bf238f1a73f1804813a41a043fe082d8b44c5..15bc5adac0dfb7366faed69d3c4a8963e50b1888 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] <unknown location> Warning:
+[eva:alarm] <unknown location>: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] issue-framac-1119.c:10: Warning:
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 abd81c8221875403a618a45bd81066104ceb1186..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,5 +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. 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/oracle/wp_call_pre.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
index 631d75f827d420ae2c29786b4c8fc31f18750369..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,5 +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. 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/oracle/wp_call_pre.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
index d9d2494634c67b2e7ba783f6f935dd48f757c76c..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,5 +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. 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/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
index 77cbd8d8902446fa20846f04d51e990a5230d8dc..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,5 +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. 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/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 d5852e56a1789c285c609b16d212a2cf833ced2d..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,5 +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. See above messages for more information.
+[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 f3b4277224c93fb69cbb10608120722ec1f105cf..5312ba5fb8e460f4897136f24a9dd288441426d4 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -37,5 +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. See above messages for more information.
+[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 b57f33e7f5f5c58944585e439afcaaf45c51dd11..1057a06adddb17f429a2b8f456f2cfa518896936 100644
--- a/tests/cil/oracle/ghost_cfg.1.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.1.res.oracle
@@ -1,5 +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. See above messages for more information.
+[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 f7d982e9f13f7f2910553db3af0c8978c792bb6c..6073d7fb31cea02c9d062f6922e56b9b8316543a 100644
--- a/tests/misc/oracle/debug_category.14.res.oracle
+++ b/tests/misc/oracle/debug_category.14.res.oracle
@@ -3,5 +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. See above messages for more information.
+[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 b33ecc559a42c3b34bcbacc30b92a4fa569cf051..a29ab32fe7aa9d67047a378568d520af0b060890 100644
--- a/tests/misc/oracle/debug_category.15.res.oracle
+++ b/tests/misc/oracle/debug_category.15.res.oracle
@@ -3,5 +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. See above messages for more information.
+[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 6857c762cdb581b0e618826742415ce950b0b6b1..29bcf983ee6ab3dd3f984e7a43306bb82b6a89ac 100644
--- a/tests/misc/oracle/debug_category.16.res.oracle
+++ b/tests/misc/oracle/debug_category.16.res.oracle
@@ -2,5 +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 64448bd5bd4427d7ac9cf9d550df0bb57d79048c..ebfdc38a7f55719c99e8da0d3c660a5388d97e14 100644
--- a/tests/misc/oracle/debug_category.17.res.oracle
+++ b/tests/misc/oracle/debug_category.17.res.oracle
@@ -3,7 +3,8 @@
[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.
+[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 66200a611dba982af8261ffa538670a8f3908d45..54dab8c4e1c9a50812e03c57b9b59dd89092ae61 100644
--- a/tests/misc/oracle/debug_category.8.res.oracle
+++ b/tests/misc/oracle/debug_category.8.res.oracle
@@ -2,5 +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. See above messages for more information.
+[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.0.res.oracle b/tests/spec/oracle/Extend_errors.0.res.oracle
index 1cd048aac0469548c28d44a6a86bd09efa947bf6..3a2a7d677657142048d8273c2931bf78c85f4fc2 100644
--- a/tests/spec/oracle/Extend_errors.0.res.oracle
+++ b/tests/spec/oracle/Extend_errors.0.res.oracle
@@ -24,11 +24,11 @@
[kernel:acsl-extension] Warning:
Trying to register ACSL extension unfold reserved by frama-c. Rename this extension to avoid conflict with the kernel. Ignored extension
[kernel] Triggering User Error :
-[kernel] <unknown location> User Error:
+[kernel] <unknown location>: User Error:
Conflicts on extension named 'foo' registered by different plugins (myplugin2,
myplugin1), use '\plugin::ext_name' syntax to avoid this ambiguity
[kernel] Triggering Unsupported :
-[kernel] <unknown location> Failure:
+[kernel] <unknown location>: Failure:
Unsupported clause extension named '\myplugin1::bar'
[kernel] Parsing Extend_errors.c (with preprocessing)
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/Extend_errors.3.res.oracle b/tests/spec/oracle/Extend_errors.3.res.oracle
index c12d7dc67efde446c9feaab6790b0eebbe0c0ffe..51589b3dc9993ff77318185a3469357edd6be5c9 100644
--- a/tests/spec/oracle/Extend_errors.3.res.oracle
+++ b/tests/spec/oracle/Extend_errors.3.res.oracle
@@ -4,5 +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. See above messages for more information.
+[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 67fa872774041b03672abbc5648fda68da0896f8..6c46069e65f6e80519e78624db7b7d0741cb2843 100644
--- a/tests/spec/oracle/import_errors.2.res.oracle
+++ b/tests/spec/oracle/import_errors.2.res.oracle
@@ -2,5 +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. See above messages for more information.
+[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 fba570a595ecc22384efbab28e1cb41a2cc58d5a..512a05613c560f577b616371a6f59e54cb7bc545 100644
--- a/tests/spec/oracle/import_errors.3.res.oracle
+++ b/tests/spec/oracle/import_errors.3.res.oracle
@@ -2,5 +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. See above messages for more information.
+[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 2f08c1db2a30eaf2d8c55dbf6f5afad12a153c21..6affd1fe76856012bfef0df5395fef33c949869c 100644
--- a/tests/syntax/oracle/cert_msc_38.1.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.1.res.oracle
@@ -1,5 +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. See above messages for more information.
+[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 fe19cf1bb736df3777123bdfcf4b2f939dc4d1af..9053bad7caeeae6b337bb484752ede57989175fd 100644
--- a/tests/syntax/oracle/cert_msc_38.2.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.2.res.oracle
@@ -1,5 +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. See above messages for more information.
+[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 e4f28025579f70f1ac20a1113b04fc604ce3d881..336bd2392f78f9646cec732a94dec7560951db3e 100644
--- a/tests/syntax/oracle/cert_msc_38.7.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.7.res.oracle
@@ -1,5 +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. See above messages for more information.
+[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 2e709e806388d3d2de3d29704a72a1f3579083b9..e35d4ba7926deebc91a2cc76689f766965bd0b15 100644
--- a/tests/syntax/oracle/ghost_cv_incompat.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_incompat.res.oracle
@@ -93,5 +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. See above messages for more information.
+[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 daaa1f8c77466c6e7bc074e39cac24b2e864f0e7..e0d860d893f5482d2983a33c830e67c0e03f2613 100644
--- a/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
@@ -57,5 +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. See above messages for more information.
+[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 5a8bba7de39ff6df5c6fd0f648ddc17b38692e7e..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,5 +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. See above messages for more information.
+[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/ghost_cv_var_decl.1.res.oracle b/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
index 67d1b6a0498df79b11293e369e1ef58b20531331..9f276448f22f09f22185eede5334a359cc20b15f 100644
--- a/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
@@ -173,21 +173,21 @@
c: ghost
[kernel] ghost_cv_var_decl.c:186
bar_1: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal
[kernel] ghost_cv_var_decl.c:187
bar_2: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal
-[kernel] :0
+[kernel] <unknown location>
b: ghost
[kernel] ghost_cv_var_decl.c:188
bar_3: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal
-[kernel] :0
+[kernel] <unknown location>
b: ghost
-[kernel] :0
+[kernel] <unknown location>
c: ghost
[kernel] ghost_cv_var_decl.c:190
pfoo_1: normal
@@ -209,21 +209,21 @@
c: ghost -> normal
[kernel] ghost_cv_var_decl.c:202
pbar_1: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal -> normal
[kernel] ghost_cv_var_decl.c:203
pbar_2: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal
-[kernel] :0
+[kernel] <unknown location>
b: ghost -> normal
[kernel] ghost_cv_var_decl.c:204
pbar_3: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal
-[kernel] :0
+[kernel] <unknown location>
b: ghost -> ghost
-[kernel] :0
+[kernel] <unknown location>
c: ghost -> normal
[kernel] ghost_cv_var_decl.c:206
afoo_1: normal
@@ -243,19 +243,19 @@
b: ghost -> ghost
[kernel] ghost_cv_var_decl.c:218
abar_1: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal -> normal
[kernel] ghost_cv_var_decl.c:219
abar_2: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal
-[kernel] :0
+[kernel] <unknown location>
b: ghost -> ghost
[kernel] ghost_cv_var_decl.c:220
abar_3: normal
-[kernel] :0
+[kernel] <unknown location>
a: normal
-[kernel] :0
+[kernel] <unknown location>
b: ghost -> ghost
[kernel] ghost_cv_var_decl.c:223
reference_functions: normal
diff --git a/tests/syntax/oracle/too_large_array.res.oracle b/tests/syntax/oracle/too_large_array.res.oracle
index c5df2b706f22b915013c35ed485c5bfbcc44301b..d5d9b4e03f57e739e40aabb0c46b7cb9024ca115 100644
--- a/tests/syntax/oracle/too_large_array.res.oracle
+++ b/tests/syntax/oracle/too_large_array.res.oracle
@@ -3,5 +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. See above messages for more information.
+[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 3270a28dd6f5ba3e83b7c88e4fb0e848db680b77..814f106104f15d6c5002db330dd3a0591e525d13 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -29,5 +29,6 @@
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
-[kernel] Warning: warning annot-error treated as deferred error. See above messages for more information.
+[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 7c23fb2f46bdc345a531f6c51dd40c56e694ed4a..ee2372e951710bca47f897e146a0bd4d82277f30 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -50,5 +50,8 @@
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. See above messages for more information.
+[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.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle
index 942c944e4ecaa136ff3b103a4c2a9a2fa22292fb..25c745dd936f56f16d6154fba07ad8bc1de8fd6f 100644
--- a/tests/value/oracle/use_spec.0.res.oracle
+++ b/tests/value/oracle/use_spec.0.res.oracle
@@ -74,5 +74,6 @@
x; y
Sure outputs:
w; z
-[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information.
+[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 ceeb03a639742555ef684cd431159b8abe3c0bc6..9d2c754b2e6e34babac58ff50d3ebb39c5a04e4b 100644
--- a/tests/value/oracle/use_spec.1.res.oracle
+++ b/tests/value/oracle/use_spec.1.res.oracle
@@ -74,5 +74,6 @@
x; y
Sure outputs:
w; z
-[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information.
+[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 3e0140e510878b7c47e20684214c596823298e18..794562d8b449ee76cf3ba291f4a5c60ee2330375 100644
--- a/tests/value/oracle/va_list.1.res.oracle
+++ b/tests/value/oracle/va_list.1.res.oracle
@@ -30,5 +30,6 @@
vlParameters; tmp
[inout] Inputs for function main:
\nothing
-[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[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.