diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 8b9ad9940e7b9dc1ae629be631c7198c39a9333e..395f3faead128c1f7ea7edff039dbd19ef888a2c 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,8 @@
Plugin WP <next-release>
########################
+- WP [2022-02-28] New option -wp-fct-timeout, used to customize the
+ provers timeout per function
- WP [2022-02-02] New option -wp-smoke-dead-local-init, smoke tests on
local variables initialization
- WP [2022-01-25] Removed deprecated "native:coq" prover
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index db792f3dc0faaa81d9ad02a501a191dacf7aebd4..f4c15057e358073c9dfb25e06ffd7b13e64cc94f 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -132,17 +132,6 @@ let location file line = {
Lexing.pos_cnum = 0 ;
}
-let timeout ~smoke = function
- | None ->
- if smoke
- then Wp_parameters.SmokeTimeout.get ()
- else Wp_parameters.Timeout.get ()
- | Some t -> t
-
-let stepout = function
- | None -> Wp_parameters.Steps.get ()
- | Some t -> t
-
let pp_file ~message ~file =
if Sys.file_exists file then
Log.print_on_output
diff --git a/src/plugins/wp/ProverTask.mli b/src/plugins/wp/ProverTask.mli
index 04bbbd08f4a0d92f56ab15723265a7e94387764b..9bbf616916535843d903d89ea27a0fb848685516 100644
--- a/src/plugins/wp/ProverTask.mli
+++ b/src/plugins/wp/ProverTask.mli
@@ -54,8 +54,6 @@ val p_until_space : string (** No space group pattern "\\([^ \t\n]*\\)" *)
val location : string -> int -> Lexing.position
-val timeout : smoke:bool -> int option -> int
-val stepout : int option -> int
type logs = [ `OUT | `ERR | `BOTH ]
class virtual command : string ->
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 60d34a27f333dc1096e369cb4547a39337540f03..1791480e5fbd30698f17ac138c3e5fd79f467f16 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -164,11 +164,14 @@ let current () = {
let default = { valid = false ; timeout = None ; stepout = None }
-let get_timeout ~smoke = function
+let get_timeout ?kf ~smoke = function
| { timeout = None } ->
if smoke
then Wp_parameters.SmokeTimeout.get ()
- else Wp_parameters.Timeout.get ()
+ else begin match Option.map Wp_parameters.FctTimeout.find kf with
+ | exception Not_found | None -> Wp_parameters.Timeout.get ()
+ | Some timeout -> timeout
+ end
| { timeout = Some t } -> t
let get_stepout = function
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 2a663cd57c450a88e0d45d17d37c1d4d7d01ef8a..fb3f4bb4fac7d16fd0ff905655a3c77ba3de0810 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -69,7 +69,9 @@ type config = {
val current : unit -> config (** Current parameters *)
val default : config (** all None *)
-val get_timeout : smoke:bool -> config -> int (** 0 means no-timeout *)
+val get_timeout : ?kf:Kernel_function.t -> smoke:bool -> config -> int
+(** 0 means no-timeout *)
+
val get_stepout : config -> int (** 0 means no-stepout *)
(** {2 Results} *)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index be99e86a3eb42d964be8794a86ce264a530c7a66..6db288e5f52cb174e773d53126034997bd183353 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1304,6 +1304,9 @@ See \texttt{-wp-interactive <mode>} option for details.
on proved goals when available (default is: \texttt{no}).
\item[\tt -wp-timeout <n>] sets the timeout (in seconds) for the calls
to the decision prover (defaults to 10 seconds).
+\item[\tt -wp-fct-timeout <f1:t1,f2:t2,...>] customize the timeout for each
+ specified function (\texttt{t1} for \texttt{f1}, \texttt{t2} for \texttt{f2},
+ etc).
\item[\tt -wp-smoke-timeout <n>] sets the timeout (in seconds) for smoke tests
(see \verb+-wp-smoke-tests+, defaults to 5 seconds).
\item[\tt -wp-interactive-timeout <n>] sets the timeout (in seconds) for checking
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index b668298cd66d39c230f7c31b74f2e70e814d2407..ab3da9f90b14a6958b80748b73d6a195eb99278a 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -35,8 +35,12 @@ let dispatch ?(config=VCS.default) mode prover wpo =
| Qed | Tactical -> Task.return VCS.no_result
| Why3 prover ->
let smoke = Wpo.is_smoke_test wpo in
+ let kf = match Wpo.get_scope wpo with
+ | Global -> None
+ | Kf kf -> Some kf
+ in
ProverWhy3.prove
- ~timeout:(VCS.get_timeout ~smoke config)
+ ~timeout:(VCS.get_timeout ?kf ~smoke config)
~steplimit:(VCS.get_stepout config)
~mode ~prover wpo
end
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 899d35209bc245448bceab0b2bf94103048028dc..780f7d2ff64ca948af531c0ab1bd58fbe66fe3d2 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -797,6 +797,29 @@ module Timeout =
"Set the timeout (in seconds) for provers (default: %d)." default
end)
+let () = Parameter_customize.set_group wp_prover
+module FctTimeout =
+ Kernel_function_map
+ (struct
+ include Datatype.Int
+ type key = Cil_types.kernel_function
+ let of_string ~key:_ ~prev:_ s =
+ Option.map
+ (fun s ->
+ try int_of_string s
+ with Failure _ ->
+ raise (Cannot_build ("'" ^ s ^ "' is not an integer")))
+ s
+ let to_string ~key:_ = Option.map string_of_int
+ end)
+ (struct
+ let option_name = "-wp-fct-timeout"
+ let arg_name = "f1:t1,...,fn:tn"
+ let help = "Customize the WP timeout (in secondes) for each specified \
+ function (t1 seconds for f1, t2 for f2, etc)."
+ let default = Kernel_function.Map.empty
+ end)
+
let () = Parameter_customize.set_group wp_prover
module SmokeTimeout =
Int(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 3434739d907fd24c8f65445200b5c041a31400a7..e46a5ab90df74b122dd5ca291df37252e0bea7d0 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -121,6 +121,10 @@ module CacheDir: Parameter_sig.String
module CachePrint: Parameter_sig.Bool
module Drivers: Parameter_sig.String_list
module Timeout: Parameter_sig.Int
+module FctTimeout:
+ Parameter_sig.Map
+ with type key = Cil_types.kernel_function
+ and type value = int
module SmokeTimeout: Parameter_sig.Int
module InteractiveTimeout: Parameter_sig.Int
module TimeExtra: Parameter_sig.Int