diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml index 75acb89eb4d1ed53cd438c23c2e0af51e3e6fcd8..ae596bfe1f4424c1a2d3ac04570e63cb69c61892 100644 --- a/src/plugins/metrics/metrics_acsl.ml +++ b/src/plugins/metrics/metrics_acsl.ml @@ -309,9 +309,9 @@ let dump_acsl_stats_html fmt = let dump () = let out = Metrics_parameters.OutputFile.get () in - if out <> "" then begin + if not (Filepath.Normalized.is_unknown out) then begin try - let chan = open_out out in + let chan = open_out (out:>string) in let fmt = Format.formatter_of_out_channel chan in (match Metrics_base.get_file_type out with | Metrics_base.Html -> dump_acsl_stats_html fmt @@ -322,6 +322,7 @@ let dump () = ); close_out chan with Sys_error s -> - Metrics_parameters.abort "Cannot open file %s (%s)" out s + Metrics_parameters.abort "Cannot open file %a (%s)" + Filepath.Normalized.pretty out s end else Metrics_parameters.result "%t" dump_acsl_stats diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml index a29fdada1c39483d090761c6af07185d31df7d24..4555837a8811f08bce4a738427e8625889174f41 100644 --- a/src/plugins/metrics/metrics_base.ml +++ b/src/plugins/metrics/metrics_base.ml @@ -251,9 +251,9 @@ type output_type = | Json ;; -let get_file_type filename = +let get_file_type (filename : Filepath.Normalized.t) = try - match get_suffix filename with + match get_suffix (filename:>string) with | "html" | "htm" -> Html | "txt" | "text" -> Text | "json" -> Json @@ -263,7 +263,8 @@ let get_file_type filename = with | No_suffix -> Metrics_parameters.abort - "File %s has no suffix. Cannot produce output.@." filename + "File %a has no suffix. Cannot produce output.@." + Filepath.Normalized.pretty filename module VarinfoByName = struct type t = Cil_types.varinfo diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli index f4c84845ca1c4ca177dd1c2fbd555e0cec255d88..a93c078c04ecda52d352be849d92e39e9da8174a 100644 --- a/src/plugins/metrics/metrics_base.mli +++ b/src/plugins/metrics/metrics_base.mli @@ -146,7 +146,7 @@ type output_type = (** get_file_type [extension] sets the output type according to [extension]. Raises an error if [extension] is not among supported extensions or is empty. *) -val get_file_type: string -> output_type;; +val get_file_type: Filepath.Normalized.t -> output_type;; (** consider_function [vinfo] returns false if the varinfo is not a function we are interested in. diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml index 962ed38461e91ff9f4f4e810d6cd14f4b026b7bb..fa6e6231852d99e964702cb164e3ebf53a88ed7e 100644 --- a/src/plugins/metrics/metrics_cilast.ml +++ b/src/plugins/metrics/metrics_cilast.ml @@ -736,9 +736,9 @@ let compute_on_cilast ~libc = (* Print the result to file if required *) let out_fname = Metrics_parameters.OutputFile.get () in begin - if out_fname <> "" then + if not (Filepath.Normalized.is_unknown out_fname) then try - let oc = open_out_bin out_fname in + let oc = open_out_bin (out_fname:>string) in let fmt = Format.formatter_of_out_channel oc in (match Metrics_base.get_file_type out_fname with | Html -> dump_html fmt cil_visitor @@ -750,7 +750,8 @@ let compute_on_cilast ~libc = ); close_out oc; with Sys_error _ -> - Metrics_parameters.failure "Cannot open file %s.@." out_fname + Metrics_parameters.failure "Cannot open file %a.@." + Filepath.Normalized.pretty out_fname else Metrics_parameters.result "%a" pp_with_funinfo cil_visitor end diff --git a/src/plugins/metrics/metrics_parameters.ml b/src/plugins/metrics/metrics_parameters.ml index 30ae2ef4d389e1a3db3a9e0f5e8fe3e35c7ac1bd..5aeae5dc6886cb3b151c7a285471a7421f72e207 100644 --- a/src/plugins/metrics/metrics_parameters.ml +++ b/src/plugins/metrics/metrics_parameters.ml @@ -44,10 +44,12 @@ module ByFunction = end) module OutputFile = - Empty_string + Filepath (struct let option_name = "-metrics-output" let arg_name = "filename" + let file_kind = "Text, HTML or JSON" + let existence = Fc_Filepath.Indifferent let help = "print some metrics into the specified file; \ the output format is recognized through the extension: \ .text/.txt for text, .html/.htm for HTML, or .json for JSON." diff --git a/src/plugins/metrics/metrics_parameters.mli b/src/plugins/metrics/metrics_parameters.mli index bc9a5e556236fb042b721a5f4bed701c44b00db8..990c31c6751adcd6cd7eced29131fc2f796fb0ae 100644 --- a/src/plugins/metrics/metrics_parameters.mli +++ b/src/plugins/metrics/metrics_parameters.mli @@ -35,7 +35,7 @@ module ValueCoverage: Parameter_sig.With_output module AstType: Parameter_sig.String (** Set the ASTs on which the metrics should be computed *) -module OutputFile: Parameter_sig.String +module OutputFile: Parameter_sig.Filepath (** Pretty print metrics to the given file. The output format will be recognized through the extension. Supported extensions are: