diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml index d4c8bb220e3a3c119abdfa520e29957e4556362d..079d3ed76a1ebdb35247e87897c45fa70228679a 100644 --- a/src/driver/call_provers.ml +++ b/src/driver/call_provers.ml @@ -295,6 +295,7 @@ let gen_id = type save_data = { vc_file : string; is_temporary : bool; + redirect : bool; limit : resource_limit; res_parser : prover_result_parser; printer_mapping : Printer.printer_mapping; @@ -303,7 +304,8 @@ type save_data = let regexs : (int, save_data) Hashtbl.t = Hashtbl.create 17 let prove_file_server ~res_parser ~command ~limit - ~printer_mapping ?(inplace=false) ?(interactive=false) + ~printer_mapping ?(redirect=true) + ?(inplace=false) ?(interactive=false) file = let id = gen_id () in let cmd, _, _ = @@ -312,6 +314,7 @@ let prove_file_server ~res_parser ~command ~limit { vc_file = file; is_temporary = not inplace; limit = limit; + redirect = redirect; res_parser = res_parser; printer_mapping = printer_mapping } in Hashtbl.add regexs id saved_data; @@ -343,6 +346,7 @@ let handle_answer answer = if save.is_temporary then Sys.remove save.vc_file; let out = read_and_delete_file answer.Prove_client.out_file in + let out = if save.redirect then out else "" in let ret = Unix.WEXITED answer.Prove_client.exit_code in let printer_mapping = save.printer_mapping in let ans = @@ -369,7 +373,7 @@ let call_on_file ~command ~limit ~res_parser ~printer_mapping ?(redirect=true) fin = fun () -> prove_file_server ~res_parser ~command ~limit ~printer_mapping - ~inplace ~interactive fin + ~redirect ~inplace ~interactive fin let get_new_results ~blocking = List.iter (fun (id, r) -> Hashtbl.add result_buffer id r) diff --git a/src/driver/call_provers.mli b/src/driver/call_provers.mli index b65764be05ea8bd6969915f2db073e3a65d7c0a8..59fdc460b26c4558f07de43a999109f7dba7f4f8 100644 --- a/src/driver/call_provers.mli +++ b/src/driver/call_provers.mli @@ -191,6 +191,7 @@ val prove_file_server : command : string -> limit : resource_limit -> printer_mapping : Printer.printer_mapping -> + ?redirect : bool -> ?inplace : bool -> ?interactive : bool -> string -> server_id