From 43eeab58e58b66e8c8797bd9b147d5b67d2a6422 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 8 Aug 2023 08:00:22 +0200
Subject: [PATCH] [ivette/wp] first basic GUI
---
ivette/src/frama-c/plugins/wp/api/index.ts | 30 +++++++--------
.../frama-c/plugins/wp/{vcs.tsx => goals.tsx} | 38 +++++++++++++++++--
ivette/src/frama-c/plugins/wp/index.tsx | 4 +-
src/plugins/wp/wpApi.ml | 2 +-
4 files changed, 52 insertions(+), 22 deletions(-)
rename ivette/src/frama-c/plugins/wp/{vcs.tsx => goals.tsx} (66%)
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index b08c22d7609..8de39b88f57 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -152,7 +152,7 @@ export const getAvailableProvers: Server.GetRequest<null,prover[]>= getAvailable
/** Data for array rows [`goals`](#goals) */
export interface goalsData {
/** Entry identifier. */
- wpo: Json.key<'#wpo'>;
+ wpo: goal;
/** Property Marker */
property: marker;
/** Informal name */
@@ -178,7 +178,7 @@ export interface goalsData {
/** Decoder for `goalsData` */
export const jGoalsData: Json.Decoder<goalsData> =
Json.jObject({
- wpo: Json.jKey<'#wpo'>('#wpo'),
+ wpo: jGoal,
property: jMarker,
name: Json.jString,
fct: Json.jOption(jFct),
@@ -194,10 +194,10 @@ export const jGoalsData: Json.Decoder<goalsData> =
/** Natural order for `goalsData` */
export const byGoalsData: Compare.Order<goalsData> =
Compare.byFields
- <{ wpo: Json.key<'#wpo'>, property: marker, name: string, fct?: fct,
- bhv?: string, thy?: string, smoke: boolean, passed: boolean,
- stats: stats, script?: string, saved: boolean }>({
- wpo: Compare.string,
+ <{ wpo: goal, property: marker, name: string, fct?: fct, bhv?: string,
+ thy?: string, smoke: boolean, passed: boolean, stats: stats,
+ script?: string, saved: boolean }>({
+ wpo: byGoal,
property: byMarker,
name: Compare.string,
fct: Compare.defined(byFct),
@@ -227,15 +227,14 @@ export const reloadGoals: Server.GetRequest<null,null>= reloadGoals_internal;
const fetchGoals_internal: Server.GetRequest<
number,
- { reload: boolean, removed: Json.key<'#wpo'>[], updated: goalsData[],
- pending: number }
+ { reload: boolean, removed: goal[], updated: goalsData[], pending: number }
> = {
kind: Server.RqKind.GET,
name: 'plugins.wp.fetchGoals',
input: Json.jNumber,
output: Json.jObject({
reload: Json.jBoolean,
- removed: Json.jArray(Json.jKey<'#wpo'>('#wpo')),
+ removed: Json.jArray(jGoal),
updated: Json.jArray(jGoalsData),
pending: Json.jNumber,
}),
@@ -244,11 +243,10 @@ const fetchGoals_internal: Server.GetRequest<
/** Data fetcher for array [`goals`](#goals) */
export const fetchGoals: Server.GetRequest<
number,
- { reload: boolean, removed: Json.key<'#wpo'>[], updated: goalsData[],
- pending: number }
+ { reload: boolean, removed: goal[], updated: goalsData[], pending: number }
>= fetchGoals_internal;
-const goals_internal: State.Array<Json.key<'#wpo'>,goalsData> = {
+const goals_internal: State.Array<goal,goalsData> = {
name: 'plugins.wp.goals',
getkey: ((d:goalsData) => d.wpo),
signal: signalGoals,
@@ -257,13 +255,13 @@ const goals_internal: State.Array<Json.key<'#wpo'>,goalsData> = {
order: byGoalsData,
};
/** Generated Goals */
-export const goals: State.Array<Json.key<'#wpo'>,goalsData> = goals_internal;
+export const goals: State.Array<goal,goalsData> = goals_internal;
/** Default value for `goalsData` */
export const goalsDataDefault: goalsData =
- { wpo: Json.jKey<'#wpo'>('#wpo')(''), property: markerDefault, name: '',
- fct: undefined, bhv: undefined, thy: undefined, smoke: false,
- passed: false, stats: statsDefault, script: undefined, saved: false };
+ { wpo: goalDefault, property: markerDefault, name: '', fct: undefined,
+ bhv: undefined, thy: undefined, smoke: false, passed: false,
+ stats: statsDefault, script: undefined, saved: false };
/** Proof Server Activity */
export const serverActivity: Server.Signal = {
diff --git a/ivette/src/frama-c/plugins/wp/vcs.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
similarity index 66%
rename from ivette/src/frama-c/plugins/wp/vcs.tsx
rename to ivette/src/frama-c/plugins/wp/goals.tsx
index 96709a56189..e0956858d83 100644
--- a/ivette/src/frama-c/plugins/wp/vcs.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -21,23 +21,55 @@
/* ************************************************************************ */
import React from 'react';
-import { Table, Column } from 'dome/table/views';
+import { Icon } from 'dome/controls/icons';
+import { Table, Column, Renderer } from 'dome/table/views';
import * as Ivette from 'ivette';
import * as States from 'frama-c/states';
import * as WP from 'frama-c/plugins/wp/api';
+const renderPassed: Renderer<boolean> =
+ (passed: boolean): JSX.Element =>
+ (<Icon
+ id={passed ? 'CIRC.CHECK' : 'CIRC.QUESTION'}
+ fill={passed ? `var(--positive-button-color)` : `var(--negative-button-color)`}
+ />);
+
function WPGoals(): JSX.Element {
const model = States.useSyncArrayModel(WP.goals);
+
+ // TODO: from AST selection, find WPO
+ const [_astSelection, updateAstSelection] = States.useSelection();
+ const [wpoSelection, setWpoSelection] = React.useState(WP.goalDefault);
+
+ const onWpoSelection = React.useCallback(
+ ({ wpo, property: marker, fct }: WP.goalsData) => {
+ const location = { fct, marker };
+ updateAstSelection({ location });
+ setWpoSelection(wpo);
+ }, [updateAstSelection],
+ );
+
return (
- <Table model={model} settings='wp.goals'>
+ <Table
+ model={model}
+ settings='wp.goals'
+ onSelection={onWpoSelection}
+ selection={wpoSelection}
+ >
+ <Column id='fct' label='Function' />
<Column id='name' label='Names' />
+ <Column
+ id='passed'
+ label='Success'
+ render={renderPassed}
+ />
</Table>
);
}
Ivette.registerComponent({
- id: 'frama-c.plugins.wp.vcs',
+ id: 'frama-c.plugins.wp.goals',
group: 'frama-c.plugins',
rank: 10,
label: 'WP Goals',
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 4369acea587..aa17e7478a6 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -25,7 +25,7 @@
// --------------------------------------------------------------------------
import * as Ivette from 'ivette';
-import './vcs';
+import './goals';
import './style.css';
// --------------------------------------------------------------------------
@@ -38,7 +38,7 @@ Ivette.registerView({
label: 'WP View',
layout: [
['frama-c.astview', 'frama-c.astinfo'],
- 'frama-c.plugins.wp.vcs',
+ 'frama-c.plugins.wp.goals',
],
});
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 3fc1548fc16..61da7c4d7db 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -214,7 +214,7 @@ let _ = S.register_array ~package ~name:"goals"
~descr:(Md.plain "Generated Goals")
~key:(fun g -> g.Wpo.po_gid)
~keyName:"wpo"
- ~keyType:(Jkey "wpo")
+ ~keyType:Goal.jtype
~iter:Wpo.iter_on_goals
~add_update_hook:Wpo.add_modified_hook
~add_remove_hook:Wpo.add_removed_hook
--
GitLab