diff --git a/ivette/.eslintrc.js b/ivette/.eslintrc.js
index b2580f8d832220299877a3d52e9e4a436e1f22f0..932e81f20ab965d17d4c95ec35da3ecf251dc3c1 100644
--- a/ivette/.eslintrc.js
+++ b/ivette/.eslintrc.js
@@ -39,8 +39,6 @@ module.exports = {
"lines-between-class-members": [
"error", "always", { "exceptAfterSingleLine": true }
],
- // Force curly brackets on newline if some item is
- "object-curly-newline": ["error", { "multiline": true }],
// Allow infinite loops but still disallow constant if-then-else
"no-constant-condition": ["error", { "checkLoops": false }],
// Prefer const including when destructuring when _all_ destructured values
diff --git a/ivette/CONTRIBUTING.md b/ivette/CONTRIBUTING.md
index d17eec67bd6ea0411c6e5ad9aeb18549787ca98b..ebdfaf6fc1be8890abe50e806fcbfb7a17ddb3a9 100644
--- a/ivette/CONTRIBUTING.md
+++ b/ivette/CONTRIBUTING.md
@@ -129,8 +129,6 @@ console.log('test');
- [lines-between-class-members](https://eslint.org/docs/rules/lines-between-class-members).
Forces empty lines between class members, except for single line declarations
(e.g. properties).
-- [object-curly-newline](https://eslint.org/docs/rules/object-curly-newline).
- Unify curly braces positions.
- [no-constant-condition](https://eslint.org/docs/rules/no-constant-condition).
Forbids constant conditions which are often used during the debug process but
should not remain in release versions. While recommended in Eslint, this
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 2069f6803d7b9388a82d6fcedc3a8cc064e74134..bb18e11256fea20bf8f980a27aff1d93f8a78984 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -124,12 +124,12 @@ function MarkButton(props: MarkButtonProps): JSX.Element {
// --------------------------------------------------------------------------
interface InfoSectionProps {
- fct: string | undefined;
scroll: React.RefObject<HTMLDivElement> | undefined;
- marker: AST.marker;
- scrolled: AST.marker | undefined;
- selected: AST.marker | undefined;
- hovered: AST.marker | undefined;
+ current: AST.decl | undefined; // current selection
+ marker: AST.marker; // of the info-section
+ scrolled: AST.marker | undefined; // among info-sections
+ selected: AST.marker | undefined; // in current selection
+ hovered: AST.marker | undefined; // in current selection
marked: boolean;
excluded: string[];
setPinned: (m: AST.marker) => void;
@@ -137,10 +137,10 @@ interface InfoSectionProps {
}
function MarkInfos(props: InfoSectionProps): JSX.Element {
- const { marker, fct, scrolled, selected, hovered, excluded } = props;
- const attrs = States.useMarker(marker);
- const scope = attrs.scope ?? fct;
- const foreign = !!scope && fct !== scope;
+ const { current, marker, scrolled, selected, hovered, excluded } = props;
+ const { decl, labelKind, titleKind, name, descr } = States.useMarker(marker);
+ const { label } = States.useDeclaration(decl);
+ const foreign = !!current && !!decl && current !== decl;
const [unfold, setUnfold] = React.useState(true);
const [expand, setExpand] = React.useState(false);
const req = React.useMemo(() =>
@@ -153,7 +153,6 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
isSelected && 'selected',
isHovered && 'hovered',
);
- const { labelKind, titleKind, name, descr } = attrs;
const filtered = markerFields.filter((fd) => !excluded.includes(fd.id));
const hasMore = filtered.length < markerFields.length;
const displayed = expand ? markerFields : filtered;
@@ -161,34 +160,30 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
evt.stopPropagation();
setUnfold(!unfold);
};
- const onChildSelected = (m: AST.marker, meta: Modifier): void => {
+ const onChildSelected = (m: AST.marker, modifier: Modifier): void => {
props.setPinned(marker);
- switch (meta) {
+ switch (modifier) {
case 'NORMAL':
- States.setSelection({ fct, marker: m });
+ States.gotoLocalMarker(m);
break;
case 'META':
- States.setSelection({ fct, marker: m }, m !== marker);
+ States.gotoLocalMarker(m, m !== marker);
break;
case 'DOUBLE':
- States.setSelection({ fct: scope, marker: m });
+ States.gotoGlobalMarker(m);
break;
}
};
const onChildHovered = (m: AST.marker | undefined): void => {
- if (m) {
- States.setHovered({ fct, marker: m });
- } else {
- States.setHovered({ fct, marker });
- }
+ States.setHovered(m || marker);
};
return (
<div
ref={isScrolled ? props.scroll : undefined}
className={`astinfo-section ${highlight}`}
- onMouseEnter={() => States.setHovered({ fct, marker })}
+ onMouseEnter={() => States.setHovered(marker)}
onMouseLeave={() => States.setHovered(undefined)}
- onClick={() => onChildSelected(marker, foreign ? 'DOUBLE' : 'NORMAL')}
+ onClick={() => onChildSelected(marker, 'NORMAL')}
onDoubleClick={() => onChildSelected(marker, 'DOUBLE')}
>
<div
@@ -210,9 +205,7 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
{labelKind}
</span> {name}
</Code>
- <Code key="SCOPE" className="" display={foreign}>
- [in: {scope}]
- </Code>
+ <Code key="SCOPE" className="" display={foreign}>[in {label}]</Code>
<MarkButton
key="MORE"
icon="CIRC.PLUS"
@@ -280,8 +273,8 @@ export default function ASTinfo(): JSX.Element {
// Selection Hooks
const [markers, setMarkers] = React.useState<AST.marker[]>([]);
const [setting, setSetting] = Dome.useStringSettings(filterSettings, '');
- const [selection] = States.useSelection();
- const [hovering] = States.useHovered();
+ const { decl: current, marker: selected } = States.useCurrent();
+ const hovered = States.useHovered();
const allFields = States.useRequest(AST.getInformation, null) ?? [];
const excluded = React.useMemo(() => makeFilter(setting), [setting]);
Dome.useEvent(States.MetaSelection, (loc: States.Location) => {
@@ -295,9 +288,6 @@ export default function ASTinfo(): JSX.Element {
scrollDiv?.scrollIntoView({ block: 'nearest' });
}, [scrollDiv]);
// Derived
- const fct = selection?.current?.fct;
- const selected = selection?.current?.marker;
- const hovered = hovering?.marker;
const allMarkers = addMarker(addMarker(markers, selected), hovered);
const scrolled = inside ? selected : (hovered || selected);
// Callbacks
@@ -312,7 +302,7 @@ export default function ASTinfo(): JSX.Element {
return (
<MarkInfos
key={marker}
- fct={fct}
+ current={current}
scroll={scroll}
marker={marker}
scrolled={scrolled}
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 35a124c9ea372b193fc00bb233abbbce9d303283..f29202829458fbab9e5982784d89c7fc1e41b266 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -28,7 +28,6 @@ import * as Editor from 'dome/text/editor';
import * as Utils from 'dome/data/arrays';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
-import { key } from 'dome/data/json';
import * as Settings from 'dome/data/settings';
import { IconButton } from 'dome/controls/buttons';
import { Filler, Inset } from 'dome/frame/toolbars';
@@ -36,6 +35,7 @@ import * as Ast from 'frama-c/kernel/api/ast';
import { text } from 'frama-c/kernel/api/data';
import * as Eva from 'frama-c/plugins/eva/api/general';
import * as Properties from 'frama-c/kernel/api/properties';
+import * as Locations from './Locations';
import { getWritesLval, getReadsLval } from 'frama-c/plugins/studia/api/studia';
import { TitleBar } from 'ivette';
@@ -49,10 +49,9 @@ import * as Preferences from 'ivette/prefs';
// An alias type for functions and locations.
type Fct = string | undefined;
+type Decl = Ast.decl | undefined;
type Marker = Ast.marker | undefined;
-const noMarker = Ast.jMarker('');
-
// A range is just a pair of position in the code.
type Range = Editor.Range;
@@ -176,7 +175,7 @@ const Ranges = Editor.createAspect({ t: Tree }, ({ t }) => markersRanges(t));
// -----------------------------------------------------------------------------
// This field contains the currently selected function.
-const Fct = Editor.createField<Fct>(undefined);
+const Decl = Editor.createField<Decl>(undefined);
// This field contains the currently selected marker.
const Marker = Editor.createField<Marker>(undefined);
@@ -184,11 +183,6 @@ const Marker = Editor.createField<Marker>(undefined);
// This field contains the current multiple selection.
const Multiple = Editor.createField<Marker[]>([]);
-// The Ivette selection must be updated by CodeMirror plugins. This input
-// add the callback in the CodeMirror internal state.
-type UpdateSelection = (a: States.SelectionActions) => void;
-const UpdateSelection = Editor.createField<UpdateSelection>(() => { return; });
-
// The marker field is considered as the ground truth on what is selected in the
// CodeMirror document. To do so, we catch the mouseup event (so when the user
// select a new part of the document) and update the Ivette selection
@@ -196,14 +190,12 @@ const UpdateSelection = Editor.createField<UpdateSelection>(() => { return; });
// component's render and thus update everything else.
const MarkerUpdater = createMarkerUpdater();
function createMarkerUpdater(): Editor.Extension {
- const deps = { fct: Fct, tree: Tree, update: UpdateSelection };
+ const deps = { decl: Decl, tree: Tree };
return Editor.createEventHandler(deps, {
- mouseup: ({ fct, tree, update }, view, event) => {
+ mouseup: ({ decl, tree }, view, event) => {
const main = view.state.selection.main;
const marker = coveringNode(tree, main.from)?.marker;
- const location = { fct, marker };
- update({ location });
- if (event.altKey) States.MetaSelection.emit(location);
+ States.setCurrent({ decl, marker }, event.altKey);
}
});
}
@@ -235,39 +227,32 @@ function createMarkerScroller(): Editor.Extension {
// This field contains the currently hovered marker.
const Hovered = Editor.createField<Marker>(undefined);
-// The Ivette hovered element must be updated by CodeMirror plugins. This
-// field add the callback in the CodeMirror internal state.
-type UpdateHovered = (h: States.Hovered) => void;
-const UpdateHovered = Editor.createField<UpdateHovered>(() => { return; });
-
// The Hovered field is updated each time the mouse moves through the CodeMirror
// document. The handlers updates the Ivette hovered information, which is then
// reflected on the Hovered field by the Editor component itself.
const HoveredUpdater = createHoveredUpdater();
function createHoveredUpdater(): Editor.Extension {
- const deps = { fct: Fct, tree: Tree, update: UpdateHovered };
+ const deps = { tree: Tree };
return Editor.createEventHandler(deps, {
mousemove: (inputs, view, event) => {
- const { fct, tree, update: updateHovered } = inputs;
+ const { tree } = inputs;
const coords = { x: event.clientX, y: event.clientY };
- const reset = (): void => updateHovered(undefined);
const pos = view.posAtCoords(coords);
- if (!pos) { reset(); return; }
- const hov = coveringNode(tree, pos);
- if (!hov) { reset(); return; }
- const from = view.coordsAtPos(hov.from);
- if (!from) { reset(); return; }
- const to = view.coordsAtPos(hov.to);
- if (!to) { reset(); return; }
+ if (!pos) { States.setHovered(); return; }
+ const node = coveringNode(tree, pos);
+ if (!node) { States.setHovered(); return; }
+ const from = view.coordsAtPos(node.from);
+ if (!from) { States.setHovered(); return; }
+ const to = view.coordsAtPos(node.to);
+ if (!to) { States.setHovered(); return; }
const left = Math.min(from.left, to.left);
const right = Math.max(from.left, to.left);
const top = Math.min(from.top, to.top);
const bottom = Math.max(from.bottom, to.bottom);
const horizontallyOk = left <= coords.x && coords.x <= right;
const verticallyOk = top <= coords.y && coords.y <= bottom;
- if (!horizontallyOk || !verticallyOk) { reset(); return; }
- const marker = hov.marker;
- updateHovered(marker ? { fct, marker } : undefined);
+ if (!horizontallyOk || !verticallyOk) { States.setHovered(); return; }
+ States.setHovered(node.marker);
}
});
}
@@ -498,28 +483,21 @@ interface StudiaProps {
kind: access,
}
-interface StudiaInfos {
- name: string,
- title: string,
- locations: { fct: key<'#fct'>, marker: Ast.marker }[],
- index: number,
-}
-
-async function studia(props: StudiaProps): Promise<StudiaInfos> {
+async function invokeStudia(props: StudiaProps): Promise<void> {
const { marker, attrs, kind } = props;
const request = kind === 'Reads' ? getReadsLval : getWritesLval;
const data = await Server.send(request, marker);
- const locations = data.direct.map(([f, m]) => ({ fct: f, marker: m }));
+ const markers = data.direct.map(([_, marker]) => marker);
const lval = attrs.name;
- if (locations.length > 0) {
- const name = `${kind} of ${lval}`;
- const acc = (kind === 'Reads') ? 'accessing' : 'modifying';
- const title =
- `List of statements ${acc} the memory location pointed by ${lval}.`;
- return { name, title, locations, index: 0 };
- }
- const name = `No ${kind.toLowerCase()} of ${lval}`;
- return { name, title: '', locations: [], index: 0 };
+ let label;
+ if (markers.length > 0)
+ label = `${kind} of ${lval}`;
+ else
+ label = `No ${kind.toLowerCase()} of ${lval}`;
+ const acc = (kind === 'Reads') ? 'accessing' : 'modifying';
+ const title =
+ `List of statements ${acc} the memory location pointed by ${lval}.`;
+ Locations.setSelection({ label, title, markers });
}
// -----------------------------------------------------------------------------
@@ -543,11 +521,15 @@ const GetMarkerData = Editor.createField<GetMarkerData>(() => undefined);
const ContextMenuHandler = createContextMenuHandler();
function createContextMenuHandler(): Editor.Extension {
- const data = { tree: Tree, callers: Callers, callees: Callees };
- const deps = { ...data, update: UpdateSelection, getData: GetMarkerData };
+ const deps = {
+ tree: Tree,
+ callers: Callers,
+ callees: Callees,
+ getData: GetMarkerData,
+ };
return Editor.createEventHandler(deps, {
contextmenu: (inputs, view, event) => {
- const { tree, callers, callees, update, getData } = inputs;
+ const { tree, callers, callees, getData } = inputs;
const coords = { x: event.clientX, y: event.clientY };
const position = view.posAtCoords(coords); if (!position) return;
const node = coveringNode(tree, position);
@@ -556,29 +538,29 @@ function createContextMenuHandler(): Editor.Extension {
const attrs = getData(node.marker);
if (attrs?.isFunDecl) {
const groupedCallers = Lodash.groupBy(callers, (cs) => cs.kf);
- const locations =
- callers.map(({ kf, stmt }) => ({ fct: kf, marker: stmt }));
- Lodash.forEach(groupedCallers, (e) => {
- const callerName = e[0].kf;
- const callSites = e.length > 1 ? `(${e.length} call sites)` : '';
- items.push({
- label: `Go to caller ${callerName} ` + callSites,
- onClick: () => update({
- name: `Call sites of function ${attrs.name}`,
- locations: locations,
- index: locations.findIndex(l => l.fct === callerName)
- })
+ Lodash.forEach(groupedCallers, (group) => {
+ const n = group.length;
+ const site = group[0];
+ const call = `Go to caller ${site.kf}`;
+ const label = n > 1 ? `${call} (${n} call sites)` : call;
+ const markers = callers.map(cs => cs.stmt);
+ const index = callers.findIndex(cs => cs.kf === site.kf);
+ const title = `Call sites of function ${attrs.name}`;
+ const onClick = (): void => Locations.setSelection({
+ label, title, markers, index
});
+ items.push({ label, onClick });
});
} else if (attrs?.isFunction) {
- const location = { fct: attrs.name };
- const onClick = (): void => update({ location });
const label = `Go to definition of ${attrs.name}`;
+ // TODO: use declaration of pointed function (not available yet)
+ const onClick = (): void => States.gotoDeclaration(attrs.decl);
items.push({ label, onClick });
}
else if (attrs?.isFunctionPointer) {
Lodash.forEach(callees, (fct) => {
- const onClick = (): void => update({ location: { fct } });
+ // TODO: use declaration of pointed function (not available yet)
+ const onClick = (): void => States.gotoDeclaration(attrs.decl);
const label = `Go to definition of ${fct} (indirect)`;
items.push({ label, onClick });
});
@@ -586,7 +568,7 @@ function createContextMenuHandler(): Editor.Extension {
const enabled = attrs?.isLval;
const onClick = (kind: access): void => {
if (attrs && node.marker)
- studia({ marker: node.marker, attrs, kind }).then(update);
+ invokeStudia({ marker: node.marker, attrs, kind });
};
const reads = 'Studia: select reads';
const writes = 'Studia: select writes';
@@ -671,8 +653,8 @@ function createTaintTooltip(): Editor.Extension {
// -----------------------------------------------------------------------------
// Server request handler returning the given function's text.
-function useFctText(fct: Fct): text {
- return States.useRequest(Ast.printFunction, fct) ?? null;
+function useAST(decl: Ast.decl | undefined): text {
+ return States.useRequest(Ast.printDeclaration, decl) ?? [];
}
// Server request handler returning the given function's dead code information.
@@ -728,48 +710,44 @@ export default function ASTview(): JSX.Element {
const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
const { view, Component } = Editor.Editor(extensions);
- // Updating CodeMirror when the selection or its callback are changed.
- const [selection, setSel] = States.useSelection();
- React.useEffect(() => UpdateSelection.set(view, setSel), [view, setSel]);
- const fct = selection?.current?.fct;
- React.useEffect(() => Fct.set(view, fct), [view, fct]);
- const marker = selection?.current?.marker;
+ // Current selection
+ const { decl, marker } = States.useCurrent();
+ React.useEffect(() => Decl.set(view, decl), [view, decl]);
React.useEffect(() => Marker.set(view, marker), [view, marker]);
- const multiple = selection?.multiple.allSelections.map(l => l.marker);
- React.useEffect(() => Multiple.set(view, multiple), [view, multiple]);
-
- // Updating CodeMirror when the <updateHovered> callback is changed.
- const [hov, setHov] = States.useHovered();
- const hovered = hov?.marker ?? noMarker;
- React.useEffect(() => UpdateHovered.set(view, setHov), [view, setHov]);
+ const hovered = States.useHovered();
React.useEffect(() => Hovered.set(view, hovered), [view, hovered]);
- // Updating CodeMirror when the <properties> synchronized array is changed.
+ // Multiple selection
+ const { markers } = Locations.useSelection();
+ React.useEffect(() => Multiple.set(view, markers), [view, markers]);
+
+ // Property status
const props = States.useSyncArrayData(Properties.status);
React.useEffect(() => PropertiesStatuses.set(view, props), [view, props]);
- // Updating CodeMirror when the <propStatusTags> map is changed.
+ // Property tags
const tags = States.useTags(Properties.propStatusTags);
React.useEffect(() => Tags.set(view, tags), [view, tags]);
- // Updating CodeMirror when the <markersInfo> synchronized array is changed.
+ // Marker attributes
const getData = States.useSyncArrayGetter(Ast.markerAttributes);
React.useEffect(() => GetMarkerData.set(view, getData), [view, getData]);
- // Retrieving data on currently selected function and updating CodeMirror when
- // they have changed.
- const text = useFctText(fct);
+ // Printed AST
+ const text = useAST(decl);
React.useEffect(() => Text.set(view, text), [view, text]);
+
+ // EVA Callbacks
+ const { kind, name } = States.useDeclaration(decl);
+ const fct = kind==='FUNCTION' ? name : undefined;
const dead = useFctDead(fct);
React.useEffect(() => Dead.set(view, dead), [view, dead]);
const callers = useFctCallers(fct);
React.useEffect(() => Callers.set(view, callers), [view, callers]);
- const taints = useFctTaints(fct);
- React.useEffect(() => TaintedLvalues.set(view, taints), [view, taints]);
-
- // Retrieving data on currently hovered marker.
const callees = useCallees(hovered);
React.useEffect(() => Callees.set(view, callees), [view, callees]);
+ const taints = useFctTaints(fct);
+ React.useEffect(() => TaintedLvalues.set(view, taints), [view, taints]);
return (
<>
diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx
index 827957171c9f59670571422193e636da8544c890..bbfdb1fbc9a11cd0912ad80bc3b3f0843c6d9b7d 100644
--- a/ivette/src/frama-c/kernel/Globals.tsx
+++ b/ivette/src/frama-c/kernel/Globals.tsx
@@ -34,7 +34,7 @@ import { Button } from 'dome/controls/buttons';
import * as Toolbars from 'dome/frame/toolbars';
import * as States from 'frama-c/states';
-import * as Kernel from 'frama-c/kernel/api/ast';
+import * as Ast from 'frama-c/kernel/api/ast';
import { computationState } from 'frama-c/plugins/eva/api/general';
import * as Eva from 'frama-c/plugins/eva/api/general';
@@ -42,21 +42,17 @@ import * as Eva from 'frama-c/plugins/eva/api/general';
// --- Global Search Hints
// --------------------------------------------------------------------------
-function makeFunctionHint(fct: functionsData): Toolbars.Hint {
- return {
- id: fct.key,
- label: fct.name,
- title: fct.signature,
- value: () => States.setSelection({ fct: fct.name }),
- };
-}
-
async function lookupGlobals(pattern: string): Promise<Toolbars.Hint[]> {
const lookup = pattern.toLowerCase();
- const fcts = States.getSyncArray(Kernel.functions).getArray();
- return fcts.filter((fn) => (
- 0 <= fn.name.toLowerCase().indexOf(lookup)
- )).map(makeFunctionHint);
+ const globals = States.getSyncArray(Ast.declAttributes).getArray();
+ return globals.filter((g) => (
+ 0 <= g.name.toLowerCase().indexOf(lookup)
+ )).map((g : Ast.declAttributesData) => ({
+ id: g.decl,
+ label: g.name,
+ title: g.label,
+ value: () => States.gotoDeclaration(g.decl)
+ }));
}
Toolbars.registerSearchHints('frama-c.globals', lookupGlobals);
@@ -68,11 +64,10 @@ Toolbars.registerSearchHints('frama-c.globals', lookupGlobals);
interface FctItemProps {
fct: functionsData;
current: string | undefined;
- onSelection: (name: string) => void;
}
function FctItem(props: FctItemProps): JSX.Element {
- const { name, signature, main, stdlib, builtin, defined } = props.fct;
+ const { name, signature, main, stdlib, builtin, defined, decl } = props.fct;
const className = classes(
main && 'globals-main',
(stdlib || builtin) && 'globals-stdlib',
@@ -87,7 +82,7 @@ function FctItem(props: FctItemProps): JSX.Element {
label={name}
title={signature}
selected={name === props.current}
- onSelection={() => props.onSelection(name)}
+ onSelection={() => States.gotoDeclaration(decl)}
>
{attributes && <span className="globals-attr">{attributes}</span>}
</Item>
@@ -99,12 +94,12 @@ function FctItem(props: FctItemProps): JSX.Element {
// --------------------------------------------------------------------------
type functionsData =
- Kernel.functionsData | (Kernel.functionsData & Eva.functionsData);
+ Ast.functionsData | (Ast.functionsData & Eva.functionsData);
type FctKey = Json.key<'#functions'>;
function computeFcts(
- ker: States.ArrayProxy<FctKey, Kernel.functionsData>,
+ ker: States.ArrayProxy<FctKey, Ast.functionsData>,
eva: States.ArrayProxy<FctKey, Eva.functionsData>,
): functionsData[] {
const arr: functionsData[] = [];
@@ -118,8 +113,9 @@ function computeFcts(
export default function Globals(): JSX.Element {
// Hooks
- const [selection, updateSelection] = States.useSelection();
- const ker = States.useSyncArrayProxy(Kernel.functions);
+ const { decl } = States.useCurrent();
+ const { kind, name } = States.useDeclaration(decl);
+ const ker = States.useSyncArrayProxy(Ast.functions);
const eva = States.useSyncArrayProxy(Eva.functions);
const fcts = React.useMemo(() => computeFcts(ker, eva), [ker, eva]);
const { useFlipSettings } = Dome;
@@ -139,20 +135,10 @@ export default function Globals(): JSX.Element {
useFlipSettings('ivette.globals.eva-analyzed', true);
const [evaUnreached, flipEvaUnreached] =
useFlipSettings('ivette.globals.eva-unreached', true);
- const [selected, flipSelected] =
- useFlipSettings('ivette.globals.selected', false);
- const multipleSelection = selection?.multiple;
- const multipleSelectionActive = multipleSelection?.allSelections.length > 0;
const evaComputed = States.useSyncValue(computationState) === 'computed';
- function isSelected(fct: functionsData): boolean {
- return multipleSelection?.allSelections.some(
- (l) => fct.name === l?.fct,
- );
- }
-
// Currently selected function.
- const current: undefined | string = selection?.current?.fct;
+ const current = (decl && kind === 'FUNCTION') ? name : undefined;
function showFunction(fct: functionsData): boolean {
const visible =
@@ -165,15 +151,10 @@ export default function Globals(): JSX.Element {
&& (evaAnalyzed || !evaComputed ||
!('eva_analyzed' in fct && fct.eva_analyzed === true))
&& (evaUnreached || !evaComputed ||
- ('eva_analyzed' in fct && fct.eva_analyzed === true))
- && (!selected || !multipleSelectionActive || isSelected(fct));
+ ('eva_analyzed' in fct && fct.eva_analyzed === true));
return !!visible;
}
- function onSelection(name: string): void {
- updateSelection({ location: { fct: name } });
- }
-
async function onContextMenu(): Promise<void> {
const items: Dome.PopupMenuItem[] = [
{
@@ -221,13 +202,6 @@ export default function Globals(): JSX.Element {
checked: evaUnreached,
onClick: flipEvaUnreached,
},
- 'separator',
- {
- label: 'Selected only',
- enabled: multipleSelectionActive,
- checked: selected,
- onClick: flipSelected,
- },
];
Dome.popupMenu(items);
}
@@ -248,10 +222,9 @@ export default function Globals(): JSX.Element {
const filteredFunctions =
filtered.map((fct) => (
<FctItem
- key={fct.name}
+ key={fct.key}
fct={fct}
current={current}
- onSelection={onSelection}
/>
));
diff --git a/ivette/src/frama-c/kernel/History.tsx b/ivette/src/frama-c/kernel/History.tsx
index 90f3fe717957615cc0876d0411cb4872614011f4..a6a350d8e63cc87a3aca24943b4d28bd4eeca610 100644
--- a/ivette/src/frama-c/kernel/History.tsx
+++ b/ivette/src/frama-c/kernel/History.tsx
@@ -29,23 +29,19 @@ import * as Toolbar from 'dome/frame/toolbars';
import * as States from 'frama-c/states';
export default function History(): JSX.Element {
- const [selection, updateSelection] = States.useSelection();
-
- const doPrevSelect = () => void updateSelection('HISTORY_PREV');
- const doNextSelect = () => void updateSelection('HISTORY_NEXT');
-
+ const selection = States.useSelection();
return (
<Toolbar.ButtonGroup>
<Toolbar.Button
icon="ANGLE.LEFT"
- onClick={doPrevSelect}
- disabled={!selection || selection.history.prevSelections.length === 0}
+ onClick={States.gotoNext}
+ enabled={selection.next.length > 0}
title="Previous location"
/>
<Toolbar.Button
icon="ANGLE.RIGHT"
- onClick={doNextSelect}
- disabled={!selection || selection.history.nextSelections.length === 0}
+ onClick={States.gotoPrev}
+ enabled={selection.prev.length > 0}
title="Next location"
/>
</Toolbar.ButtonGroup>
diff --git a/ivette/src/frama-c/kernel/Locations.tsx b/ivette/src/frama-c/kernel/Locations.tsx
index 63f6d068369d70fbf8e8966e9a2c1c32f33f1fa5..60e9802e662c7942aef2f846fb78addcac8c83e1 100644
--- a/ivette/src/frama-c/kernel/Locations.tsx
+++ b/ivette/src/frama-c/kernel/Locations.tsx
@@ -25,132 +25,161 @@
// --------------------------------------------------------------------------
import React from 'react';
+import { GlobalState, useGlobalState } from 'dome/data/states';
import * as States from 'frama-c/states';
import { CompactModel } from 'dome/table/arrays';
-import { Table, Column, Renderer } from 'dome/table/views';
+import { Table, Column } from 'dome/table/views';
import { Label } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
import { Space } from 'dome/frame/toolbars';
import { TitleBar } from 'ivette';
-import { marker, jMarker } from 'frama-c/kernel/api/ast';
+import * as Ast from 'frama-c/kernel/api/ast';
+
+// --------------------------------------------------------------------------
+// --- Global Multi-Selection
+// --------------------------------------------------------------------------
+
+export interface MultiSelection {
+ label: string;
+ title: string;
+ markers: Ast.marker[];
+ index?: number;
+}
+
+export interface MultiSelectionState {
+ label: string;
+ title: string;
+ markers: Ast.marker[];
+ index: number;
+}
+
+const emptySelection = { label: '', title: '', markers: [], index: 0 };
+const MultiSelection = new GlobalState<MultiSelectionState>(emptySelection);
+
+export function useSelection(): MultiSelectionState {
+ const [s] = useGlobalState(MultiSelection);
+ return s;
+}
+
+export function setSelection(s: MultiSelection): void
+{
+ const { index=0, ...data } = s;
+ MultiSelection.setValue({ ...data, index });
+ States.gotoGlobalMarker(data.markers[index]);
+}
+
+export function setIndex(index: number): void {
+ const s = MultiSelection.getValue();
+ setSelection({ ...s, index });
+}
+
+/**
+ Update the list of markers and select its first element,
+ or cycle to the next element wrt current selection.
+ */
+export function setNextSelection(locs: Ast.marker[]): void {
+ const selection = MultiSelection.getValue();
+ const { markers, index } = selection;
+ if (markers === locs) {
+ const target = index+1;
+ const select = target < locs.length ? target : 0;
+ setSelection({ ...selection, index: select });
+ } else {
+ setSelection({ ...selection, markers: locs, index: 0 });
+ }
+}
+
+export function clear(): void {
+ MultiSelection.setValue(emptySelection);
+}
+
+function gotoIndex(index: number): void {
+ const selection = MultiSelection.getValue();
+ if (0 <= index && index <= selection.markers.length)
+ MultiSelection.setValue({ ...selection, index });
+}
// --------------------------------------------------------------------------
// --- Locations Panel
// --------------------------------------------------------------------------
-type LocationId = States.Location & { id: number };
+interface Data {
+ index: number,
+ marker: Ast.marker,
+}
-function SourceLoc(props: { marker: marker }): JSX.Element {
- const { sloc, descr } = States.useMarker(props.marker);
- const position = `${sloc?.base}:${sloc?.line}`;
- return <Label label={position} title={descr} />;
+class Model extends CompactModel<Ast.marker, Data> {
+ constructor() { super(({ marker }) => marker); }
}
+const getIndex = (d : Data): number => d.index + 1;
+
export default function LocationsTable(): JSX.Element {
// Hooks
- const [selection, updateSelection] = States.useSelection();
- const model = React.useMemo(() => (
- new CompactModel<number, LocationId>(({ id }: LocationId) => id)
- ), []);
- const multipleSelections = selection?.multiple;
- const numberOfSelections = multipleSelections?.allSelections?.length;
-
- // Renderer for statement markers.
- const renderMarker: Renderer<string> = (loc: string) => (
- <SourceLoc marker={jMarker(loc)} />
- );
-
- // Updates [[model]] with the current multiple selections.
+ const model = React.useMemo(() => new Model(), []);
+ const getDecl = States.useSyncArrayGetter(Ast.declAttributes);
+ const getAttr = States.useSyncArrayGetter(Ast.markerAttributes);
+ const { label, title, markers, index } = useSelection();
React.useEffect(() => {
- if (numberOfSelections > 0) {
- const data: LocationId[] =
- multipleSelections.allSelections.map((d, i) => ({ ...d, id: i }));
- model.replaceAllDataWith(data);
- } else
- model.clear();
- }, [numberOfSelections, multipleSelections, model]);
-
- // Callbacks
- const onTableSelection = React.useCallback(
- ({ id }) => updateSelection({ index: id }),
- [updateSelection],
- );
+ model.replaceAllDataWith(
+ markers.map((marker, index): Data => ({ index, marker }))
+ );
+ }, [model, markers]);
+ const selected = markers[index];
+ const size = markers.length;
- const reload = (): void => {
- const location = multipleSelections.allSelections[multipleSelections.index];
- updateSelection({ location });
- };
+ const indexLabel = `${index+1} / ${size}`;
+
+ const getLocation = React.useCallback((d: Data): string => {
+ const attr = getAttr(d.marker);
+ if (!attr) return '';
+ const decl = getDecl(attr.decl);
+ if (!decl) return '';
+ return `${decl.label} ${attr.descr}`;
+ }, [getDecl, getAttr]);
// Component
return (
<>
<TitleBar>
<IconButton
- icon="RELOAD"
- onClick={reload}
- enabled={numberOfSelections > 0}
- title="Reload the current location"
- />
- <IconButton
- icon="ANGLE.LEFT"
- onClick={() => updateSelection('MULTIPLE_PREV')}
- enabled={numberOfSelections > 1 && multipleSelections?.index > 0}
- title="Previous location"
+ icon='ANGLE.LEFT'
+ title='Previous location'
+ enabled={0 < index}
+ onClick={() => gotoIndex(index-1)}
/>
<IconButton
- icon="ANGLE.RIGHT"
- onClick={() => updateSelection('MULTIPLE_NEXT')}
- enabled={
- numberOfSelections > 1 &&
- multipleSelections?.index < numberOfSelections - 1
- }
- title="Next location"
+ icon='ANGLE.RIGHT'
+ title='Next location'
+ enabled={index + 1 < size}
+ onClick={() => gotoIndex(index+1)}
/>
<Space />
<Label
- className="component-info"
- title={
- `${numberOfSelections} selected ` +
- `location${numberOfSelections > 1 ? 's' : ''}`
- }
- >
- {multipleSelections?.allSelections.length === 0 ?
- '0 / 0' :
- `${multipleSelections?.index + 1} / ${numberOfSelections}`}
- </Label>
+ className='component-info'
+ display={0 <= index && index < size}
+ label={indexLabel}
+ title='Current location index / Number of locations' />
<Space />
<IconButton
- icon="TRASH"
- onClick={() => updateSelection('MULTIPLE_CLEAR')}
- enabled={numberOfSelections > 0}
- title={`Clear location${numberOfSelections > 1 ? 's' : ''}`}
+ icon='TRASH'
/>
</TitleBar>
- <Label
- label={multipleSelections?.name}
- title={multipleSelections?.title}
- style={{ textAlign: 'center' }}
- />
- <Table
+ <Label label={label} title={title} style={{ textAlign: 'center' }} />
+ <Table<Ast.marker, Data>
model={model}
- selection={multipleSelections?.index}
- onSelection={onTableSelection}
+ selection={selected}
+ onSelection={(_marker, _data, index) => gotoIndex(index)}
>
<Column
- id="id"
- label="#"
- align="center"
- width={25}
- getter={(r: { id: number }) => r.id + 1}
+ id='index' label='#' align='center' width={25}
+ getter={getIndex}
/>
- <Column id="fct" label="Function" width={120} />
<Column
- id="marker"
- label="Statement"
- fill
- render={renderMarker}
+ id='marker' label='Location' fill
+ getter={getLocation}
/>
</Table>
</>
diff --git a/ivette/src/frama-c/kernel/Messages.tsx b/ivette/src/frama-c/kernel/Messages.tsx
index d635b8fa23449d2a3661fc008177daf3b796ff1c..2d5e58380f9ede1697d86b3ec8909e3dfa2d3bb5 100644
--- a/ivette/src/frama-c/kernel/Messages.tsx
+++ b/ivette/src/frama-c/kernel/Messages.tsx
@@ -61,7 +61,7 @@ type EmitterFilter = {
};
interface Filter {
- currentFct: boolean;
+ currentDecl: boolean;
search: Search;
kind: KindFilter;
emitter: EmitterFilter;
@@ -107,7 +107,7 @@ const emitterFilter = {
};
const defaultFilter: Filter = {
- currentFct: false,
+ currentDecl: false,
search: {},
kind: kindFilter,
emitter: emitterFilter,
@@ -175,25 +175,27 @@ function filterSearched(search: Search, msg: Message): boolean {
searchCategory(search.category, msg.category));
}
-function filterFunction(
+function filterDecl(
filter: Filter,
- kf: string | undefined,
+ decl: Ast.decl | undefined,
msg: Message
): boolean {
- if (filter.currentFct)
- return (kf === msg.fct);
+ if (filter.currentDecl)
+ return (decl === msg.decl);
return true;
}
function filterMessage(
filter: Filter,
- kf: string | undefined,
+ decl: Ast.decl | undefined,
msg: Message
): boolean {
- return (filterFunction(filter, kf, msg) &&
+ return (
+ filterDecl(filter, decl, msg) &&
filterSearched(filter.search, msg) &&
filterKind(filter.kind, msg) &&
- filterEmitter(filter.emitter, msg));
+ filterEmitter(filter.emitter, msg)
+ );
}
// --------------------------------------------------------------------------
@@ -255,7 +257,7 @@ function MessageFilter(props: { filter: State<Filter> }): JSX.Element {
<Forms.CheckboxField
label="Current function"
title="Only show messages emitted at the current function"
- state={Forms.useProperty(state, 'currentFct')}
+ state={Forms.useProperty(state, 'currentDecl')}
/>
<Section label="Search">
<Forms.TextField
@@ -370,7 +372,7 @@ const MessageColumns = (): JSX.Element => (
render={renderMessage}
/>
<Column
- id="fct"
+ id="decl"
label="Function"
width={150}
render={renderCell}
@@ -412,7 +414,7 @@ const byMessage: Compare.ByFields<Message> = {
kind: Compare.structural,
plugin: Compare.string,
category: Compare.defined(Compare.string),
- fct: Compare.defined(Compare.alpha),
+ decl: Compare.defined(Compare.alpha),
source: Compare.defined(bySource),
};
@@ -437,29 +439,27 @@ export default function RenderMessages(): JSX.Element {
const filterState = useGlobalState(globalFilterState);
const [filter] = filterState;
- const [selection, updateSelection] = States.useSelection();
- const selectedFct = selection?.current?.fct;
+ const { decl: selectedDecl } = States.useCurrent();
const [selectedMsg, selectMsg] = React.useState<Message|undefined>(undefined);
const [text, setText] = React.useState('');
React.useEffect(() => {
- if (selectedFct !== selectedMsg?.fct)
+ if (selectedDecl !== selectedMsg?.decl)
selectMsg(undefined);
- }, [selectedFct, selectedMsg?.fct]);
+ }, [selectedDecl, selectedMsg?.decl]);
React.useEffect(() => {
- model.setFilter((msg: Message) => filterMessage(filter, selectedFct, msg));
- }, [model, filter, selectedFct]);
+ model.setFilter((msg: Message) => filterMessage(filter, selectedDecl, msg));
+ }, [model, filter, selectedDecl]);
const onMessageSelection = React.useCallback(
(msg: Message) => {
selectMsg(msg);
setText(msg.message);
- if (msg.fct && msg.marker) {
- const location = { fct: msg.fct, marker: msg.marker };
- updateSelection({ location });
+ if (msg.decl || msg.marker) {
+ States.setCurrent({ decl: msg.decl, marker: msg.marker });
}
- }, [updateSelection],
+ }, []
);
const [showFilter, flipFilter] =
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 5be49e7b932d9f44dea7bd4ae0bd4fdbf2ed644b..e394979c4909bae20b78ccdcd57262fc4aa3356c 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -680,14 +680,16 @@ export default function RenderProperties(): JSX.Element {
populateModel(model, props, evaps);
}, [model, props, evaps]);
- const [selection, updateSelection] = States.useSelection();
+ const { marker } = States.useCurrent();
+ const { scope } = States.useMarker(marker);
+ const propertySelection = marker;
+ const selectedFunction = marker && scope;
const [showFilter, flipFilter] =
Dome.useFlipSettings('ivette.properties.showFilter', true);
// Updating the filter
Dome.useEvent(Reload, model.reload);
- const selectedFunction = selection?.current?.fct;
React.useEffect(() => {
model.setFilterFunction(selectedFunction);
}, [model, selectedFunction]);
@@ -695,14 +697,9 @@ export default function RenderProperties(): JSX.Element {
// Callbacks
const onPropertySelection = React.useCallback(
- ({ key: marker, fct }: Property) => {
- const location = { fct, marker };
- updateSelection({ location });
- }, [updateSelection],
+ (p: Property) => States.gotoGlobalMarker(p.key), []
);
- const propertySelection = selection?.current?.marker;
-
return (
<>
<TitleBar>
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index 69f9cc5cdc0e1b7b07397049571d33e00b54473c..63c131c4436f28cfc3650a52108104008b5101b2 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -84,11 +84,6 @@ async function edit(file: string, pos: Position, cmd: string): Promise<void> {
// Fields declarations
// -----------------------------------------------------------------------------
-// The Ivette selection must be updated by the CodeMirror plugin. This field
-// adds the callback in the CodeMirror internal state.
-type UpdateSelection = (a: States.SelectionActions) => void;
-const UpdateSelection = Editor.createField<UpdateSelection>(() => { return; });
-
// Those fields contain the source code and the file name.
const Source = Editor.createTextField<string>('', (s) => s);
const File = Editor.createField<string>('');
@@ -104,19 +99,19 @@ const GetSource = Editor.createField<GetSource>(() => undefined);
// current CodeMirror cursor) and the ivette location (i.e the locations as
// seen by the outside world). Keeping track of both of them together force
// their update in one dispatch, which prevents strange bugs.
-interface Locations { cursor?: States.Location, ivette: States.Location }
+interface Locations { cursor?: States.Location, current: States.Location }
// The Locations field. When given Locations, it will update the cursor field if
// and only if the new cursor location is not undefined. It simplifies the
// update in the SourceCode component itself.
const Locations = createLocationsField();
function createLocationsField(): Editor.Field<Locations> {
- const noField = { cursor: undefined, ivette: {} };
+ const noField = { cursor: undefined, current: {} };
const field = Editor.createField<Locations>(noField);
const set: Editor.Set<Locations> = (view, toBe) => {
const hasBeen = field.get(view?.state);
const cursor = toBe.cursor ?? hasBeen.cursor;
- field.set(view, { cursor, ivette: toBe.ivette });
+ field.set(view, { cursor, current: toBe.current });
};
return { ...field, set };
}
@@ -132,21 +127,21 @@ function createLocationsField(): Editor.Field<Locations> {
// Update the outside world when the user click somewhere in the source code.
const SyncOnUserSelection = createSyncOnUserSelection();
function createSyncOnUserSelection(): Editor.Extension {
- const actions = { cmd: Command, update: UpdateSelection };
+ const actions = { cmd: Command };
const deps = { file: File, selection: Selection, doc: Document, ...actions };
return Editor.createEventHandler(deps, {
- mouseup: async ({ file, cmd, update }, view, event) => {
+ mouseup: async ({ file, cmd }, view, event) => {
if (!view || file === '') return;
const pos = getCursorPosition(view);
- const cursor = [file, pos.line, pos.column];
+ const cursor = { file, line: pos.line, column: pos.column };
try {
- const [fct, marker] = await Server.send(Ast.getMarkerAt, cursor);
- if (fct || marker) {
+ const marker = await Server.send(Ast.getMarkerAt, cursor);
+ if (marker) {
// The forced reload should NOT be necessary but... It is...
await Server.send(Ast.reloadMarkerAttributes, null);
- const location = { fct, marker };
- update({ location });
- Locations.set(view, { cursor: location, ivette: location });
+ States.gotoGlobalMarker(marker);
+ const location = States.getCurrent();
+ Locations.set(view, { cursor: location, current: location });
}
} catch {
setError('Failure');
@@ -162,12 +157,13 @@ const SyncOnOutsideSelection = createSyncOnOutsideSelection();
function createSyncOnOutsideSelection(): Editor.Extension {
const deps = { locations: Locations, get: GetSource };
return Editor.createViewUpdater(deps, ({ locations, get }, view) => {
- const { cursor, ivette } = locations;
- if (ivette === undefined || ivette === cursor) return;
- const source = get(ivette); if (!source) return;
- const newFct = ivette.fct !== cursor?.fct && ivette.marker === undefined;
- const onTop = cursor === undefined || newFct;
- Locations.set(view, { cursor: ivette, ivette });
+ const { cursor, current } = locations;
+ if (current === undefined || current === cursor) return;
+ const source = get(current); if (!source) return;
+ const newDecl =
+ current.decl !== cursor?.decl && current.marker === undefined;
+ const onTop = cursor === undefined || newDecl;
+ Locations.set(view, { cursor: current, current });
Editor.selectLine(view, source.line, onTop);
});
}
@@ -183,7 +179,7 @@ function createSyncOnOutsideSelection(): Editor.Extension {
// This events handler takes care of the context menu.
const ContextMenu = createContextMenu();
function createContextMenu(): Editor.Extension {
- const deps = { file: File, command: Command, update: UpdateSelection };
+ const deps = { file: File, command: Command };
return Editor.createEventHandler(deps, {
contextmenu: ({ file, command }, view) => {
if (file === '') return;
@@ -212,13 +208,13 @@ function useFctSource(file: string): string {
// Build a callback that retrieves a location's source information.
function useSourceGetter(): GetSource {
const getAttr = States.useSyncArrayGetter(Ast.markerAttributes);
- const functionsData = States.useSyncArrayData(Ast.functions);
- return React.useCallback(({ fct, marker }) => {
- const markerSloc = getAttr(marker)?.sloc;
- const fctSloc = (fct !== undefined && fct !== '') ?
- functionsData.find((e) => e.name === fct)?.sloc : undefined;
- return markerSloc ?? fctSloc;
- }, [getAttr, functionsData]);
+ const getDecl = States.useSyncArrayGetter(Ast.declAttributes);
+ return React.useCallback(({ decl, marker }) => {
+ const { sloc, decl: markerDecl } = getAttr(marker) ?? {};
+ if (sloc) return sloc;
+ const { source } = getDecl(decl ?? markerDecl) ?? {};
+ return source;
+ }, [getAttr, getDecl]);
}
// -----------------------------------------------------------------------------
@@ -249,20 +245,18 @@ export default function SourceCode(): JSX.Element {
const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
const { view, Component } = Editor.Editor(extensions);
- const [selection, update] = States.useSelection();
- const loc = React.useMemo(() => selection?.current ?? {}, [selection]);
+ const current = States.useCurrent();
const getSource = useSourceGetter();
- const file = getSource(loc)?.file ?? '';
+ const file = getSource(current)?.file ?? '';
const filename = Path.parse(file).base;
const pos = getCursorPosition(view);
const source = useFctSource(file);
- React.useEffect(() => UpdateSelection.set(view, update), [view, update]);
React.useEffect(() => GetSource.set(view, getSource), [view, getSource]);
React.useEffect(() => File.set(view, file), [view, file]);
React.useEffect(() => Source.set(view, source), [view, source]);
React.useEffect(() => Command.set(view, command), [view, command]);
- React.useEffect(() => Locations.set(view, { ivette: loc }), [view, loc]);
+ React.useEffect(() => Locations.set(view, { current }), [view, current]);
const externalEditorTitle =
'Open the source file in an external editor.';
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 2c78d9fba901a5b8f7afe7041fa7fec69a90f8d8..2f5fdbff1bad4692b43ce481c8988d9d10b91dab 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -423,6 +423,8 @@ export const printFunction: Server.GetRequest<fct,text>= printFunction_internal;
export interface functionsData {
/** Entry identifier. */
key: Json.key<'#functions'>;
+ /** Declaration Tag */
+ decl: decl;
/** Name */
name: string;
/** Signature */
@@ -445,6 +447,7 @@ export interface functionsData {
export const jFunctionsData: Json.Decoder<functionsData> =
Json.jObject({
key: Json.jKey<'#functions'>('#functions'),
+ decl: jDecl,
name: Json.jString,
signature: Json.jString,
main: Json.jOption(Json.jBoolean),
@@ -458,10 +461,11 @@ export const jFunctionsData: Json.Decoder<functionsData> =
/** Natural order for `functionsData` */
export const byFunctionsData: Compare.Order<functionsData> =
Compare.byFields
- <{ key: Json.key<'#functions'>, name: string, signature: string,
- main?: boolean, defined?: boolean, stdlib?: boolean,
- builtin?: boolean, extern?: boolean, sloc: source }>({
+ <{ key: Json.key<'#functions'>, decl: decl, name: string,
+ signature: string, main?: boolean, defined?: boolean,
+ stdlib?: boolean, builtin?: boolean, extern?: boolean, sloc: source }>({
key: Compare.string,
+ decl: byDecl,
name: Compare.alpha,
signature: Compare.string,
main: Compare.defined(Compare.boolean),
@@ -523,9 +527,10 @@ export const functions: State.Array<Json.key<'#functions'>,functionsData> = func
/** Default value for `functionsData` */
export const functionsDataDefault: functionsData =
- { key: Json.jKey<'#functions'>('#functions')(''), name: '', signature: '',
- main: undefined, defined: undefined, stdlib: undefined,
- builtin: undefined, extern: undefined, sloc: sourceDefault };
+ { key: Json.jKey<'#functions'>('#functions')(''), decl: declDefault,
+ name: '', signature: '', main: undefined, defined: undefined,
+ stdlib: undefined, builtin: undefined, extern: undefined,
+ sloc: sourceDefault };
/** Updated AST information */
export const getInformationUpdate: Server.Signal = {
@@ -558,19 +563,25 @@ export const getInformation: Server.GetRequest<
>= getInformation_internal;
const getMarkerAt_internal: Server.GetRequest<
- [ string, number, number ],
- [ fct | undefined, marker | undefined ]
+ { file: string, line: number, column: number },
+ marker |
+ undefined
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getMarkerAt',
- input: Json.jTriple( Json.jString, Json.jNumber, Json.jNumber,),
- output: Json.jPair( Json.jOption(jFct), Json.jOption(jMarker),),
- signals: [],
+ input: Json.jObject({
+ file: Json.jString,
+ line: Json.jNumber,
+ column: Json.jNumber,
+ }),
+ output: Json.jOption(jMarker),
+ signals: [ { name: 'kernel.ast.changed' } ],
};
/** Returns the marker and function at a source file position, if any. Input: file path, line and column. */
export const getMarkerAt: Server.GetRequest<
- [ string, number, number ],
- [ fct | undefined, marker | undefined ]
+ { file: string, line: number, column: number },
+ marker |
+ undefined
>= getMarkerAt_internal;
const getFiles_internal: Server.GetRequest<null,string[]> = {
diff --git a/ivette/src/frama-c/kernel/api/services/index.ts b/ivette/src/frama-c/kernel/api/services/index.ts
index 145b1f0827579f831915bf44ce7291690ff60159..957ed06058fc4d4308d20d80bd8b5c4c3b3bf316 100644
--- a/ivette/src/frama-c/kernel/api/services/index.ts
+++ b/ivette/src/frama-c/kernel/api/services/index.ts
@@ -38,17 +38,17 @@ import * as Server from 'frama-c/server';
import * as State from 'frama-c/states';
//@ts-ignore
-import { byFct } from 'frama-c/kernel/api/ast';
+import { byDecl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { bySource } from 'frama-c/kernel/api/ast';
//@ts-ignore
-import { fct } from 'frama-c/kernel/api/ast';
+import { decl } from 'frama-c/kernel/api/ast';
//@ts-ignore
-import { fctDefault } from 'frama-c/kernel/api/ast';
+import { declDefault } from 'frama-c/kernel/api/ast';
//@ts-ignore
-import { jFct } from 'frama-c/kernel/api/ast';
+import { jDecl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
@@ -161,8 +161,8 @@ export interface messageData {
source?: source;
/** Marker at the message position (if any) */
marker?: marker;
- /** Function containing the message position (if any) */
- fct?: fct;
+ /** Declaration containing the message position (if any) */
+ decl?: decl;
}
/** Decoder for `messageData` */
@@ -175,7 +175,7 @@ export const jMessageData: Json.Decoder<messageData> =
category: Json.jOption(Json.jString),
source: Json.jOption(jSource),
marker: Json.jOption(jMarker),
- fct: Json.jOption(jFct),
+ decl: Json.jOption(jDecl),
});
/** Natural order for `messageData` */
@@ -183,7 +183,7 @@ export const byMessageData: Compare.Order<messageData> =
Compare.byFields
<{ key: Json.key<'#message'>, kind: logkind, plugin: string,
message: string, category?: string, source?: source, marker?: marker,
- fct?: fct }>({
+ decl?: decl }>({
key: Compare.string,
kind: byLogkind,
plugin: Compare.alpha,
@@ -191,7 +191,7 @@ export const byMessageData: Compare.Order<messageData> =
category: Compare.defined(Compare.string),
source: Compare.defined(bySource),
marker: Compare.defined(byMarker),
- fct: Compare.defined(byFct),
+ decl: Compare.defined(byDecl),
});
/** Signal for array [`message`](#message) */
@@ -247,7 +247,7 @@ export const message: State.Array<Json.key<'#message'>,messageData> = message_in
export const messageDataDefault: messageData =
{ key: Json.jKey<'#message'>('#message')(''), kind: logkindDefault,
plugin: '', message: '', category: undefined, source: undefined,
- marker: undefined, fct: undefined };
+ marker: undefined, decl: undefined };
/** Message event record. */
export interface log {
diff --git a/ivette/src/frama-c/menu.ts b/ivette/src/frama-c/menu.ts
index accc957ef5b41d000a9ecedcff13e7655e001199..6879ef815357d8a22bae15a915a4b38b06a6f1fe 100644
--- a/ivette/src/frama-c/menu.ts
+++ b/ivette/src/frama-c/menu.ts
@@ -57,7 +57,7 @@ async function setFiles(): Promise<void> {
});
if (files) {
await parseFiles(files);
- States.resetSelection();
+ States.clearSelection();
}
return;
}
@@ -90,7 +90,7 @@ async function loadSession(): Promise<void> {
const file = await Dialogs.showOpenFile({ title: 'Load a saved session' });
Status.setMessage({ text: 'Loading session…', kind: 'progress' });
const error = await Server.send(Services.load, file);
- States.resetSelection();
+ States.clearSelection();
if (error) {
Status.setMessage({
text: 'Error when loading the session',
diff --git a/ivette/src/frama-c/plugins/callgraph/api/index.ts b/ivette/src/frama-c/plugins/callgraph/api/index.ts
index e231a66fbbae3bb315cd9a85a06f47096f0311db..0ccf01428e0a1ef9bf0a61e5c85c635f31355e22 100644
--- a/ivette/src/frama-c/plugins/callgraph/api/index.ts
+++ b/ivette/src/frama-c/plugins/callgraph/api/index.ts
@@ -37,13 +37,21 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byDecl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { decl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { declDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { fct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { fctDefault } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { jDecl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byTag } from 'frama-c/kernel/api/data';
@@ -57,6 +65,8 @@ import { tagDefault } from 'frama-c/kernel/api/data';
export interface vertex {
/** The function represented by the node */
kf: fct;
+ /** The declaration tag of the function */
+ decl: decl;
/** whether this node is the root of a service */
is_root: boolean;
/** the root of this node's service */
@@ -65,20 +75,21 @@ export interface vertex {
/** Decoder for `vertex` */
export const jVertex: Json.Decoder<vertex> =
- Json.jObject({ kf: jFct, is_root: Json.jBoolean, root: jFct,});
+ Json.jObject({ kf: jFct, decl: jDecl, is_root: Json.jBoolean, root: jFct,});
/** Natural order for `vertex` */
export const byVertex: Compare.Order<vertex> =
Compare.byFields
- <{ kf: fct, is_root: boolean, root: fct }>({
+ <{ kf: fct, decl: decl, is_root: boolean, root: fct }>({
kf: byFct,
+ decl: byDecl,
is_root: Compare.boolean,
root: byFct,
});
/** Default value for `vertex` */
export const vertexDefault: vertex =
- { kf: fctDefault, is_root: false, root: fctDefault };
+ { kf: fctDefault, decl: declDefault, is_root: false, root: fctDefault };
/** Whether the call goes through services or not */
export enum edgeKind {
diff --git a/ivette/src/frama-c/plugins/callgraph/index.tsx b/ivette/src/frama-c/plugins/callgraph/index.tsx
index e0b1861ef05335fefc5bed6d61b246789f732162..d5561731df95c37fd7e168116d5a8d1571c1a835 100644
--- a/ivette/src/frama-c/plugins/callgraph/index.tsx
+++ b/ivette/src/frama-c/plugins/callgraph/index.tsx
@@ -20,7 +20,7 @@
/* */
/* ************************************************************************ */
-import React, { useEffect, useState } from 'react';
+import React from 'react';
import _ from 'lodash';
import * as Ivette from 'ivette';
import * as Server from 'frama-c/server';
@@ -36,7 +36,7 @@ import 'cytoscape-panzoom/cytoscape.js-panzoom.css';
import style from './graph-style.json';
import { useGlobalState } from 'dome/data/states';
-import { useRequest, useSelection, useSyncValue } from 'frama-c/states';
+import * as States from 'frama-c/states';
import gearsIcon from 'frama-c/plugins/eva/images/gears.svg';
import { CallstackState } from 'frama-c/plugins/eva/valuetable';
@@ -123,13 +123,14 @@ function selectCallstack(cy: Cy.Core, callstack: callstack | undefined): void {
}
function Callgraph() : JSX.Element {
- const isComputed = useSyncValue(CgAPI.isComputed);
- const graph = useSyncValue(CgAPI.callgraph);
- const [cy, setCy] = useState<Cy.Core>();
+ const isComputed = States.useSyncValue(CgAPI.isComputed);
+ const graph = States.useSyncValue(CgAPI.callgraph);
+ const [cy, setCy] = React.useState<Cy.Core>();
const [cs] = useGlobalState(CallstackState);
- const [selection, setSelection] = useSelection();
- const callstack = useRequest(ValuesAPI.getCallstackInfo, cs);
-
+ const callstack = States.useRequest(ValuesAPI.getCallstackInfo, cs);
+ const { decl } = States.useCurrent();
+ const { kind, name } = States.useDeclaration(decl);
+ const fct = kind === 'FUNCTION' ? name : undefined;
const layout = { name: 'cola', nodeSpacing: 32 };
const computedStyle = getComputedStyle(document.documentElement);
const styleVariables =
@@ -144,26 +145,23 @@ function Callgraph() : JSX.Element {
];
// Marker selection
- useEffect(() => {
- cy && selectFct(cy, selection.current?.fct);
- }, [cy, selection]);
+ React.useEffect(() => { cy && selectFct(cy, fct); }, [cy, fct]);
// Callstack selection
- useEffect(() => {
+ React.useEffect(() => {
cy && selectCallstack(cy, callstack);
}, [cy, callstack]);
// Click on graph
- useEffect(() => {
+ React.useEffect(() => {
if (cy) {
cy.off('click');
cy.on('click', 'node', (event) => {
- const fct = event.target.id() as string;
- setSelection({ location: { fct } });
+ const { decl } = event.target.data;
+ States.setCurrent({ decl });
});
}
- }, [cy, setSelection]);
-
+ }, [cy]);
if (isComputed === false) {
Server.send(CgAPI.compute, null);
diff --git a/ivette/src/frama-c/plugins/dive/index.tsx b/ivette/src/frama-c/plugins/dive/index.tsx
index 77dd2a9f9aa1316c467648d7493450d287645c96..ddb9de3edb42f6c4d292acdb39008b6b99651e0b 100644
--- a/ivette/src/frama-c/plugins/dive/index.tsx
+++ b/ivette/src/frama-c/plugins/dive/index.tsx
@@ -581,7 +581,7 @@ const GraphView = React.forwardRef<GraphViewRef | undefined, GraphViewProps>(
const { lock, layout, selectionMode } = props;
const [dive, setDive] = useState(() => new Dive());
- const [selection, updateSelection] = States.useSelection();
+ const selection = States.useCurrent();
const graph = States.useSyncArrayData(API.graph);
function setCy(cy: Cytoscape.Core): void {
@@ -609,19 +609,9 @@ const GraphView = React.forwardRef<GraphViewRef | undefined, GraphViewProps>(
}, [dive, selectionMode]);
useEffect(() => {
- /* When clicking on a node, select its writes locations as a multiple
- selection. If these locations were already selected, select the next
- location in the multiple selection. */
- dive.onSelect = (locations) => {
- if (_.isEqual(locations, selection?.multiple?.allSelections))
- updateSelection('MULTIPLE_CYCLE');
- else
- updateSelection({ locations, index: 0 });
- };
-
// Updates the graph according to the selected marker.
- dive.selectLocation(selection?.current, !lock);
- }, [dive, lock, selection, updateSelection]);
+ dive.selectLocation(selection, !lock);
+ }, [dive, lock, selection]);
return (
<CytoscapeComponent
diff --git a/ivette/src/frama-c/plugins/eva/Coverage.tsx b/ivette/src/frama-c/plugins/eva/Coverage.tsx
index 0a048970850663ee84404e3c369409b220e97509..53dbcf591d3ea066f7953f6789be258f51e315f9 100644
--- a/ivette/src/frama-c/plugins/eva/Coverage.tsx
+++ b/ivette/src/frama-c/plugins/eva/Coverage.tsx
@@ -76,16 +76,18 @@ export function CoverageTable(): JSX.Element {
model.setSorting({ sortBy: 'coverage', sortDirection: 'ASC' });
}, [model]);
- const [selection, updateSelection] = States.useSelection();
- const onSelection = ({ key }: stats): void => {
- updateSelection({ location: { fct: key } });
+ const { decl } = States.useCurrent();
+ const { kind, name } = States.useDeclaration(decl);
+ const selection = kind==='FUNCTION' ? name : undefined;
+ const onSelection = ({ decl }: stats): void => {
+ States.gotoDeclaration(decl);
};
return (
<Table
model={model}
sorting={model}
- selection={selection?.current?.fct}
+ selection={selection}
onSelection={onSelection}
settings="ivette.coverage.table"
>
diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
index 503d95e8dc93e3a33579eb94cbe091d3fbe8c947..9f7da4ed9893e9bb957850f5bcbd3886a88e5ded 100644
--- a/ivette/src/frama-c/plugins/eva/DomainStates.tsx
+++ b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
@@ -36,9 +36,7 @@ const globalSelectedDomain = new GlobalState("");
const globalFilter = new GlobalState(true);
export function EvaStates(): JSX.Element {
- const [selection] = States.useSelection();
- const selectedLoc = selection?.current;
- const marker = selectedLoc?.marker;
+ const { marker } = States.useCurrent();
const [domains, setDomains] = React.useState<string[]>([]);
const [selected, setSelected] = useGlobalState(globalSelectedDomain);
const [stateBefore, setStateBefore] = React.useState("");
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 681fa6de976e04dacd381a9b1626ae76cf8a8ee5..9bb203d2527f9d4302bcb5be29f8aa3fb7078a9d 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -37,15 +37,23 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byDecl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { decl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { declDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { fct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { fctDefault } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { jDecl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
@@ -607,6 +615,8 @@ export const programStats: State.Value<programStatsType> = programStats_internal
export interface functionStatsData {
/** Entry identifier. */
key: fct;
+ /** Function declaration tag */
+ decl: decl;
/** Coverage of the Eva analysis */
coverage: { reachable: number, dead: number };
/** Alarms raised by the Eva analysis by category */
@@ -619,6 +629,7 @@ export interface functionStatsData {
export const jFunctionStatsData: Json.Decoder<functionStatsData> =
Json.jObject({
key: jFct,
+ decl: jDecl,
coverage: Json.jObject({ reachable: Json.jNumber, dead: Json.jNumber,}),
alarmCount: Json.jArray(jAlarmEntry),
alarmStatuses: jStatusesEntry,
@@ -627,9 +638,10 @@ export const jFunctionStatsData: Json.Decoder<functionStatsData> =
/** Natural order for `functionStatsData` */
export const byFunctionStatsData: Compare.Order<functionStatsData> =
Compare.byFields
- <{ key: fct, coverage: { reachable: number, dead: number },
+ <{ key: fct, decl: decl, coverage: { reachable: number, dead: number },
alarmCount: alarmEntry[], alarmStatuses: statusesEntry }>({
key: byFct,
+ decl: byDecl,
coverage: Compare.byFields
<{ reachable: number, dead: number }>({
reachable: Compare.number,
@@ -690,8 +702,8 @@ export const functionStats: State.Array<fct,functionStatsData> = functionStats_i
/** Default value for `functionStatsData` */
export const functionStatsDataDefault: functionStatsData =
- { key: fctDefault, coverage: { reachable: 0, dead: 0 }, alarmCount: [],
- alarmStatuses: statusesEntryDefault };
+ { key: fctDefault, decl: declDefault, coverage: { reachable: 0, dead: 0 },
+ alarmCount: [], alarmStatuses: statusesEntryDefault };
const getStates_internal: Server.GetRequest<
[ marker, boolean ],
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 95a83acbc7044e37a0de10da29d3254b55f1f7ab..0ce7db49e7e585496449ad21433583d035eaf460 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -132,11 +132,12 @@ interface Callsite {
/* 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);
+ const getter = React.useCallback(
+ (c: callstack): Promise<Callsite[]> => {
+ if (c !== 'Summary') return Server.send(Values.getCallstackInfo, c);
+ else return Promise.resolve([]);
+ }, []);
+ return Dome.useCache(getter);
}
/* -------------------------------------------------------------------------- */
@@ -149,8 +150,9 @@ function useCallsitesCache(): Request<callstack, Callsite[]> {
/* A Location is a marker in a function */
interface Location {
- target: Ast.marker;
fct: string;
+ decl: Ast.decl;
+ marker: Ast.marker;
}
/* An Evaluation keeps track of the values at relevant control point around a
@@ -181,11 +183,12 @@ interface Probe extends Location {
function useEvaluationCache(): Request<[ Location, callstack ], Evaluation> {
type LocStack = [ Location, callstack ];
const toString = React.useCallback(([ l, c ] : LocStack): string => {
- return `${l.fct}:${l.target}:${c}`;
+ return `${l.fct}:${l.marker}:${c}`;
}, []);
const get: Request<LocStack, Evaluation> = React.useCallback(([ l, c ]) => {
const callstack = c === 'Summary' ? undefined : c;
- return Server.send(Values.getValues, { ...l, callstack });
+ const target = l.marker;
+ return Server.send(Values.getValues, { target, callstack });
}, []);
return Dome.useCache(get, toString);
}
@@ -195,7 +198,7 @@ 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 infos = await Server.send(Values.getProbeInfo, loc.marker);
const evaluate: Request<callstack, Evaluation> = (c) => cache([ loc, c ]);
return { ...loc, ...infos, evaluate };
}, [ cache ]);
@@ -262,22 +265,19 @@ function AlarmsInfos(probe?: Probe): Request<callstack, JSX.Element> {
interface StackInfosProps {
callsites: Callsite[];
isSelected: boolean;
- setSelection: (a: States.SelectionActions) => void;
close: () => void;
}
async function StackInfos(props: StackInfosProps): Promise<JSX.Element> {
- const { callsites, setSelection, isSelected, close } = props;
+ const { callsites, 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);
+ States.gotoGlobalMarker(stmt, meta);
};
const onClick = (evt: React.MouseEvent): void => { select(evt.altKey); };
const onDoubleClick = (evt: React.MouseEvent): void => {
@@ -328,13 +328,12 @@ interface ProbeHeaderProps {
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 { probe, status, locEvt } = props;
+ const { code = '(error)', stmt, marker, decl, 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);
@@ -347,8 +346,10 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
const isPinned = isPinnedMarker(status);
const pinText = isPinned ? 'Unpin' : 'Pin';
- const loc: States.SelectionActions = { location: { fct, marker: target } };
- const onClick = (): void => { setSelection(loc); selectProbe(); };
+ const onClick = (): void => {
+ States.setCurrent({ marker, decl });
+ selectProbe();
+ };
const onDoubleClick = (): void => pinProbe(!isPinned);
const onContextMenu = (): void => {
const items: Dome.PopupMenuItem[] = [];
@@ -389,7 +390,7 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
<div className='eva-header-text-overflow'>
<span className='dome-text-cell' title={code}>{code}</span>
</div>
- <Stmt fct={fct} stmt={stmt} marker={target} short={true}/>
+ <Stmt fct={fct} stmt={stmt} marker={marker} short={true}/>
</TableCell>
</th>
);
@@ -469,6 +470,7 @@ interface ProbeValuesProps {
function ProbeValues(props: ProbeValuesProps): Request<callstack, JSX.Element> {
const { probe, addLoc, isSelectedCallstack } = props;
+ const { fct, decl } = probe;
// Building common parts
const onContextMenu = (evaluation?: Values.evaluation) => (): void => {
@@ -480,7 +482,7 @@ function ProbeValues(props: ProbeValuesProps): Request<callstack, JSX.Element> {
pointedVars.forEach((lval) => {
const [text, lvalMarker] = lval;
const label = `Display values for ${text}`;
- const location = { fct: probe.fct, target: lvalMarker };
+ const location = { decl, fct, marker: lvalMarker };
const onItemClick = (): void => addLoc(location);
items.push({ label, onClick: onItemClick });
});
@@ -581,6 +583,7 @@ async function CallsiteCell(props: CallsiteCellProps): Promise<JSX.Element> {
interface FunctionProps {
fct: string;
+ decl: Ast.decl;
markers: Map<Ast.marker, MarkerStatus>;
close: () => void;
getProbe: Request<Location, Probe>;
@@ -596,7 +599,6 @@ interface FunctionProps {
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;
@@ -605,8 +607,8 @@ interface FunctionProps {
const PageSize = 99;
async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
- const { fct, folded, isSelectedCallstack, locEvt } = props;
- const { byCallstacks, setSelection, getCallsites } = props;
+ const { fct, decl, folded, isSelectedCallstack, locEvt } = props;
+ const { byCallstacks, getCallsites } = props;
const { addLoc, getCallstacks: getCS } = props;
const { setFolded, setByCallstacks, close } = props;
const { startingCallstack, changeStartingCallstack } = props;
@@ -628,8 +630,8 @@ async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
/* 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 data = await Promise.all(entries.map(async ([ marker, status ]) => {
+ const probe = await props.getProbe({ marker, decl, fct });
const summary = await probe.evaluate('Summary');
return { probe, summary, status } as Data;
}));
@@ -641,7 +643,7 @@ async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
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 };
+ const fcts = { selectProbe, pinProbe, removeProbe };
return ProbeHeader({ ...d, ...fcts, locEvt });
}));
@@ -763,14 +765,16 @@ async function FunctionSection(props: FunctionProps): Promise<JSX.Element> {
class FunctionInfos {
readonly fct: string; // Function's name
+ readonly decl: Ast.decl; // Function's declaration
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) {
+ constructor(fct: string, decl: Ast.decl) {
this.fct = fct;
+ this.decl = decl;
}
has(marker: Ast.marker): boolean {
@@ -799,7 +803,7 @@ class FunctionInfos {
}
markers(focusedLoc?: Location): Map<Ast.marker, MarkerStatus> {
- const { target: tgt, fct } = focusedLoc ?? {};
+ const { marker: 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 ]));
@@ -828,14 +832,14 @@ class FunctionsManager {
this.map = this.map.bind(this);
}
- newFunction(fct: string): void {
- if (!this.cache.has(fct)) this.cache.set(fct, new FunctionInfos(fct));
+ newFunction(fct: string, decl: Ast.decl): void {
+ if (!this.cache.has(fct)) this.cache.set(fct, new FunctionInfos(fct, decl));
}
- private getInfos(fct: string): FunctionInfos {
+ private getInfos(fct: string, decl: Ast.decl): FunctionInfos {
const { cache } = this;
if (cache.has(fct)) return cache.get(fct) as FunctionInfos;
- const infos = new FunctionInfos(fct);
+ const infos = new FunctionInfos(fct, decl);
this.cache.set(fct, infos);
return infos;
}
@@ -861,24 +865,24 @@ class FunctionsManager {
}
pin(loc: Location): void {
- const { target, fct } = loc;
- this.getInfos(fct).pin(target);
+ const { marker, fct, decl } = loc;
+ this.getInfos(fct, decl).pin(marker);
}
unpin(loc: Location): void {
- const { target, fct } = loc;
- this.cache.get(fct)?.pinned.delete(target);
+ const { marker, fct } = loc;
+ this.cache.get(fct)?.pinned.delete(marker);
}
track(loc: Location): void {
- const { target, fct } = loc;
- this.getInfos(fct).track(target);
+ const { marker, fct, decl } = loc;
+ this.getInfos(fct, decl).track(marker);
}
removeLocation(loc: Location): void {
- const { target, fct } = loc;
+ const { marker, fct } = loc;
const infos = this.cache.get(fct);
- if (infos) infos.delete(target);
+ if (infos) infos.delete(marker);
}
delete(fct: string): void {
@@ -917,7 +921,7 @@ ipcRenderer.on('dome.ipc.evaluate', () => evaluateEvent.emit());
interface EvaluationModeProps {
computationState : Eva.computationStateType | undefined;
- selection: States.Selection;
+ current: Location | undefined;
setLocPin: (loc: Location, pin: boolean) => void;
}
@@ -931,19 +935,19 @@ Dome.addMenuItem({
});
function useEvaluationMode(props: EvaluationModeProps): void {
- const { computationState, selection, setLocPin } = props;
+ const { computationState, current, setLocPin } = props;
const handleError = (): void => { return; };
- const addProbe = (target: Ast.marker | undefined): void => {
- const fct = selection?.current?.fct;
- if (fct && target) setLocPin({ fct, target }, true);
+ const addProbe = (marker: Ast.marker | undefined): void => {
+ if (current && marker) setLocPin({ ...current, marker }, true);
};
React.useEffect(() => {
if (computationState !== 'computed') return () => { return; };
const shortcut = System.platform === 'macos' ? 'Cmd+E' : 'Ctrl+E';
const onEnter = (pattern: string): void => {
- const marker = selection?.current?.marker;
- const data = { stmt: marker, term: pattern };
- Server.send(Ast.parseExpr, data).then(addProbe).catch(handleError);
+ if (current) {
+ const data = { stmt: current.marker, term: pattern };
+ Server.send(Ast.parseExpr, data).then(addProbe).catch(handleError);
+ }
};
const evalMode = {
label: 'Evaluation',
@@ -958,7 +962,7 @@ function useEvaluationMode(props: EvaluationModeProps): void {
return () => Toolbars.UnregisterMode.emit(evalMode);
});
React.useEffect(() => {
- Dome.setMenuItem({ id: 'EvaluateMenu', enabled: true });
+ Dome.setMenuItem({ id: 'EvaluateMenu', enabled: current !== undefined });
return () => Dome.setMenuItem({ id: 'EvaluateMenu', enabled: false });
});
}
@@ -980,8 +984,14 @@ const FocusState = new GlobalState<Probe | undefined>(undefined);
function EvaTable(): JSX.Element {
/* Component state */
- const [ selection, select ] = States.useSelection();
- const [ cs, setCS ] = useGlobalState(CallstackState);
+ const { marker, decl } = States.useCurrent();
+ const { kind, name } = States.useDeclaration(decl);
+ const fct = kind === 'FUNCTION' ? name : undefined;
+ const current: Location | undefined = React.useMemo(
+ (): Location | undefined =>
+ ((marker && decl && fct) ? { marker, decl, fct } : undefined)
+ , [marker, decl, fct]);
+ const [ cs, setCS ] = useGlobalState(CallstackState);
const [ fcts ] = useGlobalState(FunctionsManagerState);
const [ focus, setFocus ] = useGlobalState(FocusState);
@@ -1018,18 +1028,15 @@ function EvaTable(): JSX.Element {
/* 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);
+ fcts.clean(current);
const doUpdate = (p: Probe): void => {
if (!p.evaluable) { setFocus(undefined); return; }
- if (fct && p.code) fcts.newFunction(fct);
+ if (fct && decl && p.code) fcts.newFunction(fct, decl);
setFocus(p); locEvt.emit(p);
};
- if (loc) getProbe(loc).then(doUpdate);
+ if (current) getProbe(current).then(doUpdate);
else setFocus(undefined);
- }, [ fcts, selection, getProbe, setFocus, locEvt ]);
+ }, [ fcts, current, fct, decl, getProbe, setFocus, locEvt ]);
/* Callback used to pin or unpin a location */
const setLocPin = React.useCallback((loc: Location, pin: boolean): void => {
@@ -1041,8 +1048,8 @@ function EvaTable(): JSX.Element {
/* On meta-selection, pin the selected location. */
React.useEffect(() => {
const pin = (loc: States.Location): void => {
- const { marker, fct } = loc;
- if (marker && fct) setLocPin({ target: marker, fct }, true);
+ const { marker, decl } = loc;
+ if (marker && decl && fct) setLocPin({ marker, decl, fct }, true);
};
States.MetaSelection.on(pin);
return () => States.MetaSelection.off(pin);
@@ -1051,7 +1058,7 @@ function EvaTable(): JSX.Element {
/* Callback used to remove a probe */
const remove = React.useCallback((probe: Probe): void => {
fcts.removeLocation(probe);
- if (probe.target === focus?.target) {
+ if (probe.marker === focus?.marker) {
setFocus(undefined);
fcts.clean(undefined);
}
@@ -1066,7 +1073,7 @@ function EvaTable(): JSX.Element {
* memoize the promises building. */
const functionsPromise = React.useMemo(() => {
const ps = fcts.map((infos, fct) => {
- const { byCallstacks, folded } = infos;
+ const { byCallstacks, folded, decl } = infos;
const isSelectedCallstack = (c: callstack): boolean => c === cs;
const setFolded = (folded: boolean): void => {
fcts.setFolded(fct, folded);
@@ -1087,6 +1094,7 @@ function EvaTable(): JSX.Element {
};
return {
fct,
+ decl,
markers: infos.markers(focus),
close,
pinProbe: setLocPin,
@@ -1102,7 +1110,6 @@ function EvaTable(): JSX.Element {
setByCallstacks: setByCS,
selectCallstack: (c: callstack) => { setCS(c); setTic(tac + 1); },
isSelectedCallstack,
- setSelection: select,
locEvt,
startingCallstack: infos.startingCallstack,
changeStartingCallstack,
@@ -1111,7 +1118,7 @@ function EvaTable(): JSX.Element {
return Promise.all(ps.map(FunctionSection));
},
[ cs, setCS, fcts, focus, setFocus, tac, getCallsites, setLocPin, csFct,
- getCallstacks, getProbe, remove, select, locEvt ]);
+ getCallstacks, getProbe, remove, locEvt ]);
const { result: functions } = Dome.usePromise(functionsPromise);
/* Builds the alarms component. As for the function sections, it is an
@@ -1123,17 +1130,17 @@ function EvaTable(): JSX.Element {
* 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 p = (c: Callsite): boolean =>
+ c.stmt !== undefined && c.stmt === marker;
const isSelected = callsites.find(p) !== undefined;
const close = (): void => setCS('Summary');
- return StackInfos({ callsites, isSelected, setSelection: select, close });
- }, [ cs, setCS, select, getCallsites, selection ]);
+ return StackInfos({ callsites, isSelected, close });
+ }, [ cs, setCS, getCallsites, marker ]);
const { result: stackInfos } = Dome.usePromise(stackInfosPromise);
/* Handle Evaluation mode */
const computationState = States.useSyncValue(Eva.computationState);
- useEvaluationMode({ computationState, selection, setLocPin });
+ useEvaluationMode({ computationState, current, setLocPin });
/* Builds the component */
return (
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index 583cfa274865831fa597f5221d2781b6a46412af..74357758fe451362fcb8e02e4815d4fe9e211955 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -37,15 +37,23 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byDecl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { decl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { declDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { fct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { fctDefault } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { jDecl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { jFct } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
@@ -183,6 +191,8 @@ export interface goalsData {
wpo: goal;
/** Property Marker */
property: marker;
+ /** Associated declaration, if any */
+ scope?: decl;
/** Associated function, if any */
fct?: fct;
/** Associated behavior, if any */
@@ -210,6 +220,7 @@ export const jGoalsData: Json.Decoder<goalsData> =
Json.jObject({
wpo: jGoal,
property: jMarker,
+ scope: Json.jOption(jDecl),
fct: Json.jOption(jFct),
bhv: Json.jOption(Json.jString),
thy: Json.jOption(Json.jString),
@@ -225,11 +236,12 @@ export const jGoalsData: Json.Decoder<goalsData> =
/** Natural order for `goalsData` */
export const byGoalsData: Compare.Order<goalsData> =
Compare.byFields
- <{ wpo: goal, property: marker, fct?: fct, bhv?: string, thy?: string,
- name: string, smoke: boolean, passed: boolean, status: status,
- stats: stats, script?: string, saved: boolean }>({
+ <{ wpo: goal, property: marker, scope?: decl, fct?: fct, bhv?: string,
+ thy?: string, name: string, smoke: boolean, passed: boolean,
+ status: status, stats: stats, script?: string, saved: boolean }>({
wpo: byGoal,
property: byMarker,
+ scope: Compare.defined(byDecl),
fct: Compare.defined(byFct),
bhv: Compare.defined(Compare.string),
thy: Compare.defined(Compare.string),
@@ -291,10 +303,10 @@ export const goals: State.Array<goal,goalsData> = goals_internal;
/** Default value for `goalsData` */
export const goalsDataDefault: goalsData =
- { wpo: goalDefault, property: markerDefault, fct: undefined,
- bhv: undefined, thy: undefined, name: '', smoke: false, passed: false,
- status: statusDefault, stats: statsDefault, script: undefined,
- saved: false };
+ { wpo: goalDefault, property: markerDefault, scope: undefined,
+ fct: undefined, bhv: undefined, thy: undefined, name: '', smoke: false,
+ passed: false, status: statusDefault, stats: statsDefault,
+ script: undefined, saved: false };
/** Proof Server Activity */
export const serverActivity: Server.Signal = {
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 71d7af84859452f94af698093aaf6f98208af8dc..fe784bc40ceca98f6c3871cb5268a77cd67d36c0 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -25,6 +25,7 @@ import { IconKind, Cell } from 'dome/controls/labels';
import { Filter } from 'dome/table/models';
import { Table, Column } from 'dome/table/views';
import * as States from 'frama-c/states';
+import * as Ast from 'frama-c/kernel/api/ast';
import * as WP from 'frama-c/plugins/wp/api';
/* -------------------------------------------------------------------------- */
@@ -79,11 +80,11 @@ function renderStatus(s : Status): JSX.Element {
function filterGoal(
failed: boolean,
- scope: string | undefined,
+ scope: Ast.decl | undefined,
): Filter<WP.goal, WP.goalsData> {
return (goal: WP.goalsData): boolean => {
if (failed && goal.passed) return false;
- if (scope && scope && goal.fct !== scope) return false;
+ if (scope && goal.scope !== scope) return false;
return true;
};
}
@@ -93,7 +94,7 @@ function filterGoal(
/* -------------------------------------------------------------------------- */
export interface GoalTableProps {
- scope: string | undefined;
+ scope: Ast.decl | undefined;
failed: boolean;
onFilter: (goals: number, total: number) => void;
}
@@ -101,16 +102,13 @@ export interface GoalTableProps {
export function GoalTable(props: GoalTableProps): JSX.Element {
const { scope, failed, onFilter } = props;
const model = States.useSyncArrayModel(WP.goals);
- const [_, updateAstSelection] = States.useSelection();
const [wpoSelection, setWpoSelection] = React.useState(WP.goalDefault);
const onWpoSelection = React.useCallback(
- ({ wpo, property: marker, fct }: WP.goalsData) => {
- const location = { fct, marker };
- updateAstSelection({ location });
+ ({ wpo, property }: WP.goalsData) => {
+ States.gotoGlobalMarker(property);
setWpoSelection(wpo);
- }, [updateAstSelection],
- );
+ }, []);
React.useEffect(() => {
if (failed || !!scope) {
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index ebc87c0fc249c5219cf44d959727876e1f2d15e1..24a6beb1cb16da6c2afe48f45e9ca9aa45d57c4f 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -43,15 +43,14 @@ import './style.css';
function WPGoals(): JSX.Element {
const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped');
const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed');
- const [selection] = States.useSelection();
+ const { decl } = States.useCurrent();
const [goals, setGoals] = React.useState(0);
const [total, setTotal] = React.useState(0);
const onFilter = React.useCallback((goals, total) => {
setGoals(goals);
setTotal(total);
}, [setGoals, setTotal]);
- const fct = selection?.current?.fct;
- const scope = scoped ? fct : undefined;
+ const scope = scoped ? decl : undefined;
return (
<>
<Ivette.TitleBar>
@@ -60,7 +59,7 @@ function WPGoals(): JSX.Element {
</Label>
<Inset />
<IconButton icon='COMPONENT' title='Current Scope Only'
- enabled={!!fct}
+ enabled={!!scope}
selected={scoped} onClick={flipScoped} />
<IconButton icon='CIRC.QUESTION' title='Unresolved Goals Only'
selected={failed} onClick={flipFailed} />
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 1ff4fadc9ba31801b70fd96a2519b316b43cbc93..38f09f477e9f681ff6f49cac2d3c032dfe730a4f 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -38,7 +38,6 @@ import { Client, useModel } from 'dome/table/models';
import { CompactModel } from 'dome/table/arrays';
import * as Ast from 'frama-c/kernel/api/ast';
import * as Server from './server';
-import * as Status from 'frama-c/kernel/Status';
// --------------------------------------------------------------------------
// --- Pretty Printing (Browser Console)
@@ -519,305 +518,136 @@ export function onSyncArray<K, A>(
// --- Selection
// --------------------------------------------------------------------------
-/** An AST location.
- *
- * Properties [[function]] and [[marker]] are optional,
- * but at least one of the two must be set.
- */
-export type Location = {
- fct?: string;
- marker?: Ast.marker;
-};
+/**
+ A global Ivette selection.
-export interface HistorySelection {
- /** Previous locations with respect to the [[current]] one. */
- prevSelections: Location[];
- /** Next locations with respect to the [[current]] one. */
- nextSelections: Location[];
-}
+ There is no expected relation between the current marker and declaration:
-/** Actions on history selections:
- * - `HISTORY_PREV` jumps to previous history location
- * (first in [[prevSelections]]).
- * - `HISTORY_NEXT` jumps to next history location
- * (first in [[nextSelections]]).
- */
-export type HistorySelectActions = 'HISTORY_PREV' | 'HISTORY_NEXT';
+ - current marker is used to synchronize selection in components;
+ - current declaration is used to synchronize filtering in components;
+ - some components might display markers from different declarations.
-/** A selection of multiple locations. */
-export interface MultipleSelection {
- /** Name of the multiple selection. */
- name: string;
- /** Explanatory description of the multiple selection. */
- title: string;
- /** The index of the current selected location in [[allSelections]]. */
- index: number;
- /** All locations forming a multiple selection. */
- allSelections: Location[];
-}
-
-/** A select action on multiple locations. */
-export interface MultipleSelect {
- readonly name: string;
- readonly title: string;
- readonly index: number;
- readonly locations: Location[];
-}
-
-/** Select the [[index]]-nth location of the current multiple selection. */
-export interface NthSelect {
- readonly index: number;
-}
-
-/** Actions on multiple selections:
- * - [[MultipleSelect]].
- * - [[NthSelect]].
- * - `MULTIPLE_PREV` jumps to previous location of the multiple selections.
- * - `MULTIPLE_NEXT` jumps to next location of the multiple selections.
- * - `MULTIPLE_CYCLE` cycles between the multiple selections.
- * - `MULTIPLE_CLEAR` clears the multiple selection.
- */
-export type MultipleSelectActions =
- MultipleSelect | NthSelect
- | 'MULTIPLE_PREV' | 'MULTIPLE_NEXT' | 'MULTIPLE_CYCLE' | 'MULTIPLE_CLEAR';
+*/
+export interface Location {
+ decl?: Ast.decl;
+ marker?: Ast.marker;
+}
+/** Global current selection & history. */
export interface Selection {
- /** Current selection. May be one in [[history]] or [[multiple]]. */
- current?: Location;
- /** History of selections. */
- history: HistorySelection;
- /** Multiple selections at once. */
- multiple: MultipleSelection;
+ curr: Location; // might be empty
+ prev: Location[]; // last first, no empty locs
+ next: Location[]; // next first, no empty locs
}
-/** A select action on a location. */
-export interface SingleSelect {
- readonly location: Location;
-}
+const emptySelection: Selection = { curr: {}, prev: [], next: [] };
+const isEmpty = (l: Location): boolean => (!l.decl && !l.marker);
+const pushLoc = (l: Location, ls: Location[]): Location[] =>
+ (isEmpty(l) ? ls : [l, ...ls]);
-/** Actions on selection:
- * - [[SingleSelect]].
- * - [[HistorySelectActions]].
- * - [[MultipleSelectActions]].
- */
-export type SelectionActions =
- SingleSelect | HistorySelectActions | MultipleSelectActions;
+export type Hovered = Ast.marker | undefined
+export const MetaSelection = new Dome.Event<Location>('frama-c-meta-selection');
+export const GlobalHovered = new GlobalState<Hovered>(undefined);
+export const GlobalSelection = new GlobalState<Selection>(emptySelection);
-function isSingleSelect(a: SelectionActions): a is SingleSelect {
- return (a as SingleSelect).location !== undefined;
-}
+Server.onShutdown(() => GlobalSelection.setValue(emptySelection));
-function isMultipleSelect(a: SelectionActions): a is MultipleSelect {
- return (
- (a as MultipleSelect).locations !== undefined &&
- (a as MultipleSelect).index !== undefined
- );
+export function setHovered(h: Hovered = undefined): void {
+ GlobalHovered.setValue(h);
}
-function isNthSelect(a: SelectionActions): a is NthSelect {
- return (a as NthSelect).index !== undefined;
+export function useHovered(): Hovered {
+ const [h] = useGlobalState(GlobalHovered);
+ return h;
}
-/** Update selection to the given location. */
-function selectLocation(s: Selection, location: Location): Selection {
- const [prevSelections, nextSelections] =
- s.current && s.current.fct !== location.fct ?
- [[s.current, ...s.history.prevSelections], []] :
- [s.history.prevSelections, s.history.nextSelections];
- return {
- ...s,
- current: location,
- history: { prevSelections, nextSelections },
- };
+export function useSelection(): Selection {
+ const [current] = useGlobalState(GlobalSelection);
+ return current;
}
-/** Compute the next selection picking from the current history, depending on
- * action.
- */
-function fromHistory(s: Selection, action: HistorySelectActions): Selection {
- switch (action) {
- case 'HISTORY_PREV': {
- const [pS, ...prevS] = s.history.prevSelections;
- return {
- ...s,
- current: pS,
- history: {
- prevSelections: prevS,
- nextSelections:
- [(s.current as Location), ...s.history.nextSelections],
- },
- };
- }
- case 'HISTORY_NEXT': {
- const [nS, ...nextS] = s.history.nextSelections;
- return {
- ...s,
- current: nS,
- history: {
- prevSelections:
- [(s.current as Location), ...s.history.prevSelections],
- nextSelections: nextS,
- },
- };
- }
- default:
- return s;
- }
+export function clearSelection(): void {
+ GlobalHovered.setValue(undefined);
+ GlobalSelection.setValue(emptySelection);
}
-/** Compute the next selection picking from the current multiple, depending on
- * action.
- */
-function fromMultipleSelections(
- s: Selection,
- a: 'MULTIPLE_PREV' | 'MULTIPLE_NEXT' | 'MULTIPLE_CYCLE' | 'MULTIPLE_CLEAR',
-): Selection {
- switch (a) {
- case 'MULTIPLE_PREV':
- case 'MULTIPLE_NEXT':
- case 'MULTIPLE_CYCLE': {
- const idx =
- a === 'MULTIPLE_PREV' ?
- s.multiple.index - 1 :
- s.multiple.index + 1;
- const index =
- a === 'MULTIPLE_CYCLE' && idx >= s.multiple.allSelections.length ?
- 0 :
- idx;
- if (0 <= index && index < s.multiple.allSelections.length) {
- const multiple = { ...s.multiple, index };
- return selectLocation(
- { ...s, multiple },
- s.multiple.allSelections[index],
- );
- }
- return s;
- }
- case 'MULTIPLE_CLEAR':
- return {
- ...s,
- multiple: {
- name: '',
- title: '',
- index: 0,
- allSelections: [],
- },
- };
- default:
- return s;
- }
+export function getCurrent(): Location {
+ return GlobalSelection.getValue().curr;
}
-/** Compute the next selection based on the current one and the given action. */
-function reducer(s: Selection, action: SelectionActions): Selection {
- if (isSingleSelect(action)) {
- return selectLocation(s, action.location);
- }
- if (isMultipleSelect(action)) {
- const index = action.index > 0 ? action.index : 0;
- const selection =
- action.locations.length === 0 ? s :
- selectLocation(s, action.locations[index]);
- return {
- ...selection,
- multiple: {
- name: action.name,
- title: action.title,
- allSelections: action.locations,
- index,
- },
- };
- }
- if (isNthSelect(action)) {
- const { index } = action;
- if (0 <= index && index < s.multiple.allSelections.length) {
- const location = s?.multiple.allSelections[index];
- const selection = selectLocation(s, location);
- const multiple = { ...selection.multiple, index };
- return { ...selection, multiple };
- }
- return s;
- }
- switch (action) {
- case 'HISTORY_PREV':
- case 'HISTORY_NEXT':
- return fromHistory(s, action);
- case 'MULTIPLE_PREV':
- case 'MULTIPLE_NEXT':
- case 'MULTIPLE_CYCLE':
- case 'MULTIPLE_CLEAR':
- return fromMultipleSelections(s, action);
- default:
- return s;
- }
+export function useCurrent(): Location {
+ const [{ curr }] = useGlobalState(GlobalSelection);
+ return curr;
}
-/** The initial selection is empty. */
-const emptySelection = {
- current: undefined,
- history: {
- prevSelections: [],
- nextSelections: [],
- },
- multiple: {
- name: '',
- title: '',
- index: 0,
- allSelections: [],
- },
-};
+/** Move both current declaration and marker. */
+export function setCurrent(l: Location, meta = false): void {
+ const s = GlobalSelection.getValue();
+ const empty = isEmpty(l);
+ GlobalSelection.setValue({
+ curr: l,
+ next: empty ? s.next : [],
+ prev: pushLoc(s.curr, s.prev)
+ });
+ if (meta && !empty) MetaSelection.emit(l);
+}
-export type Hovered = Location | undefined;
-export const MetaSelection = new Dome.Event<Location>('frama-c-meta-selection');
-export const GlobalHovered = new GlobalState<Hovered>(undefined);
-export const GlobalSelection = new GlobalState<Selection>(emptySelection);
+/** Move to marker in current declaration. */
+export function gotoLocalMarker(
+ marker : Ast.marker | undefined,
+ meta = false
+): void
+{
+ const s = GlobalSelection.getValue();
+ setCurrent({ decl: s.curr.decl, marker }, meta);
+}
-Server.onShutdown(() => GlobalSelection.setValue(emptySelection));
+/** Move to marker in its own declaration (if any). */
+export function gotoGlobalMarker(marker : Ast.marker, meta = false): void
+{
+ const st = currentSyncArray(Ast.markerAttributes);
+ const attr = st.model.getData(marker);
+ const decl = attr?.decl;
+ if (decl) setCurrent({ decl, marker }, meta);
+ else gotoLocalMarker(marker, meta);
+}
-export function setHovered(h: Hovered): void { GlobalHovered.setValue(h); }
-export function useHovered(): [Hovered, (h: Hovered) => void] {
- return useGlobalState(GlobalHovered);
+/** Move to declaration. */
+export function gotoDeclaration(decl: Ast.decl | undefined): void
+{
+ setCurrent({ decl });
}
-export function setSelection(location: Location, meta = false): void {
+/** Move forward in history. */
+export function gotoNext(): void {
const s = GlobalSelection.getValue();
- GlobalSelection.setValue(reducer(s, { location }));
- if (meta) MetaSelection.emit(location);
-}
-
-/** Current selection. */
-export function useSelection(): [Selection, (a: SelectionActions) => void] {
- const [current, setCurrent] = useGlobalState(GlobalSelection);
- const callback = React.useCallback((action) => {
- setCurrent(reducer(current, action));
- if (isMultipleSelect(action)) {
- const l = action.locations.length;
- const markers =
- (l > 1) ? `${l} markers selected, listed in the 'Locations' panel` :
- (l === 1) ? `1 marker selected` : `no markers selected`;
- const text = `${action.name}: ${markers}`;
- Status.setMessage({ text, title: action.title, kind: 'success' });
- }
- }, [current, setCurrent]);
- return [current, callback];
+ if (s.next.length > 0) {
+ const [curr, ...next] = s.next;
+ GlobalSelection.setValue({ curr, next, prev: pushLoc(s.curr, s.prev) });
+ }
}
-/** Resets the selected locations. */
-export async function resetSelection(): Promise<void> {
- GlobalSelection.setValue(emptySelection);
- if (Server.isRunning()) {
- try {
- const main = await Server.send(Ast.getMainFunction, {});
- // If the selection has already been modified, do not change it.
- if (main && GlobalSelection.getValue() === emptySelection) {
- GlobalSelection.setValue({ ...emptySelection, current: { fct: main } });
- }
- } catch (err) {
- if (err) D.warn('Request error', err);
- }
+/** Move backward in history. */
+export function gotoPrev(): void {
+ const s = GlobalSelection.getValue();
+ if (s.prev.length > 0) {
+ const [curr, ...prev] = s.prev;
+ GlobalSelection.setValue({ curr, next: pushLoc(s.curr, s.next), prev });
}
}
+// --------------------------------------------------------------------------
+// --- Declarations
+// --------------------------------------------------------------------------
+
+export type declaration = Ast.declAttributesData;
+
+/** Access the marker attributes from AST. */
+export function useDeclaration(decl: Ast.decl | undefined): declaration {
+ const data = useSyncArrayElt(Ast.declAttributes, decl);
+ return data ?? Ast.declAttributesDataDefault;
+}
+
// --------------------------------------------------------------------------
// --- Markers
// --------------------------------------------------------------------------
@@ -826,8 +656,8 @@ export type attributes = Ast.markerAttributesData;
/** Access the marker attributes from AST. */
export function useMarker(marker: Ast.marker | undefined): attributes {
- const marks = useSyncArrayElt(Ast.markerAttributes, marker);
- return marks ?? Ast.markerAttributesDataDefault;
+ const data = useSyncArrayElt(Ast.markerAttributes, marker);
+ return data ?? Ast.markerAttributesDataDefault;
}
// --------------------------------------------------------------------------
@@ -835,8 +665,9 @@ export function useMarker(marker: Ast.marker | undefined): attributes {
// --------------------------------------------------------------------------
Server.onReady(() => {
- if (GlobalSelection.getValue() === emptySelection)
- resetSelection();
+ const s = GlobalSelection.getValue();
+ if (s.curr.decl || s.curr.marker || s.next.length > 0 || s.prev.length > 0)
+ clearSelection();
});
// --------------------------------------------------------------------------
diff --git a/src/plugins/callgraph/requests.ml b/src/plugins/callgraph/requests.ml
index cdef7f503d12adab16126d22d094cecf24057518..271a267483bab1b4fa452479bca6d5e675feec83 100644
--- a/src/plugins/callgraph/requests.ml
+++ b/src/plugins/callgraph/requests.ml
@@ -62,6 +62,8 @@ struct
let kf = field "kf" (module Kernel_ast.Function)
~descr: "The function represented by the node"
+ let decl = field "decl" (module Kernel_ast.Decl)
+ ~descr: "The declaration tag of the function"
let is_root = field "is_root" Data.jbool
~descr: "whether this node is the root of a service"
let root = field "root" (module Kernel_ast.Function)
@@ -73,6 +75,7 @@ struct
let to_json (v : Cil_types.kernel_function Service_graph.vertex) =
default |>
set kf v.node |>
+ set decl (Printer_tag.SFunction v.node) |>
set is_root v.is_root |>
set root v.root.node |>
to_json
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 253ac2362367a0b8341fda7800501bf2c22cbf7e..6e70920e0bbe1a7c14b8af476ca714e87559c369 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -726,10 +726,15 @@ let _computed_signal =
~add_hook:(Analysis.register_computation_hook ~on:Computed)
()
-let _array =
+let _functionStats =
let open Summary in
let model = States.model () in
+ States.column model ~name:"decl"
+ ~descr:(Markdown.plain "Function declaration tag")
+ ~data:(module Kernel_ast.Decl)
+ ~get:(fun (kf,_) -> Printer_tag.SFunction (Globals.Functions.get kf.svar));
+
States.column model ~name:"coverage"
~descr:(Markdown.plain "Coverage of the Eva analysis")
~data:(module Coverage)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index bb94478eefd95988adbd74d7673b9888bab12a08..cac14e656a3da1108eacc5de9499dad20c748474 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -674,6 +674,11 @@ struct
let array : kernel_function States.array =
begin
let model = States.model () in
+ States.column model
+ ~name:"decl"
+ ~descr:(Md.plain "Declaration Tag")
+ ~data:(module Decl)
+ ~get:(fun kf -> Printer_tag.SFunction kf) ;
States.column model
~name:"name"
~descr:(Md.plain "Name")
@@ -944,14 +949,12 @@ let () = Server_parameters.Debug.add_hook_on_update
(* --- Marker at a position --- *)
(* -------------------------------------------------------------------------- *)
-let get_kf_marker (file, line, col) =
+let get_marker_at ~file ~line ~col =
let pos_path = Filepath.Normalized.of_string file in
let pos =
Filepath.{ pos_path; pos_lnum = line; pos_cnum = col; pos_bol = 0; }
in
- let tag = Printer_tag.loc_to_localizable ~precise_col:true pos in
- let kf = Option.bind tag Printer_tag.kf_of_localizable in
- kf, tag
+ Printer_tag.loc_to_localizable ~precise_col:true pos
let () =
let descr =
@@ -959,11 +962,19 @@ let () =
"Returns the marker and function at a source file position, if any. \
Input: file path, line and column."
in
- Request.register
+ let signature = Request.signature
+ ~output:(module Joption(Marker)) () in
+ let get_file = Request.param signature
+ ~name:"file" ~descr:(Md.plain "File path") (module Jstring) in
+ let get_line = Request.param signature
+ ~name:"line" ~descr:(Md.plain "Line number") (module Jint) in
+ let get_col = Request.param signature
+ ~name:"column" ~descr:(Md.plain "Column number") (module Jint) in
+ Request.register_sig signature
~package ~descr ~kind:`GET ~name:"getMarkerAt"
- ~input:(module Jtriple (Jstring) (Jint) (Jint))
- ~output:(module Jpair (Joption (Function)) (Joption (Marker)))
- get_kf_marker
+ ~signals:[ast_changed_signal]
+ (fun rq () ->
+ get_marker_at ~file:(get_file rq) ~line:(get_line rq) ~col:(get_col rq))
(* -------------------------------------------------------------------------- *)
(* --- Files --- *)
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index aacea649733aa9527bff607439a5a6fc0e809712..03757b20ba614f2a8e932b9b049cad901adb4254 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -152,18 +152,18 @@ let () = States.option model ~name:"source"
let getMarker (evt, _id) =
Option.bind evt.Log.evt_source Printer_tag.loc_to_localizable
-let getFunction t =
- Option.bind (getMarker t) Printer_tag.kf_of_localizable
+let getDecl t =
+ Option.bind (getMarker t) Printer_tag.declaration_of_localizable
let () = States.option model ~name:"marker"
~descr:(Md.plain "Marker at the message position (if any)")
~data:(module Kernel_ast.Marker)
~get:getMarker
-let () = States.option model ~name:"fct"
- ~descr:(Md.plain "Function containing the message position (if any)")
- ~data:(module Kernel_ast.Function)
- ~get:getFunction
+let () = States.option model ~name:"decl"
+ ~descr:(Md.plain "Declaration containing the message position (if any)")
+ ~data:(module Kernel_ast.Decl)
+ ~get:getDecl
let iter f = ignore (Messages.fold (fun i evt -> f (evt, i); succ i) 0)
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 7f63a336980f8575a3242a71d7de1da0c6ba13d1..12fd4a74c07e9d55ff69f37261ed6a2308e9cba0 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -169,6 +169,10 @@ let () = R.register ~package ~kind:`GET ~name:"getAvailableProvers"
let gmodel : Wpo.t S.model = S.model ()
+let get_decl g = match g.Wpo.po_idx with
+ | Function(kf,_) -> Some (Printer_tag.SFunction kf)
+ | Axiomatic _ -> None (* TODO *)
+
let get_kf g = match g.Wpo.po_idx with
| Function(kf,_) -> Some kf
| Axiomatic _ -> None
@@ -192,6 +196,10 @@ let () = S.column gmodel ~name:"property"
~data:(module AST.Marker)
~get:(fun g -> Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid))
+let () = S.column gmodel ~name:"scope"
+ ~descr:(Md.plain "Associated declaration, if any")
+ ~data:(module D.Joption(AST.Decl)) ~get:get_decl
+
let () = S.column gmodel ~name:"fct"
~descr:(Md.plain "Associated function, if any")
~data:(module D.Joption(AST.Function)) ~get:get_kf