diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml index 6cef7e541ab3fe1d2e2f7b6e0c97343e2bd64307..eee8a7cb2c7ddb645508dbc005c53d62271f402e 100644 --- a/src/plugins/metrics/metrics_cilast.ml +++ b/src/plugins/metrics/metrics_cilast.ml @@ -747,9 +747,9 @@ let compute_on_cilast ~libc = Format.fprintf fmt "@." (* ensure the file ends with a newline *) ); close_out oc; - with Sys_error _ -> - Metrics_parameters.failure "Cannot open file %a.@." - Filepath.Normalized.pretty out_fname + with Sys_error s -> + Metrics_parameters.abort "Cannot open file %a (%s)." + Filepath.Normalized.pretty out_fname s end else Metrics_parameters.result "%a" pp_with_funinfo cil_visitor