diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml index 75d6995d2cd6cf56d580e45ee65fdac12e2e135f..d4d26927c93a8a7954ae98083adc2ad45f54c923 100644 --- a/src/kernel_services/plugin_entry_points/log.ml +++ b/src/kernel_services/plugin_entry_points/log.ml @@ -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 diff --git a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle index 24d6bd3cd5dfaa04bddfe39192acb4c215da9cb3..11062e0fd83fdbe5c227b400a6eaa1209e8af14f 100644 --- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle @@ -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. 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 516e8f70da093aa6abf13e8e49a7932508dfe2ff..8688011acc97bb434e94372d224c53e917b51b99 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle @@ -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. 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 07a2f42bf48fe04064bda92c5fd5d3e4a181859f..331bf238f1a73f1804813a41a043fe082d8b44c5 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] :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: