From a99a6b6bcb67fe6aa4aa841b5a9b133d9f5ff17b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 6 Jun 2024 13:29:47 +0200
Subject: [PATCH] [ivette] refactor useRequest
---
ivette/src/dome/renderer/dome.tsx | 7 +-
ivette/src/frama-c/kernel/ASTinfo.tsx | 4 +-
ivette/src/frama-c/kernel/ASTview.tsx | 38 ++--
ivette/src/frama-c/kernel/SourceCode.tsx | 2 +-
ivette/src/frama-c/kernel/api/ast/index.ts | 18 ++
.../src/frama-c/kernel/api/project/index.ts | 2 +
.../frama-c/kernel/api/properties/index.ts | 5 +
.../src/frama-c/kernel/api/services/index.ts | 8 +
.../frama-c/plugins/callgraph/api/index.ts | 4 +
.../src/frama-c/plugins/callgraph/index.tsx | 6 +-
ivette/src/frama-c/plugins/dive/api/index.ts | 12 ++
.../src/frama-c/plugins/eva/DomainStates.tsx | 2 +-
.../frama-c/plugins/eva/api/general/index.ts | 15 ++
.../frama-c/plugins/eva/api/values/index.ts | 7 +
.../plugins/pivot/api/general/index.ts | 2 +
.../plugins/studia/api/studia/index.ts | 2 +
ivette/src/frama-c/plugins/wp/api/index.ts | 14 ++
.../src/frama-c/plugins/wp/api/tac/index.ts | 6 +
.../src/frama-c/plugins/wp/api/tip/index.ts | 25 +++
ivette/src/frama-c/plugins/wp/seq.tsx | 13 +-
ivette/src/frama-c/plugins/wp/tac.tsx | 12 +-
ivette/src/frama-c/plugins/wp/tip.tsx | 27 ++-
ivette/src/frama-c/server.ts | 30 ++--
ivette/src/frama-c/states.ts | 168 +++++++++++-------
ivette/src/renderer/Controller.tsx | 6 +-
src/plugins/api-generator/api_generator.ml | 8 +-
26 files changed, 290 insertions(+), 153 deletions(-)
diff --git a/ivette/src/dome/renderer/dome.tsx b/ivette/src/dome/renderer/dome.tsx
index 28323a8814f..ffaaa36e3a5 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 e2463cc03b5..c2e6e7bb622 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 b570db21248..96db99d2d78 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 ec2d9b1815e..c69b5084da7 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 d7ffb5bcf31..8e936a7fb1e 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 e0be594c7af..e111b68e69d 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 04199344163..9a6e1bc5c5a 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 8bf260c2615..d4e700d3831 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 1b346467568..1cbea161542 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 5671107839a..a4450256bf6 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 7c5c50aff4e..9305025278b 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 7ba1bef3f85..e06725e6f2e 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 64ad2c81094..2e5a1eec5f8 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 2e8f6a15248..e5dfbd41bb7 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 5fedbe2ae87..92549423c3c 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 a3fe7357afd..958174eedac 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 c045e516ff9..151220bcedd 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 57a834a29eb..147176b824e 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 13cda42e7e9..da50ab37d51 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 75ea1082ec1..287f3c52870 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 3de7f9f55cb..cc3f0f786df 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 633427b419b..3fe0bd22009 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 b110462dc79..4fd36323ec4 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 63a83121bb9..ba94955be54 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 4986f81b54e..6a9cfe88408 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 829ffee06f4..394937e3ebf 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:"@ ]@]"
--
GitLab