diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts index 8906457a68102a451c932b45eb023dad1c1cc71d..4c8fd9181ee06030a8796e79477fba5be124f412 100644 --- a/ivette/src/frama-c/server.ts +++ b/ivette/src/frama-c/server.ts @@ -121,7 +121,7 @@ const pending = new Map<string, PendingRequest>(); let process: ChildProcess | undefined; /** Polling timeout when server is busy. */ -const pollingTimeout = 200; +const pollingTimeout = 10; let pollingTimer: NodeJS.Timeout | undefined; /** Killing timeout and timer for server process hard kill. */ diff --git a/src/plugins/server/server_socket.ml b/src/plugins/server/server_socket.ml index ad9fd893d89a29edf24804133e7420ce37ad730c..32c00fa522e393c8237ed557540a2a772c96645f 100644 --- a/src/plugins/server/server_socket.ml +++ b/src/plugins/server/server_socket.ml @@ -67,19 +67,23 @@ let feed_bytes { sock ; rcv ; brcv } = let send_bytes { sock ; snd ; bsnd } = try - (* snd buffer is only used locally *) - let n = Buffer.length bsnd in - if n > 0 then - let s = Bytes.length snd in - let w = min n s in - Buffer.blit bsnd 0 snd 0 w ; - let r = Unix.single_write sock snd 0 w in - if r > 0 then - (* TODO[LC]: inefficient move. Requires a ring-buffer. *) - let rest = Buffer.sub bsnd r (n-r) in - Buffer.reset bsnd ; - Buffer.add_string bsnd rest - with Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> () + while true do + (* snd buffer is only used locally *) + let n = Buffer.length bsnd in + if n > 0 then + let s = Bytes.length snd in + let w = min n s in + Buffer.blit bsnd 0 snd 0 w ; + let r = Unix.single_write sock snd 0 w in + if r > 0 then + (* TODO[LC]: inefficient move. Requires a ring-buffer. *) + let rest = Buffer.sub bsnd r (n-r) in + Buffer.reset bsnd ; + Buffer.add_string bsnd rest + else raise Exit + else raise Exit + done + with Exit | Unix.Unix_error((EAGAIN|EWOULDBLOCK),_,_) -> () (* -------------------------------------------------------------------------- *) (* --- Data Chunks Encoding --- *)