From 520b966f90332ef42b571d5de84e5702a6a1b28a Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Thu, 31 Mar 2022 13:59:53 +0200
Subject: [PATCH] [ivette] Get ride of the SelectedProbeInfo component
---
ivette/src/frama-c/plugins/eva/style.css | 79 ++------
ivette/src/frama-c/plugins/eva/valuetable.tsx | 173 +++++-------------
2 files changed, 62 insertions(+), 190 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index b1f806a19cd..6fab09886b9 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -1,61 +1,3 @@
-/* -------------------------------------------------------------------------- */
-/* --- Probe Panel --- */
-/* -------------------------------------------------------------------------- */
-
-.eva-probeinfo {
- min-height: 32px;
- padding-left: 6px;
- padding-top: 2px;
- padding-bottom: 4px;
- width: 100%;
- background: var(--background-profound);
- display: flex;
-}
-
-.eva-probeinfo-label {
- flex: 0 1 auto;
- min-width: 22px;
- text-align: left;
-}
-
-.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-probeinfo-stmt {
- flex: 0 0 auto;
- margin-left: 2px;
- margin-right: 0px;
- margin-top: 2px;
-}
-
-.eva-probeinfo-button {
- flex: 0 0 auto;
- margin: 1px;
- min-width: 16px;
-}
-
-.eva-probeinfo-state {
- margin-top: 2px;
- margin-bottom: 2px;
-}
-
-.eva-probeinfo-code-text {
- padding: 3px;
- white-space: pre;
- overflow: hidden;
- text-overflow: ellipsis;
-}
-
/* -------------------------------------------------------------------------- */
/* --- Call Stack Info --- */
/* -------------------------------------------------------------------------- */
@@ -222,8 +164,15 @@
gap: 0.3em;
}
-.eva-italic {
- font-style: italic;
+.eva-header-buttons-container {
+ position: absolute;
+ right: 1px;
+ top: 0px;
+ display: flex;
+}
+
+.eva-header-button {
+ padding: 2px 2px 3px 2px;
}
/* -------------------------------------------------------------------------- */
@@ -310,9 +259,17 @@ tr:first-of-type > .eva-table-callsite-box {
}
/* -------------------------------------------------------------------------- */
-/* --- Selected Element Background --- */
+/* --- Miscellaneous --- */
/* -------------------------------------------------------------------------- */
+.eva-button {
+ margin: 0px;
+}
+
+.eva-italic {
+ font-style: italic;
+}
+
.eva-focused {
background: var(--code-select);
}
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 174f8d693b9..581b6a088a4 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -28,13 +28,12 @@ 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 ControlPoint from 'frama-c/plugins/eva/ControlPoint';
import { classes } from 'dome/misc/utils';
import { Icon } from 'dome/controls/icons';
+import { Inset } from 'dome/frame/toolbars';
import { Cell, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
-import { Inset, Button, ButtonGroup } from 'dome/frame/toolbars';
import { Filler, Hpack, Hfill, Vpack, Vfill } from 'dome/layout/boxes';
@@ -44,8 +43,6 @@ import { Filler, Hpack, Hfill, Vpack, Vfill } from 'dome/layout/boxes';
/* -------------------------------------------------------------------------- */
type Request<A, B> = (a: A) => Promise<B>;
-type StateToDisplay = { before: boolean; after: boolean }
-const defaultState = { before: true, after: true };
type Alarm = [ 'True' | 'False' | 'Unknown', string ]
function getAlarmStatus(alarms: Alarm[] | undefined): string {
@@ -278,7 +275,7 @@ async function StackInfos(props: StackInfosProps): Promise<JSX.Element> {
<Hfill />
<IconButton
icon='CROSS'
- className='eva-probeinfo-button'
+ className='eva-button'
onClick={close}
/>
</div>
@@ -289,83 +286,6 @@ async function StackInfos(props: StackInfosProps): Promise<JSX.Element> {
-/* -------------------------------------------------------------------------- */
-/* --- Selected Probe Component --- */
-/* -------------------------------------------------------------------------- */
-/* --- Display informations on the currently selected probe, along with --- */
-/* --- buttons to pin, remove and change the displayed columns, i.e. if --- */
-/* --- we display the values before and/or after the statement. --- */
-/* -------------------------------------------------------------------------- */
-
-interface ProbeInfosProps {
- probe?: Probe;
- status?: MarkerStatus;
- removeProbe: (probe: Probe) => void;
- setLocPin: (loc: Location, pin: boolean) => void;
- state: StateToDisplay;
- setState: (state: StateToDisplay) => void;
-}
-
-function SelectedProbeInfos(props: ProbeInfosProps): JSX.Element {
- const { probe, status, setLocPin, removeProbe, state, setState } = props;
- const code = probe?.code;
- const stmt = probe?.stmt;
- const target = probe?.target;
- const visible = code !== undefined;
- const pinned = status ? isPinnedMarker(status) : false;
- return (
- <Hpack className="eva-probeinfo">
- <div
- className="eva-probeinfo-code"
- style={{ visibility: visible ? 'visible' : 'hidden' }}
- >
- <div className='eva-probeinfo-code-text dome-text-cell'>{code}</div>
- </div>
- <Code><Stmt stmt={stmt} marker={target} /></Code>
- <IconButton
- icon='PIN'
- className="eva-probeinfo-button"
- title='Pin the probe'
- selected={pinned}
- visible={visible}
- onClick={() => { if (probe) setLocPin(probe, !pinned); }}
- />
- <IconButton
- icon="CIRC.CLOSE"
- className="eva-probeinfo-button"
- title="Discard the probe"
- onClick={() => { if (probe) removeProbe(probe); }}
- visible={visible}
- />
- <Filler />
- <ButtonGroup className='eva-probeinfo-state'>
- <Button
- value='Before'
- selected={state.before}
- title='Show values before statement effects'
- visible={visible}
- onClick={() => setState({before: !state.before, after: state.after})}
- >
- <ControlPoint kind={'before'}/>
- </Button>
- <Button
- value='After'
- selected={state.after}
- title='Show values after statement effects'
- visible={visible}
- onClick={() => setState({before: state.before, after: !state.after})}
- >
- <ControlPoint kind={'after'}/>
- </Button>
- </ButtonGroup>
- </Hpack>
- );
-}
-
-/* -------------------------------------------------------------------------- */
-
-
-
/* -------------------------------------------------------------------------- */
/* --- Probe Header Component --- */
/* -------------------------------------------------------------------------- */
@@ -376,7 +296,6 @@ function SelectedProbeInfos(props: ProbeInfosProps): JSX.Element {
interface ProbeHeaderProps {
probe: Probe;
status: MarkerStatus;
- state: StateToDisplay;
pinProbe: (pin: boolean) => void;
selectProbe: () => void;
removeProbe: () => void;
@@ -385,30 +304,27 @@ interface ProbeHeaderProps {
}
function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
- const { probe, status, state, setSelection, locEvt } = props;
+ 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 { before, after } = state;
-
- // Computing the number of columns..
- let span = 0;
- if ((before || after) && !probe.effects && !probe.condition) span += 2;
- if (before && (probe.effects || probe.condition)) span += 2;
- if (after && probe.effects) span += 2;
- if (after && probe.condition) span += 4;
- if (span === 0) return <></>;
+ const span = 2 + (probe.effects ? 2 : 0) + (probe.condition ? 4 : 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(!isPinnedMarker(status));
+ 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);
@@ -425,6 +341,21 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
>
<span className='dome-text-cell'>{code}</span>
<Stmt stmt={stmt} marker={target} short={true}/>
+ <div className='eva-header-buttons-container'>
+ <IconButton
+ icon='PIN'
+ className={buttonClass}
+ title={`${pinText} the probe`}
+ selected={isPinned}
+ onClick={onDoubleClick}
+ />
+ <IconButton
+ icon="CIRC.CLOSE"
+ className={buttonClass}
+ title="Discard the probe"
+ onClick={() => removeProbe()}
+ />
+ </div>
</th>
);
}
@@ -442,12 +373,10 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
interface ProbeDescrProps {
probe: Probe;
- state: StateToDisplay;
}
function ProbeDescr(props: ProbeDescrProps): JSX.Element[] {
- const { probe, state } = props;
- const { before, after } = state;
+ 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);
@@ -457,13 +386,13 @@ function ProbeDescr(props: ProbeDescrProps): JSX.Element[] {
function push(title: string, children: JSX.Element | string): void {
elements.push(<td {...infos} title={title}>{children}</td>);
}
- if ((before || after) && !probe.effects && !probe.condition)
+ if (!probe.effects && !probe.condition)
push('Values at the statement', '-');
- if (before && (probe.effects || probe.condition))
+ if (probe.effects || probe.condition)
push(title('before'), 'Before');
- if (after && probe.effects)
+ if (probe.effects)
push(title('after'), 'After');
- if (after && probe.condition) {
+ if (probe.condition) {
const pushCondition = (s: string): void => {
const t = `Values after the condition, in the ${s.toLowerCase()} branch`;
const child =
@@ -497,15 +426,13 @@ interface ProbeValuesProps {
probe: Probe;
summary: Evaluation;
status: MarkerStatus;
- state: StateToDisplay;
addLoc: (loc: Location) => void;
isSelectedCallstack: (c: callstack) => boolean;
summaryOnly: boolean;
}
function ProbeValues(props: ProbeValuesProps): Request<callstack, JSX.Element> {
- const { probe, summary, state, addLoc, summaryOnly } = props;
- const { before, after } = state;
+ const { probe, summary, addLoc, summaryOnly } = props;
const summaryStatus = getAlarmStatus(summary.vBefore?.alarms);
// Building common parts
@@ -557,16 +484,16 @@ function ProbeValues(props: ProbeValuesProps): Request<callstack, JSX.Element> {
);
}
const elements: JSX.Element[] = [];
- if (before && after && probe.effects && _.isEqual(vBefore, vAfter))
+ if (probe.effects && _.isEqual(vBefore, vAfter))
elements.push(td(vBefore, 3));
else {
- if ((before || after) && !probe.effects && !probe.condition)
+ if (!probe.effects && !probe.condition)
elements.push(td(vBefore));
- if (before && (probe.effects || probe.condition))
+ if (probe.effects || probe.condition)
elements.push(td(vBefore));
- if (after && probe.effects)
+ if (probe.effects)
elements.push(td(vAfter));
- if (after && probe.condition)
+ if (probe.condition)
elements.push(td(vThen), td(vElse));
}
return <>{React.Children.toArray(elements)}</>;
@@ -626,7 +553,6 @@ async function CallsiteCell(props: CallsiteCellProps): Promise<JSX.Element> {
interface FunctionProps {
fct: string;
markers: Map<Ast.marker, MarkerStatus>;
- state: StateToDisplay;
close: () => void;
getProbe: Request<Location, Probe>;
pinProbe: (probe: Probe, pin: boolean) => void;
@@ -650,13 +576,12 @@ interface FunctionProps {
const PageSize = 99;
async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
- const { fct, state, folded, isSelectedCallstack, locEvt } = props;
+ 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 { before, after } = state;
- const displayTable = folded || !(before || after) ? 'none' : 'block';
+ 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);
@@ -686,14 +611,14 @@ async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
const selectProbe = (): void => props.selectProbe(d.probe);
const removeProbe = (): void => props.removeProbe(d.probe);
const fcts = { selectProbe, pinProbe, removeProbe, setSelection };
- return ProbeHeader({ ...d, state, ...fcts, locEvt });
+ return ProbeHeader({ ...d, ...fcts, locEvt });
}));
/* Computes the columns descriptions */
- const descrs = data.map((d) => ProbeDescr({ ...d, state })).flat();
+ const descrs = data.map((d) => ProbeDescr(d)).flat();
/* Computes the summary values */
- const miscs = { state, addLoc, isSelectedCallstack, summaryOnly };
+ const miscs = { addLoc, isSelectedCallstack, summaryOnly };
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 });
@@ -748,7 +673,7 @@ async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
</div>
<IconButton
icon="ITEMS.LIST"
- className="eva-probeinfo-button"
+ className="eva-button"
selected={byCallstacks}
disabled={summaryOnly}
title="Details by callstack"
@@ -757,7 +682,7 @@ async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
<Inset />
<IconButton
icon="CROSS"
- className="eva-probeinfo-button"
+ className="eva-button"
title="Close"
onClick={close}
/>
@@ -965,7 +890,6 @@ function EvaTable(): JSX.Element {
/* Component state */
const [ selection, select ] = States.useSelection();
- const [ state, setState ] = React.useState<StateToDisplay>(defaultState);
const [ cs, setCS ] = React.useState<callstack>('Summary');
const [ fcts ] = React.useState(new FunctionsManager());
const [ focus, setFocus ] = React.useState<Probe | undefined>(undefined);
@@ -1054,7 +978,6 @@ function EvaTable(): JSX.Element {
return {
fct,
markers: infos.markers(focus),
- state,
close: () => { fcts.delete(fct); setTic(tac + 1); },
pinProbe: setLocPin,
getProbe,
@@ -1078,7 +1001,7 @@ function EvaTable(): JSX.Element {
return Promise.all(ps.map(FunctionSection));
},
[ cs, fcts, focus, tac, getCallsites, setLocPin,
- getCallstacks, getProbe, remove, select, state, locEvt ]);
+ getCallstacks, getProbe, remove, select, locEvt ]);
const { result: functions } = Dome.usePromise(functionsPromise);
/* Builds the alarms component. As for the function sections, it is an
@@ -1102,14 +1025,6 @@ function EvaTable(): JSX.Element {
return (
<>
<Ivette.TitleBar />
- <SelectedProbeInfos
- probe={focus}
- status={fcts.status(focus)}
- setLocPin={setLocPin}
- removeProbe={remove}
- state={state}
- setState={setState}
- />
<div className='eva-functions-section'>
{React.Children.toArray(functions)}
</div>
--
GitLab