[ivette] Studia can be applied on arbitrary lvalues via a dedicated search mode.

ivette/src/dome/renderer/dark.css

@@ -88,6 +88,8 @@
     --meter-subopti:  linear-gradient(to bottom, #770 0%, #cc0 20%, #770 100%);
     --meter-evenless: linear-gradient(to bottom, #710 0%, #c50 20%, #710 100%);
 
+    --studia-search-mode: #c2c71e;
+
     --eva-evaluation-mode: #714074;
     --eva-state-before: #082032;
     --eva-state-after: #321428;

ivette/src/dome/renderer/light.css

@@ -88,6 +88,8 @@
     --meter-subopti:  linear-gradient(to bottom, #aa0 0%, #ff0 20%, #aa0 100%);
     --meter-evenless: linear-gradient(to bottom, #a40 0%, #f80 20%, #a40 100%);
 
+    --studia-search-mode: #c5dc19;
+
     --eva-evaluation-mode: #dc8fe1;
     --eva-state-before: #95f5ff;
     --eva-state-after: #fff819;

ivette/src/frama-c/plugins/studia/studia.ts

@@ -20,11 +20,21 @@
 /*                                                                          */
 /* ************************************************************************ */
 
+import React from 'react';
 import * as Dome from 'dome';
 import * as States from 'frama-c/states';
 import * as Server from 'frama-c/server';
+import * as Toolbars from 'dome/frame/toolbars';
+import * as Status from 'frama-c/kernel/Status';
 import * as Ast from 'frama-c/kernel/api/ast';
 import { getWritesLval, getReadsLval } from 'frama-c/plugins/studia/api/studia';
+import { ipcRenderer } from 'electron';
+import './style.css';
+
+const studiaWritesEvent = new Dome.Event('dome.studia.writes');
+const studiaReadsEvent = new Dome.Event('dome.studia.reads');
+ipcRenderer.on('dome.ipc.studia.writes', () => studiaWritesEvent.emit());
+ipcRenderer.on('dome.ipc.studia.reads', () => studiaReadsEvent.emit());
 
 type access = 'Reads' | 'Writes';
 
@@ -68,3 +78,46 @@ export function buildMenu(props: MenuProps) : void {
   menu.push({ label: reads, enabled, onClick: () => onClick('Reads') });
   menu.push({ label: writes, enabled, onClick: () => onClick('Writes') });
 }
+
+export function useStudiaMode(): void {
+  const [selection, setSelection] = States.useSelection();
+  async function handleError(err: string): Promise<void> {
+    const msg = `Studia failure: ${err}.`;
+    Status.setMessage({ text: msg, kind: 'error' });
+  }
+  async function onEnter(label: string, kind: access): Promise<void> {
+    const stmt = selection?.current?.marker;
+    const data = { stmt, term: label };
+    const marker = await Server.send(Ast.parseLval, data).catch(handleError);
+    if (!marker) return;
+    compute(marker, label, kind).then(setSelection).catch(handleError);
+  }
+  const shared = {
+    placeholder: "lvalue",
+    icon: 'EDIT',
+    className: 'studia-search-mode',
+    hints: () => { return Promise.resolve([]); },
+  };
+  const writesMode = {
+    ...shared,
+    label: 'Studia: select writes',
+    title: `Select all statements writing the given lvalue`,
+    onEnter: (pattern:string) => onEnter(pattern, "Writes"),
+    event: studiaWritesEvent,
+  };
+  const readsMode = {
+    ...shared,
+    label: 'Studia: select reads',
+    title: `Selects all statements reading the given lvalue`,
+    onEnter: (pattern:string) => onEnter(pattern, "Reads"),
+    event: studiaReadsEvent,
+  };
+  React.useEffect(() => {
+    Toolbars.RegisterMode.emit(writesMode);
+    Toolbars.RegisterMode.emit(readsMode);
+    return () => {
+      Toolbars.UnregisterMode.emit(writesMode);
+      Toolbars.UnregisterMode.emit(readsMode);
+    };
+  });
+}

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

+
+.studia-search-mode {
+  background: var(--studia-search-mode);
+  fill: var(--text-discrete);
+}

ivette/src/renderer/Application.tsx

@@ -36,6 +36,7 @@ import * as Controller from './Controller';
 import * as Extensions from './Extensions';
 import * as Laboratory from './Laboratory';
 import * as IvettePrefs from 'ivette/prefs';
+import * as Studia from 'frama-c/plugins/studia/studia';
 import './loader';
 import './sandbox';
 
@@ -49,6 +50,8 @@ export default function Application(): JSX.Element {
   const [viewbar, flipViewbar] =
     Dome.useFlipSettings('frama-c.viewbar.unfold', true);
 
+  Studia.useStudiaMode();
+
   return (
     <Vfill>
       <Toolbar.ToolBar>