diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts
index 990ad2cc51d520b8f6f898c009bbf4c0572bf1cb..d400a9745fe2cb5429a904414641a6def97d3a0e 100644
--- a/ivette/src/frama-c/server.ts
+++ b/ivette/src/frama-c/server.ts
@@ -756,7 +756,10 @@ export interface Killable<Data> extends Promise<Data> {
* You may _kill_ the request before its normal termination by
* invoking `kill()` on the returned promised.
*/
-export function send<In, Out>(request: Request<RqKind, In, Out>, param: In): Killable<Out> {
+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'));
const rid = `RQ.${rqCount}`;
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 7cabcbad64ff3c851c1cc28e1b747bdf79e0626f..fdb800f823f6122c261fb0e74d7055f096ade0ff 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -130,11 +130,12 @@ export function useRequest<In, Out>(
const project = useProject();
const [response, setResponse] =
React.useState<Out | undefined>(options.offline ?? undefined);
- const footprint = project ? JSON.stringify([project, rq.name, params]) : undefined;
+ const footprint =
+ project ? JSON.stringify([project, rq.name, params]) : undefined;
const update = (opt: Out | undefined | null) => {
if (opt !== null) setResponse(opt);
- }
+ };
async function trigger() {
if (project && rq && params !== undefined) {
@@ -169,7 +170,7 @@ export type Tag = {
name: string;
label?: string;
descr?: string;
-}
+};
const holdCurrent = { offline: null, pending: null, onError: null };
@@ -179,9 +180,10 @@ export function useTags(rq: GetTags): Map<string, Tag> {
const tags = useRequest(rq, null, holdCurrent);
return React.useMemo(() => {
const m = new Map<string, Tag>();
- tags && tags.forEach((tg) => m.set(tg.name, tg));
+ if (tags !== undefined)
+ tags.forEach((tg) => m.set(tg.name, tg));
return m;
- }, tags);
+ }, [tags]);
}
// --------------------------------------------------------------------------
@@ -205,7 +207,7 @@ export interface Fetches<K, A> {
reload: boolean;
pending: number;
updated: A[];
- removed: Json.key<K>[]
+ removed: Json.key<K>[];
}
export interface Array<K, A> {
@@ -216,7 +218,7 @@ export interface Array<K, A> {
reload: Server.GetRequest<null, null>;
}
-type id = { project: string, state: string };
+type id = { project: string; state: string };
// --------------------------------------------------------------------------
// --- Handler for Synchronized St byates
@@ -265,7 +267,8 @@ class SyncState<A> {
Dome.emit(this.UPDATE);
} catch (error) {
PP.error(
- `Fail to set value of syncState '${this.handler.name}'. ${error.toString()}`,
+ `Fail to set value of syncState '${this.handler.name}'.`,
+ `${error.toString()}`,
);
}
}
@@ -277,7 +280,10 @@ class SyncState<A> {
this.value = v;
Dome.emit(this.UPDATE);
} catch (error) {
- PP.error(`Fail to update syncState '${this.handler.name}'. ${error.toString()}`);
+ PP.error(
+ `Fail to update syncState '${this.handler.name}'.`,
+ `${error.toString()}`,
+ );
}
}
}
@@ -307,7 +313,9 @@ Server.onShutdown(() => syncStates.clear());
/**
Synchronization with a (projectified) server state.
*/
-export function useSyncState<A>(st: State<A>): [A | undefined, (value: A) => void] {
+export function useSyncState<A>(
+ st: State<A>,
+): [A | undefined, (value: A) => void] {
const s = getSyncState(st);
Dome.useUpdate(PROJECT, s.UPDATE);
Server.useSignal(s.handler.signal, s.update);
@@ -328,20 +336,13 @@ export function useSyncValue<A>(va: Value<A>): A | undefined {
// --- Synchronized Arrays
// --------------------------------------------------------------------------
-export interface Model<A> {
- clear(): void;
- remove(key: string): void;
- add(entry: A): void;
- clear(): void;
-}
-
// one per project
class SyncArray<K, A> {
handler: Array<K, A>;
- model: Model<A>;
+ model: ArrayModel<A>;
insync: boolean;
- constructor(h: Array<K, A>, m?: Model<A>) {
+ constructor(h: Array<K, A>, m?: ArrayModel<A>) {
this.handler = h;
this.insync = false;
this.model = m ?? new ArrayModel<A>(h.key);
@@ -354,7 +355,7 @@ class SyncArray<K, A> {
this.insync = true;
const data = await Server.send(this.handler.fetch, 50);
const { reload = false, removed = [], updated = [], pending = 0 } = data;
- const model = this.model;
+ const { model } = this;
if (reload) model.clear();
removed.forEach((k) => model.remove(k));
updated.forEach((d) => model.add(d));
@@ -388,18 +389,19 @@ class SyncArray<K, A> {
const syncArrays = new Map<id, SyncArray<any, any>>();
-function getSyncArray<K, A>(arr: Array<K, A>, model?: Model<A>): SyncArray<K, A> {
+function getSyncArray<K, A>(
+ arr: Array<K, A>,
+ model?: ArrayModel<A>,
+): SyncArray<K, A> {
const id = { project: currentProject ?? '', state: arr.name };
let a = syncArrays.get(id);
if (!a) {
a = new SyncArray(arr, model);
syncArrays.set(id, a);
- } else {
- if (model && a.model !== model) {
- model.clear();
- a.reload();
- a.model = model;
- }
+ } else if (model && a.model !== model) {
+ model.clear();
+ a.reload();
+ a.model = model;
}
return a;
}
@@ -420,7 +422,10 @@ export function reloadArray<K, A>(arr: Array<K, A>) {
/**
Use Synchronized Array (Custom React Hook).
*/
-export function useSyncArray<K, A>(arr: Array<K, A>, model?: Model<A>): Model<A> {
+export function useSyncArray<K, A>(
+ arr: Array<K, A>,
+ model?: ArrayModel<A>,
+): ArrayModel<A> {
const a = getSyncArray(arr, model);
Dome.useUpdate(PROJECT);
Server.useSignal(arr.signal, a.fetch);
@@ -431,7 +436,8 @@ export function useSyncArray<K, A>(arr: Array<K, A>, model?: Model<A>): Model<A>
// --- Selection
// --------------------------------------------------------------------------
-type AtLeastOne<T, U = { [K in keyof T]: Pick<T, K> }> = Partial<T> & U[keyof U];
+type AtLeastOne<T, U = { [K in keyof T]: Pick<T, K> }> =
+ Partial<T> & U[keyof U];
export interface FullLocation {
/** Function name. */
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index d786d7cf0384dced4a6d83799be9a40f57214523..5ec7d4272ee271fe08ada8ae7259e25ae2c9f4cc 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -7,11 +7,15 @@ import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import * as Dome from 'dome';
+import { key } from 'dome/data/json';
import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { IconButton } from 'dome/controls/buttons';
import { Component, TitleBar } from 'frama-c/LabViews';
+import { printFunction, markerInfo } from 'api/kernel/ast';
+
+
import 'codemirror/mode/clike/clike';
import 'codemirror/theme/ambiance.css';
import 'codemirror/theme/solarized.css';
@@ -41,10 +45,7 @@ async function loadAST(
buffer.log('// Loading', theFunction, '…');
(async () => {
try {
- const data = await Server.GET({
- endpoint: 'kernel.ast.printFunction',
- params: theFunction,
- });
+ const data = await Server.send(printFunction, theFunction);
buffer.operation(() => {
buffer.clear();
if (!data) {
@@ -77,7 +78,7 @@ const ASTview = () => {
const [theme, setTheme] = Dome.useGlobalSetting('ASTview.theme', 'default');
const [fontSize, setFontSize] = Dome.useGlobalSetting('ASTview.fontSize', 12);
const [wrapText, setWrapText] = Dome.useSwitch('ASTview.wrapText', false);
- const markers = States.useSyncArray('kernel.ast.markerKind');
+ const markers = States.useSyncArray(markerInfo);
const theFunction = selection?.current?.function;
const theMarker = selection?.current?.marker;
@@ -99,15 +100,15 @@ const ASTview = () => {
const zoomIn = () => fontSize < 48 && setFontSize(fontSize + 2);
const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2);
- function onTextSelection(id: string) {
+ function onTextSelection(id: key<'#markerIndo'>) {
if (selection.current) {
const location = { ...selection.current, marker: id };
updateSelection({ location });
}
}
- function onContextMenu(id: string) {
- const marker = markers[id];
+ function onContextMenu(id: key<'#markerInfo'>) {
+ const marker = markers.getData(id);
if (marker && marker.kind === 'function') {
const item = {
label: `Go to definition of ${marker.name}`,
diff --git a/ivette/src/renderer/Globals.tsx b/ivette/src/renderer/Globals.tsx
index 62a3c702e9b56067a1c3acb5cf63148e1867e5bb..94a501716c0d18f29a6ed499b6cbf46e716ddb99 100644
--- a/ivette/src/renderer/Globals.tsx
+++ b/ivette/src/renderer/Globals.tsx
@@ -3,22 +3,11 @@
// --------------------------------------------------------------------------
import React from 'react';
-import { toArray, Dictionary } from 'lodash';
+import * as Dome from 'dome';
import { Section, Item } from 'dome/frame/sidebars';
import * as States from 'frama-c/states';
import { alpha } from 'dome/data/compare';
-
-// --------------------------------------------------------------------------
-// --- Globals API
-// --------------------------------------------------------------------------
-
-interface Gfun {
- key: string;
- name: string;
- signature: string;
-}
-
-type Gfuns = undefined | Dictionary<Gfun>;
+import { functions, functionsData } from 'api/kernel/ast';
// --------------------------------------------------------------------------
// --- Globals Section
@@ -28,13 +17,25 @@ export default () => {
// Hooks
const [selection, updateSelection] = States.useSelection();
- const gfuns: Gfuns = States.useSyncArray('kernel.ast.functions');
+ const model = States.useSyncArray(functions);
+ const forceUpdate = Dome.useForceUpdate() as (() => void);
+ React.useEffect(() => {
+ model.setNaturalOrder((f1, f2) => alpha(f1.name, f2.name));
+ const client = model.link();
+ client.onReload(forceUpdate);
+ client.onUpdate(forceUpdate);
+ return client.unlink;
+ }, [model, forceUpdate]);
// Functions
- const functions = toArray(gfuns).sort((f1, f2) => alpha(f1.name, f2.name));
+ const n = model.getRowCount();
+ const fcts: functionsData[] = [];
+ for (let i = 0; i < n; i++) {
+ fcts.push(model.getRowAt(i));
+ }
const current: undefined | string = selection?.current?.function;
- const makeFctItem = (fct: Gfun) => {
+ const makeFctItem = (fct: functionsData) => {
const kf = fct.name;
return (
<Item
@@ -49,7 +50,7 @@ export default () => {
return (
<Section label="Functions">
- {functions.map(makeFctItem)}
+ {fcts.map(makeFctItem)}
</Section>
);
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index ea50893a20a871bc6cfa182fa547e3f99796ab26..6e44c4a4d550204ecd981c136c6af1170f36804e 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -87,7 +87,10 @@ const defaultFilter =
};
-function filterStatus(f: typeof defaultStatusFilter, status: Properties.propStatus) {
+function filterStatus(
+ f: typeof defaultStatusFilter,
+ status: Properties.propStatus,
+) {
switch (status) {
case 'valid':
case 'valid_but_dead': return f.valid;
@@ -104,7 +107,10 @@ function filterStatus(f: typeof defaultStatusFilter, status: Properties.propStat
}
}
-function filterKind(f: typeof defaultKindFilter, kind: Properties.propKind) {
+function filterKind(
+ f: typeof defaultKindFilter,
+ kind: Properties.propKind,
+) {
switch (kind) {
case 'assert': return f.assert;
case 'loop_invariant':
@@ -232,7 +238,7 @@ const byColumn: Arrays.ByColumns<Property> = {
file: Compare.byFields<Property>({ source: byFile }),
};
-class PropertyModel extends Arrays.ArrayModel<Property> implements States.Model<Property> {
+class PropertyModel extends Arrays.ArrayModel<Property> {
private filterFun?: string;
private filterProp = _.cloneDeep(defaultFilter);
@@ -431,7 +437,7 @@ const RenderTable = () => {
// Hooks
const model = React.useMemo(() => new PropertyModel(), []);
- States.useSyncArray<"#status", Property>(Properties.status, model);
+ States.useSyncArray<'#status', Property>(Properties.status, model);
const [selection, updateSelection] = States.useSelection();