From c71f76b1a5349013f4c701a1417de0e8f898f2c8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 27 Jul 2023 14:57:04 +0200
Subject: [PATCH] [ivette/wp] Component skeleton
---
ivette/src/frama-c/plugins/wp/index.tsx | 45 ++++++++++++++++++++++++
ivette/src/frama-c/plugins/wp/pkg.json | 3 ++
ivette/src/frama-c/plugins/wp/style.css | 0
ivette/src/frama-c/plugins/wp/vcs.tsx | 46 +++++++++++++++++++++++++
4 files changed, 94 insertions(+)
create mode 100644 ivette/src/frama-c/plugins/wp/index.tsx
create mode 100644 ivette/src/frama-c/plugins/wp/pkg.json
create mode 100644 ivette/src/frama-c/plugins/wp/style.css
create mode 100644 ivette/src/frama-c/plugins/wp/vcs.tsx
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
new file mode 100644
index 00000000000..4369acea587
--- /dev/null
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -0,0 +1,45 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/* ************************************************************************ */
+
+// --------------------------------------------------------------------------
+// --- Eva Values
+// --------------------------------------------------------------------------
+
+import * as Ivette from 'ivette';
+import './vcs';
+import './style.css';
+
+// --------------------------------------------------------------------------
+// --- Export Component
+// --------------------------------------------------------------------------
+
+Ivette.registerView({
+ id: 'wp.main',
+ rank: 5,
+ label: 'WP View',
+ layout: [
+ ['frama-c.astview', 'frama-c.astinfo'],
+ 'frama-c.plugins.wp.vcs',
+ ],
+});
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/wp/pkg.json b/ivette/src/frama-c/plugins/wp/pkg.json
new file mode 100644
index 00000000000..356002bee1e
--- /dev/null
+++ b/ivette/src/frama-c/plugins/wp/pkg.json
@@ -0,0 +1,3 @@
+{
+ "name": "Frama-C/WP"
+}
diff --git a/ivette/src/frama-c/plugins/wp/style.css b/ivette/src/frama-c/plugins/wp/style.css
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/ivette/src/frama-c/plugins/wp/vcs.tsx b/ivette/src/frama-c/plugins/wp/vcs.tsx
new file mode 100644
index 00000000000..96709a56189
--- /dev/null
+++ b/ivette/src/frama-c/plugins/wp/vcs.tsx
@@ -0,0 +1,46 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/* ************************************************************************ */
+
+import React from 'react';
+import { Table, Column } 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';
+
+function WPGoals(): JSX.Element {
+ const model = States.useSyncArrayModel(WP.goals);
+ return (
+ <Table model={model} settings='wp.goals'>
+ <Column id='name' label='Names' />
+ </Table>
+ );
+}
+
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.wp.vcs',
+ group: 'frama-c.plugins',
+ rank: 10,
+ label: 'WP Goals',
+ title: 'WP Generated Verification Conditions',
+ children: <WPGoals />,
+});
--
GitLab