From c55db9cb770b22c4bb36f0e523ecf2ea5381b09d Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 30 Mar 2022 11:21:46 +0200
Subject: [PATCH] Add global timeout as new command line option.
---
src/main.ml | 14 +++++++++-----
src/verification.ml | 3 +--
src/verification.mli | 4 +++-
3 files changed, 13 insertions(+), 8 deletions(-)
diff --git a/src/main.ml b/src/main.ml
index 34ec82cd..9a9b01a8 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -65,10 +65,10 @@ let config detect () =
Whyconf.print_prover Pp.nothing)
provers))
-let verify format loadpath memlimit prover files =
+let verify format loadpath memlimit timeout prover files =
let debug = match Logs.level () with Some Debug -> true | _ -> false in
List.iter
- ~f:(Verification.verify ~debug format loadpath ?memlimit ~prover)
+ ~f:(Verification.verify ~debug format loadpath ?memlimit ?timeout ~prover)
files
let exec_cmd cmdname cmd =
@@ -133,6 +133,10 @@ let verify_cmd =
let doc = "Memory limit (in megabytes)." in
Arg.(value & opt (some int) None & info [ "m"; "memlimit" ] ~doc)
in
+ let timeout =
+ let doc = "Timeout (in seconds)." in
+ Arg.(value & opt (some int) None & info [ "t"; "timeout" ] ~doc)
+ in
let prover =
let doc = "Prover to use." in
Arg.(required & opt (some string) None & info [ "p"; "prover" ] ~doc)
@@ -144,11 +148,11 @@ let verify_cmd =
let man = [ `S Manpage.s_description; `P doc ] in
( Term.(
ret
- (const (fun format loadpath memlimit prover files _ ->
+ (const (fun format loadpath memlimit timeout prover files _ ->
`Ok
(exec_cmd cmdname (fun () ->
- verify format loadpath memlimit prover files)))
- $ format $ loadpath $ memlimit $ prover $ files $ setup_logs)),
+ verify format loadpath memlimit timeout prover files)))
+ $ format $ loadpath $ memlimit $ timeout $ prover $ files $ setup_logs)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
let default_cmd =
diff --git a/src/verification.ml b/src/verification.ml
index 87131c10..ee4d1ded 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -69,12 +69,11 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
Call_provers.print_prover_answer answer
-let verify ?(debug = false) format loadpath ?memlimit ~prover file =
+let verify ?(debug = false) format loadpath ?memlimit ?timeout ~prover file =
let open Why3 in
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env loadpath in
let steplimit = None in
- let timeout = None in
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
let limit =
let memlimit =
diff --git a/src/verification.mli b/src/verification.mli
index fd4c7635..7f53cf82 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -9,6 +9,7 @@ val verify :
string option ->
string list ->
?memlimit:int ->
+ ?timeout:int ->
prover:string ->
string ->
unit
@@ -19,4 +20,5 @@ val verify :
@param format is the [file] format.
@param loadpath is the additional loadpath.
@param memlimit
- is the memory limit (in megabytes) granted to the verification. *)
+ is the memory limit (in megabytes) granted to the verification.
+ @param timeout is the timeout (in seconds) granted to the verification. *)
--
GitLab