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 0000000000000000000000000000000000000000..4369acea587cf9282c4b45b7581fba653f46c335 --- /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 0000000000000000000000000000000000000000..356002bee1e1f0c0b6cdb295795549f7b03852e7 --- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..96709a56189573c8fe412213867960c85e222a9e --- /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 />, +});