diff --git a/Makefile b/Makefile
index 9ac4b7b5859219d91b6ae626e9d62f0332fe8331..bc1699b5bd89bed03d5b51c0c53d5372c69b24f1 100644
--- a/Makefile
+++ b/Makefile
@@ -914,8 +914,8 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
engine/compute_functions engine/analysis register \
domains/taint_domain \
$(APRON_CMO) $(NUMERORS_CMO) \
- api/general_requests api/values_request \
- utils/unit_tests utils/results
+ utils/results api/general_requests api/values_request \
+ utils/unit_tests
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Server
diff --git a/ivette/Makefile.distrib b/ivette/Makefile.distrib
index d4eeff9d4e3f8d69a886b74a1997bcfe70d8feb5..87068f0322f67cc1f5c8ab9c6f920bfad9e9c91d 100644
--- a/ivette/Makefile.distrib
+++ b/ivette/Makefile.distrib
@@ -192,9 +192,9 @@ DISTRIB_FILES += ivette/src/frama-c/plugins/eva/valuetable.tsx
DISTRIB_FILES += ivette/src/frama-c/plugins/pivot/api/general/index.ts
DISTRIB_FILES += ivette/src/frama-c/plugins/studia/api/studia/index.ts
DISTRIB_FILES += ivette/src/frama-c/react-pivottable.d.ts
+DISTRIB_FILES += ivette/src/frama-c/richtext.tsx
DISTRIB_FILES += ivette/src/frama-c/server.ts
DISTRIB_FILES += ivette/src/frama-c/states.ts
-DISTRIB_FILES += ivette/src/frama-c/utils.ts
DISTRIB_FILES += ivette/src/ivette/index.tsx
DISTRIB_FILES += ivette/src/ivette/prefs.tsx
DISTRIB_FILES += ivette/src/ivette/sandbox.tsx
diff --git a/ivette/headers/header_spec.txt b/ivette/headers/header_spec.txt
index e4d41f1530f1c839dd642385123045132d425cc2..75e97fe5eb7d202f311cc244e23d696311dd3544 100644
--- a/ivette/headers/header_spec.txt
+++ b/ivette/headers/header_spec.txt
@@ -192,9 +192,9 @@ src/frama-c/plugins/eva/valuetable.tsx: CEA_LGPL
src/frama-c/plugins/pivot/api/general/index.ts: CEA_LGPL
src/frama-c/plugins/studia/api/studia/index.ts: CEA_LGPL
src/frama-c/react-pivottable.d.ts: CEA_LGPL
+src/frama-c/richtext.tsx: CEA_LGPL
src/frama-c/server.ts: CEA_LGPL
src/frama-c/states.ts: CEA_LGPL
-src/frama-c/utils.ts: CEA_LGPL
src/ivette/index.tsx: CEA_LGPL
src/ivette/prefs.tsx: CEA_LGPL
src/ivette/sandbox.tsx: CEA_LGPL
diff --git a/ivette/src/dome/renderer/data/settings.ts b/ivette/src/dome/renderer/data/settings.ts
index 4421943d26bd8d03cbb1626e8743950bd3b95566..585fe1405557d4015898dcea5ca6bd0428bd2cfa 100644
--- a/ivette/src/dome/renderer/data/settings.ts
+++ b/ivette/src/dome/renderer/data/settings.ts
@@ -248,26 +248,29 @@ function useSettings<A>(
D: Driver,
K?: string,
): State<A> {
- // Load value
- const loader = () => (
+ // Local State
+ const [value, setValue] = React.useState<A>(() => (
JSON.jCatch(S.decoder, S.defaultValue)(D.load(K))
- );
- // Local state
- const [value, setValue] = React.useState<A>(loader);
- // Emit update event
+ ));
+ // Foreign Settings Update
React.useEffect(() => {
const event = D.evt;
- const callback = () => setValue(loader());
- SysEmitter.on(event, callback);
- return () => { SysEmitter.off(event, callback); };
+ const onUpdate = () => {
+ const fromSettings = JSON.jCatch(S.decoder, undefined)(D.load(K));
+ if (fromSettings !== undefined)
+ setValue(fromSettings);
+ };
+ SysEmitter.on(event, onUpdate);
+ return () => { SysEmitter.off(event, onUpdate); };
});
- // Updates
+ // Hooked Settings Update
const updateValue = React.useCallback((newValue: A) => {
if (!isEqual(value, newValue)) {
setValue(newValue);
if (K) D.save(K, S.encoder(newValue));
}
}, [S, D, K, value]);
+ // Hook
return [value, updateValue];
}
diff --git a/ivette/src/dome/renderer/dome.tsx b/ivette/src/dome/renderer/dome.tsx
index 1770a29b7f2d5412424b59ab9fcdcd04940ed798..2b083a73ee982c656767deb4ec20b2d9829b2af2 100644
--- a/ivette/src/dome/renderer/dome.tsx
+++ b/ivette/src/dome/renderer/dome.tsx
@@ -173,7 +173,7 @@ export function useEvent<A>(
return () => evt.off(callback);
}
return undefined;
- });
+ }, [evt, callback]);
}
// --------------------------------------------------------------------------
@@ -704,11 +704,7 @@ export function useFlipSettings(
const [state, setState] = Settings.useWindowSettings(
key, Json.jBoolean, defaultValue,
);
- const flipState = React.useCallback(
- () => setState(!state),
- [state, setState],
- );
- return [state, flipState];
+ return [state, () => setState(!state)];
}
/** Number window settings helper. Default is `0` unless specified. */
diff --git a/ivette/src/dome/renderer/text/editors.tsx b/ivette/src/dome/renderer/text/editors.tsx
index 43df5396e92fe069852ce49cdfa8aab940e908ef..deea5d38e582dcf11ae9b182f3f57d4938e59b0d 100644
--- a/ivette/src/dome/renderer/text/editors.tsx
+++ b/ivette/src/dome/renderer/text/editors.tsx
@@ -72,6 +72,9 @@ export interface TextProps extends CodeMirror.EditorConfiguration {
/** The currently selected marker identifier. */
selection?: string;
+ /** Callback on hovered marker, if some. */
+ onHover?: (id?: string) => void;
+
/** Callback on identified marker selection. */
onSelection?: MarkerCallback;
@@ -311,6 +314,8 @@ class CodeMirrorWrapper extends React.Component<TextProps> {
if (newMarker && newMarker.hover)
this._markElementsWith(newMarker.classNameId, CSS_HOVERED);
this.marker = newMarker;
+ const callback = this.props.onHover;
+ if (callback) callback(newMarker?.id);
}
}
@@ -479,6 +484,7 @@ class CodeMirrorWrapper extends React.Component<TextProps> {
onFocus={this.onFocus}
onScroll={this.onScroll}
onMouseMove={this.onMouseMove}
+ onMouseLeave={this.onMouseMove}
/>
);
}
diff --git a/ivette/src/frama-c/api_generator.ml b/ivette/src/frama-c/api_generator.ml
index 371495e164343380571b7490cc496fffbb2b4302..b72055204a8002d9e3778a336fd422f14d2f6e69 100644
--- a/ivette/src/frama-c/api_generator.ml
+++ b/ivette/src/frama-c/api_generator.ml
@@ -349,8 +349,9 @@ let makeDeclaration fmt names d =
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident d.d_ident) ;
Format.fprintf fmt " input: %a,@\n" makeParam input ;
Format.fprintf fmt " output: %a,@\n" makeParam output ;
- Format.fprintf fmt " signals: [%a],@\n"
- (Pretty_utils.pp_list ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]"
+ Format.fprintf fmt " signals: %a,@\n"
+ (Pretty_utils.pp_list
+ ~empty:"[]" ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]"
(fun fmt s -> Format.fprintf fmt "{ name: '%s' }" s))
rq.rq_signals;
Format.fprintf fmt "};@\n" ;
diff --git a/ivette/src/frama-c/index.tsx b/ivette/src/frama-c/index.tsx
index 9c3e42d30e134a2a68a0eeb39d2357abfc9aa23c..171fbe23f912103aca11d18cb28e0add4fb7d2e0 100644
--- a/ivette/src/frama-c/index.tsx
+++ b/ivette/src/frama-c/index.tsx
@@ -55,18 +55,18 @@ Ivette.registerGroup({
Ivette.registerSidebar({ id: 'frama-c.globals', children: <Globals /> });
Ivette.registerToolbar({ id: 'frama-c.history', children: <History /> });
Ivette.registerStatusbar({ id: 'frama-c.message', children: <Status /> });
+ Ivette.registerComponent({
+ id: 'frama-c.astinfo',
+ label: 'Inspector',
+ title: 'Contextual information on selected AST elements',
+ children: <ASTinfo />
+ });
Ivette.registerComponent({
id: 'frama-c.astview',
label: 'AST',
title: 'Normalized C/ACSL Source Code',
children: <ASTview />,
});
- Ivette.registerComponent({
- id: 'frama-c.astinfo',
- label: 'Informations',
- title: 'Informations on currently selected item',
- children: <ASTinfo />,
- });
Ivette.registerComponent({
id: 'frama-c.sourcecode',
label: 'Source Code',
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 928411368bdae0c159d30feae7ece4330b2bd0c0..8eeff601e8c0a51ecd5b6460654bccddf4ce9e49 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -25,49 +25,345 @@
// --------------------------------------------------------------------------
import React from 'react';
+import * as Dome from 'dome';
+import { classes } from 'dome/misc/utils';
import * as States from 'frama-c/states';
-import * as Utils from 'frama-c/utils';
+import * as DATA from 'frama-c/kernel/api/data';
+import * as AST from 'frama-c/kernel/api/ast';
+import { Text } from 'frama-c/richtext';
+import { Icon } from 'dome/controls/icons';
+import { Code } from 'dome/controls/labels';
+import { IconButton } from 'dome/controls/buttons';
+import * as Boxes from 'dome/layout/boxes';
+import { TitleBar } from 'ivette';
-import { Vfill } from 'dome/layout/boxes';
-import { RichTextBuffer } from 'dome/text/buffers';
-import { Text } from 'dome/text/editors';
-import { getInfo } from 'frama-c/kernel/api/ast';
+// --------------------------------------------------------------------------
+// --- Marker Kinds
+// --------------------------------------------------------------------------
+
+import Kind = AST.markerKind;
+import Var = AST.markerVar
+
+function getMarkerKind (props: AST.markerInfoData): [string, string] {
+ switch (props.kind) {
+ case Kind.declaration:
+ switch (props.var) {
+ case Var.function: return ["Declaration", "Function declaration"];
+ case Var.variable: return ["Declaration", "Variable declaration"];
+ case Var.none: return ["Declaration", "Declaration"];
+ }
+ break;
+ case Kind.global: return ["Global", "Global declaration or definition"];
+ case Kind.lvalue:
+ switch (props.var) {
+ case Var.function: return ["Function", "Function"];
+ case Var.variable: return ["Variable", "C variable"];
+ case Var.none: return ["Lvalue", "C lvalue"];
+ }
+ break;
+ case Kind.expression: return ["Expression", "C expression"];
+ case Kind.statement: return ["Statement", "C statement"];
+ case Kind.property: return ["Property", "ACSL property"];
+ case Kind.term: return ["Term", "ACSL term"];
+ }
+}
+
+function markerKind (props: AST.markerInfoData): JSX.Element {
+ const [label, title] = getMarkerKind(props);
+ return <span className="astinfo-markerkind" title={title}>{label}</span>;
+}
// --------------------------------------------------------------------------
-// --- Information Panel
+// --- Information Details
// --------------------------------------------------------------------------
-export default function ASTinfo(): JSX.Element {
+interface InfoItemProps {
+ label: string;
+ title: string;
+ descr: DATA.text;
+}
- const buffer = React.useMemo(() => new RichTextBuffer(), []);
- const [selection, updateSelection] = States.useSelection();
- const marker = selection?.current?.marker;
- const data = States.useRequest(getInfo, marker);
+function InfoItem(props: InfoItemProps): JSX.Element {
+ return (
+ <div className="astinfo-infos">
+ <div
+ className="dome-text-label astinfo-kind"
+ title={props.title}
+ >
+ {props.label}
+ </div>
+ <div className="dome-text-cell astinfo-data">
+ <Text text={props.descr} />
+ </div>
+ </div>
+ );
+}
- React.useEffect(() => {
- buffer.clear();
- const style = { css: 'color: var(--text-highlighted)' };
- if (data) Utils.printTextWithTags(buffer, data, style);
- }, [buffer, data]);
-
- // Callbacks
- function onTextSelection(id: string): void {
- // For now, the only markers are functions.
- const location = { fct: id };
- updateSelection({ location });
+interface ASTinfos {
+ id: string;
+ label: string;
+ title: string;
+ descr: DATA.text;
+}
+
+interface InfoSectionProps {
+ marker: AST.marker;
+ markerInfo: AST.markerInfoData;
+ filter: string;
+ selected: boolean;
+ hovered: boolean;
+ pinned: boolean;
+ onPin: () => void;
+ onHover: (hover: boolean) => void;
+ onSelect: () => void;
+ onRemove: () => void;
+}
+
+function MarkInfos(props: InfoSectionProps): JSX.Element {
+ const [unfold, setUnfold] = React.useState(true);
+ const [more, setMore] = React.useState(false);
+ const { marker, markerInfo } = props;
+ const allInfos: ASTinfos[] =
+ States.useRequest(AST.getInformation, marker) ?? [];
+ const highlight = classes(
+ props.selected && 'selected',
+ props.hovered && 'hovered',
+ );
+ const descr = markerInfo.descr ?? markerInfo.name;
+ const kind = markerKind(markerInfo);
+ const fs = props.filter.split(':');
+ const filtered = allInfos.filter((info) => !fs.some((m) => m === info.id));
+ const infos = more ? allInfos : filtered;
+ const hasMore = filtered.length < allInfos.length;
+ const pinButton =
+ (!props.pinned || props.selected) ?
+ {
+ icon: "PIN", selected: props.pinned, onClick: props.onPin,
+ title: "Pin/unpin marker information"
+ } : {
+ icon: "CIRC.CLOSE", onClick: props.onRemove,
+ title:"Remove marker information"
+ };
+ return (
+ <div
+ className={`astinfo-section ${highlight}`}
+ onMouseEnter={() => props.onHover(true)}
+ onMouseLeave={() => props.onHover(false)}
+ onDoubleClick={props.onSelect}
+ >
+ <div
+ key="MARKER"
+ className={`astinfo-markerbar ${highlight}`}
+ title={descr}
+ >
+ <Icon
+ className="astinfo-folderbutton"
+ style={{ visibility: infos.length ? 'visible' : 'hidden' }}
+ size={9}
+ offset={-2}
+ id={unfold ? 'TRIANGLE.DOWN' : 'TRIANGLE.RIGHT'}
+ onClick={() => setUnfold(!unfold)}
+ />
+ <Code className="astinfo-markercode">
+ {kind}{descr}
+ </Code>
+ <IconButton
+ style={{ display: hasMore ? undefined : 'none' }}
+ className="astinfo-markerbutton"
+ title="Show all available information"
+ size={9}
+ offset={0}
+ icon="CIRC.PLUS"
+ selected={more}
+ onClick={() => setMore(!more)}
+ />
+ <IconButton
+ className="astinfo-markerbutton"
+ size={9}
+ offset={0}
+ {...pinButton}
+ />
+ </div>
+ {unfold && infos.map((info) => <InfoItem key={info.id} {...info} />)}
+ </div>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Information Selection State
+// --------------------------------------------------------------------------
+
+type Mark = { fct: string; marker: AST.marker };
+
+const reload = new Dome.Event('frama-c.astinfo');
+
+class InfoMarkers {
+
+ private selection: Mark[] = [];
+ private mSelected: AST.marker | undefined;
+ private mHovered: AST.marker | undefined;
+ private pinned = new Set<string>();
+
+ isPinned(marker: AST.marker): boolean {
+ return this.pinned.has(marker);
+ }
+
+ setPinned(marker: AST.marker, pinned: boolean): void {
+ const oldpin = this.isPinned(marker);
+ if (oldpin !== pinned) {
+ if (pinned)
+ this.pinned.add(marker);
+ else
+ this.pinned.delete(marker);
+ reload.emit();
+ }
}
- // Component
+ addMarker(s: Mark[], marker: AST.marker, fct: string): Mark[] {
+ if (s.some((m) => m.marker === marker))
+ return s;
+ else
+ return s.concat({ marker, fct });
+ }
+
+ setLocations(
+ selected: States.Location | undefined,
+ hovered: States.Location | undefined
+ ): void {
+ const sm = selected?.marker;
+ const sf = selected?.fct;
+ const hm = hovered?.marker;
+ const hf = hovered?.fct;
+ const s0 = this.mSelected;
+ const h0 = this.mHovered;
+ let s = this.selection.filter((mark): boolean => {
+ const m = mark.marker;
+ return this.isPinned(m) || (m !== s0 && m !== h0);
+ });
+ if (sm && sf) s = this.addMarker(s, sm, sf);
+ if (hm && hf) s = this.addMarker(s, hm, hf);
+ this.selection = s;
+ this.mSelected = sm;
+ this.mHovered = hm;
+ reload.emit();
+ }
+
+ removeMarker(marker: AST.marker): void {
+ if (marker === this.mSelected) this.mSelected = undefined;
+ if (marker === this.mHovered) this.mHovered = undefined;
+ this.selection = this.selection.filter((m) => m.marker !== marker);
+ this.pinned.delete(marker);
+ reload.emit();
+ }
+
+ getSelected(): Mark[] { return this.selection; }
+
+}
+
+// --------------------------------------------------------------------------
+// --- Context Menu Filter
+// --------------------------------------------------------------------------
+
+function openFilter(
+ infos: ASTinfos[],
+ filter: string,
+ onChange: (f: string) => void,
+): void {
+ const fs = filter.split(':');
+ const menuItems = infos.map((info) => {
+ const checked = !fs.some((m) => m === info.id);
+ const onClick = (): void => {
+ const newFs =
+ checked
+ ? fs.concat(info.id)
+ : fs.filter((m) => m !== info.id);
+ onChange(newFs.join(':'));
+ };
+ return {
+ id: info.id,
+ label: `${info.title} (${info.label})`,
+ checked,
+ onClick,
+ };
+ });
+ Dome.popupMenu(menuItems);
+ return;
+}
+
+// --------------------------------------------------------------------------
+// --- Information Panel
+// --------------------------------------------------------------------------
+
+export default function ASTinfo(): JSX.Element {
+ // Hooks
+ Dome.useUpdate(reload);
+ const markers = React.useMemo(() => new InfoMarkers(), []);
+ const markerInfos = States.useSyncArray(AST.markerInfo, false);
+ const [selection] = States.useSelection();
+ const [hoveredLoc] = States.useHovered();
+ const information = States.useRequest(AST.getInformation, null) ?? [];
+ const [filter, setFilter] =
+ Dome.useStringSettings('frama-c.sidebar.astinfo.filter', '');
+ const selectedLoc = selection?.current;
+ const selected = selectedLoc?.marker;
+ const hovered = hoveredLoc?.marker;
+ React.useEffect(() => {
+ markers.setLocations(selectedLoc, hoveredLoc);
+ }, [markers, selectedLoc, hoveredLoc]);
+ const pinMarker = React.useCallback((location: States.Location) => {
+ if (location?.marker)
+ markers.setPinned(location?.marker, true);
+ }, [markers]);
+ React.useEffect(() => {
+ States.MetaSelection.on(pinMarker);
+ return () => States.MetaSelection.off(pinMarker);
+ }, [pinMarker]);
+ const scrollTarget = React.useRef<HTMLInputElement>(null);
+ React.useEffect(() => {
+ scrollTarget.current?.scrollIntoView({ block: 'nearest' });
+ });
+ // Rendering
+ const renderMark = (mark: Mark): JSX.Element | null => {
+ const { marker } = mark;
+ const markerInfo = markerInfos.getData(marker);
+ if (!markerInfo) return null;
+ const pinned = markers.isPinned(marker);
+ const isSelected = selected === marker;
+ const isHovered = hovered === marker;
+ const onPin = () => void markers.setPinned(marker, !pinned);
+ const onRemove = () => void markers.removeMarker(marker);
+ const onSelect = () => void States.setSelection(mark);
+ const onHover =
+ (h: boolean): void => States.setHovered(h ? mark : undefined);
+ const ref = isHovered ? scrollTarget : undefined;
+ const markInfo =
+ <MarkInfos
+ key={marker}
+ marker={marker}
+ markerInfo={markerInfo}
+ pinned={pinned}
+ selected={isSelected}
+ filter={filter}
+ hovered={isHovered}
+ onPin={onPin}
+ onRemove={onRemove}
+ onHover={onHover}
+ onSelect={onSelect}
+ />;
+ return <div ref={ref}>{markInfo}</div>;
+ };
return (
<>
- <Vfill>
- <Text
- buffer={buffer}
- mode="text"
- onSelection={onTextSelection}
- readOnly
+ <TitleBar>
+ <IconButton
+ icon="CLIPBOARD"
+ onClick={() => openFilter(information, filter, setFilter)}
+ title="Information Filters"
/>
- </Vfill>
+ </TitleBar>
+ <Boxes.Scroll>
+ {markers.getSelected().map(renderMark)}
+ </Boxes.Scroll>
</>
);
}
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index e98cb526378526a9edc93cfa001493d4c42ee5ce..339961b65b0344a4dddf128fdbbeb1b71abb56b5 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -30,7 +30,7 @@ import React from 'react';
import _ from 'lodash';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
-import * as Utils from 'frama-c/utils';
+import * as RichText from 'frama-c/richtext';
import * as Dome from 'dome';
import { RichTextBuffer } from 'dome/text/buffers';
@@ -66,7 +66,7 @@ async function loadAST(
if (!data) {
buffer.log('// No code for function', theFunction);
}
- Utils.printTextWithTags(buffer, data);
+ RichText.printTextWithTags(buffer, data);
if (theMarker)
buffer.scroll(theMarker);
} catch (err) {
@@ -161,9 +161,11 @@ export default function ASTview() {
const buffer = React.useMemo(() => new RichTextBuffer(), []);
const printed = React.useRef<string | undefined>();
const [selection, updateSelection] = States.useSelection();
+ const [hoveredLoc] = States.useHovered();
const multipleSelections = selection?.multiple.allSelections;
const theFunction = selection?.current?.fct;
const theMarker = selection?.current?.marker;
+ const hovered = hoveredLoc?.marker;
const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
const markersInfo = States.useSyncArray(Ast.markerInfo);
@@ -220,16 +222,24 @@ export default function ASTview() {
return 'dead-code';
if (deadCode?.nonTerminating?.some((m) => m === marker))
return 'non-terminating';
+ if (marker === hovered)
+ return 'hovered-marker';
return undefined;
};
buffer.setDecorator(decorator);
- }, [buffer, multipleSelections, deadCode]);
+ }, [buffer, multipleSelections, hovered, deadCode]);
// Hook: marker scrolling
React.useEffect(() => {
if (theMarker) buffer.scroll(theMarker);
}, [buffer, theMarker]);
+ function onHover(markerId?: string) {
+ const marker = Ast.jMarker(markerId);
+ const fct = selection?.current?.fct;
+ States.setHovered(marker ? { fct, marker } : undefined);
+ }
+
function onSelection(markerId: string, meta = false) {
const fct = selection?.current?.fct;
const location = { fct, marker: Ast.jMarker(markerId) };
@@ -303,6 +313,7 @@ export default function ASTview() {
mode="text/x-csrc"
fontSize={fontSize}
selection={theMarker}
+ onHover={onHover}
onSelection={onSelection}
onContextMenu={onContextMenu}
gutters={['bullet']}
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 73dad1c72165f7f5bf3ababda8b50304ce305663..40bf034596919523dba48b67e06bb05d0d6a69d2 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -256,7 +256,7 @@ const markerInfo_internal: State.Array<string,markerInfoData> = {
reload: reloadMarkerInfo,
order: byMarkerInfoData,
};
-/** Marker informations */
+/** Marker information */
export const markerInfo: State.Array<string,markerInfoData> = markerInfo_internal;
/** Localizable AST markers */
@@ -458,15 +458,34 @@ const functions_internal: State.Array<Json.key<'#functions'>,functionsData> = {
/** AST Functions */
export const functions: State.Array<Json.key<'#functions'>,functionsData> = functions_internal;
-const getInfo_internal: Server.GetRequest<marker,text> = {
+/** Updated AST information */
+export const getInformationUpdate: Server.Signal = {
+ name: 'kernel.ast.getInformationUpdate',
+};
+
+const getInformation_internal: Server.GetRequest<
+ marker |
+ undefined,
+ { id: string, label: string, title: string, descr: text }[]
+ > = {
kind: Server.RqKind.GET,
- name: 'kernel.ast.getInfo',
+ name: 'kernel.ast.getInformation',
input: jMarker,
- output: jText,
- signals: [],
+ output: Json.jList(
+ Json.jObject({
+ id: Json.jFail(Json.jString,'String expected'),
+ label: Json.jFail(Json.jString,'String expected'),
+ title: Json.jFail(Json.jString,'String expected'),
+ descr: jTextSafe,
+ })),
+ signals: [ { name: 'kernel.ast.getInformationUpdate' } ],
};
-/** Get textual information about a marker */
-export const getInfo: Server.GetRequest<marker,text>= getInfo_internal;
+/** Get available information about markers. When no marker is given, returns all kinds of information (with empty `descr` field). */
+export const getInformation: Server.GetRequest<
+ marker |
+ undefined,
+ { id: string, label: string, title: string, descr: text }[]
+ >= getInformation_internal;
const getMarkerAt_internal: Server.GetRequest<
[ string, number, number ],
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index be30b0d1581daf1edff87853cd07e314138b2694..9b5d8f34ae951f23a7dd5595cb6267ef8d63b870 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -9,6 +9,18 @@
text-overflow: ellipsis;
}
+/* -------------------------------------------------------------------------- */
+/* --- Lightweight Text Markers --- */
+/* -------------------------------------------------------------------------- */
+
+.kernel-text {
+ white-space: pre;
+}
+
+.kernel-text-marker:hover {
+ background: var(--code-hover);
+}
+
/* -------------------------------------------------------------------------- */
/* --- AST View --- */
/* -------------------------------------------------------------------------- */
@@ -17,6 +29,10 @@
background-color: var(--highlighted-marker);
}
+.hovered-marker {
+ background-color: var(--code-hover);
+}
+
.dead-code {
background-color: var(--dead-code);
border-bottom: solid 0.1em var(--dead-code);
@@ -46,7 +62,7 @@
.globals-attr {
font-size: smaller;
font-weight: lighter;
- color: #aaa;
+ color: var(--info-text);
}
.globals-function-section {
@@ -54,7 +70,79 @@
}
/* -------------------------------------------------------------------------- */
-/* --- Globals --- */
+/* --- Informations --- */
+/* -------------------------------------------------------------------------- */
+
+.astinfo-section {
+ position: relative;
+ overflow: auto;
+ padding-top: 1px;
+ padding-bottom: 2px;
+}
+
+.astinfo-section.selected {
+ background: var(--code-select);
+}
+
+.astinfo-section.hovered {
+ background: var(--code-hover);
+}
+
+.astinfo-section.selected.hovered {
+ background: var(--code-select-hover);
+}
+
+.astinfo-folderbutton {
+ flex: 0 0 auto;
+}
+
+.astinfo-markerbar {
+ display: flex;
+ overflow: hidden;
+ padding-left: 4px;
+}
+
+.astinfo-markerkind {
+ background: var(--selected-element);
+ position: relative;
+ top: -1px;
+ border-radius: 2px;
+ font-size: 7pt;
+ padding: 2px;
+ color: var(--text);
+ user-select: none;
+ margin-right: 3pt;
+}
+
+.astinfo-markercode {
+ flex: 1 1 auto;
+ text-overflow: ellipsis;
+ cursor: default;
+}
+
+.astinfo-markerbutton {
+ flex: 0 1 auto;
+ margin: 0px;
+ position: relative;
+}
+
+.astinfo-infos {
+ display: flex ;
+ margin-top: 1px ;
+ margin-bottom: 1px ;
+}
+
+.astinfo-kind {
+ flex: 0 1 50px;
+ text-align: center;
+ margin-top: 1px;
+ margin-left: 8px;
+ color: var(--info-text);
+ font-size: smaller;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Messages --- */
/* -------------------------------------------------------------------------- */
.message-search {
diff --git a/ivette/src/frama-c/utils.ts b/ivette/src/frama-c/richtext.tsx
similarity index 55%
rename from ivette/src/frama-c/utils.ts
rename to ivette/src/frama-c/richtext.tsx
index 86df5df5f3d98aa58f68fddd141d156b532e5461..3a9c72c6c7c428f0a7906744e1a886a99aec61d8 100644
--- a/ivette/src/frama-c/utils.ts
+++ b/ivette/src/frama-c/richtext.tsx
@@ -26,12 +26,14 @@
/**
* @packageDocumentation
- * @module frama-c/utils
-*/
+ * @module frama-c/richtext
+ */
+import React from 'react';
import * as Dome from 'dome';
import * as DomeBuffers from 'dome/text/buffers';
import * as KernelData from 'frama-c/kernel/api/data';
+import { classes } from 'dome/misc/utils';
const D = new Dome.Debug('Utils');
@@ -42,33 +44,82 @@ const D = new Dome.Debug('Utils');
/**
* Print text containing tags into buffer.
* @param buffer Rich text buffer to print into.
- * @param contents Actual text containing tags.
+ * @param text Actual text containing tags.
* @param options Specify particular marker options.
*/
export function printTextWithTags(
buffer: DomeBuffers.RichTextBuffer,
- contents: KernelData.text,
+ text: KernelData.text,
options?: DomeBuffers.MarkerProps,
): void {
- if (Array.isArray(contents)) {
- let marker = false;
- const tag = contents.shift();
- if (tag) {
- if (Array.isArray(tag)) {
- contents.unshift(tag);
- } else {
- buffer.openTextMarker({ id: tag, ...options ?? {} });
- marker = true;
- }
+ if (Array.isArray(text)) {
+ const tag = text[0];
+ const marker = typeof (tag) === 'string';
+ if (marker) {
+ buffer.openTextMarker({ id: tag, ...options ?? {} });
+ }
+ for (let k = marker ? 1 : 0; k < text.length; k++) {
+ printTextWithTags(buffer, text[k], options);
}
- contents.forEach((txt) => printTextWithTags(buffer, txt, options));
if (marker) {
- marker = false;
buffer.closeTextMarker();
}
- } else if (typeof contents === 'string') {
- buffer.append(contents);
+ } else if (typeof text === 'string') {
+ buffer.append(text);
} else {
- D.error('Unexpected text', contents);
+ D.error('Unexpected text', text);
}
}
+
+// --------------------------------------------------------------------------
+// --- Lightweight Text Renderer
+// --------------------------------------------------------------------------
+
+interface MarkerProps {
+ marker: string;
+ onMarker?: (marker: string) => void;
+ children?: React.ReactNode;
+}
+
+function Marker(props: MarkerProps): JSX.Element {
+ const { marker, onMarker, children } = props;
+ const onClick = (): void => { if (onMarker) onMarker(marker); };
+ return (
+ <span
+ className="kernel-text-marker"
+ onClick={onClick}
+ >
+ {children}
+ </span>
+ );
+}
+
+function makeContents(text: KernelData.text): React.ReactNode {
+ if (Array.isArray(text)) {
+ const tag = text[0];
+ const marker = tag && typeof (tag) === 'string';
+ const array = marker ? text.slice(1) : text;
+ const contents = React.Children.toArray(array.map(makeContents));
+ if (marker) {
+ return <Marker marker={tag}>{contents}</Marker>;
+ }
+ return <>{contents}</>;
+ } if (typeof text === 'string') {
+ return text;
+ }
+ D.error('Unexpected text', text);
+ return null;
+}
+
+export interface TextProps {
+ text: KernelData.text;
+ onMarker?: (marker: string) => void;
+ className?: string;
+}
+
+export function Text(props: TextProps): JSX.Element {
+ const className = classes('kernel-text', 'dome-text-code', props.className);
+ return <div className={className}>{makeContents(props.text)}</div>;
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index ff7b0310ffc622958094a9f668b70a6edcf18bbb..11b59f05e8aeaacd4265712bb5ad6f52d79cae78 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -188,7 +188,7 @@ export function useRequest<In, Out>(
}
});
- const signals = options.onSignals ?? rq.signals;
+ const signals = rq.signals.concat(options.onSignals ?? []);
React.useEffect(() => {
signals.forEach((s) => Server.onSignal(s, trigger));
return () => {
@@ -767,11 +767,18 @@ const emptySelection = {
},
};
+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);
Server.onShutdown(() => GlobalSelection.setValue(emptySelection));
+export function setHovered(h: Hovered) { GlobalHovered.setValue(h); }
+export function useHovered(): [Hovered, (h: Hovered) => void] {
+ return useGlobalState(GlobalHovered);
+}
+
export function setSelection(location: Location, meta = false) {
const s = GlobalSelection.getValue();
GlobalSelection.setValue(reducer(s, { location }));
diff --git a/ivette/src/renderer/Extensions.tsx b/ivette/src/renderer/Extensions.tsx
index ae5019ccca54d54bea76c9de8232fc2909e1edf4..2d33b9f1dc520ca6f916bfc61161923db6f73a48 100644
--- a/ivette/src/renderer/Extensions.tsx
+++ b/ivette/src/renderer/Extensions.tsx
@@ -133,9 +133,12 @@ function byPanel(p: ElementProps, q: ElementProps) {
export class ElementRack {
+ private rank = 1;
private readonly items = new Map<string, ElementProps>();
register(elt: ElementProps) {
+ if (elt.rank === undefined) elt.rank = this.rank;
+ this.rank++;
this.items.set(elt.id, elt);
UPDATED.emit();
}
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index 8c59c658adf2c3ac998fbeacad5aea2939e40caa..943f93e2fe1ddb98ce547a23397196bcbab2a5e4 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -82,9 +82,11 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
SERVER_API= \
package.mli \
+ jbuffer.mli \
data.mli \
request.mli \
states.mli \
+ main.mli \
kernel_main.mli \
kernel_ast.mli \
kernel_properties.mli
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 70416e8a3b3098c7455660b4f63d5dd0c848b47f..8b9722ba5d03810f762721c6cb26adc0f929da5b 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -243,6 +243,8 @@ struct
declare ~package ~name:"text" ~descr jdef
end
+let jpretty = Jbuffer.to_json
+
(* -------------------------------------------------------------------------- *)
(* --- Functional API --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index d3e2e79bdf8285b2e600ed75f241068dac836bfd..87305705e39ce58bae376ff62110aa8b0732c062 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -87,6 +87,10 @@ module Jtext : S with type t = json
module Jmarkdown : S with type t = Markdown.text
+(** All-in-one formatter. Return the JSON encoding of formatted text. *)
+val jpretty : ?indent:int -> ?margin:int ->
+ (Format.formatter -> 'a -> unit) -> 'a -> Jtext.t
+
(* -------------------------------------------------------------------------- *)
(** {2 Constructors} *)
(* -------------------------------------------------------------------------- *)
@@ -155,11 +159,11 @@ val declare :
{[
(* ---- Exemple of Record Data --- *)
type r
- let s = Record.signature ~page ~kind ~name ~descr () in
+ let s = Record.signature () in
let fd_a = Record.field s ~name:"a" ~descr:"..." (module A) in
let fd_b = Record.field s ~name:"b" ~descr:"..." (module B) in
-
- module M = (val (Record.publish s) : Record with type r = r)
+ let r = Record.publish s ~page ~kind ~name ~descr
+ module M = (val r) : Record with type r = r)
let make a b = M.default |> M.set fd_a a |> M.set fd_b b
]}
diff --git a/src/plugins/server/jbuffer.ml b/src/plugins/server/jbuffer.ml
index 0cbac3b7d5cc087f30f2de2488ee6eba1aa2cd53..f03483fc4c1b1b323db66e6bfbce7171cd78ba3e 100644
--- a/src/plugins/server/jbuffer.ml
+++ b/src/plugins/server/jbuffer.ml
@@ -100,6 +100,7 @@ let bprintf buffer msg = Format.fprintf buffer.fmt msg
let formatter buffer = buffer.fmt
let contents buffer : json =
+ Format.pp_print_flush buffer.fmt () ;
flush buffer () ;
while buffer.stack <> [] do
pop_tag buffer ""
@@ -112,15 +113,20 @@ let contents buffer : json =
let format ?indent ?margin msg =
let buffer = create ?indent ?margin () in
Format.kfprintf
- (fun fmt -> Format.pp_print_flush fmt () ; contents buffer)
+ (fun _fmt -> contents buffer)
buffer.fmt msg
let to_json ?indent ?margin pp a =
let buffer = create ?indent ?margin () in
pp buffer.fmt a ;
- Format.pp_print_flush buffer.fmt () ;
contents buffer
+let rec is_empty (js : json) = match js with
+ | `Null -> true
+ | `List js -> List.for_all is_empty js
+ | `String "" -> true
+ | _ -> false
+
let rec fprintf fmt = function
| `Null -> ()
| `String text -> Format.pp_print_string fmt text
diff --git a/src/plugins/server/jbuffer.mli b/src/plugins/server/jbuffer.mli
index 08cc4050f3a2a35592affd977b55cacf46f5b0cd..f9e175210bd9b35522eccc4de51790f723fa6603 100644
--- a/src/plugins/server/jbuffer.mli
+++ b/src/plugins/server/jbuffer.mli
@@ -55,6 +55,9 @@ val pop_tag : buffer -> Format.stag -> unit
tags. *)
val contents : buffer -> json
+(** When [is_empty js] holds, the JSON is sure to be empty. *)
+val is_empty : json -> bool
+
(** Prints back a JSON encoding into the provided formatter.
@raise Yojson.Basic.Util.Type_error in case of ill formatted buffer. *)
val fprintf : Format.formatter -> json -> unit
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index d8cf92f5501b61b464731d4cc260528607f3f77b..84d21cb8a070f28a812fe2a47965b64a0191e041 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -260,7 +260,7 @@ struct
States.register_array
~package
~name:"markerInfo"
- ~descr:(Md.plain "Marker informations")
+ ~descr:(Md.plain "Marker information")
~key:snd ~keyType:Jstring
~iter ~add_reload_hook:ast_update_hook
model
@@ -543,74 +543,151 @@ struct
end
(* -------------------------------------------------------------------------- *)
-(* --- Information --- *)
+(* --- Marker Information --- *)
(* -------------------------------------------------------------------------- *)
-module Info = struct
- open Printer_tag
+module Information =
+struct
+
+ type info = {
+ id: string;
+ rank: int;
+ label: string;
+ title: string;
+ enable: unit -> bool;
+ pretty: Format.formatter -> Printer_tag.localizable -> unit
+ }
+
+ (* Info markers serialization *)
+
+ module S =
+ struct
+ type t = (info * Jtext.t)
+ let jtype = Package.(Jrecord[
+ "id", Jstring ;
+ "label", Jstring ;
+ "title", Jstring ;
+ "descr", Jtext.jtype ;
+ ])
+ let of_json _ = failwith "Information.Info"
+ let to_json (info,text) = `Assoc [
+ "id", `String info.id ;
+ "label", `String info.label ;
+ "title", `String info.title ;
+ "descr", text ;
+ ]
+ end
+
+ (* Info markers registry *)
+
+ let rankId = ref 0
+ let registry : (string,info) Hashtbl.t = Hashtbl.create 0
+
+ let jtext pp marker =
+ try
+ let buffer = Jbuffer.create () in
+ let fmt = Jbuffer.formatter buffer in
+ pp fmt marker;
+ Format.pp_print_flush fmt ();
+ Jbuffer.contents buffer
+ with Not_found ->
+ `Null
+
+ let rank ({rank},_) = rank
+ let by_rank a b = Stdlib.compare (rank a) (rank b)
+
+ let get_information tgt =
+ let infos = ref [] in
+ Hashtbl.iter
+ (fun _ info ->
+ if info.enable () then
+ match tgt with
+ | None -> infos := (info, `Null) :: !infos
+ | Some marker ->
+ let text = jtext info.pretty marker in
+ if not (Jbuffer.is_empty text) then
+ infos := (info, text) :: !infos
+ ) registry ;
+ List.sort by_rank !infos
+
+ let signal = Request.signal ~package
+ ~name:"getInformationUpdate"
+ ~descr:(Md.plain "Updated AST information")
+
+ let update () = Request.emit signal
+
+ let register ~id ~label ~title ?(enable = fun _ -> true) pretty =
+ let rank = incr rankId ; !rankId in
+ let info = { id ; rank ; label ; title ; enable ; pretty } in
+ if Hashtbl.mem registry id then
+ ( let msg = Format.sprintf
+ "Server.Kernel_ast.register_info: duplicate %S" id in
+ raise (Invalid_argument msg) );
+ Hashtbl.add registry id info
- let print_function fmt name =
- let stag = Format.String_tag name in
- Format.pp_open_stag fmt stag;
- Format.pp_print_string fmt name;
- Format.pp_close_stag fmt ()
-
- let print_kf fmt kf = print_function fmt (Kernel_function.get_name kf)
-
- let print_variable fmt vi =
- Format.fprintf fmt "Variable %s has type %a.@."
- vi.vname Printer.pp_typ vi.vtype;
- let kf = Kernel_function.find_defining_kf vi in
- let pp_kf fmt kf = Format.fprintf fmt " of function %a" print_kf kf in
- Format.fprintf fmt "It is a %s variable%a.@."
- (if vi.vglob then "global" else if vi.vformal then "formal" else "local")
- (Format.pp_print_option pp_kf) kf;
- if vi.vtemp then
- Format.fprintf fmt "This is a temporary variable%s.@."
- (match vi.vdescr with None -> "" | Some descr -> " for " ^ descr);
- Format.fprintf fmt "It is %sreferenced and its address is %staken."
- (if vi.vreferenced then "" else "not ")
- (if vi.vaddrof then "" else "not ")
-
- let print_varinfo fmt vi =
- if Cil.isFunctionType vi.vtype
- then
- Format.fprintf fmt "%a is a C function of type '%a'."
- print_function vi.vname Printer.pp_typ vi.vtype
- else print_variable fmt vi
-
- let print_lvalue fmt _loc = function
- | Var vi, NoOffset -> print_varinfo fmt vi
- | lval ->
- Format.fprintf fmt "This is an lvalue of type %a."
- Printer.pp_typ (Cil.typeOfLval lval)
-
- let print_localizable fmt = function
- | PExp (_, _, e) ->
- Format.fprintf fmt "This is a pure C expression of type %a."
- Printer.pp_typ (Cil.typeOf e)
- | PLval (_, _, lval) as loc -> print_lvalue fmt loc lval
- | PVDecl (_, _, vi) ->
- Format.fprintf fmt "This is the declaration of variable %a.@.@."
- Printer.pp_varinfo vi;
- print_varinfo fmt vi
- | PStmt (kf, _) | PStmtStart (kf, _) ->
- Format.fprintf fmt "This is a statement of function %a." print_kf kf
- | _ -> ()
-
- let get_marker_info loc =
- let buffer = Jbuffer.create () in
- let fmt = Jbuffer.formatter buffer in
- print_localizable fmt loc;
- Format.pp_print_flush fmt ();
- Jbuffer.contents buffer
end
let () = Request.register ~package
- ~kind:`GET ~name:"getInfo"
- ~descr:(Md.plain "Get textual information about a marker")
- ~input:(module Marker) ~output:(module Jtext)
- Info.get_marker_info
+ ~kind:`GET ~name:"getInformation"
+ ~descr:(Md.plain
+ "Get available information about markers. \
+ When no marker is given, returns all kinds \
+ of information (with empty `descr` field).")
+ ~input:(module Joption(Marker))
+ ~output:(module Jlist(Information.S))
+ ~signals:[Information.signal]
+ Information.get_information
+
+(* -------------------------------------------------------------------------- *)
+(* --- Default Kernel Information --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Information.register
+ ~id:"kernel.ast.location"
+ ~label:"Location"
+ ~title:"Source file location"
+ begin fun fmt loc ->
+ let location = Printer_tag.loc_of_localizable loc in
+ Filepath.pp_pos fmt (fst location)
+ end
+
+let () = Information.register
+ ~id:"kernel.ast.varinfo"
+ ~label:"Var"
+ ~title:"Variable Information"
+ begin fun fmt loc ->
+ match loc with
+ | PLval (_ , _, (Var x,NoOffset)) | PVDecl(_,_,x) ->
+ if not x.vreferenced then Format.pp_print_string fmt "unused " ;
+ begin
+ match x.vstorage with
+ | NoStorage -> ()
+ | Extern -> Format.pp_print_string fmt "extern "
+ | Static -> Format.pp_print_string fmt "static "
+ | Register -> Format.pp_print_string fmt "register "
+ end ;
+ if x.vghost then Format.pp_print_string fmt "ghost " ;
+ if x.vaddrof then Format.pp_print_string fmt "aliased " ;
+ if x.vformal then Format.pp_print_string fmt "formal" else
+ if x.vglob then Format.pp_print_string fmt "global" else
+ if x.vtemp then Format.pp_print_string fmt "temporary" else
+ Format.pp_print_string fmt "local" ;
+ | _ -> raise Not_found
+ end
+
+let () = Information.register
+ ~id:"kernel.ast.typeinfo"
+ ~label:"Type"
+ ~title:"Type of C/ASCL expression"
+ begin fun fmt loc ->
+ let open Printer in
+ match loc with
+ | PExp (_, _, e) -> pp_typ fmt (Cil.typeOf e)
+ | PLval (_, _, lval) -> pp_typ fmt (Cil.typeOfLval lval)
+ | PTermLval(_,_,_,lv) -> pp_logic_type fmt (Cil.typeOfTermLval lv)
+ | PVDecl (_,_,vi) -> pp_typ fmt vi.vtype
+ | _ -> raise Not_found
+ end
(* -------------------------------------------------------------------------- *)
(* --- Marker at a position --- *)
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 448d6f373dee42b1fb0d2c98e6afa7184207a340..e18092b2f9e96a5852c5a91f7789f47f33d53112 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -62,6 +62,33 @@ module KfMarker : Data.S with type t = kernel_function * Printer_tag.localizable
module Printer : Printer_tag.S_pp
+(* -------------------------------------------------------------------------- *)
+(** Ast Information *)
+(* -------------------------------------------------------------------------- *)
+
+module Information :
+sig
+ (**
+ Registers a marker information printer.
+ Identifier [id] shall be unique.
+ Label [label] shall be very short.
+ Description shall succinctly describe the kind of information.
+ If the optional [enable] function is provided, the information printer is
+ only used when [enable ()] returns true.
+ The printer is allowed to raise [Not_found] exception when there is no
+ information for the localizable.
+ *)
+ val register :
+ id:string -> label:string -> title:string -> ?enable:(unit -> bool) ->
+ (Format.formatter -> Printer_tag.localizable -> unit) -> unit
+
+ (** Updated information signal *)
+ val signal : Request.signal
+
+ (** Emits a signal to server clients to reload AST marker information. *)
+ val update : unit -> unit
+end
+
(* -------------------------------------------------------------------------- *)
(** Globals *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/request.mli b/src/plugins/server/request.mli
index 3fe2933425cba1e63980bcc07b4adc98b5d3f442..58cfd275a8cd0b598f4d65c8cd37cbe0d1a48549 100644
--- a/src/plugins/server/request.mli
+++ b/src/plugins/server/request.mli
@@ -114,12 +114,12 @@ val register :
{[
(* ---- Exemple of Request Registration --- *)
let () =
- let s = Request.signature ~page ~kind ~name ~descr () in
+ let s = Request.signature () in
let get_a = Request.param s ~name:"a" ~descr:"..." (module A) in
let get_b = Request.param s ~name:"b" ~descr:"..." (module B) in
let set_c = Request.result s ~name:"c" ~descr:"..." (module C) in
let set_d = Request.result s ~name:"d" ~descr:"..." (module D) in
- Request.register_sig s
+ Request.register_sig s ~package ~kind ~name ~descr
(fun rq () ->
let (c,d) = some_job (get_a rq) (get_b rq) in
set_c rq c ; set_d rq d)
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 007c88ce26169424d17a82635bb786fc9f086449..a1c14afd4fd0a02cc7ee8357fc5fcfb4d15cf24e 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -157,6 +157,12 @@ let md_named ~kind pp = function
let title = String.capitalize_ascii kind in
Md.table (Package.md_fields ~title pp prms)
+let md_signals signals =
+ if signals = [] then []
+ else
+ Md.quote (Md.emph "signals") @
+ Md.block Md.(list (List.map (fun x -> text (code x)) signals))
+
let descr_of_decl names decl =
match decl.d_kind with
| D_safe _ | D_loose _ | D_order _ -> assert false
@@ -181,9 +187,7 @@ let descr_of_decl names decl =
Md.quote (md_param ~kind:"output" pp rq.rq_output) @
md_named ~kind:"input" pp rq.rq_input @
md_named ~kind:"output" pp rq.rq_output @
- Md.quote (Md.emph "signals") @
- Md.block Md.(list (List.map (fun x -> text (code x))
- rq.rq_signals))
+ md_signals rq.rq_signals
let declaration page names decl =
match decl.d_kind with
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 2bf817aee3508b8c651d514c62a42298c14800d8..8c509d9484041f63f114711db0f2a2c2ebbeb86e 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -139,10 +139,41 @@ let () = Request.register ~package
~output:(module DeadCode)
dead_code
+(* ----- Register Eva information ------------------------------------------- *)
+
+let print_value fmt loc =
+ let stmt, eval =
+ match loc with
+ | Printer_tag.PLval (_kf, Kstmt stmt, lval)
+ when Cil.isScalarType (Cil.typeOfLval lval) ->
+ stmt, Results.eval_lval lval
+ | Printer_tag.PExp (_kf, Kstmt stmt, expr)
+ when Cil.isScalarType (Cil.typeOf expr) ->
+ stmt, Results.eval_exp expr
+ | _ -> raise Not_found
+ in
+ let eval_cvalue at = Results.(at stmt |> eval |> as_cvalue_or_uninitialized) in
+ let before = eval_cvalue Results.before in
+ let after = eval_cvalue Results.after in
+ let pretty = Cvalue.V_Or_Uninitialized.pretty in
+ if Cvalue.V_Or_Uninitialized.equal before after
+ then pretty fmt before
+ else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
+
+let () =
+ Server.Kernel_ast.Information.register
+ ~id:"eva.value"
+ ~label:"Value"
+ ~title:"Possible values inferred by Eva"
+ ~enable:Analysis.is_computed
+ print_value
+
+let () =
+ Analysis.register_computation_hook
+ (fun _ -> Server.Kernel_ast.Information.update ())
(* ----- Red and tainted alarms --------------------------------------------- *)
-
module Taint = struct
open Server.Data
open Taint_domain