ivette/src/dome/renderer/text/editors.tsx

@@ -386,7 +386,7 @@ class CodeMirrorWrapper extends React.Component<TextProps> {
   // --- Focus
   // --------------------------------------------------------------------------
 
-  handleKey(_cm: CodeMirror.Editor, key: string, _evt: KeyboardEvent) {
+  handleKey(_cm: CodeMirror.Editor, key: string, _evt: Event) {
     switch (key) {
       case 'Esc':
         this.props.buffer?.setFocused(false);

ivette/src/dome/template/makefile.packages

@@ -3,24 +3,26 @@
 # --------------------------------------------------------------------------
 
 DOME_DEV_PACKAGES= \
-	@babel/core@^7 \
+	@babel/core \
 	@babel/preset-env \
 	@babel/preset-react \
 	@babel/plugin-proposal-object-rest-spread \
-	electron@^7 \
+	electron@^16 \
 	electron-builder \
 	electron-webpack \
 	electron-devtools-installer \
-	webpack \
+	webpack@^4 \
 	babel-loader \
-	css-loader \
-	react-hot-loader \
-	@hot-loader/react-dom \
-	@types/react
+	css-loader@^5 \
+	react-hot-loader@^4 \
+	@hot-loader/react-dom@^16 \
+	@types/react@^16 \
+	@types/react-dom@^16 \
+	@types/react-virtualized@^9.21.0
 
 DOME_APP_PACKAGES= \
-	react@^16.8 \
-	react-dom \
+	react@^16 \
+	react-dom@^16 \
 	source-map-support \
 	lodash \
 	react-virtualized \

ivette/src/dome/template/webpack.renderer.js

@@ -55,6 +55,11 @@ module.exports = {
       'dome':         path.resolve( DOME , 'renderer' ),
       'react-dom':    '@hot-loader/react-dom'
     }
+  },
+  devServer: {
+    watchOptions: {
+      ignored: '**/.#*'
+    }
   }
 } ;
 

ivette/src/frama-c/client.ts

+/* ************************************************************************ */
+/*                                                                          */
+/*   This file is part of Frama-C.                                          */
+/*                                                                          */
+/*   Copyright (C) 2007-2021                                                */
+/*     CEA (Commissariat à l'énergie atomique et aux énergies               */
+/*          alternatives)                                                   */
+/*                                                                          */
+/*   you can redistribute it and/or modify it under the terms of the GNU    */
+/*   Lesser General Public License as published by the Free Software        */
+/*   Foundation, version 2.1.                                               */
+/*                                                                          */
+/*   It is distributed in the hope that it will be useful,                  */
+/*   but WITHOUT ANY WARRANTY; without even the implied warranty of         */
+/*   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the          */
+/*   GNU Lesser General Public License for more details.                    */
+/*                                                                          */
+/*   See the GNU Lesser General Public License version 2.1                  */
+/*   for more details (enclosed in the file licenses/LGPLv2.1).             */
+/*                                                                          */
+/* ************************************************************************ */
+
+import Emitter from 'events';
+import { json } from 'dome/data/json';
+
+// --------------------------------------------------------------------------
+// --- Frama-C Server Access (Client side)
+// --------------------------------------------------------------------------
+
+export abstract class Client {
+
+  /** Server CLI */
+  abstract commandLine(sockaddr: string, params: string[]): string[];
+
+  /** Connection */
+  abstract connect(addr: string): void;
+
+  /** Disconnection */
+  abstract disconnect(): void;
+
+  /** Send Request */
+  abstract send(kind: string, id: string, request: string, data: any): void;
+
+  /** Signal ON */
+  abstract sigOn(id: string): void;
+
+  /** Signal ON */
+  abstract sigOff(id: string): void;
+
+  /** Kill Request */
+  abstract kill(id: string): void;
+
+  /** Polling */
+  abstract poll(): void;
+
+  /** Shutdown the server */
+  abstract shutdown(): void;
+
+  /** @internal */
+  private events = new Emitter();
+
+  // --------------------------------------------------------------------------
+  // --- DATA Event
+  // --------------------------------------------------------------------------
+
+  /** Request data callback */
+  onData(callback: (id: string, data: json) => void): void {
+    this.events.on('DATA', callback);
+  }
+
+  /** @internal */
+  emitData(id: string, data: json): void {
+    this.events.emit('DATA', id, data);
+  }
+
+  // --------------------------------------------------------------------------
+  // --- REJECTED Event
+  // --------------------------------------------------------------------------
+
+  /** Rejected request callback */
+  onRejected(callback: (id: string) => void): void {
+    this.events.on('REJECTED', callback);
+  }
+
+  /** @internal */
+  emitRejected(id: string): void {
+    this.events.emit('REJECTED', id);
+  }
+
+  // --------------------------------------------------------------------------
+  // --- ERROR Event
+  // --------------------------------------------------------------------------
+
+  /** Rejected request callback */
+  onError(callback: (id: string, msg: string) => void): void {
+    this.events.on('ERROR', callback);
+  }
+
+  /** @internal */
+  emitError(id: string, msg: string): void {
+    this.events.emit('ERROR', id, msg);
+  }
+
+  // --------------------------------------------------------------------------
+  // --- KILLED Event
+  // --------------------------------------------------------------------------
+
+  /** Killed request callback */
+  onKilled(callback: (id: string) => void): void {
+    this.events.on('KILLED', callback);
+  }
+
+  /** @internal */
+  emitKilled(id: string): void {
+    this.events.emit('KILLED', id);
+  }
+
+  // --------------------------------------------------------------------------
+  // --- SIGNAL Event
+  // --------------------------------------------------------------------------
+
+  /** Signal callback */
+  onSignal(callback: (id: string) => void): void {
+    this.events.on('SIGNAL', callback);
+  }
+
+  /** @internal */
+  emitSignal(id: string): void {
+    this.events.emit('SIGNAL', id);
+  }
+
+  // --------------------------------------------------------------------------
+  // --- CONNECT Event
+  // --------------------------------------------------------------------------
+
+  /** Connection callback */
+  onConnect(callback: (err?: Error) => void): void {
+    this.events.on('CONNECT', callback);
+  }
+
+  /** @internal */
+  emitConnect(err?: Error): void {
+    this.events.emit('CONNECT', err);
+  }
+
+}
+
+// --------------------------------------------------------------------------

ivette/src/frama-c/client_socket.ts

+/* ************************************************************************ */
+/*                                                                          */
+/*   This file is part of Frama-C.                                          */
+/*                                                                          */
+/*   Copyright (C) 2007-2021                                                */
+/*     CEA (Commissariat à l'énergie atomique et aux énergies               */
+/*          alternatives)                                                   */
+/*                                                                          */
+/*   you can redistribute it and/or modify it under the terms of the GNU    */
+/*   Lesser General Public License as published by the Free Software        */
+/*   Foundation, version 2.1.                                               */
+/*                                                                          */
+/*   It is distributed in the hope that it will be useful,                  */
+/*   but WITHOUT ANY WARRANTY; without even the implied warranty of         */
+/*   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the          */
+/*   GNU Lesser General Public License for more details.                    */
+/*                                                                          */
+/*   See the GNU Lesser General Public License version 2.1                  */
+/*   for more details (enclosed in the file licenses/LGPLv2.1).             */
+/*                                                                          */
+/* ************************************************************************ */
+
+import Net from 'net';
+import { Debug } from 'dome';
+import { json } from 'dome/data/json';
+import { Client } from './client';
+
+const D = new Debug('SocketServer');
+
+const RETRIES = 10;
+const TIMEOUT = 200;
+
+// --------------------------------------------------------------------------
+// --- Frama-C Server API
+// --------------------------------------------------------------------------
+
+class SocketClient extends Client {
+
+  retries = 0;
+  running = false;
+  socket: Net.Socket | undefined;
+  timer: NodeJS.Timeout | undefined;
+  queue: json[] = [];
+  buffer: Buffer = Buffer.from('');
+
+  /** Server CLI */
+  commandLine(sockaddr: string, params: string[]): string[] {
+    return ['-server-socket', sockaddr, '-then'].concat(params);
+  }
+
+  /** Connection */
+  connect(sockaddr: string): void {
+    this.retries++;
+    if (this.socket) {
+      this.socket.destroy();
+    }
+    if (this.timer) {
+      clearTimeout(this.timer);
+      this.timer = undefined;
+    }
+    const s = Net.createConnection(sockaddr, () => {
+      this.running = true;
+      this.retries = 0;
+      this.emitConnect();
+      this._flush();
+    });
+    // Using Buffer data encoding at this level
+    s.on('end', () => this.disconnect());
+    s.on('data', (data: Buffer) => this._receive(data));
+    s.on('error', (err: Error) => {
+      s.destroy();
+      if (this.retries <= RETRIES && !this.running) {
+        this.socket = undefined;
+        this.timer = setTimeout(() => this.connect(sockaddr), TIMEOUT);
+      } else {
+        this.running = false;
+        this.emitConnect(err);
+      }
+    });
+    this.socket = s;
+  }
+
+  disconnect(): void {
+    this.queue = [];
+    this.retries = 0;
+    this.running = false;
+    if (this.timer) {
+      clearTimeout(this.timer);
+      this.timer = undefined;
+    }
+    if (this.socket) {
+      this.socket.destroy();
+      this.socket = undefined;
+    }
+  }
+
+  /** Send Request */
+  send(kind: string, id: string, request: string, data: any): void {
+    this.queue.push({ cmd: kind, id, request, data });
+    this._flush();
+  }
+
+  /** Signal ON */
+  sigOn(id: string): void {
+    this.queue.push({ cmd: 'SIGON', id });
+    this._flush();
+  }
+
+  /** Signal ON */
+  sigOff(id: string): void {
+    this.queue.push({ cmd: 'SIGOFF', id });
+    this._flush();
+  }
+
+  /** Kill Request */
+  kill(id: string): void {
+    this.queue.push({ cmd: 'KILL', id });
+    this._flush();
+  }
+
+  /** Polling */
+  poll(): void {
+    this.queue.push('POLL');
+    this._flush();
+  }
+
+  /** Shutdown the server */
+  shutdown(): void {
+    this.queue.push('SHUTDOWN');
+    this._flush();
+  }
+
+  // --------------------------------------------------------------------------
+  // --- Low-Level Management
+  // --------------------------------------------------------------------------
+
+  _flush() {
+    if (this.running) {
+      this.queue.forEach((cmd) => {
+        this._send(Buffer.from(JSON.stringify(cmd), 'utf8'));
+      });
+      this.queue = [];
+    }
+  }
+
+  _send(data: Buffer) {
+    const s = this.socket;
+    if (s) {
+      const len = data.length;
+      const hex = Number(len).toString(16).toUpperCase();
+      const padding = '0000000000000000';
+      const header =
+        len <= 0xFFF ? 'S' + padding.substring(hex.length, 3) :
+          len <= 0xFFFFFFF ? 'L' + padding.substring(hex.length, 7) :
+            'W' + padding.substring(hex.length, 15);
+      s.write(Buffer.from(header + hex));
+      s.write(data);
+    }
+  }
+
+  _fetch(): undefined | string {
+    const msg = this.buffer;
+    const len = msg.length;
+    if (len < 1) return;
+    const hd = msg.readInt8(0);
+    // 'S': 83, 'L': 76, 'W': 87
+    const phex = hd == 83 ? 4 : hd == 76 ? 8 : 16;
+    if (len < phex) return;
+    const size = Number.parseInt(msg.slice(1, phex).toString('ascii'), 16);
+    const offset = phex + size;
+    if (len < offset) return;
+    this.buffer = msg.slice(offset);
+    return msg.slice(phex, offset).toString('utf8');
+  }
+
+  _receive(chunk: Buffer) {
+    this.buffer = Buffer.concat([this.buffer, chunk]);
+    while (true) {
+      const n0 = this.buffer.length;
+      const data = this._fetch();
+      const n1 = this.buffer.length;
+      if (data === undefined || n0 <= n1) break;
+      try {
+        const cmd: any = JSON.parse(data);
+        if (cmd !== null && typeof (cmd) === 'object') {
+          switch (cmd.res) {
+            case 'DATA': this.emitData(cmd.id, cmd.data); break;
+            case 'ERROR': this.emitError(cmd.id, cmd.msg); break;
+            case 'KILLED': this.emitKilled(cmd.id); break;
+            case 'REJECTED': this.emitRejected(cmd.id); break;
+            case 'SIGNAL': this.emitSignal(cmd.id); break;
+            default:
+              D.warn('Unknown command', cmd);
+          }
+        } else
+          D.warn('Misformed data', data);
+      } catch (err) {
+        D.warn('Misformed JSON', data, err);
+      }
+    }
+  }
+
+}
+
+export const client: Client = new SocketClient();
+
+// --------------------------------------------------------------------------

ivette/src/frama-c/client_zmq.ts

+/* ************************************************************************ */
+/*                                                                          */
+/*   This file is part of Frama-C.                                          */
+/*                                                                          */
+/*   Copyright (C) 2007-2021                                                */
+/*     CEA (Commissariat à l'énergie atomique et aux énergies               */
+/*          alternatives)                                                   */
+/*                                                                          */
+/*   you can redistribute it and/or modify it under the terms of the GNU    */
+/*   Lesser General Public License as published by the Free Software        */
+/*   Foundation, version 2.1.                                               */
+/*                                                                          */
+/*   It is distributed in the hope that it will be useful,                  */
+/*   but WITHOUT ANY WARRANTY; without even the implied warranty of         */
+/*   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the          */
+/*   GNU Lesser General Public License for more details.                    */
+/*                                                                          */
+/*   See the GNU Lesser General Public License version 2.1                  */
+/*   for more details (enclosed in the file licenses/LGPLv2.1).             */
+/*                                                                          */
+/* ************************************************************************ */
+
+import * as ZMQ from 'zeromq';
+import { Debug } from 'dome';
+import { Client } from './client';
+
+const D = new Debug('ZmqServer');
+
+// --------------------------------------------------------------------------
+// --- Frama-C Server API
+// --------------------------------------------------------------------------
+
+class ZmqClient extends Client {
+
+  queue: string[] = [];
+  zmqSocket: ZMQ.Socket | undefined;
+  zmqIsBusy = false;
+
+  /** Server CLI */
+  commandLine(sockaddr: string, params: string[]): string[] {
+    return ['-server-zmq', `ipc://${sockaddr}`, '-then'].concat(params);
+  }
+
+  /** Connection */
+  connect(sockaddr: string): void {
+    if (this.zmqSocket) {
+      this.zmqSocket.close();
+    }
+    this.zmqSocket = new ZMQ.Socket('req');
+    this.zmqIsBusy = false;
+    this.zmqSocket.connect(`ipc://${sockaddr}`);
+    this.zmqSocket.on('message', (msg: string[]) => this._receive(msg));
+  }
+
+  disconnect(): void {
+    this.zmqIsBusy = false;
+    this.queue = [];
+    if (this.zmqSocket) {
+      this.zmqSocket.close();
+      this.zmqSocket = undefined;
+    }
+  }
+
+  /** Send Request */
+  send(kind: string, id: string, request: string, data: any): void {
+    if (this.zmqSocket) {
+      this.queue.push(kind, id, request, data);
+      this._flush();
+    }
+  }
+
+  /** Signal ON */
+  sigOn(id: string): void {
+    if (this.zmqSocket) {
+      this.queue.push('SIGON', id);
+      this._flush();
+    }
+  }
+
+  /** Signal ON */
+  sigOff(id: string): void {
+    if (this.zmqSocket) {
+      this.queue.push('SIGOFF', id);
+      this._flush();
+    }
+  }
+
+  /** Kill Request */
+  kill(id: string): void {
+    if (this.zmqSocket) {
+      this.queue.push('KILL', id);
+      this._flush();
+    }
+  }
+
+  /** Polling */
+  poll(): void {
+    if (this.zmqSocket && this.queue.length == 0) {
+      this.queue.push('POLL');
+    }
+    this._flush();
+  }
+
+  /** Shutdown the server */
+  shutdown(): void {
+    this.queue = [];
+    if (this.zmqSocket) {
+      this.queue.push('SHUTDOWN');
+      this._flush();
+    }
+  }
+
+  // --------------------------------------------------------------------------
+  // --- Low-Level Management
+  // --------------------------------------------------------------------------
+
+  _flush() {
+    const socket = this.zmqSocket;
+    if (socket) {
+      const cmds = this.queue;
+      if (cmds && !this.zmqIsBusy) {
+        try {
+          this.queue = [];
+          socket.send(cmds);
+          this.zmqIsBusy = true;
+        } catch (err) {
+          D.error('ZmqSocket', err);
+          this.zmqIsBusy = false;
+        }
+      }
+    } else {
+      this.queue = [];
+    }
+  }
+
+  _receive(resp: string[]) {
+    try {
+      this._decode(resp);
+    } catch (err) {
+      D.error('ZmqSocket', err);
+    } finally {
+      this.zmqIsBusy = false;
+      setImmediate(() => this._flush());
+    }
+  }
+
+  /* eslint-disable @typescript-eslint/indent */
+  _decode(resp: string[]) {
+    const shift = () => resp.shift() ?? '';
+    while (resp.length) {
+      const cmd = shift();
+      switch (cmd) {
+        case 'NONE':
+          break;
+        case 'DATA':
+          {
+            const rid = shift();
+            const data = JSON.parse(shift());
+            this.emitData(rid, data);
+          }
+          break;
+        case 'KILLED':
+          {
+            const rid = shift();
+            this.emitKilled(rid);
+          }
+          break;
+        case 'ERROR':
+          {
+            const rid = shift();
+            const msg = shift();
+            this.emitError(rid, msg);
+          }
+          break;
+        case 'REJECTED':
+          {
+            const rid = shift();
+            this.emitRejected(rid);
+          }
+          break;
+        case 'SIGNAL':
+          {
+            const rid = shift();
+            this.emitSignal(rid);
+          }
+          break;
+        case 'WRONG':
+          {
+            const err = shift();
+            D.error(`ZMQ Protocol Error: ${err}`);
+          }
+          break;
+        default:
+          D.error(`Unknown Response: ${cmd}`);
+          return;
+      }
+    }
+  }
+
+}
+
+export const client: Client = new ZmqClient();
+
+// --------------------------------------------------------------------------

ivette/src/frama-c/kernel/ASTview.tsx

@@ -186,9 +186,11 @@ export default function ASTview() {
             const markers = buffer.findTextMarker(prop.key);
             markers.forEach((marker) => {
               const pos = marker.find();
-              buffer.forEach((cm) => {
-                cm.setGutterMarker(pos.from.line, 'bullet', bullet);
-              });
+              if (pos) {
+                buffer.forEach((cm) => {
+                  cm.setGutterMarker(pos.from.line, 'bullet', bullet);
+                });
+              }
             });
           }
         }

ivette/src/frama-c/kernel/Globals.tsx

@@ -119,7 +119,7 @@ export default () => {
 
   function isSelected(fct: functionsData) {
     return multipleSelection?.allSelections.some(
-      (l) => fct.name === l?.fct
+      (l) => fct.name === l?.fct,
     );
   }
 

ivette/src/frama-c/kernel/Messages.tsx

@@ -53,7 +53,7 @@ interface Search {
 }
 
 type KindFilter = Record<logkind, boolean>;
-type PluginFilter = {[key: string]: boolean};
+type PluginFilter = { [key: string]: boolean };
 type EmitterFilter = {
   kernel: boolean;
   plugins: PluginFilter;
@@ -80,23 +80,23 @@ const kindFilter: KindFilter = {
 /* The fields must be exactly the short names of Frama-C plugins used in
    messages. They are all shown by default. */
 const pluginFilter: PluginFilter = {
-  aorai: true,
-  dive: true,
+  'aorai': true,
+  'dive': true,
   'e-acsl': true,
-  eva: true,
-  from: true,
-  impact: true,
-  inout: true,
-  metrics: true,
-  nonterm: true,
-  pdg: true,
-  report: true,
-  rte: true,
-  scope: true,
-  server: true,
-  slicing: true,
-  variadic: true,
-  wp: true,
+  'eva': true,
+  'from': true,
+  'impact': true,
+  'inout': true,
+  'metrics': true,
+  'nonterm': true,
+  'pdg': true,
+  'report': true,
+  'rte': true,
+  'scope': true,
+  'server': true,
+  'slicing': true,
+  'variadic': true,
+  'wp': true,
 };
 
 const emitterFilter = {
@@ -168,7 +168,7 @@ function searchString(search: string | undefined, msg: string) {
 
 function filterSearched(search: Search, msg: Message) {
   return (searchString(search.message, msg.message) &&
-          searchCategory(search.category, msg.category));
+    searchCategory(search.category, msg.category));
 }
 
 function filterFunction(filter: Filter, kf: string | undefined, msg: Message) {
@@ -179,20 +179,15 @@ function filterFunction(filter: Filter, kf: string | undefined, msg: Message) {
 
 function filterMessage(filter: Filter, kf: string | undefined, msg: Message) {
   return (filterFunction(filter, kf, msg) &&
-          filterSearched(filter.search, msg) &&
-          filterKind(filter.kind, msg) &&
-          filterEmitter(filter.emitter, msg));
+    filterSearched(filter.search, msg) &&
+    filterKind(filter.kind, msg) &&
+    filterEmitter(filter.emitter, msg));
 }
 
 // --------------------------------------------------------------------------
 // --- Filters panel and ratio
 // --------------------------------------------------------------------------
 
-function Checkbox(p: Forms.CheckboxFieldProps) {
-  const lbl = p.label.charAt(0).toUpperCase() + p.label.slice(1).toLowerCase();
-  return <Forms.CheckboxField label={lbl} state={p.state} />;
-}
-
 function Section(p: Forms.SectionProps) {
   const settings = `ivette.messages.filter.${p.label}`;
   return (
@@ -202,28 +197,45 @@ function Section(p: Forms.SectionProps) {
   );
 }
 
-function MessageFilter(props: {filter: State<Filter>}) {
+function Checkbox(p: Forms.CheckboxFieldProps) {
+  const lbl = p.label.charAt(0).toUpperCase() + p.label.slice(1).toLowerCase();
+  return <Forms.CheckboxField label={lbl} state={p.state} />;
+}
+
+function MessageKindCheckbox(props: {
+  kind: logkind,
+  kindState: Forms.FieldState<KindFilter>,
+}) {
+  const { kind, kindState } = props;
+  const state = Forms.useProperty(kindState, kind);
+  return <Checkbox label={kind} state={state} />;
+}
+
+function PluginCheckbox(props: {
+  plugin: string,
+  pluginState: Forms.FieldState<PluginFilter>,
+}) {
+  const state = Forms.useProperty(props.pluginState, props.plugin);
+  return <Checkbox label={props.plugin} state={state} />;
+}
+
+function MessageFilter(props: { filter: State<Filter> }) {
   const state = Forms.useValid(props.filter);
   const search = Forms.useProperty(state, 'search');
   const categoryState = Forms.useProperty(search, 'category');
   const messageState = Forms.useProperty(search, 'message');
-
-  const kind = Forms.useProperty(state, 'kind');
-  const kindState = (key: logkind) => Forms.useProperty(kind, key);
+  const kindState = Forms.useProperty(state, 'kind');
   const kindCheckboxes =
-    Object.keys(kindFilter).map((key) => (
-      <Checkbox key={key} label={key} state={kindState(key as logkind)} />
+    Object.keys(kindFilter).map((k) => (
+      <MessageKindCheckbox key={k} kind={k as logkind} kindState={kindState} />
     ));
-
-  const emitter = Forms.useProperty(state, 'emitter');
-  function EmitterCheckbox(p: {key: 'kernel' | 'others'}) {
-    return <Checkbox label={p.key} state={Forms.useProperty(emitter, p.key)} />;
-  }
-  const plugin = Forms.useProperty(emitter, 'plugins');
-  const pluginState = (key: string) => Forms.useProperty(plugin, key);
+  const emitterState = Forms.useProperty(state, 'emitter');
+  const kernelState = Forms.useProperty(emitterState, 'kernel');
+  const othersState = Forms.useProperty(emitterState, 'others');
+  const pluginState = Forms.useProperty(emitterState, 'plugins');
   const pluginCheckboxes =
-    Object.keys(pluginFilter).map((key) => (
-      <Checkbox key={key} label={key} state={pluginState(key)} />
+    Object.keys(pluginFilter).map((p) => (
+      <PluginCheckbox key={p} plugin={p} pluginState={pluginState} />
     ));
 
   return (
@@ -239,29 +251,29 @@ function MessageFilter(props: {filter: State<Filter>}) {
           state={categoryState}
           placeholder="Category"
           title={'Search in message category.\n'
-               + 'Use -<name> to hide some categories.'}
+            + 'Use -<name> to hide some categories.'}
         />
         <Forms.TextField
           label="Message"
           state={messageState}
           placeholder="Message"
           title={'Search in message text.\n'
-               + 'Case-insensitive by default.\n'
-               + 'Use "text" for an exact case-sensitive search.'}
+            + 'Case-insensitive by default.\n'
+            + 'Use "text" for an exact case-sensitive search.'}
         />
       </Section>
       <Section label="Kind">
-        { kindCheckboxes }
+        {kindCheckboxes}
       </Section>
       <Section label="Emitter">
         <div className="message-emitter-category">
-          { EmitterCheckbox({ key: 'kernel' }) }
+          <Forms.CheckboxField label='Kernel' state={kernelState} />
         </div>
         <div className="message-emitter-category">
-          { pluginCheckboxes }
+          {pluginCheckboxes}
         </div>
         <div className="message-emitter-category">
-          { EmitterCheckbox({ key: 'others' }) }
+          <Forms.CheckboxField label='Others' state={othersState} />
         </div>
       </Section>
     </Forms.Page>

ivette/src/frama-c/kernel/SourceCode.tsx

@@ -90,10 +90,14 @@ export default function SourceCode() {
     });
 
   // Updating the buffer content.
-  const errorMsg = () => { D.error(`Fail to load source code file ${file}`); };
-  const onError = () => { if (file) errorMsg(); return ''; };
-  const read = () => System.readFile(file).catch(onError);
-  const text = React.useMemo(read, [file, onError]);
+  const text = React.useMemo(async () => {
+    const onError = () => {
+      if (file)
+        D.error(`Fail to load source code file ${file}`);
+      return '';
+    };
+    return System.readFile(file).catch(onError);
+  }, [file]);
   const { result } = Dome.usePromise(text);
   React.useEffect(() => buffer.setValue(result), [buffer, result]);
 
@@ -115,29 +119,31 @@ export default function SourceCode() {
   type position = CodeMirror.Position;
   type editor = CodeMirror.Editor;
 
-  async function select(editor: editor, event: MouseEvent) {
-    const pos = editor.coordsChar({ left: event.x, top: event.y });
-    if (file === '' || !pos) return;
-    const arg = [file, pos.line + 1, pos.ch + 1];
-    Server
-      .send(getMarkerAt, arg)
-      .then(([fct, marker]) => {
-        if (fct || marker) {
-          const location = { fct, marker } as States.Location;
-          selected.current = location;
-          updateSelection({ location });
-        }
-      })
-      .catch((err) => {
-        D.error(`Failed to get marker from source file position: ${err}`);
-        Status.setMessage({
-          text: 'Failed request to Frama-C server',
-          kind: 'error',
+  const selectCallback = React.useCallback(
+    async function select(editor: editor, event: MouseEvent) {
+      const pos = editor.coordsChar({ left: event.x, top: event.y });
+      if (file === '' || !pos) return;
+      const arg = [file, pos.line + 1, pos.ch + 1];
+      Server
+        .send(getMarkerAt, arg)
+        .then(([fct, marker]) => {
+          if (fct || marker) {
+            const location = { fct, marker } as States.Location;
+            selected.current = location;
+            updateSelection({ location });
+          }
+        })
+        .catch((err) => {
+          D.error(`Failed to get marker from source file position: ${err}`);
+          Status.setMessage({
+            text: 'Failed request to Frama-C server',
+            kind: 'error',
+          });
         });
-      });
-  }
+    },
+    [file, updateSelection],
+  );
 
-  const selectCallback = React.useCallback(select, [file]);
   React.useEffect(() => {
     buffer.forEach((cm) => cm.on('mousedown', selectCallback));
     return () => buffer.forEach((cm) => cm.off('mousedown', selectCallback));

ivette/src/frama-c/kernel/Status.tsx

@@ -21,48 +21,48 @@
 /* ************************************************************************ */
 
 /* --------------------------------------------------------------------------*/
-/* --- Frama-C Selection History                                          ---*/
+/* --- Frama-C Status Message                                             ---*/
 /* --------------------------------------------------------------------------*/
 
 import React from 'react';
 import { Code } from 'dome/controls/labels';
-import { LED, IconButton } from 'dome/controls/buttons';
+import { IconButton } from 'dome/controls/buttons';
+import { LED } from 'dome/controls/displays';
 import { Icon } from 'dome/controls/icons';
 import * as Toolbars from 'dome/frame/toolbars';
 import { GlobalState, useGlobalState } from 'dome/data/states';
+import * as Server from 'frama-c/server';
 
 export type kind =
   'none' | 'info' | 'warning' | 'error' | 'success' | 'progress';
 
-export interface Message {
+export interface MessageProps {
   kind: kind;
   text: string;
   title?: string;
 }
 
-const emptyMessage: Message = { text: '', kind: 'none' };
+const emptyMessage: MessageProps = { text: '', kind: 'none' };
 
 const GlobalMessage = new GlobalState(emptyMessage);
 
-export function setMessage(message: Message) {
+export function setMessage(message: MessageProps) {
   GlobalMessage.setValue(message);
 }
 
 export default function Message() {
   const [message] = useGlobalState(GlobalMessage);
-
   return (
     <>
       <Toolbars.Space />
-      { message.kind === 'progress' && <LED status="active" blink /> }
-      { message.kind === 'success' && <Icon id="CHECK" fill="green" /> }
-      { message.kind === 'warning' && <Icon id="ATTENTION" /> }
-      { message.kind === 'error' && <Icon id="CROSS" fill="red" /> }
-      { message.kind === 'info' && <Icon id="CIRC.INFO" /> }
+      {message.kind === 'progress' && <LED status="active" blink />}
+      {message.kind === 'success' && <Icon id="CHECK" fill="green" />}
+      {message.kind === 'warning' && <Icon id="ATTENTION" />}
+      {message.kind === 'error' && <Icon id="CROSS" fill="red" />}
+      {message.kind === 'info' && <Icon id="CIRC.INFO" />}
       <Code label={message.text} title={message.title} />
-      <Toolbars.Space />
       <IconButton
-        icon="CROSS"
+        icon="CIRC.CLOSE"
         onClick={() => setMessage(emptyMessage)}
         visible={message !== emptyMessage}
         title="Hide current message"
@@ -72,4 +72,11 @@ export default function Message() {
   );
 }
 
+/* Callback on server events */
+
+{
+  Server.onReady(() => setMessage(emptyMessage));
+  Server.onShutdown(() => setMessage(emptyMessage));
+}
+
 /* --------------------------------------------------------------------------*/

ivette/src/frama-c/plugins/dive/index.tsx

@@ -217,10 +217,11 @@ class Dive {
       trigger: 'manual',
       appendTo: document.body,
       lazy: false,
-      onCreate: (instance: Tippy.Instance) => {
+      onCreate: (instance: any) => {
         const { popperInstance } = instance;
-        if (popperInstance)
+        if (popperInstance) {
           popperInstance.reference = (node as any).popperRef();
+        }
       },
     };
 
@@ -231,7 +232,8 @@ class Dive {
         ...common,
         content: node.data().values,
         placement: 'top',
-        distance: 10,
+        //distance: 10,
+        offset: [10, 10],
         arrow: true,
       }));
     }
@@ -241,7 +243,8 @@ class Dive {
         ...common,
         content: node.data().type,
         placement: 'bottom',
-        distance: 20,
+        //distance: 20,
+        offset: [20, 20],
         theme: 'light-border',
         arrow: false,
       }));

ivette/src/frama-c/plugins/eva/CoverageMeter.tsx

@@ -21,27 +21,29 @@
 /* ************************************************************************ */
 
 import React from 'react';
+import { Meter } from 'dome/controls/displays';
 
-export interface Coverage {
+export interface CoverageProps {
   reachable: number;
   dead: number;
 }
 
-export function percent(coverage: Coverage): string {
+export function percent(coverage: CoverageProps): string {
   const q = coverage.reachable / (coverage.reachable + coverage.dead);
   return `${(q * 100).toFixed(1)}%`;
 }
 
-export default function (props: {coverage: Coverage}) {
+export default function(props: { coverage: CoverageProps }) {
   const { reachable, dead } = props.coverage;
   const total = reachable + dead;
 
   return (
-    <meter
+    <Meter
       min={0}
       max={total}
-      low={0.8 * total}
-      optimum={total}
+      low={0.50 * total}
+      high={0.85 * total}
+      optimum='HIGH'
       value={reachable}
     />
   );

ivette/src/frama-c/plugins/eva/Summary.tsx

@@ -22,12 +22,11 @@
 
 // React & Dome
 import React from 'react';
+import { LED } from 'dome/controls/displays';
 import * as Ivette from 'ivette';
 import * as States from 'frama-c/states';
 import * as Eva from 'frama-c/api/plugins/eva/general';
 
-import { LED } from 'dome/controls/buttons';
-
 import CoverageMeter, { percent } from './CoverageMeter';
 
 import './summary.css';
@@ -143,10 +142,10 @@ function Alarms(data: Eva.programStatsType,
         </tbody>
       </table>
       {invalid > 0 && (
-      <div>
-        {invalid} of them {invalid === 1 ? 'is a' : 'are'} sure
-        alarm{plural(invalid)}.
-      </div>
+        <div>
+          {invalid} of them {invalid === 1 ? 'is a' : 'are'} sure
+          alarm{plural(invalid)}.
+        </div>
       )}
     </>
   );

ivette/src/frama-c/plugins/eva/probes.ts

@@ -52,7 +52,7 @@ function newLabel() {
     La = Ka;
     Lk++;
   }
-  return k > 0 ? lbl + k : lbl;
+  return k > 0 ? `${lbl}${k}` : lbl;
 }
 
 /* --------------------------------------------------------------------------*/

ivette/src/frama-c/plugins/eva/style.css

@@ -182,6 +182,7 @@
 
 .eva-cell .eva-stmt {
     margin-left: 0.2em;
+    padding: 2px 0px;
 }
 
 .eva-cell-expression {

ivette/src/frama-c/plugins/eva/valueinfos.tsx

@@ -48,9 +48,10 @@ interface StmtProps {
 }
 
 export function Stmt(props: StmtProps) {
+  const markersInfo = States.useSyncArray(Ast.markerInfo);
+
   const { stmt, marker, short } = props;
   if (!stmt) return null;
-  const markersInfo = States.useSyncArray(Ast.markerInfo);
   const line = markersInfo.getData(marker)?.sloc?.line;
   const filename = markersInfo.getData(marker)?.sloc?.base;
   const title = markersInfo.getData(stmt)?.descr;

ivette/src/frama-c/server.ts

@@ -21,29 +21,24 @@
 /* ************************************************************************ */
 
 // --------------------------------------------------------------------------
-// --- Frama-C Server
+// --- Connection to Frama-C Server
 // --------------------------------------------------------------------------
 
 /**
- * Manage the current Frama-C server/client interface
- * @packageDocumentation
- * @module frama-c/server
+   Manage the current Frama-C server/client interface
+   @packageDocumentation
+   @module frama-c/server
 */
 
-import _ from 'lodash';
+import { debounce } from 'lodash';
 import React from 'react';
 import * as Dome from 'dome';
 import * as System from 'dome/system';
 import * as Json from 'dome/data/json';
 import { RichTextBuffer } from 'dome/text/buffers';
-import { Request as ZmqRequest } from 'zeromq';
 import { ChildProcess } from 'child_process';
-
-// --------------------------------------------------------------------------
-// --- Pretty Printing (Browser Console)
-// --------------------------------------------------------------------------
-
-const D = new Dome.Debug('Server');
+import { client } from './client_socket';
+//import { client } from './client_zmq';
 
 // --------------------------------------------------------------------------
 // --- Events
@@ -88,7 +83,7 @@ export class SIGNAL extends Dome.Event {
 // --------------------------------------------------------------------------
 
 /** Server stages. */
-export enum Stage {
+export enum Status {
   /** Server is off. */
   OFF = 'OFF',
   /** Server is starting, but not on yet. */
@@ -100,34 +95,7 @@ export enum Stage {
   /** Server is restarting. */
   RESTARTING = 'RESTARTING',
   /** Server is off upon failure. */
-  FAILURE = 'FAILURE'
-}
-
-export interface OkStatus {
-  readonly stage:
-  Stage.OFF | Stage.ON | Stage.STARTING | Stage.RESTARTING | Stage.HALTING;
-}
-
-export interface ErrorStatus {
-  readonly stage: Stage.FAILURE;
-  /** Failure message. */
-  readonly error: string;
-}
-
-export type Status = OkStatus | ErrorStatus;
-
-function okStatus(
-  s: Stage.OFF | Stage.ON | Stage.STARTING | Stage.RESTARTING | Stage.HALTING,
-) {
-  return { stage: s };
-}
-
-function errorStatus(error: string): ErrorStatus {
-  return { stage: Stage.FAILURE, error };
-}
-
-export function hasErrorStatus(s: Status): s is ErrorStatus {
-  return (s as ErrorStatus).error !== undefined;
+  FAILURE = 'FAILURE',
 }
 
 // --------------------------------------------------------------------------
@@ -135,46 +103,29 @@ export function hasErrorStatus(s: Status): s is ErrorStatus {
 // --------------------------------------------------------------------------
 
 /** The current server status. */
-let status: Status = okStatus(Stage.OFF);
+let status: Status = Status.OFF;
 
 /** Request counter. */
 let rqCount = 0;
 
-type IndexedPair<T, U> = {
-  [index: string]: [T, U];
-};
-
-type ResolvePromise = (value: Json.json) => void;
-type RejectPromise = (error: Error) => void;
-
-/** Pending promise callbacks (pairs of (resolve, reject)). */
-let pending: IndexedPair<ResolvePromise, RejectPromise> = {};
-
-/** Queue of server commands to be sent. */
-let queueCmd: string[] = [];
-
-/** Waiting request ids to be sent. */
-let queueId: string[] = [];
-
-/** Polling timeout and timer. */
-const pollingTimeout = 50;
-let pollingTimer: NodeJS.Timeout | undefined;
-
-/** Flushing timer. */
-let flushingTimer: NodeJS.Immediate | undefined;
+/** Pending Requests. */
+interface PendingRequest {
+  resolve: (data: Json.json) => void;
+  reject: (err?: string) => void;
+}
+const pending = new Map<string, PendingRequest>();
 
 /** Server process. */
 let process: ChildProcess | undefined;
 
+/** Polling timeout when server is busy. */
+const pollingTimeout = 200;
+let pollingTimer: NodeJS.Timeout | undefined;
+
 /** Killing timeout and timer for server process hard kill. */
-const killingTimeout = 300;
+const killingTimeout = 500;
 let killingTimer: NodeJS.Timeout | undefined;
 
-/** ZMQ (REQ) socket. */
-let zmqSocket: ZmqRequest | undefined;
-/** Flag on whether ZMQ socket is busy. */
-let zmqIsBusy = false;
-
 // --------------------------------------------------------------------------
 // --- Server Console
 // --------------------------------------------------------------------------
@@ -205,14 +156,14 @@ export function useStatus(): Status {
  *  Whether the server is running and ready to handle requests.
  *  @return {boolean} Whether server stage is [[ON]].
  */
-export function isRunning(): boolean { return status.stage === Stage.ON; }
+export function isRunning(): boolean { return status === Status.ON; }
 
 /**
  *  Number of requests still pending.
  *  @return {number} Pending requests.
  */
 export function getPending(): number {
-  return _.reduce(pending, (n) => n + 1, 0);
+  return pending.size;
 }
 
 /**
@@ -232,16 +183,12 @@ export function onShutdown(callback: () => void) { SHUTDOWN.on(callback); }
 // --------------------------------------------------------------------------
 
 function _status(newStatus: Status) {
-  if (Dome.DEVEL && hasErrorStatus(newStatus)) {
-    D.error(newStatus.error);
-  }
-
   if (newStatus !== status) {
     const oldStatus = status;
     status = newStatus;
     STATUS.emit(newStatus);
-    if (oldStatus.stage === Stage.ON) SHUTDOWN.emit();
-    if (newStatus.stage === Stage.ON) READY.emit();
+    if (oldStatus === Status.ON) SHUTDOWN.emit();
+    if (newStatus === Status.ON) READY.emit();
   }
 }
 
@@ -257,22 +204,20 @@ function _status(newStatus: Status) {
  *  - Otherwise, the Frama-C server is spawned.
  */
 export async function start() {
-  switch (status.stage) {
-    case Stage.OFF:
-    case Stage.FAILURE:
-    case Stage.RESTARTING:
-      _status(okStatus(Stage.STARTING));
+  switch (status) {
+    case Status.OFF:
+    case Status.FAILURE:
+    case Status.RESTARTING:
+      _status(Status.STARTING);
       try {
         await _launch();
-        _status(okStatus(Stage.ON));
       } catch (error) {
-        D.error(error.toString());
-        buffer.append(error.toString(), '\n');
-        _exit(error);
+        buffer.log('[frama-c]', error);
+        _exit(false);
       }
       return;
-    case Stage.HALTING:
-      _status(okStatus(Stage.RESTARTING));
+    case Status.HALTING:
+      _status(Status.RESTARTING);
       return;
     default:
       return;
@@ -288,22 +233,18 @@ export async function start() {
  *
  *  - If the server is starting, it is hard killed.
  *  - If the server is running, it is shutdown gracefully.
- *  - If the server is restarting, restart is canceled.
  *  - Otherwise, this is a no-op.
  */
 export function stop() {
-  switch (status.stage) {
-    case Stage.STARTING:
-      _status(okStatus(Stage.HALTING));
+  switch (status) {
+    case Status.STARTING:
+      _status(Status.HALTING);
       _kill();
       return;
-    case Stage.ON:
-      _status(okStatus(Stage.HALTING));
+    case Status.ON:
+      _status(Status.HALTING);
       _shutdown();
       return;
-    case Stage.RESTARTING:
-      _status(okStatus(Stage.HALTING));
-      return;
     default:
       return;
   }
@@ -321,12 +262,12 @@ export function stop() {
  *  - Otherwise, this is a no-op.
  */
 export function kill() {
-  switch (status.stage) {
-    case Stage.STARTING:
-    case Stage.ON:
-    case Stage.HALTING:
-    case Stage.RESTARTING:
-      _status(okStatus(Stage.HALTING));
+  switch (status) {
+    case Status.STARTING:
+    case Status.ON:
+    case Status.HALTING:
+    case Status.RESTARTING:
+      _status(Status.HALTING);
       _kill();
       return;
     default:
@@ -347,17 +288,17 @@ export function kill() {
  *  - Otherwise, this is a no-op.
  */
 export function restart() {
-  switch (status.stage) {
-    case Stage.OFF:
-    case Stage.FAILURE:
+  switch (status) {
+    case Status.OFF:
+    case Status.FAILURE:
       start();
       return;
-    case Stage.ON:
-      _status(okStatus(Stage.RESTARTING));
+    case Status.ON:
+      _status(Status.RESTARTING);
       _shutdown();
       return;
-    case Stage.HALTING:
-      _status(okStatus(Stage.RESTARTING));
+    case Status.HALTING:
+      _status(Status.RESTARTING);
       return;
     default:
       return;
@@ -376,11 +317,12 @@ export function restart() {
  *  - Otherwise, this is a no-op.
  */
 export function clear() {
-  switch (status.stage) {
-    case Stage.FAILURE:
-    case Stage.OFF:
+  switch (status) {
+    case Status.FAILURE:
+    case Status.OFF:
       buffer.clear();
-      _status(okStatus(Stage.OFF));
+      _clear();
+      _status(Status.OFF);
       return;
     default:
       return;
@@ -406,7 +348,7 @@ export interface Configuration {
   /** Shutdown timeout before server is hard killed, in milliseconds
    *  (default: 300ms). */
   timeout?: number;
-  /** Server polling period in milliseconds (default: 50ms). */
+  /** Server polling period in milliseconds (default: 200ms). */
   polling?: number;
   /** Process stdout log file (default: `undefined`). */
   logout?: string;
@@ -450,7 +392,7 @@ async function _launch() {
 
   buffer.clear();
   buffer.append('$', command);
-  const size = params.reduce((n: any, p: any) => n + p.length, 0);
+  const size = params.reduce((n, p) => n + p.length, 0);
   if (size < 40) {
     buffer.append('', ...params);
   } else {
@@ -466,16 +408,14 @@ async function _launch() {
   buffer.append('\n');
 
   if (!sockaddr) {
-    const tmp = System.getTempDir();
-    const pid = System.getPID();
-    const socketfile = System.join(tmp, `ivette.frama-c.${pid}.io`);
-    System.atExit(() => System.remove(socketfile));
-    sockaddr = `ipc://${socketfile}`;
+    const tmp = Dome.getTempDir();
+    const pid = Dome.getPID();
+    sockaddr = System.join(tmp, `ivette.frama-c.${pid}.io`);
   }
   if (!cwd) cwd = System.getWorkingDir();
   logout = logout && System.join(cwd, logout);
   logerr = logerr && System.join(cwd, logerr);
-  params = ['-server-zmq', sockaddr, '-then'].concat(params);
+  params = client.commandLine(sockaddr, params);
   const options = {
     cwd,
     stdout: { path: logout, pipe: true },
@@ -493,47 +433,33 @@ async function _launch() {
   process?.stdout?.on('data', logger);
   process?.stderr?.on('data', logger);
   process?.on('exit', (code: number | null, signal: string | null) => {
-    D.log('Process exited');
-
     if (signal) {
       // [signal] is non-null.
-      buffer.log('Signal:', signal);
-      const error = new Error(`Process terminated by the signal ${signal}`);
-      _exit(error);
+      buffer.log('[frama-c]', signal);
+      _exit(false);
       return;
     }
     // [signal] is null, hence [code] is non-null (cf. NodeJS doc).
     if (code) {
-      buffer.log('Exit:', code);
-      const error = new Error(`Process exited with code ${code}`);
-      _exit(error);
+      buffer.log('[frama-c] exit', code);
+      _exit(false);
     } else {
       // [code] is zero: normal exit w/o error.
-      _exit();
+      _exit(true);
     }
   });
   // Connect to Server
-  zmqSocket = new ZmqRequest();
-  zmqIsBusy = false;
-  zmqSocket.connect(sockaddr);
+  client.connect(sockaddr);
 }
 
 // --------------------------------------------------------------------------
 // --- Low-level Killing
 // --------------------------------------------------------------------------
 
-function _reset() {
-  D.log('Reset to initial configuration');
-
+function _clear() {
   rqCount = 0;
-  queueCmd = [];
-  queueId = [];
-  _.forEach(pending, ([, reject]) => reject(new Error('Server reset')));
-  pending = {};
-  if (flushingTimer) {
-    clearImmediate(flushingTimer);
-    flushingTimer = undefined;
-  }
+  pending.forEach((p: PendingRequest) => p.reject());
+  pending.clear();
   if (pollingTimer) {
     clearTimeout(pollingTimer);
     pollingTimer = undefined;
@@ -545,20 +471,13 @@ function _reset() {
 }
 
 function _kill() {
-  D.log('Hard kill');
-
-  _reset();
-  if (process) {
-    process.kill();
-  }
+  client.disconnect();
+  if (process) process.kill();
 }
 
 async function _shutdown() {
-  D.log('Shutdown');
-
-  _reset();
-  queueCmd.push('SHUTDOWN');
-  _flush();
+  _clear();
+  client.shutdown();
   const killingPromise = new Promise((resolve) => {
     if (!killingTimer) {
       if (process) {
@@ -573,21 +492,14 @@ async function _shutdown() {
   await killingPromise;
 }
 
-function _exit(error?: Error) {
-  _reset();
-  if (zmqSocket) {
-    zmqSocket.close();
-    zmqSocket = undefined;
-  }
-  zmqIsBusy = false;
+function _exit(error: boolean) {
+  _clear();
+  client.disconnect();
   process = undefined;
-  if (status.stage === Stage.RESTARTING) {
+  if (status === Status.RESTARTING) {
     setImmediate(start);
-  } else if (error) {
-    _status(errorStatus(error.toString()));
-  } else {
-    _status(okStatus(Stage.OFF));
   }
+  _status(error ? Status.FAILURE : Status.OFF);
 }
 
 // --------------------------------------------------------------------------
@@ -595,18 +507,19 @@ function _exit(error?: Error) {
 // --------------------------------------------------------------------------
 
 class SignalHandler {
-  id: any;
+  id: string;
   event: Dome.Event;
   active: boolean;
   listen: boolean;
+  handler: _.DebouncedFunc<() => void>;
 
-  constructor(id: any) {
+  constructor(id: string) {
     this.id = id;
     this.event = new SIGNAL(id);
     this.active = false;
     this.listen = false;
     this.sigon = this.sigon.bind(this);
-    this.sigoff = _.debounce(this.sigoff.bind(this), 1000);
+    this.sigoff = this.handler = debounce(this.sigoff.bind(this), 1000);
     this.unplug = this.unplug.bind(this);
   }
 
@@ -635,8 +548,7 @@ class SignalHandler {
   sigon() {
     if (this.active && !this.listen) {
       this.listen = true;
-      queueCmd.push('SIGON', this.id);
-      _flush();
+      client.sigOn(this.id);
     }
   }
 
@@ -645,14 +557,18 @@ class SignalHandler {
     if (!this.active && this.listen) {
       if (isRunning()) {
         this.listen = false;
-        queueCmd.push('SIGOFF', this.id);
-        _flush();
+        client.sigOff(this.id);
       }
     }
   }
 
+  emit() {
+    this.event.emit();
+  }
+
   unplug() {
     this.listen = false;
+    this.handler.cancel();
   }
 }
 
@@ -660,7 +576,7 @@ class SignalHandler {
 
 const signals: Map<string, SignalHandler> = new Map();
 
-function _signal(id: any) {
+function _signal(id: string): SignalHandler {
   let s = signals.get(id);
   if (!s) {
     s = new SignalHandler(id);
@@ -679,7 +595,7 @@ function _signal(id: any) {
  *  @param {string} id The signal identifier to listen to.
  *  @param {function} callback The callback to call upon signal.
  */
-export function onSignal(s: Signal, callback: any) {
+export function onSignal(s: Signal, callback: () => void) {
   _signal(s.name).on(callback);
 }
 
@@ -691,7 +607,7 @@ export function onSignal(s: Signal, callback: any) {
  *  @param {string} id The signal identifier that was listen to.
  *  @param {function} callback The callback to remove.
  */
-export function offSignal(s: Signal, callback: any) {
+export function offSignal(s: Signal, callback: () => void) {
   _signal(s.name).off(callback);
 }
 
@@ -700,7 +616,7 @@ export function offSignal(s: Signal, callback: any) {
  *  @param {string} id The signal identifier to listen to.
  *  @param {function} callback The callback to call upon signal.
  */
-export function useSignal(s: Signal, callback: any) {
+export function useSignal(s: Signal, callback: () => void) {
   React.useEffect(() => {
     onSignal(s, callback);
     return () => { offSignal(s, callback); };
@@ -718,7 +634,6 @@ READY.on(() => {
 SHUTDOWN.on(() => {
   signals.forEach((h: SignalHandler) => {
     h.unplug();
-    (h.sigoff as unknown as _.Cancelable).cancel();
   });
 });
 
@@ -733,7 +648,7 @@ export enum RqKind {
   /** Used to write data into the Frama-C server. */
   SET = 'SET',
   /** Used to make the Frama-C server execute a task. */
-  EXEC = 'EXEC'
+  EXEC = 'EXEC',
 }
 
 /** Server signal. */
@@ -758,7 +673,7 @@ export type GetRequest<In, Out> = Request<RqKind.GET, In, Out>;
 export type SetRequest<In, Out> = Request<RqKind.SET, In, Out>;
 export type ExecRequest<In, Out> = Request<RqKind.EXEC, In, Out>;
 
-export interface Killable<Data> extends Promise<Data> {
+export interface Response<Data> extends Promise<Data> {
   kill?: () => void;
 }
 
@@ -771,153 +686,86 @@ export interface Killable<Data> extends Promise<Data> {
 export function send<In, Out>(
   request: Request<RqKind, In, Out>,
   param: In,
-): Killable<Out> {
-  if (!isRunning()) return Promise.reject(new Error('Server not running'));
-  if (!request.name) return Promise.reject(new Error('Undefined request'));
+): Response<Out> {
+  if (!isRunning()) return Promise.reject('Server not running');
+  if (!request.name) return Promise.reject('Undefined request');
   const rid = `RQ.${rqCount}`;
   rqCount += 1;
-  const data = JSON.stringify(param);
-  const promise: Killable<Out> = new Promise<Out>((resolve, reject) => {
-    const decodedResolve = (js: Json.json) => {
-      const result = Json.jTry(request.output)(js);
-      resolve(result);
+  const response: Response<Out> = new Promise<Out>((resolve, reject) => {
+    const unwrap = (js: Json.json) => {
+      const data = request.output(js);
+      resolve(data as unknown as Out);
     };
-    pending[rid] = [decodedResolve, reject];
+    pending.set(rid, { resolve: unwrap, reject });
   });
-  promise.kill = () => {
-    if (zmqSocket && pending[rid]) {
-      queueCmd.push('KILL', rid);
-      _flush();
-    }
-  };
-  queueCmd.push(request.kind, rid, request.name, data);
-  queueId.push(rid);
-  _flush();
-  return promise;
-}
-
-function _resolve(id: string | number, data: string) {
-  const [resolve] = pending[id];
-  if (resolve) {
-    delete pending[id];
-    resolve(JSON.parse(data));
-  }
-}
-
-function _reject(id: string | number, error: Error) {
-  const [, reject] = pending[id];
-  if (reject) {
-    delete pending[id];
-    reject(error);
+  response.kill = () => pending.get(rid)?.reject();
+  client.send(request.kind, rid, request.name, param);
+  if (!pollingTimer) {
+    const polling = (config && config.polling) || pollingTimeout;
+    pollingTimer = setInterval(() => {
+      client.poll();
+    }, polling);
   }
-}
-
-function _cancel(ids: any[]) {
-  ids.forEach((rid) => _reject(rid, new Error('Canceled request')));
-}
-
-function _waiting() {
-  return _.find(pending, () => true) !== undefined;
+  return response;
 }
 
 // --------------------------------------------------------------------------
-// --- Server Command Queue
+// --- Client Events
 // --------------------------------------------------------------------------
 
-function _flush() {
-  if (!flushingTimer) {
-    flushingTimer = setImmediate(() => {
-      flushingTimer = undefined;
-      _send();
-    });
+function _resolved(id: string) {
+  pending.delete(id);
+  if (pending.size == 0) {
+    rqCount = 0;
+    if (pollingTimer) {
+      clearInterval(pollingTimer);
+      pollingTimer = undefined;
+    }
   }
 }
 
-function _poll() {
-  if (!pollingTimer) {
-    const delay = (config && config.polling) || pollingTimeout;
-    pollingTimer = setTimeout(() => {
-      pollingTimer = undefined;
-      _send();
-    }, delay);
+client.onConnect((err?: Error) => {
+  if (err) {
+    _status(Status.FAILURE);
+  } else {
+    _status(Status.ON);
   }
-}
+});
 
-async function _send() {
-  // when busy, will be eventually re-triggered
-  if (!zmqIsBusy) {
-    const cmds = queueCmd;
-    if (!cmds.length) {
-      cmds.push('POLL');
-      if (!_waiting())
-        rqCount = 0; // No pending command nor pending response
-    }
-    zmqIsBusy = true;
-    const ids = queueId;
-    queueCmd = [];
-    queueId = [];
-    try {
-      await zmqSocket?.send(cmds);
-      const resp = await zmqSocket?.receive();
-      _receive(resp);
-    } catch (error) {
-      D.error(`Error in send/receive on ZMQ socket. ${error.toString()}`);
-      _cancel(ids);
-    }
-    zmqIsBusy = false;
-    STATUS.emit(status);
+client.onData((id: string, data: Json.json) => {
+  const p = pending.get(id);
+  if (p) {
+    p.resolve(data);
+    _resolved(id);
   }
-}
+});
 
-function _receive(resp: any) {
-  try {
-    let rid;
-    let data;
-    let err;
-    let cmd;
-    const shift = () => resp.shift().toString();
-    let unknownResponse = false;
-    while (resp.length && !unknownResponse) {
-      cmd = shift();
-      switch (cmd) {
-        case 'NONE':
-          break;
-        case 'DATA':
-          rid = shift();
-          data = shift();
-          _resolve(rid, data);
-          break;
-        case 'KILLED':
-          rid = shift();
-          _reject(rid, new Error('Killed'));
-          break;
-        case 'ERROR':
-          rid = shift();
-          err = shift();
-          _reject(rid, err);
-          break;
-        case 'REJECTED':
-          rid = shift();
-          _reject(rid, new Error('Rejected'));
-          break;
-        case 'SIGNAL':
-          rid = shift();
-          (new SIGNAL(rid)).emit();
-          break;
-        case 'WRONG':
-          err = shift();
-          D.error(`ZMQ Protocol Error: ${err}`);
-          break;
-        default:
-          D.error(`Unknown Response: ${cmd}`);
-          unknownResponse = true;
-          break;
-      }
-    }
-  } finally {
-    if (queueCmd.length) _flush();
-    else _poll();
+client.onKilled((id: string) => {
+  const p = pending.get(id);
+  if (p) {
+    p.reject();
+    _resolved(id);
   }
-}
+});
+
+client.onRejected((id: string) => {
+  const p = pending.get(id);
+  if (p) {
+    p.reject('rejected');
+    _resolved(id);
+  }
+});
+
+client.onError((id: string, msg: string) => {
+  const p = pending.get(id);
+  if (p) {
+    p.reject(msg);
+    _resolved(id);
+  }
+});
+
+client.onSignal((id: string) => {
+  _signal(id).emit();
+});
 
 // --------------------------------------------------------------------------

ivette/src/frama-c/states.ts

@@ -72,7 +72,7 @@ Server.onReady(async () => {
     currentProject = current.id;
     PROJECT.emit();
   } catch (error) {
-    D.error(`Fail to retrieve the current project. ${error.toString()}`);
+    D.error(`Fail to retrieve the current project. ${error}`);
   }
 });
 
@@ -116,7 +116,7 @@ export async function setProject(project: string) {
       currentProject = project;
       PROJECT.emit();
     } catch (error) {
-      D.error(`Fail to set the current project. ${error.toString()}`);
+      D.error(`Fail to set the current project. ${error}`);
     }
   }
 }
@@ -171,7 +171,7 @@ export function useRequest<In, Out>(
         const r = await Server.send(rq, params);
         update(r);
       } catch (error) {
-        D.error(`Fail in useRequest '${rq.name}'. ${error.toString()}`);
+        D.error(`Fail in useRequest '${rq.name}'. ${error}`);
         update(options.onError);
       }
     } else {
@@ -300,7 +300,7 @@ class SyncState<A> {
     } catch (error) {
       D.error(
         `Fail to set value of SyncState '${this.handler.name}'.`,
-        `${error.toString()}`,
+        `${error}`,
       );
     }
   }
@@ -308,13 +308,16 @@ class SyncState<A> {
   async update() {
     try {
       this.upToDate = true;
-      const v = await Server.send(this.handler.getter, null);
-      this.value = v;
+      this.value = undefined;
+      if (Server.isRunning()) {
+        const v = await Server.send(this.handler.getter, null);
+        this.value = v;
+      }
       this.UPDATE.emit();
     } catch (error) {
       D.error(
         `Fail to update SyncState '${this.handler.name}'.`,
-        `${error.toString()}`,
+        `${error}`,
       );
     }
   }
@@ -407,7 +410,7 @@ class SyncArray<K, A> {
     } catch (error) {
       D.error(
         `Fail to retrieve the value of syncArray '${this.handler.name}.`,
-        `${error.toString()}`,
+        `${error}`,
       );
     } finally {
       this.fetching = false;
@@ -426,7 +429,7 @@ class SyncArray<K, A> {
     } catch (error) {
       D.error(
         `Fail to set reload of syncArray '${this.handler.name}'.`,
-        `${error.toString()}`,
+        `${error}`,
       );
     }
   }
@@ -477,7 +480,7 @@ export function useSyncArray<K, A>(
 ): CompactModel<K, A> {
   Dome.useUpdate(PROJECT);
   const st = lookupSyncArray(arr);
-  React.useEffect(st.update);
+  React.useEffect(() => st.update(), [st]);
   Server.useSignal(arr.signal, st.fetch);
   useModel(st.model, sync);
   return st.model;
@@ -761,6 +764,7 @@ const emptySelection = {
 
 export const MetaSelection = new Dome.Event<Location>('frama-c-meta-selection');
 export const GlobalSelection = new GlobalState<Selection>(emptySelection);
+
 Server.onShutdown(() => GlobalSelection.setValue(emptySelection));
 
 export function setSelection(location: Location, meta = false) {
@@ -778,12 +782,19 @@ export function useSelection(): [Selection, (a: SelectionActions) => void] {
 /** Resets the selected locations. */
 export async function resetSelection() {
   GlobalSelection.setValue(emptySelection);
-  const main = await Server.send(Ast.getMainFunction, { });
-  // If the selection has already been modified, do not change it.
-  if (main && GlobalSelection.getValue() === emptySelection) {
-    GlobalSelection.setValue({ ...emptySelection, current: { fct: main } });
+  if (Server.isRunning()) {
+    try {
+      const main = await Server.send(Ast.getMainFunction, {});
+      // If the selection has already been modified, do not change it.
+      if (main && GlobalSelection.getValue() === emptySelection) {
+        GlobalSelection.setValue({ ...emptySelection, current: { fct: main } });
+      }
+    } catch (err) {
+      if (err) D.warn('Request error', err);
+    }
   }
 }
+
 /* Select the main function when the current project changes and the selection
    is still empty (which happens at the start of the GUI). */
 PROJECT.on(async () => {

ivette/src/renderer/Controller.tsx

@@ -30,7 +30,8 @@ import * as Json from 'dome/data/json';
 import * as Settings from 'dome/data/settings';
 
 import * as Toolbars from 'dome/frame/toolbars';
-import { LED, LEDstatus, IconButton } from 'dome/controls/buttons';
+import { IconButton } from 'dome/controls/buttons';
+import { LED, LEDstatus } from 'dome/controls/displays';
 import { Label, Code } from 'dome/controls/labels';
 import { RichTextBuffer } from 'dome/text/buffers';
 import { Text } from 'dome/text/editors';
@@ -149,12 +150,12 @@ export const Control = () => {
   let stop = { enabled: false, onClick: () => { } };
   let reload = { enabled: false, onClick: () => { } };
 
-  switch (status.stage) {
-    case Server.Stage.OFF:
-    case Server.Stage.FAILURE:
+  switch (status) {
+    case Server.Status.OFF:
       play = { enabled: true, onClick: Server.start };
       break;
-    case Server.Stage.ON:
+    case Server.Status.ON:
+    case Server.Status.FAILURE:
       stop = { enabled: true, onClick: Server.stop };
       reload = { enabled: true, onClick: Server.restart };
       break;
@@ -357,44 +358,45 @@ Ivette.registerView({
 export const Status = () => {
   const status = Server.useStatus();
   const pending = Server.getPending();
-  let led: LEDstatus;
-  let blink;
-  let error;
-
-  if (Server.hasErrorStatus(status)) {
-    led = 'negative';
-    blink = false;
-    error = status.error;
-  } else {
-    switch (status.stage) {
-      case Server.Stage.OFF:
-        led = 'inactive';
-        break;
-      case Server.Stage.STARTING:
-        led = 'active';
-        blink = true;
-        break;
-      case Server.Stage.ON:
-        led = pending > 0 ? 'positive' : 'active';
-        break;
-      case Server.Stage.HALTING:
-        led = 'negative';
-        blink = true;
-        break;
-      case Server.Stage.RESTARTING:
-        led = 'warning';
-        blink = true;
-        break;
-      default:
-        break;
-    }
+  let led: LEDstatus = 'inactive';
+  let icon = undefined;
+  let running = false;
+  let blink = false;
+
+  switch (status) {
+    case Server.Status.OFF:
+      break;
+    case Server.Status.STARTING:
+      led = 'active';
+      blink = true;
+      running = true;
+      break;
+    case Server.Status.ON:
+      led = pending > 0 ? 'positive' : 'active';
+      running = true;
+      break;
+    case Server.Status.HALTING:
+      led = 'negative';
+      blink = true;
+      running = true;
+      break;
+    case Server.Status.RESTARTING:
+      led = 'warning';
+      blink = true;
+      running = true;
+      break;
+    case Server.Status.FAILURE:
+      led = 'negative';
+      blink = true;
+      running = false;
+      icon = 'WARNING';
+      break;
   }
 
   return (
     <>
       <LED status={led} blink={blink} />
-      <Code label={status.stage} />
-      {error && <Label icon="WARNING" label={error} />}
+      <Code icon={icon} label={running ? 'ON' : 'OFF'} />
       <Toolbars.Separator />
     </>
   );