From 99fc3dd38df90d210fd3cf016d08af66df591334 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 30 Nov 2023 16:15:52 +0100
Subject: [PATCH] [ivette/wp] goal & list view
---
ivette/src/frama-c/plugins/wp/goals.tsx | 37 +++++++++------
ivette/src/frama-c/plugins/wp/index.tsx | 60 +++++++++++++++----------
ivette/src/frama-c/states.ts | 2 +
3 files changed, 62 insertions(+), 37 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 87d94e61690..de0453e1c9c 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -96,19 +96,27 @@ function filterGoal(
export interface GoalTableProps {
scope: Ast.decl | undefined;
failed: boolean;
- onFilter: (goals: number, total: number) => void;
+ display: boolean;
+ current: WP.goal;
+ setCurrent: (goal: WP.goal) => void;
+ setGoals: (goals: number) => void;
+ setTotal: (total: number) => void;
}
export function GoalTable(props: GoalTableProps): JSX.Element {
- const { scope, failed, onFilter } = props;
- const model = States.useSyncArrayModel(WP.goals);
- const [wpoSelection, setWpoSelection] = React.useState(WP.goalDefault);
-
- const onWpoSelection = React.useCallback(
+ const {
+ display, scope, failed,
+ current, setCurrent,
+ setGoals, setTotal,
+ } = props;
+ const { model } = States.useSyncArrayProxy(WP.goals);
+ const goals = model.getRowCount();
+ const total = model.getTotalRowCount();
+ const onSelection = React.useCallback(
({ wpo, property }: WP.goalsData) => {
States.setSelected(property);
- setWpoSelection(wpo);
- }, []);
+ setCurrent(wpo);
+ }, [setCurrent]);
React.useEffect(() => {
if (failed || !!scope) {
@@ -116,17 +124,18 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
} else {
model.setFilter();
}
- const goals = model.getRowCount();
- const total = model.getTotalRowCount();
- onFilter(goals, total);
- }, [model, scope, failed, onFilter]);
+ }, [model, scope, failed]);
+
+ React.useEffect(() => setGoals(goals), [goals, setGoals]);
+ React.useEffect(() => setTotal(total), [total, setTotal]);
return (
<Table
model={model}
+ display={display}
settings='wp.goals'
- onSelection={onWpoSelection}
- selection={wpoSelection}
+ selection={current}
+ onSelection={onSelection}
>
<Column id='scope' label='Scope'
width={150}
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index bc8223ad414..943e2471d1b 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -41,32 +41,46 @@ import './style.css';
/* -------------------------------------------------------------------------- */
function WPGoals(): JSX.Element {
- const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped');
- const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed');
+ const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped',false);
+ const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed',true);
+ const [list, flipListView] = Dome.useFlipSettings('frama-c.wp.goals.list',true);
+ const [current, setCurrent] = React.useState(WP.goalDefault);
const scope = States.useCurrentScope();
const [goals, setGoals] = React.useState(0);
const [total, setTotal] = React.useState(0);
- const onFilter = React.useCallback((goals, total) => {
- setGoals(goals);
- setTotal(total);
- }, [setGoals, setTotal]);
- const current = scoped ? scope : undefined;
- return (
- <>
- <Ivette.TitleBar>
- <Label display={goals < total}>
- {goals} / {total}
- </Label>
- <Inset />
- <IconButton icon='COMPONENT' title='Current Scope Only'
- enabled={!!current}
- selected={scoped} onClick={flipScoped} />
- <IconButton icon='CIRC.QUESTION' title='Unresolved Goals Only'
- selected={failed} onClick={flipFailed} />
- </Ivette.TitleBar>
- <GoalTable scope={scope} failed={failed} onFilter={onFilter} />
- </>
- );
+ const hasGoals = total > 0;
+ return (
+ <>
+ <Ivette.TitleBar>
+ <Label display={goals < total}>
+ {goals} / {total}
+ </Label>
+ <Inset />
+ <IconButton icon='CURSOR' title='Current Scope Only'
+ enabled={hasGoals}
+ selected={scoped}
+ onClick={flipScoped} />
+ <IconButton icon='CIRC.QUESTION' title='Unresolved Goals Only'
+ enabled={hasGoals}
+ selected={failed}
+ onClick={flipFailed} />
+ <IconButton icon='ITEMS.LIST'
+ title='Goals List / Current Goal Details'
+ enabled={hasGoals}
+ selected={list}
+ onClick={flipListView} />
+ </Ivette.TitleBar>
+ <GoalTable
+ display={list}
+ scope={scope}
+ failed={failed}
+ current={current}
+ setCurrent={setCurrent}
+ setGoals={setGoals}
+ setTotal={setTotal}
+ />
+ </>
+ );
}
Ivette.registerComponent({
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 7e1ee641c1d..abb59114db2 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -409,6 +409,7 @@ export function reloadArray<K, A>(arr: Array<K, A>): void {
/** Access to Synchronized Array elements. */
export interface ArrayProxy<K, A> {
+ model: CompactModel<K,A>;
length: number;
getData(elt: K | undefined): (A | undefined);
forEach(fn: (row: A, elt: K) => void): void;
@@ -429,6 +430,7 @@ function arrayProxy<K, A>(
_stamp: number,
): ArrayProxy<K, A> {
return {
+ model,
length: model.length(),
getData: (elt) => elt ? model.getData(elt) : undefined,
forEach: (fn) => model.forEach((r) => fn(r, model.getkey(r))),
--
GitLab