Add global timeout as new command line option.

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 =

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 =

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