diff --git a/ivette/src/dome/renderer/controls/gallery.json b/ivette/src/dome/renderer/controls/gallery.json
index 0dd269297ccd8edd04b9e7075a272b0ad0b03bba..f2da558a323bb611f7579cf52b4d8973d767c5fc 100644
--- a/ivette/src/dome/renderer/controls/gallery.json
+++ b/ivette/src/dome/renderer/controls/gallery.json
@@ -185,6 +185,11 @@
"viewBox": "0 0 16 16",
"path": "M16 6.204l-5.528-0.803-2.472-5.009-2.472 5.009-5.528 0.803 4 3.899-0.944 5.505 4.944-2.599 4.944 2.599-0.944-5.505 4-3.899z"
},
+ "SPINNER": {
+ "section": "Signs",
+ "viewBox": "0 0 32 32",
+ "path": "M32 16c-0.040-2.089-0.493-4.172-1.331-6.077-0.834-1.906-2.046-3.633-3.533-5.060-1.486-1.428-3.248-2.557-5.156-3.302-1.906-0.748-3.956-1.105-5.981-1.061-2.025 0.040-4.042 0.48-5.885 1.292-1.845 0.809-3.517 1.983-4.898 3.424s-2.474 3.147-3.193 4.994c-0.722 1.846-1.067 3.829-1.023 5.79 0.040 1.961 0.468 3.911 1.254 5.694 0.784 1.784 1.921 3.401 3.316 4.736 1.394 1.336 3.046 2.391 4.832 3.085 1.785 0.697 3.701 1.028 5.598 0.985 1.897-0.040 3.78-0.455 5.502-1.216 1.723-0.759 3.285-1.859 4.574-3.208 1.29-1.348 2.308-2.945 2.977-4.67 0.407-1.046 0.684-2.137 0.829-3.244 0.039 0.002 0.078 0.004 0.118 0.004 1.105 0 2-0.895 2-2 0-0.056-0.003-0.112-0.007-0.167h0.007zM28.822 21.311c-0.733 1.663-1.796 3.169-3.099 4.412s-2.844 2.225-4.508 2.868c-1.663 0.646-3.447 0.952-5.215 0.909-1.769-0.041-3.519-0.429-5.119-1.14-1.602-0.708-3.053-1.734-4.25-2.991s-2.141-2.743-2.76-4.346c-0.621-1.603-0.913-3.319-0.871-5.024 0.041-1.705 0.417-3.388 1.102-4.928 0.683-1.541 1.672-2.937 2.883-4.088s2.642-2.058 4.184-2.652c1.542-0.596 3.192-0.875 4.832-0.833 1.641 0.041 3.257 0.404 4.736 1.064 1.48 0.658 2.82 1.609 3.926 2.774s1.975 2.54 2.543 4.021c0.57 1.481 0.837 3.064 0.794 4.641h0.007c-0.005 0.055-0.007 0.11-0.007 0.167 0 1.032 0.781 1.88 1.784 1.988-0.195 1.088-0.517 2.151-0.962 3.156z"
+ },
"TRASH": {
"section": "Desktop",
"title": "Trash",
diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx
index 819ee2b202dfe6d3f117795ddaf4d2815bce7d60..71b6a277da8e93d1f8d43ce467b592a7942d815c 100644
--- a/ivette/src/frama-c/kernel/Globals.tsx
+++ b/ivette/src/frama-c/kernel/Globals.tsx
@@ -211,7 +211,7 @@ type functionsData =
type FctKey = Json.key<'#functions'>;
-function computeFcts(
+export function computeFcts(
ker: States.ArrayProxy<FctKey, Ast.functionsData>,
eva: States.ArrayProxy<FctKey, Eva.functionsData>,
): functionsData[] {
diff --git a/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx b/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..6a4a7aaed321679e7681e158effaf7d673ac4529
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx
@@ -0,0 +1,179 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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 Forms from 'dome/layout/forms';
+
+export type KeyVal<A> = {[key: string]: A}
+
+export interface buttonFieldInfo {
+ value: boolean,
+ label: string,
+}
+
+export type ButtonList = KeyVal<buttonFieldInfo>
+
+export interface OptionsButtonProps {
+ name: string,
+ label: string,
+ fieldState: Forms.FieldState<KeyVal<boolean>>,
+}
+
+export type RadioList = KeyVal<string>
+
+export interface RadioFieldListProps {
+ classeName?: string;
+ state: Forms.FieldState<string>;
+ values: RadioList;
+ fieldProps: Forms.GenericFieldProps;
+}
+
+export interface ButtonFieldListProps {
+ classeName?: string;
+ state: Forms.FieldState<KeyVal<boolean>>;
+ fieldProps: Forms.GenericFieldProps;
+}
+
+export type fieldsName =
+ "precision" |
+ "main" |
+ "libEntry" |
+ "domains" |
+ "iLevel" |
+ "WideningDelay" |
+ "ArrayPrecisionLevel" |
+ "LinearLevel" |
+ "EqualityCall" |
+ "OctagonCall" |
+ "sLevel" |
+ "MinLoopUnroll" |
+ "AutoLoopUnroll" |
+ "HistoryPartitioning" |
+ "SplitReturn" |
+ "AllocReturnsNull" |
+ "WarnPointerComparison"
+
+export interface EvaField {
+ label: string,
+ step?: number,
+ min?: number,
+ max?: number,
+ optionRadio?: KeyVal<string>,
+ /* eslint-disable-next-line @typescript-eslint/no-explicit-any */
+ state: Forms.FieldState<any>
+}
+
+export type EvaFormProps = {[key in fieldsName]: EvaField};
+
+/* ************************************************************************ *
+ * Option Eva Forms
+ * ************************************************************************ */
+export const fieldsPrecisionDependent: fieldsName[] = [
+ "MinLoopUnroll",
+ "AutoLoopUnroll",
+ "WideningDelay",
+ "HistoryPartitioning",
+ "sLevel",
+ "iLevel",
+ "ArrayPrecisionLevel",
+ "LinearLevel",
+ "domains",
+ "SplitReturn",
+ "EqualityCall",
+ "OctagonCall"
+];
+
+export const fieldsAlwaysVisible:fieldsName[] = [
+ "precision",
+ "main",
+ "libEntry",
+ "domains",
+ "sLevel",
+ "iLevel",
+ "AutoLoopUnroll",
+ "SplitReturn",
+ "AllocReturnsNull",
+ "WarnPointerComparison",
+];
+
+export const formEvaDomains: KeyVal<boolean> = {
+ 'equality': false,
+ 'symbolic-locations': false,
+ 'octagon': false,
+ 'gauges': false,
+ 'cvalue': false,
+};
+export const formEvaSplitReturn: KeyVal<string> = {
+ '': 'None',
+ 'full': 'Full',
+ 'auto': 'Auto'
+};
+
+export const formEvaPointerComparison: KeyVal<string> = {
+ '': 'None',
+ 'pointer': 'Pointer',
+ 'all': 'All'
+};
+
+export const formEvaEqualityCall: KeyVal<string> = {
+ 'none': 'None',
+ 'formals': 'Formals',
+ 'all': 'All'
+};
+
+export const domainsToKeyVal = (value: string[]): KeyVal<boolean> => {
+ const domains = { ...formEvaDomains };
+ for (const domain of value) { domains[domain] = true; }
+ return domains;
+};
+
+export const KeyValToDomains = (value: KeyVal<boolean>):string[] => {
+ return Object.entries(value).reduce(function (acc: string[], cur) {
+ if(cur[1]) acc.push(cur[0]);
+ return acc;
+ }, []);
+};
+
+export function buttonListEquality(
+ a: KeyVal<boolean>, b: KeyVal<boolean>
+): boolean {
+ const _a = Object.entries(a);
+ const _b = Object.entries(b);
+
+ if(_a.length !== _b.length) return false;
+ for (const [aKey, aValue] of _a.values()) {
+ const bProperty = _b.find(([bkey, ]) => bkey === aKey);
+ if(bProperty === undefined) return false;
+
+ const [, bValue] = bProperty;
+ if(aValue !== bValue) return false;
+ }
+ return true;
+}
+
+export function domainsEquality(
+ a: string[], b: string[]
+): boolean {
+ return buttonListEquality(
+ domainsToKeyVal(a),
+ domainsToKeyVal(b)
+ );
+}
diff --git a/ivette/src/frama-c/plugins/eva/EvaSidebar.tsx b/ivette/src/frama-c/plugins/eva/EvaSidebar.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..8fd99f1dd9c1f89060648848f6daf776bcbd8922
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/EvaSidebar.tsx
@@ -0,0 +1,163 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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 * as Forms from 'dome/layout/forms';
+import * as Ivette from 'ivette';
+import { useServerField } from 'frama-c/states';
+import * as EVA from 'frama-c/plugins/eva/api/general';
+import * as EvaDef from 'frama-c/plugins/eva/EvaDefinitions';
+import { EvaFormOptions } from 'frama-c/plugins/eva/components/Form';
+import EvaTools from './components/Tools';
+
+
+export function EvaSideBar(): JSX.Element {
+ const remote = Forms.useController();
+
+ /* eslint-disable max-len */
+ const precision = Forms.useBuffer(remote, useServerField(EVA.precision, 0));
+ const main = Forms.useBuffer(remote, useServerField(EVA.main, ""));
+ const libEntry = Forms.useBuffer(remote, useServerField(EVA.libEntry, false));
+ const domains = Forms.useBuffer(remote, useServerField(EVA.Domains, ["cvalue"]));
+ const domainsFiltered = Forms.useFilter(
+ domains,
+ EvaDef.domainsToKeyVal,
+ EvaDef.KeyValToDomains,
+ EvaDef.formEvaDomains
+ );
+ const WideningDelay = Forms.useBuffer(remote, useServerField(EVA.WideningDelay, 0));
+ const ArrayPrecisionLevel = Forms.useBuffer(remote, useServerField(EVA.ArrayPrecisionLevel, 0));
+ const LinearLevel = Forms.useBuffer(remote, useServerField(EVA.LinearLevel, 0));
+ const EqualityCall = Forms.useBuffer(remote, useServerField(EVA.EqualityCall, "none"));
+ const OctagonCall = Forms.useBuffer(remote, useServerField(EVA.OctagonCall, false));
+ const sLevel = Forms.useBuffer(remote, useServerField(EVA.slevel, 0));
+ const iLevel = Forms.useBuffer(remote, useServerField(EVA.ilevel, 0));
+ const AutoLoopUnroll = Forms.useBuffer(remote, useServerField(EVA.AutoLoopUnroll, 0));
+ const MinLoopUnroll = Forms.useBuffer(remote, useServerField(EVA.MinLoopUnroll, 0));
+ const SplitReturn = Forms.useBuffer(remote, useServerField(EVA.SplitReturn, "none"));
+ const HistoryPartitioning = Forms.useBuffer(remote, useServerField(EVA.HistoryPartitioning, 0));
+ const AllocReturnsNull = Forms.useBuffer(remote, useServerField(EVA.AllocReturnsNull, false));
+ const WarnPointerComparison = Forms.useBuffer(remote, useServerField(EVA.WarnPointerComparison, "none"));
+ /* eslint-enable max-len */
+
+ const evaFields = {
+ "precision": {
+ label: "Precision",
+ step: 1, min: -1, max: 11,
+ state: precision
+ },
+ "main": {
+ label: "Main",
+ state: main
+ },
+ "libEntry": {
+ label: "LibEntry",
+ state: libEntry
+ },
+ "domains": {
+ label: "Domains",
+ state: domainsFiltered
+ },
+ "sLevel": {
+ label: "Slevel",
+ step: 100, min: 0, max: 5000,
+ state: sLevel
+ },
+ "iLevel": {
+ label: "Ilevel",
+ step: 10, min: 0, max: 256,
+ state: iLevel
+ },
+ "AutoLoopUnroll": {
+ label: "Auto loop unroll",
+ step: 50, min: 0, max: 1024,
+ state: AutoLoopUnroll
+ },
+ "SplitReturn": {
+ label: "Split return",
+ optionRadio: EvaDef.formEvaSplitReturn,
+ state: SplitReturn
+ },
+ "AllocReturnsNull": {
+ label: "Alloc returns null",
+ state: AllocReturnsNull
+ },
+ "WarnPointerComparison": {
+ label: "Warn pointer comparison",
+ optionRadio: EvaDef.formEvaPointerComparison,
+ state: WarnPointerComparison
+ },
+ "MinLoopUnroll": {
+ label: "Min loop unroll",
+ step: 1, min: 0, max: 4,
+ state: MinLoopUnroll
+ },
+ "WideningDelay": {
+ label: "Widening delay",
+ step: 1, min: 1, max: 6,
+ state: WideningDelay
+ },
+ "HistoryPartitioning": {
+ label: "History partitioning",
+ step: 1, min: 0, max: 2,
+ state: HistoryPartitioning
+ },
+ "ArrayPrecisionLevel": {
+ label: "PLevel",
+ step: 100, min: 0, max: 5000,
+ state: ArrayPrecisionLevel
+ },
+ "LinearLevel": {
+ label: "Linear level",
+ step: 5, min: 0, max: 220,
+ state: LinearLevel
+ },
+ "EqualityCall": {
+ label: "Equality call",
+ optionRadio: EvaDef.formEvaEqualityCall,
+ state: EqualityCall
+ },
+ "OctagonCall": {
+ label: "Octagon call",
+ state: OctagonCall
+ },
+ };
+
+ return (
+ <>
+ <EvaTools
+ remote={remote}
+ iconSize={18}
+ />
+ <EvaFormOptions
+ fields={evaFields}
+ />
+ </>
+ );
+}
+
+Ivette.registerSidebar({
+ id: 'frama-c.plugins.eva_sidebar',
+ label: 'EVA',
+ title: 'Eva Sidebar',
+ children: <EvaSideBar />,
+});
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index c37d5121b0b153e16622f7c4a2a01e83b54d3c20..3fa6e0e86bc025c8e8e05475ba9e9ad8c75cb4f6 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -42,6 +42,8 @@ import { byDecl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { byMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { bySource } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { decl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { declDefault } from 'frama-c/kernel/api/ast';
@@ -50,10 +52,16 @@ import { jDecl } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { jMarker } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { jSource } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { marker } from 'frama-c/kernel/api/ast';
//@ts-ignore
import { markerDefault } from 'frama-c/kernel/api/ast';
//@ts-ignore
+import { source } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { sourceDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
import { byTag } from 'frama-c/kernel/api/data';
//@ts-ignore
import { jTag } from 'frama-c/kernel/api/data';
@@ -760,4 +768,663 @@ export const getStates: Server.GetRequest<
[ string, string, string ][]
>= getStates_internal;
+const getCurrentLoc_internal: Server.GetRequest<null,source> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getCurrentLoc',
+ input: Json.jNull,
+ output: jSource,
+ fallback: sourceDefault,
+ signals: [],
+};
+/** Get current location */
+export const getCurrentLoc: Server.GetRequest<null,source>= getCurrentLoc_internal;
+
+/** Signal for state [`eva`](#eva) */
+export const signalEva: Server.Signal = {
+ name: 'plugins.eva.general.signalEva',
+};
+
+const getEva_internal: Server.GetRequest<null,boolean> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getEva',
+ input: Json.jNull,
+ output: Json.jBoolean,
+ fallback: false,
+ signals: [],
+};
+/** Getter for state [`eva`](#eva) */
+export const getEva: Server.GetRequest<null,boolean>= getEva_internal;
+
+const setEva_internal: Server.SetRequest<boolean,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setEva',
+ input: Json.jBoolean,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`eva`](#eva) */
+export const setEva: Server.SetRequest<boolean,null>= setEva_internal;
+
+const eva_internal: State.State<boolean> = {
+ name: 'plugins.eva.general.eva',
+ signal: signalEva,
+ getter: getEva,
+ setter: setEva,
+};
+/** Eva enabled */
+export const eva: State.State<boolean> = eva_internal;
+
+/** Signal for state [`precision`](#precision) */
+export const signalPrecision: Server.Signal = {
+ name: 'plugins.eva.general.signalPrecision',
+};
+
+const getPrecision_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getPrecision',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`precision`](#precision) */
+export const getPrecision: Server.GetRequest<null,number>= getPrecision_internal;
+
+const setPrecision_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setPrecision',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`precision`](#precision) */
+export const setPrecision: Server.SetRequest<number,null>= setPrecision_internal;
+
+const precision_internal: State.State<number> = {
+ name: 'plugins.eva.general.precision',
+ signal: signalPrecision,
+ getter: getPrecision,
+ setter: setPrecision,
+};
+/** Precision value */
+export const precision: State.State<number> = precision_internal;
+
+/** Signal for state [`slevel`](#slevel) */
+export const signalSlevel: Server.Signal = {
+ name: 'plugins.eva.general.signalSlevel',
+};
+
+const getSlevel_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getSlevel',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`slevel`](#slevel) */
+export const getSlevel: Server.GetRequest<null,number>= getSlevel_internal;
+
+const setSlevel_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setSlevel',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`slevel`](#slevel) */
+export const setSlevel: Server.SetRequest<number,null>= setSlevel_internal;
+
+const slevel_internal: State.State<number> = {
+ name: 'plugins.eva.general.slevel',
+ signal: signalSlevel,
+ getter: getSlevel,
+ setter: setSlevel,
+};
+/** slevel value */
+export const slevel: State.State<number> = slevel_internal;
+
+/** Signal for state [`main`](#main) */
+export const signalMain: Server.Signal = {
+ name: 'plugins.eva.general.signalMain',
+};
+
+const getMain_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getMain',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`main`](#main) */
+export const getMain: Server.GetRequest<null,string>= getMain_internal;
+
+const setMain_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setMain',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`main`](#main) */
+export const setMain: Server.SetRequest<string,null>= setMain_internal;
+
+const main_internal: State.State<string> = {
+ name: 'plugins.eva.general.main',
+ signal: signalMain,
+ getter: getMain,
+ setter: setMain,
+};
+/** main function */
+export const main: State.State<string> = main_internal;
+
+/** Signal for state [`libEntry`](#libentry) */
+export const signalLibEntry: Server.Signal = {
+ name: 'plugins.eva.general.signalLibEntry',
+};
+
+const getLibEntry_internal: Server.GetRequest<null,boolean> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getLibEntry',
+ input: Json.jNull,
+ output: Json.jBoolean,
+ fallback: false,
+ signals: [],
+};
+/** Getter for state [`libEntry`](#libentry) */
+export const getLibEntry: Server.GetRequest<null,boolean>= getLibEntry_internal;
+
+const setLibEntry_internal: Server.SetRequest<boolean,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setLibEntry',
+ input: Json.jBoolean,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`libEntry`](#libentry) */
+export const setLibEntry: Server.SetRequest<boolean,null>= setLibEntry_internal;
+
+const libEntry_internal: State.State<boolean> = {
+ name: 'plugins.eva.general.libEntry',
+ signal: signalLibEntry,
+ getter: getLibEntry,
+ setter: setLibEntry,
+};
+/** slevel value */
+export const libEntry: State.State<boolean> = libEntry_internal;
+
+/** Signal for state [`Domains`](#domains) */
+export const signalDomains: Server.Signal = {
+ name: 'plugins.eva.general.signalDomains',
+};
+
+const getDomains_internal: Server.GetRequest<null,string[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getDomains',
+ input: Json.jNull,
+ output: Json.jArray(Json.jString),
+ fallback: [],
+ signals: [],
+};
+/** Getter for state [`Domains`](#domains) */
+export const getDomains: Server.GetRequest<null,string[]>= getDomains_internal;
+
+const setDomains_internal: Server.SetRequest<string[],null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setDomains',
+ input: Json.jArray(Json.jString),
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`Domains`](#domains) */
+export const setDomains: Server.SetRequest<string[],null>= setDomains_internal;
+
+const Domains_internal: State.State<string[]> = {
+ name: 'plugins.eva.general.Domains',
+ signal: signalDomains,
+ getter: getDomains,
+ setter: setDomains,
+};
+/** domains value */
+export const Domains: State.State<string[]> = Domains_internal;
+
+/** Signal for state [`ilevel`](#ilevel) */
+export const signalIlevel: Server.Signal = {
+ name: 'plugins.eva.general.signalIlevel',
+};
+
+const getIlevel_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getIlevel',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`ilevel`](#ilevel) */
+export const getIlevel: Server.GetRequest<null,number>= getIlevel_internal;
+
+const setIlevel_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setIlevel',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`ilevel`](#ilevel) */
+export const setIlevel: Server.SetRequest<number,null>= setIlevel_internal;
+
+const ilevel_internal: State.State<number> = {
+ name: 'plugins.eva.general.ilevel',
+ signal: signalIlevel,
+ getter: getIlevel,
+ setter: setIlevel,
+};
+/** ilevel value */
+export const ilevel: State.State<number> = ilevel_internal;
+
+/** Signal for state [`MinLoopUnroll`](#minloopunroll) */
+export const signalMinLoopUnroll: Server.Signal = {
+ name: 'plugins.eva.general.signalMinLoopUnroll',
+};
+
+const getMinLoopUnroll_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getMinLoopUnroll',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`MinLoopUnroll`](#minloopunroll) */
+export const getMinLoopUnroll: Server.GetRequest<null,number>= getMinLoopUnroll_internal;
+
+const setMinLoopUnroll_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setMinLoopUnroll',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`MinLoopUnroll`](#minloopunroll) */
+export const setMinLoopUnroll: Server.SetRequest<number,null>= setMinLoopUnroll_internal;
+
+const MinLoopUnroll_internal: State.State<number> = {
+ name: 'plugins.eva.general.MinLoopUnroll',
+ signal: signalMinLoopUnroll,
+ getter: getMinLoopUnroll,
+ setter: setMinLoopUnroll,
+};
+/** Min loop unroll value */
+export const MinLoopUnroll: State.State<number> = MinLoopUnroll_internal;
+
+/** Signal for state [`AutoLoopUnroll`](#autoloopunroll) */
+export const signalAutoLoopUnroll: Server.Signal = {
+ name: 'plugins.eva.general.signalAutoLoopUnroll',
+};
+
+const getAutoLoopUnroll_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getAutoLoopUnroll',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`AutoLoopUnroll`](#autoloopunroll) */
+export const getAutoLoopUnroll: Server.GetRequest<null,number>= getAutoLoopUnroll_internal;
+
+const setAutoLoopUnroll_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setAutoLoopUnroll',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`AutoLoopUnroll`](#autoloopunroll) */
+export const setAutoLoopUnroll: Server.SetRequest<number,null>= setAutoLoopUnroll_internal;
+
+const AutoLoopUnroll_internal: State.State<number> = {
+ name: 'plugins.eva.general.AutoLoopUnroll',
+ signal: signalAutoLoopUnroll,
+ getter: getAutoLoopUnroll,
+ setter: setAutoLoopUnroll,
+};
+/** Auto loop unroll value */
+export const AutoLoopUnroll: State.State<number> = AutoLoopUnroll_internal;
+
+/** Signal for state [`WideningDelay`](#wideningdelay) */
+export const signalWideningDelay: Server.Signal = {
+ name: 'plugins.eva.general.signalWideningDelay',
+};
+
+const getWideningDelay_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getWideningDelay',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`WideningDelay`](#wideningdelay) */
+export const getWideningDelay: Server.GetRequest<null,number>= getWideningDelay_internal;
+
+const setWideningDelay_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setWideningDelay',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`WideningDelay`](#wideningdelay) */
+export const setWideningDelay: Server.SetRequest<number,null>= setWideningDelay_internal;
+
+const WideningDelay_internal: State.State<number> = {
+ name: 'plugins.eva.general.WideningDelay',
+ signal: signalWideningDelay,
+ getter: getWideningDelay,
+ setter: setWideningDelay,
+};
+/** Widening delay */
+export const WideningDelay: State.State<number> = WideningDelay_internal;
+
+/** Signal for state [`HistoryPartitioning`](#historypartitioning) */
+export const signalHistoryPartitioning: Server.Signal = {
+ name: 'plugins.eva.general.signalHistoryPartitioning',
+};
+
+const getHistoryPartitioning_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getHistoryPartitioning',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`HistoryPartitioning`](#historypartitioning) */
+export const getHistoryPartitioning: Server.GetRequest<null,number>= getHistoryPartitioning_internal;
+
+const setHistoryPartitioning_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setHistoryPartitioning',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`HistoryPartitioning`](#historypartitioning) */
+export const setHistoryPartitioning: Server.SetRequest<number,null>= setHistoryPartitioning_internal;
+
+const HistoryPartitioning_internal: State.State<number> = {
+ name: 'plugins.eva.general.HistoryPartitioning',
+ signal: signalHistoryPartitioning,
+ getter: getHistoryPartitioning,
+ setter: setHistoryPartitioning,
+};
+/** History partitioning */
+export const HistoryPartitioning: State.State<number> = HistoryPartitioning_internal;
+
+/** Signal for state [`ArrayPrecisionLevel`](#arrayprecisionlevel) */
+export const signalArrayPrecisionLevel: Server.Signal = {
+ name: 'plugins.eva.general.signalArrayPrecisionLevel',
+};
+
+const getArrayPrecisionLevel_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getArrayPrecisionLevel',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`ArrayPrecisionLevel`](#arrayprecisionlevel) */
+export const getArrayPrecisionLevel: Server.GetRequest<null,number>= getArrayPrecisionLevel_internal;
+
+const setArrayPrecisionLevel_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setArrayPrecisionLevel',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`ArrayPrecisionLevel`](#arrayprecisionlevel) */
+export const setArrayPrecisionLevel: Server.SetRequest<number,null>= setArrayPrecisionLevel_internal;
+
+const ArrayPrecisionLevel_internal: State.State<number> = {
+ name: 'plugins.eva.general.ArrayPrecisionLevel',
+ signal: signalArrayPrecisionLevel,
+ getter: getArrayPrecisionLevel,
+ setter: setArrayPrecisionLevel,
+};
+/** Array precision level */
+export const ArrayPrecisionLevel: State.State<number> = ArrayPrecisionLevel_internal;
+
+/** Signal for state [`LinearLevel`](#linearlevel) */
+export const signalLinearLevel: Server.Signal = {
+ name: 'plugins.eva.general.signalLinearLevel',
+};
+
+const getLinearLevel_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getLinearLevel',
+ input: Json.jNull,
+ output: Json.jNumber,
+ fallback: 0,
+ signals: [],
+};
+/** Getter for state [`LinearLevel`](#linearlevel) */
+export const getLinearLevel: Server.GetRequest<null,number>= getLinearLevel_internal;
+
+const setLinearLevel_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setLinearLevel',
+ input: Json.jNumber,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`LinearLevel`](#linearlevel) */
+export const setLinearLevel: Server.SetRequest<number,null>= setLinearLevel_internal;
+
+const LinearLevel_internal: State.State<number> = {
+ name: 'plugins.eva.general.LinearLevel',
+ signal: signalLinearLevel,
+ getter: getLinearLevel,
+ setter: setLinearLevel,
+};
+/** Linear level */
+export const LinearLevel: State.State<number> = LinearLevel_internal;
+
+/** Signal for state [`EqualityCall`](#equalitycall) */
+export const signalEqualityCall: Server.Signal = {
+ name: 'plugins.eva.general.signalEqualityCall',
+};
+
+const getEqualityCall_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getEqualityCall',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`EqualityCall`](#equalitycall) */
+export const getEqualityCall: Server.GetRequest<null,string>= getEqualityCall_internal;
+
+const setEqualityCall_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setEqualityCall',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`EqualityCall`](#equalitycall) */
+export const setEqualityCall: Server.SetRequest<string,null>= setEqualityCall_internal;
+
+const EqualityCall_internal: State.State<string> = {
+ name: 'plugins.eva.general.EqualityCall',
+ signal: signalEqualityCall,
+ getter: getEqualityCall,
+ setter: setEqualityCall,
+};
+/** Equality call */
+export const EqualityCall: State.State<string> = EqualityCall_internal;
+
+/** Signal for state [`OctagonCall`](#octagoncall) */
+export const signalOctagonCall: Server.Signal = {
+ name: 'plugins.eva.general.signalOctagonCall',
+};
+
+const getOctagonCall_internal: Server.GetRequest<null,boolean> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getOctagonCall',
+ input: Json.jNull,
+ output: Json.jBoolean,
+ fallback: false,
+ signals: [],
+};
+/** Getter for state [`OctagonCall`](#octagoncall) */
+export const getOctagonCall: Server.GetRequest<null,boolean>= getOctagonCall_internal;
+
+const setOctagonCall_internal: Server.SetRequest<boolean,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setOctagonCall',
+ input: Json.jBoolean,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`OctagonCall`](#octagoncall) */
+export const setOctagonCall: Server.SetRequest<boolean,null>= setOctagonCall_internal;
+
+const OctagonCall_internal: State.State<boolean> = {
+ name: 'plugins.eva.general.OctagonCall',
+ signal: signalOctagonCall,
+ getter: getOctagonCall,
+ setter: setOctagonCall,
+};
+/** Octagon call */
+export const OctagonCall: State.State<boolean> = OctagonCall_internal;
+
+/** Signal for state [`SplitReturn`](#splitreturn) */
+export const signalSplitReturn: Server.Signal = {
+ name: 'plugins.eva.general.signalSplitReturn',
+};
+
+const getSplitReturn_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getSplitReturn',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`SplitReturn`](#splitreturn) */
+export const getSplitReturn: Server.GetRequest<null,string>= getSplitReturn_internal;
+
+const setSplitReturn_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setSplitReturn',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`SplitReturn`](#splitreturn) */
+export const setSplitReturn: Server.SetRequest<string,null>= setSplitReturn_internal;
+
+const SplitReturn_internal: State.State<string> = {
+ name: 'plugins.eva.general.SplitReturn',
+ signal: signalSplitReturn,
+ getter: getSplitReturn,
+ setter: setSplitReturn,
+};
+/** Split return value */
+export const SplitReturn: State.State<string> = SplitReturn_internal;
+
+/** Signal for state [`AllocReturnsNull`](#allocreturnsnull) */
+export const signalAllocReturnsNull: Server.Signal = {
+ name: 'plugins.eva.general.signalAllocReturnsNull',
+};
+
+const getAllocReturnsNull_internal: Server.GetRequest<null,boolean> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getAllocReturnsNull',
+ input: Json.jNull,
+ output: Json.jBoolean,
+ fallback: false,
+ signals: [],
+};
+/** Getter for state [`AllocReturnsNull`](#allocreturnsnull) */
+export const getAllocReturnsNull: Server.GetRequest<null,boolean>= getAllocReturnsNull_internal;
+
+const setAllocReturnsNull_internal: Server.SetRequest<boolean,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setAllocReturnsNull',
+ input: Json.jBoolean,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`AllocReturnsNull`](#allocreturnsnull) */
+export const setAllocReturnsNull: Server.SetRequest<boolean,null>= setAllocReturnsNull_internal;
+
+const AllocReturnsNull_internal: State.State<boolean> = {
+ name: 'plugins.eva.general.AllocReturnsNull',
+ signal: signalAllocReturnsNull,
+ getter: getAllocReturnsNull,
+ setter: setAllocReturnsNull,
+};
+/** AllocReturnsNull value */
+export const AllocReturnsNull: State.State<boolean> = AllocReturnsNull_internal;
+
+/** Signal for state [`WarnPointerComparison`](#warnpointercomparison) */
+export const signalWarnPointerComparison: Server.Signal = {
+ name: 'plugins.eva.general.signalWarnPointerComparison',
+};
+
+const getWarnPointerComparison_internal: Server.GetRequest<null,string> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getWarnPointerComparison',
+ input: Json.jNull,
+ output: Json.jString,
+ fallback: '',
+ signals: [],
+};
+/** Getter for state [`WarnPointerComparison`](#warnpointercomparison) */
+export const getWarnPointerComparison: Server.GetRequest<null,string>= getWarnPointerComparison_internal;
+
+const setWarnPointerComparison_internal: Server.SetRequest<string,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.eva.general.setWarnPointerComparison',
+ input: Json.jString,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Setter for state [`WarnPointerComparison`](#warnpointercomparison) */
+export const setWarnPointerComparison: Server.SetRequest<string,null>= setWarnPointerComparison_internal;
+
+const WarnPointerComparison_internal: State.State<string> = {
+ name: 'plugins.eva.general.WarnPointerComparison',
+ signal: signalWarnPointerComparison,
+ getter: getWarnPointerComparison,
+ setter: setWarnPointerComparison,
+};
+/** Warn pointer comparison value */
+export const WarnPointerComparison: State.State<string> = WarnPointerComparison_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/components/Form.tsx b/ivette/src/frama-c/plugins/eva/components/Form.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..88bf5fe38b3a91133b573db6432737b354928f63
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/components/Form.tsx
@@ -0,0 +1,289 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+// --------------------------------------------------------------------------
+// --- Sidebar Selector
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import * as Forms from 'dome/layout/forms';
+import { classes } from 'dome/misc/utils';
+import * as Globals from 'frama-c/kernel/Globals';
+import * as States from 'frama-c/states';
+import * as Ast from 'frama-c/kernel/api/ast';
+import * as Eva from 'frama-c/plugins/eva/api/general';
+import * as EvaDef from 'frama-c/plugins/eva/EvaDefinitions';
+
+/* -------------------------------------------------------------------------- */
+/* --- Eva form section --- */
+/* -------------------------------------------------------------------------- */
+function Section(p: Forms.SectionProps): JSX.Element {
+ const settings = `ivette.eva.option.${p.label}`;
+ return (
+ <Forms.Section
+ label={p.label}
+ unfold
+ error={p.error}
+ settings={settings}
+ >
+ {p.children}
+ </Forms.Section>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Button/Radio list --- */
+/* -------------------------------------------------------------------------- */
+function OptionsButton(props: EvaDef.OptionsButtonProps): JSX.Element {
+ const { name, label, fieldState } = props;
+ const state = Forms.useProperty(fieldState, name);
+ return <Forms.ButtonField label={label} state={state} />;
+}
+
+function ButtonFieldList(
+ props: EvaDef.ButtonFieldListProps
+): JSX.Element {
+ const { classeName, state, fieldProps } = props;
+ const { value } = state;
+
+ const htmlButtonList = Object.keys(value)
+ .map((p) => <OptionsButton
+ key={p}
+ name={p}
+ label={p}
+ fieldState={state}
+ />);
+ return (
+ <Forms.Field {...fieldProps}>
+ <div className={classeName}></div>
+ {htmlButtonList}
+ </Forms.Field>
+ );
+}
+
+export function RadioFieldList(
+ props: EvaDef.RadioFieldListProps
+): JSX.Element {
+ const { classeName, state, values, fieldProps } = props;
+ const htmlRadioList = Object.entries(values)
+ .map(([k, v]) => <Forms.RadioField
+ key={k}
+ label={v}
+ value={k}
+ state={state}
+ />);
+ return (
+ <Forms.Field {...fieldProps}>
+ <div className={classeName}></div>
+ {htmlRadioList}
+ </Forms.Field>
+ );
+}
+
+
+/** ***************************************************************************
+*
+******************************************************************************/
+interface EvaFormOptionsProps {
+ fields: EvaDef.EvaFormProps;
+}
+
+function getActions<A>(
+ state: Forms.FieldState<A>,
+ equal?: (a: A, b: A) => boolean,
+): JSX.Element | undefined {
+ if(!state) return undefined;
+ return (
+ <Forms.Actions>
+ <Forms.ResetButton
+ state={state}
+ title="Reset"
+ equal={equal}
+ />
+ <Forms.CommitButton
+ state={state}
+ title="Commit"
+ equal={equal}
+ />
+ </Forms.Actions>
+ );
+}
+
+export function EvaFormOptions(
+ props: EvaFormOptionsProps
+): JSX.Element {
+ const { fields } = props;
+
+ const showAllFields = Forms.useState(false);
+
+ const ker = States.useSyncArrayProxy(Ast.functions);
+ const eva = States.useSyncArrayProxy(Eva.functions);
+ const fctsList = React.useMemo(() =>
+ Globals.computeFcts(ker, eva)
+ .filter((fct) => !fct.extern && !fct.stdlib && !fct.builtin)
+ .sort((a, b) => a.name.localeCompare(b.name)),
+ [ker, eva]
+ );
+
+ function isNoAlwaysVisibleFieldsStable(): boolean {
+ let disable = false;
+ for (const [name, evaField] of Object.entries(fields)) {
+ if (EvaDef.fieldsAlwaysVisible.includes(name as EvaDef.fieldsName)) {
+ continue;
+ }
+ if (!Forms.isStable(evaField.state)) {
+ disable = true;
+ break;
+ }
+ }
+ return disable;
+ }
+
+ function getClasses<A>(
+ state: Forms.FieldState<A>,
+ name: EvaDef.fieldsName
+ ): string | undefined {
+ const isDepPrecision = EvaDef.fieldsPrecisionDependent.includes(name);
+ const notVisible =
+ !showAllFields.value &&
+ !EvaDef.fieldsAlwaysVisible.includes(name);
+ return classes(
+ !Forms.isStable(state) && "eva-field-modified",
+ isDepPrecision && "eva-precision-dep",
+ notVisible ? "hidden-field" : "visible-field"
+ );
+ }
+
+ function getSpinnerField(name: EvaDef.fieldsName): JSX.Element {
+ const field = fields[name];
+ const state = field.state;
+ return (
+ <Forms.SpinnerField
+ label={field.label}
+ step={field.step}
+ min={field.min as number}
+ max={field.max as number}
+ state={field.state as Forms.FieldState<number | undefined>}
+ className={getClasses(state, name)}
+ actions={getActions(state)}
+ />
+ );
+ }
+
+ function getRadioField(name: EvaDef.fieldsName): JSX.Element {
+ const field = fields[name];
+ const state = field.state;
+ return (
+ <RadioFieldList
+ fieldProps={{
+ label: field.label,
+ actions: getActions(state)
+ }}
+ classeName={getClasses(state, name)}
+ values={field.optionRadio as EvaDef.RadioList}
+ state={field.state}
+ />
+ );
+ }
+
+ function getBooleanField(name: EvaDef.fieldsName): JSX.Element {
+ const field = fields[name];
+ const state = field.state;
+ return (
+ <Forms.Field
+ label={field.label}
+ actions={getActions(state)}
+ >
+ <div className={getClasses(state, "libEntry")} />
+ <Forms.ButtonField
+ label={state.value ? "Enabled" : "disabled"}
+ state={state}
+ />
+ </Forms.Field>
+ );
+ }
+
+ const mainField =
+ <Forms.SelectField
+ label="Eva main"
+ state={fields["main"].state as Forms.FieldState<string | undefined>}
+ actions={getActions(fields["main"].state)}
+ >
+ {
+ fctsList.map((f) => <option
+ key={f.key} id={f.key} value={f.name}
+ className={getClasses(fields["main"].state, "main")}
+ >{f.name}</option>
+ )
+ }
+ </Forms.SelectField>;
+
+ const domainsField =
+ <ButtonFieldList
+ fieldProps={{
+ label: "Domains",
+ actions: getActions(fields["domains"].state, EvaDef.buttonListEquality)
+ }}
+ classeName={getClasses(fields["domains"].state, "domains")}
+ state={fields["domains"].state}
+ />;
+
+ return (
+ <Forms.SidebarForm className="eva-form">
+ <Forms.CheckboxField
+ label={"show all fields"}
+ title=
+ "disabled if it checked and if the fields to be hidden are not stable"
+ state={showAllFields}
+ disabled={isNoAlwaysVisibleFieldsStable()}
+ />
+
+ {getSpinnerField("precision")}
+ {mainField}
+ {getBooleanField("libEntry")}
+
+ <Section label="Abstract interpretation" >
+ {domainsField}
+ {getSpinnerField("iLevel")}
+ {getSpinnerField("WideningDelay")}
+ {getSpinnerField("ArrayPrecisionLevel")}
+ {getSpinnerField("LinearLevel")}
+ {getRadioField("EqualityCall")}
+ {getBooleanField("OctagonCall")}
+ </Section>
+
+ <Section label="State partitioning" >
+ {getSpinnerField("sLevel")}
+ {getSpinnerField("MinLoopUnroll")}
+ {getSpinnerField("AutoLoopUnroll")}
+ {getSpinnerField("HistoryPartitioning")}
+ {getRadioField("SplitReturn")}
+ </Section>
+
+ <Section label="Message" >
+ {getBooleanField("AllocReturnsNull")}
+ {getRadioField("WarnPointerComparison")}
+ </Section>
+
+ </Forms.SidebarForm>
+ );
+}
diff --git a/ivette/src/frama-c/plugins/eva/components/Tools.tsx b/ivette/src/frama-c/plugins/eva/components/Tools.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..b40233e6dec283d25796be82e76188dd37d8bf46
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/components/Tools.tsx
@@ -0,0 +1,114 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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 { IconButton } from 'dome/controls/buttons';
+import { Hbox } from 'dome/layout/boxes';
+import { Icon } from 'dome/controls/icons';
+import * as Forms from 'dome/layout/forms';
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+import * as Eva from 'frama-c/plugins/eva/api/general';
+
+
+export interface EvaToolsProps {
+ remote: Forms.BufferController;
+ iconSize: number;
+}
+
+function EvaState(
+ state: Eva.computationStateType | undefined
+): JSX.Element {
+ let id, title;
+ switch(state) {
+ case "computed": id="CHECK"; title="Computed"; break;
+ case "aborted": id="CROSS"; title="Aborted"; break;
+ case "not_computed": id="CROSS"; title="Not computed"; break;
+ case "computing": id="SPINNER"; title="Computing"; break;
+ default: id="CROSS"; title="Status undefined"; break;
+ }
+ return <Icon
+ id={id}
+ title={title}
+ className={"eva-status-icon eva-"+state}
+ size={18}
+ />;
+}
+
+export default function EvaTools(
+ props: EvaToolsProps
+): JSX.Element {
+ const { remote, iconSize } = props;
+
+ const evaComputed = States.useSyncValue(Eva.computationState);
+ const countErrors = remote.getErrors();
+ remote.resetNotified();
+
+ const compute = (): void => { Server.send(Eva.compute, null); };
+ const abort = (): void => { Server.send(Eva.abort, null); };
+ const syncFromFC = (): void => { remote.reset(); };
+ const syncToFC = (): void => { remote.commit(); };
+
+ return (
+ <Hbox className='eva-tools'>
+ <Hbox className='eva-tools-actions'>
+ <IconButton
+ icon="MEDIA.PLAY"
+ title="Launch Eva analysis"
+ size={iconSize}
+ disabled={evaComputed !== "not_computed"}
+ onClick={compute}
+ />
+ <IconButton
+ icon="MEDIA.STOP"
+ title="Abort Eva analysis"
+ size={iconSize}
+ disabled={evaComputed !== "computing"}
+ onClick={abort}
+ />
+ <IconButton
+ icon="RELOAD"
+ title="Reset form"
+ size={iconSize}
+ disabled={!remote.hasReset()}
+ onClick={syncFromFC}
+ />
+ <IconButton
+ icon="PUSH"
+ title={"Commit changes"
+ +
+ (countErrors > 0 ?
+ " : "+String(countErrors)+" error(s) in the form" : ""
+ )
+ }
+ size={iconSize}
+ kind={countErrors > 0 ? "warning" : "default"}
+ disabled={!remote.hasCommit()}
+ onClick={syncToFC}
+ />
+ </Hbox>
+ <Hbox className='eva-tools-title'>
+ {EvaState(evaComputed)}
+ </Hbox>
+ </Hbox>
+ );
+}
diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 1aced6c446efa710f2a9ce3c002b7cc4a5aaf6cf..d277a0fe8d7446e85312ffb17e8d4534b23c8a03 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -29,6 +29,7 @@ import './valuetable';
import './Summary';
import './Coverage';
import './DomainStates';
+import './EvaSidebar';
import './style.css';
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index 2d6367d5845267d7a8f76eaca15084b32936e1e0..d76029885871fff8143f2d8ee72a0ef0b3235858 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -4,8 +4,10 @@
:root {
--eva-min-width: 90px;
+ --eva-shadow-warning: darkorange;
}
+
.eva-info {
width: 100%;
display: flex;
@@ -334,3 +336,165 @@ tr:first-of-type > .eva-table-callsite-box {
}
/* -------------------------------------------------------------------------- */
+/* --- Sidebar Eva --- */
+/* -------------------------------------------------------------------------- */
+@keyframes eva-spinner {
+ from {
+ transform: rotate(-90deg);
+ } to {
+ transform: rotate(270deg);
+ }
+}
+
+/* ------------------ */
+/* --- Tools Eva --- */
+.eva-tools {
+ display: block;
+ position: sticky;
+ top: 0px;
+ z-index: 10;
+ background-color: var(--background-profound);
+ padding: 5px;
+ border: 5px outset;
+ border-color: rgb(from var(--border-discrete) r g b / .7);
+ margin: 10px;
+ display: flex;
+ flex-wrap: wrap;
+ justify-content: space-between;
+
+ .eva-tools-actions {
+ display: flex;
+ flex-wrap: wrap;
+ }
+
+ .dome-xIconButton {
+ padding: 2px 5px;
+ }
+ .dome-xIconButton:hover {
+ cursor: pointer;
+ color: var(--background-button-hover);
+ }
+ .eva-status-icon.eva-computing {
+ transform: rotate(90deg);
+ animation: eva-spinner .9s linear infinite;
+ fill: var(--eva-alarms-unknown);
+ }
+ .eva-status-icon.eva-computed { fill: var(--eva-alarms-true); }
+ .eva-status-icon.eva-aborted,
+ .eva-status-icon.eva-not_computed {
+ fill: var(--eva-alarms-false);
+ }
+}
+
+/* ------------------ */
+/* --- Form Eva --- */
+.eva-form {
+ padding: 4px 12px;
+ display: flex;
+ flex-wrap: nowrap;
+ flex-direction: column;
+
+ >label.dome-xCheckbox{
+ display: flex;
+ flex-direction: row-reverse;
+ font-size: 1.08em;
+ padding: 5px;
+
+ &:hover {
+ color: var(--text-highlighted);
+ cursor:pointer;
+ input {
+ border: 1px solid var(--text-highlighted);
+ }
+ }
+
+ &:has(input:disabled),
+ &:hover:has(input:disabled) {
+ color: var(--disabled-text) !important;
+ cursor:default;
+ }
+
+ input {
+ margin-left: 10px;
+ padding-bottom: 0;
+ border: 1px solid var(--text-discrete);
+ }
+
+ input:checked { background-color: var(--positive-button-active) }
+ }
+
+ .dome-xForm-field-actions { min-width: 42px; }
+
+ .dome-xCheckbox { overflow: hidden; }
+
+ .dome-xForm-field {
+ padding: 1px;
+
+ >input[type=radio] { display: none; }
+ &:has(> input[type=radio]) {
+ min-width: 0px;
+ border-radius: 2em 2em;
+ margin: 2px 3px;
+ padding: 2px 10px;
+ }
+
+ &:has(> input[type=radio]:checked):hover {
+ border-color: var(--border);
+ cursor:default;
+ }
+ }
+
+ .dome-xButton,
+ .dome-xForm-field:has(> input[type=radio]) {
+ border: solid 1px;
+ border-color: var(--border);
+ color: var(--text-discrete);
+ background-color: transparent;
+ background-image: none;
+ }
+
+ .dome-xButton:hover,
+ .dome-xForm-field:has(> input[type=radio]):hover {
+ cursor: pointer;
+ border-color: var(--text-highlighted);
+ color: var(--text-highlighted);
+ background-color: transparent;
+ background-image: none ;
+ }
+
+ .dome-xButton-selected,
+ .dome-xForm-field:has(> input[type=radio]:checked) {
+ color: var(--text);
+ background-color: var(--checked-element);
+ background-image: none;
+ }
+
+ .dome-xButton-selected:hover {
+ border-color: var(--text-highlighted);
+ background-image: none ;
+ background-color: var(--checked-element);
+ opacity: 0.5;
+ }
+
+ .dome-xForm-field-block:has(> .dome-xForm-field .eva-field-modified) {
+ box-shadow: -4px 0px 4px var(--eva-shadow-warning);
+ }
+
+ .dome-xForm-field-block:has(.dome-xForm-field .hidden-field) {
+ display: none;
+ }
+
+ input[type=number] {
+ background-color: var(--background-interaction);
+ color: var(--text);
+ text-align: right;
+ width: 80px;
+ max-width: 100%;
+ margin-right: 0;
+ padding: 1px;
+ margin-right: 5px;
+ border: none;
+ }
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index c5cba410e23c386073a573169696b59005e06b61..536264d211f68f1f10dd9b14da1fedc0e25bc03d 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -22,6 +22,9 @@
open Server
open Cil_types
+module D = Server.Data
+module S = Server.States
+module Md = Markdown
let package =
Package.package
@@ -869,4 +872,189 @@ let () = Request.register ~package
~signals:[computation_signal]
get_states
+let () = Request.register ~package
+ ~kind:`GET ~name:"getCurrentLoc"
+ ~descr:(Md.plain "Get current location")
+ ~input:(module Data.Junit)
+ ~output:(module Kernel_ast.Position)
+ ~signals:[]
+ (fun () -> fst (Current_loc.get ()))
+
+(* -------------------------------------------------------------------------- *)
+(* --- Eva Options --- *)
+(* -------------------------------------------------------------------------- *)
+let _ =
+ S.register_state ~package
+ ~name:"eva"
+ ~descr:(Md.plain "Eva enabled")
+ ~data:(module D.Jbool)
+ ~get:Parameters.ForceValues.get
+ ~set:Parameters.ForceValues.set
+ ~add_hook:Parameters.ForceValues.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"precision"
+ ~descr:(Md.plain "Precision value")
+ ~data:(module D.Jint)
+ ~get:Parameters.Precision.get
+ ~set:Parameters.Precision.set
+ ~add_hook:Parameters.Precision.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"slevel"
+ ~descr:(Md.plain "slevel value")
+ ~data:(module D.Jint)
+ ~get:Parameters.SemanticUnrollingLevel.get
+ ~set:Parameters.SemanticUnrollingLevel.set
+ ~add_hook:Parameters.SemanticUnrollingLevel.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"main"
+ ~descr:(Md.plain "main function")
+ ~data:(module D.Jstring)
+ ~get:Kernel.MainFunction.get
+ ~set:Kernel.MainFunction.set
+ ~add_hook:Kernel.MainFunction.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"libEntry"
+ ~descr:(Md.plain "slevel value")
+ ~data:(module D.Jbool)
+ ~get:Kernel.LibEntry.get
+ ~set:Kernel.LibEntry.set
+ ~add_hook:Kernel.LibEntry.add_hook_on_update ()
+
+let get_domains () =
+ let set = Parameters.Domains.get () in
+ Datatype.String.Set.elements set
+
+let set_domains list =
+ let option = "cvalue" in
+ let set = Datatype.String.Set.of_list list in
+ Parameters.Domains.set (Datatype.String.Set.add option set)
+
+let signal =
+ S.register_state ~package
+ ~name:"Domains"
+ ~descr:(Md.plain "domains value")
+ ~data:(module D.Jlist (D.Jstring))
+ ~get:get_domains
+ ~set:set_domains
+ ()
+
+let () =
+ Parameters.Domains.add_update_hook (fun _ _ -> Request.emit signal)
+
+let _ =
+ S.register_state ~package
+ ~name:"ilevel"
+ ~descr:(Md.plain "ilevel value")
+ ~data:(module D.Jint)
+ ~get:Parameters.ILevel.get
+ ~set:Parameters.ILevel.set
+ ~add_hook:Parameters.ILevel.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"MinLoopUnroll"
+ ~descr:(Md.plain "Min loop unroll value")
+ ~data:(module D.Jint)
+ ~get:Parameters.MinLoopUnroll.get
+ ~set:Parameters.MinLoopUnroll.set
+ ~add_hook:Parameters.MinLoopUnroll.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"AutoLoopUnroll"
+ ~descr:(Md.plain "Auto loop unroll value")
+ ~data:(module D.Jint)
+ ~get:Parameters.AutoLoopUnroll.get
+ ~set:Parameters.AutoLoopUnroll.set
+ ~add_hook:Parameters.AutoLoopUnroll.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"WideningDelay"
+ ~descr:(Md.plain "Widening delay")
+ ~data:(module D.Jint)
+ ~get:Parameters.WideningDelay.get
+ ~set:Parameters.WideningDelay.set
+ ~add_hook:Parameters.WideningDelay.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"HistoryPartitioning"
+ ~descr:(Md.plain "History partitioning")
+ ~data:(module D.Jint)
+ ~get:Parameters.HistoryPartitioning.get
+ ~set:Parameters.HistoryPartitioning.set
+ ~add_hook:Parameters.HistoryPartitioning.add_hook_on_update ()
+
+
+let _ =
+ S.register_state ~package
+ ~name:"ArrayPrecisionLevel"
+ ~descr:(Md.plain "Array precision level")
+ ~data:(module D.Jint)
+ ~get:Parameters.ArrayPrecisionLevel.get
+ ~set:Parameters.ArrayPrecisionLevel.set
+ ~add_hook:Parameters.ArrayPrecisionLevel.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"LinearLevel"
+ ~descr:(Md.plain "Linear level")
+ ~data:(module D.Jint)
+ ~get:Parameters.LinearLevel.get
+ ~set:Parameters.LinearLevel.set
+ ~add_hook:Parameters.LinearLevel.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"EqualityCall"
+ ~descr:(Md.plain "Equality call")
+ ~data:(module D.Jstring)
+ ~get:Parameters.EqualityCall.get
+ ~set:Parameters.EqualityCall.set
+ ~add_hook:Parameters.EqualityCall.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"OctagonCall"
+ ~descr:(Md.plain "Octagon call")
+ ~data:(module D.Jbool)
+ ~get:Parameters.OctagonCall.get
+ ~set:Parameters.OctagonCall.set
+ ~add_hook:Parameters.OctagonCall.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"SplitReturn"
+ ~descr:(Md.plain "Split return value")
+ ~data:(module D.Jstring)
+ ~get:Parameters.SplitReturn.get
+ ~set:Parameters.SplitReturn.set
+ ~add_hook:Parameters.SplitReturn.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"AllocReturnsNull"
+ ~descr:(Md.plain "AllocReturnsNull value")
+ ~data:(module D.Jbool)
+ ~get:Parameters.AllocReturnsNull.get
+ ~set:Parameters.AllocReturnsNull.set
+ ~add_hook:Parameters.AllocReturnsNull.add_hook_on_update ()
+
+let _ =
+ S.register_state ~package
+ ~name:"WarnPointerComparison"
+ ~descr:(Md.plain "Warn pointer comparison value")
+ ~data:(module D.Jstring)
+ ~get:Parameters.WarnPointerComparison.get
+ ~set:Parameters.WarnPointerComparison.set
+ ~add_hook:Parameters.WarnPointerComparison.add_hook_on_update ()
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index 26f6d68592e322fd5f9d67c3dd244ef7974abb63..abc4d534b12a5aab1ed20b7a300fcf0a5b0d8ca3 100644
--- a/src/plugins/eva/parameters.mli
+++ b/src/plugins/eva/parameters.mli
@@ -86,6 +86,8 @@ module SplitLimit : Parameter_sig.Int
module InterproceduralSplits : Parameter_sig.Bool
module InterproceduralHistory : Parameter_sig.Bool
+module ILevel: Parameter_sig.Int
+
module ArrayPrecisionLevel: Parameter_sig.Int
module AllocatedContextValid: Parameter_sig.Bool
@@ -116,6 +118,8 @@ module BuiltinsOverrides:
and type value = string
module BuiltinsAuto: Parameter_sig.Bool
module BuiltinsList: Parameter_sig.Bool
+
+module SplitReturn: Parameter_sig.String
module SplitReturnFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = Split_strategy.t