[Dive] use Filepath parameters for relevant options

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
 

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

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

src/plugins/dive/tests/test_config

 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'