diff --git a/ivette/src/dome/renderer/dome.tsx b/ivette/src/dome/renderer/dome.tsx
index 28323a8814fbebc68c5830116b4ee1a53aa379be..ffaaa36e3a5337beb2d6ba71cad1a934dfc279d1 100644
--- a/ivette/src/dome/renderer/dome.tsx
+++ b/ivette/src/dome/renderer/dome.tsx
@@ -780,9 +780,10 @@ export function useTimer(period: number, callback: () => void): void {
type Callback<A> = (arg: A) => void;
/**
- Protected callback against unmounted component.
- The returned callback will be only fired when the component is mounted.
- The provided callback need not be memoized.
+ * Protected callback against unwanted dependencies and unmounted component.
+ * - The provided callback need _not_ be memoized, no dependency is needed.
+ * - The provided callback will _not_ be fired after the component is unmounted.
+ * - The returned callback will be _constant_ during the entire hook lifetime.
*/
export function useProtected<A>(fn: Callback<A> | undefined): Callback<A> {
const cb = React.useRef<Callback<A>>();
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index e2463cc03b50c0a31808cce488739da0af35a70d..c2e6e7bb62261eebd51d001be2a04dfd496c80f7 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -143,7 +143,7 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
const foreign = !!current && !!scope && current !== scope;
const [unfold, setUnfold] = React.useState(true);
const [expand, setExpand] = React.useState(false);
- const markerFields = States.useRequest(Ast.getInformation, marker) ?? [];
+ const markerFields = States.useRequestValue(Ast.getInformation, marker);
const isScrolled = marker === scrolled;
const isHovered = marker === hovered;
const isSelected = marker === selected;
@@ -273,7 +273,7 @@ export default function ASTinfo(): JSX.Element {
const [setting, setSetting] = Dome.useStringSettings(filterSettings, '');
const { scope: current, marker: selected } = States.useCurrentLocation();
const hovered = States.useHovered();
- const allFields = States.useRequest(Ast.getInformation, null) ?? [];
+ const allFields = States.useRequestValue(Ast.getInformation, null);
const excluded = React.useMemo(() => makeFilter(setting), [setting]);
Dome.useEvent(States.MetaSelection, (loc: States.Location) => {
setMarkers(addMarker(markers, loc.marker));
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index b570db212483aef0f032dc4fca2d2e719881acaa..96db99d2d781adf5db22db440ac9e2c5aa45a6ac 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -418,7 +418,7 @@ function getPropertiesNodes(tree: Tree): Node[] {
// This aspect contains all the properties nodes, along with their tags.
interface Property extends Node { tag: States.Tag }
const PropertiesNodes = createPropertiesNodes();
-function createPropertiesNodes() : Editor.Aspect<Property[]> {
+function createPropertiesNodes(): Editor.Aspect<Property[]> {
const deps = { tree: Tree, tags: Tags, statuses: PropertiesStatuses };
return Editor.createAspect(deps, ({ tree, tags, statuses }) => {
const nodes = getPropertiesNodes(tree);
@@ -494,9 +494,9 @@ function createPropertiesGutter(): Editor.Extension {
type MarkerMenuExtender =
(items: Dome.PopupMenuItem[], attr: Ast.markerAttributesData) => void;
-const MarkerMenuExtenders : MarkerMenuExtender[] = [];
+const MarkerMenuExtenders: MarkerMenuExtender[] = [];
-export function registerMarkerMenuExtender(e : MarkerMenuExtender) : void {
+export function registerMarkerMenuExtender(e: MarkerMenuExtender): void {
MarkerMenuExtenders.push(e);
}
@@ -530,7 +530,7 @@ function createContextMenuHandler(): Editor.Extension {
const descr = `Calls to ${name}`;
Lodash.forEach(groupedCallers, (group) => {
const n = group.length;
- const { call } : Eva.CallSite = group[0];
+ const { call }: Eva.CallSite = group[0];
const { name: fct } = States.getDeclaration(call);
const caller = `caller ${fct}`;
const nsites = n > 1 ? `s (${n} call sites)` : '';
@@ -559,7 +559,8 @@ function createContextMenuHandler(): Editor.Extension {
onClick: () => {
const text = view.state.sliceDoc(node.from, node.to);
if (text !== '') navigator.clipboard.writeText(text);
- } });
+ }
+ });
Dome.popupMenu(items);
return;
}
@@ -635,45 +636,32 @@ function createTaintTooltip(): Editor.Extension {
// Server request handler returning the given function's text.
function useAST(decl: Ast.decl | undefined): text {
- return States.useRequest(
- Ast.printDeclaration, decl || undefined,
- { onError: [] }
- ) ?? [];
+ return States.useRequestValue(Ast.printDeclaration, decl || undefined);
}
// Server request handler returning the given function's callers.
function useCallers(decl: Decl): Eva.CallSite[] {
- return States.useRequest(
- Eva.getCallers, decl || undefined,
- { onError: [] }
- ) ?? [];
+ return States.useRequestValue(Eva.getCallers, decl || undefined);
}
// Server request handler returning the given function's callers.
function useCallees(marker: Marker): Ast.decl[] {
- return States.useRequest(
- Eva.getCallees, marker || undefined,
- { onError: [] }
- ) ?? [];
+ return States.useRequestValue(Eva.getCallees, marker || undefined);
}
// Server request handler returning the tainted lvalues.
function useTaints(decl: Decl): Eva.LvalueTaints[] {
- return States.useRequest(Eva.taintedLvalues, decl, { onError: [] }) ?? [];
+ return States.useRequestValue(Eva.taintedLvalues, decl || undefined);
}
// Server request handler returning the given function's dead code information.
function useDead(decl: Decl): Eva.deadCode {
- return States.useRequest(
- Eva.getDeadCode, decl || undefined,
- { onError: emptyDeadCode }
- ) ?? emptyDeadCode;
+ return States.useRequestValue(Eva.getDeadCode, decl || undefined)
+ ?? emptyDeadCode;
}
// -----------------------------------------------------------------------------
-
-
// -----------------------------------------------------------------------------
// AST View component
// -----------------------------------------------------------------------------
@@ -748,7 +736,7 @@ export default function ASTview(): JSX.Element {
<TitleBar>
<IconButton
icon={icon}
- onClick= {unFoldButtonClicked}
+ onClick={unFoldButtonClicked}
title={title + ' all multi-line ACSL properties'}
className="titlebar-thin-icon"
/>
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index ec2d9b1815e947343d56ee0b62b2a136cf66ceeb..c69b5084da75380dcddef525900a6d267f82f910 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -198,7 +198,7 @@ export default function SourceCode(): JSX.Element {
const selectedMarkerLine = floc?.line ?? 0;
const source = useSourceFileContents(file);
const [cursor, setCursor] = React.useState<SourceCursor>(noCursor);
- const markerAtCursor = States.useRequest(Ast.getMarkerAt, cursor);
+ const markerAtCursor = States.useRequestResponse(Ast.getMarkerAt, cursor);
const { sloc: slocAtCursor } = States.useMarker(markerAtCursor);
const openFile = React.useCallback(() => {
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index d7ffb5bcf319f3b9684e68e5dd90aa2e8debae52..8e936a7fb1e9094bce985769a4c4b55b2663a0e7 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -51,6 +51,7 @@ const compute_internal: Server.ExecRequest<null,null> = {
name: 'kernel.ast.compute',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Ensures that AST is computed */
@@ -186,6 +187,7 @@ const reloadDeclAttributes_internal: Server.GetRequest<null,null> = {
name: 'kernel.ast.reloadDeclAttributes',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`declAttributes`](#declattributes) */
@@ -205,6 +207,7 @@ const fetchDeclAttributes_internal: Server.GetRequest<
updated: Json.jArray(jDeclAttributesData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`declAttributes`](#declattributes) */
@@ -235,6 +238,7 @@ const printDeclaration_internal: Server.GetRequest<decl,text> = {
name: 'kernel.ast.printDeclaration',
input: jDecl,
output: jText,
+ fallback: textDefault,
signals: [ { name: 'kernel.ast.changed' } ],
};
/** Prints an AST Declaration */
@@ -335,6 +339,7 @@ const reloadMarkerAttributes_internal: Server.GetRequest<null,null> = {
name: 'kernel.ast.reloadMarkerAttributes',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`markerAttributes`](#markerattributes) */
@@ -354,6 +359,7 @@ const fetchMarkerAttributes_internal: Server.GetRequest<
updated: Json.jArray(jMarkerAttributesData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`markerAttributes`](#markerattributes) */
@@ -385,6 +391,7 @@ const getMainFunction_internal: Server.GetRequest<null,decl | undefined> = {
name: 'kernel.ast.getMainFunction',
input: Json.jNull,
output: Json.jOption(jDecl),
+ fallback: undefined,
signals: [],
};
/** Get the current 'main' function. */
@@ -395,6 +402,7 @@ const getFunctions_internal: Server.GetRequest<null,decl[]> = {
name: 'kernel.ast.getFunctions',
input: Json.jNull,
output: Json.jArray(jDecl),
+ fallback: [],
signals: [],
};
/** Collect all functions in the AST */
@@ -467,6 +475,7 @@ const reloadFunctions_internal: Server.GetRequest<null,null> = {
name: 'kernel.ast.reloadFunctions',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`functions`](#functions) */
@@ -486,6 +495,7 @@ const fetchFunctions_internal: Server.GetRequest<
updated: Json.jArray(jFunctionsData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`functions`](#functions) */
@@ -588,6 +598,7 @@ const reloadGlobals_internal: Server.GetRequest<null,null> = {
name: 'kernel.ast.reloadGlobals',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`globals`](#globals) */
@@ -607,6 +618,7 @@ const fetchGlobals_internal: Server.GetRequest<
updated: Json.jArray(jGlobalsData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`globals`](#globals) */
@@ -654,6 +666,7 @@ const getInformation_internal: Server.GetRequest<
descr: Json.jString,
text: jText,
})),
+ fallback: [],
signals: [ { name: 'kernel.ast.getInformationUpdate' } ],
};
/** Get available information about markers. When no marker is given, returns all kinds of information (with empty `descr` field). */
@@ -676,6 +689,7 @@ const getMarkerAt_internal: Server.GetRequest<
column: Json.jNumber,
}),
output: Json.jOption(jMarker),
+ fallback: undefined,
signals: [ { name: 'kernel.ast.changed' } ],
};
/** Returns the marker and function at a source file position, if any. Input: file path, line and column. File can be empty, in case no marker is returned. */
@@ -690,6 +704,7 @@ const getFiles_internal: Server.GetRequest<null,string[]> = {
name: 'kernel.ast.getFiles',
input: Json.jNull,
output: Json.jArray(Json.jString),
+ fallback: [],
signals: [],
};
/** Get the currently analyzed source file names */
@@ -700,6 +715,7 @@ const setFiles_internal: Server.SetRequest<string[],null> = {
name: 'kernel.ast.setFiles',
input: Json.jArray(Json.jString),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Set the source file names to analyze. */
@@ -713,6 +729,7 @@ const parseExpr_internal: Server.GetRequest<
name: 'kernel.ast.parseExpr',
input: Json.jObject({ stmt: jMarker, term: Json.jString,}),
output: jMarker,
+ fallback: markerDefault,
signals: [],
};
/** Parse a C expression and returns the associated marker */
@@ -729,6 +746,7 @@ const parseLval_internal: Server.GetRequest<
name: 'kernel.ast.parseLval',
input: Json.jObject({ stmt: jMarker, term: Json.jString,}),
output: jMarker,
+ fallback: markerDefault,
signals: [],
};
/** Parse a C lvalue and returns the associated marker */
diff --git a/ivette/src/frama-c/kernel/api/project/index.ts b/ivette/src/frama-c/kernel/api/project/index.ts
index e0be594c7af8ac1f9f60ca73ce67d7d6ae1552e1..e111b68e69d869c6030a8444f80bbf14934d25b6 100644
--- a/ivette/src/frama-c/kernel/api/project/index.ts
+++ b/ivette/src/frama-c/kernel/api/project/index.ts
@@ -68,6 +68,7 @@ const getList_internal: Server.GetRequest<null,projectInfo[]> = {
name: 'kernel.project.getList',
input: Json.jNull,
output: Json.jArray(jProjectInfo),
+ fallback: [],
signals: [],
};
/** Returns the list of all projects */
@@ -78,6 +79,7 @@ const create_internal: Server.SetRequest<string,projectInfo> = {
name: 'kernel.project.create',
input: Json.jString,
output: jProjectInfo,
+ fallback: projectInfoDefault,
signals: [],
};
/** Create a new project */
diff --git a/ivette/src/frama-c/kernel/api/properties/index.ts b/ivette/src/frama-c/kernel/api/properties/index.ts
index 04199344163025e9e8b69f4aa5d30190bef5c4fd..9a6e1bc5c5a2b2c36833ac03a18d27b30912778e 100644
--- a/ivette/src/frama-c/kernel/api/properties/index.ts
+++ b/ivette/src/frama-c/kernel/api/properties/index.ts
@@ -158,6 +158,7 @@ const propKindTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.properties.propKindTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -204,6 +205,7 @@ const propStatusTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.properties.propStatusTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -261,6 +263,7 @@ const alarmsTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.properties.alarmsTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -337,6 +340,7 @@ const reloadStatus_internal: Server.GetRequest<null,null> = {
name: 'kernel.properties.reloadStatus',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`status`](#status) */
@@ -356,6 +360,7 @@ const fetchStatus_internal: Server.GetRequest<
updated: Json.jArray(jStatusData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`status`](#status) */
diff --git a/ivette/src/frama-c/kernel/api/services/index.ts b/ivette/src/frama-c/kernel/api/services/index.ts
index 8bf260c2615bc33faddf0d18a763ebf794faf2d7..d4e700d3831fcbe4152fb91d2102cd899b975cbd 100644
--- a/ivette/src/frama-c/kernel/api/services/index.ts
+++ b/ivette/src/frama-c/kernel/api/services/index.ts
@@ -82,6 +82,7 @@ const getConfig_internal: Server.GetRequest<
datadir: Json.jArray(Json.jString),
pluginpath: Json.jArray(Json.jString),
}),
+ fallback: { version: '', datadir: [], pluginpath: [] },
signals: [],
};
/** Frama-C Kernel configuration */
@@ -95,6 +96,7 @@ const load_internal: Server.SetRequest<string,string | undefined> = {
name: 'kernel.services.load',
input: Json.jString,
output: Json.jOption(Json.jString),
+ fallback: undefined,
signals: [],
};
/** Load a save file. Returns an error, if not successfull. */
@@ -105,6 +107,7 @@ const save_internal: Server.SetRequest<string,string | undefined> = {
name: 'kernel.services.save',
input: Json.jString,
output: Json.jOption(Json.jString),
+ fallback: undefined,
signals: [],
};
/** Save the current session. Returns an error, if not successfull. */
@@ -140,6 +143,7 @@ const logkindTags_internal: Server.GetRequest<null,tag[]> = {
name: 'kernel.services.logkindTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -204,6 +208,7 @@ const reloadMessage_internal: Server.GetRequest<null,null> = {
name: 'kernel.services.reloadMessage',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`message`](#message) */
@@ -223,6 +228,7 @@ const fetchMessage_internal: Server.GetRequest<
updated: Json.jArray(jMessageData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`message`](#message) */
@@ -295,6 +301,7 @@ const setLogs_internal: Server.SetRequest<boolean,null> = {
name: 'kernel.services.setLogs',
input: Json.jBoolean,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Turn logs monitoring on/off */
@@ -305,6 +312,7 @@ const getLogs_internal: Server.GetRequest<null,log[]> = {
name: 'kernel.services.getLogs',
input: Json.jNull,
output: Json.jArray(jLog),
+ fallback: [],
signals: [],
};
/** Flush the last emitted logs since last call (max 100) */
diff --git a/ivette/src/frama-c/plugins/callgraph/api/index.ts b/ivette/src/frama-c/plugins/callgraph/api/index.ts
index 1b3464675685c76c446fc3f60b725465e95802c3..1cbea161542c8a67dd8f057f2641aad72b5094a0 100644
--- a/ivette/src/frama-c/plugins/callgraph/api/index.ts
+++ b/ivette/src/frama-c/plugins/callgraph/api/index.ts
@@ -112,6 +112,7 @@ const edgeKindTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.callgraph.edgeKindTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -176,6 +177,7 @@ const getCallgraph_internal: Server.GetRequest<null,graph | undefined> = {
name: 'plugins.callgraph.getCallgraph',
input: Json.jNull,
output: Json.jOption(jGraph),
+ fallback: undefined,
signals: [],
};
/** Getter for state [`callgraph`](#callgraph) */
@@ -199,6 +201,7 @@ const getIsComputed_internal: Server.GetRequest<null,boolean> = {
name: 'plugins.callgraph.getIsComputed',
input: Json.jNull,
output: Json.jBoolean,
+ fallback: false,
signals: [],
};
/** Getter for state [`isComputed`](#iscomputed) */
@@ -217,6 +220,7 @@ const compute_internal: Server.ExecRequest<null,null> = {
name: 'plugins.callgraph.compute',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Compute the callgraph for the current project */
diff --git a/ivette/src/frama-c/plugins/callgraph/index.tsx b/ivette/src/frama-c/plugins/callgraph/index.tsx
index 5671107839a555f06a8732e6beee43de4a9788b8..a4450256bf6071dbe1529bd6c2b9bc2d9bef7813 100644
--- a/ivette/src/frama-c/plugins/callgraph/index.tsx
+++ b/ivette/src/frama-c/plugins/callgraph/index.tsx
@@ -120,9 +120,7 @@ function Callgraph() : JSX.Element {
const graph = States.useSyncValue(CgAPI.callgraph);
const [cy, setCy] = React.useState<Cy.Core>();
const [cs] = useGlobalState(CallstackState);
- const callstack = States.useRequest(
- ValuesAPI.getCallstackInfo, cs, { onError: [] }
- );
+ const callstack = States.useRequestValue(ValuesAPI.getCallstackInfo, cs);
const scope = States.useCurrentScope();
const layout = { name: 'cola', nodeSpacing: 32 };
const computedStyle = getComputedStyle(document.documentElement);
@@ -142,7 +140,7 @@ function Callgraph() : JSX.Element {
// Callstack selection
React.useEffect(() => {
- cy && selectCallstack(cy, callstack ?? []);
+ cy && selectCallstack(cy, callstack);
}, [cy, callstack]);
// Click on graph
diff --git a/ivette/src/frama-c/plugins/dive/api/index.ts b/ivette/src/frama-c/plugins/dive/api/index.ts
index 7c5c50aff4ea1c8cf6bfd0a5e2e5efe4cb80f8e5..9305025278bf9c5b2dc982cc8c362e7d040f15f9 100644
--- a/ivette/src/frama-c/plugins/dive/api/index.ts
+++ b/ivette/src/frama-c/plugins/dive/api/index.ts
@@ -212,6 +212,7 @@ const nodeKindTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.dive.nodeKindTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -241,6 +242,7 @@ const taintTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.dive.taintTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -272,6 +274,7 @@ const explorationTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.dive.explorationTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -304,6 +307,7 @@ const nodeSpecialRangeTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.dive.nodeSpecialRangeTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -478,6 +482,7 @@ const reloadGraph_internal: Server.GetRequest<null,null> = {
name: 'plugins.dive.reloadGraph',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`graph`](#graph) */
@@ -497,6 +502,7 @@ const fetchGraph_internal: Server.GetRequest<
updated: Json.jArray(jGraphData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`graph`](#graph) */
@@ -526,6 +532,7 @@ const window_internal: Server.SetRequest<explorationWindow,null> = {
name: 'plugins.dive.window',
input: jExplorationWindow,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Set the exploration window */
@@ -536,6 +543,7 @@ const clear_internal: Server.ExecRequest<null,null> = {
name: 'plugins.dive.clear',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Erase the graph and start over with an empty one */
@@ -546,6 +554,7 @@ const add_internal: Server.ExecRequest<marker,nodeId | undefined> = {
name: 'plugins.dive.add',
input: jMarker,
output: Json.jOption(jNodeId),
+ fallback: undefined,
signals: [],
};
/** Add a node to the graph */
@@ -556,6 +565,7 @@ const explore_internal: Server.ExecRequest<nodeId,null> = {
name: 'plugins.dive.explore',
input: jNodeId,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Explore the graph starting from an existing vertex */
@@ -566,6 +576,7 @@ const show_internal: Server.ExecRequest<nodeId,null> = {
name: 'plugins.dive.show',
input: jNodeId,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Show the dependencies of an existing vertex */
@@ -576,6 +587,7 @@ const hide_internal: Server.ExecRequest<nodeId,null> = {
name: 'plugins.dive.hide',
input: jNodeId,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Hide the dependencies of an existing vertex */
diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
index 7ba1bef3f85e00847d111d3898205515c6d436da..e06725e6f2e002ecc4fc224cadfe451dca10b882 100644
--- a/ivette/src/frama-c/plugins/eva/DomainStates.tsx
+++ b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
@@ -44,7 +44,7 @@ export function EvaStates(): JSX.Element {
const [filter, setFilter] = useGlobalState(globalFilter);
const requestArg = marker ? [marker, filter] : undefined;
- const states = States.useRequest(Eva.getStates, requestArg);
+ const states = States.useRequestResponse(Eva.getStates, requestArg);
React.useEffect(() => {
if (states && states.length > 0) {
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 64ad2c81094c7820d74ccf9dc4e5d1439a878d3d..2e5a1eec5f83acdd15aae5b839502f64946bfe86 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -96,6 +96,7 @@ const getComputationState_internal: Server.GetRequest<
name: 'plugins.eva.general.getComputationState',
input: Json.jNull,
output: jComputationStateType,
+ fallback: computationStateTypeDefault,
signals: [],
};
/** Getter for state [`computationState`](#computationstate) */
@@ -136,6 +137,7 @@ const getCallers_internal: Server.GetRequest<decl,CallSite[]> = {
name: 'plugins.eva.general.getCallers',
input: jDecl,
output: Json.jArray(jCallSite),
+ fallback: [],
signals: [ { name: 'plugins.eva.general.signalComputationState' } ],
};
/** Get the list of call sites for a function */
@@ -146,6 +148,7 @@ const getCallees_internal: Server.GetRequest<marker,decl[]> = {
name: 'plugins.eva.general.getCallees',
input: jMarker,
output: Json.jArray(jDecl),
+ fallback: [],
signals: [ { name: 'plugins.eva.general.signalComputationState' } ],
};
/** Return the functions pointed to by a function pointer */
@@ -184,6 +187,7 @@ const reloadFunctions_internal: Server.GetRequest<null,null> = {
name: 'plugins.eva.general.reloadFunctions',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`functions`](#functions) */
@@ -203,6 +207,7 @@ const fetchFunctions_internal: Server.GetRequest<
updated: Json.jArray(jFunctionsData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`functions`](#functions) */
@@ -263,6 +268,7 @@ const getDeadCode_internal: Server.GetRequest<decl,deadCode | undefined> = {
name: 'plugins.eva.general.getDeadCode',
input: jDecl,
output: Json.jOption(jDeadCode),
+ fallback: undefined,
signals: [ { name: 'plugins.eva.general.signalComputationState' } ],
};
/** Get the lists of unreachable and of non terminating statements in a function */
@@ -304,6 +310,7 @@ const taintStatusTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.eva.general.taintStatusTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -338,6 +345,7 @@ const taintedLvalues_internal: Server.GetRequest<decl,LvalueTaints[]> = {
name: 'plugins.eva.general.taintedLvalues',
input: jDecl,
output: Json.jArray(jLvalueTaints),
+ fallback: [],
signals: [ { name: 'plugins.eva.general.signalComputationState' } ],
};
/** Get the tainted lvalues of a given function */
@@ -377,6 +385,7 @@ const reloadProperties_internal: Server.GetRequest<null,null> = {
name: 'plugins.eva.general.reloadProperties',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`properties`](#properties) */
@@ -396,6 +405,7 @@ const fetchProperties_internal: Server.GetRequest<
updated: Json.jArray(jPropertiesData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`properties`](#properties) */
@@ -461,6 +471,7 @@ const alarmCategoryTags_internal: Server.GetRequest<null,tag[]> = {
name: 'plugins.eva.general.alarmCategoryTags',
input: Json.jNull,
output: Json.jArray(jTag),
+ fallback: [],
signals: [],
};
/** Registered tags for the above type. */
@@ -598,6 +609,7 @@ const getProgramStats_internal: Server.GetRequest<null,programStatsType> = {
name: 'plugins.eva.general.getProgramStats',
input: Json.jNull,
output: jProgramStatsType,
+ fallback: programStatsTypeDefault,
signals: [],
};
/** Getter for state [`programStats`](#programstats) */
@@ -662,6 +674,7 @@ const reloadFunctionStats_internal: Server.GetRequest<null,null> = {
name: 'plugins.eva.general.reloadFunctionStats',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`functionStats`](#functionstats) */
@@ -681,6 +694,7 @@ const fetchFunctionStats_internal: Server.GetRequest<
updated: Json.jArray(jFunctionStatsData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`functionStats`](#functionstats) */
@@ -715,6 +729,7 @@ const getStates_internal: Server.GetRequest<
input: Json.jPair( jMarker, Json.jBoolean,),
output: Json.jArray(
Json.jTriple( Json.jString, Json.jString, Json.jString,)),
+ fallback: [],
signals: [ { name: 'plugins.eva.general.signalComputationState' } ],
};
/** Get the domain states about the given marker */
diff --git a/ivette/src/frama-c/plugins/eva/api/values/index.ts b/ivette/src/frama-c/plugins/eva/api/values/index.ts
index 2e8f6a15248b31a5ff844b00d5ef3d330d78005b..e5dfbd41bb73978a2bcc2adb8f5665c168cf6977 100644
--- a/ivette/src/frama-c/plugins/eva/api/values/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/values/index.ts
@@ -106,6 +106,7 @@ const getCallstacks_internal: Server.GetRequest<marker[],callstack[]> = {
name: 'plugins.eva.values.getCallstacks',
input: Json.jArray(jMarker),
output: Json.jArray(jCallstack),
+ fallback: [],
signals: [],
};
/** Callstacks for markers */
@@ -116,6 +117,7 @@ const getCallstackInfo_internal: Server.GetRequest<callstack,callsite[]> = {
name: 'plugins.eva.values.getCallstackInfo',
input: jCallstack,
output: Json.jArray(jCallsite),
+ fallback: [],
signals: [],
};
/** Callstack Description */
@@ -129,6 +131,7 @@ const getStmtInfo_internal: Server.GetRequest<
name: 'plugins.eva.values.getStmtInfo',
input: jMarker,
output: Json.jObject({ fct: Json.jString, rank: Json.jNumber,}),
+ fallback: { fct: '', rank: 0 },
signals: [],
};
/** Stmt Information */
@@ -152,6 +155,8 @@ const getProbeInfo_internal: Server.GetRequest<
effects: Json.jBoolean,
condition: Json.jBoolean,
}),
+ fallback: { evaluable: false, code: undefined, stmt: undefined,
+ effects: false, condition: false },
signals: [],
};
/** Probe informations */
@@ -216,6 +221,8 @@ const getValues_internal: Server.GetRequest<
vThen: Json.jOption(jEvaluation),
vElse: Json.jOption(jEvaluation),
}),
+ fallback: { vBefore: undefined, vAfter: undefined, vThen: undefined,
+ vElse: undefined },
signals: [],
};
/** Abstract values for the given marker */
diff --git a/ivette/src/frama-c/plugins/pivot/api/general/index.ts b/ivette/src/frama-c/plugins/pivot/api/general/index.ts
index 5fedbe2ae87c0b9ecd59fcceaff7724c25bc198a..92549423c3c05d29ca04b1038f0aa69853fe4223 100644
--- a/ivette/src/frama-c/plugins/pivot/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/pivot/api/general/index.ts
@@ -62,6 +62,7 @@ const getPivotState_internal: Server.GetRequest<null,tableStateType> = {
name: 'plugins.pivot.general.getPivotState',
input: Json.jNull,
output: jTableStateType,
+ fallback: tableStateTypeDefault,
signals: [],
};
/** Getter for state [`pivotState`](#pivotstate) */
@@ -80,6 +81,7 @@ const compute_internal: Server.ExecRequest<null,null> = {
name: 'plugins.pivot.general.compute',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Computes the pivot table. */
diff --git a/ivette/src/frama-c/plugins/studia/api/studia/index.ts b/ivette/src/frama-c/plugins/studia/api/studia/index.ts
index a3fe7357afde8f92a536658ccccbb4534ab4fdee..958174eedacbb8b56664ef2cbfeb39a1673931e5 100644
--- a/ivette/src/frama-c/plugins/studia/api/studia/index.ts
+++ b/ivette/src/frama-c/plugins/studia/api/studia/index.ts
@@ -77,6 +77,7 @@ const getReadsLval_internal: Server.GetRequest<marker,effects> = {
name: 'plugins.studia.studia.getReadsLval',
input: jMarker,
output: jEffects,
+ fallback: effectsDefault,
signals: [],
};
/** Get the list of statements that read a lval. */
@@ -87,6 +88,7 @@ const getWritesLval_internal: Server.GetRequest<marker,effects> = {
name: 'plugins.studia.studia.getWritesLval',
input: jMarker,
output: jEffects,
+ fallback: effectsDefault,
signals: [],
};
/** Get the list of statements that write a lval. */
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index c045e516ff9ff037f78eee2d85c92be486316c57..151220bcedd7dc5b02a3465f53aa130fa232edd1 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -88,6 +88,7 @@ const getProvers_internal: Server.GetRequest<null,prover[]> = {
name: 'plugins.wp.getProvers',
input: Json.jNull,
output: Json.jArray(jProver),
+ fallback: [],
signals: [],
};
/** Getter for state [`provers`](#provers) */
@@ -98,6 +99,7 @@ const setProvers_internal: Server.SetRequest<prover[],null> = {
name: 'plugins.wp.setProvers',
input: Json.jArray(jProver),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Setter for state [`provers`](#provers) */
@@ -122,6 +124,7 @@ const getProcess_internal: Server.GetRequest<null,number> = {
name: 'plugins.wp.getProcess',
input: Json.jNull,
output: Json.jNumber,
+ fallback: 0,
signals: [],
};
/** Getter for state [`process`](#process) */
@@ -132,6 +135,7 @@ const setProcess_internal: Server.SetRequest<number,null> = {
name: 'plugins.wp.setProcess',
input: Json.jNumber,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Setter for state [`process`](#process) */
@@ -156,6 +160,7 @@ const getTimeout_internal: Server.GetRequest<null,number> = {
name: 'plugins.wp.getTimeout',
input: Json.jNull,
output: Json.jNumber,
+ fallback: 0,
signals: [],
};
/** Getter for state [`timeout`](#timeout) */
@@ -166,6 +171,7 @@ const setTimeout_internal: Server.SetRequest<number,null> = {
name: 'plugins.wp.setTimeout',
input: Json.jNumber,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Setter for state [`timeout`](#timeout) */
@@ -221,6 +227,7 @@ const reloadProverInfos_internal: Server.GetRequest<null,null> = {
name: 'plugins.wp.reloadProverInfos',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`ProverInfos`](#proverinfos) */
@@ -240,6 +247,7 @@ const fetchProverInfos_internal: Server.GetRequest<
updated: Json.jArray(jProverInfosData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`ProverInfos`](#proverinfos) */
@@ -441,6 +449,7 @@ const reloadGoals_internal: Server.GetRequest<null,null> = {
name: 'plugins.wp.reloadGoals',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`goals`](#goals) */
@@ -459,6 +468,7 @@ const fetchGoals_internal: Server.GetRequest<
updated: Json.jArray(jGoalsData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`goals`](#goals) */
@@ -490,6 +500,7 @@ const generateRTEGuards_internal: Server.ExecRequest<marker,null> = {
name: 'plugins.wp.generateRTEGuards',
input: jMarker,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Generate RTE guards for the function */
@@ -500,6 +511,7 @@ const startProofs_internal: Server.ExecRequest<marker,null> = {
name: 'plugins.wp.startProofs',
input: jMarker,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Generate goals and run provers */
@@ -523,6 +535,7 @@ const getScheduledTasks_internal: Server.GetRequest<
done: Json.jNumber,
todo: Json.jNumber,
}),
+ fallback: { procs: 0, active: 0, done: 0, todo: 0 },
signals: [ { name: 'plugins.wp.serverActivity' } ],
};
/** Scheduled tasks in proof server */
@@ -536,6 +549,7 @@ const cancelProofTasks_internal: Server.SetRequest<null,null> = {
name: 'plugins.wp.cancelProofTasks',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Cancel all scheduled proof tasks */
diff --git a/ivette/src/frama-c/plugins/wp/api/tac/index.ts b/ivette/src/frama-c/plugins/wp/api/tac/index.ts
index 57a834a29eb7ac4b023a98604d8150c6314ff88f..147176b824eb92490f9e98409ccd85b30649a6b4 100644
--- a/ivette/src/frama-c/plugins/wp/api/tac/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tac/index.ts
@@ -228,6 +228,7 @@ const reloadTactical_internal: Server.GetRequest<null,null> = {
name: 'plugins.wp.tac.reloadTactical',
input: Json.jNull,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Force full reload for array [`tactical`](#tactical) */
@@ -247,6 +248,7 @@ const fetchTactical_internal: Server.GetRequest<
updated: Json.jArray(jTacticalData),
pending: Json.jNumber,
}),
+ fallback: { reload: false, removed: [], updated: [], pending: 0 },
signals: [],
};
/** Data fetcher for array [`tactical`](#tactical) */
@@ -277,6 +279,7 @@ const configureTactics_internal: Server.ExecRequest<node,null> = {
name: 'plugins.wp.tac.configureTactics',
input: jNode,
output: Json.jNull,
+ fallback: null,
signals: [ { name: 'plugins.wp.tip.printStatus' } ],
};
/** Configure all tactics */
@@ -295,6 +298,7 @@ const setParameter_internal: Server.ExecRequest<
value: Json.jAny,
}),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Configure tactical parameter */
@@ -308,6 +312,7 @@ const applyTactic_internal: Server.ExecRequest<tactic,node[]> = {
name: 'plugins.wp.tac.applyTactic',
input: jTactic,
output: Json.jArray(jNode),
+ fallback: [],
signals: [],
};
/** Applies the (configured) tactic */
@@ -318,6 +323,7 @@ const applyTacticAndProve_internal: Server.ExecRequest<tactic,node[]> = {
name: 'plugins.wp.tac.applyTacticAndProve',
input: jTactic,
output: Json.jArray(jNode),
+ fallback: [],
signals: [],
};
/** Applies tactic and run provers on children */
diff --git a/ivette/src/frama-c/plugins/wp/api/tip/index.ts b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
index 13cda42e7e9adad823ac2d2660b52f5123fcd050..da50ab37d512c0a688acf42a8d1ab05cf56d0801 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -126,6 +126,9 @@ const getNodeInfos_internal: Server.GetRequest<
path: Json.jArray(jNode),
children: Json.jArray(jNode),
}),
+ fallback: { title: '', proved: false, pending: 0, size: 0, stats: '',
+ results: [], tactic: undefined, header: undefined,
+ childLabel: undefined, path: [], children: [] },
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Proof node information */
@@ -144,6 +147,7 @@ const getResult_internal: Server.GetRequest<
name: 'plugins.wp.tip.getResult',
input: Json.jObject({ node: jNode, prover: jProver,}),
output: jResult,
+ fallback: resultDefault,
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Result for specified node and prover */
@@ -173,6 +177,8 @@ const getProofStatus_internal: Server.GetRequest<
tactic: Json.jOption(jTactic),
children: Json.jArray(jNode),
}),
+ fallback: { size: 0, index: 0, pending: 0, current: nodeDefault,
+ parents: [], tactic: undefined, children: [] },
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Current Proof Status of a Goal */
@@ -187,6 +193,7 @@ const goForward_internal: Server.SetRequest<goal,null> = {
name: 'plugins.wp.tip.goForward',
input: jGoal,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Go to to first pending node, or root if none */
@@ -197,6 +204,7 @@ const goToRoot_internal: Server.SetRequest<goal,null> = {
name: 'plugins.wp.tip.goToRoot',
input: jGoal,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Go to root of proof tree */
@@ -207,6 +215,7 @@ const goToIndex_internal: Server.SetRequest<[ goal, number ],null> = {
name: 'plugins.wp.tip.goToIndex',
input: Json.jPair( jGoal, Json.jNumber,),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Go to k-th pending node of proof tree */
@@ -217,6 +226,7 @@ const goToNode_internal: Server.SetRequest<node,null> = {
name: 'plugins.wp.tip.goToNode',
input: jNode,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Set current node of associated proof tree */
@@ -227,6 +237,7 @@ const clearNode_internal: Server.SetRequest<node,null> = {
name: 'plugins.wp.tip.clearNode',
input: jNode,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Cancel all node results and sub-tree (if any) */
@@ -237,6 +248,7 @@ const clearNodeTactic_internal: Server.SetRequest<node,null> = {
name: 'plugins.wp.tip.clearNodeTactic',
input: jNode,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Cancel node current tactic */
@@ -247,6 +259,7 @@ const clearParentTactic_internal: Server.SetRequest<node,null> = {
name: 'plugins.wp.tip.clearParentTactic',
input: jNode,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Cancel parent node tactic */
@@ -257,6 +270,7 @@ const clearGoal_internal: Server.SetRequest<goal,null> = {
name: 'plugins.wp.tip.clearGoal',
input: jGoal,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Remove the complete goal proof tree */
@@ -337,6 +351,7 @@ const printSequent_internal: Server.GetRequest<
unmangled: Json.jOption(Json.jBoolean),
}),
output: jText,
+ fallback: textDefault,
signals: [ { name: 'plugins.wp.tip.printStatus' } ],
};
/** Pretty-print the associated node */
@@ -351,6 +366,7 @@ const clearSelection_internal: Server.SetRequest<node,null> = {
name: 'plugins.wp.tip.clearSelection',
input: jNode,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Reset node selection */
@@ -369,6 +385,7 @@ const setSelection_internal: Server.SetRequest<
extend: Json.jOption(Json.jBoolean),
}),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Set node selection */
@@ -388,6 +405,7 @@ const getSelection_internal: Server.GetRequest<
part: Json.jOption(jPart),
term: Json.jOption(jTerm),
}),
+ fallback: { part: undefined, term: undefined },
signals: [ { name: 'plugins.wp.tip.printStatus' },
{ name: 'plugins.wp.tip.proofStatus' } ],
};
@@ -409,6 +427,7 @@ const runProvers_internal: Server.SetRequest<
provers: Json.jOption(Json.jArray(jProver)),
}),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Schedule provers on proof node */
@@ -428,6 +447,7 @@ const killProvers_internal: Server.SetRequest<
provers: Json.jOption(Json.jArray(jProver)),
}),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Interrupt running provers on proof node */
@@ -447,6 +467,7 @@ const clearProvers_internal: Server.SetRequest<
provers: Json.jOption(Json.jArray(jProver)),
}),
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Remove prover results from proof node */
@@ -467,6 +488,7 @@ const getScriptStatus_internal: Server.GetRequest<
script: Json.jOption(Json.jString),
saved: Json.jBoolean,
}),
+ fallback: { proof: false, script: undefined, saved: false },
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Script Status for a given Goal */
@@ -480,6 +502,7 @@ const saveScript_internal: Server.SetRequest<goal,null> = {
name: 'plugins.wp.tip.saveScript',
input: jGoal,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Save Script for the Goal */
@@ -490,6 +513,7 @@ const runScript_internal: Server.SetRequest<goal,null> = {
name: 'plugins.wp.tip.runScript',
input: jGoal,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Replay Saved Script for the Goal (if any) */
@@ -500,6 +524,7 @@ const clearProofScript_internal: Server.SetRequest<goal,null> = {
name: 'plugins.wp.tip.clearProofScript',
input: jGoal,
output: Json.jNull,
+ fallback: null,
signals: [],
};
/** Clear Proof and Remove any Saved Script for the Goal */
diff --git a/ivette/src/frama-c/plugins/wp/seq.tsx b/ivette/src/frama-c/plugins/wp/seq.tsx
index 75ea1082ec1d493467ba8ab6844775af85dad4dc..287f3c528706d74a4fe543ac4a2367939f9d01a9 100644
--- a/ivette/src/frama-c/plugins/wp/seq.tsx
+++ b/ivette/src/frama-c/plugins/wp/seq.tsx
@@ -165,17 +165,8 @@ export interface GoalViewProps {
export function GoalView(props: GoalViewProps): JSX.Element {
const { node, locked } = props;
- const jtext = States.useRequest(TIP.printSequent, props, {
- pending: null,
- offline: undefined,
- onError: '',
- }) ?? null;
- const { part, term } =
- States.useRequest(TIP.getSelection, node, {
- pending: null,
- offline: {},
- onError: {},
- }) ?? {};
+ const jtext = States.useRequestStable(TIP.printSequent, props);
+ const { part, term } = States.useRequestStable(TIP.getSelection, node);
const proxy = React.useMemo(() => new TextProxy(), []);
const sequent = React.useMemo(() => new Sequent(jtext), [jtext]);
React.useEffect(() => proxy.updateContents(sequent.text), [proxy, sequent]);
diff --git a/ivette/src/frama-c/plugins/wp/tac.tsx b/ivette/src/frama-c/plugins/wp/tac.tsx
index 3de7f9f55cb604b14f88c0af0d561a0ed41e224d..cc3f0f786dfd8e22fa7392eb8b1d918e139b61f0 100644
--- a/ivette/src/frama-c/plugins/wp/tac.tsx
+++ b/ivette/src/frama-c/plugins/wp/tac.tsx
@@ -162,9 +162,7 @@ export interface ProverSelection {
export function Provers(props: ProverSelection): JSX.Element {
const { node, selected, setSelected } = props;
- const { results=[] } = States.useRequest(
- TIP.getNodeInfos, node, { pending: null, onError: null }
- ) ?? {};
+ const { results=[] } = States.useRequestStable(TIP.getNodeInfos, node);
const [ provers=[], setProvers ] = States.useSyncState(WP.provers);
const setItems = (prvs: string[]): void => setProvers(prvs.map(WP.jProver));
const children = [...provers].sort().map((prover) => {
@@ -380,9 +378,7 @@ function Parameter(props: ParameterProps): JSX.Element | null
export function ConfigureProver(props: ProverSelection): JSX.Element {
const { node, selected: prover, setSelected } = props;
const { descr } = States.useSyncArrayElt(WP.ProverInfos, prover) ?? {};
- const result = States.useRequest(
- TIP.getResult, { node, prover }, { pending: null, onError: null }
- ) ?? WP.resultDefault;
+ const result = States.useRequestStable(TIP.getResult, { node, prover });
const [process = 1, setProcess] = States.useSyncState(WP.process);
const [timeout = 1, setTimeout] = States.useSyncState(WP.timeout);
const { icon, kind, clear=true, running=false, play=false, forward=0 } =
@@ -530,7 +526,7 @@ function getStatusDescription(tactical: TAC.tacticalData): StatusDescr {
export function ConfigureTactic(props: TacticSelection): JSX.Element {
const { node, locked, selected: tactic, setSelected } = props;
const tactical = useTactic(tactic);
- States.useRequest(TAC.configureTactics, node, { onError: null });
+ const { pending } = States.useRequestStatus(TAC.configureTactics, node);
const { status, label, title, params } = tactical;
const isReady = !locked && status==='Applicable';
const display = !!tactic && (locked || status !== 'NotApplicable');
@@ -558,7 +554,7 @@ export function ConfigureTactic(props: TacticSelection): JSX.Element {
>
<Item
key='tactic'
- icon='TUNINGS'
+ icon={ pending ? 'EXECUTE' : 'TUNINGS' }
title='Selected Tactic Configuration'
className="wp-config-tactic"
label={label} />
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index 633427b419bb3eaa57d32c8a26ce36f2fc751b99..3fe0bd22009cc9402ea3ff33e6c80c700e2a4375 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -130,13 +130,10 @@ function Node(props: NodeProps): JSX.Element {
child = false,
hasChildren = false,
} = props;
- const debug = `#${node}`;
const {
- title = debug, childLabel = 'Script', header,
+ title, childLabel = 'Script', header,
proved = false, pending = 0, size = 0
- } = States.useRequest(
- TIP.getNodeInfos, node, { pending: null, onError: null }
- ) ?? {};
+ } = States.useRequestStable(TIP.getNodeInfos, node);
const elt = cellRef.current;
const current = !child && !parent;
React.useEffect(() => {
@@ -238,11 +235,8 @@ export interface ServerActivity {
}
export function useServerActivity(): ServerActivity {
- const rq = States.useRequest(WP.getScheduledTasks, null, { pending: null });
- const procs = rq ? rq.procs : 0;
- const active = rq ? rq.active : 0;
- const done = rq ? rq.done : 0;
- const todo = rq ? rq.todo : 0;
+ const { procs, active, done, todo } =
+ States.useRequestStable(WP.getScheduledTasks, null);
const running = active + todo > 0;
return { procs, active, done, todo, running };
}
@@ -271,14 +265,15 @@ export function TIPView(props: TIPProps): JSX.Element {
States.useSyncArrayElt(WP.goals, goal) ?? WP.goalsDataDefault;
// --- proof status
const {
- current, index = -1, pending = 0, size = 0,
+ current, index, pending, size,
tactic: nodeTactic, parents = [], children = [],
- } = States.useRequest(TIP.getProofStatus, goal ? {
- main: goal, unproved, subtree,
- } : undefined, { pending: null }) ?? {};
+ } = States.useRequestStable(
+ TIP.getProofStatus,
+ goal ? { main: goal, unproved, subtree } : undefined,
+ );
// --- script status
- const { saved = false, proof = false, script } =
- States.useRequest(TIP.getScriptStatus, goal, { pending: null }) ?? {};
+ const { saved, proof, script } =
+ States.useRequestStable(TIP.getScriptStatus, goal);
// --- provers
const available = States.useSyncArrayData(WP.ProverInfos);
const [provers = [], setProvers] = States.useSyncState(WP.provers);
diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts
index b110462dc795dd30a01d4c640724f66d43c2042c..4fd36323ec416eafd9e2bc3fbf0cf186de54e9b9 100644
--- a/ivette/src/frama-c/server.ts
+++ b/ivette/src/frama-c/server.ts
@@ -158,7 +158,7 @@ export function useStatus(): Status {
return status;
}
-const running = (st: Status): boolean =>
+export const isRunningStatus = (st: Status): boolean =>
(st === Status.ON || st === Status.CMD);
/**
@@ -167,7 +167,7 @@ const running = (st: Status): boolean =>
* defined by status `ON` or `CMD`.
*/
export function isRunning(): boolean {
- return running(status);
+ return isRunningStatus(status);
}
/**
@@ -229,8 +229,8 @@ function _status(newStatus: Status): void {
const oldStatus = status;
status = newStatus;
STATUS.emit(newStatus);
- const oldRun = running(oldStatus);
- const newRun = running(newStatus);
+ const oldRun = isRunningStatus(oldStatus);
+ const newRun = isRunningStatus(newStatus);
if (oldRun && !newRun) SHUTDOWN.emit();
if (!oldRun && newRun) READY.emit();
}
@@ -775,6 +775,8 @@ export interface Request<Kd extends RqKind, In, Out> {
input: Json.Decoder<In>;
/** Decoder of output parameters. */
output: Json.Decoder<Out>;
+ /** Fallback output value */
+ fallback: Out;
/** Signals the request depends on */
signals: Array<Signal>;
}
@@ -783,7 +785,7 @@ export type GetRequest<In, Out> = Request<RqKind.GET, In, Out>;
export type SetRequest<In, Out> = Request<RqKind.SET, In, Out>;
export type ExecRequest<In, Out> = Request<RqKind.EXEC, In, Out>;
-export interface Response<Data> extends Promise<Data> {
+export interface ServerTask<Data> extends Promise<Data> {
kill?: () => void;
}
@@ -796,22 +798,18 @@ export interface Response<Data> extends Promise<Data> {
export function send<In, Out>(
request: Request<RqKind, In, Out>,
param: In,
-): Response<Out> {
+): ServerTask<Out> {
if (!isRunning()) return Promise.reject('Server not running');
if (!request.name) return Promise.reject('Undefined request');
const rid = `RQ.${rqCount}`;
rqCount += 1;
const { kind, name } = request;
- logModel.registerRequest(
- {
- rid,
- kind,
- name,
- param: param as unknown as Json.json,
- statut: statutLog.PENDING
- }
- );
- const response: Response<Out> = new Promise<Out>((resolve, reject) => {
+ logModel.registerRequest({
+ rid, kind, name,
+ param: param as unknown as Json.json,
+ statut: statutLog.PENDING
+ });
+ const response: ServerTask<Out> = new Promise<Out>((resolve, reject) => {
const unwrap = (js: Json.json): void => {
try {
resolve(request.output(js));
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 63a83121bb999f834dc6a2884fb35128d132d457..ba94955be54c5bcec75a19311ffe66763eff6e14 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -50,87 +50,135 @@ const D = new Dome.Debug('States');
// --- Cached GET Requests
// --------------------------------------------------------------------------
-/** Options to tweak the behavior of `useRequest()`. Null values means
- keeping the last result. */
-export interface UseRequestOptions<A> {
- /** Returned value in case where the server goes offline. */
- offline?: A | null;
- /** Temporary returned value when the request is pending. */
- pending?: A | null;
- /** Returned value when the request fails. */
- onError?: A | null;
- /** Re-send the request when any of the signals are sent. */
- onSignals?: Server.Signal[];
+/** Response of `useRequestStatus()` */
+export interface RequestStatus<Out> {
+ /** Response of the current request, when available. */
+ response: Out | undefined;
+ /** Current response, or default value when undefined. */
+ value: Out;
+ /** Last returned value, until no more request or server goes offline. */
+ stable: Out;
+ /** Current request is still pending. */
+ pending: boolean;
+ /** Current request error, if any. */
+ error: string | undefined;
+ /** Interrupt currently processed request, if any. */
+ kill: () => void;
}
/**
- Cached GET request (Custom React Hook).
+ Cached requests (Custom React Hook).
- Sends the specified GET request and returns its result. The request is send
+ Sends the specified request and returns its result. The request is send
asynchronously and cached until any change in the request parameters or server
state. The change in the server state are tracked by the signals specified
when registering the request or by the one in options.onSignals if specified.
-
- Options can be used to tune more precisely the behavior of the hook.
*/
-export function useRequest<Kd extends Server.RqKind, In, Out>(
+export function useRequestStatus<Kd extends Server.RqKind, In, Out>(
rq: Server.Request<Kd, In, Out>,
- params: In | undefined,
- options: UseRequestOptions<Out> = {},
-): Out | undefined {
- const initial = options.offline ?? undefined;
- const [response, setResponse] = React.useState<Out | undefined>(initial);
- const updateResponse = Dome.useProtected(
- (opt: Out | undefined | null): void => {
- if (opt !== null) setResponse(opt);
- }
- );
+ prm: In | undefined,
+ ...signals: Server.Signal[]
+): RequestStatus<Out> {
+
+ // Request Status Management
+ const NOP = (): void => { };
+ const killer = React.useRef(NOP);
+ const [response, setResponse] = React.useState<Out>();
+ const [stable, setStable] = React.useState<Out>(rq.fallback);
+ const [error, setError] = React.useState<string>();
+ const updateStable = Dome.useProtected(setStable);
+ const updateResponse = Dome.useProtected(setResponse);
+ const updateError = Dome.useProtected(setError);
+
// Fetch Request
- async function trigger(): Promise<void> {
- if (Server.isRunning() && params !== undefined) {
- try {
- updateResponse(options.pending);
- const r = await Server.send(rq, params);
- updateResponse(r);
- } catch (error) {
- if (options.onError === undefined) {
- D.error(`Fail in useRequest '${rq.name}'. ${error}`);
+ const trigger: () => void =
+ React.useCallback(
+ async function (): Promise<void> {
+ updateError(undefined);
+ updateResponse(undefined);
+ try {
+ if (Server.isRunning() && prm !== undefined) {
+ const task = Server.send(rq, prm);
+ killer.current = task.kill ?? NOP;
+ const result = await task;
+ updateResponse(result);
+ updateStable(result);
+ } else {
+ updateStable(rq.fallback);
+ }
+ } catch (err) {
+ updateError(`${err}`);
+ updateStable(rq.fallback);
+ } finally {
+ killer.current = NOP;
}
- updateResponse(options.onError);
- }
- } else {
- updateResponse(options.offline);
- }
- }
+ }, [ rq, prm, updateStable, updateResponse, updateError ]);
// Server & Cache Management
- Server.useStatus();
- const cached = React.useRef('');
+ const running = Server.isRunningStatus(Server.useStatus());
+ const cached = running ? JSON.stringify([rq.name, prm]) : null;
React.useEffect(() => {
- if (Server.isRunning()) {
- const footprint = JSON.stringify([rq.name, params]);
- if (cached.current !== footprint) {
- cached.current = footprint;
- trigger();
- }
+ if (cached !== null) {
+ trigger();
} else {
- if (cached.current !== '') {
- cached.current = '';
- updateResponse(options.offline);
- }
+ setResponse(undefined);
+ setStable(rq.fallback);
+ setError(undefined);
+ killer.current = NOP;
}
- });
+ }, [rq, trigger, cached] );
// Signal Management
- const signals = rq.signals.concat(options.onSignals ?? []);
+ const rqsignals = rq.signals.concat(signals);
React.useEffect(() => {
- signals.forEach((s) => Server.onSignal(s, trigger));
+ rqsignals.forEach((s) => Server.onSignal(s, trigger));
return () => {
- signals.forEach((s) => Server.offSignal(s, trigger));
+ rqsignals.forEach((s) => Server.offSignal(s, trigger));
};
});
- return response;
+ // Full Response
+ const pending =
+ running &&
+ prm !== undefined &&
+ response === undefined &&
+ error === undefined;
+ const value = response ?? rq.fallback;
+ return {
+ response, value, stable, error, pending,
+ kill: killer.current,
+ };
+}
+
+// --------------------------------------------------------------------------
+// --- useRequest shortcurs
+// --------------------------------------------------------------------------
+
+/** Shortcut to `useRequestStatus().response */
+export function useRequestResponse<Kd extends Server.RqKind, In, Out>(
+ rq: Server.Request<Kd, In, Out>,
+ prm: In | undefined,
+ ...signals: Server.Signal[]
+): Out | undefined {
+ return useRequestStatus(rq, prm, ...signals).response;
+}
+
+/** Shortcut to `useRequestStatus().value */
+export function useRequestValue<Kd extends Server.RqKind, In, Out>(
+ rq: Server.Request<Kd, In, Out>,
+ prm: In | undefined,
+ ...signals: Server.Signal[]
+): Out {
+ return useRequestStatus(rq, prm, ...signals).value;
+}
+
+/** Shortcut to `useRequestStatus().stable */
+export function useRequestStable<Kd extends Server.RqKind, In, Out>(
+ rq: Server.Request<Kd, In, Out>,
+ prm: In | undefined,
+ ...signals: Server.Signal[]
+): Out {
+ return useRequestStatus(rq, prm, ...signals).stable;
}
// --------------------------------------------------------------------------
@@ -143,12 +191,10 @@ export type Tag = {
descr?: string;
};
-const holdCurrent = { offline: null, pending: null, onError: null };
-
export type GetTags = Server.GetRequest<null, Tag[]>;
export function useTags(rq: GetTags): Map<string, Tag> {
- const tags = useRequest(rq, null, holdCurrent);
+ const tags = useRequestStable(rq, null);
return React.useMemo(() => {
const m = new Map<string, Tag>();
if (tags !== undefined)
diff --git a/ivette/src/renderer/Controller.tsx b/ivette/src/renderer/Controller.tsx
index 4986f81b54ef3bddf4ff4bdf1ea697182c7dc5f9..6a9cfe884082257f5064a19845cd02224dea0ff3 100644
--- a/ivette/src/renderer/Controller.tsx
+++ b/ivette/src/renderer/Controller.tsx
@@ -443,7 +443,9 @@ export const Status = (): JSX.Element => {
led = 'active';
blink = pending > 0;
running = 'ON';
- title = 'Server is running';
+ title = pending > 0
+ ? `Server running (${pending} pending requests)`
+ : 'Server running (idle)';
break;
case Server.Status.CMD:
led = 'positive';
@@ -473,7 +475,7 @@ export const Status = (): JSX.Element => {
return (
<>
- <LED status={led} blink={blink} />
+ <LED status={led} title={title} blink={blink} />
<Code label={running} title={title} />
</>
);
diff --git a/src/plugins/api-generator/api_generator.ml b/src/plugins/api-generator/api_generator.ml
index 829ffee06f46198eab367626ac7ac74ccdee64da..394937e3ebf4f8f1d26354baed242ddfede38776 100644
--- a/src/plugins/api-generator/api_generator.ml
+++ b/src/plugins/api-generator/api_generator.ml
@@ -353,14 +353,16 @@ let makeDeclaration fmt names d =
let prefix = String.capitalize_ascii (String.lowercase_ascii kind) in
let input = typeOfParam rq.rq_input in
let output = typeOfParam rq.rq_output in
- let makeParam fmt js = makeDecoder ~names fmt js in
+ let makeSignature fmt ty = makeDecoder ~names fmt ty in
+ let makeFallback fmt ty = makeDefault ~names fmt ty in
Format.fprintf fmt
"@[<hv 2>const %s_internal: Server.%sRequest<@,%a,@,%a@,>@] = {@\n"
self.name prefix jtype input jtype output ;
Format.fprintf fmt " kind: Server.RqKind.%s,@\n" kind ;
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 " input: %a,@\n" makeSignature input ;
+ Format.fprintf fmt " output: %a,@\n" makeSignature output ;
+ Format.fprintf fmt " fallback: %a,@\n" makeFallback output ;
Format.fprintf fmt " signals: %a,@\n"
(Pretty_utils.pp_list
~empty:"[]" ~pre:"@[<hov 2>[ " ~sep:",@ " ~suf:"@ ]@]"