[Kernel] slightly reformulate deferred error messages

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:"

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

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.

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.

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.

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.

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.

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.

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.

tests/cil/oracle/ghost_cfg.1.res.oracle

 [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.

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.

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.

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.

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:

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.

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]
 

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.

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.

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.

tests/syntax/oracle/cert_msc_38.1.res.oracle

 [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.