[wp] Add option for region dump files

src/plugins/wp/RegionAnalysis.ml

@@ -97,11 +97,16 @@ let main () =
   if Wp.Region.get () then
     begin
       Ast.compute () ;
-      let dir = Wp.get_output_dir "region" in
+      let dump =
+        if Wp_parameters.Region_output_dot.is_set () then
+          RegionDump.dump_in_file ~file:(Wp_parameters.Region_output_dot.get())
+        else
+          RegionDump.dump_in_dir ~dir:(Wp.get_output_dir "region")
+      in
       Wp.iter_kf (fun kf ->
           let map = get (Some kf) in
           if not (Region.is_empty map) then
-            RegionDump.dump ~dir kf map
+            dump (Kernel_function.get_name kf) map
         ) ;
     end
 

src/plugins/wp/RegionDump.ml

@@ -21,7 +21,6 @@
 (**************************************************************************)
 
 module Wp = Wp_parameters
-module Kf = Kernel_function
 module G = Dotgraph
 module R = G.Node(Region.Map)
 
@@ -279,13 +278,10 @@ let dotgraph dot map =
     G.run dot ;
   end
 
-let dump ~dir kf map =
+let dump_in_file ~file name map =
   if Wp.has_dkey dot_key || Wp.has_dkey pdf_key then
     begin
-      let name = Kf.get_name kf in
-      let file =
-        Format.asprintf "%a/%s.dot" Datatype.Filepath.pretty dir name
-      in
+      let file = Format.asprintf "%a" Datatype.Filepath.pretty file in
       let dot = Dotgraph.open_dot ~attr:[`LR] ~name ~file () in
       dotgraph dot map ;
       Dotgraph.close dot ;
@@ -295,3 +291,7 @@ let dump ~dir kf map =
         else file in
       Wp.result "Region Graph: %s" outcome
     end
+
+let dump_in_dir ~dir name map =
+  let file = Datatype.Filepath.concat dir (name ^ ".dot") in
+  dump_in_file ~file name map

src/plugins/wp/RegionDump.mli

@@ -23,4 +23,6 @@
 (* Dump region graphs to dir according to -wp options.
    By default, does nothing. *)
 
-val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> Region.map -> unit
+val dump_in_dir : dir:Datatype.Filepath.t -> string -> Region.map -> unit
+
+val dump_in_file : file:Datatype.Filepath.t -> string -> Region.map -> unit

src/plugins/wp/wp_parameters.ml

@@ -357,6 +357,17 @@ module Region_annot =
       let help = "Register '@region' ACSL Annotations (auto with -wp-region)"
     end)
 
+let () = Parameter_customize.set_group wp_region
+module Region_output_dot =
+  Filepath
+    (struct
+      let option_name = "-wp-region-output-dot"
+      let arg_name = "output.dot"
+      let file_kind = "DOT"
+      let existence = Fc_Filepath.Indifferent
+      let help = "Outputs the region graph in DOT format to the specified file."
+    end)
+
 (* ------------------------------------------------------------------------ *)
 (* ---  WP Strategy                                                     --- *)
 (* ------------------------------------------------------------------------ *)

src/plugins/wp/wp_parameters.mli

@@ -71,6 +71,7 @@ module Region_annot: Parameter_sig.Bool
 module Region_inline: Parameter_sig.Bool
 module Region_fixpoint: Parameter_sig.Bool
 module Region_cluster: Parameter_sig.Bool
+module Region_output_dot : Parameter_sig.Filepath
 
 (** {2 Computation Strategies} *)