From f5cffce824788a8ffbd9e5ebe26fee5146759e41 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Jan 2024 11:01:35 +0100
Subject: [PATCH] [wp] error robustness
---
ivette/src/frama-c/plugins/wp/seq.tsx | 7 ++++++-
ivette/src/frama-c/plugins/wp/tac.tsx | 16 +++++++++++-----
ivette/src/frama-c/plugins/wp/tip.tsx | 4 +++-
ivette/src/frama-c/states.ts | 2 +-
4 files changed, 21 insertions(+), 8 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/seq.tsx b/ivette/src/frama-c/plugins/wp/seq.tsx
index c1aa8dec783..3c91c3a52fa 100644
--- a/ivette/src/frama-c/plugins/wp/seq.tsx
+++ b/ivette/src/frama-c/plugins/wp/seq.tsx
@@ -170,7 +170,12 @@ export function GoalView(props: GoalViewProps): JSX.Element {
offline: undefined,
onError: '',
}) ?? null;
- const { part, term } = States.useRequest(TIP.getSelection, node) ?? {};
+ const { part, term } =
+ States.useRequest(TIP.getSelection, node, {
+ pending: null,
+ offline: {},
+ onError: {},
+ }) ?? {};
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 294e0d69ea8..914b0eda75e 100644
--- a/ivette/src/frama-c/plugins/wp/tac.tsx
+++ b/ivette/src/frama-c/plugins/wp/tac.tsx
@@ -162,8 +162,9 @@ export interface ProverSelection {
export function Provers(props: ProverSelection): JSX.Element {
const { node, selected, setSelected } = props;
- const { results=[] } =
- States.useRequest(TIP.getNodeInfos, node, { pending: null }) ?? {};
+ const { results=[] } = States.useRequest(
+ TIP.getNodeInfos, node, { pending: null, onError: null }
+ ) ?? {};
const [ provers=[], setProvers ] = States.useSyncState(WP.provers);
const setItems = (prvs: string[]): void => setProvers(prvs.map(WP.jProver));
const children = [...provers].sort().map((prover) => {
@@ -230,7 +231,12 @@ function TacticItem(props: TacticItemProps): JSX.Element | null {
const ready = !locked && status === 'Applicable';
const isSelected = selected === tactic;
const onSelect = (): void => setSelected(tactic);
- const onPlay = (): void => { if (ready) applyTactic(tactic); };
+ const onPlay = (): void => {
+ if (ready) {
+ applyTactic(tactic);
+ setSelected(undefined);
+ }
+ };
const className = classes(
'dome-color-frame wp-tactical-item',
isSelected && 'selected',
@@ -375,7 +381,7 @@ 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 }
+ TIP.getResult, { node, prover }, { pending: null, onError: null }
) ?? WP.resultDefault;
const [process = 1, setProcess] = States.useSyncState(WP.process);
const [timeout = 1, setTimeout] = States.useSyncState(WP.timeout);
@@ -524,7 +530,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);
+ States.useRequest(TAC.configureTactics, node, { onError: null });
const { status, label, title, params } = tactical;
const isReady = !locked && status==='Applicable';
const display = !!tactic && (locked || status !== 'NotApplicable');
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index 1c5fb75d6f9..8db9785cf32 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -130,7 +130,9 @@ function Node(props: NodeProps): JSX.Element
const {
title=debug, child='Script', header=debug,
proved=false, pending=0, size=0
- } = States.useRequest( TIP.getNodeInfos, node, { pending: null } ) ?? {};
+ } = States.useRequest(
+ TIP.getNodeInfos, node, { pending: null, onError: null }
+ ) ?? {};
const elt = cellRef.current;
React.useEffect(() => {
if (current && elt) elt.scrollIntoView();
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index b9eeda83851..13644db3a40 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -92,7 +92,7 @@ export function useRequest<Kd extends Server.RqKind, In, Out>(
const r = await Server.send(rq, params);
updateResponse(r);
} catch (error) {
- if (options.onError !== undefined) {
+ if (options.onError === undefined) {
D.error(`Fail in useRequest '${rq.name}'. ${error}`);
}
updateResponse(options.onError);
--
GitLab