From 3c61af04f77867fabcdff2d5dbc9c627770120cb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 4 Feb 2021 10:01:27 +0100
Subject: [PATCH] [Dive] use Filepath parameters for relevant options
---
src/plugins/dive/main.ml | 16 ++++++++--------
src/plugins/dive/self.ml | 16 ++++++++++------
src/plugins/dive/self.mli | 4 ++--
src/plugins/dive/tests/test_config | 2 +-
4 files changed, 21 insertions(+), 17 deletions(-)
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index 73873991216..c90fcad5e55 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -22,13 +22,13 @@
type format = Dot | Json
-let output format context basename =
- let filename, output_function = match format with
- | Dot -> basename ^ ".dot", Dive_graph.ouptput_to_dot
- | Json -> basename ^ ".json", Dive_graph.ouptput_to_json
+let output format context filename =
+ let output_function = match format with
+ | Dot -> Dive_graph.ouptput_to_dot
+ | Json -> Dive_graph.ouptput_to_json
in
- Self.result "output to %s" filename;
- let out_channel = open_out filename in
+ Self.result "output to %a" Filepath.Normalized.pretty filename;
+ let out_channel = open_out (filename:>string) in
output_function out_channel (Context.get_graph context);
close_out out_channel
@@ -57,9 +57,9 @@ let main () =
if not (Self.FromFunctionAlarms.is_empty ()) then
Alarms.iter add_alarm;
(* Output it *)
- if Self.OutputDot.get () <> "" then
+ if Self.OutputDot.is_known () then
output Dot context (Self.OutputDot.get ());
- if Self.OutputJson.get () <> "" then
+ if Self.OutputJson.is_known () then
output Json context (Self.OutputJson.get ());
end
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 26a925a3f54..ba3fd755c8f 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -29,18 +29,22 @@ include Plugin.Register
let help = "An interactive imprecision graph generator for Eva."
end)
-module OutputDot = Empty_string
+module OutputDot = Filepath
(struct
let option_name = "-dive-output-dot"
- let help = "Outputs the built graph into a dot file with this basename."
- let arg_name = "basename"
+ let arg_name = "output.dot"
+ let file_kind = "DOT"
+ let existence = Fc_Filepath.Indifferent
+ let help = "Outputs the built graph in DOT format to the specified file."
end)
-module OutputJson = Empty_string
+module OutputJson = Filepath
(struct
let option_name = "-dive-output-json"
- let help = "Outputs the built graph into a json file with this basename."
- let arg_name = "basename"
+ let arg_name = "output.json"
+ let file_kind = "JSON"
+ let existence = Fc_Filepath.Indifferent
+ let help = "Outputs the built graph in JSON format to the specified."
end)
module DepthLimit = Int
diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli
index cb501498246..664546c1cc6 100644
--- a/src/plugins/dive/self.mli
+++ b/src/plugins/dive/self.mli
@@ -26,8 +26,8 @@ module type Varinfo_set = Parameter_sig.Set
with type elt = Cil_types.varinfo
and type t = Cil_datatype.Varinfo.Set.t
-module OutputDot : Parameter_sig.String
-module OutputJson : Parameter_sig.String
+module OutputDot : Parameter_sig.Filepath
+module OutputJson : Parameter_sig.Filepath
module DepthLimit : Parameter_sig.Int
module FromFunctionAlarms : Parameter_sig.Kernel_function_set
module FromBases : Varinfo_set
diff --git a/src/plugins/dive/tests/test_config b/src/plugins/dive/tests/test_config
index 9ff93873375..b5de8cfbedf 100644
--- a/src/plugins/dive/tests/test_config
+++ b/src/plugins/dive/tests/test_config
@@ -1,3 +1,3 @@
LOG: @PTEST_NAME@.dot
-OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope,dive -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output-dot @PTEST_RESULT@/@PTEST_NAME@
+OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope,dive -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output-dot @PTEST_RESULT@/@PTEST_NAME@.dot
FILTER: perl -0777 -pe 's/\[server[^[]*//g'
--
GitLab