From 9f5da4959fdbab39eeaf994088ca60cb1ff2362e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 6 Jul 2023 14:59:39 +0200
Subject: [PATCH] [ivette] New file Studia.tsx for Studia related functions,
used by ASTview.
---
ivette/src/frama-c/kernel/ASTview.tsx | 54 +---------------
ivette/src/frama-c/plugins/studia/studia.ts | 70 +++++++++++++++++++++
2 files changed, 72 insertions(+), 52 deletions(-)
create mode 100644 ivette/src/frama-c/plugins/studia/studia.ts
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 35a124c9ea3..a053d494156 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -26,17 +26,15 @@ import Lodash from 'lodash';
import * as Dome from 'dome';
import * as Editor from 'dome/text/editor';
import * as Utils from 'dome/data/arrays';
-import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
-import { key } from 'dome/data/json';
import * as Settings from 'dome/data/settings';
import { IconButton } from 'dome/controls/buttons';
import { Filler, Inset } from 'dome/frame/toolbars';
+import * as Studia from 'frama-c/plugins/studia/studia';
import * as Ast from 'frama-c/kernel/api/ast';
import { text } from 'frama-c/kernel/api/data';
import * as Eva from 'frama-c/plugins/eva/api/general';
import * as Properties from 'frama-c/kernel/api/properties';
-import { getWritesLval, getReadsLval } from 'frama-c/plugins/studia/api/studia';
import { TitleBar } from 'ivette';
import * as Preferences from 'ivette/prefs';
@@ -486,46 +484,6 @@ function createPropertiesGutter(): Editor.Extension {
-// -----------------------------------------------------------------------------
-// Studia access
-// -----------------------------------------------------------------------------
-
-type access = 'Reads' | 'Writes';
-
-interface StudiaProps {
- marker: string,
- attrs: Ast.markerAttributesData,
- kind: access,
-}
-
-interface StudiaInfos {
- name: string,
- title: string,
- locations: { fct: key<'#fct'>, marker: Ast.marker }[],
- index: number,
-}
-
-async function studia(props: StudiaProps): Promise<StudiaInfos> {
- const { marker, attrs, kind } = props;
- const request = kind === 'Reads' ? getReadsLval : getWritesLval;
- const data = await Server.send(request, marker);
- const locations = data.direct.map(([f, m]) => ({ fct: f, marker: m }));
- const lval = attrs.name;
- if (locations.length > 0) {
- const name = `${kind} of ${lval}`;
- const acc = (kind === 'Reads') ? 'accessing' : 'modifying';
- const title =
- `List of statements ${acc} the memory location pointed by ${lval}.`;
- return { name, title, locations, index: 0 };
- }
- const name = `No ${kind.toLowerCase()} of ${lval}`;
- return { name, title: '', locations: [], index: 0 };
-}
-
-// -----------------------------------------------------------------------------
-
-
-
// -----------------------------------------------------------------------------
// Context menu
// -----------------------------------------------------------------------------
@@ -583,15 +541,7 @@ function createContextMenuHandler(): Editor.Extension {
items.push({ label, onClick });
});
}
- const enabled = attrs?.isLval;
- const onClick = (kind: access): void => {
- if (attrs && node.marker)
- studia({ marker: node.marker, attrs, kind }).then(update);
- };
- const reads = 'Studia: select reads';
- const writes = 'Studia: select writes';
- items.push({ label: reads, enabled, onClick: () => onClick('Reads') });
- items.push({ label: writes, enabled, onClick: () => onClick('Writes') });
+ Studia.buildMenu({ marker: node.marker, attrs, update, menu: items });
const copy = (): void => {
const text = view.state.sliceDoc(node.from, node.to);
if (text !== '') navigator.clipboard.writeText(text);
diff --git a/ivette/src/frama-c/plugins/studia/studia.ts b/ivette/src/frama-c/plugins/studia/studia.ts
new file mode 100644
index 00000000000..d84e1fb7e2a
--- /dev/null
+++ b/ivette/src/frama-c/plugins/studia/studia.ts
@@ -0,0 +1,70 @@
+/* ************************************************************************ */
+/* */
+/* 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 * as Dome from 'dome';
+import * as States from 'frama-c/states';
+import * as Server from 'frama-c/server';
+import * as Ast from 'frama-c/kernel/api/ast';
+import { getWritesLval, getReadsLval } from 'frama-c/plugins/studia/api/studia';
+
+type access = 'Reads' | 'Writes';
+
+async function compute(marker: Ast.marker, label: string, kind: access)
+ : Promise<States.MultipleSelect> {
+ const request = kind === 'Reads' ? getReadsLval : getWritesLval;
+ const data = await Server.send(request, marker);
+ const locations = data.direct.map(([f, m]) => ({ fct: f, marker: m }));
+ if (locations.length > 0) {
+ const name = `${kind} of ${label}`;
+ const acc = (kind === 'Reads') ? 'accessing' : 'modifying';
+ const title =
+ `List of statements ${acc} the memory location pointed by ${label}.`;
+ return { name, title, locations, index: 0 };
+ }
+ const name = `No ${kind.toLowerCase()} of ${label}`;
+ return { name, title: '', locations: [], index: 0 };
+}
+
+interface MenuProps {
+ /** The marker on which the menu is applied. */
+ marker: Ast.marker,
+ /** Attributes of the marker. */
+ attrs?: Ast.markerAttributesData,
+ /** Function to update the selection. */
+ update: (a: States.SelectionActions) => void,
+ /** Array to which studia menu entries are added. */
+ menu: Dome.PopupMenuItem[],
+}
+
+/** Builds the Studia entries in the contextual menu about a given marker. */
+export function buildMenu(props: MenuProps) : void {
+ const { update, marker, attrs, menu } = props;
+ const enabled = attrs?.isLval;
+ function onClick(kind: access) : void {
+ if (marker && attrs)
+ compute(marker, attrs.name, kind).then(update);
+ }
+ const reads = 'Studia: select reads';
+ const writes = 'Studia: select writes';
+ menu.push({ label: reads, enabled, onClick: () => onClick('Reads') });
+ menu.push({ label: writes, enabled, onClick: () => onClick('Writes') });
+}
--
GitLab