fixed memory access bug in why3server

src/driver/prove_client.ml

@@ -109,11 +109,20 @@ let connect_internal () =
     Filename.temp_file "why3server" "sock"
   in
   let exec = Filename.concat Config.libdir "why3server" in
-  let pid = Unix.create_process exec
+  let pid =
+    (* use this version for debugging the C code
+    Unix.create_process "valgrind"
+    [|"/usr/bin/valgrind";exec; "--socket"; socket_name;
+      "--single-client";
+      "-j"; string_of_int !max_running_provers|]
+    Unix.stdin Unix.stdout Unix.stderr
+     *)
+    Unix.create_process exec
     [|exec; "--socket"; socket_name;
       "--single-client";
       "-j"; string_of_int !max_running_provers|]
-    Unix.stdin Unix.stdout Unix.stderr in
+    Unix.stdin Unix.stdout Unix.stderr
+  in
   Unix.chdir cwd;
   (* sleep before connecting, or the server will not be ready yet *)
   let rec try_connect n d =

src/server/options.c

@@ -77,7 +77,7 @@ void parse_options(int argc, char **argv) {
      }
   }
   if (optind < argc) {
-    printf("extra arguments, stopping\n");
+    printf("extra arguments, stopping [opt_index=%d,argc=%d]\n",optind,argc);
     exit(1);
   }
   if (basename == NULL) {
@@ -85,4 +85,3 @@ void parse_options(int argc, char **argv) {
     exit(1);
   }
 }
-

src/server/request.c

@@ -81,7 +81,7 @@ prequest parse_request(char* str_req, int len, int key) {
         parallel = parallel_arg;
       }
     }
-    if (strncmp(tmp, "interrupt", pos) == 0) {
+    else if (strncmp(tmp, "interrupt", pos) == 0) {
       free(tmp);
       req = (prequest) malloc(sizeof(request));
       req->key = key;