From 64fd126fcc4097194d9cf71b47a55d7615f6bd0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 12 Sep 2023 19:50:35 +0200
Subject: [PATCH] [wp/ivette] goal scope
---
ivette/src/frama-c/plugins/wp/goals.tsx | 20 ++++++++++++++++++--
1 file changed, 18 insertions(+), 2 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index d2ef458f75c..71d7af84859 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -27,6 +27,17 @@ import { Table, Column } from 'dome/table/views';
import * as States from 'frama-c/states';
import * as WP from 'frama-c/plugins/wp/api';
+/* -------------------------------------------------------------------------- */
+/* --- Scope Column --- */
+/* -------------------------------------------------------------------------- */
+
+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 '';
+}
+
/* -------------------------------------------------------------------------- */
/* --- Status Column --- */
/* -------------------------------------------------------------------------- */
@@ -119,8 +130,13 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
onSelection={onWpoSelection}
selection={wpoSelection}
>
- <Column id='name' label='Property' width={200} />
- <Column id='status' label='Status' fill={true}
+ <Column id='scope' label='Scope'
+ width={150}
+ getter={getScope} />
+ <Column id='name' label='Property'
+ width={150} />
+ <Column id='status' label='Status'
+ fill={true}
getter={getStatus} render={renderStatus} />
</Table>
);
--
GitLab