diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index 7e9a943a7568dca9853659718c92cfbd0e1e03b4..21ebb113667d4ced7fe086951a3d1b078a7e5b4a 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/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
diff --git a/src/plugins/wp/RegionDump.ml b/src/plugins/wp/RegionDump.ml
index fd7ce7f2d612527ca39985931ffbe17cc60d58e8..acd421a0e7baeeb4c3a85f9066ae7cfbe8973a9b 100644
--- a/src/plugins/wp/RegionDump.ml
+++ b/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
diff --git a/src/plugins/wp/RegionDump.mli b/src/plugins/wp/RegionDump.mli
index 055a8797a4261a6a63aa7549238622403eaba20d..81804e946b51971c04e763a2538ad7cdffe28a87 100644
--- a/src/plugins/wp/RegionDump.mli
+++ b/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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array1/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array1.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array1/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array1.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle
index 81f1736f1ad75ca3308290d56fd71bd8785d2368..f594dcb8a6c44253248bd7915208a98c026474a0 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array2/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array2.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array2/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array2.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle
index 68f76fba80967aeb150d39872d6ca52f73f4fa05..493acb0f32107b413f25d1e04f2ad9358d77e7fc 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array3/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array3.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array3/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array3.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle
index f8d1b288590c82f859ac22234b438fe545415d0f..ff1d6ff8c4774317d4469a6f9a31d287a36c489e 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array4/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array4.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array4/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array4.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle
index 566bc12ae36a7ade9b5a2c2b19584796cbb9ee40..a98da77e19cd9c9eb3fc069ff3394fd087dc3d1e 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array5/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array5.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array5/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array5.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle
index 6e7cda1dedd75ff1706fc5f45b5f546eae950b23..49fd11f80bd23706ec5b54ff355c2fcd1775e119 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array6/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array6.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array6/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array6.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle
index a63a1285b245bb4f4ddf25acad6297d10ee33ec4..814e494ce84b36a29c84ac8253300456d1127889 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array7/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array7.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array7/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array7.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle
index 27e44f159cfaa4f38ac95cf56a9e466c2e25887f..8bd34f4ece859e898fb01537baec9fe233b95f96 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/array8/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/array8.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/array8/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/array8.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle
index f3518bbdce3e5799ac52b4ca5e337a1913df22af..045b9aa75392eb340e5721978817f7c314f76137 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/fb_ADD.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/fb_ADD/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/fb_ADD.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle b/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle
index ba8de5862e6a7dd586be174f3742ce0f935c0e7d..c174f1f4537b111fc04000bee0674114dd058fd4 100644
--- a/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing fb_ADD.i (no preprocessing)
-[wp] Region Graph: fb_ADD/region/job.dot
+[wp] Region Graph: fb_ADD.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/fb_SORT.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/fb_SORT/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/fb_SORT.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle b/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle
index efe7aeea12460a0f6fa89fd129e444b97c9fb304..bfcc8d4d3ca21cf73c28dcb50c0f414a8ac16774 100644
--- a/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing fb_SORT.i (no preprocessing)
-[wp] Region Graph: fb_SORT/region/job.dot
+[wp] Region Graph: fb_SORT.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/garbled/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/garbled.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/garbled/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/garbled.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle b/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle
index c71df0a7cab59ac8ee774285d7268085fb9bd0df..c390ec3e2ade1fc8b4890a2f7602092b90108f78 100644
--- a/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle
@@ -2,6 +2,6 @@
[wp:garbled] Garbled Clusters: A=sint32 B=float32
[wp:garbled] Garbled Clusters: A=garbled B=sint32
[wp:garbled] Garbled Clusters: A=garbled B=float32
-[wp] Region Graph: garbled/region/job.dot
+[wp] Region Graph: garbled.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/index/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/index.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/index/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/index.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/index.res.oracle b/src/plugins/wp/tests/wp_region/oracle/index.res.oracle
index a0ba6fc1f329968c769b0d6c56eb7ee51e138230..953037c02faad26a8582d6e58dfd2e5f879cff63 100644
--- a/src/plugins/wp/tests/wp_region/oracle/index.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/index.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing index.i (no preprocessing)
-[wp] Region Graph: index/region/job.dot
+[wp] Region Graph: index.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/matrix/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/matrix.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/matrix/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/matrix.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle b/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle
index 9a80a89290a1020f68c01abaa38a1d38b41f4483..01ca9097b9dfeb8be0bd47e99aa5de6975d8931e 100644
--- a/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing matrix.i (no preprocessing)
-[wp] Region Graph: matrix/region/job.dot
+[wp] Region Graph: matrix.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray1/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/structarray1.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/structarray1/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/structarray1.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle
index 61322c7a4d1ae20370584686a9c3707f4be9076c..393a63b149847c622bb8740e221e706652f5e603 100644
--- a/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing structarray1.i (no preprocessing)
-[wp] Region Graph: structarray1/region/job.dot
+[wp] Region Graph: structarray1.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray2/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/structarray2.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/structarray2/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/structarray2.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle
index 09e282b8fe8c547e40ac0a89fb5cb0ccf0b78274..f71c9e902cc6a49c9f5b16bf570b5fd58216c719 100644
--- a/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing structarray2.i (no preprocessing)
-[wp] Region Graph: structarray2/region/job.dot
+[wp] Region Graph: structarray2.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray3/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/structarray3.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/structarray3/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/structarray3.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle
index a8fd572b018915092e99a973199148591126fe72..1e7d3cfb40046d4e352658865cad70b70e222e9a 100644
--- a/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing structarray3.i (no preprocessing)
-[wp] Region Graph: structarray3/region/job.dot
+[wp] Region Graph: structarray3.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray4/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/structarray4.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/structarray4/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/structarray4.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle
index 3c11e623f76c702da7dc4c05c486ed795e4bb692..0f68a735ae39b5918b9e2fda64ca0d901879e306 100644
--- a/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing structarray4.i (no preprocessing)
-[wp] Region Graph: structarray4/region/job.dot
+[wp] Region Graph: structarray4.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/oracle/swap/region/job.dot b/src/plugins/wp/tests/wp_region/oracle/swap.0.dot
similarity index 100%
rename from src/plugins/wp/tests/wp_region/oracle/swap/region/job.dot
rename to src/plugins/wp/tests/wp_region/oracle/swap.0.dot
diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
index da7dc84114fb29f1f7a99f7a7c01b6c895b7dfec..77078dae158d2c0aab7dffec8982c49d0d4cbeb8 100644
--- a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing swap.i (no preprocessing)
-[wp] Region Graph: swap/region/job.dot
+[wp] Region Graph: swap.0.dot
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
index 95a1509ecb2186f18d78ff6184dc767638359d65..811354a69032f4702350332a084895a6047deefd 100644
--- a/src/plugins/wp/tests/wp_region/test_config
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -1,4 +1,4 @@
PLUGIN: wp,rtegen
CMD: @frama-c@
-LOG: @PTEST_NAME@/region/job.dot
-OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_RESULT@/@PTEST_NAME@ -wp-fct job
+LOG: @PTEST_NAME@.@PTEST_NUMBER@.dot
+OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-region-output-dot @PTEST_RESULT@/@PTEST_NAME@.@PTEST_NUMBER@.dot -wp-fct job
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index e15f6284180c3c5baa486d1ce1334e0f29dc5f25..858b5dcb0f1616f1a2aff888c7ddafbe96cc7b87 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -357,6 +357,18 @@ module Region_annot =
let help = "Register '@region' ACSL Annotations (auto with -wp-region)"
end)
+let () = Parameter_customize.set_group wp_region
+let () = Parameter_customize.is_invisible ()
+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 --- *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 66fce992b0384143fb7607fd4b5cb1cabce4300a..2d40d716772da3218de5e669c68c4f29e0a81efd 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/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} *)