From 009a61dce90b0ea722e9fce29cf7ce4c1e4af87b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 25 Apr 2023 13:47:13 +0200
Subject: [PATCH] [Ivette] Fixes EvaRead panel on aborted Eva analyses.
---
.../frama-c/plugins/eva/EvaReady/index.tsx | 26 +++++++++++++++++++
.../frama-c/plugins/eva/EvaReady/style.css | 2 +-
.../frama-c/plugins/eva/api/general/index.ts | 6 +++--
src/plugins/eva/api/general_requests.ml | 3 ++-
4 files changed, 33 insertions(+), 4 deletions(-)
diff --git a/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx b/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx
index 4fb100582df..4672816c59e 100644
--- a/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/EvaReady/index.tsx
@@ -21,15 +21,20 @@
/* ************************************************************************ */
import React 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';
+const ackAbortedState = new GlobalState(false);
+
const EvaReady: React.FC = ({ children }) => {
const state = States.useSyncValue(Eva.computationState);
+ const [ackAborted, setAckAborted] = useGlobalState(ackAbortedState);
switch (state) {
case undefined:
@@ -55,6 +60,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 fc2ae05a94d..35dd64ddfaa 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 {
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 18e0bc29ab4..78ef1d0ddc1 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 cd68e1dc386..6240f5be74f 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"
--
GitLab