From 7d80a26e2b352c946d18e60a9995011713a4aaa3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 22 Feb 2022 08:27:23 +0100
Subject: [PATCH] [Metrics] fix error message
Use same pattern as in metrics_acsl.ml.
---
src/plugins/metrics/metrics_cilast.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 6cef7e541ab..eee8a7cb2c7 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
--
GitLab