Merge branch 'ivette/sidebar/title' into 'master'

[Ivette] added about and credits in menu Help

See merge request frama-c/frama-c!4899

ivette/src/dome/@type/global.d.ts

@@ -26,6 +26,11 @@ declare module '*.md?raw' {
   export default content;
 }
 
+declare module '*.png' {
+  const value: string;
+  export default value;
+}
+
 declare module 'react-flame-graph';
 declare module 'react-pivottable/PivotTableUI';
 declare module 'three/examples/jsm/renderers/CSS2DRenderer';

ivette/src/dome/main/menubar.ts

@@ -273,18 +273,22 @@ const windowMenuItemsMacos: MenuSpec = windowMenuItemsLinux.concat([
 // --- Help Menu Items
 // --------------------------------------------------------------------------
 
+const helpMenuItemsCustom: MenuSpec = [];
+const helpMenuItems: MenuSpec = [];
+
 let learnMoreLink = '';
 ipcMain.handle('dome.ipc.updateLearnMore', (_, link) => {
-  if (typeof link === 'string') learnMoreLink = link;
+  if (typeof link === 'string') {
+    learnMoreLink = link;
+    helpMenuItems.push(
+      {
+        label: 'Learn More',
+        click() { shell.openExternal(learnMoreLink); },
+      },
+    );
+  }
 });
 
-const helpMenuItems: MenuSpec = [
-  {
-    label: 'Learn More',
-    click() { shell.openExternal(learnMoreLink); },
-  },
-];
-
 // --------------------------------------------------------------------------
 // --- Update MenuBar (async)
 // --------------------------------------------------------------------------
@@ -319,6 +323,7 @@ function findMenu(label: string): MenuSpec | undefined {
     case 'File': return fileMenuItemsCustom;
     case 'Edit': return editMenuItemsCustom;
     case 'View': return viewMenuItemsCustom;
+    case 'Help': return helpMenuItemsCustom;
     default: {
       const cm = customMenus.find((m) => m.label === label);
       return cm && cm.submenu;
@@ -445,7 +450,7 @@ function template(): CustomMenu[] {
           {
             label: 'Help',
             role: 'help',
-            submenu: helpMenuItems,
+            submenu: concatSep(helpMenuItems, helpMenuItemsCustom),
           },
         ],
       );
@@ -470,7 +475,9 @@ function template(): CustomMenu[] {
         customMenus,
         [
           { label: 'Window', submenu: windowMenuItemsLinux },
-          { label: 'Help', submenu: helpMenuItems },
+          {
+            label: 'Help',
+            submenu: concatSep(helpMenuItems, helpMenuItemsCustom) },
         ],
       );
   }
@@ -504,6 +511,7 @@ function reset(): void {
   fileMenuItemsCustom.length = 0;
   editMenuItemsCustom.length = 0;
   viewMenuItemsCustom.length = 0;
+  helpMenuItemsCustom.length = 0;
   customMenus.length = 0;
   customItems.clear();
   install();

ivette/src/dome/renderer/frame/style.css

@@ -103,6 +103,7 @@
       z-index: 10;
       padding: 5px;
       border-bottom: solid 1px var(--border-discrete);
+      background-color: var(--background-sidebar);
 
       .dome-xBoxes-hbox {
         max-width: 100%;

ivette/src/dome/renderer/layout/style.css

@@ -56,6 +56,10 @@
     overflow: auto ;
 }
 
+.dome-container {
+    z-index: 0;
+}
+
 .dome-container > .dome-xBoxes-fill
 {
     width:  100% ;

ivette/src/dome/renderer/style.css

@@ -278,7 +278,6 @@ input[type="checkbox"]:checked {
 }
 
 .dome-xModal-overlay {
-  z-index: 1000;
   position: fixed;
   top: 0;
   left: 0;

ivette/src/frama-c/help.tsx

+/* ************************************************************************ */
+/*                                                                          */
+/*   This file is part of Frama-C.                                          */
+/*                                                                          */
+/*   Copyright (C) 2007-2025                                                */
+/*     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 { Modal } from 'dome/dialogs';
+import { Hbox } from 'dome/layout/boxes';
+
+import { shell } from 'electron';
+import { Button } from 'dome/controls/buttons';
+import * as Server from 'frama-c/server';
+import * as Dialogs from 'dome/dialogs';
+import { getConfig } from 'frama-c/kernel/api/services';
+
+import './style.css';
+import framacImage from './frama-c.png';
+
+/* -------------------------------------------------------------------------- */
+/* --- Frama-C infos                                                      --- */
+/* -------------------------------------------------------------------------- */
+
+const synopsis =
+'Frama-C is a platform dedicated to the analysis of source code written in C.';
+const description =
+'Frama-C gathers several analysis techniques in a single collaborative \
+framework, based on analyzers, called "plug-ins", that can build upon the \
+results computed by other analyzers of the platform.\n\
+Thanks to this approach, Frama-C provides sophisticated tools, including:\n\
+- Eva, an analyzer based on abstract interpretation;\n\
+- Wp, a program proof framework based on weakest precondition calculus;\n\
+- E-ACSL, a runtime verification tool;\n\
+- Aoraï, a tool for the verification of automata-based properties;\n\
+- several tools for code base exploration and dependency analysis: \
+plug-ins From, Impact, Metrics, Occurrence, Scope, etc.';
+
+const authors = [
+    'Michele Alberti',
+    'Thibaud Antignac',
+    'Gergö Barany',
+    'Patrick Baudin',
+    'Nicolas Bellec',
+    'Thibaut Benjamin',
+    'Allan Blanchard',
+    'Lionel Blatter',
+    'François Bobot',
+    'Richard Bonichon',
+    'Vincent Botbol',
+    'Quentin Bouillaguet',
+    'David Bühler',
+    'Zakaria Chihani',
+    'Loïc Correnson',
+    'Julien Crétin',
+    'Pascal Cuoq',
+    'Zaynah Dargaye',
+    'Basile Desloges',
+    'Jean-Christophe Filliâtre',
+    'Philippe Herrmann',
+    'Maxime Jacquemin',
+    'Florent Kirchner',
+    'Alexander Kogtenkov',
+    'Remi Lazarini',
+    'Tristan Le Gall',
+    'Kilyan Le Gallic',
+    'Jean-Christophe Léchenet',
+    'Matthieu Lemerre',
+    'Dara Ly',
+    'David Maison',
+    'Claude Marché',
+    'André Maroneze',
+    'Thibault Martin',
+    'Fonenantsoa Maurica',
+    'Melody Méaulle',
+    'Benjamin Monate',
+    'Yannick Moy',
+    'Pierre Nigron',
+    'Anne Pacalet',
+    'Valentin Perrelle',
+    'Guillaume Petiot',
+    'Dario Pinto',
+    'Virgile Prevosto',
+    'Armand Puccetti',
+    'Félix Ridoux',
+    'Virgile Robles',
+    'Jan Rochel',
+    'Muriel Roger',
+    'Cécile Ruet-Cros',
+    'Julien Signoles',
+    'Nicolas Stouls',
+    'Kostyantyn Vorobyov',
+    'Boris Yakobowski'
+  ];
+const homepage = 'https://frama-c.com/';
+const doc = 'https://frama-c.com/html/documentation.html';
+const bugReports = 'https://git.frama-c.com/pub/frama-c/issues';
+const devRepo = 'https://git.frama-c.com/pub/frama-c/';
+
+const license =
+'Most sources are LGPLv2.1,\n with some isolated exceptions for \
+external libraries modified for Frama-C.\n\
+See the particular header of each source file for details.';
+const copyright =
+'© CEA and INRIA for the Frama-C kernel\n\
+© CEA for the GUI and plug-ins';
+
+/* -------------------------------------------------------------------------- */
+/* --- Frama-C About                                                      --- */
+/* -------------------------------------------------------------------------- */
+
+function FramaCLogo(): JSX.Element {
+  return (
+    <Hbox>
+      <img src={framacImage} alt="Frama-C: Software analyzers"/>
+    </Hbox>
+  );
+}
+
+interface AboutProps {
+  version: string;
+}
+
+function AboutModal(props: AboutProps): JSX.Element {
+  return (
+    <Modal className='modal-framac-infos' label='About Frama-C'>
+      <>
+        <FramaCLogo />
+        <Hbox className='modal-framac-about'>
+          <pre>version: {props.version}</pre>
+          <pre>{synopsis}</pre>
+          <Hbox>
+            <Button
+              onClick={() => shell.openExternal(homepage)}
+              label='Website' />
+            <Button
+              onClick={() => shell.openExternal(doc)}
+              label='Documentation' />
+            <Button
+              onClick={() => shell.openExternal(bugReports)}
+              label='Bug reports' />
+            <Button
+              onClick={() => shell.openExternal(devRepo)}
+              label='Git repository' />
+          </Hbox>
+          <pre className='framac-about-description'>{description}</pre>
+          <pre>{copyright}</pre>
+          <pre>{license}</pre>
+        </Hbox>
+      </>
+    </Modal>
+  );
+}
+
+export async function showAboutModal(): Promise<void> {
+  const config = await Server.send(getConfig, {});
+  const version = config.version_codename;
+  const modal = <AboutModal version = {version}/>;
+  Dialogs.showModal(modal);
+}
+
+function CreditsModal(): JSX.Element {
+  return (
+    <Modal className='modal-framac-infos' label='Credits'>
+      <>
+        <FramaCLogo />
+        <Hbox>
+          <pre style={{ fontSize: '1.2em', textAlign: "center" }}
+          >Created by:</pre>
+        </Hbox>
+        <div className='modal-framac-credits'>
+          {authors.map((author, i) => <div key={i} >{author}</div>)}
+        </div>
+      </>
+    </Modal>
+  );
+}
+
+export function showCreditsModal(): void {
+  const modal = <CreditsModal/>;
+  Dialogs.showModal(modal);
+}

ivette/src/frama-c/menu.ts

@@ -24,7 +24,6 @@
 /* --- Frama-C MENU                                                       ---*/
 /* --------------------------------------------------------------------------*/
 
-import { ipcRenderer } from 'electron';
 import * as Dome from 'dome';
 import * as Dialogs from 'dome/dialogs';
 import * as Display from 'ivette/display';
@@ -32,6 +31,7 @@ import * as Server from 'frama-c/server';
 import * as Services from 'frama-c/kernel/api/services';
 import * as Ast from 'frama-c/kernel/api/ast';
 import * as States from 'frama-c/states';
+import * as HelpMenu from './help';
 
 const cFilter = {
   name: 'C source files',
@@ -114,7 +114,6 @@ async function saveSession(): Promise<void> {
 }
 
 export function init(): void {
-  ipcRenderer.invoke('dome.ipc.updateLearnMore', 'https://frama-c.com/');
   Dome.addMenuItem({
     menu: 'File',
     label: 'Set source files…',
@@ -155,6 +154,20 @@ export function init(): void {
     onClick: saveSession,
     kind: 'normal',
   });
+  Dome.addMenuItem({
+    menu: 'Help',
+    label: 'About',
+    id: 'help_about',
+    onClick: HelpMenu.showAboutModal,
+    kind: 'normal',
+  });
+  Dome.addMenuItem({
+    menu: 'Help',
+    label: 'Credits',
+    id: 'help_credits',
+    onClick: HelpMenu.showCreditsModal,
+    kind: 'normal',
+  });
 }
 
 /* --------------------------------------------------------------------------*/

ivette/src/frama-c/style.css

+/* -------------------------------------------------------------------------- */
+/* --- About Frama-c - content                                            --- */
+/* -------------------------------------------------------------------------- */
+
+.modal-framac-infos {
+
+  .dome-xModal-body {
+    flex-direction: column;
+    padding: 20px;
+    max-height: 100%;
+
+    .modal-framac-about {
+      max-height: 100%;
+      flex-direction: column;
+      overflow: auto;
+      text-align: center;
+
+      button:hover { cursor: pointer; }
+      pre {
+        user-select: text;
+
+        &.framac-about-description {
+          text-align: justify;
+        }
+      }
+    }
+
+    .modal-framac-credits {
+      text-align: center;
+      font-size: 1.1em;
+      max-width: 100%;
+      width: 550px;
+      column-width: 170px;
+      max-height: 550px;
+      column-count: auto;
+      column-gap: 20px;
+      overflow: auto;
+
+      >div {
+        padding: 2px 0;
+        white-space: nowrap;
+        user-select: text;
+      }
+    }
+
+    .dome-xBoxes-hbox {
+      width: 100%;
+      flex-wrap: wrap;
+      justify-content: center;
+      margin-bottom: 20px;
+
+      img {
+        width: 100%;
+        max-width: 400px;
+      }
+
+      pre {
+        width: 100%;
+        margin-bottom: 10px;
+        white-space: pre-wrap;
+      }
+    }
+  }
+}

src/plugins/server/kernel_main.ml

@@ -101,6 +101,10 @@ let () =
   let result_list name descr =
     Request.result signature ~name ~descr:(Md.plain descr) (module Jlist (Jstring)) in
   let set_version = result "version" "Frama-C version" in
+  let set_codename = result "codename" "Frama-C codename" in
+  let set_version_codename =
+    result "version_codename" "Frama-C version and codename"
+  in
   let set_datadir = result_list "datadir" "Shared directory (FRAMAC_SHARE)" in
   let set_pluginpath = result_list "pluginpath" "Plugin directories (FRAMAC_PLUGIN)" in
   Request.register_sig
@@ -109,6 +113,8 @@ let () =
     signature
     begin fun rq () ->
       set_version rq System_config.Version.id ;
+      set_codename rq System_config.Version.codename ;
+      set_version_codename rq System_config.Version.id_and_codename ;
       set_datadir rq (Filepath.Normalized.to_string_list System_config.Share.dirs);
       set_pluginpath rq
         (Filepath.Normalized.to_string_list System_config.Plugins.dirs) ;