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/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 />
     </>
   );