Skip to content
Snippets Groups Projects
Commit b0c6c070 authored by Thibault Martin's avatar Thibault Martin
Browse files

[kernel] Avoid printing :0: in case of unknown loc

parent 6d05eb23
No related branches found
No related tags found
No related merge requests found
......@@ -241,12 +241,15 @@ let rec echo_lines ?(prefix=false) output text p q =
let add_source buffer = function
| None -> ()
| Some src ->
begin
(* 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 ": " ;
Buffer.add_string buffer ": "
end
let add_category buffer = function
......
......@@ -17,7 +17,7 @@
[eva] floats.i:6: Warning:
no \from part
for clause 'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'
[eva:alarm] :0: 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.
......
......@@ -17,7 +17,7 @@
[eva] floats.i:6: Warning:
no \from part
for clause 'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'
[eva:alarm] :0: 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.
......
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] :0: 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:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment