diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml index 60e196d6d4909d84e459ac13dd54c85c1a6031c0..38a9e97129761c0fae3e4dae9a1904f9c1e6b3be 100644 --- a/src/plugins/wp/Why3Provers.ml +++ b/src/plugins/wp/Why3Provers.ml @@ -26,7 +26,8 @@ let cfg = lazy begin - try Why3.Whyconf.init_config None + let extra_config = Wp_parameters.Why3ExtraConfig.get () in + try Why3.Whyconf.init_config ~extra_config None with exn -> Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn end diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml index 5a63447c8844bb2ea82f7bdb07887248f54d53e8..23ff0dda57c622e47b57170e242faee62c225069 100644 --- a/src/plugins/wp/wp_parameters.ml +++ b/src/plugins/wp/wp_parameters.ml @@ -983,6 +983,16 @@ module Why3Flags = let help = "Additional options for Why3" end) +let () = Parameter_customize.set_group wp_prover_options +let () = Parameter_customize.no_category () +module Why3ExtraConfig = + String_list + (struct + let option_name = "-wp-why3-extra-config" + let arg_name = "file,..." + let help = "Additional config files for Why3" + end) + (* ------------------------------------------------------------------------ *) (* --- PO Management --- *) (* ------------------------------------------------------------------------ *) diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli index 74e6e0376c6e09feb6272c801f8ad3d73d887be1..786bf2d170668267ba39a507a078806ac18793de 100644 --- a/src/plugins/wp/wp_parameters.mli +++ b/src/plugins/wp/wp_parameters.mli @@ -136,6 +136,7 @@ module Steps: Parameter_sig.Int module Procs: Parameter_sig.Int module ProofTrace: Parameter_sig.Bool module Why3Flags: Parameter_sig.String_list +module Why3ExtraConfig: Parameter_sig.String_list module Auto: Parameter_sig.String_list module AutoDepth: Parameter_sig.Int