Merge branch 'feature/wp/why3-extra-config' into 'master'

[WP] extra config files for Why3

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

src/plugins/wp/Changelog

@@ -24,6 +24,9 @@
 Plugin WP <next-release>
 ########################
 
+- WP          [2023-02-03] new option -wp-why3-extra-config for providing
+                           additional Why3 configuration files
+
 #####################
 Plugin WP 26.0 (Iron)
 #####################

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
@@ -41,8 +42,12 @@ let configure =
   begin fun () ->
     if !todo then
       begin
-        let args = Array.of_list ("why3"::Wp_parameters.Why3Flags.get ()) in
+        let commands = "why3"::Wp_parameters.Why3Flags.get () in
+        let args = Array.of_list commands in
         begin try
+            (* Ensure that an error message generating directly by why3 is
+               reported as coming from Why3, not from Frama-C. *)
+            Why3.Getopt.commands := commands;
             Why3.Getopt.parse_all
               (Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list])
               (fun opt -> raise (Arg.Bad ("unknown option: " ^ opt)))

src/plugins/wp/doc/manual/wp_plugin.tex

@@ -1346,6 +1346,8 @@ See \texttt{-wp-interactive <mode>} option for details.
   steps. This can be used as a machine-independent alternative to timeout.
 \item[\tt -wp-why3-opt='options,...'] provides additional options to the
   \verb+why3+ command.
+\item[\tt -wp-why3-extra-config='files,...'] provides additional configuration
+  files for \verb+why3+.
 \item[\tt -wp-prepare-scripts] initialize a script tracking directory in the
   session directory.
 \item[\tt -wp-finalize-scripts] remove untracked scripts according to the

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                                                    --- *)
 (* ------------------------------------------------------------------------ *)

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