Merge branch 'feature/wp/minimize-dune-diff-region' into 'master'

[wp] Minimize dune diff region

See merge request frama-c/frama-c!3618

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 = Pretty_utils.to_string 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/tests/wp_region/oracle/array1.res.oracle

 [kernel] Parsing array1.i (no preprocessing)
-[wp] Region Graph: array1/region/job.dot
+[wp] Region Graph: array1.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards

src/plugins/wp/tests/wp_region/oracle/array2.res.oracle

 [kernel] Parsing array2.i (no preprocessing)
-[wp] Region Graph: array2/region/job.dot
+[wp] Region Graph: array2.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards

src/plugins/wp/tests/wp_region/oracle/array3.res.oracle

 [kernel] Parsing array3.i (no preprocessing)
-[wp] Region Graph: array3/region/job.dot
+[wp] Region Graph: array3.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards

src/plugins/wp/tests/wp_region/oracle/array4.res.oracle

 [kernel] Parsing array4.i (no preprocessing)
-[wp] Region Graph: array4/region/job.dot
+[wp] Region Graph: array4.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards

src/plugins/wp/tests/wp_region/oracle/array5.res.oracle

 [kernel] Parsing array5.i (no preprocessing)
-[wp] Region Graph: array5/region/job.dot
+[wp] Region Graph: array5.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards

src/plugins/wp/tests/wp_region/oracle/array6.res.oracle

 [kernel] Parsing array6.i (no preprocessing)
-[wp] Region Graph: array6/region/job.dot
+[wp] Region Graph: array6.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards

src/plugins/wp/tests/wp_region/oracle/array7.res.oracle

 [kernel] Parsing array7.i (no preprocessing)
-[wp] Region Graph: array7/region/job.dot
+[wp] Region Graph: array7.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards

src/plugins/wp/tests/wp_region/oracle/array8.res.oracle

 [kernel] Parsing array8.i (no preprocessing)
-[wp] Region Graph: array8/region/job.dot
+[wp] Region Graph: array8.0.dot
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards