diff --git a/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx b/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx index 4fb100582df9c95189cce8da59454bbcd57ec0bc..c35354ba7231bae8bc70ce5dbbdc810cd72748e7 100644 --- a/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx +++ b/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx @@ -20,16 +20,40 @@ /* */ /* ************************************************************************ */ -import React from 'react'; +import React, { useEffect } from 'react'; +import { GlobalState, useGlobalState } from 'dome/data/states'; import * as States from 'frama-c/states'; +import { Button } from 'dome/controls/buttons'; import * as Eva from 'frama-c/plugins/eva/api/general'; import Gallery from 'dome/controls/gallery.json'; import gearsIcon from '../images/gears.svg'; import './style.css'; +import { onSignal } from 'frama-c/server'; + +class AckAbortedState extends GlobalState<boolean> { + #signalHookSet = false; + + constructor(initValue: boolean) { + super(initValue); + } + + setupSignalHooks(): void { + if (!this.#signalHookSet) { + onSignal(Eva.signalComputationState, + () => ackAbortedState.setValue(false)); + this.#signalHookSet = true; + } + } +} + +const ackAbortedState = new AckAbortedState(false); const EvaReady: React.FC = ({ children }) => { const state = States.useSyncValue(Eva.computationState); + const [ackAborted, setAckAborted] = useGlobalState(ackAbortedState); + + useEffect(() => ackAbortedState.setupSignalHooks()); switch (state) { case undefined: @@ -55,6 +79,27 @@ const EvaReady: React.FC = ({ children }) => { case 'computed': return <>{children}</>; + + case 'aborted': + if (ackAborted) { + return <>{children}</>; + } + else { + return ( + <div className="eva-status"> + <span> + The Eva analysis has been prematurely aborted by an internal error + or a user interruption: + the displayed results will be incomplete. + </span> + <Button + label="Ok" + style={{ width: "2cm" }} + onClick={() => setAckAborted(true)} + /> + </div> + ); + } } }; diff --git a/ivette/src/frama-c/plugins/eva/EvaReady/style.css b/ivette/src/frama-c/plugins/eva/EvaReady/style.css index fc2ae05a94d573ef039370d715a8d8f42a602ee9..6a68bead536b05aed50bd41f595f50aac2750057 100644 --- a/ivette/src/frama-c/plugins/eva/EvaReady/style.css +++ b/ivette/src/frama-c/plugins/eva/EvaReady/style.css @@ -3,7 +3,7 @@ flex-direction: column; gap: 20px; align-items: center; - margin:auto; + margin:10%; } .eva-status-icon { @@ -17,6 +17,10 @@ text-align: center; } +.eva-status button { + margin: auto; +} + .eva-status-computing { font-weight: bold; } 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 18e0bc29ab498a0ad6855da61bf86fff71305bc2..78ef1d0ddc13bb81fa4dc58927e653b717682a6a 100644 --- a/ivette/src/frama-c/plugins/eva/api/general/index.ts +++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts @@ -63,14 +63,16 @@ import { tag } from 'frama-c/kernel/api/data'; import { tagDefault } from 'frama-c/kernel/api/data'; /** State of the computation of Eva Analysis. */ -export type computationStateType = "not_computed" | "computing" | "computed"; +export type computationStateType = + "not_computed" | "computing" | "computed" | "aborted"; /** Decoder for `computationStateType` */ export const jComputationStateType: Json.Decoder<computationStateType> = - Json.jUnion<"not_computed" | "computing" | "computed">( + Json.jUnion<"not_computed" | "computing" | "computed" | "aborted">( Json.jTag("not_computed"), Json.jTag("computing"), Json.jTag("computed"), + Json.jTag("aborted"), ); /** Natural order for `computationStateType` */ diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml index cd68e1dc38623cdf42d756b002feeab6d2a1f8ba..6240f5be74f85e4b219665ce67416ec47d6f4e80 100644 --- a/src/plugins/eva/api/general_requests.ml +++ b/src/plugins/eva/api/general_requests.ml @@ -39,7 +39,8 @@ module ComputationState = struct Package.(Junion [ Jtag "not_computed" ; Jtag "computing" ; - Jtag "computed"]) + Jtag "computed" ; + Jtag "aborted" ]) let to_json = function | Analysis.NotComputed -> `String "not_computed" | Computing -> `String "computing"