Commit 0334be9d authored by MARCHE Claude's avatar MARCHE Claude

fix issue #174

interrupt is now properly handled by why3server
parent 5a5b51fd
......@@ -516,7 +516,6 @@ let query_call = function
let interrupt_call = function
| ServerCall id ->
Prove_client.send_interrupt ~id
| EditorCall pid ->
(try Unix.kill pid Sys.sigkill with Unix.Unix_error _ -> ())
......
......@@ -170,6 +170,7 @@ let send_interrupt ~id =
Buffer.clear send_buf;
Buffer.add_string send_buf "interrupt;";
Buffer.add_string send_buf (string_of_int id);
Buffer.add_char send_buf '\n';
let s = Buffer.contents send_buf in
send_request_string s
......
......@@ -11,6 +11,7 @@
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include "logging.h"
#include "options.h"
......@@ -22,24 +23,21 @@ void init_logging() {
}
}
void log_msg(char* s) {
void log_msg(char* fmt, ...) {
if (logging) {
fprintf (logfile, "%s\n", s);
fflush (logfile);
}
}
void log_msg_len(char* s, int len) {
if (logging) {
fprintf (logfile, "%.*s\n", len, s);
fflush (logfile);
va_list va;
va_start(va, fmt);
vfprintf(logfile, fmt, va);
fprintf(logfile, "\n");
fflush (logfile);
va_end(va);
}
}
void logging_shutdown(char* s) {
if (logging) {
log_msg(s);
fclose(logfile);
log_msg("%s",s);
fclose(logfile);
}
exit(1);
}
......@@ -14,9 +14,7 @@
void init_logging();
void log_msg(char* s);
void log_msg_len(char* s, int len);
void log_msg(char* s, ...) __attribute__ ((format (printf, 1, 2)));
void logging_shutdown(char* s);
#endif
......@@ -64,8 +64,7 @@ prequest parse_request(char* str_req, int len, int key) {
char* tmp;
bool runstdin = false;
log_msg("received query");
log_msg_len(str_req, len);
log_msg("received query %.*s",len,str_req);
semic = count_semicolons(str_req, len);
if (semic == 0) {
......
......@@ -523,6 +523,7 @@ void handle_msg(pclient client, int key) {
break;
case REQ_INTERRUPT:
// removes all occurrences of r->id from the queue
log_msg("Why3 server: removing id '%s' from queue",r->id);
remove_from_queue(r->id);
kill_processes(r->id);
free_request(r);
......
......@@ -402,7 +402,7 @@ void run_request (prequest r) {
NULL,
&si,
&pi)) {
log_msg(cmd);
log_msg("%s",cmd);
CloseHandle(outfilehandle);
CloseHandle(ghJob);
send_msg_to_client(client,
......
......@@ -505,7 +505,10 @@ let timeout_handler () =
let interrupt () =
(* Interrupt provers *)
Hashtbl.iter (fun _k e -> e.tp_callback Interrupted)
Hashtbl.iter
(fun call e ->
Call_provers.interrupt_call call;
e.tp_callback Interrupted)
prover_tasks_in_progress;
Hashtbl.clear prover_tasks_in_progress;
(* Do not interrupt editors
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment