diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml index 7387399121640d369c24df0f3323af284fe4c709..c90fcad5e55253035952c10f1de9cfb68fdb7201 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 26a925a3f5475acf84c842e7a8cb0b1ae10672ff..ba3fd755c8f3bf66b9fe0aa6d90141d7dbb9b181 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 cb5014982463f0f11c2adc18224bcc0c5ef1ea47..664546c1cc6887e6ac3a71182c88731e1a6e8eec 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 9ff9387337545ed97c88920ed5c79a722351eaa8..b5de8cfbedf81997ee828999794f2b0c93025bed 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'