diff --git a/ivette/Makefile.distrib b/ivette/Makefile.distrib
index 87068f0322f67cc1f5c8ab9c6f920bfad9e9c91d..5a9f51b860bd01aa024cfba11c79fe817b7c2e66 100644
--- a/ivette/Makefile.distrib
+++ b/ivette/Makefile.distrib
@@ -175,19 +175,10 @@ DISTRIB_FILES += ivette/src/frama-c/plugins/eva/CoverageMeter.tsx
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/Summary.tsx
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/api/general/index.ts
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/api/values/index.ts
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/cells.ts
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/diffed.tsx
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/index.tsx
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/layout.ts
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/model.ts
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/pkg.json
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/probeinfos.tsx
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/probes.ts
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/sized.tsx
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/stacks.ts
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/style.css
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/summary.css
-DISTRIB_FILES += ivette/src/frama-c/plugins/eva/valueinfos.tsx
DISTRIB_FILES += ivette/src/frama-c/plugins/eva/valuetable.tsx
DISTRIB_FILES += ivette/src/frama-c/plugins/pivot/api/general/index.ts
DISTRIB_FILES += ivette/src/frama-c/plugins/studia/api/studia/index.ts
diff --git a/ivette/headers/header_spec.txt b/ivette/headers/header_spec.txt
index 75e97fe5eb7d202f311cc244e23d696311dd3544..1bc4d6658222a8e3a2f26ecc01df72c5e949cb30 100644
--- a/ivette/headers/header_spec.txt
+++ b/ivette/headers/header_spec.txt
@@ -173,22 +173,13 @@ src/frama-c/plugins/dive/tippy.css: .ignore
src/frama-c/plugins/eva/Coverage.tsx: CEA_LGPL
src/frama-c/plugins/eva/CoverageMeter.tsx: CEA_LGPL
src/frama-c/plugins/eva/Summary.tsx: CEA_LGPL
+src/frama-c/plugins/eva/valuetable.tsx: CEA_LGPL
src/frama-c/plugins/eva/api/general/index.ts: CEA_LGPL
src/frama-c/plugins/eva/api/values/index.ts: CEA_LGPL
-src/frama-c/plugins/eva/cells.ts: CEA_LGPL
-src/frama-c/plugins/eva/diffed.tsx: CEA_LGPL
src/frama-c/plugins/eva/index.tsx: CEA_LGPL
-src/frama-c/plugins/eva/layout.ts: CEA_LGPL
-src/frama-c/plugins/eva/model.ts: CEA_LGPL
src/frama-c/plugins/eva/pkg.json: .ignore
-src/frama-c/plugins/eva/probeinfos.tsx: CEA_LGPL
-src/frama-c/plugins/eva/probes.ts: CEA_LGPL
-src/frama-c/plugins/eva/sized.tsx: CEA_LGPL
-src/frama-c/plugins/eva/stacks.ts: CEA_LGPL
src/frama-c/plugins/eva/style.css: .ignore
src/frama-c/plugins/eva/summary.css: .ignore
-src/frama-c/plugins/eva/valueinfos.tsx: CEA_LGPL
-src/frama-c/plugins/eva/valuetable.tsx: CEA_LGPL
src/frama-c/plugins/pivot/api/general/index.ts: CEA_LGPL
src/frama-c/plugins/studia/api/studia/index.ts: CEA_LGPL
src/frama-c/react-pivottable.d.ts: CEA_LGPL
diff --git a/ivette/src/dome/renderer/dome.tsx b/ivette/src/dome/renderer/dome.tsx
index 2b083a73ee982c656767deb4ec20b2d9829b2af2..51eb64b19f4f5f77a58e6cb45c3ecacd0fcfc471 100644
--- a/ivette/src/dome/renderer/dome.tsx
+++ b/ivette/src/dome/renderer/dome.tsx
@@ -582,6 +582,29 @@ export function usePromise<T>(job: Promise<T>) {
return { result, error, loading };
}
+/* Internal type alias */
+type Serialize<A> = (a: A) => string;
+
+/**
+ Hook to add a cache system to a function, allowing to reuse previous results.
+ As the equality used in JS maps does not allow to effectively implement a
+ cache for complex type, a serialization function can be procured.
+ The hook returns the cached version of the function.
+*/
+export function useCache<K, V>(r: (k: K) => V, s?: Serialize<K>): (k: K) => V {
+ const { current: cache } = React.useRef(new Map<string, V>());
+ const serialize = React.useMemo(() => s ? s : (k: K) => `${k}`, [s]);
+ const get = React.useCallback((k: K): V => {
+ const id = serialize(k);
+ if (cache.has(id))
+ return cache.get(id) as V;
+ const v = r(k);
+ cache.set(id, v);
+ return v;
+ }, [ cache, r, serialize ]);
+ return get;
+}
+
// --------------------------------------------------------------------------
// --- Timer Hooks
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/frame/toolbars.tsx b/ivette/src/dome/renderer/frame/toolbars.tsx
index 44f69e6012a22edccb1e207f77f3b0ebfd15977f..51ab7f1a51a34b6623b7188a55f2d270c6132eef 100644
--- a/ivette/src/dome/renderer/frame/toolbars.tsx
+++ b/ivette/src/dome/renderer/frame/toolbars.tsx
@@ -124,6 +124,8 @@ export interface ButtonProps<A> {
selection?: A;
/** Selection callback. Receives the button's value. */
onClick?: (value: A | undefined) => void;
+ /** Button contents */
+ children?: React.ReactNode;
}
/** Toolbar Button. */
@@ -145,6 +147,7 @@ export function Button<A = undefined>(props: ButtonProps<A>) {
>
{props.icon && <SVG id={props.icon} />}
{props.label && <label>{props.label}</label>}
+ {props.children}
</button>
);
}
diff --git a/ivette/src/frama-c/plugins/eva/api/values/index.ts b/ivette/src/frama-c/plugins/eva/api/values/index.ts
index 4f550b91b0a00dd4cabbff1f89bf799c2741af30..c286426c70a761b23db0616b0870188f7456068e 100644
--- a/ivette/src/frama-c/plugins/eva/api/values/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/values/index.ts
@@ -121,7 +121,7 @@ export const getStmtInfo: Server.GetRequest<
const getProbeInfo_internal: Server.GetRequest<
marker,
{ condition: boolean, effects: boolean, rank: number,
- stmt?: Json.key<'#stmt'>, code?: string }
+ stmt?: Json.key<'#stmt'>, code?: string, evaluable: boolean }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getProbeInfo',
@@ -132,6 +132,7 @@ const getProbeInfo_internal: Server.GetRequest<
rank: Json.jFail(Json.jNumber,'Number expected'),
stmt: Json.jKey<'#stmt'>('#stmt'),
code: Json.jString,
+ evaluable: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
signals: [],
};
@@ -139,7 +140,7 @@ const getProbeInfo_internal: Server.GetRequest<
export const getProbeInfo: Server.GetRequest<
marker,
{ condition: boolean, effects: boolean, rank: number,
- stmt?: Json.key<'#stmt'>, code?: string }
+ stmt?: Json.key<'#stmt'>, code?: string, evaluable: boolean }
>= getProbeInfo_internal;
/** Evaluation of an expression or lvalue */
diff --git a/ivette/src/frama-c/plugins/eva/cells.ts b/ivette/src/frama-c/plugins/eva/cells.ts
deleted file mode 100644
index 02e3ef3ffdcd13688398468a33c0eb1947b5dd40..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/cells.ts
+++ /dev/null
@@ -1,236 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-// --------------------------------------------------------------------------
-// --- Cells
-// --------------------------------------------------------------------------
-
-// Frama-C
-import * as Server from 'frama-c/server';
-import * as Ast from 'frama-c/kernel/api/ast';
-import * as Values from 'frama-c/plugins/eva/api/values';
-
-// --------------------------------------------------------------------------
-// --- Cell Utilities
-// --------------------------------------------------------------------------
-
-export type callback = () => void;
-
-export interface ModelCallbacks {
- forceUpdate: callback;
- forceLayout: callback;
-}
-
-export interface Size { cols: number; rows: number }
-
-export const EMPTY: Size = { cols: 0, rows: 0 };
-
-export function sizeof(text?: string): Size {
- if (text === undefined) return EMPTY;
- const lines = text.split('\n');
- return {
- rows: lines.length,
- cols: lines.reduce((w, l) => Math.max(w, l.length), 0),
- };
-}
-
-export function merge(a: Size, b: Size): Size {
- return {
- cols: Math.max(a.cols, b.cols),
- rows: Math.max(a.rows, b.rows),
- };
-}
-
-export function addH(a: Size, b: Size, padding = 0): Size {
- return {
- cols: a.cols + b.cols + padding,
- rows: Math.max(a.rows, b.rows),
- };
-}
-
-export function addV(a: Size, b: Size, padding = 0): Size {
- return {
- cols: Math.max(a.cols, b.cols),
- rows: a.rows + b.rows + padding,
- };
-}
-
-export function addS(s: Size, t: string | undefined): Size {
- return t ? merge(s, sizeof(t)) : s;
-}
-
-export function lt(a: Size, b: Size): boolean {
- return a.rows < b.rows && a.cols < b.cols;
-}
-
-export function leq(a: Size, b: Size): boolean {
- return a.rows <= b.rows && a.cols <= b.cols;
-}
-
-// --------------------------------------------------------------------------
-// --- Data
-// --------------------------------------------------------------------------
-
-export type EvaStatus = 'True' | 'False' | 'Unknown';
-export type EvaAlarm = [EvaStatus, string];
-export type EvaPointedVar = [string, Ast.marker];
-export type Evaluation = Values.evaluation;
-
-const emptyEvaluation: Values.evaluation = {
- value: '',
- alarms: [],
- pointedVars: [],
-};
-
-export interface EvaValues {
- errors?: string;
- vBefore: Evaluation;
- vAfter?: Evaluation;
- vThen?: Evaluation;
- vElse?: Evaluation;
- size: Size;
-}
-
-// --------------------------------------------------------------------------
-// --- Value Cache
-// --------------------------------------------------------------------------
-
-export interface Probe {
- fct: string | undefined;
- marker: Ast.marker;
-}
-
-export class ValueCache {
-
- private readonly state: ModelCallbacks;
- private readonly probes = new Map<Ast.marker, Size>(); // Marker -> max in column
- private readonly stacks = new Map<string, Size>(); // Callstack -> max in row
- private readonly vcache = new Map<string, EvaValues>(); // '<Marker><@Callstack>?' -> value
- private smax = EMPTY; // max cell size
-
- constructor(state: ModelCallbacks) {
- this.state = state;
- }
-
- clear(): void {
- this.smax = EMPTY;
- this.probes.clear();
- this.stacks.clear();
- this.vcache.clear();
- this.state.forceLayout();
- }
-
- // --- Cached Measures
-
- getMaxSize(): Size { return this.smax; }
-
- getProbeSize(target: Ast.marker): Size {
- return this.probes.get(target) ?? EMPTY;
- }
-
- private static stackKey(fct: string, callstack: Values.callstack): string {
- return `${fct}::${callstack}`;
- }
-
- getStackSize(fct: string, callstack: Values.callstack): Size {
- const key = ValueCache.stackKey(fct, callstack);
- return this.stacks.get(key) ?? EMPTY;
- }
-
- // --- Cached Values & Request Update
-
- getValues(
- { fct, marker }: Probe,
- callstack: Values.callstack | undefined,
- ): EvaValues {
- const key = callstack !== undefined ? `${marker}@${callstack}` : marker;
- const cache = this.vcache;
- const cached = cache.get(key);
- if (cached) return cached;
- const newValue: EvaValues = { vBefore: emptyEvaluation, size: EMPTY };
- if (callstack !== undefined && fct === undefined)
- return newValue;
- // callstack !== undefined ==> fct !== undefined)
- cache.set(key, newValue);
- Server
- .send(Values.getValues, { target: marker, callstack })
- .then((r) => {
- newValue.errors = undefined;
- if (r.vBefore) newValue.vBefore = r.vBefore;
- newValue.vAfter = r.vAfter;
- newValue.vThen = r.vThen;
- newValue.vElse = r.vElse;
- if (this.updateLayout(marker, fct, callstack, newValue))
- this.state.forceLayout();
- else
- this.state.forceUpdate();
- })
- .catch((err) => {
- newValue.errors = `$Error: ${err}`;
- this.state.forceUpdate();
- });
- return newValue;
- }
-
- // --- Updating Measures
-
- private updateLayout(
- target: Ast.marker,
- fct: string | undefined,
- callstack: Values.callstack | undefined,
- v: EvaValues,
- ): boolean {
- // measuring cell
- let s = sizeof(v.vBefore.value);
- s = addS(s, v.vAfter?.value);
- s = addS(s, v.vThen?.value);
- s = addS(s, v.vElse?.value);
- v.size = s;
- // max cell size
- const { smax } = this;
- let small = leq(s, smax);
- if (!small) this.smax = merge(s, smax);
- // max size for probe column
- const ps = this.getProbeSize(target);
- if (!leq(s, ps)) {
- this.probes.set(target, merge(ps, s));
- small = false;
- }
- // max size for stack row
- if (callstack !== undefined) {
- if (fct === undefined) small = false;
- else {
- const key = ValueCache.stackKey(fct, callstack);
- const cs = this.stacks.get(key) ?? EMPTY;
- if (!leq(s, cs)) {
- this.stacks.set(key, merge(cs, s));
- small = false;
- }
- }
- }
- // request new layout if not small enough
- return !small;
- }
-
-}
-
-// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/diffed.tsx b/ivette/src/frama-c/plugins/eva/diffed.tsx
deleted file mode 100644
index 5859784ad91d73f565d7fa09b46ac37dfd224170..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/diffed.tsx
+++ /dev/null
@@ -1,182 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-// --------------------------------------------------------------------------
-// --- Diff Text Rendering
-// --------------------------------------------------------------------------
-
-import React from 'react';
-import { Change, diffChars } from 'diff';
-
-const MODIFIED = 'eva-diff eva-diff-modified';
-const REMOVED = 'eva-diff eva-diff-removed';
-const ADDED = 'eva-diff eva-diff-added';
-const SHADOW = 'eva-diff eva-diff-shadow';
-
-export class DiffBuffer {
-
- private added = false;
- private removed = false;
- private value = '';
- private scratch = '';
- private contents: React.ReactNode[] = [];
-
- constructor() {
- this.push = this.push.bind(this);
- }
-
- clear(): void {
- this.added = false;
- this.removed = false;
- this.value = '';
- this.scratch = '';
- this.contents = [];
- }
-
- push(c: Change): void {
- if (!c.added && !c.removed) {
- this.flush();
- this.value += c.value;
- this.flush();
- } else {
- if (c.added) this.added = true;
- if (c.removed) {
- this.removed = true;
- this.value += c.value;
- }
- }
- }
-
- private flush(): void {
- const { value, added, removed } = this;
- if (added && removed) {
- if (value) {
- this.scratch += '\0'.repeat(value.length);
- this.contents.push(
- <span className={MODIFIED} title="Modified">{value}</span>,
- );
- }
- } else if (removed) {
- if (value) {
- this.contents.push(
- <span className={REMOVED} title="Removed">{value}</span>,
- );
- }
- } else if (added) {
- this.contents.push(
- <span className={ADDED}><span className={SHADOW} /></span>,
- );
- } else if (value) {
- this.scratch += value;
- this.contents.push(value);
- }
- this.value = '';
- this.added = false;
- this.removed = false;
- }
-
- getContents(): React.ReactNode {
- this.flush();
- return React.Children.toArray(this.contents);
- }
-
- getScratch(): string {
- this.flush();
- return this.scratch;
- }
-
-}
-
-/* --------------------------------------------------------------------------*/
-/* --- Diff2 Component ---*/
-/* --------------------------------------------------------------------------*/
-
-export interface Diff2Props {
- text: string;
- diff: string;
-}
-
-export function Diff2(props: Diff2Props): JSX.Element {
- const { text, diff } = props;
- const contents = React.useMemo<React.ReactNode>(() => {
- if (text === diff) return text;
- const buffer = new DiffBuffer();
- const chunks = diffChars(text, diff);
- chunks.forEach(buffer.push);
- return buffer.getContents();
- }, [text, diff]);
- return <>{contents}</>;
-}
-
-/* --------------------------------------------------------------------------*/
-/* --- Diff3 Component ---*/
-/* --------------------------------------------------------------------------*/
-
-export interface Diff3Props {
- text: string;
- diffA: string;
- diffB: string;
-}
-
-export function Diff3(props: Diff3Props): JSX.Element {
- const { text, diffA, diffB } = props;
- const contents = React.useMemo<React.ReactNode>(() => {
- if (text === diffA && text === diffB) return text;
- const buffer = new DiffBuffer();
- diffChars(diffA, diffB).forEach(buffer.push);
- const scratch = buffer.getScratch();
- buffer.clear();
- diffChars(text, scratch).forEach(buffer.push);
- return buffer.getContents();
- }, [text, diffA, diffB]);
- return <>{contents}</>;
-}
-
-/* --------------------------------------------------------------------------*/
-/* --- Diff Component ---*/
-/* --------------------------------------------------------------------------*/
-
-export interface DiffProps {
- text?: string;
- diff?: string;
- diff2?: string;
-}
-
-
-export function Diff(props: DiffProps): JSX.Element | null {
- const { text, diff, diff2 } = props;
- if (text === undefined)
- return null;
- if (diff !== undefined && diff2 !== undefined)
- return <Diff3 text={text} diffA={diff} diffB={diff2} />;
- if (diff !== undefined) {
- if (diff === text) return <>{text}</>;
- return <Diff2 text={text} diff={diff} />;
- }
- if (diff2 !== undefined) {
- if (diff2 === text) return <>{text}</>;
- return <Diff2 text={text} diff={diff2} />;
- }
- return <>{text}</>;
-}
-
-// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 26595d2539b505e4c4d894dd61c780abbcabd0f5..2df245b2abe7bf7506b891b4be2c375a894f0e8a 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -24,84 +24,16 @@
// --- Eva Values
// --------------------------------------------------------------------------
-// React & Dome
-import React from 'react';
-import * as Dome from 'dome';
import * as Ivette from 'ivette';
-import * as Server from 'frama-c/server';
-import { GlobalState, useGlobalState } from 'dome/data/states';
-import { Vfill } from 'dome/layout/boxes';
-import { IconButton } from 'dome/controls/buttons';
-import { AutoSizer } from 'react-virtualized';
-import { Model } from './model';
-
-// Locals
-import { ProbeInfos } from './probeinfos';
-import { Dimension, ValuesPanel } from './valuetable';
-import { AlarmsInfos, StackInfos } from './valueinfos';
+import { } from 'frama-c/plugins/eva/valuetable';
import { } from './Summary';
import { } from './Coverage';
import './style.css';
-// --------------------------------------------------------------------------
-// --- Values Component
-// --------------------------------------------------------------------------
-
-const globalModelState = new GlobalState(new Model());
-
-function ValuesComponent(): JSX.Element {
- const [model] = useGlobalState(globalModelState);
- model.mount();
- Dome.useUpdate(model.changed, model.laidout);
- Server.onShutdown(() => model.unmount());
- const [zoom, setZoom] = Dome.useNumberSettings('eva-zoom-factor', 0);
- return (
- <>
- <Ivette.TitleBar>
- <IconButton
- enabled={zoom > 0}
- icon="ZOOM.OUT"
- onClick={() => setZoom(zoom - 1)}
- />
- <IconButton
- enabled={zoom < 20}
- icon="ZOOM.IN"
- onClick={() => setZoom(zoom + 1)}
- />
- </Ivette.TitleBar>
- <Vfill>
- <ProbeInfos model={model} />
- <Vfill>
- <AutoSizer>
- {(dim: Dimension) => (
- <ValuesPanel
- zoom={zoom}
- model={model}
- {...dim}
- />
- )}
- </AutoSizer>
- </Vfill>
- <AlarmsInfos model={model} />
- <StackInfos model={model} />
- </Vfill>
- </>
- );
-}
-
// --------------------------------------------------------------------------
// --- Export Component
// --------------------------------------------------------------------------
-Ivette.registerComponent({
- id: 'frama-c.plugins.values',
- group: 'frama-c.plugins',
- rank: 1,
- label: 'Eva Values',
- title: 'Values inferred by the Eva analysis',
- children: <ValuesComponent />,
-});
-
Ivette.registerView({
id: 'summary',
rank: 1,
diff --git a/ivette/src/frama-c/plugins/eva/layout.ts b/ivette/src/frama-c/plugins/eva/layout.ts
deleted file mode 100644
index b8e4c1e27ebe807313b4f41b88f06e4e9e15f094..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/layout.ts
+++ /dev/null
@@ -1,237 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-/* --------------------------------------------------------------------------*/
-/* --- Layout ---*/
-/* --------------------------------------------------------------------------*/
-
-import { callstack } from 'frama-c/plugins/eva/api/values';
-import { Probe } from './probes';
-import { StacksCache } from './stacks';
-import { Size, EMPTY, leq, addH, ValueCache } from './cells';
-
-export interface LayoutProps {
- zoom?: number;
- margin: number;
-}
-
-export type RowKind = 'section' | 'probes' | 'values' | 'callstack';
-
-export interface Row {
- key: string;
- fct: string;
- kind: RowKind;
- probes: Probe[];
- headstack?: string;
- stackIndex?: number;
- stackCount?: number;
- callstack?: callstack;
- hlines: number;
-}
-
-/* --------------------------------------------------------------------------*/
-/* --- Layout Enfine ---*/
-/* --------------------------------------------------------------------------*/
-
-const HEAD_PADDING = 4; // Left margin
-const CELL_PADDING = 4; // Inter cell padding
-const TEXT_PADDING = 2; // Intra cell padding
-const HCROP = 18;
-const VCROP = 1;
-
-export class LayoutEngine {
-
- // --- Setup
-
- private readonly folded: (fct: string) => boolean;
- private readonly values: ValueCache;
- private readonly stacks: StacksCache;
- private readonly hcrop: number;
- private readonly vcrop: number;
- private readonly margin: number;
-
- constructor(
- props: undefined | LayoutProps,
- values: ValueCache,
- stacks: StacksCache,
- folded: (fct: string) => boolean,
- ) {
- this.values = values;
- this.stacks = stacks;
- this.folded = folded;
- const zoom = Math.max(0, props?.zoom ?? 0);
- this.vcrop = VCROP + 3 * zoom;
- this.hcrop = HCROP + zoom;
- this.margin = (props?.margin ?? 80) - HEAD_PADDING;
- this.push = this.push.bind(this);
- }
-
- // --- Probe Buffer
- private byFct?: string; // current function
- private byStk = new Map<string, boolean>(); // callstack probes
- private skip?: boolean; // skip current function
- private rowSize: Size = EMPTY;
- private buffer: Probe[] = [];
- private rows: Row[] = [];
- private chained?: Probe;
-
- crop(zoomed: boolean, s: Size): Size {
- const s$cols = s.cols + TEXT_PADDING;
- const cols = zoomed ? s$cols : Math.min(s$cols, this.hcrop);
- const rows = zoomed ? s.rows : Math.min(s.rows, this.vcrop);
- return {
- cols: Math.max(HCROP, cols),
- rows: Math.max(VCROP, rows),
- };
- }
-
- layout(ps: Probe[], byCallstacks: Map<string, boolean>): Row[] {
- this.chained = undefined;
- this.byStk = byCallstacks;
- ps.sort(LayoutEngine.order).forEach(this.push);
- return this.flush();
- }
-
- private static order(p: Probe, q: Probe): number {
- const fp = p.fct;
- const fq = q.fct;
- if (fp === fq) {
- const rp = p.rank ?? 0;
- const rq = q.rank ?? 0;
- if (rp < rq) return (-1);
- if (rp > rq) return (+1);
- if (p.marker < q.marker) return (-1);
- if (p.marker > q.marker) return (+1);
- }
- return 0;
- }
-
- private push(p: Probe): void {
- // --- sectionning
- const { fct } = p;
- if (fct !== this.byFct) {
- this.flush();
- this.rows.push({
- key: `S:${fct}`,
- kind: 'section',
- fct,
- probes: [],
- hlines: 1,
- });
- this.byFct = fct;
- this.csRowsCounter = 1;
- this.skip = this.folded(fct);
- }
- if (this.skip) return;
- // --- chaining
- const q = this.chained;
- if (q) q.next = p;
- p.prev = q;
- this.chained = p;
- // --- sizing
- const probeSize = this.values.getProbeSize(p.marker);
- const s = this.crop(p.zoomed, probeSize);
- p.zoomable = p.zoomed || !leq(probeSize, s);
- p.minCols = s.cols;
- p.maxCols = Math.max(p.minCols, probeSize.cols);
- // --- queueing
- if (s.cols + this.rowSize.cols > this.margin)
- this.flush();
- this.rowSize = addH(this.rowSize, s);
- this.rowSize.cols += CELL_PADDING;
- this.buffer.push(p);
- }
-
- // --- Flush Rows
-
- private csRowsCounter = 1;
-
- private flush(): Row[] {
- const ps = this.buffer;
- const rs = this.rows;
- const fct = this.byFct;
- if (fct && ps.length > 0) {
- const stk = this.byStk.get(fct);
- const hlines = this.rowSize.rows;
- if (stk) {
- // --- by callstacks
- const markers = ps.map((p) => p.marker);
- const stacks = this.stacks.getStacks(...markers);
- const summary = fct ? this.stacks.getSummary(fct) : false;
- const callstacks = stacks.length;
- const { csRowsCounter } = this;
- rs.push({
- key: `P:${fct}:${csRowsCounter}`,
- kind: 'probes',
- probes: ps,
- stackCount: callstacks,
- fct,
- hlines: 1,
- });
- if (summary && callstacks > 1) rs.push({
- key: `V:${fct}:${csRowsCounter}`,
- kind: 'values',
- probes: ps,
- stackIndex: -1,
- stackCount: stacks.length,
- fct,
- hlines,
- });
- stacks.forEach((cs, k) => {
- rs.push({
- key: `C:${fct}:${csRowsCounter}:${cs}`,
- kind: 'callstack',
- probes: ps,
- stackIndex: k,
- stackCount: callstacks,
- callstack: cs,
- fct,
- hlines,
- });
- });
- } else {
- // --- not by callstacks
- const n = rs.length;
- rs.push({
- key: `P#${n}`,
- kind: 'probes',
- probes: ps,
- fct,
- hlines: 1,
- }, {
- key: `V#${n}`,
- kind: 'values',
- probes: ps,
- fct,
- hlines,
- });
- }
- }
- this.buffer = [];
- this.rowSize = EMPTY;
- this.csRowsCounter++;
- return rs;
- }
-
-}
-
-/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/plugins/eva/model.ts b/ivette/src/frama-c/plugins/eva/model.ts
deleted file mode 100644
index 01e3d14334b3f900c850d943f1c2815a7ae76fca..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/model.ts
+++ /dev/null
@@ -1,316 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-/* eslint-disable @typescript-eslint/explicit-function-return-type */
-
-// --------------------------------------------------------------------------
-// --- Eva Values
-// --------------------------------------------------------------------------
-
-// External Libs
-import { throttle } from 'lodash';
-import equal from 'react-fast-compare';
-import * as Dome from 'dome';
-
-import * as Server from 'frama-c/server';
-import * as States from 'frama-c/states';
-import * as Values from 'frama-c/plugins/eva/api/values';
-
-// Model
-import { Probe } from './probes';
-import { StacksCache, Callsite } from './stacks';
-import { ModelCallbacks, ValueCache } from './cells';
-import { LayoutProps, LayoutEngine, Row } from './layout';
-
-export interface ModelLayout extends LayoutProps {
- location?: States.Location;
-}
-
-export type EvalStmt = 'Before' | 'After';
-export type EvalCond = 'Cond' | 'Then' | 'Else';
-
-/* --------------------------------------------------------------------------*/
-/* --- EVA Values Model ---*/
-/* --------------------------------------------------------------------------*/
-
-export class Model implements ModelCallbacks {
-
- constructor() {
- this.forceUpdate = this.forceUpdate.bind(this);
- this.forceLayout = this.forceLayout.bind(this);
- this.forceReload = this.forceReload.bind(this);
- this.computeLayout = this.computeLayout.bind(this);
- this.setLayout = throttle(this.setLayout.bind(this), 300);
- this.metaSelection = this.metaSelection.bind(this);
- this.getRowKey = this.getRowKey.bind(this);
- this.getRowCount = this.getRowCount.bind(this);
- this.getRowLines = this.getRowLines.bind(this);
- this.isFolded = this.isFolded.bind(this);
- }
-
- // --- Probes
-
- private vstmt: EvalStmt = 'Before';
- private vcond: EvalCond = 'Cond';
- private selected?: Probe;
- private focused?: Probe;
- private callstack?: Values.callstack;
- private remanent?: Probe; // last transient
- private probes = new Map<string, Probe>();
- private folded = new Map<string, boolean>(); // folded functions
- private byCallstacks = new Map<string, boolean>();
-
- getFocused() { return this.focused; }
- isFocused(p: Probe | undefined) { return this.focused === p; }
-
- getProbe(location: States.Location | undefined): Probe | undefined {
- if (!location) return undefined;
- const { fct, marker } = location;
- if (fct && marker) {
- let p = this.probes.get(marker);
- if (!p) {
- p = new Probe(this, fct, marker);
- this.probes.set(marker, p);
- p.requestProbeInfo();
- }
- return p;
- }
- return undefined;
- }
-
- addProbe(location: States.Location) {
- const { fct, marker } = location;
- if (fct && marker) {
- const probe = new Probe(this, fct, marker);
- probe.setPersistent();
- probe.requestProbeInfo();
- this.probes.set(marker, probe);
- this.forceLayout();
- }
- }
-
- removeProbe(probe: Probe) {
- probe.setTransient();
- if (this.selected === probe)
- this.clearSelection();
- }
-
- getStacks(p: Probe | undefined): Values.callstack[] {
- return p ? this.stacks.getStacks(p.marker) : [];
- }
-
- getVstmt(): EvalStmt { return this.vstmt; }
- getVcond(): EvalCond { return this.vcond; }
- setVstmt(s: EvalStmt) { this.vstmt = s; this.forceUpdate(); }
- setVcond(s: EvalCond) { this.vcond = s; this.forceUpdate(); }
-
- isFolded(fct: string): boolean {
- return (this.focused?.fct !== fct) && (this.folded.get(fct) ?? false);
- }
-
- isFoldable(fct: string): boolean {
- return this.focused?.fct !== fct;
- }
-
- setFolded(fct: string, folded: boolean) {
- this.folded.set(fct, folded);
- this.forceLayout();
- }
-
- isByCallstacks(fct: string): boolean {
- return this.byCallstacks.get(fct) ?? false;
- }
-
- setByCallstacks(fct: string, b: boolean) {
- this.byCallstacks.set(fct, b);
- this.forceLayout();
- }
-
- clearFunction(fct: string) {
- let selected = false;
- this.probes.forEach((p) => {
- if (p.fct === fct) {
- p.setTransient();
- if (this.selected === p)
- selected = true;
- }
- });
- if (selected)
- this.clearSelection();
- }
-
- // --- Caches
-
- readonly stacks = new StacksCache(this);
- readonly values = new ValueCache(this);
-
- // --- Rows
-
- private lock = false;
- private layout: ModelLayout = { margin: 80 };
- private rows: Row[] = [];
-
- getRow(index: number): Row | undefined {
- return this.rows[index];
- }
-
- getRowCount() {
- return this.rows.length;
- }
-
- getRowKey(index: number): string {
- const row = this.rows[index];
- return row ? row.key : `#${index}`;
- }
-
- getRowLines(index: number): number {
- const row = this.rows[index];
- return row ? row.hlines : 0;
- }
-
- setSelectedRow(row: Row) {
- const cs = row.callstack;
- if (cs !== this.callstack) {
- this.callstack = cs;
- this.forceUpdate();
- }
- }
-
- isSelectedRow(row: Row): boolean {
- if (!this.byCallstacks) return false;
- const cs = this.callstack;
- return cs !== undefined && cs === row.callstack;
- }
-
- isAlignedRow(row: Row): boolean {
- const cs = this.callstack;
- const cr = row.callstack;
- return cs !== undefined && cr !== undefined && this.stacks.aligned(cs, cr);
- }
-
- getCallstack(): Values.callstack | undefined {
- return this.callstack;
- }
-
- getCalls(): Callsite[] {
- const c = this.callstack;
- return c === undefined ? [] : this.stacks.getCalls(c);
- }
-
- // --- Throttled
- setLayout(ly: ModelLayout) {
- if (!equal(this.layout, ly)) {
- this.layout = ly;
- this.selected = this.getProbe(ly.location);
- this.forceLayout();
- }
- }
-
- metaSelection(location: States.Location) {
- const p = this.getProbe(location);
- if (p && p.transient)
- p.setPersistent();
- }
-
- clearSelection() {
- this.focused = undefined;
- this.selected = undefined;
- this.remanent = undefined;
- this.forceLayout();
- }
-
- // --- Recompute Layout
-
- private computeLayout() {
- if (this.lock) return;
- this.lock = true;
- const s = this.selected;
- if (!s) {
- this.focused = undefined;
- this.remanent = undefined;
- } else if (!s.loading) {
- this.focused = s;
- if (s.code && s.transient) {
- this.remanent = s;
- } else {
- this.remanent = undefined;
- }
- }
- const toLayout: Probe[] = [];
- this.probes.forEach((p) => {
- if (p.code && (!p.transient || p === this.remanent)) {
- toLayout.push(p);
- }
- });
- const engine = new LayoutEngine(
- this.layout,
- this.values,
- this.stacks,
- this.isFolded,
- );
- this.rows = engine.layout(toLayout, this.byCallstacks);
- this.laidout.emit();
- this.lock = false;
- }
-
- // --- Force Reload (empty caches)
- forceReload() {
- this.focused = undefined;
- this.remanent = undefined;
- this.selected = undefined;
- this.callstack = undefined;
- this.probes.clear();
- this.stacks.clear();
- this.values.clear();
- this.forceLayout();
- this.forceUpdate();
- }
-
- // --- Events
- readonly changed = new Dome.Event('eva-changed');
- readonly laidout = new Dome.Event('eva-laidout');
-
- // --- Force Layout
- forceLayout() {
- setImmediate(this.computeLayout);
- }
-
- // --- Foce Update
- forceUpdate() { this.changed.emit(); }
-
- // --- Global Signals
-
- mount() {
- States.MetaSelection.on(this.metaSelection);
- Server.onSignal(Values.changed, this.forceReload);
- }
-
- unmount() {
- States.MetaSelection.off(this.metaSelection);
- Server.offSignal(Values.changed, this.forceReload);
- }
-
-}
-
-export interface ModelProp {
- model: Model;
-}
diff --git a/ivette/src/frama-c/plugins/eva/probeinfos.tsx b/ivette/src/frama-c/plugins/eva/probeinfos.tsx
deleted file mode 100644
index 9baa4c9acdb5fc6ee9a3291fbee5eacd8d73f385..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/probeinfos.tsx
+++ /dev/null
@@ -1,172 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-// --------------------------------------------------------------------------
-// --- Eva Values
-// --------------------------------------------------------------------------
-
-// React & Dome
-import React from 'react';
-import { Hpack, Filler } from 'dome/layout/boxes';
-import { Code } from 'dome/controls/labels';
-import { IconButton } from 'dome/controls/buttons';
-import { ButtonGroup, Button } from 'dome/frame/toolbars';
-
-// Frama-C
-import * as States from 'frama-c/states';
-
-// Locals
-import { SizedArea } from './sized';
-import { sizeof } from './cells';
-import { ModelProp } from './model';
-import { Stmt } from './valueinfos';
-
-// --------------------------------------------------------------------------
-// --- Probe Editor
-// --------------------------------------------------------------------------
-
-function ProbeEditor(props: ModelProp): JSX.Element | null {
- const { model } = props;
- const probe = model.getFocused();
- if (!probe || !probe.code) return null;
- const { code } = probe;
- const { stmt, marker } = probe;
- const { cols, rows } = sizeof(code);
- const { transient } = probe;
- const { zoomed } = probe;
- const { zoomable } = probe;
- return (
- <>
- <div className="eva-probeinfo-code">
- <SizedArea cols={cols} rows={rows}>{code}</SizedArea>
- </div>
- <Code><Stmt stmt={stmt} marker={marker} /></Code>
- <IconButton
- icon="SEARCH"
- className="eva-probeinfo-button"
- display={zoomable}
- selected={zoomed}
- title="Resize cells to fit values"
- onClick={() => { if (probe) probe.setZoomed(!zoomed); }}
- />
- <IconButton
- icon="PIN"
- className="eva-probeinfo-button"
- selected={!transient}
- title={transient ? 'Make the probe persistent' : 'Release the probe'}
- onClick={() => {
- if (probe) {
- if (transient) probe.setPersistent();
- else probe.setTransient();
- }
- }}
- />
- <IconButton
- icon="CIRC.CLOSE"
- className="eva-probeinfo-button"
- display={!transient}
- title="Discard the probe"
- onClick={() => {
- if (probe) {
- probe.setTransient();
- const p = probe.next ?? probe.prev;
- if (p) setImmediate(() => {
- States.setSelection({ fct: p.fct, marker: p.marker });
- });
- else model.clearSelection();
- }
- }}
- />
- </>
- );
-}
-
-// --------------------------------------------------------------------------
-// --- Probe Panel
-// --------------------------------------------------------------------------
-
-export function ProbeInfos(props: ModelProp): JSX.Element {
- const { model } = props;
- const probe = model.getFocused();
- const fct = probe?.fct;
- const byCS = fct ? model.isByCallstacks(fct) : false;
- const effects = probe ? probe.effects : false;
- const condition = probe ? probe.condition : false;
- const summary = fct ? model.stacks.getSummary(fct) : false;
- const vcond = model.getVcond();
- const vstmt = model.getVstmt();
- return (
- <Hpack className="eva-probeinfo">
- <ProbeEditor model={model} />
- <Filler />
- <ButtonGroup
- enabled={!!probe}
- className="eva-probeinfo-state"
- >
- <Button
- label={'\u2211'}
- title="Show Callstacks Summary"
- selected={summary}
- visible={byCS}
- onClick={() => { if (fct) model.stacks.setSummary(fct, !summary); }}
- />
- <Button
- visible={condition}
- label="C"
- selected={vcond === 'Cond'}
- title="Show values in all conditions"
- onClick={() => model.setVcond('Cond')}
- />
- <Button
- visible={condition || vcond === 'Then'}
- selected={vcond === 'Then'}
- enabled={condition}
- label="T"
- value="Then"
- title="Show reduced values when condition holds (Then)"
- onClick={() => model.setVcond('Then')}
- />
- <Button
- visible={condition || vcond === 'Else'}
- selected={vcond === 'Else'}
- enabled={condition}
- label="E"
- value="Else"
- title="Show reduced values when condition does not hold (Else)"
- onClick={() => model.setVcond('Else')}
- />
- <Button
- visible={condition || effects}
- selected={vstmt === 'After'}
- label="A"
- value="After"
- title="Show values after/before statement effects"
- onClick={() => {
- model.setVstmt(vstmt === 'After' ? 'Before' : 'After');
- }}
- />
- </ButtonGroup>
- </Hpack>
- );
-}
-
-// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/probes.ts b/ivette/src/frama-c/plugins/eva/probes.ts
deleted file mode 100644
index e9bdb0da9ca7d49f0887b03e57d475913505cfe2..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/probes.ts
+++ /dev/null
@@ -1,114 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-/* --------------------------------------------------------------------------*/
-/* --- Probes ---*/
-/* --------------------------------------------------------------------------*/
-
-// Frama-C
-import * as Server from 'frama-c/server';
-import * as Values from 'frama-c/plugins/eva/api/values';
-import * as Ast from 'frama-c/kernel/api/ast';
-
-// Model
-import { ModelCallbacks } from './cells';
-
-/* --------------------------------------------------------------------------*/
-/* --- Probe State ---*/
-/* --------------------------------------------------------------------------*/
-
-const LabelSize = 12;
-
-export class Probe {
-
- // properties
- readonly fct: string;
- readonly marker: Ast.marker;
- readonly model: ModelCallbacks;
- next?: Probe;
- prev?: Probe;
- transient = true;
- loading = true;
- code?: string;
- stmt?: Ast.marker;
- rank?: number;
- minCols: number = LabelSize;
- maxCols: number = LabelSize;
- zoomed = true;
- zoomable = false;
- effects = false;
- condition = false;
-
- constructor(state: ModelCallbacks, fct: string, marker: Ast.marker) {
- this.fct = fct;
- this.marker = marker;
- this.model = state;
- this.requestProbeInfo = this.requestProbeInfo.bind(this);
- }
-
- requestProbeInfo(): void {
- this.loading = true;
- Server
- .send(Values.getProbeInfo, this.marker)
- .then(({ code, stmt, rank, effects, condition }) => {
- this.code = code;
- this.stmt = stmt;
- this.rank = rank;
- this.effects = effects;
- this.condition = condition;
- this.loading = false;
- })
- .catch(() => {
- this.code = '(error)';
- this.stmt = undefined;
- this.rank = undefined;
- this.effects = false;
- this.condition = false;
- this.loading = false;
- })
- .finally(this.model.forceLayout);
- }
-
- // --------------------------------------------------------------------------
- // --- Internal State
- // --------------------------------------------------------------------------
-
- setPersistent(): void { this.updateTransient(false); }
- setTransient(): void { this.updateTransient(true); }
-
- private updateTransient(tr: boolean): void {
- if (this.transient !== tr) {
- this.transient = tr;
- this.model.forceLayout();
- }
- }
-
- setZoomed(zoomed: boolean): void {
- if (zoomed !== this.zoomed) {
- this.zoomed = zoomed;
- this.model.forceLayout();
- }
- }
-
-}
-
-/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/plugins/eva/sized.tsx b/ivette/src/frama-c/plugins/eva/sized.tsx
deleted file mode 100644
index 95496201039ff396d631d14007332faca894ac48..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/sized.tsx
+++ /dev/null
@@ -1,141 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-// --------------------------------------------------------------------------
-// --- Sized Cell
-// --------------------------------------------------------------------------
-
-import React from 'react';
-
-// --------------------------------------------------------------------------
-// --- Measurer
-// --------------------------------------------------------------------------
-
-export class Streamer {
- private readonly v0: number;
- private readonly vs: number[] = [];
- private v?: number;
- constructor(v0: number) {
- this.v0 = v0;
- }
-
- push(v: number): void {
- const { vs } = this;
- vs.push(Math.round(v));
- if (vs.length > 200) vs.shift();
- }
-
- mean(): number {
- if (this.v === undefined) {
- const { vs } = this;
- const n = vs.length;
- if (n > 0) {
- const m = vs.reduce((s, v) => s + v, 0) / n;
- this.v = Math.round(m + 0.5);
- } else {
- this.v = this.v0;
- }
- }
- return this.v;
- }
-
-}
-
-export class FontSizer {
- a = 0;
- b = 0;
- k: Streamer;
- p: Streamer;
-
- constructor(k: number, p: number) {
- this.k = new Streamer(k);
- this.p = new Streamer(p);
- }
-
- push(x: number, y: number): void {
- const a0 = this.a;
- const b0 = this.b;
- if (x !== a0 && a0 !== 0) {
- const k = (y - b0) / (x - a0);
- const p = y - k * x;
- this.k.push(k);
- this.p.push(p);
- }
- this.a = x;
- this.b = y;
- }
-
- capacity(y: number): number {
- const k = this.k.mean();
- const p = this.p.mean();
- return Math.round(0.5 + (y - p) / k);
- }
-
- dimension(n: number): number {
- const k = this.k.mean();
- const p = this.p.mean();
- return p + n * k;
- }
-
- dump(x: string): string {
- const k = this.k.mean();
- const p = this.p.mean();
- return `${k}.${x}+${p}`;
- }
-
-}
-
-/* --------------------------------------------------------------------------*/
-/* --- Sizing Component ---*/
-/* --------------------------------------------------------------------------*/
-
-export const WSIZER = new FontSizer(7, 6);
-export const HSIZER = new FontSizer(15, 6);
-
-export interface SizedAreaProps {
- cols: number;
- rows: number;
- children?: React.ReactNode;
-}
-
-export function SizedArea(props: SizedAreaProps): JSX.Element {
- const { rows, cols, children } = props;
- const refSizer = React.useCallback(
- (ref: null | HTMLDivElement) => {
- if (ref) {
- const r = ref.getBoundingClientRect();
- WSIZER.push(cols, r.width);
- HSIZER.push(rows, r.height);
- }
- }, [rows, cols],
- );
- return (
- <div
- ref={refSizer}
- className="eva-sized-area dome-text-cell"
- >
- {children}
- </div>
- );
-}
-
-/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/plugins/eva/stacks.ts b/ivette/src/frama-c/plugins/eva/stacks.ts
deleted file mode 100644
index 447890eef2d65a65d95e4b89afc1dc25441241d4..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/stacks.ts
+++ /dev/null
@@ -1,141 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-// --------------------------------------------------------------------------
-// --- CallStacks
-// --------------------------------------------------------------------------
-
-import * as Server from 'frama-c/server';
-import * as Ast from 'frama-c/kernel/api/ast';
-import * as Values from 'frama-c/plugins/eva/api/values';
-
-import { ModelCallbacks } from './cells';
-
-// --------------------------------------------------------------------------
-// --- Callstack infos
-// --------------------------------------------------------------------------
-
-export type callstacks = Values.callstack[];
-export interface Callsite {
- callee: string;
- caller?: string;
- stmt?: Ast.marker;
-}
-
-function equalSite(a: Callsite, b: Callsite): boolean {
- return a.stmt === b.stmt && a.callee === b.callee;
-}
-
-// --------------------------------------------------------------------------
-// --- CallStacks Cache
-// --------------------------------------------------------------------------
-
-export class StacksCache {
-
- private readonly model: ModelCallbacks;
- private readonly stacks = new Map<string, callstacks>();
- private readonly summary = new Map<string, boolean>();
- private readonly calls = new Map<Values.callstack, Callsite[]>();
-
- // --------------------------------------------------------------------------
- // --- LifeCycle
- // --------------------------------------------------------------------------
-
- constructor(state: ModelCallbacks) {
- this.model = state;
- }
-
- clear(): void {
- this.stacks.clear();
- this.calls.clear();
- }
-
- // --------------------------------------------------------------------------
- // --- Getters
- // --------------------------------------------------------------------------
-
- getSummary(fct: string): boolean {
- return this.summary.get(fct) ?? true;
- }
-
- setSummary(fct: string, s: boolean): void {
- this.summary.set(fct, s);
- this.model.forceLayout();
- }
-
- getStacks(...markers: Ast.marker[]): callstacks {
- if (markers.length === 0) return [];
- const key = markers.join('$');
- const cs = this.stacks.get(key);
- if (cs !== undefined) return cs;
- this.stacks.set(key, []);
- this.requestStacks(key, markers);
- return [];
- }
-
- getCalls(cs: Values.callstack): Callsite[] {
- const fs = this.calls.get(cs);
- if (fs !== undefined) return fs;
- this.calls.set(cs, []);
- this.requestCalls(cs);
- return [];
- }
-
- aligned(a: Values.callstack, b: Values.callstack): boolean {
- if (a === b) return true;
- const ca = this.getCalls(a);
- const cb = this.getCalls(b);
- let ka = ca.length - 1;
- let kb = cb.length - 1;
- while (ka >= 0 && kb >= 0 && equalSite(ca[ka], cb[kb])) {
- --ka;
- --kb;
- }
- return ka < 0 || kb < 0;
- }
-
- // --------------------------------------------------------------------------
- // --- Fetchers
- // --------------------------------------------------------------------------
-
- private requestStacks(key: string, markers: Ast.marker[]): void {
- Server
- .send(Values.getCallstacks, markers)
- .then((stacks: callstacks) => {
- this.stacks.set(key, stacks);
- this.model.forceLayout();
- this.model.forceUpdate();
- });
- }
-
- private requestCalls(cs: Values.callstack): void {
- Server
- .send(Values.getCallstackInfo, cs)
- .then((calls) => {
- this.calls.set(cs, calls);
- this.model.forceUpdate();
- });
- }
-
-}
-
-// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index 3dd5be0b82191f7e234969da8d661bffaa387a1b..12f78a00a4358725fd5401b9c446e03d9fab7cdd 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -1,82 +1,62 @@
/* -------------------------------------------------------------------------- */
-/* --- Probe Panel --- */
+/* --- Call Stack Info --- */
/* -------------------------------------------------------------------------- */
-.eva-probeinfo {
- min-height: 32px;
- padding-left: 6px;
- padding-top: 2px;
- padding-bottom: 4px;
- width: 100%;
- background: var(--background-profound);
- display: flex;
+:root {
+ --eva-min-width: 90px;
}
-.eva-probeinfo-label {
- flex: 0 1 auto;
- min-width: 22px;
- text-align: left;
+.eva-info {
+ width: 100%;
+ display: flex;
+ flex-wrap: nowrap;
+ align-items: center;
+ background: var(--background-profound);
+ padding: 2px;
}
-.eva-probeinfo-code {
- flex: 0 1 auto;
- height: fit-content;
- background: var(--background-intense);
- min-width: 120px;
- width: auto;
- border: thin solid var(--border);
- padding-left: 6px;
- padding-right: 6px;
- border-radius: 4px;
- overflow: hidden;
+.eva-info-wrap {
+ flex: auto;
+ flex-wrap: wrap;
}
-.eva-probeinfo-stmt {
- flex: 0 0 auto;
- margin-left: 2px;
- margin-right: 0px;
- margin-top: 2px;
+.eva-callsite {
+ flex: 0 0 auto;
+ fill: var(--selected-element);
+ background: var(--background-softer);
+ border-radius: 4px;
+ border: thin solid var(--border);
+ padding-right: 7px;
}
-.eva-probeinfo-button {
- flex: 0 0 auto;
- margin: 1px;
- min-width: 16px;
+.eva-cell-container {
+ display: flex;
+ justify-content: center;
}
-.eva-probeinfo-state {
- margin-top: 2px;
- margin-bottom: 2px;
+.eva-cell-left {
+ flex: 1;
}
-/* -------------------------------------------------------------------------- */
-/* --- Call Satck Info --- */
-/* -------------------------------------------------------------------------- */
-
-.eva-info {
- width: 100%;
- flex-wrap: wrap;
- background: var(--background-profound);
- padding-top: 3px;
- padding-left: 12px;
- padding-bottom: 2px;
+.eva-cell-content {
+ margin-left: 4px;
+ margin-right: 4px;
+ flex: 0 auto;
+ overflow: hidden;
+ display: flex;
+ align-items: baseline;
}
-.eva-callsite {
- flex: 0 0 auto;
- fill: var(--selected-element);
- background: var(--background-softer);
- border-radius: 4px;
- border: thin solid var(--border);
- padding-right: 7px;
-}
-
-.eva-callsite.eva-focused {
- background: var(--warning-button-color);
+.eva-header-text-overflow {
+ overflow: hidden;
+ text-overflow: ellipsis;
}
-.eva-callsite.eva-focused.eva-transient {
- background: var(--code-select);
+.eva-cell-right {
+ display: flex;
+ flex: 1;
+ min-width: max-content;
+ justify-content: flex-end;
}
/* -------------------------------------------------------------------------- */
@@ -84,17 +64,16 @@
/* -------------------------------------------------------------------------- */
.eva-cell-alarms {
- fill: orange;
- position: absolute;
- top: -1px;
- right: 3px;
- z-index: 1;
+ z-index: 1;
+ margin: 0px;
+ padding: 0px;
+ margin-right: 4px;
}
.eva-alarm-info {
- font-size: x-small;
- padding: 0px;
- margin: 1px;
+ font-size: x-small;
+ padding: 0px;
+ margin: 1px;
}
.eva-alarm-none { display: none; }
@@ -103,173 +82,233 @@
.eva-alarm-Unknown { fill: var(--eva-alarms-unknown); }
/* -------------------------------------------------------------------------- */
-/* --- Styling Values --- */
+/* --- Styling Statement display --- */
/* -------------------------------------------------------------------------- */
.eva-stmt {
- color: var(--info-text);
- text-select: none;
-}
-
-.eva-sized-area {
- padding: 3px;
- white-space: pre;
- overflow: hidden;
- text-overflow: ellipsis;
+ color: var(--info-text);
+ font-weight: normal;
}
/* -------------------------------------------------------------------------- */
-/* --- Table Rows --- */
+/* --- Function Section Header --- */
/* -------------------------------------------------------------------------- */
-.eva-row {
- display: flex;
- position: relative;
- flex: 0 1 auto;
- height: 100%;
+.eva-function {
+ padding: 2px;
+ background: var(--background-profound);
+ height: 25px;
+ align-items: center;
+}
+
+.eva-fct-fold {
+ margin-left: 4px;
+ margin-right: 8px;
+ padding: 0px;
+}
+
+.eva-fct-name {
+ font-weight: bold;
}
/* -------------------------------------------------------------------------- */
-/* --- Table Heads --- */
+/* --- Table General CSS --- */
/* -------------------------------------------------------------------------- */
-.eva-function {
- padding-top: 0px;
- background: var(--background-profound);
+.eva-table {
+ border: 0px;
+ border-spacing: 0px;
+}
+
+.eva-table-header-sticky {
+ position: sticky;
+ top: 0;
+ z-index: +1;
}
-.eva-head {
- padding-top: 2px;
- color: var(--info-text);
- text-align: center;
- border-left: thin solid var(--border);
- border-bottom: thin solid var(--border);
+.eva-table tr:nth-child(n + 4) {
+ cursor: pointer;
}
-.eva-probes .eva-head {
- border-top: thin solid var(--border);
+.eva-table tr th {
+ border-right: thin solid var(--border);
+ border-top: thin solid var(--border);
+ border-bottom: thin solid var(--border);
+ height: 22px;
+ min-height: 22px;
+ max-height: 22px;
+ min-width: calc(var(--eva-min-width) + 30px);
+ max-width: calc(var(--eva-min-width) + 30px);
}
-.eva-phantom {
- visibility: hidden;
- height: 0;
+.eva-table tr:nth-child(2n) {
+ background-color: var(--background-alterning-even);
+}
+
+.eva-table tr:nth-child(2n + 1) {
+ background-color: var(--background-alterning-odd);
+}
+
+.eva-table-container {
+ position: relative;
+ overflow: auto;
+ height: 100%;
+ min-height: 66px;
+}
+
+.eva-functions-section {
+ display: grid;
+ overflow: auto;
+ align-content: start;
+}
+
+.eva-nb-callstacks {
+ color: var(--info-text);
+ padding-right: 11px;
}
/* -------------------------------------------------------------------------- */
-/* --- Table Cells --- */
+/* --- Table Headers CSS --- */
/* -------------------------------------------------------------------------- */
-.eva-fct-fold {
- margin-left: 4px;
- margin-right: 8px;
- padding: 0px;
+.eva-header-tracked {
}
-.eva-fct-name {
- padding: 2px;
- font-weight: bold;
+.eva-header-tracked-focused {
}
-.eva-cell {
- flex: 1 1 auto;
- border-right: thin solid var(--border);
- border-bottom: thin solid var(--border);
- overflow: hidden;
- display: flex;
- justify-content: center;
- position: relative;
+.eva-header-just-focused {
+ background: var(--code-select);
}
-.eva-cell .eva-stmt {
- margin-left: 0.2em;
- padding: 2px 0px;
+.eva-header-pinned {
+ background: var(--eva-probes-pinned);
}
-.eva-cell-expression {
- text-align: center;
- text-overflow: ellipsis;
- flex: 0 1 auto;
- display: inline-block;
- overflow: hidden;
+.eva-header-pinned-focused {
+ background: var(--eva-probes-pinned-focused);
}
-.eva-cell:nth-child(2) {
- border-left: thin solid var(--border);
+.eva-header-after-condition {
+ display: flex;
+ justify-content: center;
+ gap: 0.3em;
}
-.eva-probes .eva-cell {
- padding: 2px 4px;
- text-align: center;
- border-top: thin solid var(--border);
+.eva-header-buttons-container {
+ position: absolute;
+ right: 1px;
+ top: 0px;
+ padding-left: 2px;
+ display: flex;
+ z-index: +1;
+ background: inherit;
}
-.eva-cell * {
- user-select: text;
+.eva-header-button {
+ padding: 2px 2px 3px 2px;
+}
+
+.eva-header-text {
+ display: flex;
}
/* -------------------------------------------------------------------------- */
-/* --- Cell Diffs --- */
+/* --- Table Callsite Boxes --- */
/* -------------------------------------------------------------------------- */
-.eva-diff-shadow {
- border: solid transparent 2px;
- position: relative;
- z-index: -1;
+.eva-table-callsite-box {
+ width: 18px;
+ min-width: 18px;
+ background: var(--background);
+ border: 0px;
+ text-align: center;
+ color: var(--info-text);
+ border-left: thin solid var(--border);
+ border-right: thin solid var(--border);
+ border-bottom: thin solid var(--border);
+ padding: 2px;
}
-.eva-diff-added { }
-.eva-diff-removed { text-decoration: strike }
-
-.eva-state-Before .eva-diff { background: var(--eva-state-before); }
-.eva-state-After .eva-diff { background: var(--eva-state-after); }
-.eva-state-Cond .eva-diff { background: var(--eva-state-before); }
-.eva-state-Then .eva-diff { background: var(--eva-state-then); }
-.eva-state-Else .eva-diff { background: var(--eva-state-else); }
+tr:first-of-type > .eva-table-callsite-box {
+ border-top: thin solid var(--border);
+}
/* -------------------------------------------------------------------------- */
-/* --- Table Rows Background --- */
+/* --- Table Values --- */
/* -------------------------------------------------------------------------- */
-/* --- Probes --- */
+.eva-table-values {
+ position: relative;
+ border: 0px;
+ padding: 2px 3px 2px 3px;
+ border-bottom: thin solid var(--border);
+ border-right: thin solid var(--border);
+ min-width: var(--eva-min-width);
+ font-family: Andale Mono, monospace;
+ font-size: 9pt;
+ height: 22px;
+ min-height: 22px;
+ max-height: 22px;
+ white-space: pre;
+}
-.eva-probes .eva-cell {
- background: var(--eva-probes-pinned);
+.eva-table-values-left {
+ text-align: left;
}
-.eva-probes .eva-focused {
- background: var(--eva-probes-pinned-focused);
+.eva-table-values-center {
+ text-align: center;
}
-.eva-probes .eva-transient {
- background: var(--eva-probes-transient);
- align-items: center;
+.eva-table-descrs {
+ background-color: var(--background-sidebar);
+ border-right: thin solid var(--border);
}
-.eva-probes .eva-transient.eva-focused {
- background: var(--eva-probes-transient-focused);
+.eva-table-descr-sticky {
+ position: sticky;
+ top: 22px;
+ z-index: +1;
}
+.eva-table-callsite-box.eva-table-header-sticky {
+ left: 0px;
+ z-index: +2;
+}
-/* --- Values / Callstacks --- */
+.eva-table-value-sticky {
+ position: sticky;
+ left: 0px;
+ z-index: +1;
+}
-.eva-values .eva-cell {
- background: var(--background-alterning-odd);
+.eva-values-position {
+ display: inline-block;
+ width: 0px;
}
-.eva-callstack.eva-row-odd .eva-cell {
- background: var(--background-alterning-odd);
+.eva-table-text {
+ cursor: text;
+ user-select: text;
+ margin-left: 1px;
+ margin-right: 1px;
}
-.eva-callstack.eva-row-even .eva-cell {
- background: var(--background-alterning-even);
+/* -------------------------------------------------------------------------- */
+/* --- Miscellaneous --- */
+/* -------------------------------------------------------------------------- */
+
+.eva-button {
+ margin: 0px;
}
-.eva-callstack.eva-row-aligned {
- background: var(--grid-layout-holder);
+.eva-italic {
+ font-style: italic;
}
-.eva-callstack.eva-row-selected {
- background: var(--code-select);
+.eva-focused {
+ background: var(--code-select);
}
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/valueinfos.tsx b/ivette/src/frama-c/plugins/eva/valueinfos.tsx
deleted file mode 100644
index 28fb0a302494c2d5879a3b7ed5b9cf703650db45..0000000000000000000000000000000000000000
--- a/ivette/src/frama-c/plugins/eva/valueinfos.tsx
+++ /dev/null
@@ -1,148 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2022 */
-/* 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). */
-/* */
-/* ************************************************************************ */
-
-/* eslint-disable @typescript-eslint/explicit-function-return-type */
-
-// --------------------------------------------------------------------------
-// --- Info Components
-// --------------------------------------------------------------------------
-
-// React & Dome
-import React from 'react';
-import { classes } from 'dome/misc/utils';
-import { Hpack, Vpack } from 'dome/layout/boxes';
-import { Code, Cell } from 'dome/controls/labels';
-import * as States from 'frama-c/states';
-import * as Ast from 'frama-c/kernel/api/ast';
-import { ModelProp } from 'frama-c/plugins/eva/model';
-
-// Locals
-import { EvaAlarm } from './cells';
-import { Callsite } from './stacks';
-
-// --------------------------------------------------------------------------
-// --- Stmt Printer
-// --------------------------------------------------------------------------
-
-interface StmtProps {
- stmt?: Ast.marker;
- marker: Ast.marker;
- short?: boolean;
-}
-
-export function Stmt(props: StmtProps) {
- const markersInfo = States.useSyncArray(Ast.markerInfo);
-
- const { stmt, marker, short } = props;
- if (!stmt) return null;
- const line = markersInfo.getData(marker)?.sloc?.line;
- const filename = markersInfo.getData(marker)?.sloc?.base;
- const title = markersInfo.getData(stmt)?.descr;
- const text = short ? `@L${line}` : `@${filename}:${line}`;
- return (
- <span className="dome-text-cell eva-stmt" title={title}>
- {text}
- </span>
- );
-}
-
-// --------------------------------------------------------------------------
-// --- Alarms Panel
-// --------------------------------------------------------------------------
-
-export function AlarmsInfos(props: ModelProp) {
- const { model } = props;
- const probe = model.getFocused();
- if (probe) {
- const callstack = model.getCallstack();
- const domain = model.values.getValues(probe, callstack);
- const alarms = domain?.vBefore.alarms ?? [];
- if (alarms.length > 0) {
- const renderAlarm = ([status, alarm]: EvaAlarm) => {
- const className = `eva-alarm-info eva-alarm-${status}`;
- return (
- <Code className={className} icon="WARNING">{alarm}</Code>
- );
- };
- return (
- <Vpack className="eva-info">
- {React.Children.toArray(alarms.map(renderAlarm))}
- </Vpack>
- );
- }
- }
- return null;
-}
-
-// --------------------------------------------------------------------------
-// --- Stack Panel
-// --------------------------------------------------------------------------
-
-export function StackInfos(props: ModelProp) {
- const { model } = props;
- const [, setSelection] = States.useSelection();
- const focused = model.getFocused();
- const callstack = model.getCalls();
- if (callstack.length <= 1) return null;
- const makeCallsite = ({ caller, stmt }: Callsite) => {
- if (!caller || !stmt) return null;
- const key = `${caller}@${stmt}`;
- const isFocused = focused?.marker === stmt;
- const isTransient = focused?.transient;
- const className = classes(
- 'eva-callsite',
- isFocused && 'eva-focused',
- isTransient && 'eva-transient',
- );
- const select = (meta: boolean) => {
- const location = { fct: caller, marker: stmt };
- setSelection({ location });
- if (meta) States.MetaSelection.emit(location);
- };
- const onClick = (evt: React.MouseEvent) => {
- select(evt.altKey);
- };
- const onDoubleClick = (evt: React.MouseEvent) => {
- evt.preventDefault();
- select(true);
- };
- return (
- <Cell
- key={key}
- icon="TRIANGLE.LEFT"
- className={className}
- onClick={onClick}
- onDoubleClick={onDoubleClick}
- >
- {caller}
- <Stmt stmt={stmt} marker={stmt} />
- </Cell>
- );
- };
- return (
- <Hpack className="eva-info">
- {callstack.map(makeCallsite)}
- </Hpack>
- );
-}
-
-// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 3e09f9d2c5467581d8e64c430c858b864870b2d6..4c43d8c63f95e93be4924b2881075817f81c7864 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -20,396 +20,1070 @@
/* */
/* ************************************************************************ */
-/* eslint-disable @typescript-eslint/explicit-function-return-type */
-
-// --------------------------------------------------------------------------
-// --- Eva Values
-// --------------------------------------------------------------------------
-
-// React & Dome
import React from 'react';
-import * as Dome from 'dome';
+import _ from 'lodash';
+import * as Ivette from 'ivette';
+import * as Dome from 'dome/dome';
+import * as States from 'frama-c/states';
+import * as Server from 'frama-c/server';
+import * as Ast from 'frama-c/kernel/api/ast';
+import * as Values from 'frama-c/plugins/eva/api/values';
+import { GlobalState, useGlobalState } from 'dome/data/states';
+
import { classes } from 'dome/misc/utils';
-import { VariableSizeList } from 'react-window';
-import { Hpack, Filler } from 'dome/layout/boxes';
-import { Inset } from 'dome/frame/toolbars';
import { Icon } from 'dome/controls/icons';
-import { Cell } from 'dome/controls/labels';
+import { Inset } from 'dome/frame/toolbars';
+import { Cell, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
-import { ModelProp, EvalStmt, EvalCond } from 'frama-c/plugins/eva/model';
+import { Filler, Hpack, Hfill, Vpack, Vfill } from 'dome/layout/boxes';
-// Frama-C
-import * as States from 'frama-c/states';
-// Locals
-import { SizedArea, HSIZER, WSIZER } from './sized';
-import { Diff } from './diffed';
-import { sizeof, EvaValues, EvaPointedVar, Evaluation } from './cells';
-import { Probe } from './probes';
-import { Row } from './layout';
-import { Callsite } from './stacks';
-import { Stmt } from './valueinfos';
-import './style.css';
-
-// --------------------------------------------------------------------------
-// --- Cell Diffs
-// --------------------------------------------------------------------------
-
-function computeValueDiffs(v: EvaValues, vstate: EvalStmt | EvalCond) {
- let here = v.vBefore;
- let diff: undefined | Evaluation;
- let diff2: undefined | Evaluation;
- function setValue(e?: Evaluation) { if (e) { here = e; diff = v.vBefore; } }
- switch (vstate) {
- case 'Before': diff = v.vAfter; break;
- case 'After': setValue(v.vAfter); break;
- case 'Then': setValue(v.vThen); break;
- case 'Else': setValue(v.vElse); break;
- case 'Cond': diff = v.vThen; diff2 = v.vElse; break;
- }
- const vdiffs = { text: here.value, diff: diff?.value, diff2: diff2?.value };
- return { value: here, vdiffs };
-}
-// --------------------------------------------------------------------------
-// --- Table Cell
-// --------------------------------------------------------------------------
+/* -------------------------------------------------------------------------- */
+/* --- Miscellaneous definitions --- */
+/* -------------------------------------------------------------------------- */
-interface TableCellProps extends ModelProp {
- probe: Probe;
- row: Row;
-}
-
-const CELLPADDING = 12;
-
-function TableCell(props: TableCellProps) {
- const { probe, row, model } = props;
- const [, setSelection] = States.useSelection();
- const { kind, callstack } = row;
- const minWidth = CELLPADDING + WSIZER.dimension(probe.minCols);
- const maxWidth = CELLPADDING + WSIZER.dimension(probe.maxCols);
- const style = { width: minWidth, maxWidth };
- let contents: React.ReactNode = props.probe.marker;
- let valueText = '';
- let pointedVars: EvaPointedVar[] = [];
- const { transient, marker } = probe;
- const focused = model.getFocused();
- const isFocused = focused === probe;
-
- switch (kind) {
-
- // ---- Probe Contents
- case 'probes':
- {
- const { stmt, code } = probe;
- contents = (
- <>
- <span className='dome-text-cell'>{code}</span>
- <Stmt stmt={stmt} marker={marker} short />
- </>
- );
- }
- break;
-
- // ---- Values Contents
- case 'values':
- case 'callstack':
- {
- const domain = model.values.getValues(probe, callstack);
- const { condition } = probe;
- const vstate = condition ? model.getVcond() : model.getVstmt();
- const { value, vdiffs } = computeValueDiffs(domain, vstate);
- valueText = value.value;
- const text = vdiffs.text ?? vdiffs.diff;
- const { cols, rows } = sizeof(text);
- let status = 'none';
- if (value.alarms.length > 0) {
- if (value.alarms.find(([st, _]) => st === 'False')) status = 'False';
- else status = 'Unknown';
- }
- if (value.pointedVars.length > 0)
- pointedVars = value.pointedVars;
- const alarmClass = `eva-cell-alarms eva-alarm-${status}`;
- const title = 'At least one alarm is raised in one callstack';
- contents = (
- <>
- <Icon className={alarmClass} size={10} title={title} id="WARNING" />
- <SizedArea cols={cols} rows={rows}>
- <span className={`eva-state-${vstate}`}>
- <Diff {...vdiffs} />
- </span>
- </SizedArea>
- </>
- );
- }
- break;
+type Request<A, B> = (a: A) => Promise<B>;
- }
+type Alarm = [ 'True' | 'False' | 'Unknown', string ]
+function getAlarmStatus(alarms: Alarm[] | undefined): string {
+ if (!alarms) return 'none';
+ if (alarms.length === 0) return 'none';
+ if (alarms.find(([st, _]) => st === 'False')) return 'False';
+ else return 'Unknown';
+}
- // --- Cell Packing
- const className = classes(
- 'eva-cell',
- transient && 'eva-transient',
- isFocused && 'eva-focused',
- );
- const onClick = () => {
- const location = { fct: probe.fct, marker: probe.marker };
- setSelection({ location });
- model.setSelectedRow(row);
- };
- const onDoubleClick = () => {
- probe.setPersistent();
- if (probe.zoomable) probe.setZoomed(!probe.zoomed);
- };
+type MarkerTracked = [ 'Tracked', boolean ]
+type MarkerPinned = [ 'Pinned' , boolean ]
+type MarkerStatus = MarkerTracked | MarkerPinned | 'JustFocused'
- async function onContextMenu() {
- const items: Dome.PopupMenuItem[] = [];
- const copyValue = () => navigator.clipboard.writeText(valueText);
- if (valueText !== '')
- items.push({ label: 'Copy to clipboard', onClick: copyValue });
- if (items.length > 0 && pointedVars.length > 0)
- items.push('separator');
- pointedVars.forEach((lval) => {
- const [text, lvalMarker] = lval;
- const label = `Display values for ${text}`;
- const location = { fct: probe.fct, marker: lvalMarker };
- const onItemClick = () => model.addProbe(location);
- items.push({ label, onClick: onItemClick });
- });
- if (items.length > 0)
- items.push('separator');
- const remove = () => model.removeProbe(probe);
- const removeLabel = `Remove column for ${probe.code}`;
- items.push({ label: removeLabel, onClick: remove });
- if (items.length > 0) Dome.popupMenu(items);
- }
+function MarkerStatusClass(status: MarkerStatus): string {
+ if (status === 'JustFocused') return 'eva-header-just-focused';
+ const [ kind, focused ] = status;
+ return 'eva-header-' + kind.toLowerCase() + (focused ? '-focused' : '');
+}
+
+function isPinnedMarker(status: MarkerStatus): boolean {
+ if (status === 'JustFocused') return false;
+ const [ kind ] = status;
+ return kind === 'Pinned';
+}
+
+interface TableCellProps {
+ children?: JSX.Element | JSX.Element[];
+ right?: JSX.Element;
+}
+function TableCell(props: TableCellProps): JSX.Element {
+ const { children, right } = props;
return (
- <div
- className={className}
- style={style}
- onClick={onClick}
- onDoubleClick={onDoubleClick}
- onContextMenu={onContextMenu}
- >
- {contents}
+ <div className='eva-cell-container'>
+ <div className='eva-cell-left'/>
+ <div className='eva-cell-content'>
+ {children}
+ </div>
+ <div className='eva-cell-right'>
+ {right}
+ </div>
</div>
);
}
-// --------------------------------------------------------------------------
-// --- Table Section
-// --------------------------------------------------------------------------
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Callstack related definitions --- */
+/* -------------------------------------------------------------------------- */
+
+/* Callstacks are declared by the server. We add the `Summary` construction to
+ * cleanly represent the summary of all the callstacks. */
+type callstack = 'Summary' | Values.callstack
+
+/* Builds a cached version of the `getCallstacks` request */
+function useCallstacksCache(): Request<Ast.marker[], callstack[]> {
+ const g = React.useCallback((m) => Server.send(Values.getCallstacks, m), []);
+ const toString = React.useCallback((ms) => ms.join('|'), []);
+ return Dome.useCache(g, toString);
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Callsite related definitions --- */
+/* -------------------------------------------------------------------------- */
+
+/* Representation of a callsite as described in the server */
+interface Callsite {
+ callee: string;
+ caller?: string;
+ stmt?: Ast.marker;
+}
+
+/* Builds a cached version of the `getCallstackInfo` request */
+function useCallsitesCache(): Request<callstack, Callsite[]> {
+ const get = React.useCallback((c) => {
+ if (c !== 'Summary') return Server.send(Values.getCallstackInfo, c);
+ else return Promise.resolve([]);
+ }, []);
+ return Dome.useCache(get);
+}
+
+/* -------------------------------------------------------------------------- */
+
-interface TableSectionProps {
+
+/* -------------------------------------------------------------------------- */
+/* --- Probe related definitions --- */
+/* -------------------------------------------------------------------------- */
+
+/* A Location is a marker in a function */
+interface Location {
+ target: Ast.marker;
fct: string;
- folded: boolean;
- foldable: boolean;
- onClick: () => void;
- byCallstacks: boolean;
- onCallstackClick: () => void;
+}
+
+/* An Evaluation keeps track of the values at relevant control point around a
+ * statement, along with the potential errors */
+interface Evaluation {
+ errors?: string;
+ vBefore?: Values.evaluation;
+ vAfter?: Values.evaluation;
+ vThen?: Values.evaluation;
+ vElse?: Values.evaluation;
+}
+
+/* A Probe is a location along with data representing textually what it is, the
+ * considered statement, if it is an effectfull one or one with conditions.
+ * Moreover, it gives a function that computes an Evaluation for a given
+ * callstack. This computation is asynchronous. */
+interface Probe extends Location {
+ code?: string;
+ stmt?: Ast.marker;
+ rank?: number;
+ evaluable: boolean;
+ effects?: boolean;
+ condition?: boolean;
+ evaluate: Request<callstack, Evaluation>
+}
+
+/* Builds a cached version of the `getValues` request */
+function useEvaluationCache(): Request<[ Location, callstack ], Evaluation> {
+ type LocStack = [ Location, callstack ];
+ const toString = React.useCallback(([ l, c ] : LocStack): string => {
+ return `${l.fct}:${l.target}:${c}`;
+ }, []);
+ const get: Request<LocStack, Evaluation> = React.useCallback(([ l, c ]) => {
+ const callstack = c === 'Summary' ? undefined : c;
+ return Server.send(Values.getValues, { ...l, callstack });
+ }, []);
+ return Dome.useCache(get, toString);
+}
+
+/* Builds a cached function that builds a Probe given a Location */
+function useProbeCache(): Request<Location, Probe> {
+ const toString = React.useCallback((l) => `${l.fct}:${l.target}`, []);
+ const cache = useEvaluationCache();
+ const get = React.useCallback(async (loc: Location): Promise<Probe> => {
+ const infos = await Server.send(Values.getProbeInfo, loc.target);
+ const evaluate: Request<callstack, Evaluation> = (c) => cache([ loc, c ]);
+ return { ...loc, ...infos, evaluate };
+ }, [ cache ]);
+ return Dome.useCache(get, toString);
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Statement Component --- */
+/* -------------------------------------------------------------------------- */
+
+interface StmtProps {
+ stmt?: Ast.marker;
+ marker?: Ast.marker;
+ short?: boolean;
+}
+
+function Stmt(props: StmtProps): JSX.Element {
+ const markersInfo = States.useSyncArray(Ast.markerInfo);
+ const { stmt, marker, short } = props;
+ if (!stmt || !marker) return <></>;
+ const line = markersInfo.getData(marker)?.sloc?.line;
+ const filename = markersInfo.getData(marker)?.sloc?.base;
+ const title = markersInfo.getData(stmt)?.descr;
+ const text = short ? `@L${line}` : `@${filename}:${line}`;
+ const className = 'dome-text-cell eva-stmt';
+ return <span className={className} title={title}>{text}</span>;
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Informations on the alarms in a given callstack --- */
+/* -------------------------------------------------------------------------- */
+
+function AlarmsInfos(probe?: Probe): Request<callstack, JSX.Element> {
+ return async (c: callstack): Promise<JSX.Element> => {
+ const evaluation = await probe?.evaluate(c);
+ const alarms = evaluation?.vBefore?.alarms ?? [];
+ if (alarms.length <= 0) return <></>;
+ const renderAlarm = ([status, alarm]: Alarm): JSX.Element => {
+ const className = classes('eva-alarm-info', `eva-alarm-${status}`);
+ return <Code className={className} icon="WARNING">{alarm}</Code>;
+ };
+ const children = React.Children.toArray(alarms.map(renderAlarm));
+ return <Vpack className="eva-info">{children}</Vpack>;
+ };
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Informations on the selected callstack --- */
+/* -------------------------------------------------------------------------- */
+
+interface StackInfosProps {
+ callsites: Callsite[];
+ isSelected: boolean;
+ setSelection: (a: States.SelectionActions) => void;
close: () => void;
}
-function TableSection(props: TableSectionProps) {
- const { fct, foldable, folded, onClick } = props;
- const icon = folded ? 'ANGLE.RIGHT' :
- foldable ? 'ANGLE.DOWN' : 'TRIANGLE.RIGHT';
+async function StackInfos(props: StackInfosProps): Promise<JSX.Element> {
+ const { callsites, setSelection, isSelected, close } = props;
+ const selectedClass = isSelected ? 'eva-focused' : '';
+ const className = classes('eva-callsite', selectedClass);
+ if (callsites.length <= 1) return <></>;
+ const makeCallsite = ({ caller, stmt }: Callsite): JSX.Element => {
+ if (!caller || !stmt) return <></>;
+ const key = `${caller}@${stmt}`;
+ const location = { fct: caller, marker: stmt };
+ const select = (meta: boolean): void => {
+ setSelection({ location });
+ if (meta) States.MetaSelection.emit(location);
+ };
+ const onClick = (evt: React.MouseEvent): void => { select(evt.altKey); };
+ const onDoubleClick = (evt: React.MouseEvent): void => {
+ evt.preventDefault();
+ select(true);
+ };
+ return (
+ <Cell
+ key={key}
+ icon='TRIANGLE.LEFT'
+ className={className}
+ onClick={onClick}
+ onDoubleClick={onDoubleClick}
+ >
+ {caller}
+ <Stmt stmt={stmt} marker={stmt} />
+ </Cell>
+ );
+ };
+ const children = React.Children.toArray(callsites.map(makeCallsite));
return (
- <>
+ <div className='eva-info'>
+ <Hpack className='eva-info-wrap'>{children}</Hpack>
+ <Hfill />
<IconButton
- className="eva-fct-fold"
- size={10}
- offset={-1}
- icon={icon}
- enabled={foldable}
- onClick={onClick}
+ icon='CROSS'
+ className='eva-button'
+ onClick={close}
/>
- <Cell className="eva-fct-name">{fct}</Cell>
- <Filler />
+ </div>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Probe Header Component --- */
+/* -------------------------------------------------------------------------- */
+/* --- Header of a column, describing the evaluated expression and its --- */
+/* --- status inside the component (pinned, tracked, etc). --- */
+/* -------------------------------------------------------------------------- */
+
+interface ProbeHeaderProps {
+ probe: Probe;
+ status: MarkerStatus;
+ pinProbe: (pin: boolean) => void;
+ selectProbe: () => void;
+ removeProbe: () => void;
+ setSelection: (a: States.SelectionActions) => void;
+ locEvt: Dome.Event<Location>;
+}
+
+function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
+ const { probe, status, setSelection, locEvt } = props;
+ const { code = '(error)', stmt, target, fct } = probe;
+ const color = classes(MarkerStatusClass(status), 'eva-table-header-sticky');
+ const { selectProbe, removeProbe, pinProbe } = props;
+ const span = 1 + (probe.effects ? 1 : 0) + (probe.condition ? 2 : 0);
+ const buttonClass = classes('eva-button', 'eva-header-button');
+
+ // When the location is selected, we scroll the header into view, making it
+ // appears wherever it was.
+ const ref = React.createRef<HTMLTableCellElement>();
+ locEvt.on((l) => { if (l === probe) ref.current?.scrollIntoView(); });
+
+ const isPinned = isPinnedMarker(status);
+ const pinText = isPinned ? 'Unpin' : 'Pin';
+ const loc: States.SelectionActions = { location: { fct, marker: target} };
+ const onClick = (): void => { setSelection(loc); selectProbe(); };
+ const onDoubleClick = (): void => pinProbe(!isPinned);
+ const onContextMenu = (): void => {
+ const items: Dome.PopupMenuItem[] = [];
+ const pinLabel = `${pinText} column for ${code}`;
+ items.push({ label: pinLabel, onClick: onDoubleClick });
+ const removeLabel = `Remove column for ${code}`;
+ items.push({ label: removeLabel, onClick: removeProbe });
+ Dome.popupMenu(items);
+ };
+
+ const buttons =
+ <div>
<IconButton
- icon="ITEMS.LIST"
- className="eva-probeinfo-button"
- selected={props.byCallstacks}
- title="Details by callstack"
- onClick={props.onCallstackClick}
+ icon='PIN'
+ className={buttonClass}
+ title={`${pinText} the column`}
+ selected={isPinned}
+ onClick={onDoubleClick}
/>
- <Inset />
<IconButton
- icon="CROSS"
- className="eva-probeinfo-button"
- title="Close"
- onClick={props.close}
+ icon="CIRC.CLOSE"
+ className={buttonClass}
+ title="Remove the column"
+ onClick={() => removeProbe()}
/>
- </>
+ </div>;
+
+ return (
+ <th
+ ref={ref}
+ className={color}
+ colSpan={span}
+ onClick={onClick}
+ onDoubleClick={onDoubleClick}
+ onContextMenu={onContextMenu}
+ >
+ <TableCell right={buttons}>
+ <div className='eva-header-text-overflow'>
+ <span className='dome-text-cell' title={code}>{code}</span>
+ </div>
+ <Stmt stmt={stmt} marker={target} short={true}/>
+ </TableCell>
+ </th>
);
}
-// --------------------------------------------------------------------------
-// --- Table Row Header
-// --------------------------------------------------------------------------
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Probe Description Component --- */
+/* -------------------------------------------------------------------------- */
+/* --- Description of a table column, i.e. if it contains values --- */
+/* --- evaluated before or after the considered statement. --- */
+/* -------------------------------------------------------------------------- */
+
+interface ProbeDescrProps {
+ probe: Probe;
+}
+
+function ProbeDescr(props: ProbeDescrProps): JSX.Element[] {
+ const { probe } = props;
+ const valuesClass = classes('eva-table-values', 'eva-table-values-center');
+ const tableClass = classes('eva-table-descrs', 'eva-table-descr-sticky');
+ const cls = classes(valuesClass, tableClass);
+ const title = (s: string): string => `Values ${s} the statement evaluation`;
+ const elements: JSX.Element[] = [];
+ function push(title: string, children: JSX.Element | string): void {
+ elements.push(<td className={cls} title={title}>{children}</td>);
+ }
+ if (!probe.effects && !probe.condition)
+ push('Values at the statement', '-');
+ if (probe.effects || probe.condition)
+ push(title('before'), 'Before');
+ if (probe.effects)
+ push(title('after'), 'After');
+ if (probe.condition) {
+ const pushCondition = (s: string): void => {
+ const t = `Values after the condition, in the ${s.toLowerCase()} branch`;
+ const child =
+ <div className='eva-header-after-condition'>
+ After
+ <div className='eva-stmt'>{`(${s})`}</div>
+ </div>;
+ push(t, child);
+ };
+ pushCondition('Then');
+ pushCondition('Else');
+ }
+ return elements;
+}
+
+/* -------------------------------------------------------------------------- */
+
-interface TableHeadProps {
- stackCalls: Callsite[];
- stackIndex: number | undefined;
- stackCount: number | undefined;
- onClick: () => void;
+
+/* -------------------------------------------------------------------------- */
+/* --- Probe Values Component --- */
+/* -------------------------------------------------------------------------- */
+/* --- This component represents the contents of one of the table that --- */
+/* --- displays values information. As the content depends on the --- */
+/* --- considered callstack, we decided to return a function that build --- */
+/* --- the actual component when given a callstack. It avoids useless --- */
+/* --- computational boilerplate. --- */
+/* -------------------------------------------------------------------------- */
+
+interface ProbeValuesProps {
+ probe: Probe;
+ addLoc: (loc: Location) => void;
+ isSelectedCallstack: (c: callstack) => boolean;
}
-function makeStackTitle(calls: Callsite[]) {
+function ProbeValues(props: ProbeValuesProps): Request<callstack, JSX.Element> {
+ const { probe, addLoc, isSelectedCallstack } = props;
+
+ // Building common parts
+ const onContextMenu = (evaluation?: Values.evaluation) => (): void => {
+ const { value = '', pointedVars = [] } = evaluation ?? {};
+ const items: Dome.PopupMenuItem[] = [];
+ const copy = (): void => { navigator.clipboard.writeText(value); };
+ if (value !== '') items.push({ label: 'Copy to clipboard', onClick: copy });
+ if (items.length > 0 && pointedVars.length > 0) items.push('separator');
+ pointedVars.forEach((lval) => {
+ const [text, lvalMarker] = lval;
+ const label = `Display values for ${text}`;
+ const location = { fct: probe.fct, target: lvalMarker };
+ const onItemClick = (): void => addLoc(location);
+ items.push({ label, onClick: onItemClick });
+ });
+ if (items.length > 0) Dome.popupMenu(items);
+ };
+
+ return async (callstack: callstack): Promise<JSX.Element> => {
+ const evaluation = await probe.evaluate(callstack);
+ const { vBefore, vAfter, vThen, vElse } = evaluation;
+ const isSelected = isSelectedCallstack(callstack);
+ const selected = isSelected && callstack !== 'Summary' ? 'eva-focused' : '';
+ const font = callstack === 'Summary' ? 'eva-italic' : '';
+ const className = classes('eva-table-values', selected, font);
+ const kind = callstack === 'Summary' ? 'one' : 'this';
+ const title = `At least one alarm is raised in ${kind} callstack`;
+ function td(e?: Values.evaluation, colSpan = 1): JSX.Element {
+ const { alarms, value = '-' } = e ?? {};
+ const status = getAlarmStatus(alarms);
+ const alarmClass = classes('eva-cell-alarms', `eva-alarm-${status}`);
+ const align = value?.includes('\n') ? 'left' : 'center';
+ const alignClass = `eva-table-values-${align}`;
+ const c = classes(className, alignClass);
+ const warning =
+ <Icon className={alarmClass} size={10} title={title} id="WARNING" />;
+ return (
+ <td className={c} colSpan={colSpan} onContextMenu={onContextMenu(e)}>
+ <TableCell right={warning}>
+ <span className='eva-table-text'>{value}</span>
+ </TableCell>
+ </td>
+ );
+ }
+ const elements: JSX.Element[] = [];
+ if (probe.effects && _.isEqual(vBefore, vAfter))
+ elements.push(td(vBefore, 2));
+ else {
+ if (!probe.effects && !probe.condition)
+ elements.push(td(vBefore));
+ if (probe.effects || probe.condition)
+ elements.push(td(vBefore));
+ if (probe.effects)
+ elements.push(td(vAfter));
+ if (probe.condition)
+ elements.push(td(vThen), td(vElse));
+ }
+ return <>{React.Children.toArray(elements)}</>;
+ };
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Row header describing the corresponding callstack --- */
+/* -------------------------------------------------------------------------- */
+
+interface CallsiteCellProps {
+ callstack: callstack | 'Header';
+ index?: number;
+ getCallsites: Request<callstack, Callsite[]>;
+ selectedClass?: string;
+}
+
+function makeStackTitle(calls: Callsite[]): string {
const cs = calls.slice(1);
if (cs.length > 0)
return `Callstack: ${cs.map((c) => c.callee).join(' \u2190 ')}`;
return 'Callstack Details';
}
-function TableHead(props: TableHeadProps) {
- const sk = props.stackIndex;
- const sc = props.stackCount;
- const hdClass = classes('eva-head', sc ? undefined : 'dome-hidden');
- const hdHeader = sk === undefined;
- const hdSummary = sk !== undefined && sk < 0;
- const hdNumber = sk === undefined ? 0 : 1 + sk;
- const hdTitle =
- hdHeader ? 'Callstack / Summary' :
- hdSummary ? 'Summary' : makeStackTitle(props.stackCalls);
- return (
- <div
- className={hdClass}
- title={hdTitle}
- onClick={props.onClick}
- >
- <div className="eva-phantom">{'\u2211'}{sc ?? '#'}</div>
- {hdHeader ? '#' : hdSummary ? '\u2211' : `${hdNumber}`}
- </div>
- );
+async function CallsiteCell(props: CallsiteCellProps): Promise<JSX.Element> {
+ const { callstack, index, getCallsites, selectedClass = '' } = props;
+ const baseClasses = classes('eva-table-callsite-box', selectedClass);
+ switch (callstack) {
+ case 'Header': {
+ const cls = classes(baseClasses, 'eva-table-header-sticky');
+ const title = 'Callstack at which expressions are evaluated';
+ return <td className={cls} rowSpan={2} title={title}>{'#'}</td>;
+ }
+ default: {
+ const cls = classes(baseClasses, 'eva-table-value-sticky');
+ const callsites = await getCallsites(callstack);
+ const isSummary = callstack === 'Summary';
+ const summary = 'Summary: value consolidated accross all callstacks';
+ const infos = isSummary ? summary : makeStackTitle(callsites);
+ const text = isSummary ? '∑' : (index ? index.toString() : '0');
+ return <td className={cls} title={infos}>{text}</td>;
+ }
+ }
}
-// --------------------------------------------------------------------------
-// --- Table Row
-// --------------------------------------------------------------------------
+/* -------------------------------------------------------------------------- */
+
+
-interface TableRowProps {
- style: React.CSSProperties;
- index: number;
- data: ModelProp;
+/* -------------------------------------------------------------------------- */
+/* --- Function Section Component --- */
+/* -------------------------------------------------------------------------- */
+
+interface FunctionProps {
+ fct: string;
+ markers: Map<Ast.marker, MarkerStatus>;
+ close: () => void;
+ getProbe: Request<Location, Probe>;
+ pinProbe: (probe: Probe, pin: boolean) => void;
+ selectProbe: (probe: Probe) => void;
+ removeProbe: (probe: Probe) => void;
+ addLoc: (loc: Location) => void;
+ folded: boolean;
+ setFolded: (folded: boolean) => void;
+ getCallsites: Request<callstack, Callsite[]>;
+ byCallstacks: boolean;
+ getCallstacks: Request<Ast.marker[], callstack[]>;
+ setByCallstacks: (byCallstack: boolean) => void;
+ selectCallstack: (callstack: callstack) => void;
+ isSelectedCallstack: (c: callstack) => boolean;
+ setSelection: (a: States.SelectionActions) => void;
+ locEvt: Dome.Event<Location>;
+ startingCallstack: number;
+ changeStartingCallstack: (n: number) => void;
}
-function TableRow(props: TableRowProps) {
- const { model } = props.data;
- const row = model.getRow(props.index);
- if (!row) return null;
- const { kind, probes } = row;
- if (kind === 'section') {
- const { fct } = row;
- if (!fct) return null;
- const folded = model.isFolded(fct);
- const foldable = model.isFoldable(fct);
- const byCallstacks = model.isByCallstacks(fct);
+const PageSize = 99;
+
+async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
+ const { fct, folded, isSelectedCallstack, locEvt } = props;
+ const { byCallstacks, setSelection, getCallsites } = props;
+ const { addLoc, getCallstacks: getCS } = props;
+ const { setFolded, setByCallstacks, close } = props;
+ const { startingCallstack, changeStartingCallstack } = props;
+ const displayTable = folded ? 'none' : 'block';
+ type RowHandler = React.MouseEventHandler<HTMLTableRowElement>;
+ const onClick: (c: callstack) => RowHandler = (c) => (event) => {
+ const elt = document.elementFromPoint(event.clientX, event.clientY);
+ if (elt?.localName !== 'span')
+ props.selectCallstack(isSelectedCallstack(c) ? 'Summary' : c);
+ };
+
+ /* Computes the relevant callstacks */
+ const markers = Array.from(props.markers.keys());
+ const allCallstacks = await getCS(markers);
+ const summaryOnly = allCallstacks.length === 1;
+ const callstacks = byCallstacks || summaryOnly ? allCallstacks : [];
+ const nbCS = allCallstacks.length;
+
+ /* Computes the relevant data for each marker */
+ interface Data { probe: Probe; summary: Evaluation; status: MarkerStatus }
+ const entries = Array.from(props.markers.entries());
+ const data = await Promise.all(entries.map(async ([ target, status ]) => {
+ const probe = await props.getProbe({ target, fct });
+ const summary = await probe.evaluate('Summary');
+ return { probe, summary, status } as Data;
+ }));
+ const doCall = data.length > 0;
+
+ /* Computes the headers for each marker */
+ const headerCall = await CallsiteCell({ getCallsites, callstack: 'Header' });
+ const headers = await Promise.all(data.map((d: Data) => {
+ const pinProbe = (pin: boolean): void => props.pinProbe(d.probe, pin);
+ const selectProbe = (): void => props.selectProbe(d.probe);
+ const removeProbe = (): void => props.removeProbe(d.probe);
+ const fcts = { selectProbe, pinProbe, removeProbe, setSelection };
+ return ProbeHeader({ ...d, ...fcts, locEvt });
+ }));
+
+ /* Computes the columns descriptions */
+ const descrs = data.map((d) => ProbeDescr(d)).flat();
+
+ /* Computes the summary values */
+ const miscs = { addLoc, isSelectedCallstack };
+ const builders = data.map((d: Data) => ProbeValues({ ...d, ...miscs }));
+ const summary = await Promise.all(builders.map((b) => b('Summary')));
+ const summCall = await CallsiteCell({ callstack: 'Summary', getCallsites });
+ let summaryRow = <></>;
+ if (!summaryOnly) {
+ summaryRow =
+ <tr key={'Summary'} onClick={onClick('Summary')}>
+ {doCall ? summCall : undefined}
+ {React.Children.toArray(summary)}
+ </tr>;
+ }
+
+ /* Computes the values for each callstack */
+ const start = Math.max(1, startingCallstack);
+ const stop = Math.min(start + PageSize, callstacks.length);
+ const values = await Promise.all(callstacks.map(async (callstack, n) => {
+ const index = n + 1;
+ if (start > index || stop < index) return <></>;
+ const selectedClass = isSelectedCallstack(callstack) ? 'eva-focused' : '';
+ const callProps = { selectedClass, getCallsites };
+ const call = await CallsiteCell({ index, callstack, ...callProps });
+ const values = await Promise.all(builders.map((b) => b(callstack)));
return (
- <Hpack className="eva-function" style={props.style}>
- <TableSection
- fct={fct}
- folded={folded}
- foldable={foldable}
- onClick={() => model.setFolded(fct, !folded)}
- byCallstacks={byCallstacks}
- onCallstackClick={() => model.setByCallstacks(fct, !byCallstacks)}
- close={() => model.clearFunction(fct)}
- />
- </Hpack>
+ <tr key={callstack} onClick={onClick(callstack)}>
+ {call}
+ {React.Children.toArray(values)}
+ </tr>
);
- }
- const sk = row.stackIndex;
- const sc = row.stackCount;
- const cs = row.callstack;
- const calls = cs ? model.stacks.getCalls(cs) : [];
- const rowKind = `eva-${kind}`;
- const rowParity = sk !== undefined && sk % 2 === 1;
- const rowIndexKind =
- model.isSelectedRow(row) ? 'eva-row-selected' :
- model.isAlignedRow(row) ? 'eva-row-aligned' :
- rowParity ? 'eva-row-odd' : 'eva-row-even';
- const rowClass = classes('eva-row', rowKind, rowIndexKind);
- const onHeaderClick = () => model.setSelectedRow(row);
- const makeCell = (probe: Probe) => (
- <TableCell
- key={probe.marker}
- probe={probe}
- row={row}
- model={model}
- />
- );
+ }));
+
+ /* We change the starting callstack dynamically when we reach the ends of the
+ * scroll to avoid to build the complete table */
+ const onScroll: React.UIEventHandler<HTMLDivElement> = (event) => {
+ const { scrollTop, scrollHeight, clientHeight } = event.currentTarget;
+ if (scrollTop / (scrollHeight - clientHeight) <= 0.1)
+ changeStartingCallstack(Math.max(startingCallstack - 10, 0));
+ const botGap = (scrollHeight - scrollTop - clientHeight) / scrollHeight;
+ const lastCallstack = startingCallstack + PageSize;
+ if (botGap <= 0.1 && lastCallstack !== callstacks.length) {
+ const maxStart = callstacks.length - PageSize;
+ const start = Math.min(startingCallstack + 10, maxStart);
+ changeStartingCallstack(start);
+ }
+ };
+
+ /* Builds the component */
return (
- <Hpack style={props.style}>
- <div className={rowClass}>
- <TableHead
- stackIndex={sk}
- stackCount={sc}
- stackCalls={calls}
- onClick={onHeaderClick}
+ <>
+ <Hpack className="eva-function">
+ <IconButton
+ className="eva-fct-fold"
+ icon={folded ? 'ANGLE.RIGHT' : 'ANGLE.DOWN'}
+ onClick={() => setFolded(!folded)}
+ />
+ <Cell className="eva-fct-name">{fct}</Cell>
+ <Filler />
+ <div className='eva-nb-callstacks'>
+ {`${nbCS} callstack${nbCS > 1 ? 's' : ''}`}
+ </div>
+ <IconButton
+ icon="ITEMS.LIST"
+ className="eva-button"
+ selected={byCallstacks}
+ disabled={summaryOnly}
+ title="Show values by callstack"
+ onClick={() => setByCallstacks(!byCallstacks)}
+ />
+ <Inset />
+ <IconButton
+ icon="CROSS"
+ className="eva-button"
+ title="Close"
+ onClick={close}
/>
- {probes.map(makeCell)}
+ </Hpack>
+ <div
+ onScroll={onScroll}
+ className='eva-table-container'
+ style={{ display: displayTable }}
+ >
+ <table className='eva-table'>
+ <tbody>
+ <tr>
+ {doCall ? headerCall : undefined}
+ {React.Children.toArray(headers)}
+ </tr>
+ <tr>
+ {React.Children.toArray(descrs)}
+ </tr>
+ {summaryRow}
+ {React.Children.toArray(values)}
+ </tbody>
+ </table>
</div>
- <Filler />
- </Hpack>
+ </>
);
}
-// --------------------------------------------------------------------------
-// --- Values Panel
-// --------------------------------------------------------------------------
+/* -------------------------------------------------------------------------- */
-export interface Dimension {
- width: number;
- height: number;
-}
-export interface ValuesPanelProps extends Dimension, ModelProp {
- zoom: number;
+
+/* -------------------------------------------------------------------------- */
+/* --- Function Manager --- */
+/* -------------------------------------------------------------------------- */
+/* --- The Function Manager is responsible of all the data related to --- */
+/* --- programs functions. --- */
+/* -------------------------------------------------------------------------- */
+
+/* Informations on one function */
+class FunctionInfos {
+
+ readonly fct: string; // Function's name
+ readonly pinned = new Set<Ast.marker>(); // Pinned markers
+ readonly tracked = new Set<Ast.marker>(); // Tracked markers
+ startingCallstack = 1; // First displayed callstack
+ byCallstacks = false; // True if displayed by callstacks
+ folded = false; // True if folded
+
+ constructor(fct: string) {
+ this.fct = fct;
+ }
+
+ has(marker: Ast.marker): boolean {
+ const pinned = this.pinned.has(marker);
+ const tracked = this.tracked.has(marker);
+ return pinned || tracked;
+ }
+
+ pin(marker: Ast.marker): void {
+ this.pinned.add(marker);
+ this.tracked.delete(marker);
+ }
+
+ track(marker: Ast.marker): void {
+ this.tracked.add(marker);
+ this.pinned.delete(marker);
+ }
+
+ delete(marker: Ast.marker): void {
+ this.pinned.delete(marker);
+ this.tracked.delete(marker);
+ }
+
+ isEmpty(): boolean {
+ return this.pinned.size === 0 && this.tracked.size === 0;
+ }
+
+ markers(focusedLoc?: Location): Map<Ast.marker, MarkerStatus> {
+ const { target: tgt, fct } = focusedLoc ?? {};
+ const inFct = fct !== undefined && fct === this.fct;
+ const ms = new Map<Ast.marker, MarkerStatus>();
+ this.pinned.forEach((p) => ms.set(p, [ 'Pinned', inFct && tgt === p ]));
+ this.tracked.forEach((p) => ms.set(p, [ 'Tracked', inFct && tgt === p ]));
+ if (inFct && tgt && !this.has(tgt)) ms.set(tgt, 'JustFocused');
+ return new Map(Array.from(ms.entries()).reverse());
+ }
+
}
-export function ValuesPanel(props: ValuesPanelProps) {
- const { zoom, width, height, model } = props;
- // --- reset line cache
- const listRef = React.useRef<VariableSizeList>(null);
- const [rowCount, setRowCount] = React.useState(model.getRowCount());
- Dome.useEvent(model.laidout, () => {
- // The layout has changed, so the number of rows may also have changed.
- setRowCount(model.getRowCount());
- setImmediate(() => {
- const vlist = listRef.current;
- if (vlist) vlist.resetAfterIndex(0, true);
+/* State keeping tracks of informations for every relevant functions */
+class FunctionsManager {
+
+ private readonly cache = new Map<string, FunctionInfos>();
+
+ constructor() {
+ this.newFunction = this.newFunction.bind(this);
+ this.getInfos = this.getInfos.bind(this);
+ this.setByCallstacks = this.setByCallstacks.bind(this);
+ this.setFolded = this.setFolded.bind(this);
+ this.pin = this.pin.bind(this);
+ this.track = this.track.bind(this);
+ this.removeLocation = this.removeLocation.bind(this);
+ this.delete = this.delete.bind(this);
+ this.clear = this.clear.bind(this);
+ this.map = this.map.bind(this);
+ }
+
+ newFunction(fct: string): void {
+ if (!this.cache.has(fct)) this.cache.set(fct, new FunctionInfos(fct));
+ }
+
+ private getInfos(fct: string): FunctionInfos {
+ const { cache } = this;
+ if (cache.has(fct)) return cache.get(fct) as FunctionInfos;
+ const infos = new FunctionInfos(fct);
+ this.cache.set(fct, infos);
+ return infos;
+ }
+
+ isEmpty(fct: string): boolean {
+ const infos = this.cache.get(fct);
+ return infos ? infos.isEmpty() : true;
+ }
+
+ setByCallstacks(fct: string, byCallstacks: boolean): void {
+ const infos = this.cache.get(fct);
+ if (infos) infos.byCallstacks = byCallstacks;
+ }
+
+ setFolded(fct: string, folded: boolean): void {
+ const infos = this.cache.get(fct);
+ if (infos) infos.folded = folded;
+ }
+
+ changeStartingCallstack(fct: string, n: number): void {
+ const infos = this.cache.get(fct);
+ if (infos) infos.startingCallstack = n;
+ }
+
+ pin(loc: Location): void {
+ const { target, fct } = loc;
+ this.getInfos(fct).pin(target);
+ }
+
+ unpin(loc: Location): void {
+ const { target, fct } = loc;
+ this.cache.get(fct)?.pinned.delete(target);
+ }
+
+ track(loc: Location): void {
+ const { target, fct } = loc;
+ this.getInfos(fct).track(target);
+ }
+
+ removeLocation(loc: Location): void {
+ const { target, fct } = loc;
+ const infos = this.cache.get(fct);
+ if (infos) infos.delete(target);
+ }
+
+ delete(fct: string): void {
+ this.cache.delete(fct);
+ }
+
+ clear(): void {
+ this.cache.clear();
+ }
+
+ clean(focused?: Location): void {
+ const focusedFct = focused?.fct;
+ this.cache.forEach((infos) => {
+ if (focusedFct !== infos.fct && infos.isEmpty())
+ this.cache.delete(infos.fct);
});
- });
- // --- compute line height
- const getRowHeight = React.useCallback(
- (k: number) => HSIZER.dimension(model.getRowLines(k)),
- [model],
- );
- // --- compute layout
- const margin = WSIZER.capacity(width);
- const estimatedHeight = HSIZER.dimension(1);
- const [selection] = States.useSelection();
+ }
+
+ map<A>(func: (infos: FunctionInfos, fct: string) => A): A[] {
+ const entries = Array.from(this.cache.entries());
+ return entries.map(([ fct, infos ]) => func(infos, fct));
+ }
+
+}
+
+/* -------------------------------------------------------------------------- */
+
+
+
+/* -------------------------------------------------------------------------- */
+/* --- Eva Table Complet Component --- */
+/* -------------------------------------------------------------------------- */
+
+/* Table's state. It is global for when the user changes the view. */
+const CallstackState = new GlobalState<callstack>('Summary');
+const FunctionsManagerState = new GlobalState(new FunctionsManager());
+const FocusState = new GlobalState<Probe | undefined>(undefined);
+
+/* Component */
+function EvaTable(): JSX.Element {
+
+ /* Component state */
+ const [ selection, select ] = States.useSelection();
+ const [ cs, setCS ] = useGlobalState(CallstackState);
+ const [ fcts ] = useGlobalState(FunctionsManagerState);
+ const [ focus, setFocus ] = useGlobalState(FocusState);
+
+ /* Used to force the component update. We cannot use the `forceUpdate` hook
+ * proposed by Dome as we need to be able to add dependencies on a changing
+ * value (here tac) explicitly. We need to force the update as modifications
+ * of the Function Manager internal data does NOT trigger the component
+ * update. */
+ const [ tac, setTic ] = React.useState(0);
+
+ /* Event use to communicate when a location is selected. Used to scroll
+ * related column into view if needed */
+ const [ locEvt ] = React.useState(new Dome.Event<Location>('eva-location'));
+
+ /* Build cached version of needed server's requests */
+ const getProbe = useProbeCache();
+ const getCallsites = useCallsitesCache();
+ const getCallstacks = useCallstacksCache();
+
+ /* Computing the function corresponding to the selected callstack */
+ const csFctPromise = React.useMemo(async () => {
+ const selectedCSInfos = await getCallsites(cs);
+ if (selectedCSInfos.length === 0) return undefined;
+ else return selectedCSInfos[0].callee;
+ }, [ cs, getCallsites ]);
+ const { result: csFct } = Dome.usePromise(csFctPromise);
+
+ /* Reset the selected callstack when the corresponding function is removed */
+ React.useEffect(() => {
+ if (csFct && fcts.isEmpty(csFct) && focus?.fct !== csFct)
+ setCS('Summary');
+ }, [ csFct, setCS, fcts, focus?.fct ] );
+
+ /* Updated the focused Probe when the selection changes. Also emit on the
+ * `locEvent` event. */
+ React.useEffect(() => {
+ const target = selection?.current?.marker;
+ const fct = selection?.current?.fct;
+ const loc = (target && fct) ? { target, fct } : undefined;
+ fcts.clean(loc);
+ const doUpdate = (p: Probe): void => {
+ if (!p.evaluable) { setFocus(undefined); return; }
+ if (fct && p.code) fcts.newFunction(fct);
+ setFocus(p); locEvt.emit(p);
+ };
+ if (loc) getProbe(loc).then(doUpdate);
+ else setFocus(undefined);
+ }, [ fcts, selection, getProbe, setFocus, locEvt ]);
+
+ /* Callback used to pin or unpin a location */
+ const setLocPin = React.useCallback((loc: Location, pin: boolean): void => {
+ if (pin) fcts.pin(loc);
+ else fcts.unpin(loc);
+ setTic(tac + 1);
+ }, [fcts, setTic, tac]);
+
+ /* On meta-selection, pin the selected location. */
React.useEffect(() => {
- const location = selection?.current;
- model.setLayout({ zoom, margin, location });
+ const pin = (loc: States.Location): void => {
+ const {marker, fct} = loc;
+ if (marker && fct) setLocPin({ target: marker, fct }, true);
+ };
+ States.MetaSelection.on(pin);
+ return () => States.MetaSelection.off(pin);
});
- // --- render list
+
+ /* Callback used to remove a probe */
+ const remove = React.useCallback((probe: Probe): void => {
+ fcts.removeLocation(probe);
+ if (probe.target === focus?.target) {
+ setFocus(undefined);
+ fcts.clean(undefined);
+ }
+ else {
+ fcts.clean(focus);
+ }
+ setTic(tac + 1);
+ }, [ fcts, focus, setFocus, tac ]);
+
+ /* Builds the sections for each function. As the component is built
+ * asynchronously, we have to use the `usePromise` hook, which forces us to
+ * memoize the promises building. */
+ const functionsPromise = React.useMemo(() => {
+ const ps = fcts.map((infos, fct) => {
+ const { byCallstacks, folded } = infos;
+ const isSelectedCallstack = (c: callstack): boolean => c === cs;
+ const setFolded = (folded: boolean): void => {
+ fcts.setFolded(fct, folded);
+ setTic(tac + 1);
+ };
+ const setByCS = (byCS: boolean): void => {
+ fcts.setByCallstacks(fct, byCS);
+ setTic(tac + 1);
+ };
+ const changeStartingCallstack = (n: number): void => {
+ fcts.changeStartingCallstack(fct, n);
+ setTic(tac + 1);
+ };
+ const close = (): void => {
+ fcts.delete(fct);
+ if (csFct === fct) setCS('Summary');
+ setTic(tac + 1);
+ };
+ return {
+ fct,
+ markers: infos.markers(focus),
+ close,
+ pinProbe: setLocPin,
+ getProbe,
+ selectProbe: setFocus,
+ removeProbe: remove,
+ addLoc: (loc: Location) => { fcts.pin(loc); setTic(tac + 1); },
+ folded,
+ setFolded,
+ getCallsites,
+ byCallstacks,
+ getCallstacks,
+ setByCallstacks: setByCS,
+ selectCallstack: (c: callstack) => { setCS(c); setTic(tac + 1); },
+ isSelectedCallstack,
+ setSelection: select,
+ locEvt,
+ startingCallstack: infos.startingCallstack,
+ changeStartingCallstack,
+ };
+ });
+ return Promise.all(ps.map(FunctionSection));
+ },
+ [ cs, setCS, fcts, focus, setFocus, tac, getCallsites, setLocPin, csFct,
+ getCallstacks, getProbe, remove, select, locEvt ]);
+ const { result: functions } = Dome.usePromise(functionsPromise);
+
+ /* Builds the alarms component. As for the function sections, it is an
+ * asynchronous process. */
+ const alarmsProm = React.useMemo(() => AlarmsInfos(focus)(cs), [ focus, cs ]);
+ const { result: alarmsInfos } = Dome.usePromise(alarmsProm);
+
+ /* Builds the stacks component. As for the function sections, it is an
+ * asynchronous process. */
+ const stackInfosPromise = React.useMemo(async () => {
+ const callsites = await getCallsites(cs);
+ const tgt = selection.current?.marker;
+ const p = (c: Callsite): boolean => c.stmt !== undefined && c.stmt === tgt;
+ const isSelected = callsites.find(p) !== undefined;
+ const close = (): void => setCS('Summary');
+ return StackInfos({ callsites, isSelected, setSelection: select, close });
+ }, [ cs, setCS, select, getCallsites, selection ]);
+ const { result: stackInfos } = Dome.usePromise(stackInfosPromise);
+
+ /* Builds the component */
return (
- <VariableSizeList
- ref={listRef}
- itemCount={rowCount}
- itemKey={model.getRowKey}
- itemSize={getRowHeight}
- estimatedItemSize={estimatedHeight}
- width={width}
- height={height}
- itemData={{ model }}
- >
- {TableRow}
- </VariableSizeList>
+ <>
+ <Ivette.TitleBar />
+ <div className='eva-functions-section'>
+ {React.Children.toArray(functions)}
+ </div>
+ <Vfill/>
+ {alarmsInfos}
+ {stackInfos}
+ </>
);
+
}
-// --------------------------------------------------------------------------
+/* Registers the component in Ivette */
+Ivette.registerComponent({
+ id: 'frama-c.plugins.values',
+ group: 'frama-c.plugins',
+ rank: 1,
+ label: 'Eva Values',
+ title: 'Values inferred by the Eva analysis',
+ children: <EvaTable />,
+});
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 11b59f05e8aeaacd4265712bb5ad6f52d79cae78..c0d940c7f09c3083b19e9882d26889712d1812cf 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -788,7 +788,10 @@ export function setSelection(location: Location, meta = false) {
/** Current selection. */
export function useSelection(): [Selection, (a: SelectionActions) => void] {
const [current, setCurrent] = useGlobalState(GlobalSelection);
- return [current, (action) => setCurrent(reducer(current, action))];
+ const callback = React.useCallback((action) => {
+ setCurrent(reducer(current, action));
+ }, [ current, setCurrent ]);
+ return [current, callback];
}
/** Resets the selected locations. */
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index a85d9720d60264fb8450f83a879f43216583e4b0..784b1a0fa9ad832637b2d1a9d7f761b8f95e8b2f 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -85,10 +85,10 @@ let () = Analysis.register_computation_hook ~on:Computed
let next_steps s =
match s.skind with
| If (cond, _, _, _) -> [ `Then cond ; `Else cond ]
- | Instr (Set _ | Call _ | Local_init _ | Asm _ | Code_annot _)
+ | Instr (Set _ | Call _ | Local_init _) -> [ `After ]
+ | Instr (Asm _ | Code_annot _)
| Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| TryCatch _ | TryFinally _ | TryExcept _
- -> [ `After ]
| Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
let probe_stmt s =
@@ -102,6 +102,7 @@ let probe_stmt s =
let probe marker =
let open Printer_tag in
match marker with
+ | PLval (_, _, (Var vi, NoOffset)) when Cil.isFunctionType vi.vtype -> None
| PLval(_,Kstmt s,l) -> Some (Plval (l,s))
| PExp(_,Kstmt s,e) -> Some (Pexpr (e,s))
| PStmt(_,s) | PStmtStart(_,s) -> probe_stmt s
@@ -354,7 +355,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let dstate ~after stmt = function
| None -> (A.get_stmt_state ~after stmt :> dstate)
| Some cs ->
- match A.get_stmt_state_by_callstack ~after stmt with
+ match A.get_stmt_state_by_callstack ~selection:[cs] ~after stmt with
| (`Top | `Bottom) as res -> res
| `Value cmap ->
try `Value (CSmap.find cmap cs)
@@ -530,7 +531,10 @@ let () =
let () =
let getProbeInfo = Request.signature ~input:(module Jmarker) () in
- let set_code = Request.result_opt getProbeInfo
+ let set_evaluable = Request.result getProbeInfo
+ ~name:"evaluable" ~descr:(Md.plain "Can the probe be evaluated?")
+ (module Jbool)
+ and set_code = Request.result_opt getProbeInfo
~name:"code" ~descr:(Md.plain "Probe source code")
(module Jstring)
and set_stmt = Request.result_opt getProbeInfo
@@ -547,6 +551,9 @@ let () =
~default:false (module Jbool)
in
let set_probe rq pp p s =
+ let computed = Analysis.is_computed () in
+ let reachable = Results.is_reachable s in
+ set_evaluable rq (computed && reachable);
set_code rq (Some (Pretty_utils.to_string pp p)) ;
set_stmt rq (Some s) ;
set_rank rq (Ranking.stmt s) ;
@@ -563,7 +570,7 @@ let () =
match probe marker with
| Some (Plval (l, s)) -> set_probe rq Printer.pp_lval l s
| Some (Pexpr (e, s)) -> set_probe rq Printer.pp_exp e s
- | None -> ()
+ | None -> set_evaluable rq false
end
(* -------------------------------------------------------------------------- *)