diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index cafa9a5f1da9f06c0be6fedbffbec0f6e4117543..bc5a6c74469b1fedb830132f43f28c5e83e39ca2 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -87,9 +87,9 @@ module Domain = struct
let post_analysis f =
match f, Value_parameters.NumerorsLogFile.get () with
- | _, s when s = "" -> ()
+ | _, s when Filepath.Normalized.is_unknown s -> ()
| `Value _, s ->
- let log = open_out s in
+ let log = open_out (s:>string) in
let fmt = Format.formatter_of_out_channel log in
List.iter (fun f -> f fmt ()) !Numerors_Value.dprint_callstack ;
close_out log
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index ce718b03ee17ad5b2c30afd9a4d08658f3b5f7ee..408114d15682d5121126bb154111f216bf67c8f6 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -1278,7 +1278,7 @@ module D = struct
Value_parameters.failure "The trace is TOP can't generate code"
| `Value state ->
if not (Value_parameters.TracesDot.is_default ())
- then output_dot (Value_parameters.TracesDot.get ()) state;
+ then output_dot (Value_parameters.TracesDot.get ():>string) state;
if Value_parameters.TracesProject.get ()
then project_of_cfg return_exp state
end
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index 8657a9dae7c99b77cd9bb5e7c11f0b9d33a708bb..550a23adc1628036ef446d3dd056403934d6d300 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -175,8 +175,9 @@ let print_information fmt { loc; kf; alarm; kind; text; status; contexts } =
dir file lnum kf alarm kind contexts status text
let output file =
- Value_parameters.feedback "Listing red statuses in file %s" file;
- let channel = open_out file in
+ Value_parameters.feedback "Listing red statuses in file %a"
+ Filepath.Normalized.pretty file;
+ let channel = open_out (file:>string) in
let fmt = Format.formatter_of_out_channel channel in
Format.pp_set_margin fmt 1000000;
Format.fprintf fmt "@[<v>";
@@ -190,4 +191,4 @@ let output file =
let report () =
let file = Value_parameters.ReportRedStatuses.get () in
- if file <> "" then output file
+ if not (Filepath.Normalized.is_unknown file) then output file
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index e8f0be51619f58a5a7003874680638b01b43d8a4..5d310a3baca88f6d98b4e89edf44a1b55667fb14 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -396,10 +396,10 @@ let start_doing_flamegraph callstack =
| [_] ->
(* Analysis of main *)
let file = Value_parameters.ValPerfFlamegraphs.get () in
- if file <> "" then begin
+ if not (Filepath.Normalized.is_unknown file) then begin
try
(* Flamegraphs must be computed. Set up the stack and the output file *)
- let oc = open_out file in
+ let oc = open_out (file:>string) in
oc_flamegraph := Some oc;
stack_flamegraph := [ (Sys.time (), 0.) ]
with e ->
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index ec4e77fd3ed01fec6b323a0129a6a1f580db8bd0..494a55fc98f21b9986e5d52116d7f3aacecf67aa 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -351,11 +351,13 @@ module TracesUnifyLoop =
let () = add_precision_dep TracesUnifyLoop.parameter
let () = Parameter_customize.set_group domains
-module TracesDot = Empty_string
+module TracesDot = Filepath
(struct
let option_name = "-eva-traces-dot"
- let help = "Output to the given filename the Cfg in dot format."
let arg_name = "FILENAME"
+ let file_kind = "DOT"
+ let existence = Fc_Filepath.Indifferent
+ let help = "Output to the given filename the Cfg in dot format."
end)
let () = Parameter_customize.set_group domains
@@ -1070,14 +1072,15 @@ module ValShowPerf =
let () = Parameter_customize.set_group messages
module ValPerfFlamegraphs =
- String
+ Filepath
(struct
let option_name = "-eva-flamegraph"
+ let arg_name = "file"
+ let file_kind = "Text for flamegraph"
+ let existence = Fc_Filepath.Indifferent
let help = "Dump a summary of the time spent analyzing function calls \
in a format suitable for the Flamegraph tool \
(http://www.brendangregg.com/flamegraphs.html)"
- let arg_name = "file"
- let default = ""
end)
@@ -1103,11 +1106,12 @@ module PrintCallstacks =
let () = Parameter_customize.set_group messages
module ReportRedStatuses =
- String
+ Filepath
(struct
let option_name = "-eva-report-red-statuses"
let arg_name = "filename"
- let default = ""
+ let file_kind = "CSV"
+ let existence = Fc_Filepath.Indifferent
let help = "Output the list of \"red properties\" in a csv file of the \
given name. These are the properties which were invalid for \
some states. Their consolidated status may not be invalid, \
@@ -1116,13 +1120,14 @@ module ReportRedStatuses =
let () = Parameter_customize.set_group messages
module NumerorsLogFile =
- String
+ Filepath
(struct
let option_name = "-eva-numerors-log-file"
+ let arg_name = "file"
+ let file_kind = "Text"
+ let existence = Fc_Filepath.Indifferent
let help = "The Numerors domain will save each call to the DPRINT \
function in the given file"
- let arg_name = "file"
- let default = ""
end)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 3f50d6efaa7990c3c68289b0043e4259bab34ba0..9a6a7172cc20cf89b2a178a6bf40c59cf1e91779 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -42,7 +42,7 @@ module OctagonCall: Parameter_sig.Bool
module TracesUnrollLoop: Parameter_sig.Bool
module TracesUnifyLoop: Parameter_sig.Bool
-module TracesDot: Parameter_sig.String
+module TracesDot: Parameter_sig.Filepath
module TracesProject: Parameter_sig.Bool
module EqualityStorage: Parameter_sig.Bool
@@ -122,11 +122,11 @@ module SplitGlobalStrategy: State_builder.Ref with type data = Split_strategy.t
module ValShowProgress: Parameter_sig.Bool
module ValShowPerf: Parameter_sig.Bool
-module ValPerfFlamegraphs: Parameter_sig.String
+module ValPerfFlamegraphs: Parameter_sig.Filepath
module ShowSlevel: Parameter_sig.Int
module PrintCallstacks: Parameter_sig.Bool
-module ReportRedStatuses: Parameter_sig.String
-module NumerorsLogFile: Parameter_sig.String
+module ReportRedStatuses: Parameter_sig.Filepath
+module NumerorsLogFile: Parameter_sig.Filepath
module MemExecAll: Parameter_sig.Bool