diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index c3456688d68f94611757c0b3ebda22fee7812886..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 -> ()
@@ -584,11 +576,7 @@ let deferred_raise ~fatal event msg =
(* reset deferred flag. *)
let () = deferred_exn := DNo_exn in
let channel = new_channel event.evt_plugin in
- let pp_pos fmt pos =
- if Filepath.is_empty_pos pos
- then Format.fprintf fmt "<unknown location> "
- else Format.fprintf fmt "%a: " Filepath.pp_pos pos
- in
+ 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
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/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/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