diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml index 388572b8c04b69c8d47657d15717c4b3c8c7fb22..9ffcd20c2d981dccfb24f7ee3ccf00f2c9c78dc8 100644 --- a/src/driver/call_provers.ml +++ b/src/driver/call_provers.ml @@ -359,6 +359,7 @@ let call_on_file ~command ~limit ~res_parser ~printer_mapping Hashtbl.add saved_data id save; let timelimit = get_time limit in let memlimit = get_mem limit in + let use_stdin = if use_stdin then Some fin else None in Prove_client.send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd; ServerCall id diff --git a/src/driver/prove_client.ml b/src/driver/prove_client.ml index 7e530d4230e1fd5eae123c7bcfddd115805c8888..2588c4ea4514aac57c2b5b32defe1ee23ee52a02 100644 --- a/src/driver/prove_client.ml +++ b/src/driver/prove_client.ml @@ -95,7 +95,7 @@ let set_max_running_provers x = let send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd = force_connect (); let buf = Buffer.create 128 in - let servercommand = if use_stdin then "runstdin;" else "run;" in + let servercommand = if use_stdin <> None then "runstdin;" else "run;" in Buffer.add_string buf servercommand; Buffer.add_string buf (string_of_int id); Buffer.add_char buf ';'; @@ -106,6 +106,12 @@ let send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd = Buffer.add_char buf ';'; Buffer.add_string buf x) cmd; + begin match use_stdin with + | None -> () + | Some s -> + Buffer.add_char buf ';'; + Buffer.add_string buf s + end; Buffer.add_char buf '\n'; let s = Buffer.contents buf in send_request_string s diff --git a/src/driver/prove_client.mli b/src/driver/prove_client.mli index d7a14a73c09c1e7a6f032789fd2e2d32c2dbdb1e..0182b8bbbbab4fbc3606e668a3b576c58b94859f 100644 --- a/src/driver/prove_client.mli +++ b/src/driver/prove_client.mli @@ -6,7 +6,7 @@ val set_max_running_provers : int -> unit val connect : unit -> unit val send_request : - use_stdin:bool -> + use_stdin:string option -> id:int -> timelimit:int -> memlimit:int -> diff --git a/src/server/server-unix.c b/src/server/server-unix.c index 21ac85ba214aebbcadd7b021bb21cded29442a77..6e86e7309f0c48a33bfd4bf1af35dda9513f15fd 100644 --- a/src/server/server-unix.c +++ b/src/server/server-unix.c @@ -257,7 +257,7 @@ pid_t create_process(char* cmd, unix_argv = (char**)malloc(sizeof(char*) * (argc + 2)); unix_argv[0] = cmd; unix_argv[argc + 1] = NULL; - for (i = 0; i < argc; i++) { + for (i = 0; i < count; i++) { unix_argv[i + 1] = argv[i]; }