Merge branch 'feature/kernel/reprint-deferred-error' into 'master'

[kernel] Log: at the end of Frama-C execution, re-print deferred error (if any).

See merge request frama-c/frama-c!4876

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                                                 --- *)

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
 

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.

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.

src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle

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

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

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.

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.

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.

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

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.

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

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.

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.

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.

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:
   

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.

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]