From deb3a7818f3f8a0b5bd64c624fb7a4904a2f93e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 5 Feb 2024 17:21:42 +0100
Subject: [PATCH] [tip] fix scope selection
---
ivette/src/frama-c/plugins/wp/goals.tsx | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 126a125bc07..167f55efeff 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -62,7 +62,7 @@ function getScope(g : WP.goalsData): string {
if (g.bhv && g.fct) return `${g.fct} — {g.bhv}}`;
if (g.fct) return g.fct;
if (g.thy) return g.thy;
- return '';
+ return 'Global';
}
/* -------------------------------------------------------------------------- */
@@ -168,12 +168,12 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
);
React.useEffect(() => {
- if (failed || !!scope) {
+ if (failed || scoped) {
model.setFilter(filterGoal(failed, scope));
} else {
model.setFilter();
}
- }, [model, scope, failed]);
+ }, [model, failed, scoped, scope]);
React.useEffect(() => setGoals(goals), [goals, setGoals]);
React.useEffect(() => setTotal(total), [total, setTotal]);
--
GitLab