diff --git a/ivette/src/dome/renderer/dialogs.tsx b/ivette/src/dome/renderer/dialogs.tsx
index 36556d52bfd7a033d07e2def97524516bdff2779..bbdda3f02693deb736dca5a2a21142fb060662a7 100644
--- a/ivette/src/dome/renderer/dialogs.tsx
+++ b/ivette/src/dome/renderer/dialogs.tsx
@@ -157,7 +157,7 @@ export interface FileFilter {
export interface FileDialogProps {
/** Prompt message. */
- message?: string;
+ title?: string;
/** Open button label (default is « Open »). */
label?: string;
/** Initially selected path. */
@@ -196,11 +196,11 @@ export interface OpenDirProps extends FileDialogProps {
export async function showOpenFile(
props: OpenFileProps,
): Promise<string | undefined> {
- const { message, label, path, hidden = false, filters } = props;
+ const { title, label, path, hidden = false, filters } = props;
return remote.dialog.showOpenDialog(
remote.getCurrentWindow(),
{
- message,
+ title,
buttonLabel: label,
defaultPath: path && defaultPath(path),
properties: (hidden ? ['openFile', 'showHiddenFiles'] : ['openFile']),
@@ -219,12 +219,12 @@ export async function showOpenFile(
export async function showOpenFiles(
props: OpenFileProps,
): Promise<string[] | undefined> {
- const { message, label, path, hidden, filters } = props;
+ const { title, label, path, hidden, filters } = props;
return remote.dialog.showOpenDialog(
remote.getCurrentWindow(),
{
- message,
+ title,
buttonLabel: label,
defaultPath: path && defaultPath(path),
properties: (
@@ -257,11 +257,11 @@ export async function showOpenFiles(
export async function showSaveFile(
props: SaveFileProps,
): Promise<string | undefined> {
- const { message, label, path, filters } = props;
+ const { title, label, path, filters } = props;
return remote.dialog.showSaveDialog(
remote.getCurrentWindow(),
{
- message,
+ title,
buttonLabel: label,
defaultPath: path,
filters,
@@ -282,7 +282,7 @@ type openDirProperty =
export async function showOpenDir(
props: OpenDirProps,
): Promise<string | undefined> {
- const { message, label, path, hidden } = props;
+ const { title, label, path, hidden } = props;
const properties: openDirProperty[] = ['openDirectory'];
if (hidden) properties.push('showHiddenFiles');
@@ -295,7 +295,7 @@ export async function showOpenDir(
return remote.dialog.showOpenDialog(
remote.getCurrentWindow(),
{
- message,
+ title,
buttonLabel: label,
defaultPath: path,
properties,
diff --git a/ivette/src/frama-c/api/generated/kernel/ast/index.ts b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
index 03afaed2e4db3b3f14b83ae484aea67859036425..fa299dac4c294998a38c3656a84797fefe1a8592 100644
--- a/ivette/src/frama-c/api/generated/kernel/ast/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
@@ -71,6 +71,11 @@ const compute_internal: Server.ExecRequest<null,null> = {
/** Ensures that AST is computed */
export const compute: Server.ExecRequest<null,null>= compute_internal;
+/** Emitted when the AST has been changed */
+export const changed: Server.Signal = {
+ name: 'kernel.ast.changed',
+};
+
/** Marker kind */
export enum markerKind {
/** Expression */
@@ -284,6 +289,15 @@ export const byLocation: Compare.Order<location> =
marker: byMarker,
});
+const getMainFunction_internal: Server.GetRequest<null,Json.key<'#fct'>> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.getMainFunction',
+ input: Json.jNull,
+ output: Json.jKey<'#fct'>('#fct'),
+};
+/** Get the current 'main' function. */
+export const getMainFunction: Server.GetRequest<null,Json.key<'#fct'>>= getMainFunction_internal;
+
const getFunctions_internal: Server.GetRequest<null,Json.key<'#fct'>[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFunctions',
diff --git a/ivette/src/frama-c/index.tsx b/ivette/src/frama-c/index.tsx
index 2efb1200a091375e42a788cdf61d8427b1f71219..c134dfaf7dcd12e5d833711f59198a0f66a5326e 100644
--- a/ivette/src/frama-c/index.tsx
+++ b/ivette/src/frama-c/index.tsx
@@ -37,6 +37,10 @@ import Properties from 'frama-c/kernel/Properties';
import 'frama-c/kernel/style.css';
+import * as Menu from 'frama-c/menu';
+
+Menu.init();
+
/* --------------------------------------------------------------------------*/
/* --- Frama-C Kernel Groups ---*/
/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 2f2d9bbae19f40609fe3f95f0526a67ca9ada098..76879dcfca9675d4aa1aeffa73711ae6ac734aac 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -201,14 +201,20 @@ export default function ASTview() {
return () => { buffer.off('change', setBullets); };
}, [buffer, setBullets]);
+ async function reload() {
+ printed.current = theFunction;
+ loadAST(buffer, theFunction, theMarker);
+ }
+
// Hook: async loading
React.useEffect(() => {
- if (printed.current !== theFunction) {
- printed.current = theFunction;
- loadAST(buffer, theFunction, theMarker);
- }
+ if (printed.current !== theFunction)
+ reload();
});
+ // Also reload the buffer when the AST is recomputed.
+ Server.onSignal(Ast.changed, reload);
+
React.useEffect(() => {
const decorator = (marker: string) => {
if (multipleSelections?.some((location) => location?.marker === marker))
diff --git a/ivette/src/frama-c/menu.ts b/ivette/src/frama-c/menu.ts
new file mode 100644
index 0000000000000000000000000000000000000000..bb9a411c8b8608852f228b25dacf02f33af8f835
--- /dev/null
+++ b/ivette/src/frama-c/menu.ts
@@ -0,0 +1,65 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+/* --------------------------------------------------------------------------*/
+/* --- Frama-C MENU ---*/
+/* --------------------------------------------------------------------------*/
+
+import * as Dome from 'dome';
+import * as Dialogs from 'dome/dialogs';
+import * as Server from 'frama-c/server';
+import * as Ast from 'frama-c/api/kernel/ast';
+import * as States from 'frama-c/states';
+
+const cFilter = {
+ name: 'C source files',
+ extensions: ['c', 'i', 'h'],
+};
+const allFilter = {
+ name: 'all',
+ extensions: ['*'],
+};
+
+async function setFiles(): Promise<void> {
+ const files = await Dialogs.showOpenFiles({
+ title: 'Select C source files',
+ filters: [cFilter, allFilter],
+ });
+ if (files) {
+ await Server.send(Ast.setFiles, files);
+ await Server.send(Ast.compute, { });
+ States.resetSelection();
+ }
+ return;
+}
+
+export function init() {
+ Dome.addMenuItem({
+ menu: 'File',
+ label: 'Set source files',
+ id: 'file_set',
+ onClick: setFiles,
+ type: 'normal',
+ });
+}
+
+/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 876761db7b47e3b4381140df8f8739838bd794b0..7900638fce9c60e9ef144f3f82a39985d6b2f962 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -772,4 +772,23 @@ export function useSelection(): [Selection, (a: SelectionActions) => void] {
return [current, (action) => setCurrent(reducer(current, action))];
}
+/** Resets the selected locations. */
+export async function resetSelection() {
+ GlobalSelection.setValue(emptySelection);
+ const main = await Server.send(Ast.getMainFunction, { });
+ const selection = {
+ ...emptySelection,
+ current: { fct: main },
+ };
+ // If the selection has already been modified, do not change it.
+ if (GlobalSelection.getValue() === emptySelection)
+ GlobalSelection.setValue(selection);
+}
+/* Select the main function when the current project changes and the selection
+ is still empty (which happens at the start of the GUI). */
+PROJECT.on(async () => {
+ if (GlobalSelection.getValue() === emptySelection)
+ resetSelection();
+});
+
// --------------------------------------------------------------------------
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 463499a6e5af2ab46a9cc9f20b3a192e16d49c6b..57794fc7dfb9c2332082940a136deeb9901f2316 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -37,6 +37,15 @@ let () = Request.register ~package
~descr:(Md.plain "Ensures that AST is computed")
~input:(module Junit) ~output:(module Junit) Ast.compute
+let changed_signal = Request.signal ~package ~name:"changed"
+ ~descr:(Md.plain "Emitted when the AST has been changed")
+
+let ast_update_hook f =
+ Ast.add_hook_on_update f;
+ Ast.apply_after_computed (fun _ -> f ())
+
+let () = ast_update_hook (fun _ -> Request.emit changed_signal)
+
(* -------------------------------------------------------------------------- *)
(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
@@ -349,6 +358,12 @@ end
(* --- Functions --- *)
(* -------------------------------------------------------------------------- *)
+let () = Request.register ~package
+ ~kind:`GET ~name:"getMainFunction"
+ ~descr:(Md.plain "Get the current 'main' function.")
+ ~input:(module Junit) ~output:(module Kf)
+ (fun () -> fst (Globals.entry_point ()))
+
let () = Request.register ~package
~kind:`GET ~name:"getFunctions"
~descr:(Md.plain "Collect all functions in the AST")
@@ -459,7 +474,7 @@ struct
~name:"functions"
~descr:(Md.plain "AST Functions")
~iter
- ~add_reload_hook:Ast.add_hook_on_update ;
+ ~add_reload_hook:ast_update_hook
end
end