From 6916be9478c0b3e85998c2395230c17a71097a11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 8 Jun 2022 09:40:42 +0200
Subject: [PATCH] [ivette] Eva: new component prints internal domain states for
the selected marker.
The user can select the Eva domain whose state are printed.
---
.../src/frama-c/plugins/eva/DomainStates.tsx | 110 ++++++++++++++++++
ivette/src/frama-c/plugins/eva/index.tsx | 1 +
ivette/src/frama-c/plugins/eva/style.css | 16 +++
3 files changed, 127 insertions(+)
create mode 100644 ivette/src/frama-c/plugins/eva/DomainStates.tsx
diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
new file mode 100644
index 00000000000..560f298f65b
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
@@ -0,0 +1,110 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2022 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+// React & Dome
+import React from 'react';
+import * as Ivette from 'ivette';
+import * as States from 'frama-c/states';
+import * as Eva from 'frama-c/plugins/eva/api/general';
+import * as Boxes from 'dome/layout/boxes';
+import { HSplit } from 'dome/layout/splitters';
+import { Text } from 'frama-c/richtext';
+import { Select } from 'dome/controls/buttons';
+import { Label } from 'dome/controls/labels';
+
+export function EvaStates(): JSX.Element {
+ const [selection] = States.useSelection();
+ const selectedLoc = selection?.current;
+ const marker = selectedLoc?.marker;
+ const states = States.useRequest(Eva.getStates, marker);
+ const [domains, setDomains] = React.useState<string[]>([]);
+ const [selected, setSelected] = React.useState<string>();
+ const [stateBefore, setStateBefore] = React.useState("");
+ const [stateAfter, setStateAfter] = React.useState("");
+
+ React.useEffect(() => {
+ if (states && states.length > 0) {
+ const names = states.map((d) => d[0]);
+ setDomains(names);
+ if (!selected || !names.includes(selected))
+ setSelected(names[0]);
+ const selectedDomain = states.find((d) => d[0] === selected);
+ if (selectedDomain) {
+ setStateBefore(selectedDomain[1]);
+ setStateAfter(selectedDomain[2]);
+ }
+ } else
+ setDomains([]);
+ }, [states, selected]);
+
+ if (domains.length === 0)
+ return (<></>);
+
+ function makeOption(name: string): React.ReactNode {
+ return <option value={name}>{name}</option>;
+ }
+ const list = React.Children.toArray(domains.map(makeOption));
+
+ return (
+ <>
+ <Boxes.Hbox className="domain-state-box">
+ <Label>Domain: </Label>
+ <Select
+ title="Select the analysis domain to be shown"
+ value={selected}
+ onChange={setSelected}
+ >
+ {list}
+ </Select>
+ </Boxes.Hbox>
+ <HSplit
+ settings="ivette.eva.domainStates.beforeAfterSplit"
+ >
+ <div className="domain-state-box">
+ State before the selected statement:
+ <Text className="domain-state" text={stateBefore} />
+ </div>
+ <div className="domain-state-box">
+ State after the selected statement:
+ <Text className="domain-state" text={stateAfter} />
+ </div>
+ </HSplit>
+ </>);
+}
+
+function EvaStatesComponent(): JSX.Element {
+ return (
+ <>
+ <Ivette.TitleBar />
+ <EvaStates />
+ </>
+ );
+}
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.domain_states',
+ group: 'frama-c.plugins',
+ rank: 10,
+ label: 'Eva States',
+ title: 'States of the Eva analysis',
+ children: <EvaStatesComponent />,
+});
diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 8aeb22bb817..36b6dc1d5ba 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -28,6 +28,7 @@ import * as Ivette from 'ivette';
import { } from 'frama-c/plugins/eva/valuetable';
import { } from './Summary';
import { } from './Coverage';
+import { } from './DomainStates';
import './style.css';
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index e4a17e65e23..35954f92d28 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -317,3 +317,19 @@ tr:first-of-type > .eva-table-callsite-box {
}
/* -------------------------------------------------------------------------- */
+/* --- Domains state print --- */
+/* -------------------------------------------------------------------------- */
+
+.domain-state-box {
+ margin: 6px;
+}
+
+.domain-state {
+ user-select: text;
+ overflow: auto;
+ padding: 6px;
+ margin-top: 6px;
+ background-color: var(--background-report);
+}
+
+/* -------------------------------------------------------------------------- */
--
GitLab